Stream: Hierarchy Builder devs & users

Topic: instance family bug?


view this post on Zulip Lapinot (Nov 02 2020 at 16:12):

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?

view this post on Zulip Enrico Tassi (Nov 02 2020 at 16:46):

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.

view this post on Zulip Enrico Tassi (Nov 02 2020 at 16:49):

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?

view this post on Zulip Enrico Tassi (Nov 02 2020 at 16:53):

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.

view this post on Zulip Enrico Tassi (Nov 02 2020 at 16:54):

(I did not try, so I may be off)

view this post on Zulip Lapinot (Nov 02 2020 at 17:07):

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).

view this post on Zulip Lapinot (Nov 02 2020 at 17:31):

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?

view this post on Zulip Enrico Tassi (Nov 02 2020 at 17:33):

Sorry, I did not.

view this post on Zulip Lapinot (Nov 02 2020 at 17:36):

:) 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

view this post on Zulip Enrico Tassi (Nov 02 2020 at 17:51):

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.

view this post on Zulip Enrico Tassi (Nov 02 2020 at 17:53):

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.

view this post on Zulip Lapinot (Nov 02 2020 at 17:59):

Nice, thanks a lot for the fix. I'll have to take a bit more time to understand what it's about tho..

view this post on Zulip Enrico Tassi (Nov 02 2020 at 17:59):

Here the PR (and branch) https://github.com/math-comp/hierarchy-builder/pull/121

view this post on Zulip Enrico Tassi (Nov 02 2020 at 18:00):

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: Mar 29 2024 at 12:02 UTC