Solve all capture sets in types of vals and defs by default

odersky · odersky · commit 67446d2db05e · 2025-04-03T17:01:49.000+02:00
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
@@ -49,7 +49,7 @@ object ccConfig:
 
   /** Not used currently. Handy for trying out new features */
   def newScheme(using Context): Boolean =
-    Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.8`)
+    Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.7`)
 
 end ccConfig
 
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -317,14 +317,16 @@ class CheckCaptures extends Recheck, SymTransformer:
     /** Instantiate capture set variables appearing contra-variantly to their
      *  upper approximation.
      */
-    private def interpolator(startingVariance: Int = 1)(using Context) = new TypeTraverser:
+    private def interpolator(sym: Symbol, startingVariance: Int = 1)(using Context) = new TypeTraverser:
       variance = startingVariance
       override def traverse(t: Type) = t match
         case t @ CapturingType(parent, refs) =>
           refs match
             case refs: CaptureSet.Var if !refs.isConst =>
-              if variance < 0 then refs.solve()
-              else if ccConfig.newScheme then refs.markSolved(provisional = true)
+              if variance < 0 then
+                refs.solve()
+              else if ccConfig.newScheme && !sym.isAnonymousFunction then
+                refs.markSolved(provisional = !sym.isMutableVar)
             case _ =>
           traverse(parent)
         case t @ defn.RefinedFunctionOf(rinfo) =>
@@ -356,7 +358,7 @@ class CheckCaptures extends Recheck, SymTransformer:
      */
     private def interpolateVarsIn(tpt: Tree, sym: Symbol)(using Context): Unit =
       if tpt.isInstanceOf[InferredTypeTree] then
-        interpolator().traverse(tpt.nuType)
+        interpolator(sym).traverse(tpt.nuType)
           .showing(i"solved vars for $sym in ${tpt.nuType}", capt)
         anchorCaps(sym).traverse(tpt.nuType)
       for msg <- ccState.approxWarnings do
@@ -378,8 +380,9 @@ class CheckCaptures extends Recheck, SymTransformer:
               if d.isEmpty then provenance else ""
             em"$prefix included in the allowed capture set ${res.blocking}$descr$toAdd"
           target match
-            case target: CaptureSet.Var if res.blocking.isProvisionallySolved =>
-              report.warning(msg.prepend(i"Another capture checking run needs to be scheduled because:"), pos)
+            case target: CaptureSet.Var
+            if res.blocking.isProvisionallySolved =>
+              report.error(msg.prepend(i"Another capture checking run needs to be scheduled because\n"), pos)
               needAnotherRun = true
               added match
                 case added: CaptureRef => target.elems += added
@@ -745,7 +748,7 @@ class CheckCaptures extends Recheck, SymTransformer:
     protected override def recheckArg(arg: Tree, formal: Type)(using Context): Type =
       val freshenedFormal = root.capToFresh(formal)
       val argType = recheck(arg, freshenedFormal)
-        .showing(i"recheck arg $arg vs $freshenedFormal", capt)
+        .showing(i"recheck arg $arg vs $freshenedFormal = $result", capt)
       if formal.hasAnnotation(defn.UseAnnot) || formal.hasAnnotation(defn.ConsumeAnnot) then
         // The @use and/or @consume annotation is added to `formal` by `prepareFunction`
         capt.println(i"charging deep capture set of $arg: ${argType} = ${argType.deepCaptureSet}")
@@ -1016,7 +1019,7 @@ class CheckCaptures extends Recheck, SymTransformer:
 
         val saved = curEnv
         val localSet = capturedVars(sym)
-        if !localSet.isAlwaysEmpty then
+        if localSet ne CaptureSet.empty then
           curEnv = Env(sym, EnvKind.Regular, localSet, curEnv, nestedClosure(tree.rhs))
 
         // ctx with AssumedContains entries for each Contains parameter
@@ -1098,7 +1101,7 @@ class CheckCaptures extends Recheck, SymTransformer:
           .toMap
         def restoreEnvFor(sym: Symbol): Env =
           val localSet = capturedVars(sym)
-          if localSet.isAlwaysEmpty then rootEnv
+          if localSet eq CaptureSet.empty then rootEnv
           else envForOwner.get(sym) match
             case Some(e) => e
             case None => Env(sym, EnvKind.Regular, localSet, restoreEnvFor(sym.owner))
