{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE Safe #-}
module Copilot.Theorem.TransSys.Type
( Type (..)
, U (..)
) where
import Data.Type.Equality
data Type a where
Bool :: Type Bool
Integer :: Type Integer
Real :: Type Double
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
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"