Duplicate instances introduced through inheritance gives confusing errors

[adri326]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

Consider the following piece of code that our user has written:

class Add' (G: Type) extends Add G

def add' {G: Type} [Add' G] (a b: G): G := a + b

variable {G: Type}
variable [Add G]

def add (a b: G): G := a + b

theorem add_eq_add [Add' G] (a b: G): add a b = add' a b := by
  simp [add, add']
  rfl

The class Add' inherits from Add, which means that when the theorem is being formulated, two different instances of Add G are added to the context: one from the variable [Add G], used in the definition of add, and one inherited from Add' G, used in the definition of add'.

As soon as the user tries to apply the rfl tactic to solve the goal, they are met with an ambiguous error:

tactic 'rfl' failed, equality lhs
  a + b
is not definitionally equal to rhs
  a + b
G: Type
inst✝¹: Add G
inst✝: Add' G
ab: G
⊢ a + b = a + b

Supposing the user has already experienced issues with multiple instances of operator overloading, they go on and hover over the two version of a + b, to see if those might refer to different operations.
However, both print the same function used by +:

@HAdd.hAdd G G G instHAdd a b : G

At this point, the user has no idea that what is causing this issue are the two instances of Add G present in the context (one being hidden away behind Add' G), and that the additions are each defined on different instances of Add G.

To fix the error, the user should remove the variable [Add G] and move the instance requirement to the def add directly.

Context

I was working on porting a WIP proof of Rubin's theorem from Lean3 to Lean4, and was putting theorems in different files.
Since variable statements aren't physically close to the theorem that uses it, I pre-emptively put a few class instances that I thought were needed afterwards, namely:

variable {G α β : Type _}
variable [Group G]
variable [MulAction G α] [MulAction G β]

However, this file also defines the following class before that:

class ContinuousMulAction (G α : Type _) [Group G] [TopologicalSpace α] extends
    MulAction G α where
  continuous : ∀ g : G, Continuous (fun x: α => g • x)

So when a theorem also had the [ContinuousMulAction G α] requirement, I ended up having two version of the scalar multiplication operator floating around, inevitably leading to a very confusing error.

Steps to Reproduce

1. Have two classes A B, the second inheriting from the first, and the first having a method
2. Define a function fa requiring an instance of the first class
3. Define an equivalent function fb requiring an instance of the second class
4. Define a theorem that requires both an instance of A and B, such that an equality between fa and fb needs to be proven
5. Try to prove the theorem

Expected behavior:

When printing an error where two visually equal expressions are definitionally different,
Lean should give hints as to which instances of a function/operator within the expressions differ.

When doing this, Lean should also give a hint that two "conflicting" instances were present in the context, and point to how each instance relate to instance hypotheses in the current context.

Actual behavior:

An error stating that two visually equal expressions is given, and any inspection made by the user does not help them figure out the cause of the error.

Versions

$ lean --version
Lean (version 4.3.0-rc2, commit 8e5cf6466061, Release)
$ uname -a
Linux deskryx 6.5.9-arch2-1 #1 SMP PREEMPT_DYNAMIC Thu, 26 Oct 2023 00:52:20 +0000 x86_64 GNU/Linux

Additional Information

N/A

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[nomeata]

These days we produce the following error message:

tactic 'rfl' failed, the left-hand side
  @HAdd.hAdd G G G (@instHAdd G inst✝¹) a b
is not definitionally equal to the right-hand side
  @HAdd.hAdd G G G (@instHAdd G Add'.toAdd) a b
G : Type
inst✝¹ : Add G
inst✝ : Add' G
a b : G
⊢ a + b = a + b

That should resolve this, shouldn’t it?