fix: fixes #1681

src/Lean/Elab/BuiltinTerm.lean

@@ -55,7 +55,8 @@ private def elabOptLevel (stx : Syntax) : TermElabM Level :=
     elabPipeCompletion stx expectedType?
 
 @[builtinTermElab «hole»] def elabHole : TermElab := fun stx expectedType? => do
-  let mvar ← mkFreshExprMVar expectedType?
+  let kind := if (← read).inPattern || !(← read).holesAsSyntheticOpaque then MetavarKind.natural else MetavarKind.syntheticOpaque
+  let mvar ← mkFreshExprMVar expectedType? kind
   registerMVarErrorHoleInfo mvar.mvarId! stx
   pure mvar
 

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -83,29 +83,58 @@ def sortMVarIdsByIndex [MonadMCtx m] [Monad m] (mvarIds : List MVarId) : m (List
 /--
   Execute `k`, and collect new "holes" in the resulting expression.
 -/
-def withCollectingNewGoalsFrom (k : TacticM Expr) (tagSuffix : Name) (allowNaturalHoles := false) : TacticM (Expr × List MVarId) := do
-  let mvarCounterSaved := (← getMCtx).mvarCounter
-  let val ← k
-  let newMVarIds ← getMVarsNoDelayed val
-  /- ignore let-rec auxiliary variables, they are synthesized automatically later -/
-  let newMVarIds ← newMVarIds.filterM fun mvarId => return !(← Term.isLetRecAuxMVar mvarId)
-  let newMVarIds ← if allowNaturalHoles then
-    pure newMVarIds.toList
-  else
-    let naturalMVarIds ← newMVarIds.filterM fun mvarId => return (← mvarId.getKind).isNatural
-    let syntheticMVarIds ← newMVarIds.filterM fun mvarId => return !(← mvarId.getKind).isNatural
-    let naturalMVarIds ← filterOldMVars naturalMVarIds mvarCounterSaved
-    logUnassignedAndAbort naturalMVarIds
-    pure syntheticMVarIds.toList
+def withCollectingNewGoalsFrom (k : TacticM Expr) (tagSuffix : Name) (allowNaturalHoles := false) : TacticM (Expr × List MVarId) :=
   /-
-  We sort the new metavariable ids by index to ensure the new goals are ordered using the order the metavariables have been created.
-  See issue #1682.
-  Potential problem: if elaboration of subterms is delayed the order the new metavariables are created may not match the order they
-  appear in the `.lean` file. We should tell users to prefer tagged goals.
+  When `allowNaturalHoles = true`, unassigned holes should become new metavariables, including `_`s.
+  Thus, we set `holesAsSynthethicOpaque` to true if it is not already set to `true`.
+  See issue #1681. We have the tactic
+  ```
+  `refine' (fun x => _)
+  ```
+  If we create a natural metavariable `?m` for `_` with type `Nat`, then when we try to abstract `x`,
+  a new metavariable `?n` with type `Nat -> Nat` is created, and we assign `?m := ?n x`,
+  and the resulting term is `fun x => ?n x`. Then, `getMVarsNoDelayed` would return `?n` as a new goal
+  which would be confusing since it has type `Nat -> Nat`.
   -/
-  let newMVarIds ← sortMVarIdsByIndex newMVarIds
-  tagUntaggedGoals (← getMainTag) tagSuffix newMVarIds
-  return (val, newMVarIds)
+  if allowNaturalHoles then
+    withTheReader Term.Context (fun ctx => { ctx with holesAsSyntheticOpaque := ctx.holesAsSyntheticOpaque || allowNaturalHoles }) do
+      /-
+      We also enable the assignment of synthetic metavariables, otherwise we will fail to
+      elaborate terms such as `f _ x` where `f : (α : Type) → α → α` and `x : A`.
+
+      IMPORTANT: This is not a perfect solution. For example, `isDefEq` will be able assign metavariables associated with `by ...`.
+      This should not be an immediate problem since this feature is only used to implement `refine'`. If it becomes
+      an issue in practice, we should add a new kind of opaque metavariable for `refine'`, and mark the holes created using `_`
+      with it, and have a flag that allows us to assign this kind of metavariable, but prevents us from assigning metavariables
+      created by the `by ...` notation.
+      -/
+      withAssignableSyntheticOpaque go
+  else
+    go
+where
+  go := do
+    let mvarCounterSaved := (← getMCtx).mvarCounter
+    let val ← k
+    let newMVarIds ← getMVarsNoDelayed val
+    /- ignore let-rec auxiliary variables, they are synthesized automatically later -/
+    let newMVarIds ← newMVarIds.filterM fun mvarId => return !(← Term.isLetRecAuxMVar mvarId)
+    let newMVarIds ← if allowNaturalHoles then
+      pure newMVarIds.toList
+    else
+      let naturalMVarIds ← newMVarIds.filterM fun mvarId => return (← mvarId.getKind).isNatural
+      let syntheticMVarIds ← newMVarIds.filterM fun mvarId => return !(← mvarId.getKind).isNatural
+      let naturalMVarIds ← filterOldMVars naturalMVarIds mvarCounterSaved
+      logUnassignedAndAbort naturalMVarIds
+      pure syntheticMVarIds.toList
+    /-
+    We sort the new metavariable ids by index to ensure the new goals are ordered using the order the metavariables have been created.
+    See issue #1682.
+    Potential problem: if elaboration of subterms is delayed the order the new metavariables are created may not match the order they
+    appear in the `.lean` file. We should tell users to prefer tagged goals.
+    -/
+    let newMVarIds ← sortMVarIdsByIndex newMVarIds
+    tagUntaggedGoals (← getMainTag) tagSuffix newMVarIds
+    return (val, newMVarIds)
 
 def elabTermWithHoles (stx : Syntax) (expectedType? : Option Expr) (tagSuffix : Name) (allowNaturalHoles := false) : TacticM (Expr × List MVarId) := do
   withCollectingNewGoalsFrom (elabTermEnsuringType stx expectedType?) tagSuffix allowNaturalHoles

src/Lean/Elab/Term.lean

@@ -207,10 +207,19 @@ structure Context where
   inPattern        : Bool := false
   /-- Cache for the `save` tactic. It is only `some` in the LSP server. -/
   tacticCache?     : Option (IO.Ref Tactic.Cache) := none
-  /-- If `true`, we store in the `Expr` the `Syntax` for recursive applications (i.e., applications
-      of free variables tagged with `isAuxDecl`). We store the `Syntax` using `mkRecAppWithSyntax`.
-      We use the `Syntax` object to produce better error messages at `Structural.lean` and `WF.lean`. -/
+  /--
+  If `true`, we store in the `Expr` the `Syntax` for recursive applications (i.e., applications
+  of free variables tagged with `isAuxDecl`). We store the `Syntax` using `mkRecAppWithSyntax`.
+  We use the `Syntax` object to produce better error messages at `Structural.lean` and `WF.lean`. -/
   saveRecAppSyntax : Bool := true
+  /--
+  If `holesAsSyntheticOpaque` is `true`, then we mark metavariables associated
+  with `_`s as `synthethicOpaque` if they do not occur in patterns.
+  This option is useful when elaborating terms in tactics such as `refine'` where
+  we want holes there to become new goals. See issue #1681, we have
+  `refine' (fun x => _)
+  -/
+  holesAsSyntheticOpaque : Bool := false
 
 abbrev TermElabM := ReaderT Context $ StateRefT State MetaM
 abbrev TermElab  := Syntax → Option Expr → TermElabM Expr

tests/lean/1681.lean

@@ -0,0 +1,9 @@
+example : Nat → Nat := by
+  refine' (fun x => _)
+  trace_state
+  sorry
+
+example : Nat → Nat := by
+  refine' (fun x => ?_)
+  trace_state
+  sorry

tests/lean/1681.lean.expected.out

@@ -0,0 +1,6 @@
+1681.lean:1:0-1:7: warning: declaration uses 'sorry'
+x : Nat
+⊢ Nat
+1681.lean:6:0-6:7: warning: declaration uses 'sorry'
+x : Nat
+⊢ Nat