Hi, i'm starting to use hierarchy builder (so i'm possibly doing stuff wrong). I seem to be hitting a bug around get-canonical-mixins-of
where i can't derive instances for 2 unrelated structures inheriting from a base one. Minimal code to reproduce (both on 0.10.0 and master):
From HB Require Import structures.
HB.mixin Record base_m T := { A : T }.
HB.structure Definition base := { T of base_m T }.
HB.mixin Record child1_m T := { C1 : T }.
HB.structure Definition child1 := { T of base T & child1_m T }.
HB.mixin Record child2_m T := { C2 : T }.
HB.structure Definition child2 := { T of base T & child2_m T }.
Axiom ix : Type.
Definition vec T := ix -> T.
Section b.
Variable T : base.type.
HB.instance Definition v_base_m : base_m (vec T) :=
base_m.Build _ (fun _ => A).
End b.
Section c1.
Variable T : child1.type.
HB.instance Definition v_child1_m : child1_m (vec T) :=
child1_m.Build _ (fun _ => C1).
End c1.
Section c2.
Variable T : child2.type.
Fail HB.instance Definition v_child2_m : child2_m (vec T) :=
child2_m.Build _ (fun _ => C2).
End c2.
Sections c1 and c2 won't compile together (but either will), i'm getting:
The command has indeed failed with message:
elpi: HB: get-canonical-mixins-of: T = sort ST: In environment
T : child2.type
Unable to unify "vec T" with "child1.sort ?e0".
Afaik sections are required for such instance families, right? For a bit more context i have a small hierarchy of pre-ordered-sets/skew-monoids/skew-semiring and i would like to lift these structures pointwise for vectors. Btw, another question not related to above bug: at some point i'd like to have semimodule over a semiring but that structure has to be parametrized by the semiring and parametrized structures don't seem to be stable in HB. Is there any way to parametrize a structure by something else than Type
?
I tried this example on master
and it works.
Also, you lack a join between child1 and child2, which is not something HB likes in general, but maybe this is just your minimization.
FTR in master you don't need to call HB.instance in the sections, just add T to the Definition as a parameter, the section thing is done for you behind the scenes.
I hope we will manage to merge https://github.com/math-comp/hierarchy-builder/pull/119 and release 1.0 in 2 weeks.
The branch I mention above does support parameters and fixes many bugs with them. You can put anything as a parameter. What is forced to be of type Type
is the carrier of the structure (so far no hierarchies of morphisms are possible for this reason). Did I answer your second qeustion?
The bug you experience can be worked around. If I'm not mistaken this is the changelong entry that fixes it:
- Use Coq's elaborator to typecheck factories and structures (coercions are
now inserted properly)
Try to write vect (base.sort T)
instead.
(I did not try, so I may be off)
I tried this example on master and it works.
Oh ok, i must have mixed up my installation, i'm gonna try again.
Did I answer your second question?
Yes thanks a lot, i'll try that branch.
I don't think the *.sort T
coercion thing is related, i did hit this bug before and fixed it like that but here it doesn't trigger any error for the previous sections (b
and c1
in my example).
Weird, i tried again on master
and section-discharge-fight
and i get the same (original) error message on both. Did you notice i put a Fail
command?
Sorry, I did not.
:) probably my bad.. i recently learnt that command so i wanted to use it but i didn't know that it suppressed the output from coqc
This makes it work, but I have to think more about it before committing.
diff --git a/hb.elpi b/hb.elpi
index 9bb314b..3daff91 100644
--- a/hb.elpi
+++ b/hb.elpi
@@ -595,15 +595,17 @@ get-canonical-mixins-of T S MSL :- std.do! [
structure-nparams S NParams,
coq.mk-n-holes NParams Holes,
coq.mk-app Sort {std.append Holes [ST]} SortHolesST,
- std.assert-ok! (coq.unify-eq T SortHolesST) "HB: get-canonical-mixins-of: T = sort ST",
- % Hum, this unification problem is not super trivial. TODO replace by something simpler
- get-constructor S KS,
- coq.mk-app (global KS) {std.append Holes [T, C]} KSHolesC,
- std.assert-ok! (coq.unify-eq ST KSHolesC) "HB: get-canonical-mixins-of: ST = _ _ C",
- C = app Stuff,
- std.drop {calc (NParams + 2)} Stuff MIL,
- std.map MIL (mixin-srcs T) MSLL,
- std.flatten MSLL MSL
+ if (coq.unify-eq T SortHolesST ok) (
+ % Hum, this unification problem is not super trivial. TODO replace by something simpler
+ get-constructor S KS,
+ coq.mk-app (global KS) {std.append Holes [T, C]} KSHolesC,
+ std.assert-ok! (coq.unify-eq ST KSHolesC) "HB: get-canonical-mixins-of: ST = _ _ C",
+ C = app Stuff,
+ std.drop {calc (NParams + 2)} Stuff MIL,
+ std.map MIL (mixin-srcs T) MSLL,
+ std.flatten MSLL MSL
+ )
+ (MSL = [])
].
pred under-canonical-mixins-of.do! i:term, i:list prop.
There is a piece of code which filters all canonical instances in a silly way, and then expects this code to work. In your case it picks an instance that cannot work. I turned an assert failure into an if... I'll open an issue to track this.
Nice, thanks a lot for the fix. I'll have to take a bit more time to understand what it's about tho..
Here the PR (and branch) https://github.com/math-comp/hierarchy-builder/pull/121
I think it is just a programming error. The new code is for sure more safe, but I've to understand if we can do better.
Last updated: Oct 08 2024 at 15:02 UTC