    {-# 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)