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

If refine is used on an expression which includes an existing goal, then that goal will appear twice in the resulting tactic state. Example:

example : True := by
  have : True := ?a
  refine ?a -- two `case a`s in the infoview

Steps to Reproduce

1. Create a side goal.
2. refine a term which elaborates to include that goal.

Expected behavior: The goal appears only once in the infoview.

Actual behavior: The goal appears twice in the infoview.

Reproduces how often: Always

Versions

4.0.0-rc4, macOS Ventura 13.4.1 (Intel-based)

Additional Information

This occurs because withCollectingNewGoalsFrom returns all mvars encountered in the elaborated expression, and refineCore simply replaces the main goal with a list of all such goals, even if they exist on the goal list already. There are multiple ways to resolve this; some options are discussed on zulip.