fix: make delabConstWithSignature avoid using inaccessible names (#3625)

The `delabConstWithSignature` delaborator is responsible for pretty
printing constants with a declaration-like signature, with binders, a
colon, and a type. This is used by the `#check` command when it is given
just an identifier.

It used to accumulate binders from pi types indiscriminately, but this
led to unfriendly behavior. For example, `#check String.append` would
give
```
String.append (a✝ : String) (a✝¹ : String) : String
```
with inaccessible names. These appear because `String.append` is defined
using patterns, so it never names these parameters.

Now the delaborator stops accumulating binders once it reaches an
inaccessible name, and for example `#check String.append` now gives
```
String.append : String → String → String
```
We do not synthesize names for the sake of enabling binder syntax
because the binder names are part of the API of a function — one can use
`(arg := ...)` syntax to pass arguments by name. The delaborator also
now stops accumulating binders once it reaches a parameter with a name
already seen before — we then rely on the main delaborator to provide
that parameter with a fresh name when pretty printing the pi type.

As a special case, instance parameters with inaccessible names are
included as binders, pretty printing like `[LT α]`, rather than
relegating them (and all the remaining parameters) to after the colon.
It would be more accurate to pretty print this as `[inst✝ : LT α]`, but
we make the simplifying assumption that such instance parameters are
generally used via typeclass inference. Likely `inst✝` would not
directly appear in pretty printer output, and even if it appears in a
hover, users can likely figure out what is going on. (We may consider
making such `inst✝` variables pretty print as `‹LT α›` or
`infer_instance` in the future, to make this more consistent.)

Something we note here is that we do not do anything to make sure
parameters that can be used as named arguments actually appear named
after the colon (nor do we assure that the names are the correct names).
For example, one sees `foo : String → String → String` rather than `foo
: String → (baz : String) → String`. We can investigate this later if it
is wanted.

We also give `delabConstWithSignature` a `universes` flag to enable
turning off pretty printing universe levels parameters.

Closes #2846

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

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

tests/lean/714.lean.expected.out

@@ -1 +1 @@
-test {α : Type} [inst✝ : LT α] : Type
+test {α : Type} [LT α] : Type

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

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)

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"}}

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

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

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 = ([], [])

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'

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

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

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

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

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

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