{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}

-- | This module provides helpers for building dependency injection

-- environments composed of records.

--

-- It's not necessary when defining the record components themselves, in that

-- case "Dep.Has" should suffice.

--

-- >>> :{

-- type Logger :: (Type -> Type) -> Type

-- newtype Logger d = Logger {

--     info :: String -> d ()

--   }

-- --

-- data Repository d = Repository

--   { findById :: Int -> d (Maybe String)

--   , putById :: Int -> String -> d ()

--   , insert :: String -> d Int

--   }

-- --

-- data Controller d = Controller 

--   { create :: d Int

--   , append :: Int -> String -> d Bool 

--   , inspect :: Int -> d (Maybe String)

--   } 

-- --

-- type EnvHKD :: (Type -> Type) -> (Type -> Type) -> Type

-- data EnvHKD h m = EnvHKD

--   { logger :: h (Logger m),

--     repository :: h (Repository m),

--     controller :: h (Controller m)

--   } deriving stock Generic

--     deriving anyclass (FieldsFindableByType, DemotableFieldNames, Phased)

-- deriving via Autowired (EnvHKD Identity m) instance Autowireable r_ m (EnvHKD Identity m) => Has r_ m (EnvHKD Identity m)

-- :}

--

--

-- The module also provides a monad transformer-less way of performing dependency

-- injection, by means of 'fixEnv'.

--

module Dep.Env (
      -- * A general-purpose Has

      Has
      -- * Helpers for deriving Has

      -- ** via the default field name

    , TheDefaultFieldName (..)
      -- ** via arbitrary field name

    , TheFieldName (..)
      -- ** via autowiring

    , FieldsFindableByType (..)
    , Autowired (..)
    , Autowireable
      -- * Managing phases

    , Phased (..)
    , pullPhase
    , mapPhase
    , liftA2Phase
      -- ** Working with field names

    , DemotableFieldNames (..)
    , demoteFieldNames
    , mapPhaseWithFieldNames
      -- ** Constructing phases

      -- $phasehelpers

    , bindPhase
    , skipPhase  
      -- * Injecting dependencies by tying the knot

    , fixEnv
    , Constructor
    , constructor
      -- * Inductive environment with anonymous fields

    , InductiveEnv (..)
    , addDep
    , emptyEnv
    -- * Re-exports

    , Identity (..)
    , Constant (..)
    , Compose (..)
    ) where

import Dep.Has 
import Data.Kind
import GHC.Records
import GHC.TypeLits
import Data.Coerce
import GHC.Generics qualified as G
import Control.Applicative
import Data.Proxy
import Data.Functor ((<&>), ($>))
import Data.Functor.Compose
import Data.Functor.Constant
import Data.Functor.Identity
import Data.Function (fix)
import Data.String
import Data.Type.Equality (type (==))
import Data.Typeable

-- $setup

--

-- >>> :set -XTypeApplications

-- >>> :set -XMultiParamTypeClasses

-- >>> :set -XImportQualifiedPost

-- >>> :set -XTemplateHaskell

-- >>> :set -XStandaloneKindSignatures

-- >>> :set -XNamedFieldPuns

-- >>> :set -XFunctionalDependencies

-- >>> :set -XFlexibleContexts

-- >>> :set -XDataKinds

-- >>> :set -XBlockArguments

-- >>> :set -XFlexibleInstances

-- >>> :set -XTypeFamilies

-- >>> :set -XDeriveGeneric

-- >>> :set -XViewPatterns

-- >>> :set -XDerivingStrategies

-- >>> :set -XDerivingVia

-- >>> :set -XDeriveAnyClass

-- >>> :set -XStandaloneDeriving

-- >>> :set -XUndecidableInstances

-- >>> import Data.Kind

-- >>> import Dep.Has

-- >>> import Dep.Env

-- >>> import GHC.Generics (Generic)

--



-- via the default field name


-- | Helper for @DerivingVia@ 'HasField' instances.

--

-- It expects the component to have as field name the default fieldname

-- specified by 'Dep'.

--

-- This is the same behavior as the @DefaultSignatures@ implementation for

-- 'Has', so maybe it doesn't make much sense to use it, except for

