lean4#2905 non-direct class parents shouldn't be instances

Stream: mathlib4

[Kyle Miller]

It would be helpful if someone who's good at understanding typeclass synthesis issues could take a look at the lean-pr-testing-5920 branch and figure out whether my adaptations for lean4#5920 are reflecting a deep issue, or whether we're sure we can adapt and we should move forward. Here are all the changes: https://github.com/leanprover-community/mathlib4/commit/bf65d209ffe1a810aa8b391c5061c8f9edcf99e3. In particular, in ‎Mathlib/RingTheory/TensorProduct/MvPolynomial.lean the CoeFun instance simply stopped working and I wrote .toFun manually.

A reminder about what lean4#5920 does: it adjusts the rule for which instances get created from the extends list. Now it's simply that only these parents' projections become instances. Formerly, every subobject projection to a class would become an instance as well.

It's worth noting that in Mathlib/Data/NNReal/Defs.lean some instances are now noncomputable because it typeclass synthesis finds these big nested projections rather than a smaller term. (I'm wondering whether instance synthesis should collapse parent projections automatically. That would be an optimization to consider later.)

[Notification Bot]

2 messages were moved here from #mathlib4 > Ways to speed up Mathlib by Kyle Miller.

[Eric Wieser]

Kyle Miller said:

It's worth noting that in Mathlib/Data/NNReal/Defs.lean some instances are now noncomputable because it typeclass synthesis finds these big nested projections rather than a smaller term.

We lazily added shortcut instances in the past to avoid this issue; so inevitably a refactor of parent instances will leave our sparse shortcuts in the wrong places. This should be easy enough to fix in mathlib the same way we have in the past.

[Eric Wieser]

toFun is probably not the fix we want, but it's pretty common for some random unification problem to be solved by coincidence under one set of instances, but need extra explicit type arguments under another. Does adding the types to rtensor also work?

[Kyle Miller]

Yeah, toFun is not the right fix, just something to get mathlib to build. I'd really appreciate if you or someone could experiment with it if you have any time. I won't get back to this for another day or two.

[Anne Baanen]

I have some time this morning to check out your adaptations, will report back in a bit :)

[Yuyang Zhao]

I've fixed it, Lean was having problems unifying Zero (_ ⊗[_] _) and Zero (addConGen (TensorProduct.Eqv _ _ _)).Quotient.

[Eric Wieser]

Maybe we should apply your fix directly to master?

[Anne Baanen]

After @Yuyang Zhao's fixes, the only issue is that we actually have a diamond (on the master branch!) between docs#NNRat.instSemifield and docs#instNNRatLinearOrderedSemifield, where the former defines zsmul using docs#zsmulRec and the latter with docs#Nonneg.zsmul. I made #18860 to fix that diamond.

[Matthew Ballard]

In general docs#TensorProduct being a def seems like you are inviting trouble

[Kyle Miller]

Thanks everyone! It sounds like lean4#5920 doesn't have any fundamental problems and we should be able to adapt. There's a slight negative performance impact to it(*), but I take it that we should be able to add shortcut instances as necessary.

Some problems do take more heartbeats now — I bumped up the default value of synthInstance.maxHeartbeats to compensate, at least to get mathlib to build. The failure was during the simpNF linter, where there was a timeout when trying to simplify the LHSs of docs#Ideal.sup_mul_right_self, docs#Ideal.sup_mul_left_self, docs#Ideal.mul_right_self_sup, and docs#Ideal.mul_left_self_sup.

(*) I'm not sure exactly how to interpret the benchmark results for #18830. Some of the differences seem random, and I wonder if it's actually comparing with a comparable run.