Skip to content

Commit

Permalink
Fix i19315: avoid calling addOuterRefs when the actual type is box-…
Browse files Browse the repository at this point in the history
…adapted (#19323)

Fixes #19315.

The unsound code:
```scala
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
```

The `magic` function typechecks before this fix. It casts a capability
to a pure value, which is clearly unsound. The crux of the problem is
`Boxed[Logger^{this}](l)`, which relies on the subcapturing relation
`{l} <: {this}` enabled by the trick implemented `addOuterRefs`.

`addOuterRefs` augment a capture set that contains a self reference
(like `{this}`) with all outer references reachable from `this`. In this
case, the augmented set is `{this, l}`. The reasoning is that, any
captured outer references in the class can be rewritten into a field,
thus being a subcapture of `{this}`:
```
class Foo:
  val this_l: Logger^{l} = l
  def foo: Boxed[Logger^{this}] = Boxed(this.this_l)
```

But the problem with this unsound example is that, the reference to `l`
is boxed, so `l` is not captured by the class. Therefore, the above
rewriting mismatches with the actual situation.

This PR proposes a simple fix, which simply disable `addOuterRefs` when
box adaptation happens. This is of course imprecise, but all tests pass
with this fix.
  • Loading branch information
odersky authored Jan 11, 2024
2 parents 16b26ad + a40fb19 commit b2ba6dc
Show file tree
Hide file tree
Showing 2 changed files with 20 additions and 1 deletion.
6 changes: 5 additions & 1 deletion compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
Original file line number Diff line number Diff line change
Expand Up @@ -847,9 +847,13 @@ class CheckCaptures extends Recheck, SymTransformer:
* where local capture roots are instantiated to root variables.
*/
override def checkConformsExpr(actual: Type, expected: Type, tree: Tree, addenda: Addenda)(using Context): Type =
val expected1 = alignDependentFunction(addOuterRefs(expected, actual), actual.stripCapturing)
var expected1 = alignDependentFunction(expected, actual.stripCapturing)
val actualBoxed = adaptBoxed(actual, expected1, tree.srcPos)
//println(i"check conforms $actualBoxed <<< $expected1")

if actualBoxed eq actual then
// Only `addOuterRefs` when there is no box adaptation
expected1 = addOuterRefs(expected1, actual)
if isCompatible(actualBoxed, expected1) then
if debugSuccesses then tree match
case Ident(_) =>
Expand Down
15 changes: 15 additions & 0 deletions tests/neg-custom-args/captures/cc-selftype-unsound.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
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) // error
val x = new Foo
val y = x.foo.unbox // y: Logger^{x}
val z: Logger = y // now the capability becomes pure
z

0 comments on commit b2ba6dc

Please sign in to comment.