@@ -1125,7 +1128,7 @@ class CheckCaptures extends Recheck, SymTransformer:
         checkSubset(capturedVars(parent.tpe.classSymbol), localSet, parent.srcPos,
           i"\nof the references allowed to be captured by $cls")
       val saved = curEnv
-      if !localSet.isAlwaysEmpty then
+      if localSet ne CaptureSet.empty then
         curEnv = Env(cls, EnvKind.Regular, localSet, curEnv)
       try
         val thisSet = cls.classInfo.selfType.captureSet.withDescription(i"of the self type of $cls")
@@ -1779,7 +1782,7 @@ class CheckCaptures extends Recheck, SymTransformer:
           inContext(ctx.fresh.setOwner(root)):
             checkSelfAgainstParents(root, root.baseClasses)
             val selfType = root.asClass.classInfo.selfType
-            interpolator(startingVariance = -1).traverse(selfType)
+            interpolator(root, startingVariance = -1).traverse(selfType)
             selfType match
               case CapturingType(_, refs: CaptureSet.Var)
               if !root.isEffectivelySealed
diff --git a/tests/neg-custom-args/captures/byname.check b/tests/neg-custom-args/captures/byname.check
@@ -1,3 +1,8 @@
+-- Error: tests/neg-custom-args/captures/byname.scala:5:21 -------------------------------------------------------------
+5 |  def g(x: Int) = if cap2 == cap2 then 1 else x // error
+  |                     ^^^^
+  |                     Another capture checking run needs to be scheduled because
+  |                     reference (cap2 : Cap) is not included in the allowed capture set {} of method f
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/byname.scala:10:6 ----------------------------------------
 10 |  h(f2())  // error
    |    ^^^^
diff --git a/tests/neg-custom-args/captures/byname.scala b/tests/neg-custom-args/captures/byname.scala
@@ -2,7 +2,7 @@ class Cap extends caps.Capability
 
 def test(cap1: Cap, cap2: Cap) =
   def f() = if cap1 == cap1 then g else g
-  def g(x: Int) = if cap2 == cap2 then 1 else x
+  def g(x: Int) = if cap2 == cap2 then 1 else x // error
   def g2(x: Int) = if cap1 == cap1 then 1 else x
   def f2() = if cap1 == cap1 then g2 else g2
   def h(ff: => Int ->{cap2} Int) = ff
diff --git a/tests/neg-custom-args/captures/gears-problem.check b/tests/neg-custom-args/captures/gears-problem.check
@@ -8,7 +8,7 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/gears-problem.scala:24:34 --------------------------------
 24 |    val fut2: Future[T]^{fs*} = r.get // error
    |                                ^^^^^
-   |                                Found:    Future[box T^?]^{collector.futures*}
+   |                                Found:    Future[box T^{}]^{collector.futures*}
    |                                Required: Future[T]^{fs*}
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/i21313.check b/tests/neg-custom-args/captures/i21313.check
@@ -5,7 +5,7 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21313.scala:15:12 ---------------------------------------
 15 |  ac1.await(src2) // error
    |            ^^^^
-   |            Found:    (src2 : Source[Int, scala.caps.CapSet^{ac2}]^?)
+   |            Found:    (src2 : Source[Int, scala.caps.CapSet^{ac2}]^{})
    |            Required: Source[Int, scala.caps.CapSet^{ac1}]^
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/i22808.scala b/tests/neg-custom-args/captures/i22808.scala
@@ -6,8 +6,8 @@ def test1(io: Object^): Unit =
     val x = () =>
       foo()
     val y = Box(io)
-    println(y.m)
-    val _: () -> Unit = x // error
+    println(y.m)  // error: another run needs to be scheduled
+    val _: () -> Unit = x // was error
 
 def test2(io: Object^): Unit =
   def foo(): Unit = bar()
@@ -16,5 +16,5 @@ def test2(io: Object^): Unit =
       foo()
     val _: () -> Unit = x
     val y = Box(io)
-    println(y.m)  // error
+    println(y.m)  // error: another run needs to be scheduled
     val _: () -> Unit = x
diff --git a/tests/neg-custom-args/captures/lazylist.check b/tests/neg-custom-args/captures/lazylist.check
@@ -8,8 +8,8 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylist.scala:35:29 -------------------------------------
 35 |  val ref1c: LazyList[Int] = ref1 // error
    |                             ^^^^
