with in class instances can cause surprising slowdowns #2387
Description
Prerequisites
- Put an X between the brackets on this line if you have done all of the following:
- Checked that your issue isn't already filed.
- Reduced the issue to a self-contained, reproducible test case.
Description
The following different ways to make instances of a class result in different terms:
class A where
foo : String
bar : String
class B extends A where
extra : String
instance f : A := ⟨"hi", "there"⟩
instance one : B :=
{ f with
foo := f.foo
extra := "bro" }
instance two : B :=
{ toA := f
extra := "bro" }
instance three : B :=
{ f with
extra := "bro" }
instance four : B where
extra := "bro"
set_option pp.all true in
#print one
-- def one : B :=
-- let src : A := f;
-- @B.mk (A.mk (@A.foo f) (@A.bar src)) "bro"
set_option pp.all true in
#print two
-- def two : B :=
-- @B.mk f "bro"
set_option pp.all true in
#print three
-- def three : B :=
-- let src : A := f;
-- @B.mk (A.mk (@A.foo src) (@A.bar src)) "bro"
set_option pp.all true in
#print four
-- def four : B :=
-- @B.mk f "bro"
In Mathlib's algebra hierarchy, these let src terms (the terms produced by with) seem to greatly increase the amount of time taken by typeclass inference to prove that various terms are defeq. Here are two case studies from mathlib.
-
In mathlib PR [Merged by Bors] - perf: change to CommGroup instance on units leanprover-community/mathlib4#6398 I remove one
withfrom a definition and according to the speedcenter, another file now compiles 42% faster. In the Zulip post by Xavier Roblot which prompted the PR, the change makes the first example compile an order of magnitude faster. This is just one change to onewith. -
In Mathlib PR perf (MonoidAlgebra.Basic): reduce withs in structure terms leanprover-community/mathlib4#6319 , Matt Ballard removes all the
withs in just one file in mathlib, and the benchmark results are extraordinary: http://speedcenter.informatik.kit.edu/mathlib4/compare/c7852218-4442-4a5f-8923-2062c59fbe45/to/ad01e2d7-e057-449b-b3f2-2769bf28d4e0 . A sea of green.
If something could be changed in core which would save us the bother of removing many many occurrences of with in mathlib, that would be helpful.
Versions
Lean (version 4.0.0-nightly-2023-08-03, commit 125a0ba, Release)
Additional Information
Here is a comparison of the instance traces with trace.profiler true and pp.proofs.withType false in Xavier Roblot's Zulip example (case study 1 above). The diff in mathlib is this:
- { (inferInstance : Group αˣ) with
- mul_comm := fun _ _ => ext <| mul_comm _ _ }
+ { mul_comm := fun _ _ => ext <| mul_comm _ _ }Before the change things looked like this:
[Meta.isDefEq.assign] [0.392895s] ✅ ?m.2672 := torsion K
[Meta.isDefEq.assign.checkTypes] [0.392861s] ✅ (?m.2672 : Subgroup
{ x // x ∈ 𝓞 K }ˣ) := (torsion K : Subgroup { x // x ∈ 𝓞 K }ˣ)
[Meta.isDefEq] [0.392851s] ✅ Subgroup { x // x ∈ 𝓞 K }ˣ =?= Subgroup { x // x ∈ 𝓞 K }ˣ
[Meta.synthInstance] [0.041633s] ✅ CommGroup { x // x ∈ 𝓞 K }ˣ
[Meta.synthInstance] [0.032970s] ✅ apply @Units.instCommGroupUnitsToMonoid to CommGroup
{ x // x ∈ 𝓞 K }ˣ
[Meta.synthInstance.tryResolve] [0.032916s] ✅ CommGroup
{ x // x ∈ 𝓞 K }ˣ ≟ CommGroup { x // x ∈ 𝓞 K }ˣ
[Meta.isDefEq] [0.025502s] ✅ CommGroup { x // x ∈ 𝓞 K }ˣ =?= CommGroup ?m.2681ˣ
[Meta.isDefEq] [0.025467s] ✅ { x // x ∈ 𝓞 K }ˣ =?= ?m.2681ˣ
[Meta.synthInstance] [0.016779s] ✅ CommMonoid { x // x ∈ 𝓞 K }
[Meta.isDefEq] [0.351141s] ✅ CommGroup.toGroup =?= Units.instGroupUnits
[Meta.isDefEq] [0.351049s] ✅ CommGroup.toGroup =?= let src := inferInstance;
Group.mk _
[Meta.isDefEq] [0.351043s] ✅ CommGroup.toGroup =?= Group.mk _
[Meta.isDefEq] [0.350975s] ✅ Units.instCommGroupUnitsToMonoid.1 =?= Group.mk _
[Meta.isDefEq] [0.350947s] ✅ Group.mk _ =?= Group.mk _
[Meta.isDefEq] [0.343292s] ✅ Group.toDivInvMonoid =?= DivInvMonoid.mk zpowRec
[Meta.isDefEq] [0.343225s] ✅ inferInstance.1 =?= DivInvMonoid.mk zpowRec
[Meta.isDefEq] [0.343197s] ✅ DivInvMonoid.mk zpowRec =?= DivInvMonoid.mk zpowRec
[Meta.isDefEq] [0.075866s] ✅ zpowRec =?= zpowRec
[Meta.isDefEq] [0.075857s] ✅ zpowRec =?= zpowRec
...
[Meta.isDefEq] [0.106764s] ✅ Monoid.mk _ _ npowRec =?= Monoid.mk _ _ npowRec
[Meta.isDefEq] [0.053281s] ✅ npowRec =?= npowRec
...
[Meta.isDefEq] [0.037335s] ✅ Semigroup.mk _ =?= Semigroup.mk _
...
[Meta.isDefEq] [0.016048s] ✅ { one := 1 } =?= { one := 1 }
[Meta.isDefEq] [0.022721s] ✅ { inv := Inv.inv } =?= { inv := Inv.inv }
[Meta.isDefEq] [0.015109s] ✅ Inv.inv =?= Inv.inv
...
[Meta.isDefEq] [0.137621s] ✅ {
div := DivInvMonoid.div' } =?= { div := DivInvMonoid.div' }
[Meta.isDefEq] [0.137499s] ✅ DivInvMonoid.div' =?= DivInvMonoid.div'
...
with ... meaning that I removed a bunch of other lines all of which were of the form X =?= X where X and X look syntactically equal.
Lean wants to assign ?m.2672 := torsion K (torsion K is a group) and then has to check that two group structures coincide. Units.instCommGroupUnitsToMonoid is the instance which has been dewithed. Before the change, Lean goes into interminable checks that various "obviously defeq" fields from Group are defeq, each costing up to 0.1 seconds. After the change the same trace (in full) looks like this:
[Meta.isDefEq.assign] [0.051093s] ✅ ?m.1366 := torsion K
[Meta.isDefEq.assign.checkTypes] [0.051055s] ✅ (?m.1366 : Subgroup
{ x // x ∈ 𝓞 K }ˣ) := (torsion K : Subgroup { x // x ∈ 𝓞 K }ˣ)
[Meta.isDefEq] [0.051042s] ✅ Subgroup { x // x ∈ 𝓞 K }ˣ =?= Subgroup { x // x ∈ 𝓞 K }ˣ
[Meta.synthInstance] [0.043180s] ✅ CommGroup { x // x ∈ 𝓞 K }ˣ
[Meta.synthInstance] [0.034260s] ✅ apply @Units.instCommGroupUnitsToMonoid to CommGroup
{ x // x ∈ 𝓞 K }ˣ
[Meta.synthInstance.tryResolve] [0.034205s] ✅ CommGroup
{ x // x ∈ 𝓞 K }ˣ ≟ CommGroup { x // x ∈ 𝓞 K }ˣ
[Meta.isDefEq] [0.026653s] ✅ CommGroup { x // x ∈ 𝓞 K }ˣ =?= CommGroup ?m.1375ˣ
[Meta.isDefEq] [0.026616s] ✅ { x // x ∈ 𝓞 K }ˣ =?= ?m.1375ˣ
[Meta.synthInstance] [0.017559s] ✅ CommMonoid { x // x ∈ 𝓞 K }
(end)
and in particular the process has gone down from 0.4 seconds to 0.05 seconds, and the second part of the story in the original trace, beginning
[Meta.isDefEq] [0.351141s] ✅ CommGroup.toGroup =?= Units.instGroupUnits
[Meta.isDefEq] [0.351049s] ✅ CommGroup.toGroup =?= let src := inferInstance;
Group.mk _
...
has completely vanished.
Before the change, typeclass inference is taking 0.35 seconds to prove Units.instCommGroupUnitsToMonoid.1 =?= Group.mk _ , and this calculation is occurring around 20 times during elaboration of the term, which explains why it was taking 7 seconds to elaborate.