Definitional equality nightmare

Stream: mathlib4

[Antoine Chambert-Loir]

In some work, I have two algebra structures that happen to be equal, and I need to define the equality map as a linear map.
Unfortunately, the compiler complains about some stuffs not being definitionally equal. The following MWE reduces the problem to docs#MulActionHom, and I can't understand what happens, since all possible implicit arguments are given.

import Mathlib.GroupTheory.GroupAction.Hom

section SMul

variable (R : Type*) (S : Type*) (smulRS : SMul R S) (smulRS' : SMul R S) (r : R) (x : S)
    (h : smulRS = smulRS')

lemma smulRS_eq (h : smulRS = smulRS') : @SMul.smul R S smulRS r x = @SMul.smul R S smulRS' r x := by
  rw [h]

def foo' (h : smulRS = smulRS') : @MulActionHom R R id S smulRS S smulRS' where
  toFun := id
  map_smul' r x : @SMul.smul R S smulRS r x = @SMul.smul R S smulRS' r x := sorry

end SMul

The error message arises when trying to define map_smul', even if one provides its correct type — the compiler returns:

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  smulRS'
inferred
  smulRS

[Robin Arnez]

You gotta write it out explicitly:

noncomputable def foo' (h : smulRS = smulRS') : @MulActionHom R R id S smulRS S smulRS' :=
  @MulActionHom.mk _ _ _ _ (_) _ (_) (fun x => x) (fun _ _ => h ▸ rfl)

[Antoine Chambert-Loir]

Is it expected, or is it kind of a bug of the elaborator?

[Antoine Chambert-Loir]

Thanks anyway, this helps a lot!

[Eric Wieser]

I think this is expected, since you're not supposed to have multiple instances of the same typeclass around

[Eric Wieser]

We use this workaround in mathlib for things like docs#Monoid.ext

[Antoine Chambert-Loir]

In our case, we definitely have several algebras instance appearing in course of the work, and they coincide mathematically, but they are not defined at the same time by the same people, and we have to reconcile everything.
Above was a MWE, what we have is a triple tensor product involving 3 modules and two semirings.

[Kevin Buzzard]

Algebra instances are dangerous in the sense that not only do they say "R acts on A" but because of the way mathlib is set up they also say the highly non-mathematical "...and you must never find another reason for R to act on A".