Plug soundness hole for reach capabilities

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

@@ -249,6 +249,44 @@ class CheckCaptures extends Recheck, SymTransformer:
           else i"references $cs1$cs1description are not all",
           pos, provenance)
 
+    def showRef(ref: CaptureRef)(using Context): String =
+        ctx.printer.toTextCaptureRef(ref).show
+
+    // Uses 4-space indent as a trial
+    def checkReachCapsIsolated(tpe: Type, pos: SrcPos)(using Context): Unit =
+
+        object checker extends TypeTraverser:
+            var refVariances: Map[Boolean, Int] = Map.empty
+            var seenReach: CaptureRef | Null = null
+            def traverse(tp: Type) =
+                tp match
+                case CapturingType(parent, refs) =>
+                    traverse(parent)
+                    for ref <- refs.elems do
+                        if ref.isReach && !ref.stripReach.isInstanceOf[TermParamRef]
+                            || ref.isRootCapability
+                        then
+                            val isReach = ref.isReach
+                            def register() =
+                                refVariances = refVariances.updated(isReach, variance)
+                                seenReach = ref
+                            refVariances.get(isReach) match
+                                case None => register()
+                                case Some(v) => if v != 0 && variance == 0 then register()
+                case _ =>
+                    traverseChildren(tp)
+
+        checker.traverse(tpe)
+        if checker.refVariances.size == 2
+            && checker.refVariances(true) >= 0
+            && checker.refVariances(false) <= 0
+        then
+            report.error(
+                em"""Reach capability ${showRef(checker.seenReach.nn)} and universal capability cap cannot both
+                    |appear in the type $tpe of this expression""",
+                pos)
+    end checkReachCapsIsolated
+
     /** The current environment */
     private val rootEnv: Env = inContext(ictx):
       Env(defn.RootClass, EnvKind.Regular, CaptureSet.empty, null)
@@ -779,8 +817,10 @@ class CheckCaptures extends Recheck, SymTransformer:
           report.error(ex.getMessage.nn)
           tree.tpe
         finally curEnv = saved
-      if tree.isTerm && !pt.isBoxedCapturing then
-        markFree(res.boxedCaptureSet, tree.srcPos)
+      if tree.isTerm then
+        checkReachCapsIsolated(res.widen, tree.srcPos)
+        if !pt.isBoxedCapturing then
+          markFree(res.boxedCaptureSet, tree.srcPos)
       res
 
     override def recheckFinish(tpe: Type, tree: Tree, pt: Type)(using Context): Type =

tests/neg/unsound-reach-2.scala

@@ -0,0 +1,25 @@
+import language.experimental.captureChecking
+trait Consumer[-T]:
+  def apply(x: T): Unit
+
+trait File:
+  def close(): Unit
+
+def withFile[R](path: String)(op: Consumer[File]): R = ???
+
+trait Foo[+X]:
+  def use(x: File^)(op: Consumer[X]): Unit
+class Bar extends Foo[File^]:
+  def use(x: File^)(op: Consumer[File^]): Unit = op.apply(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 =>
+    boom.use(f): // error
+      new Consumer[File^{backdoor*}]:
+        def apply(f1: File^{backdoor*}) =
+          escaped = f1
+

tests/neg/unsound-reach-3.scala

@@ -0,0 +1,21 @@
+import language.experimental.captureChecking
+trait File:
+  def close(): Unit
+
+def withFile[R](path: String)(op: File^ => R): R = ???
+
+trait Foo[+X]:
+  def use(x: File^): X
+class Bar extends Foo[File^]:
+  def use(x: File^): 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
+      // boom.use: (x: File^) -> File^{backdoor*}, it is a selection so reach capabilities are allowed
+      // f: File^, so there is no reach capabilities
+

tests/neg/unsound-reach.check

@@ -0,0 +1,5 @@
+-- Error: tests/neg/unsound-reach.scala:18:9 ---------------------------------------------------------------------------
+18 |    boom.use(f): (f1: File^{backdoor*}) => // error
+   |    ^^^^^^^^
+   |    Reach capability backdoor* and universal capability cap cannot both
+   |    appear in the type (x: File^)(op: box File^{backdoor*} => Unit): Unit of this expression

tests/neg/unsound-reach.scala

@@ -0,0 +1,20 @@
+import language.experimental.captureChecking
+trait File:
+  def close(): Unit
+
+def withFile[R](path: String)(op: File^ => R): R = ???
+
+trait Foo[+X]:
+  def use(x: File^)(op: X => Unit): Unit
+class Bar extends Foo[File^]:
+  def use(x: File^)(op: File^ => Unit): Unit = op(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 =>
+    boom.use(f): (f1: File^{backdoor*}) => // error
+      escaped = f1
+