Fun with the Value Restriction

This is not a valid OCaml program:

type 'a endo = Endo of int * ('a -> 'a)
let poly = Endo ((succ 23),(fun x -> x))
type thing = { u : unit }
let mono = Endo (0,(fun { u = u } -> { u = u }))
let _ = [mono;poly]

The typechecker rejects it, with this error message:

File "vrmh.ml", line 5, characters 14-18:
This expression has type 'a endo but is here used with type thing endo
The type constructor thing would escape its scope

Removing the last line makes it typecheck. As does exchanging the second and third lines, thusly:

type 'a endo = Endo of int * ('a -> 'a)
type thing = { u : unit }
let poly = Endo ((succ 23),(fun x -> x))
let mono = Endo (0,(fun { u = u } -> { u = u }))
let _ = [mono;poly]

Yes. Notice the mysterious action-at-a-distance. Notice also how the type inferred for poly (see ocamlc -i) is not polymorphic at all, but rather thing endo, the same as mono. Notice further that it would not be possible to define it with an explicit ascription of that type before the definition (i.e., outside the scope) of thing itself. Apparently this is bad.

And then there's the reason why the type of poly didn't have its type variable generalized, thus leaving it with the type '_a endo and subject to unification with the type of mono. This is, of course, the value restriction of ML fame, which I will not explain here; but it's a little more confusing (read: I spent far too much time trying to come up with the mostly minimal test case seen here) (so, yes, this actually is something I ran into in a halfway-real program) in OCaml, where it's been relaxed in certain ways. But not others. For example, this:

type 'a endo = Endo of int * ('a -> 'a)
let poly = Endo (24,(fun x -> x))
type thing = { u : unit }
let mono = Endo (0,(fun { u = u } -> { u = u }))
let _ = [mono;poly]

Is fine.