From 3a310fb122150ed113cc7b14c8d66a750f75fc40 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 25 Mar 2022 18:22:25 -0700
Subject: [PATCH] fix: the eta for structures implementation in the elaborator
 was different from the implementation in the kernel

This issue was exposed by issue #1074
---
 src/Lean/Meta/WHNF.lean                     | 15 +++++++++------
 tests/lean/etaStructIssue.lean              | 20 ++++++++++++++++++++
 tests/lean/etaStructIssue.lean.expected.out |  6 ++++++
 3 files changed, 35 insertions(+), 6 deletions(-)
 create mode 100644 tests/lean/etaStructIssue.lean
 create mode 100644 tests/lean/etaStructIssue.lean.expected.out

diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index aebf097005..9b902fce0f 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -129,12 +129,15 @@ private def toCtorWhenStructure (inductName : Name) (major : Expr) : MetaM Expr
       return major
     match majorType.getAppFn with
     | Expr.const d us _ =>
-      let some ctorName ← getFirstCtor d | pure major
-      let ctorInfo ← getConstInfoCtor ctorName
-      let mut result := mkAppN (mkConst ctorName us) (majorType.getAppArgs.shrink ctorInfo.numParams)
-      for i in [:ctorInfo.numFields] do
-        result := mkApp result (mkProj inductName i major)
-      return result
+      if (← whnfD (← inferType majorType)) == mkSort levelZero then
+        return major -- We do not perform eta for propositions, see implementation in the kernel
+      else
+        let some ctorName ← getFirstCtor d | pure major
+        let ctorInfo ← getConstInfoCtor ctorName
+        let mut result := mkAppN (mkConst ctorName us) (majorType.getAppArgs.shrink ctorInfo.numParams)
+        for i in [:ctorInfo.numFields] do
+          result := mkApp result (mkProj inductName i major)
+        return result
     | _ => return major
 
 /-- Auxiliary function for reducing recursor applications. -/
diff --git a/tests/lean/etaStructIssue.lean b/tests/lean/etaStructIssue.lean
new file mode 100644
index 0000000000..e495024470
--- /dev/null
+++ b/tests/lean/etaStructIssue.lean
@@ -0,0 +1,20 @@
+inductive E where
+  | mk : E → E
+
+inductive F : E → Prop
+  | mk : F e → F (E.mk e)
+
+theorem dec (x : F (E.mk e)) : F e ∧ True :=
+  match x with
+  | F.mk h => ⟨h, trivial⟩
+
+def mkNat (e : E) (x : F e) : Nat :=
+  match e with
+  | E.mk e' =>
+    match dec x with
+    | ⟨h, _⟩ => mkNat e' h
+
+theorem fail (e : E) (x₁ : F e) (x₂ : F (E.mk e)) : mkNat e x₁ = mkNat (E.mk e) x₂ :=
+  /- The following rfl was succeeding in the elaborator but failing in the kernel because
+     of a discrepancy in the implementation for Eta-for-structures. -/
+  rfl -- should fail
diff --git a/tests/lean/etaStructIssue.lean.expected.out b/tests/lean/etaStructIssue.lean.expected.out
new file mode 100644
index 0000000000..f475f3c065
--- /dev/null
+++ b/tests/lean/etaStructIssue.lean.expected.out
@@ -0,0 +1,6 @@
+etaStructIssue.lean:20:2-20:5: error: type mismatch
+  rfl
+has type
+  mkNat e x₁ = mkNat e x₁ : Prop
+but is expected to have type
+  mkNat e x₁ = mkNat (E.mk e) x₂ : Prop