Leaking scoped capability when the expected type of a block is boxed

[Linyxus]

Compiler version

main branch

Minimized code

trait Cap { def use(): Int; def close(): Unit }
def mkCap(): {*} Cap = ???
type Id[T] = Unit => T

def expect[T](x: T): x.type = x

def withCap[T](op: ({*} Cap) => T): T = {
  val cap: {*} Cap = mkCap()
  val result = op(cap)
  cap.close()
  result
}

def main(): Unit = {
  def badOp(io: {*} Cap): {} Unit -> Unit = {
    val op: {} Unit -> Unit = (x: Unit) =>
      expect[{*} Cap] {
        io.use()
        io
      }
    op
  }

  val leaked: {} Unit -> Unit = withCap(badOp)
  leaked(())  // use the leaked capability
}

Output

The code compiles.

Expectation

The code should not compile. More specifically, we should issue an error when typechecking the val op: ... = ... line, since the function uses the io capability inside its body so it is impure.

The cause of this issue: when type checking the block in the expect[{*} Cap] { ... } expression, the expected type is □ {*} Cap which is boxed, so we will create a temporary boxed Env for it and prevent the captured variable inside the block from charging the outer environment. However, at runtime the block does access the capability io when executing its statements.

Ideally, we should only create a boxed environment when typechecking the expression of the block, but not its statements.

[odersky]

Yes, that's a good point. We should create boxed environments only for values and references.