HB.instance: warn on nonlocal declaration in builder mode

Author: lweqx

HB/instance.elpi

@@ -292,6 +292,11 @@ declare-instance Factory T F Clauses CFL CSL :-
   declare-canonical-instances-from-factory-and-local-builders Factory
     T F TheFactory FGR Clauses CFL CSL.
 declare-instance Factory T F Clauses CFL CSL :-
+  if (not (get-option "local" tt),
+      current-mode (builder-from U _ _ _), not (T = U))
+    (coq.warning "HB" "HB.nonlocal-instance-in-builder-mode"
+      "In builder mode, non-builder instances are always considered local.\n"
+      "Annotate this HB.instance call with #[local] to fix this warning and improve your code documentation.") true,
   declare-canonical-instances-from-factory Factory T F Clauses1 CFL CSL,
   if (get-option "export" tt)
      (coq.env.current-library File,