[Haskell] generalised algebraic data types, existential types, and phantom types

I briefly skimmed the paper mentioned in a recent mailing on the ghc-users list that describes generalised algebraic data types (http://research.microsoft.com/Users/simonpj/papers/gadt/index.htm); my reaction can be summed up as "nifty!". I was curious to see if I could implement anything similar in current haskell, and ended up with the attached code. The main point of interest for me is the combination of phantom types and existential types; I'd never had the need to combine the two before. Is there any closer approximation possible? My code is close, but the type-safety isn't checked by the compiler (although it should be safe, if only the smart constructors are used), and it has that extra "Typeable" constraint. Abe