module Control.Monad.Ology.General.Trans.Tunnel where

import Control.Monad.Ology.General.Function
import Control.Monad.Ology.General.IO
import Control.Monad.Ology.General.Inner
import Control.Monad.Ology.General.Trans.Constraint
import Control.Monad.Ology.General.Trans.Hoist
import Control.Monad.Ology.Specific.ComposeInner
import Import

-- | Monad transformers that allow \"tunneling\" (working with the monad under the transformer).
type MonadTransTunnel :: TransKind -> Constraint
class (MonadTransHoist t, MonadInner (Tunnel t)) => MonadTransTunnel t where
    -- | The tunnel monad of this transformer.
    type Tunnel t :: Type -> Type
    tunnel ::
           forall m r. Monad m
        => ((forall m1 a. Monad m1 => t m1 a -> m1 (Tunnel t a)) -> m (Tunnel t r))
        -> t m r

tunnelHoist ::
       forall t m1 m2. (MonadTransTunnel t, Monad m1, Monad m2)
    => (m1 --> m2)
    -> t m1 --> t m2
tunnelHoist :: forall (t :: TransKind) (m1 :: Type -> Type) (m2 :: Type -> Type).
(MonadTransTunnel t, Monad m1, Monad m2) =>
(m1 --> m2) -> t m1 --> t m2
tunnelHoist m1 --> m2
mma t m1 a
sm1 = ((forall (m1 :: Type -> Type) a.
  Monad m1 =>
  t m1 a -> m1 (Tunnel t a))
 -> m2 (Tunnel t a))
-> t m2 a
forall (m :: Type -> Type) r.
Monad m =>
((forall (m1 :: Type -> Type) a.
  Monad m1 =>
  t m1 a -> m1 (Tunnel t a))
 -> m (Tunnel t r))
-> t 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 =>
   t m1 a -> m1 (Tunnel t a))
  -> m2 (Tunnel t a))
 -> t m2 a)
-> ((forall (m1 :: Type -> Type) a.
     Monad m1 =>
     t m1 a -> m1 (Tunnel t a))
    -> m2 (Tunnel t a))
-> t m2 a
forall a b. (a -> b) -> a -> b
$ \forall (m1 :: Type -> Type) a.
Monad m1 =>
t m1 a -> m1 (Tunnel t a)
tun -> m1 (Tunnel t a) -> m2 (Tunnel t a)
m1 --> m2
mma (m1 (Tunnel t a) -> m2 (Tunnel t a))
-> m1 (Tunnel t a) -> m2 (Tunnel t a)
forall a b. (a -> b) -> a -> b
$ t m1 a -> m1 (Tunnel t a)
forall (m1 :: Type -> Type) a.
Monad m1 =>
t m1 a -> m1 (Tunnel t a)
tun t m1 a
sm1

hoistWith ::
       forall t m1 m2 f r. (MonadTransTunnel t, Traversable f, Monad m1, Monad m2)
    => (forall a. m1 a -> m2 (f a))
    -> t m1 r
    -> t m2 (f r)
hoistWith :: forall (t :: TransKind) (m1 :: Type -> Type) (m2 :: Type -> Type)
       (f :: Type -> Type) r.
(MonadTransTunnel t, Traversable f, Monad m1, Monad m2) =>
(forall a. m1 a -> m2 (f a)) -> t m1 r -> t m2 (f r)
hoistWith forall a. m1 a -> m2 (f a)
mma t m1 r
sm1 = ((forall (m1 :: Type -> Type) a.
  Monad m1 =>
  t m1 a -> m1 (Tunnel t a))
 -> m2 (Tunnel t (f r)))
-> t m2 (f r)
forall (m :: Type -> Type) r.
Monad m =>
((forall (m1 :: Type -> Type) a.
  Monad m1 =>
  t m1 a -> m1 (Tunnel t a))
 -> m (Tunnel t r))
-> t 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 =>
   t m1 a -> m1 (Tunnel t a))
  -> m2 (Tunnel t (f r)))
 -> t m2 (f r))
