Map cap to fresh in capture sets

Fixes #23170

This was disabled before. We also had to slightly extend fresh/cap collapsing
to make override checks go through under the new scheme.

Author: odersky

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

@@ -118,7 +118,7 @@ class CCState:
 
   private var capIsRoot: Boolean = false
 
-  private var ignoreFreshLevels: Boolean = false
+  private var collapseFresh: Boolean = false
 
 object CCState:
 
@@ -164,20 +164,21 @@ object CCState:
   /** Is `caps.cap` a root capability that is allowed to subsume other capabilities? */
   def capIsRoot(using Context): Boolean = ccState.capIsRoot
 
-  /** Run `op` under the assumption that all FreshCap instances are equal.
+  /** Run `op` under the assumption that all FreshCap instances are equal
+   *  to each other and to GlobalCap.
    *  Needed to make override checking of types containing fresh work.
    *  Asserted in override checking, tested in maxSubsumes.
    *  Is this sound? Test case is neg-custom-args/captures/leaked-curried.scala.
    */
-  inline def ignoringFreshLevels[T](op: => T)(using Context): T =
+  inline def withCollapsedFresh[T](op: => T)(using Context): T =
     if isCaptureCheckingOrSetup then
       val ccs = ccState
-      val saved = ccs.ignoreFreshLevels
-      ccs.ignoreFreshLevels = true
-      try op finally ccs.ignoreFreshLevels = saved
+      val saved = ccs.collapseFresh
+      ccs.collapseFresh = true
+      try op finally ccs.collapseFresh = saved
     else op
 
-  /** Should all FreshCap instances be treated equal? */
-  def ignoreFreshLevels(using Context): Boolean = ccState.ignoreFreshLevels
+  /** Should all FreshCap instances be treated as equal to GlobalCap? */
+  def collapseFresh(using Context): Boolean = ccState.collapseFresh
 
 end CCState

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

@@ -490,11 +490,11 @@ object Capabilities:
       || this.match
         case x: FreshCap =>
           def levelOK =
-            if ccConfig.useFreshLevels && !CCState.ignoreFreshLevels then
+            if ccConfig.useFreshLevels && !CCState.collapseFresh then
               val yOwner = y.levelOwner
               yOwner.isStaticOwner || x.ccOwner.isContainedIn(yOwner)
             else y.core match
-              case GlobalCap | ResultCap(_) | _: ParamRef => false
+              case ResultCap(_) | _: ParamRef => false
               case _ => true
 
           vs.ifNotSeen(this)(x.hiddenSet.elems.exists(_.subsumes(y)))
@@ -512,6 +512,7 @@ object Capabilities:
           y match
             case GlobalCap => true
             case _: ResultCap => false
+            case _: FreshCap if CCState.collapseFresh => true
             case _ =>
               y.derivesFromSharedCapability
               || canAddHidden && vs != VarState.HardSeparate && CCState.capIsRoot
@@ -619,8 +620,6 @@ object Capabilities:
     override def apply(t: Type) =
       if variance <= 0 then t
       else t match
-        case t @ CapturingType(parent: TypeRef, _) if parent.symbol == defn.Caps_CapSet =>
-          t
         case t @ CapturingType(_, _) =>
           mapOver(t)
         case t @ AnnotatedType(parent, ann) =>

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

@@ -184,7 +184,9 @@ sealed abstract class CaptureSet extends Showable:
    */
   def accountsFor(x: Capability)(using ctx: Context)(using vs: VarState = VarState.Separate): Boolean =
 
-    def debugInfo(using Context) = i"$this accountsFor $x"
+    def debugInfo(using Context) =
+      val suffix = if ctx.settings.YccVerbose.value then i" with ${x.captureSetOfInfo}" else ""
+      i"$this accountsFor $x$suffix"
 
     def test(using Context) = reporting.trace(debugInfo):
       elems.exists(_.subsumes(x))
@@ -210,9 +212,8 @@ sealed abstract class CaptureSet extends Showable:
    */
   def mightAccountFor(x: Capability)(using Context): Boolean =
     reporting.trace(i"$this mightAccountFor $x, ${x.captureSetOfInfo}?", show = true):
