module Control.Monad.Ology.Specific.StackT
( witTransStackDict
, IsStack
, transStackDict
, StackT(..)
, stackLift
, stackHoist
, WithTunnelConstraint
, MonadTransStackTunnel
, transStackExcept
, stackUnderliftIO
, stackBackHoist
, MonadTransStackUnlift
, concatMonadTransStackUnliftDict
, stackLiftWithUnlift
, stackConcatFst
, stackConcatSnd
, stackCommute
, transStackConcatRefl
, StackUnlift
, WStackUnlift(..)
, consWStackUnlift
, stackLiftWithStackUnlift
) where
import Control.Monad.Ology.General
import Control.Monad.Ology.Specific.ComposeInner
import Control.Monad.Ology.Specific.ExceptT
import Import
witTransStackDict ::
forall cm tt m. (cm m)
=> ListType (Compose Dict (TransConstraint cm)) tt
-> Dict (cm (ApplyStack tt m))
witTransStackDict :: forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
(m :: Type -> Type).
cm m =>
ListType (Compose Dict (TransConstraint cm)) tt
-> Dict (cm (ApplyStack tt m))
witTransStackDict ListType (Compose Dict (TransConstraint cm)) tt
NilListType = forall (a :: Constraint). a => Dict a
Dict
witTransStackDict (ConsListType (Compose Dict (TransConstraint cm a)
Dict) ListType (Compose Dict (TransConstraint cm)) lt1
lt) =
case forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
(m :: Type -> Type).
cm m =>
ListType (Compose Dict (TransConstraint cm)) tt
-> Dict (cm (ApplyStack tt m))
witTransStackDict @cm @_ @m ListType (Compose Dict (TransConstraint cm)) lt1
lt of
Dict (cm (ApplyStack lt1 m))
d -> forall (c :: (Type -> Type) -> Constraint) (t :: TransKind)
(m :: Type -> Type).
TransConstraint c t =>
Dict (c m) -> Dict (c (t m))
transConstraintDict @cm Dict (cm (ApplyStack lt1 m))
d
type IsStack :: (TransKind -> Constraint) -> [TransKind] -> Constraint
type IsStack ct = Is (ListType (Compose Dict ct))
transStackDict ::
forall cm tt m. (IsStack (TransConstraint cm) tt, cm m)
=> Dict (cm (ApplyStack tt m))
transStackDict :: forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
(m :: Type -> Type).
(IsStack (TransConstraint cm) tt, cm m) =>
Dict (cm (ApplyStack tt m))
transStackDict = forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
(m :: Type -> Type).
cm m =>
ListType (Compose Dict (TransConstraint cm)) tt
-> Dict (cm (ApplyStack tt m))
witTransStackDict @cm @tt @m forall a b. (a -> b) -> a -> b
$ forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative @_ @(ListType (Compose Dict (TransConstraint cm))) @tt
type StackT :: [TransKind] -> TransKind
newtype StackT (tt :: [TransKind]) m a = MkStackT
{ forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT :: ApplyStack tt m a
}
instance (IsStack (TransConstraint Monad) tt, Monad m) => Functor (StackT tt m) where
fmap :: forall a b. (a -> b) -> StackT tt m a -> StackT tt m b
fmap =
case forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
(m :: Type -> Type).
(IsStack (TransConstraint cm) tt, cm m) =>
Dict (cm (ApplyStack tt m))
transStackDict @Monad @tt @m of
Dict (Monad (ApplyStack tt m))
Dict -> \a -> b
ab (MkStackT ApplyStack tt m a
ma) -> forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
ab ApplyStack tt m a
ma
instance (IsStack (TransConstraint Monad) tt, Monad m) => Applicative (StackT tt m) where
pure :: forall a. a -> StackT tt m a
pure =
case forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
(m :: Type -> Type).
(IsStack (TransConstraint cm) tt, cm m) =>
Dict (cm (ApplyStack tt m))
transStackDict @Monad @tt @m of
Dict (Monad (ApplyStack tt m))
Dict -> \a
a -> forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a. Applicative f => a -> f a
pure a
a
<*> :: forall a b. StackT tt m (a -> b) -> StackT tt m a -> StackT tt m b
(<*>) =
case forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
(m :: Type -> Type).
(IsStack (TransConstraint cm) tt, cm m) =>
Dict (cm (ApplyStack tt m))
transStackDict @Monad @tt @m of
Dict (Monad (ApplyStack tt m))
Dict -> \(MkStackT ApplyStack tt m (a -> b)
mab) (MkStackT ApplyStack tt m a
ma) -> forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall a b. (a -> b) -> a -> b
$ ApplyStack tt m (a -> b)
mab forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> ApplyStack tt m a
ma
instance (IsStack (TransConstraint Monad) tt, Monad m) => Monad (StackT tt m) where
return :: forall a. a -> StackT tt m a
return = forall (f :: Type -> Type) a. Applicative f => a -> f a
pure
>>= :: forall a b. StackT tt m a -> (a -> StackT tt m b) -> StackT tt m b
(>>=) =
case forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
(m :: Type -> Type).
(IsStack (TransConstraint cm) tt, cm m) =>
Dict (cm (ApplyStack tt m))
transStackDict @Monad @tt @m of
Dict (Monad (ApplyStack tt m))
Dict -> \(MkStackT ApplyStack tt m a
ma) a -> StackT tt m b
amb -> forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall a b. (a -> b) -> a -> b
$ ApplyStack tt m a
ma forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
a -> forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT forall a b. (a -> b) -> a -> b
$ a -> StackT tt m b
amb a
a
instance (IsStack (TransConstraint Monad) tt) => TransConstraint Monad (StackT tt) where
hasTransConstraint :: forall (m :: Type -> Type). Monad m => Dict (Monad (StackT tt m))
hasTransConstraint = forall (a :: Constraint). a => Dict a
Dict
instance (IsStack (TransConstraint Monad) tt, IsStack MonadTrans tt, MonadFail m) => MonadFail (StackT tt m) where
fail :: forall a. String -> StackT tt m a
fail String
s = forall (t :: TransKind) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
s
instance (IsStack (TransConstraint Monad) tt, IsStack (TransConstraint MonadFail) tt, IsStack MonadTrans tt) =>
TransConstraint MonadFail (StackT tt) where
hasTransConstraint :: forall (m :: Type -> Type).
MonadFail m =>
Dict (MonadFail (StackT tt m))
hasTransConstraint = forall (a :: Constraint). a => Dict a
Dict
instance (IsStack (TransConstraint Monad) tt, IsStack (TransConstraint MonadFix) tt, MonadFix m) =>
MonadFix (StackT tt m) where
mfix :: forall a. (a -> StackT tt m a) -> StackT tt m a
mfix :: forall a. (a -> StackT tt m a) -> StackT tt m a
mfix =
case forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
(m :: Type -> Type).
(IsStack (TransConstraint cm) tt, cm m) =>
Dict (cm (ApplyStack tt m))
transStackDict @MonadFix @tt @m of
Dict (MonadFix (ApplyStack tt m))
Dict -> \a -> StackT tt m a
f -> forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type) a. MonadFix m => (a -> m a) -> m a
mfix forall a b. (a -> b) -> a -> b
$ \a
a -> forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT forall a b. (a -> b) -> a -> b
$ a -> StackT tt m a
f a
a
instance (IsStack (TransConstraint Monad) tt, IsStack (TransConstraint MonadFix) tt) =>
TransConstraint MonadFix (StackT tt) where
hasTransConstraint :: forall (m :: Type -> Type).
MonadFix m =>
Dict (MonadFix (StackT tt m))
hasTransConstraint = forall (a :: Constraint). a => Dict a
Dict
instance (IsStack (TransConstraint Monad) tt, IsStack (TransConstraint MonadIO) tt, MonadIO m) => MonadIO (StackT tt m) where
liftIO :: forall a. IO a -> StackT tt m a
liftIO =
case forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
(m :: Type -> Type).
(IsStack (TransConstraint cm) tt, cm m) =>
Dict (cm (ApplyStack tt m))
transStackDict @MonadIO @tt @m of
Dict (MonadIO (ApplyStack tt m))
Dict -> \IO a
ioa -> forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO IO a
ioa
instance (IsStack (TransConstraint Monad) tt, IsStack (TransConstraint MonadIO) tt) =>
TransConstraint MonadIO (StackT tt) where
hasTransConstraint :: forall (m :: Type -> Type).
MonadIO m =>
Dict (MonadIO (StackT tt m))
hasTransConstraint = forall (a :: Constraint). a => Dict a
Dict
instance (IsStack (TransConstraint Monad) tt, IsStack (TransConstraint MonadPlus) tt, MonadPlus m) =>
Alternative (StackT tt m) where
empty :: forall a. StackT tt m a
empty =
case forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
(m :: Type -> Type).
(IsStack (TransConstraint cm) tt, cm m) =>
Dict (cm (ApplyStack tt m))
transStackDict @MonadPlus @tt @m of
Dict (MonadPlus (ApplyStack tt m))
Dict -> forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall (f :: Type -> Type) a. Alternative f => f a
empty
<|> :: forall a. StackT tt m a -> StackT tt m a -> StackT tt m a
(<|>) =
case forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
(m :: Type -> Type).
(IsStack (TransConstraint cm) tt, cm m) =>
Dict (cm (ApplyStack tt m))
transStackDict @MonadPlus @tt @m of
Dict (MonadPlus (ApplyStack tt m))
Dict -> \(MkStackT ApplyStack tt m a
a) (MkStackT ApplyStack tt m a
b) -> forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall a b. (a -> b) -> a -> b
$ ApplyStack tt m a
a forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> ApplyStack tt m a
b
instance (IsStack (TransConstraint Monad) tt, IsStack (TransConstraint MonadPlus) tt, MonadPlus m) =>
MonadPlus (StackT tt m)
instance (IsStack (TransConstraint Monad) tt, IsStack (TransConstraint MonadPlus) tt) =>
TransConstraint MonadPlus (StackT tt) where
hasTransConstraint :: forall (m :: Type -> Type).
MonadPlus m =>
Dict (MonadPlus (StackT tt m))
hasTransConstraint = forall (a :: Constraint). a => Dict a
Dict
instance (IsStack (TransConstraint Monad) tt, IsStack MonadTrans tt) => MonadTrans (StackT tt) where
lift ::
forall m a. Monad m
=> m a
-> StackT tt m a
lift :: forall (m :: Type -> Type) a. Monad m => m a -> StackT tt m a
lift = let
build ::
forall tt'.
ListType (Compose Dict (TransConstraint Monad)) tt'
-> ListType (Compose Dict MonadTrans) tt'
-> (WRaised m (ApplyStack tt' m), Dict (Monad (ApplyStack tt' m)))
build :: forall (tt' :: [TransKind]).
ListType (Compose Dict (TransConstraint Monad)) tt'
-> ListType (Compose Dict MonadTrans) tt'
-> (WRaised m (ApplyStack tt' m), Dict (Monad (ApplyStack tt' m)))
build ListType (Compose Dict (TransConstraint Monad)) tt'
NilListType ListType (Compose Dict MonadTrans) tt'
NilListType = (forall {k} (cat :: k -> k -> Type) (a :: k).
Category cat =>
cat a a
id, forall (a :: Constraint). a => Dict a
Dict)
build (ConsListType (Compose Dict (TransConstraint Monad a)
Dict) ListType (Compose Dict (TransConstraint Monad)) lt1
wa) (ConsListType (Compose Dict (MonadTrans a)
Dict) ListType (Compose Dict MonadTrans) lt1
wb) =
case forall (tt' :: [TransKind]).
ListType (Compose Dict (TransConstraint Monad)) tt'
-> ListType (Compose Dict MonadTrans) tt'
-> (WRaised m (ApplyStack tt' m), Dict (Monad (ApplyStack tt' m)))
build ListType (Compose Dict (TransConstraint Monad)) lt1
wa ListType (Compose Dict MonadTrans) lt1
wb of
(WRaised m (ApplyStack lt1 m)
wmf, dcm :: Dict (Monad (ApplyStack lt1 m))
dcm@Dict (Monad (ApplyStack lt1 m))
Dict) -> (forall (t :: TransKind) (m :: Type -> Type).
(MonadTrans t, Monad m) =>
WRaised m (t m)
wLift forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. WRaised m (ApplyStack lt1 m)
wmf, forall (c :: (Type -> Type) -> Constraint) (t :: TransKind)
(m :: Type -> Type).
TransConstraint c t =>
Dict (c m) -> Dict (c (t m))
transConstraintDict @Monad Dict (Monad (ApplyStack lt1 m))
dcm)
in let
wa :: ListType (Compose Dict (TransConstraint Monad)) tt
wa = forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative @_ @(ListType (Compose Dict (TransConstraint Monad))) @tt
wb :: ListType (Compose Dict MonadTrans) tt
wb = forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative @_ @(ListType (Compose Dict MonadTrans)) @tt
in case forall (tt' :: [TransKind]).
ListType (Compose Dict (TransConstraint Monad)) tt'
-> ListType (Compose Dict MonadTrans) tt'
-> (WRaised m (ApplyStack tt' m), Dict (Monad (ApplyStack tt' m)))
build ListType (Compose Dict (TransConstraint Monad)) tt
wa ListType (Compose Dict MonadTrans) tt
wb of
(WRaised m (ApplyStack tt m)
wmf, Dict (Monad (ApplyStack tt m))
_) -> \m a
ma -> forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall a b. (a -> b) -> a -> b
$ forall k (p :: k -> Type) (q :: k -> Type). WRaised p q -> p --> q
unWRaised WRaised m (ApplyStack tt m)
wmf m a
ma
stackLift ::
forall tt m. (IsStack (TransConstraint Monad) tt, IsStack MonadTrans tt, Monad m)
=> m --> ApplyStack tt m
stackLift :: forall (tt :: [TransKind]) (m :: Type -> Type).
(IsStack (TransConstraint Monad) tt, IsStack MonadTrans tt,
Monad m) =>
m --> ApplyStack tt m
stackLift m a
ma = forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT @tt @m forall a b. (a -> b) -> a -> b
$ forall (t :: TransKind) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m a
ma
type MonadTransStackTunnel tt
= ( IsStack (TransConstraint Monad) tt
, IsStack MonadTransTunnel tt
, IsStack MonadTrans tt
, IsStack (WithTunnelConstraint Functor) tt
, IsStack (WithTunnelConstraint Applicative) tt
, IsStack (WithTunnelConstraint Monad) tt
, IsStack (WithTunnelConstraint Traversable) tt
, IsStack (WithTunnelConstraint MonadInner) tt)
concatMonadTransStackTunnelDict ::
forall tt1 tt2. (MonadTransStackTunnel tt1, MonadTransStackTunnel tt2)
=> Dict (MonadTransStackTunnel (Concat tt1 tt2))
concatMonadTransStackTunnelDict :: forall (tt1 :: [TransKind]) (tt2 :: [TransKind]).
(MonadTransStackTunnel tt1, MonadTransStackTunnel tt2) =>
Dict (MonadTransStackTunnel (Concat tt1 tt2))
concatMonadTransStackTunnelDict =
forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]) r.
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
(Is (ListType w) (Concat aa bb) => r) -> r
withConcatIs @_ @(Compose Dict (TransConstraint Monad)) @tt1 @tt2 forall a b. (a -> b) -> a -> b
$
forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]) r.
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
(Is (ListType w) (Concat aa bb) => r) -> r
withConcatIs @_ @(Compose Dict MonadTransTunnel) @tt1 @tt2 forall a b. (a -> b) -> a -> b
$
forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]) r.
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
(Is (ListType w) (Concat aa bb) => r) -> r
withConcatIs @_ @(Compose Dict MonadTrans) @tt1 @tt2 forall a b. (a -> b) -> a -> b
$
forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]) r.
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
(Is (ListType w) (Concat aa bb) => r) -> r
withConcatIs @_ @(Compose Dict (WithTunnelConstraint Functor)) @tt1 @tt2 forall a b. (a -> b) -> a -> b
$
forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]) r.
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
(Is (ListType w) (Concat aa bb) => r) -> r
withConcatIs @_ @(Compose Dict (WithTunnelConstraint Applicative)) @tt1 @tt2 forall a b. (a -> b) -> a -> b
$
forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]) r.
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
(Is (ListType w) (Concat aa bb) => r) -> r
withConcatIs @_ @(Compose Dict (WithTunnelConstraint Monad)) @tt1 @tt2 forall a b. (a -> b) -> a -> b
$
forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]) r.
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
(Is (ListType w) (Concat aa bb) => r) -> r
withConcatIs @_ @(Compose Dict (WithTunnelConstraint Traversable)) @tt1 @tt2 forall a b. (a -> b) -> a -> b
$
forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]) r.
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
(Is (ListType w) (Concat aa bb) => r) -> r
withConcatIs @_ @(Compose Dict (WithTunnelConstraint MonadInner)) @tt1 @tt2 forall a b. (a -> b) -> a -> b
$ forall (a :: Constraint). a => Dict a
Dict
newtype TunnelWrapper t = MkTunnel
{ forall (t :: TransKind).
TunnelWrapper t
-> forall (m2 :: Type -> Type) r.
Monad m2 =>
((forall (m1 :: Type -> Type) a.
Monad m1 =>
t m1 a -> m1 (Tunnel t a))
-> m2 (Tunnel t r))
-> t m2 r
unTunnel :: forall m2 r.
Monad m2 => ((forall m1 a. Monad m1 => t m1 a -> m1 (Tunnel t a)) -> m2 (Tunnel t r)) -> t m2 r
}
type WithTunnelConstraint :: ((Type -> Type) -> Constraint) -> TransKind -> Constraint
class (MonadTransTunnel t, c (Tunnel t)) => WithTunnelConstraint c t
instance (MonadTransTunnel t, c (Tunnel t)) => WithTunnelConstraint c t
type ApplyStackTunnel :: [TransKind] -> Type -> Type
type family ApplyStackTunnel tt where
ApplyStackTunnel '[] = Identity
ApplyStackTunnel (t ': tt) = ComposeInner (Tunnel t) (ApplyStackTunnel tt)
astIsWithTunnelConstraint ::
forall (c :: (Type -> Type) -> Constraint) (tt :: [TransKind]).
(c Identity, forall f1 f2. (c f1, c f2) => c (ComposeInner f1 f2))
=> ListType (Compose Dict (WithTunnelConstraint c)) tt
-> Dict (c (ApplyStackTunnel tt))
astIsWithTunnelConstraint :: forall (c :: (Type -> Type) -> Constraint) (tt :: [TransKind]).
(c Identity,
forall (f1 :: Type -> Type) (f2 :: Type -> Type).
(c f1, c f2) =>
c (ComposeInner f1 f2)) =>
ListType (Compose Dict (WithTunnelConstraint c)) tt
-> Dict (c (ApplyStackTunnel tt))
astIsWithTunnelConstraint ListType (Compose Dict (WithTunnelConstraint c)) tt
NilListType = forall (a :: Constraint). a => Dict a
Dict
astIsWithTunnelConstraint (ConsListType (Compose Dict (WithTunnelConstraint c a)
Dict) ListType (Compose Dict (WithTunnelConstraint c)) lt1
w) =
case forall (c :: (Type -> Type) -> Constraint) (tt :: [TransKind]).
(c Identity,
forall (f1 :: Type -> Type) (f2 :: Type -> Type).
(c f1, c f2) =>
c (ComposeInner f1 f2)) =>
ListType (Compose Dict (WithTunnelConstraint c)) tt
-> Dict (c (ApplyStackTunnel tt))
astIsWithTunnelConstraint ListType (Compose Dict (WithTunnelConstraint c)) lt1
w of
Dict (c (ApplyStackTunnel lt1))
Dict -> forall (a :: Constraint). a => Dict a
Dict
isWithTunnelConstraint ::
forall (c :: (Type -> Type) -> Constraint) (tt :: [TransKind]).
(c Identity, forall f1 f2. (c f1, c f2) => c (ComposeInner f1 f2))
=> IsStack (WithTunnelConstraint c) tt => Dict (c (ApplyStackTunnel tt))
isWithTunnelConstraint :: forall (c :: (Type -> Type) -> Constraint) (tt :: [TransKind]).
(c Identity,
forall (f1 :: Type -> Type) (f2 :: Type -> Type).
(c f1, c f2) =>
c (ComposeInner f1 f2),
IsStack (WithTunnelConstraint c) tt) =>
Dict (c (ApplyStackTunnel tt))
isWithTunnelConstraint =
forall (c :: (Type -> Type) -> Constraint) (tt :: [TransKind]).
(c Identity,
forall (f1 :: Type -> Type) (f2 :: Type -> Type).
(c f1, c f2) =>
c (ComposeInner f1 f2)) =>
ListType (Compose Dict (WithTunnelConstraint c)) tt
-> Dict (c (ApplyStackTunnel tt))
astIsWithTunnelConstraint @c forall a b. (a -> b) -> a -> b
$ forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative @_ @(ListType (Compose Dict (WithTunnelConstraint c))) @tt
type StackTunnel :: [TransKind] -> Type -> Type
newtype StackTunnel tt a = MkStackTunnel
{ forall (tt :: [TransKind]) a.
StackTunnel tt a -> ApplyStackTunnel tt a
unStackTunnel :: ApplyStackTunnel tt a
}
instance IsStack (WithTunnelConstraint Functor) tt => Functor (StackTunnel tt) where
fmap :: forall a b. (a -> b) -> StackTunnel tt a -> StackTunnel tt b
fmap =
case forall (c :: (Type -> Type) -> Constraint) (tt :: [TransKind]).
(c Identity,
forall (f1 :: Type -> Type) (f2 :: Type -> Type).
(c f1, c f2) =>
c (ComposeInner f1 f2),
IsStack (WithTunnelConstraint c) tt) =>
Dict (c (ApplyStackTunnel tt))
isWithTunnelConstraint @Functor @tt of
Dict (Functor (ApplyStackTunnel tt))
Dict -> \a -> b
ab (MkStackTunnel ApplyStackTunnel tt a
st) -> forall (tt :: [TransKind]) a.
ApplyStackTunnel tt a -> StackTunnel tt a
MkStackTunnel forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
ab ApplyStackTunnel tt a
st
instance (IsStack (WithTunnelConstraint Functor) tt, IsStack (WithTunnelConstraint MonadInner) tt) =>
Applicative (StackTunnel tt) where
pure :: forall a. a -> StackTunnel tt a
pure =
case forall (c :: (Type -> Type) -> Constraint) (tt :: [TransKind]).
(c Identity,
forall (f1 :: Type -> Type) (f2 :: Type -> Type).
(c f1, c f2) =>
c (ComposeInner f1 f2),
IsStack (WithTunnelConstraint c) tt) =>
Dict (c (ApplyStackTunnel tt))
isWithTunnelConstraint @MonadInner @tt of
Dict (MonadInner (ApplyStackTunnel tt))
Dict -> \a
a -> forall (tt :: [TransKind]) a.
ApplyStackTunnel tt a -> StackTunnel tt a
MkStackTunnel forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a. Applicative f => a -> f a
pure a
a
<*> :: forall a b.
StackTunnel tt (a -> b) -> StackTunnel tt a -> StackTunnel tt b
(<*>) =
case forall (c :: (Type -> Type) -> Constraint) (tt :: [TransKind]).
(c Identity,
forall (f1 :: Type -> Type) (f2 :: Type -> Type).
(c f1, c f2) =>
c (ComposeInner f1 f2),
IsStack (WithTunnelConstraint c) tt) =>
Dict (c (ApplyStackTunnel tt))
isWithTunnelConstraint @MonadInner @tt of
Dict (MonadInner (ApplyStackTunnel tt))
Dict -> \(MkStackTunnel ApplyStackTunnel tt (a -> b)
mab) (MkStackTunnel ApplyStackTunnel tt a
ma) -> forall (tt :: [TransKind]) a.
ApplyStackTunnel tt a -> StackTunnel tt a
MkStackTunnel forall a b. (a -> b) -> a -> b
$ ApplyStackTunnel tt (a -> b)
mab forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> ApplyStackTunnel tt a
ma
instance (IsStack (WithTunnelConstraint Functor) tt, IsStack (WithTunnelConstraint MonadInner) tt) =>
Foldable (StackTunnel tt) where
foldMap :: forall m a. Monoid m => (a -> m) -> StackTunnel tt a -> m
foldMap =
case forall (c :: (Type -> Type) -> Constraint) (tt :: [TransKind]).
(c Identity,
forall (f1 :: Type -> Type) (f2 :: Type -> Type).
(c f1, c f2) =>
c (ComposeInner f1 f2),
IsStack (WithTunnelConstraint c) tt) =>
Dict (c (ApplyStackTunnel tt))
isWithTunnelConstraint @MonadInner @tt of
Dict (MonadInner (ApplyStackTunnel tt))
Dict -> \a -> m
ab (MkStackTunnel ApplyStackTunnel tt a
st) -> forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
ab ApplyStackTunnel tt a
st
instance (IsStack (WithTunnelConstraint Functor) tt, IsStack (WithTunnelConstraint MonadInner) tt) =>
Traversable (StackTunnel tt) where
traverse :: forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> StackTunnel tt a -> f (StackTunnel tt b)
traverse =
case forall (c :: (Type -> Type) -> Constraint) (tt :: [TransKind]).
(c Identity,
forall (f1 :: Type -> Type) (f2 :: Type -> Type).
(c f1, c f2) =>
c (ComposeInner f1 f2),
IsStack (WithTunnelConstraint c) tt) =>
Dict (c (ApplyStackTunnel tt))
isWithTunnelConstraint @MonadInner @tt of
Dict (MonadInner (ApplyStackTunnel tt))
Dict -> \a -> f b
ab (MkStackTunnel ApplyStackTunnel tt a
st) -> forall (tt :: [TransKind]) a.
ApplyStackTunnel tt a -> StackTunnel tt a
MkStackTunnel forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
ab ApplyStackTunnel tt a
st
instance (IsStack (WithTunnelConstraint Functor) tt, IsStack (WithTunnelConstraint MonadInner) tt) =>
Monad (StackTunnel tt) where
return :: forall a. a -> StackTunnel tt a
return = forall (f :: Type -> Type) a. Applicative f => a -> f a
pure
>>= :: forall a b.
StackTunnel tt a -> (a -> StackTunnel tt b) -> StackTunnel tt b
(>>=) =
case forall (c :: (Type -> Type) -> Constraint) (tt :: [TransKind]).
(c Identity,
forall (f1 :: Type -> Type) (f2 :: Type -> Type).
(c f1, c f2) =>
c (ComposeInner f1 f2),
IsStack (WithTunnelConstraint c) tt) =>
Dict (c (ApplyStackTunnel tt))
isWithTunnelConstraint @MonadInner @tt of
Dict (MonadInner (ApplyStackTunnel tt))
Dict -> \(MkStackTunnel ApplyStackTunnel tt a
ma) a -> StackTunnel tt b
q -> forall (tt :: [TransKind]) a.
ApplyStackTunnel tt a -> StackTunnel tt a
MkStackTunnel forall a b. (a -> b) -> a -> b
$ ApplyStackTunnel tt a
ma forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (tt :: [TransKind]) a.
StackTunnel tt a -> ApplyStackTunnel tt a
unStackTunnel forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> StackTunnel tt b
q
instance (IsStack (WithTunnelConstraint Functor) tt, IsStack (WithTunnelConstraint MonadInner) tt) =>
MonadException (StackTunnel tt) where
type Exc (StackTunnel tt) = Exc (ApplyStackTunnel tt)
throwExc :: forall a. Exc (StackTunnel tt) -> StackTunnel tt a
throwExc Exc (StackTunnel tt)
e =
case forall (c :: (Type -> Type) -> Constraint) (tt :: [TransKind]).
(c Identity,
forall (f1 :: Type -> Type) (f2 :: Type -> Type).
(c f1, c f2) =>
c (ComposeInner f1 f2),
IsStack (WithTunnelConstraint c) tt) =>
Dict (c (ApplyStackTunnel tt))
isWithTunnelConstraint @MonadInner @tt of
Dict (MonadInner (ApplyStackTunnel tt))
Dict -> forall (tt :: [TransKind]) a.
ApplyStackTunnel tt a -> StackTunnel tt a
MkStackTunnel forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type) a. MonadException m => Exc m -> m a
throwExc Exc (StackTunnel tt)
e
catchExc :: forall a.
StackTunnel tt a
-> (Exc (StackTunnel tt) -> StackTunnel tt a) -> StackTunnel tt a
catchExc (MkStackTunnel ApplyStackTunnel tt a
st) Exc (StackTunnel tt) -> StackTunnel tt a
q =
case forall (c :: (Type -> Type) -> Constraint) (tt :: [TransKind]).
(c Identity,
forall (f1 :: Type -> Type) (f2 :: Type -> Type).
(c f1, c f2) =>
c (ComposeInner f1 f2),
IsStack (WithTunnelConstraint c) tt) =>
Dict (c (ApplyStackTunnel tt))
isWithTunnelConstraint @MonadInner @tt of
Dict (MonadInner (ApplyStackTunnel tt))
Dict -> forall (tt :: [TransKind]) a.
ApplyStackTunnel tt a -> StackTunnel tt a
MkStackTunnel forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type) a.
MonadException m =>
m a -> (Exc m -> m a) -> m a
catchExc ApplyStackTunnel tt a
st (forall (tt :: [TransKind]) a.
StackTunnel tt a -> ApplyStackTunnel tt a
unStackTunnel forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Exc (StackTunnel tt) -> StackTunnel tt a
q)
instance (IsStack (WithTunnelConstraint Functor) tt, IsStack (WithTunnelConstraint MonadInner) tt) =>
MonadInner (StackTunnel tt) where
retrieveInner :: forall a. StackTunnel tt a -> Result (Exc (StackTunnel tt)) a
retrieveInner =
case forall (c :: (Type -> Type) -> Constraint) (tt :: [TransKind]).
(c Identity,
forall (f1 :: Type -> Type) (f2 :: Type -> Type).
(c f1, c f2) =>
c (ComposeInner f1 f2),
IsStack (WithTunnelConstraint c) tt) =>
Dict (c (ApplyStackTunnel tt))
isWithTunnelConstraint @MonadInner @tt of
Dict (MonadInner (ApplyStackTunnel tt))
Dict -> \(MkStackTunnel ApplyStackTunnel tt a
st) -> forall (m :: Type -> Type) a.
MonadInner m =>
m a -> Result (Exc m) a
retrieveInner ApplyStackTunnel tt a
st
instance ( IsStack (WithTunnelConstraint Functor) tt
, IsStack (WithTunnelConstraint MonadInner) tt
, IsStack (WithTunnelConstraint MonadExtract) tt
, IsStack MonadTransUnlift tt
) => MonadExtract (StackTunnel tt) where
mToValue :: Extract (StackTunnel tt)
mToValue =
case forall (c :: (Type -> Type) -> Constraint) (tt :: [TransKind]).
(c Identity,
forall (f1 :: Type -> Type) (f2 :: Type -> Type).
(c f1, c f2) =>
c (ComposeInner f1 f2),
IsStack (WithTunnelConstraint c) tt) =>
Dict (c (ApplyStackTunnel tt))
isWithTunnelConstraint @MonadExtract @tt of
Dict (MonadExtract (ApplyStackTunnel tt))
Dict -> \(MkStackTunnel ApplyStackTunnel tt a
st) -> forall (m :: Type -> Type). MonadExtract m => Extract m
mToValue ApplyStackTunnel tt a
st
instance MonadTransStackTunnel tt => MonadTransHoist (StackT tt) where
hoist :: forall (m1 :: Type -> Type) (m2 :: Type -> Type).
(Monad m1, Monad m2) =>
(m1 --> m2) -> StackT tt m1 --> StackT tt m2
hoist = forall (t :: TransKind) (m1 :: Type -> Type) (m2 :: Type -> Type).
(MonadTransTunnel t, Monad m1, Monad m2) =>
(m1 --> m2) -> t m1 --> t m2
tunnelHoist
instance MonadTransStackTunnel tt => MonadTransTunnel (StackT tt) where
type Tunnel (StackT tt) = StackTunnel tt
tunnel ::
forall m2 r. Monad m2
=> ((forall m1 a. Monad m1 => StackT tt m1 a -> m1 (Tunnel (StackT tt) a)) -> m2 (Tunnel (StackT tt) r))
-> StackT tt m2 r
tunnel :: forall (m :: Type -> Type) r.
Monad m =>
((forall (m1 :: Type -> Type) a.
Monad m1 =>
StackT tt m1 a -> m1 (Tunnel (StackT tt) a))
-> m (Tunnel (StackT tt) r))
-> StackT tt m r
tunnel = let
build :: forall tt'. ListType (Compose Dict MonadTransTunnel) tt' -> TunnelWrapper (StackT tt')
build :: forall (tt' :: [TransKind]).
ListType (Compose Dict MonadTransTunnel) tt'
-> TunnelWrapper (StackT tt')
build ListType (Compose Dict MonadTransTunnel) tt'
NilListType =
forall (t :: TransKind).
(forall (m2 :: Type -> Type) r.
Monad m2 =>
((forall (m1 :: Type -> Type) a.
Monad m1 =>
t m1 a -> m1 (Tunnel t a))
-> m2 (Tunnel t r))
-> t m2 r)
-> TunnelWrapper t
MkTunnel forall a b. (a -> b) -> a -> b
$ \(forall (m1 :: Type -> Type) a.
Monad m1 =>
StackT tt' m1 a -> m1 (Tunnel (StackT tt') a))
-> m2 (Tunnel (StackT tt') r)
call ->
forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Identity a -> a
runIdentity forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (tt :: [TransKind]) a.
StackTunnel tt a -> ApplyStackTunnel tt a
unStackTunnel) forall a b. (a -> b) -> a -> b
$ (forall (m1 :: Type -> Type) a.
Monad m1 =>
StackT tt' m1 a -> m1 (Tunnel (StackT tt') a))
-> m2 (Tunnel (StackT tt') r)
call forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (tt :: [TransKind]) a.
ApplyStackTunnel tt a -> StackTunnel tt a
MkStackTunnel forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a. a -> Identity a
Identity) forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT
build (ConsListType (Compose Dict (MonadTransTunnel a)
Dict) (ListType (Compose Dict MonadTransTunnel) lt1
w :: ListType _ tt0)) =
case forall (tt' :: [TransKind]).
ListType (Compose Dict MonadTransTunnel) tt'
-> TunnelWrapper (StackT tt')
build ListType (Compose Dict MonadTransTunnel) lt1
w of
MkTunnel forall (m2 :: Type -> Type) r.
Monad m2 =>
((forall (m1 :: Type -> Type) a.
Monad m1 =>
StackT lt1 m1 a -> m1 (Tunnel (StackT lt1) a))
-> m2 (Tunnel (StackT lt1) r))
-> StackT lt1 m2 r
tunnel' -> let
tunnel'' ::
forall m2' r'. Monad m2'
=> ((forall m1 a. Monad m1 => StackT tt' m1 a -> m1 (Tunnel (StackT tt') a)) -> m2' (Tunnel (StackT tt') r'))
-> StackT tt' m2' r'
tunnel'' :: forall (m2' :: Type -> Type) r'.
Monad m2' =>
((forall (m1 :: Type -> Type) a.
Monad m1 =>
StackT tt' m1 a -> m1 (Tunnel (StackT tt') a))
-> m2' (Tunnel (StackT tt') r'))
-> StackT tt' m2' r'
tunnel'' (forall (m1 :: Type -> Type) a.
Monad m1 =>
StackT tt' m1 a -> m1 (Tunnel (StackT tt') a))
-> m2' (Tunnel (StackT tt') r')
call =
case (forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
(m :: Type -> Type).
cm m =>
ListType (Compose Dict (TransConstraint cm)) tt
-> Dict (cm (ApplyStack tt m))
witTransStackDict @Monad @tt0 @m2' forall a b. (a -> b) -> a -> b
$ forall {k} (wita :: k -> Type) (witb :: k -> Type) (t :: [k]).
(forall (t' :: k). wita t' -> witb t')
-> ListType wita t -> ListType witb t
mapListType (\(Compose Dict (MonadTransTunnel t')
Dict) -> forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose forall (a :: Constraint). a => Dict a
Dict) ListType (Compose Dict MonadTransTunnel) lt1
w) of
Dict (Monad (ApplyStack lt1 m2'))
Dict ->
forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall a b. (a -> b) -> a -> b
$
forall (t :: TransKind) (m :: Type -> Type) r.
(MonadTransTunnel t, Monad m) =>
((forall (m1 :: Type -> Type) a.
Monad m1 =>
t m1 a -> m1 (Tunnel t a))
-> m (Tunnel t r))
-> t m r
tunnel forall a b. (a -> b) -> a -> b
$ \forall (m1 :: Type -> Type) a.
Monad m1 =>
a m1 a -> m1 (Tunnel a a)
unlift1 ->
forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT forall a b. (a -> b) -> a -> b
$
forall (m2 :: Type -> Type) r.
Monad m2 =>
((forall (m1 :: Type -> Type) a.
Monad m1 =>
StackT lt1 m1 a -> m1 (Tunnel (StackT lt1) a))
-> m2 (Tunnel (StackT lt1) r))
-> StackT lt1 m2 r
tunnel' forall a b. (a -> b) -> a -> b
$ \forall (m1 :: Type -> Type) a.
Monad m1 =>
StackT lt1 m1 a -> m1 (Tunnel (StackT lt1) a)
unlift2 ->
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (tt :: [TransKind]) a.
ApplyStackTunnel tt a -> StackTunnel tt a
MkStackTunnel forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (inner :: Type -> Type) (outer :: Type -> Type) a.
ComposeInner inner outer a -> outer (inner a)
unComposeInner forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (tt :: [TransKind]) a.
StackTunnel tt a -> ApplyStackTunnel tt a
unStackTunnel) forall a b. (a -> b) -> a -> b
$
(forall (m1 :: Type -> Type) a.
Monad m1 =>
StackT tt' m1 a -> m1 (Tunnel (StackT tt') a))
-> m2' (Tunnel (StackT tt') r')
call forall a b. (a -> b) -> a -> b
$ \(MkStackT ApplyStack tt' m1 a
stt :: _ m1 _) ->
case (forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
(m :: Type -> Type).
cm m =>
ListType (Compose Dict (TransConstraint cm)) tt
-> Dict (cm (ApplyStack tt m))
witTransStackDict @Monad @tt0 @m1 forall a b. (a -> b) -> a -> b
$
forall {k} (wita :: k -> Type) (witb :: k -> Type) (t :: [k]).
(forall (t' :: k). wita t' -> witb t')
-> ListType wita t -> ListType witb t
mapListType (\(Compose Dict (MonadTransTunnel t')
Dict) -> forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose forall (a :: Constraint). a => Dict a
Dict) ListType (Compose Dict MonadTransTunnel) lt1
w) of
Dict (Monad (ApplyStack lt1 m1))
Dict ->
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (tt :: [TransKind]) a.
ApplyStackTunnel tt a -> StackTunnel tt a
MkStackTunnel forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (inner :: Type -> Type) (outer :: Type -> Type) a.
outer (inner a) -> ComposeInner inner outer a
MkComposeInner forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (tt :: [TransKind]) a.
StackTunnel tt a -> ApplyStackTunnel tt a
unStackTunnel) forall a b. (a -> b) -> a -> b
$
forall (m1 :: Type -> Type) a.
Monad m1 =>
StackT lt1 m1 a -> m1 (Tunnel (StackT lt1) a)
unlift2 forall a b. (a -> b) -> a -> b
$ forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall a b. (a -> b) -> a -> b
$ forall (m1 :: Type -> Type) a.
Monad m1 =>
a m1 a -> m1 (Tunnel a a)
unlift1 ApplyStack tt' m1 a
stt
in forall (t :: TransKind).
(forall (m2 :: Type -> Type) r.
Monad m2 =>
((forall (m1 :: Type -> Type) a.
Monad m1 =>
t m1 a -> m1 (Tunnel t a))
-> m2 (Tunnel t r))
-> t m2 r)
-> TunnelWrapper t
MkTunnel forall (m2' :: Type -> Type) r'.
Monad m2' =>
((forall (m1 :: Type -> Type) a.
Monad m1 =>
StackT tt' m1 a -> m1 (Tunnel (StackT tt') a))
-> m2' (Tunnel (StackT tt') r'))
-> StackT tt' m2' r'
tunnel''
in forall (t :: TransKind).
TunnelWrapper t
-> forall (m2 :: Type -> Type) r.
Monad m2 =>
((forall (m1 :: Type -> Type) a.
Monad m1 =>
t m1 a -> m1 (Tunnel t a))
-> m2 (Tunnel t r))
-> t m2 r
unTunnel forall a b. (a -> b) -> a -> b
$ forall (tt' :: [TransKind]).
ListType (Compose Dict MonadTransTunnel) tt'
-> TunnelWrapper (StackT tt')
build forall a b. (a -> b) -> a -> b
$ forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative @_ @(ListType (Compose Dict MonadTransTunnel)) @tt
stackHoist ::
forall tt ma mb. (MonadTransStackTunnel tt, Monad ma, Monad mb)
=> (ma --> mb)
-> ApplyStack tt ma --> ApplyStack tt mb
stackHoist :: forall (tt :: [TransKind]) (ma :: Type -> Type)
(mb :: Type -> Type).
(MonadTransStackTunnel tt, Monad ma, Monad mb) =>
(ma --> mb) -> ApplyStack tt ma --> ApplyStack tt mb
stackHoist ma --> mb
mf ApplyStack tt ma a
asta = forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT forall a b. (a -> b) -> a -> b
$ forall (t :: TransKind) (m1 :: Type -> Type) (m2 :: Type -> Type).
(MonadTransHoist t, Monad m1, Monad m2) =>
(m1 --> m2) -> t m1 --> t m2
hoist ma --> mb
mf forall a b. (a -> b) -> a -> b
$ forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT @tt ApplyStack tt ma a
asta
transStackExcept ::
forall tt m e a. (MonadTransStackTunnel tt, Monad m)
=> ApplyStack tt (ExceptT e m) a
-> ApplyStack tt m (Either e a)
transStackExcept :: forall (tt :: [TransKind]) (m :: Type -> Type) e a.
(MonadTransStackTunnel tt, Monad m) =>
ApplyStack tt (ExceptT e m) a -> ApplyStack tt m (Either e a)
transStackExcept ApplyStack tt (ExceptT e m) a
ata = forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT forall a b. (a -> b) -> a -> b
$ forall (t :: TransKind) (m :: Type -> Type) e a.
(MonadTransTunnel t, Applicative (Tunnel t), Monad m) =>
t (ExceptT e m) a -> t m (Either e a)
transExcept forall a b. (a -> b) -> a -> b
$ forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT @tt @(ExceptT e m) ApplyStack tt (ExceptT e m) a
ata
stackUnderliftIO ::
forall tt m. (MonadTransStackTunnel tt, MonadIO m)
=> ApplyStack tt IO --> ApplyStack tt m
stackUnderliftIO :: forall (tt :: [TransKind]) (m :: Type -> Type).
(MonadTransStackTunnel tt, MonadIO m) =>
ApplyStack tt IO --> ApplyStack tt m
stackUnderliftIO = forall (tt :: [TransKind]) (ma :: Type -> Type)
(mb :: Type -> Type).
(MonadTransStackTunnel tt, Monad ma, Monad mb) =>
(ma --> mb) -> ApplyStack tt ma --> ApplyStack tt mb
stackHoist @tt @IO @m forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO
stackWBackHoist ::
forall tt ma mb. (MonadTransStackUnlift tt, Monad ma, Monad mb)
=> WBackraised ma mb
-> WBackraised (ApplyStack tt ma) (ApplyStack tt mb)
stackWBackHoist :: forall (tt :: [TransKind]) (ma :: Type -> Type)
(mb :: Type -> Type).
(MonadTransStackUnlift tt, Monad ma, Monad mb) =>
WBackraised ma mb
-> WBackraised (ApplyStack tt ma) (ApplyStack tt mb)
stackWBackHoist WBackraised ma mb
mab = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (t :: TransKind) (ma :: Type -> Type) (mb :: Type -> Type).
(MonadTransTunnel t, Monad ma, Monad mb) =>
WBackraised ma mb -> WBackraised (t ma) (t mb)
wBackHoist @(StackT tt) WBackraised ma mb
mab
stackBackHoist ::
forall tt ma mb. (MonadTransStackUnlift tt, Monad ma, Monad mb)
=> (ma -/-> mb)
-> ApplyStack tt ma -/-> ApplyStack tt mb
stackBackHoist :: forall (tt :: [TransKind]) (ma :: Type -> Type)
(mb :: Type -> Type).
(MonadTransStackUnlift tt, Monad ma, Monad mb) =>
(ma -/-> mb) -> ApplyStack tt ma -/-> ApplyStack tt mb
stackBackHoist ma -/-> mb
f = forall k (p :: k -> Type) (q :: k -> Type).
WBackraised p q -> p -/-> q
unWBackraised forall a b. (a -> b) -> a -> b
$ forall (tt :: [TransKind]) (ma :: Type -> Type)
(mb :: Type -> Type).
(MonadTransStackUnlift tt, Monad ma, Monad mb) =>
WBackraised ma mb
-> WBackraised (ApplyStack tt ma) (ApplyStack tt mb)
stackWBackHoist @tt forall a b. (a -> b) -> a -> b
$ forall k (p :: k -> Type) (q :: k -> Type).
(p -/-> q) -> WBackraised p q
MkWBackraised ma -/-> mb
f
type MonadTransStackUnlift tt
= ( IsStack (TransConstraint MonadFail) tt
, IsStack (TransConstraint MonadIO) tt
, IsStack (TransConstraint MonadFix) tt
, IsStack (TransConstraint MonadTunnelIO) tt
, IsStack (TransConstraint MonadTunnelIOInner) tt
, IsStack (TransConstraint MonadUnliftIO) tt
, MonadTransStackTunnel tt
, IsStack (WithTunnelConstraint MonadExtract) tt
, IsStack MonadTransUnlift tt)
concatMonadTransStackUnliftDict ::
forall tt1 tt2. (MonadTransStackUnlift tt1, MonadTransStackUnlift tt2)
=> Dict (MonadTransStackUnlift (Concat tt1 tt2))
concatMonadTransStackUnliftDict :: forall (tt1 :: [TransKind]) (tt2 :: [TransKind]).
(MonadTransStackUnlift tt1, MonadTransStackUnlift tt2) =>
Dict (MonadTransStackUnlift (Concat tt1 tt2))
concatMonadTransStackUnliftDict =
case forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]).
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
Dict (Is (ListType w) (Concat aa bb))
concatIsDict @_ @(Compose Dict (TransConstraint MonadFail)) @tt1 @tt2 of
Dict
(Is
(ListType (Compose Dict (TransConstraint MonadFail)))
(Concat tt1 tt2))
Dict ->
case forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]).
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
Dict (Is (ListType w) (Concat aa bb))
concatIsDict @_ @(Compose Dict (TransConstraint MonadIO)) @tt1 @tt2 of
Dict
(Is
(ListType (Compose Dict (TransConstraint MonadIO)))
(Concat tt1 tt2))
Dict ->
case forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]).
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
Dict (Is (ListType w) (Concat aa bb))
concatIsDict @_ @(Compose Dict (TransConstraint MonadFix)) @tt1 @tt2 of
Dict
(Is
(ListType (Compose Dict (TransConstraint MonadFix)))
(Concat tt1 tt2))
Dict ->
case forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]).
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
Dict (Is (ListType w) (Concat aa bb))
concatIsDict @_ @(Compose Dict (TransConstraint MonadTunnelIO)) @tt1 @tt2 of
Dict
(Is
(ListType (Compose Dict (TransConstraint MonadTunnelIO)))
(Concat tt1 tt2))
Dict ->
case forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]).
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
Dict (Is (ListType w) (Concat aa bb))
concatIsDict @_ @(Compose Dict (TransConstraint MonadTunnelIOInner)) @tt1 @tt2 of
Dict
(Is
(ListType (Compose Dict (TransConstraint MonadTunnelIOInner)))
(Concat tt1 tt2))
Dict ->
case forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]).
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
Dict (Is (ListType w) (Concat aa bb))
concatIsDict
@_
@(Compose Dict (TransConstraint MonadUnliftIO))
@tt1
@tt2 of
Dict
(Is
(ListType (Compose Dict (TransConstraint MonadUnliftIO)))
(Concat tt1 tt2))
Dict ->
case forall (tt1 :: [TransKind]) (tt2 :: [TransKind]).
(MonadTransStackTunnel tt1, MonadTransStackTunnel tt2) =>
Dict (MonadTransStackTunnel (Concat tt1 tt2))
concatMonadTransStackTunnelDict @tt1 @tt2 of
Dict (MonadTransStackTunnel (Concat tt1 tt2))
Dict ->
case forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]).
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
Dict (Is (ListType w) (Concat aa bb))
concatIsDict
@_
@(Compose Dict MonadTransTunnel)
@tt1
@tt2 of
Dict
(Is (ListType (Compose Dict MonadTransTunnel)) (Concat tt1 tt2))
Dict ->
case forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]).
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
Dict (Is (ListType w) (Concat aa bb))
concatIsDict
@_
@(Compose Dict MonadTransUnlift)
@tt1
@tt2 of
Dict
(Is (ListType (Compose Dict MonadTransUnlift)) (Concat tt1 tt2))
Dict ->
case forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]).
(Representative w, Is (ListType w) aa, Is (ListType w) bb) =>
Dict (Is (ListType w) (Concat aa bb))
concatIsDict
@_
@(Compose Dict (WithTunnelConstraint MonadExtract))
@tt1
@tt2 of
Dict
(Is
(ListType (Compose Dict (WithTunnelConstraint MonadExtract)))
(Concat tt1 tt2))
Dict -> forall (a :: Constraint). a => Dict a
Dict
stackLiftWithUnlift ::
forall tt m. (MonadTransStackUnlift tt, MonadTunnelIOInner m)
=> m -/-> ApplyStack tt m
stackLiftWithUnlift :: forall (tt :: [TransKind]) (m :: Type -> Type).
(MonadTransStackUnlift tt, MonadTunnelIOInner m) =>
m -/-> ApplyStack tt m
stackLiftWithUnlift = forall k (p :: k -> Type) (q :: k -> Type).
WBackraised p q -> p -/-> q
unWBackraised forall a b. (a -> b) -> a -> b
$ coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (t :: TransKind) (m :: Type -> Type).
(MonadTransUnlift t, MonadTunnelIOInner m) =>
WBackraised m (t m)
wLiftWithUnlift @(StackT tt) @m
newtype LiftWithUnlift t = MkLiftWithUnlift
{ forall (t :: TransKind).
LiftWithUnlift t
-> forall (m :: Type -> Type) r.
MonadIO m =>
(Unlift MonadTunnelIOInner t -> m r) -> t m r
unLiftWithUnlift :: forall m r. MonadIO m => (Unlift MonadTunnelIOInner t -> m r) -> t m r
}
witFunctorOneTunnelIOStackDict ::
forall tt m. MonadInner (TunnelIO m)
=> ListType (Compose Dict MonadTransUnlift) tt
-> Dict (MonadInner (TunnelIO (ApplyStack tt m)))
witFunctorOneTunnelIOStackDict :: forall (tt :: [TransKind]) (m :: Type -> Type).
MonadInner (TunnelIO m) =>
ListType (Compose Dict MonadTransUnlift) tt
-> Dict (MonadInner (TunnelIO (ApplyStack tt m)))
witFunctorOneTunnelIOStackDict ListType (Compose Dict MonadTransUnlift) tt
NilListType = forall (a :: Constraint). a => Dict a
Dict
witFunctorOneTunnelIOStackDict (ConsListType (Compose Dict (MonadTransUnlift a)
Dict) ListType (Compose Dict MonadTransUnlift) lt1
lt) =
case forall (tt :: [TransKind]) (m :: Type -> Type).
MonadInner (TunnelIO m) =>
ListType (Compose Dict MonadTransUnlift) tt
-> Dict (MonadInner (TunnelIO (ApplyStack tt m)))
witFunctorOneTunnelIOStackDict @_ @m ListType (Compose Dict MonadTransUnlift) lt1
lt of
Dict (MonadInner (TunnelIO (ApplyStack lt1 m)))
Dict -> forall (a :: Constraint). a => Dict a
Dict
stackJoinUnlift ::
ListType (Compose Dict MonadTransUnlift) tt
-> Unlift MonadTunnelIOInner t
-> Unlift MonadTunnelIOInner (StackT tt)
-> Unlift MonadTunnelIOInner (StackT (t ': tt))
stackJoinUnlift :: forall (tt :: [TransKind]) (t :: TransKind).
ListType (Compose Dict MonadTransUnlift) tt
-> Unlift MonadTunnelIOInner t
-> Unlift MonadTunnelIOInner (StackT tt)
-> Unlift MonadTunnelIOInner (StackT (t : tt))
stackJoinUnlift ListType (Compose Dict MonadTransUnlift) tt
w Unlift MonadTunnelIOInner t
tmm Unlift MonadTunnelIOInner (StackT tt)
stmm (StackT (t : tt) m a
stma :: StackT (t ': tt) m a) =
case forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
(m :: Type -> Type).
cm m =>
ListType (Compose Dict (TransConstraint cm)) tt
-> Dict (cm (ApplyStack tt m))
witTransStackDict @MonadTunnelIOInner @tt @m forall a b. (a -> b) -> a -> b
$ forall {k} (wita :: k -> Type) (witb :: k -> Type) (t :: [k]).
(forall (t' :: k). wita t' -> witb t')
-> ListType wita t -> ListType witb t
mapListType (\(Compose Dict (MonadTransUnlift t')
Dict) -> forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose forall (a :: Constraint). a => Dict a
Dict) ListType (Compose Dict MonadTransUnlift) tt
w of
Dict (MonadTunnelIOInner (ApplyStack tt m))
Dict ->
case forall (tt :: [TransKind]) (m :: Type -> Type).
MonadInner (TunnelIO m) =>
ListType (Compose Dict MonadTransUnlift) tt
-> Dict (MonadInner (TunnelIO (ApplyStack tt m)))
witFunctorOneTunnelIOStackDict @tt @m ListType (Compose Dict MonadTransUnlift) tt
w of
Dict (MonadInner (TunnelIO (ApplyStack tt m)))
Dict -> Unlift MonadTunnelIOInner (StackT tt)
stmm forall a b. (a -> b) -> a -> b
$ forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall a b. (a -> b) -> a -> b
$ Unlift MonadTunnelIOInner t
tmm forall a b. (a -> b) -> a -> b
$ forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT StackT (t : tt) m a
stma
newtype GetDiscardingUnlift t = MkGetDiscardingUnlift
{ forall (t :: TransKind).
GetDiscardingUnlift t
-> forall (m :: Type -> Type).
Monad m =>
t m (WUnlift MonadTunnelIOInner t)
unGetDiscardingUnlift :: forall m. Monad m => t m (WUnlift MonadTunnelIOInner t)
}
instance MonadTransStackUnlift tt => MonadTransUnlift (StackT tt) where
liftWithUnlift ::
forall m r. MonadIO m
=> (Unlift MonadTunnelIOInner (StackT tt) -> m r)
-> StackT tt m r
liftWithUnlift :: forall (m :: Type -> Type) r.
MonadIO m =>
(Unlift MonadTunnelIOInner (StackT tt) -> m r) -> StackT tt m r
liftWithUnlift = let
build :: forall tt'. ListType (Compose Dict MonadTransUnlift) tt' -> LiftWithUnlift (StackT tt')
build :: forall (tt' :: [TransKind]).
ListType (Compose Dict MonadTransUnlift) tt'
-> LiftWithUnlift (StackT tt')
build ListType (Compose Dict MonadTransUnlift) tt'
NilListType = forall (t :: TransKind).
(forall (m :: Type -> Type) r.
MonadIO m =>
(Unlift MonadTunnelIOInner t -> m r) -> t m r)
-> LiftWithUnlift t
MkLiftWithUnlift forall a b. (a -> b) -> a -> b
$ \Unlift MonadTunnelIOInner (StackT tt') -> m r
call -> forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall a b. (a -> b) -> a -> b
$ Unlift MonadTunnelIOInner (StackT tt') -> m r
call forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT
build (ConsListType (Compose Dict (MonadTransUnlift a)
Dict) (ListType (Compose Dict MonadTransUnlift) lt1
w :: ListType _ tt0)) =
case forall (tt' :: [TransKind]).
ListType (Compose Dict MonadTransUnlift) tt'
-> LiftWithUnlift (StackT tt')
build ListType (Compose Dict MonadTransUnlift) lt1
w of
MkLiftWithUnlift forall (m :: Type -> Type) r.
MonadIO m =>
(Unlift MonadTunnelIOInner (StackT lt1) -> m r) -> StackT lt1 m r
liftWithUnlift' -> let
liftWithUnlift'' ::
forall m' r'. MonadIO m'
=> (Unlift MonadTunnelIOInner (StackT tt') -> m' r')
-> StackT tt' m' r'
liftWithUnlift'' :: forall (m' :: Type -> Type) r'.
MonadIO m' =>
(Unlift MonadTunnelIOInner (StackT tt') -> m' r')
-> StackT tt' m' r'
liftWithUnlift'' Unlift MonadTunnelIOInner (StackT tt') -> m' r'
call =
forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall a b. (a -> b) -> a -> b
$
case forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
(m :: Type -> Type).
cm m =>
ListType (Compose Dict (TransConstraint cm)) tt
-> Dict (cm (ApplyStack tt m))
witTransStackDict @MonadIO @tt0 @m' forall a b. (a -> b) -> a -> b
$ forall {k} (wita :: k -> Type) (witb :: k -> Type) (t :: [k]).
(forall (t' :: k). wita t' -> witb t')
-> ListType wita t -> ListType witb t
mapListType (\(Compose Dict (MonadTransUnlift t')
Dict) -> forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose forall (a :: Constraint). a => Dict a
Dict) ListType (Compose Dict MonadTransUnlift) lt1
w of
Dict (MonadIO (ApplyStack lt1 m'))
Dict ->
forall (t :: TransKind) (m :: Type -> Type) r.
(MonadTransUnlift t, MonadIO m) =>
(Unlift MonadTunnelIOInner t -> m r) -> t m r
liftWithUnlift forall a b. (a -> b) -> a -> b
$ \Unlift MonadTunnelIOInner a
unlift1 ->
forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type) r.
MonadIO m =>
(Unlift MonadTunnelIOInner (StackT lt1) -> m r) -> StackT lt1 m r
liftWithUnlift' forall a b. (a -> b) -> a -> b
$ \Unlift MonadTunnelIOInner (StackT lt1)
unlift2 -> Unlift MonadTunnelIOInner (StackT tt') -> m' r'
call forall a b. (a -> b) -> a -> b
$ forall (tt :: [TransKind]) (t :: TransKind).
ListType (Compose Dict MonadTransUnlift) tt
-> Unlift MonadTunnelIOInner t
-> Unlift MonadTunnelIOInner (StackT tt)
-> Unlift MonadTunnelIOInner (StackT (t : tt))
stackJoinUnlift ListType (Compose Dict MonadTransUnlift) lt1
w Unlift MonadTunnelIOInner a
unlift1 Unlift MonadTunnelIOInner (StackT lt1)
unlift2
in forall (t :: TransKind).
(forall (m :: Type -> Type) r.
MonadIO m =>
(Unlift MonadTunnelIOInner t -> m r) -> t m r)
-> LiftWithUnlift t
MkLiftWithUnlift forall (m' :: Type -> Type) r'.
MonadIO m' =>
(Unlift MonadTunnelIOInner (StackT tt') -> m' r')
-> StackT tt' m' r'
liftWithUnlift''
in forall (t :: TransKind).
LiftWithUnlift t
-> forall (m :: Type -> Type) r.
MonadIO m =>
(Unlift MonadTunnelIOInner t -> m r) -> t m r
unLiftWithUnlift forall a b. (a -> b) -> a -> b
$ forall (tt' :: [TransKind]).
ListType (Compose Dict MonadTransUnlift) tt'
-> LiftWithUnlift (StackT tt')
build forall a b. (a -> b) -> a -> b
$ forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative @_ @(ListType (Compose Dict MonadTransUnlift)) @tt
getDiscardingUnlift ::
forall m. Monad m
=> StackT tt m (WUnlift MonadTunnelIOInner (StackT tt))
getDiscardingUnlift :: forall (m :: Type -> Type).
Monad m =>
StackT tt m (WUnlift MonadTunnelIOInner (StackT tt))
getDiscardingUnlift = let
build :: forall tt'. ListType (Compose Dict MonadTransUnlift) tt' -> GetDiscardingUnlift (StackT tt')
build :: forall (tt' :: [TransKind]).
ListType (Compose Dict MonadTransUnlift) tt'
-> GetDiscardingUnlift (StackT tt')
build ListType (Compose Dict MonadTransUnlift) tt'
NilListType = forall (t :: TransKind).
(forall (m :: Type -> Type).
Monad m =>
t m (WUnlift MonadTunnelIOInner t))
-> GetDiscardingUnlift t
MkGetDiscardingUnlift forall a b. (a -> b) -> a -> b
$ forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (c :: (Type -> Type) -> Constraint) (t :: TransKind).
Unlift c t -> WUnlift c t
MkWUnlift forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT
build (ConsListType (Compose (Dict (MonadTransUnlift a)
Dict :: Dict (MonadTransUnlift t))) (ListType (Compose Dict MonadTransUnlift) lt1
w :: ListType _ tt0)) =
case forall (tt' :: [TransKind]).
ListType (Compose Dict MonadTransUnlift) tt'
-> GetDiscardingUnlift (StackT tt')
build ListType (Compose Dict MonadTransUnlift) lt1
w of
MkGetDiscardingUnlift forall (m :: Type -> Type).
Monad m =>
StackT lt1 m (WUnlift MonadTunnelIOInner (StackT lt1))
getDiscardingUnlift' -> let
getDiscardingUnlift'' ::
forall m'. Monad m'
=> StackT tt' m' (WUnlift MonadTunnelIOInner (StackT tt'))
getDiscardingUnlift'' :: forall (m' :: Type -> Type).
Monad m' =>
StackT tt' m' (WUnlift MonadTunnelIOInner (StackT tt'))
getDiscardingUnlift'' =
forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall a b. (a -> b) -> a -> b
$
case forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
(m :: Type -> Type).
cm m =>
ListType (Compose Dict (TransConstraint cm)) tt
-> Dict (cm (ApplyStack tt m))
witTransStackDict @Monad @tt0 @m' forall a b. (a -> b) -> a -> b
$ forall {k} (wita :: k -> Type) (witb :: k -> Type) (t :: [k]).
(forall (t' :: k). wita t' -> witb t')
-> ListType wita t -> ListType witb t
mapListType (\(Compose Dict (MonadTransUnlift t')
Dict) -> forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose forall (a :: Constraint). a => Dict a
Dict) ListType (Compose Dict MonadTransUnlift) lt1
w of
Dict (Monad (ApplyStack lt1 m'))
Dict ->
forall (c :: (Type -> Type) -> Constraint) (t :: TransKind)
(m :: Type -> Type) a.
(TransConstraint c t, c m) =>
(c (t m) => t m a) -> t m a
withTransConstraintTM @Monad forall a b. (a -> b) -> a -> b
$ do
MkWUnlift Unlift MonadTunnelIOInner a
unlift1 <- forall (t :: TransKind) (m :: Type -> Type).
(MonadTransUnlift t, Monad m) =>
t m (WUnlift MonadTunnelIOInner t)
getDiscardingUnlift
MkWUnlift Unlift MonadTunnelIOInner (StackT lt1)
unlift2 <- forall (t :: TransKind) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type).
Monad m =>
StackT lt1 m (WUnlift MonadTunnelIOInner (StackT lt1))
getDiscardingUnlift' @m'
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (c :: (Type -> Type) -> Constraint) (t :: TransKind).
Unlift c t -> WUnlift c t
MkWUnlift forall a b. (a -> b) -> a -> b
$ forall (tt :: [TransKind]) (t :: TransKind).
ListType (Compose Dict MonadTransUnlift) tt
-> Unlift MonadTunnelIOInner t
-> Unlift MonadTunnelIOInner (StackT tt)
-> Unlift MonadTunnelIOInner (StackT (t : tt))
stackJoinUnlift ListType (Compose Dict MonadTransUnlift) lt1
w Unlift MonadTunnelIOInner a
unlift1 Unlift MonadTunnelIOInner (StackT lt1)
unlift2
in forall (t :: TransKind).
(forall (m :: Type -> Type).
Monad m =>
t m (WUnlift MonadTunnelIOInner t))
-> GetDiscardingUnlift t
MkGetDiscardingUnlift forall (m' :: Type -> Type).
Monad m' =>
StackT tt' m' (WUnlift MonadTunnelIOInner (StackT tt'))
getDiscardingUnlift''
in forall (t :: TransKind).
GetDiscardingUnlift t
-> forall (m :: Type -> Type).
Monad m =>
t m (WUnlift MonadTunnelIOInner t)
unGetDiscardingUnlift forall a b. (a -> b) -> a -> b
$ forall (tt' :: [TransKind]).
ListType (Compose Dict MonadTransUnlift) tt'
-> GetDiscardingUnlift (StackT tt')
build forall a b. (a -> b) -> a -> b
$ forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative @_ @(ListType (Compose Dict MonadTransUnlift)) @tt
stackConcatFst ::
forall tt1 tt2 m. (MonadTransStackUnlift tt1, MonadTransStackUnlift tt2, Monad m)
=> ApplyStack tt1 m --> ApplyStack (Concat tt1 tt2) m
stackConcatFst :: forall (tt1 :: [TransKind]) (tt2 :: [TransKind])
(m :: Type -> Type).
(MonadTransStackUnlift tt1, MonadTransStackUnlift tt2, Monad m) =>
ApplyStack tt1 m --> ApplyStack (Concat tt1 tt2) m
stackConcatFst =
case forall (tt1 :: [TransKind]) (tt2 :: [TransKind])
(m :: Type -> Type).
MonadTransStackUnlift tt1 =>
ApplyStack (Concat tt1 tt2) m :~: ApplyStack tt1 (ApplyStack tt2 m)
transStackConcatRefl @tt1 @tt2 @m of
ApplyStack (Concat tt1 tt2) m :~: ApplyStack tt1 (ApplyStack tt2 m)
Refl ->
case forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
(m :: Type -> Type).
(IsStack (TransConstraint cm) tt, cm m) =>
Dict (cm (ApplyStack tt m))
transStackDict @Monad @tt2 @m of
Dict (Monad (ApplyStack tt2 m))
Dict -> forall (tt :: [TransKind]) (ma :: Type -> Type)
(mb :: Type -> Type).
(MonadTransStackTunnel tt, Monad ma, Monad mb) =>
(ma --> mb) -> ApplyStack tt ma --> ApplyStack tt mb
stackHoist @tt1 forall a b. (a -> b) -> a -> b
$ forall (tt :: [TransKind]) (m :: Type -> Type).
(IsStack (TransConstraint Monad) tt, IsStack MonadTrans tt,
Monad m) =>
m --> ApplyStack tt m
stackLift @tt2 @m
stackConcatSnd ::
forall tt1 tt2 m. (MonadTransStackUnlift tt1, MonadTransStackUnlift tt2, Monad m)
=> ApplyStack tt2 m --> ApplyStack (Concat tt1 tt2) m
stackConcatSnd :: forall (tt1 :: [TransKind]) (tt2 :: [TransKind])
(m :: Type -> Type).
(MonadTransStackUnlift tt1, MonadTransStackUnlift tt2, Monad m) =>
ApplyStack tt2 m --> ApplyStack (Concat tt1 tt2) m
stackConcatSnd =
case forall (tt1 :: [TransKind]) (tt2 :: [TransKind])
(m :: Type -> Type).
MonadTransStackUnlift tt1 =>
ApplyStack (Concat tt1 tt2) m :~: ApplyStack tt1 (ApplyStack tt2 m)
transStackConcatRefl @tt1 @tt2 @m of
ApplyStack (Concat tt1 tt2) m :~: ApplyStack tt1 (ApplyStack tt2 m)
Refl ->
case forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
(m :: Type -> Type).
(IsStack (TransConstraint cm) tt, cm m) =>
Dict (cm (ApplyStack tt m))
transStackDict @Monad @tt2 @m of
Dict (Monad (ApplyStack tt2 m))
Dict -> forall (tt :: [TransKind]) (m :: Type -> Type).
(IsStack (TransConstraint Monad) tt, IsStack MonadTrans tt,
Monad m) =>
m --> ApplyStack tt m
stackLift @tt1
stackCommute ::
forall tta ttb m r. (MonadTransStackUnlift tta, MonadTransStackUnlift ttb, MonadTunnelIO m)
=> ApplyStack tta (ApplyStack ttb m) r
-> ApplyStack ttb (ApplyStack tta m) r
stackCommute :: forall (tta :: [TransKind]) (ttb :: [TransKind])
(m :: Type -> Type) r.
(MonadTransStackUnlift tta, MonadTransStackUnlift ttb,
MonadTunnelIO m) =>
ApplyStack tta (ApplyStack ttb m) r
-> ApplyStack ttb (ApplyStack tta m) r
stackCommute ApplyStack tta (ApplyStack ttb m) r
aar =
case (forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
(m :: Type -> Type).
(IsStack (TransConstraint cm) tt, cm m) =>
Dict (cm (ApplyStack tt m))
transStackDict @MonadTunnelIO @tta @m, forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
(m :: Type -> Type).
(IsStack (TransConstraint cm) tt, cm m) =>
Dict (cm (ApplyStack tt m))
transStackDict @MonadTunnelIO @ttb @m) of
(Dict (MonadTunnelIO (ApplyStack tta m))
Dict, Dict (MonadTunnelIO (ApplyStack ttb m))
Dict) -> let
ssr :: StackT tta (StackT ttb m) r
ssr :: StackT tta (StackT ttb m) r
ssr = forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT forall a b. (a -> b) -> a -> b
$ forall (tt :: [TransKind]) (ma :: Type -> Type)
(mb :: Type -> Type).
(MonadTransStackTunnel tt, Monad ma, Monad mb) =>
(ma --> mb) -> ApplyStack tt ma --> ApplyStack tt mb
stackHoist @tta @(ApplyStack ttb m) @(StackT ttb m) forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT ApplyStack tta (ApplyStack ttb m) r
aar
in forall (tt :: [TransKind]) (ma :: Type -> Type)
(mb :: Type -> Type).
(MonadTransStackTunnel tt, Monad ma, Monad mb) =>
(ma --> mb) -> ApplyStack tt ma --> ApplyStack tt mb
stackHoist @ttb @(StackT tta m) @(ApplyStack tta m) forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT forall a b. (a -> b) -> a -> b
$ forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT forall a b. (a -> b) -> a -> b
$ forall (ta :: TransKind) (tb :: TransKind) (m :: Type -> Type).
(MonadTransTunnel ta, MonadTransTunnel tb, Monad (Tunnel ta),
MonadInner (Tunnel tb), Monad m) =>
ta (tb m) --> tb (ta m)
commuteT StackT tta (StackT ttb m) r
ssr
transStackConcatRefl ::
forall (tt1 :: [TransKind]) (tt2 :: [TransKind]) m. MonadTransStackUnlift tt1
=> (ApplyStack (Concat tt1 tt2) m) :~: (ApplyStack tt1 (ApplyStack tt2 m))
transStackConcatRefl :: forall (tt1 :: [TransKind]) (tt2 :: [TransKind])
(m :: Type -> Type).
MonadTransStackUnlift tt1 =>
ApplyStack (Concat tt1 tt2) m :~: ApplyStack tt1 (ApplyStack tt2 m)
transStackConcatRefl = forall k (f1 :: [k -> k]) (f2 :: [k -> k]) (a :: k)
(w :: (k -> k) -> Type).
Is (ListType w) f1 =>
ApplyStack (Concat f1 f2) a :~: ApplyStack f1 (ApplyStack f2 a)
applyConcatRefl @_ @tt1 @tt2 @m @(Compose Dict MonadTransUnlift)
type StackUnlift (tt :: [TransKind]) = forall m. MonadUnliftIO m => ApplyStack tt m --> m
newtype WStackUnlift (tt :: [TransKind]) = MkWStackUnlift
{ forall (tt :: [TransKind]). WStackUnlift tt -> StackUnlift tt
unWStackUnlift :: StackUnlift tt
}
consWStackUnlift ::
forall t tt. IsStack (TransConstraint MonadUnliftIO) tt
=> WUnlift MonadUnliftIO t
-> WStackUnlift tt
-> WStackUnlift (t ': tt)
consWStackUnlift :: forall (t :: TransKind) (tt :: [TransKind]).
IsStack (TransConstraint MonadUnliftIO) tt =>
WUnlift MonadUnliftIO t -> WStackUnlift tt -> WStackUnlift (t : tt)
consWStackUnlift (MkWUnlift Unlift MonadUnliftIO t
unlift1) (MkWStackUnlift StackUnlift tt
unliftr) = let
unlift ::
forall m. MonadUnliftIO m
=> t (ApplyStack tt m) --> m
unlift :: forall (m :: Type -> Type).
MonadUnliftIO m =>
t (ApplyStack tt m) --> m
unlift =
case forall (cm :: (Type -> Type) -> Constraint) (tt :: [TransKind])
(m :: Type -> Type).
(IsStack (TransConstraint cm) tt, cm m) =>
Dict (cm (ApplyStack tt m))
transStackDict @MonadUnliftIO @tt @m of
Dict (MonadUnliftIO (ApplyStack tt m))
Dict -> StackUnlift tt
unliftr forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Unlift MonadUnliftIO t
unlift1
in forall (tt :: [TransKind]). StackUnlift tt -> WStackUnlift tt
MkWStackUnlift forall (m :: Type -> Type).
MonadUnliftIO m =>
t (ApplyStack tt m) --> m
unlift
stackLiftWithStackUnlift ::
forall tt m r. (MonadTransStackUnlift tt, MonadIO m)
=> (StackUnlift tt -> m r)
-> ApplyStack tt m r
stackLiftWithStackUnlift :: forall (tt :: [TransKind]) (m :: Type -> Type) r.
(MonadTransStackUnlift tt, MonadIO m) =>
(StackUnlift tt -> m r) -> ApplyStack tt m r
stackLiftWithStackUnlift StackUnlift tt -> m r
call = forall (tt :: [TransKind]) (m :: Type -> Type) a.
StackT tt m a -> ApplyStack tt m a
unStackT @tt forall a b. (a -> b) -> a -> b
$ forall (t :: TransKind) (m :: Type -> Type) r.
(MonadTransUnlift t, MonadIO m) =>
(Unlift MonadTunnelIOInner t -> m r) -> t m r
liftWithUnlift forall a b. (a -> b) -> a -> b
$ \Unlift MonadTunnelIOInner (StackT tt)
unlift -> StackUnlift tt -> m r
call forall a b. (a -> b) -> a -> b
$ \ApplyStack tt m a
astm -> Unlift MonadTunnelIOInner (StackT tt)
unlift forall a b. (a -> b) -> a -> b
$ forall (tt :: [TransKind]) (m :: Type -> Type) a.
ApplyStack tt m a -> StackT tt m a
MkStackT ApplyStack tt m a
astm