I have been trying to learn GADTs but feel I don't quite grok them yet. I am playing with an implementation of SPJ's algorithm from http://research.microsoft.com/Users/simonpj/papers/higher-rank/index.htm in it, he has a data type that represents a type, but with several special cases that can't easily be expressed in haskell proper. I was thinking GADTs might help but havn't been able to come up with something good and was hoping someone could point me in the right direction or let me know what I am trying to do is impossible/improbable. right now, it looks like so data Type = ForAll [TyVar] Rho -- Forall type | Fun Type Type -- Function type | TyCon TyCon -- Type constants | TyVar TyVar -- Always bound by a ForAll with the three synonyms and their constraints being type Sigma = Type type Rho = Type -- No top-level ForAll type Tau = Type -- No ForAlls anywhere I would like the type system to distinguish the three types and enforce their properties. so far, I have come up with the following: data Sigma data Tau data Rho data Type a where ForAll :: [Id] -> Type Rho -> Type Sigma Fun :: Type a -> Type a -> Type a TyCon :: TyCon -> Type Tau TyVar :: TyVar -> Type Tau but this is obviously not right, it can't create Rho types at all, Fun should change a Sigma into a Rho but leave Tau the same, Fun should be able to be applied to different types infering the correct one. and a function that accepts a Rho should be able to accept a Tau... (though explicit upconversions would be okay, meaning I need to create TyCons for example with type 'Type Rho' in the upconverter) anyone have any ideas on how to make this work? is this even possible to express with GADTs? John -- John Meacham - ⑆repetae.net⑆john⑈