section variables are ignored during type-checking of recursive function

Prerequisites

• 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

When the name of a section variable is encountered in a non-theorem declaration, it is added as a parameter.

(https://lean-lang.org/doc/reference/latest/Namespaces-and-Sections/#section-variables)

This principle was not followed by the elaborator until the function definition is finished. Before that, the section variable was assumed to be useless. This obvious make recursive call impossible.

Context

N/A

Steps to Reproduce

Expected behavior: f1 and f2 should elaborate to the same function

Versions

Lean LSP: 4.30
OS: Windows 11

Additional Information

N/A

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 minimal Lean example from the issue and compare how f1 and f2 elaborate. Read the section-variable documentation and the elaborator's handling of recursive function definitions; the fix is complete when section variables are treated as parameters early enough for the recursive call and f1 and f2 elaborate identically.