Binder issue in HB.instance

[Lapin0t]

Hi, i'm running into an issue when using mixins where the principal argument is a function (typically to write structures such as "monotone functions").

HB.mixin Record IsFoo X (f : X -> X) := {}.
HB.structure Definition Foo X := { f of IsFoo X f }.
Fail HB.instance Definition _ := IsFoo.Build bool (fun x => x) .
(* term->gref: input has no global reference: fun `x` (global (indt «bool»)) c0 \ c0 *)

It fails while the following is accepted:

Definition bla {X} (x : X) := x .
HB.instance Definition _ := IsFoo.Build bool bla .

It seems to me there is an issue with the binder treatment in parameters.

HB version is 1.7.0 with coq 8.19.1.

[CohenCyril]

Dear @Lapin0t, thank you for reporting. The problem lies in the error message, we should fix it to output something like:

HB.instance: the subject/key of the structure must be either a global reference, a sort, a dependent product or a section variable. Other constructions are currently unsupported for the sake of determinism and efficiency.

Indeed, we should advertise this limitation of the current implementation.
Another feature request would be to extend the framework to support the example you want to deal with.

[Lapin0t]

Aha, this makes sense! Ok, I will use constants for now, although I would have guessed that the complexity of handling lambdas is more or less the same as foralls... Probably we can close this, I will ping you if I look into the code to extend HB.