Safe Haskell	None
Language	Haskell2010

Data.Barbie.Internal.ProofB

Synopsis

Documentation

class (ConstraintsB b, ProductB b) => ProofB b where Source #

Barbie-types with products have a canonical proof of instance.

There is a default bproof implementation for Generic types, so instances can derived automatically.

Methods

bproof :: ConstraintsOf c f b => b (DictOf c f) Source #

bproof :: (CanDeriveGenericInstance b, ConstraintsOfMatchesGenericDeriv c f b, ConstraintsOf c f b) => b (DictOf c f) Source #

Instances

ProofB b => ProofB (Barbie b) Source #
Methods bproof :: ConstraintsOf c f (Barbie b) => Barbie b (DictOf c f) Source #

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

Every type that admits a generic instance of ProductB and ConstraintsB, has a generic instance of ProofB as well.

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 #

class GProof (bt :: BarbieType) b rep Source #

Minimal complete definition

gbproof

Instances

GProof bt b (U1 *) Source #
Methods gbproof :: (ConstraintByType bt c f (U1 ), GConstraintsOf c f (RecRep (b (Target F)))) => Proxy Constraint (c (b f)) -> Proxy BarbieType bt -> Proxy (U1 * x) -> Repl' (Target F) (Target P) (U1 *) x
(GProof bt b l, GProof bt b r) => GProof bt b ((::) l r) Source #
Methods gbproof :: (ConstraintByType bt c f ((* :: l) r), GConstraintsOf c f (RecRep (b (Target F)))) => Proxy Constraint (c (b f)) -> Proxy BarbieType bt -> Proxy ((* :: l) r x) -> Repl' (Target F) (Target P) (( :*: l) r) x
GProof bt b x => GProof bt b (M1 * _i _c x) Source #
Methods gbproof :: (ConstraintByType bt c f (M1 * _i _c x), GConstraintsOf c f (RecRep (b (Target F)))) => Proxy Constraint (c (b f)) -> Proxy BarbieType bt -> Proxy * (M1 * _i _c x x) -> Repl' (Target F) (Target P) (M1 * _i _c x) x

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

Default implementation of bproof based on Generic.