Polysemy.Internal.Bundle

Documentation

class KnownList (l :: [k]) where

A class for type-level lists with a known spine.

This constraint is eventually satisfied as r is instantied to a concrete list.

Methods

unconsKnownList :: (l ~ '[] => a) -> (forall x r. (l ~ (x ': r), KnownList r) => Proxy x -> Proxy r -> a) -> a

Instances

KnownList ('[] :: [k])

Defined in Polysemy.Internal.Bundle

Methods

unconsKnownList :: ('[] ~ '[] => a) -> (forall (x :: k0) (r :: [k0]). ('[] ~ (x ': r), KnownList r) => Proxy x -> Proxy r -> a) -> a

KnownList r => KnownList (x ': r :: [k])

Defined in Polysemy.Internal.Bundle

Methods

unconsKnownList :: ((x ': r) ~ '[] => a) -> (forall (x0 :: k0) (r0 :: [k0]). ((x ': r) ~ (x0 ': r0), KnownList r0) => Proxy x0 -> Proxy r0 -> a) -> a

extendMembership :: forall r r' e. ElemOf e r -> ElemOf e (Append r r')

subsumeMembership :: forall r r' e. Members r r' => ElemOf e r -> ElemOf e r'

weakenList :: forall r' r m a. KnownList r' => Union r m a -> Union (Append r' r) m a

type family Append l r where ...

Equations

Append (a ': l) r = a ': Append l r

Append '[] r = r