-      CCState.withCapAsRoot:
-        CCState.ignoringFreshLevels: // OK here since we opportunistically choose an alternative which gets checked later
-          elems.exists(_.subsumes(x)(using ctx)(using VarState.ClosedUnrecorded))
+      CCState.withCollapsedFresh: // OK here since we opportunistically choose an alternative which gets checked later
+        elems.exists(_.subsumes(x)(using ctx)(using VarState.ClosedUnrecorded))
       || !x.isTerminalCapability
         && {
           val elems = x.captureSetOfInfo.elems

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

@@ -159,7 +159,7 @@ object CheckCaptures:
                     def showInOpenedFreshBinders(mts: List[MethodType]): String = mts match
                       case Nil => i"the part $t of "
                       case mt :: mts1 =>
-                        CCState.inNewExistentialScope(mt):
+                        inNewExistentialScope(mt):
                           showInOpenedFreshBinders(mts1)
                     showInOpenedFreshBinders(openScopes.reverse)
                 report.error(
@@ -1160,8 +1160,8 @@ class CheckCaptures extends Recheck, SymTransformer:
         checkSubset(localSet, thisSet, tree.srcPos) // (2)
         for param <- cls.paramGetters do
           if !param.hasAnnotation(defn.ConstructorOnlyAnnot)
-            && !param.hasAnnotation(defn.UntrackedCapturesAnnot) then
-            CCState.withCapAsRoot: // OK? We need this here since self types use `cap` instead of `fresh`
+              && !param.hasAnnotation(defn.UntrackedCapturesAnnot) then
+            withCapAsRoot: // OK? We need this here since self types use `cap` instead of `fresh`
               checkSubset(param.termRef.captureSet, thisSet, param.srcPos) // (3)
         for pureBase <- cls.pureBaseClass do // (4)
           def selfTypeTree = impl.body
@@ -1711,7 +1711,7 @@ class CheckCaptures extends Recheck, SymTransformer:
       def traverse(t: Tree)(using Context) =
         t match
           case t: Template =>
-            ignoringFreshLevels:
+            withCollapsedFresh:
               checkAllOverrides(ctx.owner.asClass, OverridingPairsCheckerCC(_, _, t))
           case _ =>
         traverseChildren(t)
@@ -1915,9 +1915,8 @@ class CheckCaptures extends Recheck, SymTransformer:
                 val normArgs = args.lazyZip(tl.paramInfos).map: (arg, bounds) =>
                   arg.withType(arg.nuType.forceBoxStatus(
                     bounds.hi.isBoxedCapturing | bounds.lo.isBoxedCapturing))
-                CCState.withCapAsRoot: // OK? We need this since bounds use `cap` instead of `fresh`
-                  CCState.ignoringFreshLevels:
-                    checkBounds(normArgs, tl)
+                withCollapsedFresh: // OK? We need this since bounds use `cap` instead of `fresh`
+                  checkBounds(normArgs, tl)
                 if ccConfig.postCheckCapturesets then
                   args.lazyZip(tl.paramNames).foreach(checkTypeParam(_, _, fun.symbol))
               case _ =>
@@ -1936,9 +1935,8 @@ class CheckCaptures extends Recheck, SymTransformer:
             case tree: InferredTypeTree =>
             case tree: New =>
             case tree: TypeTree =>
-              CCState.withCapAsRoot:
-                CCState.ignoringFreshLevels:
-                  checkAppliedTypesIn(tree.withType(tree.nuType))
+              withCollapsedFresh:
+                checkAppliedTypesIn(tree.withType(tree.nuType))
             case _ => traverseChildren(t)
         checkApplied.traverse(unit)
     end postCheck

compiler/src/dotty/tools/dotc/core/Types.scala

@@ -869,7 +869,7 @@ object Types extends TypeUtils {
             pdenot.asSingleDenotation.derivedSingleDenotation(pdenot.symbol, overridingRefinement)
           else
             val isRefinedMethod = rinfo.isInstanceOf[MethodOrPoly]
-            val joint = CCState.ignoringFreshLevels:
+            val joint = CCState.withCollapsedFresh:
                 pdenot.meet(
                   new JointRefDenotation(NoSymbol, rinfo, Period.allInRun(ctx.runId), pre, isRefinedMethod),
                   pre,

tests/neg-custom-args/captures/widen-reach.check

@@ -6,7 +6,7 @@
   |
   |                  where:    ^ refers to the universal root capability
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/widen-reach.scala:9:24 -----------------------------------
-9 |  val foo: IO^ -> IO^ = x => x // error // error
+9 |  val foo: IO^ -> IO^ = x => x // error
   |                        ^^^^^^
   |                        Found:    (x: IO^) ->? IO^{x}
   |                        Required: (x: IO^) -> IO^²
@@ -25,13 +25,3 @@
    |                           ^^^^^^
    |                           Local reach capability x* leaks into capture scope of method test.
    |                           To allow this, the parameter x should be declared with a @use annotation
--- [E164] Declaration Error: tests/neg-custom-args/captures/widen-reach.scala:9:6 --------------------------------------
-9 |  val foo: IO^ -> IO^ = x => x // error // error
-  |      ^
-  |      error overriding value foo in trait Foo of type IO^ -> box IO^;
-  |        value foo of type IO^ -> IO^² has incompatible type
-  |
-  |      where:    ^  refers to the universal root capability
-  |                ^² refers to a fresh root capability in the type of value foo
-  |
-  | longer explanation available when compiling with `-explain`

tests/neg-custom-args/captures/widen-reach.scala

@@ -6,7 +6,7 @@ trait Foo[+T]:
   val foo: IO^ -> T
 
 trait Bar extends Foo[IO^]: // error
-  val foo: IO^ -> IO^ = x => x // error // error
+  val foo: IO^ -> IO^ = x => x // error
 
 def test(x: Foo[IO^]): Unit =
   val y1: Foo[IO^{x*}] = x

tests/pos-custom-args/captures/check-override-typebounds-2.scala

@@ -0,0 +1,18 @@
+import language.experimental.captureChecking
+
+class Capbility
+
+trait A:
+  type T <: Capbility^{caps.cap.rd}
+
+class B extends A:
+  type T = C^{caps.cap.rd}
+
+class C extends Capbility
+
+
+trait A2:
+  type T[Cap^]
+
+  def takesCap[Cap^](t: T[Cap]): Unit
+

tests/pos-custom-args/captures/i23170.scala

@@ -0,0 +1,8 @@
+import caps.*
+
+trait A
+
+extension (a: A^{cap.rd})
+  def await = ()
+
+def awaitA[C <: {cap.rd}](a: A^{C}) = a.await