chore: fix implicit-reducible diamond in Lie subalgebras

[sgouezel]

The following example fails on master, is fine on the branch:

example (I : LieIdeal R L) : ((LieIdeal.lieRing R L I).toBracket : Bracket ↥I ↥I) =
    (LieIdeal.lieRingModule (↥I) I).toBracket := by
  with_reducible_and_instances rfl

---

[github-actions]

PR summary 4b13551071

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ LieIdeal.bracket
+ instance (priority := 2000) (I : LieIdeal R L) : Bracket I I := inferInstance

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[JovanGerb]

Can you explain why we now need fast_instance%?

[sgouezel]

inferInstanceAs is hiding things behind opaque definitions, but that's not what we want here: the I.toLiesubalgebra is just a trick to get the instances for free, but all the data fields have already been defined, with nice definitional definitions, so it's exactly a job for fast_instance% (although I get inferInstanceAs would also work here; the real fix in the PR is giving the bracket in explicit form)

[sgouezel]

More details: with inferInstanceAs, the Lie bracket in LieIdeal.lieRingModule is LieIdeal.lieRingModule._aux_1 M I, i.e., it's hidden behind an opaque function. That's normal, because there is no earlier bracket instance (this is more general than the above declarations). In the specific situation where M= I, this is not implicit-reducibly defeq to the bracket on I, and boom. With fast_instance%, instead, the bracket is expanded to its definition instead of being hidden, and the definition is fun a a_1 ↦ ⁅↑a, a_1⁆ : ↥I → M → M, which is what we want when M = I.

(For LieIdeal.lieAlgebra, we could use inferInstanceAs or fast_instance%, they do exactly the same thing. But semantically I think it corresponds more to what we expect from fast_instance% as we're not trying to hide anything).

[JovanGerb]

I had a look, and I propose a different solution: mark LieIdeal.toLieSubalgebra with @[implicit_reducible]. This fixes the example you provided.

[sgouezel]

That's a discussion we had on Zulip, and I'm not sure there was a conclusion: should we mark definitions constructing algebraic objects (subrings and so on) as implicit_reducible, just like we do for instances? If we do, this will indeed solve many diamonds, but maybe at the price of a performance hit. So I'm not sure.

[JovanGerb]

In this case I think it is the principled solution.

The reason why inferInstanceAs creates a diamond here is that it notices that the type of the bracket operation doesn't match up, and so it hides the definition behind a def to protect you from creating a leaky instance. This PR uses "brute force" to make a leaky instance anyways. I would rather not have a leaky instance at all.

[JovanGerb]

Ok, I have now found another solution that you may be happier with. Add the following instance:

instance (I : LieIdeal R L) : Bracket I M where
  bracket x y := ⁅(x : L), y⁆

And it will be picked up by the inferInstanceAs, and fix the diamond.

[sgouezel]

I've done that.

[JovanGerb]

If you move the new instance up a bit, then LieIdeal.lieRing can inherit from it too.

Though I don't know if this is desirable.

[sgouezel]

Good idea. I've moved it up (but still declared a shortcut instance as this will be the most common case).

[JovanGerb]

Why do you need a separate shortcut instance? Doesn't it already find the new Bracket instance as the first thing? And if not, then can't you just give it a high priority?

[sgouezel]

It does find the new bracket instance, but for that it needs to do another search for Bracket L L (while all the other instances are already there in the type of I) while with the shortcut instance it doesn't. Since I expect this bracket to show up quite often (much more than the other one), I would register the shortcut instance, just for performance reasons. I can remove it if you prefer.

[JovanGerb]

That's a good reason, thanks. I think the increased priority is not needed though, since more specific patterns are tried first in type class search.