diff --git a/README.md b/README.md index ed6ff43..51d8236 100644 --- a/README.md +++ b/README.md @@ -100,7 +100,6 @@ handling receives special attention: * Failures do not short-circuit; if a strengthening is made up of multiple smaller strengthenings, all are run and any failures collated. - * Failures display the weak and strong (target) type. * Generic strengthening is scarily verbose: see below for details. ### One definition, strong + weak views diff --git a/TODO.md b/TODO.md index 23b1e04..609c9d2 100644 --- a/TODO.md +++ b/TODO.md @@ -2,36 +2,24 @@ * split into base definitions and orphan instances? * base needs either, acc, text and prettyprinter -## Failures: Combine it all into one constructor -Same as rerefined, no need to split. It means I have to make earlier decisions -on layout, but that's fine. +## Failures: Pretty refinement failures require exposing `Doc` early +rerefined refinement failures return an ADT, which is something. But we can't +embed that directly in a strengthen failure. We have to prettify to some degree. +But that will force us to perform all the indentation etc. upfront, which is +what we're trying to avoid (since it won't work properly). -## Failures: is Typeable really the right choice? -I probably went with `TypeRep`s for filling out failure detail due to copying -refined's design. With rerefined, I've gone back on that, and I now -don't use `Typeable` at all. That said, is it the right pick here? +Is this even sensible? When a strengthen failure indents, it has semantic +meaning: in this general failure, a more specific failure occurred. Using the +indent also for "in this specific failure, a refinement error occurred" seems +bad, somehow. -* The generics don't use it at all. -* Concrete instances could use an associated type family like `type Name = - "Word32"`. - * And strongweak largely deals in concrete instances. -* We can do the same type-level `Show` stuff that rerefined does. - * And we can embed `PredicateName` for `Refined[1]` instances. +We _could_ fix this by going back on our new design, and making a failure +constructor specifically for refinement failures. But that seems like a big code +smell. -The user will have to fill out a bunch of associated type families when using -strongweak, which sucks. Or maybe we can do a shitty job automatically for -generics? Like we can get the datatype name-- no other info, but that's a good -start lol. +Alternatively, we store `Doc`s instead of `Builder`s. Then we can layout in the +`Strengthen Refined` instance. But that seems wrong, too. -The `Show`ing feels a little weird too, but I think it's just that we get away -with it thanks to having lots of concrete instances. Non-concrete instances -would drop it. - -Hmm. Not too sure how `Refined` instances will look. How do we get a `Symbol` -from the `a` in `Refined p a`? We can say "it's some type refined with this -predicate", but we apparently can't tell you the type. - -Hold on, we went with type-level show for predicates because we were doing lots -of combination. We do no such thing here. Why don't we just write in the -`TypeRep`s ourselves? Easy for concrete, fine for `Refined`. Apparently not a -problem for decomposing instances either. +Orrrr I know it's stupid, but we could have a `prettyRefineFailure :: E -> +[TBL.Builder]`, where the indents are prepared for us. Then we can add our own +base indent on top. No issue. OK, I guess we stick with the current setup. diff --git a/flake.lock b/flake.lock index 9583750..6303231 100644 --- a/flake.lock +++ b/flake.lock @@ -64,11 +64,11 @@ "rerefined": { "flake": false, "locked": { - "lastModified": 1715132473, - "narHash": "sha256-bWG2A8DJhYQ6ocOheLnN7umauZwbIfAbqdQkSsIxto0=", + "lastModified": 1715428908, + "narHash": "sha256-sjG09y2Gr/HbkIob3bqk5+7QpbogqPLp3UV77vbOPDk=", "owner": "raehik", "repo": "rerefined", - "rev": "3b8ef08d78552df46c096166629ae0090acee9be", + "rev": "0c62d89c0a394fd26d85fe32241f6c246c315509", "type": "github" }, "original": { diff --git a/src/Strongweak/Generic.hs b/src/Strongweak/Generic.hs index 9c067b9..aa78497 100644 --- a/src/Strongweak/Generic.hs +++ b/src/Strongweak/Generic.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE UndecidableInstances #-} -- required due to nested constraints + -- | Generic 'strengthen' and 'weaken'. module Strongweak.Generic @@ -13,9 +15,13 @@ module Strongweak.Generic , GenericallySW(..) ) where -import Strongweak.Generic.Weaken -import Strongweak.Generic.Strengthen -import Strongweak.Generic.Via +import Strongweak.Weaken.Generic +import Strongweak.Strengthen.Generic + +import Strongweak.Weaken ( Weaken(Weak, weaken) ) +import Strongweak.Strengthen ( Strengthen(strengthen) ) +import GHC.Generics +import Data.Kind ( Type ) {- $generic-derivation-compatibility @@ -41,3 +47,44 @@ types: for the datatype, constructors and selectors. GHC will always add this metadata for you, but manually-derived Generic instances (which are usually a bad idea) do not require it. -} + +{- | @DerivingVia@ wrapper for strongweak instances. + +We can't use 'Generically' conveniently because we need to talk about two data +types, not one -- we would have to do something like @'Generically' ('Tagged' w +s)@, which is ugly. So we instead define our own adorable little "via type" +here! + +Use like so: + +@ +data XYZ (s :: Strength) = XYZ + { xyz1 :: SW s Word8 + , xyz2 :: Word8 + , xyz3 :: () + } deriving stock Generic +deriving via (GenericallySW (XYZ 'Strong) (XYZ 'Weak)) instance Weaken (XYZ 'Strong) +deriving via (GenericallySW (XYZ 'Strong) (XYZ 'Weak)) instance Strengthen (XYZ 'Strong) +@ + +TODO can't figure out a way around multiple standalone deriving declarations :( + +TODO maybe GenericallySW1? but even so instances differ between weaken and +strengthen (weaken needs nothing) so it's kinda better this way. :) +-} + +newtype GenericallySW s (w :: Type) = GenericallySW { unGenericallySW :: s } + +instance + ( Generic s, Generic w + , GWeaken (Rep s) (Rep w) + ) => Weaken (GenericallySW s w) where + type Weak (GenericallySW s w) = w + weaken = weakenGeneric . unGenericallySW + +instance + ( Generic s, Generic w + , GStrengthenD (Rep w) (Rep s) + , Weaken (GenericallySW s w) + ) => Strengthen (GenericallySW s w) where + strengthen = fmap GenericallySW . strengthenGeneric diff --git a/src/Strongweak/Generic/Strengthen.hs b/src/Strongweak/Generic/Strengthen.hs deleted file mode 100644 index b4391ff..0000000 --- a/src/Strongweak/Generic/Strengthen.hs +++ /dev/null @@ -1,166 +0,0 @@ -{- | 'strengthen' over generic representations. - -Strengthen failures are annotated with precise information describing where the -failure occurred: datatype name, constructor name, field index (and name if -present). To achieve this, we split the generic derivation into 3 classes, each -handling/"unwrapping" a different layer of the generic representation: datatype -(D), constructor (C) and selector (S). --} - --- both required due to type class design -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE UndecidableInstances #-} - -{-# LANGUAGE OverloadedStrings #-} -- errors - -module Strongweak.Generic.Strengthen where - -import Strongweak.Strengthen -import Data.Either.Validation -import GHC.Generics -import Data.Kind -import GHC.TypeNats -import Control.Applicative qualified as A -- liftA2 export workaround -import Strongweak.Util.TypeNats ( natVal'' ) -import Data.Text.Builder.Linear qualified as TBL -import GHC.Exts ( fromString ) - -{- TODO -So, now that we're improving the error story, we can do so here as well. - -At product level in these generics, we know that neither data type names or -constructor names (weak or strong) will change. So individual fields can simply -annotate themselves with the weak & strong field identifiers. Then those can get -wrapped into a nice clean error higher up, that says "this constructor had the -following errors". - -It's gonna look like the tuple and list 'Strengthen' instances but worse. Lots -of fiddly stuff. - -Also, we can do the data type equality check I noted earlier. If weak & strong -data type names/constructor names match, we're probably doing @SW@ tricks, and -could probably shorten the error a bit. --} - --- | Strengthen a value generically. --- --- The weak and strong types must be /compatible/. See 'Strongweak.Generic' for --- the definition of compatibility in this context. -strengthenGeneric - :: (Generic w, Generic s, GStrengthenD (Rep w) (Rep s)) - => w -> Result s -strengthenGeneric = fmap to . gstrengthenD . from - --- | Generic strengthening at the datatype level. -class GStrengthenD w s where - gstrengthenD :: w p -> Result (s p) - --- | Enter a datatype, stripping its metadata wrapper. -instance GStrengthenC wcd scd w s => GStrengthenD (D1 wcd w) (D1 scd s) where - gstrengthenD = fmap M1 . gstrengthenC @wcd @scd . unM1 - --- | Generic strengthening at the constructor sum level. -class GStrengthenC wcd scd w s where - gstrengthenC :: w p -> Result (s p) - --- | Nothing to do for empty datatypes. -instance GStrengthenC wcd scd V1 V1 where gstrengthenC = Success - --- | Strengthen sum types by casing and strengthening left or right. -instance - ( GStrengthenC wcd scd wl sl - , GStrengthenC wcd scd wr sr - ) => GStrengthenC wcd scd (wl :+: wr) (sl :+: sr) where - gstrengthenC = \case L1 l -> L1 <$> gstrengthenC @wcd @scd l - R1 r -> R1 <$> gstrengthenC @wcd @scd r - --- | Enter a constructor, stripping its metadata wrapper. -instance GStrengthenS wcd scd wcc scc 0 w s - => GStrengthenC wcd scd (C1 wcc w) (C1 scc s) where - gstrengthenC = fmap M1 . gstrengthenS @wcd @scd @wcc @scc @0 . unM1 - --- | Generic strengthening at the constructor level. -class GStrengthenS wcd scd wcc scc (si :: Natural) w s where - gstrengthenS :: w p -> Result (s p) - --- | Nothing to do for empty constructors. -instance GStrengthenS wcd scd wcc scc si U1 U1 where gstrengthenS = Success - --- | Strengthen product types by strengthening left and right. -instance - ( GStrengthenS wcd scd wcc scc si wl sl - , GStrengthenS wcd scd wcc scc (si + ProdArity wl) wr sr - ) => GStrengthenS wcd scd wcc scc si (wl :*: wr) (sl :*: sr) where - -- TODO ahhh this is gonna suck. - gstrengthenS (l :*: r) = - A.liftA2 (:*:) - (gstrengthenS @wcd @scd @wcc @scc @si l) - (gstrengthenS @wcd @scd @wcc @scc @(si + ProdArity wl) r) - --- | Special case: if source and target types are equal, copy the value through. -instance GStrengthenS wcd scd wcc scc si (S1 wcs (Rec0 a)) (S1 scs (Rec0 a)) where - gstrengthenS = Success . M1 . unM1 - --- | Strengthen a field using the existing 'Strengthen' instance. -instance {-# OVERLAPS #-} - ( Weak s ~ w -- has to be here, else "illegal typesym family app in instance" - , Strengthen s - , Datatype wcd, Datatype scd - , Constructor wcc, Constructor scc - , Selector wcs, Selector scs - , KnownNat si - ) => GStrengthenS wcd scd wcc scc si (S1 wcs (Rec0 w)) (S1 scs (Rec0 s)) where - gstrengthenS = unM1 .> unK1 .> strengthen .> \case - Success s -> Success $ M1 $ K1 s - Failure e -> failStrengthen [selQN] [(mempty, e)] - where - -- TODO only using weak!! should inspect, only shorten if identical - --e = FailField wcd scd wcc scc si wcs si scs es - selQN = fromString wcd<>"."<>fromString wcc<>"."<>sw - wcd = datatypeName' @wcd - scd = datatypeName' @scd - wcc = conName' @wcc - scc = conName' @scc - scs = selName'' @scs - -- TODO can't fromDec Naturals >:(( - sw = maybe (fromString (show (natVal'' @si))) fromString - (selName'' @wcs) - - --------------------------------------------------------------------------------- - --- from flow -(.>) :: (a -> b) -> (b -> c) -> a -> c -f .> g = g . f - --------------------------------------------------------------------------------- - --- | Get the record name for a selector if present. --- --- On the type level, a 'Maybe Symbol' is stored for record names. But the --- reification is done using @fromMaybe ""@. So we have to inspect the resulting --- string to determine whether the field uses record syntax or not. (Silly.) -selName'' :: forall s. Selector s => Maybe String -selName'' = case selName' @s of "" -> Nothing - s -> Just s - --- | 'conName' without the value (only used as a proxy). Lets us push our --- 'undefined's into one place. -conName' :: forall c. Constructor c => String -conName' = conName @c undefined - --- | 'datatypeName' without the value (only used as a proxy). Lets us push our --- 'undefined's into one place. -datatypeName' :: forall d. Datatype d => String -datatypeName' = datatypeName @d undefined - --- | 'selName' without the value (only used as a proxy). Lets us push our --- 'undefined's into one place. -selName' :: forall s. Selector s => String -selName' = selName @s undefined - --------------------------------------------------------------------------------- - -type family ProdArity (f :: Type -> Type) :: Natural where - ProdArity (S1 c f) = 1 - ProdArity (l :*: r) = ProdArity l + ProdArity r diff --git a/src/Strongweak/Generic/Via.hs b/src/Strongweak/Generic/Via.hs deleted file mode 100644 index 5d8caf7..0000000 --- a/src/Strongweak/Generic/Via.hs +++ /dev/null @@ -1,50 +0,0 @@ -{-# LANGUAGE UndecidableInstances #-} -- required due to nested constraints - -module Strongweak.Generic.Via where - -import Strongweak.Generic.Weaken -import Strongweak.Generic.Strengthen -import Strongweak -import GHC.Generics -import Data.Kind - -{- | @DerivingVia@ wrapper for strongweak instances. - -We can't use 'Generically' conveniently because we need to talk about two data -types, not one -- we would have to do something like @'Generically' ('Tagged' w -s)@, which is ugly. So we instead define our own adorable little "via type" -here! - -Use like so: - -@ -data XYZ (s :: Strength) = XYZ - { xyz1 :: SW s Word8 - , xyz2 :: Word8 - , xyz3 :: () - } deriving stock Generic -deriving via (GenericallySW (XYZ 'Strong) (XYZ 'Weak)) instance Weaken (XYZ 'Strong) -deriving via (GenericallySW (XYZ 'Strong) (XYZ 'Weak)) instance Strengthen (XYZ 'Strong) -@ - -TODO can't figure out a way around multiple standalone deriving declarations :( - -TODO maybe GenericallySW1? but even so instances differ between weaken and -strengthen (weaken needs nothing) so it's kinda better this way. :) --} - -newtype GenericallySW s (w :: Type) = GenericallySW { unGenericallySW :: s } - -instance - ( Generic s, Generic w - , GWeaken (Rep s) (Rep w) - ) => Weaken (GenericallySW s w) where - type Weak (GenericallySW s w) = w - weaken = weakenGeneric . unGenericallySW - -instance - ( Generic s, Generic w - , GStrengthenD (Rep w) (Rep s) - , Weaken (GenericallySW s w) - ) => Strengthen (GenericallySW s w) where - strengthen = fmap GenericallySW . strengthenGeneric diff --git a/src/Strongweak/Strengthen.hs b/src/Strongweak/Strengthen.hs index 31fde7c..2c0b4fd 100644 --- a/src/Strongweak/Strengthen.hs +++ b/src/Strongweak/Strengthen.hs @@ -77,9 +77,8 @@ data StrengthenFailure = StrengthenFailure { strengthenFailDetail :: [TBL.Builder] -- ^ Detail on strengthen failure. -- - -- We use a list here to keep us able to prettify. We could simply concatenate - -- each element with a newline, but pretty layouts might want to apply an - -- indent, so better handle it elsewhere. + -- We use a list here for the cases where you want multiple lines of detail. + -- Separating with a newline would make prettifying later harder, so we delay. , strengthenFailInner :: [(TBL.Builder, StrengthenFailure)] -- ^ Indexed. diff --git a/src/Strongweak/Strengthen/Generic.hs b/src/Strongweak/Strengthen/Generic.hs new file mode 100644 index 0000000..4c7a3b3 --- /dev/null +++ b/src/Strongweak/Strengthen/Generic.hs @@ -0,0 +1,213 @@ +{- | 'strengthen' over generic representations. + +As with base instances, generic strengthening collates all failures rather than +short-circuiting on the first failure. Failures are annotated with precise +information describing where the failure occurred: + + * data type name + * constructor name + * field index + * field name (if present) +-} + +-- required due to type class design +{-# LANGUAGE AllowAmbiguousTypes, UndecidableInstances #-} + +{-# LANGUAGE OverloadedStrings #-} -- required for failure + +module Strongweak.Strengthen.Generic where + +import Strongweak.Strengthen +import GHC.Generics +import Data.Either.Validation +import Data.Kind ( Type ) +import GHC.TypeNats ( Natural, type (+), KnownNat ) +import Control.Applicative qualified as A -- liftA2 export workaround +import Strongweak.Util.TypeNats ( natVal'' ) +import Data.Text.Builder.Linear qualified as TBL +import GHC.Exts ( Symbol, fromString, proxy# ) +import GHC.TypeLits ( KnownSymbol, symbolVal' ) + +{- TODO +So, now that we're improving the error story, we can do so here as well. + +At product level in these generics, we know that neither data type names or +constructor names (weak or strong) will change. So individual fields can simply +annotate themselves with the weak & strong field identifiers. Then those can get +wrapped into a nice clean error higher up, that says "this constructor had the +following errors". + +It's gonna look like the tuple and list 'Strengthen' instances but worse. Lots +of fiddly stuff. + +Also, we can do the data type equality check I noted earlier. If weak & strong +data type names/constructor names match, we're probably doing @SW@ tricks, and +could probably shorten the error a bit. +-} + +-- | Strengthen a value generically. +-- +-- The weak and strong types must be /compatible/. See 'Strongweak.Generic' for +-- the definition of compatibility in this context. +strengthenGeneric + :: (Generic w, Generic s, GStrengthenD (Rep w) (Rep s)) + => w -> Result s +strengthenGeneric = fmap to . gstrengthenD . from + +-- | Generic strengthening at the datatype level. +class GStrengthenD w s where + gstrengthenD :: w p -> Result (s p) + +-- | Strengthen a generic data type, replacing its metadata wrapping. +instance GStrengthenC wdn sdn w s + => GStrengthenD + (D1 (MetaData wdn _wmd2 _wmd3 _wmd4) w) + (D1 (MetaData sdn _smd2 _smd3 _smd4) s) where + gstrengthenD = fmap M1 . gstrengthenC @wdn @sdn . unM1 + +-- | Generic strengthening at the constructor sum level. +class GStrengthenC (wdn :: Symbol) (sdn :: Symbol) w s where + gstrengthenC :: w p -> Result (s p) + +-- | Nothing to do for empty datatypes. +instance GStrengthenC wdn sdn V1 V1 where gstrengthenC = Success + +-- | Strengthen sum types by casing and strengthening left or right. +instance + ( GStrengthenC wdn sdn wl sl + , GStrengthenC wdn sdn wr sr + ) => GStrengthenC wdn sdn (wl :+: wr) (sl :+: sr) where + gstrengthenC = \case L1 l -> L1 <$> gstrengthenC @wdn @sdn l + R1 r -> R1 <$> gstrengthenC @wdn @sdn r + +-- | Enter a constructor, stripping its metadata wrapper. +instance (GStrengthenS 0 w s, ReifyCstrs wcd wcn scd scn) + => GStrengthenC wcd scd + (C1 (MetaCons wcn _wmc2 _wmc3) w) + (C1 (MetaCons scn _smc2 _smc3) s) where + gstrengthenC (M1 w) = + case gstrengthenS @0 w of + Success s -> Success (M1 s) + Failure es -> failStrengthen [reifyCstrs @wcd @wcn @scd @scn] es + +class ReifyCstrs (ld :: Symbol) (lc :: Symbol) (rd :: Symbol) (rc :: Symbol) where + reifyCstrs :: TBL.Builder + +-- | Special case: data type and constructor names are equivalent: simplify +instance {-# OVERLAPPING #-} (KnownSymbol d, KnownSymbol c) + => ReifyCstrs d c d c where + {-# INLINE reifyCstrs #-} + reifyCstrs = d<>"."<>c + where + d = fromString (symbolVal' (proxy# @d)) + c = fromString (symbolVal' (proxy# @c)) + +instance (KnownSymbol ld, KnownSymbol lc, KnownSymbol rd, KnownSymbol rc) + => ReifyCstrs ld lc rd rc where + {-# INLINE reifyCstrs #-} + reifyCstrs = ld<>"."<>lc<>" -> "<>rd<>"."<>rc + where + ld = fromString (symbolVal' (proxy# @ld)) + lc = fromString (symbolVal' (proxy# @lc)) + rd = fromString (symbolVal' (proxy# @rd)) + rc = fromString (symbolVal' (proxy# @rc)) + +-- | Generic strengthening at the constructor level. +class GStrengthenS (i :: Natural) w s where + gstrengthenS :: w p -> Validation [(TBL.Builder, StrengthenFailure)] (s p) + +-- | Nothing to do for empty constructors. +instance GStrengthenS i U1 U1 where gstrengthenS = Success + +-- | Strengthen product types by strengthening left and right. +instance + ( GStrengthenS i wl sl + , GStrengthenS (i + ProdArity wl) wr sr + ) => GStrengthenS i (wl :*: wr) (sl :*: sr) where + gstrengthenS (l :*: r) = + A.liftA2 (:*:) + (gstrengthenS @i l) + (gstrengthenS @(i + ProdArity wl) r) + +-- | Special case: if source and target types are equivalent, just replace meta. +-- +-- Note that we have to expand the metadata awkwardly for the overlapping +-- instances to work correctly. (There should be a better way to write this, but +-- it's purely style, so light TODO.) +instance {-# OVERLAPPING #-} GStrengthenS i + (S1 (MetaSel _wms1 _wms2 _wms3 _wms4) (Rec0 a)) + (S1 (MetaSel _sms1 _sms2 _sms3 _sms4) (Rec0 a)) where + gstrengthenS = Success . M1 . unM1 + +-- | Strengthen a field using the existing 'Strengthen' instance. +instance + ( Weak s ~ w -- has to be here, else "illegal typesym family app in instance" + , Strengthen s + , ReifySelector i wmr smr + ) => GStrengthenS i + (S1 (MetaSel wmr _wms2 _wms3 _wms4) (Rec0 w)) + (S1 (MetaSel smr _sms2 _sms3 _sms4) (Rec0 s)) where + gstrengthenS = unM1 .> unK1 .> strengthen .> \case + Success s -> Success $ M1 $ K1 s + Failure e -> Failure [(reifySelector @i @wmr @smr, e)] + +{- TODO +* how to separate index and record name? @.@ is good and bad, uses same syntax + as @dt.cstr@ for different reason BUT is pretty clear +* how to lay out precisely? fairly arbitrary +-} +class ReifySelector (i :: Natural) (l :: Maybe Symbol) (r :: Maybe Symbol) where + reifySelector :: TBL.Builder + +-- | Special case: both types had a record name, and they're equal +instance {-# OVERLAPPING #-} (KnownNat i, KnownSymbol lnm) + => ReifySelector i (Just lnm) (Just lnm) where + -- TODO check overlap works correct + {-# INLINE reifySelector #-} + reifySelector = i<>"."<>lnm + where + i = fromString $ show $ natVal'' @i + lnm = fromString $ symbolVal' (proxy# @lnm) + +instance (KnownNat i, KnownSymbol lnm, KnownSymbol rnm) + => ReifySelector i (Just lnm) (Just rnm) where + {-# INLINE reifySelector #-} + reifySelector = i<>"."<>lnm<>" -> "<>rnm + where + i = fromString $ show $ natVal'' @i + lnm = fromString $ symbolVal' (proxy# @lnm) + rnm = fromString $ symbolVal' (proxy# @rnm) + +instance KnownNat i => ReifySelector i Nothing Nothing where + {-# INLINE reifySelector #-} + reifySelector = fromString $ show $ natVal'' @i + +instance (KnownNat i, KnownSymbol lnm) + => ReifySelector i (Just lnm) Nothing where + {-# INLINE reifySelector #-} + reifySelector = i<>"."<>lnm + where + i = fromString $ show $ natVal'' @i + lnm = fromString $ symbolVal' (proxy# @lnm) + +instance (KnownNat i, KnownSymbol rnm) + => ReifySelector i Nothing (Just rnm) where + {-# INLINE reifySelector #-} + reifySelector = i<>" -> "<>rnm + where + i = fromString $ show $ natVal'' @i + rnm = fromString $ symbolVal' (proxy# @rnm) + +-------------------------------------------------------------------------------- + +-- from flow +(.>) :: (a -> b) -> (b -> c) -> a -> c +f .> g = g . f + +-------------------------------------------------------------------------------- + +-- could define this with @Generic.Type.Function.FoldMap.GTFoldMapC (+) 0 _@... +-- but pretty dumb LOL +type family ProdArity (f :: k -> Type) :: Natural where + ProdArity (S1 c f) = 1 + ProdArity (l :*: r) = ProdArity l + ProdArity r diff --git a/src/Strongweak/Strengthen/Unsafe.hs b/src/Strongweak/Strengthen/Unsafe.hs index e15a2d4..5563c5e 100644 --- a/src/Strongweak/Strengthen/Unsafe.hs +++ b/src/Strongweak/Strengthen/Unsafe.hs @@ -3,7 +3,7 @@ module Strongweak.Strengthen.Unsafe where import Strongweak.Weaken import Data.Word import Data.Int -import Rerefined.Refine.Unsafe +import Rerefined.Refine import Data.Vector.Generic.Sized qualified as VGS -- Shazbot! import Data.Vector.Generic qualified as VG import Data.Vector.Generic.Sized.Internal qualified diff --git a/src/Strongweak/Generic/Weaken.hs b/src/Strongweak/Weaken/Generic.hs similarity index 88% rename from src/Strongweak/Generic/Weaken.hs rename to src/Strongweak/Weaken/Generic.hs index bdfd5d7..8917c69 100644 --- a/src/Strongweak/Generic/Weaken.hs +++ b/src/Strongweak/Weaken/Generic.hs @@ -1,9 +1,8 @@ -- | 'weaken' over generic representations. -module Strongweak.Generic.Weaken where +module Strongweak.Weaken.Generic where import Strongweak.Weaken - import GHC.Generics -- | Weaken a value generically. @@ -29,11 +28,11 @@ instance GWeaken U1 U1 where gweaken = id -- | Special case: if source and target types are equal, copy the value through. -instance GWeaken (Rec0 s) (Rec0 s) where +instance {-# OVERLAPPING #-} GWeaken (Rec0 s) (Rec0 s) where gweaken = id -- | Weaken a field using the existing 'Weaken' instance. -instance {-# OVERLAPS #-} (Weaken s, Weak s ~ w) => GWeaken (Rec0 s) (Rec0 w) where +instance (Weaken s, Weak s ~ w) => GWeaken (Rec0 s) (Rec0 w) where gweaken = K1 . weaken . unK1 -- | Weaken product types by weakening left and right. diff --git a/strongweak.cabal b/strongweak.cabal index 69018ab..c736842 100644 --- a/strongweak.cabal +++ b/strongweak.cabal @@ -30,15 +30,14 @@ library exposed-modules: Strongweak Strongweak.Generic - Strongweak.Generic.Strengthen - Strongweak.Generic.Via - Strongweak.Generic.Weaken Strongweak.Strengthen + Strongweak.Strengthen.Generic Strongweak.Strengthen.Unsafe Strongweak.Util.Text Strongweak.Util.Typeable Strongweak.Util.TypeNats Strongweak.Weaken + Strongweak.Weaken.Generic other-modules: Paths_strongweak hs-source-dirs: diff --git a/test/Strongweak/StrengthenSpec.hs b/test/Strongweak/StrengthenSpec.hs index cbaf6cd..bd705a4 100644 --- a/test/Strongweak/StrengthenSpec.hs +++ b/test/Strongweak/StrengthenSpec.hs @@ -1,4 +1,4 @@ -module Strongweak.StrengthenSpec ( spec ) where +module Strongweak.StrengthenSpec where -- ( spec ) where import Strongweak.Util.Typeable import Strongweak.Util.Text @@ -13,13 +13,18 @@ import Data.Word import Data.Foldable qualified as Foldable import Data.Typeable ( TypeRep ) +spec :: Spec +spec = undefined + +{- + spec :: Spec spec = do it "returns a precise error for failed generic strengthening (named field)" $ do let w = fromIntegral (maxBound @Word32) + 1 d = DP w 43 1 2 3 :: DP 'Weak e = sfGenericSW1Show - "DP" "DP" 0 (Just "dp1f0") + "DP.DP" "0.dp1f0" (typeRep' @Natural) (typeRep' @Word32) w strengthen @(DP 'Strong) d `shouldSatisfy` svEqFail e it "returns a precise error for failed generic strengthening (unnamed field)" $ do @@ -68,3 +73,5 @@ svEqFail e = \case case Foldable.toList es of [e'] -> sfEq e e' _ -> False + +-}