From fe6f13d4f136d075515f649c49944e577b2255f6 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Mon, 7 Oct 2024 16:33:03 -0700
Subject: [PATCH] feat: add option `pp.mvars.delayed`
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Where before we had
```lean
#check fun x : Nat => ?a
-- fun x ↦ ?m.7 x : (x : Nat) → ?m.6 x
```
Now by default we have
```lean
#check fun x : Nat => ?a
-- fun x => ?a : (x : Nat) → ?m.6 x
```
in particular, delayed assignment metavariables such as `?m.7` pretty print using the name of the metavariable they are delayed assigned to, suppressing the arguments used in the delayed assignment (hence `?a` rather than `?a x`). Hovering over `?a` shows `?m.7 x`.

The benefit is that users can see the user-provided name in local contexts.

The original pretty printing behavior can be recovered using `set_option pp.mvars.delayed true`.

This PR also extends the documentation for holes and synthetic holes, with useful high-level technical details about what delayed assignments are.

(This PR supercedes #3494, which has a round-trippable notation for delayed assignments. The notation in this PR is unlikely to round trip, but it is better than the current situation, where delayed assignment metavariables never round trip.)
---
 src/Lean/Parser/Term.lean                     | 59 +++++++++++++++++--
 .../PrettyPrinter/Delaborator/Builtins.lean   | 19 ++++++
 .../PrettyPrinter/Delaborator/Options.lean    |  6 ++
 tests/lean/funParen.lean.expected.out         |  2 +-
 .../explicitAppInstHole.lean.expected.out     |  2 +-
 .../lean/interactive/hover.lean.expected.out  |  4 +-
 .../hoverBinderUndescore.lean.expected.out    | 12 ++--
 .../interactive/issue5021.lean.expected.out   |  8 +--
 tests/lean/match1.lean.expected.out           |  2 +-
 .../mulcommErrorMessage.lean.expected.out     |  4 +-
 tests/lean/namedHoles.lean.expected.out       |  4 +-
 tests/lean/run/4144.lean                      |  2 +-
 tests/lean/run/anonymous_ctor_error_msg.lean  |  2 +-
 ...gnableSyntheticOpaqueBug.lean.expected.out |  2 +-
 14 files changed, 102 insertions(+), 26 deletions(-)

diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index d5093b18ed1e..914c28ee8c92 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -140,11 +140,62 @@ def optSemicolon (p : Parser) : Parser :=
 /-- The universe of propositions. `Prop ≡ Sort 0`. -/
 @[builtin_term_parser] def prop := leading_parser
   "Prop"
-/-- A placeholder term, to be synthesized by unification. -/
+/--
+A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
+For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.
+
+The way this works is that holes create fresh metavariables.
+The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
+This is often known as *unification*.
+
+Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
+* In `match` patterns, holes are catch-all patterns.
+* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.
+
+Related concept: implicit parameters are automatically filled in with holes during the elaboration process.
+
+See also `?m` syntax (synthetic holes).
+-/
 @[builtin_term_parser] def hole := leading_parser
   "_"
-/-- Parses a "synthetic hole", that is, `?foo` or `?_`.
-This syntax is used to construct named metavariables. -/
+/--
+A *synthetic hole* (or *synthetic placeholder*), which stands for an unknown term that should should be synthesized using tactics.
+- `?_` creates a fresh metavariable with an auto-generated name.
+- `?m` either refers to a pre-existing metavariable named `m` or creates a fresh metavariable with that name.
+
+In particular, the synthetic hole syntax creates "synthetic opaque metavariables",
+the same kind of metavariable used to represent goals in the tactic state.
+
+Synthetic holes are similar to holes in that `_` also creates metavariables,
+but synthetic opaque metavariables have some different properties:
+- In tactics such as `refine`, only synthetic holes yield new goals.
+- When synthetic holes appear under binders, they capture local variables using a more complicated mechanism known as delayed assignment.
+- During elaboration, unification will not solve for synthetic opaque metavariables, they are "opaque".
+  This is to prevent counterintuitive behavior such as disappearing goals.
+
+## Delayed assigned metavariables
+
+This section gives a high-level overview of technical details of synthetic holes, which you should feel free to skip.
+When a synthetic hole appears under a binding construct, such as for example `fun (x : α) (y : β) => ?s`,
+the system creates a construct called a *delayed assignment*. This consists of
+1. A metavariable `?m` of type `α → β → γ` and whole local context is from the local context outside the `fun`,
+  where `γ` is the type of `?s`. (The type `γ` can depend on `α` and `β`.)
+2. A delayed assigment record associating `?m` to `?s` and the variables `#[x, y]` in the local context of `?s`
+
+Then, this function elaborates as `fun (x : α) (y : β) => ?m x y`, where one should understand `x` and `y` here
+as being De Bruijn indexes, since Lean uses the locally nameless encoding of lambda calculus.
+
+Once `?s` is fully solved for, in the sense that it can be fully instantiated as a metavariable-free term `e`,
+then we can make the assignment `?m := fun (x' : α) (y' : β) => e[x := x', y := y']`.
+(Implementation note: in practice, Lean only instantiates full applications `?m x' y'` of delayed assigned metavariables.)
+This delayed assignment mechanism is essential to the operation of basic tactics like `intro`,
+and a good mental model is that it is a way to "apply" the metavariable `?s` by substituting values in for some of its local variables.
+
+By default, delayed assigned metavariables pretty print with what they are delayed assigned to.
+The delayed assigned metavariables themselves can be pretty printed using `set_option pp.mvars.delayed true`.
+
+For more details, see the module docstrings in `Lean.MetavarContext`.
+-/
 @[builtin_term_parser] def syntheticHole := leading_parser
   "?" >> (ident <|> "_")
 /--
@@ -451,7 +502,7 @@ def withAnonymousAntiquot := leading_parser
 @[builtin_term_parser] def «trailing_parser» := leading_parser:leadPrec
   "trailing_parser" >> optExprPrecedence >> optExprPrecedence >> ppSpace >> termParser
 
-/-- 
+/--
 Indicates that an argument to a function marked `@[extern]` is borrowed.
 
 Being borrowed only affects the ABI and runtime behavior of the function when compiled or interpreted. From the perspective of Lean's type system, this annotation has no effect. It similarly has no effect on functions not marked `@[extern]`.
diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index e142d8e9f1cf..9145e99b6738 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -570,6 +570,25 @@ def withOverApp (arity : Nat) (x : Delab) : Delab := do
       withAnnotateTermInfo x
     delabAppCore (n - arity) delabHead (unexpand := false)
 
+@[builtin_delab app]
+def delabDelayedAssignedMVar : Delab := whenNotPPOption getPPMVarsDelayed do
+  let .mvar mvarId := (← getExpr).getAppFn | failure
+  let some decl ← getDelayedMVarAssignment? mvarId | failure
+  withOverApp decl.fvars.size do
+    let args := (← getExpr).getAppArgs
+    -- Only delaborate using decl.mvarIdPending if the delayed mvar is applied to fvars
+    guard <| args.all Expr.isFVar
+    withTypeAscription (cond := ← getPPOption getPPMVarsWithType) do
+      if ← getPPOption getPPMVars then
+        let mvarDecl ← decl.mvarIdPending.getDecl
+        let n :=
+          match mvarDecl.userName with
+          | .anonymous => decl.mvarIdPending.name.replacePrefix `_uniq `m
+          | n => n
+        `(?$(mkIdent n))
+      else
+        `(?_)
+
 /-- State for `delabAppMatch` and helpers. -/
 structure AppMatchState where
   info        : MatcherInfo
diff --git a/src/Lean/PrettyPrinter/Delaborator/Options.lean b/src/Lean/PrettyPrinter/Delaborator/Options.lean
index 504415155385..29a748e15b69 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Options.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Options.lean
@@ -95,6 +95,11 @@ register_builtin_option pp.mvars.withType : Bool := {
   group    := "pp"
   descr    := "(pretty printer) display metavariables with a type ascription"
 }
+register_builtin_option pp.mvars.delayed : Bool := {
+  defValue := false
+  group    := "pp"
+  descr    := "(pretty printer) display delayed assigned metavariables when true, otherwise display what they are assigned to"
+}
 register_builtin_option pp.beta : Bool := {
   defValue := false
   group    := "pp"
@@ -244,6 +249,7 @@ def getPPPrivateNames (o : Options) : Bool := o.get pp.privateNames.name (getPPA
 def getPPInstantiateMVars (o : Options) : Bool := o.get pp.instantiateMVars.name pp.instantiateMVars.defValue
 def getPPMVars (o : Options) : Bool := o.get pp.mvars.name pp.mvars.defValue
 def getPPMVarsWithType (o : Options) : Bool := o.get pp.mvars.withType.name pp.mvars.withType.defValue
+def getPPMVarsDelayed (o : Options) : Bool := o.get pp.mvars.delayed.name (pp.mvars.delayed.defValue || getPPAll o)
 def getPPBeta (o : Options) : Bool := o.get pp.beta.name pp.beta.defValue
 def getPPSafeShadowing (o : Options) : Bool := o.get pp.safeShadowing.name pp.safeShadowing.defValue
 def getPPProofs (o : Options) : Bool := o.get pp.proofs.name (pp.proofs.defValue || getPPAll o)
diff --git a/tests/lean/funParen.lean.expected.out b/tests/lean/funParen.lean.expected.out
index ff14986b4a4e..d4854c3661ad 100644
--- a/tests/lean/funParen.lean.expected.out
+++ b/tests/lean/funParen.lean.expected.out
@@ -1,4 +1,4 @@
 fun α [Repr α] => repr : (α : Type u_1) → [inst : Repr α] → α → Std.Format
 fun x y => x : (x : ?m) → ?m x → ?m
 funParen.lean:4:12-4:16: error: invalid pattern, constructor or constant marked with '[match_pattern]' expected
-fun x => ?m x : (x : ?m) → ?m x
+fun x => ?m : (x : ?m) → ?m x
diff --git a/tests/lean/interactive/explicitAppInstHole.lean.expected.out b/tests/lean/interactive/explicitAppInstHole.lean.expected.out
index 5b8f04d000f9..9b652e047138 100644
--- a/tests/lean/interactive/explicitAppInstHole.lean.expected.out
+++ b/tests/lean/interactive/explicitAppInstHole.lean.expected.out
@@ -4,5 +4,5 @@
  {"start": {"line": 4, "character": 29}, "end": {"line": 4, "character": 30}},
  "contents":
  {"value":
-  "```lean\ninstDecidableTrue : Decidable True\n```\n***\nA placeholder term, to be synthesized by unification. \n***\n*import Init.Core*",
+  "```lean\ninstDecidableTrue : Decidable True\n```\n***\nA *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.\nFor example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.\n\nThe way this works is that holes create fresh metavariables.\nThe elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.\nThis is often known as *unification*.\n\nNormally, all holes must be solved for. However, there are a few contexts where this is not necessary:\n* In `match` patterns, holes are catch-all patterns.\n* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.\n\nRelated concept: implicit parameters are automatically filled in with holes during the elaboration process.\n\nSee also `?m` syntax (synthetic holes).\n\n***\n*import Init.Core*",
   "kind": "markdown"}}
diff --git a/tests/lean/interactive/hover.lean.expected.out b/tests/lean/interactive/hover.lean.expected.out
index 516d51cd390b..200bc3da4519 100644
--- a/tests/lean/interactive/hover.lean.expected.out
+++ b/tests/lean/interactive/hover.lean.expected.out
@@ -507,7 +507,7 @@
   "end": {"line": 252, "character": 10}},
  "contents":
  {"value":
-  "```lean\nℕ\n```\n***\nA placeholder term, to be synthesized by unification. ",
+  "```lean\nℕ\n```\n***\nA *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.\nFor example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.\n\nThe way this works is that holes create fresh metavariables.\nThe elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.\nThis is often known as *unification*.\n\nNormally, all holes must be solved for. However, there are a few contexts where this is not necessary:\n* In `match` patterns, holes are catch-all patterns.\n* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.\n\nRelated concept: implicit parameters are automatically filled in with holes during the elaboration process.\n\nSee also `?m` syntax (synthetic holes).\n",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hover.lean"},
  "position": {"line": 252, "character": 11}}
@@ -573,7 +573,7 @@
  {"start": {"line": 269, "character": 2}, "end": {"line": 269, "character": 3}},
  "contents":
  {"value":
-  "```lean\nlet x :=\n  match 0 with\n  | x => 0;\nℕ\n```\n***\nA placeholder term, to be synthesized by unification. ",
+  "```lean\nlet x :=\n  match 0 with\n  | x => 0;\nℕ\n```\n***\nA *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.\nFor example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.\n\nThe way this works is that holes create fresh metavariables.\nThe elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.\nThis is often known as *unification*.\n\nNormally, all holes must be solved for. However, there are a few contexts where this is not necessary:\n* In `match` patterns, holes are catch-all patterns.\n* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.\n\nRelated concept: implicit parameters are automatically filled in with holes during the elaboration process.\n\nSee also `?m` syntax (synthetic holes).\n",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hover.lean"},
  "position": {"line": 272, "character": 4}}
diff --git a/tests/lean/interactive/hoverBinderUndescore.lean.expected.out b/tests/lean/interactive/hoverBinderUndescore.lean.expected.out
index c53f87cf026a..f254328c43bc 100644
--- a/tests/lean/interactive/hoverBinderUndescore.lean.expected.out
+++ b/tests/lean/interactive/hoverBinderUndescore.lean.expected.out
@@ -4,7 +4,7 @@
  {"start": {"line": 1, "character": 5}, "end": {"line": 1, "character": 6}},
  "contents":
  {"value":
-  "```lean\nNat\n```\n***\nA placeholder term, to be synthesized by unification. ",
+  "```lean\nNat\n```\n***\nA *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.\nFor example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.\n\nThe way this works is that holes create fresh metavariables.\nThe elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.\nThis is often known as *unification*.\n\nNormally, all holes must be solved for. However, there are a few contexts where this is not necessary:\n* In `match` patterns, holes are catch-all patterns.\n* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.\n\nRelated concept: implicit parameters are automatically filled in with holes during the elaboration process.\n\nSee also `?m` syntax (synthetic holes).\n",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hoverBinderUndescore.lean"},
  "position": {"line": 1, "character": 7}}
@@ -12,7 +12,7 @@
  {"start": {"line": 1, "character": 7}, "end": {"line": 1, "character": 8}},
  "contents":
  {"value":
-  "```lean\nBool\n```\n***\nA placeholder term, to be synthesized by unification. ",
+  "```lean\nBool\n```\n***\nA *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.\nFor example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.\n\nThe way this works is that holes create fresh metavariables.\nThe elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.\nThis is often known as *unification*.\n\nNormally, all holes must be solved for. However, there are a few contexts where this is not necessary:\n* In `match` patterns, holes are catch-all patterns.\n* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.\n\nRelated concept: implicit parameters are automatically filled in with holes during the elaboration process.\n\nSee also `?m` syntax (synthetic holes).\n",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hoverBinderUndescore.lean"},
  "position": {"line": 6, "character": 6}}
@@ -20,7 +20,7 @@
  {"start": {"line": 6, "character": 6}, "end": {"line": 6, "character": 7}},
  "contents":
  {"value":
-  "```lean\nNat\n```\n***\nA placeholder term, to be synthesized by unification. ",
+  "```lean\nNat\n```\n***\nA *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.\nFor example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.\n\nThe way this works is that holes create fresh metavariables.\nThe elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.\nThis is often known as *unification*.\n\nNormally, all holes must be solved for. However, there are a few contexts where this is not necessary:\n* In `match` patterns, holes are catch-all patterns.\n* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.\n\nRelated concept: implicit parameters are automatically filled in with holes during the elaboration process.\n\nSee also `?m` syntax (synthetic holes).\n",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hoverBinderUndescore.lean"},
  "position": {"line": 6, "character": 8}}
@@ -28,7 +28,7 @@
  {"start": {"line": 6, "character": 8}, "end": {"line": 6, "character": 9}},
  "contents":
  {"value":
-  "```lean\nBool\n```\n***\nA placeholder term, to be synthesized by unification. ",
+  "```lean\nBool\n```\n***\nA *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.\nFor example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.\n\nThe way this works is that holes create fresh metavariables.\nThe elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.\nThis is often known as *unification*.\n\nNormally, all holes must be solved for. However, there are a few contexts where this is not necessary:\n* In `match` patterns, holes are catch-all patterns.\n* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.\n\nRelated concept: implicit parameters are automatically filled in with holes during the elaboration process.\n\nSee also `?m` syntax (synthetic holes).\n",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hoverBinderUndescore.lean"},
  "position": {"line": 11, "character": 6}}
@@ -36,7 +36,7 @@
  {"start": {"line": 11, "character": 6}, "end": {"line": 11, "character": 7}},
  "contents":
  {"value":
-  "```lean\nNat\n```\n***\nA placeholder term, to be synthesized by unification. ",
+  "```lean\nNat\n```\n***\nA *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.\nFor example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.\n\nThe way this works is that holes create fresh metavariables.\nThe elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.\nThis is often known as *unification*.\n\nNormally, all holes must be solved for. However, there are a few contexts where this is not necessary:\n* In `match` patterns, holes are catch-all patterns.\n* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.\n\nRelated concept: implicit parameters are automatically filled in with holes during the elaboration process.\n\nSee also `?m` syntax (synthetic holes).\n",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///hoverBinderUndescore.lean"},
  "position": {"line": 11, "character": 8}}
@@ -44,5 +44,5 @@
  {"start": {"line": 11, "character": 8}, "end": {"line": 11, "character": 9}},
  "contents":
  {"value":
-  "```lean\nBool\n```\n***\nA placeholder term, to be synthesized by unification. ",
+  "```lean\nBool\n```\n***\nA *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.\nFor example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.\n\nThe way this works is that holes create fresh metavariables.\nThe elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.\nThis is often known as *unification*.\n\nNormally, all holes must be solved for. However, there are a few contexts where this is not necessary:\n* In `match` patterns, holes are catch-all patterns.\n* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.\n\nRelated concept: implicit parameters are automatically filled in with holes during the elaboration process.\n\nSee also `?m` syntax (synthetic holes).\n",
   "kind": "markdown"}}
