| 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