-   |                Found:    (ref1 : lazylists.LazyCons[Int]{val xs: () ->{cap1} lazylists.LazyList[Int]^?}^{cap1})
-   |                Required: lazylists.LazyList[Int]
+   |               Found:    (ref1 : lazylists.LazyCons[Int]{val xs: () ->{cap1} lazylists.LazyList[Int]^{}}^{cap1})
+   |               Required: lazylists.LazyList[Int]
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylist.scala:37:36 -------------------------------------
diff --git a/tests/neg-custom-args/captures/leaking-iterators.check b/tests/neg-custom-args/captures/leaking-iterators.check
@@ -1,7 +1,7 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/leaking-iterators.scala:56:16 ----------------------------
 56 |  usingLogFile: log => // error
    |                ^
-   |                Found:    (log: java.io.FileOutputStream^) ->{xs} box cctest.Iterator[Int]^{log}
+   |                Found:    (log: java.io.FileOutputStream^) ->? box cctest.Iterator[Int]^{log}
    |                Required: (log: java.io.FileOutputStream^) ->{fresh} box cctest.Iterator[Int]^?
    |
    |                Note that reference log.type
diff --git a/tests/neg-custom-args/captures/levels.check b/tests/neg-custom-args/captures/levels.check
@@ -6,10 +6,7 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/levels.scala:22:11 ---------------------------------------
 22 |    r.setV(g) // error
    |           ^
-   |           Found:    box (x: String) ->{cap3} String
-   |           Required: box (x: String) ->? String
-   |
-   |           Note that reference (cap3 : CC^), defined in method scope
-   |           cannot be included in outer capture set ? of value r
+   |           Found:    (x: String) ->{cap3} String
+   |           Required: (x: String) -> String
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/linear-buffer.check b/tests/neg-custom-args/captures/linear-buffer.check
@@ -11,7 +11,7 @@
 -- Error: tests/neg-custom-args/captures/linear-buffer.scala:6:9 -------------------------------------------------------
 6 |  def foo = // error
   |         ^
-  |Separation failure: method foo's inferred result type BadBuffer[box T^?]^ hides non-local this of class class BadBuffer.
+  |Separation failure: method foo's inferred result type BadBuffer[box T^{}]^ hides non-local this of class class BadBuffer.
   |The access must be in a @consume method to allow this.
 -- Error: tests/neg-custom-args/captures/linear-buffer.scala:19:17 -----------------------------------------------------
 19 |  val buf3 = app(buf, 3) // error
diff --git a/tests/neg-custom-args/captures/outer-var.check b/tests/neg-custom-args/captures/outer-var.check
@@ -21,19 +21,13 @@
    |         Found:    () => Unit
    |         Required: () ->{p} Unit
    |
-   |         Note that the universal capability `cap`
-   |         cannot be included in capture set {p} of variable y
-   |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/outer-var.scala:15:8 -------------------------------------
 15 |    y = q           // error, was OK under unsealed
    |        ^
    |        Found:    (q : () => Unit)
    |        Required: () ->{p} Unit
    |
-   |        Note that reference (q : () => Unit), defined in method inner
-   |        cannot be included in outer capture set {p} of variable y
-   |
    | longer explanation available when compiling with `-explain`
 -- Error: tests/neg-custom-args/captures/outer-var.scala:17:57 ---------------------------------------------------------
 17 |  var finalizeActions = collection.mutable.ListBuffer[() => Unit]() // error, was OK under unsealed
diff --git a/tests/neg-custom-args/captures/reaches.check b/tests/neg-custom-args/captures/reaches.check
@@ -9,10 +9,7 @@
 34 |      (() => f.write()) :: Nil // error
    |       ^^^^^^^^^^^^^^^^^^^^^^^
    |       Found:    List[box () ->{f} Unit]
-   |       Required: box List[box () ->{xs*} Unit]^?
-   |
-   |       Note that reference (f : File^), defined in method $anonfun
-   |       cannot be included in outer capture set {xs*} of value cur
+   |       Required: box List[box () ->{xs*} Unit]^{}
    |
    | longer explanation available when compiling with `-explain`
 -- Error: tests/neg-custom-args/captures/reaches.scala:37:6 ------------------------------------------------------------
@@ -81,31 +78,31 @@
 -- Error: tests/neg-custom-args/captures/reaches.scala:88:28 -----------------------------------------------------------
 88 |  ps.map((x, y) => compose1(x, y)) // error // error // error sepcheck
    |                            ^
