From a84291641bf910e7e7ffeb563e6b6e407b92b0b1 Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@protonmail.com>
Date: Sat, 31 Jul 2021 07:37:08 -0700
Subject: [PATCH] fix: pp.analyze restriction on _

---
 src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean | 6 ++++--
 tests/lean/run/PPTopDownAnalyze.lean                   | 6 ++++++
 2 files changed, 10 insertions(+), 2 deletions(-)

diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
index 9992786920..ec3f0d6667 100644
--- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
@@ -321,10 +321,12 @@ partial def analyze (parentIsApp : Bool := false) : AnalyzeM Unit := do
     | Expr.bvar ..    => pure ()
 where
   analyzeApp := do
-    withKnowing true true $ analyzeAppStaged (← getExpr).getAppFn (← getExpr).getAppArgs
+    let couldBottomUp ← canBottomUp (← getExpr)
+    withReader (fun ctx => { ctx with inBottomUp := ctx.inBottomUp || (!ctx.knowsType && couldBottomUp) }) do
+      withKnowing true true $ analyzeAppStaged (← getExpr).getAppFn (← getExpr).getAppArgs
 
     if !(← read).knowsType then
-      if !(← canBottomUp (← getExpr)) then
+      if !couldBottomUp then
         annotateBool `pp.analysis.needsType
         withType $ withKnowing true false $ analyze
       else
diff --git a/tests/lean/run/PPTopDownAnalyze.lean b/tests/lean/run/PPTopDownAnalyze.lean
index c164af7615..0a451215d7 100644
--- a/tests/lean/run/PPTopDownAnalyze.lean
+++ b/tests/lean/run/PPTopDownAnalyze.lean
@@ -245,6 +245,12 @@ structure S2 where x : Unit
 #testDelab (fun (u : Unit) => { x := () : S2 }) ()
   expecting (fun (u : Unit) => { x := () : S2 }) ()
 
+#testDelab Eq.refl True
+  expecting Eq.refl _
+
+#testDelab (fun (u : Unit) => Eq.refl True) ()
+  expecting  (fun (u : Unit) => Eq.refl True) ()
+
 #testDelabN Nat.brecOn
 #testDelabN Nat.below
 #testDelabN Nat.mod_lt