feat: use cast to "fix" types in the E-matching module within grind (#6750)

This PR adds support for fixing type mismatches using `cast` while
instantiating quantifiers in the E-matching module used by the grind
tactic.

src/Lean/Meta/Tactic/Grind.lean

@@ -73,5 +73,6 @@ builtin_initialize registerTraceClass `grind.debug.offset.proof
 builtin_initialize registerTraceClass `grind.debug.ematch.pattern
 builtin_initialize registerTraceClass `grind.debug.beta
 builtin_initialize registerTraceClass `grind.debug.matchCond
+builtin_initialize registerTraceClass `grind.debug.matchCond.lambda
 
 end Lean

src/Lean/Meta/Tactic/Grind/Core.lean

@@ -13,6 +13,7 @@ import Lean.Meta.Tactic.Grind.Ctor
 import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Tactic.Grind.Beta
 import Lean.Meta.Tactic.Grind.Internalize
+import Lean.Meta.Tactic.Grind.Simp
 
 namespace Lean.Meta.Grind
 
@@ -233,18 +234,19 @@ private def popNextEq? : GoalM (Option NewEq) := do
     modify fun s => { s with newEqs := s.newEqs.pop }
   return r
 
-private partial def addEqCore (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit := do
-  addEqStep lhs rhs proof isHEq
-  processTodo
-where
-  processTodo : GoalM Unit := do
+private def processNewEqs : GoalM Unit := do
+  repeat
     if (← isInconsistent) then
       resetNewEqs
       return ()
     checkSystem "grind"
-    let some { lhs, rhs, proof, isHEq } := (← popNextEq?) | return ()
+    let some { lhs, rhs, proof, isHEq } := (← popNextEq?)
+      | return ()
     addEqStep lhs rhs proof isHEq
-    processTodo
+
+private def addEqCore (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit := do
+  addEqStep lhs rhs proof isHEq
+  processNewEqs
 
 /-- Adds a new equality `lhs = rhs`. It assumes `lhs` and `rhs` have already been internalized. -/
 private def addEq (lhs rhs proof : Expr) : GoalM Unit := do
@@ -309,4 +311,56 @@ where
 def addHypothesis (fvarId : FVarId) (generation := 0) : GoalM Unit := do
   add (← fvarId.getType) (mkFVar fvarId) generation
 
+/--
+Helper function for executing `x` with a fresh `newEqs` and without modifying
+the goal state.
+ -/
+private def withoutModifyingState (x : GoalM α) : GoalM α := do
+  let saved ← get
+  modify fun goal => { goal with newEqs := {} }
+  try
+    x
+  finally
+    set saved
+
+/--
+If `e` has not been internalized yet, simplify it, and internalize the result.
+-/
+private def simpAndInternalize (e : Expr) (gen : Nat := 0) : GoalM Simp.Result := do
+  if (← alreadyInternalized e) then
+    return { expr := e }
+  else
+    let r ← simp e
+    internalize r.expr gen
+    return r
+
+/--
+Try to construct a proof that `lhs = rhs` using the information in the
+goal state. If `lhs` and `rhs` have not been internalized, this function
+will internalize then, process propagated equalities, and then check
+whether they are in the same equivalence class or not.
+The goal state is not modified by this function.
+This function mainly relies on congruence closure, and constraint
+propagation. It will not perform case analysis.
+-/
+def proveEq? (lhs rhs : Expr) : GoalM (Option Expr) := do
+  if (← alreadyInternalized lhs <&&> alreadyInternalized rhs) then
+    if (← isEqv lhs rhs) then
+      return some (← mkEqProof lhs rhs)
+    else
+      return none
+  else withoutModifyingState do
+    let lhs ← simpAndInternalize lhs
+    let rhs ← simpAndInternalize rhs
+    processNewEqs
+    unless (← isEqv lhs.expr rhs.expr) do return none
+    unless (← hasSameType lhs.expr rhs.expr) do return none
+    let h ← mkEqProof lhs.expr rhs.expr
+    let h ← match lhs.proof?, rhs.proof? with
+      | none,    none    => pure h
+      | none,    some h₂ => mkEqTrans h (← mkEqSymm h₂)
+      | some h₁, none    => mkEqTrans h₁ h
+      | some h₁, some h₂ => mkEqTrans (← mkEqTrans h₁ h) (← mkEqSymm h₂)
+    return some h
+
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/EMatch.lean

@@ -8,6 +8,7 @@ import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Intro
 import Lean.Meta.Tactic.Grind.DoNotSimp
 import Lean.Meta.Tactic.Grind.MatchCond
+import Lean.Meta.Tactic.Grind.Core
 
 namespace Lean.Meta.Grind
 namespace EMatch
@@ -270,13 +271,20 @@ private partial def instantiateTheorem (c : Choice) : M Unit := withDefault do w
     return ()
   -- Apply assignment
   for h : i in [:mvars.size] do
-    let v := c.assignment[numParams - i - 1]!
+    let mut v := c.assignment[numParams - i - 1]!
     unless isSameExpr v unassigned do
       let mvarId := mvars[i].mvarId!
       let mvarIdType ← mvarId.getType
       let vType ← inferType v
-      unless (← isDefEq mvarIdType vType <&&> mvarId.checkedAssign v) do
+      let report : M Unit := do
         reportIssue m!"type error constructing proof for {← thm.origin.pp}\nwhen assigning metavariable {mvars[i]} with {indentExpr v}\n{← mkHasTypeButIsExpectedMsg vType mvarIdType}"
+      unless (← isDefEq mvarIdType vType) do
+        let some heq ← proveEq? vType mvarIdType
+          | report
+            return ()
+        v ← mkAppM ``cast #[heq, v]
+      unless (← mvarId.checkedAssign v) do
+        report
         return ()
   -- Synthesize instances
   for mvar in mvars, bi in bis do

src/Lean/Meta/Tactic/Grind/Internalize.lean

@@ -133,6 +133,7 @@ private partial def internalizeMatchCond (matchCond : Expr) (generation : Nat) :
   lhss.forM fun lhs => do internalize lhs generation; registerParent matchCond lhs
   propagateUp matchCond
   internalize e' generation
+  trace[grind.debug.matchCond.lambda] "(idx := {(← getENode e'.getAppFn).idx}) {e'.getAppFn}"
   pushEq matchCond e' (← mkEqRefl matchCond)
 
 partial def activateTheorem (thm : EMatchTheorem) (generation : Nat) : GoalM Unit := do