HB.lock "erefl body" error message

[hivert]

If I try

HB.lock Definition Bla (T : finType) : Type := {set T}.

HB complaints with

Error:
The term "erefl body" has type "body = body" while it is expected to have type
 "body = [eta set_of]".

I think my code should be perfectly legitimate.

[hivert]

The same works with ELPI:

From elpi Require Import elpi locker.
lock Definition Bla (T : finType) : Type := {set T}.

[gares]

Yes, but that is the soft locking that does not use module types. If you try mlock instead, you get the same error.

[gares]

Looking at the elpi trace of mlock I see code roughly equivalent to:

Definition body : Finite.type -> Type := fun T : Finite.type => set_of T.
Definition unlock : (@eq (Finite.type -> Type) body (fun T : Finite.type => set_of T)) :=
  @Logic.eq_refl  (Finite.type -> Type) body (fun T : Finite.type => set_of T).

that seems correct.

I think the problem must be in the universes, eg 25742 vs 25735 in this raw log below:

coq.env.add-const body 
 (fun `T` (global (indt «Finite.type»)) c0 \
   app [global (const «set_of»), c0]) 
 (prod `T` (global (indt «Finite.type»)) c0 \ sort (typ «a.25735»)) ff 
 X33

 coq.env.add-const unlock 
  (app
    [global (indc «Logic.eq_refl»), 
     prod `T` (global (indt «Finite.type»)) c0 \ sort (typ «a.25735»), 
     global (const «body»)]) 
  (app
    [global (indt «eq»), 
     prod `T` (global (indt «Finite.type»)) c0 \ sort (typ «a.25742»), 
     global (const «body»), 
     fun `T` (global (indt «Finite.type»)) c0 \
      app [global (const «set_of»), c0]]) tt _

[gares]

It is a bug in the Coq-Elpi code, I guess I interpret the Type annotation twice without telling coq they are the same.

Poor man solution:

Definition XX := Type.
HB.lock Definition Bla (T : finType) : XX := {set T}.

[hivert]

Thanks for the workaround.

[hivert]

Reported in ELPI : LPCIC/coq-elpi#704