typeclass inferences

Stream: general

[Kenny Lau]

https://github.com/kckennylau/Lean/blob/master/enough_injectives.lean#L72
In L72 of this, I needed to type @linear_map R M (Hom_R_Q_div_Z R) _ _ (Hom_R_Q_div_Z.module R), i.e. I needed to manually provide the proof term Hom_R_Q_div_Z.module R that Hom_R_Q_div_Z R is a module, despite it being attributed as instance. Why is this the case?

[Scott Morrison]

When faced with this problem, I often try to write an example beforehand, which hopefully should summon the instance via by apply_instance, and see if I can get that working.

[Scott Morrison]

If I can't I start worrying about universe levels, which in my experience is a very common cause of typeclass inference failing.

[Scott Morrison]

(I haven't actually looked at your example.)

[Scott Morrison]

Having quickly looked at your example, I'd suggest trying to restrict to the case where the ring and the module live in the same universe.

[Kenny Lau]

hmm, would that break generality?

[Kenny Lau]

linear_map accepts three universes

[Scott Morrison]

Yeah... but that's maybe dangerous as well.

[Kenny Lau]

so other universes don't have enough injectives lol

[Scott Morrison]

at least check if this solves the inference problem

[Scott Morrison]

If it doesn't then it's irrelevant. If it does, it's probably time to consult Mario for advice.

[Scott Morrison]

(One can always ulift when you don't have enough universe polymorphism, and sometimes this is the better option.)

[Kenny Lau]

it doesn't

[Scott Morrison]

Oh well!

[Scott Morrison]

try replacing the points where you explicitly provide the instances with by apply_instance, and then set pp.all

[Kenny Lau]

wait what

[Kenny Lau]

@Scott Morrison once I removed L67-69, everything worked

[Kenny Lau]

except the fact that i of course need those lines

[Kenny Lau]

@Mario Carneiro any idea? In here, I need Hom_R_Q_div_Z.module R to tell Lean that Hom_R_Q_div_Z R is a module, but once I remove L67-69, it is no longer necessary

[Kenny Lau]

I suspect it is because of the injective.to_module

[Kenny Lau]

interfering with the typeclass resolutions