Conflict with deeply nested rec function declarations

Description

When declaring nested rec functions within inner functions with the same name, an Error <Outer function name>.<Nested function name> has already been declared is encountered.

Context

I was trying to encapsulate all my code in one definition, which lead to me deciding to nest a helper function under an already nested inner function which is where i encountered the error.

Steps to Reproduce

def  outerFunction (x : Nat) : Nat :=
let innerFunction (x : Nat) :=
  let rec helper (x : Nat) :=
    helper x
  helper x

let otherInnerFunction (x : Nat) :=
  let rec helper (x : Nat) :=
    x
  helper x

funcA x

Expected behavior: Since the first helper is nested under innerFunction and the second helper is nested under otherInnerFunction, i expected this to compile normally.

Actual behavior: In reality this gave an error under the second helper outerFunction.helper has already been declared even though this is nested under otherInnerFunction and not directly under outerFunction

Versions

Lean 4.7.0
Windows 11 Pro, 23H2

Impact

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

Run the provided nested rec reproduction on Lean 4.7.0 and confirm the duplicate-declaration error. Trace how the compiler handles the two nested helper declarations; done means the example compiles without the erroneous outerFunction.helper has already been declared error.