-
Notifications
You must be signed in to change notification settings - Fork 1.1k
Open
Labels
itype:bugstat:needs triageEvery issue needs to have an "area" and "itype" labelEvery issue needs to have an "area" and "itype" label
Description
Compiler version
Minimized code
import scala.language.experimental.captureChecking
import scala.language.experimental.separationChecking
trait Foo extends caps.ExclusiveCapability
trait Bar extends Foo, caps.Mutable
object Foo:
extension (consume self: Foo)
def sink: Unit = ()
def Test =
val x: Bar^ = new Bar {}
x.sink
x.sink // should error?Output
Compiles
Expectation
I expect the second call to x.sink to fail separation checking because x is a mutable reference (Bar^).
If we change x to val x: Foo = new Bar {}, then separation checking works as expected and the second call to x.sink fails.
I don't expect separation checking to fail if we had val x: Bar = new Bar {} (which works as expected).
Metadata
Metadata
Assignees
Labels
itype:bugstat:needs triageEvery issue needs to have an "area" and "itype" labelEvery issue needs to have an "area" and "itype" label