Diamond problem with notation

Stream: lean4

[Jesse Vogel]

Consider the structures as in the code below. The examples labeled 'bad' do not work because the types x * y and x + y do not match. Why can't Lean see these types are the same? I know one could use typeclasses, e.g. class MulAdd (α : Type u) extends Mul α, Add α, but this is not what I want to do. Is there a way to get this 'diamond problem' to work well with the custom notation?

namespace Test

structure Set where
  set : Type u

structure Mul extends Set where
  mul : set → set → set

structure Add extends Set where
  add : set → set → set

infixl:80 " * " => Mul.mul _
infixl:60 " + " => Add.add _

structure MulAdd extends Mul, Add

-- Bad: types of `x * y` and `x + y` do not match
example (X : MulAdd) (x y : X.set) : x * y = x + y := by sorry
-- Good: in this case they do match
example (X : MulAdd) (x y : X.set) : X.mul x y = X.add x y := by sorry

-- Bad: fails for the same reason as above
example (X : MulAdd) (x y : X.set) : X.mul x y = Add.add _ x y := by sorry
-- Good: this works, apparently because of the order "Mul, Add" as opposed to "Add, Mul"
example (X : MulAdd) (x y : X.set) : Mul.mul _ x y = X.add x y := by sorry

end Test

[Sebastian Ullrich]

If you use set_option pp.all true, the unification failure may appear more sensible:

type mismatch
  Test.Add.add.{?u.6126} ?m.6127 ?m.6144 ?m.6153
has type
  Test.Set.set.{?u.6126} (Test.Add.toSet.{?u.6126} ?m.6127) : Type ?u.6126
but is expected to have type
  Test.Set.set.{?u.6087} (Test.Mul.toSet.{?u.6087} (Test.MulAdd.toMul.{?u.6087} X)) : Type ?u.6087

Three parts of the diamond are present, but there is no indication to Lean that it should use the fourth part to complete the diamond. We can however give Lean the explicit hint to do so.

unif_hint (a : Add) (ma : MulAdd) where
  a =?= MulAdd.toAdd ma ⊢ Add.toSet a =?= Mul.toSet (MulAdd.toMul ma)

The unification hint system is relatively unexplored so far though, so might not be completely stable yet