Florian Lorenzen wrote:
typecheck :: Exp -> Maybe (Term t) typecheck exp = <...>
Now, I'd like to have a function that returns the GADT value corresponding to `exp' if `exp' is type correct.
Let us examine that type: typecheck :: forall t. Exp -> Maybe (Term t) Do you really mean that given expression exp, (typecheck exp) should return a (Maybe (Term t)) value for any t whatsoever? In other words, you are interested in a type-*checking* problem: given an expression _and_ given a type, return Just (Term t) if the given expression has the given type. Both expression and the type are the input. Incidentally, this problem is like `read': we give the read function a string and we should tell it to which type to parse. If that is what you mean, then the solution using Typeable will work (although you may prefer avoiding Typeable -- in which case you should build type witnesses on your own).
that returns the GADT value corresponding to `exp' if `exp' is type correct. Your comment suggests that you mean typecheck exp should return (Just term) just in case `exp' is well-typed, that is, has _some_ type. The English formulation of the problem already points us towards an existential. The typechecking function should return (Just term) and a witness of its type:
typecheck :: Exp -> Sigma (t:Type) (Term t) Then my
data TypedTerm = forall ty. (Typ ty) (Term ty)
is an approximation of the Sigma type. As Erik Hesselink rightfully pointed out, this type does not preclude type transformation functions. Indeed you have to unpack and then repack. If you want to know the concrete type, you can pattern-match on the type witness (Typ ty), to see if the inferred type is an Int, for example. Chances are that you wanted the following typecheck :: {e:Exp} -> Result e where Result e has the type (Just (Term t)) (with some t dependent on e) if e is typeable, and Nothing otherwise. But this is a dependent function type (Pi-type). No wonder we have to go through contortions like Template Haskell to emulate dependent types in Haskell. Haskell was not designed to be a dependently-typed language.