prove_goal_async fails when there are instances in the context

[rwbarton]

Prerequisites

• [x] 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.
    • Specifically, check out the wishlist, open RFCs, or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

The first thing prove_goal_async tries to do is revert everything in the context, but if there are frozen instances then this fails.

Steps to Reproduce

example {α : Type} [inhabited α] (x : α) : x = x :=
begin
do
  -- tactic.unfreeze_local_instances,
  tactic.prove_goal_async `[refl]
end

Expected behavior: The goal is solved

Actual behavior:

/home/rwbarton/lean/mathlib/obviously/bug.lean:3:0: error: failed to revert '_inst_1', it is a frozen local instance (possible solution: use tactic `tactic.unfreeze_local_instances` to reset the set of local instances)
state:
α : Type,
_inst_1 : inhabited α,
x : α
⊢ x = x

Uncommenting tactic.unfreeze_local_instances fixes this, but probably prove_goal_async should take care of this? The fact that it uses revert is an implementation detail.

In theory maybe should "refreeze" the originally frozen instances in the context in which the inner tactic will eventually run? Maybe it's not worth worrying about.

Reproduces how often: Always

Versions

Lean (version 3.11.0, commit fb3f3e88be8a, Release)

[gebner]

Now you know how old prove_goal_async is and how often it is used. :smile: Feel free to submit a PR adding unfreeze_local_instances if you want.

[rwbarton]

I think I am encountering other issues with prove_goal_async, so I will hold off for a bit.

Should prove_goal_async fail when the goal is not a Prop? Edit: by which I mean it currently doesn't fail; but this seems to lead to subsequent errors (e.g., I think it always creates a lemma, and then Lean will complain about not having VM code for the lemma when its type isn't a Prop).