{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Barbie.Internal.Constraints
( ConstraintsB(..)
, AllBF
, CanDeriveConstraintsB
, GAllBC(..)
, GAllBRep, X
, TagSelf, Self, Other
, GConstraintsB(..)
, gbaddDictsDefault
, adjProof
, ConstraintsOf
)
where
import Data.Barbie.Internal.Dicts(ClassF, Dict(..))
import Data.Barbie.Internal.Functor(FunctorB(..))
import Data.Functor.Product(Product(..))
import Data.Kind(Constraint)
import Data.Generics.GenericN
class FunctorB b => ConstraintsB b where
type AllB (c :: * -> Constraint) b :: Constraint
type AllB c b = GAllB c (GAllBRep b)
baddDicts :: forall c f. AllB c b => b f -> b (Dict c `Product` f)
default baddDicts
:: forall c f
. ( CanDeriveConstraintsB c b f
, AllB c b
)
=> b f -> b (Dict c `Product` f)
baddDicts = gbaddDictsDefault
type AllBF c f b = AllB (ClassF c f) b
{-# DEPRECATED ConstraintsOf "Renamed to AllBF (now based on AllB)" #-}
type ConstraintsOf c f b = AllBF c f b
{-# DEPRECATED adjProof "Renamed to baddDicts" #-}
adjProof
:: forall b c f. (ConstraintsB b, AllB c b) => b f -> b (Dict c `Product` f)
adjProof = baddDicts
type GAllBRep b = TagSelf b (RepN (b X))
data X a
type CanDeriveConstraintsB c b f
= ( GenericN (b f)
, GenericN (b (Dict c `Product` f))
, AllB c b ~ GAllB c (GAllBRep b)
, GConstraintsB c f (GAllBRep b) (RepN (b f)) (RepN (b (Dict c `Product` f)))
)
gbaddDictsDefault
:: forall b c f
. ( CanDeriveConstraintsB c b f
, AllB c b
)
=> b f -> b (Dict c `Product` f)
gbaddDictsDefault
= toN . gbaddDicts @c @f @(GAllBRep b) . fromN
{-# INLINE gbaddDictsDefault #-}
class GAllBC (repbf :: * -> *) where
type GAllB (c :: * -> Constraint) repbf :: Constraint
class GAllBC repbx => GConstraintsB c (f :: * -> *) repbx repbf repbdf where
gbaddDicts :: GAllB c repbx => repbf x -> repbdf x
instance GAllBC repbf => GAllBC (M1 i k repbf) where
type GAllB c (M1 i k repbf) = GAllB c repbf
instance
GConstraintsB c f repbx repbf repbdf
=> GConstraintsB c f (M1 i k repbx)
(M1 i k repbf)
(M1 i k repbdf) where
gbaddDicts = M1 . gbaddDicts @c @f @repbx . unM1
{-# INLINE gbaddDicts #-}
instance GAllBC V1 where
type GAllB c V1 = ()
instance GConstraintsB c f V1 V1 V1 where
gbaddDicts _ = undefined
instance GAllBC U1 where
type GAllB c U1 = ()
instance GConstraintsB c f U1 U1 U1 where
gbaddDicts = id
{-# INLINE gbaddDicts #-}
instance (GAllBC l, GAllBC r) => GAllBC (l :*: r) where
type GAllB c (l :*: r) = (GAllB c l, GAllB c r)
instance
( GConstraintsB c f lx lf ldf
, GConstraintsB c f rx rf rdf
) => GConstraintsB c f (lx :*: rx)
(lf :*: rf)
(ldf :*: rdf) where
gbaddDicts (l :*: r)
= (gbaddDicts @c @f @lx l) :*: (gbaddDicts @c @f @rx r)
{-# INLINE gbaddDicts #-}
instance (GAllBC l, GAllBC r) => GAllBC (l :+: r) where
type GAllB c (l :+: r) = (GAllB c l, GAllB c r)
instance
( GConstraintsB c f lx lf ldf
, GConstraintsB c f rx rf rdf
) => GConstraintsB c f (lx :+: rx)
(lf :+: rf)
(ldf :+: rdf) where
gbaddDicts = \case
L1 l -> L1 (gbaddDicts @c @f @lx l)
R1 r -> R1 (gbaddDicts @c @f @rx r)
{-# INLINE gbaddDicts #-}
type P0 = Param 0
instance GAllBC (Rec (P0 X a) (X a)) where
type GAllB c (Rec (P0 X a) (X a)) = c a
instance GConstraintsB c f (Rec (P0 X a) (X a))
(Rec (P0 f a) (f a))
(Rec (P0 (Dict c `Product` f) a)
((Dict c `Product` f) a)) where
gbaddDicts
= Rec . K1 . Pair Dict . unK1 . unRec
{-# INLINE gbaddDicts #-}
instance GAllBC (Rec (Self b (P0 X)) (b X)) where
type GAllB c (Rec (Self b (P0 X)) (b X)) = ()
instance
( ConstraintsB b
, AllB c b
) => GConstraintsB c f (Rec (Self b (P0 X)) (b X))
(Rec (b (P0 f)) (b f))
(Rec (b (P0 (Dict c `Product` f)))
(b (Dict c `Product` f))) where
gbaddDicts
= Rec . K1 . baddDicts . unK1 . unRec
{-# INLINE gbaddDicts #-}
instance
( ConstraintsB b'
, SameOrParam b b'
) => GAllBC (Rec (Other b (P0 X)) (b' X)) where
type GAllB c (Rec (Other b (P0 X)) (b' X)) = AllB c b'
instance
( SameOrParam b b'
, ConstraintsB b'
, AllB c b'
) => GConstraintsB c f (Rec (Other b (P0 X)) (b' X))
(Rec (b (P0 f)) (b' f))
(Rec (b (P0 (Dict c `Product` f)))
(b' (Dict c `Product` f))) where
gbaddDicts
= Rec . K1 . baddDicts . unK1 . unRec
{-# INLINE gbaddDicts #-}
instance GAllBC (Rec a a) where
type GAllB c (Rec a a) = ()
instance GConstraintsB c f (Rec a a)
(Rec a a)
(Rec a a) where
gbaddDicts = id
{-# INLINE gbaddDicts #-}
data Self (b :: (* -> *) -> *) (f :: * -> *)
data Other (b :: (* -> *) -> *) (f :: * -> *)
type family TagSelf (b :: (* -> *) -> *) (repbf :: * -> *) :: * -> * where
TagSelf b (M1 mt m s)
= M1 mt m (TagSelf b s)
TagSelf b (l :+: r)
= TagSelf b l :+: TagSelf b r
TagSelf b (l :*: r)
= TagSelf b l :*: TagSelf b r
TagSelf b (Rec (b f) (b g))
= Rec (Self b f) (b g)
TagSelf b (Rec (b' f) (b'' (g :: * -> *)))
= Rec (Other b' f) (b'' g)
TagSelf b (Rec p a)
= Rec p a
TagSelf b U1
= U1
TagSelf b V1
= V1