Ill-typed evar instance

[Tragicus]

The code below fails, likely (see https://coq.zulipchat.com/#narrow/stream/253928-Elpi-users-.26-devs/topic/Ill-typed.20evar.20instance/near/397185633) due to a bug in coq-elpi. In the following script, I declare proj1_sig as a coercion using elpi, then declare some additive structure on nat and a subtype evenof integers. Then, typechecking n + m : nat with n : nat and m : even fails with the error "Ill-typed evar instance". In case that is relevant, debugging shows that, at some point after mis coerced to nat, the only missing piece in the term is the additive structure of nat. Besides, replacing in the elpi code @sig lp:E _ by @sig lp:E lp:P and proj1_sigby @proj1_sig lp:E lp:P makes the error disappear.

The code:

From elpi.apps Require Import coercion.

Definition set (T : Type) := T -> Prop.

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

Coercion mem_of_set T (X : set T) : Type := @sig T X.

Elpi Accumulate coercion.db lp:{{

coercion _ V T E X :-
  std.spy (coq.unify-eq T {{ @sig lp:E _ }} ok),
  std.spy (coq.elaborate-skeleton {{ proj1_sig lp:V }} E X ok).

}}.
Elpi Typecheck coercion.

Class hasAdd T := HasAdd { add_op : T -> T -> T }.

Structure addType := AddType {
  add_sort :> Type;
  add_of_addType : hasAdd add_sort;
}.
Definition add {T} := (@add_op _ (add_of_addType T)).

Canonical generic_addType T a := AddType T a.
 
Instance nat_add : hasAdd nat := HasAdd nat plus.
Definition even : set nat := sig (fun n => exists m, n = 2 * m).

Section tests.
Variables (n : nat) (m : even).

Set Printing All.
Check (add n m) : nat.

The error message (with debugging) :

Ill-typed evar instance

----<<---- enter:  
coq.unify-eq
 (app
   [global (const «mem_of_set»), global (indt «nat»), 
    global (const «even»)]) 
 (app
   [global (indt «memType»), 
    app
     [global (const «add_sort»), 
      app [global (const «generic_addType»), global (indt «nat»), X0]], 
    X1]) ok

---->>---- exit:  
coq.unify-eq
 (app
   [global (const «mem_of_set»), global (indt «nat»), 
    global (const «even»)]) 
 (app
   [global (indt «memType»), 
    app
     [global (const «add_sort»), 
      app [global (const «generic_addType»), global (indt «nat»), X2]], 
    global (const «even»)]) ok

----<<---- enter:  
coq.elaborate-skeleton
 (app [global (const «this»), X3, X4, global (const «m»)]) 
 (app
   [global (const «add_sort»), 
    app [global (const «generic_addType»), global (indt «nat»), X2]]) X5 
 ok

---->>---- exit:  
coq.elaborate-skeleton
 (app [global (const «this»), X3, X4, global (const «m»)]) 
 (app
   [global (const «add_sort»), 
    app [global (const «generic_addType»), global (indt «nat»), X6]]) 
 (app
   [global (const «this»), global (indt «nat»), global (const «even»), 
    global (const «m»)]) ok