ring_hom.comp

Stream: general

[Kevin Buzzard]

Amelia just pointed out to me that in docs#ring_hom.comp two of the semiring instances are [] and one is {}. This surprised me! Why do we do it like this? There's no mention of this phenomenon in the module doc.

[Anne Baanen]

Something similar also happens in docs#linear_map.comp and docs#linear_map.map_neg. Presumably finding the arguments by unification gives (used to give?) less diamonds than doing it by typeclass search?

[Eric Wieser]

There's now a library note about this, somewhere

[Eric Wieser]

https://leanprover-community.github.io/mathlib_docs/notes.html#implicit%20instance%20arguments

[Eric Wieser]

As for why one is different to the others, it's probably an accident. Keeping track of which variables are currently in your scope is really hard!

[Kevin Buzzard]

Oh -- so when this is happening there should be a library note? Thanks! Yes, I figured out (in the sense of "Amelia explained it to me") how it could work in principle but then I was confused why it was happening in some places but not others.

[Reid Barton]

Non-obvious design decisions like this are what comments are for generally, and library notes are supposed to be a mechanism to deduplicate and cross-link repeating issues

[Kevin Buzzard]

This seems to be a repeating issue though -- we first discovered it in the lifting property liftq for quotient modules, and then in mkq, and then in comp.

[Reid Barton]

right, so it would be good to reference implicit instance arguments where it comes up, and then add specific comments about why it pertains to some but not all of the classes involved

[Reid Barton]

Here it's not really clear whether it's intentional, though it seems likely...

[Eric Wieser]

Maybe I'll try and tweak docgen to add backreferences from the notes section...

[Eric Wieser]

But the note _is_ there already: https://leanprover-community.github.io/mathlib_docs/algebra/ring/basic.html#ring_hom.to_monoid_with_zero_hom

[Eric Wieser]

It's just not repeated for every single definition in the file

[Chris Hughes]

@Anne Baanen its not about diamonds, it's just faster to find it by unification than type class inference.