    {-# LANGUAGE TypeFamilies          #-}
    {-# LANGUAGE EmptyDataDecls        #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    module TypeLevel.Boolean ( True
                         , False
                           -- * Boolean operations
                         , Not
                         , notT
                         , And
                         , andT
                         , Or
                         , orT
                         , Xor
                         , xorT
                         ) where

    import TypeLevel.Reify

    -- | Data type for truth
    data True
    -- | Data type for false.
    data False

    instance Show False where show :: False -> String
    show False
    _ = String
    "False"
    instance Show True  where show :: True -> String
    show True
    _ = String
    "True"

    instance Reify True  Bool where witness :: Witness True Bool
    witness = Bool -> Witness True Bool
    forall t a. a -> Witness t a
    Witness Bool
    True
    instance Reify False Bool where witness :: Witness False Bool
    witness = Bool -> Witness False Bool
    forall t a. a -> Witness t a
    Witness Bool
    False

    ----------------------------------------------------------------
    -- | Negation

    type family Not a :: *

    notT :: a -> Not a
    notT :: forall a. a -> Not a
    notT a
    _ = Not a
    forall a. HasCallStack => a
    undefined

    type instance Not False = True
    type instance Not True  = False

    ----------------------------------------------------------------
    -- | And for boolean types
    type family And a b :: *

    andT :: a -> b -> And a b
    andT :: forall a b. a -> b -> And a b
    andT a
    _ b
    _ = And a b
    forall a. HasCallStack => a
    undefined

    type instance And False False = False
    type instance And False True  = False
    type instance And True  False = False
    type instance And True  True  = True

    ----------------------------------------------------------------
    -- | Or for boolean types
    type family Or a b :: *

    orT :: a -> b -> Or a b
    orT :: forall a b. a -> b -> Or a b
    orT a
    _ b
    _ = Or a b
    forall a. HasCallStack => a
    undefined

    type instance Or False False = True
    type instance Or False True  = True
    type instance Or True  False = True
    type instance Or True  True  = False

    ----------------------------------------------------------------
    -- | Exlusive or for boolean types
    type family Xor a b :: *

    xorT :: a -> b -> Xor a b
    xorT :: forall a b. a -> b -> Xor a b
    xorT a
    _ b
    _ = Xor a b
    forall a. HasCallStack => a
    undefined

    type instance Xor False False = False
    type instance Xor False True  = True
    type instance Xor True  False = True
    type instance Xor True  True  = False