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

@@ -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 :=

tests/lean/grind/product_eta.lean

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

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]