By default don't include span captures in the underlying capset

What is the underlying capture set of a function? CC says the capture set
on the first arrow but we experimented with the capture of the span of the
function instead. This however causes a lot of complications if we want to push
it to a logical conclusion. So we now make it configurable and by default
span capture set is not used.

Author: odersky

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

@@ -1565,7 +1565,7 @@ object CaptureSet:
       // `ref` will not seem subsumed by other capabilities in a `++`.
       universal
     case c: CoreCapability =>
-      ofType(c.underlying, followResult = true)
+      ofType(c.underlying, followResult = ccConfig.useSpanCapset)
 
   /** Capture set of a type
    *  @param followResult  If true, also include capture sets of function results.

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

@@ -496,7 +496,7 @@ class CheckCaptures extends Recheck, SymTransformer:
             case _ => c.core match
               case c1: RootCapability => c1.singletonCaptureSet
               case c1: CoreCapability =>
-                CaptureSet.ofType(c1.widen, followResult = true)
+                CaptureSet.ofType(c1.widen, followResult = ccConfig.useSpanCapset)
           capt.println(i"Widen reach $c to $underlying in ${env.owner}")
           underlying.disallowBadRoots(NoSymbol): () =>
             report.error(em"Local capability $c${env.owner.qualString("in")} cannot have `cap` as underlying capture set", tree.srcPos)

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

@@ -43,6 +43,11 @@ object ccConfig:
    */
   inline val postCheckCapturesets = false
 
