Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

refine currently fails to include pre-existing natural metavariables from the refined term in the resulting goal list.

Steps to Reproduce

1. Create natural goals during a tactic proof. For example, constructor creates natural metavariables.
2. refine a term which explicitly references these natural metavariables by name (e.g. ?left).

Expected behavior: The resulting goal list should include all ?-style goals appearing in the term.

Actual behavior: Natural pre-existing metavariables referred to in the term do not appear in the resulting goal list, and can therefore be closed erroneously.

example : True ∧ True := by -- (kernel) declaration has metavariables '_example'
  constructor
  · refine ?left
  · refine ?right 

Reproduces how often: Always

Versions

4.0.0-nightly-2023-08-07, on MacOS Ventura (Intel-based).

Additional Information

Explanation & possible fix

I believe this is a bug in withCollectingNewGoalsFrom in elabTermWithHoles. Note that refine' does not suffer from this issue. refine and refine' differ only in the value of the argument allowNewMVars, which guides behavior in the following block:

    ...
    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
    ...

This properly distinguishes between new and old natural mvars for the purposes of error reporting, but fails to include the old natural mvars in the returned goals (and only returns syntheticMVarIds).

(Note that newMVarIds is simply what withCollectingNewGoalsFrom calls the collected MVarIds; mvarCounterSaved is what actually distinguishes "new" from "old", and this is not reflected in the variable names.)

Instead of separating synthetic mvars, we could simply look for ones which are both natural and new, and log and abort if we find them. If we make it through without aborting, then the MVarIds we've collected so far (newMVarIds) don't contain any erroneous mvars, and we can simply use them.

    unless allowNaturalHoles do
      let naturalMVarIds ← newMVarIds.filterM fun mvarId => return (← mvarId.getKind).isNatural
      let naturalMVarIds ← filterOldMVars naturalMVarIds mvarCounterSaved
      logUnassignedAndAbort naturalMVarIds
    let newMVarIds := newMVarIds.toList

More examples

Note that the behavior of refine' differs from refine. Contrast the above with

example : True ∧ True := by
  constructor
  · refine' ?right
    trivial
    -- note that this now occurs in the same goal focus;
    -- as expected, the current goal (`?left`) was replaced with `?right`

In general, consider

open Lean Meta Elab Tactic Term

elab "add_natural_goal" s:ident " : " t:term : tactic => do
  let g ← mkFreshExprMVar (← elabType t) .natural s.getId
  appendGoals [g.mvarId!]

elab "add_synthetic_goal" s:ident " : " t:term : tactic => do
  let g ← mkFreshExprMVar (← elabType t) .syntheticOpaque s.getId
  appendGoals [g.mvarId!]

We can see that it is indeed throwing away all natural goals; it's not just refining the main goal which causes the issue:

-- Buggy behavior:
-- Note that each focus ends with "no goals".
example : Bool × Nat := by -- (kernel) declaration has metavariables '_example'
  add_natural_goal d : Bool
  add_natural_goal e : Nat
  · refine (?d,?e)
  · refine ?d
  · refine ?e

example : Bool × Bool := by -- (kernel) declaration has metavariables '_example'
  add_natural_goal d : Bool
  add_natural_goal e : Bool
  · refine (?d,?e)
  · case d => refine ?e
  · refine ?e

-- Expected behavior:
example : Bool × Nat := by
  add_synthetic_goal d : Bool
  add_synthetic_goal e : Nat
  · refine (?d,?e) -- unsolved goals case d ⊢ Bool case e ⊢ Nat
  · refine ?d -- no goals to be solved
  · refine ?e

This was discussed briefly on zulip.

The possibility of opening a PR was mentioned in that thread; I'm happy to do so, but wanted to double-check here that it would be acceptable, given the contribution guidelines. :) In the meantime I've opened a draft PR at #2435.