fix: correctly pretty-print @Eq

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -161,12 +161,12 @@ where
           k (xs ++ ys) b
 
 @[builtinDelab app]
-def delabAppExplicit : Delab := whenPPOption getPPExplicit do
+def delabAppExplicit : Delab := do
   let paramKinds ← getParamKinds
   let (fnStx, _, argStxs) ← withAppFnArgs
     (do
       let stx ← delabAppFn
-      let needsExplicit := paramKinds.any (fun param => !param.isRegularExplicit) && stx.getKind != `Lean.Parser.Term.explicit
+      let needsExplicit := stx.getKind != ``Lean.Parser.Term.explicit
       let stx ← if needsExplicit then `(@$stx) else pure stx
       pure (stx, paramKinds.toList, #[]))
     (fun ⟨fnStx, paramKinds, argStxs⟩ => do
@@ -252,6 +252,14 @@ def delabAppImplicit : Delab := do
   if ← getPPOption getPPExplicit then
     if paramKinds.any (fun param => !param.isRegularExplicit) then failure
 
+  -- If the application has an implicit function type, fall back to delabAppExplicit.
+  -- This is e.g. necessary for `@Eq`.
+  let isImplicitApp ← try
+      let ty ← whnf (← inferType (← getExpr))
+      ty.isForall && (ty.binderInfo == BinderInfo.implicit || ty.binderInfo == BinderInfo.instImplicit)
+    catch _ => false
+  if isImplicitApp then failure
+
   let (fnStx, _, argStxs) ← withAppFnArgs
     (return (← delabAppFn, paramKinds.toList, #[]))
     (fun (fnStx, paramKinds, argStxs) => do

tests/lean/366.lean.expected.out

@@ -2,7 +2,7 @@
   [Meta.synthInstance] 
     [Meta.synthInstance] main goal Inhabited Nat
     [Meta.synthInstance.newSubgoal] Inhabited Nat
-    [Meta.synthInstance.globalInstances] Inhabited Nat, [instInhabited, instInhabitedNat]
+    [Meta.synthInstance.globalInstances] Inhabited Nat, [@instInhabited, instInhabitedNat]
     [Meta.synthInstance.generate] instance instInhabitedNat
     [Meta.synthInstance.tryResolve] 
       [Meta.synthInstance.tryResolve] Inhabited Nat =?= Inhabited Nat

tests/lean/439.lean

@@ -10,9 +10,9 @@ class Bar.{w} (P : Sort u) :=
 
 variable {P : Sort u} (B : Bar P)
 variable (fn : Fn ((p : P) -> B.fn p) ({p : P} -> B.fn p))
-#check coeFun fn -- Result is as expected (implicit)
+#check (@fn : {p : P} → Bar.fn p) -- Result is as expected (implicit)
 /-
-  fn : {p : P} → Bar.fn p
+  fn.imp : {p : P} → Bar.fn p
 -/
 
 variable (p : P)

tests/lean/439.lean.expected.out

@@ -1,4 +1,4 @@
-fn : {p : P} → Bar.fn p
+fn.imp : {p : P} → Bar.fn p
 439.lean:20:7-20:12: error: function expected at
   Fn.imp fn
 term has type

tests/lean/PPRoundtrip.lean

@@ -39,6 +39,10 @@ set_option format.width 20
 -- #eval checkM `(Type _)
 -- #eval checkM `(Type (_ + 2))
 
+#eval checkM `(@max Nat)
+#eval checkM `(@HEq Nat 1)
+#eval checkM `(@List.nil)
+
 #eval checkM `(Nat)
 #eval checkM `(List Nat)
 #eval checkM `(id Nat)

tests/lean/PPRoundtrip.lean.expected.out

@@ -2,6 +2,9 @@ Prop
 Type
 Type
 Type 1
+@max Nat
+@HEq Nat 1
+@List.nil
 Nat
 List Nat
 id Nat

tests/lean/autoBoundImplicits1.lean.expected.out

@@ -10,6 +10,6 @@ autoBoundImplicits1.lean:24:37-24:38: error: unknown identifier 'β'
 autoBoundImplicits1.lean:24:46-24:47: error: unknown identifier 'β'
 autoBoundImplicits1.lean:24:48-24:49: error: unknown identifier 'n'
 autoBoundImplicits1.lean:25:18-25:23: warning: declaration uses 'sorry'
-f : {α : Type} → {n : Nat} → Vec α n → Vec α n
+@f : {α : Type} → {n : Nat} → Vec α n → Vec α n
 f mkVec : Vec ?m 0
 f mkVec : Vec Nat 0

tests/lean/diamond2.lean.expected.out

@@ -1,5 +1,5 @@
-Foo1.mk : {α : Type} → Bar (α → α) → (β : Type) → (α → β) → Foo1 α
-Foo2.mk : {α : Type} → Bar (α → α) → (β : Type) → (α → β) → α → α → Foo2 α
+@Foo1.mk : {α : Type} → Bar (α → α) → (β : Type) → (α → β) → Foo1 α
+@Foo2.mk : {α : Type} → Bar (α → α) → (β : Type) → (α → β) → α → α → Foo2 α
 def Foo2.toBar : {α : Type} → Foo2 α → Bar (α → α) :=
 fun α self => self.1
 def Foo2.toBoo2 : {α : Type} → Foo2 α → Boo2 α :=

tests/lean/diamond5.lean.expected.out

@@ -1 +1 @@
-D.toC_1 : {α : Type} → [self : D α] → C α
+@D.toC_1 : {α : Type} → [self : D α] → C α

tests/lean/diamond7.lean.expected.out

@@ -27,7 +27,7 @@ fun (α : Type u) [self : CommMonoid.{u} α] =>
 def CommGroup.toCommMonoid.{u} : {α : Type u} → [self : CommGroup.{u} α] → CommMonoid.{u} α :=
 fun (α : Type u) [self : CommGroup.{u} α] =>
   @CommMonoid.mk.{u} α (@Group.toMonoid.{u} α (@CommGroup.toGroup.{u} α self)) (@CommGroup.mul_comm.{u} α self)
-Field.mk : {α : Type u_1} → [toDivisionRing : DivisionRing α] → (∀ (a b : α), a * b = b * a) → Field α
+@Field.mk : {α : Type u_1} → [toDivisionRing : DivisionRing α] → (∀ (a b : α), a * b = b * a) → Field α
 def Field.toDivisionRing.{u} : {α : Type u} → [self : Field.{u} α] → DivisionRing.{u} α :=
 fun (α : Type u) [self : Field.{u} α] => self.1
 def Field.toCommRing.{u} : {α : Type u} → [self : Field.{u} α] → CommRing.{u} α :=

tests/lean/elseifDoErrorPos.lean.expected.out

@@ -1,5 +1,5 @@
 elseifDoErrorPos.lean:4:7-7:14: error: application type mismatch
-  ite x
+  @ite ?m x
 argument
   x
 has type

tests/lean/infoTree.lean.expected.out

@@ -26,7 +26,7 @@
       ===>
       Prod.mk✝ x x
         (x, x) : Nat × Nat @ ⟨14, 11⟩†-⟨14, 16⟩ @ Lean.Elab.Term.elabApp
-          Prod.mk : {α β : Type} → α → β → α × β @ ⟨14, 11⟩†-⟨14, 17⟩†
+          @Prod.mk : {α β : Type} → α → β → α × β @ ⟨14, 11⟩†-⟨14, 17⟩†
           x : Nat @ ⟨14, 12⟩-⟨14, 13⟩ @ Lean.Elab.Term.elabIdent
             x : Nat @ ⟨14, 12⟩-⟨14, 13⟩
           x : Nat @ ⟨14, 15⟩-⟨14, 16⟩ @ Lean.Elab.Term.elabIdent
@@ -34,7 +34,7 @@
     y : Nat × Nat @ ⟨14, 6⟩-⟨14, 7⟩
     id y : Nat × Nat @ ⟨15, 2⟩-⟨15, 6⟩ @ Lean.Elab.Term.elabApp
       [.] `id : some Prod.{0 0} Nat Nat @ ⟨15, 2⟩-⟨15, 4⟩
-      id : {α : Type} → α → α @ ⟨15, 2⟩-⟨15, 4⟩
+      @id : {α : Type} → α → α @ ⟨15, 2⟩-⟨15, 4⟩
       y : Nat × Nat @ ⟨15, 5⟩-⟨15, 6⟩ @ Lean.Elab.Term.elabIdent
         y : Nat × Nat @ ⟨15, 5⟩-⟨15, 6⟩
   f : Nat → Nat × Nat @ ⟨13, 4⟩-⟨13, 5⟩
@@ -166,7 +166,7 @@
             ===>
             Prod.mk✝ (x + y) (x - y)
               (x + y, x - y) : Nat × Nat @ ⟨23, 18⟩†-⟨23, 31⟩ @ Lean.Elab.Term.elabApp
-                Prod.mk : {α β : Type} → α → β → α × β @ ⟨23, 18⟩†-⟨23, 32⟩†
+                @Prod.mk : {α β : Type} → α → β → α × β @ ⟨23, 18⟩†-⟨23, 32⟩†
                 x + y : Nat @ ⟨23, 19⟩-⟨23, 24⟩ @ «_aux_Init_Notation___macroRules_term_+__2»
                   Macro expansion
                   x + y
@@ -193,11 +193,11 @@
             let z1 := z + w;
             z + z1 : Nat @ ⟨23, 4⟩†-⟨25, 10⟩ @ Lean.Elab.Term.elabMatch
             x✝ : Nat × Nat @ ⟨23, 4⟩†-⟨25, 10⟩†
-            Prod.mk : {α : Type ?u} → {β : Type ?u} → α → β → α × β @ ⟨23, 4⟩†-⟨25, 10⟩†
+            @Prod.mk : {α : Type ?u} → {β : Type ?u} → α → β → α × β @ ⟨23, 4⟩†-⟨25, 10⟩†
             [.] `z : none @ ⟨23, 9⟩-⟨23, 10⟩
             [.] `w : none @ ⟨23, 12⟩-⟨23, 13⟩
             (z, w) : Nat × Nat @ ⟨23, 4⟩†-⟨23, 13⟩ @ Lean.Elab.Term.elabApp
-              Prod.mk : {α β : Type} → α → β → α × β @ ⟨23, 4⟩†-⟨25, 10⟩†
+              @Prod.mk : {α β : Type} → α → β → α × β @ ⟨23, 4⟩†-⟨25, 10⟩†
               Nat : Type @ ⟨23, 4⟩†-⟨23, 13⟩† @ Lean.Elab.Term.elabHole
               Nat : Type @ ⟨23, 4⟩†-⟨23, 13⟩† @ Lean.Elab.Term.elabHole
               z : Nat @ ⟨23, 9⟩-⟨23, 10⟩ @ Lean.Elab.Term.elabIdent
@@ -264,14 +264,14 @@
   s : Nat × Array (Array Nat) @ ⟨27, 8⟩-⟨27, 9⟩
   Array.push (Array.getOp s.snd 1) s.fst : Array Nat @ ⟨28, 2⟩-⟨28, 17⟩ @ Lean.Elab.Term.elabApp
     s : Nat × Array (Array Nat) @ ⟨28, 2⟩-⟨28, 3⟩
-    Prod.snd : {α β : Type} → α × β → β @ ⟨28, 4⟩-⟨28, 5⟩
-    Array.getOp : {α : Type} → [inst : Inhabited α] → Array α → Nat → α @ ⟨28, 5⟩-⟨28, 6⟩
+    @Prod.snd : {α β : Type} → α × β → β @ ⟨28, 4⟩-⟨28, 5⟩
+    @Array.getOp : {α : Type} → [inst : Inhabited α] → Array α → Nat → α @ ⟨28, 5⟩-⟨28, 6⟩
     1 : Nat @ ⟨28, 6⟩-⟨28, 7⟩ @ Lean.Elab.Term.elabNumLit
     [.] Array.getOp s.snd 1 : Array Nat @ ⟨28, 2⟩-⟨28, 8⟩ : some Array.{0} Nat
-    Array.push : {α : Type} → Array α → α → Array α @ ⟨28, 9⟩-⟨28, 13⟩
+    @Array.push : {α : Type} → Array α → α → Array α @ ⟨28, 9⟩-⟨28, 13⟩
     s.fst : Nat @ ⟨28, 14⟩-⟨28, 17⟩ @ Lean.Elab.Term.elabProj
       s : Nat × Array (Array Nat) @ ⟨28, 14⟩-⟨28, 15⟩
-      Prod.fst : {α β : Type} → α × β → α @ ⟨28, 16⟩-⟨28, 17⟩
+      @Prod.fst : {α β : Type} → α × β → α @ ⟨28, 16⟩-⟨28, 17⟩
   f3 : Nat × Array (Array Nat) → Array Nat @ ⟨27, 4⟩-⟨27, 6⟩
 [Elab.info] command @ ⟨30, 0⟩-⟨31, 20⟩ @ Lean.Elab.Command.elabDeclaration
   B : Type @ ⟨30, 14⟩-⟨30, 15⟩ @ Lean.Elab.Term.elabIdent
@@ -287,7 +287,7 @@
     [.] arg : B @ ⟨31, 2⟩-⟨31, 18⟩ : some Nat
     B.pair : B → A × A @ ⟨31, 6⟩-⟨31, 10⟩
     [.] arg.pair : A × A @ ⟨31, 2⟩-⟨31, 18⟩ : some Nat
-    Prod.fst : {α β : Type} → α × β → α @ ⟨31, 11⟩-⟨31, 14⟩
+    @Prod.fst : {α β : Type} → α × β → α @ ⟨31, 11⟩-⟨31, 14⟩
     [.] arg.pair.fst : A @ ⟨31, 2⟩-⟨31, 18⟩ : some Nat
     A.val : A → Nat → Nat @ ⟨31, 15⟩-⟨31, 18⟩
     0 : Nat @ ⟨31, 19⟩-⟨31, 20⟩ @ Lean.Elab.Term.elabNumLit
@@ -308,16 +308,16 @@
       ===>
       Prod.mk✝ { val := id } { val := id }
         ({ val := id }, { val := id }) : A × A @ ⟨34, 10⟩†-⟨34, 39⟩ @ Lean.Elab.Term.elabApp
-          Prod.mk : {α β : Type} → α → β → α × β @ ⟨34, 10⟩†-⟨34, 40⟩†
+          @Prod.mk : {α β : Type} → α → β → α × β @ ⟨34, 10⟩†-⟨34, 40⟩†
           { val := id } : A @ ⟨34, 11⟩-⟨34, 24⟩ @ Lean.Elab.Term.StructInst.elabStructInst
             id : Nat → Nat @ ⟨34, 20⟩-⟨34, 22⟩ @ Lean.Elab.Term.elabIdent
               [.] `id : some Nat -> Nat @ ⟨34, 20⟩-⟨34, 22⟩
-              id : {α : Type} → α → α @ ⟨34, 20⟩-⟨34, 22⟩
+              @id : {α : Type} → α → α @ ⟨34, 20⟩-⟨34, 22⟩
             val : Nat → Nat := id @ ⟨34, 13⟩-⟨34, 16⟩
           { val := id } : A @ ⟨34, 26⟩-⟨34, 39⟩ @ Lean.Elab.Term.StructInst.elabStructInst
             id : Nat → Nat @ ⟨34, 35⟩-⟨34, 37⟩ @ Lean.Elab.Term.elabIdent
               [.] `id : some Nat -> Nat @ ⟨34, 35⟩-⟨34, 37⟩
-              id : {α : Type} → α → α @ ⟨34, 35⟩-⟨34, 37⟩
+              @id : {α : Type} → α → α @ ⟨34, 35⟩-⟨34, 37⟩
             val : Nat → Nat := id @ ⟨34, 28⟩-⟨34, 31⟩
     pair : A × A := ({ val := id }, { val := id }) @ ⟨34, 2⟩-⟨34, 6⟩
   f5 : Nat → B @ ⟨33, 4⟩-⟨33, 6⟩

tests/lean/interactive/hover.lean.expected.out

@@ -80,7 +80,7 @@ null
 {"range":
  {"start": {"line": 93, "character": 8}, "end": {"line": 93, "character": 10}},
  "contents":
- {"value": "```lean\nid.{0} : ∀ {α : Prop}, α → α\n```", "kind": "markdown"}}
+ {"value": "```lean\n@id.{0} : ∀ {α : Prop}, α → α\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
  "position": {"line": 93, "character": 10}}
 {"range":

tests/lean/openScoped.lean.expected.out

@@ -1,6 +1,6 @@
 openScoped.lean:1:8-1:15: error: unknown identifier 'epsilon'
 openScoped.lean:4:2-4:24: error: failed to synthesize instance
   Decidable (f = g)
-epsilon : {α : Sort u_1} → [h : Nonempty α] → (α → Prop) → α
+@epsilon : {α : Sort u_1} → [h : Nonempty α] → (α → Prop) → α
 openScoped.lean:15:8-15:15: error: unknown identifier 'epsilon'
 openScoped.lean:20:8-20:15: error: unknown identifier 'epsilon'

tests/lean/pplevel.lean.expected.out

@@ -1,6 +1,6 @@
 Type (max u v w) : Type ((max u v w) + 1)
 Type u : Type (u + 1)
-id.{max u v w} : {α : Sort (max u v w)} → α → α
+@id.{max u v w} : {α : Sort (max u v w)} → α → α
 Monad.{max u v, w + 1} : (Type (max u v) → Type (w + 1)) → Type (max ((max u v) + 1) (w + 1))
 Type (max (u + 1) w (v + 2)) : Type ((max (u + 1) w (v + 2)) + 1)
 Type u_1 : Type (u_1 + 1)

tests/lean/sizeof.lean.expected.out

@@ -7,5 +7,5 @@
 308
 310
 11
-InfTree.node.sizeOf_spec : ∀ {α : Type u_1} [inst : SizeOf α] (children : Nat → InfTree α),
+@InfTree.node.sizeOf_spec : ∀ {α : Type u_1} [inst : SizeOf α] (children : Nat → InfTree α),
   sizeOf (InfTree.node children) = 1