From 65e55ac094bbc3e81b5de14a03abe8a8b1df93fe Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Wed, 6 Aug 2025 14:05:45 -0700
Subject: [PATCH] fix: projection propagation in `grind` (#9772)

This PR fixes a bug in the projection over constructor propagator used
in `grind`. It may construct type incorrect terms when a equivalence
class contains heterogeneous equalities.

closes #9769
---
 src/Lean/Meta/Tactic/Grind/Proj.lean | 16 +++++++++++--
 tests/lean/run/grind_9769.lean       | 35 ++++++++++++++++++++++++++++
 2 files changed, 49 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/grind_9769.lean

diff --git a/src/Lean/Meta/Tactic/Grind/Proj.lean b/src/Lean/Meta/Tactic/Grind/Proj.lean
index 42d17425d3..050ede1fbe 100644
--- a/src/Lean/Meta/Tactic/Grind/Proj.lean
+++ b/src/Lean/Meta/Tactic/Grind/Proj.lean
@@ -26,12 +26,24 @@ def propagateProjEq (parent : Expr) : GoalM Unit := do
   -- It is wasteful to add equation if `parent` is not the root of its congruence class
   unless (← isCongrRoot parent) do return ()
   let arg := parent.appArg!
-  let ctor ← getRoot arg
+  let ctorNode ← getRootENode arg
+  let ctor := ctorNode.self
   unless ctor.isAppOf info.ctorName do return ()
   let parentNew ← if isSameExpr arg ctor then
     pure parent
   else
-    let parentNew ← shareCommon (mkApp parent.appFn! ctor)
+    let parentNew ← if ctorNode.heqProofs then
+      /-
+      When the equivalence class contains heterogeneous equalities,
+      type of `arg` and `ctor` may not be definitionally equal.
+      To ensure the projection application is type correct, we use
+      the `ctor` parameters.
+      -/
+      let projFn := parent.getAppFn
+      let params := ctor.getAppArgs[:info.numParams].toArray
+      shareCommon (mkApp (mkAppN projFn params) ctor)
+    else
+      shareCommon (mkApp parent.appFn! ctor)
     internalize parentNew (← getGeneration parent)
     pure parentNew
   trace_goal[grind.debug.proj] "{parentNew}"
diff --git a/tests/lean/run/grind_9769.lean b/tests/lean/run/grind_9769.lean
new file mode 100644
index 0000000000..1579ee05d4
--- /dev/null
+++ b/tests/lean/run/grind_9769.lean
@@ -0,0 +1,35 @@
+def Foo (n : Nat) := Σ (m : Nat), {f : Fin (n + 2) → Fin (m + 2) // f 0 = 0}
+
+variable (n : Nat)
+
+def Foo.e (f : Foo n) := f.2.1
+
+def Foo.id : (Foo n) := ⟨n, ⟨fun x => x, rfl⟩⟩
+
+def Foo.EqId (f : Foo n) : Prop :=
+  f = (Foo.id _)
+
+structure Bar {n m : Nat} (f : Fin (n + 2) → Fin (m + 1)) : Prop where
+  out : f 1 = 1
+
+/--
+error: `grind` failed
+case grind
+n : Nat
+f : Foo n
+this : Bar fun x => x
+h : ¬(Foo.EqId n f → Bar (Foo.e n f))
+⊢ False
+-/
+#guard_msgs in
+theorem EqIdToZero (f : Foo n) : f.EqId → Bar f.e := by
+  have : Bar (fun x => x : Fin (n + 2) → Fin (n + 2)) := ⟨rfl⟩
+  grind -verbose [Foo.e, Foo.id, Foo.EqId]
+
+-- A simpler example that is provable and also triggers issue #9769
+
+structure Boo (n : Nat) where
+  x : Nat
+
+example (a : Boo 1) (n : Nat) : a ≍ Boo.mk (n := n) b → n = 1 → a.x = b := by
+  grind