-> ((forall (m1 :: Type -> Type) a.
     Monad m1 =>
     t m1 a -> m1 (Tunnel t a))
    -> m2 (Tunnel t (f r)))
-> t m2 (f r)
forall a b. (a -> b) -> a -> b
$ \forall (m1 :: Type -> Type) a.
Monad m1 =>
t m1 a -> m1 (Tunnel t a)
tun -> (f (Tunnel t r) -> Tunnel t (f r))
-> m2 (f (Tunnel t r)) -> m2 (Tunnel t (f 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 f (Tunnel t r) -> Tunnel t (f r)
forall (t :: Type -> Type) (f :: Type -> Type) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: Type -> Type) a. Applicative f => f (f a) -> f (f a)
sequenceA (m2 (f (Tunnel t r)) -> m2 (Tunnel t (f r)))
-> m2 (f (Tunnel t r)) -> m2 (Tunnel t (f r))
forall a b. (a -> b) -> a -> b
$ m1 (Tunnel t r) -> m2 (f (Tunnel t r))
forall a. m1 a -> m2 (f a)
mma (m1 (Tunnel t r) -> m2 (f (Tunnel t r)))
-> m1 (Tunnel t r) -> m2 (f (Tunnel t r))
forall a b. (a -> b) -> a -> b
$ t m1 r -> m1 (Tunnel t r)
forall (m1 :: Type -> Type) a.
Monad m1 =>
t m1 a -> m1 (Tunnel t a)
tun t m1 r
sm1

backHoist :: (MonadTransTunnel t, Monad ma, Monad mb) => (ma -/-> mb) -> t ma -/-> t mb
backHoist :: forall (t :: TransKind) (ma :: Type -> Type) (mb :: Type -> Type).
(MonadTransTunnel t, Monad ma, Monad mb) =>
(ma -/-> mb) -> t ma -/-> t mb
backHoist ma -/-> mb
wt (t mb --> t ma) -> t ma r
tm = ((forall (m1 :: Type -> Type) a.
  Monad m1 =>
  t m1 a -> m1 (Tunnel t a))
 -> mb (Tunnel t r))
-> t mb r
forall (m :: Type -> Type) r.
Monad m =>
((forall (m1 :: Type -> Type) a.
  Monad m1 =>
  t m1 a -> m1 (Tunnel t a))
 -> m (Tunnel t r))
-> t 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 =>
   t m1 a -> m1 (Tunnel t a))
  -> mb (Tunnel t r))
 -> t mb r)
-> ((forall (m1 :: Type -> Type) a.
     Monad m1 =>
     t m1 a -> m1 (Tunnel t a))
    -> mb (Tunnel t r))
-> t mb r
forall a b. (a -> b) -> a -> b
$ \forall (m1 :: Type -> Type) a.
Monad m1 =>
t m1 a -> m1 (Tunnel t a)
unlift -> ((mb --> ma) -> ma (Tunnel t r)) -> mb (Tunnel t r)
ma -/-> mb
wt (((mb --> ma) -> ma (Tunnel t r)) -> mb (Tunnel t r))
-> ((mb --> ma) -> ma (Tunnel t r)) -> mb (Tunnel t r)
forall a b. (a -> b) -> a -> b
$ \mb --> ma
tba -> t ma r -> ma (Tunnel t r)
forall (m1 :: Type -> Type) a.
Monad m1 =>
t m1 a -> m1 (Tunnel t a)
unlift (t ma r -> ma (Tunnel t r)) -> t ma r -> ma (Tunnel t r)
forall a b. (a -> b) -> a -> b
$ (t mb --> t ma) -> t ma r
tm ((t mb --> t ma) -> t ma r) -> (t mb --> t ma) -> t ma r
forall a b. (a -> b) -> a -> b
$ (mb --> ma) -> t mb --> t ma
forall (m1 :: Type -> Type) (m2 :: Type -> Type).
(Monad m1, Monad m2) =>
(m1 --> m2) -> t m1 --> t m2
forall (t :: TransKind) (m1 :: Type -> Type) (m2 :: Type -> Type).
(MonadTransHoist t, Monad m1, Monad m2) =>
(m1 --> m2) -> t m1 --> t m2
hoist mb a -> ma a
mb --> ma
tba

