From 86af04cc08c0dbbe0e735ea13d16edea3465f850 Mon Sep 17 00:00:00 2001
From: arthur-adjedj <arthur.adjedj@ens-paris-saclay.fr>
Date: Wed, 27 Mar 2024 18:15:01 +0100
Subject: [PATCH] fix: handle dependent fields when `deriving BEq`

---
 src/Lean/Elab/Deriving/BEq.lean | 11 ++++++++++-
 tests/lean/run/3740.lean        | 13 +++++++++++++
 2 files changed, 23 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/3740.lean

diff --git a/src/Lean/Elab/Deriving/BEq.lean b/src/Lean/Elab/Deriving/BEq.lean
index 10d2fae20a..81ffdb70ca 100644
--- a/src/Lean/Elab/Deriving/BEq.lean
+++ b/src/Lean/Elab/Deriving/BEq.lean
@@ -44,7 +44,8 @@ where
         let mut ctorArgs2 := #[]
         let mut rhs ← `(true)
         for i in [:ctorInfo.numFields] do
-          let x := xs[indVal.numParams + ctorInfo.numFields - i - 1]!
+          let pos := indVal.numParams + ctorInfo.numFields - i - 1
+          let x := xs[pos]!
           if type.containsFVar x.fvarId! then
             -- If resulting type depends on this field, we don't need to compare
             ctorArgs1 := ctorArgs1.push (← `(_))
@@ -59,6 +60,14 @@ where
               continue
             if xType.isAppOf indVal.name then
               rhs ← `($(mkIdent auxFunName):ident $a:ident $b:ident && $rhs)
+            /- If `x` appears in the type of another field, use `eq_of_beq` to
+               unify the types of the subsequent variables -/
+            else if ← xs[pos+1:].anyM
+                (fun fvar => (Lean.Expr.containsFVar · x.fvarId!) <$> (inferType fvar)) then
+              rhs ← `(if h : $a:ident == $b:ident then by
+                        cases (eq_of_beq h)
+                        exact $rhs
+                      else false)
             else
               rhs ← `($a:ident == $b:ident && $rhs)
           -- add `_` for inductive parameters, they are inaccessible
diff --git a/tests/lean/run/3740.lean b/tests/lean/run/3740.lean
new file mode 100644
index 0000000000..08511a9eeb
--- /dev/null
+++ b/tests/lean/run/3740.lean
@@ -0,0 +1,13 @@
+/-Ensure that `deriving BEq` works on structures/inductives dependently typed fields.-/
+
+structure BVBit where
+  {w : Nat}
+  idx : Fin w
+  foo : List (Fin w)
+  bar : foo = [idx]
+  deriving BEq
+
+inductive Foo where
+  | foo : (w : Nat) → Fin w → Foo
+  | bar : (w : Nat) → List (Fin w) → Foo
+  deriving BEq