Fix special capture set handling in recheckApply, Step 2 revised

odersky · odersky · commit 7db1d43518f6 · 2024-07-17T17:58:51.000+02:00
Step 2: Change the logic. The previous one was unsound. The new logic is makes use of the
distinction between regular and unboxed parameters.
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -547,36 +547,47 @@ class CheckCaptures extends Recheck, SymTransformer:
     protected override
     def recheckArg(arg: Tree, formal: Type)(using Context): Type =
       val argType = recheck(arg, formal)
-      if unboxedArgs.remove(arg) && ccConfig.useUnboxedParams then
+      if unboxedArgs.contains(arg) && ccConfig.useUnboxedParams then
         capt.println(i"charging deep capture set of $arg: ${argType} = ${CaptureSet.deepCaptureSet(argType)}")
         markFree(CaptureSet.deepCaptureSet(argType), arg.srcPos)
       argType
 
     /** A specialized implementation of the apply rule.
      *
-     *  E |- f: Ra ->Cf Rr^Cr
-     *  E |- a: Ra^Ca
+     *  E |- q: Tq^Cq
+     *  E |- q.f: Ta^Ca ->Cf Tr^Cr
+     *  E |- a: Ta
      *  ---------------------
-     *  E |- f a: Rr^C
+     *  E |- f(a): Tr^C
      *
-     *  The implementation picks as `C` one of `{f, a}` or `Cr`, depending on the
-     *  outcome of a `mightSubcapture` test. It picks `{f, a}` if this might subcapture Cr
-     *  and Cr otherwise.
+     *  If the function `f` does not have an `@unboxed` parameter, then
+     *  any unboxing it does would be charged to the environment of the function
+     *  so they have to appear in Cq. Since any capabilities of the result of the
+     *  application must already be present in the application, an upper
+     *  approximation of the result capture set is Cq \union Ca, where `Ca`
+     *  is the capture set of the argument.
+     *  If the function `f` does have an `@unboxed` parameter, then it could in addition
+     *  unbox reach capabilities over its formal parameter. Therefore, the approximation
+     *  would be `Cq \union dcs(Ca)` instead.
+     *  If the approximation is known to subcapture the declared result Cr, we pick it for C
+     *  otherwise we pick Cr.
      */
     protected override
     def recheckApplication(tree: Apply, qualType: Type, funType: MethodType, argTypes: List[Type])(using Context): Type =
-      Existential.toCap(super.recheckApplication(tree, qualType, funType, argTypes)) match
+      val appType = Existential.toCap(super.recheckApplication(tree, qualType, funType, argTypes))
+      val qualCaptures = qualType.captureSet
+      val argCaptures =
+        for (arg, argType) <- tree.args.lazyZip(argTypes) yield
+          if unboxedArgs.remove(arg) // need to ensure the remove happens, that's why argCaptures is computed even if not needed.
+          then CaptureSet.deepCaptureSet(argType)
+          else argType.captureSet
+      appType match
         case appType @ CapturingType(appType1, refs)
         if qualType.exists
             && !tree.fun.symbol.isConstructor
-            && !qualType.isBoxedCapturing // TODO: This is not strng enough, we also have
-                 // to exclude existentials in function results
-            && !argTypes.exists(_.isBoxedCapturing)
-            && qualType.captureSet.mightSubcapture(refs)
-            && argTypes.forall(_.captureSet.mightSubcapture(refs))
-        =>
-          val callCaptures = tree.args.foldLeft(qualType.captureSet): (cs, arg) =>
-              cs ++ arg.tpe.captureSet
+            && qualCaptures.mightSubcapture(refs)
+            && argCaptures.forall(_.mightSubcapture(refs)) =>
+          val callCaptures = argCaptures.foldLeft(qualCaptures)(_ ++ _)
           appType.derivedCapturingType(appType1, callCaptures)
             .showing(i"narrow $tree: $appType, refs = $refs, qual-cs = ${qualType.captureSet} = $result", capt)
         case appType =>
diff --git a/tests/neg-custom-args/captures/reaches.check b/tests/neg-custom-args/captures/reaches.check
@@ -1,12 +1,12 @@
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:24:11 --------------------------------------
-24 |    cur = (() => f.write()) :: Nil // error since {f*} !<: {xs*}
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:22:11 --------------------------------------
+22 |    cur = (() => f.write()) :: Nil // error
    |           ^^^^^^^^^^^^^^^^^^^^^^^
    |           Found:    List[box () ->{f} Unit]
    |           Required: List[box () ->{xs*} Unit]
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:35:7 ---------------------------------------
-35 |      (() => f.write()) :: Nil // error since {f*} !<: {xs*}
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:33:7 ---------------------------------------
+33 |      (() => f.write()) :: Nil // error
    |       ^^^^^^^^^^^^^^^^^^^^^^^
    |       Found:    List[box () ->{f} Unit]
    |       Required: box List[box () ->{xs*} Unit]^?
