module Control.Monad.Ology.Specific.StackT
    ( witTransStackDict
    , IsStack
    , transStackDict
    , StackT(..)
    , stackLift
    , stackHoist
    , WithTunnelConstraint
    , MonadTransStackTunnel
    , transStackExcept
    , stackUnderliftIO
    , stackBackHoist
    , MonadTransStackUnlift
    , concatMonadTransStackUnliftDict
    , stackLiftWithUnlift
    , stackConcatFst
    , stackConcatSnd
    , stackCommute
    , transStackConcatRefl
    , StackUnlift
    , WStackUnlift(..)
    , consWStackUnlift
    , stackLiftWithStackUnlift
    ) where

import Control.Monad.Ology.General
import Control.Monad.Ology.Specific.ComposeInner
import Control.Monad.Ology.Specific.ExceptT
import Import

witTransStackDict ::
       forall cm tt m. (cm m)
    => ListType (Compose Dict (TransConstraint cm)) tt
    -> Dict (cm (ApplyStack tt m))
witTransStackDict :: forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
       (m :: Type -> Type).
cm m =>
ListType (Compose Dict (TransConstraint cm)) tt
-> Dict (cm (ApplyStack tt m))
witTransStackDict ListType (Compose Dict (TransConstraint cm)) tt
NilListType = forall (a :: Constraint). a => Dict a
Dict
witTransStackDict (ConsListType (Compose Dict (TransConstraint cm a)
Dict) ListType (Compose Dict (TransConstraint cm)) lt1
lt) =
    case forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
       (m :: Type -> Type).
cm m =>
ListType (Compose Dict (TransConstraint cm)) tt
-> Dict (cm (ApplyStack tt m))
witTransStackDict @cm @_ @m ListType (Compose Dict (TransConstraint cm)) lt1
lt of
        Dict (cm (ApplyStack lt1 m))
d -> forall (c :: (Type -> Type) -> Constraint) (t :: TransKind)
       (m :: Type -> Type).
TransConstraint c t =>
Dict (c m) -> Dict (c (t m))
transConstraintDict @cm Dict (cm (ApplyStack lt1 m))
d

type IsStack :: (TransKind -> Constraint) -> [TransKind] -> Constraint
type IsStack ct = Is (ListType (Compose Dict ct))

transStackDict ::
       forall cm tt m. (IsStack (TransConstraint cm) tt, cm m)
    => Dict (cm (ApplyStack tt m))
transStackDict :: forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
       (m :: Type -> Type).
(IsStack (TransConstraint cm) tt, cm m) =>
Dict (cm (ApplyStack tt m))
transStackDict = forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
       (m :: Type -> Type).
cm m =>
ListType (Compose Dict (TransConstraint cm)) tt
-> Dict (cm (ApplyStack tt m))
witTransStackDict @cm @tt @m forall a b. (a -> b) -> a -> b
$ forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative @_ @(ListType (Compose Dict (TransConstraint cm))) @tt

-- | A monad transformer that is the composition of a list of monad transformers.
type StackT :: [TransKind] -> TransKind
newtype StackT (tt :: [TransKind]) m a = MkStackT
    { forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT :: ApplyStack tt m a
    }

instance (IsStack (TransConstraint Monad) tt, Monad m) => Functor (StackT tt m) where
    fmap :: forall a b. (a -> b) -> StackT tt m a -> StackT tt m b
fmap =
        case forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
       (m :: Type -> Type).
(IsStack (TransConstraint cm) tt, cm m) =>
Dict (cm (ApplyStack tt m))
transStackDict @Monad @tt @m of
            Dict (Monad (ApplyStack tt m))
Dict -> \a -> b
ab (MkStackT ApplyStack tt m a
ma) -> forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
ab ApplyStack tt m a
ma

instance (IsStack (TransConstraint Monad) tt, Monad m) => Applicative (StackT tt m) where
    pure :: forall a. a -> StackT tt m a
pure =
        case forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
       (m :: Type -> Type).
(IsStack (TransConstraint cm) tt, cm m) =>
Dict (cm (ApplyStack tt m))
transStackDict @Monad @tt @m of
            Dict (Monad (ApplyStack tt m))
Dict -> \a
a -> forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a. Applicative f => a -> f a
pure a
a
    <*> :: forall a b. StackT tt m (a -> b) -> StackT tt m a -> StackT tt m b
(<*>) =
        case forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
       (m :: Type -> Type).
(IsStack (TransConstraint cm) tt, cm m) =>
Dict (cm (ApplyStack tt m))
transStackDict @Monad @tt @m of
            Dict (Monad (ApplyStack tt m))
Dict -> \(MkStackT ApplyStack tt m (a -> b)
mab) (MkStackT ApplyStack tt m a
ma) -> forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall a b. (a -> b) -> a -> b
$ ApplyStack tt m (a -> b)
mab forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> ApplyStack tt m a
ma

instance (IsStack (TransConstraint Monad) tt, Monad m) => Monad (StackT tt m) where
    return :: forall a. a -> StackT tt m a
return = forall (f :: Type -> Type) a. Applicative f => a -> f a
pure
    >>= :: forall a b. StackT tt m a -> (a -> StackT tt m b) -> StackT tt m b
(>>=) =
        case forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
       (m :: Type -> Type).
(IsStack (TransConstraint cm) tt, cm m) =>
Dict (cm (ApplyStack tt m))
transStackDict @Monad @tt @m of
            Dict (Monad (ApplyStack tt m))
Dict -> \(MkStackT ApplyStack tt m a
ma) a -> StackT tt m b
amb -> forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall a b. (a -> b) -> a -> b
$ ApplyStack tt m a
ma forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
a -> forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT forall a b. (a -> b) -> a -> b
$ a -> StackT tt m b
amb a
a

instance (IsStack (TransConstraint Monad) tt) => TransConstraint Monad (StackT tt) where
    hasTransConstraint :: forall (m :: Type -> Type). Monad m => Dict (Monad (StackT tt m))
hasTransConstraint = forall (a :: Constraint). a => Dict a
Dict

instance (IsStack (TransConstraint Monad) tt, IsStack MonadTrans tt, MonadFail m) => MonadFail (StackT tt m) where
    fail :: forall a. String -> StackT tt m a
fail String
s = forall (t :: TransKind) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
s

instance (IsStack (TransConstraint Monad) tt, IsStack (TransConstraint MonadFail) tt, IsStack MonadTrans tt) =>
             TransConstraint MonadFail (StackT tt) where
    hasTransConstraint :: forall (m :: Type -> Type).
MonadFail m =>
Dict (MonadFail (StackT tt m))
hasTransConstraint = forall (a :: Constraint). a => Dict a
Dict

instance (IsStack (TransConstraint Monad) tt, IsStack (TransConstraint MonadFix) tt, MonadFix m) =>
             MonadFix (StackT tt m) where
    mfix :: forall a. (a -> StackT tt m a) -> StackT tt m a
    mfix :: forall a. (a -> StackT tt m a) -> StackT tt m a
mfix =
        case forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
       (m :: Type -> Type).
(IsStack (TransConstraint cm) tt, cm m) =>
Dict (cm (ApplyStack tt m))
transStackDict @MonadFix @tt @m of
            Dict (MonadFix (ApplyStack tt m))
Dict -> \a -> StackT tt m a
f -> forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type) a. MonadFix m => (a -> m a) -> m a
mfix forall a b. (a -> b) -> a -> b
$ \a
a -> forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT forall a b. (a -> b) -> a -> b
$ a -> StackT tt m a
f a
a

instance (IsStack (TransConstraint Monad) tt, IsStack (TransConstraint MonadFix) tt) =>
             TransConstraint MonadFix (StackT tt) where
    hasTransConstraint :: forall (m :: Type -> Type).
MonadFix m =>
Dict (MonadFix (StackT tt m))
hasTransConstraint = forall (a :: Constraint). a => Dict a
Dict

instance (IsStack (TransConstraint Monad) tt, IsStack (TransConstraint MonadIO) tt, MonadIO m) => MonadIO (StackT tt m) where
    liftIO :: forall a. IO a -> StackT tt m a
liftIO =
        case forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
       (m :: Type -> Type).
(IsStack (TransConstraint cm) tt, cm m) =>
Dict (cm (ApplyStack tt m))
transStackDict @MonadIO @tt @m of
            Dict (MonadIO (ApplyStack tt m))
Dict -> \IO a
ioa -> forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO IO a
ioa

instance (IsStack (TransConstraint Monad) tt, IsStack (TransConstraint MonadIO) tt) =>
             TransConstraint MonadIO (StackT tt) where
    hasTransConstraint :: forall (m :: Type -> Type).
MonadIO m =>
Dict (MonadIO (StackT tt m))
hasTransConstraint = forall (a :: Constraint). a => Dict a
Dict

instance (IsStack (TransConstraint Monad) tt, IsStack (TransConstraint MonadPlus) tt, MonadPlus m) =>
             Alternative (StackT tt m) where
    empty :: forall a. StackT tt m a
empty =
        case forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
       (m :: Type -> Type).
(IsStack (TransConstraint cm) tt, cm m) =>
Dict (cm (ApplyStack tt m))
transStackDict @MonadPlus @tt @m of
            Dict (MonadPlus (ApplyStack tt m))
Dict -> forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall (f :: Type -> Type) a. Alternative f => f a
empty
    <|> :: forall a. StackT tt m a -> StackT tt m a -> StackT tt m a
(<|>) =
        case forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
       (m :: Type -> Type).
(IsStack (TransConstraint cm) tt, cm m) =>
Dict (cm (ApplyStack tt m))
transStackDict @MonadPlus @tt @m of
            Dict (MonadPlus (ApplyStack tt m))
