Control.Monad.Stack.Internal

Documentation

data ContTag

ContT is polykinded, which leads to issues checking that ContT ~ ContT!

Instances

type Pop ContTag (m :: Type -> Type)

Defined in Control.Monad.Stack.Cont

type Pop ContTag (m :: Type -> Type) = PopCont m

type family StackConstraints (n :: Nat) (c :: k) (cSucc :: k' -> Constraint) (m :: k') :: Constraint where ...

Equations

StackConstraints 0 c cSucc m = ()

StackConstraints n c cSucc m = (cSucc m, StackConstraints (n - 1) c cSucc (Pop c m))

type family IteratePop (n :: Nat) (c :: k) (m :: Type -> Type) :: Type -> Type where ...

Equations

IteratePop 0 c m = m

IteratePop n c m = IteratePop (n - 1) c (Pop c m)

type family Pop (c :: k) (m :: k') :: k'

Instances

type Pop ContTag (m :: Type -> Type)

Defined in Control.Monad.Stack.Cont

type Pop ContTag (m :: Type -> Type) = PopCont m

type Pop MaybeT (m :: Type -> Type)

Defined in Control.Monad.Stack.Fail

type Pop MaybeT (m :: Type -> Type) = PopFail m

type Pop ExceptT (m :: Type -> Type)

Defined in Control.Monad.Stack.Error

type Pop ExceptT (m :: Type -> Type) = PopError m

type Pop ReaderT (m :: Type -> Type)

Defined in Control.Monad.Stack.Reader

type Pop ReaderT (m :: Type -> Type) = PopReader m

type Pop StateT (m :: Type -> Type)

Defined in Control.Monad.Stack.State

type Pop StateT (m :: Type -> Type) = PopState m

type Pop WriterT (m :: Type -> Type)

Defined in Control.Monad.Stack.Writer

type Pop WriterT (m :: Type -> Type) = PopWriter m

type Pop AccumT (m :: Type -> Type)

Defined in Control.Monad.Stack.Accum

type Pop AccumT (m :: Type -> Type) = PopAccum m

type Pop SelectT (m :: Type -> Type)

Defined in Control.Monad.Stack.Select

type Pop SelectT (m :: Type -> Type) = PopSelect m

predNat :: forall n. KnownNat n => Either (n :~: 0) (Dict (KnownNat (n - 1)))

nonZeroNat :: forall n c cSucc m a. KnownNat (n - 1) => (IteratePop n c m a :~: IteratePop (n - 1) c (Pop c m) a, StackConstraints n c cSucc m :~: (cSucc m, StackConstraints (n - 1) c cSucc (Pop c m)))

depth :: forall n c cSucc m a. (KnownNat n, StackConstraints n c cSucc m) => (forall m. cSucc m => Pop c m a -> m a) -> IteratePop n c m a -> m a

module GHC.TypeNats