priority hacks

Stream: mathlib4

[Kevin Buzzard]

I've been fiddling with priorities. There are two PRs I'd like to flag here.

The first is #34077. Core lean has docs#instSMulOfMul which is

instance (priority := 910) {α : Type u} [Mul α] : SMul α α where
  smul x y := Mul.mul x y

In particular, core has explicitly lowered the priority of this instance (recall that the default priority is 1000, so this is less than the default). On the other hand, in mathlib we have docs#Algebra.id which is Algebra.id [CommSemiring R] : Algebra R R (which includes instSMulOfMul as a component) and we give it a priority of 1100, i.e. we are saying "actually we think the priority of this instance should be higher than default". The priority of Algebra.id was increased in #13032 , saving over 100G instructions, and the Zulip discussion is here #mathlib4 > erw and IsDedekindDomain.HeightOneSpectrum.adicCompletion @ 💬 . The tl;dr is, I think, that Algebra.id [CommSemiring R] : Algebra R R is likely to be (a) correct when it applies and (b) quick to fail when it doesn't, and there is an example in the linked thread about how not applying it until too late can be costly.

In #34077 I want to argue analogously: instance [Mul α] : SMul α α is likely to be correct when it applies and quick to fail, so why not raise the priority to 1100 despite the fact that core wants it at 910 (for reasons which I don't know)? This instance priority change produces this diff https://github.com/leanprover-community/mathlib4/pull/34077#issuecomment-3916045908 and a saving of 290G instructions but slows down a Kaehler differentials file because of the defeq universe issue https://github.com/leanprover/lean4/issues/12102 here ; one declaration in that file is already really horrible because max u v isn't syntactically max v u and this mul-to-smul change for some reason makes it even more horrible. The universe hack #34088 fixes the Kaehler differentials file with a universe renaming hack and with that hack the prio increase of instSMulToMul saves 463G as can be seen here https://github.com/leanprover-community/mathlib4/pull/34077#issuecomment-3856115722 .

Right now the trail has kind of gone cold on this one; I wanted to bring up the discussion of #34077 earlier but was derailed by the universe issue, which I note is currently marked P-high by the FRO, so I've been adopting a wait and see approach. But notwithstanding the universe issue I think it's still meaningful to ask whether we want #34088.

---

The second hack is #35446 , which is a hack in the opposite direction. This was inspired by Artie's example of #synth Mul (R[X] ⧸ (⊥ : Ideal R[X])) timing out, which was traced back in this thread #mathlib4 > Typeclass Synthesis Regression @ 💬 to be a case of GradedMonoid.GradeZero.mul being applied in a situation where it was mathematically irrelevant and taking a long time to fail. Mathlib has both internally and externally graded objects, and the problem with externally-graded objects is that they eat (A : ι → Type*) which are the graded pieces A i, and Lean can sometimes try to use results of the form "If A is an externally-graded monoid then A 0 inherits a multiplication" to try and find a multiplication on an object which is coincidentally of the form A 0 for some A, for example R[X] ⧸ (⊥). This bad choice can take a long time to fail. In #35446 we lower the priority of all of the instances on A 0 in situations where A : ι → Type* is part of an externally graded object. For me the argument is the converse of instSMulToMul: here the instances might apply accidentally and can be very slow to fail. Benchmarking is here https://github.com/leanprover-community/mathlib4/pull/35446#issuecomment-3916019036 and shows a decrease of 151G instructions.

I am really unclear about whether "messing around with priorities in such a way to make mathlib faster" is actually something we should be doing (and how to document it if we do it), or whether they are hacks which are actually racking up technical debt. Both the PRs being discussed here have come from genuine user issues whether things were slow and the changes solve their problems and seem not to create other problems. I guess what I am asking is: is fiddling with instance priorities something which we should definitely not be doing because we should be looking for better solutions, or something which we should be taking on board because it is solving problems? I should be clear: I am not actively arguing "we should merge my PRs", I am saying "look what these changes (which seem to me to be reasonably motivated) can do; but should we be doing this at all?"

[Anne Baanen]

I don't have a coherent answer, so here are some disjointed thoughts on the subject.

As far as performance hacks go, instance priorities are quite innocent ones: morally, the order in which instances are tried should not give observable results except the speed at which the right instance is found. So I have few objections to a few well-reasoned-out priority bumps/nerfs spread out across Mathlib. (Especially if they have a clear test case, like #synth Mul (R[X] ⧸ (⊥ : Ideal R[X])).)

Taking this to the extreme to get ten thousand PRs that each twiddle the priority of an individual instance would be a waste of time though. So we should prefer to find patterns that are useful globally. We already have rules like "instances that always apply get lower priority", or "CancellativeWhatever to Whatever gets lower priority", and so "GradedWhatever to Whatever gets lower priority" would fit neatly in that rule too.

One thing we can do for future-proofing and documenting is, instead of writing instance (priority := low), we'd have a bunch of our own keywords so we can write instead instance (priority := gradedToUngraded). So if we later realize that graded stuff needs higher priority, we can change it all at once. We probably have so many annotations that it'd be a huge hassle to group them all though (I certainly wouldn't volunteer to do the whole job myself).

Finally a warning: I have heard that the FRO is planning to do some redesign of what the typeclass system can do (beyond the upcoming v4.29.0 changes), although I don't know any details. So this might render a lot of the priority twiddling obsolete.

[Yuyang Zhao]

I previously experimented with some adjustments in #7873. I wanted to revisit this after decoupling the algebra and the normed hierarchy, but it's currently blocked by lean4#8279.