Weird Subcapturing Interaction between reach and only

[bracevac]

Compiler version

Well, it's on this PR

Minimized code

import language.experimental.captureChecking
import language.experimental.separationChecking
import caps.*

object Levels:

  trait Read extends Classifier, Capability
  trait ReadWrite extends Classifier, Capability

  case class Box[T](access: T)

  trait File(val name: String):
    val r: Box[Read^]
    val rw: Box[ReadWrite^]
    // operations guarded by boxed capability members
    val read: () ->{r.access*} Int
    val write: Int ->{rw.access*} Unit

  object File:
    def apply(s: String): File = ???

  // Unfortunately, we do not have @use lambdas yet
  trait UseFunction[U]:
    def apply(@use f: File^): U

  def withFile[U](name: String)(block: UseFunction[U]): U = block(File(name)) // unrestricted use of files & other capabilities
  def parReduce[U](xs: Seq[U])(op: (U, U) ->{cap.only[Read]} U): U = xs.reduce(op) // only Read-classified allowed

  @main def test =
    withFile("foo.txt")(
      new UseFunction[Unit] {
        def apply(@use f: File^): Unit = {
          parReduce(1 to 1000){ (a, b) =>
            //println(f.r.access) // charges r.access* to environment
            //f.write(42)         // error, as it should be
            a + b + f.read()      // should be ok, but errors
          }
          f.write(42)         // ok, unrestricted access to file
        }
      }
    )

Output

The capture set {f.read} of the closure passed to parReduce allegedly does not conform to {cap.only[Read]}:

-- [E007] Type Mismatch Error: local/secondclass.scala:42:30 -------------------
42 |          parReduce(1 to 1000){ (a, b) =>
   |                              ^
   |Found:    (a: Int, b: Int) ->{f.read} Int
   |Required: (Int, Int) ->{cap.only[Read]} Int
   |
   |where:    cap is a fresh root capability created in method apply when checking argument to parameter op of method parReduce

However, if we uncomment the line println(f.r.access), then the program will be accepted!

Expectation

It should already be accepted as-is.

Intuitively, I'd expect that {f.read} <: {f.r.access*} <: {cap.only[Read]} holds, but somehow the compiler is only convinced of that if we explicitly unbox f.r in the superfluous println statement.

[bracevac]

It gets even weirder:

def apply(@use f: File^): Unit = {
  f.read()
  parReduce(1 to 1000){ (a, b) =>
    println(f.r.access) // charges r.access.* to environment
    //f.write(42)       // error
    a + b + f.read()  // ok
  }
  f.write(42)         // ok, unrestricted access to file
}

If we insert f.read() before the parReduce call, then the println(f.r.access) workaround will cease to work:

- [E007] Type Mismatch Error: local/secondclass.scala:43:30 -------------------
43 |          parReduce(1 to 1000){ (a, b) =>
   |                              ^
   |Found:    (a: Int, b: Int) ->{f.r.access*} Int
   |Required: (Int, Int) ->{cap.only[Read]} Int
   |
   |where:    cap is a fresh root capability created in method apply when checking argument to parameter op of method parReduce

[bracevac]

Minimization:

import language.experimental.captureChecking
import language.experimental.separationChecking
import language.`3.8`
import caps.*

object Levels:

  trait Read extends Classifier, Capability
  trait ReadWrite extends Classifier, Capability

  case class Box[T](access: T)

  def parReduce(xs: Seq[Int])(op: (Int, Int) ->{cap.only[Read]} Int): Int = xs.reduce(op)

  @main def test =
    val r: Box[Read^] = ???
    val rw: Box[ReadWrite^] = ???
    val read: () ->{r.access*} Int = ???
    val write: Int ->{rw.access*} Unit = ???
    //read() // causes error with and without the println below
    parReduce(1 to 1000) { (x, y) =>
      println(r.access) // ok only if this is uncommented
      read() + read() // should be ok
    }
    parReduce(1 to 1000) { (x, y) =>
      write(x) // should be error
      x + y + read() // should be ok
    }

[bracevac]

And here a version without putting the capabilities into boxes, it works as intended:

import language.experimental.captureChecking
import language.experimental.separationChecking
import language.`3.8`
import caps.*

object Levels:

  trait Read extends Classifier, Capability
  trait ReadWrite extends Classifier, Capability

  def parReduce(xs: Seq[Int])(op: (Int, Int) ->{cap.only[Read]} Int): Int = xs.reduce(op)

  @main def test =
    val r: Read^ = ???
    val rw: ReadWrite^ = ???
    val read: () ->{r} Int = ???
    val write: Int ->{rw} Unit = ???
    read() // ok
    parReduce(1 to 1000) { (x, y) =>
      read() + read() // ok
    }
    parReduce(1 to 1000) { (x, y) =>
      write(x) // error, as intended
      x + y + read() // ok
    }
    write(42) // ok

So there seems to be something wrong with boxing and reach caps here.

Edit: Can confirm that this boxless solution works as intended for the initial example involving withFile. I still think that the boxed version should work as well.

[Linyxus]

Looks very related to #23580. For this to work we need to check the info of p given p*.