diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index a70d1a7c69..64df8adfb6 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -300,9 +300,9 @@ def delabAppExplicitCore (fieldNotation : Bool) (numArgs : Nat) (delabHead : (in
   let fieldNotation ← pure (fieldNotation && !insertExplicit) <&&> getPPOption getPPFieldNotation
     <&&> not <$> getPPOption getPPAnalysisNoDot
     <&&> withBoundedAppFn numArgs do
-            pure (← getExpr).consumeMData.isConst
-            <&&> not <$> (pure (← getExpr).isMData <&&> getPPOption getPPMData)
-            <&&> not <$> withMDatasOptions (getPPOption getPPAnalysisBlockImplicit <|> getPPOption getPPUniverses)
+            let some (_, us) := (← getExpr).consumeMData.const? | pure false
+            not <$> (pure (← getExpr).isMData <&&> getPPOption getPPMData)
+            <&&> not <$> withMDatasOptions (getPPOption getPPAnalysisBlockImplicit <|> (pure !us.isEmpty <&&> getPPOption getPPUniverses))
   let field? ← if fieldNotation then appFieldNotationCandidate? else pure none
   let (fnStx, _, argStxs) ← withBoundedAppFnArgs numArgs
     (do return (← delabHead insertExplicit, paramKinds.toList, Array.mkEmpty numArgs))
@@ -364,9 +364,9 @@ Assumes `numArgs ≤ paramKinds.size`.
 def delabAppImplicitCore (unexpand : Bool) (numArgs : Nat) (delabHead : Delab) (paramKinds : Array ParamKind) : Delab := do
   let unexpand ← pure unexpand
     <&&> withBoundedAppFn numArgs do
-            pure (← getExpr).consumeMData.isConst
-            <&&> not <$> (pure (← getExpr).isMData <&&> getPPOption getPPMData)
-            <&&> not <$> withMDatasOptions (getPPOption getPPUniverses)
+            let some (_, us) := (← getExpr).consumeMData.const? | pure false
+            not <$> (pure (← getExpr).isMData <&&> getPPOption getPPMData)
+            <&&> (pure us.isEmpty <||> not <$> withMDatasOptions (getPPOption getPPUniverses))
   let field? ←
     if ← pure unexpand <&&> getPPOption getPPFieldNotation <&&> not <$> getPPOption getPPAnalysisNoDot then
       appFieldNotationCandidate?
diff --git a/tests/elab/2058.lean b/tests/elab/2058.lean
index 997a2513bc..230e7edc84 100644
--- a/tests/elab/2058.lean
+++ b/tests/elab/2058.lean
@@ -40,7 +40,7 @@ def foo : IO Unit := do
 /--
 info: def foo : IO Unit :=
 have x := PUnit.unit.{0};
-pure.{0, 0} Unit.unit
+pure.{0, 0} ()
 -/
 #guard_msgs in set_option pp.universes true in #print foo
 
diff --git a/tests/elab/ppUniverses.lean b/tests/elab/ppUniverses.lean
new file mode 100644
index 0000000000..a424e65b70
--- /dev/null
+++ b/tests/elab/ppUniverses.lean
@@ -0,0 +1,27 @@
+/-!
+# Tests of `pp.universe` option
+-/
+
+/-!
+This used to print `Iff p q`
+-/
+/-- info: p ↔ q : Prop -/
+#guard_msgs in
+set_option pp.universes true in
+variable (p q : Prop) in
+#check p ↔ q
+
+/-!
+These used to print `Nat.succ n`
+-/
+/-- info: n.succ : Nat -/
+#guard_msgs in
+set_option pp.universes true in
+variable (n : Nat) in
+#check Nat.succ n
+/-- info: n.succ : Nat -/
+#guard_msgs in
+set_option pp.universes true in
+set_option pp.explicit true in
+variable (n : Nat) in
+#check Nat.succ n