notations/syndefs with parameters applied to holes result in tac-in-term not being executed

[CohenCyril]

Version

The Coq Proof Assistant, version 8.8.1 (July 2018)
compiled on Jul 25 2018 17:35:15 with OCaml 4.06.0

Operating system

Linux 4.16.0-1-amd64 SMP Debian 4.16.5-1 (2018-04-29) x86_64 GNU/Linux

Description of the problem

I do not understand why the following two uses of have do not give the same result...
(I expect both to succeed, like the second one, by generalizing over left evars)

(updated code)

Notation zero := (ltac: (exact 0)).

Definition f (m n : nat) : nat := m.
Notation fzero m := (f zero m).

Lemma test : False.
Fail eset (H := fzero _).
eset (H := f zero _).
Abort.

(updated code)
The same problem happens when expanding the first notation inside the second:

Definition f (m n : nat) : nat := m.
Notation f_exact_zero m := (f (ltac: (exact 0)) m).

Lemma test : False.
Fail eset (H := f_exact_zero _).
eset (H := f (ltac: (exact 0)) _).
Abort

EDIT: however, if the notation is fully instanciated, there is no problem:

Definition f (m n : nat) : nat := m.
Notation f_exact_zero m := (f (ltac: (exact 0)) m).

Lemma test : False.
eset (H := f_exact_zero 0).
Abort.

@gares do you understand this?

[CohenCyril]

@maximedenes this is my problem...

[maximedenes]

A related issue:

Require Import ssreflect.
Notation foo := _.
Goal True.
have := foo.

produces a goal shown as foo (evar not generalized it seems).

[CohenCyril]

And by the way, the same problem goes for rewrite:

Require Import ssreflect.

Notation lt := (ltac: (exact tt)).

