How subcapturing works for this is unsound

[Linyxus]

Compiler version

main

Minimized code

import language.experimental.captureChecking
trait Logger
case class Boxed[T](unbox: T)

// a horrible function, but it typechecks
def magic(l: Logger^): Logger =
  class Foo:
    def foo: Boxed[Logger^{this}] =
      // for the following line to typecheck
      //   the capture checker assumes {l} <: {this}
      Boxed[Logger^{this}](l)
  val x = new Foo
  val y = x.foo.unbox  // y: Logger^{x}
  val z: Logger = y  // now the capability becomes pure
  z

Output

It typechecks.

Expectation

It should not typecheck. With magic one may make any capability pure.

Why it typechecks:

• When typechecking Foo, we assume l being a subcapture of this.
• The capture set of Foo is empty, as the reference to l is boxed.
• The type of the method foo is Boxed[Logger^{this}].
• When selecting x.foo, it is typed as Boxed[Logger^{x}].
• We unbox it and get Logger^{x}, which is a subtype of Logger^{}.

/cc @odersky