fix: avoid delaborating with field notation if object is a metavariab…

…le (#6014)

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/474.lean.expected.out

@@ -3,6 +3,6 @@ y.add y
 fun y_1 => y.add y_1
 fun y => Nat.add FREE y
 fun (y : Nat) => Nat.add y y
-?m.add y
+Nat.add ?m y
 Nat.add (?m #0) #0
 fun y => (y.add y).add y

tests/lean/rewrite.lean.expected.out

@@ -2,7 +2,7 @@
 as bs : List α
 ⊢ as ++ bs ++ bs = as ++ (bs ++ bs)
 rewrite.lean:18:20-18:29: error: tactic 'rewrite' failed, did not find instance of the pattern in the target expression
-  ?as.reverse.reverse
+  (List.reverse ?as).reverse
 α : Type u_1
 as bs : List α
 ⊢ as ++ [] ++ [] ++ bs ++ bs = as ++ (bs ++ bs)

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

tests/lean/run/meta2.lean

@@ -597,8 +597,8 @@ withLocalDeclD `x nat $ fun x => do
 
 /--
 info: [Meta.debug] ----- tst30 -----
-[Meta.debug] (?_ x).succ
-[Meta.debug] ?_.succ
+[Meta.debug] Nat.succ (?_ x)
+[Meta.debug] Nat.succ ?_
 [Meta.debug] fun x => ?_
 -/
 #guard_msgs in

tests/lean/run/scopedunifhint.lean

@@ -35,7 +35,7 @@ argument
 has type
   Nat : Type
 but is expected to have type
-  ?_.α : Type _
+  Magma.α ?_ : Type _
 -/
 #guard_msgs in
 #check mul x x           -- Error: unification hint is not active
@@ -48,7 +48,7 @@ argument
 has type
   Nat × Nat : Type
 but is expected to have type
-  ?_.α : Type _
+  Magma.α ?_ : Type _
 -/
 #guard_msgs in
 #check mul (x, x) (x, x) -- Error: no unification hint
@@ -63,7 +63,7 @@ argument
 has type
   Nat : Type
 but is expected to have type
-  ?_.α : Type _
+  Magma.α ?_ : Type _
 -/
 #guard_msgs in
 #check x*x -- Error: unification hint is not active
@@ -81,7 +81,7 @@ argument
 has type
   Nat × Nat : Type
 but is expected to have type
-  ?_.α : Type _
+  Magma.α ?_ : Type _
 -/
 #guard_msgs in
 #check mul (x, x) (x, x) -- still error
@@ -109,7 +109,7 @@ argument
 has type
   Nat × Nat : Type
 but is expected to have type
-  ?_.α : Type _
+  Magma.α ?_ : Type _
 -/
 #guard_msgs in
 #check (x, x) * (x, x) -- error, local hint is not active after end of section anymore