From 4d39a0b0e3d9db65295d0976162f16724ef8f2da Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Mon, 20 Nov 2023 01:51:47 -0800
Subject: [PATCH] fix: DecidableEq deriving handler could not handle fields
 whose types start with an implicit argument (#2918)

Fixes #2914
---
 src/Lean/Elab/Deriving/DecEq.lean             |  6 ++---
 .../decEqMutualInductives.lean.expected.out   | 24 +++++++++----------
 tests/lean/run/2914.lean                      |  8 +++++++
 3 files changed, 23 insertions(+), 15 deletions(-)
 create mode 100644 tests/lean/run/2914.lean

diff --git a/src/Lean/Elab/Deriving/DecEq.lean b/src/Lean/Elab/Deriving/DecEq.lean
index 2bf23e69a9..a42f1590a3 100644
--- a/src/Lean/Elab/Deriving/DecEq.lean
+++ b/src/Lean/Elab/Deriving/DecEq.lean
@@ -24,15 +24,15 @@ where
     | [] => ``(isTrue rfl)
     | (a, b, recField, isProof) :: todo => withFreshMacroScope do
       let rhs ← if isProof then
-        `(have h : $a = $b := rfl; by subst h; exact $(← mkSameCtorRhs todo):term)
+        `(have h : @$a = @$b := rfl; by subst h; exact $(← mkSameCtorRhs todo):term)
       else
-        `(if h : $a = $b then
+        `(if h : @$a = @$b then
            by subst h; exact $(← mkSameCtorRhs todo):term
           else
            isFalse (by intro n; injection n; apply h _; assumption))
       if let some auxFunName := recField then
         -- add local instance for `a = b` using the function being defined `auxFunName`
-        `(let inst := $(mkIdent auxFunName) $a $b; $rhs)
+        `(let inst := $(mkIdent auxFunName) @$a @$b; $rhs)
       else
         return rhs
 
diff --git a/tests/lean/decEqMutualInductives.lean.expected.out b/tests/lean/decEqMutualInductives.lean.expected.out
index ed660187e7..a64cfd9733 100644
--- a/tests/lean/decEqMutualInductives.lean.expected.out
+++ b/tests/lean/decEqMutualInductives.lean.expected.out
@@ -3,8 +3,8 @@
        private def decEqTree✝ (x✝ : @Tree✝) (x✝¹ : @Tree✝) : Decidable✝ (x✝ = x✝¹) :=
          match x✝, x✝¹ with
          | @Tree.node a✝, @Tree.node b✝ =>
-           let inst✝ := decEqListTree✝ a✝ b✝;
-           if h✝ : a✝ = b✝ then by subst h✝; exact isTrue✝ rfl✝
+           let inst✝ := decEqListTree✝ @a✝ @b✝;
+           if h✝ : @a✝ = @b✝ then by subst h✝; exact isTrue✝ rfl✝
            else isFalse✝ (by intro n✝; injection n✝; apply h✝ _; assumption)
        private def decEqListTree✝ (x✝² : @ListTree✝) (x✝³ : @ListTree✝) : Decidable✝ (x✝² = x✝³) :=
          match x✝², x✝³ with
@@ -12,11 +12,11 @@
          | ListTree.nil .., ListTree.cons .. => isFalse✝¹ (by intro h✝¹; injection h✝¹)
          | ListTree.cons .., ListTree.nil .. => isFalse✝¹ (by intro h✝¹; injection h✝¹)
          | @ListTree.cons a✝¹ a✝², @ListTree.cons b✝¹ b✝² =>
-           let inst✝¹ := decEqTree✝ a✝¹ b✝¹;
-           if h✝² : a✝¹ = b✝¹ then by subst h✝²;
+           let inst✝¹ := decEqTree✝ @a✝¹ @b✝¹;
+           if h✝² : @a✝¹ = @b✝¹ then by subst h✝²;
              exact
-               let inst✝² := decEqListTree✝ a✝² b✝²;
-               if h✝³ : a✝² = b✝² then by subst h✝³; exact isTrue✝² rfl✝²
+               let inst✝² := decEqListTree✝ @a✝² @b✝²;
+               if h✝³ : @a✝² = @b✝² then by subst h✝³; exact isTrue✝² rfl✝²
                else isFalse✝² (by intro n✝¹; injection n✝¹; apply h✝³ _; assumption)
            else isFalse✝³ (by intro n✝²; injection n✝²; apply h✝² _; assumption)
      end,
@@ -30,20 +30,20 @@
          | Foo₁.foo₁₁ .., Foo₁.foo₁₂ .. => isFalse✝ (by intro h✝; injection h✝)
          | Foo₁.foo₁₂ .., Foo₁.foo₁₁ .. => isFalse✝ (by intro h✝; injection h✝)
          | @Foo₁.foo₁₂ a✝, @Foo₁.foo₁₂ b✝ =>
-           let inst✝ := decEqFoo₂✝ a✝ b✝;
-           if h✝¹ : a✝ = b✝ then by subst h✝¹; exact isTrue✝¹ rfl✝¹
+           let inst✝ := decEqFoo₂✝ @a✝ @b✝;
+           if h✝¹ : @a✝ = @b✝ then by subst h✝¹; exact isTrue✝¹ rfl✝¹
            else isFalse✝¹ (by intro n✝; injection n✝; apply h✝¹ _; assumption)
        private def decEqFoo₂✝ (x✝² : @Foo₂✝) (x✝³ : @Foo₂✝) : Decidable✝ (x✝² = x✝³) :=
          match x✝², x✝³ with
          | @Foo₂.foo₂ a✝¹, @Foo₂.foo₂ b✝¹ =>
-           let inst✝¹ := decEqFoo₃✝ a✝¹ b✝¹;
-           if h✝² : a✝¹ = b✝¹ then by subst h✝²; exact isTrue✝² rfl✝²
+           let inst✝¹ := decEqFoo₃✝ @a✝¹ @b✝¹;
+           if h✝² : @a✝¹ = @b✝¹ then by subst h✝²; exact isTrue✝² rfl✝²
            else isFalse✝² (by intro n✝¹; injection n✝¹; apply h✝² _; assumption)
        private def decEqFoo₃✝ (x✝⁴ : @Foo₃✝) (x✝⁵ : @Foo₃✝) : Decidable✝ (x✝⁴ = x✝⁵) :=
          match x✝⁴, x✝⁵ with
          | @Foo₃.foo₃ a✝², @Foo₃.foo₃ b✝² =>
-           let inst✝² := decEqFoo₁✝ a✝² b✝²;
-           if h✝³ : a✝² = b✝² then by subst h✝³; exact isTrue✝³ rfl✝³
+           let inst✝² := decEqFoo₁✝ @a✝² @b✝²;
+           if h✝³ : @a✝² = @b✝² then by subst h✝³; exact isTrue✝³ rfl✝³
            else isFalse✝³ (by intro n✝²; injection n✝²; apply h✝³ _; assumption)
      end,
      instance : DecidableEq✝ (@Foo₁✝) :=
diff --git a/tests/lean/run/2914.lean b/tests/lean/run/2914.lean
new file mode 100644
index 0000000000..270038e503
--- /dev/null
+++ b/tests/lean/run/2914.lean
@@ -0,0 +1,8 @@
+/-
+The DecidableEq deriving handler should succeed even if fields have types starting with implicit arguments.
+-/
+
+structure Foo where
+  a : List Nat
+  ha : ∀ {i}, i ∈ a → 0 < i
+deriving DecidableEq