Elaboration: Filling in What the Program Did Not Say

A dependently typed program is written with holes. The type of a function mentions a length, and the length is often obvious from the arguments, so the programmer omits it. A definition’s return type is inferred from its body. A record field’s type is determined by earlier fields. None of these omissions is a convenience layered over a fully explicit language; the elaborator is the component that makes the surface language usable, and its behaviour determines which programs are accepted.

The core language is fully explicit

The checker at the bottom of the stack accepts only terms in which every binder is annotated, every implicit argument is supplied, and every universe level is fixed. This core language has a small, precisely specified syntax and typing rules, and its properties are what the metatheory is about. It is also unreadable.

Elaboration is the translation from surface syntax to core. It is bidirectional in the technical sense: the elaborator alternates between checking a term against an expected type, where the type is known and can be used to resolve omissions, and inferring a type for a term, where the term’s structure determines the type. The mode is not a property of the source but of the position: the same expression may be checked in one place and inferred in another, and the elaborator switches modes as it descends.

The switch has a cost. In inference mode, an unannotated lambda cannot be processed, because nothing determines the type of its bound variable. In checking mode the same lambda is fine, because the expected type supplies the binder’s type and the body is checked against the codomain. This is why surface languages allow a lambda in an argument position only when the expected type is known, and why an error message about an ambiguous binder often means the surrounding annotation is missing rather than that the lambda is wrong.

Metavariables as placeholders

An omitted argument is represented by a metavariable: a fresh constant that stands for a term to be determined later. Each metavariable has a type, which is itself a term possibly containing other metavariables, and a context recording which variables are in scope where it was created.

The context restriction matters. A metavariable created inside a branch of a case expression must not be solved by a term mentioning a variable bound outside that branch, or the resulting term would have a free variable with no binding. Implementations enforce this by recording the scope and rejecting solutions that escape it, which is why a solution found in one branch sometimes cannot be reused in another and the elaborator must solve the same metavariable twice.

Metavariables are solved by unification, and unification in dependent type theory is not the first-order unification of logic programming. Two types are unified when they are definitionally equal, so the unifier must reduce as it goes, and the terms being unified may contain lambdas whose bodies must be compared under fresh variables. The algorithm is therefore a constraint solver that interleaves reduction with structural decomposition, and it is incomplete: there are unifiable pairs it will not solve without help, and the standard response is to postpone the constraint and retry when more information is available.

Implicit arguments and their insertion

The surface language marks certain parameters as implicit, meaning the elaborator should insert them. When a function is applied without its implicit arguments, the elaborator creates a metavariable for each omitted one and continues. Whether the application typechecks then depends on whether those metavariables get solved by the expected type, by later arguments, or by the constraints accumulated so far.

Insertion order is a design decision with visible consequences. If a function takes an implicit type parameter and an implicit length, the elaborator inserts them left to right, and a later explicit argument that determines the length cannot help solve the earlier metavariable unless the solver postpones. Systems that postpone do better on programs written in a natural order; systems that do not require the programmer to reorder parameters or supply the argument explicitly.

The failure mode is characteristic. A metavariable that remains unsolved at the end of elaboration is reported as an unsolved constraint, and the message names a position in the source that may be far from the actual problem. A program that fails to elaborate is not necessarily ill-typed; it may be well-typed with an argument the elaborator could not find. The distinction matters because the fix is different: an ill-typed program needs a different term, an unsolved metavariable needs an annotation or an explicit argument.

Proof search inside elaboration

Some omitted arguments are not determined by unification but by search. A function may require an instance of a type class, a proof of an ordering, or a witness of a decidable predicate, and the elaborator must find one from the available instances and lemmas.

This is a bounded search over a database of candidates, with depth and branching limits. It resembles the backward search of a sequent calculus, in that both work back from a goal, but it is heuristic: it resolves the common cases and gives up on the rest. The database is typically indexed by the head of the goal, so a goal whose head is a type constructor only considers instances whose conclusion has that head, or a variable head matched against that constructor. On libraries with thousands of instances, that index is what keeps a failure from expanding into a search over the whole database.

The interaction between search and unification is where most elaboration bugs live. A search that commits to a candidate may solve metavariables in a way that later constraints contradict, and backtracking must undo those solutions. Implementations either record a trail of solved metavariables and undo it on backtracking, or restrict search so that it never solves metavariables outside its own subgoal. The first is more general and harder to get right; the second is predictable and fails on some programs that a human would consider obvious.

Why the elaborated term is the artifact

The elaborator’s output is what gets checked, stored, and printed. A definition in a compiled library is the core term, not the surface syntax, which is why recompiling with a different elaborator version can change the meaning of a program that typechecked before. It is also why error messages refer to core terms with generated names, and why a programmer reading a goal state sees metavariables numbered rather than named. Some systems record the source position that created each metavariable and print it alongside the number, which narrows the gap between the message and the program without changing what is checked.

The design constraint is that elaboration must be deterministic. Given the same source and the same environment, it must produce the same core term, or libraries cannot be reproduced and proofs cannot be checked independently. Determinism rules out search strategies that depend on hash iteration order or on timing, and it forces the elaborator to fix an order for solving constraints even when several orders would succeed.

A second constraint is that elaboration must not be trusted. The core term it produces is re-checked by a small kernel, and the kernel’s acceptance is what makes the result correct. The elaborator may be arbitrarily complicated, may have bugs, and may produce a term the programmer did not intend; if the kernel accepts it, the term is well-typed. This separation is the reason proof assistants can have large tactic libraries and complex automation without trusting them, and it is the same architecture discussed in The De Bruijn Criterion and Kernel Design.

The failure surface

Three failure modes account for most elaboration trouble.

Underdetermined arguments. A metavariable that no constraint determines. The term is ambiguous rather than wrong, and the fix is an annotation.

Overconstrained search. An instance search that commits early and fails late. The goal may be provable, and the search order prevents it. The fix is usually to restructure the instance so that its head is more specific.

Universe constraints. A definition that forces a level higher than expected, producing a constraint the solver cannot satisfy. The message is about levels rather than about logic, and the fix is to restructure the definition so that the offending quantification does not cross a universe.

None of these is a type error in the core language. All three are properties of the translation, and they are why the surface language’s documentation has to describe the elaborator’s behaviour and not only the type system’s rules.