Typesspec

Unification, and Why `T = List<T>` Must Fail

Three rules solve every type equation: decompose matching constructors, bind a variable, or fail. The fourth thing the algorithm must do is refuse to bind a variable to a term containing itself — skip that and the type is infinite and the compiler does not terminate.

The question

How does a type checker actually solve T = List<U>, U = int, and why must T = List<T> be rejected?

Source→Lexing→Tokens→Parsing→AST→Semantics→Typed→IR→Optimize→Codegen→Machine code→Link→Execute
What the program is here

A worklist of equations between *type terms*, where a term is either a variable (T, U, α) or a constructor applied to argument terms (List(U), Map(T, V), →(A, B), and nullary ones like int). The question this form answers: is there a substitution — a map from variables to terms — that makes both sides of every equation syntactically identical, and if so, what is the most general such substitution?

What this phase may assume or do

A variable may be bound to a term only if the variable does not occur anywhere inside that term. Skipping this *occurs check* produces a cyclic term, which denotes an infinite type; any later traversal of it — printing, comparing, lowering — fails to terminate. Unification is also complete only for first-order terms: once a type constructor may itself be a variable, the problem becomes higher-order unification, which Goldfarb proved undecidable in 1981, and every system that needs it (dependently typed languages, higher-kinded inference) uses an incomplete heuristic instead.

Key points

  • A type term is a variable or a constructor applied to terms. Unification asks for a substitution making both sides syntactically identical.
  • Three rules: identical terms succeed, a variable binds, matching constructors decompose. Two failures: different constructors, different arity.
  • The most general unifier is unique up to renaming, and every other solution is an instance of it.
  • A variable may not be bound to a term containing itself. That is the occurs check, and without it the type is infinite and traversal does not terminate.
  • fun x -> x x is the canonical trigger: it requires α = α → β, and the occurs check is what turns that into a message rather than a hang.
  • Unification is purely syntactic. int and float do not unify even where a conversion exists, which is why subtyping requires a different algorithm rather than a bigger one.
  • Solving order does not change which programs are accepted; it changes entirely which line gets blamed.
  • Production implementations use union-find with path compression, not composed substitutions.

Solving by rewriting: a worked run

simplifiedThe trace shows substitutions being composed explicitly, which is how the algorithm is written in textbooks and never how it is implemented. Real solvers keep each type variable as a mutable cell in a union-find structure and *link* it to its solution destructively, so step 5’s composition never happens as a separate pass and lookups follow links with path compression. The results are identical; the performance is not comparable.

Unification is a worklist algorithm. Take an equation off the list, apply whichever of three rules matches, and put any resulting equations back on. When the list is empty, the accumulated substitution is the answer; if no rule matches, the constraint set is unsatisfiable and you have a type error.

Below is a full run on a goal slightly richer than T = List<U> alone, so that all three rules appear. Read the Substitution column as the state of the solver, and the Result column as what the rule did.

Solving Map<T, List<U>> = Map<string, List<int>>, then U = intsimplified
StepConstraintSubstitutionResult
1Map<T, List<U>> = Map<string, List<int>>{}Both sides are the constructor Map with two arguments. Decompose: push T = string and List<U> = List<int>.
2T = string{ T ↦ string }T is a variable and does not occur in string. Bind. The occurs check passes trivially.
3List<U> = List<int>{ T ↦ string }Same constructor, same arity. Decompose: push U = int.
4U = int{ T ↦ string, U ↦ int }U is a variable, occurs check passes. Bind.
5— worklist empty —{ T ↦ string, U ↦ int }Apply the substitution to the original goal: Map<string, List<int>>. This is the most general unifier; every other solution is an instance of it.
AT = List<U> with U = int (the simple case){ T ↦ List<U> } then { T ↦ List<int>, U ↦ int }Bind T, bind U, then compose: T = List<int>. The composition step is why implementations resolve variables lazily rather than rewriting eagerly.
BList<T> = Set<T>{}Fail: different constructors. No substitution can make List equal Set, because unification is syntactic — it never consults a subtyping or conversion relation.
CMap<T, U> = Map<int>{}Fail: same constructor, different arity. Reported in most languages as “wrong number of type arguments”.

The occurs check

This is the sharpest point in the lesson, and the one worth carrying away.

Consider the equation T = List<T>. T is a variable, so the bind rule appears to apply: set T ↦ List<T>. But now substitute the definition into itself and watch what the type is.

