Improved error message for accidentally recursive def

Stream: lean4

[Patrick Massot]

In #general > Mathematics in Lean @ 💬, a new user got confused by a version of:

theorem bar : 0 = 0 := rfl

namespace foo

theorem bar : 0 = 0 := bar

end foo

Where the bar in the proof of foo.bar was meant to refer to _root_.bar, but Lean thinks it’s a recursive call to

fail to show termination for
  foo.bar
with errors
failed to infer structural recursion:
no parameters suitable for structural recursion

well-founded recursion cannot be used, 'foo.bar' does not take any (non-fixed) arguments

Could we add to the error message something like: “if you didn’t intend this to be a recursive definition then write nonrec theorem instead of theorem or double check you don’t have two declarations with the same name in different currently accessible namespaces”? Lean could even check if there is indeed a name clash in currently opened namespaces.

[Kenny Lau]

I think it's pretty clear from the error message what the issue is (it says foo.bar!) though...

[Damiano Testa]

I still think that mentioning nonrec in the error message is a clear improvement.

[Joachim Breitner]

I'm a bit on the fence of including text in error messages that is not specific to the concrete error instance at hand. If it's just pointing out a feature that may be useful then it's useful the first and second time you see it, and from then on its just noise and a waste of precious screen estate.

The new “error explanation” feature (a manual section dedicated to and linked from a specific error message) is a better place to put such additional information, I think.

[Joachim Breitner]

What would be a useful feature is to include a Note in the error message only if the recursive calls would resolve to something else under nonrec, i.e. if there is plausible evidence that the user did not mean to write a recursive function. Then the extra note carries actual additional value, even to non-beginners.

[Joachim Breitner]

(ah, as Patrick said in the last sentence)

[Joachim Breitner]

Issue welcome.