    {-# LANGUAGE ExistentialQuantification #-}
    {-# LANGUAGE GADTs                     #-}
    {-# LANGUAGE Safe                      #-}

    -- | Types suported by the modular transition systems.
    module Copilot.Theorem.TransSys.Type
      ( Type (..)
      , U (..)
      ) where

    import Data.Type.Equality

    -- | A type at both value and type level.
    --
    -- Real numbers are mapped to 'Double's.
    data Type a where
      Bool    :: Type Bool
      Integer :: Type Integer
      Real    :: Type Double

    -- | Proofs of type equality.
    instance TestEquality Type where
      testEquality :: forall a b. Type a -> Type b -> Maybe (a :~: b)
    testEquality Type a
    Bool    Type b
    Bool     = (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    Just a :~: a
    a :~: b
    forall {k} (a :: k). a :~: a
    Refl
      testEquality Type a
    Integer Type b
    Integer  = (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    Just a :~: a
    a :~: b
    forall {k} (a :: k). a :~: a
    Refl
      testEquality Type a
    Real    Type b
    Real     = (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    Just a :~: a
    a :~: b
    forall {k} (a :: k). a :~: a
    Refl
      testEquality Type a
    _       Type b
    _        = Maybe (a :~: b)
    forall a. Maybe a
    Nothing

    -- | Unknown types.
    --
    -- For instance, 'U Expr' is the type of an expression of unknown type
    data U f = forall t . U (f t)

    instance Show (Type t) where
      show :: Type t -> String
    show Type t
    Integer = String
    "Int"
      show Type t
    Bool    = String
    "Bool"
      show Type t
    Real    = String
    "Real"