Grind error and panic at `mkEqProofImpl`

Stream: lean4

[Snir Broshi]

inductive Foo (α : Type) (x : α) where
| c1 : Foo α x
| c2 : Foo α x

def Foo.mk (n : Nat) : Foo (Fin (n + 1)) 0 :=
  match n with
  | .zero => .c1
  | .succ _ => .c1

def Foo.num {α : Type} {x : α} (f : Foo α x) : Nat :=
  0

/--
error: <GoalM action default value>
---
info: PANIC at Lean.Meta.Grind.mkEqProofImpl Lean.Meta.Tactic.Grind.Proof:336:2: assertion violation: ( __do_lift._@.Lean.Meta.Tactic.Grind.Proof.911332591._hygCtx._hyg.11.0 )
  ⏎
backtrace:
-/
#guard_msgs in
theorem foo (n : Nat) : (Foo.mk n).num = 0 := by
  induction n with
  | zero => rfl
  | succ n ih => grind [Foo.mk]

(Foo used to be docs#SimpleGraph.Walk and Foo.num used to be docs#SimpleGraph.Walk.support)

[Snir Broshi]

(btw do grind errors have a specific thread I should've posted to? or perhaps I should've created an issue directly?)

[Snir Broshi]

the assertion in Lean/Meta/Tactic/Grind/Proof.lean

[Kim Morrison]

Reporting here is fine. I'll try to investigate in the next few days. Opening an issue directly is always okay (and very helpful if you don't get a quick response here!)

[Kim Morrison]

https://github.com/leanprover/lean4/issues/12140

Using lean-bisect, I identified this as a regression introduced by https://github.com/leanprover/lean4/pull/11658 (between nightly-2025-12-13 and nightly-2025-12-14).