diff --git a/tests/lean/interactive/issue5021.lean.expected.out b/tests/lean/interactive/issue5021.lean.expected.out
index e4179d64a8da..cba5a0e27fb5 100644
--- a/tests/lean/interactive/issue5021.lean.expected.out
+++ b/tests/lean/interactive/issue5021.lean.expected.out
@@ -4,7 +4,7 @@
  {"start": {"line": 1, "character": 9}, "end": {"line": 1, "character": 11}},
  "contents":
  {"value":
-  "```lean\nFalse\n```\n***\nParses a \"synthetic hole\", that is, `?foo` or `?_`.\nThis syntax is used to construct named metavariables. ",
+  "```lean\nFalse\n```\n***\nA *synthetic hole* (or *synthetic placeholder*), which stands for an unknown term that should should be synthesized using tactics.\n- `?_` creates a fresh metavariable with an auto-generated name.\n- `?m` either refers to a pre-existing metavariable named `m` or creates a fresh metavariable with that name.\n\nIn particular, the synthetic hole syntax creates \"synthetic opaque metavariables\",\nthe same kind of metavariable used to represent goals in the tactic state.\n\nSynthetic holes are similar to holes in that `_` also creates metavariables,\nbut synthetic opaque metavariables have some different properties:\n- In tactics such as `refine`, only synthetic holes yield new goals.\n- When synthetic holes appear under binders, they capture local variables using a more complicated mechanism known as delayed assignment.\n- During elaboration, unification will not solve for synthetic opaque metavariables, they are \"opaque\".\n  This is to prevent counterintuitive behavior such as disappearing goals.\n\n## Delayed assigned metavariables\n\nThis section gives a high-level overview of technical details of synthetic holes, which you should feel free to skip.\nWhen a synthetic hole appears under a binding construct, such as for example `fun (x : α) (y : β) => ?s`,\nthe system creates a construct called a *delayed assignment*. This consists of\n1. A metavariable `?m` of type `α → β → γ` and whole local context is from the local context outside the `fun`,\n  where `γ` is the type of `?s`. (The type `γ` can depend on `α` and `β`.)\n2. A delayed assigment record associating `?m` to `?s` and the variables `#[x, y]` in the local context of `?s`\n\nThen, this function elaborates as `fun (x : α) (y : β) => ?m x y`, where one should understand `x` and `y` here\nas being De Bruijn indexes, since Lean uses the locally nameless encoding of lambda calculus.\n\nOnce `?s` is fully solved for, in the sense that it can be fully instantiated as a metavariable-free term `e`,\nthen we can make the assignment `?m := fun (x' : α) (y' : β) => e[x := x', y := y']`.\n(Implementation note: in practice, Lean only instantiates full applications `?m x' y'` of delayed assigned metavariables.)\nThis delayed assignment mechanism is essential to the operation of basic tactics like `intro`,\nand a good mental model is that it is a way to \"apply\" the metavariable `?s` by substituting values in for some of its local variables.\n\nBy default, delayed assigned metavariables pretty print with what they are delayed assigned to.\nThe delayed assigned metavariables themselves can be pretty printed using `set_option pp.mvars.delayed true`.\n\nFor more details, see the module docstrings in `Lean.MetavarContext`.\n",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///issue5021.lean"},
  "position": {"line": 1, "character": 10}}
