Skip to content

How subcapturing works for this is unsound #19315

Closed
@Linyxus

Description

@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

Metadata

Metadata

Assignees

Labels

cc-experimentIntended to be merged with cc-experiment branch on originitype:bug

Type

No type

Projects

No projects

Milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions