Tactics in terms sometimes run twice on failure, giving exponential slowdown in failing cases

[JasonGross]

Version

8.7.0

Operating system

Linux

Description of the problem

Consider this:

Goal True.
  idtac "begin";
    try (let v := constr:(match (1+1)%nat with
                          | O => ltac:(idtac "fail";
                                       let f := constr:(I : I) in
                                       exact True)
                          | S _ => True
                          end) in
         pose v);
    idtac "end".
  (* begin
fail
fail
end *)

If I nest this, I can see exponential growth in the number of times a tactic is run. All of these elements seem to be important:

• the Gallina match,
• that the failure comes from an ill-typed constr (some others work too: fail does not trigger double execution, but idtac k (for k unbound) does, as does trying to run a constr as a tactic; rewrite Datatypes.S triggers double execution, but rewrite H (for unbound H) does not),

This shows up in my reification routine, and it is hard to work around in a way that preserves error messages.

[ppedrot]

Random thought: could that come from the pattern-matching compilation algorithm? Otherwise I don't see what in tactics-in-term could produce that...

[JasonGross]

Is there a way to trace pattern matching compilation?

[JasonGross]

Oh, this is fascinating. This prints "fail" twice:

Ltac foo _ :=
  idtac "begin";
    try (let v := constr:(match (1+1)%nat with
                          | _ => ltac:(idtac "fail";
                                       let f := constr:(I : I) in
                                       exact True)
                          | _ => True
                          end) in
         pose v);
        idtac "end".
Goal True.
  foo ().

while this:

Ltac foo _ :=
  idtac "begin";
    try (let v := constr:(match (1+1)%nat with
                          | _ => True
                          | _ => ltac:(idtac "fail";
                                       let f := constr:(I : I) in
                                       exact True)
                          end) in
         pose v);
        idtac "end".
Goal True.
  foo ().

raises the uncatchable error "This clause is redundant."

[JasonGross]

This looks like a likely candidate:

coq/pretyping/cases.ml

Lines 1530 to 1549 in 8d176db

	if not (Flags.is_program_mode ()) && (isRel sigma orig || isVar sigma orig) then
	(* Try to compile first using non expanded alias *)
	try
	if initial then f orig (Retyping.get_type_of pb.env sigma orig)
	else just_pop ()
	with e when precatchable_exception e ->
	(* Try then to compile using expanded alias *)
	(* Could be needed in case of dependent return clause *)
	pb.evdref := sigma;
	f expanded expanded_typ
	else
	(* Try to compile first using expanded alias *)
	try f expanded expanded_typ
	with e when precatchable_exception e ->
	(* Try then to compile using non expanded alias *)
	(* Could be needed in case of a recursive call which requires to
	be on a variable for size reasons *)
	pb.evdref := sigma;
	if initial then f orig (Retyping.get_type_of pb.env !(pb.evdref) orig)
	else just_pop ()

[JasonGross]

And, indeed, we have

coq/pretyping/pretype_errors.ml

Lines 64 to 67 in 8d176db

	let precatchable_exception = function
	| CErrors.UserError _ | TypeError _ | PretypeError _
	| Nametab.GlobalizationError _ -> true
	| _ -> false

which seems to match pretty well with which errors are which

[ejgallego]

The magic of control by side-effect.

[herbelin]

Sorry for late answer, I did not realize it was about match.

Indeed, the algorithm for pattern-matching compilation is potentially "exponential" in that it may try two different forms of return clauses. If you give the return clause explicitly, it will write "fail" only once:

Definition a x := match x return Prop with
                          | O => ltac:(idtac "fail";
                                       let f := constr:(I : I) in
                                       exact True)
                          | S _ => True
                          end.

There were some attemps to unify the two attempts into one but the unification was not strong enough to handle the both forms into one.

There is another source of backtrack which is the one you highlighted (in compile_alias) but it is not in play in your example. Here is an example where it shows up:

Definition a x := match x  with
                          | S (S y as z) => ltac:(idtac "fail";
                                       let f := constr:(I : I) in
                                       exact True)
                          | _ => True
                          end.
(* "fail" printed four times *)

For this second source of backtrack, it would be good to do something too.

[JasonGross]

@herbelin Thanks! Indeed, adding return _ fixes my issue.

This is fairly surprising though, I think. I think the default behavior should be that tactics in terms in matches get run only once. It might be the case that being able to interleave tactic backtracking and pattern match compilation backtracking is useful (but I'm dubious). At the very least, the user should have to explicitly specify that they want this behavior, at the site of pattern match compilation / tactic usage, to get it.

[Zimmi48]

@JasonGross Is it still high priority?