Joins with primitive projections declared by HB are not found in the canonical structure table

[Tragicus]

When HB declares a join for structures with primitive projections, it uses the compatibility constants of the projections instead of the projections themselves. However, the canonical structure table differentiates them, so the instance is unusable.

From HB Require Import structures.

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

#[primitive]
HB.structure Definition A := {T of isA T}.
#[primitive]
HB.structure Definition B := {T of isB T}.

#[primitive]
HB.structure Definition C := {T of isA T & isB T}.

Fail Check fun (a : A.type) => a : B.type.