Go back towards a pure capability system

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

@@ -525,8 +525,8 @@ object untpd extends Trees.Instance[Untyped] with UntypedTreeInfo {
   def makeRetaining(parent: Tree, refs: List[Tree], annotName: TypeName)(using Context): Annotated =
     Annotated(parent, New(scalaAnnotationDot(annotName), List(refs)))
 
-  def makeCapsOf(id: Ident)(using Context): Tree =
-    TypeApply(Select(scalaDot(nme.caps), nme.capsOf), id :: Nil)
+  def makeCapsOf(tp: Tree)(using Context): Tree =
+    TypeApply(Select(scalaDot(nme.caps), nme.capsOf), tp :: Nil)
 
   def makeCapsBound()(using Context): Tree =
     makeRetaining(

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

@@ -194,7 +194,8 @@ extension (tp: Type)
       true
     case tp: TermRef =>
       ((tp.prefix eq NoPrefix)
-      || tp.symbol.is(ParamAccessor) && tp.prefix.isThisTypeOf(tp.symbol.owner)
+      || tp.symbol.isField && !tp.symbol.isStatic && (
+        tp.prefix.isThisTypeOf(tp.symbol.owner) || tp.prefix.isTrackableRef)
       || tp.isRootCapability
       ) && !tp.symbol.isOneOf(UnstableValueFlags)
     case tp: TypeRef =>
@@ -221,19 +222,22 @@ extension (tp: Type)
     case tp: SingletonCaptureRef => tp.captureSetOfInfo
     case _ => CaptureSet.ofType(tp, followResult = false)
 
-  /** The deep capture set of a type.
-   *  For singleton capabilities `x` and reach capabilities `x*`, this is `{x*}`, provided
-   *  the underlying capture set resulting from traversing the type is non-empty.
-   *  For other types this is the union of all covariant capture sets embedded
-   *  in the type, as computed by `CaptureSet.ofTypeDeeply`.
+  /** The deep capture set of a type. This is by default the union of all
+   *  covariant capture sets embedded in the widened type, as computed by
+   *  `CaptureSet.ofTypeDeeply`. If that set is nonempty, and the type is
+   *  a singleton capability `x` or a reach capability `x*`, the deep capture
+   *  set can be narrowed to`{x*}`.
    */
   def deepCaptureSet(using Context): CaptureSet =
-    val dcs = CaptureSet.ofTypeDeeply(tp)
-    if dcs.isAlwaysEmpty then dcs
+    val dcs = CaptureSet.ofTypeDeeply(tp.widen.stripCapturing)
+    if dcs.isAlwaysEmpty then tp.captureSet
     else tp match
-      case tp @ ReachCapability(_) => tp.singletonCaptureSet
-      case tp: SingletonCaptureRef => tp.reach.singletonCaptureSet
-      case _ => dcs
+      case tp @ ReachCapability(_) =>
+        tp.singletonCaptureSet
+      case tp: SingletonCaptureRef if tp.isTrackableRef =>
+        tp.reach.singletonCaptureSet
+      case _ =>
+        tp.captureSet ++ dcs
 
   /** A type capturing `ref` */
   def capturing(ref: CaptureRef)(using Context): Type =
@@ -273,6 +277,28 @@ extension (tp: Type)
     case _ =>
       tp
 
+  /** The first element of this path type */
+  final def pathRoot(using Context): Type = tp.dealias match
+    case tp1: NamedType if tp1.symbol.owner.isClass => tp1.prefix.pathRoot
+    case tp1 @ ReachCapability(tp2) => tp2.pathRoot
+    case _ => tp
+
+  /** If this part starts with `C.this`, the class `C`.
+   *  Otherwise, if it starts with a reference `r`, `r`'s owner.
+   *  Otherwise NoSymbol.
+   */
+  final def pathOwner(using Context): Symbol = pathRoot match
+    case tp1: NamedType => tp1.symbol.owner
+    case tp1: ThisType => tp1.cls
+    case _ => NoSymbol
+
+  final def isParamPath(using Context): Boolean = tp.dealias match
+    case tp1: NamedType =>
+      tp1.prefix match
+        case _: ThisType | NoPrefix => tp1.symbol.isOneOf(Param | ParamAccessor)
+        case prefix => prefix.isParamPath
+    case _ => false
+
   /** If this is a unboxed capturing type with nonempty capture set, its boxed version.
    *  Or, if type is a TypeBounds of capturing types, the version where the bounds are boxed.
    *  The identity for all other types.
@@ -468,29 +494,23 @@ extension (tp: Type)
     end CheckContraCaps
 
     object narrowCaps extends TypeMap:
-      /** Has the variance been flipped at this point? */
-      private var isFlipped: Boolean = false
-
       def apply(t: Type) =
-        val saved = isFlipped
-        try
-          if variance <= 0 then isFlipped = true
-          t.dealias match
-            case t1 @ CapturingType(p, cs) if cs.isUniversal && !isFlipped =>
-              t1.derivedCapturingType(apply(p), ref.reach.singletonCaptureSet)
-            case t1 @ FunctionOrMethod(args, res @ Existential(_, _))
-            if args.forall(_.isAlwaysPure) =>
-              // Also map existentials in results to reach capabilities if all
-              // preceding arguments are known to be always pure
-              apply(t1.derivedFunctionOrMethod(args, Existential.toCap(res)))
-            case Existential(_, _) =>
-              t
-            case _ => t match
-              case t @ CapturingType(p, cs) =>
-                t.derivedCapturingType(apply(p), cs) // don't map capture set variables
-              case t =>
-                mapOver(t)
-        finally isFlipped = saved
+        if variance <= 0 then t
+        else t.dealiasKeepAnnots match
+          case t @ CapturingType(p, cs) if cs.isUniversal =>
+            t.derivedCapturingType(apply(p), ref.reach.singletonCaptureSet)
+          case t @ AnnotatedType(parent, ann) =>
+            // Don't map annotations, which includes capture sets
+            t.derivedAnnotatedType(this(parent), ann)
+          case t @ FunctionOrMethod(args, res @ Existential(_, _))
+          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)))
+          case Existential(_, _) =>
+            t
+          case _ =>
+            mapOver(t)
     end narrowCaps
 
     ref match
@@ -507,6 +527,14 @@ extension (tp: Type)
       case _ =>
         tp
 
+  /** Add implied captures as defined by `CaptureSet.addImplied`. */
+  def withImpliedCaptures(using Context): Type =
+    if tp.isValueType && !tp.isAlwaysPure then
+      val implied = CaptureSet.addImplied()(CaptureSet.empty, tp)
+      if !implied.isAlwaysEmpty then capt.println(i"Add implied $implied to $tp")
+      tp.capturing(implied)
+    else tp
+
   def level(using Context): Level =
     tp match
     case tp: TermRef => tp.symbol.ccLevel
@@ -639,8 +667,8 @@ object CapsOfApply:
 class AnnotatedCapability(annot: Context ?=> ClassSymbol):
   def apply(tp: Type)(using Context) =
     AnnotatedType(tp, Annotation(annot, util.Spans.NoSpan))
-  def unapply(tree: AnnotatedType)(using Context): Option[SingletonCaptureRef] = tree match
-    case AnnotatedType(parent: SingletonCaptureRef, ann) if ann.symbol == annot => Some(parent)
+  def unapply(tree: AnnotatedType)(using Context): Option[CaptureRef] = tree match
+    case AnnotatedType(parent: CaptureRef, ann) if ann.symbol == annot => Some(parent)
     case _ => None
 
 /** An extractor for `ref @annotation.internal.reachCapability`, which is used to express

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

@@ -61,18 +61,19 @@ trait CaptureRef extends TypeProxy, ValueType:
     case tp: TermParamRef => tp.underlying.derivesFrom(defn.Caps_Exists)
     case _ => false
 
-  /** Normalize reference so that it can be compared with `eq` for equality */
-  final def normalizedRef(using Context): CaptureRef = this match
-    case tp @ AnnotatedType(parent: CaptureRef, annot) if tp.isTrackableRef =>
-      tp.derivedAnnotatedType(parent.normalizedRef, annot)
-    case tp: TermRef if tp.isTrackableRef =>
-      tp.symbol.termRef
-    case _ => this
+  // With the support of pathes, we don't need to normalize the `TermRef`s anymore.
+  // /** Normalize reference so that it can be compared with `eq` for equality */
+  // final def normalizedRef(using Context): CaptureRef = this match
+  //   case tp @ AnnotatedType(parent: CaptureRef, annot) if tp.isTrackableRef =>
+  //     tp.derivedAnnotatedType(parent.normalizedRef, annot)
+  //   case tp: TermRef if tp.isTrackableRef =>
+  //     tp.symbol.termRef
+  //   case _ => this
 
   /** The capture set consisting of exactly this reference */
   final def singletonCaptureSet(using Context): CaptureSet.Const =
     if mySingletonCaptureSet == null then