@@ -15,52 +15,34 @@
    |       cannot be included in outer capture set {xs*} of value cur
    |
    | longer explanation available when compiling with `-explain`
--- Error: tests/neg-custom-args/captures/reaches.scala:38:6 ------------------------------------------------------------
-38 |  var cur: List[Proc] = xs // error: Illegal type for var
-   |      ^
-   |      Mutable variable cur cannot have type List[box () => Unit] since
-   |      the part box () => Unit of that type captures the root capability `cap`.
--- Error: tests/neg-custom-args/captures/reaches.scala:45:15 -----------------------------------------------------------
-45 |  val cur = Ref[List[Proc]](xs) // error: illegal type for type argument to Ref
-   |            ^^^^^^^^^^^^^^^
-   |            Sealed type variable T cannot be instantiated to List[box () => Unit] since
-   |            the part box () => Unit of that type captures the root capability `cap`.
-   |            This is often caused by a local capability in an argument of constructor Ref
-   |            leaking as part of its result.
--- Error: tests/neg-custom-args/captures/reaches.scala:55:31 -----------------------------------------------------------
-55 |  val id: Id[Proc, Proc] = new Id[Proc, () -> Unit] // error
-   |                               ^^^^^^^^^^^^^^^^^^^^
-   |                               Sealed type variable A cannot be instantiated to box () => Unit since
-   |                               that type captures the root capability `cap`.
-   |                               This is often caused by a local capability in an argument of constructor Id
-   |                               leaking as part of its result.
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:57:6 ---------------------------------------
-57 |    id(() => f.write())  // error
-   |    ^^^^^^^^^^^^^^^^^^^
-   |    Found:    () => Unit
-   |    Required: () ->? Unit
-   |
-   |    Note that the universal capability `cap`
-   |    cannot be included in capture set ?
-   |
-   | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:64:27 --------------------------------------
-64 |    val f1: File^{id*} = id(f) // error, since now id(f): File^
+-- Error: tests/neg-custom-args/captures/reaches.scala:38:31 -----------------------------------------------------------
+38 |    val next: () => Unit = cur.head // error
+   |                           ^^^^^^^^
+   |                       The expression's type box () => Unit is not allowed to capture the root capability `cap`.
+   |                       This usually means that a capability persists longer than its allowed lifetime.
+-- Error: tests/neg-custom-args/captures/reaches.scala:45:35 -----------------------------------------------------------
+45 |    val next: () => Unit = cur.get.head // error
+   |                           ^^^^^^^^^^^^
+   |                       The expression's type box () => Unit is not allowed to capture the root capability `cap`.
+   |                       This usually means that a capability persists longer than its allowed lifetime.
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:62:27 --------------------------------------
+62 |    val f1: File^{id*} = id(f) // error, since now id(f): File^
    |                         ^^^^^
-   |                         Found:    File^{id, f}
+   |                         Found:    File^{f}
    |                         Required: File^{id*}
    |
    | longer explanation available when compiling with `-explain`
--- Error: tests/neg-custom-args/captures/reaches.scala:81:5 ------------------------------------------------------------
-81 |  ps.map((x, y) => compose1(x, y)) // error: cannot mix cap and * (should work now) // error // error
-   |  ^^^^^^
-   |  Reach capability cap and universal capability cap cannot both
-   |  appear in the type [B](f: ((box A ->{ps*} A, box A ->{ps*} A)) => B): List[B] of this expression
--- Error: tests/neg-custom-args/captures/reaches.scala:81:10 -----------------------------------------------------------
-81 |  ps.map((x, y) => compose1(x, y)) // error: cannot mix cap and * (should work now) // error // error
+-- Error: tests/neg-custom-args/captures/reaches.scala:79:10 -----------------------------------------------------------
+79 |  ps.map((x, y) => compose1(x, y)) // error // error
    |          ^
    |          Local reach capability ps* leaks into capture scope of method mapCompose
--- Error: tests/neg-custom-args/captures/reaches.scala:81:13 -----------------------------------------------------------
-81 |  ps.map((x, y) => compose1(x, y)) // error: cannot mix cap and * (should work now) // error // error
+-- Error: tests/neg-custom-args/captures/reaches.scala:79:13 -----------------------------------------------------------
+79 |  ps.map((x, y) => compose1(x, y)) // error // error
    |             ^
    |             Local reach capability ps* leaks into capture scope of method mapCompose
