Ltac2: deprecate the current implementation of `refine` in favor of `unshelve eexact`?

[JasonGross]

As I understand it, Control.refine f and Control.unshelve (fun () => let c := f () in eexact $f) should have the same behavior modulo side-condition ordering.

Today I have run into an issue much like #20628 where Control.refine (fun () => c) instantiates some evar which occurs neither in c nor the type of c nor in the goal type (and which I believe is not a class).

If we can, I propose that we deprecate the current behavior of Control.refine and re-implement it with unshelve and eexact, unless there is something particularly important about the current quirks.

[ppedrot]

FTR eexact uses the legacy unification algorithm whereas refine doesn't , so there is no chance we implement the latter with the former.

[SkySkimmer]

FTR eexact uses the legacy unification algorithm

No AFAIK

EDIT ltac1 eexact does, but not ltac2 eexact

[SkySkimmer]

Note that in ltac2 eexact takes a preterm but refine takes a constr. Turning a thunked constr into a preterm (I guess preterm:(ltac2:(let c := c() in exact $c)) is not necessarily faithful to the desired behaviour.

[ppedrot]

I'm am a strong proponent of having basic tactics that don't do magic, and refine is one of them (modulo unification, obviously). Starting to turn thunks into preterms is definitely magic.

[SkySkimmer]

What we could do is implement refine in terms of unification + exact_no_check

[JasonGross]

Am I missing something? Is the thunking in Control.refine used for more than management of the shelved status of goals, i.e., is Control.refine (fun () => f ()) not identical to unshelve (fun () => let c := f () in Control.refine (fun () => c))?
(I know that in Ltac1, the goal order of unshelve (refine and simple refine differ, but if there's a similar issue here, I'd consider it a bug that we can't separate the ordering behavior from refining.)

Also, as I understand it, let p := preterm:($c) in constr:($preterm:p) should be a no-op on valid constrs (I guess it does retyping or something and so will fail on unbound rels?). Is there some unfaithfulness/magic going on here?

What we could do is implement refine in terms of unification + exact_no_check

Indeed, if refine uses a different flavor of unification than (e)exact, I'd very much like to see this exposed user-side in Ltac2. Currently (e)exact is implemented as pretyping + exact_no_check. I guess refine would be implemented as unshelve (fun () => let c := f () in Unification.unify (Constr.type c) (Control.goal ()) in exact_no_check c)? (Or are the arguments passed to unify in the opposite order?)

[SkySkimmer]

Indeed, if refine uses a different flavor of unification than (e)exact

It does not.
Instead of making wild guesses about what's causing your problem you should post it as an issue.

[JasonGross]

Okay, on my concrete issue, Control.refine (fun () => f ()) results in (improper) instantiation of additional evars, relative to Control.unshelve (fun () => let c := f () in Control.refine (fun () => c)). What is refine doing differently than unshelve?

(I will post an example when I manage to minimize it.)