module Singleraeh.Either where

import Data.Kind ( Type )

-- | Singleton 'Either'.
type SEither :: (a -> Type) -> (b -> Type) -> Either a b -> Type
data SEither sa sb eab where
    SLeft  :: sa a -> SEither sa sb (Left  a)
    SRight :: sb b -> SEither sa sb (Right b)

demoteSEither
    :: forall dl dr sl sr elr
    .  (forall l. sl l -> dl)
    -> (forall r. sr r -> dr)
    -> SEither sl sr elr
    -> Either dl dr
demoteSEither :: forall {a} {b} dl dr (sl :: a -> Type) (sr :: b -> Type)
       (elr :: Either a b).
(forall (l :: a). sl l -> dl)
-> (forall (r :: b). sr r -> dr)
-> SEither sl sr elr
-> Either dl dr
demoteSEither forall (l :: a). sl l -> dl
demoteSL forall (r :: b). sr r -> dr
demoteSR = \case
  SLeft  sl a
sl -> dl -> Either dl dr
forall a b. a -> Either a b
Left  (dl -> Either dl dr) -> dl -> Either dl dr
forall a b. (a -> b) -> a -> b
$ sl a -> dl
forall (l :: a). sl l -> dl
demoteSL sl a
sl
  SRight sr b
sr -> dr -> Either dl dr
forall a b. b -> Either a b
Right (dr -> Either dl dr) -> dr -> Either dl dr
forall a b. (a -> b) -> a -> b
$ sr b -> dr
forall (r :: b). sr r -> dr
demoteSR sr b
sr