[Merged by Bors] - fix(ring_theory/localization): remove coe_submodule instance #3832
Conversation
| variables {f} | ||
| /-- Map from ideals of `R` to submodules of `S` induced by `f`. | ||
| (This was previously a `has_coe` instance, but if `f.codomain = R` then this will loop.) -/ | ||
| def coe_submodule (I : ideal R) : submodule R f.codomain := submodule.map f.lin_coe I |
There was a problem hiding this comment.
This is also dangerous as a has_coe_t instance? How does this relate to the note [use has_coe_t]?
What do you exactly mean with this?
if
f.codomain = Rthen this will loop
There was a problem hiding this comment.
If f.codomain = R then both sides are defeq, i.e. it is an identity coercion. has_coe_t would help somewhat here, but that's not the only problem with this instance; f is not determined by the lhs so instance search goes down a rabbit hole.
There was a problem hiding this comment.
localization_map.codomain is not reducible, so I thought that for the purposes of type-class inference f.codomain and R are never considered definitionally equal?
If it were a has_coe_t instance, I'm sure if the fact that f is not determined by the lhs is important...?
There was a problem hiding this comment.
Changing it to a has_coe_t instance is enough to avoid the loop that exposed this, yes.
There was a problem hiding this comment.
I'm happy to keep it a def though, I'm not sure whether this is a good coercion. Maybe a note saying that it doesn't loop as a has_coe_t is nice?
Vierkantor
added
the
awaiting-author
robertylewis
removed
the
awaiting-author
|
bors merge |
github-actions
bot
added
the
ready-to-merge
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
This coe can loop. See zulip discussion at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Unknown.20error.20while.20type-checking.20with.20.60use.60/near/207089095