Safe Haskell	None
Language	Haskell2010

Control.Monad.Stack.Internal

Synopsis

data ContTag
type family StackConstraints (n :: Nat) (c :: k) (cSucc :: k' -> Constraint) (m :: k') :: Constraint where ...
type family IteratePop (n :: Nat) (c :: k) (m :: Type -> Type) :: Type -> Type where ...
type family Pop (c :: k) (m :: k') :: k'
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

Documentation

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

Instances

type Pop ContTag (m :: Type -> Type) Source #
Instance details 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 ... Source #

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 ... Source #

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' Source #

Instances

type Pop ContTag (m :: Type -> Type) Source #
Instance details Defined in Control.Monad.Stack.Cont type Pop ContTag (m :: Type -> Type) = PopCont m
type Pop MaybeT (m :: Type -> Type) Source #
Instance details Defined in Control.Monad.Stack.Fail type Pop MaybeT (m :: Type -> Type) = PopFail m
type Pop ExceptT (m :: Type -> Type) Source #
Instance details Defined in Control.Monad.Stack.Error type Pop ExceptT (m :: Type -> Type) = PopError m
type Pop ReaderT (m :: Type -> Type) Source #
Instance details Defined in Control.Monad.Stack.Reader type Pop ReaderT (m :: Type -> Type) = PopReader m
type Pop StateT (m :: Type -> Type) Source #
Instance details Defined in Control.Monad.Stack.State type Pop StateT (m :: Type -> Type) = PopState m
type Pop WriterT (m :: Type -> Type) Source #
Instance details Defined in Control.Monad.Stack.Writer type Pop WriterT (m :: Type -> Type) = PopWriter m
type Pop AccumT (m :: Type -> Type) Source #
Instance details Defined in Control.Monad.Stack.Accum type Pop AccumT (m :: Type -> Type) = PopAccum m
type Pop SelectT (m :: Type -> Type) Source #
Instance details Defined in Control.Monad.Stack.Select type Pop SelectT (m :: Type -> Type) = PopSelect m

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))) Source #

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 Source #