MissingJoin

A "missing join structure" makes certain unification problem fail in a tricky to understand way. Everything may work fine until you combine in the same statements two operations, and that fails mysteriously. HB detects that scenario an suggests to insert an intermediate structure.

This is a synthetic example, and its corresponding fix. Later we show a real, but more involved, instance of the problem.

From HB Require Import structures.

Module MissingJoin.

HB.mixin Record isTop M := { }.
HB.structure Definition Top := {M of isTop M}.

HB.mixin Record isA1 M of Top M := { }.
HB.structure Definition A1 := {M of isA1 M & isTop M}.

HB.mixin Record isA2 M of Top M := { }.
HB.structure Definition A2 := {M of isA2 M & isTop M}.

HB.mixin Record isB1 M of A1 M := { }.
HB.structure Definition B1 := {M of isB1 M & }.

HB.mixin Record isB2 M of A2 M := { }.
HB.structure Definition B2 :=  {M of isB2 M & isA2 M }.

HB.structure Definition B2A1 := {M of B2 M & A1 M }.

Fail HB.structure Definition A2B1 := {M of A2 M & B1 M }.

HB.graph "missing_join.dot".

End MissingJoin.

If we tred missing_join.dot | xdot - we see this (where the red node is the one we failed to add)

The solution is to declare a structure which both A2B1 and B2A1 can inherit from.

From HB Require Import structures.

Module GoodJoin.

HB.mixin Record isTop M := { }.
HB.structure Definition Top := {M of isTop M}.

HB.mixin Record isA1 M of Top M := { }.
HB.structure Definition A1 := {M of isA1 M & isTop M}.

HB.mixin Record isA2 M of Top M := { }.
HB.structure Definition A2 := {M of isA2 M & isTop M}.

HB.mixin Record isB1 M of A1 M := { }.
HB.structure Definition B1 := {M of isB1 M & }.

HB.mixin Record isB2 M of A2 M := { }.
HB.structure Definition B2 :=  {M of isB2 M & isA2 M }.

HB.structure Definition join := {M of A1 M & A2 M }.


HB.structure Definition B2A1 := {M of B2 M & A1 M }.
HB.structure Definition A2B1 := {M of A2 M & B1 M }.

HB.graph "good_join.dot".

End GoodJoin.

This problem arose in practice when porting the coq-monae project to HB

As you may see, there is a missing join structure between nondetState and exceptStateRun (for example).