diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index b34c32b4e4..101c17d4f5 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -1082,41 +1082,85 @@ private unsafe def evalSyntaxConstantUnsafe (env : Environment) (opts : Options)
 @[implemented_by evalSyntaxConstantUnsafe]
 private opaque evalSyntaxConstant (env : Environment) (opts : Options) (constName : Name) : ExceptT String Id Syntax := throw ""
 
-/-- Pretty-prints a constant `c` as `c.{<levels>} <params> : <type>`. -/
-partial def delabConstWithSignature : Delab := do
+/--
+Pretty-prints a constant `c` as `c.{<levels>} <params> : <type>`.
+
+If `universes` is `false`, then the universe level parameters are omitted.
+-/
+partial def delabConstWithSignature (universes : Bool := true) : Delab := do
   let e ← getExpr
   -- use virtual expression node of arity 2 to separate name and type info
   let idStx ← descend e 0 <|
-    withOptions (pp.universes.set · true |> (pp.fullNames.set · true)) <|
+    withOptions (pp.universes.set · universes |> (pp.fullNames.set · true)) <|
       delabConst
   descend (← inferType e) 1 <|
-    delabParams idStx #[] #[]
+    delabParams {} idStx #[]
 where
-  -- follows `delabBinders`, but does not uniquify binder names and accumulates all binder groups
-  delabParams (idStx : Ident) (groups : TSyntaxArray ``bracketedBinder) (curIds : Array Ident) := do
-    if let .forallE n d _ i ← getExpr then
-      let stxN ← annotateCurPos (mkIdent n)
-      let curIds := curIds.push ⟨stxN⟩
-      if ← shouldGroupWithNext then
-        withBindingBody n <| delabParams idStx groups curIds
-      else
-        let delabTy := withOptions (pp.piBinderTypes.set · true) delab
-        let group ← withBindingDomain do
-          match i with
-          | .implicit       => `(bracketedBinderF|{$curIds* : $(← delabTy)})
-          | .strictImplicit => `(bracketedBinderF|⦃$curIds* : $(← delabTy)⦄)
-          | .instImplicit   => `(bracketedBinderF|[$curIds.back : $(← delabTy)])
-          | _ =>
-            if d.isOptParam then
-              `(bracketedBinderF|($curIds* : $(← withAppFn <| withAppArg delabTy) := $(← withAppArg delabTy)))
-            else if let some (.const tacticDecl _) := d.getAutoParamTactic? then
-              let tacticSyntax ← ofExcept <| evalSyntaxConstant (← getEnv) (← getOptions) tacticDecl
-              `(bracketedBinderF|($curIds* : $(← withAppFn <| withAppArg delabTy) := by $tacticSyntax))
-            else
-              `(bracketedBinderF|($curIds* : $(← delabTy)))
-        withBindingBody n <| delabParams idStx (groups.push group) #[]
+  /--
+  For types in the signature, we want to be sure pi binder types are pretty printed.
+  -/
+  delabTy : DelabM Term := withOptions (pp.piBinderTypes.set · true) delab
+  /-
+  Similar to `delabBinders`, but does not uniquify binder names (since for named arguments we want to know the name),
+  and it always merges binder groups when possible.
+  Once it reaches a binder with an inaccessible name, or a name that has already been used,
+  the remaining binders appear in pi types after the `:` of the declaration.
+  -/
+  delabParams (bindingNames : NameSet) (idStx : Ident) (groups : TSyntaxArray ``bracketedBinder) := do
+    let e ← getExpr
+    if e.isForall && e.binderInfo.isInstImplicit && e.bindingName!.hasMacroScopes then
+      -- Assumption: this instance can be found by instance search, so it does not need to be named.
+      -- The oversight here is that this inaccessible name can appear in the pretty printed expression.
+      -- We could check to see whether the instance appears in the type and avoid omitting the instance name,
+      -- 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
+      delabParamsAux bindingNames idStx groups #[]
     else
