Dot notation and iterated namespaces

Stream: lean4

[Michael Stoll]

Is the following a bug?

def A.B.C (n : Nat) : Nat := 37 + n

def A (α : Type) : Type := α → Nat

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

(I noticed this when trying to write I.Quotient.mk with I : Ideal R, which gives an error even though Ideal.Quotient.mk exists.)

[Matt Diamond]

I think this would be a better example, since dot notation doesn't work unless the function has an argument with the root type:

def A (α : Type) : Type := α → Nat

def A.B.C (_ : A Nat) (n : Nat) : Nat := 37 + n

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

My understanding of dot notation is that A.B.C is interpreted as (A.B).C and not A.(B.C), in which case your example is not a bug, but I don't know if that's the actual expected behavior.

[Michael Stoll]

Matt Diamond said:

I think this would be a better example, since dot notation doesn't work unless the function has an argument with the root type:

True (I may have had a bit too much prosecco yesterday night :smile:). But your example (and docs#Ideal.Quotient.mk as well) shows that there really is an issue.

[Michael Stoll]

Unfortunately, x.(B.C) doesn't parse...

[Michael Stoll]

Is there any possible ambiguity in (x.B).C versus x.(B.C)? Perhaps the parser could try the latter when the former does not make sense?

[Junyan Xu]

In Lean 3 it's possible to write ^.quotient.mk. Would be nice if the same works in Lean 4. Maybe open an issue (if there isn't already one)?

[Michael Stoll]

lean4#6491