Wrong handling of reach capabilities of local vals #23579
Description
Compiler version
3.7
Minimized example
import language.experimental.captureChecking // no separation checking def localReach() = val xs: List[() => Unit] = ??? var ys: List[() ->{xs*} Unit] = xs var x: () ->{xs*} Unit = ys.head while ys.nonEmpty do ys = ys.tail x = ys.head def localReach2(op: () => Unit) = val xs: List[() => Unit] = op :: Nil var ys: List[() ->{xs*} Unit] = xs var x: () ->{xs*} Unit = ys.head while ys.nonEmpty do ys = ys.tail x = ys.head def localReach3(ops: List[() => Unit]) = val xs: List[() => Unit] = ops var ys: List[() ->{xs*} Unit] = xs var x: () ->{xs*} Unit = ys.head while ys.nonEmpty do ys = ys.tail x = ys.head // errorOutput
Without separation checking:
-- Error: localReaches.scala:11:11 --------------------------------------------- 11 | x = ys.head | ^^^^^^^ |Local reach capability xs* leaks into capture scope of method localReach -- Error: localReaches.scala:19:11 --------------------------------------------- 19 | x = ys.head | ^^^^^^^ |Local reach capability xs* leaks into capture scope of method localReach2 -- Error: localReaches.scala:27:11 --------------------------------------------- 27 | x = ys.head // error | ^^^^^^^ |Local reach capability xs* leaks into capture scope of method localReach3 3 errors foundWith separation checking:
-- Error: localReaches.scala:14:10 --------------------------------------------- 14 | val xs: List[() => Unit] = op :: Nil | ^^^^^^^^^^^^^^^^ |Separation failure: value xs's type List[() => Unit] hides parameter op. |The parameter needs to be annotated with @consume to allow this. -- Error: localReaches.scala:22:10 --------------------------------------------- 22 | val xs: List[() => Unit] = ops | ^^^^^^^^^^^^^^^^ |Separation failure: value xs's type List[() => Unit] hides parameter ops. |The parameter needs to be annotated with @consume to allow this. 2 errors found Expectation
Without separation checking we would expect only the last error on line 27 to be issued. With separation checking we'd still expect the error on line 27 to be issued. The problem is that the other separation errors can be made to go away by using cap.only[Sharable] instead of cap. So we should not rely on separation checking to ensure non-escaping reaches.