Dict -> \(MkStackT ApplyStack tt m a
a) (MkStackT ApplyStack tt m a
b) -> forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall a b. (a -> b) -> a -> b
$ ApplyStack tt m a
a forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> ApplyStack tt m a
b

instance (IsStack (TransConstraint Monad) tt, IsStack (TransConstraint MonadPlus) tt, MonadPlus m) =>
             MonadPlus (StackT tt m)

instance (IsStack (TransConstraint Monad) tt, IsStack (TransConstraint MonadPlus) tt) =>
             TransConstraint MonadPlus (StackT tt) where
    hasTransConstraint :: forall (m :: Type -> Type).
MonadPlus m =>
Dict (MonadPlus (StackT tt m))
hasTransConstraint = forall (a :: Constraint). a => Dict a
Dict

instance (IsStack (TransConstraint Monad) tt, IsStack MonadTrans tt) => MonadTrans (StackT tt) where
    lift ::
           forall m a. Monad m
        => m a
        -> StackT tt m a
    lift :: forall (m :: Type -> Type) a. Monad m => m a -> StackT tt m a
lift = let
        build ::
               forall tt'.
               ListType (Compose Dict (TransConstraint Monad)) tt'
            -> ListType (Compose Dict MonadTrans) tt'
            -> (WRaised m (ApplyStack tt' m), Dict (Monad (ApplyStack tt' m)))
        build :: forall (tt' :: [TransKind]).
ListType (Compose Dict (TransConstraint Monad)) tt'
-> ListType (Compose Dict MonadTrans) tt'
-> (WRaised m (ApplyStack tt' m), Dict (Monad (ApplyStack tt' m)))
build ListType (Compose Dict (TransConstraint Monad)) tt'
NilListType ListType (Compose Dict MonadTrans) tt'
NilListType = (forall {k} (cat :: k -> k -> Type) (a :: k).
Category cat =>
cat a a
id, forall (a :: Constraint). a => Dict a
Dict)
        build (ConsListType (Compose Dict (TransConstraint Monad a)
Dict) ListType (Compose Dict (TransConstraint Monad)) lt1
wa) (ConsListType (Compose Dict (MonadTrans a)
Dict) ListType (Compose Dict MonadTrans) lt1
wb) =
            case forall (tt' :: [TransKind]).
ListType (Compose Dict (TransConstraint Monad)) tt'
-> ListType (Compose Dict MonadTrans) tt'
-> (WRaised m (ApplyStack tt' m), Dict (Monad (ApplyStack tt' m)))
build ListType (Compose Dict (TransConstraint Monad)) lt1
wa ListType (Compose Dict MonadTrans) lt1
wb of
                (WRaised m (ApplyStack lt1 m)
wmf, dcm :: Dict (Monad (ApplyStack lt1 m))
dcm@Dict (Monad (ApplyStack lt1 m))
Dict) -> (forall (t :: TransKind) (m :: Type -> Type).
(MonadTrans t, Monad m) =>
WRaised m (t m)
wLift forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. WRaised m (ApplyStack lt1 m)
wmf, forall (c :: (Type -> Type) -> Constraint) (t :: TransKind)
       (m :: Type -> Type).
TransConstraint c t =>
Dict (c m) -> Dict (c (t m))
transConstraintDict @Monad Dict (Monad (ApplyStack lt1 m))
dcm)
        in let
               wa :: ListType (Compose Dict (TransConstraint Monad)) tt
wa = forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative @_ @(ListType (Compose Dict (TransConstraint Monad))) @tt
               wb :: ListType (Compose Dict MonadTrans) tt
wb = forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative @_ @(ListType (Compose Dict MonadTrans)) @tt
               in case forall (tt' :: [TransKind]).
ListType (Compose Dict (TransConstraint Monad)) tt'
-> ListType (Compose Dict MonadTrans) tt'
-> (WRaised m (ApplyStack tt' m), Dict (Monad (ApplyStack tt' m)))
build ListType (Compose Dict (TransConstraint Monad)) tt
wa ListType (Compose Dict MonadTrans) tt
wb of
                      (WRaised m (ApplyStack tt m)
wmf, Dict (Monad (ApplyStack tt m))
_) -> \m a
ma -> forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall a b. (a -> b) -> a -> b
$ forall k (p :: k -> Type) (q :: k -> Type). WRaised p q -> p --> q
unWRaised WRaised m (ApplyStack tt m)
wmf m a
ma

stackLift ::
       forall tt m. (IsStack (TransConstraint Monad) tt, IsStack MonadTrans tt, Monad m)
    => m --> ApplyStack tt m
stackLift :: forall (tt :: [TransKind]) (m :: Type -> Type).
(IsStack (TransConstraint Monad) tt, IsStack MonadTrans tt,
 Monad m) =>
m --> ApplyStack tt m
stackLift m a
ma = forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT @tt @m forall a b. (a -> b) -> a -> b
$ forall (t :: TransKind) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m a
ma

type MonadTransStackTunnel tt
     = ( IsStack (TransConstraint Monad) tt
       , IsStack MonadTransTunnel tt
       , IsStack MonadTrans tt
       , IsStack (WithTunnelConstraint Functor) tt
       , IsStack (WithTunnelConstraint Applicative) tt
       , IsStack (WithTunnelConstraint Monad) tt
       , IsStack (WithTunnelConstraint Traversable) tt
       , IsStack (WithTunnelConstraint MonadInner) tt)

concatMonadTransStackTunnelDict ::
       forall tt1 tt2. (MonadTransStackTunnel tt1, MonadTransStackTunnel tt2)
    => Dict (MonadTransStackTunnel (Concat tt1 tt2))
concatMonadTransStackTunnelDict :: forall (tt1 :: [TransKind]) (tt2 :: [TransKind]).
(MonadTransStackTunnel tt1, MonadTransStackTunnel tt2) =>
Dict (MonadTransStackTunnel (Concat tt1 tt2))
concatMonadTransStackTunnelDict =
    forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]) r.
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
(Is (ListType w) (Concat aa bb) => r) -> r
withConcatIs @_ @(Compose Dict (TransConstraint Monad)) @tt1 @tt2 forall a b. (a -> b) -> a -> b
$
    forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]) r.
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
(Is (ListType w) (Concat aa bb) => r) -> r
withConcatIs @_ @(Compose Dict MonadTransTunnel) @tt1 @tt2 forall a b. (a -> b) -> a -> b
$
    forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]) r.
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
(Is (ListType w) (Concat aa bb) => r) -> r
withConcatIs @_ @(Compose Dict MonadTrans) @tt1 @tt2 forall a b. (a -> b) -> a -> b
$
    forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]) r.
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
(Is (ListType w) (Concat aa bb) => r) -> r
withConcatIs @_ @(Compose Dict (WithTunnelConstraint Functor)) @tt1 @tt2 forall a b. (a -> b) -> a -> b
$
    forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]) r.
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
(Is (ListType w) (Concat aa bb) => r) -> r
withConcatIs @_ @(Compose Dict (WithTunnelConstraint Applicative)) @tt1 @tt2 forall a b. (a -> b) -> a -> b
$
    forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]) r.
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
(Is (ListType w) (Concat aa bb) => r) -> r
withConcatIs @_ @(Compose Dict (WithTunnelConstraint Monad)) @tt1 @tt2 forall a b. (a -> b) -> a -> b
$
    forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]) r.
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
(Is (ListType w) (Concat aa bb) => r) -> r
withConcatIs @_ @(Compose Dict (WithTunnelConstraint Traversable)) @tt1 @tt2 forall a b. (a -> b) -> a -> b
$
    forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]) r.
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
(Is (ListType w) (Concat aa bb) => r) -> r
withConcatIs @_ @(Compose Dict (WithTunnelConstraint MonadInner)) @tt1 @tt2 forall a b. (a -> b) -> a -> b
$ forall (a :: Constraint). a => Dict a
Dict

newtype TunnelWrapper t = MkTunnel
    { forall (t :: TransKind).
TunnelWrapper t
-> forall (m2 :: Type -> Type) r.
   Monad m2 =>
   ((forall (m1 :: Type -> Type) a.
     Monad m1 =>
     t m1 a -> m1 (Tunnel t a))
    -> m2 (Tunnel t r))
   -> t m2 r
unTunnel :: forall m2 r.
                      Monad m2 => ((forall m1 a. Monad m1 => t m1 a -> m1 (Tunnel t a)) -> m2 (Tunnel t r)) -> t m2 r
    }

type WithTunnelConstraint :: ((Type -> Type) -> Constraint) -> TransKind -> Constraint
class (MonadTransTunnel t, c (Tunnel t)) => WithTunnelConstraint c t

instance (MonadTransTunnel t, c (Tunnel t)) => WithTunnelConstraint c t

