Failing to infer Module instance from Algebra

Stream: mathlib4

[Kyle Miller]

Is it a known error that you can't get a Module instance if A is a Ring rather than a Semiring?

import Mathlib.Algebra.Algebra.Basic

section
variable [Field k] [Ring A] [Algebra k A]
#check (inferInstance : Semiring A) -- OK
#check (inferInstance : Module k A) -- fails
end

section
variable [Field k] [Semiring A] [Algebra k A]
#check (inferInstance : Semiring A) -- OK
#check (inferInstance : Module k A) -- OK
end

[Kyle Miller]

I would expect docs4#Algebra.toModule to apply in both cases.

[Matthew Ballard]

Fixed by etaExperiment

[Matthew Ballard]

So I guess that answer is yes

[Jireh Loreaux]

yes, this was one of the early examples in lean4#2074 (see the second post)

[Alex Kontorovich]

What's the status of this bug? I think @Heather Macbeth and I may have encountered it again just now. See mathlib4#3211. It's a case where we have a field but Lean can't seem to infer that it's a ring.

[Eric Wieser]

What's the error message you get?

[Eric Wieser]

Either way, lean4#2074 is alive and well, and I don't think any imminent fix is incoming

[Eric Wieser]

There's a workaround for mathlib4 that's in the works (!4#3171), but it's not ready yet

[Eric Wieser]

Oh, I assume you mean these lines

[Eric Wieser]

You can use set_option synthInstance.etaExperiment true in ... to test whether the problem is lean4#2074. If it works with that setting and not without, then it's lean4#2074.

[Heather Macbeth]

Yup, I just tried it. That's the issue. (cc @Alex Kontorovich)

[Heather Macbeth]

So is the current advice to turn that option on in declarations which need it?

[Heather Macbeth]

I pushed the change assuming so.