[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. _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
