can't synthesize module instance

Stream: Is there code for X?

[Edison Xie]

Why would the first work and the second doesn't? Should we change the instance so that it's about actual Modules and not ModuleCat since it has nothing to do with category theory?

import Mathlib

variable (R₀ R M : Type*) [CommSemiring R₀] [Ring R] [Algebra R₀ R]
  [AddCommGroup M] [Module R M] (M' : ModuleCat R)

open ModuleCat.Algebra
#synth Module R₀ M' -- works
#synth Module R₀ M -- don't work

[Edison Xie]

but changing the instance to module gives:

cannot find synthesization order for instance instModule with type
(R₀ : Type u_1) →
(R : Type u_2) →
(M : Type u_3) →
[inst : CommSemiring R₀] →
[inst_1 : Ring R] → [Algebra R₀ R] → [inst_3 : AddCommGroup M] → [Module R M] → Module R₀ M
all remaining arguments have metavariables:
Ring ?R
@Algebra R₀ ?R inst✝⁴ Ring.toSemiring
@Module ?R M Ring.toSemiring inst✝¹.toAddCommMonoid

Is there just no good ways to do this? Should I always do letI := ...?

[Notification Bot]

This topic was moved here from #Is there code for X? > can't synthesize instance by Edison Xie.

[Aaron Liu]

To solve this typeclass problem Lean would have to guess and fill in R, but since R doesn't appear in the typeclass goal or any outParam or semiOutParam of any of the typeclass arguments, then Lean has no way of doing that

[Aaron Liu]

If R₀ is acting on M in the statement of a lemma or in the body of a definition, then you should additionally assume [Module R₀ M] [IsScalarTower R₀ R M], but if it's in the body of a proof then proof irrelevance means we don't care about it so you can just letI := ....

[Aaron Liu]

It works with M' instead of M because M' appears in the goal and R appears in the type of M', so Lean doesn't have to guess what R could be since it (transitively) appears in the goal

[Edison Xie]

thanks aaron :-)