Another FunLike issue, with linear maps

Stream: mathlib4

[Joël Riou]

While trying to port Algebra.Category.Module.Basic !4#3260, some basic instances are not found. Here is an example of the problem:

example {R M N : Type _} [Semiring R] [AddCommMonoid M] [Module R M]
  [AddCommMonoid N] [Module R N] : FunLike (M →ₗ[R] N) M (fun _ => N) := inferInstance-- works

example {R M N : Type _} [Ring R] [AddCommGroup M] [Module R M]
  [AddCommGroup N] [Module R N] : FunLike (M →ₗ[R] N) M (fun _ => N) := inferInstance --fails

[Anne Baanen]

Does (temporarily) enabling etaExperiment help?

[Matthew Ballard]

Does attribute [-instance] Ring.toNonAssocRing in fix it?

[Joël Riou]

Indeed, both etaExperiment or -instance work!

[Moritz Doll]

Can we have a 2074 emoji?