dot ident notation cannot refer to recursive call

[cppio]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• 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

The dot ident notation currently cannot be used to refer to the function being recursively defined, and attempting to do so results in a confusing error message.

Steps to Reproduce

def Nat.id : Nat → Nat
  | .zero => .zero
  | .succ n => .succ (.id n)

Expected behavior: .id n is equivalent to Nat.id n and n.id, which both succeed with no errors.

Actual behavior: The following error:

invalid dotted identifier notation, unknown identifier `Nat.id` from expected type
  Nat

Versions

Lean 4.16.0-nightly-2025-01-10
Appears in Lean 4.0.0-m5

Impact

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

[cppio]

Currently when the identifier is not found in the environment, the expected type is unfolded and the identifier is then searched for in the namespace of the unfolded type. This means that fixing this bug (as done in #6602) can break code that relies on the fallback occurring for a dot ident with the same name as the current function.
This can occur when defining an alias to another type, and defining a function that just applies the function of the same name from the original type. For example, code such as the following will be broken by the change:

opaque f : Nat → Nat
def MyEq (x y : Nat) := f x = f y -- an example type which unfolds to Eq
def MyEq.symm : MyEq x y → MyEq y x := .symm

In MyEq.symm, .symm currently cannot find MyEq.symm, so MyEq is unfolded and .symm resolves to Eq.symm. After fixing this bug, .symm will resolve to MyEq.symm, causing a termination error.

The fix for this pattern is simple: mark the definition as nonrec. This is consistent with the postfix dot notation:

def MyEq.symm (h : MyEq x y) : MyEq y x := h.symm -- fail to show termination
nonrec def MyEq.symm (h : MyEq x y) : MyEq y x := h.symm -- works

This pattern of delegating to the same function name in the original type occurs in batteries and mathlib, for example in https://github.com/leanprover-community/batteries/blob/66225aab4f6bd1687053b03916105f7cab140507/Batteries/Data/UnionFind/Lemmas.lean#L100-L101. All of the breakage in batteries and mathlib can be fixed by adding nonrec to the appropriate definitions.

[nomeata]

Thanks for the analysis, in particular that it needs the unfold-and-look-again ambiguity.

Especially since postfix dot notation works already as you suggest, I agree with your analysis and fix, and that the broken code was only working accidentally.

Thanks for that!