From 7e9ea00ac002761b3e040c593cc28a122861ff11 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Sat, 13 Sep 2025 22:15:04 -0700
Subject: [PATCH] feat: add option `pp.piBinderNames` (#10374)

This PR adds the options `pp.piBinderNames` and
`pp.piBinderNames.hygienic`. Enabling `pp.piBinderNames` causes
non-dependent pi binder names to be pretty printed, rather than be
omitted. When `pp.piBinderNames.hygienic` is false (the default) then
only non-hygienic such biner names are pretty printed. Setting `pp.all`
enables `pp.piBinderNames` if it is not otherwise explicitly set.

Implementation note: this is exposing the secret pretty printer option
`pp.piBinderNames` that was being used within the signature pretty
printer.

Closes #1134.
---
 .../PrettyPrinter/Delaborator/Builtins.lean   | 12 ++-
 .../PrettyPrinter/Delaborator/Options.lean    | 13 +++
 tests/lean/276.lean.expected.out              |  2 +-
 .../lean/eagerCoeExpansion.lean.expected.out  |  2 +-
 tests/lean/run/meta1.lean                     |  2 +-
 tests/lean/run/ppPiBinderNames.lean           | 97 +++++++++++++++++++
 tests/lean/unifHintAndTC.lean.expected.out    |  2 +-
 7 files changed, 121 insertions(+), 9 deletions(-)
 create mode 100644 tests/lean/run/ppPiBinderNames.lean

diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index ea76daa6c0..3a68ec815b 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -954,8 +954,6 @@ def delabLam : Delab :=
 
 /-- Don't do any renaming for forall binders, but do add fresh macro scopes when there is shadowing. -/
 private def ppPiPreserveNames := `pp.piPreserveNames
-/-- Causes non-dependent foralls to print with binder names. -/
-private def ppPiBinderNames := `pp.piBinderNames
 
 /--
 Similar to `delabBinders`, but tracking whether `forallE` is dependent or not.
@@ -964,7 +962,11 @@ See issue #1571
 -/
 private partial def delabForallBinders (prop : Bool) (delabGroup : Array Syntax → Bool → Syntax → Delab) (curNames : Array Syntax := #[]) (curDep := false) : Delab := do
   -- Logic note: wanting to print with binder names is equivalent to pretending the forall is dependent.
-  let mut dep := !(← getExpr).isArrow || (← getOptionsAtCurrPos).get ppPiBinderNames false
+  let opts ← getOptionsAtCurrPos
+  let mut dep :=
+    !(← getExpr).isArrow
+    || (getPPPiBinderNames opts
+        && (!(← getExpr).bindingName!.hasMacroScopes || getPPPiBinderNamesHygienic opts))
   if !dep && prop && (← getExpr).binderInfo.isExplicit then
     -- RFC #1834: If `∀` notation is enabled, avoid using `→` for propositions if the domain is not a proposition.
     -- We can pretend the type is dependent in this case.
@@ -975,7 +977,7 @@ private partial def delabForallBinders (prop : Bool) (delabGroup : Array Syntax
     -- don't group
     delabGroup curNames curDep (← delab)
   else
-    let preserve := (← getOptionsAtCurrPos).get ppPiPreserveNames false
+    let preserve := opts.get ppPiPreserveNames false
     let curDep := dep
     if ← shouldGroupWithNext then
       -- group with nested binder => recurse immediately
@@ -1554,7 +1556,7 @@ where
         if n.hasMacroScopes then
           return (opts, .forallE n t b' bi)
         else if !used then
-          let opts := opts.insertAt subExpr.pos ppPiBinderNames true
+          let opts := opts.insertAt subExpr.pos pp.piBinderNames.name true
           return (opts, .forallE n t b' bi)
         else
           let n' ← withFreshMacroScope <| MonadQuotation.addMacroScope n
diff --git a/src/Lean/PrettyPrinter/Delaborator/Options.lean b/src/Lean/PrettyPrinter/Delaborator/Options.lean
index 6f21bd0893..f1ec4ab4b0 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Options.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Options.lean
@@ -88,6 +88,17 @@ register_builtin_option pp.piBinderTypes : Bool := {
   group    := "pp"
   descr    := "(pretty printer) display types of pi parameters"
 }
+register_builtin_option pp.piBinderNames : Bool := {
+  defValue := false
+  group    := "pp"
+  descr    := "(pretty printer) display names for pi parameters, even if they are unused; \
+    when `pp.piBinderNames.hygienic` is false then unused hygienic parameters are not displayed."
+}
+register_builtin_option pp.piBinderNames.hygienic : Bool := {
+  defValue := false
+  group    := "pp"
+  descr    := "(pretty printer) if false, disables displaying names for unused pi parameters with hygienic names."
+}
 register_builtin_option pp.foralls : Bool := {
   defValue := true
   group    := "pp"
@@ -276,6 +287,8 @@ def getPPMaxSteps (o : Options) : Nat := o.get pp.maxSteps.name pp.maxSteps.defV
 def getPPAll (o : Options) : Bool := o.get pp.all.name false
 def getPPFunBinderTypes (o : Options) : Bool := o.get pp.funBinderTypes.name (getPPAll o)
 def getPPPiBinderTypes (o : Options) : Bool := o.get pp.piBinderTypes.name pp.piBinderTypes.defValue
+def getPPPiBinderNames (o : Options) : Bool := o.get pp.piBinderNames.name (getPPAll o)
+def getPPPiBinderNamesHygienic (o : Options) : Bool := o.get pp.piBinderNames.hygienic.name pp.piBinderNames.hygienic.defValue
 def getPPLetVarTypes (o : Options) : Bool := o.get pp.letVarTypes.name (getPPAll o)
 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)
diff --git a/tests/lean/276.lean.expected.out b/tests/lean/276.lean.expected.out
index d5b5529d3b..cc59490b45 100644
--- a/tests/lean/276.lean.expected.out
+++ b/tests/lean/276.lean.expected.out
@@ -1,2 +1,2 @@
-fun {α : Sort v} => PEmpty.rec.{v, u_1} fun (x : PEmpty.{u_1}) => α : {α : Sort v} → PEmpty.{u_1} → α
+fun {α : Sort v} => PEmpty.rec.{v, u_1} fun (x : PEmpty.{u_1}) => α : {α : Sort v} → (t : PEmpty.{u_1}) → α
 276.lean:9:4-9:16: error: code generator does not support recursor `PEmpty.rec` yet, consider using 'match ... with' and/or structural recursion
diff --git a/tests/lean/eagerCoeExpansion.lean.expected.out b/tests/lean/eagerCoeExpansion.lean.expected.out
index 2d221fd564..3f081cbc12 100644
--- a/tests/lean/eagerCoeExpansion.lean.expected.out
+++ b/tests/lean/eagerCoeExpansion.lean.expected.out
@@ -2,7 +2,7 @@ def h : BV 32 → Array Bool :=
 fun x => (fun x => g (f x).val) x
 def r : Nat → Prop :=
 fun a => if (a == 0) = true then (a != 1) = true else (a != 2) = true
-def r : Nat → Prop :=
+def r : (a : Nat) → Prop :=
 fun (a : Nat) =>
   @ite.{1} Prop
     (@Eq.{1} Bool
diff --git a/tests/lean/run/meta1.lean b/tests/lean/run/meta1.lean
index df4dde5d22..aab1ec1c1e 100644
--- a/tests/lean/run/meta1.lean
+++ b/tests/lean/run/meta1.lean
@@ -65,7 +65,7 @@ mkAppN add #[mkLit (Literal.natVal 3), mkLit (Literal.natVal 5)]
 #eval tstWHNF t5
 
 set_option pp.all true
-/-- info: @List.cons.{0} Nat : Nat → List.{0} Nat → List.{0} Nat -/
+/-- info: @List.cons.{0} Nat : (head : Nat) → (tail : List.{0} Nat) → List.{0} Nat -/
 #guard_msgs in
 #check @List.cons Nat
 
diff --git a/tests/lean/run/ppPiBinderNames.lean b/tests/lean/run/ppPiBinderNames.lean
new file mode 100644
index 0000000000..3ba54e75b8
--- /dev/null
+++ b/tests/lean/run/ppPiBinderNames.lean
@@ -0,0 +1,97 @@
+/-!
+# Testing pretty printing option `pp.piBinderNames`
+-/
+
+/-!
+Tests of default options.
+-/
+section
+
+/-!
+Unused name, doesn't print.
+-/
+/-- info: Nat → Type : Type 1 -/
+#guard_msgs in #check (x : Nat) → Type
+
+/-!
+Unused hygienic name, doesn't print.
+-/
+/-- info: Nat → Type : Type 1 -/
+#guard_msgs in #check Nat → Type
+
+end
+
+/-!
+Tests with `pp.piBinderNames` enabled.
+-/
+section
+set_option pp.piBinderNames true
+
+/-!
+Unused name, prints since not hygienic.
+-/
+/-- info: (x : Nat) → Type : Type 1 -/
+#guard_msgs in #check (x : Nat) → Type
+
+/-!
+Unused hygienic name, doesn't print.
+-/
+/-- info: Nat → Type : Type 1 -/
+#guard_msgs in #check Nat → Type
+
+end
+
+/-!
+Tests with `pp.piBinderNames` and `pp.piBinderNames.hygienic` enabled.
+-/
+section
+set_option pp.piBinderNames true
+set_option pp.piBinderNames.hygienic true
+
+/-!
+Prints unused name.
+-/
+/-- info: (x : Nat) → Type : Type 1 -/
+#guard_msgs in #check (x : Nat) → Type
+
+/-!
+Prints unused hygienic name.
+-/
+/-- info: (a : Nat) → Type : Type 1 -/
+#guard_msgs in #check Nat → Type
+
+end
+
+/-!
+Tests with `pp.all`. Enables `pp.piBinderNames`.
+-/
+section
+set_option pp.all true
+
+/-!
+Unused name, prints since not hygienic.
+-/
+/-- info: (x : Nat) → Type : Type 1 -/
+#guard_msgs in #check (x : Nat) → Type
+
+/-!
+Unused hygienic name, doesn't print.
+-/
+/-- info: Nat → Type : Type 1 -/
+#guard_msgs in #check Nat → Type
+
+set_option pp.piBinderNames.hygienic true
+
+/-!
+Prints unused name.
+-/
+/-- info: (x : Nat) → Type : Type 1 -/
+#guard_msgs in #check (x : Nat) → Type
+
+/-!
+Prints unused hygienic name.
+-/
+/-- info: (a : Nat) → Type : Type 1 -/
+#guard_msgs in #check Nat → Type
+
+end
diff --git a/tests/lean/unifHintAndTC.lean.expected.out b/tests/lean/unifHintAndTC.lean.expected.out
index de5b4ff4b5..a645915b7c 100644
--- a/tests/lean/unifHintAndTC.lean.expected.out
+++ b/tests/lean/unifHintAndTC.lean.expected.out
@@ -1,4 +1,4 @@
 (100, 400)
 (49, 576, 576)
-def g : Int → Int → Int :=
+def g : (x y : Int) → Int :=
 fun (x y : Int) => @mul.{0} (@magmaOfMul.{0} Int Int.instMul) x y