wBackHoist :: (MonadTransTunnel t, Monad ma, Monad mb) => WBackraised ma mb -> WBackraised (t ma) (t mb)
wBackHoist :: forall (t :: TransKind) (ma :: Type -> Type) (mb :: Type -> Type).
(MonadTransTunnel t, Monad ma, Monad mb) =>
WBackraised ma mb -> WBackraised (t ma) (t mb)
wBackHoist (MkWBackraised ma -/-> mb
f) = (t ma -/-> t mb) -> WBackraised (t ma) (t mb)
forall k (p :: k -> Type) (q :: k -> Type).
(p -/-> q) -> WBackraised p q
MkWBackraised ((t ma -/-> t mb) -> WBackraised (t ma) (t mb))
-> (t ma -/-> t mb) -> WBackraised (t ma) (t mb)
forall a b. (a -> b) -> a -> b
$ (ma -/-> mb) -> t ma -/-> t mb
forall (t :: TransKind) (ma :: Type -> Type) (mb :: Type -> Type).
(MonadTransTunnel t, Monad ma, Monad mb) =>
(ma -/-> mb) -> t ma -/-> t mb
backHoist ((mb --> ma) -> ma r) -> mb r
ma -/-> mb
f

-- | Commute two transformers in a transformer stack, by commuting their tunnel monads.
commuteTWith ::
       forall ta tb m. (MonadTransTunnel ta, MonadTransTunnel tb, Monad m)
    => (forall r. Tunnel tb (Tunnel ta r) -> Tunnel ta (Tunnel tb r))
    -> ta (tb m) --> tb (ta m)
commuteTWith :: forall (ta :: TransKind) (tb :: TransKind) (m :: Type -> Type).
(MonadTransTunnel ta, MonadTransTunnel tb, Monad m) =>
(forall r. Tunnel tb (Tunnel ta r) -> Tunnel ta (Tunnel tb r))
-> ta (tb m) --> tb (ta m)
commuteTWith forall r. Tunnel tb (Tunnel ta r) -> Tunnel ta (Tunnel tb r)
commutef ta (tb m) a
tabm =
    case forall (c :: (Type -> Type) -> Constraint) (t :: TransKind)
       (m :: Type -> Type).
(TransConstraint c t, c m) =>
Dict (c (t m))
hasTransConstraint @Monad @ta @m of
        Dict (Monad (ta m))
Dict ->
            case forall (c :: (Type -> Type) -> Constraint) (t :: TransKind)
       (m :: Type -> Type).
(TransConstraint c t, c m) =>
Dict (c (t m))
hasTransConstraint @Monad @tb @m of
                Dict (Monad (tb m))
Dict -> ((forall (m1 :: Type -> Type) a.
  Monad m1 =>
  tb m1 a -> m1 (Tunnel tb a))
 -> ta m (Tunnel tb a))
-> tb (ta m) a
forall (m :: Type -> Type) r.
Monad m =>
((forall (m1 :: Type -> Type) a.
  Monad m1 =>
  tb m1 a -> m1 (Tunnel tb a))
 -> m (Tunnel tb r))
-> tb 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 =>
   tb m1 a -> m1 (Tunnel tb a))
  -> ta m (Tunnel tb a))
 -> tb (ta m) a)
-> ((forall (m1 :: Type -> Type) a.
     Monad m1 =>
     tb m1 a -> m1 (Tunnel tb a))
    -> ta m (Tunnel tb a))
-> tb (ta m) a
forall a b. (a -> b) -> a -> b
$ \forall (m1 :: Type -> Type) a.
Monad m1 =>
tb m1 a -> m1 (Tunnel tb a)
unliftb -> ((forall (m1 :: Type -> Type) a.
  Monad m1 =>
  ta m1 a -> m1 (Tunnel ta a))
 -> m (Tunnel ta (Tunnel tb a)))
-> ta m (Tunnel tb a)
forall (m :: Type -> Type) r.
Monad m =>
((forall (m1 :: Type -> Type) a.
  Monad m1 =>
  ta m1 a -> m1 (Tunnel ta a))
 -> m (Tunnel ta r))
