failed synth instance

Stream: mathlib4

[Jon Eugster]

Consider this MWE (see webeditor)

import Mathlib.Algebra.Module.LinearMap

variable {R M : Type} [Semiring R] [AddCommMonoid M] [Module R M]
#synth SemilinearMapClass (M →ₗ[R] M) (RingHom.id R) M M
-- works:
-- [Meta.synthInstance] ✅ SemilinearMapClass (M →ₗ[R] M) (RingHom.id R) M M ▼
--   [] ✅ apply @LinearMap.instSemilinearMapClassLinearMap to SemilinearMapClass (M →ₗ[R] M) (RingHom.id R) M M ▼
--     [tryResolve] ✅ SemilinearMapClass (M →ₗ[R] M) (RingHom.id R) M M ≟ SemilinearMapClass (M →ₗ[R] M) (RingHom.id R) M M

variable {S N : Type} [Ring S] [AddCommMonoid N] [Module S N]
#synth SemilinearMapClass (N →ₗ[S] N) (RingHom.id S) N N
-- fails:
-- [Meta.synthInstance] ❌ SemilinearMapClass (N →ₗ[S] N) (RingHom.id S) N N ▼
--   [] ❌ apply @LinearMap.instSemilinearMapClassLinearMap to SemilinearMapClass (N →ₗ[S] N) ?m.5106 ?m.5107 ?m.5108 ▼
--     [tryResolve] ❌ SemilinearMapClass (N →ₗ[S] N) ?m.5106 ?m.5107 ?m.5108 ≟ SemilinearMapClass (?m.5120 →ₛₗ[?m.5128] ?m.5121) ?m.5128 ?m.5120 ?m.5121

Does somebody know why lean fails with a Ring instead of a Semiring. In particular, why does the TC insert these ?m.5106 ?m.5107 ?m.5108 in the first step, when it appears that it should not do that.

The original problem was that it failed to coe a linear map over a ring to a function:

variable (f : N →ₗ[S] N)
#check (f : N → N) -- fails, does not find a coersion.

[Eric Wieser]

I would guess this is lean4#2074

[Eric Wieser]

Pretty much everything about linear maps over rings is going to be affected by that

[Jon Eugster]

oh I see, thx. Is there a workaround I could use for now?

[Eric Wieser]

Search though mathlib4 for mentions of "2074" for ideas