type ApplyStackTunnel :: [TransKind] -> Type -> Type
type family ApplyStackTunnel tt where
    ApplyStackTunnel '[] = Identity
    ApplyStackTunnel (t ': tt) = ComposeInner (Tunnel t) (ApplyStackTunnel tt)

astIsWithTunnelConstraint ::
       forall (c :: (Type -> Type) -> Constraint) (tt :: [TransKind]).
       (c Identity, forall f1 f2. (c f1, c f2) => c (ComposeInner f1 f2))
    => ListType (Compose Dict (WithTunnelConstraint c)) tt
    -> Dict (c (ApplyStackTunnel tt))
astIsWithTunnelConstraint :: forall (c :: (Type -> Type) -> Constraint) (tt :: [TransKind]).
(c Identity,
 forall (f1 :: Type -> Type) (f2 :: Type -> Type).
 (c f1, c f2) =>
 c (ComposeInner f1 f2)) =>
ListType (Compose Dict (WithTunnelConstraint c)) tt
-> Dict (c (ApplyStackTunnel tt))
astIsWithTunnelConstraint ListType (Compose Dict (WithTunnelConstraint c)) tt
NilListType = forall (a :: Constraint). a => Dict a
Dict
astIsWithTunnelConstraint (ConsListType (Compose Dict (WithTunnelConstraint c a)
Dict) ListType (Compose Dict (WithTunnelConstraint c)) lt1
w) =
    case forall (c :: (Type -> Type) -> Constraint) (tt :: [TransKind]).
(c Identity,
 forall (f1 :: Type -> Type) (f2 :: Type -> Type).
 (c f1, c f2) =>
 c (ComposeInner f1 f2)) =>
ListType (Compose Dict (WithTunnelConstraint c)) tt
-> Dict (c (ApplyStackTunnel tt))
astIsWithTunnelConstraint ListType (Compose Dict (WithTunnelConstraint c)) lt1
w of
        Dict (c (ApplyStackTunnel lt1))
Dict -> forall (a :: Constraint). a => Dict a
Dict

isWithTunnelConstraint ::
       forall (c :: (Type -> Type) -> Constraint) (tt :: [TransKind]).
       (c Identity, forall f1 f2. (c f1, c f2) => c (ComposeInner f1 f2))
    => IsStack (WithTunnelConstraint c) tt => Dict (c (ApplyStackTunnel tt))
isWithTunnelConstraint :: forall (c :: (Type -> Type) -> Constraint) (tt :: [TransKind]).
(c Identity,
 forall (f1 :: Type -> Type) (f2 :: Type -> Type).
 (c f1, c f2) =>
 c (ComposeInner f1 f2),
 IsStack (WithTunnelConstraint c) tt) =>
Dict (c (ApplyStackTunnel tt))
isWithTunnelConstraint =
    forall (c :: (Type -> Type) -> Constraint) (tt :: [TransKind]).
(c Identity,
 forall (f1 :: Type -> Type) (f2 :: Type -> Type).
 (c f1, c f2) =>
 c (ComposeInner f1 f2)) =>
ListType (Compose Dict (WithTunnelConstraint c)) tt
-> Dict (c (ApplyStackTunnel tt))
astIsWithTunnelConstraint @c forall a b. (a -> b) -> a -> b
$ forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative @_ @(ListType (Compose Dict (WithTunnelConstraint c))) @tt

type StackTunnel :: [TransKind] -> Type -> Type
newtype StackTunnel tt a = MkStackTunnel
    { forall (tt :: [TransKind]) a.
StackTunnel tt a -> ApplyStackTunnel tt a
unStackTunnel :: ApplyStackTunnel tt a
    }

instance IsStack (WithTunnelConstraint Functor) tt => Functor (StackTunnel tt) where
    fmap :: forall a b. (a -> b) -> StackTunnel tt a -> StackTunnel tt b
fmap =
        case forall (c :: (Type -> Type) -> Constraint) (tt :: [TransKind]).
(c Identity,
 forall (f1 :: Type -> Type) (f2 :: Type -> Type).
 (c f1, c f2) =>
 c (ComposeInner f1 f2),
 IsStack (WithTunnelConstraint c) tt) =>
Dict (c (ApplyStackTunnel tt))
isWithTunnelConstraint @Functor @tt of
            Dict (Functor (ApplyStackTunnel tt))
Dict -> \a -> b
ab (MkStackTunnel ApplyStackTunnel tt a
st) -> forall (tt :: [TransKind]) a.
ApplyStackTunnel tt a -> StackTunnel tt a
MkStackTunnel forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
ab ApplyStackTunnel tt a
st

instance (IsStack (WithTunnelConstraint Functor) tt, IsStack (WithTunnelConstraint MonadInner) tt) =>
             Applicative (StackTunnel tt) where
    pure :: forall a. a -> StackTunnel tt a
pure =
        case forall (c :: (Type -> Type) -> Constraint) (tt :: [TransKind]).
(c Identity,
 forall (f1 :: Type -> Type) (f2 :: Type -> Type).
 (c f1, c f2) =>
 c (ComposeInner f1 f2),
 IsStack (WithTunnelConstraint c) tt) =>
Dict (c (ApplyStackTunnel tt))
isWithTunnelConstraint @MonadInner @tt of
            Dict (MonadInner (ApplyStackTunnel tt))
Dict -> \a
a -> forall (tt :: [TransKind]) a.
ApplyStackTunnel tt a -> StackTunnel tt a
MkStackTunnel forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a. Applicative f => a -> f a
pure a
a
    <*> :: forall a b.
StackTunnel tt (a -> b) -> StackTunnel tt a -> StackTunnel tt b
(<*>) =
        case forall (c :: (Type -> Type) -> Constraint) (tt :: [TransKind]).
(c Identity,
 forall (f1 :: Type -> Type) (f2 :: Type -> Type).
 (c f1, c f2) =>
 c (ComposeInner f1 f2),
 IsStack (WithTunnelConstraint c) tt) =>
Dict (c (ApplyStackTunnel tt))
isWithTunnelConstraint @MonadInner @tt of
            Dict (MonadInner (ApplyStackTunnel tt))
Dict -> \(MkStackTunnel ApplyStackTunnel tt (a -> b)
mab) (MkStackTunnel ApplyStackTunnel tt a
ma) -> forall (tt :: [TransKind]) a.
ApplyStackTunnel tt a -> StackTunnel tt a
MkStackTunnel forall a b. (a -> b) -> a -> b
$ ApplyStackTunnel tt (a -> b)
mab forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> ApplyStackTunnel tt a
ma

instance (IsStack (WithTunnelConstraint Functor) tt, IsStack (WithTunnelConstraint MonadInner) tt) =>
             Foldable (StackTunnel tt) where
    foldMap :: forall m a. Monoid m => (a -> m) -> StackTunnel tt a -> m
foldMap =
        case forall (c :: (Type -> Type) -> Constraint) (tt :: [TransKind]).
(c Identity,
 forall (f1 :: Type -> Type) (f2 :: Type -> Type).
 (c f1, c f2) =>
 c (ComposeInner f1 f2),
 IsStack (WithTunnelConstraint c) tt) =>
Dict (c (ApplyStackTunnel tt))
isWithTunnelConstraint @MonadInner @tt of
            Dict (MonadInner (ApplyStackTunnel tt))
Dict -> \a -> m
ab (MkStackTunnel ApplyStackTunnel tt a
st) -> forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
ab ApplyStackTunnel tt a
st

instance (IsStack (WithTunnelConstraint Functor) tt, IsStack (WithTunnelConstraint MonadInner) tt) =>
             Traversable (StackTunnel tt) where
    traverse :: forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> StackTunnel tt a -> f (StackTunnel tt b)
traverse =
        case forall (c :: (Type -> Type) -> Constraint) (tt :: [TransKind]).
(c Identity,
 forall (f1 :: Type -> Type) (f2 :: Type -> Type).
 (c f1, c f2) =>
 c (ComposeInner f1 f2),
 IsStack (WithTunnelConstraint c) tt) =>
Dict (c (ApplyStackTunnel tt))
isWithTunnelConstraint @MonadInner @tt of
            Dict (MonadInner (ApplyStackTunnel tt))
Dict -> \a -> f b
ab (MkStackTunnel ApplyStackTunnel tt a
st) -> forall (tt :: [TransKind]) a.
ApplyStackTunnel tt a -> StackTunnel tt a
MkStackTunnel forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
ab ApplyStackTunnel tt a
st

instance (IsStack (WithTunnelConstraint Functor) tt, IsStack (WithTunnelConstraint MonadInner) tt) =>
             Monad (StackTunnel tt) where
    return :: forall a. a -> StackTunnel tt a
return = forall (f :: Type -> Type) a. Applicative f => a -> f a
pure
    >>= :: forall a b.
StackTunnel tt a -> (a -> StackTunnel tt b) -> StackTunnel tt b
(>>=) =
        case forall (c :: (Type -> Type) -> Constraint) (tt :: [TransKind]).
(c Identity,
 forall (f1 :: Type -> Type) (f2 :: Type -> Type).
 (c f1, c f2) =>
 c (ComposeInner f1 f2),
 IsStack (WithTunnelConstraint c) tt) =>
Dict (c (ApplyStackTunnel tt))
isWithTunnelConstraint @MonadInner @tt of
            Dict (MonadInner (ApplyStackTunnel tt))
Dict -> \(MkStackTunnel ApplyStackTunnel tt a
ma) a -> StackTunnel tt b
q -> forall (tt :: [TransKind]) a.
ApplyStackTunnel tt a -> StackTunnel tt a
MkStackTunnel forall a b. (a -> b) -> a -> b
$ ApplyStackTunnel tt a
ma forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (tt :: [TransKind]) a.
StackTunnel tt a -> ApplyStackTunnel tt a
unStackTunnel forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> StackTunnel tt b
q

instance (IsStack (WithTunnelConstraint Functor) tt, IsStack (WithTunnelConstraint MonadInner) tt) =>
             MonadException (StackTunnel tt) where
    type Exc (StackTunnel tt) = Exc (ApplyStackTunnel tt)
    throwExc :: forall a. Exc (StackTunnel tt) -> StackTunnel tt a
throwExc Exc (StackTunnel tt)
e =
        case forall (c :: (Type -> Type) -> Constraint) (tt :: [TransKind]).
(c Identity,
 forall (f1 :: Type -> Type) (f2 :: Type -> Type).
 (c f1, c f2) =>
 c (ComposeInner f1 f2),
 IsStack (WithTunnelConstraint c) tt) =>
Dict (c (ApplyStackTunnel tt))
isWithTunnelConstraint @MonadInner @tt of
            Dict (MonadInner (ApplyStackTunnel tt))
Dict -> forall (tt :: [TransKind]) a.
ApplyStackTunnel tt a -> StackTunnel tt a
MkStackTunnel forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type) a. MonadException m => Exc m -> m a
throwExc Exc (StackTunnel tt)
e
    catchExc :: forall a.