-> ta 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 =>
   ta m1 a -> m1 (Tunnel ta a))
  -> m (Tunnel ta (Tunnel tb a)))
 -> ta m (Tunnel tb a))
-> ((forall (m1 :: Type -> Type) a.
     Monad m1 =>
     ta m1 a -> m1 (Tunnel ta a))
    -> m (Tunnel ta (Tunnel tb a)))
-> ta m (Tunnel tb a)
forall a b. (a -> b) -> a -> b
$ \forall (m1 :: Type -> Type) a.
Monad m1 =>
ta m1 a -> m1 (Tunnel ta a)
unlifta -> (Tunnel tb (Tunnel ta a) -> Tunnel ta (Tunnel tb a))
-> m (Tunnel tb (Tunnel ta a)) -> m (Tunnel ta (Tunnel tb a))
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Tunnel tb (Tunnel ta a) -> Tunnel ta (Tunnel tb a)
forall r. Tunnel tb (Tunnel ta r) -> Tunnel ta (Tunnel tb r)
commutef (m (Tunnel tb (Tunnel ta a)) -> m (Tunnel ta (Tunnel tb a)))
-> m (Tunnel tb (Tunnel ta a)) -> m (Tunnel ta (Tunnel tb a))
forall a b. (a -> b) -> a -> b
$ tb m (Tunnel ta a) -> m (Tunnel tb (Tunnel ta a))
forall (m1 :: Type -> Type) a.
Monad m1 =>
tb m1 a -> m1 (Tunnel tb a)
unliftb (tb m (Tunnel ta a) -> m (Tunnel tb (Tunnel ta a)))
-> tb m (Tunnel ta a) -> m (Tunnel tb (Tunnel ta a))
forall a b. (a -> b) -> a -> b
$ ta (tb m) a -> tb m (Tunnel ta a)
forall (m1 :: Type -> Type) a.
Monad m1 =>
ta m1 a -> m1 (Tunnel ta a)
unlifta ta (tb m) a
tabm

-- | Commute two transformers in a transformer stack.
commuteT ::
       forall ta tb m. (MonadTransTunnel ta, MonadTransTunnel tb, Monad m)
    => ta (tb m) --> tb (ta m)
commuteT :: forall (ta :: TransKind) (tb :: TransKind) (m :: Type -> Type).
(MonadTransTunnel ta, MonadTransTunnel tb, Monad m) =>
ta (tb m) --> tb (ta m)
commuteT = (forall r. Tunnel tb (Tunnel ta r) -> Tunnel ta (Tunnel tb r))
-> ta (tb m) --> tb (ta m)
forall (ta :: TransKind) (tb :: TransKind) (m :: Type -> Type).
(MonadTransTunnel ta, MonadTransTunnel tb, Monad m) =>
(forall r. Tunnel tb (Tunnel ta r) -> Tunnel ta (Tunnel tb r))
-> ta (tb m) --> tb (ta m)
commuteTWith Tunnel tb (Tunnel ta r) -> Tunnel ta (Tunnel tb r)
forall r. Tunnel tb (Tunnel ta r) -> Tunnel ta (Tunnel tb r)
forall (m :: Type -> Type) (f :: Type -> Type) a.
(MonadInner m, Applicative f) =>
m (f a) -> f (m a)
commuteInner

commuteTBack ::
       forall ta tb m. (MonadTransTunnel ta, MonadTransTunnel tb, Monad m)
    => ta (tb m) -/-> tb (ta m)