@@ -12,7 +12,7 @@
  {"start": {"line": 1, "character": 9}, "end": {"line": 1, "character": 11}},
  "contents":
  {"value":
-  "```lean\nFalse\n```\n***\nParses a \"synthetic hole\", that is, `?foo` or `?_`.\nThis syntax is used to construct named metavariables. ",
+  "```lean\nFalse\n```\n***\nA *synthetic hole* (or *synthetic placeholder*), which stands for an unknown term that should should be synthesized using tactics.\n- `?_` creates a fresh metavariable with an auto-generated name.\n- `?m` either refers to a pre-existing metavariable named `m` or creates a fresh metavariable with that name.\n\nIn particular, the synthetic hole syntax creates \"synthetic opaque metavariables\",\nthe same kind of metavariable used to represent goals in the tactic state.\n\nSynthetic holes are similar to holes in that `_` also creates metavariables,\nbut synthetic opaque metavariables have some different properties:\n- In tactics such as `refine`, only synthetic holes yield new goals.\n- When synthetic holes appear under binders, they capture local variables using a more complicated mechanism known as delayed assignment.\n- During elaboration, unification will not solve for synthetic opaque metavariables, they are \"opaque\".\n  This is to prevent counterintuitive behavior such as disappearing goals.\n\n## Delayed assigned metavariables\n\nThis section gives a high-level overview of technical details of synthetic holes, which you should feel free to skip.\nWhen a synthetic hole appears under a binding construct, such as for example `fun (x : α) (y : β) => ?s`,\nthe system creates a construct called a *delayed assignment*. This consists of\n1. A metavariable `?m` of type `α → β → γ` and whole local context is from the local context outside the `fun`,\n  where `γ` is the type of `?s`. (The type `γ` can depend on `α` and `β`.)\n2. A delayed assigment record associating `?m` to `?s` and the variables `#[x, y]` in the local context of `?s`\n\nThen, this function elaborates as `fun (x : α) (y : β) => ?m x y`, where one should understand `x` and `y` here\nas being De Bruijn indexes, since Lean uses the locally nameless encoding of lambda calculus.\n\nOnce `?s` is fully solved for, in the sense that it can be fully instantiated as a metavariable-free term `e`,\nthen we can make the assignment `?m := fun (x' : α) (y' : β) => e[x := x', y := y']`.\n(Implementation note: in practice, Lean only instantiates full applications `?m x' y'` of delayed assigned metavariables.)\nThis delayed assignment mechanism is essential to the operation of basic tactics like `intro`,\nand a good mental model is that it is a way to \"apply\" the metavariable `?s` by substituting values in for some of its local variables.\n\nBy default, delayed assigned metavariables pretty print with what they are delayed assigned to.\nThe delayed assigned metavariables themselves can be pretty printed using `set_option pp.mvars.delayed true`.\n\nFor more details, see the module docstrings in `Lean.MetavarContext`.\n",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///issue5021.lean"},
  "position": {"line": 7, "character": 9}}
