Don't flag local fresh capabilities as errors in markFree

Author: odersky

Diff for: compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala

@@ -486,9 +486,15 @@ class CheckCaptures extends Recheck, SymTransformer:
             // The path-use.scala neg test contains an example.
             val underlying = CaptureSet.ofTypeDeeply(c1.widen)
             capt.println(i"Widen reach $c to $underlying in ${env.owner}")
-            underlying.disallowRootCapability: () =>
-              report.error(em"Local reach capability $c leaks into capture scope of ${env.ownerString}", tree.srcPos)
-            recur(underlying, env, null)
+            if ccConfig.useSepChecks then
+              recur(underlying.filter(!_.isMaxCapability), env, null)
+                // we don't want to disallow underlying Fresh.Cap, since these are typically locally created
+                // fresh capabilities. We don't need to also follow the hidden set since separation
+                // checking makes ure that locally hidden references need to go to @consume parameters.
+            else
+              underlying.disallowRootCapability: () =>
+                report.error(em"Local reach capability $c leaks into capture scope of ${env.ownerString}", tree.srcPos)
+              recur(underlying, env, null)
         case c: TypeRef if c.isParamPath =>
           checkUseDeclared(c, env, null)
         case _ =>

Diff for: tests/neg-custom-args/captures/delayedRunops.check

@@ -3,10 +3,6 @@
    |             ^^^^
    |             reference ops* is not included in the allowed capture set {}
    |             of an enclosing function literal with expected type () -> Unit
--- Error: tests/neg-custom-args/captures/delayedRunops.scala:23:13 -----------------------------------------------------
-23 |      runOps(ops1)  // error
-   |             ^^^^
-   |             Local reach capability ops1* leaks into capture scope of enclosing function
 -- Error: tests/neg-custom-args/captures/delayedRunops.scala:29:13 -----------------------------------------------------
 29 |      runOps(ops1)  // error
    |             ^^^^

Diff for: tests/neg-custom-args/captures/delayedRunops.scala

@@ -20,7 +20,7 @@ import caps.{use, consume}
   def delayedRunOps2(@consume ops: List[() => Unit]): () ->{} Unit =
     () =>
       val ops1: List[() => Unit] = ops // error
-      runOps(ops1)  // error
+      runOps(ops1)  // was error
 
   // unsound: impure operation pretended pure
   def delayedRunOps3(ops: List[() => Unit]): () ->{} Unit =

Diff for: tests/neg-custom-args/captures/i21401.check

@@ -23,7 +23,3 @@
    |                                         ^^^^^^^^^^^^^^^^^^^^^^^^
    |Type variable X of value leaked cannot be instantiated to Boxed[box IO^] -> (ex$20: caps.Exists) -> Boxed[box IO^{ex$20}] since
    |the part box IO^{ex$20} of that type captures the root capability `cap`.
--- Error: tests/neg-custom-args/captures/i21401.scala:18:21 ------------------------------------------------------------
-18 |  val y: IO^{x*} = x.unbox // error
-   |                   ^^^^^^^
-   |                   Local reach capability x* leaks into capture scope of method test2

Diff for: tests/neg-custom-args/captures/i21401.scala

@@ -15,5 +15,5 @@ def test2() =
   val a = usingIO[IO^](x => x) // error
   val leaked: [R, X <: Boxed[IO^] -> R] -> (op: X) -> R = usingIO[Res](mkRes) // error
   val x: Boxed[IO^] = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x) // error // error
-  val y: IO^{x*} = x.unbox // error
+  val y: IO^{x*} = x.unbox // was error
   y.println("boom")

Diff for: tests/neg-custom-args/captures/i21442.check

@@ -3,10 +3,6 @@
    |           ^^^^^^^
    |           Local reach capability x* leaks into capture scope of method foo.
    |           To allow this, the parameter x should be declared with a @use annotation
--- Error: tests/neg-custom-args/captures/i21442.scala:18:14 ------------------------------------------------------------
-18 |  val io = x1.unbox // error
-   |           ^^^^^^^^
-   |           Local reach capability x1* leaks into capture scope of method bar
 -- Error: tests/neg-custom-args/captures/i21442.scala:17:10 ------------------------------------------------------------
 17 |  val x1: Boxed[IO^] = x // error
    |          ^^^^^^^^^^

Diff for: tests/neg-custom-args/captures/i21442.scala

@@ -15,5 +15,5 @@ def foo(x: Boxed[IO^]): Unit =
 // But, no type error reported.
 def bar(x: Boxed[IO^]): Unit =
   val x1: Boxed[IO^] = x // error
-  val io = x1.unbox // error
+  val io = x1.unbox // was error
   io.use()

Diff for: tests/neg-custom-args/captures/leak-problem.scala

@@ -25,7 +25,7 @@ def test(): Unit =
   def useBoxedAsync1(@use x: Box[Async^]): Unit = x.get.read()
 
   val xs: Box[Async^] = ???
-  val xsLambda = () => useBoxedAsync(xs) // error
+  val xsLambda = () => useBoxedAsync(xs) // was error now ok
   val _: () ->{xs*} Unit = xsLambda
   val _: () -> Unit = xsLambda // error
 

Diff for: tests/neg-custom-args/captures/path-use.check

@@ -44,10 +44,6 @@
    |                                                   ^
    |                                Type variable A of constructor Id cannot be instantiated to box () => Unit since
    |                                that type captures the root capability `cap`.
--- Error: tests/neg-custom-args/captures/reaches.scala:56:6 ------------------------------------------------------------
-56 |    id(() => f.write()) // error
-   |    ^^^^^^^^^^^^^^^^^^^
-   |    Local reach capability id* leaks into capture scope of method test
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:63:27 --------------------------------------
 63 |    val f1: File^{id*} = id(f) // error, since now id(f): File^ // error
    |                         ^^^^^

Diff for: tests/neg-custom-args/captures/path-use.scala

@@ -53,7 +53,7 @@ class Id[-A,  +B >: A]():
 def test =
   val id: Id[Proc, Proc] = new Id[Proc, () -> Unit] // error
   usingFile: f =>
-    id(() => f.write()) // error
+    id(() => f.write()) // was error
 
 def attack2 =
   val id: File^ -> File^ = x => x

Diff for: tests/neg-custom-args/captures/reaches.check

@@ -10,10 +10,6 @@
    |                             Required: Foo[box File^]
    |
    | longer explanation available when compiling with `-explain`
--- Error: tests/neg-custom-args/captures/unsound-reach-4.scala:25:22 ---------------------------------------------------
-25 |    escaped = boom.use(f)  // error
-   |              ^^^^^^^^^^^
-   |              Local reach capability backdoor* leaks into capture scope of method bad
 -- [E164] Declaration Error: tests/neg-custom-args/captures/unsound-reach-4.scala:17:6 ---------------------------------
 17 |  def use(@consume x: F): File^ = x // error @consume override
    |      ^

Diff for: tests/neg-custom-args/captures/reaches.scala

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

Diff for: tests/neg-custom-args/captures/unsound-reach-4.check

@@ -15,8 +15,3 @@
    |                               Required: Foo[box File^]
    |
    | longer explanation available when compiling with `-explain`
--- Error: tests/neg-custom-args/captures/unsound-reach.scala:23:21 -----------------------------------------------------
-23 |        boom.use(f): (f1: File^{backdoor*}) => // error
-   |                     ^
-   |                     Local reach capability backdoor* leaks into capture scope of method bad
-24 |            escaped = f1

Diff for: tests/neg-custom-args/captures/unsound-reach-4.scala

@@ -20,6 +20,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
             escaped = f1
 

Diff for: tests/neg-custom-args/captures/unsound-reach.check

@@ -0,0 +1,28 @@
+import caps.Mutable
+import caps.cap
+
+class Ref extends Mutable:
+  var x = 0
+  def get: Int = x
+  mut def put(y: Int): Unit = x = y
+
+case class Pair[+X, +Y](val fst: X, val snd: Y)
+
+def twoRefs(): Pair[Ref^, Ref^] =
+  val r1 = Ref()
+  val r2 = Ref()
+  Pair(r1, r2)
+
+def twoRefsBad(): Pair[Ref^, Ref^] =
+  Pair(Ref(), Ref()) // error: universal capability cannot be included in capture set
+                     // even though this is morally equivalent to `twoRefs`
+
+
+def test(io: Object^): Unit =
+  val two = twoRefs()
+  val fst = two.fst // error: local reach capability two* leaks into test
+                    // first, the leakage makes no sense
+                    // second, the capture should be two.fst, not two*
+  val snd = two.snd
+  val three: Pair[Ref^{io}, Ref^{io}] = ???
+  val bad = three.fst

Diff for: tests/neg-custom-args/captures/unsound-reach.scala

@@ -1,5 +1,4 @@
 import language.experimental.namedTuples
-import caps.use
 
 class IO
 
@@ -9,14 +8,18 @@ class C(val f: IO^):
 type Proc = () => Unit
 
 def test(io: IO^) =
-  def test1(@use c: C { val f: IO^{io}}^{io}) =
-    val f = () => println(c.f)
-    val _: () ->{c.f} Unit = f
+  val c = C(io)
+  val f = () => println(c.f)
+  val _: () ->{c.f} Unit = f
 
-    val x = c.procs
-    val _: List[() ->{c.procs*} Unit] = x
+  val x = c.procs
+  val _: List[() ->{c.procs*} Unit] = x
 
-    val g = () => println(c.procs.head)
-    val _: () ->{c.procs*} Unit = g
-  test1(C(io))
+  val g = () => println(c.procs.head) // was error, local reach capability c.procs* leaks
+  val _: () ->{c.procs*} Unit = g
 
+  val cc: C { val f: IO^{io}; val procs: List[() ->{io} Unit] }^{io} =
+    ???
+
+  val gg = () => println(cc.procs.head) // OK, since cc.procs* has {io} as underlying capture set
+  val _: () ->{io} Unit = gg