From a2ed4db562fda1455b850896c311c6c239a86827 Mon Sep 17 00:00:00 2001
From: Arthur Adjedj <aarthuur01@gmail.com>
Date: Thu, 18 Jan 2024 03:32:51 +0100
Subject: [PATCH] fix: `derive BEq` on structure with `Prop`-fields (#3191)

Closes #3140

---------

Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
---
 src/Lean/Elab/Deriving/BEq.lean   |  5 ++++-
 src/Lean/Elab/Deriving/DecEq.lean |  5 +++--
 tests/lean/3140.lean              | 11 +++++++++++
 tests/lean/3140.lean.expected.out |  3 +++
 4 files changed, 21 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/3140.lean
 create mode 100644 tests/lean/3140.lean.expected.out

diff --git a/src/Lean/Elab/Deriving/BEq.lean b/src/Lean/Elab/Deriving/BEq.lean
index 7ebe5cbbdfc0..ab9aca093b4c 100644
--- a/src/Lean/Elab/Deriving/BEq.lean
+++ b/src/Lean/Elab/Deriving/BEq.lean
@@ -57,7 +57,10 @@ where
             let b := mkIdent (← mkFreshUserName `b)
             ctorArgs1 := ctorArgs1.push a
             ctorArgs2 := ctorArgs2.push b
-            if (← inferType x).isAppOf indVal.name then
+            let xType ← inferType x
+            if (← isProp xType) then
+              continue
+            if xType.isAppOf indVal.name then
               rhs ← `($rhs && $(mkIdent auxFunName):ident $a:ident $b:ident)
             else
               rhs ← `($rhs && $a:ident == $b:ident)
diff --git a/src/Lean/Elab/Deriving/DecEq.lean b/src/Lean/Elab/Deriving/DecEq.lean
index 09b0a83cdfa8..d2ab52bce931 100644
--- a/src/Lean/Elab/Deriving/DecEq.lean
+++ b/src/Lean/Elab/Deriving/DecEq.lean
@@ -67,11 +67,12 @@ where
                 let b := mkIdent (← mkFreshUserName `b)
                 ctorArgs1 := ctorArgs1.push a
                 ctorArgs2 := ctorArgs2.push b
+                let xType ← inferType x
                 let indValNum :=
                   ctx.typeInfos.findIdx?
-                  ((← inferType x).isAppOf ∘ ConstantVal.name ∘ InductiveVal.toConstantVal)
+                  (xType.isAppOf ∘ ConstantVal.name ∘ InductiveVal.toConstantVal)
                 let recField  := indValNum.map (ctx.auxFunNames[·]!)
-                let isProof   := (← inferType (← inferType x)).isProp
+                let isProof ← isProp xType
                 todo := todo.push (a, b, recField, isProof)
             patterns := patterns.push (← `(@$(mkIdent ctorName₁):ident $ctorArgs1:term*))
             patterns := patterns.push (← `(@$(mkIdent ctorName₁):ident $ctorArgs2:term*))
diff --git a/tests/lean/3140.lean b/tests/lean/3140.lean
new file mode 100644
index 000000000000..6d93a65ddabe
--- /dev/null
+++ b/tests/lean/3140.lean
@@ -0,0 +1,11 @@
+/- Verify that `deriving BEq` works on structures with `Prop`-fields.-/
+
+structure S where
+  foo : Nat
+  p : True
+  Bar : Nat
+  deriving BEq
+
+#eval (⟨1,⟨⟩,2⟩ : S) == ⟨1,⟨⟩,3⟩ -- false
+#eval (⟨1,⟨⟩,2⟩ : S) == ⟨2,⟨⟩,2⟩ -- false
+#eval (⟨1,⟨⟩,2⟩ : S) == ⟨1,⟨⟩,2⟩ -- true
diff --git a/tests/lean/3140.lean.expected.out b/tests/lean/3140.lean.expected.out
new file mode 100644
index 000000000000..52289c68f91b
--- /dev/null
+++ b/tests/lean/3140.lean.expected.out
@@ -0,0 +1,3 @@
+false
+false
+true