Predicativity?

Predicativity?

[Wei Hu]

Hello,

Isn't OCaml's polymorphism predicative? Then, why does the following code in 
the interactive toplevel type check?

# let id x = x;;
val id : 'a -> 'a = <fun>
# let f x = (id id) x;;
val f : 'a -> 'a = <fun>

I thought id could not be applied to itself under predicative polymorphism. Is 
my understanding wrong? Can you show an example that doesn't type check in 
OCaml, but would type check under impredicate polymorphism?

Thanks!