Open hivert opened 3 hours ago
The same works with ELPI:
From elpi Require Import elpi locker.
lock Definition Bla (T : finType) : Type := {set T}.
Yes, but that is the soft locking that does not use module types. If you try mlock
instead, you get the same error.
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 _
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}.
Thanks for the workaround.
Reported in ELPI : https://github.com/LPCIC/coq-elpi/issues/704
If I try
HB complaints with
I think my code should be perfectly legitimate.