Re-order typeclass hypotheses for performance

Stream: mathlib4

[Michael Rothgang]

#21449 speeds up TC synthesis by re-ordering two hypotheses to a lemma --- apparently, this makes failing searches much faster. (Trying to synthesise IsPrime p before IsArtinian R for an ideal p in a ring R is more useful.) I wonder if this can be done or investigated more systematically: do others see a way to do so?

[Damiano Testa]

There are several similar tricks that have been used and are not really documented. Someone, maybe Matthew Ballard, suggested keeping track of it and we might as well start here!

[Damiano Testa]

#21323 also has several tricks for speed ups.

[Kevin Buzzard]

So is this speedup because it just happens to be the case that IsPrime typically fails faster than IsArtinian in today's mathlib?

[Jovan Gerbscheid]

Yes. The only example where this makes a difference actually tries to synthesize IsPrime. The only instance it finds for IsPrime is IsMaximal. Then for IsMaximal it only finds the instance with IsPrime and IsArtinian. If it tries IsPrime, it finds a loop and stops.

[Jovan Gerbscheid]

We don't want a search for IsPrime _ to cause a search for IsArtinian. Especially since when it does find IsArtinian, it gets into a loop immediately anyways.

[Kevin Buzzard]

I see! So this is very specific to the setup we have with these instances and the relationships between them. We could add IsDomain R -> Subsingleton P -> IsPrime P one day and mess up your argument :-)

[Jovan Gerbscheid]

Well, I think IsDomain might be less expensive that IsArtinian? Depending on the context of course.

[Jovan Gerbscheid]

And for that instance one could also think about which order is faster: first synthesize IsDomain or Subsingleton?

[Kim Morrison]

Just an aside here: we have the file MathlibTest/TCSynth.lean, and I would strongly encourage adding to it anytime someone achieves a typeclass search speedup, to guard against subsequent regressions.

[Kim Morrison]

Unfortunately this file is not very findable --- any suggestions for encouraging additions to it very welcome.

[Edward van de Meent]

Could we make successful speedup messages from the speedcenter suggest this?

[Damiano Testa]

The bench-summary bot could certainly say something in its report and might probably even be made aware of the results and comment it when appropriate.

I'm not sure what would be a good measure of "TC speedup", though.

[Jovan Gerbscheid]

Kim Morrison said:

we have the file MathlibTest/TCSynth.lean, and I would strongly encourage adding to it anytime someone achieves a typeclass search speedup, to guard against subsequent regressions.

I've added a test for the type class search that was fixed. #21499