-      mySingletonCaptureSet = CaptureSet(this.normalizedRef)
+      mySingletonCaptureSet = CaptureSet(this)
     mySingletonCaptureSet.uncheckedNN
 
   /** The capture set of the type underlying this reference */
@@ -97,27 +98,45 @@ trait CaptureRef extends TypeProxy, ValueType:
    *   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
+   *   TODO: Document path cases
    */
   final def subsumes(y: CaptureRef)(using Context): Boolean =
+
+    def subsumingRefs(x: Type, y: Type): Boolean = x match
+      case x: CaptureRef => y match
+        case y: CaptureRef => x.subsumes(y)
+        case _ => false
+      case _ => false
+
+    def viaInfo(info: Type)(test: Type => Boolean): Boolean = info.match
+      case info: SingletonCaptureRef => test(info)
+      case info: AndType => test(info.tp1) || test(info.tp2)
+      case info: OrType => test(info.tp1) && test(info.tp2)
+      case _ => false
+
     (this eq y)
     || this.isRootCapability
     || y.match
         case y: TermRef =>
-          (y.prefix eq this)
-          || y.info.match
-              case y1: SingletonCaptureRef => this.subsumes(y1)
+            y.prefix.match
+              case ypre: CaptureRef =>
+                this.subsumes(ypre)
+                || this.match
+                    case x @ TermRef(xpre: CaptureRef, _) if x.symbol == y.symbol =>
+                      subsumingRefs(xpre, ypre) && subsumingRefs(ypre, xpre)
+                    case _ =>
+                      false
               case _ => false
+          || viaInfo(y.info)(subsumingRefs(this, _))
         case MaybeCapability(y1) => this.stripMaybe.subsumes(y1)
         case _ => false
     || this.match
         case ReachCapability(x1) => x1.subsumes(y.stripReach)
-        case x: TermRef =>
-          x.info match
-            case x1: SingletonCaptureRef => x1.subsumes(y)
-            case _ => false
+        case x: TermRef => viaInfo(x.info)(subsumingRefs(_, y))
         case x: TermParamRef => subsumesExistentially(x, y)
         case x: TypeRef => assumedContainsOf(x).contains(y)
         case _ => false
+  end subsumes
 
   def assumedContainsOf(x: TypeRef)(using Context): SimpleIdentitySet[CaptureRef] =
     CaptureSet.assumedContains.getOrElse(x, SimpleIdentitySet.empty)

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

@@ -374,7 +374,7 @@ object CaptureSet:
 
   def apply(elems: CaptureRef*)(using Context): CaptureSet.Const =
     if elems.isEmpty then empty
-    else Const(SimpleIdentitySet(elems.map(_.normalizedRef.ensuring(_.isTrackableRef))*))
+    else Const(SimpleIdentitySet(elems.map(_.ensuring(_.isTrackableRef))*))
 
   def apply(elems: Refs)(using Context): CaptureSet.Const =
     if elems.isEmpty then empty else Const(elems)
@@ -508,7 +508,11 @@ object CaptureSet:
         !noUniversal
       else elem match
         case elem: TermRef if level.isDefined =>
-          elem.symbol.ccLevel <= level
+          elem.prefix match
+            case prefix: CaptureRef =>
+              levelOK(prefix)
+            case _ =>
+              elem.symbol.ccLevel <= level
         case elem: ThisType if level.isDefined =>
           elem.cls.ccLevel.nextInner <= level
         case ReachCapability(elem1) =>
@@ -817,6 +821,10 @@ object CaptureSet:
         // If this is the union of a constant and a variable,
         // propagate `elem` to the variable part to avoid slack
         // between the operands and the union.
