fix: fixes #1571

The previous implementation was using the following heuristic
```lean
      -- heuristic: use non-dependent arrows only if possible for whole group to avoid
      -- noisy mix like `(α : Type) → Type → (γ : Type) → ...`.
      let dependent := curNames.any fun n => hasIdent n.getId stxBody
```
The result produced by this heuristic was **not** producing an
accidental name capture, but I agree
it was confusing to have `∀ (a : True), ∃ a, a = a : Prop` instead of
`True → ∃ a, a = a : Prop` since there is no dependency.
AFAICT, all examples affected by this commit have a better output now.

cc @digma0 @kha

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -550,9 +550,29 @@ def delabLam : Delab :=
       | `(fun $binderGroups* => $stxBody) => `(fun $group $binderGroups* => $stxBody)
       | _                                 => `(fun $group => $stxBody)
 
+/--
+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
+  let dep := !(← getExpr).isArrow
+  if !curNames.isEmpty && dep != curDep then
+    -- don't group
+    delabGroup curNames curDep (← delab)
+  else
+    let curDep := dep
+    if ← shouldGroupWithNext then
+      -- group with nested binder => recurse immediately
+      withBindingBodyUnusedName fun stxN => delabForallBinders delabGroup (curNames.push stxN) curDep
+    else
+      -- don't group => delab body and prepend current binder group
+      let (stx, stxN) ← withBindingBodyUnusedName fun stxN => return (← delab, stxN)
+      delabGroup (curNames.push stxN) curDep stx
+
 @[builtinDelab forallE]
-def delabForall : Delab :=
-  delabBinders fun curNames stxBody => do
+def delabForall : Delab := do
+  delabForallBinders fun curNames dependent stxBody => do
     let e ← getExpr
     let prop ← try isProp e catch _ => pure false
     let stxT ← withBindingDomain delab
@@ -562,9 +582,6 @@ def delabForall : Delab :=
     -- here `curNames.size == 1`
     | BinderInfo.instImplicit   => `(bracketedBinderF|[$curNames.back : $stxT])
     | _                         =>
-      -- heuristic: use non-dependent arrows only if possible for whole group to avoid
-      -- noisy mix like `(α : Type) → Type → (γ : Type) → ...`.
-      let dependent := curNames.any fun n => hasIdent n.getId stxBody
       -- NOTE: non-dependent arrows are available only for the default binder info
       if dependent then
         if prop && !(← getPPOption getPPPiBinderTypes) then

tests/lean/1571.lean

@@ -0,0 +1,5 @@
+#check True → (∃ a : Nat, a = a)
+-- True → ∃ a, a = a : Prop
+
+#check True → (∃ b : Nat, b = b)
+-- True → ∃ b, b = b : Prop

tests/lean/1571.lean.expected.out

@@ -0,0 +1,2 @@
+True → ∃ a, a = a : Prop
+True → ∃ b, b = b : Prop

tests/lean/815b.lean.expected.out

@@ -141,7 +141,7 @@
           IsSmooth fun g => g
         Transformer
           fun redf a => redf
-  [Meta.synthInstance.resume] propagating ∀ (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] size: 2
   [Meta.synthInstance.resume] propagating ∀ (a : α),
@@ -155,10 +155,10 @@
           IsSmooth fun g => g
         Transformer
           fun redf a => redf
-  [Meta.synthInstance.resume] propagating ∀ (a : α),
+  [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: 8
-  [Meta.synthInstance.resume] propagating ∀ (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] size: 5
   [Meta.synthInstance.resume] propagating ∀ (a : α),

tests/lean/PPRoundtrip.lean.expected.out

@@ -30,7 +30,8 @@ fun {α}
     a =>
   @toString α inst a
 (α : Type) → α
-(α β : Type) → α
+(α : Type) →
+  Type → α
 Type → Type → Type
 (α : Type) → α → α
 {α : Type} → α

tests/lean/autoIssue.lean.expected.out

@@ -5,7 +5,7 @@ this : z.x = 1
 z : A
 this : z.x = 1
 ⊢ z.x = 1
-@A.rec : {motive : A → Sort u_1} → ((x : Nat) → x = 1 → motive (A.mk x)) → (t : A) → motive t
+@A.rec : {motive : A → Sort u_1} → ((x : Nat) → (a' : x = 1) → motive (A.mk x)) → (t : A) → motive t
 z : A
 x : Nat
 a' : x = 1

tests/lean/congrThm.lean.expected.out

@@ -1,8 +1,8 @@
 ∀ (p p_1 : Prop),
   p = p_1 →
-    ∀ {inst : Decidable p} {inst_1 : Decidable p_1} (a a_1 : Nat),
-      a = a_1 → ∀ (h : a > 0), g p a h = g p_1 a_1 (_ : a_1 > 0)
+    ∀ {inst : Decidable p} {inst_1 : Decidable p_1} (a a_1 : Nat) (e_3 : a = a_1) (h : a > 0),
+      g p a h = g p_1 a_1 (_ : a_1 > 0)
 ∀ (p p_1 : Prop),
   p = p_1 →
-    ∀ {inst : Decidable p} [inst_1 : Decidable p_1] (a a_1 : Nat),
-      a = a_1 → ∀ (h : a > 0), g p a h = g p_1 a_1 (_ : a_1 > 0)
+    ∀ {inst : Decidable p} [inst_1 : Decidable p_1] (a a_1 : Nat) (e_3 : a = a_1) (h : a > 0),
+      g p a h = g p_1 a_1 (_ : a_1 > 0)

tests/lean/congrThmIssue.lean.expected.out

@@ -4,7 +4,7 @@ cap : Nat
 backing : Fin cap → Option α
 size : Nat
 h_size : size ≤ cap
-h_full : ∀ (i : Nat), i < size → Option.isSome (backing { val := i, isLt := (_ : i < cap) }) = true
+h_full : ∀ (i : Nat) (h : i < size), Option.isSome (backing { val := i, isLt := (_ : i < cap) }) = true
 i : Nat
 h : i < size
 ⊢ Option.isSome

tests/lean/ppMotives.lean.expected.out

@@ -11,7 +11,7 @@ protected def Nat.add : Nat → Nat → Nat :=
 fun x x_1 =>
   Nat.brecOn (motive := fun x => Nat → Nat) x_1
     (fun x f x_2 =>
-      (match (motive := (x x : Nat) → Nat.below (motive := fun x => Nat → Nat) x → Nat) x_2, x with
+      (match (motive := Nat → (x : Nat) → Nat.below (motive := fun x => Nat → Nat) x → Nat) x_2, x with
         | a, Nat.zero => fun x => a
         | a, Nat.succ b => fun x => Nat.succ (PProd.fst x.fst a))
         f)

tests/lean/precissues.lean.expected.out

@@ -25,6 +25,6 @@ p ∧ ¬q : Prop
 ¬p = q : Prop
 ¬p = q : Prop
 id ¬p : Prop
-∀ (a a : Nat), a = a : Prop
+Nat → ∀ (a : Nat), a = a : Prop
 id : ?m → ?m
 precissues.lean:41:10: error: expected command