Explicitly polymorphic annotation in nested context

Question

In the code below, I am not sure I understand why there is a type error on _nested2.

Does that mean that only toplevel definitions generalize their inferred type to match an explicitly polymorphic signature?

let toplevel1 : 'a. 'a -> int = (fun _ -> 0)
let toplevel2 : 'a. 'a -> int = (fun (_ : 'a) -> 0)

let nest1 =
  let _nested1 : 'a. 'a -> int = (fun _ -> 0) in 0

let nest2 =
  let _nested2 : 'a. 'a -> int = (fun (_ : 'a) -> 0) in 0
(*                               ^^^^^^^^^^^^^^^^^^^
   Error: This definition has type 'a -> int which is less general than
            'a0. 'a0 -> int
*)

Answer 1

The issue is that the 'a type variable in the (l': 'a t) annotation lives in the whole toplevel definition and thus outlives the polymorphic annotation.

In order to illustrate this scope issue for type variables, consider

let int, id = 
  let f (x:'a) = x in
   (0:'a), f

Here, maybe surprisingly, the type of id ends up being int ->int rather than 'a. 'a -> 'a because the type variable 'a is shared between (x:'a) and (0:'a).

Coming back to the issue at end, this means that it is not yet possible to generalize the type of _nested2 on the second line of the nest2 function due to the escaping variable 'a.

Moreover, it is only with recent versions of OCaml (after OCaml 4.11.0) that the toplevel2 function:

let toplevel2 : 'a. 'a -> int = (fun (_ : 'a) -> 0)

is accepted.

Older versions of OCaml fail with

Error: This definition has type 'a -> int which is less general > than 'a0. 'a0 -> int

because the algorithm for checking explicit polymorphic annotation in earlier versions did not detect that the unification type variable is not escaping the scope of the toplevel definition.

The short version is thus that is is better to not mix explicit polymorphic annotation with (unification) type variables.