Nested dot notation x.B.C does not work

[MichaelStollBayreuth]

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

If there is a declaration A.B.C taking an argument of type A and x : A, then x.B.C results in an error.

Context

See this thread on Zulip.

This comes up in the context of Mathlib, where, e.g.,

def Ideal.Quotient.mk {R : Type u} [CommRing R] (I : Ideal R) : R →+* R ⧸ I

and one would like to write I.Quotient.mk where I : Ideal R.

Steps to Reproduce

def A : Type := Nat

def A.B.C (a : A) : Nat := a

/- invalid field 'B', the environment does not contain 'A.B' -/
example (x : A) : x.B.C = x := rfl

Expected behavior:

x.B.C is interpreted as A.B.C x.

Actual behavior:

An error results.

Versions

4.15.0-rc1 (on (live.lean-lang.org)[https://live.lean-lang.org/#codez=CYUwZgBAghBcEBUCeAHEcC8EByBDALgFCGiRQB0AQuQMIQAUuc0AlM3vphLsQPQC0EAJYA7AG64ANkOAQwQkJNkBySsoA0EfAAt0IcUIBOAexEBbfZ2DGQAZwgjjnAMan8uURGUU1Efr0IQAA9cMxRJdHog5ig2eCCqWggsaNgsQzBJQiA]

Additional Information

May be related to lean4#6400.

In Lean 3, it was possible to write x^.B.C to achieve the desired behavior. This does no longer work (and neither does x.(B.C)). Could x.B.C elaborate as A.B.C x when A.B x does not make sense?

Impact

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

[nomeata]

Thanks for your input. I'd say this isn't a bug (as the behavior is intended by whoever built it), and more a proposal to change the design.

[kmill]

Given that this is an RFC, I think there needs to be a strong argument why renaming the function to Ideal.quotientMk (or Ideal.quotientMap?) is insufficient.

Algorithmically, the full resolution problem suggested in this RFC is O(C(n)) (where C(n) is the Catalan numbers), which is O(4^n / n^{3/2}). If we allowed x.B.C for A.B.C x, we would need to support the full resolution algorithm because users would be surprised if either of y.D.B.C and x.B.C.E were not resolvable as (y.D).B.C and (x.B.C).E, right?

When there is ambiguity in dot notation resolution, what takes precedence over what? It's easy to come up with examples where both interpretations x.(B.C) and (x.B).C would resolve to something.

In Lean 3, it was possible to write x^.B.C to achieve the desired behavior.

IIRC, the ^. notation was the original notation in Lean 3, which was extended at some point to have the current current behavior. Lean 4 decided to only take the current notation.

Perhaps x.(B.C) would be reasonable modern notation, since it chains with things such as x.(B.C).(D.E).F, and it also would support using swift notation like .(B.C).

[MichaelStollBayreuth]

Thanks for your input. I'd say this isn't a bug (as the behavior is intended by whoever built it), and more a proposal to change the design.

OK. I find the binary choice between "bug" and "RFC" sometimes a bit inconvenient...

[MichaelStollBayreuth]

Perhaps x.(B.C) would be reasonable modern notation, since it chains with things such as x.(B.C).(D.E).F, and it also would support using swift notation like .(B.C).

That looks reasonable to me.

[kmill]

Never mind, I forgot that .(x) is Lean.Parser.Term.inaccessible, so that's not a good choice.

[nomeata]

We discussed this proposal, and decided that although there are use-cases where this would be nice to have, but given the increased complexity (e.g. more ambiguities) we decided to reject this proposal.