Assertion failed in coq_elpi_HOAS.ml · Elpi users & devs

Hi. In the following script, I have a Check that fails due to a failed assertion in coq_elpi_HOAS.ml.

I define two tactics that print their goal, try to solve it and fallback on tc's typeclass instanciation upon failure. Then I declare a structure for sets, a class for the set membership predicate and a structure memType bundling the two (hence mimicking sig, but with a structure). I define a coercion from a type to any of its induced memTypes that delegates finding the missing membership proof to one of the previously declared tactic. Then I declare an instance of mem that delegates finding the proof term to one of the tactics. Now, trying to coerce an element of nat to some dummy memType nat P fails exactly when the coercion uses the done tactic, with the above mentioned error.

Debugging shows that the coercion calls the tactic, which in turn calls typeclass inference. The tc-mem predicate goes to the line where it should call the tactic and then fails without the tactic ever printing anything. If I change the dummy predicate to something that done2 can not prove, the whole process fails normally.

The question here is not so much how I should make the tactic work (since this example is minimized), but rather what happens at the failure point. Does anyone have an idea?

From Coq Require Import ssreflect.
From elpi.apps Require Import tc coercion.

Ltac done := (match goal with |- ?G => idtac "goal " G end);
  (do ![trivial | split]); idtac "apply"; apply _ .
Ltac done2 := (match goal with |- ?G => idtac "goal2 " G end);
  (do !split); trivial; idtac "apply"; apply _.

Structure set (T : Type) := MkSet {
  set_to_pred : T -> Prop
}.

Class mem T (X : set T) (x : T) : Prop := Mem { IsMem : set_to_pred T X x }.

Structure memType T (X : set T) := MemType {
  this : T;
  memP : mem T X this
}.

Elpi Accumulate coercion.db lp:{{

coercion _ V T E R :-
  coq.unify-eq E {{ @memType lp:T (lp:X : set lp:T) }} ok,
  R = {{ @MemType lp:T lp:X lp:V _ }},
  % we call the solver
  coq.ltac.collect-goals R [G] [],
  coq.ltac.open (coq.ltac.call-ltac1 "done") G [].

}}.
Elpi Typecheck coercion.

Elpi Accumulate TC.Solver lp:{{

tc-buffer3.tc-mem T X V R :-
  R = {{ @Mem lp:T lp:X lp:V _ }},
  coq.say R,
  % we call the solver
  coq.ltac.collect-goals R [G] [],
  std.spy (coq.ltac.open (coq.ltac.call-ltac1 "done") G []).
}}.

Elpi Typecheck TC.Solver.

Check fun (x : nat) => x : memType nat (@MkSet nat (fun x : nat => True)).
Fail Check fun (x : nat) => x : memType nat (@MkSet nat (fun x : nat => exists y, y = x)).

Anomaly
"File "src/coq_elpi_HOAS.ml", line 3365, characters 42-48: Assertion failed."
Please report at http://coq.inria.fr/bugs/.

goal  (mem nat {| set_to_pred := fun _ : nat => True |} x)

apply

app
 [global (indc «Mem»), global (indt «nat»),
  app
   [global (indc «MkSet»), global (indt «nat»),
    fun `elpi_ctx_entry_1_` (global (indt «nat»)) c1 \
     global (indt «True»)], c0, X0^1]

----<<---- enter:
coq.ltac.open (coq.ltac.call-ltac1 done)
 (nabla c1 \
   seal
    (goal [decl c1 `x` (global (indt «nat»))] (X1 c1) (X2 c1) (X1 c1) []))
 []

Stream: Elpi users & devs

Topic: Assertion failed in coq_elpi_HOAS.ml

Quentin VERMANDE (Nov 10 2023 at 13:47):

Enrico Tassi (Nov 10 2023 at 14:00):