HB.structure does not give the right type to its operations

[MevenBertrand]

Here is a MWE:

From HB Require Import structures.

#[primitive] HB.mixin Record IsBaseSetTheory (set : Type -> Type) := {
  member {A : Type} : A -> set A -> Prop ;
  set_ext T (X Y : set T) : (forall t, member t X <-> member t Y) -> X = Y ;
  }.

#[short(type="BaseSetTheory"),primitive]
HB.structure Definition basesettheory :=
  { set & IsBaseSetTheory set }.

Notation "x ∈ X" := (member x X) (at level 60).

Check set_ext.

With Check in the last line, we get

set_ext
     : forall (T : Type) (X Y : ?s T),
(forall t : T,
IsBaseSetTheory.member _ (basesettheory.class ?s) T t X <->
IsBaseSetTheory.member _ (basesettheory.class ?s) T t Y) -> X = Y

while I expect

set_ext : forall (T : Type) (X Y : ?s T), (forall t : T, t ∈ X <-> t ∈ Y) -> X = Y

The issue seems to be that in the HB.structure definition, the type of the set_ext projection is not computed to refer to the member of BaseSetTheorybut ofIsBaseSetTheory`. (Note, though, that the two types are defeq).