Value restriction

also: relaxed value restriction, weak type variable, _weak

The rule that only syntactic values have their type variables generalized in a let. An application such as List.map f is not a value, so its type variables stay weak, fixed by the first use. OCaml relaxes the rule for type variables that occur only covariantly.

Without the restriction, mutable state breaks the type system. If ref [] had type 'a list ref for every 'a, one use could store an int in it and another read a string out of it. The restriction stops that by refusing to generalize the result of any computation, since a computation might have allocated state.

A value is a constant, a variable, a function, or a constructor applied to values. Anything else is an application.

let r = ref []
let id_list = List.map (fun x -> x)
let id_list' l = List.map (fun x -> x) l
let empty = List.rev []

What ocamlc -i infers, OCaml 5.5.1.

val r : '_weak1 list ref
val id_list : '_weak2 list -> '_weak2 list
val id_list' : 'a list -> 'a list
val empty : 'a list

The fix for id_list is eta-expansion: adding the parameter back turns the application into a function, which is a value. The last line is the relaxation. 'a appears in empty's type only covariantly, as the element type of a list it returns, and a covariant variable can be generalized safely even for the result of a computation, because no one can store into it through that type.

A weak variable is not an error by itself. It becomes fixed at its first use, and it is an error only if the compilation unit ends with it still unfixed and exported.