[Haskell] Polymorphic types without type constructors?

[Greg Morrisett]

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