The Type Checker: Hindley–Milner, Written in Mere

The evaluator runs a program without caring whether it makes sense. The type checker is the component that cares — the one that rejects 1 + "hello" before it ever runs instead of failing halfway through. It is the harder of the two to self-host, and the reason is a difference in kind: the evaluator only has to compute, walking the tree and producing values, but the type checker has to solve, running the quiet inference algorithm that sits at the very center of the language.

The algorithm the evaluator didn’t need

That algorithm is Hindley–Milner inference, the same one named back in the episode on the minimal core — the machinery that lets you write fn x -> x with no type annotation and have the compiler work out, on its own, that it can be used at int and at bool. Self-hosting the type checker means rebuilding that machinery in Mere, and it comes down to a few pieces that keep reappearing in any HM implementation.

There is a fresh type variable — a placeholder for a type not yet known, minted whenever the checker meets something it can’t pin down immediately. There is unification, the heart of the whole thing: given two types that must be equal — the parameter a function expects and the argument it was handed — make them equal, binding the unknowns as you go, or fail if they can’t be reconciled (int against str is a type error; a function type against a function type recurses into argument and result). Unification is guarded by an occurs check, which refuses to bind a variable to a type that contains it, so inference can’t build an infinite type. And there is the pair that makes polymorphism work: generalization, which turns an inferred type into a reusable scheme by quantifying over the unknowns that are genuinely free, and instantiation, which gives each use of a polymorphic value its own fresh copy of that scheme. Generalize-then-instantiate is exactly what lets one id serve every type — the subtle, load-bearing detail of let-polymorphism, and the part it would be easiest to get quietly wrong.

The evaluator needed none of this. Computing a value is direct; solving for a type is a constraint problem, and expressing the solver in Mere is the language articulating the very mechanism that gives it its types.

Most of the original isn’t in scope

The OCaml type checker is nearly nineteen hundred lines, and as with the evaluator, the honest move is to notice how much of that does not need self-hosting. Roughly a third of it is the advanced static analysis from earlier parts — the borrow checker, region tracking, capability and effect inference, the machinery of Parts II and III. Another slice is user-experience polish: did-you-mean suggestions for misspelled names, the niceties that make an error message kind. Set those aside, as out of scope for now, and what remains is the core Hindley–Milner inference — around seven hundred lines of Mere, the same order of size as the evaluator.

That scoping is itself a decision worth stating plainly, in the spirit of the coverage ledger from Part IV. The self-hosted type checker checks the polymorphic functional heart of the language; it does not yet re-implement the borrow modes, the regions, or the effect system that make Mere distinctive. Those stay in the OCaml reference for now, and saying so is more honest than letting “the type checker is self-hosted” imply more than it does. Self-hosting advances one layer at a time, and this layer is the classical core.

One place two variables had to be told apart

A small but telling wrinkle sits at the start. The syntax tree already has a notion of a type variable — the 'a a programmer writes in an annotation, carried through by the parser. But the inference algorithm needs its own kind of variable: the fresh unknowns it invents while solving, which are a different thing entirely. One is a name the user wrote; the other is a hole the checker is trying to fill. They look alike — both are “type variables” — and conflating them would be a bug, so the self-hosted checker had to give the inference unknowns a distinct representation.

This is the language’s own recurring instinct — when one name is quietly carrying two meanings, split them — surfacing now inside its own implementation. The same discipline that unified region and arena, and that separated the two axes of a borrow, applies here to two things that both happen to be called type variables and are not the same. Writing the type checker in Mere meant confronting a distinction the language’s design cares about, in the checker that enforces the language’s design.

The pipeline closes

Like every self-hosted component, the type checker is cross-validated: the types it infers are checked against the types the OCaml type checker infers, on a corpus of programs, and required to match. And with it in place, the whole front-to-back pipeline exists in Mere — parse, type-check, evaluate — each stage written in the language, sharing the one syntax tree, each held to its OCaml reference. Compiled to Wasm and dropped into a browser, it becomes the thing the demo had been reaching toward across three episodes: paste a Mere program, and a Mere pipeline infers its type and computes its result, entirely self-hosted.

There is a closing-of-the-loop worth naming. The very first episodes argued that Mere optimizes for programs you can be sure of, and that inference and explicitness were meant to reconcile rather than fight — you write the types that matter and let the rest be inferred. The type checker is the machine that makes that reconciliation real, and it is now written in Mere itself. The mechanism that gives the language its guarantees is expressed in the language it guarantees.

One piece of the compiler is still missing from the self-hosted set. The pipeline can read, check, and interpret Mere — but interpreting is not compiling. To close self-hosting completely, Mere must be able to emit code: to take a checked program and produce something a machine runs directly. Next: the code generator, written in Mere, and the moment the language can compile itself.