The Type Checker Finds the Most General Shape

The nicest type error is the one that tells you the shape of your program.

Not the surface shape:

let id = \x -> x in pair (id 1) (id true)

The hidden shape:

(Int, Bool)

and the receipt:

id : forall 'a. 'a -> 'a

That small forall is doing more work than it looks. It says the function was checked once, then used at two different types without duplicating code and without lying about either call site. In a Hindley-Milner language, the type checker is not guessing that receipt. It is solving equations and returning a principal type scheme: the most general type from which the other valid types can be obtained by substitution.

This post is about that receipt. It is not a tour of every modern type-system feature. No classes, no traits, no subtyping, no row polymorphism, no effects system. Just the little machine that made ML-style inference feel unreasonably good: unification, Algorithm W, let-generalization, and the occurs check.

The Receipt Is More General Than The Purchase

Take the identity function:

\x -> x

It could have type:

Int -> Int
Bool -> Bool
(Int, Bool) -> (Int, Bool)

Those are not three unrelated facts. They are instances of one fact:

forall 'a. 'a -> 'a

Replace 'a with Int and you get Int -> Int. Replace it with Bool and you get Bool -> Bool. The principal type is the shape that has not yet spent its degrees of freedom.

Hindley’s 1969 paper proved this kind of principal type-scheme theorem for combinatory logic.¹ Milner’s 1978 paper brought a polymorphic type discipline and a working inference algorithm into the setting of a programming language, motivated by ML in the Edinburgh LCF system.² Damas and Milner’s POPL 1982 paper then gave the classic principal-type result for functional programs and the algorithmic account now usually taught as Algorithm W.³

The historical line matters because it explains the vibe. The type checker is not a bag of local warnings. It is a theorem-producing machine. Its output says:

here is the weakest type claim strong enough to explain this expression

Weakest is good. A more specific type throws away reusable information.

The Lab

The lab below implements a tiny deterministic Algorithm W for a lambda calculus with integers, booleans, functions, pairs, let, and two primitive functions:

inc : Int -> Int
not : Bool -> Bool

The controls are intentionally narrow. Choose a program, toggle let-polymorphism, and toggle the occurs check. The trace panel shows the checker manufacturing fresh type variables, looking up schemes, unifying equations, and binding substitutions. The comparison panel reruns the same program under nearby rules so the contract becomes visible.

Program: Let rule: generalize lets Safety: occurs check

let id = \x -> x in pair (id 1) (id true)

Fresh variable Unification Binding / success Generalization / warning Type error

Deterministic toy implementation. The AST is fixed by the selected preset, so the experiment is about inference rather than parsing. The exported audit checks polymorphic reuse, monomorphic-let failure, occurs-check failure, recursive-type behavior when the occurs check is disabled, primitive mismatch, and the rank-2-shaped lambda case.

At the default setting, the checker accepts the program:

let id = \x -> x in pair (id 1) (id true)

The result is:

(Int, Bool)

The important event is not the final pair. It is the let-bound scheme:

id : forall 'a. 'a -> 'a

Turn off generalize lets and the same program fails. The checker now treats id as having one monomorphic type variable. The first use binds that variable to Int; the second tries to bind it to Bool. The complaint is not a quirk. It is the direct consequence of removing the one place where ordinary Hindley-Milner creates reusable polymorphism.

Unification Is The Accountant

Robinson’s 1965 resolution paper made unification central to automated deduction: find a substitution that makes two symbolic expressions the same.⁴ Hindley-Milner inference uses the same kind of machinery on types.

For a function application:

f x

the checker invents a fresh result type:

'r

then asks for:

type(f) = type(x) -> 'r

If f is inc, the equation becomes:

Int -> Int = type(x) -> 'r

Unification decomposes arrows, producing:

type(x) = Int
'r      = Int

Those bindings form a substitution. The substitution is not commentary. It is the state of the proof. Every later equation is read through it.

That is why the lab’s substitution ledger is the heart of the visualization. Algorithm W is often presented as a recursive function:

W(env, expr) -> (substitution, type)

but the operational feel is a ledger:

make a fresh variable
emit an equation
solve the equation
rewrite the world through the solution
continue

The elegance comes from how little local syntax the checker needs. A lambda introduces a fresh type for its parameter. A variable instantiates a scheme from the environment. A pair infers two sides. A let infers the right-hand side, generalizes what is not already forced by the environment, and continues.

