From d1a99d8d45a3460f9150997201345aadc398ab19 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Fri, 8 Nov 2024 12:57:37 -0800
Subject: [PATCH] fix: avoid delaborating with field notation if object is a
 metavariable (#6014)

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

Closes #5993
---
 .../PrettyPrinter/Delaborator/Builtins.lean   |  9 ++++--
 tests/lean/474.lean.expected.out              |  2 +-
 tests/lean/rewrite.lean.expected.out          |  2 +-
 tests/lean/run/5993.lean                      | 32 +++++++++++++++++++
 tests/lean/run/meta2.lean                     |  4 +--
 tests/lean/run/scopedunifhint.lean            | 10 +++---
 6 files changed, 47 insertions(+), 12 deletions(-)
 create mode 100644 tests/lean/run/5993.lean

diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 277078e464..b81d514199 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/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)
 
 /--
diff --git a/tests/lean/474.lean.expected.out b/tests/lean/474.lean.expected.out
index b656f5c6b1..0bb9fb7d33 100644
--- a/tests/lean/474.lean.expected.out
+++ b/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
diff --git a/tests/lean/rewrite.lean.expected.out b/tests/lean/rewrite.lean.expected.out
index d848327ad7..8757fb8ced 100644
--- a/tests/lean/rewrite.lean.expected.out
+++ b/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)
diff --git a/tests/lean/run/5993.lean b/tests/lean/run/5993.lean
new file mode 100644
index 0000000000..b96ec43370
--- /dev/null
+++ b/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
diff --git a/tests/lean/run/meta2.lean b/tests/lean/run/meta2.lean
index 26b9130d7c..c2096ce305 100644
--- a/tests/lean/run/meta2.lean
+++ b/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
diff --git a/tests/lean/run/scopedunifhint.lean b/tests/lean/run/scopedunifhint.lean
index bb8fdd5c9a..09125d2521 100644
--- a/tests/lean/run/scopedunifhint.lean
+++ b/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