{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE UndecidableInstances #-}

-- This Source Code Form is subject to the terms of the Mozilla Public
-- License, v. 2.0. If a copy of the MPL was not distributed with this
-- file, You can obtain one at https://mozilla.org/MPL/2.0/.

{- |
Copyright   :  (c) 2023-2024 Yamada Ryo
License     :  MPL-2.0 (see the file LICENSE)
Maintainer  :  ymdfield@outlook.jp
Stability   :  experimental
Portability :  portable

A Hefty carrier that can be used as a handler for effect systems based
on [@data-effects@](https://hackage.haskell.org/package/data-effects).
-}
module Control.Effect.Hefty where

import Control.Arrow ((>>>))
import Control.Effect (type (~>))
import Control.Effect.Key (sendInsBy, sendSigBy)
import Control.Freer (Freer, InjectIns, InjectInsBy, injectIns, injectInsBy, interpretFreer, liftIns, transformFreer)
import Control.Hefty (Hefty (Hefty), InjectSig, InjectSigBy, injectSig, injectSigBy, overHefty, unHefty)
import Control.Monad.Cont (Cont, ContT (ContT), lift, runContT)
import Control.Monad.Freer (MonadFreer, interpretFreerK)
import Control.Monad.Identity (Identity (Identity), runIdentity)
import Control.Monad.Trans (MonadTrans)
import Data.Coerce (coerce)
import Data.Effect (LiftIns (LiftIns), Nop, SigClass, unliftIns)
import Data.Effect.HFunctor (HFunctor, caseH, hfmap, (:+:) (Inl, Inr))
import Data.Effect.Key (Key (Key), KeyH (KeyH), unKey, unKeyH, type (##>), type (#>))
import Data.Effect.Tag (Tag (Tag, unTag), TagH (TagH, unTagH), type (#), type (##))
import Data.Free.Sum (caseF, pattern L1, pattern R1, type (+))
import Data.Hefty.Union (
    HFunctorUnion,
    HFunctorUnion_ (ForallHFunctor),
    HasMembershipRec,
    HeadIns,
    LiftInsIfSingle (liftInsIfSingle, unliftInsIfSingle),
    Lookup,
    Member,
    MemberBy,
    MemberH,
    MemberHBy,
    MemberRec,
    U,
    UH,
    Union (HasMembership, exhaust, inject0, weaken, weakenUnder, (|+:)),
    UnliftIfSingle,
    flipUnion,
    flipUnion3,
    flipUnionUnder,
    injectRec,
    projectRec,
    weaken2,
    weaken2Under,
    weaken2Under2,
    weaken3,
    weaken3Under,
    weaken4,
    weakenUnder2,
    weakenUnder3,
    (|+),
 )
import Data.Hefty.Union.Strengthen (Strengthen, StrengthenUnder, strengthenN, strengthenNUnderM)
import Data.Hefty.Union.Weaken (Weaken, WeakenUnder, weakenN, weakenNUnderM)
import Data.Kind (Type)
import Data.Maybe.Singletons (FromJust)

{- |
A common type for representing first-order and higher-order extensible effectful programs that can
issue effects belonging to the specified list of effect classes.
-}
type Eff u fr ehs efs = Hefty fr (EffUnion u ehs efs)

{- |
A common type for representing first-order and higher-order extensible effectful programs that can
issue effects belonging to the specified sum of effect classes.
-}
type Effectful u fr eh ef = Eff u fr (UH u eh) (U u ef)

{- |
A common wrapper data type for representing first-order and higher-order extensible effect union.
-}
newtype EffUnion (u :: [SigClass] -> SigClass) ehs efs f a = EffUnion
    {forall (u :: [SigClass] -> SigClass) (ehs :: [SigClass])
       (efs :: [SigClass]) (f :: * -> *) a.
EffUnion u ehs efs f a -> (+) (u ehs f) (u efs Nop) a
unEffUnion :: (u ehs f + u efs Nop) a}

caseHF :: (u ehs f a -> r) -> (u efs Nop a -> r) -> EffUnion u ehs efs f a -> r
caseHF :: forall (u :: [SigClass] -> SigClass) (ehs :: [SigClass])
       (f :: * -> *) a r (efs :: [SigClass]).
(u ehs f a -> r)
-> (u efs Nop a -> r) -> EffUnion u ehs efs f a -> r
caseHF u ehs f a -> r
f u efs Nop a -> r
g = forall {k} (f :: k -> *) (a :: k) r (g :: k -> *).
(f a -> r) -> (g a -> r) -> (+) f g a -> r
caseF u ehs f a -> r
f u efs Nop a -> r
g forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [SigClass] -> SigClass) (ehs :: [SigClass])
       (efs :: [SigClass]) (f :: * -> *) a.
EffUnion u ehs efs f a -> (+) (u ehs f) (u efs Nop) a
unEffUnion

instance HFunctor (u ehs) => HFunctor (EffUnion u ehs efs) where
    hfmap :: forall (f :: * -> *) (g :: * -> *).
(f :-> g) -> EffUnion u ehs efs f :-> EffUnion u ehs efs g
hfmap f :-> g
f = forall (u :: [SigClass] -> SigClass) (ehs :: [SigClass])
       (efs :: [SigClass]) (f :: * -> *) a.
(+) (u ehs f) (u efs Nop) a -> EffUnion u ehs efs f a
EffUnion forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k) r (g :: k -> *).
(f a -> r) -> (g a -> r) -> (+) f g a -> r
caseF (forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (h :: SigClass) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap f :-> g
f) forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [SigClass] -> SigClass) (ehs :: [SigClass])
       (efs :: [SigClass]) (f :: * -> *) a.
EffUnion u ehs efs f a -> (+) (u ehs f) (u efs Nop) a
unEffUnion
    {-# INLINE hfmap #-}

instance MemberRec u (LiftIns e) efs => InjectIns e (EffUnion u ehs efs f) where
    injectIns :: e ~> EffUnion u ehs efs f
injectIns = forall (u :: [SigClass] -> SigClass) (ehs :: [SigClass])
       (efs :: [SigClass]) (f :: * -> *) a.
(+) (u ehs f) (u efs Nop) a -> EffUnion u ehs efs f a
EffUnion forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [SigClass] -> SigClass) (e :: SigClass)
       (es :: [SigClass]) (f :: * -> *).
MemberRec u e es =>
e f ~> u es f
injectRec forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (ins :: * -> *) (f :: * -> *) a. ins a -> LiftIns ins f a
LiftIns
    {-# INLINE injectIns #-}

instance MemberRec u e ehs => InjectSig e (EffUnion u ehs efs) where
    injectSig :: forall (f :: * -> *). e f ~> EffUnion u ehs efs f
injectSig = forall (u :: [SigClass] -> SigClass) (ehs :: [SigClass])
       (efs :: [SigClass]) (f :: * -> *) a.
(+) (u ehs f) (u efs Nop) a -> EffUnion u ehs efs f a
EffUnion forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [SigClass] -> SigClass) (e :: SigClass)
       (es :: [SigClass]) (f :: * -> *).
MemberRec u e es =>
e f ~> u es f
injectRec
    {-# INLINE injectSig #-}

type HasMembershipF u e efs = HasMembership u (LiftIns e) efs

infixr 3 $
infixr 4 $$

-- | Type-level infix applcation for functors.
type (f :: Type -> Type) $ a = f a

-- | Type-level infix applcation for higher-order functors.
type (h :: (Type -> Type) -> Type -> Type) $$ f = h f

type Elab e f = e f ~> f

injectH :: (Freer c f, HFunctor (u ehs)) => u ehs (Eff u f ehs efs) ~> Eff u f ehs efs
injectH :: forall (c :: (* -> *) -> Constraint) (f :: SigClass)
       (u :: [SigClass] -> SigClass) (ehs :: [SigClass])
       (efs :: [SigClass]).
(Freer c f, HFunctor (u ehs)) =>
u ehs (Eff u f ehs efs) ~> Eff u f ehs efs
injectH = forall (f :: SigClass) (e :: SigClass) a.
f (e (Hefty f e)) a -> Hefty f e a
Hefty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: (* -> *) -> Constraint) (f :: SigClass) (e :: * -> *)
       a.
Freer c f =>
e a -> f e a
liftIns forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [SigClass] -> SigClass) (ehs :: [SigClass])
       (efs :: [SigClass]) (f :: * -> *) a.
(+) (u ehs f) (u efs Nop) a -> EffUnion u ehs efs f a
EffUnion forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1
{-# INLINE injectH #-}

injectF :: Freer c f => u efs Nop ~> Eff u f ehs efs
injectF :: forall (c :: (* -> *) -> Constraint) (f :: SigClass)
       (u :: [SigClass] -> SigClass) (efs :: [SigClass])
       (ehs :: [SigClass]).
Freer c f =>
u efs Nop ~> Eff u f ehs efs
injectF = forall (f :: SigClass) (e :: SigClass) a.
f (e (Hefty f e)) a -> Hefty f e a
Hefty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: (* -> *) -> Constraint) (f :: SigClass) (e :: * -> *)
       a.
Freer c f =>
e a -> f e a
liftIns forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [SigClass] -> SigClass) (ehs :: [SigClass])
       (efs :: [SigClass]) (f :: * -> *) a.
(+) (u ehs f) (u efs Nop) a -> EffUnion u ehs efs f a
EffUnion forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1
{-# INLINE injectF #-}

{-  all types of interpret-family functions:
        - interpret   :                 e  ~> E r           ->    E (e + r)  ~> E r
        - reinterpret :                 e1 ~> E (e2 + r)    ->    E (e1 + r) ~> E (e2 + r)
        - interpose   :  e <| es  =>    e  ~> E es          ->    E es       ~> E es

        all possible suffix patterns of interpret functions:
            { <none> , K , ContT , Fin , T } x { <none> , H , FH }
            - Rec
            - RecH
            - RecFH

        all possible suffix patterns of interpret-family functions (except 'interpret'):
            - <none>
            - K
            - ContT
            - Fin ('interpose' only)
            - T
            - Rec
            - RecH
            - RecFH

    all types of transform-family functions:
        - transform :                  e1 ~> e2    ->    E (e1 + r) ~> E (e2 + r)
        - translate :  e2 <| r   =>    e1 ~> e2    ->    E (e1 + r) ~> E r
        - rewrite   :  e  <| es  =>    e  ~> e     ->    E es       ~> E es

        all possible suffix patterns of transform-family functions:
            - <none>
            - H
            - FH

    todo patterns:
        - *FH in interpret-family ( (5+1) + 2 = 8 functions )

        + *By (for keyed effects) in interpose/translate/rewrite ( 8 + 2x3 = 14 functions )
-}

-- | Using the provided interpretation function, interpret first-order effects.
interpret ::
    forall e r ehs fr u c.
    (Freer c fr, Union u, HeadIns e) =>
    UnliftIfSingle e ~> Eff u fr ehs r ->
    Eff u fr '[] (e ': r) ~> Eff u fr ehs r
interpret :: forall (e :: SigClass) (r :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HeadIns e) =>
(UnliftIfSingle e ~> Eff u fr ehs r)
-> Eff u fr '[] (e : r) ~> Eff u fr ehs r
interpret UnliftIfSingle e ~> Eff u fr ehs r
i = forall (ehs' :: [SigClass]) (efs' :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u) =>
(u efs Nop ~> Eff u fr ehs' efs')
-> Eff u fr '[] efs ~> Eff u fr ehs' efs'
interpretAllE forall a b. (a -> b) -> a -> b
$ UnliftIfSingle e ~> Eff u fr ehs r
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (e :: * -> *) (le :: SigClass).
LiftInsIfSingle e le =>
le Nop ~> e
unliftInsIfSingle forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       a r (es :: [SigClass]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (c :: (* -> *) -> Constraint) (f :: SigClass)
       (u :: [SigClass] -> SigClass) (efs :: [SigClass])
       (ehs :: [SigClass]).
Freer c f =>
u efs Nop ~> Eff u f ehs efs
injectF
{-# INLINE interpret #-}

interpretH ::
    forall eh ehs efs fr u c.
    (Freer c fr, Union u) =>
    eh (Eff u fr '[eh] efs) ~> Eff u fr ehs efs ->
    Eff u fr '[eh] efs ~> Eff u fr ehs efs
interpretH :: forall (eh :: SigClass) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u) =>
(eh (Eff u fr '[eh] efs) ~> Eff u fr ehs efs)
-> Eff u fr '[eh] efs ~> Eff u fr ehs efs
interpretH eh (Eff u fr '[eh] efs) ~> Eff u fr ehs efs
i = forall (ehs' :: [SigClass]) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u) =>
(u ehs (Eff u fr ehs efs) ~> Eff u fr ehs' efs)
-> Eff u fr ehs efs ~> Eff u fr ehs' efs
interpretAllH forall a b. (a -> b) -> a -> b
$ eh (Eff u fr '[eh] efs) ~> Eff u fr ehs efs
i forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       a r (es :: [SigClass]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [SigClass] -> SigClass) (f :: * -> *) a x.
Union u =>
u '[] f a -> x
exhaust
{-# INLINE interpretH #-}

-- | Interpret the leading first-order effect class using delimited continuations.
interpretK ::
    forall e rs r a ehs fr u c.
    (MonadFreer c fr, Union u, HeadIns e, c (Eff u fr ehs rs)) =>
    (a -> Eff u fr ehs rs r) ->
    (forall x. (x -> Eff u fr ehs rs r) -> UnliftIfSingle e x -> Eff u fr ehs rs r) ->
    Eff u fr '[] (e ': rs) a ->
    Eff u fr ehs rs r
interpretK :: forall (e :: SigClass) (rs :: [SigClass]) r a (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, HeadIns e, c (Eff u fr ehs rs)) =>
(a -> Eff u fr ehs rs r)
-> (forall x.
    (x -> Eff u fr ehs rs r)
    -> UnliftIfSingle e x -> Eff u fr ehs rs r)
-> Eff u fr '[] (e : rs) a
-> Eff u fr ehs rs r
interpretK = forall {k} (e :: * -> *) (r :: k) (m :: k -> *) (f :: * -> *)
       (m' :: k -> *) a.
((e ~> ContT r m) -> f ~> ContT r m')
-> (a -> m' r)
-> (forall x. (x -> m r) -> e x -> m r)
-> f a
-> m' r
toInterpretKFromContT forall (e :: SigClass) (rs :: [SigClass]) r (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, HeadIns e, c (Eff u fr ehs rs)) =>
(UnliftIfSingle e ~> ContT r (Eff u fr ehs rs))
-> Eff u fr '[] (e : rs) ~> ContT r (Eff u fr ehs rs)
interpretContT
{-# INLINE interpretK #-}

interpretKH ::
    forall e r ehs efs a fr u c.
    (MonadFreer c fr, Union u, c (Eff u fr ehs efs)) =>
    (a -> Eff u fr ehs efs r) ->
    (forall x. (x -> Eff u fr ehs efs r) -> e (Eff u fr '[e] efs) x -> Eff u fr ehs efs r) ->
    Eff u fr '[e] efs a ->
    Eff u fr ehs efs r
interpretKH :: forall (e :: SigClass) r (ehs :: [SigClass]) (efs :: [SigClass]) a
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, c (Eff u fr ehs efs)) =>
(a -> Eff u fr ehs efs r)
-> (forall x.
    (x -> Eff u fr ehs efs r)
    -> e (Eff u fr '[e] efs) x -> Eff u fr ehs efs r)
-> Eff u fr '[e] efs a
-> Eff u fr ehs efs r
interpretKH = forall {k} (e :: * -> *) (r :: k) (m :: k -> *) (f :: * -> *)
       (m' :: k -> *) a.
((e ~> ContT r m) -> f ~> ContT r m')
-> (a -> m' r)
-> (forall x. (x -> m r) -> e x -> m r)
-> f a
-> m' r
toInterpretKFromContT forall (e :: SigClass) r (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, c (Eff u fr ehs efs)) =>
(e (Eff u fr '[e] efs) ~> ContT r (Eff u fr ehs efs))
-> Eff u fr '[e] efs ~> ContT r (Eff u fr ehs efs)
interpretContTH
{-# INLINE interpretKH #-}

-- | Interpret the leading first-order effect class using a continuation monad transformer.
interpretContT ::
    forall e rs r ehs fr u c.
    (MonadFreer c fr, Union u, HeadIns e, c (Eff u fr ehs rs)) =>
    (UnliftIfSingle e ~> ContT r (Eff u fr ehs rs)) ->
    Eff u fr '[] (e ': rs) ~> ContT r (Eff u fr ehs rs)
interpretContT :: forall (e :: SigClass) (rs :: [SigClass]) r (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, HeadIns e, c (Eff u fr ehs rs)) =>
(UnliftIfSingle e ~> ContT r (Eff u fr ehs rs))
-> Eff u fr '[] (e : rs) ~> ContT r (Eff u fr ehs rs)
interpretContT UnliftIfSingle e ~> ContT r (Eff u fr ehs rs)
i =
    forall {k} (g :: k -> *) (r :: k) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u) =>
(u efs Nop ~> ContT r g) -> Eff u fr '[] efs ~> ContT r g
interpretContTAll forall a b. (a -> b) -> a -> b
$ UnliftIfSingle e ~> ContT r (Eff u fr ehs rs)
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (e :: * -> *) (le :: SigClass).
LiftInsIfSingle e le =>
le Nop ~> e
unliftInsIfSingle forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       a r (es :: [SigClass]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (t :: SigClass) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: (* -> *) -> Constraint) (f :: SigClass)
       (u :: [SigClass] -> SigClass) (efs :: [SigClass])
       (ehs :: [SigClass]).
Freer c f =>
u efs Nop ~> Eff u f ehs efs
injectF
{-# INLINE interpretContT #-}

interpretContTH ::
    forall e r ehs efs fr u c.
    (MonadFreer c fr, Union u, c (Eff u fr ehs efs)) =>
    (e (Eff u fr '[e] efs) ~> ContT r (Eff u fr ehs efs)) ->
    Eff u fr '[e] efs ~> ContT r (Eff u fr ehs efs)
interpretContTH :: forall (e :: SigClass) r (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, c (Eff u fr ehs efs)) =>
(e (Eff u fr '[e] efs) ~> ContT r (Eff u fr ehs efs))
-> Eff u fr '[e] efs ~> ContT r (Eff u fr ehs efs)
interpretContTH e (Eff u fr '[e] efs) ~> ContT r (Eff u fr ehs efs)
i = forall (ehs' :: [SigClass]) r (ehs :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, c (Eff u fr ehs' efs)) =>
(u ehs (Eff u fr ehs efs) ~> ContT r (Eff u fr ehs' efs))
-> Eff u fr ehs efs ~> ContT r (Eff u fr ehs' efs)
interpretContTAllH forall a b. (a -> b) -> a -> b
$ e (Eff u fr '[e] efs) ~> ContT r (Eff u fr ehs efs)
i forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       a r (es :: [SigClass]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [SigClass] -> SigClass) (f :: * -> *) a x.
Union u =>
u '[] f a -> x
exhaust
{-# INLINE interpretContTH #-}

-- | Interpret the leading first-order effect class into the carrier @f@.
interpretFin ::
    forall e r f fr u c.
    (Freer c fr, Union u, HeadIns e, c f) =>
    (u r Nop ~> f) ->
    UnliftIfSingle e ~> f ->
    Eff u fr '[] (e ': r) ~> f
interpretFin :: forall (e :: SigClass) (r :: [SigClass]) (f :: * -> *)
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HeadIns e, c f) =>
(u r Nop ~> f)
-> (UnliftIfSingle e ~> f) -> Eff u fr '[] (e : r) ~> f
interpretFin u r Nop ~> f
liftFin UnliftIfSingle e ~> f
i = forall (g :: * -> *) (efs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, c g) =>
(u efs Nop ~> g) -> Eff u fr '[] efs ~> g
interpretAll forall a b. (a -> b) -> a -> b
$ UnliftIfSingle e ~> f
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (e :: * -> *) (le :: SigClass).
LiftInsIfSingle e le =>
le Nop ~> e
unliftInsIfSingle forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       a r (es :: [SigClass]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: u r Nop ~> f
liftFin
{-# INLINE interpretFin #-}

interpretFinH ::
    forall e f efs fr u c.
    (Freer c fr, Union u, c f) =>
    (u efs Nop ~> f) ->
    e (Eff u fr '[e] efs) ~> f ->
    Eff u fr '[e] efs ~> f
interpretFinH :: forall (e :: SigClass) (f :: * -> *) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, c f) =>
(u efs Nop ~> f)
-> (e (Eff u fr '[e] efs) ~> f) -> Eff u fr '[e] efs ~> f
interpretFinH u efs Nop ~> f
liftFin e (Eff u fr '[e] efs) ~> f
i = forall (g :: * -> *) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, c g) =>
(u ehs (Eff u fr ehs efs) ~> g)
-> (u efs Nop ~> g) -> Eff u fr ehs efs ~> g
interpretAllFH (e (Eff u fr '[e] efs) ~> f
i forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       a r (es :: [SigClass]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [SigClass] -> SigClass) (f :: * -> *) a x.
Union u =>
u '[] f a -> x
exhaust) u efs Nop ~> f
liftFin
{-# INLINE interpretFinH #-}

-- | Interpret the leading first-order effect class using a monad transformer.
interpretT ::
    forall e r t ehs fr u c.
    ( Freer c fr
    , Union u
    , MonadTrans t
    , HeadIns e
    , Monad (Eff u fr ehs r)
    , c (t (Eff u fr ehs r))
    ) =>
    UnliftIfSingle e ~> t (Eff u fr ehs r) ->
    Eff u fr '[] (e ': r) ~> t (Eff u fr ehs r)
interpretT :: forall (e :: SigClass) (r :: [SigClass]) (t :: SigClass)
       (ehs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, MonadTrans t, HeadIns e,
 Monad (Eff u fr ehs r), c (t (Eff u fr ehs r))) =>
(UnliftIfSingle e ~> t (Eff u fr ehs r))
-> Eff u fr '[] (e : r) ~> t (Eff u fr ehs r)
interpretT = forall (e :: SigClass) (r :: [SigClass]) (f :: * -> *)
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HeadIns e, c f) =>
(u r Nop ~> f)
-> (UnliftIfSingle e ~> f) -> Eff u fr '[] (e : r) ~> f
interpretFin forall a b. (a -> b) -> a -> b
$ forall (t :: SigClass) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: (* -> *) -> Constraint) (f :: SigClass)
       (u :: [SigClass] -> SigClass) (efs :: [SigClass])
       (ehs :: [SigClass]).
Freer c f =>
u efs Nop ~> Eff u f ehs efs
injectF
{-# INLINE interpretT #-}

interpretTH ::
    forall e t ehs efs fr u c.
    (Freer c fr, Union u, MonadTrans t, Monad (Eff u fr ehs efs), c (t (Eff u fr ehs efs))) =>
    e (Eff u fr '[e] efs) ~> t (Eff u fr ehs efs) ->
    Eff u fr '[e] efs ~> t (Eff u fr ehs efs)
interpretTH :: forall (e :: SigClass) (t :: SigClass) (ehs :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, MonadTrans t, Monad (Eff u fr ehs efs),
 c (t (Eff u fr ehs efs))) =>
(e (Eff u fr '[e] efs) ~> t (Eff u fr ehs efs))
-> Eff u fr '[e] efs ~> t (Eff u fr ehs efs)
interpretTH = forall (e :: SigClass) (f :: * -> *) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, c f) =>
(u efs Nop ~> f)
-> (e (Eff u fr '[e] efs) ~> f) -> Eff u fr '[e] efs ~> f
interpretFinH forall a b. (a -> b) -> a -> b
$ forall (t :: SigClass) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: (* -> *) -> Constraint) (f :: SigClass)
       (u :: [SigClass] -> SigClass) (efs :: [SigClass])
       (ehs :: [SigClass]).
Freer c f =>
u efs Nop ~> Eff u f ehs efs
injectF
{-# INLINE interpretTH #-}

{- |
Using the provided interpretation function, interpret first-order effects. For actions (scopes)
within higher-order effects that are currently unhandled, interpretation is applied recursively.

Note that if the interpretation function is stateful (i.e., not a monad morphism), the state is not
maintained across the scopes.
-}
interpretRec ::
    forall e rs ehs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs), HeadIns e) =>
    UnliftIfSingle e ~> Eff u fr ehs rs ->
    Eff u fr ehs (e ': rs) ~> Eff u fr ehs rs
interpretRec :: forall (e :: SigClass) (rs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs), HeadIns e) =>
(UnliftIfSingle e ~> Eff u fr ehs rs)
-> Eff u fr ehs (e : rs) ~> Eff u fr ehs rs
interpretRec UnliftIfSingle e ~> Eff u fr ehs rs
i = forall (efs' :: [SigClass]) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u efs Nop ~> Eff u fr ehs efs')
-> Eff u fr ehs efs ~> Eff u fr ehs efs'
interpretAllRec forall a b. (a -> b) -> a -> b
$ UnliftIfSingle e ~> Eff u fr ehs rs
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (e :: * -> *) (le :: SigClass).
LiftInsIfSingle e le =>
le Nop ~> e
unliftInsIfSingle forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       a r (es :: [SigClass]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (c :: (* -> *) -> Constraint) (f :: SigClass)
       (u :: [SigClass] -> SigClass) (efs :: [SigClass])
       (ehs :: [SigClass]).
Freer c f =>
u efs Nop ~> Eff u f ehs efs
injectF
{-# INLINE interpretRec #-}

{- |
Using the provided interpretation function, interpret higher-order effects. For actions (scopes)
within higher-order effects that are currently unhandled, interpretation is applied recursively.

Note that if the interpretation function is stateful (i.e., not a monad morphism), the state is not
maintained across the scopes.
-}
interpretRecH ::
    forall e rs efs fr u c.
    (Freer c fr, Union u, HFunctor e, HFunctor (u rs), HFunctor (u (e ': rs))) =>
    e (Eff u fr rs efs) ~> Eff u fr rs efs ->
    Eff u fr (e ': rs) efs ~> Eff u fr rs efs
interpretRecH :: forall (e :: SigClass) (rs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor e, HFunctor (u rs),
 HFunctor (u (e : rs))) =>
(e (Eff u fr rs efs) ~> Eff u fr rs efs)
-> Eff u fr (e : rs) efs ~> Eff u fr rs efs
interpretRecH e (Eff u fr rs efs) ~> Eff u fr rs efs
i = forall (ehs' :: [SigClass]) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs) ~> Eff u fr ehs' efs)
-> Eff u fr ehs efs ~> Eff u fr ehs' efs
interpretAllRecH forall a b. (a -> b) -> a -> b
$ e (Eff u fr rs efs) ~> Eff u fr rs efs
i forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       a r (es :: [SigClass]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (c :: (* -> *) -> Constraint) (f :: SigClass)
       (u :: [SigClass] -> SigClass) (ehs :: [SigClass])
       (efs :: [SigClass]).
(Freer c f, HFunctor (u ehs)) =>
u ehs (Eff u f ehs efs) ~> Eff u f ehs efs
injectH
{-# INLINE interpretRecH #-}

reinterpret ::
    forall e2 e1 r ehs fr u c.
    (Freer c fr, Union u, HeadIns e1, HFunctor (u '[])) =>
    UnliftIfSingle e1 ~> Eff u fr ehs (e2 ': r) ->
    Eff u fr '[] (e1 ': r) ~> Eff u fr ehs (e2 ': r)
reinterpret :: forall (e2 :: SigClass) (e1 :: SigClass) (r :: [SigClass])
       (ehs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HeadIns e1, HFunctor (u '[])) =>
(UnliftIfSingle e1 ~> Eff u fr ehs (e2 : r))
-> Eff u fr '[] (e1 : r) ~> Eff u fr ehs (e2 : r)
reinterpret UnliftIfSingle e1 ~> Eff u fr ehs (e2 : r)
f = forall (e :: SigClass) (r :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HeadIns e) =>
(UnliftIfSingle e ~> Eff u fr ehs r)
-> Eff u fr '[] (e : r) ~> Eff u fr ehs r
interpret UnliftIfSingle e1 ~> Eff u fr ehs (e2 : r)
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (e1 :: SigClass) (e2 :: SigClass) (r :: [SigClass])
       (ehs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
Eff u fr ehs (e2 : r) ~> Eff u fr ehs (e2 : e1 : r)
raiseUnder
{-# INLINE reinterpret #-}

reinterpretK ::
    forall e2 e1 rs r a ehs fr u c.
    (MonadFreer c fr, Union u, HeadIns e1, HFunctor (u '[]), c (Eff u fr ehs (e2 ': rs))) =>
    (a -> Eff u fr ehs (e2 ': rs) r) ->
    ( forall x.
      (x -> Eff u fr ehs (e2 ': rs) r) ->
      UnliftIfSingle e1 x ->
      Eff u fr ehs (e2 ': rs) r
    ) ->
    Eff u fr '[] (e1 ': rs) a ->
    Eff u fr ehs (e2 ': rs) r
reinterpretK :: forall (e2 :: SigClass) (e1 :: SigClass) (rs :: [SigClass]) r a
       (ehs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, HeadIns e1, HFunctor (u '[]),
 c (Eff u fr ehs (e2 : rs))) =>
(a -> Eff u fr ehs (e2 : rs) r)
-> (forall x.
    (x -> Eff u fr ehs (e2 : rs) r)
    -> UnliftIfSingle e1 x -> Eff u fr ehs (e2 : rs) r)
-> Eff u fr '[] (e1 : rs) a
-> Eff u fr ehs (e2 : rs) r
reinterpretK = forall {k} (e :: * -> *) (r :: k) (m :: k -> *) (f :: * -> *)
       (m' :: k -> *) a.
((e ~> ContT r m) -> f ~> ContT r m')
-> (a -> m' r)
-> (forall x. (x -> m r) -> e x -> m r)
-> f a
-> m' r
toInterpretKFromContT forall (e2 :: SigClass) (e1 :: SigClass) (rs :: [SigClass]) r
       (ehs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, HeadIns e1, HFunctor (u '[]),
 c (Eff u fr ehs (e2 : rs))) =>
(UnliftIfSingle e1 ~> ContT r (Eff u fr ehs (e2 : rs)))
-> Eff u fr '[] (e1 : rs) ~> ContT r (Eff u fr ehs (e2 : rs))
reinterpretContT
{-# INLINE reinterpretK #-}

reinterpretContT ::
    forall e2 e1 rs r ehs fr u c.
    (MonadFreer c fr, Union u, HeadIns e1, HFunctor (u '[]), c (Eff u fr ehs (e2 ': rs))) =>
    (UnliftIfSingle e1 ~> ContT r (Eff u fr ehs (e2 ': rs))) ->
    Eff u fr '[] (e1 ': rs) ~> ContT r (Eff u fr ehs (e2 ': rs))
reinterpretContT :: forall (e2 :: SigClass) (e1 :: SigClass) (rs :: [SigClass]) r
       (ehs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, HeadIns e1, HFunctor (u '[]),
 c (Eff u fr ehs (e2 : rs))) =>
(UnliftIfSingle e1 ~> ContT r (Eff u fr ehs (e2 : rs)))
-> Eff u fr '[] (e1 : rs) ~> ContT r (Eff u fr ehs (e2 : rs))
reinterpretContT UnliftIfSingle e1 ~> ContT r (Eff u fr ehs (e2 : rs))
i = forall (e :: SigClass) (rs :: [SigClass]) r (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, HeadIns e, c (Eff u fr ehs rs)) =>
(UnliftIfSingle e ~> ContT r (Eff u fr ehs rs))
-> Eff u fr '[] (e : rs) ~> ContT r (Eff u fr ehs rs)
interpretContT UnliftIfSingle e1 ~> ContT r (Eff u fr ehs (e2 : rs))
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (e1 :: SigClass) (e2 :: SigClass) (r :: [SigClass])
       (ehs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
Eff u fr ehs (e2 : r) ~> Eff u fr ehs (e2 : e1 : r)
raiseUnder
{-# INLINE reinterpretContT #-}

reinterpretT ::
    forall e2 e1 t r ehs fr u c.
    ( Freer c fr
    , Union u
    , MonadTrans t
    , HeadIns e1
    , HFunctor (u '[])
    , Monad (Eff u fr ehs (e2 ': r))
    , c (t (Eff u fr ehs (e2 ': r)))
    ) =>
    UnliftIfSingle e1 ~> t (Eff u fr ehs (e2 ': r)) ->
    Eff u fr '[] (e1 ': r) ~> t (Eff u fr ehs (e2 ': r))
reinterpretT :: forall (e2 :: SigClass) (e1 :: SigClass) (t :: SigClass)
       (r :: [SigClass]) (ehs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, MonadTrans t, HeadIns e1, HFunctor (u '[]),
 Monad (Eff u fr ehs (e2 : r)), c (t (Eff u fr ehs (e2 : r)))) =>
(UnliftIfSingle e1 ~> t (Eff u fr ehs (e2 : r)))
-> Eff u fr '[] (e1 : r) ~> t (Eff u fr ehs (e2 : r))
reinterpretT UnliftIfSingle e1 ~> t (Eff u fr ehs (e2 : r))
i = forall (e :: SigClass) (r :: [SigClass]) (t :: SigClass)
       (ehs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, MonadTrans t, HeadIns e,
 Monad (Eff u fr ehs r), c (t (Eff u fr ehs r))) =>
(UnliftIfSingle e ~> t (Eff u fr ehs r))
-> Eff u fr '[] (e : r) ~> t (Eff u fr ehs r)
interpretT UnliftIfSingle e1 ~> t (Eff u fr ehs (e2 : r))
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (e1 :: SigClass) (e2 :: SigClass) (r :: [SigClass])
       (ehs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
Eff u fr ehs (e2 : r) ~> Eff u fr ehs (e2 : e1 : r)
raiseUnder
{-# INLINE reinterpretT #-}

reinterpretRec ::
    forall e2 e1 r ehs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs), HeadIns e1) =>
    UnliftIfSingle e1 ~> Eff u fr ehs (e2 ': r) ->
    Eff u fr ehs (e1 ': r) ~> Eff u fr ehs (e2 ': r)
reinterpretRec :: forall (e2 :: SigClass) (e1 :: SigClass) (r :: [SigClass])
       (ehs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs), HeadIns e1) =>
(UnliftIfSingle e1 ~> Eff u fr ehs (e2 : r))
-> Eff u fr ehs (e1 : r) ~> Eff u fr ehs (e2 : r)
reinterpretRec UnliftIfSingle e1 ~> Eff u fr ehs (e2 : r)
i = forall (e :: SigClass) (rs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs), HeadIns e) =>
(UnliftIfSingle e ~> Eff u fr ehs rs)
-> Eff u fr ehs (e : rs) ~> Eff u fr ehs rs
interpretRec UnliftIfSingle e1 ~> Eff u fr ehs (e2 : r)
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (e1 :: SigClass) (e2 :: SigClass) (r :: [SigClass])
       (ehs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
Eff u fr ehs (e2 : r) ~> Eff u fr ehs (e2 : e1 : r)
raiseUnder
{-# INLINE reinterpretRec #-}

reinterpretRecH ::
    forall e2 e1 r efs fr u c.
    (Freer c fr, HFunctorUnion u, HFunctor e1, HFunctor e2, ForallHFunctor u r) =>
    e1 (Eff u fr (e2 ': r) efs) ~> Eff u fr (e2 ': r) efs ->
    Eff u fr (e1 ': r) efs ~> Eff u fr (e2 ': r) efs
reinterpretRecH :: forall (e2 :: SigClass) (e1 :: SigClass) (r :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, HFunctorUnion u, HFunctor e1, HFunctor e2,
 ForallHFunctor u r) =>
(e1 (Eff u fr (e2 : r) efs) ~> Eff u fr (e2 : r) efs)
-> Eff u fr (e1 : r) efs ~> Eff u fr (e2 : r) efs
reinterpretRecH e1 (Eff u fr (e2 : r) efs) ~> Eff u fr (e2 : r) efs
i = forall (e :: SigClass) (rs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor e, HFunctor (u rs),
 HFunctor (u (e : rs))) =>
(e (Eff u fr rs efs) ~> Eff u fr rs efs)
-> Eff u fr (e : rs) efs ~> Eff u fr rs efs
interpretRecH e1 (Eff u fr (e2 : r) efs) ~> Eff u fr (e2 : r) efs
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (e1 :: SigClass) (e2 :: SigClass) (r :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u (e2 : r))) =>
Eff u fr (e2 : r) efs ~> Eff u fr (e2 : e1 : r) efs
raiseUnderH
{-# INLINE reinterpretRecH #-}

interpose ::
    forall e efs fr u c.
    (Freer c fr, Union u, Member u e efs) =>
    e ~> Eff u fr '[] efs ->
    Eff u fr '[] efs ~> Eff u fr '[] efs
interpose :: forall (e :: * -> *) (efs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, Member u e efs) =>
(e ~> Eff u fr '[] efs) -> Eff u fr '[] efs ~> Eff u fr '[] efs
interpose e ~> Eff u fr '[] efs
f =
    forall (ehs' :: [SigClass]) (efs' :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u) =>
(u efs Nop ~> Eff u fr ehs' efs')
-> Eff u fr '[] efs ~> Eff u fr ehs' efs'
interpretAllE
        \u efs Nop x
u -> case forall (u :: [SigClass] -> SigClass) (e :: SigClass)
       (es :: [SigClass]) (f :: * -> *) a.
MemberRec u e es =>
u es f a -> Maybe (e f a)
projectRec u efs Nop x
u of
            Just (LiftIns e x
e) -> e ~> Eff u fr '[] efs
f e x
e
            Maybe (LiftIns e Nop x)
Nothing -> forall (c :: (* -> *) -> Constraint) (f :: SigClass)
       (u :: [SigClass] -> SigClass) (efs :: [SigClass])
       (ehs :: [SigClass]).
Freer c f =>
u efs Nop ~> Eff u f ehs efs
injectF u efs Nop x
u

interposeK ::
    forall e efs r a fr u c.
    (MonadFreer c fr, Union u, Member u e efs, c (Eff u fr '[] efs)) =>
    (a -> Eff u fr '[] efs r) ->
    (forall x. (x -> Eff u fr '[] efs r) -> e x -> Eff u fr '[] efs r) ->
    Eff u fr '[] efs a ->
    Eff u fr '[] efs r
interposeK :: forall (e :: * -> *) (efs :: [SigClass]) r a (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, Member u e efs, c (Eff u fr '[] efs)) =>
(a -> Eff u fr '[] efs r)
-> (forall x.
    (x -> Eff u fr '[] efs r) -> e x -> Eff u fr '[] efs r)
-> Eff u fr '[] efs a
-> Eff u fr '[] efs r
interposeK = forall {k} (e :: * -> *) (r :: k) (m :: k -> *) (f :: * -> *)
       (m' :: k -> *) a.
((e ~> ContT r m) -> f ~> ContT r m')
-> (a -> m' r)
-> (forall x. (x -> m r) -> e x -> m r)
-> f a
-> m' r
toInterpretKFromContT forall (e :: * -> *) (efs :: [SigClass]) r (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, Member u e efs, c (Eff u fr '[] efs)) =>
(e ~> ContT r (Eff u fr '[] efs))
-> Eff u fr '[] efs ~> ContT r (Eff u fr '[] efs)
interposeContT
{-# INLINE interposeK #-}

interposeContT ::
    forall e efs r fr u c.
    (MonadFreer c fr, Union u, Member u e efs, c (Eff u fr '[] efs)) =>
    (e ~> ContT r (Eff u fr '[] efs)) ->
    Eff u fr '[] efs ~> ContT r (Eff u fr '[] efs)
interposeContT :: forall (e :: * -> *) (efs :: [SigClass]) r (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, Member u e efs, c (Eff u fr '[] efs)) =>
(e ~> ContT r (Eff u fr '[] efs))
-> Eff u fr '[] efs ~> ContT r (Eff u fr '[] efs)
interposeContT e ~> ContT r (Eff u fr '[] efs)
f =
    forall {k} (g :: k -> *) (r :: k) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u) =>
(u efs Nop ~> ContT r g) -> Eff u fr '[] efs ~> ContT r g
interpretContTAll
        \u efs Nop x
u -> case forall (u :: [SigClass] -> SigClass) (e :: SigClass)
       (es :: [SigClass]) (f :: * -> *) a.
MemberRec u e es =>
u es f a -> Maybe (e f a)
projectRec u efs Nop x
u of
            Just (LiftIns e x
e) -> e ~> ContT r (Eff u fr '[] efs)
f e x
e
            Maybe (LiftIns e Nop x)
Nothing -> forall (t :: SigClass) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (c :: (* -> *) -> Constraint) (f :: SigClass)
       (u :: [SigClass] -> SigClass) (efs :: [SigClass])
       (ehs :: [SigClass]).
Freer c f =>
u efs Nop ~> Eff u f ehs efs
injectF u efs Nop x
u
{-# INLINE interposeContT #-}

interposeFin ::
    forall e f efs fr u c.
    (Freer c fr, Union u, Member u e efs, c f) =>
    u efs Nop ~> f ->
    e ~> f ->
    Eff u fr '[] efs ~> f
interposeFin :: forall (e :: * -> *) (f :: * -> *) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, Member u e efs, c f) =>
(u efs Nop ~> f) -> (e ~> f) -> Eff u fr '[] efs ~> f
interposeFin u efs Nop ~> f
liftFin e ~> f
f =
    forall (g :: * -> *) (efs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, c g) =>
(u efs Nop ~> g) -> Eff u fr '[] efs ~> g
interpretAll
        \u efs Nop x
u -> case forall (u :: [SigClass] -> SigClass) (e :: SigClass)
       (es :: [SigClass]) (f :: * -> *) a.
MemberRec u e es =>
u es f a -> Maybe (e f a)
projectRec u efs Nop x
u of
            Just (LiftIns e x
e) -> e ~> f
f e x
e
            Maybe (LiftIns e Nop x)
Nothing -> u efs Nop ~> f
liftFin u efs Nop x
u
{-# INLINE interposeFin #-}

interposeT ::
    forall e t efs fr u c.
    ( Freer c fr
    , Union u
    , MonadTrans t
    , Member u e efs
    , Monad (Eff u fr '[] efs)
    , c (t (Eff u fr '[] efs))
    ) =>
    e ~> t (Eff u fr '[] efs) ->
    Eff u fr '[] efs ~> t (Eff u fr '[] efs)
interposeT :: forall (e :: * -> *) (t :: SigClass) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, MonadTrans t, Member u e efs,
 Monad (Eff u fr '[] efs), c (t (Eff u fr '[] efs))) =>
(e ~> t (Eff u fr '[] efs))
-> Eff u fr '[] efs ~> t (Eff u fr '[] efs)
interposeT = forall (e :: * -> *) (f :: * -> *) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, Member u e efs, c f) =>
(u efs Nop ~> f) -> (e ~> f) -> Eff u fr '[] efs ~> f
interposeFin forall a b. (a -> b) -> a -> b
$ forall (t :: SigClass) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: (* -> *) -> Constraint) (f :: SigClass)
       (u :: [SigClass] -> SigClass) (efs :: [SigClass])
       (ehs :: [SigClass]).
Freer c f =>
u efs Nop ~> Eff u f ehs efs
injectF
{-# INLINE interposeT #-}

interposeRec ::
    forall e ehs efs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs), Member u e efs) =>
    e ~> Eff u fr ehs efs ->
    Eff u fr ehs efs ~> Eff u fr ehs efs
interposeRec :: forall (e :: * -> *) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs), Member u e efs) =>
(e ~> Eff u fr ehs efs) -> Eff u fr ehs efs ~> Eff u fr ehs efs
interposeRec e ~> Eff u fr ehs efs
f =
    forall (efs' :: [SigClass]) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u efs Nop ~> Eff u fr ehs efs')
-> Eff u fr ehs efs ~> Eff u fr ehs efs'
interpretAllRec
        \u efs Nop x
u -> case forall (u :: [SigClass] -> SigClass) (e :: SigClass)
       (es :: [SigClass]) (f :: * -> *) a.
MemberRec u e es =>
u es f a -> Maybe (e f a)
projectRec u efs Nop x
u of
            Just (LiftIns e x
e) -> e ~> Eff u fr ehs efs
f e x
e
            Maybe (LiftIns e Nop x)
Nothing -> forall (c :: (* -> *) -> Constraint) (f :: SigClass)
       (u :: [SigClass] -> SigClass) (efs :: [SigClass])
       (ehs :: [SigClass]).
Freer c f =>
u efs Nop ~> Eff u f ehs efs
injectF u efs Nop x
u
{-# INLINE interposeRec #-}

interposeRecH ::
    forall e ehs efs fr u c.
    (Freer c fr, HFunctorUnion u, HFunctor e, ForallHFunctor u ehs, MemberH u e ehs) =>
    e (Eff u fr ehs efs) ~> Eff u fr ehs efs ->
    Eff u fr ehs efs ~> Eff u fr ehs efs
interposeRecH :: forall (e :: SigClass) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, HFunctorUnion u, HFunctor e, ForallHFunctor u ehs,
 MemberH u e ehs) =>
(e (Eff u fr ehs efs) ~> Eff u fr ehs efs)
-> Eff u fr ehs efs ~> Eff u fr ehs efs
interposeRecH e (Eff u fr ehs efs) ~> Eff u fr ehs efs
f =
    forall (ehs' :: [SigClass]) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs) ~> Eff u fr ehs' efs)
-> Eff u fr ehs efs ~> Eff u fr ehs' efs
interpretAllRecH
        \u ehs (Eff u fr ehs efs) x
u -> case forall (u :: [SigClass] -> SigClass) (e :: SigClass)
       (es :: [SigClass]) (f :: * -> *) a.
MemberRec u e es =>
u es f a -> Maybe (e f a)
projectRec u ehs (Eff u fr ehs efs) x
u of
            Just e (Eff u fr ehs efs) x
e -> e (Eff u fr ehs efs) ~> Eff u fr ehs efs
f e (Eff u fr ehs efs) x
e
            Maybe (e (Eff u fr ehs efs) x)
Nothing -> forall (c :: (* -> *) -> Constraint) (f :: SigClass)
       (u :: [SigClass] -> SigClass) (ehs :: [SigClass])
       (efs :: [SigClass]).
(Freer c f, HFunctor (u ehs)) =>
u ehs (Eff u f ehs efs) ~> Eff u f ehs efs
injectH u ehs (Eff u fr ehs efs) x
u
{-# INLINE interposeRecH #-}

interpretAll ::
    forall g efs fr u c.
    (Freer c fr, Union u, c g) =>
    u efs Nop ~> g ->
    Eff u fr '[] efs ~> g
interpretAll :: forall (g :: * -> *) (efs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, c g) =>
(u efs Nop ~> g) -> Eff u fr '[] efs ~> g
interpretAll = forall (g :: * -> *) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, c g) =>
(u ehs (Eff u fr ehs efs) ~> g)
-> (u efs Nop ~> g) -> Eff u fr ehs efs ~> g
interpretAllFH forall (u :: [SigClass] -> SigClass) (f :: * -> *) a x.
Union u =>
u '[] f a -> x
exhaust
{-# INLINE interpretAll #-}

interpretAllE ::
    forall ehs' efs' efs fr u c.
    (Freer c fr, Union u) =>
    u efs Nop ~> Eff u fr ehs' efs' ->
    Eff u fr '[] efs ~> Eff u fr ehs' efs'
interpretAllE :: forall (ehs' :: [SigClass]) (efs' :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u) =>
(u efs Nop ~> Eff u fr ehs' efs')
-> Eff u fr '[] efs ~> Eff u fr ehs' efs'
interpretAllE = forall (ehs' :: [SigClass]) (efs' :: [SigClass])
       (ehs :: [SigClass]) (efs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u) =>
(u ehs (Eff u fr ehs efs) ~> Eff u fr ehs' efs')
-> (u efs Nop ~> Eff u fr ehs' efs')
-> Eff u fr ehs efs ~> Eff u fr ehs' efs'
interpretAllFHE forall (u :: [SigClass] -> SigClass) (f :: * -> *) a x.
Union u =>
u '[] f a -> x
exhaust
{-# INLINE interpretAllE #-}

interpretAllRecH ::
    forall ehs' ehs efs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs)) =>
    u ehs (Eff u fr ehs' efs) ~> Eff u fr ehs' efs ->
    Eff u fr ehs efs ~> Eff u fr ehs' efs
interpretAllRecH :: forall (ehs' :: [SigClass]) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs) ~> Eff u fr ehs' efs)
-> Eff u fr ehs efs ~> Eff u fr ehs' efs
interpretAllRecH u ehs (Eff u fr ehs' efs) ~> Eff u fr ehs' efs
fh =
    forall (ehs' :: [SigClass]) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u) =>
(u ehs (Eff u fr ehs efs) ~> Eff u fr ehs' efs)
-> Eff u fr ehs efs ~> Eff u fr ehs' efs
interpretAllH forall a b. (a -> b) -> a -> b
$ u ehs (Eff u fr ehs' efs) ~> Eff u fr ehs' efs
fh forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (h :: SigClass) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap (forall (ehs' :: [SigClass]) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs) ~> Eff u fr ehs' efs)
-> Eff u fr ehs efs ~> Eff u fr ehs' efs
interpretAllRecH u ehs (Eff u fr ehs' efs) ~> Eff u fr ehs' efs
fh)

interpretAllH ::
    forall ehs' ehs efs fr u c.
    (Freer c fr, Union u) =>
    u ehs (Eff u fr ehs efs) ~> Eff u fr ehs' efs ->
    Eff u fr ehs efs ~> Eff u fr ehs' efs
interpretAllH :: forall (ehs' :: [SigClass]) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u) =>
(u ehs (Eff u fr ehs efs) ~> Eff u fr ehs' efs)
-> Eff u fr ehs efs ~> Eff u fr ehs' efs
interpretAllH u ehs (Eff u fr ehs efs) ~> Eff u fr ehs' efs
fh = forall (ehs' :: [SigClass]) (efs' :: [SigClass])
       (ehs :: [SigClass]) (efs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u) =>
(u ehs (Eff u fr ehs efs) ~> Eff u fr ehs' efs')
-> (u efs Nop ~> Eff u fr ehs' efs')
-> Eff u fr ehs efs ~> Eff u fr ehs' efs'
interpretAllFHE u ehs (Eff u fr ehs efs) ~> Eff u fr ehs' efs
fh forall (c :: (* -> *) -> Constraint) (f :: SigClass)
       (u :: [SigClass] -> SigClass) (efs :: [SigClass])
       (ehs :: [SigClass]).
Freer c f =>
u efs Nop ~> Eff u f ehs efs
injectF
{-# INLINE interpretAllH #-}

interpretAllRecFH ::
    forall g ehs efs fr u c.
    (Freer c fr, Union u, c g, HFunctor (u ehs)) =>
    u ehs g ~> g ->
    u efs Nop ~> g ->
    Eff u fr ehs efs ~> g
interpretAllRecFH :: forall (g :: * -> *) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, c g, HFunctor (u ehs)) =>
(u ehs g ~> g) -> (u efs Nop ~> g) -> Eff u fr ehs efs ~> g
interpretAllRecFH u ehs g ~> g
fh u efs Nop ~> g
ff =
    forall (g :: * -> *) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, c g) =>
(u ehs (Eff u fr ehs efs) ~> g)
-> (u efs Nop ~> g) -> Eff u fr ehs efs ~> g
interpretAllFH (u ehs g ~> g
fh forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (h :: SigClass) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap (forall (g :: * -> *) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, c g, HFunctor (u ehs)) =>
(u ehs g ~> g) -> (u efs Nop ~> g) -> Eff u fr ehs efs ~> g
interpretAllRecFH u ehs g ~> g
fh u efs Nop ~> g
ff)) u efs Nop ~> g
ff

interpretAllFH ::
    forall g ehs efs fr u c.
    (Freer c fr, Union u, c g) =>
    u ehs (Eff u fr ehs efs) ~> g ->
    u efs Nop ~> g ->
    Eff u fr ehs efs ~> g
interpretAllFH :: forall (g :: * -> *) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, c g) =>
(u ehs (Eff u fr ehs efs) ~> g)
-> (u efs Nop ~> g) -> Eff u fr ehs efs ~> g
interpretAllFH u ehs (Eff u fr ehs efs) ~> g
fh u efs Nop ~> g
ff = forall (c :: (* -> *) -> Constraint) (f :: SigClass) (m :: * -> *)
       (e :: * -> *) a.
(Freer c f, c m) =>
(e ~> m) -> f e a -> m a
interpretFreer (forall (u :: [SigClass] -> SigClass) (ehs :: [SigClass])
       (f :: * -> *) a r (efs :: [SigClass]).
(u ehs f a -> r)
-> (u efs Nop a -> r) -> EffUnion u ehs efs f a -> r
caseHF u ehs (Eff u fr ehs efs) ~> g
fh u efs Nop ~> g
ff) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: SigClass) (e :: SigClass) a.
Hefty f e a -> f (e (Hefty f e)) a
unHefty
{-# INLINE interpretAllFH #-}

interpretAllRecFHE ::
    forall ehs' efs' ehs efs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs)) =>
    u ehs (Eff u fr ehs' efs') ~> Eff u fr ehs' efs' ->
    u efs Nop ~> Eff u fr ehs' efs' ->
    Eff u fr ehs efs ~> Eff u fr ehs' efs'
interpretAllRecFHE :: forall (ehs' :: [SigClass]) (efs' :: [SigClass])
       (ehs :: [SigClass]) (efs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs') ~> Eff u fr ehs' efs')
-> (u efs Nop ~> Eff u fr ehs' efs')
-> Eff u fr ehs efs ~> Eff u fr ehs' efs'
interpretAllRecFHE u ehs (Eff u fr ehs' efs') ~> Eff u fr ehs' efs'
fh u efs Nop ~> Eff u fr ehs' efs'
ff =
    forall (ehs' :: [SigClass]) (efs' :: [SigClass])
       (ehs :: [SigClass]) (efs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u) =>
(u ehs (Eff u fr ehs efs) ~> Eff u fr ehs' efs')
-> (u efs Nop ~> Eff u fr ehs' efs')
-> Eff u fr ehs efs ~> Eff u fr ehs' efs'
interpretAllFHE (u ehs (Eff u fr ehs' efs') ~> Eff u fr ehs' efs'
fh forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (h :: SigClass) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap (forall (ehs' :: [SigClass]) (efs' :: [SigClass])
       (ehs :: [SigClass]) (efs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs') ~> Eff u fr ehs' efs')
-> (u efs Nop ~> Eff u fr ehs' efs')
-> Eff u fr ehs efs ~> Eff u fr ehs' efs'
interpretAllRecFHE u ehs (Eff u fr ehs' efs') ~> Eff u fr ehs' efs'
fh u efs Nop ~> Eff u fr ehs' efs'
ff)) u efs Nop ~> Eff u fr ehs' efs'
ff
{-# INLINE interpretAllRecFHE #-}

interpretAllFHE ::
    forall ehs' efs' ehs efs fr u c.
    (Freer c fr, Union u) =>
    u ehs (Eff u fr ehs efs) ~> Eff u fr ehs' efs' ->
    u efs Nop ~> Eff u fr ehs' efs' ->
    Eff u fr ehs efs ~> Eff u fr ehs' efs'
interpretAllFHE :: forall (ehs' :: [SigClass]) (efs' :: [SigClass])
       (ehs :: [SigClass]) (efs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u) =>
(u ehs (Eff u fr ehs efs) ~> Eff u fr ehs' efs')
-> (u efs Nop ~> Eff u fr ehs' efs')
-> Eff u fr ehs efs ~> Eff u fr ehs' efs'
interpretAllFHE u ehs (Eff u fr ehs efs) ~> Hefty fr (EffUnion u ehs' efs')
fh u efs Nop ~> Hefty fr (EffUnion u ehs' efs')
ff =
    forall (f :: SigClass) (e :: SigClass) a (f' :: SigClass)
       (e' :: SigClass) b.
(f (e (Hefty f e)) a -> f' (e' (Hefty f' e')) b)
-> Hefty f e a -> Hefty f' e' b
overHefty forall a b. (a -> b) -> a -> b
$ forall (c :: (* -> *) -> Constraint) (f :: SigClass) (m :: * -> *)
       (e :: * -> *) a.
(Freer c f, c m) =>
(e ~> m) -> f e a -> m a
interpretFreer forall a b. (a -> b) -> a -> b
$ forall (f :: SigClass) (e :: SigClass) a.
Hefty f e a -> f (e (Hefty f e)) a
unHefty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [SigClass] -> SigClass) (ehs :: [SigClass])
       (f :: * -> *) a r (efs :: [SigClass]).
(u ehs f a -> r)
-> (u efs Nop a -> r) -> EffUnion u ehs efs f a -> r
caseHF u ehs (Eff u fr ehs efs) ~> Hefty fr (EffUnion u ehs' efs')
fh u efs Nop ~> Hefty fr (EffUnion u ehs' efs')
ff

interpretKAll ::
    forall r a efs fr u c.
    (MonadFreer c fr, Union u) =>
    (a -> Eff u fr '[] efs r) ->
    (forall x. (x -> Eff u fr '[] efs r) -> u efs Nop x -> Eff u fr '[] efs r) ->
    Eff u fr '[] efs a ->
    Eff u fr '[] efs r
interpretKAll :: forall r a (efs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u) =>
(a -> Eff u fr '[] efs r)
-> (forall x.
    (x -> Eff u fr '[] efs r) -> u efs Nop x -> Eff u fr '[] efs r)
-> Eff u fr '[] efs a
-> Eff u fr '[] efs r
interpretKAll = forall {k} (e :: * -> *) (r :: k) (m :: k -> *) (f :: * -> *)
       (m' :: k -> *) a.
((e ~> ContT r m) -> f ~> ContT r m')
-> (a -> m' r)
-> (forall x. (x -> m r) -> e x -> m r)
-> f a
-> m' r
toInterpretKFromContT forall {k} (g :: k -> *) (r :: k) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u) =>
(u efs Nop ~> ContT r g) -> Eff u fr '[] efs ~> ContT r g
interpretContTAll
{-# INLINE interpretKAll #-}

interpretKAllRecH ::
    forall ehs' r a ehs efs fr u c.
    (MonadFreer c fr, Union u, HFunctor (u ehs), c (Eff u fr ehs' efs)) =>
    (a -> Eff u fr ehs' efs r) ->
    ( forall x.
      (x -> Eff u fr ehs' efs r) ->
      u ehs (ContT r (Eff u fr ehs' efs)) x ->
      Eff u fr ehs' efs r
    ) ->
    Eff u fr ehs efs a ->
    Eff u fr ehs' efs r
interpretKAllRecH :: forall (ehs' :: [SigClass]) r a (ehs :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, HFunctor (u ehs),
 c (Eff u fr ehs' efs)) =>
(a -> Eff u fr ehs' efs r)
-> (forall x.
    (x -> Eff u fr ehs' efs r)
    -> u ehs (ContT r (Eff u fr ehs' efs)) x -> Eff u fr ehs' efs r)
-> Eff u fr ehs efs a
-> Eff u fr ehs' efs r
interpretKAllRecH = forall {k} (e :: * -> *) (r :: k) (m :: k -> *) (f :: * -> *)
       (m' :: k -> *) a.
((e ~> ContT r m) -> f ~> ContT r m')
-> (a -> m' r)
-> (forall x. (x -> m r) -> e x -> m r)
-> f a
-> m' r
toInterpretKFromContT forall (ehs' :: [SigClass]) r (ehs :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, HFunctor (u ehs),
 c (Eff u fr ehs' efs)) =>
(u ehs (ContT r (Eff u fr ehs' efs))
 ~> ContT r (Eff u fr ehs' efs))
-> Eff u fr ehs efs ~> ContT r (Eff u fr ehs' efs)
interpretContTAllRecH
{-# INLINE interpretKAllRecH #-}

interpretKAllH ::
    forall ehs' r a ehs efs fr u c.
    (MonadFreer c fr, Union u, c (Eff u fr ehs' efs)) =>
    (a -> Eff u fr ehs' efs r) ->
    ( forall x.
      (x -> Eff u fr ehs' efs r) ->
      u ehs (Eff u fr ehs efs) x ->
      Eff u fr ehs' efs r
    ) ->
    Eff u fr ehs efs a ->
    Eff u fr ehs' efs r
interpretKAllH :: forall (ehs' :: [SigClass]) r a (ehs :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, c (Eff u fr ehs' efs)) =>
(a -> Eff u fr ehs' efs r)
-> (forall x.
    (x -> Eff u fr ehs' efs r)
    -> u ehs (Eff u fr ehs efs) x -> Eff u fr ehs' efs r)
-> Eff u fr ehs efs a
-> Eff u fr ehs' efs r
interpretKAllH = forall {k} (e :: * -> *) (r :: k) (m :: k -> *) (f :: * -> *)
       (m' :: k -> *) a.
((e ~> ContT r m) -> f ~> ContT r m')
-> (a -> m' r)
-> (forall x. (x -> m r) -> e x -> m r)
-> f a
-> m' r
toInterpretKFromContT forall (ehs' :: [SigClass]) r (ehs :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, c (Eff u fr ehs' efs)) =>
(u ehs (Eff u fr ehs efs) ~> ContT r (Eff u fr ehs' efs))
-> Eff u fr ehs efs ~> ContT r (Eff u fr ehs' efs)
interpretContTAllH
{-# INLINE interpretKAllH #-}

interpretKAllRecFH ::
    forall g r a ehs efs fr u c.
    (MonadFreer c fr, Union u, HFunctor (u ehs)) =>
    (a -> g r) ->
    (forall x. (x -> g r) -> u ehs (ContT r g) x -> g r) ->
    (forall x. (x -> g r) -> u efs Nop x -> g r) ->
    Eff u fr ehs efs a ->
    g r
interpretKAllRecFH :: forall {k} (g :: k -> *) (r :: k) a (ehs :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, HFunctor (u ehs)) =>
(a -> g r)
-> (forall x. (x -> g r) -> u ehs (ContT r g) x -> g r)
-> (forall x. (x -> g r) -> u efs Nop x -> g r)
-> Eff u fr ehs efs a
-> g r
interpretKAllRecFH = forall {k} (e1 :: * -> *) (r :: k) (m :: k -> *) (e2 :: * -> *)
       (f :: * -> *) (m' :: k -> *) a.
((e1 ~> ContT r m) -> (e2 ~> ContT r m) -> f ~> ContT r m')
-> (a -> m' r)
-> (forall x. (x -> m r) -> e1 x -> m r)
-> (forall x. (x -> m r) -> e2 x -> m r)
-> f a
-> m' r
toInterpretKFromContT2 forall {k} (g :: k -> *) (r :: k) (ehs :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (ContT r g) ~> ContT r g)
-> (u efs Nop ~> ContT r g) -> Eff u fr ehs efs ~> ContT r g
interpretContTAllRecFH
{-# INLINE interpretKAllRecFH #-}

interpretKAllFH ::
    forall g r a ehs efs fr u c.
    (MonadFreer c fr, Union u) =>
    (a -> g r) ->
    (forall x. (x -> g r) -> u ehs (Eff u fr ehs efs) x -> g r) ->
    (forall x. (x -> g r) -> u efs Nop x -> g r) ->
    Eff u fr ehs efs a ->
    g r
interpretKAllFH :: forall {k} (g :: k -> *) (r :: k) a (ehs :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u) =>
(a -> g r)
-> (forall x. (x -> g r) -> u ehs (Eff u fr ehs efs) x -> g r)
-> (forall x. (x -> g r) -> u efs Nop x -> g r)
-> Eff u fr ehs efs a
-> g r
interpretKAllFH = forall {k} (e1 :: * -> *) (r :: k) (m :: k -> *) (e2 :: * -> *)
       (f :: * -> *) (m' :: k -> *) a.
((e1 ~> ContT r m) -> (e2 ~> ContT r m) -> f ~> ContT r m')
-> (a -> m' r)
-> (forall x. (x -> m r) -> e1 x -> m r)
-> (forall x. (x -> m r) -> e2 x -> m r)
-> f a
-> m' r
toInterpretKFromContT2 forall {k} (g :: k -> *) (r :: k) (ehs :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u) =>
(u ehs (Eff u fr ehs efs) ~> ContT r g)
-> (u efs Nop ~> ContT r g) -> Eff u fr ehs efs ~> ContT r g
interpretContTAllFH
{-# INLINE interpretKAllFH #-}

interpretContTAll ::
    forall g r efs fr u c.
    (MonadFreer c fr, Union u) =>
    u efs Nop ~> ContT r g ->
    Eff u fr '[] efs ~> ContT r g
interpretContTAll :: forall {k} (g :: k -> *) (r :: k) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u) =>
(u efs Nop ~> ContT r g) -> Eff u fr '[] efs ~> ContT r g
interpretContTAll u efs Nop ~> ContT r g
f =
    forall {k} (m :: k -> *) (r :: k). Cont (m r) ~> ContT r m
transCont
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: (* -> *) -> Constraint) (fr :: SigClass) (e :: * -> *)
       r.
MonadFreer c fr =>
(e ~> Cont r) -> fr e ~> Cont r
interpretFreerK (forall (u :: [SigClass] -> SigClass) (ehs :: [SigClass])
       (f :: * -> *) a r (efs :: [SigClass]).
(u ehs f a -> r)
-> (u efs Nop a -> r) -> EffUnion u ehs efs f a -> r
caseHF forall (u :: [SigClass] -> SigClass) (f :: * -> *) a x.
Union u =>
u '[] f a -> x
exhaust (forall {k} (r :: k) (m :: k -> *). ContT r m ~> Cont (m r)
detransContT forall b c a. (b -> c) -> (a -> b) -> a -> c
. u efs Nop ~> ContT r g
f))
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: SigClass) (e :: SigClass) a.
Hefty f e a -> f (e (Hefty f e)) a
unHefty

interpretContTAllRecH ::
    forall ehs' r ehs efs fr u c.
    (MonadFreer c fr, Union u, HFunctor (u ehs), c (Eff u fr ehs' efs)) =>
    u ehs (ContT r (Eff u fr ehs' efs)) ~> ContT r (Eff u fr ehs' efs) ->
    Eff u fr ehs efs ~> ContT r (Eff u fr ehs' efs)
interpretContTAllRecH :: forall (ehs' :: [SigClass]) r (ehs :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, HFunctor (u ehs),
 c (Eff u fr ehs' efs)) =>
(u ehs (ContT r (Eff u fr ehs' efs))
 ~> ContT r (Eff u fr ehs' efs))
-> Eff u fr ehs efs ~> ContT r (Eff u fr ehs' efs)
interpretContTAllRecH u ehs (ContT r (Eff u fr ehs' efs)) ~> ContT r (Eff u fr ehs' efs)
fh = forall {k} (g :: k -> *) (r :: k) (ehs :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (ContT r g) ~> ContT r g)
-> (u efs Nop ~> ContT r g) -> Eff u fr ehs efs ~> ContT r g
interpretContTAllRecFH u ehs (ContT r (Eff u fr ehs' efs)) ~> ContT r (Eff u fr ehs' efs)
fh (forall (t :: SigClass) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: (* -> *) -> Constraint) (f :: SigClass)
       (u :: [SigClass] -> SigClass) (efs :: [SigClass])
       (ehs :: [SigClass]).
Freer c f =>
u efs Nop ~> Eff u f ehs efs
injectF)
{-# INLINE interpretContTAllRecH #-}

interpretContTAllH ::
    forall ehs' r ehs efs fr u c.
    (MonadFreer c fr, Union u, c (Eff u fr ehs' efs)) =>
    u ehs (Eff u fr ehs efs) ~> ContT r (Eff u fr ehs' efs) ->
    Eff u fr ehs efs ~> ContT r (Eff u fr ehs' efs)
interpretContTAllH :: forall (ehs' :: [SigClass]) r (ehs :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, c (Eff u fr ehs' efs)) =>
(u ehs (Eff u fr ehs efs) ~> ContT r (Eff u fr ehs' efs))
-> Eff u fr ehs efs ~> ContT r (Eff u fr ehs' efs)
interpretContTAllH u ehs (Eff u fr ehs efs) ~> ContT r (Eff u fr ehs' efs)
fh = forall {k} (g :: k -> *) (r :: k) (ehs :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u) =>
(u ehs (Eff u fr ehs efs) ~> ContT r g)
-> (u efs Nop ~> ContT r g) -> Eff u fr ehs efs ~> ContT r g
interpretContTAllFH u ehs (Eff u fr ehs efs) ~> ContT r (Eff u fr ehs' efs)
fh (forall (t :: SigClass) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: (* -> *) -> Constraint) (f :: SigClass)
       (u :: [SigClass] -> SigClass) (efs :: [SigClass])
       (ehs :: [SigClass]).
Freer c f =>
u efs Nop ~> Eff u f ehs efs
injectF)
{-# INLINE interpretContTAllH #-}

interpretContTAllRecFH ::
    forall g r ehs efs fr u c.
    (MonadFreer c fr, Union u, HFunctor (u ehs)) =>
    u ehs (ContT r g) ~> ContT r g ->
    u efs Nop ~> ContT r g ->
    Eff u fr ehs efs ~> ContT r g
interpretContTAllRecFH :: forall {k} (g :: k -> *) (r :: k) (ehs :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (ContT r g) ~> ContT r g)
-> (u efs Nop ~> ContT r g) -> Eff u fr ehs efs ~> ContT r g
interpretContTAllRecFH u ehs (ContT r g) ~> ContT r g
fh u efs Nop ~> ContT r g
ff =
    forall {k} (m :: k -> *) (r :: k). Cont (m r) ~> ContT r m
transCont
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: (* -> *) -> Constraint) (fr :: SigClass) (e :: * -> *)
       r.
MonadFreer c fr =>
(e ~> Cont r) -> fr e ~> Cont r
interpretFreerK (forall {k} (r :: k) (m :: k -> *). ContT r m ~> Cont (m r)
detransContT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [SigClass] -> SigClass) (ehs :: [SigClass])
       (f :: * -> *) a r (efs :: [SigClass]).
(u ehs f a -> r)
-> (u efs Nop a -> r) -> EffUnion u ehs efs f a -> r
caseHF (u ehs (ContT r g) ~> ContT r g
fh forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (h :: SigClass) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap (forall {k} (g :: k -> *) (r :: k) (ehs :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (ContT r g) ~> ContT r g)
-> (u efs Nop ~> ContT r g) -> Eff u fr ehs efs ~> ContT r g
interpretContTAllRecFH u ehs (ContT r g) ~> ContT r g
fh u efs Nop ~> ContT r g
ff)) u efs Nop ~> ContT r g
ff)
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: SigClass) (e :: SigClass) a.
Hefty f e a -> f (e (Hefty f e)) a
unHefty

interpretContTAllFH ::
    forall g r ehs efs fr u c.
    (MonadFreer c fr, Union u) =>
    u ehs (Eff u fr ehs efs) ~> ContT r g ->
    u efs Nop ~> ContT r g ->
    Eff u fr ehs efs ~> ContT r g
interpretContTAllFH :: forall {k} (g :: k -> *) (r :: k) (ehs :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u) =>
(u ehs (Eff u fr ehs efs) ~> ContT r g)
-> (u efs Nop ~> ContT r g) -> Eff u fr ehs efs ~> ContT r g
interpretContTAllFH u ehs (Eff u fr ehs efs) ~> ContT r g
fh u efs Nop ~> ContT r g
ff =
    forall {k} (m :: k -> *) (r :: k). Cont (m r) ~> ContT r m
transCont
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: (* -> *) -> Constraint) (fr :: SigClass) (e :: * -> *)
       r.
MonadFreer c fr =>
(e ~> Cont r) -> fr e ~> Cont r
interpretFreerK (forall {k} (r :: k) (m :: k -> *). ContT r m ~> Cont (m r)
detransContT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [SigClass] -> SigClass) (ehs :: [SigClass])
       (f :: * -> *) a r (efs :: [SigClass]).
(u ehs f a -> r)
-> (u efs Nop a -> r) -> EffUnion u ehs efs f a -> r
caseHF u ehs (Eff u fr ehs efs) ~> ContT r g
fh u efs Nop ~> ContT r g
ff)
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: SigClass) (e :: SigClass) a.
Hefty f e a -> f (e (Hefty f e)) a
unHefty

transCont :: Cont (m r) ~> ContT r m
transCont :: forall {k} (m :: k -> *) (r :: k). Cont (m r) ~> ContT r m
transCont (ContT (x -> Identity (m r)) -> Identity (m r)
f) = forall {k} (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT \x -> m r
k -> coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ (x -> Identity (m r)) -> Identity (m r)
f forall a b. (a -> b) -> a -> b
$ coerce :: forall a b. Coercible a b => a -> b
coerce forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> m r
k
{-# INLINE transCont #-}

detransContT :: ContT r m ~> Cont (m r)
detransContT :: forall {k} (r :: k) (m :: k -> *). ContT r m ~> Cont (m r)
detransContT (ContT (x -> m r) -> m r
f) = forall {k} (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT \x -> Identity (m r)
k -> coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ (x -> m r) -> m r
f forall a b. (a -> b) -> a -> b
$ coerce :: forall a b. Coercible a b => a -> b
coerce forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Identity (m r)
k
{-# INLINE detransContT #-}

toInterpretKFromContT ::
    ((e ~> ContT r m) -> f ~> ContT r m') ->
    (a -> m' r) ->
    (forall x. (x -> m r) -> e x -> m r) ->
    f a ->
    m' r
toInterpretKFromContT :: forall {k} (e :: * -> *) (r :: k) (m :: k -> *) (f :: * -> *)
       (m' :: k -> *) a.
((e ~> ContT r m) -> f ~> ContT r m')
-> (a -> m' r)
-> (forall x. (x -> m r) -> e x -> m r)
-> f a
-> m' r
toInterpretKFromContT (e ~> ContT r m) -> f ~> ContT r m'
intContT a -> m' r
k forall x. (x -> m r) -> e x -> m r
i = (forall {k} (r :: k) (m :: k -> *) a.
ContT r m a -> (a -> m r) -> m r
`runContT` a -> m' r
k) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (e ~> ContT r m) -> f ~> ContT r m'
intContT \e x
e -> forall {k} (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT (forall x. (x -> m r) -> e x -> m r
`i` e x
e)
{-# INLINE toInterpretKFromContT #-}

toInterpretKFromContT2 ::
    ((e1 ~> ContT r m) -> (e2 ~> ContT r m) -> f ~> ContT r m') ->
    (a -> m' r) ->
    (forall x. (x -> m r) -> e1 x -> m r) ->
    (forall x. (x -> m r) -> e2 x -> m r) ->
    f a ->
    m' r
toInterpretKFromContT2 :: forall {k} (e1 :: * -> *) (r :: k) (m :: k -> *) (e2 :: * -> *)
       (f :: * -> *) (m' :: k -> *) a.
((e1 ~> ContT r m) -> (e2 ~> ContT r m) -> f ~> ContT r m')
-> (a -> m' r)
-> (forall x. (x -> m r) -> e1 x -> m r)
-> (forall x. (x -> m r) -> e2 x -> m r)
-> f a
-> m' r
toInterpretKFromContT2 (e1 ~> ContT r m) -> (e2 ~> ContT r m) -> f ~> ContT r m'
intContT a -> m' r
k forall x. (x -> m r) -> e1 x -> m r
i1 forall x. (x -> m r) -> e2 x -> m r
i2 =
    (forall {k} (r :: k) (m :: k -> *) a.
ContT r m a -> (a -> m r) -> m r
`runContT` a -> m' r
k) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (e1 ~> ContT r m) -> (e2 ~> ContT r m) -> f ~> ContT r m'
intContT (\e1 x
e -> forall {k} (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT (forall x. (x -> m r) -> e1 x -> m r
`i1` e1 x
e)) (\e2 x
e -> forall {k} (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT (forall x. (x -> m r) -> e2 x -> m r
`i2` e2 x
e))
{-# INLINE toInterpretKFromContT2 #-}

interpretTAll ::
    forall t g efs fr u c.
    (Freer c fr, Union u, c (t g)) =>
    u efs Nop ~> t g ->
    Eff u fr '[] efs ~> t g
interpretTAll :: forall {k} (t :: k -> * -> *) (g :: k) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, c (t g)) =>
(u efs Nop ~> t g) -> Eff u fr '[] efs ~> t g
interpretTAll = forall (g :: * -> *) (efs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, c g) =>
(u efs Nop ~> g) -> Eff u fr '[] efs ~> g
interpretAll
{-# INLINE interpretTAll #-}

interpretTAllRecH ::
    forall ehs' t ehs efs fr u c.
    ( Freer c fr
    , Union u
    , MonadTrans t
    , HFunctor (u ehs)
    , Monad (Eff u fr ehs' efs)
    , c (t (Eff u fr ehs' efs))
    ) =>
    u ehs (t (Eff u fr ehs' efs)) ~> t (Eff u fr ehs' efs) ->
    Eff u fr ehs efs ~> t (Eff u fr ehs' efs)
interpretTAllRecH :: forall (ehs' :: [SigClass]) (t :: SigClass) (ehs :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, MonadTrans t, HFunctor (u ehs),
 Monad (Eff u fr ehs' efs), c (t (Eff u fr ehs' efs))) =>
(u ehs (t (Eff u fr ehs' efs)) ~> t (Eff u fr ehs' efs))
-> Eff u fr ehs efs ~> t (Eff u fr ehs' efs)
interpretTAllRecH u ehs (t (Eff u fr ehs' efs)) ~> t (Eff u fr ehs' efs)
i = forall (g :: * -> *) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, c g, HFunctor (u ehs)) =>
(u ehs g ~> g) -> (u efs Nop ~> g) -> Eff u fr ehs efs ~> g
interpretAllRecFH u ehs (t (Eff u fr ehs' efs)) ~> t (Eff u fr ehs' efs)
i (forall (t :: SigClass) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: (* -> *) -> Constraint) (f :: SigClass)
       (u :: [SigClass] -> SigClass) (efs :: [SigClass])
       (ehs :: [SigClass]).
Freer c f =>
u efs Nop ~> Eff u f ehs efs
injectF)
{-# INLINE interpretTAllRecH #-}

interpretTAllH ::
    forall ehs' t ehs efs fr u c.
    (Freer c fr, Union u, MonadTrans t, Monad (Eff u fr ehs' efs), c (t (Eff u fr ehs' efs))) =>
    u ehs (Eff u fr ehs efs) ~> t (Eff u fr ehs' efs) ->
    Eff u fr ehs efs ~> t (Eff u fr ehs' efs)
interpretTAllH :: forall (ehs' :: [SigClass]) (t :: SigClass) (ehs :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, MonadTrans t, Monad (Eff u fr ehs' efs),
 c (t (Eff u fr ehs' efs))) =>
(u ehs (Eff u fr ehs efs) ~> t (Eff u fr ehs' efs))
-> Eff u fr ehs efs ~> t (Eff u fr ehs' efs)
interpretTAllH u ehs (Eff u fr ehs efs) ~> t (Eff u fr ehs' efs)
i = forall (g :: * -> *) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, c g) =>
(u ehs (Eff u fr ehs efs) ~> g)
-> (u efs Nop ~> g) -> Eff u fr ehs efs ~> g
interpretAllFH u ehs (Eff u fr ehs efs) ~> t (Eff u fr ehs' efs)
i (forall (t :: SigClass) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: (* -> *) -> Constraint) (f :: SigClass)
       (u :: [SigClass] -> SigClass) (efs :: [SigClass])
       (ehs :: [SigClass]).
Freer c f =>
u efs Nop ~> Eff u f ehs efs
injectF)
{-# INLINE interpretTAllH #-}

interpretAllRec ::
    forall efs' ehs efs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs)) =>
    u efs Nop ~> Eff u fr ehs efs' ->
    Eff u fr ehs efs ~> Eff u fr ehs efs'
interpretAllRec :: forall (efs' :: [SigClass]) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u efs Nop ~> Eff u fr ehs efs')
-> Eff u fr ehs efs ~> Eff u fr ehs efs'
interpretAllRec = forall (ehs' :: [SigClass]) (efs' :: [SigClass])
       (ehs :: [SigClass]) (efs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs') ~> Eff u fr ehs' efs')
-> (u efs Nop ~> Eff u fr ehs' efs')
-> Eff u fr ehs efs ~> Eff u fr ehs' efs'
interpretAllRecFHE forall (c :: (* -> *) -> Constraint) (f :: SigClass)
       (u :: [SigClass] -> SigClass) (ehs :: [SigClass])
       (efs :: [SigClass]).
(Freer c f, HFunctor (u ehs)) =>
u ehs (Eff u f ehs efs) ~> Eff u f ehs efs
injectH
{-# INLINE interpretAllRec #-}

transform ::
    forall e2 e1 r ehs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs), HeadIns e1, HeadIns e2) =>
    (UnliftIfSingle e1 ~> UnliftIfSingle e2) ->
    Eff u fr ehs (e1 ': r) ~> Eff u fr ehs (e2 ': r)
transform :: forall (e2 :: SigClass) (e1 :: SigClass) (r :: [SigClass])
       (ehs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs), HeadIns e1, HeadIns e2) =>
(UnliftIfSingle e1 ~> UnliftIfSingle e2)
-> Eff u fr ehs (e1 : r) ~> Eff u fr ehs (e2 : r)
transform UnliftIfSingle e1 ~> UnliftIfSingle e2
f =
    forall (efs' :: [SigClass]) (efs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u efs Nop ~> u efs' Nop) -> Eff u fr ehs efs ~> Eff u fr ehs efs'
transformAll forall a b. (a -> b) -> a -> b
$
        forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       (es :: [SigClass]).
Union u =>
e f ~> u (e : es) f
inject0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (e :: * -> *) (le :: SigClass).
LiftInsIfSingle e le =>
e ~> le Nop
liftInsIfSingle forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnliftIfSingle e1 ~> UnliftIfSingle e2
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (e :: * -> *) (le :: SigClass).
LiftInsIfSingle e le =>
le Nop ~> e
unliftInsIfSingle forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       a r (es :: [SigClass]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [SigClass] -> SigClass) (es :: [SigClass])
       (f :: * -> *) (e :: SigClass).
Union u =>
u es f ~> u (e : es) f
weaken
{-# INLINE transform #-}

transformH ::
    forall e2 e1 r efs fr u c.
    (Freer c fr, Union u, HFunctor (u (e1 ': r))) =>
    (e1 (Eff u fr (e2 ': r) efs) ~> e2 (Eff u fr (e2 ': r) efs)) ->
    Eff u fr (e1 ': r) efs ~> Eff u fr (e2 ': r) efs
transformH :: forall (e2 :: SigClass) (e1 :: SigClass) (r :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u (e1 : r))) =>
(e1 (Eff u fr (e2 : r) efs) ~> e2 (Eff u fr (e2 : r) efs))
-> Eff u fr (e1 : r) efs ~> Eff u fr (e2 : r) efs
transformH e1 (Eff u fr (e2 : r) efs) ~> e2 (Eff u fr (e2 : r) efs)
f = forall (ehs' :: [SigClass]) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs) ~> u ehs' (Eff u fr ehs' efs))
-> Eff u fr ehs efs ~> Eff u fr ehs' efs
transformAllH forall a b. (a -> b) -> a -> b
$ forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       (es :: [SigClass]).
Union u =>
e f ~> u (e : es) f
inject0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. e1 (Eff u fr (e2 : r) efs) ~> e2 (Eff u fr (e2 : r) efs)
f forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       a r (es :: [SigClass]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [SigClass] -> SigClass) (es :: [SigClass])
       (f :: * -> *) (e :: SigClass).
Union u =>
u es f ~> u (e : es) f
weaken
{-# INLINE transformH #-}

transformFH ::
    forall e2h e2f e1h e1f rh rf fr u c.
    (Freer c fr, Union u, HFunctor (u (e1h ': rh)), HeadIns e1f, HeadIns e2f) =>
    (e1h (Eff u fr (e2h ': rh) (e2f ': rf)) ~> e2h (Eff u fr (e2h ': rh) (e2f ': rf))) ->
    (UnliftIfSingle e1f ~> UnliftIfSingle e2f) ->
    Eff u fr (e1h ': rh) (e1f ': rf) ~> Eff u fr (e2h ': rh) (e2f ': rf)
transformFH :: forall (e2h :: SigClass) (e2f :: SigClass) (e1h :: SigClass)
       (e1f :: SigClass) (rh :: [SigClass]) (rf :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u (e1h : rh)), HeadIns e1f,
 HeadIns e2f) =>
(e1h (Eff u fr (e2h : rh) (e2f : rf))
 ~> e2h (Eff u fr (e2h : rh) (e2f : rf)))
-> (UnliftIfSingle e1f ~> UnliftIfSingle e2f)
-> Eff u fr (e1h : rh) (e1f : rf) ~> Eff u fr (e2h : rh) (e2f : rf)
transformFH e1h (Eff u fr (e2h : rh) (e2f : rf))
~> e2h (Eff u fr (e2h : rh) (e2f : rf))
fh UnliftIfSingle e1f ~> UnliftIfSingle e2f
ff =
    forall (ehs' :: [SigClass]) (efs' :: [SigClass])
       (ehs :: [SigClass]) (efs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs') ~> u ehs' (Eff u fr ehs' efs'))
-> (u efs Nop ~> u efs' Nop)
-> Eff u fr ehs efs ~> Eff u fr ehs' efs'
transformAllFH
        (forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       (es :: [SigClass]).
Union u =>
e f ~> u (e : es) f
inject0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. e1h (Eff u fr (e2h : rh) (e2f : rf))
~> e2h (Eff u fr (e2h : rh) (e2f : rf))
fh forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       a r (es :: [SigClass]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [SigClass] -> SigClass) (es :: [SigClass])
       (f :: * -> *) (e :: SigClass).
Union u =>
u es f ~> u (e : es) f
weaken)
        (forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       (es :: [SigClass]).
Union u =>
e f ~> u (e : es) f
inject0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (e :: * -> *) (le :: SigClass).
LiftInsIfSingle e le =>
e ~> le Nop
liftInsIfSingle forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnliftIfSingle e1f ~> UnliftIfSingle e2f
ff forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (e :: * -> *) (le :: SigClass).
LiftInsIfSingle e le =>
le Nop ~> e
unliftInsIfSingle forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       a r (es :: [SigClass]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [SigClass] -> SigClass) (es :: [SigClass])
       (f :: * -> *) (e :: SigClass).
Union u =>
u es f ~> u (e : es) f
weaken)
{-# INLINE transformFH #-}

translate ::
    forall e2 e1 es ehs fr u c.
    (Freer c fr, Union u, Member u e2 es, HFunctor (u ehs), HeadIns e1) =>
    (UnliftIfSingle e1 ~> e2) ->
    Eff u fr ehs (e1 ': es) ~> Eff u fr ehs es
translate :: forall (e2 :: * -> *) (e1 :: SigClass) (es :: [SigClass])
       (ehs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, Member u e2 es, HFunctor (u ehs),
 HeadIns e1) =>
(UnliftIfSingle e1 ~> e2)
-> Eff u fr ehs (e1 : es) ~> Eff u fr ehs es
translate UnliftIfSingle e1 ~> e2
f =
    forall (efs' :: [SigClass]) (efs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u efs Nop ~> u efs' Nop) -> Eff u fr ehs efs ~> Eff u fr ehs efs'
transformAll forall a b. (a -> b) -> a -> b
$
        forall (u :: [SigClass] -> SigClass) (e :: SigClass)
       (es :: [SigClass]) (f :: * -> *).
MemberRec u e es =>
e f ~> u es f
injectRec forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (ins :: * -> *) (f :: * -> *) a. ins a -> LiftIns ins f a
LiftIns forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnliftIfSingle e1 ~> e2
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (e :: * -> *) (le :: SigClass).
LiftInsIfSingle e le =>
le Nop ~> e
unliftInsIfSingle forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       a r (es :: [SigClass]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall a. a -> a
id
{-# INLINE translate #-}

translateH ::
    forall e2 e1 es efs fr u c.
    (Freer c fr, Union u, MemberH u e2 es, HFunctor (u (e1 ': es))) =>
    (e1 (Eff u fr es efs) ~> e2 (Eff u fr es efs)) ->
    Eff u fr (e1 ': es) efs ~> Eff u fr es efs
translateH :: forall (e2 :: SigClass) (e1 :: SigClass) (es :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, MemberH u e2 es, HFunctor (u (e1 : es))) =>
(e1 (Eff u fr es efs) ~> e2 (Eff u fr es efs))
-> Eff u fr (e1 : es) efs ~> Eff u fr es efs
translateH e1 (Eff u fr es efs) ~> e2 (Eff u fr es efs)
f = forall (ehs' :: [SigClass]) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs) ~> u ehs' (Eff u fr ehs' efs))
-> Eff u fr ehs efs ~> Eff u fr ehs' efs
transformAllH forall a b. (a -> b) -> a -> b
$ forall (u :: [SigClass] -> SigClass) (e :: SigClass)
       (es :: [SigClass]) (f :: * -> *).
MemberRec u e es =>
e f ~> u es f
injectRec forall b c a. (b -> c) -> (a -> b) -> a -> c
. e1 (Eff u fr es efs) ~> e2 (Eff u fr es efs)
f forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       a r (es :: [SigClass]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall a. a -> a
id
{-# INLINE translateH #-}

translateFH ::
    forall e2h e2f e1h e1f ehs efs fr u c.
    ( Freer c fr
    , Union u
    , MemberH u e2h ehs
    , Member u e2f efs
    , HFunctor (u (e1h ': ehs))
    , HeadIns e1f
    ) =>
    (e1h (Eff u fr ehs efs) ~> e2h (Eff u fr ehs efs)) ->
    (UnliftIfSingle e1f ~> e2f) ->
    Eff u fr (e1h ': ehs) (e1f ': efs) ~> Eff u fr ehs efs
translateFH :: forall (e2h :: SigClass) (e2f :: * -> *) (e1h :: SigClass)
       (e1f :: SigClass) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, MemberH u e2h ehs, Member u e2f efs,
 HFunctor (u (e1h : ehs)), HeadIns e1f) =>
(e1h (Eff u fr ehs efs) ~> e2h (Eff u fr ehs efs))
-> (UnliftIfSingle e1f ~> e2f)
-> Eff u fr (e1h : ehs) (e1f : efs) ~> Eff u fr ehs efs
translateFH e1h (Eff u fr ehs efs) ~> e2h (Eff u fr ehs efs)
fh UnliftIfSingle e1f ~> e2f
ff =
    forall (ehs' :: [SigClass]) (efs' :: [SigClass])
       (ehs :: [SigClass]) (efs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs') ~> u ehs' (Eff u fr ehs' efs'))
-> (u efs Nop ~> u efs' Nop)
-> Eff u fr ehs efs ~> Eff u fr ehs' efs'
transformAllFH
        (forall (u :: [SigClass] -> SigClass) (e :: SigClass)
       (es :: [SigClass]) (f :: * -> *).
MemberRec u e es =>
e f ~> u es f
injectRec forall b c a. (b -> c) -> (a -> b) -> a -> c
. e1h (Eff u fr ehs efs) ~> e2h (Eff u fr ehs efs)
fh forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       a r (es :: [SigClass]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall a. a -> a
id)
        (forall (u :: [SigClass] -> SigClass) (e :: SigClass)
       (es :: [SigClass]) (f :: * -> *).
MemberRec u e es =>
e f ~> u es f
injectRec forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (ins :: * -> *) (f :: * -> *) a. ins a -> LiftIns ins f a
LiftIns forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnliftIfSingle e1f ~> e2f
ff forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (e :: * -> *) (le :: SigClass).
LiftInsIfSingle e le =>
le Nop ~> e
unliftInsIfSingle forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       a r (es :: [SigClass]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall a. a -> a
id)
{-# INLINE translateFH #-}

rewrite ::
    forall e efs ehs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs), Member u e efs) =>
    (e ~> e) ->
    Eff u fr ehs efs ~> Eff u fr ehs efs
rewrite :: forall (e :: * -> *) (efs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs), Member u e efs) =>
(e ~> e) -> Eff u fr ehs efs ~> Eff u fr ehs efs
rewrite e ~> e
f =
    forall (efs' :: [SigClass]) (efs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u efs Nop ~> u efs' Nop) -> Eff u fr ehs efs ~> Eff u fr ehs efs'
transformAll
        \u efs Nop x
u -> case forall (u :: [SigClass] -> SigClass) (e :: SigClass)
       (es :: [SigClass]) (f :: * -> *) a.
MemberRec u e es =>
u es f a -> Maybe (e f a)
projectRec u efs Nop x
u of
            Just (LiftIns e x
e) -> forall (u :: [SigClass] -> SigClass) (e :: SigClass)
       (es :: [SigClass]) (f :: * -> *).
MemberRec u e es =>
e f ~> u es f
injectRec forall a b. (a -> b) -> a -> b
$ forall (ins :: * -> *) (f :: * -> *) a. ins a -> LiftIns ins f a
LiftIns forall a b. (a -> b) -> a -> b
$ e ~> e
f e x
e
            Maybe (LiftIns e Nop x)
Nothing -> u efs Nop x
u
{-# INLINE rewrite #-}

rewriteH ::
    forall e efs ehs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs), MemberH u e ehs) =>
    (e (Eff u fr ehs efs) ~> e (Eff u fr ehs efs)) ->
    Eff u fr ehs efs ~> Eff u fr ehs efs
rewriteH :: forall (e :: SigClass) (efs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs), MemberH u e ehs) =>
(e (Eff u fr ehs efs) ~> e (Eff u fr ehs efs))
-> Eff u fr ehs efs ~> Eff u fr ehs efs
rewriteH e (Eff u fr ehs efs) ~> e (Eff u fr ehs efs)
f =
    forall (ehs' :: [SigClass]) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs) ~> u ehs' (Eff u fr ehs' efs))
-> Eff u fr ehs efs ~> Eff u fr ehs' efs
transformAllH
        \u ehs (Eff u fr ehs efs) x
u -> case forall (u :: [SigClass] -> SigClass) (e :: SigClass)
       (es :: [SigClass]) (f :: * -> *) a.
MemberRec u e es =>
u es f a -> Maybe (e f a)
projectRec u ehs (Eff u fr ehs efs) x
u of
            Just e (Eff u fr ehs efs) x
e -> forall (u :: [SigClass] -> SigClass) (e :: SigClass)
       (es :: [SigClass]) (f :: * -> *).
MemberRec u e es =>
e f ~> u es f
injectRec forall a b. (a -> b) -> a -> b
$ e (Eff u fr ehs efs) ~> e (Eff u fr ehs efs)
f e (Eff u fr ehs efs) x
e
            Maybe (e (Eff u fr ehs efs) x)
Nothing -> u ehs (Eff u fr ehs efs) x
u
{-# INLINE rewriteH #-}

rewriteFH ::
    forall eh ef efs ehs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs), MemberH u eh ehs, Member u ef efs) =>
    (eh (Eff u fr ehs efs) ~> eh (Eff u fr ehs efs)) ->
    (ef ~> ef) ->
    Eff u fr ehs efs ~> Eff u fr ehs efs
rewriteFH :: forall (eh :: SigClass) (ef :: * -> *) (efs :: [SigClass])
       (ehs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs), MemberH u eh ehs,
 Member u ef efs) =>
(eh (Eff u fr ehs efs) ~> eh (Eff u fr ehs efs))
-> (ef ~> ef) -> Eff u fr ehs efs ~> Eff u fr ehs efs
rewriteFH eh (Eff u fr ehs efs) ~> eh (Eff u fr ehs efs)
fh ef ~> ef
ff =
    forall (ehs' :: [SigClass]) (efs' :: [SigClass])
       (ehs :: [SigClass]) (efs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs') ~> u ehs' (Eff u fr ehs' efs'))
-> (u efs Nop ~> u efs' Nop)
-> Eff u fr ehs efs ~> Eff u fr ehs' efs'
transformAllFH
        ( \u ehs (Eff u fr ehs efs) x
u -> case forall (u :: [SigClass] -> SigClass) (e :: SigClass)
       (es :: [SigClass]) (f :: * -> *) a.
MemberRec u e es =>
u es f a -> Maybe (e f a)
projectRec u ehs (Eff u fr ehs efs) x
u of
            Just eh (Eff u fr ehs efs) x
e -> forall (u :: [SigClass] -> SigClass) (e :: SigClass)
       (es :: [SigClass]) (f :: * -> *).
MemberRec u e es =>
e f ~> u es f
injectRec forall a b. (a -> b) -> a -> b
$ eh (Eff u fr ehs efs) ~> eh (Eff u fr ehs efs)
fh eh (Eff u fr ehs efs) x
e
            Maybe (eh (Eff u fr ehs efs) x)
Nothing -> u ehs (Eff u fr ehs efs) x
u
        )
        ( \u efs Nop x
u -> case forall (u :: [SigClass] -> SigClass) (e :: SigClass)
       (es :: [SigClass]) (f :: * -> *) a.
MemberRec u e es =>
u es f a -> Maybe (e f a)
projectRec u efs Nop x
u of
            Just (LiftIns ef x
e) -> forall (u :: [SigClass] -> SigClass) (e :: SigClass)
       (es :: [SigClass]) (f :: * -> *).
MemberRec u e es =>
e f ~> u es f
injectRec forall a b. (a -> b) -> a -> b
$ forall (ins :: * -> *) (f :: * -> *) a. ins a -> LiftIns ins f a
LiftIns forall a b. (a -> b) -> a -> b
$ ef ~> ef
ff ef x
e
            Maybe (LiftIns ef Nop x)
Nothing -> u efs Nop x
u
        )
{-# INLINE rewriteFH #-}

transformAll ::
    forall efs' efs ehs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs)) =>
    u efs Nop ~> u efs' Nop ->
    Eff u fr ehs efs ~> Eff u fr ehs efs'
transformAll :: forall (efs' :: [SigClass]) (efs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u efs Nop ~> u efs' Nop) -> Eff u fr ehs efs ~> Eff u fr ehs efs'
transformAll = forall (ehs' :: [SigClass]) (efs' :: [SigClass])
       (ehs :: [SigClass]) (efs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs') ~> u ehs' (Eff u fr ehs' efs'))
-> (u efs Nop ~> u efs' Nop)
-> Eff u fr ehs efs ~> Eff u fr ehs' efs'
transformAllFH forall a. a -> a
id
{-# INLINE transformAll #-}

transformAllH ::
    forall ehs' ehs efs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs)) =>
    u ehs (Eff u fr ehs' efs) ~> u ehs' (Eff u fr ehs' efs) ->
    Eff u fr ehs efs ~> Eff u fr ehs' efs
transformAllH :: forall (ehs' :: [SigClass]) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs) ~> u ehs' (Eff u fr ehs' efs))
-> Eff u fr ehs efs ~> Eff u fr ehs' efs
transformAllH u ehs (Eff u fr ehs' efs) ~> u ehs' (Eff u fr ehs' efs)
f = forall (ehs' :: [SigClass]) (efs' :: [SigClass])
       (ehs :: [SigClass]) (efs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs') ~> u ehs' (Eff u fr ehs' efs'))
-> (u efs Nop ~> u efs' Nop)
-> Eff u fr ehs efs ~> Eff u fr ehs' efs'
transformAllFH u ehs (Eff u fr ehs' efs) ~> u ehs' (Eff u fr ehs' efs)
f forall a. a -> a
id
{-# INLINE transformAllH #-}

transformAllFH ::
    forall ehs' efs' ehs efs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs)) =>
    u ehs (Eff u fr ehs' efs') ~> u ehs' (Eff u fr ehs' efs') ->
    (u efs Nop ~> u efs' Nop) ->
    Eff u fr ehs efs ~> Eff u fr ehs' efs'
transformAllFH :: forall (ehs' :: [SigClass]) (efs' :: [SigClass])
       (ehs :: [SigClass]) (efs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs') ~> u ehs' (Eff u fr ehs' efs'))
-> (u efs Nop ~> u efs' Nop)
-> Eff u fr ehs efs ~> Eff u fr ehs' efs'
transformAllFH u ehs (Eff u fr ehs' efs') ~> u ehs' (Eff u fr ehs' efs')
fh u efs Nop ~> u efs' Nop
ff =
    forall (f :: SigClass) (e :: SigClass) a (f' :: SigClass)
       (e' :: SigClass) b.
(f (e (Hefty f e)) a -> f' (e' (Hefty f' e')) b)
-> Hefty f e a -> Hefty f' e' b
overHefty forall a b. (a -> b) -> a -> b
$
        forall (c :: (* -> *) -> Constraint) (f :: SigClass) (e :: * -> *)
       (e' :: * -> *) a.
Freer c f =>
(e ~> e') -> f e a -> f e' a
transformFreer forall a b. (a -> b) -> a -> b
$
            forall (u :: [SigClass] -> SigClass) (ehs :: [SigClass])
       (efs :: [SigClass]) (f :: * -> *) a.
(+) (u ehs f) (u efs Nop) a -> EffUnion u ehs efs f a
EffUnion
                forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [SigClass] -> SigClass) (ehs :: [SigClass])
       (f :: * -> *) a r (efs :: [SigClass]).
(u ehs f a -> r)
-> (u efs Nop a -> r) -> EffUnion u ehs efs f a -> r
caseHF
                    (forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. u ehs (Eff u fr ehs' efs') ~> u ehs' (Eff u fr ehs' efs')
fh forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (h :: SigClass) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap (forall (ehs' :: [SigClass]) (efs' :: [SigClass])
       (ehs :: [SigClass]) (efs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs') ~> u ehs' (Eff u fr ehs' efs'))
-> (u efs Nop ~> u efs' Nop)
-> Eff u fr ehs efs ~> Eff u fr ehs' efs'
transformAllFH u ehs (Eff u fr ehs' efs') ~> u ehs' (Eff u fr ehs' efs')
fh u efs Nop ~> u efs' Nop
ff))
                    (forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. u efs Nop ~> u efs' Nop
ff)

raiseN ::
    forall n ef' eh fr u c ef.
    (Weaken n ef ef', Freer c fr, Union u, HFunctor (u eh)) =>
    Eff u fr eh ef ~> Eff u fr eh ef'
raiseN :: forall (n :: Natural) (ef' :: [SigClass]) (eh :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint) (ef :: [SigClass]).
(Weaken n ef ef', Freer c fr, Union u, HFunctor (u eh)) =>
Eff u fr eh ef ~> Eff u fr eh ef'
raiseN = forall (efs' :: [SigClass]) (efs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u efs Nop ~> u efs' Nop) -> Eff u fr ehs efs ~> Eff u fr ehs efs'
transformAll forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) (u :: [SigClass] -> SigClass)
       (es' :: [SigClass]) (f :: * -> *) (es :: [SigClass]).
(Union u, Weaken n es es') =>
u es f ~> u es' f
weakenN @n

raiseNH ::
    forall n eh' ef fr u c eh.
    (Weaken n eh eh', Freer c fr, Union u, HFunctor (u eh)) =>
    Eff u fr eh ef ~> Eff u fr eh' ef
raiseNH :: forall (n :: Natural) (eh' :: [SigClass]) (ef :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint) (eh :: [SigClass]).
(Weaken n eh eh', Freer c fr, Union u, HFunctor (u eh)) =>
Eff u fr eh ef ~> Eff u fr eh' ef
raiseNH = forall (ehs' :: [SigClass]) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs) ~> u ehs' (Eff u fr ehs' efs))
-> Eff u fr ehs efs ~> Eff u fr ehs' efs
transformAllH forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) (u :: [SigClass] -> SigClass)
       (es' :: [SigClass]) (f :: * -> *) (es :: [SigClass]).
(Union u, Weaken n es es') =>
u es f ~> u es' f
weakenN @n

raiseNUnderM ::
    forall n m ef' eh fr u c ef.
    (WeakenUnder n m ef ef', Freer c fr, Union u, HFunctor (u eh)) =>
    Eff u fr eh ef ~> Eff u fr eh ef'
raiseNUnderM :: forall (n :: Natural) (m :: Natural) (ef' :: [SigClass])
       (eh :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint) (ef :: [SigClass]).
(WeakenUnder n m ef ef', Freer c fr, Union u, HFunctor (u eh)) =>
Eff u fr eh ef ~> Eff u fr eh ef'
raiseNUnderM = forall (efs' :: [SigClass]) (efs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u efs Nop ~> u efs' Nop) -> Eff u fr ehs efs ~> Eff u fr ehs efs'
transformAll forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) (m :: Natural) (u :: [SigClass] -> SigClass)
       (es' :: [SigClass]) (f :: * -> *) (es :: [SigClass]).
(Union u, WeakenUnder n m es es') =>
u es f ~> u es' f
weakenNUnderM @n @m

raiseNUnderMH ::
    forall n m eh' ef fr u c eh.
    (WeakenUnder n m eh eh', Freer c fr, Union u, HFunctor (u eh)) =>
    Eff u fr eh ef ~> Eff u fr eh' ef
raiseNUnderMH :: forall (n :: Natural) (m :: Natural) (eh' :: [SigClass])
       (ef :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint) (eh :: [SigClass]).
(WeakenUnder n m eh eh', Freer c fr, Union u, HFunctor (u eh)) =>
Eff u fr eh ef ~> Eff u fr eh' ef
raiseNUnderMH = forall (ehs' :: [SigClass]) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs) ~> u ehs' (Eff u fr ehs' efs))
-> Eff u fr ehs efs ~> Eff u fr ehs' efs
transformAllH forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) (m :: Natural) (u :: [SigClass] -> SigClass)
       (es' :: [SigClass]) (f :: * -> *) (es :: [SigClass]).
(Union u, WeakenUnder n m es es') =>
u es f ~> u es' f
weakenNUnderM @n @m

subsumeN ::
    forall n ef' eh fr u c ef.
    (Strengthen n u ef ef', Freer c fr, Union u, HFunctor (u eh)) =>
    Eff u fr eh ef ~> Eff u fr eh ef'
subsumeN :: forall (n :: Natural) (ef' :: [SigClass]) (eh :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint) (ef :: [SigClass]).
(Strengthen n u ef ef', Freer c fr, Union u, HFunctor (u eh)) =>
Eff u fr eh ef ~> Eff u fr eh ef'
subsumeN = forall (efs' :: [SigClass]) (efs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u efs Nop ~> u efs' Nop) -> Eff u fr ehs efs ~> Eff u fr ehs efs'
transformAll forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) (u :: [SigClass] -> SigClass)
       (es' :: [SigClass]) (f :: * -> *) (es :: [SigClass]).
Strengthen n u es es' =>
u es f ~> u es' f
strengthenN @n

subsumeNH ::
    forall n eh' ef fr u c eh.
    (Strengthen n u eh eh', Freer c fr, Union u, HFunctor (u eh)) =>
    Eff u fr eh ef ~> Eff u fr eh' ef
subsumeNH :: forall (n :: Natural) (eh' :: [SigClass]) (ef :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint) (eh :: [SigClass]).
(Strengthen n u eh eh', Freer c fr, Union u, HFunctor (u eh)) =>
Eff u fr eh ef ~> Eff u fr eh' ef
subsumeNH = forall (ehs' :: [SigClass]) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs) ~> u ehs' (Eff u fr ehs' efs))
-> Eff u fr ehs efs ~> Eff u fr ehs' efs
transformAllH forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) (u :: [SigClass] -> SigClass)
       (es' :: [SigClass]) (f :: * -> *) (es :: [SigClass]).
Strengthen n u es es' =>
u es f ~> u es' f
strengthenN @n

subsumeNUnderM ::
    forall n m ef' eh fr u c ef.
    (StrengthenUnder n m u ef ef', Freer c fr, Union u, HFunctor (u eh)) =>
    Eff u fr eh ef ~> Eff u fr eh ef'
subsumeNUnderM :: forall (n :: Natural) (m :: Natural) (ef' :: [SigClass])
       (eh :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint) (ef :: [SigClass]).
(StrengthenUnder n m u ef ef', Freer c fr, Union u,
 HFunctor (u eh)) =>
Eff u fr eh ef ~> Eff u fr eh ef'
subsumeNUnderM = forall (efs' :: [SigClass]) (efs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u efs Nop ~> u efs' Nop) -> Eff u fr ehs efs ~> Eff u fr ehs efs'
transformAll forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) (m :: Natural) (u :: [SigClass] -> SigClass)
       (es' :: [SigClass]) (f :: * -> *) (es :: [SigClass]).
StrengthenUnder n m u es es' =>
u es f ~> u es' f
strengthenNUnderM @n @m

subsumeNUnderMH ::
    forall n m eh' ef fr u c eh.
    (StrengthenUnder n m u eh eh', Freer c fr, Union u, HFunctor (u eh)) =>
    Eff u fr eh ef ~> Eff u fr eh' ef
subsumeNUnderMH :: forall (n :: Natural) (m :: Natural) (eh' :: [SigClass])
       (ef :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint) (eh :: [SigClass]).
(StrengthenUnder n m u eh eh', Freer c fr, Union u,
 HFunctor (u eh)) =>
Eff u fr eh ef ~> Eff u fr eh' ef
subsumeNUnderMH = forall (ehs' :: [SigClass]) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs) ~> u ehs' (Eff u fr ehs' efs))
-> Eff u fr ehs efs ~> Eff u fr ehs' efs
transformAllH forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) (m :: Natural) (u :: [SigClass] -> SigClass)
       (es' :: [SigClass]) (f :: * -> *) (es :: [SigClass]).
StrengthenUnder n m u es es' =>
u es f ~> u es' f
strengthenNUnderM @n @m

raise ::
    forall e r ehs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs)) =>
    Eff u fr ehs r ~> Eff u fr ehs (e ': r)
raise :: forall (e :: SigClass) (r :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
Eff u fr ehs r ~> Eff u fr ehs (e : r)
raise = forall (efs' :: [SigClass]) (efs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u efs Nop ~> u efs' Nop) -> Eff u fr ehs efs ~> Eff u fr ehs efs'
transformAll forall (u :: [SigClass] -> SigClass) (es :: [SigClass])
       (f :: * -> *) (e :: SigClass).
Union u =>
u es f ~> u (e : es) f
weaken
{-# INLINE raise #-}

raise2 ::
    forall e2 e1 r ehs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs)) =>
    Eff u fr ehs r ~> Eff u fr ehs (e2 ': e1 ': r)
raise2 :: forall (e2 :: SigClass) (e1 :: SigClass) (r :: [SigClass])
       (ehs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
Eff u fr ehs r ~> Eff u fr ehs (e2 : e1 : r)
raise2 = forall (efs' :: [SigClass]) (efs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u efs Nop ~> u efs' Nop) -> Eff u fr ehs efs ~> Eff u fr ehs efs'
transformAll forall (u :: [SigClass] -> SigClass) (es :: [SigClass])
       (f :: * -> *) (e1 :: SigClass) (e2 :: SigClass).
Union u =>
u es f ~> u (e1 : e2 : es) f
weaken2
{-# INLINE raise2 #-}

raise3 ::
    forall e3 e2 e1 r ehs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs)) =>
    Eff u fr ehs r ~> Eff u fr ehs (e3 ': e2 ': e1 ': r)
raise3 :: forall (e3 :: SigClass) (e2 :: SigClass) (e1 :: SigClass)
       (r :: [SigClass]) (ehs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
Eff u fr ehs r ~> Eff u fr ehs (e3 : e2 : e1 : r)
raise3 = forall (efs' :: [SigClass]) (efs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u efs Nop ~> u efs' Nop) -> Eff u fr ehs efs ~> Eff u fr ehs efs'
transformAll forall (u :: [SigClass] -> SigClass) (es :: [SigClass])
       (f :: * -> *) (e1 :: SigClass) (e2 :: SigClass) (e3 :: SigClass).
Union u =>
u es f ~> u (e1 : e2 : e3 : es) f
weaken3
{-# INLINE raise3 #-}

raise4 ::
    forall e4 e3 e2 e1 r ehs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs)) =>
    Eff u fr ehs r ~> Eff u fr ehs (e4 ': e3 ': e2 ': e1 ': r)
raise4 :: forall (e4 :: SigClass) (e3 :: SigClass) (e2 :: SigClass)
       (e1 :: SigClass) (r :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
Eff u fr ehs r ~> Eff u fr ehs (e4 : e3 : e2 : e1 : r)
raise4 = forall (efs' :: [SigClass]) (efs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u efs Nop ~> u efs' Nop) -> Eff u fr ehs efs ~> Eff u fr ehs efs'
transformAll forall (u :: [SigClass] -> SigClass) (es :: [SigClass])
       (f :: * -> *) (e1 :: SigClass) (e2 :: SigClass) (e3 :: SigClass)
       (e4 :: SigClass).
Union u =>
u es f ~> u (e1 : e2 : e3 : e4 : es) f
weaken4
{-# INLINE raise4 #-}

raiseH ::
    forall e r efs fr u c.
    (Freer c fr, Union u, HFunctor (u r)) =>
    Eff u fr r efs ~> Eff u fr (e ': r) efs
raiseH :: forall (e :: SigClass) (r :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u r)) =>
Eff u fr r efs ~> Eff u fr (e : r) efs
raiseH = forall (ehs' :: [SigClass]) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs) ~> u ehs' (Eff u fr ehs' efs))
-> Eff u fr ehs efs ~> Eff u fr ehs' efs
transformAllH forall (u :: [SigClass] -> SigClass) (es :: [SigClass])
       (f :: * -> *) (e :: SigClass).
Union u =>
u es f ~> u (e : es) f
weaken
{-# INLINE raiseH #-}

raise2H ::
    forall e2 e1 r efs fr u c.
    (Freer c fr, Union u, HFunctor (u r)) =>
    Eff u fr r efs ~> Eff u fr (e2 ': e1 ': r) efs
raise2H :: forall (e2 :: SigClass) (e1 :: SigClass) (r :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u r)) =>
Eff u fr r efs ~> Eff u fr (e2 : e1 : r) efs
raise2H = forall (ehs' :: [SigClass]) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs) ~> u ehs' (Eff u fr ehs' efs))
-> Eff u fr ehs efs ~> Eff u fr ehs' efs
transformAllH forall (u :: [SigClass] -> SigClass) (es :: [SigClass])
       (f :: * -> *) (e1 :: SigClass) (e2 :: SigClass).
Union u =>
u es f ~> u (e1 : e2 : es) f
weaken2
{-# INLINE raise2H #-}

raise3H ::
    forall e3 e2 e1 r efs fr u c.
    (Freer c fr, Union u, HFunctor (u r)) =>
    Eff u fr r efs ~> Eff u fr (e3 ': e2 ': e1 ': r) efs
raise3H :: forall (e3 :: SigClass) (e2 :: SigClass) (e1 :: SigClass)
       (r :: [SigClass]) (efs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u r)) =>
Eff u fr r efs ~> Eff u fr (e3 : e2 : e1 : r) efs
raise3H = forall (ehs' :: [SigClass]) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs) ~> u ehs' (Eff u fr ehs' efs))
-> Eff u fr ehs efs ~> Eff u fr ehs' efs
transformAllH forall (u :: [SigClass] -> SigClass) (es :: [SigClass])
       (f :: * -> *) (e1 :: SigClass) (e2 :: SigClass) (e3 :: SigClass).
Union u =>
u es f ~> u (e1 : e2 : e3 : es) f
weaken3
{-# INLINE raise3H #-}

raise4H ::
    forall e4 e3 e2 e1 r efs fr u c.
    (Freer c fr, Union u, HFunctor (u r)) =>
    Eff u fr r efs ~> Eff u fr (e4 ': e3 ': e2 ': e1 ': r) efs
raise4H :: forall (e4 :: SigClass) (e3 :: SigClass) (e2 :: SigClass)
       (e1 :: SigClass) (r :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u r)) =>
Eff u fr r efs ~> Eff u fr (e4 : e3 : e2 : e1 : r) efs
raise4H = forall (ehs' :: [SigClass]) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs) ~> u ehs' (Eff u fr ehs' efs))
-> Eff u fr ehs efs ~> Eff u fr ehs' efs
transformAllH forall (u :: [SigClass] -> SigClass) (es :: [SigClass])
       (f :: * -> *) (e1 :: SigClass) (e2 :: SigClass) (e3 :: SigClass)
       (e4 :: SigClass).
Union u =>
u es f ~> u (e1 : e2 : e3 : e4 : es) f
weaken4
{-# INLINE raise4H #-}

raiseUnder ::
    forall e1 e2 r ehs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs)) =>
    Eff u fr ehs (e2 ': r) ~> Eff u fr ehs (e2 ': e1 ': r)
raiseUnder :: forall (e1 :: SigClass) (e2 :: SigClass) (r :: [SigClass])
       (ehs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
Eff u fr ehs (e2 : r) ~> Eff u fr ehs (e2 : e1 : r)
raiseUnder = forall (efs' :: [SigClass]) (efs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u efs Nop ~> u efs' Nop) -> Eff u fr ehs efs ~> Eff u fr ehs efs'
transformAll forall (u :: [SigClass] -> SigClass) (e1 :: SigClass)
       (es :: [SigClass]) (f :: * -> *) (e2 :: SigClass).
Union u =>
u (e1 : es) f ~> u (e1 : e2 : es) f
weakenUnder
{-# INLINE raiseUnder #-}

raiseUnder2 ::
    forall e1 e2 e3 r ehs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs)) =>
    Eff u fr ehs (e3 ': e2 ': r) ~> Eff u fr ehs (e3 ': e2 ': e1 ': r)
raiseUnder2 :: forall (e1 :: SigClass) (e2 :: SigClass) (e3 :: SigClass)
       (r :: [SigClass]) (ehs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
Eff u fr ehs (e3 : e2 : r) ~> Eff u fr ehs (e3 : e2 : e1 : r)
raiseUnder2 = forall (efs' :: [SigClass]) (efs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u efs Nop ~> u efs' Nop) -> Eff u fr ehs efs ~> Eff u fr ehs efs'
transformAll forall (u :: [SigClass] -> SigClass) (e1 :: SigClass)
       (e2 :: SigClass) (es :: [SigClass]) (f :: * -> *) (e3 :: SigClass).
Union u =>
u (e1 : e2 : es) f ~> u (e1 : e2 : e3 : es) f
weakenUnder2
{-# INLINE raiseUnder2 #-}

raiseUnder3 ::
    forall e1 e2 e3 e4 r ehs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs)) =>
    Eff u fr ehs (e4 ': e3 ': e2 ': r) ~> Eff u fr ehs (e4 ': e3 ': e2 ': e1 ': r)
raiseUnder3 :: forall (e1 :: SigClass) (e2 :: SigClass) (e3 :: SigClass)
       (e4 :: SigClass) (r :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
Eff u fr ehs (e4 : e3 : e2 : r)
~> Eff u fr ehs (e4 : e3 : e2 : e1 : r)
raiseUnder3 = forall (efs' :: [SigClass]) (efs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u efs Nop ~> u efs' Nop) -> Eff u fr ehs efs ~> Eff u fr ehs efs'
transformAll forall (u :: [SigClass] -> SigClass) (e1 :: SigClass)
       (e2 :: SigClass) (e3 :: SigClass) (es :: [SigClass]) (f :: * -> *)
       (e4 :: SigClass).
Union u =>
u (e1 : e2 : e3 : es) f ~> u (e1 : e2 : e3 : e4 : es) f
weakenUnder3
{-# INLINE raiseUnder3 #-}

raise2Under2 ::
    forall e1 e2 e3 e4 r ehs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs)) =>
    Eff u fr ehs (e4 ': e3 ': r) ~> Eff u fr ehs (e4 ': e3 ': e2 ': e1 ': r)
raise2Under2 :: forall (e1 :: SigClass) (e2 :: SigClass) (e3 :: SigClass)
       (e4 :: SigClass) (r :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
Eff u fr ehs (e4 : e3 : r) ~> Eff u fr ehs (e4 : e3 : e2 : e1 : r)
raise2Under2 = forall (efs' :: [SigClass]) (efs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u efs Nop ~> u efs' Nop) -> Eff u fr ehs efs ~> Eff u fr ehs efs'
transformAll forall (u :: [SigClass] -> SigClass) (e1 :: SigClass)
       (e2 :: SigClass) (es :: [SigClass]) (f :: * -> *) (e3 :: SigClass)
       (e4 :: SigClass).
Union u =>
u (e1 : e2 : es) f ~> u (e1 : e2 : e3 : e4 : es) f
weaken2Under2
{-# INLINE raise2Under2 #-}

raise2Under ::
    forall e1 e2 e3 r ehs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs)) =>
    Eff u fr ehs (e3 ': r) ~> Eff u fr ehs (e3 ': e2 ': e1 ': r)
raise2Under :: forall (e1 :: SigClass) (e2 :: SigClass) (e3 :: SigClass)
       (r :: [SigClass]) (ehs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
Eff u fr ehs (e3 : r) ~> Eff u fr ehs (e3 : e2 : e1 : r)
raise2Under = forall (efs' :: [SigClass]) (efs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u efs Nop ~> u efs' Nop) -> Eff u fr ehs efs ~> Eff u fr ehs efs'
transformAll forall (u :: [SigClass] -> SigClass) (e1 :: SigClass)
       (es :: [SigClass]) (f :: * -> *) (e2 :: SigClass) (e3 :: SigClass).
Union u =>
u (e1 : es) f ~> u (e1 : e2 : e3 : es) f
weaken2Under
{-# INLINE raise2Under #-}

raise3Under ::
    forall e1 e2 e3 e4 r ehs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs)) =>
    Eff u fr ehs (e4 ': r) ~> Eff u fr ehs (e4 ': e3 ': e2 ': e1 ': r)
raise3Under :: forall (e1 :: SigClass) (e2 :: SigClass) (e3 :: SigClass)
       (e4 :: SigClass) (r :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
Eff u fr ehs (e4 : r) ~> Eff u fr ehs (e4 : e3 : e2 : e1 : r)
raise3Under = forall (efs' :: [SigClass]) (efs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u efs Nop ~> u efs' Nop) -> Eff u fr ehs efs ~> Eff u fr ehs efs'
transformAll forall (u :: [SigClass] -> SigClass) (e1 :: SigClass)
       (es :: [SigClass]) (f :: * -> *) (e2 :: SigClass) (e3 :: SigClass)
       (e4 :: SigClass).
Union u =>
u (e1 : es) f ~> u (e1 : e2 : e3 : e4 : es) f
weaken3Under
{-# INLINE raise3Under #-}

raiseUnderH ::
    forall e1 e2 r efs fr u c.
    (Freer c fr, Union u, HFunctor (u (e2 ': r))) =>
    Eff u fr (e2 ': r) efs ~> Eff u fr (e2 ': e1 ': r) efs
raiseUnderH :: forall (e1 :: SigClass) (e2 :: SigClass) (r :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u (e2 : r))) =>
Eff u fr (e2 : r) efs ~> Eff u fr (e2 : e1 : r) efs
raiseUnderH = forall (ehs' :: [SigClass]) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs) ~> u ehs' (Eff u fr ehs' efs))
-> Eff u fr ehs efs ~> Eff u fr ehs' efs
transformAllH forall (u :: [SigClass] -> SigClass) (e1 :: SigClass)
       (es :: [SigClass]) (f :: * -> *) (e2 :: SigClass).
Union u =>
u (e1 : es) f ~> u (e1 : e2 : es) f
weakenUnder
{-# INLINE raiseUnderH #-}

raiseUnder2H ::
    forall e1 e2 e3 r efs fr u c.
    (Freer c fr, Union u, HFunctor (u (e3 ': e2 ': r))) =>
    Eff u fr (e3 ': e2 ': r) efs ~> Eff u fr (e3 ': e2 ': e1 ': r) efs
raiseUnder2H :: forall (e1 :: SigClass) (e2 :: SigClass) (e3 :: SigClass)
       (r :: [SigClass]) (efs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u (e3 : e2 : r))) =>
Eff u fr (e3 : e2 : r) efs ~> Eff u fr (e3 : e2 : e1 : r) efs
raiseUnder2H = forall (ehs' :: [SigClass]) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs) ~> u ehs' (Eff u fr ehs' efs))
-> Eff u fr ehs efs ~> Eff u fr ehs' efs
transformAllH forall (u :: [SigClass] -> SigClass) (e1 :: SigClass)
       (e2 :: SigClass) (es :: [SigClass]) (f :: * -> *) (e3 :: SigClass).
Union u =>
u (e1 : e2 : es) f ~> u (e1 : e2 : e3 : es) f
weakenUnder2
{-# INLINE raiseUnder2H #-}

raiseUnder3H ::
    forall e1 e2 e3 e4 r efs fr u c.
    (Freer c fr, Union u, HFunctor (u (e4 ': e3 ': e2 ': r))) =>
    Eff u fr (e4 ': e3 ': e2 ': r) efs ~> Eff u fr (e4 ': e3 ': e2 ': e1 ': r) efs
raiseUnder3H :: forall (e1 :: SigClass) (e2 :: SigClass) (e3 :: SigClass)
       (e4 :: SigClass) (r :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u (e4 : e3 : e2 : r))) =>
Eff u fr (e4 : e3 : e2 : r) efs
~> Eff u fr (e4 : e3 : e2 : e1 : r) efs
raiseUnder3H = forall (ehs' :: [SigClass]) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs) ~> u ehs' (Eff u fr ehs' efs))
-> Eff u fr ehs efs ~> Eff u fr ehs' efs
transformAllH forall (u :: [SigClass] -> SigClass) (e1 :: SigClass)
       (e2 :: SigClass) (e3 :: SigClass) (es :: [SigClass]) (f :: * -> *)
       (e4 :: SigClass).
Union u =>
u (e1 : e2 : e3 : es) f ~> u (e1 : e2 : e3 : e4 : es) f
weakenUnder3
{-# INLINE raiseUnder3H #-}

raise2Under2H ::
    forall e1 e2 e3 e4 r efs fr u c.
    (Freer c fr, Union u, HFunctor (u (e4 ': e3 ': r))) =>
    Eff u fr (e4 ': e3 ': r) efs ~> Eff u fr (e4 ': e3 ': e2 ': e1 ': r) efs
raise2Under2H :: forall (e1 :: SigClass) (e2 :: SigClass) (e3 :: SigClass)
       (e4 :: SigClass) (r :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u (e4 : e3 : r))) =>
Eff u fr (e4 : e3 : r) efs ~> Eff u fr (e4 : e3 : e2 : e1 : r) efs
raise2Under2H = forall (ehs' :: [SigClass]) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs) ~> u ehs' (Eff u fr ehs' efs))
-> Eff u fr ehs efs ~> Eff u fr ehs' efs
transformAllH forall (u :: [SigClass] -> SigClass) (e1 :: SigClass)
       (e2 :: SigClass) (es :: [SigClass]) (f :: * -> *) (e3 :: SigClass)
       (e4 :: SigClass).
Union u =>
u (e1 : e2 : es) f ~> u (e1 : e2 : e3 : e4 : es) f
weaken2Under2
{-# INLINE raise2Under2H #-}

raise2UnderH ::
    forall e1 e2 e3 r efs fr u c.
    (Freer c fr, Union u, HFunctor (u (e3 ': r))) =>
    Eff u fr (e3 ': r) efs ~> Eff u fr (e3 ': e2 ': e1 ': r) efs
raise2UnderH :: forall (e1 :: SigClass) (e2 :: SigClass) (e3 :: SigClass)
       (r :: [SigClass]) (efs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u (e3 : r))) =>
Eff u fr (e3 : r) efs ~> Eff u fr (e3 : e2 : e1 : r) efs
raise2UnderH = forall (ehs' :: [SigClass]) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs) ~> u ehs' (Eff u fr ehs' efs))
-> Eff u fr ehs efs ~> Eff u fr ehs' efs
transformAllH forall (u :: [SigClass] -> SigClass) (e1 :: SigClass)
       (es :: [SigClass]) (f :: * -> *) (e2 :: SigClass) (e3 :: SigClass).
Union u =>
u (e1 : es) f ~> u (e1 : e2 : e3 : es) f
weaken2Under
{-# INLINE raise2UnderH #-}

raise3UnderH ::
    forall e1 e2 e3 e4 r efs fr u c.
    (Freer c fr, Union u, HFunctor (u (e4 ': r))) =>
    Eff u fr (e4 ': r) efs ~> Eff u fr (e4 ': e3 ': e2 ': e1 ': r) efs
raise3UnderH :: forall (e1 :: SigClass) (e2 :: SigClass) (e3 :: SigClass)
       (e4 :: SigClass) (r :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u (e4 : r))) =>
Eff u fr (e4 : r) efs ~> Eff u fr (e4 : e3 : e2 : e1 : r) efs
raise3UnderH = forall (ehs' :: [SigClass]) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs) ~> u ehs' (Eff u fr ehs' efs))
-> Eff u fr ehs efs ~> Eff u fr ehs' efs
transformAllH forall (u :: [SigClass] -> SigClass) (e1 :: SigClass)
       (es :: [SigClass]) (f :: * -> *) (e2 :: SigClass) (e3 :: SigClass)
       (e4 :: SigClass).
Union u =>
u (e1 : es) f ~> u (e1 : e2 : e3 : e4 : es) f
weaken3Under
{-# INLINE raise3UnderH #-}

raiseAll ::
    forall ehs efs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs)) =>
    Eff u fr ehs '[] ~> Eff u fr ehs efs
raiseAll :: forall (ehs :: [SigClass]) (efs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
Eff u fr ehs '[] ~> Eff u fr ehs efs
raiseAll = forall (efs' :: [SigClass]) (efs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u efs Nop ~> u efs' Nop) -> Eff u fr ehs efs ~> Eff u fr ehs efs'
transformAll forall (u :: [SigClass] -> SigClass) (f :: * -> *) a x.
Union u =>
u '[] f a -> x
exhaust
{-# INLINE raiseAll #-}

raiseAllH ::
    forall ehs efs fr u c.
    (Freer c fr, Union u) =>
    Eff u fr '[] efs ~> Eff u fr ehs efs
raiseAllH :: forall (ehs :: [SigClass]) (efs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u) =>
Eff u fr '[] efs ~> Eff u fr ehs efs
raiseAllH = forall (f :: SigClass) (e :: SigClass) a (f' :: SigClass)
       (e' :: SigClass) b.
(f (e (Hefty f e)) a -> f' (e' (Hefty f' e')) b)
-> Hefty f e a -> Hefty f' e' b
overHefty forall a b. (a -> b) -> a -> b
$ forall (c :: (* -> *) -> Constraint) (f :: SigClass) (e :: * -> *)
       (e' :: * -> *) a.
Freer c f =>
(e ~> e') -> f e a -> f e' a
transformFreer forall a b. (a -> b) -> a -> b
$ forall (u :: [SigClass] -> SigClass) (ehs :: [SigClass])
       (efs :: [SigClass]) (f :: * -> *) a.
(+) (u ehs f) (u efs Nop) a -> EffUnion u ehs efs f a
EffUnion forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [SigClass] -> SigClass) (ehs :: [SigClass])
       (f :: * -> *) a r (efs :: [SigClass]).
(u ehs f a -> r)
-> (u efs Nop a -> r) -> EffUnion u ehs efs f a -> r
caseHF forall (u :: [SigClass] -> SigClass) (f :: * -> *) a x.
Union u =>
u '[] f a -> x
exhaust forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1
{-# INLINE raiseAllH #-}

flipEff ::
    forall e1 e2 r ehs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs)) =>
    Eff u fr ehs (e1 ': e2 ': r) ~> Eff u fr ehs (e2 ': e1 ': r)
flipEff :: forall (e1 :: SigClass) (e2 :: SigClass) (r :: [SigClass])
       (ehs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
Eff u fr ehs (e1 : e2 : r) ~> Eff u fr ehs (e2 : e1 : r)
flipEff = forall (efs' :: [SigClass]) (efs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u efs Nop ~> u efs' Nop) -> Eff u fr ehs efs ~> Eff u fr ehs efs'
transformAll forall (u :: [SigClass] -> SigClass) (e1 :: SigClass)
       (e2 :: SigClass) (es :: [SigClass]) (f :: * -> *).
Union u =>
u (e1 : e2 : es) f ~> u (e2 : e1 : es) f
flipUnion
{-# INLINE flipEff #-}

flipEff3 ::
    forall e1 e2 e3 r ehs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs)) =>
    Eff u fr ehs (e1 ': e2 ': e3 ': r) ~> Eff u fr ehs (e3 ': e2 ': e1 ': r)
flipEff3 :: forall (e1 :: SigClass) (e2 :: SigClass) (e3 :: SigClass)
       (r :: [SigClass]) (ehs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
Eff u fr ehs (e1 : e2 : e3 : r) ~> Eff u fr ehs (e3 : e2 : e1 : r)
flipEff3 = forall (efs' :: [SigClass]) (efs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u efs Nop ~> u efs' Nop) -> Eff u fr ehs efs ~> Eff u fr ehs efs'
transformAll forall (u :: [SigClass] -> SigClass) (e1 :: SigClass)
       (e2 :: SigClass) (e3 :: SigClass) (es :: [SigClass]) (f :: * -> *).
Union u =>
u (e1 : e2 : e3 : es) f ~> u (e3 : e2 : e1 : es) f
flipUnion3
{-# INLINE flipEff3 #-}

flipEffUnder ::
    forall e1 e2 e3 r ehs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs)) =>
    Eff u fr ehs (e3 ': e1 ': e2 ': r) ~> Eff u fr ehs (e3 ': e2 ': e1 ': r)
flipEffUnder :: forall (e1 :: SigClass) (e2 :: SigClass) (e3 :: SigClass)
       (r :: [SigClass]) (ehs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
Eff u fr ehs (e3 : e1 : e2 : r) ~> Eff u fr ehs (e3 : e2 : e1 : r)
flipEffUnder = forall (efs' :: [SigClass]) (efs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u efs Nop ~> u efs' Nop) -> Eff u fr ehs efs ~> Eff u fr ehs efs'
transformAll forall (u :: [SigClass] -> SigClass) (e1 :: SigClass)
       (e2 :: SigClass) (e3 :: SigClass) (es :: [SigClass]) (f :: * -> *).
Union u =>
u (e1 : e2 : e3 : es) f ~> u (e1 : e3 : e2 : es) f
flipUnionUnder
{-# INLINE flipEffUnder #-}

flipEffH ::
    forall e1 e2 r efs fr u c.
    (Freer c fr, Union u, HFunctor (u (e1 ': e2 ': r))) =>
    Eff u fr (e1 ': e2 ': r) efs ~> Eff u fr (e2 ': e1 ': r) efs
flipEffH :: forall (e1 :: SigClass) (e2 :: SigClass) (r :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u (e1 : e2 : r))) =>
Eff u fr (e1 : e2 : r) efs ~> Eff u fr (e2 : e1 : r) efs
flipEffH = forall (ehs' :: [SigClass]) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs) ~> u ehs' (Eff u fr ehs' efs))
-> Eff u fr ehs efs ~> Eff u fr ehs' efs
transformAllH forall (u :: [SigClass] -> SigClass) (e1 :: SigClass)
       (e2 :: SigClass) (es :: [SigClass]) (f :: * -> *).
Union u =>
u (e1 : e2 : es) f ~> u (e2 : e1 : es) f
flipUnion
{-# INLINE flipEffH #-}

flipEff3H ::
    forall e1 e2 e3 r efs fr u c.
    (Freer c fr, Union u, HFunctor (u (e1 ': e2 ': e3 ': r))) =>
    Eff u fr (e1 ': e2 ': e3 ': r) efs ~> Eff u fr (e3 ': e2 ': e1 ': r) efs
flipEff3H :: forall (e1 :: SigClass) (e2 :: SigClass) (e3 :: SigClass)
       (r :: [SigClass]) (efs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u (e1 : e2 : e3 : r))) =>
Eff u fr (e1 : e2 : e3 : r) efs ~> Eff u fr (e3 : e2 : e1 : r) efs
flipEff3H = forall (ehs' :: [SigClass]) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs) ~> u ehs' (Eff u fr ehs' efs))
-> Eff u fr ehs efs ~> Eff u fr ehs' efs
transformAllH forall (u :: [SigClass] -> SigClass) (e1 :: SigClass)
       (e2 :: SigClass) (e3 :: SigClass) (es :: [SigClass]) (f :: * -> *).
Union u =>
u (e1 : e2 : e3 : es) f ~> u (e3 : e2 : e1 : es) f
flipUnion3
{-# INLINE flipEff3H #-}

flipEffUnderH ::
    forall e1 e2 e3 r efs fr u c.
    (Freer c fr, Union u, HFunctor (u (e3 ': e1 ': e2 ': r))) =>
    Eff u fr (e3 ': e1 ': e2 ': r) efs ~> Eff u fr (e3 ': e2 ': e1 ': r) efs
flipEffUnderH :: forall (e1 :: SigClass) (e2 :: SigClass) (e3 :: SigClass)
       (r :: [SigClass]) (efs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u (e3 : e1 : e2 : r))) =>
Eff u fr (e3 : e1 : e2 : r) efs ~> Eff u fr (e3 : e2 : e1 : r) efs
flipEffUnderH = forall (ehs' :: [SigClass]) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs) ~> u ehs' (Eff u fr ehs' efs))
-> Eff u fr ehs efs ~> Eff u fr ehs' efs
transformAllH forall (u :: [SigClass] -> SigClass) (e1 :: SigClass)
       (e2 :: SigClass) (e3 :: SigClass) (es :: [SigClass]) (f :: * -> *).
Union u =>
u (e1 : e2 : e3 : es) f ~> u (e1 : e3 : e2 : es) f
flipUnionUnder
{-# INLINE flipEffUnderH #-}

subsume ::
    forall e r ehs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs), HasMembershipRec u e r) =>
    Eff u fr ehs (e ': r) ~> Eff u fr ehs r
subsume :: forall (e :: SigClass) (r :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs), HasMembershipRec u e r) =>
Eff u fr ehs (e : r) ~> Eff u fr ehs r
subsume = forall (efs' :: [SigClass]) (efs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u efs Nop ~> u efs' Nop) -> Eff u fr ehs efs ~> Eff u fr ehs efs'
transformAll forall a b. (a -> b) -> a -> b
$ forall (u :: [SigClass] -> SigClass) (e :: SigClass)
       (es :: [SigClass]) (f :: * -> *).
MemberRec u e es =>
e f ~> u es f
injectRec forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       a r (es :: [SigClass]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall a. a -> a
id
{-# INLINE subsume #-}

subsumeH ::
    forall e r efs fr u c.
    (Freer c fr, Union u, HFunctor (u (e ': r)), HasMembershipRec u e r) =>
    Eff u fr (e ': r) efs ~> Eff u fr r efs
subsumeH :: forall (e :: SigClass) (r :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u (e : r)),
 HasMembershipRec u e r) =>
Eff u fr (e : r) efs ~> Eff u fr r efs
subsumeH = forall (ehs' :: [SigClass]) (ehs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u ehs (Eff u fr ehs' efs) ~> u ehs' (Eff u fr ehs' efs))
-> Eff u fr ehs efs ~> Eff u fr ehs' efs
transformAllH forall a b. (a -> b) -> a -> b
$ forall (u :: [SigClass] -> SigClass) (e :: SigClass)
       (es :: [SigClass]) (f :: * -> *).
MemberRec u e es =>
e f ~> u es f
injectRec forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       a r (es :: [SigClass]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall a. a -> a
id
{-# INLINE subsumeH #-}

copyEff ::
    forall e r ehs fr u c.
    ( Freer c fr
    , Union u
    , HFunctor (u ehs)
    , Applicative (Eff u fr ehs (e ': r))
    , HeadIns e
    , HasMembershipRec u e r
    ) =>
    Eff u fr ehs (e ': r) ~> Eff u fr ehs (e ': r)
copyEff :: forall (e :: SigClass) (r :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs),
 Applicative (Eff u fr ehs (e : r)), HeadIns e,
 HasMembershipRec u e r) =>
Eff u fr ehs (e : r) ~> Eff u fr ehs (e : r)
copyEff = forall (e2 :: SigClass) (e1 :: SigClass) (r :: [SigClass])
       (ehs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs), HeadIns e1) =>
(UnliftIfSingle e1 ~> Eff u fr ehs (e2 : r))
-> Eff u fr ehs (e1 : r) ~> Eff u fr ehs (e2 : r)
reinterpretRec \UnliftIfSingle e x
e ->
    forall (c :: (* -> *) -> Constraint) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (e :: SigClass) (eh :: [SigClass])
       (r :: [SigClass]).
(Freer c fr, Union u, HeadIns e) =>
UnliftIfSingle e ~> Eff u fr eh (e : r)
send0 UnliftIfSingle e x
e forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (c :: (* -> *) -> Constraint) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (ef :: [SigClass])
       (eh :: [SigClass]).
(Freer c fr, Union u) =>
u ef Nop ~> Eff u fr eh ef
liftEff (forall (u :: [SigClass] -> SigClass) (es :: [SigClass])
       (f :: * -> *) (e :: SigClass).
Union u =>
u es f ~> u (e : es) f
weaken forall a b. (a -> b) -> a -> b
$ forall (u :: [SigClass] -> SigClass) (e :: SigClass)
       (es :: [SigClass]) (f :: * -> *).
MemberRec u e es =>
e f ~> u es f
injectRec forall a b. (a -> b) -> a -> b
$ forall (e :: * -> *) (le :: SigClass).
LiftInsIfSingle e le =>
e ~> le Nop
liftInsIfSingle @_ @e UnliftIfSingle e x
e)

copyEffH ::
    forall e r ef fr u c.
    ( Freer c fr
    , Union u
    , HFunctorUnion u
    , HFunctor e
    , ForallHFunctor u r
    , Applicative (Eff u fr (e ': r) ef)
    , HasMembershipRec u e r
    ) =>
    Eff u fr (e ': r) ef ~> Eff u fr (e ': r) ef
copyEffH :: forall (e :: SigClass) (r :: [SigClass]) (ef :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctorUnion u, HFunctor e,
 ForallHFunctor u r, Applicative (Eff u fr (e : r) ef),
 HasMembershipRec u e r) =>
Eff u fr (e : r) ef ~> Eff u fr (e : r) ef
copyEffH = forall (e2 :: SigClass) (e1 :: SigClass) (r :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, HFunctorUnion u, HFunctor e1, HFunctor e2,
 ForallHFunctor u r) =>
(e1 (Eff u fr (e2 : r) efs) ~> Eff u fr (e2 : r) efs)
-> Eff u fr (e1 : r) efs ~> Eff u fr (e2 : r) efs
reinterpretRecH \e (Eff u fr (e : r) ef) x
e -> forall (c :: (* -> *) -> Constraint) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (e :: SigClass) (r :: [SigClass])
       (ef :: [SigClass]).
(Freer c fr, Union u) =>
e (Eff u fr (e : r) ef) ~> Eff u fr (e : r) ef
send0H e (Eff u fr (e : r) ef) x
e forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (c :: (* -> *) -> Constraint) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (eh :: [SigClass])
       (ef :: [SigClass]).
(Freer c fr, Union u) =>
u eh (Eff u fr eh ef) ~> Eff u fr eh ef
liftEffH (forall (u :: [SigClass] -> SigClass) (es :: [SigClass])
       (f :: * -> *) (e :: SigClass).
Union u =>
u es f ~> u (e : es) f
weaken forall a b. (a -> b) -> a -> b
$ forall (u :: [SigClass] -> SigClass) (e :: SigClass)
       (es :: [SigClass]) (f :: * -> *).
MemberRec u e es =>
e f ~> u es f
injectRec e (Eff u fr (e : r) ef) x
e)

dupEff ::
    forall e r ehs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs), Applicative (Eff u fr ehs (e ': e ': r)), HeadIns e) =>
    Eff u fr ehs (e ': r) ~> Eff u fr ehs (e ': e ': r)
dupEff :: forall (e :: SigClass) (r :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs),
 Applicative (Eff u fr ehs (e : e : r)), HeadIns e) =>
Eff u fr ehs (e : r) ~> Eff u fr ehs (e : e : r)
dupEff = forall (e1 :: SigClass) (e2 :: SigClass) (r :: [SigClass])
       (ehs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
Eff u fr ehs (e2 : r) ~> Eff u fr ehs (e2 : e1 : r)
raiseUnder forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (e2 :: SigClass) (e1 :: SigClass) (r :: [SigClass])
       (ehs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs), HeadIns e1) =>
(UnliftIfSingle e1 ~> Eff u fr ehs (e2 : r))
-> Eff u fr ehs (e1 : r) ~> Eff u fr ehs (e2 : r)
reinterpretRec \UnliftIfSingle e x
e -> forall (c :: (* -> *) -> Constraint) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (e :: SigClass) (eh :: [SigClass])
       (r :: [SigClass]).
(Freer c fr, Union u, HeadIns e) =>
UnliftIfSingle e ~> Eff u fr eh (e : r)
send0 UnliftIfSingle e x
e forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (c :: (* -> *) -> Constraint) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (e1 :: SigClass) (eh :: [SigClass])
       (e2 :: SigClass) (r :: [SigClass]).
(Freer c fr, Union u, HeadIns e1) =>
UnliftIfSingle e1 ~> Eff u fr eh (e2 : e1 : r)
send1 UnliftIfSingle e x
e
{-# INLINE dupEff #-}

dupEffH ::
    forall e r ef fr u c.
    ( Freer c fr
    , Union u
    , Applicative (Eff u fr (e ': e ': r) ef)
    , HFunctorUnion u
    , HFunctor e
    , ForallHFunctor u r
    ) =>
    Eff u fr (e ': r) ef ~> Eff u fr (e ': e ': r) ef
dupEffH :: forall (e :: SigClass) (r :: [SigClass]) (ef :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, Applicative (Eff u fr (e : e : r) ef),
 HFunctorUnion u, HFunctor e, ForallHFunctor u r) =>
Eff u fr (e : r) ef ~> Eff u fr (e : e : r) ef
dupEffH = forall (e1 :: SigClass) (e2 :: SigClass) (r :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u (e2 : r))) =>
Eff u fr (e2 : r) efs ~> Eff u fr (e2 : e1 : r) efs
raiseUnderH forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (e2 :: SigClass) (e1 :: SigClass) (r :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, HFunctorUnion u, HFunctor e1, HFunctor e2,
 ForallHFunctor u r) =>
(e1 (Eff u fr (e2 : r) efs) ~> Eff u fr (e2 : r) efs)
-> Eff u fr (e1 : r) efs ~> Eff u fr (e2 : r) efs
reinterpretRecH \e (Eff u fr (e : e : r) ef) x
e -> forall (c :: (* -> *) -> Constraint) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (e :: SigClass) (r :: [SigClass])
       (ef :: [SigClass]).
(Freer c fr, Union u) =>
e (Eff u fr (e : r) ef) ~> Eff u fr (e : r) ef
send0H e (Eff u fr (e : e : r) ef) x
e forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (c :: (* -> *) -> Constraint) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (e1 :: SigClass) (e2 :: SigClass)
       (r :: [SigClass]) (ef :: [SigClass]).
(Freer c fr, Union u) =>
e1 (Eff u fr (e2 : e1 : r) ef) ~> Eff u fr (e2 : e1 : r) ef
send1H e (Eff u fr (e : e : r) ef) x
e
{-# INLINE dupEffH #-}

bundle ::
    forall e r ehs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs)) =>
    Eff u fr ehs (e ': r) ~> Eff u fr ehs (u '[e] ': r)
bundle :: forall (e :: SigClass) (r :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
Eff u fr ehs (e : r) ~> Eff u fr ehs (u '[e] : r)
bundle = forall (efs' :: [SigClass]) (efs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u efs Nop ~> u efs' Nop) -> Eff u fr ehs efs ~> Eff u fr ehs efs'
transformAll forall a b. (a -> b) -> a -> b
$ forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       (es :: [SigClass]).
Union u =>
e f ~> u (e : es) f
inject0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       (es :: [SigClass]).
Union u =>
e f ~> u (e : es) f
inject0 forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       a r (es :: [SigClass]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [SigClass] -> SigClass) (es :: [SigClass])
       (f :: * -> *) (e :: SigClass).
Union u =>
u es f ~> u (e : es) f
weaken

unbundle ::
    forall e r ehs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs)) =>
    Eff u fr ehs (u '[e] ': r) ~> Eff u fr ehs (e ': r)
unbundle :: forall (e :: SigClass) (r :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
Eff u fr ehs (u '[e] : r) ~> Eff u fr ehs (e : r)
unbundle = forall (efs' :: [SigClass]) (efs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u efs Nop ~> u efs' Nop) -> Eff u fr ehs efs ~> Eff u fr ehs efs'
transformAll forall a b. (a -> b) -> a -> b
$ forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       (es :: [SigClass]).
Union u =>
e f ~> u (e : es) f
inject0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> a
id forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       a r (es :: [SigClass]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [SigClass] -> SigClass) (f :: * -> *) a x.
Union u =>
u '[] f a -> x
end) forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       a r (es :: [SigClass]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [SigClass] -> SigClass) (es :: [SigClass])
       (f :: * -> *) (e :: SigClass).
Union u =>
u es f ~> u (e : es) f
weaken

pushBundle ::
    forall e r1 r2 ehs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs)) =>
    Eff u fr ehs (u r1 ': e ': r2) ~> Eff u fr ehs (u (e ': r1) ': r2)
pushBundle :: forall (e :: SigClass) (r1 :: [SigClass]) (r2 :: [SigClass])
       (ehs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
Eff u fr ehs (u r1 : e : r2) ~> Eff u fr ehs (u (e : r1) : r2)
pushBundle = forall (efs' :: [SigClass]) (efs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u efs Nop ~> u efs' Nop) -> Eff u fr ehs efs ~> Eff u fr ehs efs'
transformAll forall a b. (a -> b) -> a -> b
$ forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       (es :: [SigClass]).
Union u =>
e f ~> u (e : es) f
inject0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [SigClass] -> SigClass) (es :: [SigClass])
       (f :: * -> *) (e :: SigClass).
Union u =>
u es f ~> u (e : es) f
weaken forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       a r (es :: [SigClass]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       (es :: [SigClass]).
Union u =>
e f ~> u (e : es) f
inject0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       (es :: [SigClass]).
Union u =>
e f ~> u (e : es) f
inject0 forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       a r (es :: [SigClass]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [SigClass] -> SigClass) (es :: [SigClass])
       (f :: * -> *) (e :: SigClass).
Union u =>
u es f ~> u (e : es) f
weaken

popBundle ::
    forall e r1 r2 ehs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs)) =>
    Eff u fr ehs (u (e ': r1) ': r2) ~> Eff u fr ehs (u r1 ': e ': r2)
popBundle :: forall (e :: SigClass) (r1 :: [SigClass]) (r2 :: [SigClass])
       (ehs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
Eff u fr ehs (u (e : r1) : r2) ~> Eff u fr ehs (u r1 : e : r2)
popBundle = forall (efs' :: [SigClass]) (efs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u efs Nop ~> u efs' Nop) -> Eff u fr ehs efs ~> Eff u fr ehs efs'
transformAll forall a b. (a -> b) -> a -> b
$ (forall (u :: [SigClass] -> SigClass) (es :: [SigClass])
       (f :: * -> *) (e :: SigClass).
Union u =>
u es f ~> u (e : es) f
weaken forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       (es :: [SigClass]).
Union u =>
e f ~> u (e : es) f
inject0 forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       a r (es :: [SigClass]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       (es :: [SigClass]).
Union u =>
e f ~> u (e : es) f
inject0) forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       a r (es :: [SigClass]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [SigClass] -> SigClass) (es :: [SigClass])
       (f :: * -> *) (e1 :: SigClass) (e2 :: SigClass).
Union u =>
u es f ~> u (e1 : e2 : es) f
weaken2

enqueSum ::
    forall e1 e2 r ehs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs)) =>
    Eff u fr ehs (e1 ': e2 ': r) ~> Eff u fr ehs (e1 :+: e2 ': r)
enqueSum :: forall (e1 :: SigClass) (e2 :: SigClass) (r :: [SigClass])
       (ehs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
Eff u fr ehs (e1 : e2 : r) ~> Eff u fr ehs ((e1 :+: e2) : r)
enqueSum = forall (efs' :: [SigClass]) (efs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u efs Nop ~> u efs' Nop) -> Eff u fr ehs efs ~> Eff u fr ehs efs'
transformAll forall a b. (a -> b) -> a -> b
$ forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       (es :: [SigClass]).
Union u =>
e f ~> u (e : es) f
inject0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: (* -> *) -> k -> *) (g :: (* -> *) -> k -> *)
       (h :: * -> *) (e :: k).
f h e -> (:+:) f g h e
Inl forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       a r (es :: [SigClass]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       (es :: [SigClass]).
Union u =>
e f ~> u (e : es) f
inject0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: (* -> *) -> k -> *) (g :: (* -> *) -> k -> *)
       (h :: * -> *) (e :: k).
g h e -> (:+:) f g h e
Inr forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       a r (es :: [SigClass]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [SigClass] -> SigClass) (es :: [SigClass])
       (f :: * -> *) (e :: SigClass).
Union u =>
u es f ~> u (e : es) f
weaken

dequeSum ::
    forall e1 e2 r ehs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs)) =>
    Eff u fr ehs (e1 :+: e2 ': r) ~> Eff u fr ehs (e1 ': e2 ': r)
dequeSum :: forall (e1 :: SigClass) (e2 :: SigClass) (r :: [SigClass])
       (ehs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
Eff u fr ehs ((e1 :+: e2) : r) ~> Eff u fr ehs (e1 : e2 : r)
dequeSum = forall (efs' :: [SigClass]) (efs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
(u efs Nop ~> u efs' Nop) -> Eff u fr ehs efs ~> Eff u fr ehs efs'
transformAll forall a b. (a -> b) -> a -> b
$ forall {k} (f :: (* -> *) -> k -> *) (a :: * -> *) (b :: k) c
       (g :: (* -> *) -> k -> *).
(f a b -> c) -> (g a b -> c) -> (:+:) f g a b -> c
caseH forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       (es :: [SigClass]).
Union u =>
e f ~> u (e : es) f
inject0 (forall (u :: [SigClass] -> SigClass) (es :: [SigClass])
       (f :: * -> *) (e :: SigClass).
Union u =>
u es f ~> u (e : es) f
weaken forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       (es :: [SigClass]).
Union u =>
e f ~> u (e : es) f
inject0) forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       a r (es :: [SigClass]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [SigClass] -> SigClass) (es :: [SigClass])
       (f :: * -> *) (e1 :: SigClass) (e2 :: SigClass).
Union u =>
u es f ~> u (e1 : e2 : es) f
weaken2

liftInsEff ::
    forall e eh ef fr u c.
    (Freer c fr, Union u, HFunctor (u eh), HFunctor e) =>
    Eff u fr eh (e ': ef) ~> Eff u fr (e ': eh) ef
liftInsEff :: forall (e :: SigClass) (eh :: [SigClass]) (ef :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u eh), HFunctor e) =>
Eff u fr eh (e : ef) ~> Eff u fr (e : eh) ef
liftInsEff =
    forall (f :: SigClass) (e :: SigClass) a (f' :: SigClass)
       (e' :: SigClass) b.
(f (e (Hefty f e)) a -> f' (e' (Hefty f' e')) b)
-> Hefty f e a -> Hefty f' e' b
overHefty forall a b. (a -> b) -> a -> b
$
        forall (c :: (* -> *) -> Constraint) (f :: SigClass) (e :: * -> *)
       (e' :: * -> *) a.
Freer c f =>
(e ~> e') -> f e a -> f e' a
transformFreer forall a b. (a -> b) -> a -> b
$
            forall (u :: [SigClass] -> SigClass) (ehs :: [SigClass])
       (efs :: [SigClass]) (f :: * -> *) a.
(+) (u ehs f) (u efs Nop) a -> EffUnion u ehs efs f a
EffUnion
                forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [SigClass] -> SigClass) (ehs :: [SigClass])
       (f :: * -> *) a r (efs :: [SigClass]).
(u ehs f a -> r)
-> (u efs Nop a -> r) -> EffUnion u ehs efs f a -> r
caseHF
                    (forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [SigClass] -> SigClass) (es :: [SigClass])
       (f :: * -> *) (e :: SigClass).
Union u =>
u es f ~> u (e : es) f
weaken forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (h :: SigClass) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap forall (e :: SigClass) (eh :: [SigClass]) (ef :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u eh), HFunctor e) =>
Eff u fr eh (e : ef) ~> Eff u fr (e : eh) ef
liftInsEff)
                    (forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       (es :: [SigClass]).
Union u =>
e f ~> u (e : es) f
inject0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (h :: SigClass) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap \case {} forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       a r (es :: [SigClass]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1)

splitEff ::
    forall fr' e r ehs fr u c.
    (Freer c fr', Freer c fr, Union u, HeadIns e) =>
    Eff u fr '[] (e ': r) ~> fr' (UnliftIfSingle e + Eff u fr ehs r)
splitEff :: forall (fr' :: SigClass) (e :: SigClass) (r :: [SigClass])
       (ehs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr', Freer c fr, Union u, HeadIns e) =>
Eff u fr '[] (e : r) ~> fr' (UnliftIfSingle e + Eff u fr ehs r)
splitEff = forall (g :: * -> *) (efs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, c g) =>
(u efs Nop ~> g) -> Eff u fr '[] efs ~> g
interpretAll forall a b. (a -> b) -> a -> b
$ forall (c :: (* -> *) -> Constraint) (f :: SigClass) (e :: * -> *)
       a.
Freer c f =>
e a -> f e a
liftIns forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (e :: * -> *) (le :: SigClass).
LiftInsIfSingle e le =>
le Nop ~> e
unliftInsIfSingle forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       a r (es :: [SigClass]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: (* -> *) -> Constraint) (f :: SigClass)
       (u :: [SigClass] -> SigClass) (efs :: [SigClass])
       (ehs :: [SigClass]).
Freer c f =>
u efs Nop ~> Eff u f ehs efs
injectF)
{-# INLINE splitEff #-}

mergeEff ::
    forall fr' e r ehs fr u c.
    (Freer c fr', Freer c fr, Union u, HeadIns e, c (Eff u fr ehs (e ': r)), HFunctor (u ehs)) =>
    fr' (UnliftIfSingle e + Eff u fr ehs r) ~> Eff u fr ehs (e ': r)
mergeEff :: forall (fr' :: SigClass) (e :: SigClass) (r :: [SigClass])
       (ehs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr', Freer c fr, Union u, HeadIns e,
 c (Eff u fr ehs (e : r)), HFunctor (u ehs)) =>
fr' (UnliftIfSingle e + Eff u fr ehs r) ~> Eff u fr ehs (e : r)
mergeEff = forall (c :: (* -> *) -> Constraint) (f :: SigClass) (m :: * -> *)
       (e :: * -> *) a.
(Freer c f, c m) =>
(e ~> m) -> f e a -> m a
interpretFreer forall a b. (a -> b) -> a -> b
$ forall {k} (f :: k -> *) (a :: k) r (g :: k -> *).
(f a -> r) -> (g a -> r) -> (+) f g a -> r
caseF forall (c :: (* -> *) -> Constraint) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (e :: SigClass) (eh :: [SigClass])
       (r :: [SigClass]).
(Freer c fr, Union u, HeadIns e) =>
UnliftIfSingle e ~> Eff u fr eh (e : r)
send0 forall (e :: SigClass) (r :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
Eff u fr ehs r ~> Eff u fr ehs (e : r)
raise
{-# INLINE mergeEff #-}

mergeEffH ::
    forall fr' e r efs fr u c.
    ( Freer c fr'
    , Freer c fr
    , Union u
    , c (Eff u fr (e ': r) efs)
    , HFunctor (u r)
    , HFunctor e
    ) =>
    Hefty fr' (e :+: LiftIns (Eff u fr r efs)) ~> Eff u fr (e ': r) efs
mergeEffH :: forall (fr' :: SigClass) (e :: SigClass) (r :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr', Freer c fr, Union u, c (Eff u fr (e : r) efs),
 HFunctor (u r), HFunctor e) =>
Hefty fr' (e :+: LiftIns (Eff u fr r efs)) ~> Eff u fr (e : r) efs
mergeEffH =
    forall (c :: (* -> *) -> Constraint) (f :: SigClass) (m :: * -> *)
       (e :: * -> *) a.
(Freer c f, c m) =>
(e ~> m) -> f e a -> m a
interpretFreer
        ( forall {k} (f :: (* -> *) -> k -> *) (a :: * -> *) (b :: k) c
       (g :: (* -> *) -> k -> *).
(f a b -> c) -> (g a b -> c) -> (:+:) f g a b -> c
caseH
            (forall (c :: (* -> *) -> Constraint) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (e :: SigClass) (r :: [SigClass])
       (ef :: [SigClass]).
(Freer c fr, Union u) =>
e (Eff u fr (e : r) ef) ~> Eff u fr (e : r) ef
send0H forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (h :: SigClass) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap forall (fr' :: SigClass) (e :: SigClass) (r :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr', Freer c fr, Union u, c (Eff u fr (e : r) efs),
 HFunctor (u r), HFunctor e) =>
Hefty fr' (e :+: LiftIns (Eff u fr r efs)) ~> Eff u fr (e : r) efs
mergeEffH)
            (forall (e :: SigClass) (r :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u r)) =>
Eff u fr r efs ~> Eff u fr (e : r) efs
raiseH forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (ins :: * -> *) (f :: * -> *) a. LiftIns ins f a -> ins a
unliftIns)
        )
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: SigClass) (e :: SigClass) a.
Hefty f e a -> f (e (Hefty f e)) a
unHefty

send0 :: (Freer c fr, Union u, HeadIns e) => UnliftIfSingle e ~> Eff u fr eh (e ': r)
send0 :: forall (c :: (* -> *) -> Constraint) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (e :: SigClass) (eh :: [SigClass])
       (r :: [SigClass]).
(Freer c fr, Union u, HeadIns e) =>
UnliftIfSingle e ~> Eff u fr eh (e : r)
send0 = forall (c :: (* -> *) -> Constraint) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (ef :: [SigClass])
       (eh :: [SigClass]).
(Freer c fr, Union u) =>
u ef Nop ~> Eff u fr eh ef
liftEff forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       (es :: [SigClass]).
Union u =>
e f ~> u (e : es) f
inject0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (e :: * -> *) (le :: SigClass).
LiftInsIfSingle e le =>
e ~> le Nop
liftInsIfSingle
{-# INLINE send0 #-}

send1 :: (Freer c fr, Union u, HeadIns e1) => UnliftIfSingle e1 ~> Eff u fr eh (e2 ': e1 ': r)
send1 :: forall (c :: (* -> *) -> Constraint) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (e1 :: SigClass) (eh :: [SigClass])
       (e2 :: SigClass) (r :: [SigClass]).
(Freer c fr, Union u, HeadIns e1) =>
UnliftIfSingle e1 ~> Eff u fr eh (e2 : e1 : r)
send1 = forall (c :: (* -> *) -> Constraint) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (ef :: [SigClass])
       (eh :: [SigClass]).
(Freer c fr, Union u) =>
u ef Nop ~> Eff u fr eh ef
liftEff forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [SigClass] -> SigClass) (es :: [SigClass])
       (f :: * -> *) (e :: SigClass).
Union u =>
u es f ~> u (e : es) f
weaken forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       (es :: [SigClass]).
Union u =>
e f ~> u (e : es) f
inject0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (e :: * -> *) (le :: SigClass).
LiftInsIfSingle e le =>
e ~> le Nop
liftInsIfSingle
{-# INLINE send1 #-}

send0H :: (Freer c fr, Union u) => e (Eff u fr (e ': r) ef) ~> Eff u fr (e ': r) ef
send0H :: forall (c :: (* -> *) -> Constraint) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (e :: SigClass) (r :: [SigClass])
       (ef :: [SigClass]).
(Freer c fr, Union u) =>
e (Eff u fr (e : r) ef) ~> Eff u fr (e : r) ef
send0H = forall (c :: (* -> *) -> Constraint) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (eh :: [SigClass])
       (ef :: [SigClass]).
(Freer c fr, Union u) =>
u eh (Eff u fr eh ef) ~> Eff u fr eh ef
liftEffH forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       (es :: [SigClass]).
Union u =>
e f ~> u (e : es) f
inject0
{-# INLINE send0H #-}

send1H :: (Freer c fr, Union u) => e1 (Eff u fr (e2 ': e1 ': r) ef) ~> Eff u fr (e2 ': e1 ': r) ef
send1H :: forall (c :: (* -> *) -> Constraint) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (e1 :: SigClass) (e2 :: SigClass)
       (r :: [SigClass]) (ef :: [SigClass]).
(Freer c fr, Union u) =>
e1 (Eff u fr (e2 : e1 : r) ef) ~> Eff u fr (e2 : e1 : r) ef
send1H = forall (c :: (* -> *) -> Constraint) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (eh :: [SigClass])
       (ef :: [SigClass]).
(Freer c fr, Union u) =>
u eh (Eff u fr eh ef) ~> Eff u fr eh ef
liftEffH forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [SigClass] -> SigClass) (es :: [SigClass])
       (f :: * -> *) (e :: SigClass).
Union u =>
u es f ~> u (e : es) f
weaken forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       (es :: [SigClass]).
Union u =>
e f ~> u (e : es) f
inject0
{-# INLINE send1H #-}

liftEff :: (Freer c fr, Union u) => u ef Nop ~> Eff u fr eh ef
liftEff :: forall (c :: (* -> *) -> Constraint) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (ef :: [SigClass])
       (eh :: [SigClass]).
(Freer c fr, Union u) =>
u ef Nop ~> Eff u fr eh ef
liftEff = forall (f :: SigClass) (e :: SigClass) a.
f (e (Hefty f e)) a -> Hefty f e a
Hefty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: (* -> *) -> Constraint) (f :: SigClass) (e :: * -> *)
       a.
Freer c f =>
e a -> f e a
liftIns forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [SigClass] -> SigClass) (ehs :: [SigClass])
       (efs :: [SigClass]) (f :: * -> *) a.
(+) (u ehs f) (u efs Nop) a -> EffUnion u ehs efs f a
EffUnion forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1
{-# INLINE liftEff #-}

liftEffH :: (Freer c fr, Union u) => u eh (Eff u fr eh ef) ~> Eff u fr eh ef
liftEffH :: forall (c :: (* -> *) -> Constraint) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (eh :: [SigClass])
       (ef :: [SigClass]).
(Freer c fr, Union u) =>
u eh (Eff u fr eh ef) ~> Eff u fr eh ef
liftEffH = forall (f :: SigClass) (e :: SigClass) a.
f (e (Hefty f e)) a -> Hefty f e a
Hefty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: (* -> *) -> Constraint) (f :: SigClass) (e :: * -> *)
       a.
Freer c f =>
e a -> f e a
liftIns forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [SigClass] -> SigClass) (ehs :: [SigClass])
       (efs :: [SigClass]) (f :: * -> *) a.
(+) (u ehs f) (u efs Nop) a -> EffUnion u ehs efs f a
EffUnion forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1
{-# INLINE liftEffH #-}

runEff :: forall f fr u c. (Freer c fr, Union u, c f) => Eff u fr '[] '[LiftIns f] ~> f
runEff :: forall (f :: * -> *) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, c f) =>
Eff u fr '[] '[LiftIns f] ~> f
runEff = forall (g :: * -> *) (efs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, c g) =>
(u efs Nop ~> g) -> Eff u fr '[] efs ~> g
interpretAll forall a b. (a -> b) -> a -> b
$ forall a. a -> a
id forall (u :: [SigClass] -> SigClass) (e :: * -> *) a r
       (es :: [SigClass]) (f :: * -> *).
Union u =>
(e a -> r) -> (u es f a -> r) -> u (LiftIns e : es) f a -> r
|+ forall (u :: [SigClass] -> SigClass) (f :: * -> *) a x.
Union u =>
u '[] f a -> x
exhaust
{-# INLINE runEff #-}

runPure :: forall a fr u c. (Freer c fr, Union u, c Identity) => Eff u fr '[] '[] a -> a
runPure :: forall a (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, c Identity) =>
Eff u fr '[] '[] a -> a
runPure = forall a. Identity a -> a
runIdentity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (g :: * -> *) (efs :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, c g) =>
(u efs Nop ~> g) -> Eff u fr '[] efs ~> g
interpretAll forall (u :: [SigClass] -> SigClass) (f :: * -> *) a x.
Union u =>
u '[] f a -> x
exhaust
{-# INLINE runPure #-}

tagEff ::
    forall tag e r ehs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs)) =>
    Eff u fr ehs (LiftIns e ': r) ~> Eff u fr ehs (LiftIns (e # tag) ': r)
tagEff :: forall {k} (tag :: k) (e :: * -> *) (r :: [SigClass])
       (ehs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
Eff u fr ehs (LiftIns e : r)
~> Eff u fr ehs (LiftIns (e # tag) : r)
tagEff = forall (e2 :: SigClass) (e1 :: SigClass) (r :: [SigClass])
       (ehs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs), HeadIns e1, HeadIns e2) =>
(UnliftIfSingle e1 ~> UnliftIfSingle e2)
-> Eff u fr ehs (e1 : r) ~> Eff u fr ehs (e2 : r)
transform forall {k} (ins :: * -> *) (tag :: k) a. ins a -> Tag ins tag a
Tag
{-# INLINE tagEff #-}

tagEffH ::
    forall tag e r efs fr u c.
    (Freer c fr, Union u, HFunctor (u (e ': r))) =>
    Eff u fr (e ': r) efs ~> Eff u fr (e ## tag ': r) efs
tagEffH :: forall {k} (tag :: k) (e :: SigClass) (r :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u (e : r))) =>
Eff u fr (e : r) efs ~> Eff u fr ((e ## tag) : r) efs
tagEffH = forall (e2 :: SigClass) (e1 :: SigClass) (r :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u (e1 : r))) =>
(e1 (Eff u fr (e2 : r) efs) ~> e2 (Eff u fr (e2 : r) efs))
-> Eff u fr (e1 : r) efs ~> Eff u fr (e2 : r) efs
transformH forall {k} (sig :: SigClass) (tag :: k) (f :: * -> *) a.
sig f a -> TagH sig tag f a
TagH
{-# INLINE tagEffH #-}

untagEff ::
    forall tag e r ehs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs)) =>
    Eff u fr ehs (LiftIns (e # tag) ': r) ~> Eff u fr ehs (LiftIns e ': r)
untagEff :: forall {k} (tag :: k) (e :: * -> *) (r :: [SigClass])
       (ehs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
Eff u fr ehs (LiftIns (e # tag) : r)
~> Eff u fr ehs (LiftIns e : r)
untagEff = forall (e2 :: SigClass) (e1 :: SigClass) (r :: [SigClass])
       (ehs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs), HeadIns e1, HeadIns e2) =>
(UnliftIfSingle e1 ~> UnliftIfSingle e2)
-> Eff u fr ehs (e1 : r) ~> Eff u fr ehs (e2 : r)
transform forall {k} (ins :: * -> *) (tag :: k) a. Tag ins tag a -> ins a
unTag
{-# INLINE untagEff #-}

untagEffH ::
    forall tag e r efs fr u c.
    (Freer c fr, Union u, HFunctor (u (e ## tag ': r))) =>
    Eff u fr (e ## tag ': r) efs ~> Eff u fr (e ': r) efs
untagEffH :: forall {k} (tag :: k) (e :: SigClass) (r :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ((e ## tag) : r))) =>
Eff u fr ((e ## tag) : r) efs ~> Eff u fr (e : r) efs
untagEffH = forall (e2 :: SigClass) (e1 :: SigClass) (r :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u (e1 : r))) =>
(e1 (Eff u fr (e2 : r) efs) ~> e2 (Eff u fr (e2 : r) efs))
-> Eff u fr (e1 : r) efs ~> Eff u fr (e2 : r) efs
transformH forall {k} (sig :: SigClass) (tag :: k) (f :: * -> *) a.
TagH sig tag f a -> sig f a
unTagH
{-# INLINE untagEffH #-}

-- keyed effects

instance
    (MemberRec u (LiftIns (key #> e)) efs, LiftIns (key #> e) ~ FromJust (Lookup key efs)) =>
    InjectInsBy key e (EffUnion u ehs efs f)
    where
    injectInsBy :: e ~> EffUnion u ehs efs f
injectInsBy = forall (u :: [SigClass] -> SigClass) (ehs :: [SigClass])
       (efs :: [SigClass]) (f :: * -> *) a.
(+) (u ehs f) (u efs Nop) a -> EffUnion u ehs efs f a
EffUnion forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [SigClass] -> SigClass) (e :: SigClass)
       (es :: [SigClass]) (f :: * -> *).
MemberRec u e es =>
e f ~> u es f
injectRec forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (ins :: * -> *) (f :: * -> *) a. ins a -> LiftIns ins f a
LiftIns forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (key :: k) (ins :: * -> *) a. ins a -> Key key ins a
Key @key
    {-# INLINE injectInsBy #-}

instance
    (MemberRec u (key ##> e) ehs, key ##> e ~ FromJust (Lookup key ehs)) =>
    InjectSigBy key e (EffUnion u ehs efs)
    where
    injectSigBy :: forall (f :: * -> *). e f ~> EffUnion u ehs efs f
injectSigBy = forall (u :: [SigClass] -> SigClass) (ehs :: [SigClass])
       (efs :: [SigClass]) (f :: * -> *) a.
(+) (u ehs f) (u efs Nop) a -> EffUnion u ehs efs f a
EffUnion forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [SigClass] -> SigClass) (e :: SigClass)
       (es :: [SigClass]) (f :: * -> *).
MemberRec u e es =>
e f ~> u es f
injectRec forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (key :: k) (sig :: SigClass) (f :: * -> *) a.
sig f a -> KeyH key sig f a
KeyH @key
    {-# INLINE injectSigBy #-}

unkeyEff ::
    forall key e r ehs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs)) =>
    Eff u fr ehs (LiftIns (key #> e) ': r) ~> Eff u fr ehs (LiftIns e ': r)
unkeyEff :: forall {k} (key :: k) (e :: * -> *) (r :: [SigClass])
       (ehs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
Eff u fr ehs (LiftIns (key #> e) : r)
~> Eff u fr ehs (LiftIns e : r)
unkeyEff = forall (e2 :: SigClass) (e1 :: SigClass) (r :: [SigClass])
       (ehs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs), HeadIns e1, HeadIns e2) =>
(UnliftIfSingle e1 ~> UnliftIfSingle e2)
-> Eff u fr ehs (e1 : r) ~> Eff u fr ehs (e2 : r)
transform forall {k} (key :: k) (ins :: * -> *) a. Key key ins a -> ins a
unKey
{-# INLINE unkeyEff #-}

unkeyEffH ::
    forall key e r efs fr u c.
    (Freer c fr, Union u, HFunctor (u (key ##> e ': r))) =>
    Eff u fr (key ##> e ': r) efs ~> Eff u fr (e ': r) efs
unkeyEffH :: forall {k} (key :: k) (e :: SigClass) (r :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ((key ##> e) : r))) =>
Eff u fr ((key ##> e) : r) efs ~> Eff u fr (e : r) efs
unkeyEffH = forall (e2 :: SigClass) (e1 :: SigClass) (r :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u (e1 : r))) =>
(e1 (Eff u fr (e2 : r) efs) ~> e2 (Eff u fr (e2 : r) efs))
-> Eff u fr (e1 : r) efs ~> Eff u fr (e2 : r) efs
transformH forall {k} (key :: k) (sig :: SigClass) (f :: * -> *) a.
KeyH key sig f a -> sig f a
unKeyH
{-# INLINE unkeyEffH #-}

keySubsume ::
    forall key e r ehs fr u c.
    (Freer c fr, Union u, HFunctor (u ehs), MemberBy u key e r) =>
    Eff u fr ehs (LiftIns e ': r) ~> Eff u fr ehs r
keySubsume :: forall {k} (key :: k) (e :: * -> *) (r :: [SigClass])
       (ehs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs), MemberBy u key e r) =>
Eff u fr ehs (LiftIns e : r) ~> Eff u fr ehs r
keySubsume = forall (e :: SigClass) (rs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs), HeadIns e) =>
(UnliftIfSingle e ~> Eff u fr ehs rs)
-> Eff u fr ehs (e : rs) ~> Eff u fr ehs rs
interpretRec forall a b. (a -> b) -> a -> b
$ forall {k} (key :: k) (ins :: * -> *) (f :: * -> *) a.
SendInsBy key ins f =>
ins a -> f a
sendInsBy @key
{-# INLINE keySubsume #-}

keySubsumeH ::
    forall key e r efs fr u c.
    (Freer c fr, HFunctorUnion u, HFunctor e, ForallHFunctor u r, MemberHBy u key e r) =>
    Eff u fr (e ': r) efs ~> Eff u fr r efs
keySubsumeH :: forall {k} (key :: k) (e :: SigClass) (r :: [SigClass])
       (efs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, HFunctorUnion u, HFunctor e, ForallHFunctor u r,
 MemberHBy u key e r) =>
Eff u fr (e : r) efs ~> Eff u fr r efs
keySubsumeH = forall (e :: SigClass) (rs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor e, HFunctor (u rs),
 HFunctor (u (e : rs))) =>
(e (Eff u fr rs efs) ~> Eff u fr rs efs)
-> Eff u fr (e : rs) efs ~> Eff u fr rs efs
interpretRecH forall a b. (a -> b) -> a -> b
$ forall {k} (key :: k) (sig :: SigClass) (f :: * -> *) a.
SendSigBy key sig f =>
sig f a -> f a
sendSigBy @key
{-# INLINE keySubsumeH #-}

end :: Union u => u '[] f a -> x
end :: forall (u :: [SigClass] -> SigClass) (f :: * -> *) a x.
Union u =>
u '[] f a -> x
end = forall (u :: [SigClass] -> SigClass) (f :: * -> *) a x.
Union u =>
u '[] f a -> x
exhaust
{-# INLINE end #-}