Let Is The Polymorphism Gate

Why should let get special treatment?

Because the expression:

let id = \x -> x in pair (id 1) (id true)

has a sharing boundary. The right-hand side can be checked once:

\x -> x : 'a -> 'a

and then the variables not mentioned by the surrounding environment can be closed into a scheme:

forall 'a. 'a -> 'a

Each use of id instantiates that scheme with fresh variables:

id 1     : instantiate forall 'a. 'a -> 'a as 't0 -> 't0
id true  : instantiate forall 'a. 'a -> 'a as 't1 -> 't1

The two call sites do not fight over a single 'a.

Lambda-bound variables are different. Try the lab’s needs rank-2 polymorphism preset:

\f -> pair (f 1) (f true)

It fails in vanilla Hindley-Milner. The parameter f is introduced with one monomorphic type variable in that lambda body. The first call wants:

f : Int -> 'a

The second call wants:

f : Bool -> 'b

Those demands are incompatible. You may know a function such as identity could serve both roles, but the expression promises that any argument f can do so. That requires a type more like:

(forall 'a. 'a -> 'a) -> (Int, Bool)

where the argument itself is polymorphic. That is rank-2 polymorphism. It is not inferred by plain Algorithm W.

This distinction is one of the reasons HM inference feels both powerful and restrained. It gives you polymorphic let without asking for annotations, but it does not infer arbitrary higher-rank types.

The Occurs Check Is Where Infinity Knocks

Now choose:

\x -> x x

The checker gives x a fresh type:

'a

The application x x asks for the left x to be a function from the right x to some result:

'a = 'a -> 'b

That equation has no finite simple type. It says a type must contain itself. The occurs check rejects it.

Turn off occurs check in the lab. The machine will record a recursive binding instead of stopping. That is not a sound version of the tiny HM system; it is a way to see the forbidden shape. Some languages deliberately include recursive types, but then the type algebra and proof obligations change. Vanilla Algorithm W is not secretly doing that.

Milner calls out this limitation in a related form: equations such as a stream type that unfolds into a function returning more of itself are not solvable by ordinary unification unless infinite type expressions are admitted.² The occurs check is the guardrail that keeps “most general” from becoming “infinitely self-referential.”

Principal Does Not Mean Omniscient

A principal type is not the same thing as “the best type a human could imagine.” It is the best type within a particular system.

Plain HM has a very clean bargain:

lambda parameters are monomorphic within the body
let-bound expressions may be generalized
applications generate equations
unification solves first-order type variables

Stay inside that bargain and the checker can infer principal types without annotations. Move outside it and something must give.

Higher-rank polymorphism is one example. Effects are another. In a pure language, generalizing many let-bound expressions is fine. In a strict language with references, exceptions, or continuations, naive polymorphic generalization can become unsound. Wright’s “Simple Imperative Polymorphism” describes the standard practical repair: restrict polymorphism to values, sacrificing some pure-HM-typable expressions to smoothly incorporate imperative features.⁵ OCaml exposes the same pressure through weak type variables and the value restriction.⁶

That does not make Algorithm W a museum piece. It makes it a reference design. Modern type checkers keep renegotiating the same contract:

How much can the compiler infer?
How general should inferred types be?
Which effects or abstractions make generalization unsafe?
Where should the programmer annotate intent?

The miracle of the classic system is that the base contract is small enough to implement in a blog post lab and strong enough to explain a family of real languages.

A Debugging Habit

When a HM-like checker surprises you, read the program as equations.

For an application, ask:

what type did the function position need to have?
what type did the argument position actually force?

For a let binding, ask:

which variables were generalized?
which variables were already fixed by the environment?
is the right-hand side a value in this language?

For a strange infinite-looking error, ask:

did some variable need to be both a value and a function over itself?

This habit is better than memorizing error messages. The checker is not judging style. It is solving a constraint system and showing you where the ledger stopped balancing.

The Shape It Returns

I like principal types because they are a rare compiler artifact with humility.

They do not say:

this is the only way to think about your program

They say:

within this language of types, this is the least commitment that explains it

That is a beautiful kind of static analysis. The checker walks the syntax, spends fresh variables, accumulates equations, refuses infinite self-reference, and generalizes exactly at the boundary where reuse becomes sound.

The result feels like magic when it appears under your cursor:

compose : forall 'a 'b 'c. ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b

But it is not magic. It is accounting, done with taste.