What `T = List<T>` denotes
T = List<T>

  T  ↦  List<T>
     ↦  List<List<T>>
     ↦  List<List<List<T>>>
     ↦  List<List<List<List<T>>>>
     ↦  ...

There is no finite type term satisfying this equation.
The BIND rule must therefore be guarded:

    bind(v, t):
        if occurs(v, t) then FAIL "recursive/infinite type"
        else  v := t

occurs(v, t) walks t looking for v. It is the whole
difference between a compiler that reports an error and
a compiler that allocates until the machine gives up.

Where the occurs check actually fires

implementationOCaml’s -rectypes flag disables the occurs check and admits equi-recursive types; it is supported and strongly discouraged, because ordinary mistakes then produce large well-typed programs instead of errors. ISO Prolog specifies = without an occurs check and provides unify_with_occurs_check/2 separately; SWI-Prolog detects and prints cyclic terms rather than looping, while naive implementations do not. TypeScript’s TS2589 is a fixed instantiation-depth limit, currently in the low hundreds, and the exact threshold has changed across releases.

It is easy to think T = List<T> is a contrived equation nobody would generate. It is generated constantly, by one of the most ordinary mistakes there is: applying something to itself, or forgetting an argument.

The canonical case is fun x -> x x. The parameter gets a variable α. The body applies x to x, so from T-App the checker needs α = α → β. Bind α to α → β and you have α = ((α → β) → β) → β = ..., unbounded. The occurs check fires and the language reports something like “this expression has type 'a -> 'b but an expression was expected of type 'a; the type variable 'a occurs inside 'a -> 'b”. That message names the occurs check directly, and once you recognise it, the class of mistake behind it — a self-application, a missing argument, a recursive definition without a base case in its types — is immediate.

The same failure appears far from the lambda calculus. In TypeScript, a recursive conditional or mapped type that expands into itself produces “Type instantiation is excessively deep and possibly infinite” — the same guard, implemented as a depth limit rather than an occurs check, because TypeScript’s type-level language is expressive enough that a true occurs check would not suffice. In Rust, error[E0072]: recursive type has infinite size is the value-level cousin: a struct containing itself by value has no finite layout, and the fix is the same as the type-level one, indirection through a pointer.

And the systems that deliberately allow it are instructive. OCaml has -rectypes, which switches the occurs check off and admits equi-recursive types; almost nobody uses it, because the resulting error messages become unreadable and a genuine mistake now type-checks into something enormous. Prolog omits the occurs check from its default = for performance, which is standardised behaviour, and unifying X = f(X) there creates a cyclic term; printing it in a naive implementation does not terminate, and modern systems detect the cycle and print a marker instead.

The same guard, four languages
1OCaml    let f = fun x -> x x;;
2  Error: This expression has type 'a -> 'b
3         but an expression was expected of type 'a
4         The type variable 'a occurs inside 'a -> 'b
5 
6Haskell  f x = x x
7  Error: Occurs check: cannot construct the infinite type:
8         t0 ~ t0 -> t1
9 
10Rust     struct Node { next: Node }
11  error[E0072]: recursive type `Node` has infinite size
12  help: insert some indirection (e.g. a `Box`)
13 
14TS       type Deep<T> = { v: T; next: Deep<Deep<T>> }
15  error TS2589: Type instantiation is excessively deep
16                and possibly infinite.

Haskell names the check explicitly and prints the equation. OCaml describes it. Rust hits the value-level version — a type with no finite layout. TypeScript uses a depth limit rather than an occurs check because its type-level language can compute, so “does this variable occur” is not a decidable question there. Four responses to one underlying condition: a term cannot contain itself.

The whole algorithm, and why it is only three rules

Unification is small. Robinson published it in 1965 and the core has not changed. What has changed is the data structure underneath, and that is where all the engineering is.

The pseudocode below is the complete algorithm for first-order terms. Everything a production implementation adds — union-find cells, path compression, level numbering for [[hindley-milner]]’s generalization, span tracking for error messages — is around this, not inside it.

  • The variable store is a hash-table-backed union-find structure; resolve is a find with path compression, and bind is a link.
  • The occurs check is O(size of the term) each time it runs, and running it on every bind is what makes naive unification quadratic on pathological input. Some implementations amortise it with the level numbering they already keep.
  • Because unification is syntactic, Vec<i32> and Vec<i64> fail even though both are vectors of integers, and no message about “similar types” can be generated by the solver itself — it has to be added afterwards as a diagnostic heuristic.
  • Order matters for errors and not for results: the same constraint set yields the same substitution regardless of solving order, but *which* equation is reported as the failure depends entirely on it.
Unification for first-order terms, complete
unify(s, t):
    s := resolve(s)          # follow links to the current binding
    t := resolve(t)

    if s is t:                                  return           # identical

    if s is a variable:
        if occurs(s, t): FAIL "infinite type"
        bind s := t;                            return

    if t is a variable:                         unify(t, s)      # symmetric

    if s = C(s₁..sₙ) and t = C(t₁..tₙ):                          # same ctor,
        for i in 1..n: unify(sᵢ, tᵢ)            return           # same arity

    FAIL "cannot unify"                                          # ctor mismatch
                                                                 # or arity mismatch

Three success rules, two failure rules, one guard.
Note what is NOT here: no subtyping, no coercion, no
conversion. Unification is SYNTACTIC. `int` and `float`
do not unify even in a language where an int converts
to a float — which is precisely why adding subtyping
means replacing this algorithm, not extending it.

Which constraint gets blamed

typicalProvenance tracking and annotation-first ordering are what mainstream inference engines converged on (GHC, rustc, the OCaml compiler have all added them incrementally), not something any specification requires. Type-error slicing remains largely a research technique; Helium for Haskell is the best-known implementation and it is not what any production compiler ships.

This is the practical consequence of everything above, and the reason [[type-inference]] is a tradeoff rather than a free win.

A unifier fails at the first equation that contradicts the accumulated substitution. That equation is not necessarily related to the mistake — it is merely the first place the mistake became visible. Swap the order in which two constraints are pushed and the error moves to a different line, with a different message, blaming a different function. Both messages are correct and neither points at the bug.

Implementations fight this in three ways, and none of them fully wins. Provenance: record, with each constraint, the source span and the rule that generated it, so the error can say “this argument, because of that parameter”. Ordering heuristics: solve constraints from annotated positions first, so contradictions surface against types the programmer wrote. Type-error slicing: compute the whole set of constraints that jointly cause the failure and report all of them, which is more honest and much harder to read. Rust’s and GHC’s error quality over the last decade is mostly a story of investment in the first two.

The engineering lesson generalises past compilers: any constraint solver — a package version resolver, a scheduling engine, a policy checker — has this problem, and the fix is the same. Record why each constraint exists before you need it, because reconstructing that after the contradiction is found is not possible.

How it works

The steps, in the order the compiler takes them.

  • Maintain a worklist of equations and a store mapping each type variable to its binding, initially empty.
  • Pop an equation. Resolve both sides by following existing bindings to their current representatives.
  • If the two sides are the same variable or the same nullary constructor, discard the equation.
  • If one side is an unbound variable, run the occurs check on the other side; on success, bind; on failure, report an infinite type.
  • If both sides are constructors, require the same constructor and the same arity, then push one equation per argument pair.
  • Otherwise report a mismatch, naming the two constructors and the spans of the constraints that produced them.
  • When the worklist empties, apply the store to every type in the program so the tree carries resolved types.

How it breaks

What the engineer observes when it goes wrong — not what goes wrong internally.

  • Without an occurs check the compiler builds a cyclic term and then hangs or exhausts memory while printing, comparing or lowering it. The observable symptom is a compiler that never returns on one file and gives no error.
  • The error is reported against a call site in another module, phrased in terms of type variables the programmer never wrote, because that is where the first contradiction happened to surface.
  • The reported error moves when an unrelated line is reordered or a helper is inlined, which convinces engineers the compiler is unreliable when it is behaving deterministically.
  • An “occurs check” message is produced by a missing argument — the programmer wrote f x where f x y was meant — and the message describes an infinite type rather than the missing argument.
  • A mismatch between Vec<i32> and Vec<i64> is reported as a bare constructor mismatch with no hint that a numeric conversion was intended, because the solver has no notion of conversion at all.
  • On generated code with deeply nested generics, unification with repeated occurs checks turns quadratic and one file takes minutes while every other file is instant.

When it helps

  • Reading an ML, OCaml, Haskell or Rust inference error: identifying which rule failed — bind, decompose, occurs — tells you what class of mistake to look for before reading the types at all.
  • Implementing inference for a DSL, schema language or template system, where unification is the correct, small, well-understood engine and hand-rolled matching is where the bugs are.
  • Understanding generic call resolution in any language: “does this type argument unify with that parameter” is the question every generic call site asks.
  • Debugging pattern matching and destructuring, which is the same algorithm applied to values rather than types.

