Switch to new scheme for bound caps

Drop old-style existentials and use instead Fresh instances that refer
to that MethodType which defines the scope of the Fresh as its result type.

Author: odersky

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

@@ -195,7 +195,7 @@ extension (tp: Type)
    */
   final def isTrackableRef(using Context): Boolean = tp match
     case _: ThisType => true
-    case tp: TermParamRef => !Existential.isBinder(tp)
+    case tp: TermParamRef => !Existential.isBinderOLD(tp)
     case tp: TermRef =>
       ((tp.prefix eq NoPrefix)
       || tp.symbol.isField && !tp.symbol.isStatic && tp.prefix.isTrackableRef
@@ -205,7 +205,8 @@ extension (tp: Type)
       tp.symbol.isType && tp.derivesFrom(defn.Caps_CapSet)
     case tp: TypeParamRef =>
       tp.derivesFrom(defn.Caps_CapSet)
-    case Existential.Var(_) => true
+    case Existential.VarOLD(_) => true
+    case Existential.Vble(_) => true
     case AnnotatedType(parent, annot) =>
       defn.capabilityWrapperAnnots.contains(annot.symbol) && parent.isTrackableRef
     case _ =>
@@ -526,11 +527,11 @@ extension (tp: Type)
           case t @ AnnotatedType(parent, ann) =>
             // Don't map annotations, which includes capture sets
             t.derivedAnnotatedType(this(parent), ann)
-          case t @ FunctionOrMethod(args, res @ Existential(_, _))
+          case t @ FunctionOrMethod(args, res)
           if args.forall(_.isAlwaysPure) =>
             // Also map existentials in results to reach capabilities if all
             // preceding arguments are known to be always pure
-            apply(t.derivedFunctionOrMethod(args, Existential.toCap(res)))
+            t.derivedFunctionOrMethod(args, apply(Existential.toCap(res)))
           case Existential(_, _) =>
             t
           case _ =>
@@ -572,6 +573,11 @@ extension (tp: Type)
     case tp: ThisType => tp.cls.ccLevel.nextInner
     case _ => undefinedLevel
 
+  def hasSuffix(other: MethodType)(using Context): Boolean =
+    (tp eq other) || tp.match
+      case tp: MethodOrPoly => tp.resType.hasSuffix(other)
+      case _ => false
+
 extension (cls: ClassSymbol)
 
   def pureBaseClass(using Context): Option[Symbol] =

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

@@ -6,7 +6,7 @@ import core.*
 import Types.*, Symbols.*, Contexts.*, Decorators.*
 import util.{SimpleIdentitySet, Property}
 import typer.ErrorReporting.Addenda
-import TypeComparer.subsumesExistentially
+import TypeComparer.subsumesExistentiallyOLD
 import util.common.alwaysTrue
 import scala.collection.mutable
 import CCState.*
@@ -110,7 +110,8 @@ trait CaptureRef extends TypeProxy, ValueType:
    */
   final def isMaxCapability(using Context): Boolean = this match
     case tp: TermRef => tp.isCap || tp.info.derivesFrom(defn.Caps_Exists)
-    case Existential.Var(_) => true
+    case Existential.VarOLD(_) => true
+    case Existential.Vble(_) => true
     case Fresh(_) => true
     case ReadOnlyCapability(tp1) => tp1.isMaxCapability
     case _ => false
@@ -228,7 +229,7 @@ trait CaptureRef extends TypeProxy, ValueType:
         case _ => false
     || this.match
         case ReachCapability(x1) => x1.subsumes(y.stripReach)
-        case Existential.Var(bv) => subsumesExistentially(bv, y)
+        case Existential.VarOLD(bv) => subsumesExistentiallyOLD(bv, y)
         case x: TermRef => viaInfo(x.info)(subsumingRefs(_, y))
         case x: TypeRef if assumedContainsOf(x).contains(y) => true
         case x: TypeRef if x.derivesFrom(defn.Caps_CapSet) =>
@@ -258,6 +259,10 @@ trait CaptureRef extends TypeProxy, ValueType:
       case Fresh(hidden) =>
         vs.ifNotSeen(this)(hidden.elems.exists(_.subsumes(y)))
         || !y.stripReadOnly.isCap && canAddHidden && vs.addHidden(hidden, y)
+      case Existential.Vble(binder) =>
+        y.stripReadOnly match
+          case Existential.Vble(binder1) => binder1.hasSuffix(binder)
+          case _ => true
       case _ =>
         this.isCap && canAddHidden && vs != VarState.HardSeparate
         || y.match

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

@@ -104,7 +104,8 @@ sealed abstract class CaptureSet extends Showable:
 
   final def isUnboxable(using Context) =
     elems.exists:
-      case Existential.Var(_) => true
+      case Existential.VarOLD(_) => true
+      case Existential.Vble(_) => true
       case elem => elem.isRootCapability
 
   final def isReadOnly(using Context): Boolean =
@@ -547,7 +548,7 @@ object CaptureSet:
     final def addThisElem(elem: CaptureRef)(using Context, VarState): CompareResult =
       if isConst || !recordElemsState() then // Fail if variable is solved or given VarState is frozen
         addIfHiddenOrFail(elem)
-      else if Existential.isBadExistential(elem) then // Fail if `elem` is an out-of-scope existential
+      else if Existential.isBadExistentialOLD(elem) then // Fail if `elem` is an out-of-scope existential
         CompareResult.Fail(this :: Nil)
       else if !levelOK(elem) then
         CompareResult.LevelError(this, elem)    // or `elem` is not visible at the level of the set.
@@ -567,15 +568,21 @@ object CaptureSet:
           elems -= elem
           res.addToTrace(this)
 
+    // TODO: Also track allowable TermParamRefs and Existential.Vbles in capture sets
     private def levelOK(elem: CaptureRef)(using Context): Boolean =
       if elem.isRootCapability then
         !noUniversal
       else elem match
-        case Existential.Var(bv) =>
+        case Existential.VarOLD(bv) =>
           !noUniversal
           && !TypeComparer.isOpenedExistential(bv)
             // Opened existentials on the left cannot be added to nested capture sets on the right
             // of a comparison. Test case is open-existential.scala.
+        case elem @ Existential.Vble(mt) =>
+          !noUniversal
+          && !TypeComparer.isOpenedExistential(elem)
+            // Opened existentials on the left cannot be added to nested capture sets on the right
+            // of a comparison. Test case is open-existential.scala.
         case elem: TermRef if level.isDefined =>
           elem.prefix match
             case prefix: CaptureRef =>
@@ -629,7 +636,8 @@ object CaptureSet:
         try
           val approx = computeApprox(origin).ensuring(_.isConst)
           if approx.elems.exists:
-            case Existential.Var(_) => true
+            case Existential.VarOLD(_) => true
+            case Existential.Vble(_) => true
             case _ => false
           then
             ccState.approxWarnings +=
@@ -1304,7 +1312,7 @@ object CaptureSet:
       ref1.captureSetOfInfo.map(ReadOnlyMap())
     case _ =>
       if ref.isMaxCapability then ref.singletonCaptureSet
-      else ofType(ref.underlying, followResult = true)
+      else ofType(ref.underlying, followResult = true) // TODO: why followResult = true?
 
   /** Capture set of a type */
   def ofType(tp: Type, followResult: Boolean)(using Context): CaptureSet =
@@ -1317,7 +1325,9 @@ object CaptureSet:
         case tp: (TypeRef | TypeParamRef) =>
           if tp.derivesFrom(defn.Caps_CapSet) then tp.captureSet
           else empty
-        case tp @ Existential.Var(_) =>
+        case tp @ Existential.VarOLD(_) =>
+          tp.captureSet
+        case tp @ Existential.Vble(_) =>
           tp.captureSet
         case CapturingType(parent, refs) =>
           recur(parent) ++ refs
@@ -1332,8 +1342,11 @@ object CaptureSet:
               CaptureSet.ofTypeDeeply(parent.widen)
         case tpd @ defn.RefinedFunctionOf(rinfo: MethodType) if followResult =>
           ofType(tpd.parent, followResult = false)             // pick up capture set from parent type
-          ++ (recur(rinfo.resType)                             // add capture set of result
-          -- CaptureSet(rinfo.paramRefs.filter(_.isTracked)*)) // but disregard bound parameters
+          ++ recur(rinfo.resType)                             // add capture set of result
+              .filter:
+                case TermParamRef(binder, _) => binder ne rinfo
+                case Existential.Vble(binder) => binder ne rinfo
+                case _ => true
         case tpd @ AppliedType(tycon, args) =>
           if followResult && defn.isNonRefinedFunction(tpd) then
             recur(args.last)
@@ -1359,7 +1372,7 @@ object CaptureSet:
    *  capture sets. Nested existential sets are approximated with `cap`.
    *  NOTE: The traversal logic needs to be in sync with narrowCaps in CaptureOps, which
    *  replaces caps with reach capabilties. The one exception to this is invariant
-   *  arguments. This have to be included to be conservative in dcs but must be
+   *  arguments. These have to be included to be conservative in dcs but must be
    *  excluded in narrowCaps.
    */
   def ofTypeDeeply(tp: Type, includeTypevars: Boolean = false)(using Context): CaptureSet =
@@ -1377,9 +1390,9 @@ object CaptureSet:
             val upper = t.info.bounds.hi
             if includeTypevars && upper.isExactlyAny then CaptureSet.fresh(t.symbol)
             else this(cs, upper)
-          case t @ FunctionOrMethod(args, res @ Existential(_, _))
-          if args.forall(_.isAlwaysPure) =>
-            this(cs, Existential.toCap(res))
+          case t @ FunctionOrMethod(args, res) =>
+            if args.forall(_.isAlwaysPure) then this(cs, Existential.toCap(res))
+            else cs
           case t @ Existential(_, _) =>
             cs
           case _ =>

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

@@ -23,7 +23,7 @@ import CCState.*
 import StdNames.nme
 import NameKinds.{DefaultGetterName, WildcardParamName, UniqueNameKind}
 import reporting.{trace, Message, OverrideError}
-import Existential.derivedExistentialType
+import Existential.derivedExistentialTypeOLD
 import Annotations.Annotation
 
 /** The capture checker */
@@ -850,7 +850,7 @@ class CheckCaptures extends Recheck, SymTransformer:
           // added capture set to result.
           augmentConstructorType(parent, initCs ++ refs)
         case core @ Existential(boundVar, core1) =>
-          core.derivedExistentialType(augmentConstructorType(core1, initCs))
+          core.derivedExistentialTypeOLD(augmentConstructorType(core1, initCs))
         case _ =>
           val (refined, cs) = addParamArgRefinements(core, initCs)
           refined.capturing(cs)
@@ -922,7 +922,7 @@ class CheckCaptures extends Recheck, SymTransformer:
           // which are less intelligible. An example is the line `a = x` in
           // neg-custom-args/captures/vars.scala. That's why this code is conditioned.
           // to apply only to closures that are not eta expansions.
-          val res1 = Existential.toCapDeeply(res)
+          val res1 = Existential.toCapDeeply(res) // TODO: why toCapDeeply?
           val pt1 = Existential.toCapDeeply(pt)
             // We need to open existentials here in order not to get vars mixed up in them
             // We do the proper check with existentials when we are finished with the closure block.
@@ -1433,7 +1433,7 @@ class CheckCaptures extends Recheck, SymTransformer:
         // Get existentials and wildcards out of the way
         actual match
           case actual @ Existential(_, actualUnpacked) =>
-            return Existential.derivedExistentialType(actual):
+            return Existential.derivedExistentialTypeOLD(actual):
                 recur(actualUnpacked, expected, covariant)
           case _ =>
         expected match