Existential capabilities design draft

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

@@ -14,6 +14,7 @@ import tpd.*
 import StdNames.nme
 import config.Feature
 import collection.mutable
+import CCState.*
 
 private val Captures: Key[CaptureSet] = Key()
 
@@ -64,11 +65,47 @@ class CCState:
    */
   var levelError: Option[CaptureSet.CompareResult.LevelError] = None
 
+  private var curLevel: Level = outermostLevel
+  private val symLevel: mutable.Map[Symbol, Int] = mutable.Map()
+
+object CCState:
+
+  opaque type Level = Int
+
+  val undefinedLevel: Level = -1
+
+  val outermostLevel: Level = 0
+
+  /** The level of the current environment. Levels start at 0 and increase for
+   *  each nested function or class. -1 means the level is undefined.
+   */
+  def currentLevel(using Context): Level = ccState.curLevel
+
+  inline def inNestedLevel[T](inline op: T)(using Context): T =
+    val ccs = ccState
+    val saved = ccs.curLevel
+    ccs.curLevel = ccs.curLevel.nextInner
+    try op finally ccs.curLevel = saved
+
+  inline def inNestedLevelUnless[T](inline p: Boolean)(inline op: T)(using Context): T =
+    val ccs = ccState
+    val saved = ccs.curLevel
+    if !p then ccs.curLevel = ccs.curLevel.nextInner
+    try op finally ccs.curLevel = saved
+
+  extension (x: Level)
+    def isDefined: Boolean = x >= 0
+    def <= (y: Level) = (x: Int) <= y
+    def nextInner: Level = if isDefined then x + 1 else x
+
+  extension (sym: Symbol)(using Context)
+    def ccLevel: Level = ccState.symLevel.getOrElse(sym, -1)
+    def recordLevel() = ccState.symLevel(sym) = currentLevel
 end CCState
 
 /** The currently valid CCState */
 def ccState(using Context) =
