Cannot infer parameters

[zstone1]

A different manifestation of what might be the same bug as #446 but I can't tell from the outside

Variant testTy := A | B.
HB.mixin Record Stack1 T := { prop1 : unit }.
HB.structure Definition JustStack1 := { T of Stack1 T }.
HB.mixin Record Stack1Param R T := { prop2 : unit }.
HB.structure Definition JustStack1Param R := { T of Stack1Param R T }.

HB.mixin Record Stack2 T := { prop3 : unit }.
HB.structure Definition JustStack2 := { T of Stack2 T }.
HB.mixin Record Mixed T of Stack1 T & Stack2 T := { prop4 : unit }.
HB.structure Definition JustMixed := { T of Mixed T & Stack1 T & Stack2 T}.
HB.structure Definition JustMixedParam R := 
  { T of Mixed T & Stack1 T & Stack1Param R T & Stack2 T}.

HB.instance Definition _ := @Stack1.Build testTy tt.
HB.instance Definition _ := @Stack2.Build testTy tt.

(*
Fails with 

HB: cannot infer some information in 
topology_testTy__canonical__topology_JustMixedParam : 
JustMixedParam.type ?e0 := 
{|
  JustMixedParam.sort := testTy;
  JustMixedParam.class :=
    {|
      JustMixedParam.topology_Stack1Param_mixin := HB_unnamed_factory_14783 ?e0;
      JustMixedParam.topology_Stack1_mixin := HB_unnamed_factory_14132;
      JustMixedParam.topology_Stack2_mixin := HB_unnamed_factory_14188;
      JustMixedParam.topology_Mixed_mixin := HB_unnamed_factory_14785
    |}
|}

HB.instance Definition _ {R} := @Stack1Param.Build R testTy tt.
HB.instance Definition _ := @Mixed.Build testTy tt.
*)

(* this order succeeds *)
HB.instance Definition _ := @Mixed.Build testTy tt.
HB.instance Definition _ {R} := @Stack1Param.Build R testTy tt.

It notices that it needs to make a JustMixedParam, which is what I expect. But I would also expect that it can figure out the parameters for the instances. The workaround of just reordering stuff is forcing me to make some rather large structural changes.

However, once I add an instance with a parameter like HB.instance Definition _ {R} := @Stack1Param.Build R testTy tt., all new instances mixed into the stack1 hierarchy will fail. I would be fine if there were a way for me to manually tell is how to introduce extra arguments, but I don't see how I can do that.

[CohenCyril]

We need to call the same code as HB.saturate which abstracts unresolved evars (like ?e0 above) with lambdas when creating new instances. See
https://github.com/math-comp/hierarchy-builder/blob/811c9ddcdd393eacc71a883729199e4d3dc0410f/HB/common/stdpp.elpi#L307C11-L362