RFC: pretty printing dot notation with CoeFun

[edegeltje]

Description

In the wake of #1910 , it has become possible to use dot notation with namespaced non-function declarations.
However, pretty printing doesn't show these terms as using dot notation.

adapting the example given for that issue:

structure Equiv (α β : Sort _) where
  toFun : α → β
  invFun : β → α

infixl:25 " ≃ " => Equiv

instance: CoeFun (α ≃ β) fun _ => α → β where
  coe := Equiv.toFun

def Foo := Nat
def Bar := Nat
def Foo.toBar : Foo ≃ Bar := ⟨id, id⟩

variable (f : Foo)

#check f.toBar -- Foo.toBar f : Bar

ideally, the latter #check command should display f.toBar by default.

Just as dot notation improves the experience of writing and reading code, pretty printing this new instance of dot notation will allow users to more clearly see the structure of code by hiding redundant information, i.e. the namespace of the declaration.

Community Feedback

This initiative started because all porting notes referring to #1910 in mathlib came under review, and some of them mentioned that certain uses of the pp_nodot attribute were not useful yet because the dot notation wasn't available for the declarations the porting notes were referring to. See also this discussion on Zulip.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.