-  Phases.checkCapturesPhase.asInstanceOf[CheckCaptures].ccState
+  Phases.checkCapturesPhase.asInstanceOf[CheckCaptures].ccState1
 
 class NoCommonRoot(rs: Symbol*)(using Context) extends Exception(
   i"No common capture root nested in ${rs.mkString(" and ")}"
@@ -203,6 +240,23 @@ extension (tp: Type)
     case _ =>
       false
 
+  /** Tests whether the type derives from `caps.Capability`, which means
+   *  references of this type are maximal capabilities.
+   */
+  def derivesFromCapability(using Context): Boolean = tp.dealias match
+    case tp: (TypeRef | AppliedType) =>
+      val sym = tp.typeSymbol
+      if sym.isClass then sym.derivesFrom(defn.Caps_Capability)
+      else tp.superType.derivesFromCapability
+    case tp: TypeProxy =>
+      tp.superType.derivesFromCapability
+    case tp: AndType =>
+      tp.tp1.derivesFromCapability || tp.tp2.derivesFromCapability
+    case tp: OrType =>
+      tp.tp1.derivesFromCapability && tp.tp2.derivesFromCapability
+    case _ =>
+      false
+
   /** Drop @retains annotations everywhere */
   def dropAllRetains(using Context): Type = // TODO we should drop retains from inferred types before unpickling
     val tm = new TypeMap:
@@ -322,6 +376,12 @@ extension (tp: Type)
       case _ =>
         tp
 
+  def level(using Context): Level =
+    tp match
+    case tp: TermRef => tp.symbol.ccLevel
+    case tp: ThisType => tp.cls.ccLevel.nextInner
+    case _ => undefinedLevel
+
 extension (cls: ClassSymbol)
 
   def pureBaseClass(using Context): Option[Symbol] =
@@ -406,9 +466,7 @@ extension (sym: Symbol)
     || sym.is(Method, butNot = Accessor)
 
   /** The owner of the current level. Qualifying owners are
-   *   - methods other than constructors and anonymous functions
-   *   - anonymous functions, provided they either define a local
-   *     root of type caps.Cap, or they are the rhs of a val definition.
+   *   - methods, other than accessors
    *   - classes, if they are not staticOwners
    *   - _root_
    */

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

@@ -14,8 +14,10 @@ import printing.{Showable, Printer}
 import printing.Texts.*
 import util.{SimpleIdentitySet, Property}
 import typer.ErrorReporting.Addenda
+import TypeComparer.linkOK
 import util.common.alwaysTrue
 import scala.collection.mutable
+import CCState.*
 
 /** A class for capture sets. Capture sets can be constants or variables.
  *  Capture sets support inclusion constraints <:< where <:< is subcapturing.
@@ -55,10 +57,14 @@ sealed abstract class CaptureSet extends Showable:
    */
   def isAlwaysEmpty: Boolean
 
-  /** An optional level limit, or NoSymbol if none exists. All elements of the set
-   *  must be in scopes visible from the level limit.
+  /** An optional level limit, or undefinedLevel if none exists. All elements of the set
+   *  must be at levels equal or smaller than the level of the set, if it is defined.
    */
-  def levelLimit: Symbol
+  def level: Level
+
+  /** An optional owner, or NoSymbol if none exists. Used for diagnstics
+   */
+  def owner: Symbol
 
   /** Is this capture set definitely non-empty? */
   final def isNotEmpty: Boolean = !elems.isEmpty
@@ -115,7 +121,7 @@ sealed abstract class CaptureSet extends Showable:
    *  capture set.
    */
   protected final def addNewElem(elem: CaptureRef)(using Context, VarState): CompareResult =
-    if elem.isRootCapability || summon[VarState] == FrozenState then
+    if elem.isMaxCapability || summon[VarState] == FrozenState then
       addThisElem(elem)
     else
       addThisElem(elem).orElse:
@@ -147,17 +153,28 @@ sealed abstract class CaptureSet extends Showable:
    *   this subsumes this.f
    *   x subsumes y  ==>  x* subsumes y, x subsumes y?
    *   x subsumes y  ==>  x* subsumes y*, x? subsumes y?
+   *   x: x1.type /\ x1 subsumes y  ==>  x subsumes y
    */
   extension (x: CaptureRef)
      private def subsumes(y: CaptureRef)(using Context): Boolean =
       (x eq y)
       || x.isRootCapability
       || y.match
-          case y: TermRef => y.prefix eq x
+          case y: TermRef =>
+            (y.prefix eq x)
+            || y.info.match
+                case y1: CaptureRef => x.subsumes(y1)
+                case _ => false
+          case y: TermParamRef => linkOK(y, x)
           case MaybeCapability(y1) => x.stripMaybe.subsumes(y1)
           case _ => false
       || x.match
           case ReachCapability(x1) => x1.subsumes(y.stripReach)
+          case x: TermRef =>
+            x.info match
+              case x1: CaptureRef => x1.subsumes(y)
+              case _ => false
+          case x: TermParamRef => linkOK(x, y)
           case _ => false
 
   /** {x} <:< this   where <:< is subcapturing, but treating all variables
@@ -167,11 +184,11 @@ sealed abstract class CaptureSet extends Showable:
     if comparer.isInstanceOf[ExplainingTypeComparer] then // !!! DEBUG
       reporting.trace.force(i"$this accountsFor $x, ${x.captureSetOfInfo}?", show = true):
         elems.exists(_.subsumes(x))
-        || !x.isRootCapability && x.captureSetOfInfo.subCaptures(this, frozen = true).isOK
+        || !x.isMaxCapability && x.captureSetOfInfo.subCaptures(this, frozen = true).isOK
     else
       reporting.trace(i"$this accountsFor $x, ${x.captureSetOfInfo}?", show = true):
         elems.exists(_.subsumes(x))
-        || !x.isRootCapability && x.captureSetOfInfo.subCaptures(this, frozen = true).isOK
+        || !x.isMaxCapability && x.captureSetOfInfo.subCaptures(this, frozen = true).isOK
 
   /** A more optimistic version of accountsFor, which does not take variable supersets
    *  of the `x` reference into account. A set might account for `x` if it accounts
@@ -183,7 +200,7 @@ sealed abstract class CaptureSet extends Showable:
   def mightAccountFor(x: CaptureRef)(using Context): Boolean =
     reporting.trace(i"$this mightAccountFor $x, ${x.captureSetOfInfo}?", show = true) {
       elems.exists(_.subsumes(x))
-      || !x.isRootCapability
+      || !x.isMaxCapability
         && {
           val elems = x.captureSetOfInfo.elems
           !elems.isEmpty && elems.forall(mightAccountFor)
@@ -230,9 +247,7 @@ sealed abstract class CaptureSet extends Showable:
     if this.subCaptures(that, frozen = true).isOK then that
     else if that.subCaptures(this, frozen = true).isOK then this
     else if this.isConst && that.isConst then Const(this.elems ++ that.elems)
-    else Var(
-        this.levelLimit.maxNested(that.levelLimit, onConflict = (sym1, sym2) => sym1),
-        this.elems ++ that.elems)
+    else Var(initialElems = this.elems ++ that.elems)
       .addAsDependentTo(this).addAsDependentTo(that)
 
   /** The smallest superset (via <:<) of this capture set that also contains `ref`.
@@ -383,7 +398,7 @@ object CaptureSet:
 
   def apply(elems: CaptureRef*)(using Context): CaptureSet.Const =
     if elems.isEmpty then empty
-    else Const(SimpleIdentitySet(elems.map(_.normalizedRef)*))
+    else Const(SimpleIdentitySet(elems.map(_.normalizedRef.ensuring(_.isTrackableRef))*))
 
   def apply(elems: Refs)(using Context): CaptureSet.Const =
     if elems.isEmpty then empty else Const(elems)
@@ -402,7 +417,9 @@ object CaptureSet:
 
     def withDescription(description: String): Const = Const(elems, description)
 
-    def levelLimit = NoSymbol
+    def level = undefinedLevel
+
+    def owner = NoSymbol
 
     override def toString = elems.toString
   end Const
@@ -422,7 +439,7 @@ object CaptureSet:
   end Fluid
 
   /** The subclass of captureset variables with given initial elements */
-  class Var(directOwner: Symbol, initialElems: Refs = emptySet)(using @constructorOnly ictx: Context) extends CaptureSet:
+  class Var(override val owner: Symbol = NoSymbol, initialElems: Refs = emptySet, val level: Level = undefinedLevel, underBox: Boolean = false)(using @constructorOnly ictx: Context) extends CaptureSet:
 
     /** A unique identification number for diagnostics */
     val id =
@@ -431,9 +448,6 @@ object CaptureSet:
 
     //assert(id != 40)
 
-    override val levelLimit =
-      if directOwner.exists then directOwner.levelOwner else NoSymbol
-
     /** A variable is solved if it is aproximated to a from-then-on constant set. */
     private var isSolved: Boolean = false
 
@@ -491,6 +505,7 @@ object CaptureSet:
         CompareResult.LevelError(this, elem)
       else
         //if id == 34 then assert(!elem.isUniversalRootCapability)
+        assert(elem.isTrackableRef, elem)
         elems += elem
         if elem.isRootCapability then
           rootAddedHandler()
@@ -506,12 +521,10 @@ object CaptureSet:
     private def levelOK(elem: CaptureRef)(using Context): Boolean =
       if elem.isRootCapability then !noUniversal
       else elem match
-        case elem: TermRef if levelLimit.exists =>
-          var sym = elem.symbol
-          if sym.isLevelOwner then sym = sym.owner
-          levelLimit.isContainedIn(sym.levelOwner)
-        case elem: ThisType if levelLimit.exists =>
-          levelLimit.isContainedIn(elem.cls.levelOwner)
+        case elem: TermRef if level.isDefined =>
+          elem.symbol.ccLevel <= level
+        case elem: ThisType if level.isDefined =>
+          elem.cls.ccLevel.nextInner <= level
         case ReachCapability(elem1) =>
           levelOK(elem1)
         case MaybeCapability(elem1) =>
@@ -589,8 +602,8 @@ object CaptureSet:
       val debugInfo =
         if !isConst && ctx.settings.YccDebug.value then ids else ""
       val limitInfo =
-        if ctx.settings.YprintLevel.value && levelLimit.exists
-        then i"<in $levelLimit>"
+        if ctx.settings.YprintLevel.value && level.isDefined
+        then i"<at level ${level.toString}>"
         else ""
       debugInfo ++ limitInfo
 
@@ -609,13 +622,6 @@ object CaptureSet:
     override def toString = s"Var$id$elems"
   end Var
 
-  /** Variables that represent refinements of class parameters can have the universal
-   *  capture set, since they represent only what is the result of the constructor.
-   *  Test case: Without that tweak, logger.scala would not compile.
-   */
-  class RefiningVar(directOwner: Symbol)(using Context) extends Var(directOwner):
-    override def disallowRootCapability(handler: () => Context ?=> Unit)(using Context) = this
-
   /** A variable that is derived from some other variable via a map or filter. */
   abstract class DerivedVar(owner: Symbol, initialElems: Refs)(using @constructorOnly ctx: Context)
   extends Var(owner, initialElems):
@@ -644,7 +650,7 @@ object CaptureSet:
    */
   class Mapped private[CaptureSet]
     (val source: Var, tm: TypeMap, variance: Int, initial: CaptureSet)(using @constructorOnly ctx: Context)
-  extends DerivedVar(source.levelLimit, initial.elems):
+  extends DerivedVar(source.owner, initial.elems):
     addAsDependentTo(initial)  // initial mappings could change by propagation
 
     private def mapIsIdempotent = tm.isInstanceOf[IdempotentCaptRefMap]
@@ -741,7 +747,7 @@ object CaptureSet:
    */
   final class BiMapped private[CaptureSet]
     (val source: Var, bimap: BiTypeMap, initialElems: Refs)(using @constructorOnly ctx: Context)
-  extends DerivedVar(source.levelLimit, initialElems):
+  extends DerivedVar(source.owner, initialElems):
 
     override def tryInclude(elem: CaptureRef, origin: CaptureSet)(using Context, VarState): CompareResult =
       if origin eq source then
@@ -775,7 +781,7 @@ object CaptureSet:
   /** A variable with elements given at any time as { x <- source.elems | p(x) } */
   class Filtered private[CaptureSet]
     (val source: Var, p: Context ?=> CaptureRef => Boolean)(using @constructorOnly ctx: Context)
-  extends DerivedVar(source.levelLimit, source.elems.filter(p)):
+  extends DerivedVar(source.owner, source.elems.filter(p)):
 
     override def tryInclude(elem: CaptureRef, origin: CaptureSet)(using Context, VarState): CompareResult =
       if accountsFor(elem) then
@@ -805,7 +811,7 @@ object CaptureSet:
   extends Filtered(source, !other.accountsFor(_))
 
   class Intersected(cs1: CaptureSet, cs2: CaptureSet)(using Context)
-  extends Var(cs1.levelLimit.minNested(cs2.levelLimit), elemIntersection(cs1, cs2)):
+  extends Var(initialElems = elemIntersection(cs1, cs2)):
     addAsDependentTo(cs1)
     addAsDependentTo(cs2)
     deps += cs1
@@ -895,7 +901,7 @@ object CaptureSet:
             if ctx.settings.YccDebug.value then printer.toText(trace, ", ")
             else blocking.show
           case LevelError(cs: CaptureSet, elem: CaptureRef) =>
-            Str(i"($elem at wrong level for $cs in ${cs.levelLimit})")
+            Str(i"($elem at wrong level for $cs at level ${cs.level.toString})")
 
     /** The result is OK */
     def isOK: Boolean = this == OK
@@ -1032,7 +1038,9 @@ object CaptureSet:
 
   /** The capture set of the type underlying CaptureRef */
   def ofInfo(ref: CaptureRef)(using Context): CaptureSet = ref match
-    case ref: TermRef if ref.isRootCapability => ref.singletonCaptureSet
+    case ref: (TermRef | TermParamRef) if ref.isMaxCapability =>
+      if ref.isTrackableRef then ref.singletonCaptureSet
+      else CaptureSet.universal
     case ReachCapability(ref1) => deepCaptureSet(ref1.widen)
       .showing(i"Deep capture set of $ref: ${ref1.widen} = $result", capt)
     case _ => ofType(ref.underlying, followResult = true)
@@ -1046,7 +1054,8 @@ object CaptureSet:
         case tp: TermParamRef =>
           tp.captureSet
         case tp: TypeRef =>
-          if tp.typeSymbol == defn.Caps_Cap then universal else empty
+          if tp.derivesFromCapability then universal // TODO: maybe return another value that indicates that the underltinf ref is maximal?
+          else empty
         case _: TypeParamRef =>
           empty
         case CapturingType(parent, refs) =>
@@ -1074,7 +1083,7 @@ object CaptureSet:
         case _ =>
           empty
     recur(tp)
-      .showing(i"capture set of $tp = $result", captDebug)
+      //.showing(i"capture set of $tp = $result", captDebug)
 
   private def deepCaptureSet(tp: Type)(using Context): CaptureSet =
     val collect = new TypeAccumulator[CaptureSet]:
@@ -1135,6 +1144,6 @@ object CaptureSet:
           i"""
             |
             |Note that reference ${ref}$levelStr
-            |cannot be included in outer capture set $cs which is associated with ${cs.levelLimit}"""
+            |cannot be included in outer capture set $cs"""
 
 end CaptureSet