[Haskell] Re: A question about fundeps <-> GADT interaction

[Sorry for possible duplication, our DNS server seems to be broken, and the sysadm is on vacation] I don't think that is the problem with GADTs. The following works

untype :: Term f a -> Term Untyped () untype (Lit x) = Lit x untype (Succ t) = Succ (untype t) untype (IsZero t) = IsZero ((untype t)::Term Untyped ()) untype (If c t e) = If ((untype c)::Term Untyped ()) ((untype t)::Term Untyped ()) ((untype e)::Term Untyped ())

Here's a more extensive example:

tlit :: Int->Term Typed Int tlit = Lit

[l0,l1,l2] = map tlit [0..]

--ex2 :: Term Untyped () ex2' = If (IsZero (Succ (Lit 0))) (untype l1) (IsZero (untype l2))

ex2' of course won't typecheck if `untype' are removed.