When it hurts

  • When the language has subtyping. Unification solves equalities; subtyping needs inequalities, and pretending otherwise gives a solver that rejects correct programs — see [[subtyping]] and [[variance]].
  • When you want a “did you mean” suggestion. The solver knows only that two constructors differ; similarity is a separate heuristic layered on top.
  • As an explanation for TypeScript’s generic inference, which is candidate collection with priority rules rather than constraint solving, and behaves differently on the same input.
  • In higher-order settings, where the constructor itself may be a variable. That problem is undecidable, and any system claiming to solve it is using a heuristic with cases it silently gives up on.

What it costs

Every one of these is paid by something.

  • The occurs check buys termination and comprehensible errors, and pays a traversal of the term on every binding — the cost that makes naive unification quadratic on adversarial input, and the reason Prolog’s standard = omits it.
  • Union-find with destructive linking buys near-linear solving and pays in a mutable global store, which makes backtracking, speculative solving and error recovery substantially harder to implement than with composed substitutions.
  • Constraint provenance buys attributable error messages and pays memory on every constraint plus discipline in every rule that generates one — and it cannot be added retroactively, because the information is gone by the time the contradiction is found.
  • Solving eagerly as constraints arrive buys early failure and small working sets, and pays in blame quality: the first contradiction is reported, and it is often not the informative one. Solving lazily buys better ordering heuristics and pays in memory and complexity.

What else you could do

What a different compiler or language does instead, and when that is better.

  • Matching rather than unification: only one side may contain variables. Simpler, cheaper, sufficient for template instantiation and pattern matching, and insufficient for inference where both sides have unknowns.
  • Subtype constraint solving, which collects inequalities S <: T and computes a solution over a lattice. Necessary in any language with subtyping, much harder, and the source of algebraic subtyping and MLsub.
  • Semantic unification modulo a theory — E-unification — where terms are compared up to equations such as associativity or commutativity. Needed for type-level arithmetic and for associated-type families; usually undecidable in general and handled by incomplete solvers.
  • Higher-order pattern unification (Miller patterns), a decidable fragment of higher-order unification used by dependently typed languages to handle metavariables applied to distinct bound variables, with an explicit “I cannot solve this, please annotate” escape.
  • SMT solving, where type constraints are discharged by a general solver. This is what refinement-type systems (Liquid Haskell, F*) do, and it buys enormous expressive power at the cost of a solver in the compiler and errors that come back as unsatisfiable cores.

See it for yourself

The flag, dump or tool that shows you this directly.

  • OCaml: let f = fun x -> x x;; in the top level prints the occurs-check error verbatim in about a second. The fastest possible demonstration.
  • Haskell: ghci and let f x = x x gives “Occurs check: cannot construct the infinite type”. -ddump-tc-trace shows every constraint generated and the order they were solved in.
  • OCaml with -rectypes accepts the same expression and prints a recursive type — worth doing once, to see why the flag is discouraged.
  • Prolog: X = f(X). in SWI-Prolog prints a cyclic term; unify_with_occurs_check(X, f(X)). fails instead. The two calls side by side are the clearest illustration that the check is a choice.
  • Rust: struct Node { next: Node } gives E0072 with the Box suggestion; rustc --explain E0072 explains the finite-layout requirement.
  • Our unification stepper at /compilers/types runs the worklist one equation at a time, showing the substitution grow and the occurs check firing.

Plausible wrong readings

Stated the way a confident engineer states them.

  • “The occurs check is an optimization.” It is a correctness requirement. Without it the solver produces a cyclic term and a later phase does not terminate.
  • “T = List<T> is just a recursive type, and languages have those.” Recursive *type definitions* are fine — type List<T> = Nil | Cons(T, List<T>) names the recursion behind a constructor. An unguarded equation between a variable and a term containing it does not; the difference is iso-recursive versus equi-recursive types.
  • “Unification handles subtyping if you are careful.” It solves equalities. Subtyping needs inequalities and a lattice, and that is a different algorithm with different complexity.
  • “The error message tells me where the bug is.” It tells you where the first contradiction was found. Those coincide only when annotations bounded the search.
  • “Unification is a type-system concept.” It is a general term-solving algorithm — Prolog resolution, pattern matching, template instantiation and generic call resolution are all the same machinery.

Misconceptions

The claim, and what is actually true.

