fix: panic during the processing of generalized patterns in grind

This PR fixes a panic that occurred during the processing of
generalized E-matching patterns in `grind`.

Closes #10983

Author: leodemoura

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

@@ -528,16 +528,34 @@ private def assignGeneralizedPatternProof (mvarId : MVarId) (eqProof : Expr) (or
     reportEMatchIssue! "invalid generalized pattern at `{origin.pp}`\nfailed to assign {mkMVar mvarId}\nwith{indentExpr eqProof}"
     failure
 
+/--
+At `processDelayed`, `lhs` is extracted using `instantiateMVars`. We know it is structurally equal to a term in `assignment`, but
+it is not necessarily pointer equal. This can happen when the type of `lhs` depends on previous parameters, and we have a
+metavariable application.
+If the `lhs` has already been internalized, nothing needs to be done. Otherwise, we traverse the assignment looking for
+a term that is structurally equal.
+**Note**: If this solution is not robust enough, we should store the original `lhs` when we perform an delayed assignment.
+-/
+private def findOriginalGeneralizedPatternLhs (lhs : Expr) : OptionT (StateT Choice M) Expr := do
+  if (← alreadyInternalized lhs) then return lhs
+  for val in (← get).assignment do
+    if val == lhs then
+      return val
+  reportEMatchIssue! "invalid generalized pattern at `{(← read).thm.origin.pp}`\nwhen processing argument{indentExpr lhs}"
+  failure
+
 /-- Helper function for `applyAssignment. -/
 private def processDelayed (mvars : Array Expr) (i : Nat) (h : i < mvars.size) : OptionT (StateT Choice M) Unit := do
   let thm := (← read).thm
   let mvarId := mvars[i].mvarId!
   let mvarIdType ← instantiateMVars (← mvarId.getType)
   match_expr mvarIdType with
   | Eq α lhs rhs =>
+    let lhs ← findOriginalGeneralizedPatternLhs lhs
     let rhs ← preprocessGeneralizedPatternRHS lhs rhs thm.origin mvarIdType
     assignGeneralizedPatternProof mvarId (← mkEqProof lhs rhs) thm.origin
   | HEq α lhs β rhs =>
+    let lhs ← findOriginalGeneralizedPatternLhs lhs
     let rhs ← preprocessGeneralizedPatternRHS lhs rhs thm.origin mvarIdType
     assignGeneralizedPatternProof mvarId (← mkHEqProof lhs rhs) thm.origin
   | _ =>

tests/lean/run/grind_10983.lean

@@ -0,0 +1,14 @@
+structure Equiv (α : Type _) (β : Type _) where
+  toFun : α → β
+  invFun : β → α
+  left_inv : ∀ x, invFun (toFun x) = x
+
+def sumEquivSigmaBool (α β) : Equiv (α ⊕ β) (Σ b, bif b then β else α) where
+  toFun s := s.elim (fun x => ⟨false, x⟩) fun x => ⟨true, x⟩
+  invFun s :=
+    match s with
+    | ⟨false, a⟩ => .inl a
+    | ⟨true, b⟩ => .inr b
+  left_inv := fun s => by
+    fail_if_success grind
+    sorry