diff --git a/HB/instance.elpi b/HB/instance.elpi
index f3cc9b1c3..3f0e64777 100644
--- a/HB/instance.elpi
+++ b/HB/instance.elpi
@@ -42,7 +42,8 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [
 
   % identify the factory
   std.assert! (coq.safe-dest-app SectionTy (global FactoryAlias) Args) "The type of the instance is not a factory",
-  factory-alias->gref FactoryAlias Factory,
+  if (factory-alias->gref FactoryAlias Factory) true
+     (coq.error "HB:" {coq.term->string (global FactoryAlias)} "is not a factory or its library was not correctly imported"),
   std.assert! (factory-nparams Factory NParams) "Not a factory synthesized by HB",
 
   % declare the constant for the factory instance
diff --git a/Makefile.test-suite.coq.local b/Makefile.test-suite.coq.local
index d9c69747e..b26e6e9a4 100644
--- a/Makefile.test-suite.coq.local
+++ b/Makefile.test-suite.coq.local
@@ -26,4 +26,5 @@ post-all::
 	$(call DIFF, tests/missing_join_error.v)
 	$(call DIFF, tests/not_same_key.v)
 	$(call DIFF, tests/hnf.v)
-	$(call DIFF, tests/err_miss_dep.v)
\ No newline at end of file
+	$(call DIFF, tests/err_miss_dep.v)
+	$(call DIFF, tests/err_bad_mix.v)
diff --git a/tests/err_bad_mix.v b/tests/err_bad_mix.v
new file mode 100644
index 000000000..0d0407bae
--- /dev/null
+++ b/tests/err_bad_mix.v
@@ -0,0 +1,20 @@
+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.
diff --git a/tests/err_bad_mix.v.out b/tests/err_bad_mix.v.out
new file mode 100644
index 000000000..a33d3e833
--- /dev/null
+++ b/tests/err_bad_mix.v.out
@@ -0,0 +1,5 @@
+Interactive Module Test started
+Interactive Module Exports started
+The command has indeed failed with message:
+HB: Test.Mixin.axioms_ 
+is not a factory or its library was not correctly imported