Incorrect coercion

Stream: general

[Oliver Nash]

I briefly confused myself this morning after I made a typo in a lemma about coercions that Lean did not flag. Here's an example:

import algebra.group.hom

variables (M N : Type*) [monoid M] [monoid N] (f : M →* N)

lemma right : ((f : mul_hom M N) : M → N) = ⇑f := rfl

lemma wrong₁ : ((f : mul_hom M N) : M → M) = ⇑f := rfl
lemma wrong₂ : ((f : mul_hom M N) : N → N) = ⇑f := rfl
lemma wrong₃ : ((f : mul_hom M N) : N → M) = ⇑f := rfl
-- etc.

-- The resulting Props have the same type since this type checks
example : right = wrong₁ := rfl
example : right = wrong₂ := rfl
example : right = wrong₃ := rfl

-- Or even these (which Lean allows but at least the linter catches for unused arguments):
lemma wrong₄ (P Q : Type*) : ((f : mul_hom M N) : Q → P) = ⇑f := rfl
lemma wrong₅ : ((monoid_hom.id M : M →* M) : M → N) = id := rfl

Lean does not complain about any of the above, which surprises me. Is this a known issue?