Ensure monotonicity of the types of closures#26193
Conversation
36a4c5d to
2412b6a
Compare
|
@bracevac Can you take a look at the scaladoc test failure? It's hard to see what goes on here. |
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.
|
@odersky I fixed the test in question. But tbh, this one was no different than a cc compilation test, so it's not unreasonable to expect someone working on cc to fix them. Certain other tests for scaladoc and REPL I will absolutely insist on keeping them, as they affect user experience. |
odersky
left a comment
There was a problem hiding this comment.
Yes, that's much better! I completely agree we need snippet tests for specific cc code. But we should be 100% dumb for generic functionality such as whether more than one expectation per line is checked.
|
We now see extra errors on already |
|
I ended up with a simpler change that lets |
|
|
||
| val _: () -> One^{fresh} = () => One() // ok | ||
| val _: () => One^{fresh} = () => One() // ok | ||
| val _: () => One^{fresh} = f2 // ok |
There was a problem hiding this comment.
I wonder: does the notion of fresh here ever make sense without an ExclusiveCapability?
Which is to say, if One is already known to be exclusive, why can't One^ just mean fresh?
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.
5ff528f to
4b737ca
Compare
Previously, a closure could return an unscoped type with
anyin it(e.g.,
Ref^) but its type would be a pure function type. We now propagatethe
anyinto the function type. This has to be done with care though, sincethe
^of a closure might come from the expected type, in which case weshould ignore it. The tricky bit is distinguishing one from the other.