Elaboration: from syntax to Expr

Macros run first

A macro maps syntax to syntax. Asking for one step of expansion of the same term shows what if is notation for:

let_mvar% ?m✝ := 1 < 2; wait_if_type_mvar% ?m✝; ite✝ ?m✝ 3 4

I expected ite (1 < 2) 3 4, and the last step is that call. The two steps before it are instructions to the elaborator: elaborate the condition into a metavariable ?m (a hole to be filled later), and don't continue until its type is known. The macro can't check the type itself, because types don't exist at this stage. All it can do is emit syntax telling the elaborator what to check. The ✝ marks names made hygienic by the macro system, so a local variable you happen to call ite can't capture the call.

What the elaborator produces

Turning off notation in the pretty printer shows the term the elaborator built:

ite (LT.lt 1 2) 3 4 : Nat

ite also takes a Decidable (1 < 2) instance, which is how it can compute with a proposition. That argument is in square brackets in the signature of ite, so the printer leaves it out. Even this view hides a lot. pp.all prints every implicit argument and instance. Here is 1 + 1:

@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat)
  (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))
  (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1))) : Nat

The three characters 1 + 1 became a call to HAdd.hAdd with three type arguments, universe levels and an instance. Each 1 became OfNat.ofNat applied to a type, a raw literal (nat_lit 1) and another instance. The elaborator chose Nat for all of them because nothing else constrained the type, a rule covered later in this post.

Expr is an ordinary inductive type

The result is a value of Lean.Expr, an inductive type with constructors for constants, applications, lambdas, bound variables and a few more. Calling the elaborator directly and printing the raw value shows them. (mkIdent stops the quotation from making x hygienic, which would print as a long generated name.)

Lean.Expr.lam `x (Lean.Expr.const `Nat []) (Lean.Expr.bvar 0) (Lean.BinderInfo.default)

Reading it from left to right: a lambda (lam) whose binder is named x, whose binder type is the constant Nat with no universe arguments, whose body is bvar 0, and whose binder is explicit (BinderInfo.default, as opposed to {x} or [x]). The body refers to x as bvar 0, not by name. Bound variables are de Bruijn indices: bvar 0 means "the nearest enclosing binder", bvar 1 the one outside that, and so on. The name x is kept only for printing, which is why renaming a bound variable never changes the term.

This is the whole interface between the elaborator and the kernel. The kernel never sees Syntax, macros, implicit arguments or instances as such. It sees an Expr in which all of those have already been written out, and it checks that term. The rest of this post looks at how the elaborator fills in the parts you left out.

An underscore is a metavariable

Writing _ asks the elaborator to make a metavariable and fill it by unification. Here the witness of an existential is left out:

Exists.intro 3 rfl : ∃ n, n + 2 = 5

The anonymous constructor became Exists.intro ?w rfl. The expected type says rfl must prove ?w + 2 = 5, and rfl proves a = a, so unification has to solve ?w + 2 =?= 5. That's the same literal trick as before, one level deeper, and it gives ?w := 3.

Unification finds a solution, not the value you might have in mind. If the hole is on the right of an equation, the obvious solution is to copy the left side:

rfl : 2 + 3 = 2 + 3

The hole was filled with 2 + 3, not 5. Nothing asked for the sum to be computed, and copying is the first solution isDefEq finds.

When a hole stays empty

If nothing constrains a metavariable, it's still unassigned when the elaborator finishes, and the definition is rejected:

don't know how to synthesize implicit argument `α`
  @id ?m.4 ?m.3
context:
⊢ Sort ?u.2

don't know how to synthesize placeholder for argument `a`
context:
⊢ ?m.4

Failed to infer type of definition `mystery`

There are three errors because there are three holes. id has the signature {α : Sort u} → α → α, so id _ creates ?u for the universe, ?m.4 for α and ?m.3 for the argument. The only constraint is that the argument has type ?m.4, which relates two holes without filling either. There is no expected type either, since mystery has no type annotation. Adding one fixes α but not the argument:

don't know how to synthesize placeholder for argument `a`
context:
⊢ Nat

Unification only ever solves an equation. It never invents a term out of nothing.

The elaborator does have a few tricks for holes that unification can't fill. Instance resolution fills [...] arguments, coercions repair type mismatches, and default instances choose a type for a bare numeral. The next sections cover them.

Implicit arguments are metavariables

An argument in curly braces is implicit. You don't write it. At each use, the elaborator creates a metavariable for it and lets unification fill it in. @ turns this off and shows the full signature, and a named argument fills one implicit argument by hand:

id 5 : Nat

@id : {α : Sort u_1} → α → α

id 5 : Int

In id 5, the elaborator makes ?α, then elaborates 5 against the expected type ?α. A numeral alone doesn't fix its type, so ?α becomes Nat by the default rule covered at the end of this post. With (α := Int) the hole is filled before 5 is elaborated, so the same numeral becomes an Int. α is one argument, and implicit only means the elaborator usually fills it in for you.

Instance arguments are filled by search

An argument in square brackets is an instance argument. It also becomes a metavariable, but unification is the wrong tool for it. Nothing in 1 + 1 mentions an addition function, so no equation could determine it. Here is the signature of the function behind +:

@HAdd.hAdd : {α : Type u_1} → {β : Type u_2} → {γ : outParam (Type u_3)} → [self : HAdd α β γ] → α → β → γ

The types of the two operands, α and β, are implicit and come from unification with the operands. The instance [self : HAdd α β γ] can't come from unification. The result type γ is marked outParam, which tells instance resolution not to wait for γ to be known: it searches using α and β alone, and the instance it finds decides γ.

