Merge pull request #481 from math-comp/fix-error-bad-mix

improve error message on instance of not a factory

Author: gares

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

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)
+	$(call DIFF, tests/err_miss_dep.v)
+	$(call DIFF, tests/err_bad_mix.v)

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.

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