John Meacham wrote:

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.

Perhaps the enclosed code might be of help. Tests: test1 = TyCon "Int" *Forall> :t test1 test1 :: Type FANil test2 = Forall ["a"] (Fun (TyVar "a") (TyVar "a")) *Forall> :t test2 test2 :: Type FATop -- Inferred type! test3 = Fun test2 test1 *Forall> :t test3 test3 :: Type FASomewhere test3' = Fun test1 test1 *Forall> :t test3' test3' :: Type FANil test4 = Forall ["b"] test3 *Forall> :t test4 test4 :: Type FATop test4' = Forall ["b"] test2 -- Error! No instance for (RhoC FATop) arising from use of `Forall' at /tmp/m.hs:43:9-14 That is, in test4, the second argument of Forall is not of the type rho! Typeclasses would work too. I'm lacking a good example to show off this machinery... {-# OPTIONS -fglasgow-exts #-} module Forall where data FANil data FATop data FASomewhere type Id = String type Tau = Type FANil data Type a where Forall :: (RhoC a) => [Id] -> Type a -> Type FATop Fun :: (FAMerge a b c) => Type a -> Type b -> Type c TyCon :: Id -> Type FANil TyVar :: Id -> Type FANil type Sigma a = Type a --type (RhoC a) => Rho a = Type a -- I wish that worked... class RhoC a instance RhoC FANil instance RhoC FASomewhere class FAMerge a b c | a b -> c instance FAMerge FANil FANil FANil instance FAMerge FANil FASomewhere FASomewhere instance FAMerge FANil FATop FASomewhere instance FAMerge FATop a FASomewhere instance FAMerge FASomewhere a FASomewhere test1 = TyCon "Int" test2 = Forall ["a"] (Fun (TyVar "a") (TyVar "a")) test3 = Fun test2 test1 test3' = Fun test1 test1 -- I guess we need to hide the data constructors of Type and use -- functions like rho, fun, tycon, etc. to construct the values of -- Type rho :: (RhoC a) => Type a -> Type a rho = id test4 = Forall ["b"] test3 -- The following is error! --test4' = Forall ["b"] test2