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 = Dict (cm m)
Dict (cm (ApplyStack tt m))
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 (ListType (Compose Dict (TransConstraint cm)) tt
 -> Dict (cm (ApplyStack tt m)))
-> ListType (Compose Dict (TransConstraint cm)) tt
-> Dict (cm (ApplyStack 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) -> ApplyStack tt m b -> StackT tt m b
forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT (ApplyStack tt m b -> StackT tt m b)
-> ApplyStack tt m b -> StackT tt m b
forall a b. (a -> b) -> a -> b
$ (a -> b) -> ApplyStack tt m a -> ApplyStack tt m b
forall a b. (a -> b) -> ApplyStack tt m a -> ApplyStack tt m 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 -> ApplyStack tt m a -> StackT tt m a
forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT (ApplyStack tt m a -> StackT tt m a)
-> ApplyStack tt m a -> StackT tt m a
forall a b. (a -> b) -> a -> b
$ a -> ApplyStack tt m a
forall a. a -> ApplyStack tt m a
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) -> ApplyStack tt m b -> StackT tt m b
forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT (ApplyStack tt m b -> StackT tt m b)
-> ApplyStack tt m b -> StackT tt m b
forall a b. (a -> b) -> a -> b
$ ApplyStack tt m (a -> b)
mab ApplyStack tt m (a -> b) -> ApplyStack tt m a -> ApplyStack tt m b
forall a b.
ApplyStack tt m (a -> b) -> ApplyStack tt m a -> ApplyStack tt m b
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 = a -> StackT tt m a
forall a. a -> StackT tt m a
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 -> ApplyStack tt m b -> StackT tt m b
forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT (ApplyStack tt m b -> StackT tt m b)
-> ApplyStack tt m b -> StackT tt m b
forall a b. (a -> b) -> a -> b
$ ApplyStack tt m a
ma ApplyStack tt m a -> (a -> ApplyStack tt m b) -> ApplyStack tt m b
forall a b.
ApplyStack tt m a -> (a -> ApplyStack tt m b) -> ApplyStack tt m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
a -> StackT tt m b -> ApplyStack tt m b
forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT (StackT tt m b -> ApplyStack tt m b)
-> StackT tt m b -> ApplyStack tt m b
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 = Dict (Monad (StackT tt m))
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 = m a -> StackT tt m a
forall (m :: Type -> Type) a. Monad m => m a -> StackT tt m a
forall (t :: TransKind) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a -> StackT tt m a) -> m a -> StackT tt m a
forall a b. (a -> b) -> a -> b
$ String -> m a
forall a. String -> m a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
s

instance (IsStack (TransConstraint Monad) tt, IsStack MonadTrans tt) => TransConstraint MonadFail (StackT tt) where
    hasTransConstraint :: forall (m :: Type -> Type).
