From HB Require Import structures.
HB.mixin Record IsA (T' : Type) T := { opA : T -> T' }.
HB.structure Definition A (T' : Type) := {T of IsA T' T}.
HB.mixin Record IsB (T : Type) of A T T := { opB : T }.
Fail HB.structure Definition B (T : Type) := {T of A T T & IsB T}.
(*
axioms_ is defined
test_IsA_mixin is defined
test_IsB_mixin is defined
type is defined
sort is defined
class is defined
phant_clone is defined
pack_ is defined
test_B_class__to__test_A_class is defined
test_B__to__test_A is defined
phant_on_ is defined
T is declared
T0 is declared
HB_unnamed_factory_7 is defined
test_B__to__test_IsA is defined
test_B__to__test_IsB is defined
HB_unnamed_mixin_10 is defined
The command has indeed failed with message:
HB: cannot infer some information in structures_eta__canonical__test_B :
type ?e0 :=
{|
sort := eta T0;
class :=
{|
test_IsA_mixin := HB_unnamed_mixin_4 T0 T0;
test_IsB_mixin := HB_unnamed_mixin_10
|}
|}
*)
So in the end, I think this should be an error with error message: Argument T of B is not used. All the parameters of a structure should be used in the mixins.
Minimized and reported by @proux01 on zulip