[Haskell-cafe] Predicativity?

[Wei Hu]

Hello,

I only have a vague understanding of predicativity/impredicativity, but cannot 
map this concept to practice.

We know the type of id is forall a. a -> a. I thought id could not be applied 
to itself under predicative polymorphism. But Haksell and OCaml both type check 
(id id) with no problem. Is my understanding wrong? Can you show an example 
that doesn't type check under predicative polymorphism, but would type check 
under impredicative polymorphism?

Thanks!