-   |                      Separation failure: argument of type  A ->{x} box A^?
-   |                      to method compose1: [A, B, C](f: A => B, g: B => C): A ->{f, g} C
-   |                      corresponds to capture-polymorphic formal parameter f of type  box A^? => box A^?
-   |                      and hides capabilities  {x}.
-   |                      Some of these overlap with the captures of the second argument with type  A ->{y} box A^?.
+   |                            Separation failure: argument of type  A ->{x} A
+   |                            to method compose1: [A, B, C](f: A => B, g: B => C): A ->{f, g} C
+   |                            corresponds to capture-polymorphic formal parameter f of type  box A^? => box A^?
+   |                            and hides capabilities  {x}.
+   |                            Some of these overlap with the captures of the second argument with type  A ->{y} A.
    |
-   |                        Hidden set of current argument        : {x}
-   |                        Hidden footprint of current argument  : {x, ps*}
-   |                        Capture set of second argument        : {y}
-   |                        Footprint set of second argument      : {y, ps*}
-   |                        The two sets overlap at               : {ps*}
+   |                              Hidden set of current argument        : {x}
+   |                              Hidden footprint of current argument  : {x, ps*}
+   |                              Capture set of second argument        : {y}
+   |                              Footprint set of second argument      : {y, ps*}
+   |                              The two sets overlap at               : {ps*}
 -- Error: tests/neg-custom-args/captures/reaches.scala:91:28 -----------------------------------------------------------
 91 |  ps.map((x, y) => compose1(x, y)) // error sepcheck
    |                            ^
-   |                      Separation failure: argument of type  A ->{x} box A^?
-   |                      to method compose1: [A, B, C](f: A => B, g: B => C): A ->{f, g} C
-   |                      corresponds to capture-polymorphic formal parameter f of type  box A^? => box A^?
-   |                      and hides capabilities  {x}.
-   |                      Some of these overlap with the captures of the second argument with type  A ->{y} box A^?.
+   |                            Separation failure: argument of type  A ->{x} A
+   |                            to method compose1: [A, B, C](f: A => B, g: B => C): A ->{f, g} C
+   |                            corresponds to capture-polymorphic formal parameter f of type  box A^? => box A^?
+   |                            and hides capabilities  {x}.
+   |                            Some of these overlap with the captures of the second argument with type  A ->{y} A.
    |
-   |                        Hidden set of current argument        : {x}
-   |                        Hidden footprint of current argument  : {x, ps*}
-   |                        Capture set of second argument        : {y}
-   |                        Footprint set of second argument      : {y, ps*}
-   |                        The two sets overlap at               : {ps*}
+   |                              Hidden set of current argument        : {x}
+   |                              Hidden footprint of current argument  : {x, ps*}
+   |                              Capture set of second argument        : {y}
+   |                              Footprint set of second argument      : {y, ps*}
+   |                              The two sets overlap at               : {ps*}
 -- Error: tests/neg-custom-args/captures/reaches.scala:62:31 -----------------------------------------------------------
 62 |  val leaked = usingFile[File^{id*}]: f => // error
    |                               ^^^
diff --git a/tests/neg-custom-args/captures/reaches2.check b/tests/neg-custom-args/captures/reaches2.check
@@ -11,14 +11,14 @@
 -- Error: tests/neg-custom-args/captures/reaches2.scala:10:28 ----------------------------------------------------------
 10 |  ps.map((x, y) => compose1(x, y)) // error // error // error
    |                            ^
-   |                      Separation failure: argument of type  A ->{x} box A^?
-   |                      to method compose1: [A, B, C](f: A => B, g: B => C): A ->{f, g} C
-   |                      corresponds to capture-polymorphic formal parameter f of type  box A^? => box A^?
-   |                      and hides capabilities  {x}.
-   |                      Some of these overlap with the captures of the second argument with type  A ->{y} box A^?.
+   |                            Separation failure: argument of type  A ->{x} A
+   |                            to method compose1: [A, B, C](f: A => B, g: B => C): A ->{f, g} C
+   |                            corresponds to capture-polymorphic formal parameter f of type  box A^? => box A^?
+   |                            and hides capabilities  {x}.
+   |                            Some of these overlap with the captures of the second argument with type  A ->{y} A.
    |
