Drop checkReachCapsIsolated restriction

Author: odersky

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

@@ -259,7 +259,7 @@ class CheckCaptures extends Recheck, SymTransformer:
         ctx.printer.toTextCaptureRef(ref).show
 
     // Uses 4-space indent as a trial
-    def checkReachCapsIsolated(tpe: Type, pos: SrcPos)(using Context): Unit =
+    private def checkReachCapsIsolated(tpe: Type, pos: SrcPos)(using Context): Unit =
 
         object checker extends TypeTraverser:
             var refVariances: Map[Boolean, Int] = Map.empty
@@ -854,7 +854,8 @@ class CheckCaptures extends Recheck, SymTransformer:
           tree.tpe
         finally curEnv = saved
       if tree.isTerm then
-        checkReachCapsIsolated(res.widen, tree.srcPos)
+        if !ccConfig.useExistentials then
+          checkReachCapsIsolated(res.widen, tree.srcPos)
         if !pt.isBoxedCapturing then
           markFree(res.boxedCaptureSet, tree.srcPos)
       res

tests/neg-custom-args/captures/unsound-reach.check

@@ -1,8 +1,3 @@
--- Error: tests/neg-custom-args/captures/unsound-reach.scala:18:13 -----------------------------------------------------
-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
 -- [E164] Declaration Error: tests/neg-custom-args/captures/unsound-reach.scala:10:8 -----------------------------------
 10 |    def use(x: File^)(op: File^ => Unit): Unit = op(x) // error, was OK using sealed checking
    |        ^

tests/neg-custom-args/captures/unsound-reach.scala

@@ -15,6 +15,6 @@ def bad(): Unit =
 
     var escaped: File^{backdoor*} = null
     withFile("hello.txt"): f =>
-        boom.use(f): (f1: File^{backdoor*}) => // error
+        boom.use(f): (f1: File^{backdoor*}) => // was error before existentials
             escaped = f1
 

tests/neg-custom-args/captures/widen-reach.check

@@ -0,0 +1,14 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/widen-reach.scala:13:26 ----------------------------------
+13 |  val y2: IO^ -> IO^ = y1.foo      // error
+   |                       ^^^^^^
+   |                       Found:    IO^ ->{x*} IO^{x*}
+   |                       Required: IO^ -> (ex$6: caps.Exists) -> IO^{ex$6}
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/widen-reach.scala:14:30 ----------------------------------
+14 |  val y3: IO^ -> IO^{x*} = y1.foo  // error
+   |                           ^^^^^^
+   |                           Found:    IO^ ->{x*} IO^{x*}
+   |                           Required: IO^ -> IO^{x*}
+   |
+   | longer explanation available when compiling with `-explain`

tests/neg-custom-args/captures/widen-reach.scala

@@ -0,0 +1,14 @@
+import language.experimental.captureChecking
+
+trait IO
+
+trait Foo[+T]:
+  val foo: IO^ -> T
+
+trait Bar extends Foo[IO^]:
+  val foo: IO^ -> IO^ = x => x
+
+def test(x: Foo[IO^]): Unit =
+  val y1: Foo[IO^{x*}] = x
+  val y2: IO^ -> IO^ = y1.foo      // error
+  val y3: IO^ -> IO^{x*} = y1.foo  // error

tests/neg/i20503.scala

@@ -9,8 +9,8 @@ class List[+A]:
 
 def runOps(ops: List[() => Unit]): Unit =
   // See i20156, due to limitation in expressiveness of current system,
-  // we cannot map over the list of impure elements.
-  ops.foreach(op => op()) // error
+  // we could map over the list of impure elements. OK with existentials.
+  ops.foreach(op => op())
 
 def main(): Unit =
   val f: List[() => Unit] -> Unit = runOps  // error