`HB.instance failed without giving a specific error message` when instantiating an unexported mixin

[Ef55]

The following fails without an explanation of the issue

From HB Require Import structures.

Module Test.
  HB.mixin Record Mixin T := {
    zero: T;
  }.

  HB.structure Definition Struct := { T of Mixin T }.

  HB.instance Definition struct_bool := Mixin.Build bool true.

  Module Exports.
    HB.reexport.
  End Exports.
End Test.
(** Uncommenting any of these two prevents the issue *)
(* Export Test.Exports. *)
(* HB.export Test. *)

Fail HB.instance Definition struct_nat := Test.Mixin.Build nat 0.
(*
  The elpi tactic/command HB.instance failed without giving a specific error message.
  Please report this inconvenience to the authors of the program.
*)

I don't know whether one should be able to instantiate a mixin this way (i.e. using its fully qualified name), or if the mixin must always be exported first.
If it's the latter, maybe the error message should say so.

[gares]

Thanks for reporting.

[proux01]

We should improve the error message (something like "Test.Mixin is not declared as a mixin/factory (missing export?)"