fix: make withOverApp annotate the expression position and register TermInfo (#3327)

This makes it so that when `withOverApp` is handling overapplied
functions, the term produced by the supplied delaborator is hoverable in
the Infoview.

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -269,11 +269,22 @@ def shouldOmitExpr (e : Expr) : DelabM Bool := do
 
   return depthExcess > 0 && !isShallowExpression
 
+/--
+Annotates the term with the current expression position and registers `TermInfo`
+to associate the term to the current expression.
+-/
 def annotateTermInfo (stx : Term) : Delab := do
   let stx ← annotateCurPos stx
   addTermInfo (← getPos) stx (← getExpr)
   pure stx
 
+/--
+Modifies the delaborator so that it annotates the resulting term with the current expression
+position and registers `TermInfo` to associate the term to the current expression.
+-/
+def withAnnotateTermInfo (d : Delab) : Delab := do
+  let stx ← d
+  annotateTermInfo stx
 
 /--
 Delaborates the current expression as `⋯` and attaches `Elab.OmissionInfo`, which influences how the

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -331,7 +331,11 @@ With this combinator one can use an arity-2 delaborator to pretty print this as
   The combinator will fail if fewer than this number of arguments are passed,
   and if more than this number of arguments are passed the arguments are handled using
   the standard application delaborator.
-* `x`: constructs data corresponding to the main application (`f x` in the example)
+* `x`: constructs data corresponding to the main application (`f x` in the example).
+
+In the event of overapplication, the delaborator `x` is wrapped in
+`Lean.PrettyPrinter.Delaborator.withAnnotateTermInfo` to register `TermInfo` for the resulting term.
+The effect of this is that the term is hoverable in the Infoview.
 -/
 def withOverApp (arity : Nat) (x : Delab) : Delab := do
   let n := (← getExpr).getAppNumArgs
@@ -339,7 +343,7 @@ def withOverApp (arity : Nat) (x : Delab) : Delab := do
   if n == arity then
     x
   else
-    delabAppCore (n - arity) x
+    delabAppCore (n - arity) (withAnnotateTermInfo x)
 
 /-- State for `delabAppMatch` and helpers. -/
 structure AppMatchState where