CC: Type variables can be used to bypass unboxing

[Linyxus]

Compiler version

main

Minimized code

import language.experimental.captureChecking
trait Op:
  def run(): Unit
def helper[X <: Op^](op: X): () -> Unit = () => op.run()  // should be error, but ok
def runOpForFree(op: Op^): () -> Unit = () => helper(op)

Output

It compiles.

Expectation

But it shouldn't. It converts arbitrary impure operation into a pure one, which is clearly unsound.

After some initial investigation, this seems to be an interaction between type variables, boxes, and asSeenFrom.

This is derived from the issue @noti0na1 showed during the group meeting.

[noti0na1]

trait IO:
  def f(): Unit

case class BoxIO[+T <: IO^](value: T) extends IO:
  def f(): Unit = value.f()

def test(io: IO^): IO =
  val b: BoxIO[IO^] = BoxIO(io)
  val a: IO = b // leak
  a

[noti0na1]

Related to #23574

[noti0na1]

trait IO:
def f(): Unit

case class BoxIO[+T <: IO^](value: T) extends IO:
def f(): Unit = value.f()

def test(io: IO^): IO =
val b: BoxIO[IO^] = BoxIO(io)
val a: IO = b // leak
a

Is this issue also addressed by the PR?

[Linyxus]

Unfortunately no. It is related to how we handle local freshcaps. I will open a new subissue.