Comment author: @garrigue

This is a feature:
Since ('a -> int) -> int is an instance of 'b -> int (where 'b is contravariant), it would not be principal to allow generalizing it. So the precise definition is that a type variable is generalizable if it doesn't appear under a negative position (simply stated, inside the left side of an arrow, or as inside the parameter of a contravariant or invariant type).
There is no such problem with 'a X.t, as X.t is covariant, and 'a is its direct parameter.

If we were to document this, I'm not sure where it would go: there is no statement about the value restriction in the reference manual, as far as I know. Maybe we should add a section about typing somewhere, but we cannot write down all the specification there...

Comment author: @lpw25

IIUC this is because contravariant variables cannot be generalised, which is because OCaml doesn't have a uniform value representation, which is because of the float array hack. So if in the future the float array hack were removed then this issue could be addressed.

Comment author: @Drup

this is because contravariant variables cannot be generalised, which is because OCaml doesn't have a uniform value representation

Can you explain that part ?

Comment author: @gasche

Can you explain that part ?

You should have a look at Jacques' article on the value restriction:

Relaxing the Value Restriction
Jacques Garrigue, 2004
http://caml.inria.fr/pub/papers/garrigue-value_restriction-fiwflp04.pdf

this question is discussed in the Conclusion section.

The intuition for the argument is as follows: to justify that generalizing variables occurring in positive solutions is sound (generalizing T('_a)), one may consider unifying them with the bottom type (no inhabitant, subtype of everything), and using subtyping to argue that T(bottom) is a subtype of T('a) for any 'a, and thus (forall 'a . T('a)) is a valid type.

To work on types that occur in negative positions, we would need to instantiate with T(top). But the current OCaml implementation admits no top type, as is suggest by the following segfault (example from the article):

let t = Array.create 2 (Obj.repr 0.0);;
t.(1) <- Obj.repr 1;; (* segfault *)

(With GADTs or first-class modules we can pack any value in an existential, but this always implies the use of a boxing construction. A top type would require subtyping, that is cast to a universal type without change to the value representation.)