bug with pp.implicit and structure fields

[semorrison]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

The following example shows the pretty-printer generating invalid code, when a structure field has implicit arguments

Steps to Reproduce

set_option pp.implicit true

structure C := ( d : Π { X : Type }, list X → list X )

def P(c : C):= c.d [0]

#print P

Actual behavior:

#print P shows:

def P : C → list ℕ :=
λ (c : C), c.d ℕ [0]

however c.d ℕ [0] is invalid notation, because it's missing an @.

Expected behavior:

#print P should show

def P : C → list ℕ :=
λ (c : C), @C.d c ℕ [0]

Versions

Lean (version 3.3.1, commit 6da6c14, RELEASE)