Fix special capture set handling in recheckApply, Step 2

Step 2: Change the logic. The previous one was unsound. The new logic is a bot too
conservative. I left comments in tests where it could be improved.

Author: odersky

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

@@ -554,30 +554,26 @@ class CheckCaptures extends Recheck, SymTransformer:
 
     /** 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 ->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.
+     *  The implementation picks `C` as `Cq` instead of `Cr`, if
+     *   1. The argument(s) Ta are always pure
+     *   2. `Cq` might subcapture `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
         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)
+            && argTypes.forall(_.isAlwaysPure)
             && qualType.captureSet.mightSubcapture(refs)
-            && argTypes.forall(_.captureSet.mightSubcapture(refs))
         =>
-          val callCaptures = tree.args.foldLeft(qualType.captureSet): (cs, arg) =>
-              cs ++ arg.tpe.captureSet
-          appType.derivedCapturingType(appType1, callCaptures)
+          appType.derivedCapturingType(appType1, qualType.captureSet)
             .showing(i"narrow $tree: $appType, refs = $refs, qual-cs = ${qualType.captureSet} = $result", capt)
         case appType =>
           appType

scala2-library-cc/src/scala/collection/Iterator.scala

@@ -17,7 +17,7 @@ import scala.annotation.tailrec
 import scala.annotation.unchecked.uncheckedVariance
 import scala.runtime.Statics
 import language.experimental.captureChecking
-
+import caps.unsafe.unsafeAssumePure
 
 /** Iterators are data structures that allow to iterate over a sequence
   * of elements. They have a `hasNext` method for checking
@@ -595,7 +595,8 @@ trait Iterator[+A] extends IterableOnce[A] with IterableOnceOps[A, Iterator, Ite
 
     private[this] def nextCur(): Unit = {
       cur = null
-      cur = f(self.next()).iterator
+      cur = f(self.next()).iterator.unsafeAssumePure
+        // !!! see explanation in colltest5.CollectionStrawManCC5_1.flatMap why the unsafeAssumePure is needed
       _hasNext = -1
     }
 

scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala

@@ -25,6 +25,7 @@ import scala.runtime.Statics
 import language.experimental.captureChecking
 import annotation.unchecked.uncheckedCaptures
 import caps.untrackedCaptures
+import caps.unsafe.unsafeAssumePure
 
 /**  This class implements an immutable linked list. We call it "lazy"
   *  because it computes its elements only when they are needed.
@@ -1041,7 +1042,8 @@ object LazyListIterable extends IterableFactory[LazyListIterable] {
       var itHasNext       = false
       var rest            = restRef           // var rest = restRef.elem
       while (!itHasNext && !rest.isEmpty) {
-        it        = f(rest.head).iterator
+        it        = f(rest.head).iterator.unsafeAssumePure
+          // !!! see explanation in colltest5.CollectionStrawManCC5_1.flatMap why the unsafeAssumePure is needed
         itHasNext = it.hasNext
         if (!itHasNext) {                     // wait to advance `rest` because `it.next()` can throw
           rest    = rest.tail

scala2-library-cc/src/scala/collection/mutable/Buffer.scala

@@ -16,6 +16,7 @@ package mutable
 import scala.annotation.nowarn
 import language.experimental.captureChecking
 import caps.unboxed
+import caps.unsafe.unsafeAssumePure
 
 /** A `Buffer` is a growable and shrinkable `Seq`. */
 trait Buffer[A]
@@ -185,7 +186,10 @@ trait IndexedBuffer[A] extends IndexedSeq[A]
     var i = 0
     val s = size
     val newElems = new Array[(IterableOnce[A]^{f*})](s)
-    while (i < s) { newElems(i) = f(this(i)); i += 1 }
+    while i < s do
+      newElems(i) = f(this(i)).unsafeAssumePure
+        // !!! see explanation in colltest5.CollectionStrawManCC5_1.flatMap why the unsafeAssumePure is needed
+      i += 1
     clear()
     i = 0
     while (i < s) { ++=(newElems(i)); i += 1 }

tests/neg-custom-args/captures/reaches.check

@@ -47,7 +47,7 @@
 -- [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^
    |                         ^^^^^
-   |                         Found:    File^{id, f}
+   |                         Found:    File^
    |                         Required: File^{id*}
    |
    | longer explanation available when compiling with `-explain`

tests/pos-custom-args/captures/nested-classes-2.scala

@@ -20,5 +20,5 @@ def test2(x1: (() => Unit), x2: (() => Unit) => Unit) =
   def test3(y1: (() => Unit), y2: (() => Unit) => Unit) =
     val cc1: C1^{y1, y2} = C1(y1, y2)
     val cc2 = cc1.c2(x1, x2)
-    val cc3: cc1.C2^{cc1, x1, x2} = cc2
+    val cc3: cc1.C2^{cc2} = cc2
 

tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala

@@ -5,6 +5,7 @@ import Predef.{augmentString as _, wrapString as _, *}
 import scala.reflect.ClassTag
 import annotation.unchecked.{uncheckedVariance, uncheckedCaptures}
 import annotation.tailrec
+import caps.unsafe.unsafeAssumePure
 
 /** A strawman architecture for new collections. It contains some
  *  example collection classes and methods with the intent to expose
@@ -555,7 +556,16 @@ object CollectionStrawMan5 {
       private var myCurrent: Iterator[B]^{this, f} = Iterator.empty
       private def current = {
         while (!myCurrent.hasNext && self.hasNext)
-          myCurrent = f(self.next()).iterator
+          myCurrent = f(self.next()).iterator.unsafeAssumePure
+            // !!! This is unsafe since the iterator's result could return a capability
+            // depending on the argument self.next() of type A. To exclude that we'd have
+            // to define f to be of type EX c. A ->{c} IterableOnce[B]^{c}, i.e. `c` may
+            // not depend on A. But to get there we have to
+            //  - improve the way we express existentials using `^`
+            //  - rework the recheckApplication code to cater for this. Right now
+            //    we cannot do anything since `A` is not always pure. But if we took
+            //    the existential scope of the result into account, this could provide
+            //    a solution.
         myCurrent
       }
       def hasNext = current.hasNext