Capture leak by pattern matching on type parameter

[noti0na1]

Compiler version

3.7.3-RC1-bin-SNAPSHOT-nonbootstrapped-git-42fdd76

Minimized code

import language.experimental.captureChecking
import caps.*

trait IO

def assertIO[T](x: T): IO = x match
  case io: IO => io
  case _ => throw new Exception("Expected an IO instance")

def leakIO(x: IO^): IO = assertIO(x)

Output

Compile success

Expectation

Error at case io: IO => io, io should not be a pure IO.

Even with #23524, the bug still presents, because T is boxed, so the capture set of x is empty.

Since we don't have a way to represent the capture set boxed by a type parameter, the bug cannot be fixed easily.

[odersky]

I think we need to assume in pattern matching somehow that io: IO^.

[noti0na1]

I think we need to assume in pattern matching somehow that io: IO^.

How do we know which class we want to add ^? Also, returning a "fresh" reference would still be unsafe, because the type says the returned reference is different from the tracked reference we passed in.