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?

The code:

```
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)).
```

The error and debugging messages :

```
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) []))
[]
```

what elpi commit is this?

what is the assert on?

I am three commits ahead of the master branch (commit 2f7f589b, the subsequent commits only change the coercion hook, I would prefer not to recompile coq and coq-elpi, but if you think it is relevant I can).

The assert is on the result of `get_goal_ref`

. I do not know what it does, though, and since I am still quite new to coq-elpi, it is quite hard to guess.

probably should be in the elpi stream instead of coq devs

Oh sorry, I meant to put it there, but messed up. You are absolutely right.

Quentin VERMANDE has marked this topic as resolved.

Last updated: Oct 13 2024 at 01:02 UTC