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

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

That is, if I try the following:

```
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 & }.
```

I get the following (somewhat uninformative) error message:

```
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?

If I, somewhat arbitrarily, make `Ops`

depend on `Setoid`

, then the problem disappears.

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

@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

After all, it's a matter of replacing a `x`

with a `o`

in the picture ;-)

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.

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.

Last updated: Apr 21 2024 at 01:02 UTC