Definition f (u' u : unit) : u = u' :=
  match u, u' with tt, tt => eq_refl end.

Notation flt u := (f lt u).

Lemma test (u : unit) : u = tt.
Fail have := flt _.
(* The command has indeed failed with message: *)
(* Ltac call to "have (ssrhavefwdwbinders)" failed. *)
(* Cannot infer an internal placeholder of type "Type" in environment: *)
(* u : unit *)
have := f lt _.
Fail rewrite [u](flt _). (* same error *)
rewrite [u](f lt _).
done.
Qed.

[gares]

I think the notation is not affecting have...

Require Import ssreflect.
Notation foo := _ (only parsing).
Goal True.
have := foo.

[gares]

Notations are affecting tactic in terms, the bug has nothing to do with ssr:

Notation zero := (ltac: (exact 0)).
Definition f (m n : nat) : nat := m.
Notation fzero m := (f zero m).
Lemma test : False.
Fail eassert (H : fzero _ = 3). (* no space, notation with an indirect use of tac in terms *)
eassert (H : f zero _ = 3).

[gares]

The behavior is the following:

• if a term uses a notation with an ltac:.. inside, things are fine (interp_open_constr evaluates the ltac code).
• if a term contains a notation that contains a notation with an ltac:.. then the ltac code is not evaluated and the evar is let ther.

To me there are two bugs here:

• notations/sydefs do somehow remove the "ltac decoration" from the GHole node
• eassert complains about unresolved evars (coming from this oblivious kind of GHole)... shouln't it be ok with it? How many kinds of GHole are there?

[gares]

@CohenCyril could you update the first message of this PR with a pointer down here?

[gares]

My bet is that notations are stores as fully developed. Indeed the second notation emits a warning that it cannot be used for printing, since it contains some ltac code. It does not, but uses another notation that does. Maybe this inlining breaks the ltac-annotated GHole.

[CohenCyril]

The bug is affected by the presence of parameters in the notations, because this works:

Notation zero := (ltac: (exact 0)).
Definition f (m n : nat) : nat := m.
Notation fzero := (f zero).
Lemma test : False.
eassert (H : fzero = fun _ =>3).

[CohenCyril]

Actually, my bug happens ONLY with parameters, and when they are applied to holes when using the notation, cf third example in original post.

[gares]

One can reproduce the bug using Check so I removed the labels ltac and tactics

[gares]

The minimal example is

Notation zero := (ltac: (exact 0)).
Notation foo x := (x + zero).

(* Let's use foo, the offending notation with a parameter *)
Check foo 1.
Fail Check foo _. (* here I pass _ for the parameter *)

(* Now I get rid of `foo` and do the unfolding by hand *)
Check (1 + zero).
Check (_ + zero).

[herbelin]

Hi, the problem seems to be a bit tricky. The notation (roughly) generates the following Ltac code:

Check ltac:(let x := (eval cbn in _) in exact 0).

which indeed fails. (Note: it should be an identity conversion rather than cbn but I don't know how to express this in the syntax.)

Ideally, one should generate instead the code

Check ltac:(let a := open_constr:(_) in exact a).

internally using a TacGeneric with the appropriate tag. This is in Tacintern.notation_subst. Don't hesitate to give it a try, that would be wonderful.

[gares]

I must confess I do not understand your message at all, and I don't have time to learn this part of the system I've never looked at. Please just confirm I've assigned the bug to the right persons.

[herbelin]

Sorry for not having been clear. When there is an ltac:(tactic dependent on some arguments) in a notation (as found in Constrinterp.instantiate_notation_constr, case NHole), it is elaborated into Ltac code. To pass the arguments of the notation to the tactic, the arguments are added in front of the tactic code using Ltac's lets. It is this macrogeneration (in Tacintern.notation_subst via Genintern.generic_substitute_notation) which has to be fixed.

This code was initially written by @ppedrot but I'm also knowledgeable to fix it. So, it basically depends on the urgency for a fix. I must confess that I don't have time to work on it today, which means basically that it shall get tomorrow a level of priority comparable to a lot of pending things I have to do, and this is why I was asking whether you would be interested to look at it, first to get it fixed quickly, second thinking that you may have been interested in getting more expertise in notations, since getting more expertise in notations shall never be useless. In any case, the assignees are indeed appropriate persons.

[CohenCyril]

When there is an ltac:(tactic dependent on some arguments)

Hi @herbelin, it seems to me that in the example Notation zero := (ltac: (exact 0)). there is no argument in the tactic. Where does your let x := (eval cbn in _) in come from in your example?

[herbelin]

@CohenCyril: What matters in the example is the argument to foo when foo x expands to x + ltac: (exact 0). Doing an analysis of variables which occur effectively would indeed be another direction to fix this issue, since, here ltac: (exact 0) does not depend on x. But it would not fix e.g.:

Notation foo x := (1 + ltac:(exact (@id x 1))).
Check foo _.

I've seen examples where collecting ltac variables which effectively occur could be useful. So, both directions (i.e. moving the constr's passed to ltac to open_constr's and avoiding passing the arguments which do not occur) are indeed worth.

[CohenCyril]

@herbelin oh ok, I think I understand now! Thanks

[CohenCyril]

@herbelin I played a little bit to understand where the cbn happened and I do not find it. The code you mention uses

let c = ConstrMayEval (ConstrTerm c) in [...]

and not something like

let cbn = Cbn {rBeta = true; rMatch = true; rFix = true; rCofix = true;
                   rZeta = true; rDelta = true; rConst = []} in
let c = ConstrMayEval (ConstrEval (cbn, c)) in [...]

[herbelin]

@CohenCyril:

I played a little bit to understand where the cbn happened and I do not find it

Great.

The code you mention uses

let c = ConstrMayEval (ConstrTerm c) in [...]

Yes, there is no cbn in the code. I'm very sorry to have introduced a confusion by talking about cbn as I only wanted to build a parsable Coq equivalent of what is in the OCaml code. I did not know how to tell to build a ConstrMayEval (ConstrTerm c) from the concrete syntax, so I used a dummy cbn as a replacement to an absent conversion function.

So, yes, this is the line, and I suspect it could be replaced by a TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_open_constr) c) or something like that (there are examples of use of TacGeneric in the ssr or setoid_ring plugins). By doing so, if I'm not mistaken, this would build the expression let x := open_constr:(x) in exact 0 which shall not fail on _.

[CohenCyril]

@herbelin the exact code you gave fixed my problem. I still do not understand what the identity conversion (ConstrMayEval (ConstrTerm c)) is supposed to do compared to TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_open_constr) c) and whether there should also be a primitive for the latter, but I'm submitting a pull request #8200 and people can discuss it there, I suppose...

[herbelin]

I still do not understand what the identity conversion (ConstrMayEval (ConstrTerm c)) is supposed to do compared to TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_open_constr) c) and whether there should also be a primitive for the latter, but I'm submitting a pull request #8200 and people can discuss it there, I suppose...

This is a very good question. Using ConstrMayEval (ConstrTerm c) fails because its interpretation function Tacinterp.interp_constr_may_eval interprets c with the function interp_constr and this latter function checks that all holes are resolved. This means that 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). Maybe @JasonGross has an opinion.

[JasonGross]

Where is ConstrMayEval (ConstrTerm c) used, currently? I suspect I would have an opinion, if I knew the scope of what this change would do.

(However, I believe that The Correct thing to do, given the current scope of notations, is interpret binders as ident and non-binders as uconstr, for Notation.)

[maximedenes]

@CohenCyril did you have some code that fixed this issue? Was it ever submitted as a PR?

[JasonGross]

There is code at #8200 It stalled for lack of a good option. In particular:

• if we pass in terms as uconstr, then in order to, e.g., match on the variable, you need to first wrap it in constr:(...) (backwards incompatibly)
• if we pass in variables as open_constr, then typeclasses are not resolved, holes from unused variables stick around as evars, etc
• if we pass in variables as constr, then we run into the current problems

I think the ideal design is using uconstr (or preterm in Ltac2?), and having automatic coercions from uconstr to constr, but this is probably too invasive a change to make for Ltac1, and goes in the wrong direction for Ltac2.

[ppedrot]

IIRC in Ltac2 the problem is already solved since you get a preterm in the notation expansion. So you can do whatever you want with it (in theory, no pretyping knobs are exported currently).