Wrong handling of reach capabilities of local vals

[odersky]

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  // error

Output

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 found

With 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.