+        // TODO: This means there's no back-propagation to the operands
+        // of a union of two variables. That could be a source of unsoundness.
+        // Altermative would be to be conservatibe and back-propagate to one
+        // of the operands arbitrarily or even to both of them.
         if res.isOK && (origin ne cs1) && (origin ne cs2) then
           if cs1.isConst then cs2.tryInclude(elem, origin)
           else if cs2.isConst then cs1.tryInclude(elem, origin)
@@ -1060,10 +1068,43 @@ object CaptureSet:
     case ref: (TermRef | TermParamRef) if ref.isMaxCapability =>
       if ref.isTrackableRef then ref.singletonCaptureSet
       else CaptureSet.universal
-    case ReachCapability(ref1) => deepCaptureSet(ref1.widen)
+    case ReachCapability(ref1) => ref1.widen.deepCaptureSet
       .showing(i"Deep capture set of $ref: ${ref1.widen} = $result", capt)
     case _ => ofType(ref.underlying, followResult = true)
 
+  /** Add captures implied by a type. This means: if we have a contravarint, boxed
+   *  capability in a function parameter and the capability is either `cap`, or a
+   *  reach capability, or a capture set variable, add the same capability to the enclosing
+   *  function arrow. For instance `List[() ->{ops*} Unit] -> Unit` would become
+   *  `List[() ->{ops*} Unit] ->{ops*} Unit`. This is needed to make
+   *  the `delayedRunops*.scala` tests produce errors.
+   *  TODO: Investigate whether we can roll this into a widening rule like
+   *
+   *      List[() ->{cap} Unit] -> Unit <: List[() ->{ops*} Unit] ->{ops*} Unit
+   *
+   *  but not
+   *
+   *      List[() ->{cap} Unit] -> Unit <: List[() ->{ops*} Unit] -> Unit
+   *
+   *  It would mean that a reach capability can no longer be a subtype of `cap`.
+   */
+  class addImplied(using Context) extends TypeAccumulator[CaptureSet]:
+    var boundVars: Set[CaptureRef] = Set.empty
+    def isImplied(tp: CaptureRef) =
+      (tp.isRootCapability || tp.isReach || tp.derivesFrom(defn.Caps_CapSet))
+      && !boundVars.contains(tp.stripReach)
+    def apply(cs: CaptureSet, t: Type) = t match
+      case t @ CapturingType(parent, cs1) =>
+        val cs2 = this(cs, parent)
+        if variance <= 0 && t.isBoxed then cs2 ++ cs1.filter(isImplied)
+        else cs2
+      case t: MethodOrPoly =>
+        val saved = boundVars
+        boundVars ++= t.paramRefs.asInstanceOf[List[CaptureRef]]
+        try foldOver(cs, t) finally boundVars = saved
+      case _ =>
+        foldOver(cs, t)
+
   /** Capture set of a type */
   def ofType(tp: Type, followResult: Boolean)(using Context): CaptureSet =
     def recur(tp: Type): CaptureSet = trace(i"ofType $tp, ${tp.getClass} $followResult", show = true):
@@ -1111,17 +1152,25 @@ object CaptureSet:
 
   /** The deep capture set of a type is the union of all covariant occurrences of
    *  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.
    */
   def ofTypeDeeply(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 t @ Existential(_, _) =>
-          apply(cs, Existential.toCap(t))
-        case _ =>
-          foldOver(cs, t)
+      def apply(cs: CaptureSet, t: Type) =
+        if variance <= 0 then cs
+        else t.dealias match
+          case t @ CapturingType(p, cs1) =>
+            this(cs, p) ++ cs1
+          case t @ AnnotatedType(parent, ann) =>
+            this(cs, parent)
+          case t @ FunctionOrMethod(args, res @ Existential(_, _))
+          if args.forall(_.isAlwaysPure) =>
+            this(cs, Existential.toCap(res))
+          case t @ Existential(_, _) =>
+            cs
+          case _ =>
+            foldOver(cs, t)
     collect(CaptureSet.empty, tp)
 
   type AssumedContains = immutable.Map[TypeRef, SimpleIdentitySet[CaptureRef]]