free vars of `termination_by` in local where/letrec not considered when floating defs

It seems that mentioning a parameter of the enclosing function (here j) in the termination_by clause of an inner function does not cause that variable to be in scope. The termination_by can access those parameters that the body of the inner function happens to mention:

-- works
def foo (xs : Array Nat) : Nat := 
  go 0
where
  go i := if i < xs.size then go (i + 1) else 0
  termination_by xs.size - i


/-- error: unknown identifier 'j' -/
#guard_msgs in
def bar (xs : Array Nat) (j : Nat) : Nat := 
  go 0
where
  go i := if i < xs.size then go (i + 1) else 0
  termination_by xs.size - i - j


-- works
def baz (xs : Array Nat) (j : Nat) : Nat := 
  go 0
where
  go i := if i < xs.size then go (i + 1 + j) else 0
  termination_by xs.size - i + j

(Practical use-case can arise when proof arguments of the outer functions are needed only for the termination of the inner one.)

Versions

Lean 4.20.0-nightly-2025-04-29

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by reproducing the foo, bar, and baz examples from the issue, then inspect the implementation handling local where/letrec definitions when floating them. Done means the bar example can reference the enclosing parameter j from its termination_by clause, with coverage for the reported behavior.