GADT typechecking and existentials

typecheck.hs

{-# LANGUAGE GADTs, StandaloneDeriving, TypeOperators, ExistentialQuantification, EmptyCase #-}

import Data.Type.Equality
import Data.Void

data UTerm = UTrue
      | UFalse
      | UIf UTerm UTerm UTerm
      | UZero
      | USucc UTerm
      | UIsZero UTerm
    deriving (Show)

data TTerm a where
  TTrue :: TTerm Bool
  TFalse :: TTerm Bool
  TIf :: TTerm Bool -> TTerm a -> TTerm a -> TTerm a
  TZero :: TTerm Int
  TSucc :: TTerm Int -> TTerm Int
  TIsZero :: TTerm Int -> TTerm Bool

deriving instance Show (TTerm a)

data Type a where
    TInt :: Type Int
    TBool :: Type Bool

deriving instance Show (Type a)

data ETerm = forall a b. (a ~ b) => ETerm (Type a) (TTerm b)

deriving instance Show ETerm

typeEq :: Type a -> Type b -> Maybe (a :~: b)
typeEq TInt TInt = Just Refl
typeEq TBool TBool = Just Refl
typeEq _ _ = Nothing

typeEq2 :: Type a -> Type b -> Either (a :~: b) ((a :~: b) -> Void)
typeEq2 TBool TBool = Left Refl
typeEq2 TInt TInt = Left Refl
typeEq2 _ _ = Right (\eq -> case eq of)

typecheck :: UTerm -> Maybe ETerm
typecheck UTrue = Just $ ETerm TBool TTrue
typecheck UFalse = Just $ ETerm TBool TFalse
typecheck UZero = Just $ ETerm TInt TZero 
typecheck (USucc a) = do
    (ETerm TInt a') <- typecheck a
    return $ ETerm TInt (TSucc a')
typecheck (UIsZero a) = do
    (ETerm TInt a') <- typecheck a
    return $ ETerm TBool (TIsZero a')
typecheck (UIf ucond ut uf) = do
    (ETerm TBool tcond) <- typecheck ucond
    (ETerm tyt tt) <- typecheck ut
    (ETerm tyf tf) <- typecheck uf
    -- pattern match will fail and we'll get Nothing if tyt (the type of the
    -- true branch) and tyf (the type of the false branch) aren't equal
    Refl <- typeEq tyt tyf
    return $ ETerm tyt (TIf tcond tt tf)


reduce :: TTerm a -> TTerm a
reduce TTrue = TTrue
reduce TFalse = TFalse
reduce TZero = TZero
reduce (TSucc a) = TSucc $ reduce a
reduce (TIf TTrue t _) = t
reduce (TIf TFalse _ f) = f
reduce (TIf cond t f) = TIf (reduce cond) t f
reduce (TIsZero TZero) = TTrue
reduce (TIsZero (TSucc _)) = TFalse
reduce (TIsZero a) = TIsZero (reduce a)

eReduce :: ETerm -> ETerm
eReduce (ETerm t a) = ETerm t (reduce a)