Unification is specific to functional languages.
It is the engine behind generic call resolution in Java, C#, Rust and Swift, behind C++ template argument deduction, behind Prolog, and behind pattern matching. The ML family is simply where it is most visible.
A most general unifier might not be unique.
For first-order terms it is unique up to renaming of variables. That uniqueness is what gives Hindley–Milner its principal-types property, and it is exactly what subtyping destroys.
If two types “mean the same thing”, unification will accept them.
It is syntactic. A type alias is expanded first, but a conversion, a coercion or a subtype relation is invisible to it. int and float do not unify anywhere.
Better error messages need a better solver.
They need provenance recorded at constraint-generation time. By the moment the solver fails, the information about why each constraint exists is already gone unless someone kept it.

Go deeper

The same idea at increasing depth. Stop wherever it stops being useful.

overview

Unification solves equations between types. If you have T = List<U> and U = int, you substitute forward and get T = List<int>. There are only three moves: if both sides are the same constructor, match up their arguments and keep going; if one side is a variable, set it equal to the other side; otherwise fail. The one extra rule is the important one: a variable can never be set equal to something that contains it. T = List<T> would mean T is a list of lists of lists forever, and there is no such type. Checking for this before every binding is called the occurs check, and a solver without it does not stop.

practical

When a functional-language compiler reports an occurs check or an infinite type, do not look for a recursive data structure. Look for a missing argument or an accidental self-application: f x where f x y was meant, a partially applied function passed where a value was expected, or a recursive helper whose base case returns the wrong shape. Those generate α = α → β and nothing else does. More generally, treat the reported line as the place the contradiction surfaced rather than the place the mistake lives, and narrow the search by adding a type annotation to the function you are most confident about — that pins one end of the constraint chain and forces the error to move toward the actual problem.

advanced

The occurs check is where the iso-recursive versus equi-recursive distinction becomes concrete. Equi-recursive types treat T and List<T> as *equal* when the equation holds, which requires deciding equality of infinite trees — decidable for regular trees, and it makes error messages unusable, which is why OCaml hides it behind -rectypes. Iso-recursive types, which is what every mainstream language uses, require the recursion to pass through a named type constructor with explicit fold and unfold operations — in practice, through a struct or a data declaration. That is why type List<T> = Nil | Cons(T, List<T>) is accepted while a bare equation is not: the name is the fold, and it gives unification a finite term to work with. The same distinction explains Rust’s E0072: a struct Node { next: Node } is iso-recursive at the type level and still has no finite *layout*, so the fix is indirection, which introduces a pointer and thereby a finite size. Type-level recursion and value-level recursion need the same guard for different reasons, and a language has to answer both.

How much this depends on

Nothing in this domain is true of every compiler. These say how much.

specRobinson’s unification algorithm and the uniqueness of the most general unifier up to variable renaming are standard results for first-order terms. Higher-order unification — where the head of an application may be a variable — was proved undecidable by Goldfarb in 1981, which is why dependently typed languages restrict themselves to decidable fragments such as Miller pattern unification and ask for annotations elsewhere.
specISO Prolog specifies =/2 without an occurs check, for performance, and provides unify_with_occurs_check/2 for when it is wanted. This makes Prolog the standard example of a system that deliberately omits the guard; the consequence is cyclic terms, which conforming implementations handle differently — some detect and print a marker, others loop.
implementationOCaml’s -rectypes accepts equi-recursive types by disabling the occurs check; it is supported and discouraged in the manual because ordinary errors then produce large accepted programs. TypeScript uses a fixed instantiation-depth limit (TS2589) rather than an occurs check, because its type-level language is expressive enough that occurrence is not the right question; the exact depth has changed across releases.
simplifiedThe trace and pseudocode compose substitutions explicitly and run the occurs check on every bind. Production implementations use destructive union-find linking with path compression, and several amortise or approximate the occurs check using the level numbering they already maintain for generalization. The accepted programs are the same; the constant factors and the memory behaviour are not.

If you were asked this in an interview

  • Solve Map<T, List<U>> = Map<string, List<int>> by hand and state the most general unifier.
  • Why must T = List<T> fail? What happens in a solver that does not check?
  • What ordinary programming mistake produces an occurs-check error, and why?
  • Why can unification not be extended to handle subtyping?

Connections

DSAunion-findhash-tabledag
Domains that do not exist yet
  • Testing & Reliability Engineering — Property-based testing of a solver: idempotence, most-generality, and termination on cyclic input
    Unification has unusually clean algebraic properties, which makes it one of the best targets for property-based testing. Designing that suite is a testing subject; the properties themselves are stated here.