diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
index f8f22f5b24..eaa559472c 100644
--- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
@@ -407,7 +407,8 @@ where
           match bInfos[i] with
           | BinderInfo.default =>
             if !(← valUnknown mvars[i]) && !(← read).inBottomUp && !(← isFunLike arg) then
-              annotateBool `pp.analysis.hole
+              if ← checkpointDefEq mvars[i] arg then
+                annotateBool `pp.analysis.hole
 
           | BinderInfo.implicit =>
             if (← valUnknown mvars[i] <||> higherOrders[i]) && !forceRegularApp then