Dependent function application can leak a scoped capability

[Linyxus]

Compiler version

main branch

Minimized code

import language.experimental.captureChecking
import java.io.*

object Test:
  class Logger(f: OutputStream^):
    def log(msg: String): Unit = ???

  def usingFile[sealed T](name: String, op: OutputStream^ => T): T =
    val f = new FileOutputStream(name)
    val result = op(f)
    f.close()
    result

  def usingLogger[sealed T](f: OutputStream^)(op: Logger^{f} => T): T = ???

  usingFile(
    "foo",
    file => {
      usingLogger(file)(l => () => l.log("test"))  // leaking the local logger
    }
  )  // should be error but it compiles

Output

It compiles, but the last lines should be rejected since the scoped capability is leaked in the result.

Expectation

There should be an error on the last lines.

[Linyxus]

This is a soundness problem related to capture set inference. To better see the problem we first inspect the typed tree of the usingFile application:

  usingFile[() ->?1 Unit](
    "foo",
    file => {
      usingLogger[() ->?2 Unit](file)(l => () => l.log("test"))  // leaking the local logger
    }
  )  // should be error but it compiles

The problem comes down to the inference of the capture set variables ?1 and ?2. What happens here? Let's inspect the flow of captured reference from the innermost of the expression:

• First, the capture-checked type of l => () => l.log("test") will be (l : Logger^{file}) -> () ->{file} Unit.
• After checking the conformance between the expected type and the actual type, the local parameter reference l is propagated to ?2.
• Afterwards, l is propagated from ?2 to ?1.
• When "healing" the captured references in ?1, we see that l is a TermParamRef and we widen it to its context capture set, which is {file}.
• At this point, we should have further widen file to *, which would correct generate the error, but file here is a TermRef. Although it is a TermRef to a parameter bound by a later lambda, the current "healing" logic is not aware of it and does not widen it.
• The code passes compilation, and we get a soundness problem.