I'd like to transform a value of an ADT to a GADT. Suppose I have the
simple expression language

> data Exp = Lit Int > | Succ Exp > | IsZero Exp > | If Exp Exp Exp

and the GADT

> data Term t where > TLit :: Int -> Term Int > TSucc :: Term Int ->
Term Int > TIsZero :: Term Int -> Term Bool > TIf :: Term Bool -> Term
ty -> Term ty -> Term ty

that encodes the typing rules.

Now, I'd like to have a function

> typecheck :: Exp -> Maybe (Term t) > typecheck exp = <...>

that returns the GADT value corresponding to `exp' if `exp' is type
correct.

It's not pretty, but it should still be safe...

import Control.Applicative

import Unsafe.Coerce

tcInt :: Exp -> Maybe (Term Int)

tcInt (Lit i) = pure (TLit i)

tcInt (Succ e) = TSucc <$> tcInt e

tcInt (If c e1 e2) = TIf <$> tcBool c <*> tcInt e1 <*> tcInt e2

tcInt _ = empty

tcBool :: Exp -> Maybe (Term Bool)

tcBool (IsZero e) = TIsZero <$> tcInt e

tcBool (If c e1 e2) = TIf <$> tcBool c <*> tcBool e1 <*> tcBool e2

tcBool _ = empty

typecheck :: Exp -> Maybe (Term t)

typecheck e = forget <$> tcInt e <|> forget <$> tcBool e

where

forget :: Term a -> Term b

forget = unsafeCoerce

Regards,

Sean