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

[oleg at pobox.com]

[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.