CoeOut instance from Submodule R M to ModuleCat R

Stream: mathlib4

[Amelia Livingston]

The CoeOut instance from Submodule R M to ModuleCat R in the last two lines of Mathlib.Algebra.Category.ModuleCat.Basic causes this:

import Mathlib.LinearAlgebra.Basic
import Mathlib.Algebra.Category.ModuleCat.Basic
variable {R M : Type _} [CommRing R] [AddCommGroup M] [Module R M]
variable (S₁ : Submodule R M) (T : Submodule R S₁) (f : T)

#check T -- with 2nd import, says `Submodule R ↑(ModuleCat.of R { x // x ∈ S₁ })`
#check (f : M) -- so this fails with 2nd import

In Lean 3 the instance was just a has_coe and this example doesn't fail. Is the failure known/expected? (edited to minimise)

[Eric Wieser]

I guess the contention here is Submodule -> ModuleCat -> Type vs Submodule -> Type

[Eric Wieser]

The two paths are defeq. That was enough in Lean3 because they shared the same coe head symbol, but in Lean4 coercions are transparent so you need syntactic equality

[Amelia Livingston]

I see, thanks. What's the right approach - do I need to avoid this coercion?

[Amelia Livingston]

Oh, is the answer to this "just use Subtype.val, since it's now syntactically equal to the coercion when the coercion works"?

[Eric Wieser]

I think the Submodule -> ModuleCat coercion is just bad

[Eric Wieser]

Does anything in mathlib use it?

[Amelia Livingston]

apparently not! I'll open a PR

[Eric Wieser]

It's probably a good idea to track down the blame in mathlib3 and link to the PR that added it