-- explicitness.

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) = u -> r_ m
coerce (u -> r_ m) -> (env_ m -> u) -> env_ m -> r_ m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (x :: k) r a. HasField x r a => r -> a
forall r a. HasField (DefaultFieldName r_) r a => r -> a
getField @(DefaultFieldName r_) (env_ m -> r_ m) -> env_ m -> r_ m
forall a b. (a -> b) -> a -> b
$ env_ m
env

-- | Helper for @DerivingVia@ 'HasField' instances.

--

-- The field name is specified as a 'Symbol'.

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) = u -> r_ m
coerce (u -> r_ m) -> (env_ m -> u) -> env_ m -> r_ m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (x :: k) r a. HasField x r a => r -> a
forall r a. HasField name r a => r -> a
getField @name (env_ m -> r_ m) -> env_ m -> r_ m
forall a b. (a -> b) -> a -> b
$ env_ m
env

-- via autowiring


-- | Class for getting the field name from the field's type.

--

-- The default implementation of 'FindFieldByType' requires a 'G.Generic'

-- instance, but users can write their own implementations.

type FieldsFindableByType :: Type -> Constraint
class FieldsFindableByType (env :: Type) where
    type FindFieldByType env (r :: Type) :: Symbol 
    type FindFieldByType env r = FindFieldByType_ env r

-- | Helper for @DerivingVia@ 'HasField' instances.

--

-- The fields are identified by their types.

--

-- It uses 'FindFieldByType' under the hood.

--

-- __BEWARE__: for large records with many components, this technique might

-- incur in long compilation times.

type Autowired :: Type -> Type
newtype Autowired (env :: Type) = Autowired env

-- | Constraints required when @DerivingVia@ /all/ possible instances of 'Has' in

-- a single definition.

--

-- This only works for environments where all the fields come wrapped in