@@ -20,7 +20,7 @@
  {"start": {"line": 7, "character": 9}, "end": {"line": 7, "character": 12}},
  "contents":
  {"value":
-  "```lean\nFalse\n```\n***\nParses a \"synthetic hole\", that is, `?foo` or `?_`.\nThis syntax is used to construct named metavariables. ",
+  "```lean\nFalse\n```\n***\nA *synthetic hole* (or *synthetic placeholder*), which stands for an unknown term that should should be synthesized using tactics.\n- `?_` creates a fresh metavariable with an auto-generated name.\n- `?m` either refers to a pre-existing metavariable named `m` or creates a fresh metavariable with that name.\n\nIn particular, the synthetic hole syntax creates \"synthetic opaque metavariables\",\nthe same kind of metavariable used to represent goals in the tactic state.\n\nSynthetic holes are similar to holes in that `_` also creates metavariables,\nbut synthetic opaque metavariables have some different properties:\n- In tactics such as `refine`, only synthetic holes yield new goals.\n- When synthetic holes appear under binders, they capture local variables using a more complicated mechanism known as delayed assignment.\n- During elaboration, unification will not solve for synthetic opaque metavariables, they are \"opaque\".\n  This is to prevent counterintuitive behavior such as disappearing goals.\n\n## Delayed assigned metavariables\n\nThis section gives a high-level overview of technical details of synthetic holes, which you should feel free to skip.\nWhen a synthetic hole appears under a binding construct, such as for example `fun (x : α) (y : β) => ?s`,\nthe system creates a construct called a *delayed assignment*. This consists of\n1. A metavariable `?m` of type `α → β → γ` and whole local context is from the local context outside the `fun`,\n  where `γ` is the type of `?s`. (The type `γ` can depend on `α` and `β`.)\n2. A delayed assigment record associating `?m` to `?s` and the variables `#[x, y]` in the local context of `?s`\n\nThen, this function elaborates as `fun (x : α) (y : β) => ?m x y`, where one should understand `x` and `y` here\nas being De Bruijn indexes, since Lean uses the locally nameless encoding of lambda calculus.\n\nOnce `?s` is fully solved for, in the sense that it can be fully instantiated as a metavariable-free term `e`,\nthen we can make the assignment `?m := fun (x' : α) (y' : β) => e[x := x', y := y']`.\n(Implementation note: in practice, Lean only instantiates full applications `?m x' y'` of delayed assigned metavariables.)\nThis delayed assignment mechanism is essential to the operation of basic tactics like `intro`,\nand a good mental model is that it is a way to \"apply\" the metavariable `?s` by substituting values in for some of its local variables.\n\nBy default, delayed assigned metavariables pretty print with what they are delayed assigned to.\nThe delayed assigned metavariables themselves can be pretty printed using `set_option pp.mvars.delayed true`.\n\nFor more details, see the module docstrings in `Lean.MetavarContext`.\n",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file:///issue5021.lean"},
  "position": {"line": 7, "character": 11}}
