fix: allow dot idents to resolve to local names

[cppio]

This PR allows the dot ident notation to resolve to the current definition, or to any of the other definitions in the same mutual block. Existing code that uses dot ident notation may need to have nonrec added if the ident has the same name as the definition.

Closes #6601

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-6602 build failed against this PR. (2025-01-10 20:49:37) View Log
• 💥 Mathlib branch lean-pr-testing-6602 build failed against this PR. (2025-01-10 22:13:14) View Log
• 💥 Mathlib branch lean-pr-testing-6602 build failed against this PR. (2025-01-11 03:35:40) View Log

[nomeata]

(nevermind, looks like there is more work to be done)

[cppio]

This causes breakage in Batteries and Mathlib due to code such as https://github.com/leanprover-community/batteries/blob/66225aab4f6bd1687053b03916105f7cab140507/Batteries/Data/UnionFind/Lemmas.lean#L100-L101 which rely on the dot ident not resolving to the current definition. This can easily be fixed by using nonrec, which the linked code already does for rfl.

[nomeata]

Thanks for the investigation. Can you add this analysis to #6601, ideally with a self-contained example of the idiom that this fix would be breaking (so that we can use it for the test suite)? Under which circumstaces can .foo refer to both an existing constant and the current definitions?

Also, if possible, contrast the behavior with the a.foo notation for A.foo (a : A); ideally .foo and a.foo resolution behave the same with regard to recursive definitions.

(invalidated by breakage)

[cppio]

changelog-language

[nomeata]

Please ping me here once mathlib is green (this likely requires pinning the mathlib adaption branch to the fixed batteries branch that you created, but should be possible)