RingTheory.Ideal.Prod !4#2877

Stream: mathlib4

[Jakob von Raumer]

I've got some weird trouble here with for a ring R the instances (@Semiring.toNonAssocSemiring.{u} R (@Ring.toSemiring.{u} R _)) and (@NonAssocRing.toNonAssocSemiring.{u} R (@Ring.toNonAssocRing.{u} R _)) being equal by rfl but it makes a difference for type inference which one is used :frown:

[Jakob von Raumer]

Okay it works using set_option synthInstance.etaExperiment true

[Jireh Loreaux]

You can generally get around this by disabling some of those instances, like Ring.toNonAssocRing.

[Jakob von Raumer]

@Gabriel Ebner What's the status of etaExperiment? Is it expected to be turned on by default at some point?

[Patrick Massot]

I think the status is still that we should be patient. Gabriel knows we are waiting for this, he is working, and I'm fairly sure he'll tell us when there will be news about it.