{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Barbie.Internal.ProofB
( ProofB(..)
, CanDeriveGenericInstance, ConstraintsOfMatchesGenericDeriv
, GConstraintsOf
, GProof
, gbproofDefault
)
where
import Data.Barbie.Internal.Classification (BarbieType(..), ClassifyBarbie)
import Data.Barbie.Internal.Dicts(DictOf(..), packDict)
import Data.Barbie.Internal.Generics
import Data.Barbie.Internal.Constraints hiding (CanDeriveGenericInstance, ConstraintsOfMatchesGenericDeriv)
import Data.Barbie.Internal.Product(ProductB(..))
import Data.Barbie.Internal.Tags(P, F)
import Data.Barbie.Internal.Wear(Wear)
import Data.Proxy
import GHC.Generics
class (ConstraintsB b, ProductB b) => ProofB b where
bproof :: ConstraintsOf c f b => b (DictOf c f)
default bproof
:: ( CanDeriveGenericInstance b
, ConstraintsOfMatchesGenericDeriv c f b
, ConstraintsOf c f b
)
=> b (DictOf c f)
bproof = gbproofDefault
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)))
)
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)))
)
gbproofDefault
:: forall b c f
. ( CanDeriveGenericInstance b
, ConstraintsOfMatchesGenericDeriv c f b
, ConstraintsOf c f b
)
=> b (DictOf c f)
gbproofDefault
= unsafeUntargetBarbie @P $ to $ gbproof pcbf pbt pb
where
pcbf = Proxy :: Proxy (c (b f))
pbt = Proxy :: Proxy (ClassifyBarbie b)
pb = Proxy :: Proxy (RecRep (b (Target F)) x)
class GProof (bt :: BarbieType) b rep where
gbproof
:: ( ConstraintByType bt c f rep
, GConstraintsOf c f (RecRep (b (Target F)))
)
=> Proxy (c (b f))
-> Proxy bt
-> Proxy (rep x)
-> Repl' (Target F) (Target P) rep x
instance GProof bt b x => GProof bt b (M1 _i _c x) where
{-# INLINE gbproof #-}
gbproof pcbf pbt pm1
= M1 (gbproof pcbf pbt (unM1 <$> pm1))
instance GProof bt b U1 where
{-# INLINE gbproof #-}
gbproof _ _ _ = U1
instance (GProof bt b l, GProof bt b r) => GProof bt b (l :*: r) where
{-# INLINE gbproof #-}
gbproof pcbf pbt pp
=
gbproof pcbf pbt (left <$> pp) :*: gbproof pcbf pbt (right <$> pp)
where
left (l :*: _) = l
right (_ :*: r) = r
instance {-# OVERLAPPING #-} GProof 'WearBarbie b (K1 R (NonRec (Target (W F) a))) where
{-# INLINE gbproof #-}
gbproof pcbf _ _
= K1 $ unsafeTarget @(W P) (mkProof pcbf)
where
mkProof :: (c (f a), Wear f a ~ f a) => Proxy (c (b f)) -> DictOf c f a
mkProof _ = packDict
instance {-# OVERLAPPING #-} GProof 'NonWearBarbie b (K1 R (NonRec (Target F a))) where
{-# INLINE gbproof #-}
gbproof pcbf _ _
= K1 $ unsafeTarget @P (mkProof pcbf)
where
mkProof :: c (f a) => Proxy (c (b f)) -> DictOf c f a
mkProof _ = packDict
instance {-# OVERLAPPING #-}
( CanDeriveGenericInstance b
, bt ~ ClassifyBarbie b
)
=> GProof bt b (K1 R (RecUsage (b (Target F)))) where
{-# INLINE gbproof #-}
gbproof pcbf pbt _
= K1 $ to $ gbproof pcbf pbt pr
where
pr = Proxy :: Proxy (RecRep (b (Target F)) x)
instance {-# OVERLAPPING #-}
ProofB b' => GProof bt b (K1 R (NonRec (b' (Target F)))) where
{-# INLINE gbproof #-}
gbproof pcbf _ _
= K1 $ unsafeTargetBarbie @P (proof' pcbf)
where
proof' :: ConstraintsOf c f b' => Proxy (c (b f)) -> b' (DictOf c f)
proof' _ = bproof