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.

[CohenCyril]

I'm not sure what breaks and shouldn't. Could you provide a MWE with a failure at definition time or during proofs? (using e.g. Fail ... to highlight it)

[Tragicus]

In the following code, the first rewrite rewrites the first occurrence of fb _ while the second one rewrites the second one.

From HB Require Import structures.
From mathcomp Require Import ssreflect.

HB.mixin Record isA (T : Type) := {fa : T -> T}.
HB.mixin Record isB (T : Type) := {xb : T; fb : T -> T}.
HB.mixin Record isC (T : Type) := {fc : T -> T}.

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

Axiom fbS0E : forall (T : S0.type) (x : T), fb x = xb.

Goal forall (T : S0.type) (x : T), fb (fc x) = fb x.
Proof. move=> T x; rewrite fbS0E.
Abort.

Axiom fbSE : forall (T : S.type) (x : T), fb x = xb.

Goal forall (T : S.type) (x : T), fb (fa x) = fb x.
Proof. move=> T x; rewrite fbSE.

[CohenCyril]

I think this is not a HB problem, and rather this Rocq problem

[Tragicus]

I believe this non-local name-dependent behavior of HB is an issue, even if the example also illustrates an issue with Rocq.

[pi8027]

Declaring join instances in both directions should also solve (or at least mitigate) the issue: math-comp/math-comp#1256 (comment) math-comp/math-comp#1125 (comment)