HB.no-new-instance, where I would expect a new instance

[damien-pous]

I encounter a problem in the attached small file, where HB.instance fails to declare a new instance.
CCing @CohenCyril with whom I discussed the bug.

hb.v.txt

I'm copying the file below as .v are not allowed and the file is short:

From HB Require Import structures.

(* Elpi lock *) 
Definition d (X: Type) := X. 

HB.mixin Record isA X := {}.
HB.structure Definition A := { X of isA X }.
HB.instance Definition _ (X: A.type) := isA.Build (d X).

Check fun X: A.type => d X: A.type.

HB.mixin Record isB1 X of A X := {}.
HB.structure Definition B1 := { X of isB1 X & }.
HB.mixin Record isB2 X of A X := {}.
HB.structure Definition B2 := { X of isB2 X & }.

HB.instance Definition _ (X: B1.type) := isB2.Build (d X).
HB.instance Definition _ (X: B2.type) := isB1.Build (d X).

Check fun X: B1.type => d X: B2.type.
Check fun X: B2.type => d X: B1.type.

HB.mixin Record isC1 X of A X := {}.
HB.structure Definition C1 := { X of isC1 X & B1 X }.
HB.mixin Record isC2 X of A X := {}.
HB.structure Definition C2 := { X of isC2 X & B2 X }.

Check fun X: C1.type => d X: B2.type.
Check fun X: C2.type => d X: B1.type.

HB.instance Definition _ (X: C1.type) := isC2.Build (d X).
HB.instance Definition _ (X: C2.type) := isC1.Build (d X). (* warning, no new instance *)

Check fun X: C1.type => d X: C2.type.
Check fun X: C2.type => d X: C1.type. (* fails, I would expect this to work *)


(* NOTES:

- locking d (e.g., uncommenting L3) solves the problem
- removing the A layer (i.e., letting Bi, Ci depend on just Type) also solves it

 *)