+  /** If true take as the underlying capture set of a capability of function type
+   *  the capture set along the span, including capture sets of function results.
+   */
+  inline val useSpanCapset = false
+
   /** If true, do level checking for FreshCap instances */
   def useFreshLevels(using Context): Boolean =
     Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.7`)

library/src/scala/collection/Iterator.scala

@@ -9,7 +9,6 @@
  * See the NOTICE file distributed with this work for
  * additional information regarding copyright ownership.
  */
-
 package scala.collection
 
 import scala.language.`2.13`

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

@@ -7,12 +7,3 @@
   |         Note that capability f is not included in capture set {}.
   |
   | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/eta.scala:7:7 --------------------------------------------
-7 |       () => { stowaway.apply().apply() }  // error (was ok)
-  |       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-  |       Found:    () ->{stowaway} Unit
-  |       Required: () -> Unit
-  |
-  |       Note that capability stowaway is not included in capture set {}.
-  |
-  | longer explanation available when compiling with `-explain`

tests/neg-custom-args/captures/eta.scala

@@ -4,4 +4,4 @@
          g  // error
        val stowaway: () -> Proc^{f} =
          bar( () => f )  // was error now OK
-       () => { stowaway.apply().apply() }  // error (was ok)
+       () => { stowaway.apply().apply() }

tests/neg-custom-args/captures/scoped-caps.check

@@ -49,14 +49,17 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:12:20 ----------------------------------
 12 |  val _: A^ -> B^ = x => g(x)      // error: g is no longer pure, since it contains the ^ of B
    |                    ^^^^^^^^^
-   |                    Found:    (x: A^) ->{g} B^²
+   |                    Found:    (x: A^) ->'s1 B^²
    |                    Required: A^ -> B^³
    |
-   |                    Note that capability g is not included in capture set {}.
+   |                    Note that capability cap is not included in capture set {cap²}
+   |                    because cap is not visible from cap² in value _$5.
    |
-   |                    where:    ^  refers to the universal root capability
-   |                              ^² refers to a root capability associated with the result type of (x: A^): B^²
-   |                              ^³ refers to a fresh root capability in the type of value _$5
+   |                    where:    ^    refers to the universal root capability
+   |                              ^²   refers to a root capability associated with the result type of (x: A^): B^²
+   |                              ^³   refers to a fresh root capability in the type of value _$5
+   |                              cap  is a root capability associated with the result type of (x: A^): B^²
+   |                              cap² is a fresh root capability in the type of value _$5
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:16:24 ----------------------------------
@@ -75,61 +78,35 @@
    |                                 cap is a root capability associated with the result type of (x: S^): B^²
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:17:24 ----------------------------------
-17 |  val _: (x: S) -> B^ = (x: S) => h(x)  // error: eta expansion fails
-   |                        ^^^^^^^^^^^^^^
-   |                        Found:    (x: S^) ->{h} B^²
-   |                        Required: (x: S^) -> B^³
-   |
-   |                        Note that capability h is not included in capture set {}.
-   |
-   |                        where:    ^  refers to the universal root capability
-   |                                  ^² refers to a root capability associated with the result type of (x: S^): B^²
-   |                                  ^³ refers to a root capability associated with the result type of (x: S^): B^³
-   |
-   | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:21:23 ----------------------------------
-21 |  val _: (x: S) -> S = (x: S) => h2(x)  // error: eta conversion fails since `h2` is now impure (result type S is a capability)
-   |                       ^^^^^^^^^^^^^^^
-   |                       Found:    (x: S^) ->{h2} S^²
-   |                       Required: (x: S^) -> S^³
-   |
-   |                       Note that capability h2 is not included in capture set {}.
-   |
-   |                       where:    ^  refers to the universal root capability
-   |                                 ^² refers to a root capability associated with the result type of (x: S^): S^²
-   |                                 ^³ refers to a root capability associated with the result type of (x: S^): S^³
-   |
-   | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:27:19 ----------------------------------
-27 |  val _: S -> B^ = j               // error
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:26:19 ----------------------------------
+26 |  val _: S -> B^ = j               // error
    |                   ^
    |                   Found:    (j : (x: S) -> B^)
    |                   Required: S^² -> B^³
    |
    |                   Note that capability cap is not included in capture set {cap²}
-   |                   because cap is not visible from cap² in value _$14.
+   |                   because cap is not visible from cap² in value _$13.
    |
    |                   where:    ^    refers to a root capability associated with the result type of (x: S^²): B^
    |                             ^²   refers to the universal root capability
-   |                             ^³   refers to a fresh root capability in the type of value _$14
+   |                             ^³   refers to a fresh root capability in the type of value _$13
    |                             cap  is a root capability associated with the result type of (x: S^²): B^
-   |                             cap² is a fresh root capability in the type of value _$14
+   |                             cap² is a fresh root capability in the type of value _$13
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:28:19 ----------------------------------
-28 |  val _: S -> B^ = x => j(x)       // error
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:27:19 ----------------------------------
+27 |  val _: S -> B^ = x => j(x)       // error
    |                   ^^^^^^^^^
-   |                   Found:    (x: S^) ->'s1 B^²
+   |                   Found:    (x: S^) ->'s2 B^²
    |                   Required: S^ -> B^³
    |
    |                   Note that capability cap is not included in capture set {cap²}
-   |                   because cap is not visible from cap² in value _$15.
+   |                   because cap is not visible from cap² in value _$14.
    |
    |                   where:    ^    refers to the universal root capability
    |                             ^²   refers to a root capability associated with the result type of (x: S^): B^²
-   |                             ^³   refers to a fresh root capability in the type of value _$15
+   |                             ^³   refers to a fresh root capability in the type of value _$14
    |                             cap  is a root capability associated with the result type of (x: S^): B^²
-   |                             cap² is a fresh root capability in the type of value _$15
+   |                             cap² is a fresh root capability in the type of value _$14
    |
    | longer explanation available when compiling with `-explain`

tests/neg-custom-args/captures/scoped-caps.scala

@@ -14,12 +14,11 @@ def test(io: Object^): Unit =
 
   val h: S -> B^ = ???
   val _: (x: S) -> B^ = h          // error: direct conversion fails
-  val _: (x: S) -> B^ = (x: S) => h(x)  // error: eta expansion fails
+  val _: (x: S) -> B^ = (x: S) => h(x)  // eta expansion is ok
 
   val h2: S -> S = ???
   val _: (x: S) -> S = h2               // direct conversion OK for shared S
-  val _: (x: S) -> S = (x: S) => h2(x)  // error: eta conversion fails since `h2` is now impure (result type S is a capability)
-  val _: (x: S) ->{h2} S = (x: S) => h2(x) // eta expansion OK
+  val _: (x: S) -> S = (x: S) => h2(x)  // eta conversion is also OK
 
   val j: (x: S) -> B^ = ???
   val _: (x: S) -> B^ = j

tests/neg-custom-args/captures/scoped-caps2.check

@@ -7,14 +7,15 @@
   |                   Note that the existential capture root in C^
   |                   cannot subsume the capability cap..
   |
-  |                   Note that capability cap is not included in capture set {cap²}.
+  |                   Note that capability cap² is not included in capture set {cap³}.
   |
   |                   where:    =>   refers to a fresh root capability in the type of value b
   |                             =>²  refers to a fresh root capability in the type of value _$1
   |                             ^    refers to the universal root capability
   |                             ^²   refers to a root capability associated with the result type of (x: C^): C^²
   |                             cap  is a fresh root capability classified as SharedCapability in the type of value b
   |                             cap² is a fresh root capability in the type of value b
+  |                             cap³ is a fresh root capability in the type of value _$1
   |
   | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps2.scala:6:18 ----------------------------------
@@ -65,19 +66,6 @@
    |                  cap² is a fresh root capability classified as SharedCapability in the type of value _$6
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps2.scala:15:23 ---------------------------------
-15 |  val _: (x: C) -> C = (x: C) => b(x) // error
-   |                       ^^^^^^^^^^^^^^
-   |                       Found:    (x: C^) ->{b} C^²
-   |                       Required: (x: C^) -> C^³
-   |
-   |                       Note that capability b is not included in capture set {}.
-   |
-   |                       where:    ^  refers to the universal root capability
-   |                                 ^² refers to a root capability associated with the result type of (x: C^): C^²
-   |                                 ^³ refers to a root capability associated with the result type of (x: C^): C^³
-   |
-   | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps2.scala:16:29 ---------------------------------
 16 |  val _: C -> C = (x: C) => a(x) // error
    |                            ^^^^

tests/neg-custom-args/captures/scoped-caps2.scala

@@ -4,14 +4,14 @@ def test1(c: C) =
   val b: C => C = ???
   val _: (x: C) => C = b // error
   val _: C => C = a // error
-  val _: (x: C) => C = (x: C) => b(x) // OK
+  val _: (x: C) => C = (x: C) => (b(x): C) // OK
   val _: C => C = (x: C) => a(x) // error
 
 def test2(c: C) =
   val a: (x: C) -> C = ???
   val b: C -> C = ???
   val _: (x: C) -> C = b // OK
   val _: C -> C = a // error
-  val _: (x: C) -> C = (x: C) => b(x) // error
+  val _: (x: C) -> C = (x: C) => b(x) // ok
   val _: C -> C = (x: C) => a(x) // error