Add warning about implicitly local `HB.instance` calls, improve error messages

[lweqx]

For more context, see the corresponding topic on Zulip.

Demo:

From HB Require Import structures.

HB.mixin Record Mixin T := {}.
HB.structure Definition _ := { T of Mixin T }.

HB.factory Record Factory T := {}.

HB.builders Context U of Factory U.

(* New warning:
  In builder mode, non-builder instances are always considered local.
  Annotate this HB.instance call with #[local] to fix this warning and improve your code documentation.
  [HB.nonlocal-instance-in-builder-mode,HB,elpi,default]
*)
HB.instance Definition _ := Mixin.Build unit.

(* Rocq error: HB: No builders on U to declare. This HB.builders section must HB.instance at least one mixin or factory on U.

  Previously: No builders to declare, did you forget HB.instance? 
*)
Fail HB.end.

(* Still ok *)
HB.instance Definition _ := Mixin.Build U.

(* Rocq error:
  HB: declare-instance: cannot make builders local. 
  If you want temporary instances, make an alias, e.g. with let U' := U

  Previously:
    HB: declare-instance: cannot make builders local.
        If you want temporary instances, make an alias, e.g. with let T' := T
*)
Fail #[local]
HB.instance Definition _ := Mixin.Build U.

HB.end.