One line change gives type class search speedup of 17%

Stream: lean4

[Jovan Gerbscheid]

In lean#8915, I replaced if (← isDefEq mvar instVal) then with mvar.mvarId!.assign instVal in the type class search code that instantiates a type class goal with its value. This is possible, because mvar is an unassigned metavariable, and a different isDefEq call a few lines earlier guarantees that the type of mvar and instVal are the same.

The result on mathlib is pretty big:

| typeclass inference | -2104 s      | -17,2% |
| build               | -8500.60⬝10⁹ | -5.62% |
| lint                | -407.986⬝10⁹ | -5.78% |

A small catch

There is a bug that got exposed by this, which is that synthPending can assign metavariables that live in a lower withNewMCtxDepth depth. This bug has a funny interaction with the instance projection binderinfos that were changed in lean#5376. For example, if you write

import Mathlib

variable {α : Type} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] (a b : α)
#check IsOrderedMonoid.mul_le_mul_left a b
-- IsOrderedMonoid.mul_le_mul_left {α : Type u} {_ : CommMonoid α} {_ : PartialOrder α}
--   [self : IsOrderedMonoid α] (a b : α) : a ≤ b → ∀ (c : α), c * a ≤ c * b

Then type class synthesis gets the goal @IsOrderedMonoid α ?m.97 ?m.98, and these two metavariables get assigned illegally during the type class search, due to the bug. But if IsOrderedMonoid.mul_le_mul_left would have had the original ([CommMonoid α] [PartialOrder α]) binderinfos, this problem wouldn't arise.

There were only two places in mathlib where I had to fix something related to this.

