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

L0 typechecking errors, matching names but differing numbers #207

Open
jazullo opened this issue Mar 30, 2023 · 0 comments
Open

L0 typechecking errors, matching names but differing numbers #207

jazullo opened this issue Mar 30, 2023 · 0 comments

Comments

@jazullo
Copy link
Collaborator

jazullo commented Mar 30, 2023

Consider this code
This results in the following error:

~/gibbon$ cabal v2-exec gibbon -- --packed --no-gc --to-exe ../llrbt/break.hs
gibbon: lookupDataCon: could not find constructor "Nil_v_236", in datatypes:
  [(Maybe,
  DDef {tyName = "Maybe",
        tyArgs = [b:a_26],
        dataCons = [("Just", [(False, TyVar b:a_26)]),("Nothing", [])]}),
 (PList,
  DDef {tyName = "PList",
        tyArgs = [b:a_27],
        dataCons = [("Nil", []),
                    ("Cons",
                     [(False, TyVar b:a_27),
                      (False, PackedTy "PList" [TyVar b:a_27])])]}),
 (PList_v_239,
  DDef {tyName = "PList_v_239",
        tyArgs = [],
        dataCons = [("Nil_v_239", []),
                    ("Cons_v_239",
                     [(False, PackedTy "Maybe_v_235" []),
                      (False, PackedTy "PList_v_239" [])])]}),
 (PList_v_237,
  DDef {tyName = "PList_v_237",
        tyArgs = [],
        dataCons = [("Nil_v_237", []),
                    ("Cons_v_237",
                     [(False, PackedTy "Maybe" [IntTy]),
                      (False, PackedTy "PList_v_237" [])])]}),
 (Maybe_v_235,
  DDef {tyName = "Maybe_v_235",
        tyArgs = [],
        dataCons = [("Just_v_235", [(False, IntTy)]),
                    ("Nothing_v_235", [])]})]
CallStack (from HasCallStack):
  error, called at src/Gibbon/Language/Syntax.hs:149:11 in gibbon-0.2-inplace:Gibbon.Language.Syntax

There is a Nil defined, but for some reason it is differentiated from the sought-after Nil.
When commenting out the active line in the main function and replacing it with the line below, a similar-but-different type checking error is produced instead:

~/gibbon$ cabal v2-exec gibbon -- --packed --no-gc --to-exe ../llrbt/break.hs
gibbon: L0.Typecheck:
    Couldn't match type 'PackedTy "PList_v_232"
                                  []' with 'PackedTy "PList_v_235" []'
    Expected type: PackedTy "PList_v_235" []
    Actual type: PackedTy "PList_v_232" []
    In the expression:
      AppE "fold_plist_233"
           []
           [Ext (FunRefE [] "alt_maybe_230"),
            DataConE (ProdTy []) "Nothing_v_231" [],
            DataConE (ProdTy []) "Nil_v_232" []]
CallStack (from HasCallStack):
  error, called at src/Gibbon/L0/Typecheck.hs:66:32 in gibbon-0.2-inplace:Gibbon.L0.Typecheck

These functions are able to typecheck in translations to OCaml

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