Dot notation and abbreviation change

Stream: lean4

[Bhavik Mehta]

Is the difference in pretty printing for dot notation on abbreviations a known problem? MWE:

variable {V V' K : Type}

def Foo (V V' K : Type) := V → V' → K

abbrev Bar (V K : Type) := Foo V V K

def Bar.val [Inhabited V] (C : Bar V K) : K := C default default

example [Inhabited V] {C : Bar V K} : C.val = C.val := sorry

The goal here looks like Bar.val C = Bar.val C, whereas in Lean 3 it looks like C.val = C.val

[Eric Wieser]

I think the abbrev is a distraction here, even using Foo alone results in no dot notation

[Bhavik Mehta]

Oh true, I didn't realise that!

[Bhavik Mehta]

variable {V K : Type}
def Foo (V K : Type) := V → K
def Foo.val [Inhabited V] (C : Foo V K) : K := C default
example [Inhabited V] {C : Foo V K} : C.val = C.val := sorry

So this version also doesn't use dot notation in the goal, whereas the Lean 3 version does

[Eric Rodriguez]

I think there's a delaborator for this? But it should be automatic imo

[Yaël Dillies]

You now need to tag definitions which you want to be displayed with dot notation using @[pp_dot] rather than the ones you don't want using @[pp_no_dot].

[Yaël Dillies]

Whether that's the correct default is arguable (spoiler: it's not)