math-comp
Unused structure is required
As required by @CohenCyril in math-comp/analysis#750, I have a substantially minified example here:
From mathcomp Require Import all_ssreflect.
From HB Require Import structures.
HB.mixin Record IsX {T: Type} (f : T -> T) := { x_dummy_value : nat }.
HB.structure Definition XStruct {T : Type} := {f of @IsX T f}.
HB.mixin Record IsY {T: Type} (f : T -> T) := { y_dummy_value : bool }.
(* HB.structure Definition YStruct {T: Type} := {f of @IsY T f}.*)
HB.structure Definition XandY {T : Type} := {f of @IsX T f & @IsY T f}.
Section Examples.
Context {T: Type} (f : T -> T).
HB.instance Definition _ := @IsY.Build T f false.
HB.instance Definition _ := @IsX.Build T f 0%N.
Definition OnlyWorksWhenYStuctDefined := [the (@XandY.type _) of f].
End Examples.
Same errors as before, but much more clear. It looks like a bug to me, at least based on my understanding of how HB should work.
Oooh I understand now! Thanks a lot, the explantion is quite simple now you minimized.
HB mixin instances can survive only when there is an existing structure instance that contain them (since we compile everything to canonical structure declarations). Since the first structure which contains mixin Y is XandY, if you declare an instance for Y before the instance for X, the first one is not save hence the bug you encounter.
Until we update the design pattern (in two possible ways) I see only one fix: print an error message when an instance for Y is declared without a priori instance for X.
I see. Fascinating. Naively, I would not have expected the order of instance declarations to ever matter. Although with your explanation I do see how that happened. An error message would be great. Two follow up questions then.
- Is there ever a case where you'd want the order of instance declarations to matter?
- Is just defining the dummy structure my best choice for a workaround?
- No I do not think the order should matter at all, currently that's just an artifact of the encoding.
- Sure, it's the best workaround as of now.