@Kyle Miller had already proposed to switch the binderinfos back to how they were in another conversation (#lean4 > projection instance binderinfo problem @ 💬), so this gives another reason to do so.

[Kyle Miller]

Jovan Gerbscheid said:

This is possible, because mvar is an unassigned metavariable

Why does this invariant hold? It seems to me that instances can appear inside the types of other instance metavariables, and through previous isDefEqs they might be partially solved for. Is that not the case?

[Kyle Miller]

Jovan Gerbscheid said:

There is a bug that got exposed by this

Could you clarify whether this is a pre-existing bug or if it is a bug introduced by using MVarId.assign without doing any checks that the assignment is valid?

[Jovan Gerbscheid]

The bug is pre-existing, and lean#5376 caused Lean to rely on this bug when elaborating class projections.

[Kyle Miller]

Typeclass inference shouldn't be making illegal metavariable assignments no matter which way the class command decides to set up binderinfos. I'm sure you know this, but I'm not sure I understand why you mention fixing mathlib instead of fixing a bug in synthPending (or what the bug in synthPending is — I don't see anything in lean4#8915).

Do you agree that the bug in synthPendingImp is that it's using Lean.MVarId.assign directly instead of using isDefEq, which would verify the assignment is allowed?

[Jovan Gerbscheid]

I think the better fix would be to just add an explicit check for the depth in synthPendingImp. I don't think that the assignment created by synthPendingImp needs to be checked using an occurs check.

[Jovan Gerbscheid]

The reason why I haven't yet added a fix for the bug in lean#8915 is that then I would have to also revert the change made in lean#5376. Which would get rid of half of the speedup. Instead of plainly reverting lean#5376, I'd rather see some version of your proposal about choosing a better synthOrder. Although I guess that could also be done in a later PR.

[Jovan Gerbscheid]

(The fix in mathlib here is not meant as a permanent fix, but instead to be able to do the benchmarking)

[Jovan Gerbscheid]

Kyle Miller said:

Jovan Gerbscheid said:

This is possible, because mvar is an unassigned metavariable

Why does this invariant hold?

Good point, but looking closely, we can see that in consume, we filter out all the subgoals that already have been assigned. Thus, new gNodes will always have their metavariable unassigned (and since they store their own metavariable context without changing it, the metavariable stays unassigned).

[Kyle Miller]

Jovan Gerbscheid said:

I don't think that the assignment created by synthPendingImp needs to be checked using an occurs check.

Maybe it's impossible to induce a cycle, but I don't see why it's correct without an occurs check.

Jovan Gerbscheid said:

Instead of plainly reverting lean#5376

I have to check: are you working with any core developers on any of these changes? Touching typeclass inference is not something I understood anyone was going to be doing right now.

Reverting this is not going to happen just to avoid a bug in synthPendingImp. The synthOrder algorithm definitely needs to be fixed, but as far as I'm understanding it, it is independent of your changes to tryResolve, except in that your changes let it trigger a bug.

Here's my feeling about this:

• I'm still not convinced that using MVarId.assign instead of isDefEq is correct here.
• Getting speedups by using unsafe functions is not surprising (interesting, but not surprising). Just because there's a speedup using unsafe functions does not mean it's worth pursuing right now.
• I don't see why you aren't attributing the bugs to this change in tryResolve. Doesn't it seem suspicious that this causes errors elsewhere? What is assign not doing that isDefEq does?
• For core to be interested, I think it needs to be extremely well justified, and come at the right time, when someone is actively working on typeclass inference. It's a lot easier to get a bug fix in than a performance improvement that requires a careful understanding of subtle invariants in a complicated system as well.
• My understanding is that touching typeclass inference now is not the right time. I could be wrong though, since it's not my area of Lean.

Sorry to pour cold water on this (especially if I'm wrong and there's a core developer interested in pursuing your idea right now!)

[Jovan Gerbscheid]

Kyle Miller said:

Maybe it's impossible to induce a cycle, but I don't see why it's correct without an occurs check.

I'm not sure what you mean here. I thought the occurs check is to check that we don't induce a cycle.

Kyle Miller said:

are you working with any core developers?

No, I'm working on this myself

Kyle Miller said:

• I'm still not convinced that using MVarId.assign instead of isDefEq is correct here.

The things we need to check are: (1) the metavariable is unassigned, (2) the type of the assignment is correct, and (3) we don't introduce cycles.

1. As I explained above, when creating a gNode, we have already checked that the mvar is not assigned
2. With isDefEq mvarTypeBody instTypeBody we checked that the forall-body of the type of mvar is the same as the type of the lambda body of the instVal that we are assigning to it, which gives what we want. And we know that the mkLambdaFVars xs isn't doing any funny business to metavariables, because the metavariables in instVal don't depend on any of the xs.
3. instVal is created by applying an instance to the forall-body of the type of mvar. mvar is created in type class search, so it cannot appear in the (local) instances. And mvar cannot appear in any way in the type of mvar. So the constructed instVal cannot in any way contain mvar. Hence we don't need an occurs check.

Kyle Miller said:

• Doesn't it seem suspicious that this causes errors elsewhere? What is assign not doing that isDefEq does?

I agree that this is extremely suspicious, but I can explain it. In the current implementation, this isDefEq at some point reaches a subgoal that looks like f ?m =?= f ?m. Then instead of terminating with a true, the function isDefEqArgs calls the function trySynthPending on argument ?m, which causes ?m to be illegally assigned. So even though ?m =?= ?m already is true, isDefEq still decides to assign?m to the synthesized value. So the 2 mathlib failures were cases where this illegal assignment didn't happend; and thus we were left with a metavariable that Lean didn't know how to fill in.

Kyle Miller said:

• For core to be interested, I think it needs to be extremely well justified

Of course that makes a lot of sense, and I hope that I can justify it well enough.

[Jovan Gerbscheid]

As you say, I think the most sensible order to fix these things is to

• fix the binderinfos (to what they were before lean#5376) and improve the synthOrder algorithm
• then fix the synthPendingImp bug
• and then the improvement that I'm proposing here.

[Jovan Gerbscheid]

I'd be happy to have a go at the first point some time.

[Jovan Gerbscheid]

Here's the #mwe where isDefEq does something that MVarId.assign doesn't do:

import Mathlib

variable {α : Type} [LinearOrder α] [SuccOrder α] [PredOrder α] [IsSuccArchimedean α]
set_option trace.Meta.synthInstance true in
set_option trace.Meta.isDefEq true in
#check IsPredArchimedean.exists_pred_iterate_of_le (α := α)

The trace starts with:

[Meta.synthInstance] ✅️ IsPredArchimedean α ▼
  [] new goal IsPredArchimedean α ▶
  [] ✅️ apply @LinearLocallyFiniteOrder.instIsPredArchimedeanOfLocallyFiniteOrder to IsPredArchimedean α ▼
    [tryResolve] ✅️ IsPredArchimedean α ≟ IsPredArchimedean α ▼
      [isDefEq] ✅️ IsPredArchimedean α =?= IsPredArchimedean ?m.1260 ▶
      [isDefEq] ✅️ ?m.1256 =?= LinearLocallyFiniteOrder.instIsPredArchimedeanOfLocallyFiniteOrder ▼
        [] ?m.1256 [assignable] =?= LinearLocallyFiniteOrder.instIsPredArchimedeanOfLocallyFiniteOrder [nonassignable]
        [] ✅️ IsPredArchimedean α =?= IsPredArchimedean α ▼
          [] ✅️ α =?= α
          [] ✅️ instDistribLatticeOfLinearOrder.toSemilatticeInf.toPreorder =?= instDistribLatticeOfLinearOrder.toSemilatticeInf.toPreorder
          [synthInstance] ✅️ PredOrder α ▶
          [] ✅️ inst✝¹ =?= inst✝¹

The last isDefEq in the trace is the one that I removed in my PR. It reaches the subgoal IsPredArchimedean α =?= IsPredArchimedean α, which is actually @IsPredArchimedean α _ ?m.1251 =?= @IsPredArchimedean α _ ?m.1251. And here the metavariable ?m.1251 gets illegally assigned.

[Sébastien Gouëzel]

@Kyle Miller , @Jovan Gerbscheid Do you think that the bug in #mathlib4 > Bug in instance synthesis? @ 💬 could be related to the one described in this thread? (it probably features prominently synthPending and various reducibility settings)

[Sébastien Gouëzel]

(I can't test myself if the issue disappears with the branch of #26163, as the Lean binaries are not available)