-      let type ← delab
+      let type ← delabTy
       `(declSigWithId| $idStx:ident $groups* : $type)
+  /--
+  Inner loop for `delabParams`, collecting binders.
+  Invariants:
+  - The current expression is a forall.
+  - It has a name that's not inaccessible.
+  - It has a name that hasn't been used yet.
+  -/
+  delabParamsAux (bindingNames : NameSet) (idStx : Ident) (groups : TSyntaxArray ``bracketedBinder) (curIds : Array Ident) := do
+    let e@(.forallE n d e' i) ← getExpr | unreachable!
+    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
+    else
+      let group ← withBindingDomain do
+        match i with
+        | .implicit       => `(bracketedBinderF|{$curIds* : $(← delabTy)})
+        | .strictImplicit => `(bracketedBinderF|⦃$curIds* : $(← delabTy)⦄)
+        | .instImplicit   => `(bracketedBinderF|[$stxN : $(← delabTy)])
+        | _ =>
+          if d.isOptParam then
+            `(bracketedBinderF|($curIds* : $(← withAppFn <| withAppArg delabTy) := $(← withAppArg delabTy)))
+          else if let some (.const tacticDecl _) := d.getAutoParamTactic? then
+            let tacticSyntax ← ofExcept <| evalSyntaxConstant (← getEnv) (← getOptions) tacticDecl
+            `(bracketedBinderF|($curIds* : $(← withAppFn <| withAppArg delabTy) := by $tacticSyntax))
+          else
+            `(bracketedBinderF|($curIds* : $(← delabTy)))
+      withBindingBody n <| 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.
+  -/
+  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.binderInfo == e'.binderInfo &&
+    e.bindingDomain! == e'.bindingDomain! &&
+    -- Inst implicits can't be grouped:
+    e'.binderInfo != BinderInfo.instImplicit
 
 end Lean.PrettyPrinter.Delaborator
diff --git a/tests/lean/1377.lean.expected.out b/tests/lean/1377.lean.expected.out
index b3ffd2cae8..b22940f237 100644
--- a/tests/lean/1377.lean.expected.out
+++ b/tests/lean/1377.lean.expected.out
@@ -1,2 +1,2 @@
 1377.lean:3:2-3:5: warning: declaration uses 'sorry'
-foo.bar (x✝ : Unit) {n : Nat} (a✝ : Fin n) : Fin n
+foo.bar : Unit → {n : Nat} → Fin n → Fin n
diff --git a/tests/lean/714.lean.expected.out b/tests/lean/714.lean.expected.out
index 3b2a4c4368..de9e1ff1be 100644
--- a/tests/lean/714.lean.expected.out
+++ b/tests/lean/714.lean.expected.out
@@ -1 +1 @@
-test {α : Type} [inst✝ : LT α] : Type
+test {α : Type} [LT α] : Type
diff --git a/tests/lean/974.lean.expected.out b/tests/lean/974.lean.expected.out
index 418dba1e98..afc0622e0a 100644
--- a/tests/lean/974.lean.expected.out
+++ b/tests/lean/974.lean.expected.out
@@ -1,7 +1,9 @@
-Formula.count_quantifiers._eq_1.{u_1} (x✝ : Nat) (f₁ f₂ : Formula x✝) :
-  Formula.count_quantifiers (Formula.imp f₁ f₂) = Formula.count_quantifiers f₁ + Formula.count_quantifiers f₂
-Formula.count_quantifiers._eq_2.{u_1} (x✝ : Nat) (f : Formula (x✝ + 1)) :
-  Formula.count_quantifiers (Formula.all f) = Formula.count_quantifiers f + 1
-Formula.count_quantifiers._eq_3.{u_1} (x✝ : Nat) (x✝¹ : Formula x✝)
-  (x_4 : ∀ (f₁ f₂ : Formula x✝), x✝¹ = Formula.imp f₁ f₂ → False)
-  (x_5 : ∀ (f : Formula (x✝ + 1)), x✝¹ = Formula.all f → False) : Formula.count_quantifiers x✝¹ = 0
+Formula.count_quantifiers._eq_1.{u_1} :
+  ∀ (x : Nat) (f₁ f₂ : Formula x),
+    Formula.count_quantifiers (Formula.imp f₁ f₂) = Formula.count_quantifiers f₁ + Formula.count_quantifiers f₂
+Formula.count_quantifiers._eq_2.{u_1} :
+  ∀ (x : Nat) (f : Formula (x + 1)), Formula.count_quantifiers (Formula.all f) = Formula.count_quantifiers f + 1
+Formula.count_quantifiers._eq_3.{u_1} :
+  ∀ (x : Nat) (x_1 : Formula x),
+    (∀ (f₁ f₂ : Formula x), x_1 = Formula.imp f₁ f₂ → False) →
+      (∀ (f : Formula (x + 1)), x_1 = Formula.all f → False) → Formula.count_quantifiers x_1 = 0
diff --git a/tests/lean/autoImplicitChainNameIssue.lean.expected.out b/tests/lean/autoImplicitChainNameIssue.lean.expected.out
index e68366ea75..e6b966055a 100644
--- a/tests/lean/autoImplicitChainNameIssue.lean.expected.out
+++ b/tests/lean/autoImplicitChainNameIssue.lean.expected.out
@@ -3,4 +3,4 @@ case nil
 α✝ : Type u_1
 as : List α✝
 ⊢ Palindrome (List.reverse [])
-palindrome_reverse.{u_1} {α✝ : Type u_1} {as : List α✝} (h : Palindrome as) : Palindrome (List.reverse as)
+palindrome_reverse.{u_1} : ∀ {α : Type u_1} {as : List α}, Palindrome as → Palindrome (List.reverse as)
diff --git a/tests/lean/interactive/hover.lean.expected.out b/tests/lean/interactive/hover.lean.expected.out
index 8b6baeb070..5437b2017f 100644
--- a/tests/lean/interactive/hover.lean.expected.out
+++ b/tests/lean/interactive/hover.lean.expected.out
@@ -120,7 +120,7 @@
  {"start": {"line": 73, "character": 38}, "end": {"line": 73, "character": 45}},
  "contents":
  {"value":
-  "```lean\nNat.add (a✝a✝¹ : Nat) : Nat\n```\n***\nAddition of natural numbers.\n\nThis definition is overridden in both the kernel and the compiler to efficiently\nevaluate using the \"bignum\" representation (see `Nat`). The definition provided\nhere is the logical model (and it is soundness-critical that they coincide).\n\n***\n*import Init.Prelude*",
+  "```lean\nNat.add : Nat → Nat → Nat\n```\n***\nAddition of natural numbers.\n\nThis definition is overridden in both the kernel and the compiler to efficiently\nevaluate using the \"bignum\" representation (see `Nat`). The definition provided\nhere is the logical model (and it is soundness-critical that they coincide).\n\n***\n*import Init.Prelude*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hover.lean"},
  "position": {"line": 77, "character": 10}}
@@ -620,7 +620,7 @@
   "end": {"line": 291, "character": 20}},
  "contents":
  {"value":
-  "```lean\nList.map.{u, v} {α : Type u} {β : Type v} (f : α → β) (a✝ : List α) : List β\n```\n***\n`O(|l|)`. `map f l` applies `f` to each element of the list.\n* `map f [a, b, c] = [f a, f b, f c]`\n\n***\n*import Init.Data.List.Basic*",
+  "```lean\nList.map.{u, v} {α : Type u} {β : Type v} (f : α → β) : List α → List β\n```\n***\n`O(|l|)`. `map f l` applies `f` to each element of the list.\n* `map f [a, b, c] = [f a, f b, f c]`\n\n***\n*import Init.Data.List.Basic*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hover.lean"},
  "position": {"line": 294, "character": 26}}
@@ -629,7 +629,7 @@
   "end": {"line": 294, "character": 29}},
  "contents":
  {"value":
-  "```lean\nList.zip.{u, v} {α : Type u} {β : Type v} (a✝ : List α) (a✝¹ : List β) : List (α × β)\n```\n***\n`O(min |xs| |ys|)`. Combines the two lists into a list of pairs, with one element from each list.\nThe longer list is truncated to match the shorter list.\n* `zip [x₁, x₂, x₃] [y₁, y₂, y₃, y₄] = [(x₁, y₁), (x₂, y₂), (x₃, y₃)]`\n\n***\n*import Init.Data.List.Basic*",
+  "```lean\nList.zip.{u, v} {α : Type u} {β : Type v} : List α → List β → List (α × β)\n```\n***\n`O(min |xs| |ys|)`. Combines the two lists into a list of pairs, with one element from each list.\nThe longer list is truncated to match the shorter list.\n* `zip [x₁, x₂, x₃] [y₁, y₂, y₃, y₄] = [(x₁, y₁), (x₂, y₂), (x₃, y₃)]`\n\n***\n*import Init.Data.List.Basic*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hover.lean"},
  "position": {"line": 294, "character": 19}}
@@ -638,5 +638,5 @@
   "end": {"line": 294, "character": 22}},
  "contents":
  {"value":
-  "```lean\nList.zip.{u, v} {α : Type u} {β : Type v} (a✝ : List α) (a✝¹ : List β) : List (α × β)\n```\n***\n`O(min |xs| |ys|)`. Combines the two lists into a list of pairs, with one element from each list.\nThe longer list is truncated to match the shorter list.\n* `zip [x₁, x₂, x₃] [y₁, y₂, y₃, y₄] = [(x₁, y₁), (x₂, y₂), (x₃, y₃)]`\n\n***\n*import Init.Data.List.Basic*",
+  "```lean\nList.zip.{u, v} {α : Type u} {β : Type v} : List α → List β → List (α × β)\n```\n***\n`O(min |xs| |ys|)`. Combines the two lists into a list of pairs, with one element from each list.\nThe longer list is truncated to match the shorter list.\n* `zip [x₁, x₂, x₃] [y₁, y₂, y₃, y₄] = [(x₁, y₁), (x₂, y₂), (x₃, y₃)]`\n\n***\n*import Init.Data.List.Basic*",
   "kind": "markdown"}}
diff --git a/tests/lean/levelNGen.lean.expected.out b/tests/lean/levelNGen.lean.expected.out
index 743e0c5919..927f2ce745 100644
--- a/tests/lean/levelNGen.lean.expected.out
+++ b/tests/lean/levelNGen.lean.expected.out
@@ -1,5 +1,5 @@
-test1.{u_1, u_2} {α : Sort u_2} (a✝ : α) : Sort u_1
+test1.{u_1, u_2} {α : Sort u_2} : α → Sort u_1
 levelNGen.lean:3:4-3:9: warning: declaration uses 'sorry'
-test2.{u_1, u_2} {α : Sort u_2} (a✝ : α) : Sort u_1
+test2.{u_1, u_2} {α : Sort u_2} : α → Sort u_1
 levelNGen.lean:5:33-5:38: warning: declaration uses 'sorry'
-test3.{u_1, u_2} {α : Sort u_2} (a✝ : α) : Sort u_1
+test3.{u_1, u_2} {α : Sort u_2} : α → Sort u_1
diff --git a/tests/lean/match1.lean.expected.out b/tests/lean/match1.lean.expected.out
index f7dab2aa43..7e2fbddbb4 100644
--- a/tests/lean/match1.lean.expected.out
+++ b/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 α) → ((a : α) → motive [a]) → ((x : List α) → motive x) → motive x
 fun e => nomatch e : Empty → False
diff --git a/tests/lean/namePatEqThm.lean.expected.out b/tests/lean/namePatEqThm.lean.expected.out
index 17bd2acfba..73e55b147d 100644
--- a/tests/lean/namePatEqThm.lean.expected.out
+++ b/tests/lean/namePatEqThm.lean.expected.out
@@ -2,5 +2,7 @@ iota._eq_1 : iota 0 = []
 iota._eq_2 (n : Nat) : iota (Nat.succ n) = Nat.succ n :: iota n
 f._eq_1 (x_1 y : Nat) : f [x_1, y] = ([x_1, y], [y])
 f._eq_2 (x_1 y : Nat) (zs : List Nat) (x_2 : zs = [] → False) : f (x_1 :: y :: zs) = f zs
-f._eq_3 (x✝ : List Nat) (x_2 : ∀ (x y : Nat), x✝ = [x, y] → False)
-  (x_3 : ∀ (x y : Nat) (zs : List Nat), x✝ = x :: y :: zs → False) : f x✝ = ([], [])
+f._eq_3 :
+  ∀ (x : List Nat),
+    (∀ (x_1 y : Nat), x = [x_1, y] → False) →
+      (∀ (x_1 y : Nat) (zs : List Nat), x = x_1 :: y :: zs → False) → f x = ([], [])
diff --git a/tests/lean/run/2846.lean b/tests/lean/run/2846.lean
new file mode 100644
index 0000000000..d519eb3bae
--- /dev/null
+++ b/tests/lean/run/2846.lean
@@ -0,0 +1,74 @@
+/-!
+# `delabConstWithSignature` avoids using inaccessible names
+-/
+
+/-!
+Defined without named arguments, prints without named arguments.
+-/
+/-- info: String.append : String → String → String -/
+#guard_msgs in #check String.append
+
+/-!
+The List argument is not named, it is not printed as a named argument.
+-/
+/-- info: List.length.{u_1} {α : Type u_1} : List α → Nat -/
+#guard_msgs in #check List.length
+
+/-!
+All arguments are named, all are printed as named arguments.
+-/
+/-- info: Nat.pos_pow_of_pos {n : Nat} (m : Nat) (h : 0 < n) : 0 < n ^ m -/
+#guard_msgs in #check Nat.pos_pow_of_pos
+
+/-!
+The hypothesis is not a named argument, so it's not printed as a named argument.
+-/
+def Nat.pos_pow_of_pos' {n : Nat} (m : Nat) : 0 < n → 0 < n ^ m := Nat.pos_pow_of_pos m
+
+/-- info: Nat.pos_pow_of_pos' {n : Nat} (m : Nat) : 0 < n → 0 < n ^ m -/
+#guard_msgs in #check Nat.pos_pow_of_pos'
+
+/-!
+Repetition of a named argument, only the first is printed as a named argument.
+-/
+def foo (n n : Nat) : Fin (n + 1) := 0
+
+/-- info: foo (n : Nat) : (n : Nat) → Fin (n + 1) -/
+#guard_msgs in #check foo
+
+/-!
+Repetition of a named argument, only the first is printed as a named argument.
+This is checking that shadowing is handled correctly (that's not the responsibility of
+`delabConstWithSignature`, but it assumes that the main delaborator will handle this correctly).
+-/
+def foo' (n n : Nat) (a : Fin ((by clear n; exact n) + 1)) : Fin (n + 1) := 0
+
+/-- info: foo' (n : Nat) : (n_1 : Nat) → Fin (n + 1) → Fin (n_1 + 1) -/
+#guard_msgs in #check foo'
+
+/-!
+Named argument after inaccesible name, still stays after the colon.
+But, it does not print using named pi notation since this is not a dependent type.
+-/
+def foo'' : String → (needle : String) → String := fun _ yo => yo
+
+/-- info: foo'' : String → String → String -/
+#guard_msgs in #check foo''
+
+/-!
+Named argument after inaccessible name, still stays after the colon.
+Here, because it's a dependent type the named pi notation shows the name.
+-/
+def bar : String → (n : Nat) → Fin (n+1) := fun _ n => ⟨0, Nat.zero_lt_succ n⟩
+
+/-- info: bar : String → (n : Nat) → Fin (n + 1) -/
+#guard_msgs in #check bar
+
+/-!
+Instance argument is an inaccessible name, and we assume that it is a nameless instance,
+so it goes before the colon.
+-/
+def bar' [LT α] (x : α) : x < x := sorry
+
+/-- info: bar'.{u_1} {α : Type u_1} [LT α] (x : α) : x < x -/
+#guard_msgs in #check bar'
diff --git a/tests/lean/run/funind_demo.lean b/tests/lean/run/funind_demo.lean
index e7ea42bfb0..6091baa4f4 100644
--- a/tests/lean/run/funind_demo.lean
+++ b/tests/lean/run/funind_demo.lean
@@ -10,7 +10,7 @@ derive_functional_induction ackermann
 info: ackermann.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m)
   (case2 : ∀ (n : Nat), motive n 1 → motive (Nat.succ n) 0)
   (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive (Nat.succ n) (Nat.succ m))
-  (x x : Nat) : motive x x
+  (x : Nat) : ∀ (x_1 : Nat), motive x x_1
 -/
 #guard_msgs in
 #check ackermann.induct
diff --git a/tests/lean/run/funind_mutual_dep.lean b/tests/lean/run/funind_mutual_dep.lean
index e3a4d6c96c..229c26fa42 100644
--- a/tests/lean/run/funind_mutual_dep.lean
+++ b/tests/lean/run/funind_mutual_dep.lean
@@ -65,7 +65,7 @@ info: Finite.functions.induct (motive1 : Finite → Prop) (motive2 : (x : Type)
         (∀ (rest : List (Finite.asType (Finite.arr t1 t2) → α)),
             motive2 (Finite.asType (Finite.arr t1 t2) → α) t2 rest) →
           motive2 α (Finite.arr t1 t2) results)
-  (x : Type) (x : Finite) (x : List x) : motive2 x x x
+  (x : Type) : ∀ (x_1 : Finite) (x_2 : List x), motive2 x x_1 x_2
 -/
 #guard_msgs in
 #check Finite.functions.induct
diff --git a/tests/lean/run/funind_tests.lean b/tests/lean/run/funind_tests.lean
index 175cf0069d..1e3cdd5262 100644
--- a/tests/lean/run/funind_tests.lean
+++ b/tests/lean/run/funind_tests.lean
@@ -32,7 +32,7 @@ derive_functional_induction ackermann
 info: Binary.ackermann.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m)
   (case2 : ∀ (n : Nat), motive n 1 → motive (Nat.succ n) 0)
   (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive (Nat.succ n) (Nat.succ m))
-  (x x : Nat) : motive x x
+  (x : Nat) : ∀ (x_1 : Nat), motive x x_1
 -/
 #guard_msgs in
 #check ackermann.induct
@@ -244,7 +244,7 @@ derive_functional_induction with_arg_refining_match1
 /--
 info: with_arg_refining_match1.induct (motive : Nat → Nat → Prop) (case1 : ∀ (i : Nat), motive i 0)
   (case2 : ∀ (n : Nat), motive 0 (Nat.succ n))
-  (case3 : ∀ (i n : Nat), ¬i = 0 → motive (i - 1) n → motive i (Nat.succ n)) (x x : Nat) : motive x x
+  (case3 : ∀ (i n : Nat), ¬i = 0 → motive (i - 1) n → motive i (Nat.succ n)) (x : Nat) : ∀ (x_1 : Nat), motive x x_1
 -/
 #guard_msgs in
 #check with_arg_refining_match1.induct
@@ -259,7 +259,8 @@ derive_functional_induction with_arg_refining_match2
 /--
 info: with_arg_refining_match2.induct (motive : Nat → Nat → Prop) (case1 : ∀ (n : Nat), motive 0 n)
   (case2 : ∀ (i : Nat), ¬i = 0 → motive i 0)
-  (case3 : ∀ (i : Nat), ¬i = 0 → ∀ (n : Nat), motive (i - 1) n → motive i (Nat.succ n)) (x x : Nat) : motive x x
+  (case3 : ∀ (i : Nat), ¬i = 0 → ∀ (n : Nat), motive (i - 1) n → motive i (Nat.succ n)) (x : Nat) :
+  ∀ (x_1 : Nat), motive x x_1
 -/
 #guard_msgs in
 #check with_arg_refining_match2.induct
@@ -293,7 +294,8 @@ derive_functional_induction with_mixed_match_tailrec
 
 /--
 info: with_mixed_match_tailrec.induct (motive : Nat → Nat → Nat → Nat → Prop) (case1 : ∀ (c d x : Nat), motive 0 x c d)
-  (case2 : ∀ (c d a x : Nat), motive a x (c % 2) (d % 2) → motive (Nat.succ a) x c d) (x x x x : Nat) : motive x x x x
+  (case2 : ∀ (c d a x : Nat), motive a x (c % 2) (d % 2) → motive (Nat.succ a) x c d) (x : Nat) :
+  ∀ (x_1 x_2 x_3 : Nat), motive x x_1 x_2 x_3
 -/
 #guard_msgs in
 #check with_mixed_match_tailrec.induct
@@ -312,8 +314,8 @@ derive_functional_induction with_mixed_match_tailrec2
 /--
 info: with_mixed_match_tailrec2.induct (motive : Nat → Nat → Nat → Nat → Nat → Prop)
   (case1 : ∀ (a b c d : Nat), motive 0 a b c d) (case2 : ∀ (c d n x : Nat), motive (Nat.succ n) 0 x c d)
-  (case3 : ∀ (c d n a x : Nat), motive n a x (c % 2) (d % 2) → motive (Nat.succ n) (Nat.succ a) x c d)
-  (x x x x x : Nat) : motive x x x x x
+  (case3 : ∀ (c d n a x : Nat), motive n a x (c % 2) (d % 2) → motive (Nat.succ n) (Nat.succ a) x c d) (x : Nat) :
+  ∀ (x_1 x_2 x_3 x_4 : Nat), motive x x_1 x_2 x_3 x_4
 -/
 #guard_msgs in
 #check with_mixed_match_tailrec2.induct
@@ -404,7 +406,7 @@ derive_functional_induction binary
 
 /--
 info: UnusedExtraParams.binary.induct (base : Nat) (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m)
-  (case2 : ∀ (n m : Nat), motive n m → motive (Nat.succ n) m) (x x : Nat) : motive x x
+  (case2 : ∀ (n m : Nat), motive n m → motive (Nat.succ n) m) (x : Nat) : ∀ (x_1 : Nat), motive x x_1
 -/
 #guard_msgs in
 #check binary.induct
@@ -543,7 +545,7 @@ termination_by xs => xs
 derive_functional_induction foo
 /--
 info: LetFun.foo.induct.{u_1} {α : Type u_1} (x : α) (motive : List α → Prop) (case1 : motive [])
-  (case2 : ∀ (_y : α) (ys : List α), motive ys → motive (_y :: ys)) (x : List α) : motive x
+  (case2 : ∀ (_y : α) (ys : List α), motive ys → motive (_y :: ys)) : ∀ (x : List α), motive x
 -/
 #guard_msgs in
 #check foo.induct
@@ -559,7 +561,7 @@ termination_by xs => xs
 derive_functional_induction bar
 /--
 info: LetFun.bar.induct.{u_1} {α : Type u_1} (x : α) (motive : List α → Prop) (case1 : motive [])
-  (case2 : ∀ (_y : α) (ys : List α), motive ys → motive (_y :: ys)) (x : List α) : motive x
+  (case2 : ∀ (_y : α) (ys : List α), motive ys → motive (_y :: ys)) : ∀ (x : List α), motive x
 -/
 #guard_msgs in
 #check bar.induct
@@ -694,7 +696,7 @@ derive_functional_induction foo
 
 /--
 info: DefaultArgument.foo.induct (fixed : Bool) (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m)
-  (case2 : ∀ (m n : Nat), motive n m → motive (Nat.succ n) m) (x x : Nat) : motive x x
+  (case2 : ∀ (m n : Nat), motive n m → motive (Nat.succ n) m) (x : Nat) : ∀ (x_1 : Nat), motive x x_1
 -/
 #guard_msgs in
 #check foo.induct
@@ -721,7 +723,7 @@ info: Nary.foo.induct (motive : Nat → Nat → (x : Nat) → Fin x → Prop)
   (case5 :
     ∀ (n m k : Nat) (x : Fin (k + 2)),
       motive n m (k + 1) { val := 0, isLt := ⋯ } → motive (Nat.succ n) (Nat.succ m) (Nat.succ (Nat.succ k)) x)
-  (x x x : Nat) (x : Fin x) : motive x x x x
+  (x : Nat) : ∀ (x_1 x_2 : Nat) (x_3 : Fin x_2), motive x x_1 x_2 x_3
 -/
 #guard_msgs in
 #check foo.induct
diff --git a/tests/lean/sizeof.lean.expected.out b/tests/lean/sizeof.lean.expected.out
index b732b071d9..52020debae 100644
--- a/tests/lean/sizeof.lean.expected.out
+++ b/tests/lean/sizeof.lean.expected.out
@@ -7,5 +7,4 @@
 308
 310
 11
-InfTree.node.sizeOf_spec.{u} {α : Type u} [inst✝ : SizeOf α] (children : Nat → InfTree α) :
-  sizeOf (InfTree.node children) = 1
+InfTree.node.sizeOf_spec.{u} {α : Type u} [SizeOf α] (children : Nat → InfTree α) : sizeOf (InfTree.node children) = 1
diff --git a/tests/lean/terminationFailure.lean.expected.out b/tests/lean/terminationFailure.lean.expected.out
index e2951ec50d..824aff87fe 100644
--- a/tests/lean/terminationFailure.lean.expected.out
+++ b/tests/lean/terminationFailure.lean.expected.out
@@ -16,7 +16,7 @@ x1 =
 
 Please use `termination_by` to specify a decreasing measure.
 f (x : Nat) : Nat
-f.g (a✝ : Nat) : Nat
+f.g : Nat → Nat
 1
 2
 terminationFailure.lean:24:9-24:12: error: fail to show termination for
diff --git a/tests/lean/varBinderUpdate.lean.expected.out b/tests/lean/varBinderUpdate.lean.expected.out
index e789dfabe9..b23fdb0d80 100644
--- a/tests/lean/varBinderUpdate.lean.expected.out
+++ b/tests/lean/varBinderUpdate.lean.expected.out
@@ -1,6 +1,6 @@
 f Nat 5 : Nat
 g 5 : Nat
-Ex1.f (α : Type) [inst✝ : Add α] (a : α) : α
+Ex1.f (α : Type) [Add α] (a : α) : α
 Ex1.g {α : Type} (b : α) : α
 f Nat 5 : Nat
 g 5 : Nat