Confusing error message when a structure parameter is unused

[CohenCyril]

Minimized and reported by @proux01 on zulip

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
    |}
|}
*)

[CohenCyril]

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.