feat: display coercions with a type ascription (leanprover#6119)

This PR adds a new delab option `pp.coercions.types` which, when
enabled, will display all coercions with an explicit type ascription.

[Link to Zulip
discussion](https://leanprover.zulipchat.com/#narrow/channel/239415-metaprogramming-.2F-tactics/topic/Roundtripping.20delaboration.20involving.20coercions)

Towards leanprover#4315

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -1115,17 +1115,18 @@ def coeDelaborator : Delab := whenPPOption getPPCoercions do
     delabAppCore nargs (delabHead info nargs) (unexpand := false)
 where
   delabHead (info : CoeFnInfo) (nargs : Nat) (insertExplicit : Bool) : Delab := do
-    guard <| !insertExplicit
-    if info.type == .coeFun && nargs > 0 then
-      -- In the CoeFun case, annotate with the coercee itself.
-      -- We can still see the whole coercion expression by hovering over the whitespace between the arguments.
-      withNaryArg info.coercee <| withAnnotateTermInfo delab
-    else
-      withAnnotateTermInfo do
-        match info.type with
-        | .coe     => `(↑$(← withNaryArg info.coercee delab))
-        | .coeFun  => `(⇑$(← withNaryArg info.coercee delab))
-        | .coeSort => `(↥$(← withNaryArg info.coercee delab))
+    withTypeAscription (cond := ← getPPOption getPPCoercionsTypes) do
+      guard <| !insertExplicit
+      if info.type == .coeFun && nargs > 0 then
+        -- In the CoeFun case, annotate with the coercee itself.
+        -- We can still see the whole coercion expression by hovering over the whitespace between the arguments.
+        withNaryArg info.coercee <| withAnnotateTermInfo delab
+      else
+        withAnnotateTermInfo do
+          match info.type with
+          | .coe     => `(↑$(← withNaryArg info.coercee delab))
+          | .coeFun  => `(⇑$(← withNaryArg info.coercee delab))
+          | .coeSort => `(↥$(← withNaryArg info.coercee delab))
 
 @[builtin_delab app.dite]
 def delabDIte : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPNotation <| withOverApp 5 do

src/Lean/PrettyPrinter/Delaborator/Options.lean

@@ -44,6 +44,11 @@ register_builtin_option pp.coercions : Bool := {
   group    := "pp"
   descr    := "(pretty printer) hide coercion applications"
 }
+register_builtin_option pp.coercions.types : Bool := {
+  defValue := false
+  group    := "pp"
+  descr    := "(pretty printer) display coercion applications with a type ascription"
+}
 register_builtin_option pp.universes : Bool := {
   defValue := false
   group    := "pp"
@@ -251,6 +256,7 @@ def getPPLetVarTypes (o : Options) : Bool := o.get pp.letVarTypes.name (getPPAll
 def getPPNumericTypes (o : Options) : Bool := o.get pp.numericTypes.name pp.numericTypes.defValue
 def getPPNatLit (o : Options) : Bool := o.get pp.natLit.name (getPPNumericTypes o && !getPPAll o)
 def getPPCoercions (o : Options) : Bool := o.get pp.coercions.name (!getPPAll o)
+def getPPCoercionsTypes (o : Options) : Bool := o.get pp.coercions.types.name pp.coercions.types.defValue
 def getPPExplicit (o : Options) : Bool := o.get pp.explicit.name (getPPAll o)
 def getPPNotation (o : Options) : Bool := o.get pp.notation.name (!getPPAll o)
 def getPPParens (o : Options) : Bool := o.get pp.parens.name pp.parens.defValue

tests/lean/run/coeAttrs.lean

@@ -0,0 +1,26 @@
+/-!
+# Tests for `pp.coercions.types` option
+-/
+
+-- With the option off (default)
+/--
+info: n : Nat
+h : n = 0
+⊢ ↑n = 0
+-/
+#guard_msgs in
+example (n : Nat) (h : n = 0) : (↑n : Int) = 0 := by
+  trace_state
+  simp [h]
+
+-- With the option on
+/--
+info: n : Nat
+h : n = 0
+⊢ (↑n : Int) = 0
+-/
+#guard_msgs in
+set_option pp.coercions.types true in
+example (n : Nat) (h : n = 0) : (↑n : Int) = 0 := by
+  trace_state
+  simp [h]