From d3972f5baf963932a8580e243bc19249cae42f7f Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Mon, 19 Sep 2022 11:01:42 -0700
Subject: [PATCH 1/8] feat(frontends/lean/pp): use forall notation for all pi
 types from a Type to a Prop

---
 src/frontends/lean/pp.cpp                     | 54 ++++++++++---------
 tests/lean/1917.lean.expected.out             |  2 +-
 tests/lean/elab_error_msgs.lean.expected.out  |  2 +-
 tests/lean/error_pos.lean.expected.out        |  2 +-
 tests/lean/let1.lean                          |  2 +
 tests/lean/let1.lean.expected.out             |  8 +--
 tests/lean/pp_forall.lean                     | 12 +++++
 tests/lean/pp_forall.lean.expected.out        | 11 ++++
 tests/lean/pp_parens.lean                     |  1 +
 tests/lean/pp_parens.lean.expected.out        |  3 +-
 .../lean/pp_shadowed_const.lean.expected.out  |  2 +-
 11 files changed, 66 insertions(+), 33 deletions(-)
 create mode 100644 tests/lean/pp_forall.lean
 create mode 100644 tests/lean/pp_forall.lean.expected.out

diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 3b78ec72e0..cab756a461 100755
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -1102,32 +1102,38 @@ static bool is_default_arrow(expr const & e) {
 }
 template<class T>
 auto pretty_fn<T>::pp_pi(expr const & e) -> result {
-    if (is_default_arrow(e)) {
-        result lhs = pp_child_at(binding_domain(e), get_arrow_prec(), expr_address::binding_type(e));
-        expr   b   = lift_free_vars(binding_body(e), 1);
-        address pb = expr_address::pi_body();
-        result rhs = is_pi(b) ? pp_at(b, pb) : pp_child_at(b, get_arrow_prec() - 1, pb);
-        T r   = group(lhs.fmt() + space() + (m_unicode ? *g_arrow_n_fmt : *g_arrow_fmt) + line() + rhs.fmt());
-        return result(get_arrow_prec(), get_arrow_prec()-1, r);
-    } else {
-        expr b = e;
-        address adr;
-        buffer<subexpr> locals;
-        while (is_pi(b) && !is_default_arrow(b)) {
-            auto p = binding_body_fresh(b, true);
-            locals.push_back(mk_pair(p.second, cons(expr_coord::pi_var_type, adr)));
-            b = p.first;
-            adr = cons(expr_coord::pi_body, adr);
+    expr b = e;
+    address adr;
+    buffer<subexpr> locals;
+    while (is_pi(b)) {
+        auto p = binding_body_fresh(b, true);
+        if (is_default_arrow(b) && !(!is_prop(binding_domain(b)) && is_prop(p.first))) {
+            // Then this is an arrow that isn't from a Type to a Prop (we prefer forall notation for such a case)
+            if (locals.size() == 0) {
+                // Then we pretty print an arrow immediately
+                result lhs = pp_child_at(binding_domain(b), get_arrow_prec(), expr_address::binding_type(b));
+                b = p.first;
+                address pb = expr_address::pi_body();
+                result rhs = is_pi(b) ? pp_at(b, pb) : pp_child_at(b, get_arrow_prec() - 1, pb);
+                T r = group(lhs.fmt() + space() + (m_unicode ? *g_arrow_n_fmt : *g_arrow_fmt) + line() + rhs.fmt());
+                return result(get_arrow_prec(), get_arrow_prec()-1, r);
+            } else {
+                // Then we are done with the loop and pretty print the pi/forall
+                break;
+            }
         }
-        T r;
-        if (is_prop(b))
-            r = m_unicode ? *g_forall_n_fmt : *g_forall_fmt;
-        else
-            r = m_unicode ? *g_pi_n_fmt : *g_pi_fmt;
-        r += pp_binders(locals);
-        r += group(compose(comma(), nest(m_indent, compose(line(), pp_child_at(b, 0, adr).fmt()))));
-        return result(0, r);
+        locals.push_back(mk_pair(p.second, cons(expr_coord::pi_var_type, adr)));
+        b = p.first;
+        adr = cons(expr_coord::pi_body, adr);
     }
+    T r;
+    if (is_prop(b))
+        r = m_unicode ? *g_forall_n_fmt : *g_forall_fmt;
+    else
+        r = m_unicode ? *g_pi_n_fmt : *g_pi_fmt;
+    r += pp_binders(locals);
+    r += group(compose(comma(), nest(m_indent, compose(line(), pp_child_at(b, 0, adr).fmt()))));
+    return result(0, r);
 }
 
 static bool is_have(expr const & e) {
diff --git a/tests/lean/1917.lean.expected.out b/tests/lean/1917.lean.expected.out
index 563b52dbe5..b68cbc6a42 100644
--- a/tests/lean/1917.lean.expected.out
+++ b/tests/lean/1917.lean.expected.out
@@ -7,6 +7,6 @@ The nested exception contains the failure state for the decreasing tactic.
 nested exception message:
 default_dec_tac failed
 state:
-foo : ℕ → false,
+foo : ∀ (ᾰ : ℕ), false,
 x y : ℕ
 ⊢ y < x
diff --git a/tests/lean/elab_error_msgs.lean.expected.out b/tests/lean/elab_error_msgs.lean.expected.out
index ca9d05ce3c..7f0d3689b9 100644
--- a/tests/lean/elab_error_msgs.lean.expected.out
+++ b/tests/lean/elab_error_msgs.lean.expected.out
@@ -3,7 +3,7 @@ elab_error_msgs.lean:2:0: error: type mismatch at application
 term
   λ (ha : ?m_1) (hb : ?m_2) (hb : ?m_3[ha, hb]), ha
 has type
-  Π (ha : ?m_1) (hb : ?m_2), ?m_3[ha, hb] → ?m_1
+  ∀ (ha : ?m_1) (hb : ?m_2) (hb : ?m_3[ha, hb]), ?m_1
 but is expected to have type
   ?m_1 → ?m_2 → ?m_3
 Additional information:
diff --git a/tests/lean/error_pos.lean.expected.out b/tests/lean/error_pos.lean.expected.out
index 088d76770c..9318101b4c 100644
--- a/tests/lean/error_pos.lean.expected.out
+++ b/tests/lean/error_pos.lean.expected.out
@@ -16,7 +16,7 @@ error_pos.lean:11:36: error: type expected at
   B
 term has type
   A → Type
-λ (A : Type) (B : A → Type), ⁇ → true : Π (A : Type), (A → Type) → Prop
+λ (A : Type) (B : A → Type), ∀ (ᾰ : ⁇), true : Π (A : Type), (A → Type) → Prop
 error_pos.lean:13:43: error: type expected at
   B
 term has type
diff --git a/tests/lean/let1.lean b/tests/lean/let1.lean
index cccbb7b45d..711c2894ed 100644
--- a/tests/lean/let1.lean
+++ b/tests/lean/let1.lean
@@ -12,6 +12,8 @@ prelude -- Correct version
 
 -- TODO(Leo): fix expected output as soon as elaborator starts #checking let-expression type again
 
+-- Note(kmill): some pretty printing oddities with forall since it's bool rather than Prop
+
 #check let bool                := Sort 0,
           and  (p q : bool)   := ∀ c : bool, (p → q → c) → c,
           infixl `∧`:25       := and,
diff --git a/tests/lean/let1.lean.expected.out b/tests/lean/let1.lean.expected.out
index 5de34178bb..da2933d8db 100644
--- a/tests/lean/let1.lean.expected.out
+++ b/tests/lean/let1.lean.expected.out
@@ -1,20 +1,20 @@
 let bool : Type := Prop,
     and : bool → bool → Prop := λ (p q : bool), Π (c : bool), (p → q → c) → c,
-    and_intro : Π (p q : bool), p → q → and p q :=
+    and_intro : Π (p q : bool), p → ∀ (H2 : q), and p q :=
       λ (p q : bool) (H1 : p) (H2 : q) (c : bool) (H : p → q → c), H H1 H2,
     and_elim_left : Π (p q : bool), and p q → p := λ (p q : bool) (H : and p q), H p (λ (H1 : p) (H2 : q), H1),
     and_elim_right : Π (p q : bool), and p q → q := λ (p q : bool) (H : and p q), H q (λ (H1 : p) (H2 : q), H2)
 in and_intro :
   ∀ (p q : Prop), p → q → ∀ (c : Prop), (p → q → c) → c
-let1.lean:19:17: error: invalid let-expression, term
+let1.lean:21:17: error: invalid let-expression, term
   λ (p q : bool) (H1 : p) (H2 : q) (c : bool) (H : p → q → c), H H1 H2
 has type
   Π (p q : bool), p → q → Π (c : bool), (p → q → c) → c
 but is expected to have type
-  Π (p q : bool), p → q → and q p
+  Π (p q : bool), p → ∀ (H2 : q), and q p
 let bool : Type := Prop,
     and : bool → bool → Prop := λ (p q : bool), Π (c : bool), (p → q → c) → c,
-    and_intro : Π (p q : bool), p → q → and q p := ⁇,
+    and_intro : Π (p q : bool), p → ∀ (H2 : q), and q p := ⁇,
     and_elim_left : Π (p q : bool), and p q → p := λ (p q : bool) (H : and p q), H p (λ (H1 : p) (H2 : q), H1),
     and_elim_right : Π (p q : bool), and p q → q := λ (p q : bool) (H : and p q), H q (λ (H1 : p) (H2 : q), H2)
 in and_intro :
diff --git a/tests/lean/pp_forall.lean b/tests/lean/pp_forall.lean
new file mode 100644
index 0000000000..5a1bb6875f
--- /dev/null
+++ b/tests/lean/pp_forall.lean
@@ -0,0 +1,12 @@
+variables (p q : Prop)
+#check p → q
+#check p → ℕ
+#check ℕ → p
+#check ℕ → ℕ
+#check ℕ → Prop
+#check ℕ → Type
+#check ∀ (n : ℕ), n > 0
+#check ∀ (n : ℕ), 1 = 2
+#check Π (n : ℕ), ℤ
+#check Π (n : ℕ), fin n
+#check ∀ n : ℕ, ¬∃ x : ℕ, x ≠ x
diff --git a/tests/lean/pp_forall.lean.expected.out b/tests/lean/pp_forall.lean.expected.out
new file mode 100644
index 0000000000..4917e63be2
--- /dev/null
+++ b/tests/lean/pp_forall.lean.expected.out
@@ -0,0 +1,11 @@
+p → q : Prop
+p → ℕ : Type
+∀ (ᾰ : ℕ), p : Prop
+ℕ → ℕ : Type
+ℕ → Prop : Type
+ℕ → Type : Type 1
+∀ (n : ℕ), n > 0 : Prop
+∀ (n : ℕ), 1 = 2 : Prop
+ℕ → ℤ : Type
+Π (n : ℕ), fin n : Type
+∀ (n : ℕ), ¬∃ (x : ℕ), x ≠ x : Prop
diff --git a/tests/lean/pp_parens.lean b/tests/lean/pp_parens.lean
index 331eb00ff3..f16fd87e01 100644
--- a/tests/lean/pp_parens.lean
+++ b/tests/lean/pp_parens.lean
@@ -7,6 +7,7 @@ set_option pp.parens true
 #check [1,2,3]++[3,4,5]
 
 #check ∀ (x y z : ℤ), x - (-3) = -2 + x
+#check Π (x y : ℤ), {x : ℤ // x - (-3) = -2 + x}
 #check ∀ (p : ℕ → ℕ → Prop), p (1 + 2) 3
 #check ∀ (f : ℕ → ℕ → ℕ), f 2 (f 3 4 + 1) + 2 = f 1 2
 
diff --git a/tests/lean/pp_parens.lean.expected.out b/tests/lean/pp_parens.lean.expected.out
index 279b6cc61f..6de39b3398 100644
--- a/tests/lean/pp_parens.lean.expected.out
+++ b/tests/lean/pp_parens.lean.expected.out
@@ -1,7 +1,8 @@
 ((1 + (2 * 3)) + 4) : ℕ
 nat.add_assoc : ∀ (n m k : ℕ), (((n + m) + k) = (n + (m + k)))
 (([1, 2, 3]) ++ ([3, 4, 5])) : list ℕ
-∀ (x : ℤ), ℤ → ℤ → ((x - (-3)) = ((-2) + x)) : Prop
+∀ (x y z : ℤ), ((x - (-3)) = ((-2) + x)) : Prop
+ℤ → ℤ → {x // ((x - (-3)) = ((-2) + x))} : Type
 ∀ (p : ℕ → ℕ → Prop), p (1 + 2) 3 : Prop
 ∀ (f : ℕ → ℕ → ℕ), ((f 2 (f 3 4 + 1) + 2) = f 1 2) : Prop
 (set.univ = (⋃ (n : ℕ), {m : ℕ | (m < n)})) : Prop
diff --git a/tests/lean/pp_shadowed_const.lean.expected.out b/tests/lean/pp_shadowed_const.lean.expected.out
index 7686c56565..215532aaa5 100644
--- a/tests/lean/pp_shadowed_const.lean.expected.out
+++ b/tests/lean/pp_shadowed_const.lean.expected.out
@@ -1,7 +1,7 @@
 pp_shadowed_const.lean:1:55: error: don't know how to synthesize placeholder
 context:
 bool : ℕ
-⊢ _root_.bool → _root_.bool = _root_.bool
+⊢ ∀ (b : _root_.bool), _root_.bool = _root_.bool
 def g : 1 == 1 → 1 == 1 :=
 λ (heq_1 : 1 == 1), heq_1.symm
 pp_shadowed_const.lean:7:39: error: don't know how to synthesize placeholder

From d205cc56826106507358631ba415196daa31e7c8 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Fri, 23 Sep 2022 00:43:12 -0400
Subject: [PATCH 2/8] make non-dependent pi bindings pp as _

---
 src/frontends/lean/pp.cpp              | 14 ++++++++++++--
 tests/lean/pp_forall.lean              |  1 +
 tests/lean/pp_forall.lean.expected.out |  7 ++++---
 3 files changed, 17 insertions(+), 5 deletions(-)

diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index cab756a461..296fa0f362 100755
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -1037,7 +1037,11 @@ T pretty_fn<T>::pp_binder_block(buffer<name> const & names, expr const & type, b
     if (m_binder_types || bi != binder_info())
         r += T(open_binder_string(bi, m_unicode));
     for (name const & n : names) {
-        r += escape(n);
+        if (n.is_anonymous()) {
+            r += T("_");
+        } else {
+            r += escape(n);
+        }
         r += space();
     }
     if (m_binder_types) {
@@ -1122,7 +1126,13 @@ auto pretty_fn<T>::pp_pi(expr const & e) -> result {
                 break;
             }
         }
-        locals.push_back(mk_pair(p.second, cons(expr_coord::pi_var_type, adr)));
+        expr local = p.second;
+        if (is_arrow(b)) {
+            // To let the user know this is a non-dependent pi we make the name for the local be anonymous.
+            // This prints as '_'.
+            local = mk_local(name(), name(), binding_domain(b), binding_info(b));
+        }
+        locals.push_back(mk_pair(local, cons(expr_coord::pi_var_type, adr)));
         b = p.first;
         adr = cons(expr_coord::pi_body, adr);
     }
diff --git a/tests/lean/pp_forall.lean b/tests/lean/pp_forall.lean
index 5a1bb6875f..05e7ee31d7 100644
--- a/tests/lean/pp_forall.lean
+++ b/tests/lean/pp_forall.lean
@@ -8,5 +8,6 @@ variables (p q : Prop)
 #check ∀ (n : ℕ), n > 0
 #check ∀ (n : ℕ), 1 = 2
 #check Π (n : ℕ), ℤ
+#check Π {n : ℕ}, ℤ
 #check Π (n : ℕ), fin n
 #check ∀ n : ℕ, ¬∃ x : ℕ, x ≠ x
diff --git a/tests/lean/pp_forall.lean.expected.out b/tests/lean/pp_forall.lean.expected.out
index 4917e63be2..ebfb3eec51 100644
--- a/tests/lean/pp_forall.lean.expected.out
+++ b/tests/lean/pp_forall.lean.expected.out
@@ -1,11 +1,12 @@
 p → q : Prop
 p → ℕ : Type
-∀ (ᾰ : ℕ), p : Prop
+∀ (_ : ℕ), p : Prop
 ℕ → ℕ : Type
 ℕ → Prop : Type
 ℕ → Type : Type 1
 ∀ (n : ℕ), n > 0 : Prop
-∀ (n : ℕ), 1 = 2 : Prop
+∀ (_ : ℕ), 1 = 2 : Prop
 ℕ → ℤ : Type
+Π {_ : ℕ}, ℤ : Type
 Π (n : ℕ), fin n : Type
-∀ (n : ℕ), ¬∃ (x : ℕ), x ≠ x : Prop
+∀ (_ : ℕ), ¬∃ (x : ℕ), x ≠ x : Prop

From a9cbf4997a06a2c1b0b3cf9c034ab0dbd0c59def Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Fri, 23 Sep 2022 00:47:27 -0400
Subject: [PATCH 3/8] blindly fix tests

---
 tests/lean/1917.lean.expected.out              | 2 +-
 tests/lean/error_pos.lean.expected.out         | 2 +-
 tests/lean/let1.lean.expected.out              | 6 +++---
 tests/lean/pp_parens.lean.expected.out         | 2 +-
 tests/lean/pp_shadowed_const.lean.expected.out | 2 +-
 5 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/tests/lean/1917.lean.expected.out b/tests/lean/1917.lean.expected.out
index b68cbc6a42..b1139eae3b 100644
--- a/tests/lean/1917.lean.expected.out
+++ b/tests/lean/1917.lean.expected.out
@@ -7,6 +7,6 @@ The nested exception contains the failure state for the decreasing tactic.
 nested exception message:
 default_dec_tac failed
 state:
-foo : ∀ (ᾰ : ℕ), false,
+foo : ∀ (_ : ℕ), false,
 x y : ℕ
 ⊢ y < x
diff --git a/tests/lean/error_pos.lean.expected.out b/tests/lean/error_pos.lean.expected.out
index 9318101b4c..7f7c4e0568 100644
--- a/tests/lean/error_pos.lean.expected.out
+++ b/tests/lean/error_pos.lean.expected.out
@@ -16,7 +16,7 @@ error_pos.lean:11:36: error: type expected at
   B
 term has type
   A → Type
-λ (A : Type) (B : A → Type), ∀ (ᾰ : ⁇), true : Π (A : Type), (A → Type) → Prop
+λ (A : Type) (B : A → Type), ∀ (_ : ⁇), true : Π (A : Type), (A → Type) → Prop
 error_pos.lean:13:43: error: type expected at
   B
 term has type
diff --git a/tests/lean/let1.lean.expected.out b/tests/lean/let1.lean.expected.out
index da2933d8db..ee391fc5f5 100644
--- a/tests/lean/let1.lean.expected.out
+++ b/tests/lean/let1.lean.expected.out
@@ -1,6 +1,6 @@
 let bool : Type := Prop,
     and : bool → bool → Prop := λ (p q : bool), Π (c : bool), (p → q → c) → c,
-    and_intro : Π (p q : bool), p → ∀ (H2 : q), and p q :=
+    and_intro : Π (p q : bool), p → ∀ (_ : q), and p q :=
       λ (p q : bool) (H1 : p) (H2 : q) (c : bool) (H : p → q → c), H H1 H2,
     and_elim_left : Π (p q : bool), and p q → p := λ (p q : bool) (H : and p q), H p (λ (H1 : p) (H2 : q), H1),
     and_elim_right : Π (p q : bool), and p q → q := λ (p q : bool) (H : and p q), H q (λ (H1 : p) (H2 : q), H2)
@@ -11,10 +11,10 @@ let1.lean:21:17: error: invalid let-expression, term
 has type
   Π (p q : bool), p → q → Π (c : bool), (p → q → c) → c
 but is expected to have type
-  Π (p q : bool), p → ∀ (H2 : q), and q p
+  Π (p q : bool), p → ∀ (_ : q), and q p
 let bool : Type := Prop,
     and : bool → bool → Prop := λ (p q : bool), Π (c : bool), (p → q → c) → c,
-    and_intro : Π (p q : bool), p → ∀ (H2 : q), and q p := ⁇,
+    and_intro : Π (p q : bool), p → ∀ (_ : q), and q p := ⁇,
     and_elim_left : Π (p q : bool), and p q → p := λ (p q : bool) (H : and p q), H p (λ (H1 : p) (H2 : q), H1),
     and_elim_right : Π (p q : bool), and p q → q := λ (p q : bool) (H : and p q), H q (λ (H1 : p) (H2 : q), H2)
 in and_intro :
diff --git a/tests/lean/pp_parens.lean.expected.out b/tests/lean/pp_parens.lean.expected.out
index 6de39b3398..76686e50a5 100644
--- a/tests/lean/pp_parens.lean.expected.out
+++ b/tests/lean/pp_parens.lean.expected.out
@@ -1,7 +1,7 @@
 ((1 + (2 * 3)) + 4) : ℕ
 nat.add_assoc : ∀ (n m k : ℕ), (((n + m) + k) = (n + (m + k)))
 (([1, 2, 3]) ++ ([3, 4, 5])) : list ℕ
-∀ (x y z : ℤ), ((x - (-3)) = ((-2) + x)) : Prop
+∀ (x _ _ : ℤ), ((x - (-3)) = ((-2) + x)) : Prop
 ℤ → ℤ → {x // ((x - (-3)) = ((-2) + x))} : Type
 ∀ (p : ℕ → ℕ → Prop), p (1 + 2) 3 : Prop
 ∀ (f : ℕ → ℕ → ℕ), ((f 2 (f 3 4 + 1) + 2) = f 1 2) : Prop
diff --git a/tests/lean/pp_shadowed_const.lean.expected.out b/tests/lean/pp_shadowed_const.lean.expected.out
index 215532aaa5..fc8e570331 100644
--- a/tests/lean/pp_shadowed_const.lean.expected.out
+++ b/tests/lean/pp_shadowed_const.lean.expected.out
@@ -1,7 +1,7 @@
 pp_shadowed_const.lean:1:55: error: don't know how to synthesize placeholder
 context:
 bool : ℕ
-⊢ ∀ (b : _root_.bool), _root_.bool = _root_.bool
+⊢ ∀ (_ : _root_.bool), _root_.bool = _root_.bool
 def g : 1 == 1 → 1 == 1 :=
 λ (heq_1 : 1 == 1), heq_1.symm
 pp_shadowed_const.lean:7:39: error: don't know how to synthesize placeholder

From 24e8eacf9ea55f87dab2bc37f579a2729aa1043e Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Fri, 23 Sep 2022 01:15:09 -0400
Subject: [PATCH 4/8] failing tests

---
 tests/lean/584a.lean.expected.out                 |  6 +++---
 tests/lean/634d.lean.expected.out                 |  4 ++--
 tests/lean/652.lean.expected.out                  |  8 ++++----
 tests/lean/as_is_leak_bug.lean.expected.out       |  8 ++++----
 tests/lean/class_instance_param.lean.expected.out |  4 ++--
 tests/lean/derive.lean.expected.out               |  6 +++---
 tests/lean/elab6.lean.expected.out                |  8 ++++----
 tests/lean/elab9.lean.expected.out                |  2 +-
 tests/lean/elab_error_msgs.lean.expected.out      |  2 +-
 tests/lean/extends_priority.lean.expected.out     | 12 ++++++------
 tests/lean/interactive/info.lean.expected.out     |  2 +-
 tests/lean/out_param_proj.lean.expected.out       |  2 +-
 tests/lean/pp_zero_bug.lean.expected.out          |  4 ++--
 tests/lean/struct_class.lean.expected.out         |  4 ++--
 14 files changed, 36 insertions(+), 36 deletions(-)

diff --git a/tests/lean/584a.lean.expected.out b/tests/lean/584a.lean.expected.out
index e9343289d3..c4d657dba8 100644
--- a/tests/lean/584a.lean.expected.out
+++ b/tests/lean/584a.lean.expected.out
@@ -1,5 +1,5 @@
-foo : Π (A : Type u_1) [H : inhabited A], A → A
-foo' : Π {A : Type u_1} [H : inhabited A] {x : A}, A
+foo : Π (A : Type u_1) [_ : inhabited A], A → A
+foo' : Π {A : Type u_1} [_ : inhabited A] {x : A}, A
 foo ℕ 10 : ℕ
-def test : ∀ {A : Type u} [H : inhabited A], @foo' ℕ nat.inhabited (5 + 5) = 10 :=
+def test : ∀ {A : Type u} [_ : inhabited A], @foo' ℕ nat.inhabited (5 + 5) = 10 :=
 λ {A : Type u} [H : inhabited A], @rfl ℕ (@foo' ℕ nat.inhabited (5 + 5))
diff --git a/tests/lean/634d.lean.expected.out b/tests/lean/634d.lean.expected.out
index 05560ab3a9..c7f2e0bc45 100644
--- a/tests/lean/634d.lean.expected.out
+++ b/tests/lean/634d.lean.expected.out
@@ -3,8 +3,8 @@ _root_.A : Type → Type
 A : Sort l → Sort l
 _root_.A.{1} : Type → Type
 P : B → B
-_root_.P : Π {n : ℕ}, ℕ → ℕ
+_root_.P : Π {_ : ℕ}, ℕ → ℕ
 P : B → B
 _root_.P.{1} : ?M_1 → ?M_1
 @P 2 : B → B
-@_root_.P.{1} ℕ : Π {n : ℕ}, ℕ → ℕ
+@_root_.P.{1} ℕ : Π {_ : ℕ}, ℕ → ℕ
diff --git a/tests/lean/652.lean.expected.out b/tests/lean/652.lean.expected.out
index f4402e127c..0b276d8587 100644
--- a/tests/lean/652.lean.expected.out
+++ b/tests/lean/652.lean.expected.out
@@ -1,6 +1,6 @@
-R : Π {b c : bool}, Prop
+R : Π {_ _ : bool}, Prop
 R2 : bool → bool → Prop
 R3 : bool → bool → Prop
-R4 : bool → Π {c : bool}, Prop
-R5 : Π {b c : bool}, Prop
-R6 : Π {b : bool}, bool → Prop
+R4 : bool → Π {_ : bool}, Prop
+R5 : Π {_ _ : bool}, Prop
+R6 : Π {_ : bool}, bool → Prop
diff --git a/tests/lean/as_is_leak_bug.lean.expected.out b/tests/lean/as_is_leak_bug.lean.expected.out
index 074366fefc..46cab8a7c9 100644
--- a/tests/lean/as_is_leak_bug.lean.expected.out
+++ b/tests/lean/as_is_leak_bug.lean.expected.out
@@ -1,8 +1,8 @@
-def f : Π {α : Type} [_inst_1 : has_to_string α], α → string :=
+def f : Π {α : Type} [_ : has_to_string α], α → string :=
 λ {α : Type} [_inst_1 : has_to_string α] (a : α), to_string a
-def g : Π {α : Type} [_inst_1 : has_to_string α], α → string :=
+def g : Π {α : Type} [_ : has_to_string α], α → string :=
 λ {α : Type} [_inst_1 : has_to_string α], f
-def g' : Π {α : Type} [_inst_1 : has_to_string α], (α → string) × Type :=
+def g' : Π {α : Type} [_ : has_to_string α], (α → string) × Type :=
 λ {α : Type} [_inst_1 : has_to_string α], (f, α)
-def h : Π {α : Type} [_inst_1 : has_to_string α], (α → string) × (α → string) × ((α → string) × Type) × Type :=
+def h : Π {α : Type} [_ : has_to_string α], (α → string) × (α → string) × ((α → string) × Type) × Type :=
 λ {α : Type} [_inst_1 : has_to_string α], (f, g, g', α)
diff --git a/tests/lean/class_instance_param.lean.expected.out b/tests/lean/class_instance_param.lean.expected.out
index aa72cba00b..3201d8cd88 100644
--- a/tests/lean/class_instance_param.lean.expected.out
+++ b/tests/lean/class_instance_param.lean.expected.out
@@ -1,7 +1,7 @@
-densely_ordered : Π (α : Type u_1) [_inst_1 : preorder α], Prop
+densely_ordered : Π (α : Type u_1) [_ : preorder α], Prop
 densely_ordered.mk :
   ∀ {α : Type u_1} [_inst_1 : preorder α],
     (∀ (a c : α), a < c → (∃ (b : α), a < b ∧ b < c)) → densely_ordered α
 densely_ordered.dense :
-  ∀ {α : Type u_1} [_inst_1 : preorder α] [self : densely_ordered α] (a c : α),
+  ∀ {α : Type u_1} [_inst_1 : preorder α] [_ : densely_ordered α] (a c : α),
     a < c → (∃ (b : α), a < b ∧ b < c)
diff --git a/tests/lean/derive.lean.expected.out b/tests/lean/derive.lean.expected.out
index 9b895b510f..c38d4ae90a 100644
--- a/tests/lean/derive.lean.expected.out
+++ b/tests/lean/derive.lean.expected.out
@@ -1,9 +1,9 @@
 foo.has_reflect :
-  Π (α : Type) [a : has_reflect α] (β : Type) [a : has_reflect β] [a : reflected Type α] [a : reflected Type β],
+  Π (α : Type) [_ : has_reflect α] (β : Type) [_ : has_reflect β] [_ : reflected Type α] [_ : reflected Type β],
     has_reflect (foo α β)
 foo'.decidable_eq :
-  Π (α : Type u_1) [a : decidable_eq α] (β : Type u_1) [a : decidable_eq β] (n ᾰ : ℕ),
+  Π (α : Type u_1) [_ : decidable_eq α] (β : Type u_1) [_ : decidable_eq β] (n ᾰ : ℕ),
     decidable_eq (foo' α β n ᾰ)
 foo'.has_sizeof :
-  Π (α : Type u_1) [a : has_sizeof α] (β : Type u_1) [a : has_sizeof β] (n ᾰ : ℕ),
+  Π (α : Type u_1) [_ : has_sizeof α] (β : Type u_1) [_ : has_sizeof β] (n ᾰ : ℕ),
     has_sizeof (foo' α β n ᾰ)
diff --git a/tests/lean/elab6.lean.expected.out b/tests/lean/elab6.lean.expected.out
index ff4b1ada64..9789cd1256 100644
--- a/tests/lean/elab6.lean.expected.out
+++ b/tests/lean/elab6.lean.expected.out
@@ -1,10 +1,10 @@
 H : @transitive.{1} nat R
-@F.{u_1} ?M_1 : Π ⦃a : ?M_1⦄ {b : ?M_1}, ?M_1 → Π ⦃e : ?M_1⦄, ?M_1 → ?M_1 → ?M_1
-@F.{0} bool ?M_1 ?M_2 bool.tt : Π ⦃e : bool⦄, bool → bool → bool
+@F.{u_1} ?M_1 : Π ⦃_ : ?M_1⦄ {_ : ?M_1}, ?M_1 → Π ⦃_ : ?M_1⦄, ?M_1 → ?M_1 → ?M_1
+@F.{0} bool ?M_1 ?M_2 bool.tt : Π ⦃_ : bool⦄, bool → bool → bool
 @F.{0} bool ?M_1 ?M_2 bool.tt ?M_3 bool.tt : bool → bool
 @F.{0} bool ?M_1 ?M_2 bool.tt ?M_3 bool.tt bool.tt : bool
 H : @transitive.{1} nat R
-@F.{u_1} ?M_1 : Π ⦃a : ?M_1⦄ {b : ?M_1}, ?M_1 → Π ⦃e : ?M_1⦄, ?M_1 → ?M_1 → ?M_1
-@F.{0} bool ?M_1 ?M_2 bool.tt : Π ⦃e : bool⦄, bool → bool → bool
+@F.{u_1} ?M_1 : Π ⦃_ : ?M_1⦄ {_ : ?M_1}, ?M_1 → Π ⦃_ : ?M_1⦄, ?M_1 → ?M_1 → ?M_1
+@F.{0} bool ?M_1 ?M_2 bool.tt : Π ⦃_ : bool⦄, bool → bool → bool
 @F.{0} bool ?M_1 ?M_2 bool.tt ?M_3 bool.tt : bool → bool
 @F.{0} bool ?M_1 ?M_2 bool.tt ?M_3 bool.tt bool.tt : bool
diff --git a/tests/lean/elab9.lean.expected.out b/tests/lean/elab9.lean.expected.out
index 5a4b0acd8a..e0a49bb327 100644
--- a/tests/lean/elab9.lean.expected.out
+++ b/tests/lean/elab9.lean.expected.out
@@ -7,4 +7,4 @@
     Π [_inst_3 : has_add A],
       @eq A a (@has_add.add A _inst_3 (@has_zero.zero A _inst_2) (@has_zero.zero A _inst_2)) → A
 λ (a b : nat) (H : @gt nat nat.has_lt a b) [_inst_1 : has_lt nat], @has_lt.lt nat _inst_1 a b :
-  Π (a b : nat), @gt nat nat.has_lt a b → Π [_inst_1 : has_lt nat], Prop
+  Π (a b : nat), @gt nat nat.has_lt a b → Π [_ : has_lt nat], Prop
diff --git a/tests/lean/elab_error_msgs.lean.expected.out b/tests/lean/elab_error_msgs.lean.expected.out
index 7f0d3689b9..01116eee9b 100644
--- a/tests/lean/elab_error_msgs.lean.expected.out
+++ b/tests/lean/elab_error_msgs.lean.expected.out
@@ -3,7 +3,7 @@ elab_error_msgs.lean:2:0: error: type mismatch at application
 term
   λ (ha : ?m_1) (hb : ?m_2) (hb : ?m_3[ha, hb]), ha
 has type
-  ∀ (ha : ?m_1) (hb : ?m_2) (hb : ?m_3[ha, hb]), ?m_1
+  ∀ (ha : ?m_1) (hb : ?m_2) (_ : ?m_3[ha, hb]), ?m_1
 but is expected to have type
   ?m_1 → ?m_2 → ?m_3
 Additional information:
diff --git a/tests/lean/extends_priority.lean.expected.out b/tests/lean/extends_priority.lean.expected.out
index f53ae8d42e..a9a1a20c7a 100644
--- a/tests/lean/extends_priority.lean.expected.out
+++ b/tests/lean/extends_priority.lean.expected.out
@@ -1,18 +1,18 @@
 @[instance, priority 100, reducible]
-def B.to_A : Π {α : Type} [self : B α], A α :=
+def B.to_A : Π {α : Type} [_ : B α], A α :=
 λ (α : Type) [self : B α], [B.to_A self]
 @[instance, priority 37, reducible]
-def C.to_B : Π {α : Type} [self : C α], B α :=
+def C.to_B : Π {α : Type} [_ : C α], B α :=
 λ (α : Type) [self : C α], [C.to_B self]
 @[instance, priority 100, reducible]
-def D.to_C : Π {α : Type} [self : D α], C α :=
+def D.to_C : Π {α : Type} [_ : D α], C α :=
 λ (α : Type) [self : D α], [D.to_C self]
 @[instance, priority 100]
-def B'.to_A' : Π (α : Type) [self : B' α], A' α :=
+def B'.to_A' : Π (α : Type) [_ : B' α], A' α :=
 λ (α : Type) [self : B' α], A'.mk
 @[instance, priority 37]
-def C'.to_B' : Π (α : Type) [self : C' α], B' α :=
+def C'.to_B' : Π (α : Type) [_ : C' α], B' α :=
 λ (α : Type) [self : C' α], B'.mk
 @[instance, priority 100]
-def D'.to_C' : Π (α : Type) [self : D' α], C' α :=
+def D'.to_C' : Π (α : Type) [_ : D' α], C' α :=
 λ (α : Type) [self : D' α], C'.mk
diff --git a/tests/lean/interactive/info.lean.expected.out b/tests/lean/interactive/info.lean.expected.out
index df20c51652..7d5ed2514c 100644
--- a/tests/lean/interactive/info.lean.expected.out
+++ b/tests/lean/interactive/info.lean.expected.out
@@ -5,5 +5,5 @@
 {"record":{"full-id":"bool.tt","source":,"state":"⊢ bool","type":"bool"},"response":"ok","seq_num":7}
 {"record":{"doc":"(trace) enable/disable tracing for the given module and submodules"},"response":"ok","seq_num":10}
 {"record":{"full-id":"list.cons","source":,"state":"⊢ list bool","type":"Π {T : Type}, T → list T → list T"},"response":"ok","seq_num":13}
-{"record":{"full-id":"has_append.append","source":,"state":"⊢ list bool","type":"Π {α : Type} [self : has_append α], α → α → α"},"response":"ok","seq_num":16}
+{"record":{"full-id":"has_append.append","source":,"state":"⊢ list bool","type":"Π {α : Type} [_ : has_append α], α → α → α"},"response":"ok","seq_num":16}
 {"record":{"full-id":"id","source":,"type":"Π {α : Sort u}, α → α"},"response":"ok","seq_num":19}
diff --git a/tests/lean/out_param_proj.lean.expected.out b/tests/lean/out_param_proj.lean.expected.out
index 935c77853d..699977de92 100644
--- a/tests/lean/out_param_proj.lean.expected.out
+++ b/tests/lean/out_param_proj.lean.expected.out
@@ -1,3 +1,3 @@
 @[instance, priority 100, reducible]
-def module.to_add_comm_group : Π {α : Type u} {β : Type v} {_inst_1 : ring α} [self : module α β], add_comm_group β :=
+def module.to_add_comm_group : Π {α : Type u} {β : Type v} {_inst_1 : ring α} [_ : module α β], add_comm_group β :=
 λ {α : Type u} (β : Type v) {_inst_1 : ring α} [self : module α β], [module.to_add_comm_group self]
diff --git a/tests/lean/pp_zero_bug.lean.expected.out b/tests/lean/pp_zero_bug.lean.expected.out
index efe231685b..ebefdab510 100644
--- a/tests/lean/pp_zero_bug.lean.expected.out
+++ b/tests/lean/pp_zero_bug.lean.expected.out
@@ -1,2 +1,2 @@
-has_zero.zero : Π {α : Type u_1} [self : has_zero α], α
-has_zero.zero : Π [self : has_zero ℕ], ℕ
+has_zero.zero : Π {α : Type u_1} [_ : has_zero α], α
+has_zero.zero : Π [_ : has_zero ℕ], ℕ
diff --git a/tests/lean/struct_class.lean.expected.out b/tests/lean/struct_class.lean.expected.out
index 4c197e4115..b4e2905cfc 100644
--- a/tests/lean/struct_class.lean.expected.out
+++ b/tests/lean/struct_class.lean.expected.out
@@ -1,8 +1,8 @@
 @[class]
 structure point : Type u_1 → Type u_2 → Type (max u_1 u_2)
 fields:
-point.x : Π {A : Type u_1} (B : Type u_2) [self : point A B], A
-point.y : Π (A : Type u_1) {B : Type u_2} [self : point A B], B
+point.x : Π {A : Type u_1} (B : Type u_2) [_ : point A B], A
+point.y : Π (A : Type u_1) {B : Type u_2} [_ : point A B], B
 structure point2 : Type u_1 → Type u_2 → Type (max u_1 u_2)
 fields:
 point2.x : Π {A : Type u_1} {B : Type u_2}, point2 A B → A

From d2d4eded7332b153153c0677779ee9963dab7ce7 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Fri, 23 Sep 2022 01:38:28 -0400
Subject: [PATCH 5/8] missed a test fix

---
 tests/lean/584a.lean.expected.out | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/lean/584a.lean.expected.out b/tests/lean/584a.lean.expected.out
index c4d657dba8..b68af96b43 100644
--- a/tests/lean/584a.lean.expected.out
+++ b/tests/lean/584a.lean.expected.out
@@ -1,5 +1,5 @@
 foo : Π (A : Type u_1) [_ : inhabited A], A → A
-foo' : Π {A : Type u_1} [_ : inhabited A] {x : A}, A
+foo' : Π {A : Type u_1} [_ : inhabited A] {_ : A}, A
 foo ℕ 10 : ℕ
 def test : ∀ {A : Type u} [_ : inhabited A], @foo' ℕ nat.inhabited (5 + 5) = 10 :=
 λ {A : Type u} [H : inhabited A], @rfl ℕ (@foo' ℕ nat.inhabited (5 + 5))

From 920495c2577419377ebeb592b1475ec757b0c94a Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Tue, 27 Sep 2022 15:28:11 -0400
Subject: [PATCH 6/8] Mario suggestion of preferring [foo] over [_ : foo]

---
 src/frontends/lean/pp.cpp                     | 32 +++++++++++--------
 tests/lean/584a.lean.expected.out             |  6 ++--
 tests/lean/as_is_leak_bug.lean.expected.out   |  8 ++---
 .../class_instance_param.lean.expected.out    |  5 ++-
 tests/lean/derive.lean.expected.out           |  8 ++---
 tests/lean/elab9.lean.expected.out            |  2 +-
 tests/lean/extends_priority.lean.expected.out | 12 +++----
 tests/lean/interactive/info.lean.expected.out |  2 +-
 tests/lean/out_param_proj.lean.expected.out   |  2 +-
 tests/lean/pp_zero_bug.lean.expected.out      |  4 +--
 tests/lean/struct_class.lean.expected.out     |  4 +--
 11 files changed, 44 insertions(+), 41 deletions(-)

diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 296fa0f362..c880868eaa 100755
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -1036,16 +1036,22 @@ T pretty_fn<T>::pp_binder_block(buffer<name> const & names, expr const & type, b
     T r;
     if (m_binder_types || bi != binder_info())
         r += T(open_binder_string(bi, m_unicode));
-    for (name const & n : names) {
-        if (n.is_anonymous()) {
-            r += T("_");
-        } else {
-            r += escape(n);
+    if (bi.is_inst_implicit() && names.size() == 1 && names[0].is_anonymous()) {
+        // Prefer printing non-dependent instance implicit binder as `[foo]` rather than `[_ : foo]`.
+        // (Note: instance implicits always have `names.size() == 1`.)
+        r += pp_child(type, 0).fmt();
+    } else {
+        for (name const & n : names) {
+            if (n.is_anonymous()) {
+                r += T("_");
+            } else {
+                r += escape(n);
+            }
+            r += space();
+        }
+        if (m_binder_types) {
+            r += compose(colon(), nest(m_indent, compose(line(), pp_child(type, 0).fmt())));
         }
-        r += space();
-    }
-    if (m_binder_types) {
-        r += compose(colon(), nest(m_indent, compose(line(), pp_child(type, 0).fmt())));
     }
     if (m_binder_types || bi != binder_info())
         r += T(close_binder_string(bi, m_unicode));
@@ -1112,7 +1118,7 @@ auto pretty_fn<T>::pp_pi(expr const & e) -> result {
     while (is_pi(b)) {
         auto p = binding_body_fresh(b, true);
         if (is_default_arrow(b) && !(!is_prop(binding_domain(b)) && is_prop(p.first))) {
-            // Then this is an arrow that isn't from a Type to a Prop (we prefer forall notation for such a case)
+            // Then this is an arrow that isn't from a Type to a Prop (we instead prefer forall notation in such cases)
             if (locals.size() == 0) {
                 // Then we pretty print an arrow immediately
                 result lhs = pp_child_at(binding_domain(b), get_arrow_prec(), expr_address::binding_type(b));
@@ -1128,9 +1134,9 @@ auto pretty_fn<T>::pp_pi(expr const & e) -> result {
         }
         expr local = p.second;
         if (is_arrow(b)) {
-            // To let the user know this is a non-dependent pi we make the name for the local be anonymous.
-            // This prints as '_'.
-            local = mk_local(name(), name(), binding_domain(b), binding_info(b));
+            // To let the user know this is a non-dependent pi we make the pp name for the local be anonymous,
+            // which is printed by `pp_binders` as '_'.
+            local = mk_local(binding_name(b), name(), binding_domain(b), binding_info(b));
         }
         locals.push_back(mk_pair(local, cons(expr_coord::pi_var_type, adr)));
         b = p.first;
diff --git a/tests/lean/584a.lean.expected.out b/tests/lean/584a.lean.expected.out
index b68af96b43..55599b17f4 100644
--- a/tests/lean/584a.lean.expected.out
+++ b/tests/lean/584a.lean.expected.out
@@ -1,5 +1,5 @@
-foo : Π (A : Type u_1) [_ : inhabited A], A → A
-foo' : Π {A : Type u_1} [_ : inhabited A] {_ : A}, A
+foo : Π (A : Type u_1) [inhabited A], A → A
+foo' : Π {A : Type u_1} [inhabited A] {_ : A}, A
 foo ℕ 10 : ℕ
-def test : ∀ {A : Type u} [_ : inhabited A], @foo' ℕ nat.inhabited (5 + 5) = 10 :=
+def test : ∀ {A : Type u} [inhabited A], @foo' ℕ nat.inhabited (5 + 5) = 10 :=
 λ {A : Type u} [H : inhabited A], @rfl ℕ (@foo' ℕ nat.inhabited (5 + 5))
diff --git a/tests/lean/as_is_leak_bug.lean.expected.out b/tests/lean/as_is_leak_bug.lean.expected.out
index 46cab8a7c9..82fd0ef321 100644
--- a/tests/lean/as_is_leak_bug.lean.expected.out
+++ b/tests/lean/as_is_leak_bug.lean.expected.out
@@ -1,8 +1,8 @@
-def f : Π {α : Type} [_ : has_to_string α], α → string :=
+def f : Π {α : Type} [has_to_string α], α → string :=
 λ {α : Type} [_inst_1 : has_to_string α] (a : α), to_string a
-def g : Π {α : Type} [_ : has_to_string α], α → string :=
+def g : Π {α : Type} [has_to_string α], α → string :=
 λ {α : Type} [_inst_1 : has_to_string α], f
-def g' : Π {α : Type} [_ : has_to_string α], (α → string) × Type :=
+def g' : Π {α : Type} [has_to_string α], (α → string) × Type :=
 λ {α : Type} [_inst_1 : has_to_string α], (f, α)
-def h : Π {α : Type} [_ : has_to_string α], (α → string) × (α → string) × ((α → string) × Type) × Type :=
+def h : Π {α : Type} [has_to_string α], (α → string) × (α → string) × ((α → string) × Type) × Type :=
 λ {α : Type} [_inst_1 : has_to_string α], (f, g, g', α)
diff --git a/tests/lean/class_instance_param.lean.expected.out b/tests/lean/class_instance_param.lean.expected.out
index 3201d8cd88..c7241c906e 100644
--- a/tests/lean/class_instance_param.lean.expected.out
+++ b/tests/lean/class_instance_param.lean.expected.out
@@ -1,7 +1,6 @@
-densely_ordered : Π (α : Type u_1) [_ : preorder α], Prop
+densely_ordered : Π (α : Type u_1) [preorder α], Prop
 densely_ordered.mk :
   ∀ {α : Type u_1} [_inst_1 : preorder α],
     (∀ (a c : α), a < c → (∃ (b : α), a < b ∧ b < c)) → densely_ordered α
 densely_ordered.dense :
-  ∀ {α : Type u_1} [_inst_1 : preorder α] [_ : densely_ordered α] (a c : α),
-    a < c → (∃ (b : α), a < b ∧ b < c)
+  ∀ {α : Type u_1} [_inst_1 : preorder α] [densely_ordered α] (a c : α), a < c → (∃ (b : α), a < b ∧ b < c)
diff --git a/tests/lean/derive.lean.expected.out b/tests/lean/derive.lean.expected.out
index c38d4ae90a..fbc2b0e0a8 100644
--- a/tests/lean/derive.lean.expected.out
+++ b/tests/lean/derive.lean.expected.out
@@ -1,9 +1,7 @@
 foo.has_reflect :
-  Π (α : Type) [_ : has_reflect α] (β : Type) [_ : has_reflect β] [_ : reflected Type α] [_ : reflected Type β],
+  Π (α : Type) [has_reflect α] (β : Type) [has_reflect β] [reflected Type α] [reflected Type β],
     has_reflect (foo α β)
 foo'.decidable_eq :
-  Π (α : Type u_1) [_ : decidable_eq α] (β : Type u_1) [_ : decidable_eq β] (n ᾰ : ℕ),
-    decidable_eq (foo' α β n ᾰ)
+  Π (α : Type u_1) [decidable_eq α] (β : Type u_1) [decidable_eq β] (n ᾰ : ℕ), decidable_eq (foo' α β n ᾰ)
 foo'.has_sizeof :
-  Π (α : Type u_1) [_ : has_sizeof α] (β : Type u_1) [_ : has_sizeof β] (n ᾰ : ℕ),
-    has_sizeof (foo' α β n ᾰ)
+  Π (α : Type u_1) [has_sizeof α] (β : Type u_1) [has_sizeof β] (n ᾰ : ℕ), has_sizeof (foo' α β n ᾰ)
diff --git a/tests/lean/elab9.lean.expected.out b/tests/lean/elab9.lean.expected.out
index e0a49bb327..233b94366b 100644
--- a/tests/lean/elab9.lean.expected.out
+++ b/tests/lean/elab9.lean.expected.out
@@ -7,4 +7,4 @@
     Π [_inst_3 : has_add A],
       @eq A a (@has_add.add A _inst_3 (@has_zero.zero A _inst_2) (@has_zero.zero A _inst_2)) → A
 λ (a b : nat) (H : @gt nat nat.has_lt a b) [_inst_1 : has_lt nat], @has_lt.lt nat _inst_1 a b :
-  Π (a b : nat), @gt nat nat.has_lt a b → Π [_ : has_lt nat], Prop
+  Π (a b : nat), @gt nat nat.has_lt a b → Π [has_lt nat], Prop
diff --git a/tests/lean/extends_priority.lean.expected.out b/tests/lean/extends_priority.lean.expected.out
index a9a1a20c7a..e1c9a79f7c 100644
--- a/tests/lean/extends_priority.lean.expected.out
+++ b/tests/lean/extends_priority.lean.expected.out
@@ -1,18 +1,18 @@
 @[instance, priority 100, reducible]
-def B.to_A : Π {α : Type} [_ : B α], A α :=
+def B.to_A : Π {α : Type} [B α], A α :=
 λ (α : Type) [self : B α], [B.to_A self]
 @[instance, priority 37, reducible]
-def C.to_B : Π {α : Type} [_ : C α], B α :=
+def C.to_B : Π {α : Type} [C α], B α :=
 λ (α : Type) [self : C α], [C.to_B self]
 @[instance, priority 100, reducible]
-def D.to_C : Π {α : Type} [_ : D α], C α :=
+def D.to_C : Π {α : Type} [D α], C α :=
 λ (α : Type) [self : D α], [D.to_C self]
 @[instance, priority 100]
-def B'.to_A' : Π (α : Type) [_ : B' α], A' α :=
+def B'.to_A' : Π (α : Type) [B' α], A' α :=
 λ (α : Type) [self : B' α], A'.mk
 @[instance, priority 37]
-def C'.to_B' : Π (α : Type) [_ : C' α], B' α :=
+def C'.to_B' : Π (α : Type) [C' α], B' α :=
 λ (α : Type) [self : C' α], B'.mk
 @[instance, priority 100]
-def D'.to_C' : Π (α : Type) [_ : D' α], C' α :=
+def D'.to_C' : Π (α : Type) [D' α], C' α :=
 λ (α : Type) [self : D' α], C'.mk
diff --git a/tests/lean/interactive/info.lean.expected.out b/tests/lean/interactive/info.lean.expected.out
index 7d5ed2514c..7291bf9311 100644
--- a/tests/lean/interactive/info.lean.expected.out
+++ b/tests/lean/interactive/info.lean.expected.out
@@ -5,5 +5,5 @@
 {"record":{"full-id":"bool.tt","source":,"state":"⊢ bool","type":"bool"},"response":"ok","seq_num":7}
 {"record":{"doc":"(trace) enable/disable tracing for the given module and submodules"},"response":"ok","seq_num":10}
 {"record":{"full-id":"list.cons","source":,"state":"⊢ list bool","type":"Π {T : Type}, T → list T → list T"},"response":"ok","seq_num":13}
-{"record":{"full-id":"has_append.append","source":,"state":"⊢ list bool","type":"Π {α : Type} [_ : has_append α], α → α → α"},"response":"ok","seq_num":16}
+{"record":{"full-id":"has_append.append","source":,"state":"⊢ list bool","type":"Π {α : Type} [has_append α], α → α → α"},"response":"ok","seq_num":16}
 {"record":{"full-id":"id","source":,"type":"Π {α : Sort u}, α → α"},"response":"ok","seq_num":19}
diff --git a/tests/lean/out_param_proj.lean.expected.out b/tests/lean/out_param_proj.lean.expected.out
index 699977de92..8c41a7daa0 100644
--- a/tests/lean/out_param_proj.lean.expected.out
+++ b/tests/lean/out_param_proj.lean.expected.out
@@ -1,3 +1,3 @@
 @[instance, priority 100, reducible]
-def module.to_add_comm_group : Π {α : Type u} {β : Type v} {_inst_1 : ring α} [_ : module α β], add_comm_group β :=
+def module.to_add_comm_group : Π {α : Type u} {β : Type v} {_inst_1 : ring α} [module α β], add_comm_group β :=
 λ {α : Type u} (β : Type v) {_inst_1 : ring α} [self : module α β], [module.to_add_comm_group self]
diff --git a/tests/lean/pp_zero_bug.lean.expected.out b/tests/lean/pp_zero_bug.lean.expected.out
index ebefdab510..02d780192b 100644
--- a/tests/lean/pp_zero_bug.lean.expected.out
+++ b/tests/lean/pp_zero_bug.lean.expected.out
@@ -1,2 +1,2 @@
-has_zero.zero : Π {α : Type u_1} [_ : has_zero α], α
-has_zero.zero : Π [_ : has_zero ℕ], ℕ
+has_zero.zero : Π {α : Type u_1} [has_zero α], α
+has_zero.zero : Π [has_zero ℕ], ℕ
diff --git a/tests/lean/struct_class.lean.expected.out b/tests/lean/struct_class.lean.expected.out
index b4e2905cfc..a1ca840fc8 100644
--- a/tests/lean/struct_class.lean.expected.out
+++ b/tests/lean/struct_class.lean.expected.out
@@ -1,8 +1,8 @@
 @[class]
 structure point : Type u_1 → Type u_2 → Type (max u_1 u_2)
 fields:
-point.x : Π {A : Type u_1} (B : Type u_2) [_ : point A B], A
-point.y : Π (A : Type u_1) {B : Type u_2} [_ : point A B], B
+point.x : Π {A : Type u_1} (B : Type u_2) [point A B], A
+point.y : Π (A : Type u_1) {B : Type u_2} [point A B], B
 structure point2 : Type u_1 → Type u_2 → Type (max u_1 u_2)
 fields:
 point2.x : Π {A : Type u_1} {B : Type u_2}, point2 A B → A

From e483cf620be08a98d3edba14665dfebce4b77cb3 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Tue, 15 Nov 2022 14:09:37 +0100
Subject: [PATCH 7/8] extra tests for multiple binders

---
 tests/lean/pp_forall.lean              | 11 +++++++++++
 tests/lean/pp_forall.lean.expected.out | 11 +++++++++++
 2 files changed, 22 insertions(+)

diff --git a/tests/lean/pp_forall.lean b/tests/lean/pp_forall.lean
index 05e7ee31d7..237e78a4e3 100644
--- a/tests/lean/pp_forall.lean
+++ b/tests/lean/pp_forall.lean
@@ -11,3 +11,14 @@ variables (p q : Prop)
 #check Π {n : ℕ}, ℤ
 #check Π (n : ℕ), fin n
 #check ∀ n : ℕ, ¬∃ x : ℕ, x ≠ x
+#check Π (m n : ℕ), ℤ
+#check Π (m n : ℕ), fin m
+#check Π (m n : ℕ), fin n
+#check ∀ (m n : ℕ), 1 = 2
+#check ∀ (m n : ℕ), m = 1
+#check ∀ (m n : ℕ), n = 1
+#check ∀ (m n : ℕ), m = n
+#check ∀ (m : ℕ) (h : p), q ∧ m = 1
+#check ∀ (m : ℕ) (h : p), q
+#check ∀ (h : p) (m : ℕ), q ∧ m = 1
+#check ∀ (h : p) (m : ℕ), q
diff --git a/tests/lean/pp_forall.lean.expected.out b/tests/lean/pp_forall.lean.expected.out
index ebfb3eec51..2963707650 100644
--- a/tests/lean/pp_forall.lean.expected.out
+++ b/tests/lean/pp_forall.lean.expected.out
@@ -10,3 +10,14 @@ p → ℕ : Type
 Π {_ : ℕ}, ℤ : Type
 Π (n : ℕ), fin n : Type
 ∀ (_ : ℕ), ¬∃ (x : ℕ), x ≠ x : Prop
+ℕ → ℕ → ℤ : Type
+Π (m : ℕ), ℕ → fin m : Type
+ℕ → Π (n : ℕ), fin n : Type
+∀ (_ _ : ℕ), 1 = 2 : Prop
+∀ (m _ : ℕ), m = 1 : Prop
+∀ (_ n : ℕ), n = 1 : Prop
+∀ (m n : ℕ), m = n : Prop
+∀ (m : ℕ), p → q ∧ m = 1 : Prop
+∀ (_ : ℕ), p → q : Prop
+p → ∀ (m : ℕ), q ∧ m = 1 : Prop
+p → ∀ (_ : ℕ), q : Prop

From cf3b7c5fa86bac793e97804a2aef5a8613bb017e Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Tue, 15 Nov 2022 15:01:38 +0100
Subject: [PATCH 8/8] test showing limitation

---
 tests/lean/pp_forall.lean              | 12 ++++++++++++
 tests/lean/pp_forall.lean.expected.out |  2 ++
 2 files changed, 14 insertions(+)

diff --git a/tests/lean/pp_forall.lean b/tests/lean/pp_forall.lean
index 237e78a4e3..0abc392982 100644
--- a/tests/lean/pp_forall.lean
+++ b/tests/lean/pp_forall.lean
@@ -22,3 +22,15 @@ variables (p q : Prop)
 #check ∀ (m : ℕ) (h : p), q
 #check ∀ (h : p) (m : ℕ), q ∧ m = 1
 #check ∀ (h : p) (m : ℕ), q
+
+section
+-- A limitation due to use of relaxed weak head normal form:
+
+#check let Prop' := Prop, not' (p : Prop') := ¬ p in ∀ (p : Prop'), p → not' p
+-- shows ∀ (p : Prop') (_ : p), not' p
+
+abbreviation Prop' := Sort 0
+#check let not' (p : Prop') := ¬ p in ∀ (p : Prop'), p → not' p
+-- shows ∀ (p : Prop'), p → not' p
+
+end
diff --git a/tests/lean/pp_forall.lean.expected.out b/tests/lean/pp_forall.lean.expected.out
index 2963707650..1194567379 100644
--- a/tests/lean/pp_forall.lean.expected.out
+++ b/tests/lean/pp_forall.lean.expected.out
@@ -21,3 +21,5 @@ p → ℕ : Type
 ∀ (_ : ℕ), p → q : Prop
 p → ∀ (m : ℕ), q ∧ m = 1 : Prop
 p → ∀ (_ : ℕ), q : Prop
+let Prop' : Type := Prop, not' : Prop' → Prop := λ (p : Prop'), ¬p in ∀ (p : Prop') (_ : p), not' p : Prop
+let not' : Prop' → Prop := λ (p : Prop'), ¬p in ∀ (p : Prop'), p → not' p : Prop