Printing of notation with @

Description

Printing of notation doesn't seem to work when the declaration used @.

Steps to Reproduce

-- uncomment one

notation A `⁻` := set.compl A -- prints & parses correctly
-- notation A `⁻` := @set.compl _ A -- parses correctly, doesn't print
-- notation A `⁻` := @set.compl A -- parses incorrectly (as expected), but still prints!

example (X : Type) (A : set X) : A ∪ A.compl = set.univ := by {  }
example (X : Type) (A : set X) : A ∪ (A⁻) = set.univ := by {  }

The original question was to get the following notation print correctly.

notation X `\` A := @has_neg.neg (set X) _ A
example (X : Type) (A : set X) : A ∪ (X \ A) = set.univ := by {  }

This bug probably applies, but maybe there is also something else going on because \ is overloaded. (in this example the goal is printed as A ∪ (λ (x_1 : Type), has_neg.neg) X A = set.univ, but if I replace \ by \\ everywhere, the goal is printed as A ∪ -A = set.univ)

Additional Information

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Notation.20with.20implicit.20arguments.20.3F

Run the provided Lean notation examples, comparing declarations that use set.compl directly with those using @set.compl and the overloaded \ notation. Trace the notation printer behavior for implicit arguments and confirm that the affected expressions print using their declared notation without changing parsing behavior.