+-- [E057] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:53:51 --------------------------------------
+53 |  val id: Id[Proc, Proc] = new Id[Proc, () -> Unit] // error
+   |                                                   ^
+   |                                             Type argument () -> Unit does not conform to lower bound () => Unit
+   |
+   | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/reaches.scala b/tests/neg-custom-args/captures/reaches.scala
@@ -1,5 +1,3 @@
-//> using options -source 3.4
-// (to make sure we use the sealed policy)
 import caps.unboxed
 class File:
   def write(): Unit = ???
@@ -14,14 +12,14 @@ class Ref[T](init: T):
   def set(y: T) = { x = y }
 
 def runAll0(@unboxed xs: List[Proc]): Unit =
-  var cur: List[() ->{xs*} Unit] = xs  // OK, by revised VAR
+  var cur: List[() ->{xs*} Unit] = xs
   while cur.nonEmpty do
     val next: () ->{xs*} Unit = cur.head
     next()
     cur = cur.tail: List[() ->{xs*} Unit]
 
   usingFile: f =>
-    cur = (() => f.write()) :: Nil // error since {f*} !<: {xs*}
+    cur = (() => f.write()) :: Nil // error
 
 def runAll1(@unboxed xs: List[Proc]): Unit =
   val cur = Ref[List[() ->{xs*} Unit]](xs)  // OK, by revised VAR
@@ -32,19 +30,19 @@ def runAll1(@unboxed xs: List[Proc]): Unit =
 
   usingFile: f =>
     cur.set:
-      (() => f.write()) :: Nil // error since {f*} !<: {xs*}
+      (() => f.write()) :: Nil // error
 
 def runAll2(xs: List[Proc]): Unit =
-  var cur: List[Proc] = xs // error: Illegal type for var
+  var cur: List[Proc] = xs
   while cur.nonEmpty do
-    val next: () => Unit = cur.head
+    val next: () => Unit = cur.head // error
     next()
     cur = cur.tail
 
 def runAll3(xs: List[Proc]): Unit =
-  val cur = Ref[List[Proc]](xs) // error: illegal type for type argument to Ref
+  val cur = Ref[List[Proc]](xs)
   while cur.get.nonEmpty do
-    val next: () => Unit = cur.get.head
+    val next: () => Unit = cur.get.head // error
     next()
     cur.set(cur.get.tail: List[Proc])
 
@@ -54,7 +52,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())
 
 def attack2 =
   val id: File^ -> File^ = x => x
@@ -78,4 +76,7 @@ def compose1[A, B, C](f: A => B, g: B => C): A ->{f, g} C =
   z => g(f(z))
 
 def mapCompose[A](ps: List[(A => A, A => A)]): List[A ->{ps*} A] =
-  ps.map((x, y) => compose1(x, y)) // error: cannot mix cap and * (should work now) // error // error
+  ps.map((x, y) => compose1(x, y)) // error // error
+
+def mapCompose2[A](@unboxed ps: List[(A => A, A => A)]): List[A ->{ps*} A] =
+  ps.map((x, y) => compose1(x, y))
diff --git a/tests/pos-custom-args/captures/Buffer.scala b/tests/pos-custom-args/captures/Buffer.scala
@@ -0,0 +1,22 @@
+import language.experimental.captureChecking
+
+// Extract of the problem in collection.mutable.Buffers
+trait Buffer[A]:
+
+  def apply(i: Int): A = ???
+
+  def flatMapInPlace(f: A => IterableOnce[A]^): this.type = {
+    val g = f
+    val s = 10
+     // capture checking: we need the copy since we box/unbox on g* on the next line
+      // TODO: This looks fishy, need to investigate
+      // Alternative would be to mark `f` as @unboxed. It's not inferred
+      // since `^ appears in a function result, not under a box.
+    val newElems = new Array[(IterableOnce[A]^{f})](s)
+    var i = 0
+    while i < s do
+      val x = g(this(i))
+      newElems(i) = x
+      i += 1
+    this
+  }
diff --git a/tests/pos-custom-args/captures/opaque-inline-problem.scala b/tests/pos-custom-args/captures/opaque-inline-problem.scala
@@ -4,9 +4,8 @@ trait Async extends caps.Capability:
 object Async:
   inline def current(using async: Async): async.type = async
   opaque type Spawn <: Async = Async
-  def blocking[T](f: Spawn => T): T = ???
+  def blocking[T](f: Spawn ?=> T): T = ???
 
 def main() =
-  Async.blocking: spawn =>
-    val c = Async.current(using spawn)
-    val a = c.group
+  Async.blocking:
+    val a = Async.current.group
