Join declaration unstable under renaming

[Tragicus]

The joins HB declares depend on the name of the structures, which breaks things when we want to rename structures. Here is a MWE, where the first Check uses the join of A and B, and the second one uses the coercion from S0 to B.

From HB Require Import structures.

HB.mixin Record isA (T : Type) := {}.
HB.mixin Record isB (T : Type) := {}.
HB.mixin Record isC (T : Type) := {}.

HB.structure Definition A := {T of isA T}.
HB.structure Definition B := {T of isB T}.
HB.structure Definition C := {T of isC T}.

HB.structure Definition S := {T of A T & B T}.
HB.structure Definition S0 := {T of C T & B T}.

Set Printing All.
Check fun (T : S.type) => (T : A.type) : B.type.
Check fun (T : S0.type) => (T : C.type) : B.type.