Alternative scheme for cc encapsulation

compiler/src/dotty/tools/dotc/ast/Desugar.scala

@@ -1858,6 +1858,8 @@ object desugar {
             Annotated(
               AppliedTypeTree(ref(defn.SeqType), t),
               New(ref(defn.RepeatedAnnot.typeRef), Nil :: Nil))
+        else if op.name == nme.CC_REACH then
+          Apply(ref(defn.Caps_reachCapability), t :: Nil)
         else
           assert(ctx.mode.isExpr || ctx.reporter.errorsReported || ctx.mode.is(Mode.Interactive), ctx.mode)
           Select(t, op.name)

compiler/src/dotty/tools/dotc/ast/TreeInfo.scala

@@ -376,17 +376,6 @@ trait TreeInfo[T <: Untyped] { self: Trees.Instance[T] =>
     case _ =>
       tree.tpe.isInstanceOf[ThisType]
   }
-
-  /** Under capture checking, an extractor for qualified roots `cap[Q]`.
-   */
-  object QualifiedRoot:
-
-    def unapply(tree: Apply)(using Context): Option[String] = tree match
-      case Apply(fn, Literal(lit) :: Nil) if fn.symbol == defn.Caps_capIn =>
-        Some(lit.value.asInstanceOf[String])
-      case _ =>
-        None
-  end QualifiedRoot
 }
 
 trait UntypedTreeInfo extends TreeInfo[Untyped] { self: Trees.Instance[Untyped] =>

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

@@ -63,7 +63,7 @@ case class CaptureAnnotation(refs: CaptureSet, boxed: Boolean)(cls: Symbol) exte
     val elems = refs.elems.toList
     val elems1 = elems.mapConserve(tm)
     if elems1 eq elems then this
-    else if elems1.forall(_.isInstanceOf[CaptureRef])
+    else if elems1.forall(_.isTrackableRef)
     then derivedAnnotation(CaptureSet(elems1.asInstanceOf[List[CaptureRef]]*), boxed)
     else EmptyAnnotation
 

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

@@ -59,9 +59,6 @@ class IllegalCaptureRef(tpe: Type) extends Exception(tpe.toString)
 /** Capture checking state, which is known to other capture checking components */
 class CCState:
 
-  /** Associates nesting level owners with the local roots valid in their scopes. */
-  val localRoots: mutable.HashMap[Symbol, Symbol] = new mutable.HashMap
-
   /** The last pair of capture reference and capture set where
    *  the reference could not be added to the set due to a level conflict.
    */
@@ -81,13 +78,13 @@ extension (tree: Tree)
 
   /** Map tree with CaptureRef type to its type, throw IllegalCaptureRef otherwise */
   def toCaptureRef(using Context): CaptureRef = tree match
-    case QualifiedRoot(outer) =>
-      ctx.owner.levelOwnerNamed(outer)
-        .orElse(defn.RootClass) // non-existing outer roots are reported in Setup's checkQualifiedRoots
-        .localRoot.termRef
+    case ReachCapabilityApply(arg) =>
+      arg.toCaptureRef.reach
     case _ => tree.tpe match
-      case ref: CaptureRef => ref
-      case tpe => throw IllegalCaptureRef(tpe) // if this was compiled from cc syntax, problem should have been reported at Typer
+      case ref: CaptureRef if ref.isTrackableRef =>
+        ref
+      case tpe =>
+        throw IllegalCaptureRef(tpe) // if this was compiled from cc syntax, problem should have been reported at Typer
 
   /** Convert a @retains or @retainsByName annotation tree to the capture set it represents.
    *  For efficience, the result is cached as an Attachment on the tree.
@@ -166,7 +163,7 @@ extension (tp: Type)
   def forceBoxStatus(boxed: Boolean)(using Context): Type = tp.widenDealias match
     case tp @ CapturingType(parent, refs) if tp.isBoxed != boxed =>
       val refs1 = tp match
-        case ref: CaptureRef if ref.isTracked => ref.singletonCaptureSet
+        case ref: CaptureRef if ref.isTracked || ref.isReach => ref.singletonCaptureSet
         case _ => refs
       CapturingType(parent, refs1, boxed)
     case _ =>
@@ -206,12 +203,6 @@ extension (tp: Type)
     case _: TypeRef | _: AppliedType => tp.typeSymbol.hasAnnotation(defn.CapabilityAnnot)
     case _ => false
 
-  def isSealed(using Context): Boolean = tp match
-    case tp: TypeParamRef => tp.underlying.isSealed
-    case tp: TypeBounds => tp.hi.hasAnnotation(defn.Caps_SealedAnnot)
-    case tp: TypeRef => tp.symbol.is(Sealed) || tp.info.isSealed // TODO: drop symbol flag?
-    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:
@@ -222,6 +213,62 @@ extension (tp: Type)
           mapOver(t)
     tm(tp)
 
+  /** If `x` is a capture ref, its reach capability `x*`, represented internally
+   *  as `x @reachCapability`. `x*` stands for all capabilities reachable through `x`".
+   *  We have `{x} <: {x*} <: dcs(x)}` where the deep capture set `dcs(x)` of `x`
+   *  is the union of all capture sets that appear in covariant position in the
+   *  type of `x`. If `x` and `y` are different variables then `{x*}` and `{y*}`
+   *  are unrelated.
+   */
+  def reach(using Context): CaptureRef =
+    assert(tp.isTrackableRef)
+    AnnotatedType(tp, Annotation(defn.ReachCapabilityAnnot, util.Spans.NoSpan))
+
+  /** If `ref` is a trackable capture ref, and `tp` has only covariant occurrences of a
+   *  universal capture set, replace all these occurrences by `{ref*}`. This implements
+   *  the new aspect of the (Var) rule, which can now be stated as follows:
+   *
+   *     x: T in E
+   *     -----------
+   *     E |- x: T'
+   *
+   *  where T' is T with (1) the toplevel capture set replaced by `{x}` and
+   *  (2) all covariant occurrences of cap replaced by `x*`, provided there
+   *  are no occurrences in `T` at other variances. (1) is standard, whereas
+   *  (2) is new.
+   *
+   *  Why is this sound? Covariant occurrences of cap must represent capabilities
+   *  that are reachable from `x`, so they are included in the meaning of `{x*}`.
+   *  At the same time, encapsulation is still maintained since no covariant
+   *  occurrences of cap are allowed in instance types of type variables.
+   */
+  def withReachCaptures(ref: Type)(using Context): Type =
+    object narrowCaps extends TypeMap:
+      var ok = true
+      def apply(t: Type) = t.dealias match
+        case t1 @ CapturingType(p, cs) if cs.isUniversal =>
+          if variance > 0 then
+            t1.derivedCapturingType(apply(p), ref.reach.singletonCaptureSet)
+          else
+            ok = false
+            t
+        case _ => t match
+          case t @ CapturingType(p, cs) =>
+            t.derivedCapturingType(apply(p), cs) // don't map capture set variables
+          case t =>
+            mapOver(t)
+    ref match
+      case ref: CaptureRef if ref.isTrackableRef =>
+        val tp1 = narrowCaps(tp)
+        if narrowCaps.ok then
+          if tp1 ne tp then capt.println(i"narrow $tp of $ref to $tp1")
+          tp1
+        else
+          capt.println(i"cannot narrow $tp of $ref to $tp1")
+          tp
+      case _ =>
+        tp
+
 extension (cls: ClassSymbol)
 
   def pureBaseClass(using Context): Option[Symbol] =
@@ -281,24 +328,13 @@ extension (sym: Symbol)
     && sym != defn.Caps_unsafeBox
     && sym != defn.Caps_unsafeUnbox
 
-  /** Can this symbol possibly own a local root?
-   *  TODO: Disallow anonymous functions?
+  /** Does this symbol define a level where we do not want to let local variables
+   *  escape into outer capture sets?
    */
   def isLevelOwner(using Context): Boolean =
     sym.isClass
     || sym.is(Method, butNot = Accessor)
 
-  /** The level owner enclosing `sym` which has the given name, or NoSymbol
-   *  if none exists.
-   */
-  def levelOwnerNamed(name: String)(using Context): Symbol =
-    def recur(sym: Symbol): Symbol =
-      if sym.name.toString == name then
-        if sym.isLevelOwner then sym else NoSymbol
-      else if sym == defn.RootClass then NoSymbol
-      else recur(sym.owner)
-    recur(sym)
-
   /** The owner of the current level. Qualifying owners are
    *   - methods other than constructors and anonymous functions
    *   - anonymous functions, provided they either define a local
@@ -313,14 +349,6 @@ extension (sym: Symbol)
       else recur(sym.owner)
     recur(sym)
 
-  /** The local root corresponding to sym's level owner */
-  def localRoot(using Context): Symbol =
-    val owner = sym.levelOwner
-    assert(owner.exists)
-    def newRoot = newSymbol(if owner.isClass then newLocalDummy(owner) else owner,
-      nme.LOCAL_CAPTURE_ROOT, Synthetic, defn.Caps_Cap.typeRef)
-    ccState.localRoots.getOrElseUpdate(owner, newRoot)
-
   /** The outermost symbol owned by both `sym` and `other`. if none exists
    *  since the owning scopes of `sym` and `other` are not nested, invoke
    *  `onConflict` to return a symbol.
@@ -342,3 +370,21 @@ extension (tp: AnnotatedType)
   def isBoxed(using Context): Boolean = tp.annot match
     case ann: CaptureAnnotation => ann.boxed
     case _ => false
+
+/** An extractor for `caps.reachCapability(ref)`, which is used to express a reach
+ *  capability as a tree in a @retains annotation.
+ */
+object ReachCapabilityApply:
+  def unapply(tree: Apply)(using Context): Option[Tree] = tree match
+    case Apply(reach, arg :: Nil) if reach.symbol == defn.Caps_reachCapability => Some(arg)
+    case _ => None
+
+/** An extractor for `ref @annotation.internal.reachCapability`, which is used to express
+ *  the reach capability `ref*` as a type.
+ */
+object ReachCapability:
+  def unapply(tree: AnnotatedType)(using Context): Option[SingletonCaptureRef] = tree match
+    case AnnotatedType(parent: SingletonCaptureRef, ann)
+    if ann.symbol == defn.ReachCapabilityAnnot => Some(parent)
+    case _ => None
+

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

@@ -77,19 +77,8 @@ sealed abstract class CaptureSet extends Showable:
 
   /** Does this capture set contain the root reference `cap` as element? */
   final def isUniversal(using Context) =
-    elems.exists(_.isUniversalRootCapability)
-
-  /** Does this capture set contain the root reference `cap` as element? */
-  final def containsRoot(using Context) =
     elems.exists(_.isRootCapability)
 
-  /** Does this capture set disallow an addiiton of `cap`, whereas it
-   *  might allow an addition of a local root?
-   */
-  final def disallowsUniversal(using Context) =
-    if isConst then !isUniversal && elems.exists(_.isLocalRootCapability)
-    else asVar.noUniversal
-
   /** Try to include an element in this capture set.
    *  @param elem    The element to be added
    *  @param origin  The set that originated the request, or `empty` if the request came from outside.
@@ -154,39 +143,21 @@ sealed abstract class CaptureSet extends Showable:
     cs.addDependent(this)(using ctx, UnrecordedState)
     this
 
-  extension (x: CaptureRef)(using Context)
-
-    /* x subsumes y if one of the following is true:
-    *   - x is the same as y,
-    *   - x is a this reference and y refers to a field of x
-    *   - x is a super root of y
-    */
-    private def subsumes(y: CaptureRef) =
+  /** x subsumes x
+   *   this subsumes this.f
+   *   x subsumes y  ==>  x* subsumes y
+   *   x subsumes y  ==>  x* subsumes y*
+   */
+  extension (x: CaptureRef)
+     private def subsumes(y: CaptureRef)(using Context): Boolean =
       (x eq y)
-      || x.isSuperRootOf(y)
+      || x.isRootCapability
       || y.match
-          case y: TermRef => y.prefix eq x
+          case y: TermRef => !y.isReach && (y.prefix eq x)
+          case _ => false
+      || x.match
+          case ReachCapability(x1) => x1.subsumes(y.stripReach)
           case _ => false
-
-    /** x <:< cap,   cap[x] <:< cap
-     *  cap[y] <:< cap[x] if y encloses x
-     *  y <:< cap[x] if y's level owner encloses x's local root owner
-     */
-    private def isSuperRootOf(y: CaptureRef): Boolean = x match
-      case x: TermRef =>
-        x.isUniversalRootCapability
-        || x.isLocalRootCapability && !y.isUniversalRootCapability && {
-          val xowner = x.localRootOwner
-          y match
-            case y: TermRef =>
-              xowner.isContainedIn(y.symbol.levelOwner)
-            case y: ThisType =>
-              xowner.isContainedIn(y.cls)
-            case _ =>
-              false
-        }
-      case _ => false
-  end extension
 
   /** {x} <:< this   where <:< is subcapturing, but treating all variables
    *                 as frozen.
@@ -210,7 +181,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(elem => elem.subsumes(x) || elem.isRootCapability)
+      elems.exists(_.subsumes(x))
       || !x.isRootCapability
         && {
           val elems = x.captureSetOfInfo.elems
@@ -516,7 +487,7 @@ object CaptureSet:
       else
         //if id == 34 then assert(!elem.isUniversalRootCapability)
         elems += elem
-        if elem.isUniversalRootCapability then
+        if elem.isRootCapability then
           rootAddedHandler()
         newElemAddedHandler(elem)
         // assert(id != 5 || elems.size != 3, this)
@@ -527,19 +498,17 @@ object CaptureSet:
           res.addToTrace(this)
 
     private def levelOK(elem: CaptureRef)(using Context): Boolean =
-      if elem.isUniversalRootCapability then !noUniversal
+      if elem.isRootCapability then !noUniversal
       else elem match
-        case elem: TermRef =>
-          if levelLimit.exists then
-            var sym = elem.symbol
-            if sym.isLevelOwner then sym = sym.owner
-            levelLimit.isContainedIn(sym.levelOwner)
-          else true
-        case elem: ThisType =>
-          if levelLimit.exists then
-            levelLimit.isContainedIn(elem.cls.levelOwner)
-          else true
-        case elem: TermParamRef =>
+        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 ReachCapability(elem1) =>
+          levelOK(elem1)
+        case _ =>
           true
 
     def addDependent(cs: CaptureSet)(using Context, VarState): CompareResult =
@@ -567,10 +536,9 @@ object CaptureSet:
      *  of this set. The universal set {cap} is a sound fallback.
      */
     final def upperApprox(origin: CaptureSet)(using Context): CaptureSet =
-      if isConst then this
-      else if elems.exists(_.isRootCapability) then
-        CaptureSet(elems.filter(_.isRootCapability).toList*)
-      else if computingApprox then
+      if isConst then
+        this
+      else if elems.exists(_.isRootCapability) || computingApprox then
         universal
       else
         computingApprox = true
@@ -633,6 +601,13 @@ 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):
@@ -1037,6 +1012,8 @@ 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 ReachCapability(ref1) => deepCaptureSet(ref1.widen)
+      .showing(i"Deep capture set of $ref: ${ref1.widen} = $result", capt)
     case _ => ofType(ref.underlying, followResult = true)
 
   /** Capture set of a type */
@@ -1078,6 +1055,16 @@ object CaptureSet:
     recur(tp)
       .showing(i"capture set of $tp = $result", captDebug)
 
+  private def deepCaptureSet(tp: Type)(using Context): CaptureSet =
+    val collect = new TypeAccumulator[CaptureSet]:
+      def apply(cs: CaptureSet, t: Type) = t.dealias match
+        case t @ CapturingType(p, cs1) =>
+          val cs2 = apply(cs, p)
+          if variance > 0 then cs2 ++ cs1 else cs2
+        case _ =>
+          foldOver(cs, t)
+    collect(CaptureSet.empty, tp)
+
   private val ShownVars: Property.Key[mutable.Set[Var]] = Property.Key()
 
   /** Perform `op`. Under -Ycc-debug, collect and print info about all variables reachable
@@ -1115,7 +1102,7 @@ object CaptureSet:
     override def toAdd(using Context) =
       for CompareResult.LevelError(cs, ref) <- ccState.levelError.toList yield
         ccState.levelError = None
-        if ref.isUniversalRootCapability then
+        if ref.isRootCapability then
           i"""
             |
             |Note that the universal capability `cap`