Implicit arguments for mixins and structures are discarded and sometimes inferred wrong

[CohenCyril]

The implicit arguments directives are simply ignored by HB.

Indeed in the following context

From HB Require Import structures.
Require Import ssreflect.

HB.mixin Record isPointed T := { point : T }.
#[short(type="pType")]
HB.structure Definition pointed := { T of isPointed T }.
HB.instance Definition _ := isPointed.Build nat 0.
Definition nat_pointed := [the pType of nat : Type].

The following mixin does not have the prescribed implicits:

HB.mixin Record isPointedMap {T U : pType} (f : T -> U) :=
  { fix_point : f point = point }.
(* {T U} was not honoured for isPointedMap *)
Check isPointedMap nat_pointed nat_pointed (plus 0).

---

Moreover when Set Implicit Arguments and Unset Strict Implicit are activated, this leads to a weird default setting where one parameter is implicit while the other is not, without understandable rationale.

Set Implicit Arguments.
Unset Strict Implicit.
HB.structure Definition pointedMap T U := {f of isPointedMap T U f}.
Check pointedMap nat_pointed (plus 0). (* weird mix *)
 (* as it should be without @ *)
Check @pointedMap nat_pointed nat_pointed (plus 0).

CC @gares