Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

(Could be a duplicate of #4548 or any of the other "unknown free variable" issues, but I'm a beginner at Lean so I can't verify.)

This MWE causes the Lean compiler to throw an error, unknown free variable '_fvar.639', at the definition of goList:

  inductive Tree : Type where
    | leaf
    | node (p : Nat) (brs : List Tree)

  def Tree.substNats (M: Tree) (σ : Nat → Nat) : Tree :=
    let rec go M : Tree := match M with
      | .leaf => leaf
      | .node p brs =>
        let rec goList: List Tree → List Tree   -- unknown free variable '_fvar.639'
          | [] => []
          | M :: Ms => go M :: goList Ms
        .node (σ p) (goList brs)
    go M

Context

Prior discussion on Zulip: https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Termination.20check.20bug.3F.20unknown.20free.20variable.20'_fvar.2E35433'

Versions

• 4.13.0 on MacOS 15.3
• 4.16.0-nightly-2025-02-03 on the Lean Live Editor