Linear map diamond?

Stream: mathlib4

[Moritz Doll]

I wanted to port LinearPMap, but the definition already fails miserably:

import Mathlib.LinearAlgebra.Basic
import Mathlib.LinearAlgebra.Prod

open Set

universe u v w

structure LinearPmap (R : Type u) [Ring R] (E : Type v) [AddCommGroup E] [Module R E] (F : Type w)
  [AddCommGroup F] [Module R F] where
  domain : Submodule R E
  toFun : domain →ₗ[R] F

throws the error

application type mismatch
  LinearMap (RingHom.id R)
argument
  RingHom.id R
has type
  @RingHom R R NonAssocRing.toNonAssocSemiring NonAssocRing.toNonAssocSemiring : Type u
but is expected to have type
  @RingHom R R Semiring.toNonAssocSemiring Semiring.toNonAssocSemiring : Type u

It is probably the same issue as https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/LinearAlgebra.2ESpan.20!4.232248 and https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/LinearAlgebra.2EBasic.20!4.231979/near/327458361
Am I correct in assuming that we have to wait for the long-term solution before porting more linear algebra?

[Frédéric Dupuis]

You can try locally turning off instances to cut off one side of the problematic diamond, but otherwise this issue is indeed a show-stopper as far as I can tell.

[Eric Wieser]

This definitely looks like lean4#2074 to me

[Kevin Buzzard]

Well what are you waiting for -- try set_option synthInstance.etaExperiment true!

[Kevin Buzzard]

Oh, you're waiting for this to find its way into mathlib I guess

[Moritz Doll]

I just tried it and yes, it does not exist yet in mathlib4.

[Eric Wieser]

I was waiting for the github notification to make me aware that we now had that!

[Johan Commelin]

I guess we'll have a new nightly in a few hours