@@ -28,5 +28,5 @@
  {"start": {"line": 7, "character": 9}, "end": {"line": 7, "character": 12}},
  "contents":
  {"value":
-  "```lean\nFalse\n```\n***\nParses a \"synthetic hole\", that is, `?foo` or `?_`.\nThis syntax is used to construct named metavariables. ",
+  "```lean\nFalse\n```\n***\nA *synthetic hole* (or *synthetic placeholder*), which stands for an unknown term that should should be synthesized using tactics.\n- `?_` creates a fresh metavariable with an auto-generated name.\n- `?m` either refers to a pre-existing metavariable named `m` or creates a fresh metavariable with that name.\n\nIn particular, the synthetic hole syntax creates \"synthetic opaque metavariables\",\nthe same kind of metavariable used to represent goals in the tactic state.\n\nSynthetic holes are similar to holes in that `_` also creates metavariables,\nbut synthetic opaque metavariables have some different properties:\n- In tactics such as `refine`, only synthetic holes yield new goals.\n- When synthetic holes appear under binders, they capture local variables using a more complicated mechanism known as delayed assignment.\n- During elaboration, unification will not solve for synthetic opaque metavariables, they are \"opaque\".\n  This is to prevent counterintuitive behavior such as disappearing goals.\n\n## Delayed assigned metavariables\n\nThis section gives a high-level overview of technical details of synthetic holes, which you should feel free to skip.\nWhen a synthetic hole appears under a binding construct, such as for example `fun (x : α) (y : β) => ?s`,\nthe system creates a construct called a *delayed assignment*. This consists of\n1. A metavariable `?m` of type `α → β → γ` and whole local context is from the local context outside the `fun`,\n  where `γ` is the type of `?s`. (The type `γ` can depend on `α` and `β`.)\n2. A delayed assigment record associating `?m` to `?s` and the variables `#[x, y]` in the local context of `?s`\n\nThen, this function elaborates as `fun (x : α) (y : β) => ?m x y`, where one should understand `x` and `y` here\nas being De Bruijn indexes, since Lean uses the locally nameless encoding of lambda calculus.\n\nOnce `?s` is fully solved for, in the sense that it can be fully instantiated as a metavariable-free term `e`,\nthen we can make the assignment `?m := fun (x' : α) (y' : β) => e[x := x', y := y']`.\n(Implementation note: in practice, Lean only instantiates full applications `?m x' y'` of delayed assigned metavariables.)\nThis delayed assignment mechanism is essential to the operation of basic tactics like `intro`,\nand a good mental model is that it is a way to \"apply\" the metavariable `?s` by substituting values in for some of its local variables.\n\nBy default, delayed assigned metavariables pretty print with what they are delayed assigned to.\nThe delayed assigned metavariables themselves can be pretty printed using `set_option pp.mvars.delayed true`.\n\nFor more details, see the module docstrings in `Lean.MetavarContext`.\n",
   "kind": "markdown"}}
