Capture leak by pattern matching on GADT

[Alex1005a]

Compiler version

3.8.4-RC1-bin-20260222-dd3cd80-NIGHTLY

Minimized code

sealed trait AbstractBox[A]
case class Box[A](x: A) extends AbstractBox[A]
def leak[A](x: AbstractBox[A^]): A = {
  x match {
    case Box(y) => y
  }
}

It is also possible to compile code with a leaky non-polymorphic capability without a GADT.

case class Foo()
case class Box[A](x: A)
def fooLeak(x: Box[Foo^]): Box[Foo] = {
  x match {
    case Box(y) => Box(y)
  }
}

Output

Both examples compile.

Expectation

Should not compile.

[bracevac]

Pattern matching is not yet 100% fleshed out for cc.

I've tried these on #25316 and I agree that the first example is a problem, here's the -Vprint:cc output:

def leak[A](x: AbstractBox[A^]): A =
      {
        matchResult4[A^'s1]: 
          {
            case val x5: (x : AbstractBox[A^]) = x
            if x5.$isInstanceOf[Box[A]] then
              {
                case val x6: Box[A^{}]^{} = x5.$asInstanceOf[Box[A]^{x5}]
                case val x7: Box[A^{}]^{} = Box.unapply[A^'s2](x6)
                case val x8: A^{} = x7._1
                case val y: A^{} = x8
                return[matchResult4]
                  {
                    y:(A^'s3)
                  }
              }
             else ()
            throw new MatchError(x5)
          }
      }
    def whoops: Foo^{} = leak[Foo^'s4](Box.apply[Foo^](new Foo()))

This doesn't look right. Though note that if we upper-bound all the As in the example with <: SharedCapability, we'll get a proper compile-time error. However, the -Vprint:cc output in that case also looks weird.

Edit: I should add that I tried the following use site

class Foo extends SharedCapability
def whoops =
  leak(Box(Foo()))

As for the second example, I disagree that this is a bug: Foo is not declared a tracked capability type, and is from the capture-checking perspective "pure".
If we change it to

case class Foo() extends SharedCapability

then it fails as expected.

Summoning the boxing-and-GADT-meister @Linyxus

[Alex1005a]

Thanks for the quick reply. Regarding the second example: it turns out that it will not be possible to control the lifetime for capabilities that do not inherit Capability? For example, the documentation contains the Logger class, which does not inherit from anything, and the logged function for safe use. Using the second example, you can leak Logger when using logged.

class Logger
def logged[T](op: Logger^ => T): T = ???

case class Box[A](x: A)
def loggerLeak(x: Box[Logger^]): Box[Logger] = {
  x match {
    case Box(y) => Box(y)
  }
}

def testLeak: Logger = {
  logged(l => loggerLeak(Box(l))).x
}

[bracevac]

Thanks for the quick reply. Regarding the second example: it turns out that it will not be possible to control the lifetime for capabilities that do not inherit Capability? For example, the documentation contains the Logger class, which does not inherit from anything, and the logged function for safe use. Using the second example, you can leak Logger when using logged.

Your example simplifies too much away, here's the full context from the overview doc:

import language.experimental.captureChecking
import caps.*

class File(path: String) extends ExclusiveCapability
class Logger(f: File)
def logged[T](op: Logger^ => T): T = ???

case class Box[A](x: A)
def loggerLeak(x: Box[Logger^]): Box[Logger] = {
  x match {
    case Box(y) => Box(y) // error
  }
}

def testLeak: Logger = {
  logged(l => loggerLeak(Box(l))).x // error
}

It's important that Logger depends on Files which are marked as tracked capabilities.

[Alex1005a]

It's important that Logger depends on Files which are marked as tracked capabilities.

But there are also examples in the documentation where classes do not depend on tracked capabilities, for example java.io.FileOutputStream. There will be no compilation error for them.

I also wanted to ask a question about a problem that caused me to find the original bug. Maybe this is also a bug. There is a code where capabilities Foo are in the list. If you try to return this list from the function, a compilation error occurs correctly. But if you try to call some function to iterate through the list, error Local reach capability foos* leaks into capture scope of an enclosing function occurs. Do I need to write a separate foreach function specifically for lists with capabilities?

class Foo extends SharedCapability
def usingFoos[A](f: List[Foo] => A): A = ???

def testFoo = {
  usingFoos { foos =>
    foos.foreach(_ => ()) // error here
    ()
  }
}

[bracevac]

But there are also examples in the documentation where classes do not depend on tracked capabilities, for example java.io.FileOutputStream. There will be no compilation error for them.

Good point, then I'm convinced that the second example is also a bug.
I was initially thinking that we are observing a cc feature that relies on non-abstract, non-open classes in Scala 3 being by default sealed and hence the capture checker would automatically infer class Logger (without the constructor parameter) is always pure. But changing it to abstract or a trait won't affect the outcome.

Do I need to write a separate foreach function specifically for lists with capabilities?

This is a known bug #25093