MonadFail m =>
Dict (MonadFail (StackT tt m))
hasTransConstraint = Dict (MonadFail (StackT tt m))
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 -> ApplyStack tt m a -> StackT tt m a
forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT (ApplyStack tt m a -> StackT tt m a)
-> ApplyStack tt m a -> StackT tt m a
forall a b. (a -> b) -> a -> b
$ (a -> ApplyStack tt m a) -> ApplyStack tt m a
forall a. (a -> ApplyStack tt m a) -> ApplyStack tt m a
forall (m :: Type -> Type) a. MonadFix m => (a -> m a) -> m a
mfix ((a -> ApplyStack tt m a) -> ApplyStack tt m a)
-> (a -> ApplyStack tt m a) -> ApplyStack tt m a
forall a b. (a -> b) -> a -> b
$ \a
a -> StackT tt m a -> ApplyStack tt m a
forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT (StackT tt m a -> ApplyStack tt m a)
-> StackT tt m a -> ApplyStack tt m a
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 = Dict (MonadFix (StackT tt m))
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 -> ApplyStack tt m a -> StackT tt m a
forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT (ApplyStack tt m a -> StackT tt m a)
-> ApplyStack tt m a -> StackT tt m a
forall a b. (a -> b) -> a -> b
$ IO a -> ApplyStack tt m a
forall a. IO a -> ApplyStack tt m a
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 = Dict (MonadIO (StackT tt m))
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 -> ApplyStack tt m a -> StackT tt m a
forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT ApplyStack tt m a
forall a. ApplyStack tt m a
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) -> ApplyStack tt m a -> StackT tt m a
forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT (ApplyStack tt m a -> StackT tt m a)
-> ApplyStack tt m a -> StackT tt m a
forall a b. (a -> b) -> a -> b
$ ApplyStack tt m a
a ApplyStack tt m a -> ApplyStack tt m a -> ApplyStack tt m a
forall a.
ApplyStack tt m a -> ApplyStack tt m a -> ApplyStack tt m 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 = Dict (MonadPlus (StackT tt m))
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 = (WRaised m m
WRaised m (ApplyStack tt' m)
forall {k} (cat :: k -> k -> Type) (a :: k).
Category cat =>
cat a a
forall (a :: Type -> Type). WRaised a a
id, Dict (Monad m)
Dict (Monad (ApplyStack tt' m))
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 ListType (Compose Dict (TransConstraint Monad)) lt1
-> ListType (Compose Dict MonadTrans) lt1
-> (WRaised m (ApplyStack lt1 m), Dict (Monad (ApplyStack lt1 m)))
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
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) -> (WRaised (ApplyStack lt1 m) (a (ApplyStack lt1 m))
forall (t :: TransKind) (m :: Type -> Type).
(MonadTrans t, Monad m) =>
WRaised m (t m)
wLift WRaised (ApplyStack lt1 m) (a (ApplyStack lt1 m))
-> WRaised m (ApplyStack lt1 m) -> WRaised m (a (ApplyStack lt1 m))
forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
forall (b :: Type -> Type) (c :: Type -> Type) (a :: Type -> Type).
WRaised b c -> WRaised a b -> WRaised 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 ListType (Compose Dict (TransConstraint Monad)) tt
-> ListType (Compose Dict MonadTrans) tt
-> (WRaised m (ApplyStack tt m), Dict (Monad (ApplyStack tt m)))
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 -> ApplyStack tt m a -> StackT tt m a
forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT (ApplyStack tt m a -> StackT tt m a)
-> ApplyStack tt m a -> StackT tt m a
forall a b. (a -> b) -> a -> b
$ WRaised m (ApplyStack tt m) -> m --> ApplyStack tt m
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 (StackT tt m a -> ApplyStack tt m a)
-> StackT tt m a -> ApplyStack tt m a
forall a b. (a -> b) -> a -> b
$ m a -> StackT tt m a
forall (m :: Type -> Type) a. Monad m => m a -> StackT tt m a
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 ((Is
    (ListType (Compose Dict (TransConstraint Monad)))
    (Concat tt1 tt2) =>
  Dict (MonadTransStackTunnel (Concat tt1 tt2)))
 -> Dict (MonadTransStackTunnel (Concat tt1 tt2)))
-> (Is
      (ListType (Compose Dict (TransConstraint Monad)))
      (Concat tt1 tt2) =>
    Dict (MonadTransStackTunnel (Concat tt1 tt2)))
-> Dict (MonadTransStackTunnel (Concat 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 ((Is (ListType (Compose Dict MonadTransTunnel)) (Concat tt1 tt2) =>
  Dict (MonadTransStackTunnel (Concat tt1 tt2)))
 -> Dict (MonadTransStackTunnel (Concat tt1 tt2)))
-> (Is
      (ListType (Compose Dict MonadTransTunnel)) (Concat tt1 tt2) =>
    Dict (MonadTransStackTunnel (Concat tt1 tt2)))
-> Dict (MonadTransStackTunnel (Concat 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 ((Is (ListType (Compose Dict MonadTrans)) (Concat tt1 tt2) =>
  Dict (MonadTransStackTunnel (Concat tt1 tt2)))
 -> Dict (MonadTransStackTunnel (Concat tt1 tt2)))
-> (Is (ListType (Compose Dict MonadTrans)) (Concat tt1 tt2) =>
    Dict (MonadTransStackTunnel (Concat tt1 tt2)))
-> Dict (MonadTransStackTunnel (Concat 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 ((Is
    (ListType (Compose Dict (WithTunnelConstraint Functor)))
    (Concat tt1 tt2) =>
  Dict (MonadTransStackTunnel (Concat tt1 tt2)))
 -> Dict (MonadTransStackTunnel (Concat tt1 tt2)))
-> (Is
      (ListType (Compose Dict (WithTunnelConstraint Functor)))
      (Concat tt1 tt2) =>
    Dict (MonadTransStackTunnel (Concat tt1 tt2)))
-> Dict (MonadTransStackTunnel (Concat 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 ((Is
    (ListType (Compose Dict (WithTunnelConstraint Applicative)))
    (Concat tt1 tt2) =>
  Dict (MonadTransStackTunnel (Concat tt1 tt2)))
 -> Dict (MonadTransStackTunnel (Concat tt1 tt2)))
-> (Is
      (ListType (Compose Dict (WithTunnelConstraint Applicative)))
      (Concat tt1 tt2) =>
    Dict (MonadTransStackTunnel (Concat tt1 tt2)))
-> Dict (MonadTransStackTunnel (Concat 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 ((Is
    (ListType (Compose Dict (WithTunnelConstraint Monad)))
    (Concat tt1 tt2) =>
  Dict (MonadTransStackTunnel (Concat tt1 tt2)))
 -> Dict (MonadTransStackTunnel (Concat tt1 tt2)))
-> (Is
      (ListType (Compose Dict (WithTunnelConstraint Monad)))
      (Concat tt1 tt2) =>
    Dict (MonadTransStackTunnel (Concat tt1 tt2)))
-> Dict (MonadTransStackTunnel (Concat 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 ((Is
    (ListType (Compose Dict (WithTunnelConstraint Traversable)))
    (Concat tt1 tt2) =>
  Dict (MonadTransStackTunnel (Concat tt1 tt2)))
 -> Dict (MonadTransStackTunnel (Concat tt1 tt2)))
-> (Is
      (ListType (Compose Dict (WithTunnelConstraint Traversable)))
      (Concat tt1 tt2) =>
    Dict (MonadTransStackTunnel (Concat tt1 tt2)))
-> Dict (MonadTransStackTunnel (Concat 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 ((Is
    (ListType (Compose Dict (WithTunnelConstraint MonadInner)))
    (Concat tt1 tt2) =>
  Dict (MonadTransStackTunnel (Concat tt1 tt2)))
 -> Dict (MonadTransStackTunnel (Concat tt1 tt2)))
-> (Is
      (ListType (Compose Dict (WithTunnelConstraint MonadInner)))
      (Concat tt1 tt2) =>
    Dict (MonadTransStackTunnel (Concat tt1 tt2)))
-> Dict (MonadTransStackTunnel (Concat tt1 tt2))
forall a b. (a -> b) -> a -> b
$ Dict (MonadTransStackTunnel (Concat tt1 tt2))
Is
  (ListType (Compose Dict (WithTunnelConstraint MonadInner)))
  (Concat tt1 tt2) =>
Dict (MonadTransStackTunnel (Concat tt1 tt2))
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 = Dict (c Identity)
Dict (c (ApplyStackTunnel tt))
forall (a :: Constraint). a => Dict a
Dict
astIsWithTunnelConstraint (ConsListType (Compose Dict (WithTunnelConstraint c a)
Dict) ListType (Compose Dict (WithTunnelConstraint c)) lt1
w) =
    case ListType (Compose Dict (WithTunnelConstraint c)) lt1
-> Dict (c (ApplyStackTunnel lt1))
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 -> Dict (c (ComposeInner (Tunnel a) (ApplyStackTunnel lt1)))
Dict (c (ApplyStackTunnel tt))
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 (ListType (Compose Dict (WithTunnelConstraint c)) tt
 -> Dict (c (ApplyStackTunnel tt)))
-> ListType (Compose Dict (WithTunnelConstraint c)) tt
-> Dict (c (ApplyStackTunnel tt))
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) -> ApplyStackTunnel tt b -> StackTunnel tt b
forall (tt :: [TransKind]) a.
ApplyStackTunnel tt a -> StackTunnel tt a
MkStackTunnel (ApplyStackTunnel tt b -> StackTunnel tt b)
-> ApplyStackTunnel tt b -> StackTunnel tt b
forall a b. (a -> b) -> a -> b
$ (a -> b) -> ApplyStackTunnel tt a -> ApplyStackTunnel tt b
forall a b.
(a -> b) -> ApplyStackTunnel tt a -> ApplyStackTunnel tt 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 -> ApplyStackTunnel tt a -> StackTunnel tt a
forall (tt :: [TransKind]) a.
ApplyStackTunnel tt a -> StackTunnel tt a
MkStackTunnel (ApplyStackTunnel tt a -> StackTunnel tt a)
-> ApplyStackTunnel tt a -> StackTunnel tt a
forall a b. (a -> b) -> a -> b
$ a -> ApplyStackTunnel tt a
forall a. a -> ApplyStackTunnel tt a
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) -> ApplyStackTunnel tt b -> StackTunnel tt b
forall (tt :: [TransKind]) a.
ApplyStackTunnel tt a -> StackTunnel tt a
MkStackTunnel (ApplyStackTunnel tt b -> StackTunnel tt b)
-> ApplyStackTunnel tt b -> StackTunnel tt b
forall a b. (a -> b) -> a -> b
$ ApplyStackTunnel tt (a -> b)
mab ApplyStackTunnel tt (a -> b)
-> ApplyStackTunnel tt a -> ApplyStackTunnel tt b
forall a b.
ApplyStackTunnel tt (a -> b)
-> ApplyStackTunnel tt a -> ApplyStackTunnel tt b
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) -> (a -> m) -> ApplyStackTunnel tt a -> m
forall m a. Monoid m => (a -> m) -> ApplyStackTunnel tt a -> m
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) -> ApplyStackTunnel tt b -> StackTunnel tt b
forall (tt :: [TransKind]) a.
ApplyStackTunnel tt a -> StackTunnel tt a
MkStackTunnel (ApplyStackTunnel tt b -> StackTunnel tt b)
-> f (ApplyStackTunnel tt b) -> f (StackTunnel tt b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> f b) -> ApplyStackTunnel tt a -> f (ApplyStackTunnel tt b)
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> ApplyStackTunnel tt a -> f (ApplyStackTunnel tt 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 = a -> StackTunnel tt a
forall a. a -> StackTunnel tt a
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 -> ApplyStackTunnel tt b -> StackTunnel tt b
forall (tt :: [TransKind]) a.
ApplyStackTunnel tt a -> StackTunnel tt a
MkStackTunnel (ApplyStackTunnel tt b -> StackTunnel tt b)
-> ApplyStackTunnel tt b -> StackTunnel tt b
forall a b. (a -> b) -> a -> b
$ ApplyStackTunnel tt a
ma ApplyStackTunnel tt a
-> (a -> ApplyStackTunnel tt b) -> ApplyStackTunnel tt b
forall a b.
ApplyStackTunnel tt a
-> (a -> ApplyStackTunnel tt b) -> ApplyStackTunnel tt b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= StackTunnel tt b -> ApplyStackTunnel tt b
forall (tt :: [TransKind]) a.
StackTunnel tt a -> ApplyStackTunnel tt a
unStackTunnel (StackTunnel tt b -> ApplyStackTunnel tt b)
-> (a -> StackTunnel tt b) -> a -> ApplyStackTunnel tt b
forall b c a. (b -> c) -> (a -> b) -> a -> c
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 -> ApplyStackTunnel tt a -> StackTunnel tt a
forall (tt :: [TransKind]) a.
ApplyStackTunnel tt a -> StackTunnel tt a
MkStackTunnel (ApplyStackTunnel tt a -> StackTunnel tt a)
-> ApplyStackTunnel tt a -> StackTunnel tt a
forall a b. (a -> b) -> a -> b
$ Exc (ApplyStackTunnel tt) -> ApplyStackTunnel tt a
forall a. Exc (ApplyStackTunnel tt) -> ApplyStackTunnel tt a
forall (m :: Type -> Type) a. MonadException m => Exc m -> m a
throwExc Exc (StackTunnel tt)
Exc (ApplyStackTunnel 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 -> ApplyStackTunnel tt a -> StackTunnel tt a
forall (tt :: [TransKind]) a.
ApplyStackTunnel tt a -> StackTunnel tt a
MkStackTunnel (ApplyStackTunnel tt a -> StackTunnel tt a)
-> ApplyStackTunnel tt a -> StackTunnel tt a
forall a b. (a -> b) -> a -> b
$ ApplyStackTunnel tt a
-> (Exc (ApplyStackTunnel tt) -> ApplyStackTunnel tt a)
-> ApplyStackTunnel tt a
forall a.
ApplyStackTunnel tt a
-> (Exc (ApplyStackTunnel tt) -> ApplyStackTunnel tt a)
-> ApplyStackTunnel tt a
forall (m :: Type -> Type) a.
MonadException m =>
m a -> (Exc m -> m a) -> m a
catchExc ApplyStackTunnel tt a
st (StackTunnel tt a -> ApplyStackTunnel tt a
forall (tt :: [TransKind]) a.
StackTunnel tt a -> ApplyStackTunnel tt a
unStackTunnel (StackTunnel tt a -> ApplyStackTunnel tt a)
-> (Exc (ApplyStackTunnel tt) -> StackTunnel tt a)
-> Exc (ApplyStackTunnel tt)
-> ApplyStackTunnel tt a
forall b c a. (b -> c) -> (a -> b) -> a -> c
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
Exc (ApplyStackTunnel 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) -> ApplyStackTunnel tt a -> Result (Exc (ApplyStackTunnel tt)) a
forall a.
ApplyStackTunnel tt a -> Result (Exc (ApplyStackTunnel tt)) a
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
         ) => 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) -> ApplyStackTunnel tt a -> a
Extract (ApplyStackTunnel tt)
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 = (m1 --> m2) -> StackT tt m1 --> StackT tt m2
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 (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)
-> TunnelWrapper (StackT tt')
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)
 -> TunnelWrapper (StackT tt'))
-> (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)
-> TunnelWrapper (StackT tt')
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 ->
                ApplyStack tt' m2 r -> StackT tt' m2 r
forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT (ApplyStack tt' m2 r -> StackT tt' m2 r)
-> ApplyStack tt' m2 r -> StackT tt' m2 r
forall a b. (a -> b) -> a -> b
$ (StackTunnel '[] r -> r)
-> ApplyStack tt' m2 (StackTunnel '[] r) -> ApplyStack tt' m2 r
forall a b. (a -> b) -> ApplyStack tt' m2 a -> ApplyStack tt' m2 b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Identity r -> r
forall a. Identity a -> a
runIdentity (Identity r -> r)
-> (StackTunnel '[] r -> Identity r) -> StackTunnel '[] r -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. StackTunnel '[] r -> Identity r
StackTunnel '[] r -> ApplyStackTunnel '[] r
forall (tt :: [TransKind]) a.
StackTunnel tt a -> ApplyStackTunnel tt a
unStackTunnel) (ApplyStack tt' m2 (StackTunnel '[] r) -> ApplyStack tt' m2 r)
-> ApplyStack tt' m2 (StackTunnel '[] r) -> ApplyStack tt' m2 r
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 (m1 :: Type -> Type) a.
  Monad m1 =>
  StackT tt' m1 a -> m1 (Tunnel (StackT tt') a))
 -> m2 (Tunnel (StackT tt') r))
-> (forall (m1 :: Type -> Type) a.
    Monad m1 =>
    StackT tt' m1 a -> m1 (Tunnel (StackT tt') a))
-> m2 (Tunnel (StackT tt') r)
forall a b. (a -> b) -> a -> b
$ (a -> StackTunnel '[] a) -> m1 a -> m1 (StackTunnel '[] a)
forall a b. (a -> b) -> m1 a -> m1 b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Identity a -> StackTunnel '[] a
ApplyStackTunnel '[] a -> StackTunnel '[] a
forall (tt :: [TransKind]) a.
ApplyStackTunnel tt a -> StackTunnel tt a
MkStackTunnel (Identity a -> StackTunnel '[] a)
-> (a -> Identity a) -> a -> StackTunnel '[] a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> Identity a
forall a. a -> Identity a
Identity) (m1 a -> m1 (StackTunnel '[] a))
-> (StackT '[] m1 a -> m1 a)
-> StackT '[] m1 a
-> m1 (StackTunnel '[] a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. StackT '[] m1 a -> m1 a
StackT '[] m1 a -> ApplyStack '[] m1 a
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 ListType (Compose Dict MonadTransTunnel) lt1
-> TunnelWrapper (StackT lt1)
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' (ListType (Compose Dict (TransConstraint Monad)) lt1
 -> Dict (Monad (ApplyStack lt1 m2')))
-> ListType (Compose Dict (TransConstraint Monad)) lt1
-> Dict (Monad (ApplyStack lt1 m2'))
forall a b. (a -> b) -> a -> b
$ (forall (t' :: TransKind).
 Compose Dict MonadTransTunnel t'
 -> Compose Dict (TransConstraint Monad) t')
-> ListType (Compose Dict MonadTransTunnel) lt1
-> ListType (Compose Dict (TransConstraint Monad)) lt1
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) -> Dict (TransConstraint Monad t')
-> Compose Dict (TransConstraint Monad) t'
forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose Dict (TransConstraint Monad t')
forall (a :: Constraint). a => Dict a
Dict) ListType (Compose Dict MonadTransTunnel) lt1
w) of
                            Dict (Monad (ApplyStack lt1 m2'))
Dict ->
                                ApplyStack tt' m2' r' -> StackT tt' m2' r'
forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT (ApplyStack tt' m2' r' -> StackT tt' m2' r')
-> ApplyStack tt' m2' r' -> StackT tt' m2' r'
forall a b. (a -> b) -> a -> b
$
                                ((forall (m1 :: Type -> Type) a.
  Monad m1 =>
  a m1 a -> m1 (Tunnel a a))
 -> ApplyStack lt1 m2' (Tunnel a r'))
-> a (ApplyStack lt1 m2') r'
forall (m :: Type -> Type) r.
Monad m =>
((forall (m1 :: Type -> Type) a.
  Monad m1 =>
  a m1 a -> m1 (Tunnel a a))
 -> m (Tunnel a r))
-> a m r
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 (m1 :: Type -> Type) a.
   Monad m1 =>
   a m1 a -> m1 (Tunnel a a))
  -> ApplyStack lt1 m2' (Tunnel a r'))
 -> a (ApplyStack lt1 m2') r')
-> ((forall (m1 :: Type -> Type) a.
     Monad m1 =>
     a m1 a -> m1 (Tunnel a a))
    -> ApplyStack lt1 m2' (Tunnel a r'))
-> a (ApplyStack lt1 m2') r'
forall a b. (a -> b) -> a -> b
$ \forall (m1 :: Type -> Type) a.
Monad m1 =>
a m1 a -> m1 (Tunnel a a)
unlift1 ->
                                    StackT lt1 m2' (Tunnel a r') -> ApplyStack lt1 m2' (Tunnel a r')
forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT (StackT lt1 m2' (Tunnel a r') -> ApplyStack lt1 m2' (Tunnel a r'))
-> StackT lt1 m2' (Tunnel a r') -> ApplyStack lt1 m2' (Tunnel a r')
forall a b. (a -> b) -> a -> b
$
                                    ((forall (m1 :: Type -> Type) a.
  Monad m1 =>
  StackT lt1 m1 a -> m1 (Tunnel (StackT lt1) a))
 -> m2' (Tunnel (StackT lt1) (Tunnel a r')))
-> StackT lt1 m2' (Tunnel a r')
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 (m1 :: Type -> Type) a.
   Monad m1 =>
   StackT lt1 m1 a -> m1 (Tunnel (StackT lt1) a))
  -> m2' (Tunnel (StackT lt1) (Tunnel a r')))
 -> StackT lt1 m2' (Tunnel a r'))
-> ((forall (m1 :: Type -> Type) a.
     Monad m1 =>
     StackT lt1 m1 a -> m1 (Tunnel (StackT lt1) a))
    -> m2' (Tunnel (StackT lt1) (Tunnel a r')))
-> StackT lt1 m2' (Tunnel a r')
forall a b. (a -> b) -> a -> b
$ \forall (m1 :: Type -> Type) a.
Monad m1 =>
StackT lt1 m1 a -> m1 (Tunnel (StackT lt1) a)
unlift2 ->
                                        (StackTunnel (a : lt1) r' -> Tunnel (StackT lt1) (Tunnel a r'))
-> m2' (StackTunnel (a : lt1) r')
-> m2' (Tunnel (StackT lt1) (Tunnel a r'))
forall a b. (a -> b) -> m2' a -> m2' b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (ApplyStackTunnel lt1 (Tunnel a r') -> StackTunnel lt1 (Tunnel a r')
forall (tt :: [TransKind]) a.
ApplyStackTunnel tt a -> StackTunnel tt a
MkStackTunnel (ApplyStackTunnel lt1 (Tunnel a r')
 -> StackTunnel lt1 (Tunnel a r'))
-> (StackTunnel (a : lt1) r' -> ApplyStackTunnel lt1 (Tunnel a r'))
-> StackTunnel (a : lt1) r'
-> StackTunnel lt1 (Tunnel a r')
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ComposeInner (Tunnel a) (ApplyStackTunnel lt1) r'
-> ApplyStackTunnel lt1 (Tunnel a r')
forall (inner :: Type -> Type) (outer :: Type -> Type) a.
ComposeInner inner outer a -> outer (inner a)
unComposeInner (ComposeInner (Tunnel a) (ApplyStackTunnel lt1) r'
 -> ApplyStackTunnel lt1 (Tunnel a r'))
-> (StackTunnel (a : lt1) r'
    -> ComposeInner (Tunnel a) (ApplyStackTunnel lt1) r')
-> StackTunnel (a : lt1) r'
-> ApplyStackTunnel lt1 (Tunnel a r')
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. StackTunnel (a : lt1) r'
-> ComposeInner (Tunnel a) (ApplyStackTunnel lt1) r'
StackTunnel (a : lt1) r' -> ApplyStackTunnel (a : lt1) r'
forall (tt :: [TransKind]) a.
StackTunnel tt a -> ApplyStackTunnel tt a
unStackTunnel) (m2' (StackTunnel (a : lt1) r')
 -> m2' (Tunnel (StackT lt1) (Tunnel a r')))
-> m2' (StackTunnel (a : lt1) r')
-> m2' (Tunnel (StackT lt1) (Tunnel a r'))
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 (m1 :: Type -> Type) a.
  Monad m1 =>
  StackT tt' m1 a -> m1 (Tunnel (StackT tt') a))
 -> m2' (Tunnel (StackT tt') r'))
-> (forall (m1 :: Type -> Type) a.
    Monad m1 =>
    StackT tt' m1 a -> m1 (Tunnel (StackT tt') a))
-> m2' (Tunnel (StackT tt') r')
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 (ListType (Compose Dict (TransConstraint Monad)) lt1
 -> Dict (Monad (ApplyStack lt1 m1)))
-> ListType (Compose Dict (TransConstraint Monad)) lt1
-> Dict (Monad (ApplyStack lt1 m1))
forall a b. (a -> b) -> a -> b
$
                                                  (forall (t' :: TransKind).
 Compose Dict MonadTransTunnel t'
 -> Compose Dict (TransConstraint Monad) t')
-> ListType (Compose Dict MonadTransTunnel) lt1
-> ListType (Compose Dict (TransConstraint Monad)) lt1
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) -> Dict (TransConstraint Monad t')
-> Compose Dict (TransConstraint Monad) t'
forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose Dict (TransConstraint Monad t')
forall (a :: Constraint). a => Dict a
Dict) ListType (Compose Dict MonadTransTunnel) lt1
w) of
                                                Dict (Monad (ApplyStack lt1 m1))
Dict ->
                                                    (StackTunnel lt1 (Tunnel a a) -> Tunnel (StackT tt') a)
-> m1 (StackTunnel lt1 (Tunnel a a)) -> m1 (Tunnel (StackT tt') a)
forall a b. (a -> b) -> m1 a -> m1 b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (ComposeInner (Tunnel a) (ApplyStackTunnel lt1) a
-> StackTunnel (a : lt1) a
ApplyStackTunnel (a : lt1) a -> StackTunnel (a : lt1) a
forall (tt :: [TransKind]) a.
ApplyStackTunnel tt a -> StackTunnel tt a
MkStackTunnel (ComposeInner (Tunnel a) (ApplyStackTunnel lt1) a
 -> StackTunnel (a : lt1) a)
-> (StackTunnel lt1 (Tunnel a a)
    -> ComposeInner (Tunnel a) (ApplyStackTunnel lt1) a)
-> StackTunnel lt1 (Tunnel a a)
-> StackTunnel (a : lt1) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ApplyStackTunnel lt1 (Tunnel a a)
-> ComposeInner (Tunnel a) (ApplyStackTunnel lt1) a
forall (inner :: Type -> Type) (outer :: Type -> Type) a.
outer (inner a) -> ComposeInner inner outer a
MkComposeInner (ApplyStackTunnel lt1 (Tunnel a a)
 -> ComposeInner (Tunnel a) (ApplyStackTunnel lt1) a)
-> (StackTunnel lt1 (Tunnel a a)
    -> ApplyStackTunnel lt1 (Tunnel a a))
-> StackTunnel lt1 (Tunnel a a)
-> ComposeInner (Tunnel a) (ApplyStackTunnel lt1) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. StackTunnel lt1 (Tunnel a a) -> ApplyStackTunnel lt1 (Tunnel a a)
forall (tt :: [TransKind]) a.
StackTunnel tt a -> ApplyStackTunnel tt a
unStackTunnel) (m1 (StackTunnel lt1 (Tunnel a a)) -> m1 (Tunnel (StackT tt') a))
-> m1 (StackTunnel lt1 (Tunnel a a)) -> m1 (Tunnel (StackT tt') a)
forall a b. (a -> b) -> a -> b
$
                                                    StackT lt1 m1 (Tunnel a a) -> m1 (Tunnel (StackT lt1) (Tunnel a a))
forall (m1 :: Type -> Type) a.
Monad m1 =>
StackT lt1 m1 a -> m1 (Tunnel (StackT lt1) a)
unlift2 (StackT lt1 m1 (Tunnel a a)
 -> m1 (Tunnel (StackT lt1) (Tunnel a a)))
-> StackT lt1 m1 (Tunnel a a)
-> m1 (Tunnel (StackT lt1) (Tunnel a a))
forall a b. (a -> b) -> a -> b
$ ApplyStack lt1 m1 (Tunnel a a) -> StackT lt1 m1 (Tunnel a a)
forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT (ApplyStack lt1 m1 (Tunnel a a) -> StackT lt1 m1 (Tunnel a a))
-> ApplyStack lt1 m1 (Tunnel a a) -> StackT lt1 m1 (Tunnel a a)
forall a b. (a -> b) -> a -> b
$ a (ApplyStack lt1 m1) a -> ApplyStack lt1 m1 (Tunnel a a)
forall (m1 :: Type -> Type) a.
Monad m1 =>
a m1 a -> m1 (Tunnel a a)
unlift1 a (ApplyStack lt1 m1) a
ApplyStack tt' m1 a
stt
                    in (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)
-> TunnelWrapper (StackT tt')
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 (m1 :: Type -> Type) a.
  Monad m1 =>
  StackT tt' m1 a -> m1 (Tunnel (StackT tt') a))
 -> m2 (Tunnel (StackT tt') r))
-> StackT tt' m2 r
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 TunnelWrapper (StackT tt)
-> 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
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 (TunnelWrapper (StackT tt)
 -> 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)
-> TunnelWrapper (StackT tt)
-> 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
forall a b. (a -> b) -> a -> b
$ ListType (Compose Dict MonadTransTunnel) tt
-> TunnelWrapper (StackT tt)
forall (tt' :: [TransKind]).
ListType (Compose Dict MonadTransTunnel) tt'
-> TunnelWrapper (StackT tt')
build (ListType (Compose Dict MonadTransTunnel) tt
 -> TunnelWrapper (StackT tt))
-> ListType (Compose Dict MonadTransTunnel) tt
-> TunnelWrapper (StackT tt)
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 = StackT tt mb a -> ApplyStack tt mb a
forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT (StackT tt mb a -> ApplyStack tt mb a)
-> StackT tt mb a -> ApplyStack tt mb a
forall a b. (a -> b) -> a -> b
$ (ma --> mb) -> StackT tt ma --> StackT tt mb
forall (m1 :: Type -> Type) (m2 :: Type -> Type).
(Monad m1, Monad m2) =>
(m1 --> m2) -> StackT tt m1 --> StackT tt m2
forall (t :: TransKind) (m1 :: Type -> Type) (m2 :: Type -> Type).
(MonadTransHoist t, Monad m1, Monad m2) =>
(m1 --> m2) -> t m1 --> t m2
hoist ma a -> mb a
ma --> mb
mf (StackT tt ma a -> StackT tt mb a)
-> StackT tt ma a -> StackT tt mb a
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 = StackT tt m (Either e a) -> ApplyStack tt m (Either e a)
forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT (StackT tt m (Either e a) -> ApplyStack tt m (Either e a))
-> StackT tt m (Either e a) -> ApplyStack tt m (Either e a)
forall a b. (a -> b) -> a -> b
$ StackT tt (ExceptT e m) a -> StackT tt m (Either e a)
forall (t :: TransKind) (m :: Type -> Type) e a.
(MonadTransTunnel t, Monad m) =>
t (ExceptT e m) a -> t m (Either e a)
transExcept (StackT tt (ExceptT e m) a -> StackT tt m (Either e a))
-> StackT tt (ExceptT e m) a -> StackT tt m (Either e a)
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 IO a -> m a
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 = WBackraised (StackT tt ma) (StackT tt mb)
-> WBackraised (ApplyStack tt ma) (ApplyStack tt mb)
forall a b. Coercible a b => a -> b
coerce (WBackraised (StackT tt ma) (StackT tt mb)
 -> WBackraised (ApplyStack tt ma) (ApplyStack tt mb))
-> WBackraised (StackT tt ma) (StackT tt mb)
-> WBackraised (ApplyStack tt ma) (ApplyStack tt mb)
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 = WBackraised (ApplyStack tt ma) (ApplyStack tt mb)
-> ApplyStack tt ma -/-> ApplyStack tt mb
forall k (p :: k -> Type) (q :: k -> Type).
WBackraised p q -> p -/-> q
unWBackraised (WBackraised (ApplyStack tt ma) (ApplyStack tt mb)
 -> ApplyStack tt ma -/-> ApplyStack tt mb)
-> WBackraised (ApplyStack tt ma) (ApplyStack tt mb)
-> ApplyStack tt ma -/-> ApplyStack tt mb
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 (WBackraised ma mb
 -> WBackraised (ApplyStack tt ma) (ApplyStack tt mb))
-> WBackraised ma mb
-> WBackraised (ApplyStack tt ma) (ApplyStack tt mb)
forall a b. (a -> b) -> a -> b
$ (ma -/-> mb) -> WBackraised ma mb
forall k (p :: k -> Type) (q :: k -> Type).
(p -/-> q) -> WBackraised p q
MkWBackraised ((mb --> ma) -> ma r) -> mb r
ma -/-> mb
f

type MonadTransStackUnlift tt
     = ( IsStack (TransConstraint MonadFail) tt
       , IsStack (TransConstraint MonadIO) tt
       , IsStack (TransConstraint MonadFix) tt
       , IsStack (TransConstraint MonadTunnelIO) 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 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 -> Dict (MonadTransStackUnlift (Concat tt1 tt2))
forall (a :: Constraint). a => Dict a
Dict

stackLiftWithUnlift ::
       forall tt m. (MonadTransStackUnlift tt, MonadTunnelIO m)
    => m -/-> ApplyStack tt m
stackLiftWithUnlift :: forall (tt :: [TransKind]) (m :: Type -> Type).
(MonadTransStackUnlift tt, MonadTunnelIO m) =>
m -/-> ApplyStack tt m
stackLiftWithUnlift = WBackraised m (ApplyStack tt m) -> m -/-> ApplyStack tt m
forall k (p :: k -> Type) (q :: k -> Type).
WBackraised p q -> p -/-> q
unWBackraised (WBackraised m (ApplyStack tt m) -> m -/-> ApplyStack tt m)
-> WBackraised m (ApplyStack tt m) -> m -/-> ApplyStack tt m
forall a b. (a -> b) -> a -> b
$ WBackraised m (StackT tt m) -> WBackraised m (ApplyStack tt m)
forall a b. Coercible a b => a -> b
coerce (WBackraised m (StackT tt m) -> WBackraised m (ApplyStack tt m))
-> WBackraised m (StackT tt m) -> WBackraised m (ApplyStack tt m)
forall a b. (a -> b) -> a -> b
$ forall (t :: TransKind) (m :: Type -> Type).
(MonadTransUnlift t, MonadTunnelIO 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 MonadTunnelIO t -> m r) -> t m r
unLiftWithUnlift :: forall m r. MonadIO m => (Unlift MonadTunnelIO 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 = Dict (MonadInner (TunnelIO m))
Dict (MonadInner (TunnelIO (ApplyStack tt m)))
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 -> Dict
  (MonadInner
     (ComposeInner (Tunnel a) (TunnelIO (ApplyStack lt1 m))))
Dict (MonadInner (TunnelIO (ApplyStack tt m)))
forall (a :: Constraint). a => Dict a
Dict

stackJoinUnlift ::
       ListType (Compose Dict MonadTransUnlift) tt
    -> Unlift MonadTunnelIO t
    -> Unlift MonadTunnelIO (StackT tt)
    -> Unlift MonadTunnelIO (StackT (t ': tt))
stackJoinUnlift :: forall (tt :: [TransKind]) (t :: TransKind).
ListType (Compose Dict MonadTransUnlift) tt
-> Unlift MonadTunnelIO t
-> Unlift MonadTunnelIO (StackT tt)
-> Unlift MonadTunnelIO (StackT (t : tt))
stackJoinUnlift ListType (Compose Dict MonadTransUnlift) tt
w Unlift MonadTunnelIO t
tmm Unlift MonadTunnelIO (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 @MonadTunnelIO @tt @m (ListType (Compose Dict (TransConstraint MonadTunnelIO)) tt
 -> Dict (MonadTunnelIO (ApplyStack tt m)))
-> ListType (Compose Dict (TransConstraint MonadTunnelIO)) tt
-> Dict (MonadTunnelIO (ApplyStack tt m))
forall a b. (a -> b) -> a -> b
$ (forall (t' :: TransKind).
 Compose Dict MonadTransUnlift t'
 -> Compose Dict (TransConstraint MonadTunnelIO) t')
-> ListType (Compose Dict MonadTransUnlift) tt
-> ListType (Compose Dict (TransConstraint MonadTunnelIO)) tt
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) -> Dict (TransConstraint MonadTunnelIO t')
-> Compose Dict (TransConstraint MonadTunnelIO) t'
forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose Dict (TransConstraint MonadTunnelIO t')
forall (a :: Constraint). a => Dict a
Dict) ListType (Compose Dict MonadTransUnlift) tt
w of
        Dict (MonadTunnelIO (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 -> StackT tt m a -> m a
StackT tt m --> m
Unlift MonadTunnelIO (StackT tt)
stmm (StackT tt m a -> m a) -> StackT tt m a -> m a
forall a b. (a -> b) -> a -> b
$ ApplyStack tt m a -> StackT tt m a
forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT (ApplyStack tt m a -> StackT tt m a)
-> ApplyStack tt m a -> StackT tt m a
forall a b. (a -> b) -> a -> b
$ t (ApplyStack tt m) a -> ApplyStack tt m a
t (ApplyStack tt m) --> ApplyStack tt m
Unlift MonadTunnelIO t
tmm (t (ApplyStack tt m) a -> ApplyStack tt m a)
-> t (ApplyStack tt m) a -> ApplyStack tt m a
forall a b. (a -> b) -> a -> b
$ StackT (t : tt) m a -> ApplyStack (t : tt) m a
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 MonadTunnelIO t)
unGetDiscardingUnlift :: forall m. Monad m => t m (WUnlift MonadTunnelIO t)
    }

instance MonadTransStackUnlift tt => MonadTransUnlift (StackT tt) where
    liftWithUnlift ::
           forall m r. MonadIO m
        => (Unlift MonadTunnelIO (StackT tt) -> m r)
        -> StackT tt m r
    liftWithUnlift :: forall (m :: Type -> Type) r.
MonadIO m =>
(Unlift MonadTunnelIO (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 (m :: Type -> Type) r.
 MonadIO m =>
 (Unlift MonadTunnelIO (StackT tt') -> m r) -> StackT tt' m r)
-> LiftWithUnlift (StackT tt')
forall (t :: TransKind).
(forall (m :: Type -> Type) r.
 MonadIO m =>
 (Unlift MonadTunnelIO t -> m r) -> t m r)
-> LiftWithUnlift t
MkLiftWithUnlift ((forall (m :: Type -> Type) r.
  MonadIO m =>
  (Unlift MonadTunnelIO (StackT tt') -> m r) -> StackT tt' m r)
 -> LiftWithUnlift (StackT tt'))
-> (forall (m :: Type -> Type) r.
    MonadIO m =>
    (Unlift MonadTunnelIO (StackT tt') -> m r) -> StackT tt' m r)
-> LiftWithUnlift (StackT tt')
forall a b. (a -> b) -> a -> b
$ \Unlift MonadTunnelIO (StackT tt') -> m r
call -> ApplyStack tt' m r -> StackT tt' m r
forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT (ApplyStack tt' m r -> StackT tt' m r)
-> ApplyStack tt' m r -> StackT tt' m r
forall a b. (a -> b) -> a -> b
$ Unlift MonadTunnelIO (StackT tt') -> m r
call StackT tt' m a -> m a
StackT tt' m a -> ApplyStack tt' m a
forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
Unlift MonadTunnelIO (StackT tt')
unStackT
        build (ConsListType (Compose Dict (MonadTransUnlift a)
Dict) (ListType (Compose Dict MonadTransUnlift) lt1
w :: ListType _ tt0)) =
            case ListType (Compose Dict MonadTransUnlift) lt1
-> LiftWithUnlift (StackT lt1)
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 MonadTunnelIO (StackT lt1) -> m r) -> StackT lt1 m r
liftWithUnlift' -> let
                    liftWithUnlift'' ::
                           forall m' r'. MonadIO m'
                        => (Unlift MonadTunnelIO (StackT tt') -> m' r')
                        -> StackT tt' m' r'
                    liftWithUnlift'' :: forall (m :: Type -> Type) r.
MonadIO m =>
(Unlift MonadTunnelIO (StackT tt') -> m r) -> StackT tt' m r
liftWithUnlift'' Unlift MonadTunnelIO (StackT tt') -> m' r'
call =
                        ApplyStack tt' m' r' -> StackT tt' m' r'
forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT (ApplyStack tt' m' r' -> StackT tt' m' r')
-> ApplyStack tt' m' r' -> StackT tt' m' r'
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' (ListType (Compose Dict (TransConstraint MonadIO)) lt1
 -> Dict (MonadIO (ApplyStack lt1 m')))
-> ListType (Compose Dict (TransConstraint MonadIO)) lt1
-> Dict (MonadIO (ApplyStack lt1 m'))
forall a b. (a -> b) -> a -> b
$ (forall (t' :: TransKind).
 Compose Dict MonadTransUnlift t'
 -> Compose Dict (TransConstraint MonadIO) t')
-> ListType (Compose Dict MonadTransUnlift) lt1
-> ListType (Compose Dict (TransConstraint MonadIO)) lt1
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) -> Dict (TransConstraint MonadIO t')
-> Compose Dict (TransConstraint MonadIO) t'
forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose Dict (TransConstraint MonadIO t')
forall (a :: Constraint). a => Dict a
Dict) ListType (Compose Dict MonadTransUnlift) lt1
w of
                            Dict (MonadIO (ApplyStack lt1 m'))
Dict ->
                                (Unlift MonadTunnelIO a -> ApplyStack lt1 m' r')
-> a (ApplyStack lt1 m') r'
forall (m :: Type -> Type) r.
MonadIO m =>
(Unlift MonadTunnelIO a -> m r) -> a m r
forall (t :: TransKind) (m :: Type -> Type) r.
(MonadTransUnlift t, MonadIO m) =>
(Unlift MonadTunnelIO t -> m r) -> t m r
liftWithUnlift ((Unlift MonadTunnelIO a -> ApplyStack lt1 m' r')
 -> a (ApplyStack lt1 m') r')
-> (Unlift MonadTunnelIO a -> ApplyStack lt1 m' r')
-> a (ApplyStack lt1 m') r'
forall a b. (a -> b) -> a -> b
$ \Unlift MonadTunnelIO a
unlift1 ->
                                    StackT lt1 m' r' -> ApplyStack lt1 m' r'
forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT (StackT lt1 m' r' -> ApplyStack lt1 m' r')
-> StackT lt1 m' r' -> ApplyStack lt1 m' r'
forall a b. (a -> b) -> a -> b
$ (Unlift MonadTunnelIO (StackT lt1) -> m' r') -> StackT lt1 m' r'
forall (m :: Type -> Type) r.
MonadIO m =>
(Unlift MonadTunnelIO (StackT lt1) -> m r) -> StackT lt1 m r
liftWithUnlift' ((Unlift MonadTunnelIO (StackT lt1) -> m' r') -> StackT lt1 m' r')
-> (Unlift MonadTunnelIO (StackT lt1) -> m' r') -> StackT lt1 m' r'
forall a b. (a -> b) -> a -> b
$ \Unlift MonadTunnelIO (StackT lt1)
unlift2 -> Unlift MonadTunnelIO (StackT tt') -> m' r'
call (Unlift MonadTunnelIO (StackT tt') -> m' r')
-> Unlift MonadTunnelIO (StackT tt') -> m' r'
forall a b. (a -> b) -> a -> b
$ ListType (Compose Dict MonadTransUnlift) lt1
-> Unlift MonadTunnelIO a
-> Unlift MonadTunnelIO (StackT lt1)
-> Unlift MonadTunnelIO (StackT (a : lt1))
forall (tt :: [TransKind]) (t :: TransKind).
ListType (Compose Dict MonadTransUnlift) tt
-> Unlift MonadTunnelIO t
-> Unlift MonadTunnelIO (StackT tt)
-> Unlift MonadTunnelIO (StackT (t : tt))
stackJoinUnlift ListType (Compose Dict MonadTransUnlift) lt1
w a m a -> m a
a m --> m
Unlift MonadTunnelIO a
unlift1 StackT lt1 m a -> m a
StackT lt1 m --> m
Unlift MonadTunnelIO (StackT lt1)
unlift2
                    in (forall (m :: Type -> Type) r.
 MonadIO m =>
 (Unlift MonadTunnelIO (StackT tt') -> m r) -> StackT tt' m r)
-> LiftWithUnlift (StackT tt')
forall (t :: TransKind).
(forall (m :: Type -> Type) r.
 MonadIO m =>
 (Unlift MonadTunnelIO t -> m r) -> t m r)
-> LiftWithUnlift t
MkLiftWithUnlift (Unlift MonadTunnelIO (StackT tt') -> m r) -> StackT tt' m r
forall (m :: Type -> Type) r.
MonadIO m =>
(Unlift MonadTunnelIO (StackT tt') -> m r) -> StackT tt' m r
liftWithUnlift''
        in LiftWithUnlift (StackT tt)
-> forall (m :: Type -> Type) r.
   MonadIO m =>
   (Unlift MonadTunnelIO (StackT tt) -> m r) -> StackT tt m r
forall (t :: TransKind).
LiftWithUnlift t
-> forall (m :: Type -> Type) r.
   MonadIO m =>
   (Unlift MonadTunnelIO t -> m r) -> t m r
unLiftWithUnlift (LiftWithUnlift (StackT tt)
 -> forall (m :: Type -> Type) r.
    MonadIO m =>
    (Unlift MonadTunnelIO (StackT tt) -> m r) -> StackT tt m r)
-> LiftWithUnlift (StackT tt)
-> forall (m :: Type -> Type) r.
   MonadIO m =>
   (Unlift MonadTunnelIO (StackT tt) -> m r) -> StackT tt m r
forall a b. (a -> b) -> a -> b
$ ListType (Compose Dict MonadTransUnlift) tt
-> LiftWithUnlift (StackT tt)
forall (tt' :: [TransKind]).
ListType (Compose Dict MonadTransUnlift) tt'
-> LiftWithUnlift (StackT tt')
build (ListType (Compose Dict MonadTransUnlift) tt
 -> LiftWithUnlift (StackT tt))
-> ListType (Compose Dict MonadTransUnlift) tt
-> LiftWithUnlift (StackT tt)
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 MonadTunnelIO (StackT tt))
    getDiscardingUnlift :: forall (m :: Type -> Type).
Monad m =>
StackT tt m (WUnlift MonadTunnelIO (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 (m :: Type -> Type).
 Monad m =>
 StackT tt' m (WUnlift MonadTunnelIO (StackT tt')))
-> GetDiscardingUnlift (StackT tt')
forall (t :: TransKind).
(forall (m :: Type -> Type).
 Monad m =>
 t m (WUnlift MonadTunnelIO t))
-> GetDiscardingUnlift t
MkGetDiscardingUnlift ((forall (m :: Type -> Type).
  Monad m =>
  StackT tt' m (WUnlift MonadTunnelIO (StackT tt')))
 -> GetDiscardingUnlift (StackT tt'))
-> (forall (m :: Type -> Type).
    Monad m =>
    StackT tt' m (WUnlift MonadTunnelIO (StackT tt')))
-> GetDiscardingUnlift (StackT tt')
forall a b. (a -> b) -> a -> b
$ ApplyStack tt' m (WUnlift MonadTunnelIO (StackT tt'))
-> StackT tt' m (WUnlift MonadTunnelIO (StackT tt'))
forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT (ApplyStack tt' m (WUnlift MonadTunnelIO (StackT tt'))
 -> StackT tt' m (WUnlift MonadTunnelIO (StackT tt')))
-> ApplyStack tt' m (WUnlift MonadTunnelIO (StackT tt'))
-> StackT tt' m (WUnlift MonadTunnelIO (StackT tt'))
forall a b. (a -> b) -> a -> b
$ WUnlift MonadTunnelIO (StackT tt')
-> ApplyStack tt' m (WUnlift MonadTunnelIO (StackT tt'))
forall a. a -> ApplyStack tt' m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (WUnlift MonadTunnelIO (StackT tt')
 -> ApplyStack tt' m (WUnlift MonadTunnelIO (StackT tt')))
-> WUnlift MonadTunnelIO (StackT tt')
-> ApplyStack tt' m (WUnlift MonadTunnelIO (StackT tt'))
forall a b. (a -> b) -> a -> b
$ Unlift MonadTunnelIO (StackT tt')
-> WUnlift MonadTunnelIO (StackT tt')
forall (c :: (Type -> Type) -> Constraint) (t :: TransKind).
Unlift c t -> WUnlift c t
MkWUnlift StackT tt' m a -> m a
StackT tt' m a -> ApplyStack tt' m a
forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
Unlift MonadTunnelIO (StackT tt')
unStackT
        build (ConsListType (Compose (Dict (MonadTransUnlift a)
Dict :: Dict (MonadTransUnlift t))) (ListType (Compose Dict MonadTransUnlift) lt1
w :: ListType _ tt0)) =
            case ListType (Compose Dict MonadTransUnlift) lt1
-> GetDiscardingUnlift (StackT lt1)
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 MonadTunnelIO (StackT lt1))
getDiscardingUnlift' -> let
                    getDiscardingUnlift'' ::
                           forall m'. Monad m'
                        => StackT tt' m' (WUnlift MonadTunnelIO (StackT tt'))
                    getDiscardingUnlift'' :: forall (m :: Type -> Type).
Monad m =>
StackT tt' m (WUnlift MonadTunnelIO (StackT tt'))
getDiscardingUnlift'' =
                        ApplyStack tt' m' (WUnlift MonadTunnelIO (StackT tt'))
-> StackT tt' m' (WUnlift MonadTunnelIO (StackT tt'))
forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT (ApplyStack tt' m' (WUnlift MonadTunnelIO (StackT tt'))
 -> StackT tt' m' (WUnlift MonadTunnelIO (StackT tt')))
-> ApplyStack tt' m' (WUnlift MonadTunnelIO (StackT tt'))
-> StackT tt' m' (WUnlift MonadTunnelIO (StackT tt'))
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' (ListType (Compose Dict (TransConstraint Monad)) lt1
 -> Dict (Monad (ApplyStack lt1 m')))
-> ListType (Compose Dict (TransConstraint Monad)) lt1
-> Dict (Monad (ApplyStack lt1 m'))
forall a b. (a -> b) -> a -> b
$ (forall (t' :: TransKind).
 Compose Dict MonadTransUnlift t'
 -> Compose Dict (TransConstraint Monad) t')
-> ListType (Compose Dict MonadTransUnlift) lt1
-> ListType (Compose Dict (TransConstraint Monad)) lt1
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) -> Dict (TransConstraint Monad t')
-> Compose Dict (TransConstraint Monad) t'
forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose Dict (TransConstraint Monad t')
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 ((Monad (a (ApplyStack lt1 m')) =>
  a (ApplyStack lt1 m') (WUnlift MonadTunnelIO (StackT tt')))
 -> a (ApplyStack lt1 m') (WUnlift MonadTunnelIO (StackT tt')))
-> (Monad (a (ApplyStack lt1 m')) =>
    a (ApplyStack lt1 m') (WUnlift MonadTunnelIO (StackT tt')))
-> a (ApplyStack lt1 m') (WUnlift MonadTunnelIO (StackT tt'))
forall a b. (a -> b) -> a -> b
$ do
                                    MkWUnlift Unlift MonadTunnelIO a
unlift1 <- a (ApplyStack lt1 m') (WUnlift MonadTunnelIO a)
forall (m :: Type -> Type).
Monad m =>
a m (WUnlift MonadTunnelIO a)
forall (t :: TransKind) (m :: Type -> Type).
(MonadTransUnlift t, Monad m) =>
t m (WUnlift MonadTunnelIO t)
getDiscardingUnlift
                                    MkWUnlift Unlift MonadTunnelIO (StackT lt1)
unlift2 <- ApplyStack lt1 m' (WUnlift MonadTunnelIO (StackT lt1))
-> a (ApplyStack lt1 m') (WUnlift MonadTunnelIO (StackT lt1))
forall (m :: Type -> Type) a. Monad m => m a -> a m a
forall (t :: TransKind) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ApplyStack lt1 m' (WUnlift MonadTunnelIO (StackT lt1))
 -> a (ApplyStack lt1 m') (WUnlift MonadTunnelIO (StackT lt1)))
-> ApplyStack lt1 m' (WUnlift MonadTunnelIO (StackT lt1))
-> a (ApplyStack lt1 m') (WUnlift MonadTunnelIO (StackT lt1))
forall a b. (a -> b) -> a -> b
$ StackT lt1 m' (WUnlift MonadTunnelIO (StackT lt1))
-> ApplyStack lt1 m' (WUnlift MonadTunnelIO (StackT lt1))
forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT (StackT lt1 m' (WUnlift MonadTunnelIO (StackT lt1))
 -> ApplyStack lt1 m' (WUnlift MonadTunnelIO (StackT lt1)))
-> StackT lt1 m' (WUnlift MonadTunnelIO (StackT lt1))
-> ApplyStack lt1 m' (WUnlift MonadTunnelIO (StackT lt1))
forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type).
Monad m =>
StackT lt1 m (WUnlift MonadTunnelIO (StackT lt1))
getDiscardingUnlift' @m'
                                    WUnlift MonadTunnelIO (StackT tt')
-> a (ApplyStack lt1 m') (WUnlift MonadTunnelIO (StackT tt'))
forall a. a -> a (ApplyStack lt1 m') a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (WUnlift MonadTunnelIO (StackT tt')
 -> a (ApplyStack lt1 m') (WUnlift MonadTunnelIO (StackT tt')))
-> WUnlift MonadTunnelIO (StackT tt')
-> a (ApplyStack lt1 m') (WUnlift MonadTunnelIO (StackT tt'))
forall a b. (a -> b) -> a -> b
$ Unlift MonadTunnelIO (StackT tt')
-> WUnlift MonadTunnelIO (StackT tt')
forall (c :: (Type -> Type) -> Constraint) (t :: TransKind).
Unlift c t -> WUnlift c t
MkWUnlift (Unlift MonadTunnelIO (StackT tt')
 -> WUnlift MonadTunnelIO (StackT tt'))
-> Unlift MonadTunnelIO (StackT tt')
-> WUnlift MonadTunnelIO (StackT tt')
forall a b. (a -> b) -> a -> b
$ ListType (Compose Dict MonadTransUnlift) lt1
-> Unlift MonadTunnelIO a
-> Unlift MonadTunnelIO (StackT lt1)
-> Unlift MonadTunnelIO (StackT (a : lt1))
forall (tt :: [TransKind]) (t :: TransKind).
ListType (Compose Dict MonadTransUnlift) tt
-> Unlift MonadTunnelIO t
-> Unlift MonadTunnelIO (StackT tt)
-> Unlift MonadTunnelIO (StackT (t : tt))
stackJoinUnlift ListType (Compose Dict MonadTransUnlift) lt1
w a m a -> m a
a m --> m
Unlift MonadTunnelIO a
unlift1 StackT lt1 m a -> m a
StackT lt1 m --> m
Unlift MonadTunnelIO (StackT lt1)
unlift2
                    in (forall (m :: Type -> Type).
 Monad m =>
 StackT tt' m (WUnlift MonadTunnelIO (StackT tt')))
-> GetDiscardingUnlift (StackT tt')
forall (t :: TransKind).
(forall (m :: Type -> Type).
 Monad m =>
 t m (WUnlift MonadTunnelIO t))
-> GetDiscardingUnlift t
MkGetDiscardingUnlift StackT tt' m (WUnlift MonadTunnelIO (StackT tt'))
forall (m :: Type -> Type).
Monad m =>
StackT tt' m (WUnlift MonadTunnelIO (StackT tt'))
getDiscardingUnlift''
        in GetDiscardingUnlift (StackT tt)
-> forall (m :: Type -> Type).
   Monad m =>
   StackT tt m (WUnlift MonadTunnelIO (StackT tt))
forall (t :: TransKind).
GetDiscardingUnlift t
-> forall (m :: Type -> Type).
   Monad m =>
   t m (WUnlift MonadTunnelIO t)
unGetDiscardingUnlift (GetDiscardingUnlift (StackT tt)
 -> forall (m :: Type -> Type).
    Monad m =>
    StackT tt m (WUnlift MonadTunnelIO (StackT tt)))
-> GetDiscardingUnlift (StackT tt)
-> forall (m :: Type -> Type).
   Monad m =>
   StackT tt m (WUnlift MonadTunnelIO (StackT tt))
forall a b. (a -> b) -> a -> b
$ ListType (Compose Dict MonadTransUnlift) tt
-> GetDiscardingUnlift (StackT tt)
forall (tt' :: [TransKind]).
ListType (Compose Dict MonadTransUnlift) tt'
-> GetDiscardingUnlift (StackT tt')
build (ListType (Compose Dict MonadTransUnlift) tt
 -> GetDiscardingUnlift (StackT tt))
-> ListType (Compose Dict MonadTransUnlift) tt
-> GetDiscardingUnlift (StackT tt)
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 ((m --> ApplyStack tt2 m)
 -> ApplyStack tt1 m --> ApplyStack tt1 (ApplyStack tt2 m))
-> (m --> ApplyStack tt2 m)
-> ApplyStack tt1 m --> ApplyStack tt1 (ApplyStack tt2 m)
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 = ApplyStack tta (StackT ttb m) r -> StackT tta (StackT ttb m) r
forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT (ApplyStack tta (StackT ttb m) r -> StackT tta (StackT ttb m) r)
-> ApplyStack tta (StackT ttb m) r -> StackT tta (StackT ttb m) r
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) ApplyStack ttb m a -> StackT ttb m a
forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
ApplyStack ttb m --> StackT ttb m
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) StackT tta m a -> ApplyStack tta m a
forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
StackT tta m --> ApplyStack tta m
unStackT (ApplyStack ttb (StackT tta m) r
 -> ApplyStack ttb (ApplyStack tta m) r)
-> ApplyStack ttb (StackT tta m) r
-> ApplyStack ttb (ApplyStack tta m) r
forall a b. (a -> b) -> a -> b
$ StackT ttb (StackT tta m) r -> ApplyStack ttb (StackT tta m) r
forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT (StackT ttb (StackT tta m) r -> ApplyStack ttb (StackT tta m) r)
-> StackT ttb (StackT tta m) r -> ApplyStack ttb (StackT tta m) r
forall a b. (a -> b) -> a -> b
$ StackT tta (StackT ttb m) r -> StackT ttb (StackT tta m) r
StackT tta (StackT ttb m) --> StackT ttb (StackT tta m)
forall (ta :: TransKind) (tb :: TransKind) (m :: Type -> Type).
(MonadTransTunnel ta, MonadTransTunnel 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 -> ApplyStack tt m a -> m a
ApplyStack tt m --> m
StackUnlift tt
unliftr (ApplyStack tt m a -> m a)
-> (t (ApplyStack tt m) a -> ApplyStack tt m a)
-> t (ApplyStack tt m) a
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. t (ApplyStack tt m) a -> ApplyStack tt m a
t (ApplyStack tt m) --> ApplyStack tt m
Unlift MonadUnliftIO t
unlift1
    in StackUnlift (t : tt) -> WStackUnlift (t : tt)
forall (tt :: [TransKind]). StackUnlift tt -> WStackUnlift tt
MkWStackUnlift t (ApplyStack tt m) a -> m a
ApplyStack (t : tt) m a -> m a
t (ApplyStack tt m) --> m
forall (m :: Type -> Type).
MonadUnliftIO m =>
t (ApplyStack tt m) --> m
StackUnlift (t : tt)
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 (StackT tt m r -> ApplyStack tt m r)
-> StackT tt m r -> ApplyStack tt m r
forall a b. (a -> b) -> a -> b
$ (Unlift MonadTunnelIO (StackT tt) -> m r) -> StackT tt m r
forall (m :: Type -> Type) r.
MonadIO m =>
(Unlift MonadTunnelIO (StackT tt) -> m r) -> StackT tt m r
forall (t :: TransKind) (m :: Type -> Type) r.
(MonadTransUnlift t, MonadIO m) =>
(Unlift MonadTunnelIO t -> m r) -> t m r
liftWithUnlift ((Unlift MonadTunnelIO (StackT tt) -> m r) -> StackT tt m r)
-> (Unlift MonadTunnelIO (StackT tt) -> m r) -> StackT tt m r
forall a b. (a -> b) -> a -> b
$ \Unlift MonadTunnelIO (StackT tt)
unlift -> StackUnlift tt -> m r
call (StackUnlift tt -> m r) -> StackUnlift tt -> m r
forall a b. (a -> b) -> a -> b
$ \ApplyStack tt m a
astm -> StackT tt m a -> m a
StackT tt m --> m
Unlift MonadTunnelIO (StackT tt)
unlift (StackT tt m a -> m a) -> StackT tt m a -> m a
forall a b. (a -> b) -> a -> b
$ ApplyStack tt m a -> StackT tt m a
forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT ApplyStack tt m a
astm