-
Notifications
You must be signed in to change notification settings - Fork 88
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
Fix polarity for polymorphic contract failure #831
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The polarity isn't always positive:
let evaluate_incr_at_1 : (forall a. (a -> a) -> a -> a) -> Num = fun ev =>
ev ((+) 1) 1 in
evaluate_incr_at_1 (fun f x => null)
This should blame the caller, not evaluate_incr_at_1
. The point is, the polarity is not the one of the occurrence of the type variable, but is the polarity of the introducing forall _
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM. Because the logic is not obvious, a little comment in the code could help our decedent (important information: we set the polarity of the label to lPol
because this is what's important for blaming polymorphic contracts).
In the future it could be nice to have an even more specialized error message. But that can come in a later PR. In general I've been thinking lately about enriching the interface of label
in the Nickel language itself, so that custom contracts can set "notes" and additional messages by themselves, instead on relying only on the erase-on-write msg
field
Interesting. This would probably require adding a new operator to set the "notes" field. |
Yes. Maybe at some point it would be easier to make it an actual Nickel record, so that you can at least set polarity, message and other basic things directly using |
Closes #821