CC: Tracked Non-Capability Classes Can Leak

[bracevac]

Compiler version

3.8 nightly

Minimized code

import language.experimental.captureChecking
import caps.*

object Test:
  trait Closeable:
    def close(): Unit

  class FileOutputStream(path: String) extends Closeable:
    def write(data: Array[Byte]): Unit = ???
    def close(): Unit = ???

  def using[A <: Closeable, B](acquire: A^)(f: A^{acquire} => B): B =
    val resource = acquire
    val result = f(resource)
    resource.close()
    result

  // should not compile because output captures acquire which is not allowed
  val output = using(FileOutputStream("out"))(identity)

Output

This is accepted, but should be rejected.

Let's take a look at the -Vprint:cc -Ycc-verbose output of the last line:

val output: Test.FileOutputStream^{} =
      Test.using[box Test.FileOutputStream^'s2, box Test.FileOutputStream^'s3](
        new Test.FileOutputStream("out"))((x: Test.FileOutputStream^'s4) =>
        identity[box Test.FileOutputStream^'s5](x))

Somehow it determines that the result is a pure FileOutputStream and has a bunch of unsolved constraint variables.

Expectation

It should be rejected. It will rightfully reject if we declare trait Closable extends SharedCapability.

-- [E007] Type Mismatch Error: local/ccadrien.scala:19:46 ----------------------
19 |  val output = using(FileOutputStream("out"))(identity)
   |                                              ^^^^^^^^
   |Found:    (x: box Test.FileOutputStream^'s1) ->'s2 box Test.FileOutputStream^'s3
   |Required: (box Test.FileOutputStream^'{cap.rd})^{cap.rd} ->{cap²}
   |  box Test.FileOutputStream^'s4
   |
   |Note that capability cap³.rd cannot be included in outer capture set 's4.
   |
   |where:    cap  is a fresh root capability classified as SharedCapability created in value output when constructing Capability instance Test.FileOutputStream
   |          cap² is a fresh root capability created in value output when checking argument to parameter f of method using
   |          cap³ is a root capability associated with the result type of (x: (box Test.FileOutputStream^'{cap.rd})^{cap.rd}):
   |  box Test.FileOutputStream^'s4
   |
   | longer explanation available when compiling with `-explain`

and here's the debug output of the last line for comparison:

val output: Test.FileOutputStream^{} =
      Test.using[
        
          box Test.FileOutputStream^'{<fresh in val output hiding 's8
             classified as SharedCapability>.rd}
        ,
      box Test.FileOutputStream^'s4](new Test.FileOutputStream("out"))((
        x: Test.FileOutputStream^'s1) =>
        identity[box Test.FileOutputStream^'s9](x))

[noti0na1]

It also compiles even without the type parameter A.

[bracevac]

After internal discussion, we concluded this is not a bug:

1. For preventing escaping in a try-with-resources pattern, we should use just the hat f: A^ => B. That will already fix the given example.

2. Java classes like FileOutputStream are generally considered "pure" classes, so their capture set can be dropped. If they are supposed to be fully tracked, then they need to be encapsulated in some capability class.