-   |                        Hidden set of current argument        : {x}
-   |                        Hidden footprint of current argument  : {x, ps*}
-   |                        Capture set of second argument        : {y}
-   |                        Footprint set of second argument      : {y, ps*}
-   |                        The two sets overlap at               : {ps*}
+   |                              Hidden set of current argument        : {x}
+   |                              Hidden footprint of current argument  : {x, ps*}
+   |                              Capture set of second argument        : {y}
+   |                              Footprint set of second argument      : {y, ps*}
+   |                              The two sets overlap at               : {ps*}
diff --git a/tests/neg-custom-args/captures/sep-box.check b/tests/neg-custom-args/captures/sep-box.check
@@ -1,14 +1,14 @@
 -- Error: tests/neg-custom-args/captures/sep-box.scala:41:9 ------------------------------------------------------------
 41 |  par(h1.value, h2.value) // error
    |      ^^^^^^^^
-   |      Separation failure: argument of type  Ref^{xs*}
+   |      Separation failure: argument of type  Ref^{h1.value*}
    |      to method par: (x: Ref^, y: Ref^): Unit
    |      corresponds to capture-polymorphic formal parameter x of type  Ref^
-   |      and hides capabilities  {xs*}.
-   |      Some of these overlap with the captures of the second argument with type  Ref^{xs*}.
+   |      and hides capabilities  {h1.value*}.
+   |      Some of these overlap with the captures of the second argument with type  Ref^{h2.value*}.
    |
-   |        Hidden set of current argument        : {xs*}
-   |        Hidden footprint of current argument  : {xs*}
-   |        Capture set of second argument        : {xs*}
-   |        Footprint set of second argument      : {xs*}
+   |        Hidden set of current argument        : {h1.value*}
+   |        Hidden footprint of current argument  : {h1.value*, xs*}
+   |        Capture set of second argument        : {h2.value*}
+   |        Footprint set of second argument      : {h2.value*, xs*}
    |        The two sets overlap at               : {xs*}
diff --git a/tests/neg-custom-args/captures/sep-compose.check b/tests/neg-custom-args/captures/sep-compose.check
diff --git a/tests/neg-custom-args/captures/use-capset.check b/tests/neg-custom-args/captures/use-capset.check
diff --git a/tests/neg-custom-args/captures/vars.check b/tests/neg-custom-args/captures/vars.check

Original file line number	Diff line number	Diff line change
`@@ -8,7 +8,7 @@`
`8`	`8`	`-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/gears-problem.scala:24:34 --------------------------------`
`9`	`9`	`24 \| val fut2: Future[T]^{fs*} = r.get // error`
`10`	`10`	`\| ^^^^^`
`11`		`- \| Found: Future[box T^?]^{collector.futures*}`
	`11`	`+ \| Found: Future[box T^{}]^{collector.futures*}`
`12`	`12`	`\| Required: Future[T]^{fs*}`
`13`	`13`	`\|`
`14`	`14`	\| longer explanation available when compiling with `-explain`
Original file line number	Diff line number	Diff line change
`@@ -5,7 +5,7 @@`
`5`	`5`	`-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21313.scala:15:12 ---------------------------------------`
`6`	`6`	`15 \| ac1.await(src2) // error`
`7`	`7`	`\| ^^^^`
`8`		`- \| Found: (src2 : Source[Int, scala.caps.CapSet^{ac2}]^?)`
	`8`	`+ \| Found: (src2 : Source[Int, scala.caps.CapSet^{ac2}]^{})`
`9`	`9`	`\| Required: Source[Int, scala.caps.CapSet^{ac1}]^`
`10`	`10`	`\|`
`11`	`11`	\| longer explanation available when compiling with `-explain`
Original file line number	Diff line number	Diff line change
`@@ -1,7 +1,7 @@`
`1`	`1`	`-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/leaking-iterators.scala:56:16 ----------------------------`
`2`	`2`	`56 \| usingLogFile: log => // error`
`3`	`3`	`\| ^`
`4`		`- \| Found: (log: java.io.FileOutputStream^) ->{xs} box cctest.Iterator[Int]^{log}`
	`4`	`+ \| Found: (log: java.io.FileOutputStream^) ->? box cctest.Iterator[Int]^{log}`
`5`	`5`	`\| Required: (log: java.io.FileOutputStream^) ->{fresh} box cctest.Iterator[Int]^?`
`6`	`6`	`\|`
`7`	`7`	`\| Note that reference log.type`