{-# OPTIONS_HADDOCK not-home #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Generic.HKD.Types
( HKD (..)
, HKD_
, GHKD_
, Tuple (..)
) where
import Barbies (ConstraintsB (..), FunctorB (..), ApplicativeB (..), TraversableB (..))
import Barbies.Constraints (Dict (..))
import Data.Function (on)
import Data.Functor.Contravariant (Contravariant (..), phantom)
import Data.Functor.Product (Product (..))
import Data.Kind (Constraint, Type)
import Data.Proxy (Proxy (..))
import Data.Void (Void)
import GHC.Generics
import GHC.TypeLits (KnownSymbol, symbolVal)
import Test.QuickCheck.Arbitrary (Arbitrary (..), CoArbitrary (..))
import Test.QuickCheck.Function (Function (..), functionMap)
newtype HKD (structure :: Type) (f :: Type -> Type)
= HKD { forall structure (f :: * -> *).
HKD structure f -> HKD_ f structure Void
runHKD :: HKD_ f structure Void }
instance (Contravariant (HKD_ f structure), Functor (HKD_ f structure))
=> Generic (HKD structure f) where
type Rep (HKD structure f) = HKD_ f structure
from :: forall x. HKD structure f -> Rep (HKD structure f) x
from = forall (f :: * -> *) a b.
(Functor f, Contravariant f) =>
f a -> f b
phantom forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall structure (f :: * -> *).
HKD structure f -> HKD_ f structure Void
runHKD
to :: forall x. Rep (HKD structure f) x -> HKD structure f
to = forall structure (f :: * -> *).
HKD_ f structure Void -> HKD structure f
HKD forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b.
(Functor f, Contravariant f) =>
f a -> f b
phantom
type HKD_ (f :: Type -> Type) (structure :: Type)
= GHKD_ f (Rep structure)
type family GHKD_ (f :: Type -> Type) (rep :: Type -> Type)
= (output :: Type -> Type) | output -> f rep where
GHKD_ f (M1 index meta inner) = M1 index meta (GHKD_ f inner)
GHKD_ f (left :*: right) = GHKD_ f left :*: GHKD_ f right
GHKD_ f (K1 index value) = K1 index (f value)
GHKD_ f (left :+: right) = GHKD_ f left :+: GHKD_ f right
instance (Eq tuple, Generic xs, Tuple f xs tuple)
=> Eq (HKD xs f) where
== :: HKD xs f -> HKD xs f -> Bool
(==) = forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall (f :: * -> *) structure tuple.
Tuple f structure tuple =>
HKD structure f -> tuple
toTuple
instance (Ord tuple, Generic xs, Tuple f xs tuple)
=> Ord (HKD xs f) where
compare :: HKD xs f -> HKD xs f -> Ordering
compare = forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall (f :: * -> *) structure tuple.
Tuple f structure tuple =>
HKD structure f -> tuple
toTuple
instance (Semigroup tuple, Generic xs, Tuple f xs tuple)
=> Semigroup (HKD xs f) where
HKD xs f
x <> :: HKD xs f -> HKD xs f -> HKD xs f
<> HKD xs f
y = forall (f :: * -> *) structure tuple.
Tuple f structure tuple =>
tuple -> HKD structure f
fromTuple (forall (f :: * -> *) structure tuple.
Tuple f structure tuple =>
HKD structure f -> tuple
toTuple HKD xs f
x forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) structure tuple.
Tuple f structure tuple =>
HKD structure f -> tuple
toTuple HKD xs f
y)
instance (Monoid tuple, Generic xs, Tuple f xs tuple)
=> Monoid (HKD xs f) where
mempty :: HKD xs f
mempty = forall (f :: * -> *) structure tuple.
Tuple f structure tuple =>
tuple -> HKD structure f
fromTuple forall a. Monoid a => a
mempty
instance (Arbitrary tuple, GToTuple (HKD_ f structure) tuple)
=> Arbitrary (HKD structure f) where
arbitrary :: Gen (HKD structure f)
arbitrary = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall structure (f :: * -> *).
HKD_ f structure Void -> HKD structure f
HKD forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rep :: * -> *) tuple p.
GToTuple rep tuple =>
tuple -> rep p
gfromTuple) forall a. Arbitrary a => Gen a
arbitrary
instance (CoArbitrary tuple, GToTuple (HKD_ f structure) tuple)
=> CoArbitrary (HKD structure f) where
coarbitrary :: forall b. HKD structure f -> Gen b -> Gen b
coarbitrary (HKD HKD_ f structure Void
x) = forall a b. CoArbitrary a => a -> Gen b -> Gen b
coarbitrary (forall (rep :: * -> *) tuple p.
GToTuple rep tuple =>
rep p -> tuple
gtoTuple HKD_ f structure Void
x)
instance (Generic structure, Function tuple, Tuple f structure tuple)
=> Function (HKD structure f) where
function :: forall b. (HKD structure f -> b) -> HKD structure f :-> b
function = forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
functionMap forall (f :: * -> *) structure tuple.
Tuple f structure tuple =>
HKD structure f -> tuple
toTuple forall (f :: * -> *) structure tuple.
Tuple f structure tuple =>
tuple -> HKD structure f
fromTuple
class GShow (named :: Bool) (rep :: Type -> Type) where
gshow :: rep p -> String
instance GShow named inner => GShow named (D1 meta inner) where
gshow :: forall p. D1 meta inner p -> String
gshow = forall (named :: Bool) (rep :: * -> *) p.
GShow named rep =>
rep p -> String
gshow @named forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1
instance (GShow 'True inner, KnownSymbol name)
=> GShow any (C1 ('MetaCons name fixity 'True) inner) where
gshow :: forall p. C1 ('MetaCons name fixity 'True) inner p -> String
gshow (M1 inner p
x) = forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
Proxy @name) forall a. Semigroup a => a -> a -> a
<> String
" {" forall a. Semigroup a => a -> a -> a
<> forall (named :: Bool) (rep :: * -> *) p.
GShow named rep =>
rep p -> String
gshow @'True inner p
x forall a. Semigroup a => a -> a -> a
<> String
"}"
instance (GShow 'False inner, KnownSymbol name)
=> GShow any (C1 ('MetaCons name fixity 'False) inner) where
gshow :: forall p. C1 ('MetaCons name fixity 'False) inner p -> String
gshow (M1 inner p
x) = forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
Proxy @name) forall a. Semigroup a => a -> a -> a
<> String
" " forall a. Semigroup a => a -> a -> a
<> forall (named :: Bool) (rep :: * -> *) p.
GShow named rep =>
rep p -> String
gshow @'False inner p
x
instance (GShow 'True left, GShow 'True right)
=> GShow 'True (left :*: right) where
gshow :: forall p. (:*:) left right p -> String
gshow (left p
left :*: right p
right) = forall (named :: Bool) (rep :: * -> *) p.
GShow named rep =>
rep p -> String
gshow @'True left p
left forall a. Semigroup a => a -> a -> a
<> String
", " forall a. Semigroup a => a -> a -> a
<> forall (named :: Bool) (rep :: * -> *) p.
GShow named rep =>
rep p -> String
gshow @'True right p
right
instance (GShow 'False left, GShow 'False right)
=> GShow 'False (left :*: right) where
gshow :: forall p. (:*:) left right p -> String
gshow (left p
left :*: right p
right) = forall (named :: Bool) (rep :: * -> *) p.
GShow named rep =>
rep p -> String
gshow @'False left p
left forall a. Semigroup a => a -> a -> a
<> String
" " forall a. Semigroup a => a -> a -> a
<> forall (named :: Bool) (rep :: * -> *) p.
GShow named rep =>
rep p -> String
gshow @'False right p
right
instance (GShow 'True inner, KnownSymbol field)
=> GShow 'True (S1 ('MetaSel ('Just field) i d c) inner) where
gshow :: forall p. S1 ('MetaSel ('Just field) i d c) inner p -> String
gshow (M1 inner p
inner) = forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
Proxy @field) forall a. Semigroup a => a -> a -> a
<> String
" = " forall a. Semigroup a => a -> a -> a
<> forall (named :: Bool) (rep :: * -> *) p.
GShow named rep =>
rep p -> String
gshow @'True inner p
inner
instance GShow 'False inner => GShow 'False (S1 meta inner) where
gshow :: forall p. S1 meta inner p -> String
gshow (M1 inner p
inner) = forall (named :: Bool) (rep :: * -> *) p.
GShow named rep =>
rep p -> String
gshow @'False inner p
inner
instance (Show (f inner)) => GShow named (K1 R (f inner)) where
gshow :: forall p. K1 R (f inner) p -> String
gshow (K1 f inner
x) = forall a. Show a => a -> String
show f inner
x
instance (Generic structure, GShow 'True (HKD_ f structure))
=> Show (HKD structure f) where
show :: HKD structure f -> String
show (HKD HKD_ f structure Void
x) = forall (named :: Bool) (rep :: * -> *) p.
GShow named rep =>
rep p -> String
gshow @'True HKD_ f structure Void
x
class Tuple (f :: Type -> Type) (structure :: Type) (tuple :: Type)
| f structure -> tuple where
toTuple :: HKD structure f -> tuple
fromTuple :: tuple -> HKD structure f
class GToTuple (rep :: Type -> Type) (tuple :: Type)
| rep -> tuple where
gfromTuple :: tuple -> rep p
gtoTuple :: rep p -> tuple
instance GToTuple inner tuple
=> GToTuple (M1 index meta inner) tuple where
gfromTuple :: forall p. tuple -> M1 index meta inner p
gfromTuple = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rep :: * -> *) tuple p.
GToTuple rep tuple =>
tuple -> rep p
gfromTuple
gtoTuple :: forall p. M1 index meta inner p -> tuple
gtoTuple = forall (rep :: * -> *) tuple p.
GToTuple rep tuple =>
rep p -> tuple
gtoTuple forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1
instance (GToTuple left left', GToTuple right right')
=> GToTuple (left :*: right) (left', right') where
gfromTuple :: forall p. (left', right') -> (:*:) left right p
gfromTuple (left'
x, right'
y) = forall (rep :: * -> *) tuple p.
GToTuple rep tuple =>
tuple -> rep p
gfromTuple left'
x forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall (rep :: * -> *) tuple p.
GToTuple rep tuple =>
tuple -> rep p
gfromTuple right'
y
gtoTuple :: forall p. (:*:) left right p -> (left', right')
gtoTuple (left p
x :*: right p
y) = (forall (rep :: * -> *) tuple p.
GToTuple rep tuple =>
rep p -> tuple
gtoTuple left p
x, forall (rep :: * -> *) tuple p.
GToTuple rep tuple =>
rep p -> tuple
gtoTuple right p
y)
instance GToTuple (K1 index inner) inner where
gfromTuple :: forall p. inner -> K1 index inner p
gfromTuple = forall k i c (p :: k). c -> K1 i c p
K1
gtoTuple :: forall p. K1 index inner p -> inner
gtoTuple = forall k i c (p :: k). K1 i c p -> c
unK1
instance (Generic structure, GToTuple (HKD_ f structure) tuple)
=> Tuple f structure tuple where
toTuple :: HKD structure f -> tuple
toTuple = forall (rep :: * -> *) tuple p.
GToTuple rep tuple =>
rep p -> tuple
gtoTuple forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall structure (f :: * -> *).
HKD structure f -> HKD_ f structure Void
runHKD
fromTuple :: tuple -> HKD structure f
fromTuple = forall structure (f :: * -> *).
HKD_ f structure Void -> HKD structure f
HKD forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rep :: * -> *) tuple p.
GToTuple rep tuple =>
tuple -> rep p
gfromTuple
class GFunctorB (rep :: Type -> Type) where
gbmap :: (forall a. f a -> g a) -> GHKD_ f rep p -> GHKD_ g rep p
instance GFunctorB inner => GFunctorB (M1 index meta inner) where
gbmap :: forall (f :: * -> *) (g :: * -> *) p.
(forall a. f a -> g a)
-> GHKD_ f (M1 index meta inner) p
-> GHKD_ g (M1 index meta inner) p
gbmap forall a. f a -> g a
f = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rep :: * -> *) (f :: * -> *) (g :: * -> *) p.
GFunctorB rep =>
(forall a. f a -> g a) -> GHKD_ f rep p -> GHKD_ g rep p
gbmap @inner forall a. f a -> g a
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1
instance (GFunctorB left, GFunctorB right)
=> GFunctorB (left :*: right) where
gbmap :: forall (f :: * -> *) (g :: * -> *) p.
(forall a. f a -> g a)
-> GHKD_ f (left :*: right) p -> GHKD_ g (left :*: right) p
gbmap forall a. f a -> g a
f (GHKD_ f left p
left :*: GHKD_ f right p
right) = forall (rep :: * -> *) (f :: * -> *) (g :: * -> *) p.
GFunctorB rep =>
(forall a. f a -> g a) -> GHKD_ f rep p -> GHKD_ g rep p
gbmap @left forall a. f a -> g a
f GHKD_ f left p
left forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall (rep :: * -> *) (f :: * -> *) (g :: * -> *) p.
GFunctorB rep =>
(forall a. f a -> g a) -> GHKD_ f rep p -> GHKD_ g rep p
gbmap @right forall a. f a -> g a
f GHKD_ f right p
right
instance GFunctorB (K1 index inner) where
gbmap :: forall (f :: * -> *) (g :: * -> *) p.
(forall a. f a -> g a)
-> GHKD_ f (K1 index inner) p -> GHKD_ g (K1 index inner) p
gbmap forall a. f a -> g a
f (K1 f inner
x) = forall k i c (p :: k). c -> K1 i c p
K1 (forall a. f a -> g a
f f inner
x)
instance GFunctorB (Rep structure) => FunctorB (HKD structure) where
bmap :: forall (f :: * -> *) (g :: * -> *).
(forall a. f a -> g a) -> HKD structure f -> HKD structure g
bmap forall a. f a -> g a
f = forall structure (f :: * -> *).
HKD_ f structure Void -> HKD structure f
HKD forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rep :: * -> *) (f :: * -> *) (g :: * -> *) p.
GFunctorB rep =>
(forall a. f a -> g a) -> GHKD_ f rep p -> GHKD_ g rep p
gbmap @(Rep structure) forall a. f a -> g a
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall structure (f :: * -> *).
HKD structure f -> HKD_ f structure Void
runHKD
class GTraversableB (rep :: Type -> Type) where
gbtraverse
:: Applicative t
=> (forall a. f a -> t (g a))
-> GHKD_ f rep p -> t (GHKD_ g rep p)
instance GTraversableB inner => GTraversableB (M1 index meta inner) where
gbtraverse :: forall (t :: * -> *) (f :: * -> *) (g :: * -> *) p.
Applicative t =>
(forall a. f a -> t (g a))
-> GHKD_ f (M1 index meta inner) p
-> t (GHKD_ g (M1 index meta inner) p)
gbtraverse forall a. f a -> t (g a)
f = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rep :: * -> *) (t :: * -> *) (f :: * -> *) (g :: * -> *) p.
(GTraversableB rep, Applicative t) =>
(forall a. f a -> t (g a)) -> GHKD_ f rep p -> t (GHKD_ g rep p)
gbtraverse @inner forall a. f a -> t (g a)
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1
instance (GTraversableB left, GTraversableB right)
=> GTraversableB (left :*: right) where
gbtraverse :: forall (t :: * -> *) (f :: * -> *) (g :: * -> *) p.
Applicative t =>
(forall a. f a -> t (g a))
-> GHKD_ f (left :*: right) p -> t (GHKD_ g (left :*: right) p)
gbtraverse forall a. f a -> t (g a)
f (GHKD_ f left p
left :*: GHKD_ f right p
right)
= forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
(:*:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (rep :: * -> *) (t :: * -> *) (f :: * -> *) (g :: * -> *) p.
(GTraversableB rep, Applicative t) =>
(forall a. f a -> t (g a)) -> GHKD_ f rep p -> t (GHKD_ g rep p)
gbtraverse @left forall a. f a -> t (g a)
f GHKD_ f left p
left
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (rep :: * -> *) (t :: * -> *) (f :: * -> *) (g :: * -> *) p.
(GTraversableB rep, Applicative t) =>
(forall a. f a -> t (g a)) -> GHKD_ f rep p -> t (GHKD_ g rep p)
gbtraverse @right forall a. f a -> t (g a)
f GHKD_ f right p
right
instance GTraversableB (K1 index inner) where
gbtraverse :: forall (t :: * -> *) (f :: * -> *) (g :: * -> *) p.
Applicative t =>
(forall a. f a -> t (g a))
-> GHKD_ f (K1 index inner) p -> t (GHKD_ g (K1 index inner) p)
gbtraverse forall a. f a -> t (g a)
f (K1 f inner
x) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k i c (p :: k). c -> K1 i c p
K1 (forall a. f a -> t (g a)
f f inner
x)
instance (FunctorB (HKD structure), GTraversableB (Rep structure))
=> TraversableB (HKD structure) where
btraverse :: forall (e :: * -> *) (f :: * -> *) (g :: * -> *).
Applicative e =>
(forall a. f a -> e (g a))
-> HKD structure f -> e (HKD structure g)
btraverse forall a. f a -> e (g a)
f = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall structure (f :: * -> *).
HKD_ f structure Void -> HKD structure f
HKD forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rep :: * -> *) (t :: * -> *) (f :: * -> *) (g :: * -> *) p.
(GTraversableB rep, Applicative t) =>
(forall a. f a -> t (g a)) -> GHKD_ f rep p -> t (GHKD_ g rep p)
gbtraverse @(Rep structure) forall a. f a -> e (g a)
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall structure (f :: * -> *).
HKD structure f -> HKD_ f structure Void
runHKD
class GApplicativeB (rep :: Type -> Type) where
gbprod :: GHKD_ f rep p -> GHKD_ g rep p -> GHKD_ (f `Product` g) rep p
gbpure :: (forall a. f a) -> GHKD_ f rep p
instance GApplicativeB inner => GApplicativeB (M1 index meta inner) where
gbprod :: forall (f :: * -> *) p (g :: * -> *).
GHKD_ f (M1 index meta inner) p
-> GHKD_ g (M1 index meta inner) p
-> GHKD_ (Product f g) (M1 index meta inner) p
gbprod (M1 GHKD_ f inner p
x) (M1 GHKD_ g inner p
y) = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (forall (rep :: * -> *) (f :: * -> *) p (g :: * -> *).
GApplicativeB rep =>
GHKD_ f rep p -> GHKD_ g rep p -> GHKD_ (Product f g) rep p
gbprod @inner GHKD_ f inner p
x GHKD_ g inner p
y)
gbpure :: forall (f :: * -> *) p.
(forall a. f a) -> GHKD_ f (M1 index meta inner) p
gbpure forall a. f a
zero = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (forall (rep :: * -> *) (f :: * -> *) p.
GApplicativeB rep =>
(forall a. f a) -> GHKD_ f rep p
gbpure @inner forall a. f a
zero)
instance (GApplicativeB left, GApplicativeB right)
=> GApplicativeB (left :*: right) where
gbprod :: forall (f :: * -> *) p (g :: * -> *).
GHKD_ f (left :*: right) p
-> GHKD_ g (left :*: right) p
-> GHKD_ (Product f g) (left :*: right) p
gbprod (GHKD_ f left p
leftX :*: GHKD_ f right p
rightX) (GHKD_ g left p
leftY :*: GHKD_ g right p
rightY)
= forall (rep :: * -> *) (f :: * -> *) p (g :: * -> *).
GApplicativeB rep =>
GHKD_ f rep p -> GHKD_ g rep p -> GHKD_ (Product f g) rep p
gbprod @left GHKD_ f left p
leftX GHKD_ g left p
leftY forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall (rep :: * -> *) (f :: * -> *) p (g :: * -> *).
GApplicativeB rep =>
GHKD_ f rep p -> GHKD_ g rep p -> GHKD_ (Product f g) rep p
gbprod @right GHKD_ f right p
rightX GHKD_ g right p
rightY
gbpure :: forall (f :: * -> *) p.
(forall a. f a) -> GHKD_ f (left :*: right) p
gbpure forall a. f a
zero
= forall (rep :: * -> *) (f :: * -> *) p.
GApplicativeB rep =>
(forall a. f a) -> GHKD_ f rep p
gbpure @left forall a. f a
zero forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall (rep :: * -> *) (f :: * -> *) p.
GApplicativeB rep =>
(forall a. f a) -> GHKD_ f rep p
gbpure @right forall a. f a
zero
instance GApplicativeB (K1 index inner) where
gbprod :: forall (f :: * -> *) p (g :: * -> *).
GHKD_ f (K1 index inner) p
-> GHKD_ g (K1 index inner) p
-> GHKD_ (Product f g) (K1 index inner) p
gbprod (K1 f inner
x) (K1 g inner
y) = forall k i c (p :: k). c -> K1 i c p
K1 (forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair f inner
x g inner
y)
gbpure :: forall (f :: * -> *) p.
(forall a. f a) -> GHKD_ f (K1 index inner) p
gbpure forall a. f a
zero = forall k i c (p :: k). c -> K1 i c p
K1 forall a. f a
zero
instance (FunctorB (HKD structure), GApplicativeB (Rep structure))
=> ApplicativeB (HKD structure) where
bprod :: forall (f :: * -> *) (g :: * -> *).
HKD structure f -> HKD structure g -> HKD structure (Product f g)
bprod (HKD HKD_ f structure Void
x) (HKD HKD_ g structure Void
y) = forall structure (f :: * -> *).
HKD_ f structure Void -> HKD structure f
HKD (forall (rep :: * -> *) (f :: * -> *) p (g :: * -> *).
GApplicativeB rep =>
GHKD_ f rep p -> GHKD_ g rep p -> GHKD_ (Product f g) rep p
gbprod @(Rep structure) HKD_ f structure Void
x HKD_ g structure Void
y)
bpure :: forall (f :: * -> *). (forall a. f a) -> HKD structure f
bpure forall a. f a
zero = forall structure (f :: * -> *).
HKD_ f structure Void -> HKD structure f
HKD (forall (rep :: * -> *) (f :: * -> *) p.
GApplicativeB rep =>
(forall a. f a) -> GHKD_ f rep p
gbpure @(Rep structure) forall a. f a
zero)
class GAllBC (rep :: Type -> Type) where
type GAllB (c :: Type -> Constraint) rep :: Constraint
class GConstraintsB (rep :: Type -> Type) where
gbaddDicts :: GAllB c rep => GHKD_ f rep p -> GHKD_ (Dict c `Product` f) rep p
instance GAllBC inner => GAllBC (M1 index meta inner) where
type GAllB c (M1 index meta inner) = GAllB c inner
instance GConstraintsB inner => GConstraintsB (M1 index meta inner) where
gbaddDicts :: forall (c :: * -> Constraint) (f :: * -> *) p.
GAllB c (M1 index meta inner) =>
GHKD_ f (M1 index meta inner) p
-> GHKD_ (Product (Dict c) f) (M1 index meta inner) p
gbaddDicts (M1 GHKD_ f inner p
x) = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (forall (rep :: * -> *) (c :: * -> Constraint) (f :: * -> *) p.
(GConstraintsB rep, GAllB c rep) =>
GHKD_ f rep p -> GHKD_ (Product (Dict c) f) rep p
gbaddDicts @inner GHKD_ f inner p
x)
instance (GAllBC left, GAllBC right) => GAllBC (left :*: right) where
type GAllB c (left :*: right) = (GAllB c left, GAllB c right)
instance (GConstraintsB left, GConstraintsB right)
=> GConstraintsB (left :*: right) where
gbaddDicts :: forall (c :: * -> Constraint) (f :: * -> *) p.
GAllB c (left :*: right) =>
GHKD_ f (left :*: right) p
-> GHKD_ (Product (Dict c) f) (left :*: right) p
gbaddDicts (GHKD_ f left p
left :*: GHKD_ f right p
right)
= forall (rep :: * -> *) (c :: * -> Constraint) (f :: * -> *) p.
(GConstraintsB rep, GAllB c rep) =>
GHKD_ f rep p -> GHKD_ (Product (Dict c) f) rep p
gbaddDicts @left GHKD_ f left p
left forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall (rep :: * -> *) (c :: * -> Constraint) (f :: * -> *) p.
(GConstraintsB rep, GAllB c rep) =>
GHKD_ f rep p -> GHKD_ (Product (Dict c) f) rep p
gbaddDicts @right GHKD_ f right p
right
instance GAllBC (K1 index inner) where
type GAllB c (K1 index inner) = c inner
instance GConstraintsB (K1 index inner) where
gbaddDicts :: forall (c :: * -> Constraint) (f :: * -> *) p.
GAllB c (K1 index inner) =>
GHKD_ f (K1 index inner) p
-> GHKD_ (Product (Dict c) f) (K1 index inner) p
gbaddDicts (K1 f inner
x) = forall k i c (p :: k). c -> K1 i c p
K1 (forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict f inner
x)
instance
( FunctorB (HKD structure)
, GConstraintsB (Rep structure)
, GAllBC (Rep structure)
)
=> ConstraintsB (HKD structure) where
type AllB c (HKD structure) = GAllB c (Rep structure)
baddDicts
:: forall c f
. AllB c (HKD structure)
=> HKD structure f
-> HKD structure (Dict c `Product` f)
baddDicts :: forall (c :: * -> Constraint) (f :: * -> *).
AllB c (HKD structure) =>
HKD structure f -> HKD structure (Product (Dict c) f)
baddDicts (HKD HKD_ f structure Void
x)
= forall structure (f :: * -> *).
HKD_ f structure Void -> HKD structure f
HKD (forall (rep :: * -> *) (c :: * -> Constraint) (f :: * -> *) p.
(GConstraintsB rep, GAllB c rep) =>
GHKD_ f rep p -> GHKD_ (Product (Dict c) f) rep p
gbaddDicts @(Rep structure) HKD_ f structure Void
x)