From 91fd6c20bdddaed0f21739f620e67516c999292a Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 1 Apr 2024 12:12:00 +0100 Subject: [PATCH 1/2] Dealias type before checking reach refinements --- .../dotty/tools/dotc/cc/CheckCaptures.scala | 2 +- tests/neg/unsound-reach-4.check | 5 +++++ tests/neg/unsound-reach-4.scala | 20 +++++++++++++++++++ 3 files changed, 26 insertions(+), 1 deletion(-) create mode 100644 tests/neg/unsound-reach-4.check create mode 100644 tests/neg/unsound-reach-4.scala diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 675cd012e801..9b6217033ede 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -259,7 +259,7 @@ class CheckCaptures extends Recheck, SymTransformer: var refVariances: Map[Boolean, Int] = Map.empty var seenReach: CaptureRef | Null = null def traverse(tp: Type) = - tp match + tp.dealias match case CapturingType(parent, refs) => traverse(parent) for ref <- refs.elems do diff --git a/tests/neg/unsound-reach-4.check b/tests/neg/unsound-reach-4.check new file mode 100644 index 000000000000..47256baf408a --- /dev/null +++ b/tests/neg/unsound-reach-4.check @@ -0,0 +1,5 @@ +-- Error: tests/neg/unsound-reach-4.scala:20:19 ------------------------------------------------------------------------ +20 | escaped = boom.use(f) // error + | ^^^^^^^^ + | Reach capability backdoor* and universal capability cap cannot both + | appear in the type (x: F): box File^{backdoor*} of this expression diff --git a/tests/neg/unsound-reach-4.scala b/tests/neg/unsound-reach-4.scala new file mode 100644 index 000000000000..fa395fa117ca --- /dev/null +++ b/tests/neg/unsound-reach-4.scala @@ -0,0 +1,20 @@ +import language.experimental.captureChecking +trait File: + def close(): Unit + +def withFile[R](path: String)(op: File^ => R): R = ??? + +type F = File^ + +trait Foo[+X]: + def use(x: F): X +class Bar extends Foo[File^]: + def use(x: F): File^ = x + +def bad(): Unit = + val backdoor: Foo[File^] = new Bar + val boom: Foo[File^{backdoor*}] = backdoor + + var escaped: File^{backdoor*} = null + withFile("hello.txt"): f => + escaped = boom.use(f) // error From 52f3c08ac2e7525c758f78d6cdb10e3b216a8869 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Fri, 5 Apr 2024 00:11:35 +0200 Subject: [PATCH 2/2] Dealias types when checking contra-variant caps --- compiler/src/dotty/tools/dotc/cc/CaptureOps.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala index 7c75ed833945..12ec1fdafb32 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala @@ -289,7 +289,7 @@ extension (tp: Type) var ok = true def traverse(t: Type): Unit = if ok then - t match + t.dealias match case CapturingType(_, cs) if cs.isUniversal && variance <= 0 => ok = false case _ =>