module Control.Monad.Levels
(
MonadTower_(..)
, MonadTower
, MonadLevel_(..)
, MonadLevel
, Unwrapper
, LowerMonadValue
, WithLower
, CanUnwrap
, CanUnwrapSelf
, WithLowerC
, AddInternalM(..)
, CanAddInternalM
, AddIM(..)
, AddInternal(..)
, CanAddInternal
, AddI(..)
, AddIdent(..)
, GetInternal(..)
, CanGetInternal
, AddIG(..)
, lift
, IsBaseMonad
, HasBaseMonad
, liftBase
, BaseMonadOf
, liftIO
, HasTransformer
, TransformedMonad
, liftT
) where
import Control.Monad.Levels.Constraints
import Control.Monad.Levels.Definitions
import Control.Monad.Levels.Transformers
import Data.Constraint ((\\))
lift :: forall m a. (MonadLevel m) => LowerMonad m a -> m a
lift lm = wrap a (\ _unwrap addI -> addInternalM addI lm) \\ proofInst m a
where
m :: Proxy m
m = Proxy
a :: Proxy a
a = Proxy
type HasBaseMonad m = SatisfyConstraint IsBaseMonad m
liftBase :: (HasBaseMonad m) => BaseMonad m a -> m a
liftBase m = liftSat (Proxy :: Proxy IsBaseMonad) m
type BaseMonadOf b m = (HasBaseMonad m, BaseMonad m ~ b, b ~ BaseMonad m)
liftIO :: (BaseMonadOf IO m) => IO a -> m a
liftIO = liftBase