commuteTBack :: forall (ta :: TransKind) (tb :: TransKind) (m :: Type -> Type).
(MonadTransTunnel ta, MonadTransTunnel tb, Monad m) =>
ta (tb m) -/-> tb (ta m)
commuteTBack (tb (ta m) --> ta (tb m)) -> ta (tb m) r
call = ta (tb m) r -> tb (ta m) r
ta (tb m) --> tb (ta m)
forall (ta :: TransKind) (tb :: TransKind) (m :: Type -> Type).
(MonadTransTunnel ta, MonadTransTunnel tb, Monad m) =>
ta (tb m) --> tb (ta m)
commuteT (ta (tb m) r -> tb (ta m) r) -> ta (tb m) r -> tb (ta m) r
forall a b. (a -> b) -> a -> b
$ (tb (ta m) --> ta (tb m)) -> ta (tb m) r
call tb (ta m) a -> ta (tb m) a
tb (ta m) --> ta (tb m)
forall (ta :: TransKind) (tb :: TransKind) (m :: Type -> Type).
(MonadTransTunnel ta, MonadTransTunnel tb, Monad m) =>
ta (tb m) --> tb (ta m)
commuteT

instance forall inner. MonadInner inner => MonadTransTunnel (ComposeInner inner) where
    type Tunnel (ComposeInner inner) = inner
    tunnel :: forall (m :: Type -> Type) r.
Monad m =>
((forall (m1 :: Type -> Type) a.
  Monad m1 =>
  ComposeInner inner m1 a -> m1 (Tunnel (ComposeInner inner) a))
 -> m (Tunnel (ComposeInner inner) r))
-> ComposeInner inner m r
tunnel (forall (m1 :: Type -> Type) a.
 Monad m1 =>
 ComposeInner inner m1 a -> m1 (Tunnel (ComposeInner inner) a))
-> m (Tunnel (ComposeInner inner) r)
call = m (Tunnel (ComposeInner inner) r)
-> ComposeInner (Tunnel (ComposeInner inner)) m r
forall (inner :: Type -> Type) (outer :: Type -> Type) a.
outer (inner a) -> ComposeInner inner outer a
MkComposeInner (m (Tunnel (ComposeInner inner) r)
 -> ComposeInner (Tunnel (ComposeInner inner)) m r)
-> m (Tunnel (ComposeInner inner) r)
-> ComposeInner (Tunnel (ComposeInner inner)) m r
forall a b. (a -> b) -> a -> b
$ (forall (m1 :: Type -> Type) a.
 Monad m1 =>
 ComposeInner inner m1 a -> m1 (Tunnel (ComposeInner inner) a))
-> m (Tunnel (ComposeInner inner) r)
call ComposeInner inner m1 a -> m1 (inner a)
ComposeInner inner m1 a -> m1 (Tunnel (ComposeInner inner) a)
forall (m1 :: Type -> Type) a.
Monad m1 =>
ComposeInner inner m1 a -> m1 (Tunnel (ComposeInner inner) a)
forall (inner :: Type -> Type) (outer :: Type -> Type) a.
ComposeInner inner outer a -> outer (inner a)
unComposeInner

class (MonadHoistIO m, MonadInner (TunnelIO m)) => MonadTunnelIO m where
    type TunnelIO m :: Type -> Type
    tunnelIO :: forall r. ((forall a. m a -> IO (TunnelIO m a)) -> IO (TunnelIO m r)) -> m r

hoistWithIO ::
       forall m f r. (MonadTunnelIO m, Traversable f)
    => (forall a. IO a -> IO (f a))
    -> m r
    -> m (f r)
hoistWithIO :: forall (m :: Type -> Type) (f :: Type -> Type) r.
(MonadTunnelIO m, Traversable f) =>
(forall a. IO a -> IO (f a)) -> m r -> m (f r)
hoistWithIO forall a. IO a -> IO (f a)
iifa m r
mr = ((forall a. m a -> IO (TunnelIO m a)) -> IO (TunnelIO m (f r)))
-> m (f r)
forall r.
((forall a. m a -> IO (TunnelIO m a)) -> IO (TunnelIO m r)) -> m r
forall (m :: Type -> Type) r.
MonadTunnelIO m =>
((forall a. m a -> IO (TunnelIO m a)) -> IO (TunnelIO m r)) -> m r
tunnelIO (((forall a. m a -> IO (TunnelIO m a)) -> IO (TunnelIO m (f r)))
 -> m (f r))
