Let-Polymorphism and Where Generalization Happens

Hindley-Milner inference gives a function the most general type consistent with its body, and then allows that function to be used at several different types in the same scope. The mechanism that permits this is generalization at let, and its correctness depends on a subtle distinction between metavariables that may be quantified and metavariables that must not be. Getting that distinction wrong produces either a checker that rejects legal programs or, worse, one that accepts unsound ones.

The problem: sharing a metavariable across uses

Consider a definition of the identity function and two uses of it, one on an integer and one on a string. If the definition is checked by creating a fresh metavariable α for the parameter, unifying α with the body’s type, and then leaving α in the environment, the first use unifies α with Int and the second unifies it with String. The second unification fails, and the definition is usable at exactly one type.

That behavior is correct for a lambda parameter: a parameter has one type within its scope, and λf. (f 1, f "x") should be rejected because f cannot be both. It is wrong for a let-bound name, because the definition is checked once and the name may then be used at many types. The difference is that the let body’s uses are separate instantiations of one scheme, while the lambda’s uses are uses of one variable.

Generalization is the operation that turns a type containing metavariables into a scheme by quantifying over some of them. Instantiation is the inverse: replacing the quantified variables with fresh metavariables at each use. Together they implement the sharing that let is supposed to provide.

Levels: the mechanism that makes generalization local

The naive rule “generalize every metavariable that is not free in the environment” is correct and, implemented literally, quadratic: computing the free metavariables of the environment at every let requires walking it.

The standard implementation replaces the walk with a numeric level attached to each metavariable. Entering a let-bound definition increments the current level; metavariables created inside the definition carry the new level; leaving the definition decrements the level and generalizes every metavariable whose level is greater than the current one. Metavariables created outside the definition have a level at or below the current one and are not generalized, which is exactly the condition “not free in the environment” — because a metavariable created outside can only appear in the environment if it was created there.

The check on generalization is therefore an integer comparison per metavariable, and the traversal of the type being generalized is the only work. This is the technique used in OCaml’s type checker and described in the literature on efficient HM implementations.

Two operations must respect levels. Unification of a metavariable with a type must lower the level of every metavariable in that type to the level of the bound one, because the type is now visible at that outer level. Skipping the lowering produces a metavariable whose level is too high, which is then wrongly generalized at the next let, producing a scheme that quantifies a variable still shared with the environment. The consequence is not a crash but a scheme whose quantified variable can be instantiated at two incompatible types in one context, which is the same failure shape as the ref [] example below.

What the value restriction protects

Generalization is not sound for every expression, and the counterexample is refutation in the presence of mutable state.

A definition of the form let r = ref [] creates a mutable cell holding an empty list. Generalizing gives r : ∀α. α list ref, and the two uses r := [1] and print (List.hd !r : string) then typecheck while the cell holds an integer where a string is expected. The type system has proved a falsehood because the two uses share one storage location.

The value restriction blocks this by generalizing only syntactic values — lambdas, constants, variables, constructors applied to values — and treating everything else as monomorphic, with all its metavariables unified at the definition site. let r = ref [] is an application, not a value, so r gets type α list ref with α fixed at the definition, and the unsound program is rejected.

The restriction is conservative and rejects legal programs. The common workaround is eta-expansion: rewriting let f = g as let f x = g x makes the right-hand side a function abstraction, which is a value, so generalization applies. The rewrite changes when g is evaluated — at each call rather than once — and can therefore duplicate work, so it is a source-level fix, not a compiler transformation.

OCaml and SML both impose the restriction. Haskell does not, because its mutable state lives in the IO and ST monads, whose types prevent the offending sharing: the type of a mutable reference in ST carries a phantom type parameter tied to the runST scope, so two uses cannot escape into the same scope with different element types. That is a type-system answer to the same problem, and it costs the complexity of rank-2 types in runST’s signature.

Where generalization is placed in the algorithm

The choice of placement changes which programs are accepted, and implementations differ.

Generalizing at let alone is the textbook rule. It accepts the identity function used at two types and rejects a lambda parameter used at two types, which is the intended distinction. It also means that a top-level definition in a module is generalized, since top-level bindings are let bindings.

Generalizing at lambda parameters as well is unsound without further restriction: the parameter’s type would become a scheme, and two uses of the parameter in one body would then be independent instantiations that no single argument type has to satisfy. The value restriction does not rescue that case, because a parameter has no right-hand side to test for value-hood.

Generalizing a whole group of mutually recursive bindings at once, rather than one let at a time, is what SML and OCaml do; the group is checked monomorphically and generalized together afterwards. Extending that to the whole compilation unit is not the usual design: a top-level binding is still generalized after its own definition is checked, and treating the module as one recursion group would leave every top-level name monomorphic until the file ended.

In a bidirectional system, described in Bidirectional Checking Versus Full Inference, generalization must be placed where synthesis produces a complete type. A let whose right-hand side is checked against an annotation has no metavariables to generalize — the annotation fixed the type — and generalizing it is a no-op. A let whose right-hand side is synthesized has metavariables, and whether they are generalizable depends on whether they escaped into the surrounding context during the checking of the body.

Instantiation and the order of operations

Instantiation must create fresh metavariables for every quantified variable, and it must do so at every use, not once per scheme. A checker that instantiates once and caches the result reintroduces the sharing that generalization removed.

For a scheme with nested quantifiers — a function taking a polymorphic argument — instantiation is not a single substitution. The argument’s scheme must be instantiated at the point where the argument is applied, which requires the callee’s type to carry a scheme in a position that ordinary function types cannot express. That is rank-2 polymorphism, and it is why runST’s type cannot be written in HM.

In OCaml, a let-bound name’s scheme is instantiated when the name is used, and the same instantiation applies when a polymorphic function is passed as a function argument. The limitation that remains is the one above: a parameter’s own type is monomorphic inside the callee, so a function cannot apply its parameter at two different types, which requires a record field holding a polymorphic function or a first-class module. That limitation is a direct consequence of keeping instantiation at the use site of a name rather than at every type position.

Diagnostics

The errors produced by a generalization bug are among the worst in a compiler, because they name types the user never wrote.

A missing level lowering produces “this expression has type α but an expression was expected of type int” where α is an internal metavariable that should have been generalized. The message is unhelpful and, worse, the program may compile under a different traversal order. A checker should print unbound metavariables as a distinct placeholder rather than as a type variable, so the user can tell an inference failure from a genuine type mismatch.

A missing value restriction produces no error at all in the common case and an unsound acceptance in the rare one, which is why the restriction’s absence is usually caught by a test suite that includes the ref [] counterexample rather than by users.

The third diagnostic issue is the interaction with recursive definitions. A recursive let cannot generalize its own binding during the checking of its body, because the body’s uses would each be instantiated and the recursion would have no single type. Implementations type the recursive occurrence monomorphically and generalize after the body is checked, which is why polymorphic recursion requires an explicit annotation. A checker that generalized the recursive occurrence too early would report a type error inside the definition when the recursive call used a different instantiation from the one inferred for the name — the error appears while checking the body, not at run time.

The last is the boundary with modules. A signature ascription that hides a type variable forces the definition to be less polymorphic than inference would make it, and the error appears at the ascription rather than at the definition. Preserving the connection between the two — so the message can say which constraint came from the signature — requires the checker to record, for each metavariable, the constraint that introduced it, which is the same provenance machinery that Error Types and Recovery in a Type Checker needs for recovery.