# LANGUAGE KindSignatures #
{-# LANGUAGE DataKinds      #-}
# LANGUAGE GADTs           #


  | Type level literals , inspired by  .

module Agda.Utils.TypeLits where

-- | Singleton for type level booleans.

data SBool (b :: Bool) where
  STrue  :: SBool 'True
  SFalse :: SBool 'False

eraseSBool :: SBool b -> Bool
eraseSBool b = case b of
  STrue  -> True
  SFalse -> False

-- | A known boolean is one we can obtain a singleton for.
--   Concrete values are trivially known.

class KnownBool (b :: Bool) where
  boolSing :: SBool b

instance KnownBool 'True where
  boolSing = STrue

instance KnownBool 'False where
  boolSing = SFalse

boolVal :: forall proxy b. KnownBool b => proxy b -> Bool
boolVal _ = eraseSBool (boolSing :: SBool b)

# LANGUAGE DataKinds      #
 | Singleton for type level booleans.
 | A known boolean is one we can obtain a singleton for.
   Concrete values are trivially known.
# LANGUAGE KindSignatures #
# LANGUAGE GADTs           #


  | Type level literals , inspired by  .

module Agda.Utils.TypeLits where


data SBool (b :: Bool) where
  STrue  :: SBool 'True
  SFalse :: SBool 'False

eraseSBool :: SBool b -> Bool
eraseSBool b = case b of
  STrue  -> True
  SFalse -> False


class KnownBool (b :: Bool) where
  boolSing :: SBool b

instance KnownBool 'True where
  boolSing = STrue

instance KnownBool 'False where
  boolSing = SFalse

boolVal :: forall proxy b. KnownBool b => proxy b -> Bool
boolVal _ = eraseSBool (boolSing :: SBool b)
