"criss-cross" inheritance · Hierarchy Builder devs & users

It seems there is a problem with using HB for the following "criss-cross" inheritance pattern:

O   O
|\ /|
| X |
|/ \|
O   O

From HB Require Import structures.

HB.mixin Record Setoid_of_Type A :=
  { eqv : A -> A -> Prop }.
HB.structure Definition Setoid := { A of Setoid_of_Type A }.
Infix "≡" := eqv (at level 79).

HB.mixin Record Ops_of_Type A (* of Setoid_of_Type A *) :=
  { par: A -> A -> A }.
HB.structure Definition Ops := { A of Ops_of_Type A}.
Notation "x ∥ y" := (par x y) (left associativity, at level 40, format "x ∥ y").

HB.mixin Record Pttdom_of_Ops A of Ops_of_Type A & Setoid_of_Type A :=
  { parA: forall x y z: A, x ∥ (y ∥ z) ≡ (x ∥ y) ∥ z }.
HB.structure Definition Pttdom := { A of Pttdom_of_Ops A & }.

HB.mixin Record Ptt_of_Ops A of Ops_of_Type A & Setoid_of_Type A :=
  { parC: forall x y: A, x ∥ y ≡ y ∥ x }.
HB.structure Definition Ptt := { A of Ptt_of_Ops A & }.

The command has indeed failed with message:
You must declare
class (indt «axioms») (global (indt «type»))
 (w-params.nil `A` (sort (typ «bug.9333»)) c0 \
   [triple (indt «Ops_of_Type.axioms_») [] c0,
    triple (indt «Setoid_of_Type.axioms_») [] c0,
    triple (indt «Ptt_of_Ops.axioms_») [] c0]) before
indt «Pttdom.axioms»

Is this pattern inherently problematic, or is this just a current limitation of the tool?

Christian Doczkal (Jul 20 2020 at 08:25):

If I, somewhat arbitrarily, make Ops depend on Setoid, then the problem disappears.

Enrico Tassi (Jul 20 2020 at 09:21):

I've opened an issue about the error message: https://github.com/math-comp/hierarchy-builder/issues/91 but I don't recall why the invariant is needed, we will need to wait for @Cyril Cohen or @Kazuhiko Sakaguchi in order to get an answer

Kazuhiko Sakaguchi (Jul 20 2020 at 11:29):

@Christian Doczkal In your hierarchy diagram, the join of Setoid and Ops is ambiguous. The join of Setoid and Ops (without any extra axiom) has to be defined first, and Pttdom and Ptt should inherit from it. See Sect. 4 (in particular Fig. 3 and 4) of https://arxiv.org/abs/2002.00620. CC: @Enrico Tassi

Enrico Tassi (Jul 20 2020 at 12:08):

Christian Doczkal (Jul 20 2020 at 12:20):

Yes, except that (a) then two of the links become transitive/redundant, and (b) in my case making one of the two upper structures inherit the other is more natural. Thanks Anyway.

Cyril Cohen (Jul 20 2020 at 14:37):

My plan was to fix that by making anonymous structures and remapping cs (for which we need overloading of canonical instances asap!) when possible ambiguous joins are created.

Stream: Hierarchy Builder devs & users