On Fri, Dec 23, 2005 at 03:34:40AM -0000, oleg@pobox.com wrote:
[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 ())
I just checked that the only required change is the one in type signature. But I can't explain it at this moment. Best regards Tomasz -- I am searching for a programmer who is good at least in some of [Haskell, ML, C++, Linux, FreeBSD, math] for work in Warsaw, Poland