Bug in elaboration?

Stream: lean4

[Jireh Loreaux]

Per our variable inclusion rules, it seems to me that B should not be included. But if you look at the trace, you'll see Add B is mentioned. This seems like a bug to me. Am I wrong, if so, why?

import Lean

variable {A B : Type} [Add A] [Add B]

set_option trace.profiler.useHeartbeats true in
set_option trace.profiler true in
theorem foo (a₁ a₂ : A) : a₁ + a₂ = a₁ + a₂ := rfl

[Aaron Liu]

I think you are still in the statement at that point

[Jireh Loreaux]

(Note: B is not included in the declaration added to the environment, but I don't understand why Add B appears in the trace at all.)

[Jireh Loreaux]

yes, so?

[Aaron Liu]

All the variables are included when elaborating the statement, and then only relevant ones are included when elaborating the proof

[Aaron Liu]

Otherwise you wouldn't be able to refer to A

[Kyle Miller]

The local context at rfl is

A : Type
inst✝ : Add A
a₁ a₂ : A
⊢ a₁ + a₂ = a₁ + a₂

which looks right.

[Jireh Loreaux]

aha, so here's a footgun I just realized we have. Including variable headers, especially with lots of type class hypotheses, at the top of a file leads to potentially expensive elaboration of every declaration in the file.

[Jireh Loreaux]

Also, don't we have asynchronous elaboration of the statement and the proof? or is it asynchronicity of elaboration and kernel checking?

[Sebastian Ullrich]

The statement is still synchronous

[Aaron Liu]

How would you begin elaborating the proof if you don't know the statement yet? Therefore the statement must be synchronous.

[Jireh Loreaux]

Aaron, you can infer the type of the statement from the proof, if it's provided in term mode, so that's one way. But yes, I understand your point.

[Kyle Miller]

If it's in term mode and the term doesn't need an expected type (many proof terms rely heavily on the expected type!)

[Jireh Loreaux]

yes, I understand.

[Jireh Loreaux]

By the way, the reason I came across this footgun is that it actually came up in practice in #24013

[Kyle Miller]

I think Sebastian is saying that the statement headers are synchronous by the way. There's a synchronization point between the statement header and the theorem body more specifically, and the bodies are asynchronous. (Sebastian can correct me if I'm wrong. I'm just going by what I've seen what the orange bars do on heavy files.)

One could imagine a much more complicated statement header elaborator that is asynchronous, where headers can figure out what they're defining and then later headers can wait if the type is needed.

[Kyle Miller]

What's the footgun @Jireh Loreaux?

[Jireh Loreaux]

Jireh Loreaux said:

aha, so here's a footgun I just realized we have. Including variable headers, especially with lots of type class hypotheses, at the top of a file leads to potentially expensive elaboration of every declaration in the file.

[Kyle Miller]

If I understand correctly, the reason that variables are re-elaborated at every declaration is because auto-implicits are placed before all other binders. (Autoimplicits have quadratic behavior: every time a binder has a new autoimplicit, all the binders before it are elaborated again.)

For an example of this "before all other binders" behavior, on y there is a type mismatch y has type ?m.43 : Sort ?u.42 but is expected to have type α : Type error:

def baz (α : Type) (x : α) (h : x = y) : Nat := 2

If this restriction were relaxed (perhaps each variables block could be its own autoimplicits checkpoint, and binder lists could be checkpoints as well), then I think it would be possible to elaborate a variables block just once.

Complexities:

• It's possible people have depended on autoimplicits appearing at the front.
• Variable lists can have metavariables, so we'd need to save the metavariable context. (The alternative is to turn metavariables into free variables, which is the Lean 3 behavior. I expect that would break things. Side note: Mathlib's Type* is mimicking the Lean 3 Type* when it appeared in a variable list. Lean 3 Type* is actually Type _, but the metavariable was turned into a new universe level variable at the end of variable.)
• addAutoBoundImplicits would need to be aware that autoimplicits can appear elsewhere in a parameter list, not just the front.

A benefit is that once a variable list elaborates, it's known good. Currently it's possible to break a previously elaborating variable list.