Simon Peyton-Jones wrote:
You have it exactly right. The key word is "predicative". GHC has a predicative type system, that only allows you to instantiate a type variable with a monotype, not a polytype. An impredicative system (which is the one you want here) is more expressive, but it makes type inference very much more difficult.
Just to be anal, GHC is actually impredicative. You can instantiate a type variable with a newtype that *contains* a polymorphic type. So, there is no simple set-theoretic stratification of the universes of monotypes and polytypes. Rather, GHC enforces a sub-kind constraint on variables that precludes them from ranging over types whose top-most constructor is a forall (and has a few more structural constraints.) The distinction is subtle, but important. A predicative version of Haskell would have a much, much simpler denotational semantics, but also prevent a number of things that are useful and interesting. -Greg