Module elaborate 

R4 — the elaborator: metavariables, unification, and implicit-argument inference.

The layer between the surface language and the trusted kernel. A user writes id 0 and means id Nat 0; length xs and means length Nat xs. The elaborator fills the gaps: it inserts METAVARIABLES (?A, …) for the omitted/implicit arguments and SOLVES them by UNIFICATION against the types it infers, producing a fully-explicit kernel Term that infer_type then re-checks. Nothing here is trusted — elaboration only constructs a term; the kernel still certifies it.

A metavariable is represented as a Term::Var whose name starts with ? (a character no real binder uses), so the whole machinery rides on the existing Term with no new variant. Scope: first-order unification with the occurs-check, and implicit-argument insertion driven by an explicit implicit/explicit mask — the core that makes the surface usable. (Higher-order / pattern unification is the next layer.)

Structs

MetaCtx

The metavariable context: fresh-name supply + the substitution being solved.

Enums

ParamKind

How a function parameter is supplied during elaboration.

Constants

ANON_CTOR_MARKER

Reserved head marking a surface anonymous constructor ⟨e₁, …, eₙ⟩ (E3). The parser emits ⟨anon⟩ e₁ … eₙ; the elaborator (this module) rewrites it to the sole constructor of the expected inductive and then discards the marker — it NEVER reaches a kernel term. The name contains ⟨/⟩, characters the identifier lexer cannot produce, so it can never collide with a user global. Like the ?-prefixed metavariables above, this rides on the existing Term with no new variant.

DOT_MARKER

Reserved head marking surface dot notation receiver.field (E4). The parser emits ⟨proj⟩ receiver field (the field name carried as a Global); the elaborator rewrites it to the projection H_field params… receiver and discards the marker. Collision-proof for the same reason as ANON_CTOR_MARKER.

Functions

auto_bind_implicits

Auto-bind free type variables as leading implicit parameters. A definition written id : A -> A := fun a : A => a mentions A as a FREE, unregistered, single-uppercase global — the type-variable convention. This pass generalizes each such variable: it prepends Π(A:Type) to the type and λ(A:Type) to the body (converting Global(A) to the bound Var(A)), and returns the new implicit count, so A becomes an inferred implicit argument. Definitions that already bind their parameters reference them as Vars, not free Globals, so they are untouched — this only rescues what was previously an unbound-variable error.

bind_self_recursion

Replace every Global(name) by Var(name) (turning a free type-variable reference into a reference to the binder this pass prepends). Recursive-definition sugar: if body refers to the definition’s own name as a free Global, bind that self-reference with a fix so the definition can call itself — Definition f : T := … f … . becomes f := fix f. …. The kernel’s termination guard (run by infer_type) then certifies the recursion decreases structurally; a body with no self-reference (or one that already wrote an explicit fix, whose self-references are already bound Vars) is returned unchanged. A self-reference SHADOWS any same-named global, so a recursive Definition add over Nat overrides a built-in add.

elaborate

Elaborate term (which may contain Holes) against an optional expected type, solving the holes by unification. Returns the elaborated term and its type (both still containing metavariables until instantiated).

elaborate_anon_ctor

Elaborate an ANONYMOUS CONSTRUCTOR ⟨f₀, …, fₙ⟩ (E3) against an EXPECTED inductive/ structure type H a…. It applies H’s (unique) constructor to the type parameters a…, read off the expected type, then the field values — so ⟨Zero, true⟩ expected at Prod Nat Bool becomes Prod_mk Nat Bool Zero true. Each field is elaborated against its declared type (so coercions/implicits fire), and the whole is kernel-certified.

elaborate_app

Elaborate an application of head (of type head_ty) where leading parameters may be implicit or instance-implicit (kinds[i]). A fresh metavariable is inserted for each implicit position; instance positions get a placeholder metavariable whose resolution is DEFERRED until all explicit arguments (which may pin the class’s type variables) have been unified. Returns the fully explicit, metavariable-instantiated term and type.

elaborate_app_against

Like elaborate_app but with an EXPECTED result type. After the explicit arguments are processed, the result type is unified with expected — so an implicit that the arguments alone do not pin (e.g. the A of nil : {A} → List A, which has no value argument) is solved from the surrounding context. The expected-type pass runs BEFORE instance resolution, so a class’s type variable can be fixed by the context too.

elaborate_dot

Elaborate DOT notation receiver.field (E4). The receiver’s type head names an inductive/structure H; the projection is H_field (K4’s convention), applied to H’s parameters — read off the receiver’s type — and then the receiver itself. So p.fst with p : Prod A B becomes Prod_fst A B p. Returns an error if no such projection exists or the result does not type-check.

elaborate_in

Like elaborate but under a LOCAL CONTEXT lctx of bound variables. ctx is the kernel context already EXTENDED with those same variables (so infer_type sees them at the leaves), while lctx is the parallel (name, type) list the unifier uses for higher-order PATTERN unification. Descending under a λ extends both — which is how a metavariable applied to a bound variable (a motive ?P n) gets solved in a body.

fill_match_motives

Fill in inferred motives for match expressions written WITHOUT a return clause (the Hole motive the parser leaves). The motive is a CONSTANT λ_:I. T — covering non-dependent matches — where T is the EXPECTED type (a definition’s declared result type, propagated through binders) or, lacking one, the type of a nullary first branch. The pass threads the kernel context through binders so the discriminant’s type resolves; a match it cannot give a motive (a dependent case, no expected type) is reported so the user can add an explicit return.

instantiate

Substitute every solved metavariable throughout term (transitively, since a solution may itself mention other metavariables — the occurs-check keeps this terminating).

is_meta

Whether name denotes a metavariable (the ?-prefix convention).

resolve_coercion

Find a registered coercion carrying from to to (up to unification), returning the coercion FUNCTION to wrap the argument in — Lean’s ↑. The elaborator calls this when an argument’s type does not match the expected parameter type; a match commits the unification (a polymorphic coercion’s type variables get solved).

resolve_instance

Search the Context’s instance database for an instance proving required, returning the (metavariable-instantiated) instance term. Handles POLYMORPHIC / RECURSIVE instances (instance {A} [Inhabited A] : Inhabited (List A)): the instance’s parameter telescope is freshened to metavariables, its conclusion is unified against required (solving the type parameters), and each PREMISE parameter is then resolved RECURSIVELY. The first instance that fully resolves wins; failed trials never pollute mctx (each runs on a clone, committed only on success).

surface_elaborate

Elaborate a whole surface term: walk it, and at every application of a global with declared implicit parameters (Context::implicit_args), insert and infer those arguments — so id 0 becomes id Int 0. Terms with no implicits are returned unchanged. The result is fully explicit and metavariable-free; the kernel certifies it as usual. This is the seam that wires the elaborator into the REPL.

surface_elaborate_against

Like surface_elaborate but with an EXPECTED type (e.g. a definition’s declared type). The expected type is propagated to the top-level application/global so an implicit with no value argument — nil : {A} → List A used where a List Int is wanted — is inferred from context.

unify

First-order unification of a and b, solving metavariables into mctx. Returns whether they were made equal. A metavariable unifies with anything (after the occurs-check); everything else decomposes structurally.

unify_in

Unify a and b under a LOCAL CONTEXT lctx ((name, type) of the bound variables in scope). The local context enables higher-order PATTERN (Miller) unification: ?M x̄ =?= t, where ?M is a metavariable applied to distinct bound variables x̄, is solved by ?M := λx̄. t. The top-level unify runs with an empty context, so its behavior — and every existing caller — is the first-order one.