Closed
Description
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 assumel
being a subcapture ofthis
. - The capture set of
Foo
is empty, as the reference tol
is boxed. - The type of the method
foo
isBoxed[Logger^{this}]
. - When selecting
x.foo
, it is typed asBoxed[Logger^{x}]
. - We unbox it and get
Logger^{x}
, which is a subtype ofLogger^{}
.
/cc @odersky