{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
module Language.Symantic.Lib.Data.Bool where

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

-- * Class 'IBool'
-- | Implicitely construct a 'SBool' from a type of kind 'Bool'.
class    IBool b      where iBool :: SBool b
instance IBool 'True  where iBool = STrue
instance IBool 'False where iBool = SFalse

-- * Type family 'HEq'
-- | Host-type equality.
type family HEq x y :: Bool where
	HEq x x = 'True
	HEq x y = 'False