Apologies for the double-reply... Your mail prompted me to finally get around to adding a mono/polytype system to an interpreter I've been working on for pure type systems, to see what a GHC-alike type system would look like. Here's what I came up with. Constants are: *m, []m, *p and []p Axioms are: *m : []m, *p : []p Rules go as follows: (*m,*m,*m) This is obvious, because it allows normal functions. ([]m,[]m,[]m) This gives arbitrary order type constructors (that is, it expands the m-kinds to km ::= *m | km -> km) ([]m,*m,*p) ([]m,*p,*p) These allows quantification over types. Note that if you erase the mono/poly distinctions, you get the single rule ([],*,*), which is the impredicative rule for the lambda cube. However, this system tracks a distinction, so it remains predicative (universal quantifiers don't range over types that contain universal quantifiers). With just these rules, I think we accept just the types valid in ordinary Haskell. We have higher order types, but we can only have polytypes in prenex normal form, because quantification sticks a type into *p, and the only thing we can do with a *p is add more quantifiers (over []m) to the beginning.r To get rank-n types back, we need to be able to write functions that accept and return polytypes as arguments. This corresponds to the rules: (*m,*p,*p) (*p,*m,*p) (*p,*p,*p) Note that []p never appears in our rules; it exists only to give *p a type (which may not strictly be necessary, even, but it doesn't hurt). Data types would have kinds like: Maybe : *m -> *m and so types like Maybe (forall a. a -> a) would be invalid, because it's trying to use the type constructor with a *p. This type system is a bit stricter than the one GHC uses for rank-n types, as if you have: id : forall a : *m. a -> a You cannot instantiate a to forall a. a -> a, because it has kind *p. GHC allows that sort of impredicative instantiation with just rank-n types turned on. As alluded to earlier, one can recover an ordinary impredicative F_w by erasing the mono/poly distinctions. The rules collapse to: (*,*,*) ([],*,*) ([],[],[]) If anyone's interested in playing with the checker, it can be found at http://code.haskell.org/~dolio/ in the pts repository (I'll try to get a little documentation for the REPL uploaded). And let me know if you find something that types but shouldn't, or some such nonsense. Cheers, -- Dan