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

@@ -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. -/

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

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