Singleraeh.Either

Documentation

data SEither sl sr elr where

Singleton Either.

Constructors

SLeft :: sl l -> SEither sl sr (Left l)

SRight :: sr r -> SEither sl sr (Right r)

Instances

(Demotable sl, Demotable sr) => Demotable (SEither sl sr :: Either l r -> Type)

Defined in Singleraeh.Either

Associated Types

type Demote (SEither sl sr)

Methods

demote :: forall (k1 :: k). SEither sl sr k1 -> Demote (SEither sl sr)

type Demote (SEither sl sr :: Either l r -> Type)

Defined in Singleraeh.Either

type Demote (SEither sl sr :: Either l r -> Type) = Either (Demote sl) (Demote sr)

demoteSEither :: forall dl dr sl sr elr. (forall l. sl l -> dl) -> (forall r. sr r -> dr) -> SEither sl sr elr -> Either dl dr

class SingEither (cl :: lk -> Constraint) (cr :: rk -> Constraint) (sl :: lk -> Type) (sr :: rk -> Type) (elr :: Either lk rk) where

Methods

singEither' :: (forall l. cl l => sl l) -> (forall r. cr r => sr r) -> SEither sl sr elr

Instances

cl l => SingEither (cl :: a -> Constraint) (cr :: rk -> Constraint) (sl :: a -> Type) (sr :: rk -> Type) ('Left l :: Either a rk)

Defined in Singleraeh.Either

Methods

singEither' :: (forall (l0 :: lk). cl l0 => sl l0) -> (forall (r :: rk0). cr r => sr r) -> SEither sl sr ('Left l)

cr r => SingEither (cl :: lk -> Constraint) (cr :: b -> Constraint) (sl :: lk -> Type) (sr :: b -> Type) ('Right r :: Either lk b)

Defined in Singleraeh.Either

Methods

singEither' :: (forall (l :: lk0). cl l => sl l) -> (forall (r0 :: rk). cr r0 => sr r0) -> SEither sl sr ('Right r)

singEither :: forall cl cr sl sr elr. SingEither cl cr sl sr elr => (forall l. cl l => sl l) -> (forall r. cr r => sr r) -> SEither sl sr elr