{-# 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,
InductiveEnv (..),
addDep,
emptyEnv,
Phased (..),
liftAH,
pullPhase,
mapPhase,
liftA2Phase,
DemotableFieldNames (..),
demoteFieldNames,
mapPhaseWithFieldNames,
bindPhase,
skipPhase,
Bare,
fromBare,
toBare,
fixEnv,
Constructor,
constructor,
fixEnvAccum,
AccumConstructor,
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
import Dep.Phases hiding ((>>=), (>>))
newtype TheDefaultFieldName (env :: Type) = TheDefaultFieldName env
{-# DEPRECATED TheDefaultFieldName "more intrusive than useful" #-}
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
{-# DEPRECATED DemotableFieldNames "using the field names directly is usually a bad idea" #-}
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)
{-# DEPRECATED demoteFieldNames "using the field names directly is usually a bad idea" #-}
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))))
{-# DEPRECATED mapPhaseWithFieldNames "using the field names directly is usually a bad idea" #-}
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)
{-# DEPRECATED skipPhase "use pure () in combination with bindPhase" #-}
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
{-# DEPRECATED Constructor "use the one in Dep.Constructor" #-}
type Constructor (env :: Type) = ((->) env) `Compose` Identity
{-# DEPRECATED constructor "use the one in Dep.Constructor" #-}
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
{-# DEPRECATED AccumConstructor "use the one in Dep.Constructor" #-}
type AccumConstructor (w :: Type) (env :: Type) = (->) (w, env) `Compose` (,) w `Compose` Identity
{-# DEPRECATED fixEnv "use the one in Dep.Constructor" #-}
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)
{-# DEPRECATED fixEnvAccum "use the one in Dep.Constructor" #-}
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