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
Relaxing the value restriction some more #7320
Comments
This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc. |
@garrigue @lpw25 this sounds like a proposal you would have opinions about. Did you review this issue during its stale period? (I think that the level mechanism suggested doesn't really work as an implementation approach because levels are only bumped in this example at |
Indeed, we discussed this with @garrigue and also @xavierleroy a long time ago, and yes, we only need to disallow generalization of type variables that contribute to the type of an exposed expansive expression where application of contructors are non-expansive and expressions under abstractions are not exposed. This is known to be sound. I am not sure that this alone cannot be fixed in the current implementation, but there are other more interesting and more useful examples that we would like to allow which we have also been considering with @garrigue which would imply deeper changes and require more discussions. |
Original bug ID: 7320
Reporter: @sliquister
Status: acknowledged (set by @damiendoligez on 2017-04-14T14:46:53Z)
Resolution: open
Priority: normal
Severity: feature
Target version: later
Category: typing
Monitored by: @gasche @yallop
Bug description
Relaxing the value restriction some more
If I write this:
the type f is not generalized. But I don't name the intermediate value:
or I name it at toplevel:
then the type is generalized.
It would be nice if, when I want to write something like the first snippet, I didn't have to write something like the third snippet instead, to work around the value restriction.
I think [
let x = e1 in e2
] should be generalized by saying:e1
is non-expansive, then generalize the type of the whole expressione2
to try to generalize it (the level mechanism would prevent generalization of the variables shared with the type ofe1
)ie when an expression is not non-expansive, instead of giving up on generalizing it, try to generalize the non-expansive parts of it instead.
This would make all 3 examples behave the same.
The text was updated successfully, but these errors were encountered: