Bug: grind linarith crashes in the presence of conflicting `hAdd` instances

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The existence of overlapping instances of hAdd lead to a crash in grind linarith.

Steps to Reproduce

Minimal reproducer:

@[reducible] def Poly := Vector (Fin 7) 4
 
-- Add and HAdd already exist for Vector
-- Redefining Add here creates another instance of HAdd (derived from Add)
@[reducible]
instance myAdd : Add Poly where -- an instance of HAdd is 
   add f g := Vector.map (fun i => f[i]! + g[i]!) (Vector.range 4)
 
 example (n : Nat) (p q : Poly) (hp : p + q = p) : n = n := by
   grind  -- ERROR: expected instHAdd to be defeq to instHAdd

Small variant (we directly redefine HAdd)

@[reducible] def Poly := Vector (Fin 7) 4
 
 instance myHAdd : HAdd Poly Poly Poly where
   hAdd f g := Vector.map (fun i => f[i]! + g[i]!) (Vector.range 4)
 
 example (n : Nat) (p q : Poly) (hp : p + q = p) : n = n := by
   grind  -- ERROR: expected myHAdd to be defeq to instHAdd

Expected behavior: grind doesn't crash

Actual behavior: grind crashes

Versions

Tested on Lean 4.29.0

Impact

Minor on my side as the fix is straightforward.

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

Start by running the minimal reproducer with Lean nightly and tracing the grind linarith path involved in resolving the conflicting hAdd instances. Use both reproducer variants to isolate the crash, then add a regression test showing that grind completes without crashing and preserves the expected behavior.