{-# 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
Description : Type declarations for the HKD structure.
Copyright   : (c) Tom Harding, 2019
License     : MIT
Maintainer  : tom.harding@habito.com
Stability   : experimental
-}
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)

-- | Higher-kinded data (HKD) is the design pattern in which every field in our
-- type is wrapped in some functor @f@:
--
-- @
--   data User f
--    = User
--        { name :: f String
--        , age  :: f Int
--        }
-- @
--
-- Depending on the functor, we can get different behaviours: with 'Maybe', we
-- get a partial structure; with 'Validation', we get a piecemeal validator;
-- and so on. The @HKD@ newtype allows us to lift any type into an HKD-style
-- API via its generic representation.
--
-- >>> :set -XDeriveGeneric -XTypeApplications
-- >>> :{
-- data User
--   = User { name :: String, age :: Int }
--   deriving Generic
-- :}
--
-- The @HKD@ type is indexed by our choice of functor and the structure we're
-- lifting. In other words, we can define a synonym for our behaviour:
--
-- >>> import Data.Monoid (Last (..))
-- >>> type Partial a = HKD a Last
--
-- ... and then we're ready to go!
--
-- >>> mempty @(Partial User)
-- User {name = Last {getLast = Nothing}, age = Last {getLast = Nothing}}
--
-- >>> mempty @(HKD (Int, Bool) [])
-- (,) [] []
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

-------------------------------------------------------------------------------

-- | Calculate the "partial representation" of a type.
type HKD_ (f :: Type -> Type) (structure :: Type)
  = GHKD_ f (Rep structure)

-- | Calculate the "partial representation" of a generic rep.
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

-------------------------------------------------------------------------------

-- | Often, we can get instances by using an 'HKD' type's isomorphism with a
-- certain size of tuple. This class witnesses the isomorphism with a certain
-- tuple (specifically a nested tree of pairs) to allow us to derive "via"
-- these shapes.
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)