{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
module Dep.Env
(
Has,
TheDefaultFieldName (..),
TheFieldName (..),
FieldsFindableByType (..),
Autowired (..),
Autowireable,
Phased (..),
pullPhase,
mapPhase,
liftA2Phase,
DemotableFieldNames (..),
demoteFieldNames,
mapPhaseWithFieldNames,
bindPhase,
skipPhase,
Bare,
fromBare,
toBare,
fixEnv,
Constructor,
constructor,
fixEnvAccum,
AccumConstructor,
InductiveEnv (..),
addDep,
emptyEnv,
Identity (..),
Constant (..),
Compose (..),
)
where
import Control.Applicative
import Data.Coerce
import Data.Function (fix)
import Data.Functor (($>), (<&>))
import Data.Functor.Compose
import Data.Functor.Constant
import Data.Functor.Identity
import Data.Kind
import Data.Proxy
import Data.String
import Data.Type.Equality (type (==))
import Data.Typeable
import Dep.Has
import GHC.Generics qualified as G
import GHC.Records
import GHC.TypeLits
newtype TheDefaultFieldName (env :: Type) = TheDefaultFieldName env
instance
(Dep r_, HasField (DefaultFieldName r_) (env_ m) u, Coercible u (r_ m)) =>
Has r_ m (TheDefaultFieldName (env_ m))
where
dep :: TheDefaultFieldName (env_ m) -> r_ m
dep (TheDefaultFieldName env_ m
env) = coerce :: forall a b. Coercible a b => a -> b
coerce forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (x :: k) r a. HasField x r a => r -> a
getField @(DefaultFieldName r_) forall a b. (a -> b) -> a -> b
$ env_ m
env
type TheFieldName :: Symbol -> Type -> Type
newtype TheFieldName (name :: Symbol) (env :: Type) = TheFieldName env
instance
(HasField name (env_ m) u, Coercible u (r_ m)) =>
Has r_ m (TheFieldName name (env_ m))
where
dep :: TheFieldName name (env_ m) -> r_ m
dep (TheFieldName env_ m
env) = coerce :: forall a b. Coercible a b => a -> b
coerce forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (x :: k) r a. HasField x r a => r -> a
getField @name forall a b. (a -> b) -> a -> b
$ env_ m
env
type FieldsFindableByType :: Type -> Constraint
class FieldsFindableByType (env :: Type) where
type FindFieldByType env (r :: Type) :: Symbol
type FindFieldByType env r = FindFieldByType_ env r
type Autowired :: Type -> Type
newtype Autowired (env :: Type) = Autowired env
type Autowireable r_ (m :: Type -> Type) (env :: Type) = HasField (FindFieldByType env (r_ m)) env (Identity (r_ m))
instance
( FieldsFindableByType (env_ m),
HasField (FindFieldByType (env_ m) (r_ m)) (env_ m) u,
Coercible u (r_ m)
) =>
Has r_ m (Autowired (env_ m))
where
dep :: Autowired (env_ m) -> r_ m
dep (Autowired env_ m
env) = coerce :: forall a b. Coercible a b => a -> b
coerce @u forall a b. (a -> b) -> a -> b
$ forall {k} (x :: k) r a. HasField x r a => r -> a
getField @(FindFieldByType (env_ m) (r_ m)) env_ m
env
type FindFieldByType_ :: Type -> Type -> Symbol
type family FindFieldByType_ env r where
FindFieldByType_ env r = IfMissing r (GFindFieldByType (ExtractProduct (G.Rep env)) r)
type ExtractProduct :: (k -> Type) -> k -> Type
type family envRep where
(G.D1 _ (G.C1 _ z)) = z
type IfMissing :: Type -> Maybe Symbol -> Symbol
type family IfMissing r ms where
IfMissing r Nothing =
TypeError
( Text "The component "
:<>: ShowType r
:<>: Text " could not be found in environment."
)
IfMissing _ (Just name) = name
type GFindFieldByType :: (k -> Type) -> Type -> Maybe Symbol
type family GFindFieldByType r x where
GFindFieldByType (left G.:*: right) r =
WithLeftResult_ (GFindFieldByType left r) right r
GFindFieldByType (G.S1 (G.MetaSel ('Just name) _ _ _) (G.Rec0 r)) r = Just name
GFindFieldByType (G.S1 (G.MetaSel ('Just name) _ _ _) (G.Rec0 (_ r))) r = Just name
GFindFieldByType _ _ = Nothing
type WithLeftResult_ :: Maybe Symbol -> (k -> Type) -> Type -> Maybe Symbol
type family WithLeftResult_ leftResult right r where
WithLeftResult_ ('Just ls) right r = 'Just ls
WithLeftResult_ Nothing right r = GFindFieldByType right r
type Phased :: ((Type -> Type) -> (Type -> Type) -> Type) -> Constraint
class Phased (env_ :: (Type -> Type) -> (Type -> Type) -> Type) where
traverseH ::
forall
(h :: Type -> Type)
(f :: Type -> Type)
(g :: Type -> Type)
(m :: Type -> Type).
(
Applicative f,
Typeable f,
Typeable g,
Typeable h,
Typeable m
) =>
(forall x. Typeable x => h x -> f (g x)) ->
env_ h m ->
f (env_ g m)
default traverseH ::
forall
(h :: Type -> Type)
(f :: Type -> Type)
(g :: Type -> Type)
(m :: Type -> Type).
( Applicative f,
Typeable f,
Typeable g,
Typeable h,
Typeable m,
G.Generic (env_ h m),
G.Generic (env_ g m),
GTraverseH h g (G.Rep (env_ h m)) (G.Rep (env_ g m))
) =>
(forall x. Typeable x => h x -> f (g x)) ->
env_ h m ->
f (env_ g m)
traverseH forall x. Typeable x => h x -> f (g x)
t env_ h m
env = forall a x. Generic a => Rep a x -> a
G.to forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} {k} (h :: k -> *) (g :: k -> *) (env :: k -> *)
(env' :: k -> *) (f :: * -> *) (x :: k).
(GTraverseH h g env env', Applicative f) =>
(forall (x :: k). Typeable x => h x -> f (g x))
-> env x -> f (env' x)
gTraverseH forall x. Typeable x => h x -> f (g x)
t (forall a x. Generic a => a -> Rep a x
G.from env_ h m
env)
liftA2H ::
forall (a :: Type -> Type) (f :: Type -> Type) (f' :: Type -> Type) (m :: Type -> Type).
( Typeable a,
Typeable f,
Typeable f',
Typeable m
) =>
(forall x. Typeable x => a x -> f x -> f' x) ->
env_ a m ->
env_ f m ->
env_ f' m
default liftA2H ::
forall (a :: Type -> Type) (f :: Type -> Type) (f' :: Type -> Type) m.
( Typeable a,
Typeable f,
Typeable f',
Typeable m,
G.Generic (env_ a m),
G.Generic (env_ f m),
G.Generic (env_ f' m),
GLiftA2Phase a f f' (G.Rep (env_ a m)) (G.Rep (env_ f m)) (G.Rep (env_ f' m))
) =>
(forall x. Typeable x => a x -> f x -> f' x) ->
env_ a m ->
env_ f m ->
env_ f' m
liftA2H forall x. Typeable x => a x -> f x -> f' x
f env_ a m
enva env_ f m
env = forall a x. Generic a => Rep a x -> a
G.to (forall {k} {k} (a :: k -> *) (f :: k -> *) (f' :: k -> *)
(enva :: k -> *) (env :: k -> *) (env' :: k -> *) (x :: k).
GLiftA2Phase a f f' enva env env' =>
(forall (r :: k). Typeable r => a r -> f r -> f' r)
-> enva x -> env x -> env' x
gLiftA2Phase forall x. Typeable x => a x -> f x -> f' x
f (forall a x. Generic a => a -> Rep a x
G.from env_ a m
enva) (forall a x. Generic a => a -> Rep a x
G.from env_ f m
env))
pullPhase ::
forall (f :: Type -> Type) (g :: Type -> Type) (m :: Type -> Type) env_.
(Phased env_, Applicative f, Typeable f, Typeable g, Typeable m) =>
env_ (Compose f g) m ->
f (env_ g m)
pullPhase :: forall (f :: * -> *) (g :: * -> *) (m :: * -> *)
(env_ :: (* -> *) -> (* -> *) -> *).
(Phased env_, Applicative f, Typeable f, Typeable g, Typeable m) =>
env_ (Compose f g) m -> f (env_ g m)
pullPhase = forall (env_ :: (* -> *) -> (* -> *) -> *) (h :: * -> *)
(f :: * -> *) (g :: * -> *) (m :: * -> *).
(Phased env_, Applicative f, Typeable f, Typeable g, Typeable h,
Typeable m) =>
(forall x. Typeable x => h x -> f (g x))
-> env_ h m -> f (env_ g m)
traverseH @env_ forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose
mapPhase ::
forall (f :: Type -> Type) (f' :: Type -> Type) (g :: Type -> Type) (m :: Type -> Type) env_.
(Phased env_, Typeable f, Typeable f', Typeable g, Typeable m) =>
(forall x. Typeable x => f x -> f' x) ->
env_ (Compose f g) m ->
env_ (Compose f' g) m
mapPhase :: forall (f :: * -> *) (f' :: * -> *) (g :: * -> *) (m :: * -> *)
(env_ :: (* -> *) -> (* -> *) -> *).
(Phased env_, Typeable f, Typeable f', Typeable g, Typeable m) =>
(forall x. Typeable x => f x -> f' x)
-> env_ (Compose f g) m -> env_ (Compose f' g) m
mapPhase forall x. Typeable x => f x -> f' x
f env_ (Compose f g) m
env = forall a. Identity a -> a
runIdentity forall a b. (a -> b) -> a -> b
$ forall (env_ :: (* -> *) -> (* -> *) -> *) (h :: * -> *)
(f :: * -> *) (g :: * -> *) (m :: * -> *).
(Phased env_, Applicative f, Typeable f, Typeable g, Typeable h,
Typeable m) =>
(forall x. Typeable x => h x -> f (g x))
-> env_ h m -> f (env_ g m)
traverseH @env_ (\(Compose f (g x)
fg) -> forall a. a -> Identity a
Identity (forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (forall x. Typeable x => f x -> f' x
f f (g x)
fg))) env_ (Compose f g) m
env
liftA2Phase ::
forall (a :: Type -> Type) (f' :: Type -> Type) (f :: Type -> Type) (g :: Type -> Type) (m :: Type -> Type) env_.
(Phased env_, Typeable a, Typeable f, Typeable f', Typeable g, Typeable m) =>
(forall x. Typeable x => a x -> f x -> f' x) ->
env_ (Compose a g) m ->
env_ (Compose f g) m ->
env_ (Compose f' g) m
liftA2Phase :: forall (a :: * -> *) (f' :: * -> *) (f :: * -> *) (g :: * -> *)
(m :: * -> *) (env_ :: (* -> *) -> (* -> *) -> *).
(Phased env_, Typeable a, Typeable f, Typeable f', Typeable g,
Typeable m) =>
(forall x. Typeable x => a x -> f x -> f' x)
-> env_ (Compose a g) m
-> env_ (Compose f g) m
-> env_ (Compose f' g) m
liftA2Phase forall x. Typeable x => a x -> f x -> f' x
f = forall (env_ :: (* -> *) -> (* -> *) -> *) (a :: * -> *)
(f :: * -> *) (f' :: * -> *) (m :: * -> *).
(Phased env_, Typeable a, Typeable f, Typeable f', Typeable m) =>
(forall x. Typeable x => a x -> f x -> f' x)
-> env_ a m -> env_ f m -> env_ f' m
liftA2H @env_ (\(Compose a (g x)
fa) (Compose f (g x)
fg) -> forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (forall x. Typeable x => a x -> f x -> f' x
f a (g x)
fa f (g x)
fg))
class GTraverseH h g env env' | env -> h, env' -> g where
gTraverseH :: Applicative f => (forall x. Typeable x => h x -> f (g x)) -> env x -> f (env' x)
instance
(GTraverseH h g fields fields') =>
GTraverseH
h
g
(G.D1 metaData (G.C1 metaCons fields))
(G.D1 metaData (G.C1 metaCons fields'))
where
gTraverseH :: forall (f :: * -> *) (x :: k).
Applicative f =>
(forall (x :: k). Typeable x => h x -> f (g x))
-> D1 metaData (C1 metaCons fields) x
-> f (D1 metaData (C1 metaCons fields') x)
gTraverseH forall (x :: k). Typeable x => h x -> f (g x)
t (G.M1 (G.M1 fields x
fields)) =
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} {k} (h :: k -> *) (g :: k -> *) (env :: k -> *)
(env' :: k -> *) (f :: * -> *) (x :: k).
(GTraverseH h g env env', Applicative f) =>
(forall (x :: k). Typeable x => h x -> f (g x))
-> env x -> f (env' x)
gTraverseH @h @g forall (x :: k). Typeable x => h x -> f (g x)
t fields x
fields
instance
( GTraverseH h g left left',
GTraverseH h g right right'
) =>
GTraverseH h g (left G.:*: right) (left' G.:*: right')
where
gTraverseH :: forall (f :: * -> *) (x :: k).
Applicative f =>
(forall (x :: k). Typeable x => h x -> f (g x))
-> (:*:) left right x -> f ((:*:) left' right' x)
gTraverseH forall (x :: k). Typeable x => h x -> f (g x)
t (left x
left G.:*: right x
right) =
let left' :: f (left' x)
left' = forall {k} {k} (h :: k -> *) (g :: k -> *) (env :: k -> *)
(env' :: k -> *) (f :: * -> *) (x :: k).
(GTraverseH h g env env', Applicative f) =>
(forall (x :: k). Typeable x => h x -> f (g x))
-> env x -> f (env' x)
gTraverseH @h @g forall (x :: k). Typeable x => h x -> f (g x)
t left x
left
right' :: f (right' x)
right' = forall {k} {k} (h :: k -> *) (g :: k -> *) (env :: k -> *)
(env' :: k -> *) (f :: * -> *) (x :: k).
(GTraverseH h g env env', Applicative f) =>
(forall (x :: k). Typeable x => h x -> f (g x))
-> env x -> f (env' x)
gTraverseH @h @g forall (x :: k). Typeable x => h x -> f (g x)
t right x
right
in forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
(G.:*:) f (left' x)
left' f (right' x)
right'
instance
Typeable bean =>
GTraverseH
h
g
(G.S1 metaSel (G.Rec0 (h bean)))
(G.S1 metaSel (G.Rec0 (g bean)))
where
gTraverseH :: forall (f :: * -> *) (x :: k).
Applicative f =>
(forall (x :: k). Typeable x => h x -> f (g x))
-> S1 metaSel (Rec0 (h bean)) x -> f (S1 metaSel (Rec0 (g bean)) x)
gTraverseH forall (x :: k). Typeable x => h x -> f (g x)
t (G.M1 (G.K1 h bean
hbean)) =
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k i c (p :: k). c -> K1 i c p
G.K1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (x :: k). Typeable x => h x -> f (g x)
t h bean
hbean
class GLiftA2Phase a f f' enva env env' | enva -> a, env -> f, env' -> f' where
gLiftA2Phase :: (forall r. Typeable r => a r -> f r -> f' r) -> enva x -> env x -> env' x
instance
GLiftA2Phase a f f' fieldsa fields fields' =>
GLiftA2Phase
a
f
f'
(G.D1 metaData (G.C1 metaCons fieldsa))
(G.D1 metaData (G.C1 metaCons fields))
(G.D1 metaData (G.C1 metaCons fields'))
where
gLiftA2Phase :: forall (x :: k).
(forall (r :: k). Typeable r => a r -> f r -> f' r)
-> D1 metaData (C1 metaCons fieldsa) x
-> D1 metaData (C1 metaCons fields) x
-> D1 metaData (C1 metaCons fields') x
gLiftA2Phase forall (r :: k). Typeable r => a r -> f r -> f' r
f (G.M1 (G.M1 fieldsa x
fieldsa)) (G.M1 (G.M1 fields x
fields)) =
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (forall {k} {k} (a :: k -> *) (f :: k -> *) (f' :: k -> *)
(enva :: k -> *) (env :: k -> *) (env' :: k -> *) (x :: k).
GLiftA2Phase a f f' enva env env' =>
(forall (r :: k). Typeable r => a r -> f r -> f' r)
-> enva x -> env x -> env' x
gLiftA2Phase @a @f @f' forall (r :: k). Typeable r => a r -> f r -> f' r
f fieldsa x
fieldsa fields x
fields))
instance
( GLiftA2Phase a f f' lefta left left',
GLiftA2Phase a f f' righta right right'
) =>
GLiftA2Phase a f f' (lefta G.:*: righta) (left G.:*: right) (left' G.:*: right')
where
gLiftA2Phase :: forall (x :: k).
(forall (r :: k). Typeable r => a r -> f r -> f' r)
-> (:*:) lefta righta x
-> (:*:) left right x
-> (:*:) left' right' x
gLiftA2Phase forall (r :: k). Typeable r => a r -> f r -> f' r
f (lefta x
lefta G.:*: righta x
righta) (left x
left G.:*: right x
right) =
let left' :: left' x
left' = forall {k} {k} (a :: k -> *) (f :: k -> *) (f' :: k -> *)
(enva :: k -> *) (env :: k -> *) (env' :: k -> *) (x :: k).
GLiftA2Phase a f f' enva env env' =>
(forall (r :: k). Typeable r => a r -> f r -> f' r)
-> enva x -> env x -> env' x
gLiftA2Phase @a @f @f' forall (r :: k). Typeable r => a r -> f r -> f' r
f lefta x
lefta left x
left
right' :: right' x
right' = forall {k} {k} (a :: k -> *) (f :: k -> *) (f' :: k -> *)
(enva :: k -> *) (env :: k -> *) (env' :: k -> *) (x :: k).
GLiftA2Phase a f f' enva env env' =>
(forall (r :: k). Typeable r => a r -> f r -> f' r)
-> enva x -> env x -> env' x
gLiftA2Phase @a @f @f' forall (r :: k). Typeable r => a r -> f r -> f' r
f righta x
righta right x
right
in forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
(G.:*:) left' x
left' right' x
right'
instance
Typeable bean =>
GLiftA2Phase
a
f
f'
(G.S1 metaSel (G.Rec0 (a bean)))
(G.S1 metaSel (G.Rec0 (f bean)))
(G.S1 metaSel (G.Rec0 (f' bean)))
where
gLiftA2Phase :: forall (x :: k).
(forall (r :: k). Typeable r => a r -> f r -> f' r)
-> S1 metaSel (Rec0 (a bean)) x
-> S1 metaSel (Rec0 (f bean)) x
-> S1 metaSel (Rec0 (f' bean)) x
gLiftA2Phase forall (r :: k). Typeable r => a r -> f r -> f' r
f (G.M1 (G.K1 a bean
abean)) (G.M1 (G.K1 f bean
fgbean)) =
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (forall k i c (p :: k). c -> K1 i c p
G.K1 (forall (r :: k). Typeable r => a r -> f r -> f' r
f a bean
abean f bean
fgbean))
type DemotableFieldNames :: ((Type -> Type) -> (Type -> Type) -> Type) -> Constraint
class DemotableFieldNames env_ where
demoteFieldNamesH :: (forall x. String -> h String x) -> env_ (h String) m
default demoteFieldNamesH ::
( G.Generic (env_ (h String) m),
GDemotableFieldNamesH h (G.Rep (env_ (h String) m))
) =>
(forall x. String -> h String x) ->
env_ (h String) m
demoteFieldNamesH forall x. String -> h String x
f = forall a x. Generic a => Rep a x -> a
G.to (forall {k} {k} (h :: * -> k -> *) (env :: k -> *) (x :: k).
GDemotableFieldNamesH h env =>
(forall (x :: k). String -> h String x) -> env x
gDemoteFieldNamesH forall x. String -> h String x
f)
demoteFieldNames :: forall env_ m. DemotableFieldNames env_ => env_ (Constant String) m
demoteFieldNames :: forall (env_ :: (* -> *) -> (* -> *) -> *) (m :: * -> *).
DemotableFieldNames env_ =>
env_ (Constant String) m
demoteFieldNames = forall (env_ :: (* -> *) -> (* -> *) -> *) (h :: * -> * -> *)
(m :: * -> *).
DemotableFieldNames env_ =>
(forall x. String -> h String x) -> env_ (h String) m
demoteFieldNamesH forall {k} a (b :: k). a -> Constant a b
Constant
class GDemotableFieldNamesH h env | env -> h where
gDemoteFieldNamesH :: (forall x. String -> h String x) -> env x
instance
GDemotableFieldNamesH h fields =>
GDemotableFieldNamesH h (G.D1 metaData (G.C1 metaCons fields))
where
gDemoteFieldNamesH :: forall (x :: k).
(forall (x :: k). String -> h String x)
-> D1 metaData (C1 metaCons fields) x
gDemoteFieldNamesH forall (x :: k). String -> h String x
f = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (forall {k} {k} (h :: * -> k -> *) (env :: k -> *) (x :: k).
GDemotableFieldNamesH h env =>
(forall (x :: k). String -> h String x) -> env x
gDemoteFieldNamesH forall (x :: k). String -> h String x
f))
instance
( GDemotableFieldNamesH h left,
GDemotableFieldNamesH h right
) =>
GDemotableFieldNamesH h (left G.:*: right)
where
gDemoteFieldNamesH :: forall (x :: k).
(forall (x :: k). String -> h String x) -> (:*:) left right x
gDemoteFieldNamesH forall (x :: k). String -> h String x
f =
forall {k} {k} (h :: * -> k -> *) (env :: k -> *) (x :: k).
GDemotableFieldNamesH h env =>
(forall (x :: k). String -> h String x) -> env x
gDemoteFieldNamesH forall (x :: k). String -> h String x
f forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
G.:*: forall {k} {k} (h :: * -> k -> *) (env :: k -> *) (x :: k).
GDemotableFieldNamesH h env =>
(forall (x :: k). String -> h String x) -> env x
gDemoteFieldNamesH forall (x :: k). String -> h String x
f
instance KnownSymbol name => GDemotableFieldNamesH h (G.S1 (G.MetaSel ('Just name) u v w) (G.Rec0 (h String bean))) where
gDemoteFieldNamesH :: forall (x :: k).
(forall (x :: k). String -> h String x)
-> S1 ('MetaSel ('Just name) u v w) (Rec0 (h String bean)) x
gDemoteFieldNamesH forall (x :: k). String -> h String x
f =
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (forall k i c (p :: k). c -> K1 i c p
G.K1 (forall (x :: k). String -> h String x
f (forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
Proxy @name))))
mapPhaseWithFieldNames ::
forall (f :: Type -> Type) (f' :: Type -> Type) (g :: Type -> Type) (m :: Type -> Type) env_.
( Phased env_,
DemotableFieldNames env_,
Typeable f,
Typeable f',
Typeable g,
Typeable m
) =>
(forall x. Typeable x => String -> f x -> f' x) ->
env_ (Compose f g) m ->
env_ (Compose f' g) m
mapPhaseWithFieldNames :: forall (f :: * -> *) (f' :: * -> *) (g :: * -> *) (m :: * -> *)
(env_ :: (* -> *) -> (* -> *) -> *).
(Phased env_, DemotableFieldNames env_, Typeable f, Typeable f',
Typeable g, Typeable m) =>
(forall x. Typeable x => String -> f x -> f' x)
-> env_ (Compose f g) m -> env_ (Compose f' g) m
mapPhaseWithFieldNames forall x. Typeable x => String -> f x -> f' x
f env_ (Compose f g) m
env =
forall (a :: * -> *) (f' :: * -> *) (f :: * -> *) (g :: * -> *)
(m :: * -> *) (env_ :: (* -> *) -> (* -> *) -> *).
(Phased env_, Typeable a, Typeable f, Typeable f', Typeable g,
Typeable m) =>
(forall x. Typeable x => a x -> f x -> f' x)
-> env_ (Compose a g) m
-> env_ (Compose f g) m
-> env_ (Compose f' g) m
liftA2Phase (\(Constant String
name) f x
z -> forall x. Typeable x => String -> f x -> f' x
f String
name f x
z) (forall a. Identity a -> a
runIdentity forall a b. (a -> b) -> a -> b
$ forall (env_ :: (* -> *) -> (* -> *) -> *) (h :: * -> *)
(f :: * -> *) (g :: * -> *) (m :: * -> *).
(Phased env_, Applicative f, Typeable f, Typeable g, Typeable h,
Typeable m) =>
(forall x. Typeable x => h x -> f (g x))
-> env_ h m -> f (env_ g m)
traverseH @env_ (\(Constant String
z) -> forall a. a -> Identity a
Identity (forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (forall {k} a (b :: k). a -> Constant a b
Constant String
z))) forall (env_ :: (* -> *) -> (* -> *) -> *) (m :: * -> *).
DemotableFieldNames env_ =>
env_ (Constant String) m
demoteFieldNames) env_ (Compose f g) m
env
bindPhase :: forall f g a b. Functor f => f a -> (a -> g b) -> Compose f g b
bindPhase :: forall {k1} (f :: * -> *) (g :: k1 -> *) a (b :: k1).
Functor f =>
f a -> (a -> g b) -> Compose f g b
bindPhase f a
f a -> g b
k = forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f a
f forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> a -> g b
k)
skipPhase :: forall f g a. Applicative f => g a -> Compose f g a
skipPhase :: forall {k1} (f :: * -> *) (g :: k1 -> *) (a :: k1).
Applicative f =>
g a -> Compose f g a
skipPhase g a
g = forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (forall (f :: * -> *) a. Applicative f => a -> f a
pure g a
g)
type Bare :: Type -> Type
type family Bare x where
Bare (Compose outer inner x) = Bare (outer (Bare (inner x)))
Bare (Identity x) = x
Bare (Const x k) = x
Bare (Constant x k) = x
Bare other = other
fromBare :: Coercible phases (Bare phases) => Bare phases -> phases
fromBare :: forall phases.
Coercible phases (Bare phases) =>
Bare phases -> phases
fromBare = coerce :: forall a b. Coercible a b => a -> b
coerce
toBare :: Coercible phases (Bare phases) => phases -> Bare phases
toBare :: forall phases.
Coercible phases (Bare phases) =>
phases -> Bare phases
toBare = coerce :: forall a b. Coercible a b => a -> b
coerce
type Constructor (env :: Type) = ((->) env) `Compose` Identity
constructor :: forall r_ m env. (env -> r_ m) -> Constructor env (r_ m)
constructor :: forall {k} (r_ :: k -> *) (m :: k) env.
(env -> r_ m) -> Constructor env (r_ m)
constructor = coerce :: forall a b. Coercible a b => a -> b
coerce
type AccumConstructor (w :: Type) (env :: Type) = (->) (w, env) `Compose` (,) w `Compose` Identity
fixEnv ::
(Phased env_, Typeable env_, Typeable m) =>
env_ (Constructor (env_ Identity m)) m ->
env_ Identity m
fixEnv :: forall (env_ :: (* -> *) -> (* -> *) -> *) (m :: * -> *).
(Phased env_, Typeable env_, Typeable m) =>
env_ (Constructor (env_ Identity m)) m -> env_ Identity m
fixEnv env_ (Constructor (env_ Identity m)) m
env = forall a. (a -> a) -> a
fix (forall (f :: * -> *) (g :: * -> *) (m :: * -> *)
(env_ :: (* -> *) -> (* -> *) -> *).
(Phased env_, Applicative f, Typeable f, Typeable g, Typeable m) =>
env_ (Compose f g) m -> f (env_ g m)
pullPhase env_ (Constructor (env_ Identity m)) m
env)
fixEnvAccum ::
(Phased env_, Typeable env_, Typeable m, Monoid w, Typeable w) =>
env_ (AccumConstructor w (env_ Identity m)) m ->
(w, env_ Identity m)
fixEnvAccum :: forall (env_ :: (* -> *) -> (* -> *) -> *) (m :: * -> *) w.
(Phased env_, Typeable env_, Typeable m, Monoid w, Typeable w) =>
env_ (AccumConstructor w (env_ Identity m)) m
-> (w, env_ Identity m)
fixEnvAccum env_ (AccumConstructor w (env_ Identity m)) m
env =
let f :: (w, env_ Identity m) -> (w, env_ Identity m)
f = forall (f :: * -> *) (g :: * -> *) (m :: * -> *)
(env_ :: (* -> *) -> (* -> *) -> *).
(Phased env_, Applicative f, Typeable f, Typeable g, Typeable m) =>
env_ (Compose f g) m -> f (env_ g m)
pullPhase forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (f :: * -> *) (g :: * -> *) (m :: * -> *)
(env_ :: (* -> *) -> (* -> *) -> *).
(Phased env_, Applicative f, Typeable f, Typeable g, Typeable m) =>
env_ (Compose f g) m -> f (env_ g m)
pullPhase env_ (AccumConstructor w (env_ Identity m)) m
env
in forall a. (a -> a) -> a
fix (w, env_ Identity m) -> (w, env_ Identity m)
f
data InductiveEnv (rs :: [(Type -> Type) -> Type]) (h :: Type -> Type) (m :: Type -> Type) where
AddDep :: forall r_ m rs h. Typeable r_ => h (r_ m) -> InductiveEnv rs h m -> InductiveEnv (r_ : rs) h m
EmptyEnv :: forall m h. InductiveEnv '[] h m
addDep :: forall r_ m rs. Typeable r_ => r_ m -> InductiveEnv rs Identity m -> InductiveEnv (r_ : rs) Identity m
addDep :: forall (r_ :: (* -> *) -> *) (m :: * -> *) (rs :: [(* -> *) -> *]).
Typeable r_ =>
r_ m
-> InductiveEnv rs Identity m -> InductiveEnv (r_ : rs) Identity m
addDep = forall (r_ :: (* -> *) -> *) (m :: * -> *) (rs :: [(* -> *) -> *])
(h :: * -> *).
Typeable r_ =>
h (r_ m) -> InductiveEnv rs h m -> InductiveEnv (r_ : rs) h m
AddDep @r_ @m @rs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Identity a
Identity
emptyEnv :: forall m. InductiveEnv '[] Identity m
emptyEnv :: forall (m :: * -> *). InductiveEnv '[] Identity m
emptyEnv = forall (m :: * -> *) (h :: * -> *). InductiveEnv '[] h m
EmptyEnv @m @Identity
instance Phased (InductiveEnv rs) where
traverseH :: forall (h :: * -> *) (f :: * -> *) (g :: * -> *) (m :: * -> *).
(Applicative f, Typeable f, Typeable g, Typeable h, Typeable m) =>
(forall x. Typeable x => h x -> f (g x))
-> InductiveEnv rs h m -> f (InductiveEnv rs g m)
traverseH forall x. Typeable x => h x -> f (g x)
t InductiveEnv rs h m
EmptyEnv = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (m :: * -> *) (h :: * -> *). InductiveEnv '[] h m
EmptyEnv
traverseH forall x. Typeable x => h x -> f (g x)
t (AddDep h (r_ m)
hx InductiveEnv rs h m
rest) =
let headF :: f (g (r_ m))
headF = forall x. Typeable x => h x -> f (g x)
t h (r_ m)
hx
restF :: f (InductiveEnv rs g m)
restF = forall (env_ :: (* -> *) -> (* -> *) -> *) (h :: * -> *)
(f :: * -> *) (g :: * -> *) (m :: * -> *).
(Phased env_, Applicative f, Typeable f, Typeable g, Typeable h,
Typeable m) =>
(forall x. Typeable x => h x -> f (g x))
-> env_ h m -> f (env_ g m)
traverseH forall x. Typeable x => h x -> f (g x)
t InductiveEnv rs h m
rest
in forall (r_ :: (* -> *) -> *) (m :: * -> *) (rs :: [(* -> *) -> *])
(h :: * -> *).
Typeable r_ =>
h (r_ m) -> InductiveEnv rs h m -> InductiveEnv (r_ : rs) h m
AddDep forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (g (r_ m))
headF forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f (InductiveEnv rs g m)
restF
liftA2H :: forall (a :: * -> *) (f :: * -> *) (f' :: * -> *) (m :: * -> *).
(Typeable a, Typeable f, Typeable f', Typeable m) =>
(forall x. Typeable x => a x -> f x -> f' x)
-> InductiveEnv rs a m
-> InductiveEnv rs f m
-> InductiveEnv rs f' m
liftA2H forall x. Typeable x => a x -> f x -> f' x
t InductiveEnv rs a m
EmptyEnv InductiveEnv rs f m
EmptyEnv = forall (m :: * -> *) (h :: * -> *). InductiveEnv '[] h m
EmptyEnv
liftA2H forall x. Typeable x => a x -> f x -> f' x
t (AddDep a (r_ m)
ax InductiveEnv rs a m
arest) (AddDep f (r_ m)
hx InductiveEnv rs f m
hrest) =
forall (r_ :: (* -> *) -> *) (m :: * -> *) (rs :: [(* -> *) -> *])
(h :: * -> *).
Typeable r_ =>
h (r_ m) -> InductiveEnv rs h m -> InductiveEnv (r_ : rs) h m
AddDep (forall x. Typeable x => a x -> f x -> f' x
t a (r_ m)
ax f (r_ m)
hx) (forall (env_ :: (* -> *) -> (* -> *) -> *) (a :: * -> *)
(f :: * -> *) (f' :: * -> *) (m :: * -> *).
(Phased env_, Typeable a, Typeable f, Typeable f', Typeable m) =>
(forall x. Typeable x => a x -> f x -> f' x)
-> env_ a m -> env_ f m -> env_ f' m
liftA2H forall x. Typeable x => a x -> f x -> f' x
t InductiveEnv rs a m
arest InductiveEnv rs f m
hrest)
instance InductiveEnvFind r_ m rs => Has r_ m (InductiveEnv rs Identity m) where
dep :: InductiveEnv rs Identity m -> r_ m
dep = forall (r_ :: (* -> *) -> *) (m :: * -> *) (rs :: [(* -> *) -> *]).
InductiveEnvFind r_ m rs =>
InductiveEnv rs Identity m -> r_ m
inductiveEnvDep
class InductiveEnvFind r_ m rs where
inductiveEnvDep :: InductiveEnv rs Identity m -> r_ m
instance
TypeError
( Text "The component "
:<>: ShowType r_
:<>: Text " could not be found in environment."
) =>
InductiveEnvFind r_ m '[]
where
inductiveEnvDep :: InductiveEnv '[] Identity m -> r_ m
inductiveEnvDep = forall a. HasCallStack => String -> a
error String
"never happens"
instance InductiveEnvFind' (r_ == r_') r_ m (r_' : rs) => InductiveEnvFind r_ m (r_' : rs) where
inductiveEnvDep :: InductiveEnv (r_' : rs) Identity m -> r_ m
inductiveEnvDep = forall (matches :: Bool) (r_ :: (* -> *) -> *) (m :: * -> *)
(rs :: [(* -> *) -> *]).
InductiveEnvFind' matches r_ m rs =>
InductiveEnv rs Identity m -> r_ m
inductiveEnvDep' @(r_ == r_')
class InductiveEnvFind' (matches :: Bool) r_ m rs where
inductiveEnvDep' :: InductiveEnv rs Identity m -> r_ m
instance InductiveEnvFind' True r_ m (r_ : rs) where
inductiveEnvDep' :: InductiveEnv (r_ : rs) Identity m -> r_ m
inductiveEnvDep' (AddDep (Identity r_ m
r) InductiveEnv rs Identity m
_) = r_ m
r
instance InductiveEnvFind r_ m rs => InductiveEnvFind' False r_ m (x : rs) where
inductiveEnvDep' :: InductiveEnv (x : rs) Identity m -> r_ m
inductiveEnvDep' (AddDep Identity (r_ m)
_ InductiveEnv rs Identity m
rest) = forall (r_ :: (* -> *) -> *) (m :: * -> *) (rs :: [(* -> *) -> *]).
InductiveEnvFind r_ m rs =>
InductiveEnv rs Identity m -> r_ m
inductiveEnvDep InductiveEnv rs Identity m
rest