{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
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)