StackTunnel tt a
-> (Exc (StackTunnel tt) -> StackTunnel tt a) -> StackTunnel tt a
catchExc (MkStackTunnel ApplyStackTunnel tt a
st) Exc (StackTunnel tt) -> StackTunnel tt a
q =
        case forall (c :: (Type -> Type) -> Constraint) (tt :: [TransKind]).
(c Identity,
 forall (f1 :: Type -> Type) (f2 :: Type -> Type).
 (c f1, c f2) =>
 c (ComposeInner f1 f2),
 IsStack (WithTunnelConstraint c) tt) =>
Dict (c (ApplyStackTunnel tt))
isWithTunnelConstraint @MonadInner @tt of
            Dict (MonadInner (ApplyStackTunnel tt))
Dict -> forall (tt :: [TransKind]) a.
ApplyStackTunnel tt a -> StackTunnel tt a
MkStackTunnel forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type) a.
MonadException m =>
m a -> (Exc m -> m a) -> m a
catchExc ApplyStackTunnel tt a
st (forall (tt :: [TransKind]) a.
StackTunnel tt a -> ApplyStackTunnel tt a
unStackTunnel forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Exc (StackTunnel tt) -> StackTunnel tt a
q)

instance (IsStack (WithTunnelConstraint Functor) tt, IsStack (WithTunnelConstraint MonadInner) tt) =>
             MonadInner (StackTunnel tt) where
    retrieveInner :: forall a. StackTunnel tt a -> Result (Exc (StackTunnel tt)) a
retrieveInner =
        case forall (c :: (Type -> Type) -> Constraint) (tt :: [TransKind]).
(c Identity,
 forall (f1 :: Type -> Type) (f2 :: Type -> Type).
 (c f1, c f2) =>
 c (ComposeInner f1 f2),
 IsStack (WithTunnelConstraint c) tt) =>
Dict (c (ApplyStackTunnel tt))
isWithTunnelConstraint @MonadInner @tt of
            Dict (MonadInner (ApplyStackTunnel tt))
Dict -> \(MkStackTunnel ApplyStackTunnel tt a
st) -> forall (m :: Type -> Type) a.
MonadInner m =>
m a -> Result (Exc m) a
retrieveInner ApplyStackTunnel tt a
st

instance ( IsStack (WithTunnelConstraint Functor) tt
         , IsStack (WithTunnelConstraint MonadInner) tt
         , IsStack (WithTunnelConstraint MonadExtract) tt
         , IsStack MonadTransUnlift tt
         ) => MonadExtract (StackTunnel tt) where
    mToValue :: Extract (StackTunnel tt)
mToValue =
        case forall (c :: (Type -> Type) -> Constraint) (tt :: [TransKind]).
(c Identity,
 forall (f1 :: Type -> Type) (f2 :: Type -> Type).
 (c f1, c f2) =>
 c (ComposeInner f1 f2),
 IsStack (WithTunnelConstraint c) tt) =>
Dict (c (ApplyStackTunnel tt))
isWithTunnelConstraint @MonadExtract @tt of
            Dict (MonadExtract (ApplyStackTunnel tt))
Dict -> \(MkStackTunnel ApplyStackTunnel tt a
st) -> forall (m :: Type -> Type). MonadExtract m => Extract m
mToValue ApplyStackTunnel tt a
st

instance MonadTransStackTunnel tt => MonadTransHoist (StackT tt) where
    hoist :: forall (m1 :: Type -> Type) (m2 :: Type -> Type).
(Monad m1, Monad m2) =>
(m1 --> m2) -> StackT tt m1 --> StackT tt m2
hoist = forall (t :: TransKind) (m1 :: Type -> Type) (m2 :: Type -> Type).
(MonadTransTunnel t, Monad m1, Monad m2) =>
(m1 --> m2) -> t m1 --> t m2
tunnelHoist

instance MonadTransStackTunnel tt => MonadTransTunnel (StackT tt) where
    type Tunnel (StackT tt) = StackTunnel tt
    tunnel ::
           forall m2 r. Monad m2
        => ((forall m1 a. Monad m1 => StackT tt m1 a -> m1 (Tunnel (StackT tt) a)) -> m2 (Tunnel (StackT tt) r))
        -> StackT tt m2 r
    tunnel :: forall (m :: Type -> Type) r.
Monad m =>
((forall (m1 :: Type -> Type) a.
  Monad m1 =>
  StackT tt m1 a -> m1 (Tunnel (StackT tt) a))
 -> m (Tunnel (StackT tt) r))
-> StackT tt m r
tunnel = let
        build :: forall tt'. ListType (Compose Dict MonadTransTunnel) tt' -> TunnelWrapper (StackT tt')
        build :: forall (tt' :: [TransKind]).
ListType (Compose Dict MonadTransTunnel) tt'
-> TunnelWrapper (StackT tt')
build ListType (Compose Dict MonadTransTunnel) tt'
NilListType =
            forall (t :: TransKind).
(forall (m2 :: Type -> Type) r.
 Monad m2 =>
 ((forall (m1 :: Type -> Type) a.
   Monad m1 =>
   t m1 a -> m1 (Tunnel t a))
  -> m2 (Tunnel t r))
 -> t m2 r)
-> TunnelWrapper t
MkTunnel forall a b. (a -> b) -> a -> b
$ \(forall (m1 :: Type -> Type) a.
 Monad m1 =>
 StackT tt' m1 a -> m1 (Tunnel (StackT tt') a))
-> m2 (Tunnel (StackT tt') r)
call ->
                forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Identity a -> a
runIdentity forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (tt :: [TransKind]) a.
StackTunnel tt a -> ApplyStackTunnel tt a
unStackTunnel) forall a b. (a -> b) -> a -> b
$ (forall (m1 :: Type -> Type) a.
 Monad m1 =>
 StackT tt' m1 a -> m1 (Tunnel (StackT tt') a))
-> m2 (Tunnel (StackT tt') r)
call forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (tt :: [TransKind]) a.
ApplyStackTunnel tt a -> StackTunnel tt a
MkStackTunnel forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a. a -> Identity a
Identity) forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT
        build (ConsListType (Compose Dict (MonadTransTunnel a)
Dict) (ListType (Compose Dict MonadTransTunnel) lt1
w :: ListType _ tt0)) =
            case forall (tt' :: [TransKind]).
ListType (Compose Dict MonadTransTunnel) tt'
-> TunnelWrapper (StackT tt')
build ListType (Compose Dict MonadTransTunnel) lt1
w of
                MkTunnel forall (m2 :: Type -> Type) r.
Monad m2 =>
((forall (m1 :: Type -> Type) a.
  Monad m1 =>
  StackT lt1 m1 a -> m1 (Tunnel (StackT lt1) a))
 -> m2 (Tunnel (StackT lt1) r))
-> StackT lt1 m2 r
tunnel' -> let
                    tunnel'' ::
                           forall m2' r'. Monad m2'
                        => ((forall m1 a. Monad m1 => StackT tt' m1 a -> m1 (Tunnel (StackT tt') a)) -> m2' (Tunnel (StackT tt') r'))
                        -> StackT tt' m2' r'
                    tunnel'' :: forall (m2' :: Type -> Type) r'.
Monad m2' =>
((forall (m1 :: Type -> Type) a.
  Monad m1 =>
  StackT tt' m1 a -> m1 (Tunnel (StackT tt') a))
 -> m2' (Tunnel (StackT tt') r'))
-> StackT tt' m2' r'
tunnel'' (forall (m1 :: Type -> Type) a.
 Monad m1 =>
 StackT tt' m1 a -> m1 (Tunnel (StackT tt') a))
