From 498d41633b4453a15465d52804e4e6b046092a8a Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Thu, 14 Nov 2024 17:45:38 -0800
Subject: [PATCH] fix: pretty print `.coeFun` with terminfo of coercee (#6085)

This PR improves the term info for coercions marked with
`CoeFnType.coeFun` (such as `DFunLike.coe` in Mathlib), making "go to
definition" on the function name work. Hovering over such a coerced
function will show the coercee rather than the coercion expression. The
coercion expression can still be seen by hovering over the whitespace in
the function application.
---
 .../PrettyPrinter/Delaborator/Builtins.lean   | 30 ++++++++++++-------
 1 file changed, 20 insertions(+), 10 deletions(-)

diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index b81d514199..8d106035e4 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -1092,19 +1092,29 @@ def coeDelaborator : Delab := whenPPOption getPPCoercions do
   let e ← getExpr
   let .const declName _ := e.getAppFn | failure
   let some info ← Meta.getCoeFnInfo? declName | failure
+  let n := e.getAppNumArgs
+  guard <| n ≥ info.numArgs
   if (← getPPOption getPPExplicit) && info.coercee != 0 then
     -- Approximation: the only implicit arguments come before the coercee
     failure
-  let n := e.getAppNumArgs
-  withOverApp info.numArgs do
-    match info.type with
-    | .coe => `(↑$(← withNaryArg info.coercee delab))
-    | .coeFun =>
-      if n = info.numArgs then
-        `(⇑$(← withNaryArg info.coercee delab))
-      else
-        withNaryArg info.coercee delab
-    | .coeSort => `(↥$(← withNaryArg info.coercee delab))
+  if n == info.numArgs then
+    delabHead info 0 false
+  else
+    let nargs := n - info.numArgs
+    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))
 
 @[builtin_delab app.dite]
 def delabDIte : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPNotation <| withOverApp 5 do