module Singleraeh.Either where

import Singleraeh.Demote
import Data.Kind ( Type, Constraint )

-- | Singleton 'Either'.
type SEither :: (l -> Type) -> (r -> Type) -> Either l r -> Type
data SEither sl sr elr where
    SLeft  :: sl l -> SEither sl sr (Left  l)
    SRight :: sr r -> SEither sl sr (Right r)

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 {l} {r} dl dr (sl :: l -> Type) (sr :: r -> Type)
       (elr :: Either l r).
(forall (l :: l). sl l -> dl)
-> (forall (r :: r). sr r -> dr)
-> SEither sl sr elr
-> Either dl dr
demoteSEither forall (l :: l). sl l -> dl
demoteSL forall (r :: r). sr r -> dr
demoteSR = \case
  SLeft  sl l
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 l -> dl
forall (l :: l). sl l -> dl
demoteSL sl l
sl
  SRight sr r
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 r -> dr
forall (r :: r). sr r -> dr
demoteSR sr r
sr

class SingEither (cl :: lk -> Constraint) (cr :: rk -> Constraint) (sl :: lk -> Type) (sr :: rk -> Type) (elr :: Either lk rk) where
    singEither'
        :: (forall l. cl l => sl l)
        -> (forall r. cr r => sr r)
        -> SEither sl sr elr

-- reordered types (hidden lk, rk because implied)
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
singEither :: forall {l} {r} (cl :: l -> Constraint) (cr :: r -> Constraint)
       (sl :: l -> Type) (sr :: r -> Type) (elr :: Either l r).
SingEither cl cr sl sr elr =>
(forall (l :: l). cl l => sl l)
-> (forall (r :: r). cr r => sr r) -> SEither sl sr elr
singEither = forall {l} {r} (cl :: l -> Constraint) (cr :: r -> Constraint)
       (sl :: l -> Type) (sr :: r -> Type) (elr :: Either l r).
SingEither cl cr sl sr elr =>
(forall (l :: l). cl l => sl l)
-> (forall (r :: r). cr r => sr r) -> SEither sl sr elr
singEither' @_ @_ @cl @cr

instance cl l => SingEither cl cr sl sr (Left  l) where
    singEither' :: (forall (l :: a). cl l => sl l)
-> (forall (r :: rk). cr r => sr r) -> SEither sl sr ('Left l)
singEither'  forall (l :: a). cl l => sl l
singL forall (r :: rk). cr r => sr r
_singR = sl l -> SEither sl sr ('Left l)
forall {l} {r} (sl :: l -> Type) (r :: l) (sr :: r -> Type).
sl r -> SEither sl sr ('Left r)
SLeft  sl l
forall (l :: a). cl l => sl l
singL
instance cr r => SingEither cl cr sl sr (Right r) where
    singEither' :: (forall (l :: lk). cl l => sl l)
-> (forall (r :: b). cr r => sr r) -> SEither sl sr ('Right r)
singEither' forall (l :: lk). cl l => sl l
_singL  forall (r :: b). cr r => sr r
singR = sr r -> SEither sl sr ('Right r)
forall {r} {l} (sr :: r -> Type) (r :: r) (sl :: l -> Type).
sr r -> SEither sl sr ('Right r)
SRight sr r
forall (r :: b). cr r => sr r
singR

instance (Demotable sl, Demotable sr) => Demotable (SEither sl sr) where
    type Demote (SEither sl sr) = Either (Demote sl) (Demote sr)
    demote :: forall (k1 :: Either l r).
SEither sl sr k1 -> Demote (SEither sl sr)
demote = (forall (l :: l). sl l -> Demote sl)
-> (forall (r :: r). sr r -> Demote sr)
-> SEither sl sr k1
-> Either (Demote sl) (Demote sr)
forall {l} {r} dl dr (sl :: l -> Type) (sr :: r -> Type)
       (elr :: Either l r).
(forall (l :: l). sl l -> dl)
-> (forall (r :: r). sr r -> dr)
-> SEither sl sr elr
-> Either dl dr
demoteSEither sl l -> Demote sl
forall (l :: l). sl l -> Demote sl
forall k (sk :: k -> Type) (k1 :: k).
Demotable sk =>
sk k1 -> Demote sk
demote sr r -> Demote sr
forall (r :: r). sr r -> Demote sr
forall k (sk :: k -> Type) (k1 :: k).
Demotable sk =>
sk k1 -> Demote sk
demote