-
Notifications
You must be signed in to change notification settings - Fork 1.1k
CC: Various fixes and simplifications #23881
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
Conversation
These problems were discovered once we started recording uses of this references. The recording is not yet part of this commit because it requires downstream bugfixes in the compiler.
These fell through the cracks before since we only considered named outer refs. But inner classes can have outer this references check needd to be tracked in use sets.
Previously there was a boundary condition where this could be the case for outermost classes.
A constructor should never capture `this`, the object it constructs.
Was shockingly missing before.
- Charge the use set of the initializer to the class constructor - Charge the declared capture set to the class
The level checking should do the proper avoidance so that local symbols would not leak into type variables of the expected type.
This can lead to unsoundness. For instance: class C extends SharedCapability val b: C => C Then `b` is the owner of the FreshCap implicitly added to the result C, yet it should not be added to the hidden set, since `b` itself is not a SharedCapability.
What is the underlying capture set of a function? CC says the capture set on the first arrow but we experimented with the capture of the span of the function instead. This however causes a lot of complications if we want to push it to a logical conclusion. So we now make it configurable and by default span capture set is not used.
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 changes looks great to me!
Though I believe the original issue remains unsound. A mini example:
import language.experimental.captureChecking
import caps.*
class Console extends SharedCapability:
def println(msg: Any): Unit = ()
class C1:
this: C1^ =>
val console: Console^ = Console()
val foo: () ->{this.console} Unit = () =>
console.println(42)
def expect(x: C1^)(op: () ->{x.console} Unit): () ->{x} Unit = op
def test(whatever: () => Unit): Unit =
val c1: C1^{} = C1()
val pureFoo: () -> Unit = expect(c1)(c1.foo)
// ^^^ the same console effect, but pure!
The problem is that although this.console
is properly tracked inside the class, but the class that creates and uses the console capability (class C1
) remains pure. Then, with a simple trick, we can treat an operation with I/O effect as pure (the pureFoo
line).
But maybe this can be addressed in a follow-up PR? I am approving this one for now.
Yes, we are not there yet. There will be a follow-up PR to address the following:
|
Propagate expected type into blocks
The level checking should do the proper avoidance so that local symbols
would not leak into type variables of the expected type.
Don't automatically add a FreshCap owner to its hidden set
Don't use span capture sets for function types as the underlying set
Based on #23874