-> ((forall a. m a -> IO (TunnelIO m a)) -> IO (TunnelIO m (f r)))
-> m (f r)
forall a b. (a -> b) -> a -> b
$ \forall a. m a -> IO (TunnelIO m a)
tun -> (f (TunnelIO m r) -> TunnelIO m (f r))
-> IO (f (TunnelIO m r)) -> IO (TunnelIO m (f r))
forall a b. (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap f (TunnelIO m r) -> TunnelIO m (f r)
forall (t :: Type -> Type) (f :: Type -> Type) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: Type -> Type) a. Applicative f => f (f a) -> f (f a)
sequenceA (IO (f (TunnelIO m r)) -> IO (TunnelIO m (f r)))
-> IO (f (TunnelIO m r)) -> IO (TunnelIO m (f r))
forall a b. (a -> b) -> a -> b
$ IO (TunnelIO m r) -> IO (f (TunnelIO m r))
forall a. IO a -> IO (f a)
iifa (IO (TunnelIO m r) -> IO (f (TunnelIO m r)))
-> IO (TunnelIO m r) -> IO (f (TunnelIO m r))
forall a b. (a -> b) -> a -> b
$ m r -> IO (TunnelIO m r)
forall a. m a -> IO (TunnelIO m a)
tun m r
mr

instance MonadTunnelIO IO where
    type TunnelIO IO = Identity
    tunnelIO :: forall r.
((forall a. IO a -> IO (TunnelIO IO a)) -> IO (TunnelIO IO r))
-> IO r
tunnelIO (forall a. IO a -> IO (TunnelIO IO a)) -> IO (TunnelIO IO r)
call = (Identity r -> r) -> IO (Identity r) -> IO r
forall a b. (a -> b) -> IO a -> IO 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 (IO (Identity r) -> IO r) -> IO (Identity r) -> IO r
forall a b. (a -> b) -> a -> b
$ (forall a. IO a -> IO (TunnelIO IO a)) -> IO (TunnelIO IO r)
call ((forall a. IO a -> IO (TunnelIO IO a)) -> IO (TunnelIO IO r))
-> (forall a. IO a -> IO (TunnelIO IO a)) -> IO (TunnelIO IO r)
forall a b. (a -> b) -> a -> b
$ \IO a
ma -> (a -> TunnelIO IO a) -> IO a -> IO (TunnelIO IO a)
forall a b. (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Identity a
a -> TunnelIO IO a
forall a. a -> Identity a
Identity (IO a -> IO (TunnelIO IO a)) -> IO a -> IO (TunnelIO IO a)
forall a b. (a -> b) -> a -> b
$ IO a
ma

instance (MonadTransTunnel t, MonadTunnelIO m, MonadIO (t m)) => MonadTunnelIO (t m) where
    type TunnelIO (t m) = ComposeInner (Tunnel t) (TunnelIO m)
    tunnelIO :: forall r.
((forall a. t m a -> IO (TunnelIO (t m) a))
 -> IO (TunnelIO (t m) r))
-> t m r
tunnelIO (forall a. t m a -> IO (TunnelIO (t m) a)) -> IO (TunnelIO (t m) r)
call =
        ((forall (m1 :: Type -> Type) a.
  Monad m1 =>
  t m1 a -> m1 (Tunnel t a))
 -> m (Tunnel t r))
-> t m r
forall (m :: Type -> Type) r.
Monad m =>
((forall (m1 :: Type -> Type) a.
  Monad m1 =>
  t m1 a -> m1 (Tunnel t a))
 -> m (Tunnel t r))
-> t 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 =>
   t m1 a -> m1 (Tunnel t a))
  -> m (Tunnel t r))
 -> t m r)
-> ((forall (m1 :: Type -> Type) a.
     Monad m1 =>
     t m1 a -> m1 (Tunnel t a))
    -> m (Tunnel t r))
-> t m r
forall a b. (a -> b) -> a -> b
$ \forall (m1 :: Type -> Type) a.
Monad m1 =>
t m1 a -> m1 (Tunnel t a)
unlift -> ((forall a. m a -> IO (TunnelIO m a))
 -> IO (TunnelIO m (Tunnel t r)))
