Confusing error when making a parameterized `SubNegMonoid`

Stream: mathlib4

[Geoffrey Irving]

This was a surprisingly weird error:

import Mathlib.Algebra.Group.Defs

/-- RGBA colors -/
structure Color (α : Type) where
  r : α
  g : α
  b : α
  a : α

variable {α β : Type}

lemma Color.ext_iff (x y : Color α) : x = y ↔ x.r = y.r ∧ x.g = y.g ∧ x.b = y.b ∧ x.a = y.a := by
  induction x; induction y; simp only [mk.injEq]

-- Componentwise operations
instance [Zero α] : Zero (Color α) where zero := ⟨0, 0, 0, 0⟩
instance [Neg α] : Neg (Color α) where neg x := ⟨-x.r, -x.g, -x.b, -x.a⟩
instance [Add α] : Add (Color α) where add x y := ⟨x.r + y.r, x.g + y.g, x.b + y.b, x.a + y.a⟩
instance [Sub α] : Sub (Color α) where sub x y := ⟨x.r - y.r, x.g - y.g, x.b - y.b, x.a - y.a⟩

-- Definition lemmas (unfortunately duplication here)
lemma zero_def [Zero α] : (0 : Color α) = ⟨0, 0, 0, 0⟩ := rfl
lemma neg_def [Neg α] (x : Color α): -x = ⟨-x.r, -x.g, -x.b, -x.a⟩ := rfl
lemma add_def [Add α] (x y : Color α): x + y = ⟨x.r + y.r, x.g + y.g, x.b + y.b, x.a + y.a⟩ := rfl
lemma sub_def [Sub α] (x y : Color α): x - y = ⟨x.r - y.r, x.g - y.g, x.b - y.b, x.a - y.a⟩ := rfl

/-- Colors form an additive monoid -/
instance [AddMonoid α] : AddMonoid (Color α) where
  add_assoc _ _ _ := by simp only [Color.ext_iff, add_def, add_assoc]
  zero_add _ := by simp only [Color.ext_iff, add_def, zero_def, zero_add]
  add_zero _ := by simp only [Color.ext_iff, add_def, zero_def, add_zero]

/-- Colors form a `SubNegMonoid` -/
instance [SubNegMonoid α] : SubNegMonoid (Color α) where
  -- Produces the confusing error
  --   type mismatch
  --     HEq.rfl
  --   has type
  --     HEq ?m.7366 ?m.7366 : Prop
  --   but is expected to have type
  --     a✝ - b✝ = a✝ + -b✝ : Prop
  -- Adding the following line fixes it
  --   sub_eq_add_neg _ _ := by simp only [Color.ext_iff, add_def, neg_def, sub_def, sub_eq_add_neg]

The problem is just that I haven't defined the sub_eq_add_neg part of SubNegMonoid (which is the whole thing, really). But instead of saying "you've left out sub_eq_add_neg", it produces a weird HEq.rfl error.

[Geoffrey Irving]

Oh, I see, there's just a default value there since for non-computational things one might not define Sub. I suppose this is hard to fix then.

[Ruben Van de Velde]

The error could perhaps be clarified. The reason this happens is that SubNegMonoid has a default definition for Sub (defining a - b := a + (-b), and a default proof for sub_eq_add_neg ("it's true by definition"). But that proof doesn't work when you manually define Sub

[Geoffrey Irving]

Yeah, if the error could somehow mention sub_eq_add_neg it would be ideal, but that might not be worth the trouble.

[Ruben Van de Velde]

Oh, I hadn't even noticed that it doesn't mention the field. That seems worth filing as an issue on lean, if it hasn't been filed yet

[Geoffrey Irving]

Originally I hit the error trying to define AddGroup directly, so it was not at all obvious what was going on.

[Eric Wieser]

This has been discussed a lot before, but I don't know if an issue was ever filed

[Geoffrey Irving]

Here is a no-import example:

variable {α : Type}

class Yop (α : Type) where
  yop : α → α

class Nop (α : Type) [Yop α] where
  nop : ∀ x : α, Yop.yop x = x := by intro; rfl

structure A where
  x : Nat

instance : Yop A where
  yop a := ⟨a.x + 1⟩

instance : Nop A where
  -- `nop` is not defined, but the error message does not mention `nop`:
  --   tactic 'rfl' failed, equality lhs
  --     Yop.yop x✝
  --   is not definitionally equal to rhs
  --     x✝
  --   α: Type
  --   x✝: A
  --   ⊢ Yop.yop x✝ = x✝

[Matthew Ballard]

Is there a tactic to prepend/append to the error message on failure?

[Matthew Ballard]

There should be a core issue asking for more informative errors for default values if there isn’t one already

[Geoffrey Irving]

https://github.com/leanprover/lean4/issues/2950

[Matthew Ballard]

Great! I :+1:’ed it