Quentin VERMANDE (Nov 13 2023 at 16:15): Quentin VERMANDE (Nov 13 2023 at 16:15):Hi. I have come accross an infinite loop that I can not explain. Usually this happens when make a mistake in the term I return, but here the control flow does not even reach the end of the predicate.
I declare a class C with two parameters and a structure S bundling the second parameter with an associated instance of C. I declare a coercion from the first parameter to S, which builds the instance of C using coq.elaborate-skeleton and an instance of C 1 b that builds an element x of S 0 whose first fields is b and then the instance using x. Now, when I try to coerce something to S 1, the coercion triggers, then the tc predicate triggers. It tries to coerce something to S 0, which triggers again the tc predicate, which in turn fails because there is no clause that can build an instance of C 0 b. Here, I would expect the elaboration to stop and either fail or return an incomplete term, but instead the tc predicate triggers again with the same argument as the first time, leading to an infinite loop.
Why is the predicate called again and how can it be called with arguments that are completely unrelated to the elaboration problem at hand? Is there a way to prevent this?
The code ```
From elpi.apps Require Import tc coercion.
Class C (N : nat) (b : bool) : Prop := Mem { IsMem : True }.
Structure S (N : nat) := {
sb : bool;
_ : C N sb
}.
Elpi Accumulate coercion.db lp:{{
coercion _ B T E R :-
coq.unify-eq E {{ @S lp:N }} ok,
coq.unify-eq T {{ bool }} ok,
coq.elaborate-skeleton {{ @Build_S lp:N lp:B _ }} E R ok,
coq.ltac.collect-goals R [] [].
}}.
Elpi Typecheck coercion.
Elpi Typecheck TC.Solver.
Lemma C1 (x : S 0) : C 1 (@sb 0 x).
Proof. exists; trivial. Qed.
Elpi Accumulate TC.Solver lp:{{
tc-buffer4.tc-C N B {{ @C1 lp:D }} :-
coq.unify-eq N {{ 1 }} ok,
std.spy (coq.elaborate-skeleton B {{ @S 0 }} D ok),
coq.ltac.collect-goals D [] [].
}}.
Elpi Typecheck TC.Solver.
Timeout 1
Check true : S 1.
It is a problem we have already found and have to manage.
You have a tc goal that fails. In solver.elpi we are therefore
in the else branch (line 80). There we return GL = [seal G]
as the list of goals to be treated (which contains exactly the original goal).
Coq sees this new goal and tries to
solve it again with the tc solver, but it fails to find a solution, so
it calls tc and so on forever :melting_face:
For the moment, to avoid the loop, you can either deactivate
the Resolution For Conversion flag with
Unset Typeclass Resolution For Conversion. or
modify line 80 and replace it with (coq.error "Your message")
Quentin VERMANDE (Nov 13 2023 at 18:56):But then would not std.spy tell me that it exists the elaboration? I implemented your second suggestion and I never see the message.
Paolo Giarrusso (Nov 13 2023 at 18:58):Possibly relevant, but I'd expect coq.elaborate-skeleton to be called into do blocks to disable backtracking
Paolo Giarrusso (Nov 13 2023 at 18:59):do just inserts Prolog-style cuts
Paolo Giarrusso (Nov 13 2023 at 19:00):If coq.error causes backtrackin, that might explain why you don't see the error
Quentin VERMANDE (Nov 13 2023 at 19:02):Oh never mind, I am blind, the message does appear. I still have the loop, though.
The do block did not solve the problem either.
Davide F (Nov 13 2023 at 20:53):Paolo Giarrusso said:
do just inserts Prolog-style cuts
Maybe I'm wrong, but I think that in this particular situation, the loop is not caused by prolog search.
This is due to the fact that 1. Coq calls elpi with goal G, 2. elpi gives coq the old goal G,
Quentin VERMANDE said:
Oh never mind, I am blind, the message does appear. I still have the loop, though.
The do block did not solve the problem either.
You still have the loop after the coq.error ? This is quite weird. Anyway, @Quentin VERMANDE we can discuss it tomorrow at the office
Enrico Tassi (Nov 14 2023 at 09:53):didn't we add a @no-tc! flag to use as in @no-tc! => coq.elaborate-skeleton to avoid this?
There is still a corner case one has to disable with an option, something like Typeclasses For Conversion, do you recall @Davide F ?
Davide F (Nov 14 2023 at 10:22):Yep, you can do something like:
[@no-tc! | Clauses] => if (tc-recursive-search Ty Proof)
(
if (is-option-active {oTC-ignore-eta-reduction})
(Proof' = Proof) (coq.reduction.eta-contract Proof Proof'),
std.time (refine Proof' G GL) Refine-Time,
if (is-option-active {oTC-time-refine}) (coq.say "Refine Time" Refine-Time) true;
coq.error "illtyped solution:" {coq.term->string Proof}
)
(GL = [seal G]).
with the flag @no-tc! in the list of clauses accumulated with =>
Last updated: Oct 13 2024 at 01:02 UTC