diff --git a/tests/lean/match1.lean.expected.out b/tests/lean/match1.lean.expected.out
index d816cd23c041..14f9bcfa50e7 100644
--- a/tests/lean/match1.lean.expected.out
+++ b/tests/lean/match1.lean.expected.out
@@ -21,7 +21,7 @@ constructor expected
 [false, true, true]
 match1.lean:136:7-136:22: error: invalid match-expression, type of pattern variable 'a' contains metavariables
   ?m
-fun x => ?m x : ?m × ?m → ?m
+fun x => ?m : ?m × ?m → ?m
 fun x =>
   match x with
   | (a, b) => a + b : Nat × Nat → Nat
diff --git a/tests/lean/mulcommErrorMessage.lean.expected.out b/tests/lean/mulcommErrorMessage.lean.expected.out
index c84c42700008..e2e6b0d8590e 100644
--- a/tests/lean/mulcommErrorMessage.lean.expected.out
+++ b/tests/lean/mulcommErrorMessage.lean.expected.out
@@ -1,5 +1,5 @@
 mulcommErrorMessage.lean:8:13-13:25: error: type mismatch
-  fun a b => ?m a b
+  fun a b => ?m
 has type
   (a : ?m) → (b : ?m a) → ?m a b : Sort (imax ?u ?u ?u)
 but is expected to have type
