move dependent params to left of colon

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -1279,7 +1279,7 @@ where
       -- but this would be the usual case.
       let group ← withBindingDomain do `(bracketedBinderF|[$(← delabTy)])
       withBindingBody e.bindingName! <| delabParams bindingNames idStx (groups.push group)
-    else if e.isForall && !e.bindingName!.hasMacroScopes && !bindingNames.contains e.bindingName! then
+    else if e.isForall && (!e.isArrow || !(e.bindingName!.hasMacroScopes || bindingNames.contains e.bindingName!)) then
       delabParamsAux bindingNames idStx groups #[]
     else
       let (opts', e') ← processSpine {} (← readThe SubExpr)
@@ -1295,6 +1295,7 @@ where
   -/
   delabParamsAux (bindingNames : NameSet) (idStx : Ident) (groups : TSyntaxArray ``bracketedBinder) (curIds : Array Ident) := do
     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⟩
@@ -1320,10 +1321,11 @@ where
   -/
   shouldGroupWithNext (bindingNames : NameSet) (e e' : Expr) : Bool :=
     e'.isForall &&
-    -- At the first sign of an inaccessible name, stop merging binders:
-    !e'.bindingName!.hasMacroScopes &&
-    -- If it's a name that has already been used, stop merging binders:
-    !bindingNames.contains e'.bindingName! &&
+    (!e'.isArrow ||
+      -- At the first sign of an inaccessible name, stop merging binders:
+    !(e'.bindingName!.hasMacroScopes ||
+      -- If it's a name that has already been used, stop merging binders:
+      bindingNames.contains e'.bindingName!)) &&
     e.binderInfo == e'.binderInfo &&
     e.bindingDomain! == e'.bindingDomain! &&
     -- Inst implicits can't be grouped:

tests/lean/autoImplicitChainNameIssue.lean.expected.out

@@ -3,4 +3,4 @@ case nil
 α✝ : Type u_1
 as : List α✝
 ⊢ Palindrome [].reverse
-palindrome_reverse.{u_1} : ∀ {α✝ : Type u_1} {as : List α✝} (h : Palindrome as), Palindrome as.reverse
+palindrome_reverse.{u_1} {α✝ : Type u_1} {as : List α✝} (h : Palindrome as) : Palindrome as.reverse

tests/lean/match1.lean.expected.out

@@ -46,6 +46,6 @@ fun x =>
   | #[] => 0
   | #[3, 4, 5] => 3
   | 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✝
+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

tests/lean/run/2846.lean

@@ -34,7 +34,7 @@ The second is made hygienic.
 -/
 def foo (n n : Nat) : Fin (n + 1) := 0
 
-/-- info: foo (n : Nat) : (n✝ : Nat) → Fin (n✝ + 1) -/
+/-- info: foo (n n✝ : Nat) : Fin (n✝ + 1) -/
 #guard_msgs in #check foo
 
 /-!
@@ -43,11 +43,11 @@ Same, but a named argument still follows, and its name is preserved.
 
 def foo' (n n : Nat) (a : Fin ((by clear n; exact n) + 1)) : Fin (n + 1) := 0
 
-/-- info: foo' (n : Nat) : (n✝ : Nat) → (a : Fin (n + 1)) → Fin (n✝ + 1) -/
+/-- info: foo' (n n✝ : Nat) (a : Fin (n + 1)) : Fin (n✝ + 1) -/
 #guard_msgs in #check foo'
 
 /-!
-Named argument after inaccessible name, still stays after the colon.
+Named argument after non-dependent inaccessible name, still stays after the colon.
 Prints with named pi notation.
 -/
 def foo'' : String → (needle : String) → String := fun _ yo => yo
@@ -57,12 +57,12 @@ def foo'' : String → (needle : String) → String := fun _ yo => yo
 
 /-!
 Named argument after inaccessible name that's still a dependent argument.
-Stays after the colon, and the names are grouped.
+Stays before the colon, and the names are grouped.
 -/
 
 def foo''' : (_ : Nat) → (n : Nat) → Fin (n + by clear n; assumption) := sorry
 
-/-- info: foo''' : (x✝ n : Nat) → Fin (n + x✝) -/
+/-- info: foo''' (x✝ n : Nat) : Fin (n + x✝) -/
 #guard_msgs in #check foo'''
 
 /-!

tests/lean/run/4320.lean

@@ -8,7 +8,7 @@ def many_map {α β : Type} (f : α → β) : Many α → Many β
 
 /--
 info: many_map.induct {α β : Type} (f : α → β) (motive : Many α → Prop) (case1 : motive Many.none)
-  (case2 : ∀ (x : α) (xs : Unit → Many α), motive (xs ()) → motive (Many.more x xs)) : ∀ (a✝ : Many α), motive a✝
+  (case2 : ∀ (x : α) (xs : Unit → Many α), motive (xs ()) → motive (Many.more x xs)) (a✝ : Many α) : motive a✝
 -/
 #guard_msgs in
 #check many_map.induct

tests/lean/run/974.lean

@@ -11,23 +11,23 @@ def Formula.count_quantifiers : {n:Nat} → Formula n → Nat
 attribute [simp] Formula.count_quantifiers
 
 /--
-info: Formula.count_quantifiers.eq_1.{u_1} :
-  ∀ (x✝ : Nat) (f₁ f₂ : Formula x✝), (f₁.imp f₂).count_quantifiers = f₁.count_quantifiers + f₂.count_quantifiers
+info: Formula.count_quantifiers.eq_1.{u_1} (x✝ : Nat) (f₁ f₂ : Formula x✝) :
+  (f₁.imp f₂).count_quantifiers = f₁.count_quantifiers + f₂.count_quantifiers
 -/
 #guard_msgs in
 #check Formula.count_quantifiers.eq_1
 
 /--
-info: Formula.count_quantifiers.eq_2.{u_1} :
-  ∀ (x✝ : Nat) (f : Formula (x✝ + 1)), f.all.count_quantifiers = f.count_quantifiers + 1
+info: Formula.count_quantifiers.eq_2.{u_1} (x✝ : Nat) (f : Formula (x✝ + 1)) :
+  f.all.count_quantifiers = f.count_quantifiers + 1
 -/
 #guard_msgs in
 #check Formula.count_quantifiers.eq_2
 
 /--
-info: Formula.count_quantifiers.eq_3.{u_1} :
-  ∀ (x✝ : Nat) (x✝¹ : Formula x✝) (x_4 : ∀ (f₁ f₂ : Formula x✝), x✝¹ = f₁.imp f₂ → False)
-    (x_5 : ∀ (f : Formula (x✝ + 1)), x✝¹ = f.all → False), x✝¹.count_quantifiers = 0
+info: Formula.count_quantifiers.eq_3.{u_1} (x✝ : Nat) (x✝¹ : Formula x✝)
+  (x_4 : ∀ (f₁ f₂ : Formula x✝), x✝¹ = f₁.imp f₂ → False) (x_5 : ∀ (f : Formula (x✝ + 1)), x✝¹ = f.all → False) :
+  x✝¹.count_quantifiers = 0
 -/
 #guard_msgs in
 #check Formula.count_quantifiers.eq_3

tests/lean/run/eqnsPrio.lean

@@ -11,15 +11,13 @@ def foo : Bool → Nat → Nat
   | _, n+1 => foo .false n
 termination_by _ n => n
 
-/-- info: foo.eq_1 : ∀ (x✝ : Bool), foo x✝ 0 = 0 -/
+/-- info: foo.eq_1 (x✝ : Bool) : foo x✝ 0 = 0 -/
 #guard_msgs in
 #check foo.eq_1
 /-- info: foo.eq_2 (n : Nat) : foo true n.succ = foo true n -/
 #guard_msgs in
 #check foo.eq_2
-/--
-info: foo.eq_3 : ∀ (x✝ : Bool) (n : Nat) (x_3 : x✝ = true → False), foo x✝ n.succ = foo false n
--/
+/-- info: foo.eq_3 (x✝ : Bool) (n : Nat) (x_3 : x✝ = true → False) : foo x✝ n.succ = foo false n -/
 #guard_msgs in
 #check foo.eq_3
 

tests/lean/run/funind_demo.lean

@@ -8,8 +8,8 @@ def ackermann : Nat → Nat → Nat
 /--
 info: ackermann.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m)
   (case2 : ∀ (n : Nat), motive n 1 → motive n.succ 0)
-  (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive n.succ m.succ) :
-  ∀ (a✝ a✝¹ : Nat), motive a✝ a✝¹
+  (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive n.succ m.succ) (a✝ a✝¹ : Nat) :
+  motive a✝ a✝¹
 -/
 #guard_msgs in
 #check ackermann.induct
@@ -19,7 +19,7 @@ def Tree.rev : Tree → Tree | node ts => .node (ts.attach.map (fun ⟨t, _ht⟩
 
 /--
 info: Tree.rev.induct (motive : Tree → Prop)
-  (case1 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive t) → motive (Tree.node ts)) : ∀ (a✝ : Tree), motive a✝
+  (case1 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive t) → motive (Tree.node ts)) (a✝ : Tree) : motive a✝
 -/
 #guard_msgs in
 #check Tree.rev.induct

tests/lean/run/funind_fewer_levels.lean

@@ -10,8 +10,8 @@ def foo.{u} : Nat → PUnit.{u}
 | n+1 => foo n
 
 /--
-info: Structural.foo.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ) :
-  ∀ (a✝ : Nat), motive a✝
+info: Structural.foo.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ)
+  (a✝ : Nat) : motive a✝
 -/
 #guard_msgs in
 #check foo.induct
@@ -31,7 +31,7 @@ termination_by xs => xs
 
 /--
 info: WellFounded.foo.induct.{v} {α : Type v} (motive : List α → Prop) (case1 : motive [])
-  (case2 : ∀ (head : α) (xs : List α), motive xs → motive (head :: xs)) : ∀ (a✝ : List α), motive a✝
+  (case2 : ∀ (head : α) (xs : List α), motive xs → motive (head :: xs)) (a✝ : List α) : motive a✝
 -/
 #guard_msgs in
 #check foo.induct
@@ -58,7 +58,7 @@ end
 
 /--
 info: Mutual.foo.induct (motive1 motive2 : Nat → Prop) (case1 : motive1 0) (case2 : ∀ (n : Nat), motive2 n → motive1 n.succ)
-  (case3 : motive2 0) (case4 : ∀ (n : Nat), motive1 n → motive2 n.succ) : ∀ (a✝ : Nat), motive1 a✝
+  (case3 : motive2 0) (case4 : ∀ (n : Nat), motive1 n → motive2 n.succ) (a✝ : Nat) : motive1 a✝
 -/
 #guard_msgs in
 #check foo.induct

tests/lean/run/funind_proof.lean

@@ -35,7 +35,7 @@ info: Term.replaceConst.induct (a b : String) (motive1 : Term → Prop) (motive2
   (case1 : ∀ (a_1 : String), (a == a_1) = true → motive1 (const a_1))
   (case2 : ∀ (a_1 : String), ¬(a == a_1) = true → motive1 (const a_1))
   (case3 : ∀ (a : String) (cs : List Term), motive2 cs → motive1 (app a cs)) (case4 : motive2 [])
-  (case5 : ∀ (c : Term) (cs : List Term), motive1 c → motive2 cs → motive2 (c :: cs)) : ∀ (a✝ : Term), motive1 a✝
+  (case5 : ∀ (c : Term) (cs : List Term), motive1 c → motive2 cs → motive2 (c :: cs)) (a✝ : Term) : motive1 a✝
 -/
 #guard_msgs in
 #check replaceConst.induct

tests/lean/run/funind_structural.lean

@@ -11,7 +11,7 @@ termination_by structural x => x
 
 /--
 info: fib.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1)
-  (case3 : ∀ (n : Nat), motive n → motive (n + 1) → motive n.succ.succ) : ∀ (a✝ : Nat), motive a✝
+  (case3 : ∀ (n : Nat), motive n → motive (n + 1) → motive n.succ.succ) (a✝ : Nat) : motive a✝
 -/
 #guard_msgs in
 #check fib.induct
@@ -24,8 +24,8 @@ termination_by structural x => x
 
 /--
 info: binary.induct (motive : Nat → Nat → Prop) (case1 : ∀ (acc : Nat), motive 0 acc) (case2 : ∀ (acc : Nat), motive 1 acc)
-  (case3 : ∀ (n acc : Nat), motive (n + 1) acc → motive n (binary (n + 1) acc) → motive n.succ.succ acc) :
-  ∀ (a✝ a✝¹ : Nat), motive a✝ a✝¹
+  (case3 : ∀ (n acc : Nat), motive (n + 1) acc → motive n (binary (n + 1) acc) → motive n.succ.succ acc)
+  (a✝ a✝¹ : Nat) : motive a✝ a✝¹
 -/
 #guard_msgs in
 #check binary.induct
@@ -40,8 +40,8 @@ termination_by structural _ x => x
 /--
 info: binary'.induct (motive : Bool → Nat → Prop) (case1 : ∀ (acc : Bool), motive acc 0)
   (case2 : ∀ (acc : Bool), motive acc 1)
-  (case3 : ∀ (acc : Bool) (n : Nat), motive acc (n + 1) → motive (binary' acc (n + 1)) n → motive acc n.succ.succ) :
-  ∀ (a✝ : Bool) (a✝¹ : Nat), motive a✝ a✝¹
+  (case3 : ∀ (acc : Bool) (n : Nat), motive acc (n + 1) → motive (binary' acc (n + 1)) n → motive acc n.succ.succ)
+  (a✝ : Bool) (a✝¹ : Nat) : motive a✝ a✝¹
 -/
 #guard_msgs in
 #check binary'.induct
@@ -55,8 +55,8 @@ termination_by structural x => x
 /--
 info: zip.induct.{u_1, u_2} {α : Type u_1} {β : Type u_2} (motive : List α → List β → Prop)
   (case1 : ∀ (x : List β), motive [] x) (case2 : ∀ (t : List α), (t = [] → False) → motive t [])
-  (case3 : ∀ (x : α) (xs : List α) (y : β) (ys : List β), motive xs ys → motive (x :: xs) (y :: ys)) :
-  ∀ (a✝ : List α) (a✝¹ : List β), motive a✝ a✝¹
+  (case3 : ∀ (x : α) (xs : List α) (y : β) (ys : List β), motive xs ys → motive (x :: xs) (y :: ys)) (a✝ : List α)
+  (a✝¹ : List β) : motive a✝ a✝¹
 -/
 #guard_msgs in
 #check zip.induct
@@ -94,7 +94,7 @@ info: Finn.min.induct (motive : Bool → {n : Nat} → Nat → Finn n → Finn n
   (case1 : ∀ (x : Bool) (m n : Nat) (x_1 : Finn n), motive x m Finn.fzero x_1)
   (case2 : ∀ (x : Bool) (m n : Nat) (x_1 : Finn n), (x_1 = Finn.fzero → False) → motive x m x_1 Finn.fzero)
   (case3 : ∀ (x : Bool) (m n : Nat) (i j : Finn n), motive (!x) (m + 1) i j → motive x m i.fsucc j.fsucc) (x : Bool)
-  {n : Nat} (m : Nat) : ∀ (a✝ f : Finn n), motive x m a✝ f
+  {n : Nat} (m : Nat) (a✝ f : Finn n) : motive x m a✝ f
 -/
 #guard_msgs in
 #check Finn.min.induct
@@ -195,7 +195,7 @@ info: TermDenote.Term.denote.induct (motive : {ctx : List Ty} → {ty : Ty} →
   (case6 :
     ∀ (a : List Ty) (ty ty₁ : Ty) (a_1 : Term a ty₁) (b : Term (ty₁ :: a) ty) (env : HList Ty.denote a),
       motive a_1 env → motive b (HList.cons (a_1.denote env) env) → motive (a_1.let b) env)
-  {ctx : List Ty} {ty : Ty} : ∀ (a✝ : Term ctx ty) (a✝¹ : HList Ty.denote ctx), motive a✝ a✝¹
+  {ctx : List Ty} {ty : Ty} (a✝ : Term ctx ty) (a✝¹ : HList Ty.denote ctx) : motive a✝ a✝¹
 -/
 #guard_msgs in
 #check TermDenote.Term.denote.induct

tests/lean/run/funind_structural_mutual.lean

@@ -25,8 +25,8 @@ end
 info: Tree.size.induct.{u_1} {α : Type u_1} (motive_1 : Tree α → Prop) (motive_2 : List (Tree α) → Prop)
   (case1 :
     ∀ (a : α) (tsf : Bool → List (Tree α)), motive_2 (tsf true) → motive_2 (tsf false) → motive_1 (Tree.node a tsf))
-  (case2 : motive_2 []) (case3 : ∀ (t : Tree α) (ts : List (Tree α)), motive_1 t → motive_2 ts → motive_2 (t :: ts)) :
-  ∀ (a✝ : Tree α), motive_1 a✝
+  (case2 : motive_2 []) (case3 : ∀ (t : Tree α) (ts : List (Tree α)), motive_1 t → motive_2 ts → motive_2 (t :: ts))
+  (a✝ : Tree α) : motive_1 a✝
 -/
 #guard_msgs in
 #check Tree.size.induct