-
Notifications
You must be signed in to change notification settings - Fork 59
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
Partial application for erased types, type parameters and implicits should be permitted when lowering to C #112
Comments
Both of these examples can be fixed by marking
However, I would still consider this is a usability issue, at the very least. The fundamental reason for this is, in Low*, However, we have no way through the syntax of types to figure out which one of these two a user intended to express. This means that the user will have a very hard time even writing higher-order function types since there's not even syntax for it. So, by default, What KreMLin does to recover from this limitation is look at the number of arguments on a function definition. At definition-time, we can do second-order, and "chop" the function type according to the number of arguments. So if you do:
KreMLin will know that
the first argument of Now about this specific bug report. What happens is, when matching a function definition against its type, and trying to "chop up" the function type to match the number of arguments, due to the type abbreviation, there are now less arrows than the number of arguments, which gets the extraction confused. This is an F* warning and looks as follows:
confusingly, the function is (right now) extracted nonetheless because making this a hard fail caused a regression in other parts of Everest. My goal is to at least make this a fatal warning, so that KreMLin doesn't receive invalid information. Then, F* should be able to do the inlining automatically so that the user doesn't have to write inline_for_extraction on the type definition. Hope this helps, Jonathan |
Thank you for the detailed explanation. I will try the suggested workaround for example 1
and report if anything else comes up |
In general partial application is not permitted in Low* to C extraction. However, for certain parameters, this can be reasonably allowed - namely
Reason why above should be possible
Some of these cases are partially supported and may partially work with some of the listed workarounds below, but still run into issues. Here are examples for the first 2 cases that cause some issues
Example of erased type partial application failure
This fails with the following error
Marking foo with
unfold
orinline_with_extraction
lets it go further but it now fails withExample of type parameters partial application failure
This creates the following error
Workaround - However, the workaround of marking
t_F
asinline_for_extraction
allows this example to work, but there are likely other examples, where this would not suffice.The text was updated successfully, but these errors were encountered: