From 3c1a0fe544934f2b9691061e9a585f08b1c94ad1 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Fri, 14 Feb 2025 09:28:54 -0800
Subject: [PATCH] feat: make binders in `#check` be hoverable (#7074)

This PR modifies the signature pretty printer to add hover information
for parameters in binders. This makes the binders be consistent with the
hovers in pi types.

Suggested by @david-christiansen
---
 .../PrettyPrinter/Delaborator/Builtins.lean   | 35 +++++++++++++------
 1 file changed, 24 insertions(+), 11 deletions(-)

diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 44a435655a32b..2e7f912a4227d 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -1386,25 +1386,38 @@ where
     let e@(.forallE n d e' i) ← getExpr | unreachable!
     let n ← if bindingNames.contains n then withFreshMacroScope <| MonadQuotation.addMacroScope n else pure n
     let bindingNames := bindingNames.insert n
-    let stxN := mkIdent n
-    let curIds := curIds.push ⟨stxN⟩
     if shouldGroupWithNext bindingNames e e' then
-      withBindingBody n <| delabParamsAux bindingNames idStx groups curIds
+      withBindingBody' n (mkAnnotatedIdent n) fun stxN =>
+        delabParamsAux bindingNames idStx groups (curIds.push stxN)
     else
-      let group ← withBindingDomain do
+      /-
+      `mkGroup` constructs binder syntax for the binder names `curIds : Array Ident`, which all have the same type and binder info.
+      This being a function is solving the following issue:
+      - To get the last binder name, we need to be under `withBindingBody'`, which lets us annotate the binder with its fvar.
+      - However, we should delaborate the binder type from outside `withBindingBody'`.
+      - Thus, we need to partially construct the binder syntax, waiting on the final value of `curIds`.
+      -/
+      let mkGroup : Array Ident → DelabM Syntax ← withBindingDomain do
         match i with
-        | .implicit       => `(bracketedBinderF|{$curIds* : $(← delabTy)})
-        | .strictImplicit => `(bracketedBinderF|⦃$curIds* : $(← delabTy)⦄)
-        | .instImplicit   => `(bracketedBinderF|[$stxN : $(← delabTy)])
+        | .implicit       => let ty ← delabTy; pure fun curIds => `(bracketedBinderF|{$curIds* : $ty})
+        | .strictImplicit => let ty ← delabTy; pure fun curIds => `(bracketedBinderF|⦃$curIds* : $ty⦄)
+        | .instImplicit   => let ty ← delabTy; pure fun curIds => `(bracketedBinderF|[$(curIds[0]!) : $ty])
         | _ =>
           if d.isOptParam then
-            `(bracketedBinderF|($curIds* : $(← withAppFn <| withAppArg delabTy) := $(← withAppArg delabTy)))
+            let ty ← withAppFn <| withAppArg delabTy
+            let val ← withAppArg delabTy
+            pure fun curIds => `(bracketedBinderF|($curIds* : $ty := $val))
           else if let some (.const tacticDecl _) := d.getAutoParamTactic? then
+            let ty ← withAppFn <| withAppArg delabTy
             let tacticSyntax ← ofExcept <| evalSyntaxConstant (← getEnv) (← getOptions) tacticDecl
-            `(bracketedBinderF|($curIds* : $(← withAppFn <| withAppArg delabTy) := by $tacticSyntax))
+            pure fun curIds => `(bracketedBinderF|($curIds* : $ty := by $tacticSyntax))
           else
-            `(bracketedBinderF|($curIds* : $(← delabTy)))
-      withBindingBody n <| delabParams bindingNames idStx (groups.push group)
+            let ty ← delabTy
+            pure fun curIds => `(bracketedBinderF|($curIds* : $ty))
+      withBindingBody' n (mkAnnotatedIdent n) fun stxN => do
+        let curIds := curIds.push stxN
+        let group ← mkGroup curIds
+        delabParams bindingNames idStx (groups.push group)
   /-
   Given the forall `e` with body `e'`, determines if the binder from `e'` (if it is a forall) should be grouped with `e`'s binder.
   -/