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


-- | Type level literals, inspired by GHC.TypeLits.

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 :: forall (b :: Bool). SBool b -> Bool
eraseSBool = \case
  SBool b
STrue  -> Bool
True
  SBool b
SFalse -> Bool
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 :: SBool 'True
boolSing = SBool 'True
STrue

instance KnownBool 'False where
  boolSing :: SBool 'False
boolSing = SBool 'False
SFalse

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