fix: handle dependent fields when deriving BEq

src/Init/Data/Nat/Linear.lean

@@ -173,13 +173,13 @@ instance : LawfulBEq PolyCnstr where
   eq_of_beq {a b} h := by
     cases a; rename_i eq₁ lhs₁ rhs₁
     cases b; rename_i eq₂ lhs₂ rhs₂
-    have h : eq₁ == eq₂ && lhs₁ == lhs₂ && rhs₁ == rhs₂ := h
+    have h : eq₁ == eq₂ && (lhs₁ == lhs₂ && rhs₁ == rhs₂) := h
     simp at h
-    have ⟨⟨h₁, h₂⟩, h₃⟩ := h
+    have ⟨h₁, h₂, h₃⟩ := h
     rw [h₁, h₂, h₃]
   rfl {a} := by
     cases a; rename_i eq lhs rhs
-    show (eq == eq && lhs == lhs && rhs == rhs) = true
+    show (eq == eq && (lhs == lhs && rhs == rhs)) = true
     simp [LawfulBEq.rfl]
 
 def PolyCnstr.mul (k : Nat) (c : PolyCnstr) : PolyCnstr :=

src/Lean/Elab/Deriving/BEq.lean

@@ -43,12 +43,10 @@ where
         let mut ctorArgs1 := #[]
         let mut ctorArgs2 := #[]
         let mut rhs ← `(true)
-        -- add `_` for inductive parameters, they are inaccessible
-        for _ in [:indVal.numParams] do
-          ctorArgs1 := ctorArgs1.push (← `(_))
-          ctorArgs2 := ctorArgs2.push (← `(_))
+        let mut rhs_empty := true
         for i in [:ctorInfo.numFields] do
-          let x := xs[indVal.numParams + i]!
+          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 (← `(_))
@@ -62,11 +60,32 @@ where
             if (← isProp xType) then
               continue
             if xType.isAppOf indVal.name then
-              rhs ← `($rhs && $(mkIdent auxFunName):ident $a:ident $b:ident)
+              if rhs_empty then
+                rhs ← `($(mkIdent auxFunName):ident $a:ident $b:ident)
+                rhs_empty := false
+              else
+                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 => (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)
+              rhs_empty := false
             else
-              rhs ← `($rhs && $a:ident == $b:ident)
-        patterns := patterns.push (← `(@$(mkIdent ctorName):ident $ctorArgs1:term*))
-        patterns := patterns.push (← `(@$(mkIdent ctorName):ident $ctorArgs2:term*))
+              if rhs_empty then
+                rhs ← `($a:ident == $b:ident)
+                rhs_empty := false
+              else
+                rhs ← `($a:ident == $b:ident && $rhs)
+          -- add `_` for inductive parameters, they are inaccessible
+        for _ in [:indVal.numParams] do
+          ctorArgs1 := ctorArgs1.push (← `(_))
+          ctorArgs2 := ctorArgs2.push (← `(_))
+        patterns := patterns.push (← `(@$(mkIdent ctorName):ident $ctorArgs1.reverse:term*))
+        patterns := patterns.push (← `(@$(mkIdent ctorName):ident $ctorArgs2.reverse:term*))
         `(matchAltExpr| | $[$patterns:term],* => $rhs:term)
       alts := alts.push alt
     alts := alts.push (← mkElseAlt)