how does changing imports affect tc synthesis

Stream: mathlib4

[Matthew Ballard]

There are some obvious things: removing a necessary instance will cause failure. But should I expect that importing additional files causes instance synthesis to change from successful to unsuccessful? Here is an example to play with

import Mathlib.Data.MvPolynomial.Equiv
import Mathlib.Data.MvPolynomial.CommRing
import Mathlib

variable {R : Type} {σ : Type} [CommRing R]

set_option maxHeartbeats 0 in
set_option trace.Meta.synthInstance true in
#synth Module (MvPolynomial σ R) (MvPolynomial σ R)

If you try different subsets of the import list, you can see the different behavior. I don't understand the behavior. Any explanation would be appreciated.

[Eric Wieser]

Can you explain what the combinations with unexpected observations are?

[Eric Wieser]

The instance this is finding is docs4#instModuleToSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRing

[Eric Wieser]

Which is a workaround instance for lean4#2074 breaking docs4#Semiring.toModule

[Eric Wieser]

We should either remove that workaround, or move it to Algebra.Module.Basic

[Eric Wieser]

Because right now one solution to Module R R not working (as in your example) is import Mathlib.Topology.Algebra.UniformMulAction and that's ridiculous

[Matthew Ballard]

Reordered. No imports fails of course. First, succeeds with Semiring.toModule. Include the second, it fails no matter the heartbeat limit. Include all of Mathlib at it gets the one you said.

[Matthew Ballard]

So something in the second is triggering a diamond?

[Eric Wieser]

attribute [-instance] MvPolynomial.instCommRingMvPolynomialToCommSemiring in causes a difference

[Eric Wieser]

import Mathlib.Data.MvPolynomial.Equiv
import Mathlib.Data.MvPolynomial.CommRing

variable {R : Type} {σ : Type} [CommRing R]

set_option maxHeartbeats 0 in
set_option trace.Meta.synthInstance true in
-- comment the next line (equivalent to removing the `CommRing` import) to make this fail
attribute [-instance] MvPolynomial.instCommRingMvPolynomialToCommSemiring in
#synth Module (MvPolynomial σ R) (MvPolynomial σ R)

[Eric Wieser]

This succeeds, so it's not a non-defeq diamond:

example :
    (MvPolynomial.instCommRingMvPolynomialToCommSemiring : CommRing (MvPolynomial σ R)).toCommSemiring =
      MvPolynomial.commSemiring :=
  by rfl

[Eric Wieser]

Did you mean set_option synthInstance.maxHeartbeats 0 in instead of set_option maxHeartbeats 0 in? It seems to succeed with the former

[Matthew Ballard]

Eric Wieser said:

This succeeds, so it's not a non-defeq diamond:

example :
    (MvPolynomial.instCommRingMvPolynomialToCommSemiring : CommRing (MvPolynomial σ R)).toCommSemiring =
      MvPolynomial.commSemiring :=
  by rfl

Thanks @Eric Wieser ! Should I be guessing that this rfl is not succeeding in tc synthesis with CommRing import?

What about import Mathlib fixes the problem?

[Eric Wieser]

The CommRing import is what defines MvPolynomial.instCommRingMvPolynomialToCommSemiring so it doesn't make sense to ask if it works without the import

[Eric Wieser]

I think this is just a performance thing, all versions succeed with synthInstance.maxHeartbeats as 0

[Matthew Ballard]

Ah right. Performance I agree with. But I guess I don't understand the underlying algorithm well enough to understand how performance changes with the different instances in the context

[Eric Wieser]

Having MvPolynomial.instCommRingMvPolynomialToCommSemiring available seems to send it on a wild goose chase

[Eric Wieser]

While having instModuleToSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRing available gives it a shortcut back to sanity again

[Matthew Ballard]

I did not see that in the trace. Did you find it?

[Eric Wieser]

Did you see my message above where I showed attribute [-instance] MvPolynomial.instCommRingMvPolynomialToCommSemiring fixes the problem?

[Matthew Ballard]

Eric Wieser said:

Because right now one solution to Module R R not working (as in your example) is import Mathlib.Topology.Algebra.UniformMulAction and that's ridiculous

Can this fix other problems in my life?! :wink:

[Matthew Ballard]

Eric Wieser said:

Did you see my message above where I showed attribute [-instance] MvPolynomial.instCommRingMvPolynomialToCommSemiring fixes the problem?

Yes. I did but I would hope the trace had more information about what is going on under the hood

[Eric Wieser]

I'm not very familiar with those traces, perhaps @Gabriel Ebner could take a look

[Matthew Ballard]

Is there a shorter way to dump the traces to a file than building it on the command line? For example, is there anything I can specify in my editor?

[Gabriel Ebner]

Just saw this:

-- Porting note: Needed to add the following line
private instance : Module R S := Algebra.toModule

[Gabriel Ebner]

Is there a shorter way to dump the traces to a file than building it on the command line? For example, is there anything I can specify in my editor?

Filed as https://github.com/leanprover/vscode-lean4/issues/293

[Reid Barton]

private instance? I wonder what the odds are that this does what it was intended to do

[Matthew Ballard]

Gabriel Ebner said:

Just saw this:

-- Porting note: Needed to add the following line
private instance : Module R S := Algebra.toModule

etaExperiment removes this. Testing now

[Matthew Ballard]

At least for !4#3067 this change moved dsimp took 408s

[Matthew Ballard]

from #mathlib4 > dsimp took 83.3s