v4.18.0 regression on well-founded recursion

Stream: general

[pandaman]

I'm updating lean-regex from v4.17.0 to v4.18.0, but Lean started to fail typecheck a function with a well-founded recursion. Here is a minimized example

#eval Lean.versionString

-- REPRO: SparseSet needs to take a parameter to reproduce.
structure SparseSet (n : Nat) where

def SparseSet.insert {n} (set : SparseSet n) (v : Fin n) : SparseSet n := sorry

inductive Node where
  | epsilon (next : Nat)

structure NFA where
  nodes : Array Node

def NFA.get (nfa : NFA) (i : Nat) (h : i < nfa.nodes.size) : Node :=
  nfa.nodes[i]

structure Strategy' where
  T : Type

def εClosure (σ : Strategy') (nfa : NFA) (states : SparseSet nfa.nodes.size) (stack : List (Fin nfa.nodes.size)) :
  -- REPRO: using `σ.T` is necessary to reproduce.
  Option σ.T :=
  match stack with
  | [] => .none
  | state :: stack' =>
    -- REPRO: removing this `if` fixes the error.
    if true then
      εClosure σ nfa states stack'
    else
      -- REPRO: this insert is necessary to reproduce.
      let states' := states.insert state
      match nfa.get state state.isLt with
      | .epsilon state' =>
        -- REPRO: this line is also necessary to reproduce.
        have isLt : state' < nfa.nodes.size := sorry
        sorry
-- REPRO: using well-founded recursion is necessary to reproduce.
-- NOTE: the original code uses well-founded recursion to take visited states (`states`) into account.
termination_by /-structural-/ stack

The εClosure definition emits an error like this:

application type mismatch
  let_congr (Eq.refl ((wfParam states).insert (wfParam state))) fun states' =>
    congrArg
      (εClosure.match_1 (fun x => Option (wfParam σ.T))
        ((wfParam nfa).get (wfParam ↑state) (id (Eq.refl (wfParam ↑state)) ▸ (wfParam state).isLt)))
      (funext fun state' => letFun_body_congr sorry fun isLt => Eq.refl sorry)
argument
  fun states' =>
    congrArg
      (εClosure.match_1 (fun x => Option (wfParam σ.T))
        ((wfParam nfa).get (wfParam ↑state) (id (Eq.refl (wfParam ↑state)) ▸ (wfParam state).isLt)))
      (funext fun state' => letFun_body_congr sorry fun isLt => Eq.refl sorry)
has type
  SparseSet (wfParam nfa).nodes.size →
    (match (wfParam nfa).get (wfParam ↑state) ⋯ with
      | Node.epsilon x => sorry) =
      match (wfParam nfa).get (wfParam ↑state) ⋯ with
      | Node.epsilon x => sorry : Prop
but is expected to have type
  ∀ (x : SparseSet (wfParam nfa.nodes).size), ?b x = ?b' x : Prop

[pandaman]

@Joachim Breitner As well-founded recursion is necessary to reproduce and I see wfParam in the errors, this issue might be introduced by auto-attach https://github.com/leanprover/lean4/issues/5471. It would be great if you could take a look!

[pandaman]

Filed https://github.com/leanprover/lean4/issues/7826