module Singleraeh.Bool where

import Data.Kind ( Type )
import Singleraeh.Demote

-- | Singleton 'Bool'.
type SBool :: Bool -> Type
data SBool b where
    STrue  :: SBool True
    SFalse :: SBool False

demoteSBool :: SBool b -> Bool
demoteSBool :: forall (b :: Bool). SBool b -> Bool
demoteSBool = \case SBool b
STrue -> Bool
True; SBool b
SFalse -> Bool
False

instance Demotable SBool where
    type Demote SBool = Bool
    demote :: forall (k1 :: Bool). SBool k1 -> Demote SBool
demote = SBool k1 -> Bool
SBool k1 -> Demote SBool
forall (b :: Bool). SBool b -> Bool
demoteSBool

class SingBool (b :: Bool) where singBool :: SBool b
instance SingBool True  where singBool :: SBool 'True
singBool = SBool 'True
STrue
instance SingBool False where singBool :: SBool 'False
singBool = SBool 'False
SFalse