Skip to content

Commit f3139cd

Browse files
authored
Tighten the screws a bit more to seal the soundness hole for reach capabilities (#20056)
2 parents d07f6cc + 52f3c08 commit f3139cd

File tree

4 files changed

+27
-2
lines changed

4 files changed

+27
-2
lines changed

compiler/src/dotty/tools/dotc/cc/CaptureOps.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -289,7 +289,7 @@ extension (tp: Type)
289289
var ok = true
290290
def traverse(t: Type): Unit =
291291
if ok then
292-
t match
292+
t.dealias match
293293
case CapturingType(_, cs) if cs.isUniversal && variance <= 0 =>
294294
ok = false
295295
case _ =>

compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -259,7 +259,7 @@ class CheckCaptures extends Recheck, SymTransformer:
259259
var refVariances: Map[Boolean, Int] = Map.empty
260260
var seenReach: CaptureRef | Null = null
261261
def traverse(tp: Type) =
262-
tp match
262+
tp.dealias match
263263
case CapturingType(parent, refs) =>
264264
traverse(parent)
265265
for ref <- refs.elems do

tests/neg/unsound-reach-4.check

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
-- Error: tests/neg/unsound-reach-4.scala:20:19 ------------------------------------------------------------------------
2+
20 | escaped = boom.use(f) // error
3+
| ^^^^^^^^
4+
| Reach capability backdoor* and universal capability cap cannot both
5+
| appear in the type (x: F): box File^{backdoor*} of this expression

tests/neg/unsound-reach-4.scala

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
import language.experimental.captureChecking
2+
trait File:
3+
def close(): Unit
4+
5+
def withFile[R](path: String)(op: File^ => R): R = ???
6+
7+
type F = File^
8+
9+
trait Foo[+X]:
10+
def use(x: F): X
11+
class Bar extends Foo[File^]:
12+
def use(x: F): File^ = x
13+
14+
def bad(): Unit =
15+
val backdoor: Foo[File^] = new Bar
16+
val boom: Foo[File^{backdoor*}] = backdoor
17+
18+
var escaped: File^{backdoor*} = null
19+
withFile("hello.txt"): f =>
20+
escaped = boom.use(f) // error

0 commit comments

Comments
 (0)