Closed
Description
Compiler version
main
Minimized code
import language.experimental.captureChecking
trait IO:
def use(): Unit
case class Boxed[+T](unbox: T)
// `foo` is a function that unboxes its parameter
// and uses the capability boxed inside the parameter.
def foo(x: Boxed[IO^]): Unit =
x.unbox.use() // error: local reach capability {x*} leaks
// `bar` is a function that does the same thing in a
// slightly different way.
// But, no type error reported.
def bar(x: Boxed[IO^]): Unit =
val x1: Boxed[IO^] = x
val io = x1.unbox
io.use()
Output
-- Error: issues/localreach.scala:9:4 ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
9 | x.unbox.use() // error: local reach capability {x*} leaks
| ^^^^^^^
| Local reach capability x* leaks into capture scope of method foo
(only one error reported)
Expectation
Both functions should have a type error.
/cc @odersky