When ltac is used in a notation, insert the variables bound by the notation as uconstr.

[CohenCyril]

Kind: bug fix

Fixes #8190, #3278 and #4728

• Entry added in CHANGES.

[CohenCyril]

Hi @JasonGross, both fiat-crypto and bedrock fail now... could you have a look?
Maybe one would need to insert additional let x' := open_constr:(x) in [...] in the code to restore compatiblity?

[herbelin]

I did not realize that it would solve 3 bugs at the same time!

Anyway, that's perfect to me. Maybe the CHANGES text might look a bit cryptic for a non-expert though. Assuming that this is acceptable for @gares and @JasonGross, I would either say something like "Notations expanding to expressions containing calls to ltac:(tac) now accept their arguments to have unresolved existential variables." or just say nothing.

[herbelin]

Seeing last comment by @CohenCyril at #8190, I realized that other fixes are possible, with other implications, which seem related to the above discussion on using type classes or not. I don't know if it is better to have the discussion here or there, but I copy-paste my answer:

Another fix could be to change instead the interpretation function for ConstrMayEval (ConstrTerm c) to interp_open_constr (or interp_open_constr_with_classes). Doing this change would have a bigger impact than just in ltac:(...) subterms of a notation. It would have the effect e.g. that

Goal nat.
let x := eval cbn in _ in exact (@id x 0).

works, while, currently, it fails with Cannot infer an internal placeholder of type "Type".. I'm not experienced enough in tactic programming to evaluate which semantics is better (if ever one is uniformly better, and, if the open_constr one, with type classes or not).

[JasonGross]

Hi @JasonGross, both fiat-crypto and bedrock fail now... could you have a look?

I am not sure what's up with bedrock running out of memory (@andres-erbsen, do you know?). For fiat-crypto, I've reported the issue as #8208. I can push a fix for this particular instance, though since I don't have this branch checked out locally, I'm not going to build all of fiat-crypto with it at the moment. Feel free to submit an overlay PR that wraps all the relevant bindings of Notation variables in constr:(...) (since they were previously interpreted as constr, wrapping them in constr is the appropriate backwards-compatible fix).

[JasonGross]

And, given that this is not a strictly backwards compatible fix (because things like match and cbv [..] don't automatically coerce uconstr to constr), I think it does not qualify for backporting to 8.8.2. (@Zimmi48 , is this correct?)

open_constr has been changed to uconstr, as I requested

[JasonGross]

It seems like it might be better to fix #4425 and #8208 than to have to wrap things in constr:(...) when using them from notations.... @ppedrot, what do you think?

[Zimmi48]

Indeed, the need for overlays makes this a non-backportable fix in the end. Sorry @CohenCyril, you'll have to backtrack on creating the new CHANGES section and move this back where it was initially.

[ppedrot]

I don't quite like the fact that Ltac automatically performs coercions to emulate dynamic subtyping. This really doesn't scale (e.g. what about lists of uconstrs?).

The same kind of problem with term notations will arise in Ltac2 and by design there is no way there to get the runtime to perfom coercion. That means that the type of variables coming from notations would be uconstr rather than constr. Unluckily uconstr are not really well supported, be it in Ltac1 or Ltac2, as they rely on hacks in the pretyper to be correctly closed over. I am personally really not happy about their implementation and I don't think we should encourage their use. In Ltac2, I'd definitely use a thunk unit -> constr instead, this naturally handles all the closure fuss at the price of less flexibility (e.g. no way to set the typeclass resolution flag), although this could be solved by taking the flags as arguments.

Therefore, for the time being I think I'd rather prefer having Ltac1 taking term notation arguments as open_constr, as they share the same runtime representation as constr, even though this goes against potential flexibility. This would provide better backward compatibility.

[andres-erbsen]

Other than performance (which is how uconstr is introduced in the manual), what flexibility does uconstr provide? I do find myself writing unshelve (idtac; let e := open_constr:(_) in sometac (f e)); shelve_unifiable to get the behavior I intuitively expect from standard library tactics, but I guess I have not yet been corrupted enough to use uconstr for anything other than making working code run faster. I do remember using coq8.4 context[] to work with ill-typed terms, but apparently @JasonGross was able to port the code to work with typed terms when tactics in terms happened. So what is there that can be done with uconstr but not with open_constr under a hypthetical extended context?

[JasonGross]

@andres-erbsen:

• uconstr can be used to describe patterns that can be matched against multiple different constrs
• uconstrs can be discarded, but open_constrs must always be filled with terms
• uconstrs permit the user to decide whether or not typeclass resolution should happen in their holes, but open_constrs force a lack of typeclass resolution (this may break backwards compatibility in various places?)

@ppedrot I'm not convinced. Note that Ltac1 already dynamically casts uconstr to constr in some locations. For example, let v := uconstr:(I) in pose v. works just fine. So does

Tactic Notation "mycbv" constr(c) tactic3(tac) := let v := eval cbv in c in tac v.
Goal True.
  let v := uconstr:(I) in mycbv v (fun v' => pose v').

I think this support should be extended to constructions like match, lazymatch, cbv, etc, and then I think Ltac1 notations should bind arguments as uconstr.

In Ltac2 describing things as flags -> constr seems fine. In fact, defining uconstr in Ltac2 to be flags -> constr seems probably fine.

[Zimmi48]

Traditionally, this section was called "Changes beyond 8.8" to avoid anticipating too much (and was renamed at release time). Now, a 8.8.2 should indeed likely happen so this section title will likely reveal accurate.

[herbelin]

How to make this PR progress?

Is there an agreement on uconstr vs open_constr?

My alternative proposal here is probably better than encoding an ltac:(), but I guess that the uconstr vs open_constr will be relevant there too (and with the additional question of trying to infer or not the instances).

[CohenCyril]

I actually have no clue how to decide which of the four options (i.e. {your first proposal, your alternative proposal} * {uconstr, open_constr} ...)

[herbelin]

@CohenCyril: re-reading the discussion, my feeling is that answering the uconstr vs open_constr question would require first the implementation of some related features, like giving a better user control to type-class resolution, like not instantiating too many holes of a term so that the same term can be matched against several disjoint patterns.

So, my feeling is that to make this PR progress, one need to make a temporary somehow arbitrary choice. We can keep it as it is. We can throw a dice. If you have some more time to dedicate to the PR, I can make a choice for you. If not, as far as I'm concerned, I'd be happy as it is.

[ppedrot]

In any case, I think this is too big a change for 8.9, as it will break subtle code in the wild. If anything, let's have a technical discussion and postpone this to 8.10.

[SkySkimmer]

Looks like there are design problems which need to be worked out. A PR is not the place for that, try an issue, cep or maybe discourse thread.