-- "Data.Functor.Identity".

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) = forall b. Coercible u b => u -> b
coerce @u (u -> r_ m) -> u -> r_ m
forall a b. (a -> b) -> a -> b
$ env_ m -> u
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 ExtractProduct envRep where
    ExtractProduct (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

-- The k -> Type alwasy trips me up

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
    -- Here we are saying "any wrapper whatsoever over r". Too general?

    -- If the wrapper is not coercible to the underlying r, we'll fail later.

    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

--

--

-- Managing Phases


-- see also https://github.com/haskell/cabal/issues/7394#issuecomment-861767980


-- | Class of 2-parameter environments for which the first parameter @h@ wraps

-- each field and corresponds to phases in the construction of the environment,

-- and the second parameter @m@ is the effect monad used by each component.

--

-- @h@ will typically be a composition of applicative functors, each one

-- representing a phase. We advance through the phases by \"pulling out\" the

-- outermost phase and running it in some way, until we are are left with a

-- 'Constructor' phase, which we can remove using 'fixEnv'.

--

-- 'Phased' resembles [FunctorT, TraversableT and ApplicativeT](https://hackage.haskell.org/package/barbies-2.0.3.0/docs/Data-Functor-Transformer.html) from the [barbies](https://hackage.haskell.org/package/barbies) library. 'Phased' instances can be written in terms of them.

type Phased :: ((Type -> Type) -> (Type -> Type) -> Type) -> Constraint
class Phased (env_ :: (Type -> Type) -> (Type -> Type) -> Type) where
    -- | Used to implement 'pullPhase' and 'mapPhase',  typically you should use those functions instead.

    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 . 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 . h x -> f (g x)) -> env_ h m -> f (env_ g m)
    traverseH forall x. h x -> f (g x)
t env_ h m
env = Rep (env_ g m) Any -> env_ g m
forall a x. Generic a => Rep a x -> a
G.to (Rep (env_ g m) Any -> env_ g m)
-> f (Rep (env_ g m) Any) -> f (env_ g m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall x. h x -> f (g x))
-> Rep (env_ h m) Any -> f (Rep (env_ g m) Any)
forall k k (h :: k -> *) (g :: k -> *) (env :: k -> *)
       (env' :: k -> *) (f :: * -> *) (x :: k).
(GTraverseH h g env env', Applicative f) =>
(forall (x :: k). h x -> f (g x)) -> env x -> f (env' x)
gTraverseH forall x. h x -> f (g x)
t (env_ h m -> Rep (env_ h m) Any
forall a x. Generic a => a -> Rep a x
G.from env_ h m
env)
    -- | Used to implement 'liftA2Phase', typically you should use that function instead.

    liftA2H
        :: forall (a :: Type -> Type) (f :: Type -> Type) (f' :: Type -> Type) (m :: Type -> Type) .
        ( Typeable a
        , Typeable f
        , Typeable f'
        , Typeable m
        )
        => 
        (forall 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. a x -> f x -> f' x) -> env_ a m -> env_ f m -> env_ f' m
    liftA2H forall x. a x -> f x -> f' x
f env_ a m
enva env_ f m
env = Rep (env_ f' m) Any -> env_ f' m
forall a x. Generic a => Rep a x -> a
G.to ((forall x. a x -> f x -> f' x)
-> Rep (env_ a m) Any -> Rep (env_ f m) Any -> Rep (env_ f' m) Any
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). a r -> f r -> f' r) -> enva x -> env x -> env' x
gLiftA2Phase forall x. a x -> f x -> f' x
f (env_ a m -> Rep (env_ a m) Any
forall a x. Generic a => a -> Rep a x
G.from env_ a m
enva) (env_ f m -> Rep (env_ f m) Any
forall a x. Generic a => a -> Rep a x
G.from env_ f m
env))

-- | Take the outermost phase wrapping each component and \"pull it outwards\",

-- aggregating the phase's applicative effects.

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)
-- f first to help annotate the phase

pullPhase :: env_ (Compose f g) m -> f (env_ g m)
pullPhase = (forall x. Compose f g x -> f (g x))
-> env_ (Compose f g) m -> f (env_ g m)
forall (env_ :: (* -> *) -> (* -> *) -> *) (h :: * -> *)
       (f :: * -> *) (g :: * -> *) (m :: * -> *).
(Phased env_, Applicative f, Typeable f, Typeable g, Typeable h,
 Typeable m) =>
(forall x. h x -> f (g x)) -> env_ h m -> f (env_ g m)
traverseH @env_ forall x. Compose f g x -> f (g x)
forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose

-- | Modify the outermost phase wrapping each component.

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. f x -> f' x) 
         -> 
         -- |

         env_ (Compose f g) m 
         -> 
         -- |

         env_ (Compose f' g) m
-- f' first to help annotate the *target* of the transform?

mapPhase :: (forall x. f x -> f' x)
-> env_ (Compose f g) m -> env_ (Compose f' g) m
mapPhase forall x. f x -> f' x
f env_ (Compose f g) m
env = Identity (env_ (Compose f' g) m) -> env_ (Compose f' g) m
forall a. Identity a -> a
runIdentity (Identity (env_ (Compose f' g) m) -> env_ (Compose f' g) m)
-> Identity (env_ (Compose f' g) m) -> env_ (Compose f' g) m
forall a b. (a -> b) -> a -> b
$ (forall x. Compose f g x -> Identity (Compose f' g x))
-> env_ (Compose f g) m -> Identity (env_ (Compose f' g) m)
forall (env_ :: (* -> *) -> (* -> *) -> *) (h :: * -> *)
       (f :: * -> *) (g :: * -> *) (m :: * -> *).
(Phased env_, Applicative f, Typeable f, Typeable g, Typeable h,
 Typeable m) =>
(forall x. h x -> f (g x)) -> env_ h m -> f (env_ g m)
traverseH @env_ (\(Compose fg) -> Compose f' g x -> Identity (Compose f' g x)
forall a. a -> Identity a
Identity (f' (g x) -> Compose f' g x
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (g x) -> f' (g x)
forall x. f x -> f' x
f f (g x)
fg))) env_ (Compose f g) m
env

-- | Combine two environments with a function that works on their outermost phases.

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. a x -> f x -> f' x) 
    -> 
    -- |

    env_ (Compose a g) m 
    -> 
    -- |

    env_ (Compose f g) m 
    -> 
    -- |

    env_ (Compose f' g) m
-- f' first to help annotate the *target* of the transform?

liftA2Phase :: (forall 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. a x -> f x -> f' x
f = (forall x. Compose a g x -> Compose f g x -> Compose f' g x)
-> env_ (Compose a g) m
-> env_ (Compose f g) m
-> env_ (Compose f' g) m
forall (env_ :: (* -> *) -> (* -> *) -> *) (a :: * -> *)
       (f :: * -> *) (f' :: * -> *) (m :: * -> *).
(Phased env_, Typeable a, Typeable f, Typeable f', Typeable m) =>
(forall x. a x -> f x -> f' x) -> env_ a m -> env_ f m -> env_ f' m
liftA2H @env_ (\(Compose fa) (Compose fg) -> f' (g x) -> Compose f' g x
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (a (g x) -> f (g x) -> f' (g x)
forall 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 . 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 (x :: k). h x -> f (g x))
-> D1 metaData (C1 metaCons fields) x
-> f (D1 metaData (C1 metaCons fields') x)
gTraverseH forall (x :: k). h x -> f (g x)
t (G.M1 (G.M1 fields x
fields)) = 
        M1 C metaCons fields' x -> D1 metaData (C1 metaCons fields') x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (M1 C metaCons fields' x -> D1 metaData (C1 metaCons fields') x)
-> (fields' x -> M1 C metaCons fields' x)
-> fields' x
-> D1 metaData (C1 metaCons fields') x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. fields' x -> M1 C metaCons fields' x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (fields' x -> D1 metaData (C1 metaCons fields') x)
-> f (fields' x) -> f (D1 metaData (C1 metaCons fields') x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: k). h x -> f (g x)) -> fields x -> f (fields' x)
forall k k (h :: k -> *) (g :: k -> *) (env :: k -> *)
       (env' :: k -> *) (f :: * -> *) (x :: k).
(GTraverseH h g env env', Applicative f) =>
(forall (x :: k). h x -> f (g x)) -> env x -> f (env' x)
gTraverseH @h @g forall (x :: k). 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 (x :: k). h x -> f (g x))
-> (:*:) left right x -> f ((:*:) left' right' x)
gTraverseH forall (x :: k). h x -> f (g x)
t (left x
left G.:*: right x
right) = 
        let left' :: f (left' x)
left' = (forall (x :: k). h x -> f (g x)) -> left x -> f (left' x)
forall k k (h :: k -> *) (g :: k -> *) (env :: k -> *)
       (env' :: k -> *) (f :: * -> *) (x :: k).
(GTraverseH h g env env', Applicative f) =>
(forall (x :: k). h x -> f (g x)) -> env x -> f (env' x)
gTraverseH @h @g forall (x :: k). h x -> f (g x)
t left x
left
            right' :: f (right' x)
right' = (forall (x :: k). h x -> f (g x)) -> right x -> f (right' x)
forall k k (h :: k -> *) (g :: k -> *) (env :: k -> *)
       (env' :: k -> *) (f :: * -> *) (x :: k).
(GTraverseH h g env env', Applicative f) =>
(forall (x :: k). h x -> f (g x)) -> env x -> f (env' x)
gTraverseH @h @g forall (x :: k). h x -> f (g x)
t right x
right
         in (left' x -> right' x -> (:*:) left' right' x)
-> f (left' x) -> f (right' x) -> f ((:*:) left' right' x)
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 left' x -> right' x -> (:*:) left' right' x
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 GTraverseH h g (G.S1 metaSel (G.Rec0 (h bean))) 
                   (G.S1 metaSel (G.Rec0 (g bean))) where
     gTraverseH :: (forall (x :: k). h x -> f (g x))
-> S1 metaSel (Rec0 (h bean)) x -> f (S1 metaSel (Rec0 (g bean)) x)
gTraverseH forall (x :: k). h x -> f (g x)
t (G.M1 (G.K1 (h bean
hbean))) =
         K1 R (g bean) x -> S1 metaSel (Rec0 (g bean)) x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (K1 R (g bean) x -> S1 metaSel (Rec0 (g bean)) x)
-> (g bean -> K1 R (g bean) x)
-> g bean
-> S1 metaSel (Rec0 (g bean)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g bean -> K1 R (g bean) x
forall k i c (p :: k). c -> K1 i c p
G.K1 (g bean -> S1 metaSel (Rec0 (g bean)) x)
-> f (g bean) -> f (S1 metaSel (Rec0 (g bean)) x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> h bean -> f (g bean)
forall (x :: k). 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. 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 (r :: k). 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). a r -> f r -> f' r
f (G.M1 (G.M1 fieldsa x
fieldsa)) (G.M1 (G.M1 fields x
fields)) = 
        M1 C metaCons fields' x -> D1 metaData (C1 metaCons fields') x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (fields' x -> M1 C metaCons fields' x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 ((forall (r :: k). a r -> f r -> f' r)
-> fieldsa x -> fields x -> fields' x
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). a r -> f r -> f' r) -> enva x -> env x -> env' x
gLiftA2Phase @a @f @f' forall (r :: k). 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 (r :: k). a r -> f r -> f' r)
-> (:*:) lefta righta x
-> (:*:) left right x
-> (:*:) left' right' x
gLiftA2Phase forall (r :: k). 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 (r :: k). a r -> f r -> f' r)
-> lefta x -> left x -> left' x
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). a r -> f r -> f' r) -> enva x -> env x -> env' x
gLiftA2Phase @a @f @f' forall (r :: k). a r -> f r -> f' r
f lefta x
lefta left x
left
            right' :: right' x
right' = (forall (r :: k). a r -> f r -> f' r)
-> righta x -> right x -> right' x
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). a r -> f r -> f' r) -> enva x -> env x -> env' x
gLiftA2Phase @a @f @f' forall (r :: k). a r -> f r -> f' r
f righta x
righta right x
right
         in left' x -> right' x -> (:*:) left' right' x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
(G.:*:) left' x
left' right' x
right'

instance   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 (r :: k). 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). a r -> f r -> f' r
f (G.M1 (G.K1 a bean
abean)) (G.M1 (G.K1 f bean
fgbean)) =
         K1 R (f' bean) x -> S1 metaSel (Rec0 (f' bean)) x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (f' bean -> K1 R (f' bean) x
forall k i c (p :: k). c -> K1 i c p
G.K1 (a bean -> f bean -> f' bean
forall (r :: k). a r -> f r -> f' r
f a bean
abean f bean
fgbean))

-- | Class of 2-parameter environments for which it's possible to obtain the

-- names of each field as values.

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 = Rep (env_ (h String) m) Any -> env_ (h String) m
forall a x. Generic a => Rep a x -> a
G.to ((forall x. String -> h String x) -> Rep (env_ (h String) m) Any
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)

-- | Bring down the field names of the environment to the term level and store

-- them in the accumulator of "Data.Functor.Constant".

demoteFieldNames :: forall env_ m . DemotableFieldNames env_ => env_ (Constant String) m
demoteFieldNames :: env_ (Constant String) m
demoteFieldNames = (forall x. String -> Constant String x) -> env_ (Constant String) m
forall (env_ :: (* -> *) -> (* -> *) -> *) (h :: * -> * -> *)
       (m :: * -> *).
DemotableFieldNames env_ =>
(forall x. String -> h String x) -> env_ (h String) m
demoteFieldNamesH forall x. String -> Constant String x
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). String -> h String x)
-> D1 metaData (C1 metaCons fields) x
gDemoteFieldNamesH forall (x :: k). String -> h String x
f = M1 C metaCons fields x -> D1 metaData (C1 metaCons fields) x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (fields x -> M1 C metaCons fields x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 ((forall (x :: k). String -> h String x) -> fields x
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). String -> h String x) -> (:*:) left right x
gDemoteFieldNamesH forall (x :: k). String -> h String x
f = 
         (forall (x :: k). String -> h String x) -> left x
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 left x -> right x -> (:*:) left right x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
G.:*: (forall (x :: k). String -> h String x) -> right x
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). 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 = 
         K1 R (h String bean) x
-> S1 ('MetaSel ('Just name) u v w) (Rec0 (h String bean)) x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (h String bean -> K1 R (h String bean) x
forall k i c (p :: k). c -> K1 i c p
G.K1 (String -> h String bean
forall (x :: k). String -> h String x
f (Proxy name -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (Proxy name
forall k (t :: k). Proxy t
Proxy @name))))

-- | Modify the outermost phase wrapping each component, while having access to

-- the field name of the component.

--

-- A typical usage is modifying a \"parsing the configuration\" phase so that

-- each component looks into a different section of the global configuration

-- field.

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. String -> f x -> f' x) 
    -> 
    -- |

    env_ (Compose f g) m 
    -> 
    -- |

    env_ (Compose f' g) m
-- f' first to help annotate the *target* of the transform?

mapPhaseWithFieldNames :: (forall x. String -> f x -> f' x)
-> env_ (Compose f g) m -> env_ (Compose f' g) m
mapPhaseWithFieldNames  forall x. String -> f x -> f' x
f env_ (Compose f g) m
env =
    (forall x. Constant String x -> f x -> f' x)
-> env_ (Compose (Constant String) g) m
-> env_ (Compose f g) m
-> env_ (Compose f' g) m
forall (a :: * -> *) (f' :: * -> *) (f :: * -> *) (g :: * -> *)
       (m :: * -> *) (env_ :: (* -> *) -> (* -> *) -> *).
(Phased env_, Typeable a, Typeable f, Typeable f', Typeable g,
 Typeable m) =>
(forall x. a x -> f x -> f' x)
-> env_ (Compose a g) m
-> env_ (Compose f g) m
-> env_ (Compose f' g) m
liftA2Phase (\(Constant name) f x
z -> String -> f x -> f' x
forall x. String -> f x -> f' x
f String
name f x
z) (Identity (env_ (Compose (Constant String) g) m)
-> env_ (Compose (Constant String) g) m
forall a. Identity a -> a
runIdentity (Identity (env_ (Compose (Constant String) g) m)
 -> env_ (Compose (Constant String) g) m)
-> Identity (env_ (Compose (Constant String) g) m)
-> env_ (Compose (Constant String) g) m
forall a b. (a -> b) -> a -> b
$ (forall x.
 Constant String x -> Identity (Compose (Constant String) g x))
-> env_ (Constant String) m
-> Identity (env_ (Compose (Constant String) g) m)
forall (env_ :: (* -> *) -> (* -> *) -> *) (h :: * -> *)
       (f :: * -> *) (g :: * -> *) (m :: * -> *).
(Phased env_, Applicative f, Typeable f, Typeable g, Typeable h,
 Typeable m) =>
(forall x. h x -> f (g x)) -> env_ h m -> f (env_ g m)
traverseH @env_ (\(Constant z) -> Compose (Constant String) g x
-> Identity (Compose (Constant String) g x)
forall a. a -> Identity a
Identity (Constant String (g x) -> Compose (Constant String) g x
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (String -> Constant String (g x)
forall k a (b :: k). a -> Constant a b
Constant String
z))) env_ (Constant String) m
forall (env_ :: (* -> *) -> (* -> *) -> *) (m :: * -> *).
DemotableFieldNames env_ =>
env_ (Constant String) m
demoteFieldNames) env_ (Compose f g) m
env


-- constructing phases


-- $phasehelpers

--

-- Small convenience functions to help build nested compositions of functors.

--


-- | Use the result of the previous phase to build the next one.

--

-- Can be useful infix.

bindPhase :: forall f g a b . Functor f => f a -> (a -> g b) -> Compose f g b 
-- f as first type parameter to help annotate the current phase

bindPhase :: f a -> (a -> g b) -> Compose f g b
bindPhase f a
f a -> g b
k = f (g b) -> Compose f g b
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f a
f f a -> (a -> g b) -> f (g b)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> a -> g b
k)

-- | Don't do anything for the current phase, just wrap the next one.

skipPhase :: forall f g a . Applicative f => g a -> Compose f g a 
-- f as first type parameter to help annotate the current phase

skipPhase :: g a -> Compose f g a
skipPhase g a
g = f (g a) -> Compose f g a
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (g a -> f (g a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure g a
g)

-- | A phase with the effect of \"constructing each component by reading its

-- dependencies from a completed environment\". 

--

-- The 'Constructor' phase for an environment will typically be parameterized

-- with the environment itself.

type Constructor (env :: Type) = ((->) env) `Compose` Identity


-- | Turn an environment-consuming function into a 'Constructor' that can be slotted 

-- into some field of a 'Phased' environment.

constructor :: forall r_ m env . (env -> r_ m) -> Constructor env (r_ m)
-- same order of type parameters as Has

constructor :: (env -> r_ m) -> Constructor env (r_ m)
constructor = (env -> r_ m) -> Constructor env (r_ m)
coerce

-- | This is a method of performing dependency injection that doesn't require

-- "Control.Monad.Dep.DepT" at all. In fact, it doesn't require the use of

-- /any/ monad transformer!

--

-- If we have a environment whose fields are functions that construct each

-- component by searching for its dependencies in a \"fully built\" version of

-- the environment, we can \"tie the knot\" to obtain the \"fully built\"

-- environment. This works as long as there aren't any circular dependencies

-- between components.

--

-- Think of it as a version of "Data.Function.fix" that, instead of \"tying\" a single

-- function, ties a whole record of them.

--

-- The @env_ (Constructor env_ m) m@ parameter might be the result of peeling

-- away successive layers of applicative functor composition using 'pullPhase',

-- until only the wiring phase remains.

fixEnv :: (Phased env_, Typeable env_, Typeable m) => env_ (Constructor (env_ Identity m) ) m -> env_ Identity m
fixEnv :: env_ (Constructor (env_ Identity m)) m -> env_ Identity m
fixEnv env_ (Constructor (env_ Identity m)) m
env = (env_ Identity m -> env_ Identity m) -> env_ Identity m
forall a. (a -> a) -> a
fix (env_ (Constructor (env_ Identity m)) m
-> env_ Identity m -> env_ Identity m
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)

-- | An inductively constructed environment with anonymous fields.

--

-- Can be useful for simple tests, and also for converting `Has`-based

-- components into functions that take their dependencies as separate

-- positional parameters.

--

-- > makeController :: (Monad m, Has Logger m env, Has Repository m env) => env -> Controller m

-- > makeController = undefined

-- > makeControllerPositional :: Monad m => Logger m -> Repository m -> Controller m

-- > makeControllerPositional a b = makeController $ addDep @Logger a $ addDep @Repository b $ emptyEnv

-- 

--

--

data InductiveEnv (rs :: [(Type -> Type) -> Type]) (h :: Type -> Type) (m :: Type -> Type) where
    AddDep :: forall r_ m rs h . h (r_ m) -> InductiveEnv rs h m -> InductiveEnv (r_ : rs) h m
    EmptyEnv :: forall m h . InductiveEnv '[] h m

-- | Unlike the 'AddDep' constructor, this sets @h@ to 'Identity'.

addDep :: forall r_ m rs . r_ m -> InductiveEnv rs Identity m -> InductiveEnv (r_ : rs) Identity m
addDep :: r_ m
-> InductiveEnv rs Identity m -> InductiveEnv (r_ : rs) Identity m
addDep = forall (h :: * -> *).
h (r_ m) -> InductiveEnv rs h m -> InductiveEnv (r_ : rs) h m
forall (r_ :: (* -> *) -> *) (m :: * -> *) (rs :: [(* -> *) -> *])
       (h :: * -> *).
h (r_ m) -> InductiveEnv rs h m -> InductiveEnv (r_ : rs) h m
AddDep @r_ @m @rs (Identity (r_ m)
 -> InductiveEnv rs Identity m -> InductiveEnv (r_ : rs) Identity m)
-> (r_ m -> Identity (r_ m))
-> r_ m
-> InductiveEnv rs Identity m
-> InductiveEnv (r_ : rs) Identity m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. r_ m -> Identity (r_ m)
forall a. a -> Identity a
Identity

-- | Unlike the 'EmptyEnv' constructor, this sets @h@ to 'Identity'.

emptyEnv :: forall m . InductiveEnv '[] Identity m
emptyEnv :: InductiveEnv '[] Identity m
emptyEnv = InductiveEnv '[] Identity m
forall (m :: * -> *) (h :: * -> *). InductiveEnv '[] h m
EmptyEnv @m @Identity

instance Phased (InductiveEnv rs) where
    traverseH :: (forall x. h x -> f (g x))
-> InductiveEnv rs h m -> f (InductiveEnv rs g m)
traverseH forall x. h x -> f (g x)
t InductiveEnv rs h m
EmptyEnv = InductiveEnv '[] g m -> f (InductiveEnv '[] g m)
forall (f :: * -> *) a. Applicative f => a -> f a
pure InductiveEnv '[] g m
forall (m :: * -> *) (h :: * -> *). InductiveEnv '[] h m
EmptyEnv
    traverseH forall x. h x -> f (g x)
t (AddDep h (r_ m)
hx InductiveEnv rs h m
rest) = 
        let headF :: f (g (r_ m))
headF = h (r_ m) -> f (g (r_ m))
forall x. h x -> f (g x)
t h (r_ m)
hx
            restF :: f (InductiveEnv rs g m)
restF = (forall x. h x -> f (g x))
-> InductiveEnv rs h m -> f (InductiveEnv rs g m)
forall (env_ :: (* -> *) -> (* -> *) -> *) (h :: * -> *)
       (f :: * -> *) (g :: * -> *) (m :: * -> *).
(Phased env_, Applicative f, Typeable f, Typeable g, Typeable h,
 Typeable m) =>
(forall x. h x -> f (g x)) -> env_ h m -> f (env_ g m)
traverseH forall x. h x -> f (g x)
t InductiveEnv rs h m
rest
         in g (r_ m) -> InductiveEnv rs g m -> InductiveEnv (r_ : rs) g m
forall (r_ :: (* -> *) -> *) (m :: * -> *) (rs :: [(* -> *) -> *])
       (h :: * -> *).
h (r_ m) -> InductiveEnv rs h m -> InductiveEnv (r_ : rs) h m
AddDep (g (r_ m) -> InductiveEnv rs g m -> InductiveEnv (r_ : rs) g m)
-> f (g (r_ m))
-> f (InductiveEnv rs g m -> InductiveEnv (r_ : rs) g m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (g (r_ m))
headF f (InductiveEnv rs g m -> InductiveEnv (r_ : rs) g m)
-> f (InductiveEnv rs g m) -> f (InductiveEnv (r_ : rs) g m)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f (InductiveEnv rs g m)
restF
    liftA2H :: (forall x. a x -> f x -> f' x)
-> InductiveEnv rs a m
-> InductiveEnv rs f m
-> InductiveEnv rs f' m
liftA2H forall x. a x -> f x -> f' x
t InductiveEnv rs a m
EmptyEnv InductiveEnv rs f m
EmptyEnv = InductiveEnv rs f' m
forall (m :: * -> *) (h :: * -> *). InductiveEnv '[] h m
EmptyEnv
    liftA2H forall 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) = 
        f' (r_ m) -> InductiveEnv rs f' m -> InductiveEnv (r_ : rs) f' m
forall (r_ :: (* -> *) -> *) (m :: * -> *) (rs :: [(* -> *) -> *])
       (h :: * -> *).
h (r_ m) -> InductiveEnv rs h m -> InductiveEnv (r_ : rs) h m
AddDep (a (r_ m) -> f (r_ m) -> f' (r_ m)
forall x. a x -> f x -> f' x
t a (r_ m)
ax f (r_ m)
f (r_ m)
hx) ((forall x. a x -> f x -> f' x)
-> InductiveEnv rs a m
-> InductiveEnv rs f m
-> InductiveEnv rs f' m
forall (env_ :: (* -> *) -> (* -> *) -> *) (a :: * -> *)
       (f :: * -> *) (f' :: * -> *) (m :: * -> *).
(Phased env_, Typeable a, Typeable f, Typeable f', Typeable m) =>
(forall x. a x -> f x -> f' x) -> env_ a m -> env_ f m -> env_ f' m
liftA2H forall x. a x -> f x -> f' x
t InductiveEnv rs a m
arest InductiveEnv rs f m
InductiveEnv rs f m
hrest)
 
-- | Works by searching on the list of types.

instance InductiveEnvFind r_ m rs => Has r_ m (InductiveEnv rs Identity m) where
    dep :: InductiveEnv rs Identity m -> r_ m
dep = InductiveEnv rs Identity m -> r_ m
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 = String -> InductiveEnv '[] Identity m -> r_ m
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
forall (r_ :: (* -> *) -> *) (m :: * -> *) (rs :: [(* -> *) -> *]).
InductiveEnvFind' (r_ == r_') 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_ 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) = InductiveEnv rs Identity m -> r_ m
forall (r_ :: (* -> *) -> *) (m :: * -> *) (rs :: [(* -> *) -> *]).
InductiveEnvFind r_ m rs =>
InductiveEnv rs Identity m -> r_ m
inductiveEnvDep InductiveEnv rs Identity m
rest