Extra parameters in instances cause bad errors

[zstone1]

A bug I am encountering when working with topologicalType vs pseudoMetricType where the metric has an extra parameter:

HB.mixin Record Basic T := { prop1 : forall (x : T), x = x }.

HB.structure Definition JustBasic := {T of Basic T}.

HB.mixin Record WithExtraParam {R : Type} T of Basic T := {
  prop2 : forall (r : R) (x : T), x = x
}. 

HB.structure Definition WithExtra {R} := {T of WithExtraParam R T & Basic T}.

HB.factory Record BasicAlt T := { prop3 : forall (x:T), x = x }.

HB.builders Context T of BasicAlt T.
HB.instance Definition _ := Basic.Build T prop3.
HB.instance Definition _ {R} := @WithExtraParam.Build R T (fun=>prop3).
HB.end.

HB.instance Definition _ := @BasicAlt.Build bool (fun=> erefl).

The factory and builder work fine, but I get

take run out of list items

as the error, which is pretty meaningless to me. I can tell that the issue is with the R parameter of HB.instance Definition _ {R} .

Ideally, I want HB to know how to build a WithExtraParam R when it encounters one, but not try to build one right now. Which is what I would get if I did

HB.builders Context R T of BasicAlt R T.
HB.instance Definition _ := Basic.Build T prop3.
HB.instance Definition _ := @WithExtraParam.Build R T (fun=>prop3).
HB.end.

HB.instance Definition _ {R} := @BasicAlt.Build R bool (fun=> erefl).

but now I can't build my Basic without an R.

The workaround for now seems to be to have two factories, R-dependent and R-independent portions. Then build an instance for both like

HB.factory Record BasicAlt T := { prop3 : forall (x:T), x = x }.

HB.builders Context T of BasicAlt T.
HB.instance Definition _ := Basic.Build T prop3.
HB.end.

HB.factory Record BasicAltWithParam R T of BasicAlt T := {}.
HB.builders Context R T of BasicAltWithParam R T.
HB.instance Definition _ := @WithExtraParam.Build R T (fun _ _ => erefl).
HB.end.

HB.instance Definition _ := @BasicAlt.Build bool (fun=> erefl).
HB.instance Definition _ {R} := @BasicAltWithParam.Build R bool.

Ideally, I'd like it to infer those extra parameters to the instances. But I'm fine with this split solution in the interim. But then the hb.end or the hb.instance in the first example should fail. And of course the current error message is not great.