Builders for mixins should be an error

[CohenCyril]

Or at least a warning...
See example from @MathisBD posted on zulip

From HB Require Import structures.

HB.mixin Record IsFunctor (F : Type -> Type) := {
  fmap : forall A B, (A -> B) -> F A -> F B
}.

HB.mixin Record IsMonad (M : Type -> Type) := {
  ret : forall A, A -> M A ;
  bind : forall A B, M A -> (A -> M B) -> M B
}.

HB.structure Definition Functor := { F of IsFunctor F }.
HB.structure Definition Monad := { M of IsMonad M }.

HB.builders Context M of IsMonad M.
  Let fmap A B (f : A -> B) (x : M A) := bind _ _ x (fun x => ret _ (f x)).
  HB.instance Definition _ := IsFunctor.Build M fmap.
HB.end.

[CohenCyril]

As of today this results in the following behaviour:

HB.instance Definition _ := IsMonad.Build option
  (@Some) (fun A B x f => match x with Some a => f a | None => None end).

Check option : Functor.type. (* succeeds *)