@@ -21,7 +21,7 @@ has type
 but is expected to have type
   false = true : Prop
 mulcommErrorMessage.lean:16:3-17:47: error: type mismatch
-  fun a b => ?m a b
+  fun a b => ?m
 has type
   (a : ?m) → (b : ?m a) → ?m a b : Sort (imax ?u ?u ?u)
 but is expected to have type
diff --git a/tests/lean/namedHoles.lean.expected.out b/tests/lean/namedHoles.lean.expected.out
index 626a786aea8b..85577d3d735f 100644
--- a/tests/lean/namedHoles.lean.expected.out
+++ b/tests/lean/namedHoles.lean.expected.out
@@ -9,10 +9,10 @@ but is expected to have type
 f ?x (sorryAx Bool true) : Nat
 g ?x ?x : Nat
 20
-foo (fun x => ?m x) ?hole : Nat
+foo (fun x => ?hole) ?hole : Nat
 bla ?hole fun x => ?hole : Nat
 namedHoles.lean:35:38-35:43: error: synthetic hole has already been defined with an incompatible local context
-boo (fun x => ?m x) fun y => sorryAx Nat true : Nat
+boo (fun x => ?hole) fun y => sorryAx Nat true : Nat
 11
 12
 namedHoles.lean:58:26-58:31: error: synthetic hole has already been defined and assigned to value incompatible with the current context
