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

import Control.Monad.Ology.General.Extract
import Control.Monad.Ology.General.Function
import Control.Monad.Ology.General.IO
import Control.Monad.Ology.General.Identity
import Control.Monad.Ology.General.Outer
import Control.Monad.Ology.General.Trans.Constraint
import Control.Monad.Ology.General.Trans.Trans
import Control.Monad.Ology.General.Trans.Tunnel
import Control.Monad.Ology.General.Trans.Unlift
import Control.Monad.Ology.Specific.ComposeOuter
import Import

-- | A transformer that has no effects (such as state change or output).
class MonadTransUnlift t => MonadTransAskUnlift t where
    askUnlift ::
           forall m. Monad m
        => t m (WUnlift Monad t)
    default askUnlift :: forall m. (MonadIdentity (Tunnel t), Monad m) => t m (WUnlift Monad t)
    askUnlift = 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 =>
t m1 a -> m1 (Tunnel t a)
unlift -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a. Applicative f => a -> f a
pure 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
$ \t m a
tma -> forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (m :: Type -> Type). MonadExtract m => Extract m
mToValue forall a b. (a -> b) -> a -> b
$ forall (m1 :: Type -> Type) a.
Monad m1 =>
t m1 a -> m1 (Tunnel t a)
unlift t m a
tma

-- | A monad that has no effects over IO (such as state change or output).
class MonadUnliftIO m => MonadAskUnliftIO m where
    askUnliftIO :: m (WRaised m IO)
    askUnliftIO = forall (m :: Type -> Type) r.
MonadTunnelIO m =>
((forall a. m a -> IO (TunnelIO m a)) -> IO (TunnelIO m r)) -> m r
tunnelIO forall a b. (a -> b) -> a -> b
$ \forall a. m a -> IO (TunnelIO m a)
unlift -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall k (p :: k -> Type) (q :: k -> Type).
(p --> q) -> WRaised p q
MkWRaised forall a b. (a -> b) -> a -> b
$ \m a
ma -> forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (m :: Type -> Type). MonadExtract m => Extract m
mToValue forall a b. (a -> b) -> a -> b
$ forall a. m a -> IO (TunnelIO m a)
unlift m a
ma

instance MonadAskUnliftIO IO where
    askUnliftIO :: IO (WRaised IO IO)
askUnliftIO = forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k (p :: k -> Type) (q :: k -> Type).
(p --> q) -> WRaised p q
MkWRaised forall {k} (cat :: k -> k -> Type) (a :: k).
Category cat =>
cat a a
id

instance (MonadTransAskUnlift t, MonadAskUnliftIO m, MonadFail (t m), MonadIO (t m), MonadFix (t m)) =>
             MonadAskUnliftIO (t m) where
    askUnliftIO :: t m (WRaised (t m) IO)
askUnliftIO = do
        MkWUnlift Unlift Monad t
unlift <- forall (t :: TransKind) (m :: Type -> Type).
(MonadTransAskUnlift t, Monad m) =>
t m (WUnlift Monad t)
askUnlift
        MkWRaised m --> IO
unliftIO <- forall (t :: TransKind) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: Type -> Type). MonadAskUnliftIO m => m (WRaised m IO)
askUnliftIO
        forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k (p :: k -> Type) (q :: k -> Type).
(p --> q) -> WRaised p q
MkWRaised forall a b. (a -> b) -> a -> b
$ m --> IO
unliftIO forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Unlift Monad t
unlift

instance MonadTransAskUnlift t => TransConstraint MonadAskUnliftIO t where
    hasTransConstraint :: forall (m :: Type -> Type).
MonadAskUnliftIO m =>
Dict (MonadAskUnliftIO (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 @MonadFail forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ 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 @MonadFix forall a b. (a -> b) -> a -> b
$ forall (a :: Constraint). a => Dict a
Dict

instance MonadOuter outer => MonadTransAskUnlift (ComposeOuter outer)

contractT ::
       forall (t :: TransKind) m. (MonadTransAskUnlift t, Monad m)
    => t (t m) --> t m
contractT :: forall (t :: TransKind) (m :: Type -> Type).
(MonadTransAskUnlift t, Monad m) =>
t (t m) --> t m
contractT t (t m) a
ttma =
    case forall (c :: (Type -> Type) -> Constraint) (t :: TransKind)
       (m :: Type -> Type).
(TransConstraint c t, c m) =>
Dict (c (t m))
hasTransConstraint @Monad @t @m of
        Dict (Monad (t m))
Dict -> do
            MkWUnlift Unlift Monad t
unlift <- forall (t :: TransKind) (m :: Type -> Type).
(MonadTransAskUnlift t, Monad m) =>
t m (WUnlift Monad t)
askUnlift
            Unlift Monad t
unlift t (t m) a
ttma

contractTBack ::
       forall (t :: TransKind) m. (MonadTransAskUnlift t, Monad m)
    => t (t m) -/-> t m
contractTBack :: forall (t :: TransKind) (m :: Type -> Type).
(MonadTransAskUnlift t, Monad m) =>
t (t m) -/-> t m
contractTBack (t m --> t (t m)) -> t (t m) r
call =
    case forall (c :: (Type -> Type) -> Constraint) (t :: TransKind)
       (m :: Type -> Type).
(TransConstraint c t, c m) =>
Dict (c (t m))
hasTransConstraint @Monad @t @m of
        Dict (Monad (t m))
Dict -> forall (t :: TransKind) (m :: Type -> Type).
(MonadTransAskUnlift t, Monad m) =>
t (t m) --> t m
contractT forall a b. (a -> b) -> a -> b
$ (t m --> t (t m)) -> t (t m) r
call forall (t :: TransKind) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift