Strongweak.Generic.Strengthen

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).

Documentation

strengthenGeneric :: (Generic w, Generic s, GStrengthenD (Rep w) (Rep s)) => w -> Result s

Strengthen a value generically.

The weak and strong types must be compatible. See Generic for the definition of compatibility in this context.

class GStrengthenD w s where

Generic strengthening at the datatype level.

Methods

gstrengthenD :: w p -> Result (s p)

Instances

GStrengthenC wcd scd w s => GStrengthenD (D1 wcd w :: k -> Type) (D1 scd s :: k -> Type)

Enter a datatype, stripping its metadata wrapper.

Defined in Strongweak.Generic.Strengthen

Methods

gstrengthenD :: forall (p :: k0). D1 wcd w p -> Result (D1 scd s p)

class GStrengthenC wcd scd w s where

Generic strengthening at the constructor sum level.

Methods

gstrengthenC :: w p -> Result (s p)

Instances

GStrengthenC (wcd :: k1) (scd :: k2) (V1 :: k3 -> Type) (V1 :: k3 -> Type)

Nothing to do for empty datatypes.

Defined in Strongweak.Generic.Strengthen

Methods

gstrengthenC :: forall (p :: k20). V1 p -> Result (V1 p)

(GStrengthenC wcd scd wl sl, GStrengthenC wcd scd wr sr) => GStrengthenC (wcd :: k1) (scd :: k2) (wl :+: wr :: k3 -> Type) (sl :+: sr :: k3 -> Type)

Strengthen sum types by casing and strengthening left or right.

Defined in Strongweak.Generic.Strengthen

Methods

gstrengthenC :: forall (p :: k20). (wl :+: wr) p -> Result ((sl :+: sr) p)

GStrengthenS wcd scd wcc scc 0 w s => GStrengthenC (wcd :: k1) (scd :: k2) (C1 wcc w :: k3 -> Type) (C1 scc s :: k3 -> Type)

Enter a constructor, stripping its metadata wrapper.

Defined in Strongweak.Generic.Strengthen

Methods

gstrengthenC :: forall (p :: k20). C1 wcc w p -> Result (C1 scc s p)

class GStrengthenS wcd scd wcc scc (si :: Natural) w s where

Generic strengthening at the constructor level.

Methods

gstrengthenS :: w p -> Result (s p)

Instances

GStrengthenS (wcd :: k1) (scd :: k2) (wcc :: k3) (scc :: k4) si (U1 :: k5 -> Type) (U1 :: k5 -> Type)

Nothing to do for empty constructors.

Defined in Strongweak.Generic.Strengthen

Methods

gstrengthenS :: forall (p :: k40). U1 p -> Result (U1 p)

(GStrengthenS wcd scd wcc scc si wl sl, GStrengthenS wcd scd wcc scc (si + ProdArity wl) wr sr) => GStrengthenS (wcd :: k1) (scd :: k2) (wcc :: k3) (scc :: k4) si (wl :*: wr :: Type -> Type) (sl :*: sr :: Type -> Type)

Strengthen product types by strengthening left and right.

Defined in Strongweak.Generic.Strengthen

Methods

gstrengthenS :: forall (p :: k40). (wl :*: wr) p -> Result ((sl :*: sr) p)

GStrengthenS (wcd :: k1) (scd :: k2) (wcc :: k3) (scc :: k4) si (S1 wcs (Rec0 a) :: k5 -> Type) (S1 scs (Rec0 a) :: k5 -> Type)

Special case: if source and target types are equal, copy the value through.

Defined in Strongweak.Generic.Strengthen

Methods

gstrengthenS :: forall (p :: k40). S1 wcs (Rec0 a) p -> Result (S1 scs (Rec0 a) p)

(Weak s ~ w, Strengthen s, Datatype wcd, Datatype scd, Constructor wcc, Constructor scc, Selector wcs, Selector scs, KnownNat si) => GStrengthenS (wcd :: k1) (scd :: k2) (wcc :: k3) (scc :: k4) si (S1 wcs (Rec0 w) :: k5 -> Type) (S1 scs (Rec0 s) :: k5 -> Type)

Strengthen a field using the existing Strengthen instance.

Defined in Strongweak.Generic.Strengthen

Methods

gstrengthenS :: forall (p :: k40). S1 wcs (Rec0 w) p -> Result (S1 scs (Rec0 s) p)

(.>) :: (a -> b) -> (b -> c) -> a -> c

selName'' :: forall s. Selector s => Maybe String

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.)

conName' :: forall c. Constructor c => String

conName without the value (only used as a proxy). Lets us push our undefineds into one place.

datatypeName' :: forall d. Datatype d => String

datatypeName without the value (only used as a proxy). Lets us push our undefineds into one place.

selName' :: forall s. Selector s => String

selName without the value (only used as a proxy). Lets us push our undefineds into one place.

type family ProdArity (f :: Type -> Type) :: Natural where ...

Equations

ProdArity (S1 c f) = 1

ProdArity (l :*: r) = ProdArity l + ProdArity r

natVal'' :: forall n. KnownNat n => Natural