Conflict with deeply nested rec function declarations

[JaafarTanoukhi]

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 :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

[leodemoura]

This behavior is by design. Lean creates a global name for all nested recursive functions. The name is based on the outer function. The global names are important when writing proofs. Min fix: improve error message.

Workaround: add rec to the auxiliary let declarations. Example:

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

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

#check outerFunction.innerFunction.helper
#check outerFunction.otherInnerFunction.helper

Remark: improved error message may suggest this solution. Remark: It is not viable to take every single let-declaration into account when generating the auxiliary global name. Reason: too long names.

Another possible fix: Lean adds the suffix _<idx> for the user. In the example above, the second helper would be named helper_2. Cons: if there are many nested functions with the same name, the user would have to "guess" the correspondence between helper_<idx> global functions when writing proofs. It seems better for the user to write the let rec using different names. Example:

partial def  outerFunction (x : Nat) : Nat :=
let innerFunction (x : Nat) :=
  let rec helper_1 (x : Nat) : Nat :=
    helper_1 x
  helper_1 x

let otherInnerFunction (x : Nat) :=
  let rec helper_2 (x : Nat) : Nat :=
    x
  helper_2 x
innerFunction x + otherInnerFunction x

#check outerFunction.helper_1
#check outerFunction.helper_2

Remark: improved error message may also suggest this solution.