[Haskell-cafe] GADT question

[Simon Peyton-Jones]

| 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

It looks as if you want a kind of subtyping relationship, so that Tau <
Rho < Sigma.  The standard way to achieve that is using polymorphism
(see, for example, papers about FFI to object-oriented languages)

data Sigma a = S a
data Rho a = R a
data Tau = Tau

data Type a where
|     ForAll :: [Id] -> Type (Sigma (Rho a)) -> Type (Sigma b)
|     Fun :: Type a -> Type a -> Type a
|     TyCon :: TyCon -> Type (Sigma (Rho Tau))
|     TyVar :: TyVar -> Type (Sigma (Rho Tau))

I'm not sure if this would work.

Simon