Safe Haskell | None |
---|---|

Language | Haskell2010 |

- class FunctorB b => ConstraintsB b where
- type ConstraintsOf (c :: * -> Constraint) (f :: * -> *) b :: Constraint

- type CanDeriveGenericInstance b = (Generic (b (Target F)), Generic (b (Target PxF)), GAdjProof (ClassifyBarbie b) b (RecRep (b (Target F))), Rep (b (Target PxF)) ~ Repl' (Target F) (Target PxF) (RecRep (b (Target F))))
- type ConstraintsOfMatchesGenericDeriv c f b = (ConstraintsOf c f b ~ GConstraintsOf c f (RecRep (b (Target F))), ConstraintsOf c f b ~ ConstraintByType (ClassifyBarbie b) c f (RecRep (b (Target F))))
- type GConstraintsOf c f r = ConstraintByType (GClassifyBarbie r) c f r
- class GAdjProof (bt :: BarbieType) b rep
- gadjProofDefault :: forall b c f. (CanDeriveGenericInstance b, ConstraintsOfMatchesGenericDeriv c f b, ConstraintsOf c f b) => b f -> b (Product (DictOf c f) f)
- type family ConstraintByType bt (c :: * -> Constraint) (f :: * -> *) r :: Constraint where ...

# Documentation

class FunctorB b => ConstraintsB b where Source #

Instances of this class provide means to talk about constraints,
both at compile-time, using `ConstraintsOf`

and at run-time,
in the form of class instance dictionaries, via `adjProof`

.

A manual definition would look like this:

data T f = A (f`Int`

) (f`String`

) | B (f`Bool`

) (f`Int`

) instance`ConstraintsB`

T where type`ConstraintsOf`

c f T = (c (f`Int`

), c (f`String`

), c (f`Bool`

)) adjProof t = case t of A x y -> A (`Pair`

(`packDict`

x) (`packDict`

y)) B z w -> B (`Pair`

(`packDict`

z) (`packDict`

w))

There is a default implementation of `ConstraintsOf`

for
`Generic`

types, so in practice one will simply do:

derive instance`Generic`

T instance`ConstraintsB`

T

type ConstraintsOf (c :: * -> Constraint) (f :: * -> *) b :: Constraint Source #

should contain a constraint `ConstraintsOf`

c f b`c (f x)`

for each `f x`

occurring in `b`

. E.g.:

`ConstraintsOf`

`Show`

f Barbie = (`Show`

(f`String`

),`Show`

(f`Int`

))

adjProof :: forall c f. ConstraintsOf c f b => b f -> b (Product (DictOf c f) f) Source #

Adjoint a proof-of-instance to a barbie-type.

adjProof :: forall c f. (CanDeriveGenericInstance b, ConstraintsOfMatchesGenericDeriv c f b, ConstraintsOf c f b) => b f -> b (Product (DictOf c f) f) Source #

Adjoint a proof-of-instance to a barbie-type.

ConstraintsB b => ConstraintsB (Barbie b) Source # | |

type CanDeriveGenericInstance b = (Generic (b (Target F)), Generic (b (Target PxF)), GAdjProof (ClassifyBarbie b) b (RecRep (b (Target F))), Rep (b (Target PxF)) ~ Repl' (Target F) (Target PxF) (RecRep (b (Target F)))) Source #

Intuivively, the requirements to have

derived are:`ConstraintsB`

B

- There is an instance of

for every`Generic`

(B f)`f`

- If
`f`

is used as argument to some type in the definition of`B`

, it is only on a Barbie-type with a`ConstraintsB`

instance.

type ConstraintsOfMatchesGenericDeriv c f b = (ConstraintsOf c f b ~ GConstraintsOf c f (RecRep (b (Target F))), ConstraintsOf c f b ~ ConstraintByType (ClassifyBarbie b) c f (RecRep (b (Target F)))) Source #

type GConstraintsOf c f r = ConstraintByType (GClassifyBarbie r) c f r Source #

gadjProofDefault :: forall b c f. (CanDeriveGenericInstance b, ConstraintsOfMatchesGenericDeriv c f b, ConstraintsOf c f b) => b f -> b (Product (DictOf c f) f) Source #

type family ConstraintByType bt (c :: * -> Constraint) (f :: * -> *) r :: Constraint where ... Source #

ConstraintByType bt c f (M1 _i _c x) = ConstraintByType bt c f x | |

ConstraintByType bt c f V1 = () | |

ConstraintByType bt c f U1 = () | |

ConstraintByType bt c f (l :*: r) = (ConstraintByType bt c f l, ConstraintByType bt c f r) | |

ConstraintByType bt c f (l :+: r) = (ConstraintByType bt c f l, ConstraintByType bt c f r) | |

ConstraintByType WearBarbie c f (K1 R (NonRec (Target (W F) a))) = (c (Wear f a), Wear f a ~ f a) | |

ConstraintByType NonWearBarbie c f (K1 R (NonRec (Target F a))) = c (f a) | |

ConstraintByType bt c f (K1 R (NonRec (b (Target F)))) = ConstraintsOf c f b | |

ConstraintByType bt c f (K1 R (RecUsage (b (Target F)))) = () | |

ConstraintByType bt c f (K1 _i _c) = () |