-> m2' (Tunnel (StackT tt') r')
call =
                        case (forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
       (m :: Type -> Type).
cm m =>
ListType (Compose Dict (TransConstraint cm)) tt
-> Dict (cm (ApplyStack tt m))
witTransStackDict @Monad @tt0 @m2' forall a b. (a -> b) -> a -> b
$ forall {k} (wita :: k -> Type) (witb :: k -> Type) (t :: [k]).
(forall (t' :: k). wita t' -> witb t')
-> ListType wita t -> ListType witb t
mapListType (\(Compose Dict (MonadTransTunnel t')
Dict) -> forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose forall (a :: Constraint). a => Dict a
Dict) ListType (Compose Dict MonadTransTunnel) lt1
w) of
                            Dict (Monad (ApplyStack lt1 m2'))
Dict ->
                                forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall a b. (a -> b) -> a -> b
$
                                forall (t :: TransKind) (m :: Type -> Type) r.
(MonadTransTunnel t, Monad m) =>
((forall (m1 :: Type -> Type) a.
  Monad m1 =>
  t m1 a -> m1 (Tunnel t a))
 -> m (Tunnel t r))
-> t m r
tunnel forall a b. (a -> b) -> a -> b
$ \forall (m1 :: Type -> Type) a.
Monad m1 =>
a m1 a -> m1 (Tunnel a a)
unlift1 ->
                                    forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT forall a b. (a -> b) -> a -> b
$
                                    forall (m2 :: Type -> Type) r.
Monad m2 =>
((forall (m1 :: Type -> Type) a.
  Monad m1 =>
  StackT lt1 m1 a -> m1 (Tunnel (StackT lt1) a))
 -> m2 (Tunnel (StackT lt1) r))
-> StackT lt1 m2 r
tunnel' forall a b. (a -> b) -> a -> b
$ \forall (m1 :: Type -> Type) a.
Monad m1 =>
StackT lt1 m1 a -> m1 (Tunnel (StackT lt1) a)
unlift2 ->
                                        forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (tt :: [TransKind]) a.
ApplyStackTunnel tt a -> StackTunnel tt a
MkStackTunnel forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (inner :: Type -> Type) (outer :: Type -> Type) a.
ComposeInner inner outer a -> outer (inner a)
unComposeInner forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (tt :: [TransKind]) a.
StackTunnel tt a -> ApplyStackTunnel tt a
unStackTunnel) forall a b. (a -> b) -> a -> b
$
                                        (forall (m1 :: Type -> Type) a.
 Monad m1 =>
 StackT tt' m1 a -> m1 (Tunnel (StackT tt') a))
-> m2' (Tunnel (StackT tt') r')
call forall a b. (a -> b) -> a -> b
$ \(MkStackT ApplyStack tt' m1 a
stt :: _ m1 _) ->
                                            case (forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
       (m :: Type -> Type).
cm m =>
ListType (Compose Dict (TransConstraint cm)) tt
-> Dict (cm (ApplyStack tt m))
witTransStackDict @Monad @tt0 @m1 forall a b. (a -> b) -> a -> b
$
                                                  forall {k} (wita :: k -> Type) (witb :: k -> Type) (t :: [k]).
(forall (t' :: k). wita t' -> witb t')
-> ListType wita t -> ListType witb t
mapListType (\(Compose Dict (MonadTransTunnel t')
Dict) -> forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose forall (a :: Constraint). a => Dict a
Dict) ListType (Compose Dict MonadTransTunnel) lt1
w) of
                                                Dict (Monad (ApplyStack lt1 m1))
Dict ->
                                                    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (tt :: [TransKind]) a.
ApplyStackTunnel tt a -> StackTunnel tt a
MkStackTunnel forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (inner :: Type -> Type) (outer :: Type -> Type) a.
outer (inner a) -> ComposeInner inner outer a
MkComposeInner forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (tt :: [TransKind]) a.
StackTunnel tt a -> ApplyStackTunnel tt a
unStackTunnel) forall a b. (a -> b) -> a -> b
$
                                                    forall (m1 :: Type -> Type) a.
Monad m1 =>
StackT lt1 m1 a -> m1 (Tunnel (StackT lt1) a)
unlift2 forall a b. (a -> b) -> a -> b
$ forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall a b. (a -> b) -> a -> b
$ forall (m1 :: Type -> Type) a.
Monad m1 =>
a m1 a -> m1 (Tunnel a a)
unlift1 ApplyStack tt' m1 a
stt
                    in forall (t :: TransKind).
(forall (m2 :: Type -> Type) r.
 Monad m2 =>
 ((forall (m1 :: Type -> Type) a.
   Monad m1 =>
   t m1 a -> m1 (Tunnel t a))
  -> m2 (Tunnel t r))
 -> t m2 r)
-> TunnelWrapper t
MkTunnel forall (m2' :: Type -> Type) r'.
Monad m2' =>
((forall (m1 :: Type -> Type) a.
  Monad m1 =>
  StackT tt' m1 a -> m1 (Tunnel (StackT tt') a))
 -> m2' (Tunnel (StackT tt') r'))
-> StackT tt' m2' r'
tunnel''
        in forall (t :: TransKind).
TunnelWrapper t
-> forall (m2 :: Type -> Type) r.
   Monad m2 =>
   ((forall (m1 :: Type -> Type) a.
     Monad m1 =>
     t m1 a -> m1 (Tunnel t a))
    -> m2 (Tunnel t r))
   -> t m2 r
unTunnel forall a b. (a -> b) -> a -> b
$ forall (tt' :: [TransKind]).
ListType (Compose Dict MonadTransTunnel) tt'
-> TunnelWrapper (StackT tt')
build forall a b. (a -> b) -> a -> b
$ forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative @_ @(ListType (Compose Dict MonadTransTunnel)) @tt

stackHoist ::
       forall tt ma mb. (MonadTransStackTunnel tt, Monad ma, Monad mb)
    => (ma --> mb)
    -> ApplyStack tt ma --> ApplyStack tt mb
stackHoist :: forall (tt :: [TransKind]) (ma :: Type -> Type)
       (mb :: Type -> Type).
(MonadTransStackTunnel tt, Monad ma, Monad mb) =>
(ma --> mb) -> ApplyStack tt ma --> ApplyStack tt mb
stackHoist ma --> mb
mf ApplyStack tt ma a
asta = forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT forall a b. (a -> b) -> a -> b
$ forall (t :: TransKind) (m1 :: Type -> Type) (m2 :: Type -> Type).
(MonadTransHoist t, Monad m1, Monad m2) =>
(m1 --> m2) -> t m1 --> t m2
hoist ma --> mb
mf forall a b. (a -> b) -> a -> b
$ forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT @tt ApplyStack tt ma a
asta

transStackExcept ::
       forall tt m e a. (MonadTransStackTunnel tt, Monad m)
    => ApplyStack tt (ExceptT e m) a
    -> ApplyStack tt m (Either e a)
transStackExcept :: forall (tt :: [TransKind]) (m :: Type -> Type) e a.
(MonadTransStackTunnel tt, Monad m) =>
ApplyStack tt (ExceptT e m) a -> ApplyStack tt m (Either e a)
transStackExcept ApplyStack tt (ExceptT e m) a
ata = forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT forall a b. (a -> b) -> a -> b
$ forall (t :: TransKind) (m :: Type -> Type) e a.
(MonadTransTunnel t, Applicative (Tunnel t), Monad m) =>
t (ExceptT e m) a -> t m (Either e a)
transExcept forall a b. (a -> b) -> a -> b
$ forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT @tt @(ExceptT e m) ApplyStack tt (ExceptT e m) a
ata

stackUnderliftIO ::
       forall tt m. (MonadTransStackTunnel tt, MonadIO m)
    => ApplyStack tt IO --> ApplyStack tt m
stackUnderliftIO :: forall (tt :: [TransKind]) (m :: Type -> Type).
(MonadTransStackTunnel tt, MonadIO m) =>
ApplyStack tt IO --> ApplyStack tt m
stackUnderliftIO = forall (tt :: [TransKind]) (ma :: Type -> Type)
       (mb :: Type -> Type).
(MonadTransStackTunnel tt, Monad ma, Monad mb) =>
(ma --> mb) -> ApplyStack tt ma --> ApplyStack tt mb
stackHoist @tt @IO @m forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO

stackWBackHoist ::
       forall tt ma mb. (MonadTransStackUnlift tt, Monad ma, Monad mb)
    => WBackraised ma mb
    -> WBackraised (ApplyStack tt ma) (ApplyStack tt mb)
stackWBackHoist :: forall (tt :: [TransKind]) (ma :: Type -> Type)
       (mb :: Type -> Type).
(MonadTransStackUnlift tt, Monad ma, Monad mb) =>
WBackraised ma mb
-> WBackraised (ApplyStack tt ma) (ApplyStack tt mb)
stackWBackHoist WBackraised ma mb
mab = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (t :: TransKind) (ma :: Type -> Type) (mb :: Type -> Type).
(MonadTransTunnel t, Monad ma, Monad mb) =>
WBackraised ma mb -> WBackraised (t ma) (t mb)
wBackHoist @(StackT tt) WBackraised ma mb
mab

stackBackHoist ::
       forall tt ma mb. (MonadTransStackUnlift tt, Monad ma, Monad mb)
    => (ma -/-> mb)
    -> ApplyStack tt ma -/-> ApplyStack tt mb
stackBackHoist :: forall (tt :: [TransKind]) (ma :: Type -> Type)
       (mb :: Type -> Type).
(MonadTransStackUnlift tt, Monad ma, Monad mb) =>
(ma -/-> mb) -> ApplyStack tt ma -/-> ApplyStack tt mb
stackBackHoist ma -/-> mb
f = forall k (p :: k -> Type) (q :: k -> Type).
WBackraised p q -> p -/-> q
unWBackraised forall a b. (a -> b) -> a -> b
$ forall (tt :: [TransKind]) (ma :: Type -> Type)
       (mb :: Type -> Type).
(MonadTransStackUnlift tt, Monad ma, Monad mb) =>
WBackraised ma mb
-> WBackraised (ApplyStack tt ma) (ApplyStack tt mb)
stackWBackHoist @tt forall a b. (a -> b) -> a -> b
$ forall k (p :: k -> Type) (q :: k -> Type).
(p -/-> q) -> WBackraised p q
MkWBackraised ma -/-> mb
f

type MonadTransStackUnlift tt
     = ( IsStack (TransConstraint MonadFail) tt
       , IsStack (TransConstraint MonadIO) tt
       , IsStack (TransConstraint MonadFix) tt
       , IsStack (TransConstraint MonadTunnelIO) tt
       , IsStack (TransConstraint MonadTunnelIOInner) tt
       , IsStack (TransConstraint MonadUnliftIO) tt
       , MonadTransStackTunnel tt
       , IsStack (WithTunnelConstraint MonadExtract) tt
       , IsStack MonadTransUnlift tt)

concatMonadTransStackUnliftDict ::
       forall tt1 tt2. (MonadTransStackUnlift tt1, MonadTransStackUnlift tt2)
    => Dict (MonadTransStackUnlift (Concat tt1 tt2))
concatMonadTransStackUnliftDict :: forall (tt1 :: [TransKind]) (tt2 :: [TransKind]).
(MonadTransStackUnlift tt1, MonadTransStackUnlift tt2) =>
Dict (MonadTransStackUnlift (Concat tt1 tt2))
concatMonadTransStackUnliftDict =
    case forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]).
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
Dict (Is (ListType w) (Concat aa bb))
concatIsDict @_ @(Compose Dict (TransConstraint MonadFail)) @tt1 @tt2 of
        Dict
  (Is
     (ListType (Compose Dict (TransConstraint MonadFail)))
     (Concat tt1 tt2))
Dict ->
            case forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]).
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
Dict (Is (ListType w) (Concat aa bb))
concatIsDict @_ @(Compose Dict (TransConstraint MonadIO)) @tt1 @tt2 of
                Dict
  (Is
     (ListType (Compose Dict (TransConstraint MonadIO)))
     (Concat tt1 tt2))
