{-# OPTIONS_HADDOCK not-home #-}

{-# LANGUAGE AllowAmbiguousTypes    #-}
{-# LANGUAGE ConstraintKinds        #-}
{-# LANGUAGE DataKinds              #-}
{-# 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 { 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 :: HKD structure f -> Rep (HKD structure f) x
from = GHKD_ f (Rep structure) Void -> GHKD_ f (Rep structure) x
forall (f :: * -> *) a b.
(Functor f, Contravariant f) =>
f a -> f b
phantom (GHKD_ f (Rep structure) Void -> GHKD_ f (Rep structure) x)
-> (HKD structure f -> GHKD_ f (Rep structure) Void)
-> HKD structure f
-> GHKD_ f (Rep structure) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HKD structure f -> GHKD_ f (Rep structure) Void
forall structure (f :: * -> *).
HKD structure f -> HKD_ f structure Void
runHKD
  to :: Rep (HKD structure f) x -> HKD structure f
to   = GHKD_ f (Rep structure) Void -> HKD structure f
forall structure (f :: * -> *).
HKD_ f structure Void -> HKD structure f
HKD (GHKD_ f (Rep structure) Void -> HKD structure f)
-> (GHKD_ f (Rep structure) x -> GHKD_ f (Rep structure) Void)
-> GHKD_ f (Rep structure) x
-> HKD structure f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GHKD_ f (Rep structure) x -> GHKD_ f (Rep structure) Void
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
(==) = tuple -> tuple -> Bool
forall a. Eq a => a -> a -> Bool
(==) (tuple -> tuple -> Bool)
-> (HKD xs f -> tuple) -> HKD xs f -> HKD xs f -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` HKD xs f -> tuple
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 = tuple -> tuple -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (tuple -> tuple -> Ordering)
-> (HKD xs f -> tuple) -> HKD xs f -> HKD xs f -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` HKD xs f -> tuple
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 = tuple -> HKD xs f
forall (f :: * -> *) structure tuple.
Tuple f structure tuple =>
tuple -> HKD structure f
fromTuple (HKD xs f -> tuple
forall (f :: * -> *) structure tuple.
Tuple f structure tuple =>
HKD structure f -> tuple
toTuple HKD xs f
x tuple -> tuple -> tuple
forall a. Semigroup a => a -> a -> a
<> HKD xs f -> tuple
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 = tuple -> HKD xs f
forall (f :: * -> *) structure tuple.
Tuple f structure tuple =>
tuple -> HKD structure f
fromTuple tuple
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 = (tuple -> HKD structure f) -> Gen tuple -> Gen (HKD structure f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (GHKD_ f (Rep structure) Void -> HKD structure f
forall structure (f :: * -> *).
HKD_ f structure Void -> HKD structure f
HKD (GHKD_ f (Rep structure) Void -> HKD structure f)
-> (tuple -> GHKD_ f (Rep structure) Void)
-> tuple
-> HKD structure f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. tuple -> GHKD_ f (Rep structure) Void
forall (rep :: * -> *) tuple p.
GToTuple rep tuple =>
tuple -> rep p
gfromTuple) Gen tuple
forall a. Arbitrary a => Gen a
arbitrary

instance (CoArbitrary tuple, GToTuple (HKD_ f structure) tuple)
    => CoArbitrary (HKD structure f) where
  coarbitrary :: HKD structure f -> Gen b -> Gen b
coarbitrary (HKD HKD_ f structure Void
x) = tuple -> Gen b -> Gen b
forall a b. CoArbitrary a => a -> Gen b -> Gen b
coarbitrary (HKD_ f structure Void -> tuple
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 :: (HKD structure f -> b) -> HKD structure f :-> b
function = (HKD structure f -> tuple)
-> (tuple -> HKD structure f)
-> (HKD structure f -> b)
-> HKD structure f :-> b
forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
functionMap HKD structure f -> tuple
forall (f :: * -> *) structure tuple.
Tuple f structure tuple =>
HKD structure f -> tuple
toTuple tuple -> HKD structure f
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 :: D1 meta inner p -> String
gshow = forall (named :: Bool) (rep :: * -> *) p.
GShow named rep =>
rep p -> String
forall (rep :: * -> *) p. GShow named rep => rep p -> String
gshow @named (inner p -> String)
-> (D1 meta inner p -> inner p) -> D1 meta inner p -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. D1 meta inner p -> inner p
forall i (c :: Meta) k (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 :: C1 ('MetaCons name fixity 'True) inner p -> String
gshow (M1 inner p
x) = Proxy name -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (Proxy name
forall k (t :: k). Proxy t
Proxy @name) String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" {" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> inner p -> String
forall (named :: Bool) (rep :: * -> *) p.
GShow named rep =>
rep p -> String
gshow @'True inner p
x String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"}"

instance (GShow 'False inner, KnownSymbol name)
    => GShow any (C1 ('MetaCons name fixity 'False) inner) where
  gshow :: C1 ('MetaCons name fixity 'False) inner p -> String
gshow (M1 inner p
x) = Proxy name -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (Proxy name
forall k (t :: k). Proxy t
Proxy @name) String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> inner p -> String
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 :: (:*:) left right p -> String
gshow (left p
left :*: right p
right) = left p -> String
forall (named :: Bool) (rep :: * -> *) p.
GShow named rep =>
rep p -> String
gshow @'True left p
left String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
", " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> right p -> String
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 :: (:*:) left right p -> String
gshow (left p
left :*: right p
right) = left p -> String
forall (named :: Bool) (rep :: * -> *) p.
GShow named rep =>
rep p -> String
gshow @'False left p
left String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> right p -> String
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 :: S1 ('MetaSel ('Just field) i d c) inner p -> String
gshow (M1 inner p
inner) = Proxy field -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (Proxy field
forall k (t :: k). Proxy t
Proxy @field) String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" = " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> inner p -> String
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 :: S1 meta inner p -> String
gshow (M1 inner p
inner) = inner p -> String
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 :: K1 R (f inner) p -> String
gshow (K1 f inner
x) = f inner -> String
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) = HKD_ f structure Void -> String
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 :: tuple -> M1 index meta inner p
gfromTuple = inner p -> M1 index meta inner p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (inner p -> M1 index meta inner p)
-> (tuple -> inner p) -> tuple -> M1 index meta inner p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. tuple -> inner p
forall (rep :: * -> *) tuple p.
GToTuple rep tuple =>
tuple -> rep p
gfromTuple
  gtoTuple :: M1 index meta inner p -> tuple
gtoTuple   = inner p -> tuple
forall (rep :: * -> *) tuple p.
GToTuple rep tuple =>
rep p -> tuple
gtoTuple (inner p -> tuple)
-> (M1 index meta inner p -> inner p)
-> M1 index meta inner p
-> tuple
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 index meta inner p -> inner p
forall i (c :: Meta) k (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 :: (left', right') -> (:*:) left right p
gfromTuple (left'
x, right'
y) = left' -> left p
forall (rep :: * -> *) tuple p.
GToTuple rep tuple =>
tuple -> rep p
gfromTuple left'
x left p -> right p -> (:*:) left right p
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: right' -> right p
forall (rep :: * -> *) tuple p.
GToTuple rep tuple =>
tuple -> rep p
gfromTuple right'
y
  gtoTuple :: (:*:) left right p -> (left', right')
gtoTuple (left p
x :*: right p
y) = (left p -> left'
forall (rep :: * -> *) tuple p.
GToTuple rep tuple =>
rep p -> tuple
gtoTuple left p
x, right p -> right'
forall (rep :: * -> *) tuple p.
GToTuple rep tuple =>
rep p -> tuple
gtoTuple right p
y)

instance GToTuple (K1 index inner) inner where
  gfromTuple :: inner -> K1 index inner p
gfromTuple = inner -> K1 index inner p
forall k i c (p :: k). c -> K1 i c p
K1
  gtoTuple :: K1 index inner p -> inner
gtoTuple = K1 index inner p -> inner
forall i c k (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 = GHKD_ f (Rep structure) Void -> tuple
forall (rep :: * -> *) tuple p.
GToTuple rep tuple =>
rep p -> tuple
gtoTuple (GHKD_ f (Rep structure) Void -> tuple)
-> (HKD structure f -> GHKD_ f (Rep structure) Void)
-> HKD structure f
-> tuple
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HKD structure f -> GHKD_ f (Rep structure) Void
forall structure (f :: * -> *).
HKD structure f -> HKD_ f structure Void
runHKD
  fromTuple :: tuple -> HKD structure f
fromTuple = GHKD_ f (Rep structure) Void -> HKD structure f
forall structure (f :: * -> *).
HKD_ f structure Void -> HKD structure f
HKD (GHKD_ f (Rep structure) Void -> HKD structure f)
-> (tuple -> GHKD_ f (Rep structure) Void)
-> tuple
-> HKD structure f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. tuple -> GHKD_ f (Rep structure) Void
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 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 = GHKD_ g inner p -> M1 index meta (GHKD_ g inner) p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (GHKD_ g inner p -> M1 index meta (GHKD_ g inner) p)
-> (M1 index meta (GHKD_ f inner) p -> GHKD_ g inner p)
-> M1 index meta (GHKD_ f inner) p
-> M1 index meta (GHKD_ g inner) p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. f a -> g a) -> GHKD_ f inner p -> GHKD_ g inner p
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 (GHKD_ f inner p -> GHKD_ g inner p)
-> (M1 index meta (GHKD_ f inner) p -> GHKD_ f inner p)
-> M1 index meta (GHKD_ f inner) p
-> GHKD_ g inner p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 index meta (GHKD_ f inner) p -> GHKD_ f inner p
forall i (c :: Meta) k (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1

instance (GFunctorB left, GFunctorB right)
    => GFunctorB (left :*: right) where
  gbmap :: (forall a. f a -> g a)
-> GHKD_ f (left :*: right) p -> GHKD_ g (left :*: right) p
gbmap forall a. f a -> g a
f (left :*: right) = (forall a. f a -> g a) -> GHKD_ f left p -> GHKD_ g left p
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 GHKD_ g left p
-> GHKD_ g right p -> (:*:) (GHKD_ g left) (GHKD_ g right) p
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: (forall a. f a -> g a) -> GHKD_ f right p -> GHKD_ g right 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 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 x) = g inner -> K1 index (g inner) p
forall k i c (p :: k). c -> K1 i c p
K1 (f inner -> g inner
forall a. f a -> g a
f f inner
x)

instance GFunctorB (Rep structure) => FunctorB (HKD structure) where
  bmap :: (forall a. f a -> g a) -> HKD structure f -> HKD structure g
bmap forall a. f a -> g a
f = GHKD_ g (Rep structure) Void -> HKD structure g
forall structure (f :: * -> *).
HKD_ f structure Void -> HKD structure f
HKD (GHKD_ g (Rep structure) Void -> HKD structure g)
-> (HKD structure f -> GHKD_ g (Rep structure) Void)
-> HKD structure f
-> HKD structure g
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. f a -> g a)
-> GHKD_ f (Rep structure) Void -> GHKD_ g (Rep structure) Void
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 (GHKD_ f (Rep structure) Void -> GHKD_ g (Rep structure) Void)
-> (HKD structure f -> GHKD_ f (Rep structure) Void)
-> HKD structure f
-> GHKD_ g (Rep structure) Void
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HKD structure f -> GHKD_ f (Rep structure) Void
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 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 = (GHKD_ g inner p -> M1 index meta (GHKD_ g inner) p)
-> t (GHKD_ g inner p) -> t (M1 index meta (GHKD_ g inner) p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap GHKD_ g inner p -> M1 index meta (GHKD_ g inner) p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (t (GHKD_ g inner p) -> t (M1 index meta (GHKD_ g inner) p))
-> (M1 index meta (GHKD_ f inner) p -> t (GHKD_ g inner p))
-> M1 index meta (GHKD_ f inner) p
-> t (M1 index meta (GHKD_ g inner) p)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. f a -> t (g a))
-> GHKD_ f inner p -> t (GHKD_ g inner p)
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 (GHKD_ f inner p -> t (GHKD_ g inner p))
-> (M1 index meta (GHKD_ f inner) p -> GHKD_ f inner p)
-> M1 index meta (GHKD_ f inner) p
-> t (GHKD_ g inner p)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 index meta (GHKD_ f inner) p -> GHKD_ f inner p
forall i (c :: Meta) k (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1

instance (GTraversableB left, GTraversableB right)
    => GTraversableB (left :*: right) where
  gbtraverse :: (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 (left :*: right)
    = GHKD_ g left p
-> GHKD_ g right p -> (:*:) (GHKD_ g left) (GHKD_ g right) p
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
(:*:) (GHKD_ g left p
 -> GHKD_ g right p -> (:*:) (GHKD_ g left) (GHKD_ g right) p)
-> t (GHKD_ g left p)
-> t (GHKD_ g right p -> (:*:) (GHKD_ g left) (GHKD_ g right) p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. f a -> t (g a)) -> GHKD_ f left p -> t (GHKD_ g left p)
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
            t (GHKD_ g right p -> (:*:) (GHKD_ g left) (GHKD_ g right) p)
-> t (GHKD_ g right p)
-> t ((:*:) (GHKD_ g left) (GHKD_ g right) p)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall a. f a -> t (g a))
-> GHKD_ f right p -> t (GHKD_ g right p)
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 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 x) = (g inner -> K1 index (g inner) p)
-> t (g inner) -> t (K1 index (g inner) p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap g inner -> K1 index (g inner) p
forall k i c (p :: k). c -> K1 i c p
K1 (f inner -> t (g inner)
forall a. f a -> t (g a)
f f inner
x)

instance (FunctorB (HKD structure), GTraversableB (Rep structure))
    => TraversableB (HKD structure) where
  btraverse :: (forall a. f a -> e (g a))
-> HKD structure f -> e (HKD structure g)
btraverse forall a. f a -> e (g a)
f = (GHKD_ g (Rep structure) Void -> HKD structure g)
-> e (GHKD_ g (Rep structure) Void) -> e (HKD structure g)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap GHKD_ g (Rep structure) Void -> HKD structure g
forall structure (f :: * -> *).
HKD_ f structure Void -> HKD structure f
HKD (e (GHKD_ g (Rep structure) Void) -> e (HKD structure g))
-> (HKD structure f -> e (GHKD_ g (Rep structure) Void))
-> HKD structure f
-> e (HKD structure g)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. f a -> e (g a))
-> GHKD_ f (Rep structure) Void -> e (GHKD_ g (Rep structure) Void)
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 (GHKD_ f (Rep structure) Void -> e (GHKD_ g (Rep structure) Void))
-> (HKD structure f -> GHKD_ f (Rep structure) Void)
-> HKD structure f
-> e (GHKD_ g (Rep structure) Void)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HKD structure f -> GHKD_ f (Rep structure) Void
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 :: 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 x) (M1 y) = GHKD_ (Product f g) inner p
-> M1 index meta (GHKD_ (Product f g) inner) p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (GHKD_ f inner p -> GHKD_ g inner p -> GHKD_ (Product f g) inner p
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 a. f a) -> GHKD_ f (M1 index meta inner) p
gbpure forall a. f a
zero = GHKD_ f inner p -> M1 index meta (GHKD_ f inner) p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 ((forall a. f a) -> GHKD_ f inner p
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 :: GHKD_ f (left :*: right) p
-> GHKD_ g (left :*: right) p
-> GHKD_ (Product f g) (left :*: right) p
gbprod (leftX :*: rightX) (leftY :*: rightY)
    = GHKD_ f left p -> GHKD_ g left p -> GHKD_ (Product f g) left p
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 GHKD_ (Product f g) left p
-> GHKD_ (Product f g) right p
-> (:*:) (GHKD_ (Product f g) left) (GHKD_ (Product f g) right) p
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: GHKD_ f right p -> GHKD_ g right p -> GHKD_ (Product f g) right 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 a. f a) -> GHKD_ f (left :*: right) p
gbpure forall a. f a
zero
    = (forall a. f a) -> GHKD_ f left p
forall (rep :: * -> *) (f :: * -> *) p.
GApplicativeB rep =>
(forall a. f a) -> GHKD_ f rep p
gbpure @left forall a. f a
zero GHKD_ f left p
-> GHKD_ f right p -> (:*:) (GHKD_ f left) (GHKD_ f right) p
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: (forall a. f a) -> GHKD_ f right 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 :: GHKD_ f (K1 index inner) p
-> GHKD_ g (K1 index inner) p
-> GHKD_ (Product f g) (K1 index inner) p
gbprod (K1 x) (K1 y) = Product f g inner -> K1 index (Product f g inner) p
forall k i c (p :: k). c -> K1 i c p
K1 (f inner -> g inner -> Product f g inner
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 a. f a) -> GHKD_ f (K1 index inner) p
gbpure forall a. f a
zero = f inner -> K1 index (f inner) p
forall k i c (p :: k). c -> K1 i c p
K1 f inner
forall a. f a
zero

instance (FunctorB (HKD structure), GApplicativeB (Rep structure))
    => ApplicativeB (HKD structure) where
  bprod :: HKD structure f -> HKD structure g -> HKD structure (Product f g)
bprod (HKD HKD_ f structure Void
x) (HKD HKD_ g structure Void
y) = HKD_ (Product f g) structure Void -> HKD structure (Product f g)
forall structure (f :: * -> *).
HKD_ f structure Void -> HKD structure f
HKD (HKD_ f structure Void
-> HKD_ g structure Void -> HKD_ (Product f g) structure Void
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 a. f a) -> HKD structure f
bpure forall a. f a
zero            = HKD_ f structure Void -> HKD structure f
forall structure (f :: * -> *).
HKD_ f structure Void -> HKD structure f
HKD ((forall a. f a) -> HKD_ f structure Void
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 :: GHKD_ f (M1 index meta inner) p
-> GHKD_ (Product (Dict c) f) (M1 index meta inner) p
gbaddDicts (M1 x) = GHKD_ (Product (Dict c) f) inner p
-> M1 index meta (GHKD_ (Product (Dict c) f) inner) p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (GHKD_ f inner p -> GHKD_ (Product (Dict c) f) inner p
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 :: GHKD_ f (left :*: right) p
-> GHKD_ (Product (Dict c) f) (left :*: right) p
gbaddDicts (left :*: right)
    = GHKD_ f left p -> GHKD_ (Product (Dict c) f) left p
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 GHKD_ (Product (Dict c) f) left p
-> GHKD_ (Product (Dict c) f) right p
-> (:*:)
     (GHKD_ (Product (Dict c) f) left)
     (GHKD_ (Product (Dict c) f) right)
     p
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: GHKD_ f right p -> GHKD_ (Product (Dict c) f) right 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 :: GHKD_ f (K1 index inner) p
-> GHKD_ (Product (Dict c) f) (K1 index inner) p
gbaddDicts (K1 x) = Product (Dict c) f inner -> K1 index (Product (Dict c) f inner) p
forall k i c (p :: k). c -> K1 i c p
K1 (Dict c inner -> f inner -> Product (Dict c) f inner
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair Dict c inner
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 :: HKD structure f -> HKD structure (Product (Dict c) f)
baddDicts (HKD HKD_ f structure Void
x)
    = HKD_ (Product (Dict c) f) structure Void
-> HKD structure (Product (Dict c) f)
forall structure (f :: * -> *).
HKD_ f structure Void -> HKD structure f
HKD (HKD_ f structure Void -> HKD_ (Product (Dict c) f) structure Void
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)