`CoeFun` and implicit arguments

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

Function applications going through CoeFun do not respect the implicitness of the parameters declared in the instance head, rather they take the implicitness information from the instance implementation.

Context

Steps to Reproduce

structure Foo where app : ∀α, (x : α) → α

def foo := Foo.mk fun _ => id

instance : CoeFun Foo fun _ => ∀{α}, α → α where
  coe := Foo.app

/-- info: CoeFun.coe foo Nat : Type -/
#guard_msgs in
#check CoeFun.coe foo Nat
/-- info: foo.app Nat : Nat → Nat -/
#guard_msgs in
#check foo Nat

Expected behavior:

• Both cases desugar as Foo.app foo (α:=Type) (x:=Nat), and infer the type Type

Actual behavior:

• The first one infers the correct type, but the second desugars as Foo.app foo (α:=Nat) and infers the type Nat → Nat.

Versions

4.13.0

Additional Information

The problem can be reversed by making the structure field have implicit ∀{α} and the instance head have the explicit ∀α.
https://github.com/leanprover/lean4/issues/1891 seems relevant.

Impact

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

Start by running the self-contained reproducer against Lean 4.13.0 and a current nightly, then compare the elaboration behavior with issue 1891. Trace the CoeFun application elaboration path; done means implicitness from the instance head is respected in both the direct coercion and function-application forms, including the reversed case.