fix: avoid delaborating with field notation if object is a metavariable

This PR prevents `Nat.succ ?_` from pretty printing as `?_.succ`, which should make `apply?` be more usable.

Closes #5993

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -245,13 +245,16 @@ def appFieldNotationCandidate? : DelabM (Option (Nat × Name)) := do
     | return none
   unless idx < e.getAppNumArgs do return none
   /-
-  There are some kinds of expressions that cause issues with field notation,
-  so we prevent using it in these cases.
-  For example, `2.succ` is not parseable.
+  There are some kinds of expressions that cause issues with field notation, so we prevent using it in these cases.
   -/
   let obj := e.getArg! idx
+  --  `(2).fn` is unlikely to elaborate.
   if obj.isRawNatLit || obj.isAppOfArity ``OfNat.ofNat 3 || obj.isAppOfArity ``OfScientific.ofScientific 5 then
     return none
+  -- `(?m).fn` is unlikely to elaborate. https://github.com/leanprover/lean4/issues/5993
+  -- We also exclude metavariable applications (these are delayed assignments for example)
+  if obj.getAppFn.isMVar then
+    return none
   return (idx, field)
 
 /--

tests/lean/run/5993.lean

@@ -0,0 +1,32 @@
+/-!
+# Avoid delaborating with field notation if object is a metavariable application.
+
+https://github.com/leanprover/lean4/issues/5993
+-/
+
+set_option pp.mvars false
+
+/-!
+No field notation notation here. Used to print `refine ?_.succ` and `refine ?_.snd`.
+-/
+
+/--
+info: Try this: refine Nat.succ ?_
+---
+info: Try this: refine Prod.snd ?_
+-/
+#guard_msgs in
+example : Nat := by
+  show_term refine Nat.succ ?_
+  show_term refine Prod.snd (α := Int) ?_
+  exact default
+
+/-!
+No field notation even under binders. (That is, be aware of delayed assignment metavariables.)
+-/
+
+/-- info: Try this: refine fun x => Nat.succ ?_ -/
+#guard_msgs in
+example : Nat → Nat := by
+  show_term refine fun _ => Nat.succ ?_
+  exact default