diff --git a/tests/lean/run/4144.lean b/tests/lean/run/4144.lean
index ff9d22bf6b5e..f4cae530b4f4 100644
--- a/tests/lean/run/4144.lean
+++ b/tests/lean/run/4144.lean
@@ -18,7 +18,7 @@ case refine'_4
 ⊢ ?refine'_1
 
 case refine'_5
-⊢ ¬(fun x => ?m.17 x) ?refine'_3 = (fun x => ?m.17 x) ?refine'_4
+⊢ ¬(fun x => ?m.16) ?refine'_3 = (fun x => ?m.16) ?refine'_4
 -/
 #guard_msgs in
 example : False := by
diff --git a/tests/lean/run/anonymous_ctor_error_msg.lean b/tests/lean/run/anonymous_ctor_error_msg.lean
index 665d41a29bac..a19e797a60f0 100644
--- a/tests/lean/run/anonymous_ctor_error_msg.lean
+++ b/tests/lean/run/anonymous_ctor_error_msg.lean
@@ -30,7 +30,7 @@ error: invalid constructor ⟨...⟩, expected type must be an inductive type 
 info: let x1 := { n := 1 };
 let x2 := { n := 2 };
 let x3 := { n := 3 };
-let x4 := ?_ x1 x2 x3;
+let x4 := ?_;
 let x5 := { n := 5 };
 let x6 := { n := 6 };
 Foo.sum [x1, x2, x3, x5, x6] : Foo
diff --git a/tests/lean/withAssignableSyntheticOpaqueBug.lean.expected.out b/tests/lean/withAssignableSyntheticOpaqueBug.lean.expected.out
index a21a5d6cbdde..ac3ca385f6a5 100644
--- a/tests/lean/withAssignableSyntheticOpaqueBug.lean.expected.out
+++ b/tests/lean/withAssignableSyntheticOpaqueBug.lean.expected.out
@@ -1,4 +1,4 @@
-fun x => ?m x
+fun x => ?m
 none
 (some (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)))
 0