Drop reach capabilities#26246
Draft
odersky wants to merge 17 commits into
Draft
Conversation
Previously, anonymous functions were excluded. lambda-fresh-2.scala shows why this is unsound. We now drop the special treatment of anonymous functions, and at the same time exclude LocalCaps that come from outside the function from checking.
Previously, a closure could return an unscoped type with `any` in it (e.g., `Ref^`) but its type would be a pure function type. We now propagate the `any` into the function type. This has to be done with care though, since the `^` of a closure might come from the expected type, in which case we should ignore it. The tricky bit is distinguishing one from the other.
Drop two unused parameters.
Don't elide even if the capset belongs to a Capability class.
This replaces the special treatment of UnScoped in the ToResult map and makes Unscoped capabilities more versatile.
A LocalCap never accounts for a ResultCap, even if the classifier is Unscoped.
We need to do it after we widened an Unscoped fresh to any.
Both `// error` and `// warn` will now match one _or more_ error/warning. In user-facing docs, we usually do not want to mark every single error/warning, but just indicate that there should be some.
This is no longer needed since we now ensure monotonocity of closure types.
If a test can be rewritten using capset variables, do that, otherwise move to tests/disabled/reaches.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Based on #26193