From e579dfdb145337e213c42b01781ac0664f48c635 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Fri, 13 Feb 2026 16:43:15 -0800
Subject: [PATCH] fix: assertion violation in `mkEqProofImpl` (#12473)

This PR fixes an assertion violation in `grind` reported at #12246 This
assertion fails when in examples containing heterogenous equalities with
elements of different types (e.g., `Fin n` and `Fin m`) attached to the
same theory solver.

Closes #12246
---
 src/Lean/Meta/Tactic/Grind/Proof.lean |  3 +-
 src/Lean/Meta/Tactic/Grind/Types.lean | 11 +++++--
 tests/lean/run/grind_12246.lean       | 42 +++++++++++++++++++++++++++
 3 files changed, 53 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/grind_12246.lean

diff --git a/src/Lean/Meta/Tactic/Grind/Proof.lean b/src/Lean/Meta/Tactic/Grind/Proof.lean
index a3f4af97f7..73a6f5f56a 100644
--- a/src/Lean/Meta/Tactic/Grind/Proof.lean
+++ b/src/Lean/Meta/Tactic/Grind/Proof.lean
@@ -334,7 +334,8 @@ It assumes `a` and `b` are in the same equivalence class.
 -/
 @[export lean_grind_mk_eq_proof]
 def mkEqProofImpl (a b : Expr) : GoalM Expr := do
-  assert! (← hasSameType a b)
+  unless (← hasSameType a b) do
+    throwError "internal `grind` error, `mkEqProof` invoked with terms of different types{indentExpr a}\nhas type{indentExpr (← inferType a)}\nbut{indentExpr b}\nhas type{indentExpr (← inferType b)}"
   mkEqProofCore a b (heq := false)
 
 @[export lean_grind_mk_heq_proof]
diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean
index ef858b0f7d..6f33c91174 100644
--- a/src/Lean/Meta/Tactic/Grind/Types.lean
+++ b/src/Lean/Meta/Tactic/Grind/Types.lean
@@ -1967,7 +1967,10 @@ def SolverExtension.markTerm (ext : SolverExtension σ) (e : Expr) : GoalM Unit
     | .nil => return .next id e .nil
     | .next id' e' sTerms' =>
       if id == id' then
-        (← solverExtensionsRef.get)[id]!.newEq e e'
+        -- Skip if `e` and `e'` have different types (e.g., they were merged via `HEq` from `cast`).
+        -- This can happen when we have heterogenous equalities in an equivalence class containing types such as `Fin n` and `Fin m`
+        if (← pure !root.heqProofs <||> hasSameType e e') then
+          (← solverExtensionsRef.get)[id]!.newEq e e'
         return sTerms
       else if id < id' then
         return .next id e sTerms
@@ -2047,7 +2050,11 @@ where
     match p with
     | .nil => return ()
     | .eq solverId lhs rhs rest =>
-      (← solverExtensionsRef.get)[solverId]!.newEq lhs rhs
+      -- Skip if `lhs` and `rhs` have different types (e.g., they were merged via `HEq` from `cast`).
+      -- This can happen when we have heterogenous equalities in an equivalence class containing types such as `Fin n` and `Fin m`
+      let root ← getRootENode lhs
+      if (← pure !root.heqProofs <||> hasSameType lhs rhs) then
+        (← solverExtensionsRef.get)[solverId]!.newEq lhs rhs
       go rest
     | .diseqs solverId parentSet rest =>
       forEachDiseq parentSet (propagateDiseqOf solverId)
diff --git a/tests/lean/run/grind_12246.lean b/tests/lean/run/grind_12246.lean
new file mode 100644
index 0000000000..5138d036c5
--- /dev/null
+++ b/tests/lean/run/grind_12246.lean
@@ -0,0 +1,42 @@
+import Std.Do
+import Std.Tactic.Do
+
+def Matrix' (α β γ : Type) : Type := α → β → γ
+
+namespace Matrix'
+
+variable {α : Type} {m n : Nat} {M : Matrix' (Fin m) (Fin n) α}
+variable {i i' : Fin m} {j j' : Fin n}
+
+def shuffleRows (M : Matrix' (Fin m) (Fin n) α) (j : Fin n) :
+    Matrix' (Fin m) (Fin n) α := sorry
+
+def altColSort (M : Matrix' (Fin m) (Fin n) α) :
+    Matrix' (Fin m) (Fin n) α := Id.run do
+  let mut M' : Matrix' (Fin m) (Fin n) α := M
+  for hj : j in [:n] do M' := M'.shuffleRows ⟨j, by sorry⟩
+  return M'
+
+open Std.Do
+
+variable [LE α] [Std.IsLinearOrder α]
+
+set_option mvcgen.warning false
+
+def Monotone' {α : Type} [LE α] (f : Fin n → α) : Prop := ∀ i j, i ≤ j → f i ≤ f j
+
+attribute [grind =] Fin.le_def Monotone'
+
+theorem altColSort_rowSorted' (hM : ∀ i, Monotone' (M i)) (i : Fin m) :
+    Monotone' (M.altColSort i) := by
+  generalize h : M.altColSort = x
+  apply Id.of_wp_run_eq h
+  mvcgen invariants
+  | inv1 => ⇓⟨cur, M'⟩ => ⌜(∀ j : Fin n, j < cur.pos → Monotone' (M' · j))⌝
+  case vc2 => grind
+  case vc3 => sorry
+  case vc1 =>
+    fail_if_success grind -verbose
+    sorry
+
+end Matrix'