Value restriction

If one shared reference initially contains an empty list and is generalized independently at every use, one use could store integers while another reads booleans. The same mutable cell would acquire incompatible assumptions.

The problem is not the empty list alone. It is generalizing a binding that creates shared mutable storage as though each use were an independent polymorphic instance.

References: [1]

SML ’97 ties generalization to whether the right-hand side is nonexpansive. Constants, variables, function expressions and permitted constructor or record forms qualify; arbitrary function application does not qualify merely because its result is a function.

A function expression may perform work when later called. The rule concerns evaluation at the binding, not a blanket requirement that every function body avoid mutable state.

References: [2]

The rule is conservative: some harmless computations lose polymorphism, and local uses may instead determine one monomorphic instance. An annotation or a suitable reformulation can make that intended instance clearer.

Garrigue’s relaxed scheme recovers some safe generalization using covariant type-variable occurrences. ML implementations differ, so one system’s displayed weak-variable notation is not the definition of the restriction itself.

References: [1] [2]