Dot notation and `CoeFun`

Description

This is a question that came up in mathport, resulting from an incompatibility between how dot notation is elaborated in Leans 3 and 4.

In Lean 3, we can (mis?)use dot notation in cases where the applied constant is in the right namespace but does not have an argument of the right type. In the example below

structure equiv (α : Sort*) (β : Sort*) :=
(to_fun    : α → β)
(inv_fun   : β → α)

infix ` ≃ `:25 := equiv

instance {α : Sort*} {β : Sort*} : has_coe_to_fun (α ≃ β) (λ _, α → β) :=
  ⟨equiv.to_fun⟩

def foo := nat
def bar := nat
def foo.to_bar : foo ≃ bar := ⟨id, id⟩

example (f : foo) : f.to_bar = f.to_bar := rfl

the term f.to_bar is first transformed to foo.to_bar f, at which point the standard function application elaborator kicks in and finds a has_coe_to_fun instance. The current community edition implementation is described in the last paragraph here. In practice, this is used for applying bundled morphisms (with equivalences being a special case) as if they were functions, for example enat.to_nat.

In Lean 4, this does not work.

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

infixl:25 " ≃ " => Equiv

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

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

/- invalid field notation, function 'Foo.to_Bar' does not have argument with type (Foo ...)
that can be used, it must be explicit or implicit with an unique name -/
example (f : Foo) : f.to_Bar = f.to_Bar := sorry

From the Zulip discussion it seems that this is useful to have but it is not immediately clear whether Lean 4 should definitely have this feature, so this is a request for feedback.

leanprover / lean4

Dot notation and `CoeFun` #1910

Description