[Haskell-cafe] GADT question

[John Meacham]

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⑈