diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
index ecc59911b7..3cfc7d8d70 100644
--- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
@@ -303,14 +303,27 @@ where
     -- Unify with the expected type
     tryUnify (← inferType (mkAppN f args)) resultType
 
-    -- Collect explicit arguments that can be elaborated without expected type
     let mut bottomUps := mkArray args.size false
+
+    -- Collect explicit arguments that can be elaborated without expected type, with *no* top-down info
+    -- Note: we perform this before the next pass because we prefer simple bottom-ups to unify first before
+    -- more complex ones.
     for i in [:args.size] do
       if bInfos[i] == BinderInfo.default then
+        if (← valUnknown mvars[i]) && (← okBottomUp? args[i]).isSafe then
+          tryUnify args[i] mvars[i]
+          bottomUps := bottomUps.set! i true
+
+    -- Now, collect explicit arguments that can be elaborated with *incomplete* top-down info
+    for i in [:args.size] do
+      if !bottomUps[i] && bInfos[i] == BinderInfo.default then
         if (← valUnknown mvars[i]) && (← okBottomUp? args[i] mvars[i]).isSafe then
           tryUnify args[i] mvars[i]
           bottomUps := bottomUps.set! i true
-      else if bInfos[i] == BinderInfo.instImplicit then
+
+    -- Next, look at out params
+    for i in [:args.size] do
+      if bInfos[i] == BinderInfo.instImplicit then
         inspectOutParams args[i] mvars[i]
 
     -- Collect implicit higher-order arguments