Dict ->
                    case forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]).
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
Dict (Is (ListType w) (Concat aa bb))
concatIsDict @_ @(Compose Dict (TransConstraint MonadFix)) @tt1 @tt2 of
                        Dict
  (Is
     (ListType (Compose Dict (TransConstraint MonadFix)))
     (Concat tt1 tt2))
Dict ->
                            case forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]).
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
Dict (Is (ListType w) (Concat aa bb))
concatIsDict @_ @(Compose Dict (TransConstraint MonadTunnelIO)) @tt1 @tt2 of
                                Dict
  (Is
     (ListType (Compose Dict (TransConstraint MonadTunnelIO)))
     (Concat tt1 tt2))
Dict ->
                                    case forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]).
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
Dict (Is (ListType w) (Concat aa bb))
concatIsDict @_ @(Compose Dict (TransConstraint MonadTunnelIOInner)) @tt1 @tt2 of
                                        Dict
  (Is
     (ListType (Compose Dict (TransConstraint MonadTunnelIOInner)))
     (Concat tt1 tt2))
Dict ->
                                            case forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]).
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
Dict (Is (ListType w) (Concat aa bb))
concatIsDict
                                                     @_
                                                     @(Compose Dict (TransConstraint MonadUnliftIO))
                                                     @tt1
                                                     @tt2 of
                                                Dict
  (Is
     (ListType (Compose Dict (TransConstraint MonadUnliftIO)))
     (Concat tt1 tt2))
Dict ->
                                                    case forall (tt1 :: [TransKind]) (tt2 :: [TransKind]).
(MonadTransStackTunnel tt1, MonadTransStackTunnel tt2) =>
Dict (MonadTransStackTunnel (Concat tt1 tt2))
concatMonadTransStackTunnelDict @tt1 @tt2 of
                                                        Dict (MonadTransStackTunnel (Concat tt1 tt2))
Dict ->
                                                            case forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]).
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
Dict (Is (ListType w) (Concat aa bb))
concatIsDict
                                                                     @_
                                                                     @(Compose Dict MonadTransTunnel)
                                                                     @tt1
                                                                     @tt2 of
                                                                Dict
  (Is (ListType (Compose Dict MonadTransTunnel)) (Concat tt1 tt2))
Dict ->
                                                                    case forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]).
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
Dict (Is (ListType w) (Concat aa bb))
concatIsDict
                                                                             @_
                                                                             @(Compose Dict MonadTransUnlift)
                                                                             @tt1
                                                                             @tt2 of
                                                                        Dict
  (Is (ListType (Compose Dict MonadTransUnlift)) (Concat tt1 tt2))
Dict ->
                                                                            case forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]).
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
Dict (Is (ListType w) (Concat aa bb))
concatIsDict
                                                                                     @_
                                                                                     @(Compose Dict (WithTunnelConstraint MonadExtract))
                                                                                     @tt1
                                                                                     @tt2 of
                                                                                Dict
  (Is
     (ListType (Compose Dict (WithTunnelConstraint MonadExtract)))
     (Concat tt1 tt2))
Dict -> forall (a :: Constraint). a => Dict a
Dict

stackLiftWithUnlift ::
       forall tt m. (MonadTransStackUnlift tt, MonadTunnelIOInner m)
    => m -/-> ApplyStack tt m
stackLiftWithUnlift :: forall (tt :: [TransKind]) (m :: Type -> Type).
(MonadTransStackUnlift tt, MonadTunnelIOInner m) =>
m -/-> ApplyStack tt m
stackLiftWithUnlift = forall k (p :: k -> Type) (q :: k -> Type).
WBackraised p q -> p -/-> q
unWBackraised forall a b. (a -> b) -> a -> b
$ coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (t :: TransKind) (m :: Type -> Type).
(MonadTransUnlift t, MonadTunnelIOInner m) =>
WBackraised m (t m)
wLiftWithUnlift @(StackT tt) @m

newtype LiftWithUnlift t = MkLiftWithUnlift
    { forall (t :: TransKind).
LiftWithUnlift t
-> forall (m :: Type -> Type) r.
   MonadIO m =>
   (Unlift MonadTunnelIOInner t -> m r) -> t m r
unLiftWithUnlift :: forall m r. MonadIO m => (Unlift MonadTunnelIOInner t -> m r) -> t m r
    }

witFunctorOneTunnelIOStackDict ::
       forall tt m. MonadInner (TunnelIO m)
    => ListType (Compose Dict MonadTransUnlift) tt
    -> Dict (MonadInner (TunnelIO (ApplyStack tt m)))
witFunctorOneTunnelIOStackDict :: forall (tt :: [TransKind]) (m :: Type -> Type).
MonadInner (TunnelIO m) =>
ListType (Compose Dict MonadTransUnlift) tt
-> Dict (MonadInner (TunnelIO (ApplyStack tt m)))
witFunctorOneTunnelIOStackDict ListType (Compose Dict MonadTransUnlift) tt
NilListType = forall (a :: Constraint). a => Dict a
Dict
witFunctorOneTunnelIOStackDict (ConsListType (Compose Dict (MonadTransUnlift a)
Dict) ListType (Compose Dict MonadTransUnlift) lt1
lt) =
    case forall (tt :: [TransKind]) (m :: Type -> Type).
MonadInner (TunnelIO m) =>
ListType (Compose Dict MonadTransUnlift) tt
-> Dict (MonadInner (TunnelIO (ApplyStack tt m)))
witFunctorOneTunnelIOStackDict @_ @m ListType (Compose Dict MonadTransUnlift) lt1
lt of
        Dict (MonadInner (TunnelIO (ApplyStack lt1 m)))
Dict -> forall (a :: Constraint). a => Dict a
Dict

