Skip to content

Commit

Permalink
Dealias type before checking reach refinements
Browse files Browse the repository at this point in the history
  • Loading branch information
Linyxus committed Apr 1, 2024
1 parent cc55381 commit 91fd6c2
Show file tree
Hide file tree
Showing 3 changed files with 26 additions and 1 deletion.
2 changes: 1 addition & 1 deletion compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
5 changes: 5 additions & 0 deletions tests/neg/unsound-reach-4.check
Original file line number Diff line number Diff line change
@@ -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
20 changes: 20 additions & 0 deletions tests/neg/unsound-reach-4.scala
Original file line number Diff line number Diff line change
@@ -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

0 comments on commit 91fd6c2

Please sign in to comment.