Closed
Description
Compiler version
main
Minimized code
import language.experimental.captureChecking
trait IO:
def println(s: String): Unit
def usingIO[R](op: IO^ => R): R = ???
case class Boxed[+T](unbox: T)
type Res = [R, X <: Boxed[IO^] -> R] -> (op: X) -> R
def mkRes(x: IO^): Res =
[R, X <: Boxed[IO^] -> R] => (op: X) =>
val op1: Boxed[IO^] -> R = op
op1(Boxed(x))
def test2(): Unit =
val leaked: Res = usingIO[Res](mkRes)
val x = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x)
x.unbox.println("boom") // out of scope access to the scoped capability
Output
It compiles.
Expectation
It should not. It allows an out-of-scoped access to a scoped capability.
/cc @odersky