-> m (Tunnel t r)
forall r.
((forall a. m a -> IO (TunnelIO m a)) -> IO (TunnelIO m r)) -> m r
forall (m :: Type -> Type) r.
MonadTunnelIO m =>
((forall a. m a -> IO (TunnelIO m a)) -> IO (TunnelIO m r)) -> m r
tunnelIO (((forall a. m a -> IO (TunnelIO m a))
  -> IO (TunnelIO m (Tunnel t r)))
 -> m (Tunnel t r))
-> ((forall a. m a -> IO (TunnelIO m a))
    -> IO (TunnelIO m (Tunnel t r)))
-> m (Tunnel t r)
forall a b. (a -> b) -> a -> b
$ \forall a. m a -> IO (TunnelIO m a)
unliftIO -> (ComposeInner (Tunnel t) (TunnelIO m) r -> TunnelIO m (Tunnel t r))
-> IO (ComposeInner (Tunnel t) (TunnelIO m) r)
-> IO (TunnelIO m (Tunnel t r))
forall a b. (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ComposeInner (Tunnel t) (TunnelIO m) r -> TunnelIO m (Tunnel t r)
forall (inner :: Type -> Type) (outer :: Type -> Type) a.
ComposeInner inner outer a -> outer (inner a)
unComposeInner (IO (ComposeInner (Tunnel t) (TunnelIO m) r)
 -> IO (TunnelIO m (Tunnel t r)))
-> IO (ComposeInner (Tunnel t) (TunnelIO m) r)
-> IO (TunnelIO m (Tunnel t r))
forall a b. (a -> b) -> a -> b
$ (forall a. t m a -> IO (TunnelIO (t m) a)) -> IO (TunnelIO (t m) r)
call ((forall a. t m a -> IO (TunnelIO (t m) a))
 -> IO (TunnelIO (t m) r))
-> (forall a. t m a -> IO (TunnelIO (t m) a))
-> IO (TunnelIO (t m) r)
forall a b. (a -> b) -> a -> b
$ (TunnelIO m (Tunnel t a) -> ComposeInner (Tunnel t) (TunnelIO m) a)
-> IO (TunnelIO m (Tunnel t a))
-> IO (ComposeInner (Tunnel t) (TunnelIO m) a)
forall a b. (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap TunnelIO m (Tunnel t a) -> ComposeInner (Tunnel t) (TunnelIO m) a
forall (inner :: Type -> Type) (outer :: Type -> Type) a.
outer (inner a) -> ComposeInner inner outer a
MkComposeInner (IO (TunnelIO m (Tunnel t a))
 -> IO (ComposeInner (Tunnel t) (TunnelIO m) a))
-> (t m a -> IO (TunnelIO m (Tunnel t a)))
-> t m a
-> IO (ComposeInner (Tunnel t) (TunnelIO 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
. m (Tunnel t a) -> IO (TunnelIO m (Tunnel t a))
forall a. m a -> IO (TunnelIO m a)
unliftIO (m (Tunnel t a) -> IO (TunnelIO m (Tunnel t a)))
-> (t m a -> m (Tunnel t a))
-> t m a
-> IO (TunnelIO m (Tunnel t 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 m a -> m (Tunnel t a)
forall (m1 :: Type -> Type) a.
Monad m1 =>
t m1 a -> m1 (Tunnel t a)
unlift

instance (MonadTransTunnel t, TransConstraint MonadIO t) => TransConstraint MonadTunnelIO t where
    hasTransConstraint :: forall (m :: Type -> Type).
MonadTunnelIO m =>
Dict (MonadTunnelIO (t m))
hasTransConstraint = forall (c :: (Type -> Type) -> Constraint) (t :: TransKind)
       (m :: Type -> Type) (c' :: (Type -> Type) -> Constraint).
(TransConstraint c t, c m) =>
(c (t m) => Dict (c' (t m))) -> Dict (c' (t m))
withTransConstraintDict @MonadIO Dict (MonadTunnelIO (t m))
MonadIO (t m) => Dict (MonadTunnelIO (t m))
forall (a :: Constraint). a => Dict a
Dict