For an argument like this, the elaborator runs instance resolution. It looks for a declaration marked instance whose type matches the goal. #synth runs the same search directly:

instHAdd

That's the @instHAdd Nat instAddNat in the pp.all output earlier. instHAdd itself has an instance argument, [Add α], so finding it started a second search, for Add Nat, which instAddNat answers.

Watching the search

Instances that take instance arguments are how type classes compose, and the search can be traced. Here is a small class, a base instance, and an instance that builds a Shape for a pair out of Shape instances for its parts:

instShapePair

[Meta.synthInstance] ✅️ Shape (Pair Square Square)
[Meta.synthInstance] ✅️ new goal Shape (Pair Square Square)
[Meta.synthInstance.instances] #[@instShapePair]
[Meta.synthInstance.apply] ✅️ apply @instShapePair to Shape (Pair Square Square)
[Meta.synthInstance.tryResolve] ✅️ Shape (Pair Square Square) ≟ Shape (Pair Square Square)
[Meta.synthInstance] ✅️ new goal Shape Square
[Meta.synthInstance.instances] #[instShapeSquare]
[Meta.synthInstance.apply] ✅️ apply instShapeSquare to Shape Square
[Meta.synthInstance.tryResolve] ✅️ Shape Square ≟ Shape Square
[Meta.synthInstance.answer] ✅️ Shape Square
[Meta.synthInstance.resume] ✅️ propagating Shape Square to subgoal Shape Square of Shape (Pair Square Square)
[Meta.synthInstance.resume] size: 1
[Meta.synthInstance.resume] ✅️ propagating Shape Square to subgoal Shape Square of Shape (Pair Square Square)
[Meta.synthInstance.resume] size: 2
[Meta.synthInstance.answer] ✅️ Shape (Pair Square Square)
[Meta.synthInstance] result instShapePair

On the page the trace starts collapsed; click its first line to expand it. Reading it from the top:

1. For the goal Shape (Pair Square Square), only one instance has a matching type, the unnamed pair instance, which Lean named instShapePair.

2. Applying it uses unification (≟) to match its conclusion Shape (Pair ?α ?β) against the goal, which sets ?α and ?β to Square. That leaves its two instance arguments as new goals, both Shape Square.

3. instShapeSquare answers Shape Square.

4. The answer is passed back up to both waiting arguments (size: 1, then size: 2), and with both filled the original goal is answered.

new goal Shape Square appears only once, although two arguments needed it. The search stores every answer it finds and reuses it when the same goal comes up again, so Shape Square was solved once.

When the search fails

If no instance matches, the elaborator reports the goal it couldn't solve:

failed to synthesize instance of type class
  HAdd String String ?m.3

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

fun s => sorry : (s : String) → ?m.6 s

The goal still has a metavariable in it: ?m.3 is the outParam result type, which only a matching instance could have filled. Strings are joined with ++ (HAppend), and there is no HAdd String instance. The second message shows that elaboration doesn't stop at the first error. The failed subterm is replaced by sorry and the rest of the term is still elaborated, which is how one mistake doesn't hide every error after it.

Coercions repair a failed unification

When an argument's type doesn't unify with the type the function expects, the elaborator doesn't give up straight away. It searches for a coercion from one type to the other, using the Coe family of classes, and wraps the argument in it:

fun n => addInt (↑n) 1 : Nat → Int

fun n => addInt n.cast (OfNat.ofNat 1) : Nat → Int

n : Nat failed to unify with Int, so the elaborator inserted a coercion, printed ↑n. Turning off pp.coercions shows what's really in the term: Nat.cast n. With the option off, numerals also print as OfNat.ofNat calls. That's a printing difference only, and the term is the same. Note what didn't change: 1 was elaborated as an Int from the start, because its expected type was known, so it needed no coercion.

The coercion isn't kept as a call to Coe.coe. The elaborator unfolds the instance and puts its body in the term. A user-defined coercion makes this visible:

twice { val := Nat.toFloat 3 } : Meters

twice { val := Nat.toFloat (OfNat.ofNat 3) } : Meters

There's no ↑ this time, even with coercion printing on. The instance body ⟨n.toFloat⟩ was put into the term, and nothing marks it as a coercion. Nat.cast printed as ↑ because it is tagged @[coe], which tells the printer to show it as an arrow. Wrapping the body in a tagged function brings the arrow back:

twice ↑3 : Meters

There are now two Coe Nat Meters instances. When instances have the same priority, the one declared later is tried first, so this one wins.

Because coercions are unfolded during elaboration, the kernel never sees anything special. It checks an ordinary function application.

Default instances choose a type for numerals

A numeral like 1 elaborates to OfNat.ofNat ?α 1, which needs an OfNat ?α 1 instance. If nothing ever determines ?α, there is no type to search for. For this case Lean has default instances. instOfNatNat is marked @[default_instance], so when the elaborator runs out of other work with an OfNat ?α n goal still open, it tries that instance, which sets ?α := Nat:

fun x => x + 1 : Nat → Nat

Nothing said what x is. Its type and the type of 1 were both holes, linked by +, and the default filled both with Nat.

A default is a last resort. It applies only after the other constraints have had their chance, even when the constraint comes later in the text:

(fun x => x) 5 : Nat

(fun x => x + 1) 5 : Int

In the second line, (1 : Int) inside the function fixes the type of x, and so the type of 5, before any default is tried.

The default can surprise you, because Nat subtraction truncates at zero:

0

-1

Nothing in 2 - 3 asks for a type, so the default makes it a Nat subtraction.