feat: pretty print props with → only if domain is prop, add pp.foralls (#7812)

This PR modifies the pretty printing of pi types. Now `∀` will be preferred over `→` for propositions if the domain is not a proposition. For example, `∀ (n : Nat), True` pretty prints as `∀ (n : Nat), True` rather than as `Nat → True`. There is also now an option `pp.foralls` (default true) that when false disables using `∀` at all, for pedagogical purposes. This PR also adjusts instance implicit binder pretty printing — nondependent pi types won't show the instance binder name. Closes #1834. The linked RFC also suggests using `_` for binder names in case of non-dependance. We're tabling that idea. Potentially it is useful for hygienic names; this could improve how `Nat → True` pretty prints as `∀ (a : Nat), True`, with this `a` that's chosen by implication notation elaboration. Relatedly, this PR exposes even further the issue where binder names are reused in a confusing way. Consider: `Nat → Nat → (a : Nat) → a = a` pretty prints as `∀ (a a a : Nat), a = a`.
2026-03-17 18:34:06 +00:00 · 2025-04-03 19:55:47 -07:00
parent 906edd4529
commit 407a59d697
21 changed files with 227 additions and 59 deletions
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -964,9 +964,15 @@ Similar to `delabBinders`, but tracking whether `forallE` is dependent or not.

 See issue #1571
 -/
-private partial def delabForallBinders (delabGroup : Array Syntax → Bool → Syntax → Delab) (curNames : Array Syntax := #[]) (curDep := false) : Delab := do
+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 dep := !(← getExpr).isArrow || (← getOptionsAtCurrPos).get ppPiBinderNames false
+  let mut dep := !(← getExpr).isArrow || (← getOptionsAtCurrPos).get ppPiBinderNames false
+  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.
+    if (← getPPOption getPPForalls) then
+      let domProp ← try isProp (← getExpr).bindingDomain! catch _ => pure false
+      dep := !domProp
  if !curNames.isEmpty && dep != curDep then
    -- don't group
    delabGroup curNames curDep (← delab)
@@ -975,7 +981,7 @@ private partial def delabForallBinders (delabGroup : Array Syntax → Bool → S
    let curDep := dep
    if ← shouldGroupWithNext then
      -- group with nested binder => recurse immediately
-      withBindingBodyUnusedName (preserveName := preserve) fun stxN => delabForallBinders delabGroup (curNames.push stxN) curDep
+      withBindingBodyUnusedName (preserveName := preserve) fun stxN => delabForallBinders prop delabGroup (curNames.push stxN) curDep
    else
      -- don't group => delab body and prepend current binder group
      let (stx, stxN) ← withBindingBodyUnusedName (preserveName := preserve) fun stxN => return (← delab, stxN)
@@ -983,25 +989,30 @@ private partial def delabForallBinders (delabGroup : Array Syntax → Bool → S

@[builtin_delab forallE]
 def delabForall : Delab := do
-  delabForallBinders fun curNames dependent stxBody => do
+  let prop ← try isProp (← getExpr) catch _ => pure false
+  delabForallBinders prop fun curNames dependent stxBody => do
    let e ← getExpr
-    let prop ← try isProp e catch _ => pure false
    let stxT ← withBindingDomain delab
    let group ← match e.binderInfo with
    | BinderInfo.implicit       => `(bracketedBinderF|{$curNames* : $stxT})
    | BinderInfo.strictImplicit => `(bracketedBinderF|⦃$curNames* : $stxT⦄)
-    -- here `curNames.size == 1`
-    | BinderInfo.instImplicit   => `(bracketedBinderF|[$curNames.back! : $stxT])
+    | BinderInfo.instImplicit   =>
+      -- here `curNames.size == 1`
+      if dependent || !e.bindingName!.hasMacroScopes then
+        `(bracketedBinderF|[$curNames.back! : $stxT])
+      else
+        -- omit the binder name if it's not used and not accessible
+        `(bracketedBinderF|[$stxT])
    | _                         =>
      -- NOTE: non-dependent arrows are available only for the default binder info
      if dependent then
-        if prop && !(← getPPOption getPPPiBinderTypes) then
+        if prop && !(← getPPOption getPPPiBinderTypes) && (← getPPOption getPPForalls) then
          return ← `(∀ $curNames:ident*, $stxBody)
        else
          `(bracketedBinderF|($curNames* : $stxT))
      else
        return ← curNames.foldrM (fun _ stxBody => `($stxT → $stxBody)) stxBody
-    if prop then
+    if prop && (← getPPOption getPPForalls) then
      match stxBody with
      | `(∀ $groups*, $stxBody) => `(∀ $group $groups*, $stxBody)
      | _                       => `(∀ $group, $stxBody)
--- a/src/Lean/PrettyPrinter/Delaborator/Options.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Options.lean
@@ -79,6 +79,11 @@ register_builtin_option pp.piBinderTypes : Bool := {
  group    := "pp"
  descr    := "(pretty printer) display types of pi parameters"
 }
+register_builtin_option pp.foralls : Bool := {
+  defValue := true
+  group    := "pp"
+  descr    := "(pretty printer) display pi types that are propositions using `∀` notation rather than with dependent arrows"
+}
 register_builtin_option pp.letVarTypes : Bool := {
  defValue := false
  group    := "pp"
@@ -268,6 +273,7 @@ def getPPNatLit (o : Options) : Bool := o.get pp.natLit.name (getPPNumericTypes
 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 getPPForalls (o : Options) : Bool := o.get pp.foralls.name pp.foralls.defValue
 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
 def getPPUnicodeFun (o : Options) : Bool := o.get pp.unicode.fun.name false
--- a/tests/lean/1682.lean.expected.out
+++ b/tests/lean/1682.lean.expected.out
@@ -2,7 +2,7 @@
 case a
 p : Sort u_1
 q r : Prop
-⊢ p → q
+⊢ ∀ (a : p), q

 case b
 p : Sort u_1
--- a/tests/lean/2115.lean.expected.out
+++ b/tests/lean/2115.lean.expected.out
@@ -1,8 +1,8 @@
-def foo : {α : Type} → [inst : D α] → A α :=
+def foo : {α : Type} → [D α] → A α :=
 fun {α : Type} [inst : D α] => @inferInstance.{1} (A α) (@B.toA α (@D.toB α inst))
-def bla : {α : Type} → [inst : D α] → A α :=
+def bla : {α : Type} → [D α] → A α :=
 fun {α : Type} [inst : D α] => @inferInstance.{1} (A α) (@C.toA α (@D.toC α inst))
-def boo : {α : Type} → [inst : D α] → A α :=
+def boo : {α : Type} → [D α] → A α :=
 fun {α : Type} [inst : D α] => @inferInstance.{1} (A α) (@B.toA α (@D.toB α inst))
-def boo2 : {α : Type} → [inst : D α] → A α :=
+def boo2 : {α : Type} → [D α] → A α :=
 fun {α : Type} [inst : D α] => @inferInstance.{1} (A α) (@C.toA α (@D.toC α inst))
--- a/tests/lean/815b.lean.expected.out
+++ b/tests/lean/815b.lean.expected.out
@@ -18,7 +18,7 @@
    [Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a) d ≟ IsSmooth f
  [Meta.synthInstance] ✅️ apply @diag to ∀ (a : α), IsSmooth fun g => f (g a) d
    [Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a) d ≟ IsSmooth fun a_1 => f (a_1 a) d
-    [Meta.synthInstance.unusedArgs] α → IsSmooth f
+    [Meta.synthInstance.unusedArgs] ∀ (a : α), IsSmooth f
        has unused arguments, reduced type
          IsSmooth f
        Transformer
@@ -30,15 +30,15 @@
    [Meta.synthInstance.answer] ✅️ IsSmooth f
  [Meta.synthInstance.resume] propagating IsSmooth f to subgoal IsSmooth f of ∀ (a : α), IsSmooth fun g => f (g a) d
    [Meta.synthInstance.resume] size: 1
-    [Meta.synthInstance.unusedArgs] α → IsSmooth f
+    [Meta.synthInstance.unusedArgs] ∀ (a : α), IsSmooth f
        has unused arguments, reduced type
          IsSmooth f
        Transformer
          fun redf a => redf
-  [Meta.synthInstance.resume] propagating α →
-        IsSmooth f to subgoal α → IsSmooth f of ∀ (a : α), IsSmooth fun g => f (g a) d
+  [Meta.synthInstance.resume] propagating ∀ (a : α),
+        IsSmooth f to subgoal ∀ (a : α), IsSmooth f of ∀ (a : α), IsSmooth fun g => f (g a) d
    [Meta.synthInstance.resume] size: 2
-    [Meta.synthInstance.unusedArgs] α → ∀ (b : β), IsSmooth (f b)
+    [Meta.synthInstance.unusedArgs] ∀ (a : α) (b : β), IsSmooth (f b)
        has unused arguments, reduced type
          ∀ (b : β), IsSmooth (f b)
        Transformer
@@ -63,15 +63,15 @@
    [Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth f
  [Meta.synthInstance] ✅️ apply @diag to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
    [Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => f (a_1 a✝) a
-    [Meta.synthInstance.unusedArgs] α → δ → IsSmooth f
+    [Meta.synthInstance.unusedArgs] ∀ (a : α) (a : δ), IsSmooth f
        has unused arguments, reduced type
          IsSmooth f
        Transformer
          fun redf a a => redf
-  [Meta.synthInstance.resume] propagating α →
-        δ → IsSmooth f to subgoal α → δ → IsSmooth f of ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
+  [Meta.synthInstance.resume] propagating ∀ (a : α) (a : δ),
+        IsSmooth f to subgoal ∀ (a : α) (a : δ), IsSmooth f of ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
    [Meta.synthInstance.resume] size: 1
-    [Meta.synthInstance.unusedArgs] α → δ → ∀ (b : β), IsSmooth (f b)
+    [Meta.synthInstance.unusedArgs] ∀ (a : α) (a : δ) (b : β), IsSmooth (f b)
        has unused arguments, reduced type
          ∀ (b : β), IsSmooth (f b)
        Transformer
@@ -81,7 +81,7 @@
          f (g a✝) a ≟ IsSmooth fun a_1 => ?m a✝ a (?m a✝ a a_1)
  [Meta.synthInstance] ✅️ apply @parm to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
    [Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => f (a_1 a✝) a
-    [Meta.synthInstance.unusedArgs] ∀ (a : α), δ → IsSmooth fun g => f (g a)
+    [Meta.synthInstance.unusedArgs] ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a)
        has unused arguments, reduced type
          ∀ (a : α), IsSmooth fun g => f (g a)
        Transformer
@@ -95,13 +95,13 @@
          f (g a) ≟ IsSmooth fun a_1 => ?m a (?m a a_1) (?m a a_1)
  [Meta.synthInstance] ✅️ apply @comp to ∀ (a : α), IsSmooth fun g => f (g a)
    [Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a) ≟ IsSmooth fun a_1 => f (a_1 a)
-    [Meta.synthInstance.unusedArgs] α → IsSmooth f
+    [Meta.synthInstance.unusedArgs] ∀ (a : α), IsSmooth f
        has unused arguments, reduced type
          IsSmooth f
        Transformer
          fun redf a => redf
-  [Meta.synthInstance.resume] propagating α →
-        IsSmooth f to subgoal α → IsSmooth f of ∀ (a : α), IsSmooth fun g => f (g a)
+  [Meta.synthInstance.resume] propagating ∀ (a : α),
+        IsSmooth f to subgoal ∀ (a : α), IsSmooth f of ∀ (a : α), IsSmooth fun g => f (g a)
    [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance] new goal ∀ (a : α), IsSmooth fun g => g a
      [Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, inst✝]
@@ -114,7 +114,7 @@
    [Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g a ≟ IsSmooth fun a_1 => ?m a (?m a a_1)
  [Meta.synthInstance] ✅️ apply @parm to ∀ (a : α), IsSmooth fun g => g a
    [Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => g a ≟ IsSmooth fun a_1 => a_1 a
-    [Meta.synthInstance.unusedArgs] α → IsSmooth fun g => g
+    [Meta.synthInstance.unusedArgs] ∀ (a : α), IsSmooth fun g => g
        has unused arguments, reduced type
          IsSmooth fun g => g
        Transformer
@@ -139,13 +139,13 @@
  [Meta.synthInstance.resume] propagating IsSmooth fun a =>
        a to subgoal IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
    [Meta.synthInstance.resume] size: 1
-    [Meta.synthInstance.unusedArgs] α → IsSmooth fun g => g
+    [Meta.synthInstance.unusedArgs] ∀ (a : α), IsSmooth fun g => g
        has unused arguments, reduced type
          IsSmooth fun g => g
        Transformer
          fun redf a => redf
-  [Meta.synthInstance.resume] propagating α →
-        IsSmooth fun a => a to subgoal α → IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
+  [Meta.synthInstance.resume] propagating ∀ (a : α),
+        IsSmooth fun a => a to subgoal ∀ (a : α), IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
    [Meta.synthInstance.resume] size: 2
    [Meta.synthInstance.answer] ✅️ ∀ (a : α), IsSmooth fun g => g a
  [Meta.synthInstance.resume] propagating ∀ (a : α),
@@ -155,17 +155,17 @@
  [Meta.synthInstance.resume] propagating IsSmooth fun b a =>
        b a to subgoal IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
    [Meta.synthInstance.resume] size: 4
-    [Meta.synthInstance.unusedArgs] α → IsSmooth fun g => g
+    [Meta.synthInstance.unusedArgs] ∀ (a : α), IsSmooth fun g => g
        has unused arguments, reduced type
          IsSmooth fun g => g
        Transformer
          fun redf a => redf
-  [Meta.synthInstance.resume] propagating α →
-        IsSmooth fun b a => b a to subgoal α → IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
+  [Meta.synthInstance.resume] propagating ∀ (a : α),
+        IsSmooth fun b a => b a to subgoal ∀ (a : α), IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
    [Meta.synthInstance.resume] size: 8
    [Meta.synthInstance.answer] ✅️ ∀ (a : α), IsSmooth fun g => g a
-  [Meta.synthInstance.resume] propagating α →
-        IsSmooth fun a => a to subgoal α → IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
+  [Meta.synthInstance.resume] propagating ∀ (a : α),
+        IsSmooth fun a => a to subgoal ∀ (a : α), IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
    [Meta.synthInstance.resume] size: 5
    [Meta.synthInstance.answer] ✅️ ∀ (a : α), IsSmooth fun g => g a
  [Meta.synthInstance.resume] propagating ∀ (a : α),
--- a/tests/lean/PPRoundtrip.lean.expected.out
+++ b/tests/lean/PPRoundtrip.lean.expected.out
@@ -36,13 +36,10 @@ Type → Type → Type
 (α : Type) → α → α
 {α : Type} → α
 {α : Type} →
-  [inst :
-      ToString α] →
-    α
+  [ToString α] → α
 ∀ (x : Nat), x = x
 ∀ {x : Nat}
-  [inst :
-    ToString Nat],
+  [ToString Nat],
  x = x
 ∀ x, x = x
 0
--- a/tests/lean/funParen.lean.expected.out
+++ b/tests/lean/funParen.lean.expected.out
@@ -1,4 +1,4 @@
-fun α [Repr α] => repr : (α : Type u_1) → [inst : Repr α] → α → Std.Format
+fun α [Repr α] => repr : (α : Type u_1) → [Repr α] → α → Std.Format
 fun x y => x : (x : ?m) → ?m x → ?m
 funParen.lean:4:12-4:16: error: invalid pattern, constructor or constant marked with '[match_pattern]' expected
 fun x => ?m : (x : ?m) → ?m x
--- a/tests/lean/interactive/Diff.lean.expected.out
+++ b/tests/lean/interactive/Diff.lean.expected.out
@@ -103,10 +103,15 @@
                         { type := Lean.Widget.TaggedText.tag
                                     { subexprPos := "/", diffStatus? := none }
                                     (Lean.Widget.TaggedText.append
-                                       #[Lean.Widget.TaggedText.tag
+                                       #[Lean.Widget.TaggedText.text "∀ (",
+                                         Lean.Widget.TaggedText.tag
+                                           { subexprPos := "/", diffStatus? := none }
+                                           (Lean.Widget.TaggedText.text "a"),
+                                         Lean.Widget.TaggedText.text " : ",
+                                         Lean.Widget.TaggedText.tag
                                           { subexprPos := "/0", diffStatus? := none }
                                           (Lean.Widget.TaggedText.text "α"),
-                                         Lean.Widget.TaggedText.text " → ",
+                                         Lean.Widget.TaggedText.text "), ",
                                         Lean.Widget.TaggedText.tag
                                           { subexprPos := "/1", diffStatus? := none }
                                           (Lean.Widget.TaggedText.append
@@ -154,10 +159,15 @@
                         { type := Lean.Widget.TaggedText.tag
                                     { subexprPos := "/", diffStatus? := none }
                                     (Lean.Widget.TaggedText.append
-                                       #[Lean.Widget.TaggedText.tag
+                                       #[Lean.Widget.TaggedText.text "∀ (",
+                                         Lean.Widget.TaggedText.tag
+                                           { subexprPos := "/", diffStatus? := none }
+                                           (Lean.Widget.TaggedText.text "a"),
+                                         Lean.Widget.TaggedText.text " : ",
+                                         Lean.Widget.TaggedText.tag
                                           { subexprPos := "/0", diffStatus? := none }
                                           (Lean.Widget.TaggedText.text "α"),
-                                         Lean.Widget.TaggedText.text " → ",
+                                         Lean.Widget.TaggedText.text "), ",
                                         Lean.Widget.TaggedText.tag
                                           { subexprPos := "/1", diffStatus? := none }
                                           (Lean.Widget.TaggedText.append
--- a/tests/lean/interactive/incrementalTactic.lean.expected.out
+++ b/tests/lean/interactive/incrementalTactic.lean.expected.out
@@ -22,7 +22,7 @@ t 2
   "severity": 1,
   "range":
   {"start": {"line": 2, "character": 22}, "end": {"line": 3, "character": 0}},
-   "message": "unsolved goals\nthis : Nat → Nat → True\n⊢ True",
+   "message": "unsolved goals\nthis : ∀ (a a : Nat), True\n⊢ True",
   "leanTags": [1],
   "fullRange":
   {"start": {"line": 2, "character": 22},
--- a/tests/lean/interactive/plainGoal.lean.expected.out
+++ b/tests/lean/interactive/plainGoal.lean.expected.out
@@ -82,9 +82,9 @@
 {"textDocument": {"uri": "file:///plainGoal.lean"},
 "position": {"line": 55, "character": 3}}
 {"rendered":
- "```lean\nα : Sort u_1\np : α → Prop\na b : α\ninst✝ : DecidablePred p\nh : ∀ {p : α → Prop} [inst : DecidablePred p], p a → p b\n⊢ p a\n```",
+ "```lean\nα : Sort u_1\np : α → Prop\na b : α\ninst✝ : DecidablePred p\nh : ∀ {p : α → Prop} [DecidablePred p], p a → p b\n⊢ p a\n```",
 "goals":
- ["α : Sort u_1\np : α → Prop\na b : α\ninst✝ : DecidablePred p\nh : ∀ {p : α → Prop} [inst : DecidablePred p], p a → p b\n⊢ p a"]}
+ ["α : Sort u_1\np : α → Prop\na b : α\ninst✝ : DecidablePred p\nh : ∀ {p : α → Prop} [DecidablePred p], p a → p b\n⊢ p a"]}
 {"textDocument": {"uri": "file:///plainGoal.lean"},
 "position": {"line": 61, "character": 3}}
 {"rendered": "```lean\ncase left\n⊢ True\n```", "goals": ["case left\n⊢ True"]}
--- a/tests/lean/lcnfTypes.lean.expected.out
+++ b/tests/lean/lcnfTypes.lean.expected.out
@@ -15,7 +15,7 @@ MonadControl.liftWith : {m : Type u → Type v} →
  {n : Type u → Type w} → [self : MonadControl m n] → {α : Type u} → (({β : Type u} → n β → m ◾) → m α) → n α
 MonadControl.restoreM : {m : Type u → Type v} → {n : Type u → Type w} → [self : MonadControl m n] → {α : Type u} → m ◾ → n α
 Decidable.casesOn : {p : Prop} → {motive : Decidable ◾ → Sort u} → Decidable ◾ → (◾ → motive ◾) → (◾ → motive ◾) → motive ◾
-Lean.getConstInfo : {m : Type → Type} → [inst : Monad m] → [inst : MonadEnv m] → [inst : MonadError m] → Name → m ConstantInfo
+Lean.getConstInfo : {m : Type → Type} → [Monad m] → [MonadEnv m] → [MonadError m] → Name → m ConstantInfo
 Lean.Meta.instMonadMetaM : Monad fun α =>
  Context → ST.Ref PUnit State → Core.Context → ST.Ref PUnit Core.State → PUnit → EStateM.Result Exception PUnit α
 Lean.Meta.inferType : Expr →
--- a/tests/lean/match1.lean.expected.out
+++ b/tests/lean/match1.lean.expected.out
@@ -48,4 +48,4 @@ fun x =>
  | x => 4 : Array Nat → Nat
 g.match_1.{u_1, u_2} {α : Type u_1} (motive : List α → Sort u_2) (x✝ : List α) (h_1 : (a : α) → motive [a])
  (h_2 : (x : List α) → motive x) : motive x✝
-fun e => nomatch e : Empty → False
+fun e => nomatch e : ∀ (e : Empty), False
--- a/tests/lean/precissues.lean.expected.out
+++ b/tests/lean/precissues.lean.expected.out
@@ -25,6 +25,6 @@ p ∧ ¬q : Prop
 ¬p = q : Prop
 ¬p = q : Prop
 id ¬p : Prop
-Nat → ∀ (a : Nat), a = a : Prop
+∀ (a a : Nat), a = a : Prop
 id.{u} {α : Sort u} (a : α) : α
 precissues.lean:41:10-41:14: error: unexpected token 'foo!'; expected command
--- a/tests/lean/run/1156.lean
+++ b/tests/lean/run/1156.lean
@@ -28,7 +28,7 @@ inductive Foo : Nat → Char → Prop
 info: inductive Ex2.Foo : Nat → Char → Prop
 number of parameters: 1
 constructors:
-Ex2.Foo.mk : ∀ (n : Nat), natToType n → ∀ (c : Char), Foo n c
+Ex2.Foo.mk : ∀ (n : Nat) (elem : natToType n) (c : Char), Foo n c
 -/
 #guard_msgs in
 #print Foo
--- a/tests/lean/run/1834.lean
+++ b/tests/lean/run/1834.lean
@@ -0,0 +1,144 @@
+/-!
+# Pretty print with `∀` instead of `→` when domain is type
+
+https://github.com/leanprover/lean4/issues/1834
+-/
+
+set_option linter.unusedVariables false
+
+/-!
+Tests of various pi types.
+-/
+section
+variable (α : Nat → Type) (p q : Prop) (P : Nat → Prop)
+
+-- default nondep
+/-- info: Nat → Nat : Type -/
+#guard_msgs in #check (i : Nat) → Nat
+-- implicit nondep
+/-- info: {i : Nat} → Nat : Type -/
+#guard_msgs in #check {i : Nat} → Nat
+-- instance implicit nondep
+/-- info: [Inhabited Nat] → Nat : Type -/
+#guard_msgs in #check [Inhabited Nat] → Nat
+-- default nondep, both prop
+/-- info: p → q : Prop -/
+#guard_msgs in #check (h : p) → q
+-- default nondep, only codomain prop
+/-- info: ∀ (i : Nat), p : Prop -/
+#guard_msgs in #check (i : Nat) → p
+-- implicit nondep, only codomain prop
+/-- info: ∀ {i : Nat}, p : Prop -/
+#guard_msgs in #check {i : Nat} → p
+-- instance implicit nondep, only codomain prop, hygienic name
+/-- info: ∀ [Inhabited Nat], p : Prop -/
+#guard_msgs in #check [Inhabited Nat] → p
+-- instance implicit nondep, only codomain prop, user-provided name
+/-- info: ∀ [instNat : Inhabited Nat], p : Prop -/
+#guard_msgs in #check [instNat : Inhabited Nat] → p
+-- default dep
+/-- info: (i : Nat) → α i : Type -/
+#guard_msgs in #check (i : Nat) → α i
+-- implicit dep
+/-- info: {i : Nat} → α i : Type -/
+#guard_msgs in #check {i : Nat} → α i
+-- instance implicit dep
+/-- info: [inst : Inhabited Nat] → α default : Type -/
+#guard_msgs in #check [Inhabited Nat] → α default
+-- default dep, codomain prop
+/-- info: ∀ (i : Nat), P i : Prop -/
+#guard_msgs in #check (i : Nat) → P i
+-- implicit dep, codomain prop
+/-- info: ∀ {i : Nat}, P i : Prop -/
+#guard_msgs in #check {i : Nat} → P i
+-- instance implicit dep, codomain prop, hygienic name
+/-- info: ∀ [inst : Inhabited Nat], P default : Prop -/
+#guard_msgs in #check [Inhabited Nat] → P default
+-- instance implicit dep, codomain prop, user-provided name
+/-- info: ∀ [instNat : Inhabited Nat], P default : Prop -/
+#guard_msgs in #check [instNat : Inhabited Nat] → P default
+
+-- Same tests but with `pp.foralls` set to false.
+set_option pp.foralls false
+
+-- default nondep
+/-- info: Nat → Nat : Type -/
+#guard_msgs in #check (i : Nat) → Nat
+-- implicit nondep
+/-- info: {i : Nat} → Nat : Type -/
+#guard_msgs in #check {i : Nat} → Nat
+-- default nondep, both prop
+/-- info: p → q : Prop -/
+#guard_msgs in #check (h : p) → q
+-- default nondep, only codomain prop
+/-- info: Nat → p : Prop -/
+#guard_msgs in #check (i : Nat) → p
+-- default dep
+/-- info: (i : Nat) → α i : Type -/
+#guard_msgs in #check (i : Nat) → α i
+-- implicit dep
+/-- info: {i : Nat} → α i : Type -/
+#guard_msgs in #check {i : Nat} → α i
+-- default dep, codomain prop
+/-- info: (i : Nat) → P i : Prop -/
+#guard_msgs in #check (i : Nat) → P i
+-- implicit dep, codomain prop
+/-- info: {i : Nat} → P i : Prop -/
+#guard_msgs in #check {i : Nat} → P i
+-- implicit nondep, only codomain prop
+/-- info: {i : Nat} → p : Prop -/
+#guard_msgs in #check {i : Nat} → p
+end
+
+/-!
+Rewrote forall, remains a forall, since domain is `Nat`.
+-/
+/--
+info: P : Nat → Prop
+q : Prop
+h : ∀ (n : Nat), P n = q
+hq : q
+⊢ ∀ (n : Nat), q
+-/
+#guard_msgs in
+example (P : Nat → Prop) (q : Prop) (h : ∀ n, P n = q) (hq : q) :
+    ∀ n, P n := by
+  conv => enter [n]; rw [h]
+  trace_state
+  exact fun _ => hq
+
+/-!
+When `pp.foralls` is false, uses non-dependent `→`.
+-/
+/--
+info: P : Nat → Prop
+q : Prop
+h : (n : Nat) → P n = q
+hq : q
+⊢ Nat → q
+-/
+#guard_msgs in
+set_option pp.foralls false in
+example (P : Nat → Prop) (q : Prop) (h : ∀ n, P n = q) (hq : q) :
+    ∀ n, P n := by
+  conv => enter [n]; rw [h]
+  trace_state
+  exact fun _ => hq
+
+/-!
+Rewrote forall, turns into an implication, since domain is a proposition.
+-/
+/--
+info: p : Prop
+P : p → Prop
+q : Prop
+h : ∀ (n : p), P n = q
+hq : q
+⊢ p → q
+-/
+#guard_msgs in
+example (p : Prop) (P : p → Prop) (q : Prop) (h : ∀ n, P n = q) (hq : q) :
+    ∀ n, P n := by
+  conv => enter [n]; rw [h]
+  trace_state
+  exact fun _ => hq
--- a/tests/lean/run/4365.lean
+++ b/tests/lean/run/4365.lean
@@ -26,7 +26,7 @@ info: fun {α} => id (id sorry) : {α : Sort u} → α

 /--
 error: numerals are data in Lean, but the expected type is a proposition
-  Nat → True : Prop
+  ∀ (n : Nat), True : Prop
 -/
 #guard_msgs in
 #check (1 : ∀ (n : Nat), True)
--- a/tests/lean/run/funind_tests.lean
+++ b/tests/lean/run/funind_tests.lean
@@ -545,7 +545,7 @@ termination_by xs => xs

 /--
 info: LetFun.bar.induct.{u_1} {α : Type u_1} (x : α) (motive : List α → Prop) (case1 : motive [])
-  (case2 : ∀ (_y : α) (ys : List α), Nat → motive ys → motive (_y :: ys)) (a✝ : List α) : motive a✝
+  (case2 : ∀ (_y : α) (ys : List α) (this : Nat), motive ys → motive (_y :: ys)) (a✝ : List α) : motive a✝
 -/
 #guard_msgs in
 #check bar.induct
--- a/tests/lean/run/genindices.lean
+++ b/tests/lean/run/genindices.lean
@@ -25,7 +25,7 @@ pure ()
 set_option trace.Elab true

 /--
-info: [Elab] ⊢ ∀ (α : Type u) (xs : List (List α)), Pred (List α) xs → xs ≠ [] → xs = xs
+info: [Elab] ⊢ ∀ (α : Type u) (xs : List (List α)) (h : Pred (List α) xs), xs ≠ [] → xs = xs
 [Elab] α✝ : Type u
    xs✝ : List (List α✝)
    h✝ : Pred (List α✝) xs✝
--- a/tests/lean/run/print_cmd.lean
+++ b/tests/lean/run/print_cmd.lean
@@ -17,7 +17,7 @@ fun α [self : Inhabited α] => self.1
 -/
 #guard_msgs in #print default
 /--
-info: protected def ReaderT.read.{u, v} : {ρ : Type u} → {m : Type u → Type v} → [inst : Monad m] → ReaderT ρ m ρ :=
+info: protected def ReaderT.read.{u, v} : {ρ : Type u} → {m : Type u → Type v} → [Monad m] → ReaderT ρ m ρ :=
 fun {ρ} {m} [Monad m] => pure
 -/
 #guard_msgs in #print ReaderT.read
--- a/tests/lean/sanitychecks.lean.expected.out
+++ b/tests/lean/sanitychecks.lean.expected.out
@@ -14,7 +14,7 @@ Additional diagnostic information may be available using the `set_option diagnos
 sanitychecks.lean:18:12-18:20: error: invalid use of 'partial', 'Foo.unsound3' is not a function
  False
 sanitychecks.lean:20:0-20:54: error: failed to compile 'partial' definition 'Foo.unsound4', could not prove that the type
-  Unit → False
+  ∀ (x : Unit), False
 is nonempty.

 This process uses multiple strategies:
--- a/tests/lean/synthorder.lean.expected.out
+++ b/tests/lean/synthorder.lean.expected.out
@@ -1,7 +1,7 @@
 synthorder.lean:4:0-4:40: error: instance does not provide concrete values for (semi-)out-params
  Foo A (B × ?C)
 synthorder.lean:7:0-7:38: error: cannot find synthesization order for instance @instFooNat with type
-  {A : Type} → [inst : Foo A Nat] → Foo Nat A
+  {A : Type} → [Foo A Nat] → Foo Nat A
 all remaining arguments have metavariables:
  Foo ?A Nat
 [Meta.synthOrder] synthesizing the arguments of @instFoo in the order [3, 4]: