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

@@ -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)

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*))

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

tests/lean/3140.lean.expected.out

@@ -0,0 +1,3 @@
+false
+false
+true