Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Cannot infer parameters #447

Open
zstone1 opened this issue Sep 20, 2024 · 0 comments
Open

Cannot infer parameters #447

zstone1 opened this issue Sep 20, 2024 · 0 comments

Comments

@zstone1
Copy link

zstone1 commented Sep 20, 2024

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant