From 069fb4351cd6146af1f185b1feda4fcfb9dc7aff Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Fri, 30 May 2025 00:35:29 -0400
Subject: [PATCH] fix: inappropriate `whnfD` uses in `grind` (#8542)

This PR fixes two inappropriate uses of `whnfD` in `grind`. They were
potential performance foot guns, and were producing unexpected errors
since `whnfD` is not consistently used (and it should not be) in all
modules.
---
 src/Lean/Meta/Tactic/Grind/Internalize.lean   |  8 +--
 tests/lean/grind/product_eta.lean             | 19 -------
 .../lean/run/grind_product_eta_and_split.lean | 50 +++++++++++++++++++
 3 files changed, 55 insertions(+), 22 deletions(-)
 delete mode 100644 tests/lean/grind/product_eta.lean
 create mode 100644 tests/lean/run/grind_product_eta_and_split.lean

diff --git a/src/Lean/Meta/Tactic/Grind/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Internalize.lean
index 8a6c859363..ca9d58d915 100644
--- a/src/Lean/Meta/Tactic/Grind/Internalize.lean
+++ b/src/Lean/Meta/Tactic/Grind/Internalize.lean
@@ -87,7 +87,7 @@ private def checkAndAddSplitCandidate (e : Expr) : GoalM Unit := do
       else if (← getConfig).splitIndPred then
         addSplitCandidate (.default e)
   | .fvar .. =>
-    let .const declName _ := (← whnfD (← inferType e)).getAppFn | return ()
+    let .const declName _ := (← whnf (← inferType e)).getAppFn | return ()
     if (← get).split.casesTypes.isSplit declName then
       addSplitCandidate (.default e)
   | .forallE _ d _ _ =>
@@ -201,7 +201,7 @@ these facts.
 -/
 private def propagateEtaStruct (a : Expr) (generation : Nat) : GoalM Unit := do
   unless (← getConfig).etaStruct do return ()
-  let aType ← whnfD (← inferType a)
+  let aType ← whnf (← inferType a)
   matchConstStructureLike aType.getAppFn (fun _ => return ()) fun inductVal us ctorVal => do
     unless a.isAppOf ctorVal.name do
       -- TODO: remove ctorVal.numFields after update stage0
@@ -215,7 +215,9 @@ private def propagateEtaStruct (a : Expr) (generation : Nat) : GoalM Unit := do
           ctorApp := mkApp ctorApp proj
         ctorApp ← preprocessLight ctorApp
         internalize ctorApp generation
-        pushEq a ctorApp <| (← mkEqRefl a)
+        let u ← getLevel aType
+        let expectedProp := mkApp3 (mkConst ``Eq [u]) aType a ctorApp
+        pushEq a ctorApp <| mkExpectedPropHint (mkApp2 (mkConst ``Eq.refl [u]) aType a) expectedProp
 
 /-- Returns `true` if we can ignore `ext` for functions occurring as arguments of a `declName`-application. -/
 private def extParentsToIgnore (declName : Name) : Bool :=
diff --git a/tests/lean/grind/product_eta.lean b/tests/lean/grind/product_eta.lean
deleted file mode 100644
index 288ebc01fc..0000000000
--- a/tests/lean/grind/product_eta.lean
+++ /dev/null
@@ -1,19 +0,0 @@
--- In nightly-2025-05-27 this leads to grind internal error "trying to assert equality c = (c.fst, c.snd) with proof Eq.refl c which has type c = c which is not definitionally equal with `reducible` transparency setting"
-
-set_option grind.warning false
-set_option grind.debug true
-
-
-def α : Type := Unit × Unit
-
-def p (_ : α) : Prop := False
-/--
-error: tactic 'grind.cases' failed, (non-recursive) inductive type expected at c
-  α
-case grind
-c : α
-h : p c
-⊢ False
--/
-#guard_msgs in
-example : p c → False := by grind
diff --git a/tests/lean/run/grind_product_eta_and_split.lean b/tests/lean/run/grind_product_eta_and_split.lean
new file mode 100644
index 0000000000..bd1291b868
--- /dev/null
+++ b/tests/lean/run/grind_product_eta_and_split.lean
@@ -0,0 +1,50 @@
+set_option grind.warning false
+set_option grind.debug true
+
+def α : Type := Unit × Unit
+
+def p (_ : α) : Prop := False
+
+/--
+error: `grind` failed
+case grind
+c : α
+h : p c
+⊢ False
+[grind] Goal diagnostics
+  [facts] Asserted facts
+    [prop] p c
+  [eqc] True propositions
+    [prop] p c
+-/
+#guard_msgs in
+example : p c → False := by
+  grind
+
+example : p c → False := by
+  grind [p]
+
+
+def PosFin (n : Nat) := {x : Nat // 0 < x ∧ x < n}
+
+def f (_ : PosFin n) : Prop := False
+
+/--
+error: `grind` failed
+case grind
+n : Nat
+fst : PosFin n
+h : f fst
+⊢ False
+[grind] Goal diagnostics
+  [facts] Asserted facts
+    [prop] f fst
+  [eqc] True propositions
+    [prop] f fst
+-/
+#guard_msgs in
+example (n : Nat) (fst : PosFin n) (h : f fst) : False := by
+  grind
+
+example (n : Nat) (fst : PosFin n) (h : f fst) : False := by
+  grind [f]