search

math-comp / hierarchy-builder

High level commands to declare a hierarchy based on packed classes
MIT License
95 stars 20 forks source link

Binder issue in `HB.instance` #419

Open Lapin0t opened 4 months ago

Lapin0t commented 4 months ago

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 commented 4 months ago

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 commented 4 months ago

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.