[Merged by Bors] - fix: change instance priorities in algebra hierarchy

[kbuzzard]

WIP: experiments with changing instance priorities. See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/std4.20.2F.20Lean4.20bump/near/374996945 .

---

[kbuzzard]

!bench

[eric-wieser]

I'm glad to see I'm not the only one who consistently mispells "hierarchy"...

[leanprover-bot]

Here are the benchmark results for commit 4c08f67.
There were significant changes against commit f1fbf07:

  Benchmark                                         Metric         Change
  =======================================================================
+ build                                             maxrss         -28.8%
- ~Mathlib.Algebra.DirectSum.Module                 instructions     6.5%
+ ~Mathlib.Algebra.Lie.DirectSum                    instructions    -5.2%
+ ~Mathlib.Analysis.Analytic.Linear                 instructions   -19.5%
+ ~Mathlib.Analysis.InnerProductSpace.Adjoint       instructions   -31.2%
+ ~Mathlib.Analysis.NormedSpace.Multilinear         instructions    -7.1%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm        instructions    -6.1%
+ ~Mathlib.CategoryTheory.Sites.Sheaf               instructions    -5.9%
- ~Mathlib.Data.Polynomial.Monomial                 instructions     5.4%
+ ~Mathlib.FieldTheory.IsAlgClosed.Basic            instructions   -10.5%
- ~Mathlib.LinearAlgebra.DirectSum.Finsupp          instructions    25.3%
- ~Mathlib.LinearAlgebra.DirectSum.TensorProduct    instructions     8.4%
+ ~Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots   instructions    -8.1%
+ ~Mathlib.RingTheory.Adjoin.Field                  instructions   -30.9%
+ ~Mathlib.RingTheory.AlgebraicIndependent          instructions   -18.3%
+ ~Mathlib.RingTheory.Norm                          instructions   -10.6%
+ ~Mathlib.Topology.Instances.Complex               instructions    -6.6%

[sgouezel]

Can this be done automatically? I mean, when declaring a new class, put priority 200 on classes it extends with a toA, priority 100 otherwise (and maybe priority 1000 if it is a specific instance that doesn't always apply, like we did in mathlib3)?

[Kha]

I think it's worth opening a lean4 issue about this

[eric-wieser]

What's supposed to happen here?

structure AB extends A
structure AC extends A
structure ABC extends AB, AC
structure ACB extends AC. AB

Do we need a weight-style system like Coq, where the priority is the sum of all the paths, instead of a global priority on each step?

[fpvandoorn]

I opened leanprover/lean4#2325

@eric-wieser: just warn the user that they do something stupid, and ask them to reorder the extended structures. The sum of priorities is not good: you want to make sure that all the highest priority paths only use the "correct" projections.

[eric-wieser]

I worry that this effectively forces us to choose a global partial order over all typeclasses that exist; potentially something as silly as "the extends clause must be in alphabetical order"...

[kbuzzard]

LeftCancelMonoid, RightCancelMonoid and CommMonoid all extend Monoid, and if we declare commutativity to be our favourite path (it's surely the most common path) then CancelMonoid, which extends LeftCancelMonoid and RightCancelMonoid, is left with no "correct" projection.

[fpvandoorn]

I think we can merge this without my comment, since it already saves a lot of memory usage. We can fix more instance priorities systematically in later PRs.

[fpvandoorn]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style