stackJoinUnlift ::
       ListType (Compose Dict MonadTransUnlift) tt
    -> Unlift MonadTunnelIOInner t
    -> Unlift MonadTunnelIOInner (StackT tt)
    -> Unlift MonadTunnelIOInner (StackT (t ': tt))
stackJoinUnlift :: forall (tt :: [TransKind]) (t :: TransKind).
ListType (Compose Dict MonadTransUnlift) tt
-> Unlift MonadTunnelIOInner t
-> Unlift MonadTunnelIOInner (StackT tt)
-> Unlift MonadTunnelIOInner (StackT (t : tt))
stackJoinUnlift ListType (Compose Dict MonadTransUnlift) tt
w Unlift MonadTunnelIOInner t
tmm Unlift MonadTunnelIOInner (StackT tt)
stmm (StackT (t : tt) m a
stma :: StackT (t ': tt) m a) =
    case forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
       (m :: Type -> Type).
cm m =>
ListType (Compose Dict (TransConstraint cm)) tt
-> Dict (cm (ApplyStack tt m))
witTransStackDict @MonadTunnelIOInner @tt @m forall a b. (a -> b) -> a -> b
$ forall {k} (wita :: k -> Type) (witb :: k -> Type) (t :: [k]).
(forall (t' :: k). wita t' -> witb t')
-> ListType wita t -> ListType witb t
mapListType (\(Compose Dict (MonadTransUnlift t')
Dict) -> forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose forall (a :: Constraint). a => Dict a
Dict) ListType (Compose Dict MonadTransUnlift) tt
w of
        Dict (MonadTunnelIOInner (ApplyStack tt m))
Dict ->
            case forall (tt :: [TransKind]) (m :: Type -> Type).
MonadInner (TunnelIO m) =>
ListType (Compose Dict MonadTransUnlift) tt
-> Dict (MonadInner (TunnelIO (ApplyStack tt m)))
witFunctorOneTunnelIOStackDict @tt @m ListType (Compose Dict MonadTransUnlift) tt
w of
                Dict (MonadInner (TunnelIO (ApplyStack tt m)))
Dict -> Unlift MonadTunnelIOInner (StackT tt)
stmm forall a b. (a -> b) -> a -> b
$ forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall a b. (a -> b) -> a -> b
$ Unlift MonadTunnelIOInner t
tmm forall a b. (a -> b) -> a -> b
$ forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT StackT (t : tt) m a
stma

newtype GetDiscardingUnlift t = MkGetDiscardingUnlift
    { forall (t :: TransKind).
GetDiscardingUnlift t
-> forall (m :: Type -> Type).
   Monad m =>
   t m (WUnlift MonadTunnelIOInner t)
unGetDiscardingUnlift :: forall m. Monad m => t m (WUnlift MonadTunnelIOInner t)
    }

instance MonadTransStackUnlift tt => MonadTransUnlift (StackT tt) where
    liftWithUnlift ::
           forall m r. MonadIO m
        => (Unlift MonadTunnelIOInner (StackT tt) -> m r)
        -> StackT tt m r
    liftWithUnlift :: forall (m :: Type -> Type) r.
MonadIO m =>
(Unlift MonadTunnelIOInner (StackT tt) -> m r) -> StackT tt m r
liftWithUnlift = let
        build :: forall tt'. ListType (Compose Dict MonadTransUnlift) tt' -> LiftWithUnlift (StackT tt')
        build :: forall (tt' :: [TransKind]).
ListType (Compose Dict MonadTransUnlift) tt'
-> LiftWithUnlift (StackT tt')
build ListType (Compose Dict MonadTransUnlift) tt'
NilListType = forall (t :: TransKind).
(forall (m :: Type -> Type) r.
 MonadIO m =>
 (Unlift MonadTunnelIOInner t -> m r) -> t m r)
-> LiftWithUnlift t
MkLiftWithUnlift forall a b. (a -> b) -> a -> b
$ \Unlift MonadTunnelIOInner (StackT tt') -> m r
call -> forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall a b. (a -> b) -> a -> b
$ Unlift MonadTunnelIOInner (StackT tt') -> m r
call forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT
        build (ConsListType (Compose Dict (MonadTransUnlift a)
Dict) (ListType (Compose Dict MonadTransUnlift) lt1
w :: ListType _ tt0)) =
            case forall (tt' :: [TransKind]).
ListType (Compose Dict MonadTransUnlift) tt'
-> LiftWithUnlift (StackT tt')
build ListType (Compose Dict MonadTransUnlift) lt1
w of
                MkLiftWithUnlift forall (m :: Type -> Type) r.
MonadIO m =>
(Unlift MonadTunnelIOInner (StackT lt1) -> m r) -> StackT lt1 m r
liftWithUnlift' -> let
                    liftWithUnlift'' ::
                           forall m' r'. MonadIO m'
                        => (Unlift MonadTunnelIOInner (StackT tt') -> m' r')
                        -> StackT tt' m' r'
                    liftWithUnlift'' :: forall (m' :: Type -> Type) r'.
MonadIO m' =>
(Unlift MonadTunnelIOInner (StackT tt') -> m' r')
-> StackT tt' m' r'
liftWithUnlift'' Unlift MonadTunnelIOInner (StackT tt') -> m' r'
call =
                        forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall a b. (a -> b) -> a -> b
$
                        case forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
       (m :: Type -> Type).
cm m =>
ListType (Compose Dict (TransConstraint cm)) tt
-> Dict (cm (ApplyStack tt m))
witTransStackDict @MonadIO @tt0 @m' forall a b. (a -> b) -> a -> b
$ forall {k} (wita :: k -> Type) (witb :: k -> Type) (t :: [k]).
(forall (t' :: k). wita t' -> witb t')
-> ListType wita t -> ListType witb t
mapListType (\(Compose Dict (MonadTransUnlift t')
Dict) -> forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose forall (a :: Constraint). a => Dict a
Dict) ListType (Compose Dict MonadTransUnlift) lt1
w of
                            Dict (MonadIO (ApplyStack lt1 m'))
Dict ->
                                forall (t :: TransKind) (m :: Type -> Type) r.
(MonadTransUnlift t, MonadIO m) =>
(Unlift MonadTunnelIOInner t -> m r) -> t m r
liftWithUnlift forall a b. (a -> b) -> a -> b
$ \Unlift MonadTunnelIOInner a
unlift1 ->
                                    forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type) r.
MonadIO m =>
(Unlift MonadTunnelIOInner (StackT lt1) -> m r) -> StackT lt1 m r
liftWithUnlift' forall a b. (a -> b) -> a -> b
$ \Unlift MonadTunnelIOInner (StackT lt1)
unlift2 -> Unlift MonadTunnelIOInner (StackT tt') -> m' r'
call forall a b. (a -> b) -> a -> b
$ forall (tt :: [TransKind]) (t :: TransKind).
ListType (Compose Dict MonadTransUnlift) tt
-> Unlift MonadTunnelIOInner t
-> Unlift MonadTunnelIOInner (StackT tt)
-> Unlift MonadTunnelIOInner (StackT (t : tt))
stackJoinUnlift ListType (Compose Dict MonadTransUnlift) lt1
w Unlift MonadTunnelIOInner a
unlift1 Unlift MonadTunnelIOInner (StackT lt1)
unlift2
                    in forall (t :: TransKind).
(forall (m :: Type -> Type) r.
 MonadIO m =>
 (Unlift MonadTunnelIOInner t -> m r) -> t m r)
-> LiftWithUnlift t
MkLiftWithUnlift forall (m' :: Type -> Type) r'.
MonadIO m' =>
(Unlift MonadTunnelIOInner (StackT tt') -> m' r')
-> StackT tt' m' r'
liftWithUnlift''
        in forall (t :: TransKind).
LiftWithUnlift t
-> forall (m :: Type -> Type) r.
   MonadIO m =>
   (Unlift MonadTunnelIOInner t -> m r) -> t m r
unLiftWithUnlift forall a b. (a -> b) -> a -> b
$ forall (tt' :: [TransKind]).
ListType (Compose Dict MonadTransUnlift) tt'
-> LiftWithUnlift (StackT tt')
build forall a b. (a -> b) -> a -> b
$ forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative @_ @(ListType (Compose Dict MonadTransUnlift)) @tt
    getDiscardingUnlift ::
           forall m. Monad m
        => StackT tt m (WUnlift MonadTunnelIOInner (StackT tt))
    getDiscardingUnlift :: forall (m :: Type -> Type).
Monad m =>
StackT tt m (WUnlift MonadTunnelIOInner (StackT tt))
getDiscardingUnlift = let
        build :: forall tt'. ListType (Compose Dict MonadTransUnlift) tt' -> GetDiscardingUnlift (StackT tt')
        build :: forall (tt' :: [TransKind]).
ListType (Compose Dict MonadTransUnlift) tt'
-> GetDiscardingUnlift (StackT tt')
build ListType (Compose Dict MonadTransUnlift) tt'
NilListType = forall (t :: TransKind).
(forall (m :: Type -> Type).
 Monad m =>
 t m (WUnlift MonadTunnelIOInner t))
-> GetDiscardingUnlift t
MkGetDiscardingUnlift forall a b. (a -> b) -> a -> b
$ forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (c :: (Type -> Type) -> Constraint) (t :: TransKind).
Unlift c t -> WUnlift c t
MkWUnlift forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT
        build (ConsListType (Compose (Dict (MonadTransUnlift a)
Dict :: Dict (MonadTransUnlift t))) (ListType (Compose Dict MonadTransUnlift) lt1
w :: ListType _ tt0)) =
            case forall (tt' :: [TransKind]).
ListType (Compose Dict MonadTransUnlift) tt'
-> GetDiscardingUnlift (StackT tt')
build ListType (Compose Dict MonadTransUnlift) lt1
w of
                MkGetDiscardingUnlift forall (m :: Type -> Type).
Monad m =>
StackT lt1 m (WUnlift MonadTunnelIOInner (StackT lt1))
getDiscardingUnlift' -> let
                    getDiscardingUnlift'' ::
                           forall m'. Monad m'
                        => StackT tt' m' (WUnlift MonadTunnelIOInner (StackT tt'))
                    getDiscardingUnlift'' :: forall (m' :: Type -> Type).
Monad m' =>
StackT tt' m' (WUnlift MonadTunnelIOInner (StackT tt'))
getDiscardingUnlift'' =
                        forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall a b. (a -> b) -> a -> b
$
                        case forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
       (m :: Type -> Type).
cm m =>
ListType (Compose Dict (TransConstraint cm)) tt
-> Dict (cm (ApplyStack tt m))
witTransStackDict @Monad @tt0 @m' forall a b. (a -> b) -> a -> b
$ forall {k} (wita :: k -> Type) (witb :: k -> Type) (t :: [k]).
(forall (t' :: k). wita t' -> witb t')
-> ListType wita t -> ListType witb t
mapListType (\(Compose Dict (MonadTransUnlift t')
Dict) -> forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose forall (a :: Constraint). a => Dict a
Dict) ListType (Compose Dict MonadTransUnlift) lt1
w of
                            Dict (Monad (ApplyStack lt1 m'))
Dict ->
                                forall (c :: (Type -> Type) -> Constraint) (t :: TransKind)
       (m :: Type -> Type) a.
(TransConstraint c t, c m) =>
(c (t m) => t m a) -> t m a
withTransConstraintTM @Monad forall a b. (a -> b) -> a -> b
$ do
                                    MkWUnlift Unlift MonadTunnelIOInner a
unlift1 <- forall (t :: TransKind) (m :: Type -> Type).
(MonadTransUnlift t, Monad m) =>
t m (WUnlift MonadTunnelIOInner t)
getDiscardingUnlift
                                    MkWUnlift Unlift MonadTunnelIOInner (StackT lt1)
unlift2 <- forall (t :: TransKind) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type).
Monad m =>
StackT lt1 m (WUnlift MonadTunnelIOInner (StackT lt1))
getDiscardingUnlift' @m'
                                    forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (c :: (Type -> Type) -> Constraint) (t :: TransKind).
Unlift c t -> WUnlift c t
MkWUnlift forall a b. (a -> b) -> a -> b
$ forall (tt :: [TransKind]) (t :: TransKind).
ListType (Compose Dict MonadTransUnlift) tt
-> Unlift MonadTunnelIOInner t
-> Unlift MonadTunnelIOInner (StackT tt)
-> Unlift MonadTunnelIOInner (StackT (t : tt))
stackJoinUnlift ListType (Compose Dict MonadTransUnlift) lt1
w Unlift MonadTunnelIOInner a
unlift1 Unlift MonadTunnelIOInner (StackT lt1)
unlift2
                    in forall (t :: TransKind).
(forall (m :: Type -> Type).
 Monad m =>
 t m (WUnlift MonadTunnelIOInner t))
-> GetDiscardingUnlift t
MkGetDiscardingUnlift forall (m' :: Type -> Type).
Monad m' =>
StackT tt' m' (WUnlift MonadTunnelIOInner (StackT tt'))
getDiscardingUnlift''
        in forall (t :: TransKind).
GetDiscardingUnlift t
-> forall (m :: Type -> Type).
   Monad m =>
   t m (WUnlift MonadTunnelIOInner t)
unGetDiscardingUnlift forall a b. (a -> b) -> a -> b
$ forall (tt' :: [TransKind]).
ListType (Compose Dict MonadTransUnlift) tt'
-> GetDiscardingUnlift (StackT tt')
build forall a b. (a -> b) -> a -> b
$ forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative @_ @(ListType (Compose Dict MonadTransUnlift)) @tt

stackConcatFst ::
       forall tt1 tt2 m. (MonadTransStackUnlift tt1, MonadTransStackUnlift tt2, Monad m)
    => ApplyStack tt1 m --> ApplyStack (Concat tt1 tt2) m
stackConcatFst :: forall (tt1 :: [TransKind]) (tt2 :: [TransKind])
       (m :: Type -> Type).
(MonadTransStackUnlift tt1, MonadTransStackUnlift tt2, Monad m) =>
ApplyStack tt1 m --> ApplyStack (Concat tt1 tt2) m
stackConcatFst =
    case forall (tt1 :: [TransKind]) (tt2 :: [TransKind])
       (m :: Type -> Type).
MonadTransStackUnlift tt1 =>
ApplyStack (Concat tt1 tt2) m :~: ApplyStack tt1 (ApplyStack tt2 m)
transStackConcatRefl @tt1 @tt2 @m of
        ApplyStack (Concat tt1 tt2) m :~: ApplyStack tt1 (ApplyStack tt2 m)
Refl ->
            case forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
       (m :: Type -> Type).
(IsStack (TransConstraint cm) tt, cm m) =>
Dict (cm (ApplyStack tt m))
transStackDict @Monad @tt2 @m of
                Dict (Monad (ApplyStack tt2 m))
Dict -> forall (tt :: [TransKind]) (ma :: Type -> Type)
       (mb :: Type -> Type).
(MonadTransStackTunnel tt, Monad ma, Monad mb) =>
(ma --> mb) -> ApplyStack tt ma --> ApplyStack tt mb
stackHoist @tt1 forall a b. (a -> b) -> a -> b
$ forall (tt :: [TransKind]) (m :: Type -> Type).
(IsStack (TransConstraint Monad) tt, IsStack MonadTrans tt,
 Monad m) =>
m --> ApplyStack tt m
stackLift @tt2 @m

stackConcatSnd ::
       forall tt1 tt2 m. (MonadTransStackUnlift tt1, MonadTransStackUnlift tt2, Monad m)
    => ApplyStack tt2 m --> ApplyStack (Concat tt1 tt2) m
stackConcatSnd :: forall (tt1 :: [TransKind]) (tt2 :: [TransKind])
       (m :: Type -> Type).
(MonadTransStackUnlift tt1, MonadTransStackUnlift tt2, Monad m) =>
ApplyStack tt2 m --> ApplyStack (Concat tt1 tt2) m
stackConcatSnd =
    case forall (tt1 :: [TransKind]) (tt2 :: [TransKind])
       (m :: Type -> Type).
MonadTransStackUnlift tt1 =>
ApplyStack (Concat tt1 tt2) m :~: ApplyStack tt1 (ApplyStack tt2 m)
transStackConcatRefl @tt1 @tt2 @m of
        ApplyStack (Concat tt1 tt2) m :~: ApplyStack tt1 (ApplyStack tt2 m)
Refl ->
            case forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
       (m :: Type -> Type).
(IsStack (TransConstraint cm) tt, cm m) =>
Dict (cm (ApplyStack tt m))
transStackDict @Monad @tt2 @m of
                Dict (Monad (ApplyStack tt2 m))
Dict -> forall (tt :: [TransKind]) (m :: Type -> Type).
(IsStack (TransConstraint Monad) tt, IsStack MonadTrans tt,
 Monad m) =>
m --> ApplyStack tt m
stackLift @tt1

stackCommute ::
       forall tta ttb m r. (MonadTransStackUnlift tta, MonadTransStackUnlift ttb, MonadTunnelIO m)
    => ApplyStack tta (ApplyStack ttb m) r
    -> ApplyStack ttb (ApplyStack tta m) r
stackCommute :: forall (tta :: [TransKind]) (ttb :: [TransKind])
       (m :: Type -> Type) r.
(MonadTransStackUnlift tta, MonadTransStackUnlift ttb,
 MonadTunnelIO m) =>
ApplyStack tta (ApplyStack ttb m) r
-> ApplyStack ttb (ApplyStack tta m) r
stackCommute ApplyStack tta (ApplyStack ttb m) r
aar =
    case (forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
       (m :: Type -> Type).
(IsStack (TransConstraint cm) tt, cm m) =>
Dict (cm (ApplyStack tt m))
transStackDict @MonadTunnelIO @tta @m, forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
       (m :: Type -> Type).
(IsStack (TransConstraint cm) tt, cm m) =>
Dict (cm (ApplyStack tt m))
transStackDict @MonadTunnelIO @ttb @m) of
        (Dict (MonadTunnelIO (ApplyStack tta m))
Dict, Dict (MonadTunnelIO (ApplyStack ttb m))
Dict) -> let
            ssr :: StackT tta (StackT ttb m) r
            ssr :: StackT tta (StackT ttb m) r
ssr = forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall a b. (a -> b) -> a -> b
$ forall (tt :: [TransKind]) (ma :: Type -> Type)
       (mb :: Type -> Type).
(MonadTransStackTunnel tt, Monad ma, Monad mb) =>
(ma --> mb) -> ApplyStack tt ma --> ApplyStack tt mb
stackHoist @tta @(ApplyStack ttb m) @(StackT ttb m) forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT ApplyStack tta (ApplyStack ttb m) r
aar
            in forall (tt :: [TransKind]) (ma :: Type -> Type)
       (mb :: Type -> Type).
(MonadTransStackTunnel tt, Monad ma, Monad mb) =>
(ma --> mb) -> ApplyStack tt ma --> ApplyStack tt mb
stackHoist @ttb @(StackT tta m) @(ApplyStack tta m) forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT forall a b. (a -> b) -> a -> b
$ forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT forall a b. (a -> b) -> a -> b
$ forall (ta :: TransKind) (tb :: TransKind) (m :: Type -> Type).
(MonadTransTunnel ta, MonadTransTunnel tb, Monad (Tunnel ta),
 MonadInner (Tunnel tb), Monad m) =>
ta (tb m) --> tb (ta m)
commuteT StackT tta (StackT ttb m) r
ssr

transStackConcatRefl ::
       forall (tt1 :: [TransKind]) (tt2 :: [TransKind]) m. MonadTransStackUnlift tt1
    => (ApplyStack (Concat tt1 tt2) m) :~: (ApplyStack tt1 (ApplyStack tt2 m))
transStackConcatRefl :: forall (tt1 :: [TransKind]) (tt2 :: [TransKind])
       (m :: Type -> Type).
MonadTransStackUnlift tt1 =>
ApplyStack (Concat tt1 tt2) m :~: ApplyStack tt1 (ApplyStack tt2 m)
transStackConcatRefl = forall k (f1 :: [k -> k]) (f2 :: [k -> k]) (a :: k)
       (w :: (k -> k) -> Type).
Is (ListType w) f1 =>
ApplyStack (Concat f1 f2) a :~: ApplyStack f1 (ApplyStack f2 a)
applyConcatRefl @_ @tt1 @tt2 @m @(Compose Dict MonadTransUnlift)

type StackUnlift (tt :: [TransKind]) = forall m. MonadUnliftIO m => ApplyStack tt m --> m

newtype WStackUnlift (tt :: [TransKind]) = MkWStackUnlift
    { forall (tt :: [TransKind]). WStackUnlift tt -> StackUnlift tt
unWStackUnlift :: StackUnlift tt
    }

consWStackUnlift ::
       forall t tt. IsStack (TransConstraint MonadUnliftIO) tt
    => WUnlift MonadUnliftIO t
    -> WStackUnlift tt
    -> WStackUnlift (t ': tt)
consWStackUnlift :: forall (t :: TransKind) (tt :: [TransKind]).
IsStack (TransConstraint MonadUnliftIO) tt =>
WUnlift MonadUnliftIO t -> WStackUnlift tt -> WStackUnlift (t : tt)
consWStackUnlift (MkWUnlift Unlift MonadUnliftIO t
unlift1) (MkWStackUnlift StackUnlift tt
unliftr) = let
    unlift ::
           forall m. MonadUnliftIO m
        => t (ApplyStack tt m) --> m
    unlift :: forall (m :: Type -> Type).
MonadUnliftIO m =>
t (ApplyStack tt m) --> m
unlift =
        case forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
       (m :: Type -> Type).
(IsStack (TransConstraint cm) tt, cm m) =>
Dict (cm (ApplyStack tt m))
transStackDict @MonadUnliftIO @tt @m of
            Dict (MonadUnliftIO (ApplyStack tt m))
Dict -> StackUnlift tt
unliftr forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Unlift MonadUnliftIO t
unlift1
    in forall (tt :: [TransKind]). StackUnlift tt -> WStackUnlift tt
MkWStackUnlift forall (m :: Type -> Type).
MonadUnliftIO m =>
t (ApplyStack tt m) --> m
unlift

stackLiftWithStackUnlift ::
       forall tt m r. (MonadTransStackUnlift tt, MonadIO m)
    => (StackUnlift tt -> m r)
    -> ApplyStack tt m r
stackLiftWithStackUnlift :: forall (tt :: [TransKind]) (m :: Type -> Type) r.
(MonadTransStackUnlift tt, MonadIO m) =>
(StackUnlift tt -> m r) -> ApplyStack tt m r
stackLiftWithStackUnlift StackUnlift tt -> m r
call = forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT @tt forall a b. (a -> b) -> a -> b
$ forall (t :: TransKind) (m :: Type -> Type) r.
(MonadTransUnlift t, MonadIO m) =>
(Unlift MonadTunnelIOInner t -> m r) -> t m r
liftWithUnlift forall a b. (a -> b) -> a -> b
$ \Unlift MonadTunnelIOInner (StackT tt)
unlift -> StackUnlift tt -> m r
call forall a b. (a -> b) -> a -> b
$ \ApplyStack tt m a
astm -> Unlift MonadTunnelIOInner (StackT tt)
unlift forall a b. (a -> b) -> a -> b
$ forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT ApplyStack tt m a
astm