Polishings

Author: odersky

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

@@ -232,7 +232,9 @@ extension (tp: Type)
       case tp @ ReachCapability(_) =>
         tp.singletonCaptureSet
       case ReadOnlyCapability(ref) =>
-        ref.deepCaptureSet(includeTypevars)
+        val refDcs = ref.deepCaptureSet(includeTypevars)
+        if refDcs.isConst then CaptureSet(refDcs.elems.map(_.readOnly))
+        else refDcs // this case should not happen for correct programs
       case tp: SingletonCaptureRef if tp.isTrackableRef =>
         tp.reach.singletonCaptureSet
       case _ =>
@@ -279,17 +281,19 @@ extension (tp: Type)
     case _ =>
       tp
 
-  /** The first element of this path type */
+  /** The first element of this path type. Note that class parameter references
+   *  are of the form this.C but their pathroot is still this.C, not this.
+   */
   final def pathRoot(using Context): Type = tp.dealias match
     case tp1: TermRef if tp1.symbol.maybeOwner.isClass => tp1.prefix.pathRoot
     case tp1: TypeRef if !tp1.symbol.is(Param) => tp1.prefix.pathRoot
     case tp1 => tp1
 
   /** The first element of a path type, but stop at references extending
-   *  SharableCapability
+   *  SharedCapability.
    */
   final def pathRootOrShared(using Context): Type =
-    if tp.derivesFrom(defn.Caps_SharedCapability) then tp
+    if tp.derivesFromSharedCapability then tp
     else tp.dealias match
       case tp1: TermRef if tp1.symbol.maybeOwner.isClass => tp1.prefix.pathRoot
       case tp1: TypeRef if !tp1.symbol.is(Param) => tp1.prefix.pathRoot
@@ -427,6 +431,7 @@ extension (tp: Type)
 
   def derivesFromCapability(using Context): Boolean = derivesFromCapTrait(defn.Caps_Capability)
   def derivesFromMutable(using Context): Boolean = derivesFromCapTrait(defn.Caps_Mutable)
+  def derivesFromSharedCapability(using Context): Boolean = derivesFromCapTrait(defn.Caps_SharedCapability)
 
   /** Drop @retains annotations everywhere */
   def dropAllRetains(using Context): Type = // TODO we should drop retains from inferred types before unpickling
@@ -466,6 +471,11 @@ extension (tp: Type)
    *  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.
+   *
+   *  Reach capabilities cannot wrap read-only capabilities or maybe capabilities.
+   *  We have
+   *      (x.rd).reach = x*.rd
+   *      (x.rd)?      = (x*)?
    */
   def reach(using Context): CaptureRef = tp match
     case tp @ AnnotatedType(tp1: CaptureRef, annot)
@@ -483,6 +493,10 @@ extension (tp: Type)
   /** If `x` is a capture ref, its read-only capability `x.rd`, represented internally
    *  as `x @readOnlyCapability`. We have {x.rd} <: {x}. If `x` is a reach capability `y*`,
    *  then its read-only version is `x.rd*`.
+   *
+   *  Read-only capabilities cannot wrap maybe capabilities
+   *  but they can wrap reach capabilities. We have
+   *      (x?).readOnly = (x.rd)?
    */
   def readOnly(using Context): CaptureRef = tp match
     case tp @ AnnotatedType(tp1: CaptureRef, annot)

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

@@ -100,19 +100,25 @@ trait CaptureRef extends TypeProxy, ValueType:
   /** Is this reference the generic root capability `cap` or a Fresh.Cap instance? */
   final def isCapOrFresh(using Context): Boolean = isCap || isFresh
 
-  /** Is this reference one the generic root capabilities `cap` or `cap.rd` ? */
+  /** Is this reference one of the generic root capabilities `cap` or `cap.rd` ? */
   final def isRootCapability(using Context): Boolean = this match
     case ReadOnlyCapability(tp1) => tp1.isCapOrFresh
     case _ => isCapOrFresh
 
-  /** Is this reference capability that does not derive from another capability ? */
+  /** Is this reference a capability that does not derive from another capability?
+   *  Includes read-only versions of maximal capabilities.
+   */
   final def isMaxCapability(using Context): Boolean = this match
     case tp: TermRef => tp.isCap || tp.info.derivesFrom(defn.Caps_Exists)
     case tp: TermParamRef => tp.underlying.derivesFrom(defn.Caps_Exists)
     case Fresh.Cap(_) => true
     case ReadOnlyCapability(tp1) => tp1.isMaxCapability
     case _ => false
 
+  /** An exclusive capability is a capability that derives
+   *  indirectly from a maximal capability without goinh through
+   *  a read-only capability first.
+   */
   final def isExclusive(using Context): Boolean =
     !isReadOnly && (isMaxCapability || captureSetOfInfo.isExclusive)
 
@@ -159,8 +165,6 @@ trait CaptureRef extends TypeProxy, ValueType:
    *   X: CapSet^c1...CapSet^c2, (CapSet^c1) subsumes y  ==>  X subsumes y
    *   Y: CapSet^c1...CapSet^c2, x subsumes (CapSet^c2)  ==>  x subsumes Y
    *   Contains[X, y]  ==>  X subsumes y
-   *
-   *   TODO: Move to CaptureSet
    */
   final def subsumes(y: CaptureRef)(using ctx: Context, vs: VarState = VarState.Separate): Boolean =
 
@@ -239,7 +243,7 @@ trait CaptureRef extends TypeProxy, ValueType:
   end subsumes
 
   /** This is a maximal capabaility that subsumes `y` in given context and VarState.
-   *  @param canAddHidden  If true we allow maximal capabilties to subsume all other capabilities.
+   *  @param canAddHidden  If true we allow maximal capabilities to subsume all other capabilities.
    *                       We add those capabilities to the hidden set if this is Fresh.Cap
    *                       If false we only accept `y` elements that are already in the
    *                       hidden set of this Fresh.Cap. The idea is that in a VarState that

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

@@ -636,7 +636,8 @@ object CaptureSet:
      */
     def solve()(using Context): Unit =
       if !isConst then
-        val approx = upperApprox(empty).map(Fresh.FromCap(NoSymbol).inverse)
+        val approx = upperApprox(empty)
+          .map(Fresh.FromCap(NoSymbol).inverse)    // Fresh.Cap --> cap
           .showing(i"solve $this = $result", capt)
         //println(i"solving var $this $approx ${approx.isConst} deps = ${deps.toList}")
         val newElems = approx.elems -- elems
@@ -1139,6 +1140,7 @@ object CaptureSet:
 
   /** A template for maps on capabilities where f(c) <: c and f(f(c)) = c */
   private abstract class NarrowingCapabilityMap(using Context) extends BiTypeMap:
+
     def mapRef(ref: CaptureRef): CaptureRef
 
     def apply(t: Type) = t match

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

@@ -519,8 +519,7 @@ class CheckCaptures extends Recheck, SymTransformer:
     def includeCallCaptures(sym: Symbol, resType: Type, tree: Tree)(using Context): Unit = resType match
       case _: MethodOrPoly => // wait until method is fully applied
       case _ =>
-        if sym.exists then
-          if curEnv.isOpen then markFree(capturedVars(sym), tree)
+        if sym.exists && curEnv.isOpen then markFree(capturedVars(sym), tree)
 
     /** Under the sealed policy, disallow the root capability in type arguments.
      *  Type arguments come either from a TypeApply node or from an AppliedType
@@ -556,16 +555,21 @@ class CheckCaptures extends Recheck, SymTransformer:
           if param.isUseParam then markFree(arg.nuType.deepCaptureSet, errTree)
     end disallowCapInTypeArgs
 
+    /** Rechecking idents involves:
+     *   - adding call captures for idents referring to methods
+     *   - marking as free the identifier with any selections or .rd
+     *     modifiers implied by the expected type
+     */
     override def recheckIdent(tree: Ident, pt: Type)(using Context): Type =
       val sym = tree.symbol
       if sym.is(Method) then
         // If ident refers to a parameterless method, charge its cv to the environment
         includeCallCaptures(sym, sym.info, tree)
       else if !sym.isStatic then
-        // Otherwise charge its symbol, but add all selections implied by the e
-        // expected type `pt`.
-        // Example: If we have `x` and the expected type says we select that with `.a.b`,
-        // we charge `x.a.b` instead of `x`.
+        // Otherwise charge its symbol, but add all selections and also any `.rd`
+        // modifier implied by the expected type `pt`.
+        // Example: If we have `x` and the expected type says we select that with `.a.b`
+        // where `b` is a read-only method, we charge `x.a.b.rd` instead of `x`.
         def addSelects(ref: TermRef, pt: Type): CaptureRef = pt match
           case pt: PathSelectionProto if ref.isTracked =>
             if pt.sym.isReadOnlyMethod then
@@ -582,7 +586,8 @@ class CheckCaptures extends Recheck, SymTransformer:
       super.recheckIdent(tree, pt)
 
     /** The expected type for the qualifier of a selection. If the selection
-     *  could be part of a capabaility path, we return a PathSelectionProto.
+     *  could be part of a capability path or is a a read-only method, we return
+     *  a PathSelectionProto.
      */
     override def selectionProto(tree: Select, pt: Type)(using Context): Type =
       val sym = tree.symbol
@@ -616,6 +621,9 @@ class CheckCaptures extends Recheck, SymTransformer:
           }
         case _ => denot
 
+      // Don't allow update methods to be called unless the qualifier captures
+      // contain an exclusive referenece. TODO This should probabkly rolled into
+      // qualifier logic once we have it.
       if tree.symbol.isUpdateMethod && !qualType.captureSet.isExclusive then
         report.error(
             em"""cannot call update ${tree.symbol} from $qualType,
@@ -651,8 +659,8 @@ class CheckCaptures extends Recheck, SymTransformer:
           selType
     }//.showing(i"recheck sel $tree, $qualType = $result")
 
-    /** Hook for massaging a function before it is applied. Copies all @use annotations
-     *  on method parameter symbols to the corresponding paramInfo types.
+    /** Hook for massaging a function before it is applied. Copies all @use and @consume
+     *  annotations on method parameter symbols to the corresponding paramInfo types.
      */
     override def prepareFunction(funtpe: MethodType, meth: Symbol)(using Context): MethodType =
       val paramInfosWithUses =
@@ -682,7 +690,8 @@ class CheckCaptures extends Recheck, SymTransformer:
         includeCallCaptures(meth, res, tree)
         res
 
-    /** Recheck argument, and, if formal parameter carries a `@use`,
+    /** Recheck argument against a "freshened" version of `formal` where toplevel `cap`
+     *  occurrences are replaced by `Fresh.Cap`. Also, if formal parameter carries a `@use`,
      *  charge the deep capture set of the actual argument to the environment.
      */
     protected override def recheckArg(arg: Tree, formal: Type)(using Context): Type =
@@ -773,16 +782,21 @@ class CheckCaptures extends Recheck, SymTransformer:
 
       /** First half of result pair:
        *  Refine the type of a constructor call `new C(t_1, ..., t_n)`
-       *  to C{val x_1: T_1, ..., x_m: T_m} where x_1, ..., x_m are the tracked
-       *  parameters of C and T_1, ..., T_m are the types of the corresponding arguments.
+       *  to C{val x_1: @refineOverride T_1, ..., x_m: @refineOverride T_m}
+       *  where x_1, ..., x_m are the tracked parameters of C and
+       *  T_1, ..., T_m are the types of the corresponding arguments. The @refineOveride
+       *  annotations avoid problematic intersections of capture sets when those
+       *  parameters are selected.
        *
        *  Second half: union of initial capture set and all capture sets of arguments
-       *  to tracked parameters.
+       *  to tracked parameters. The initial capture set `initCs` is augmented with
+       *   - Fresh.Cap    if `core` extends Mutable
+       *   - Fresh.Cap.rd if `core` extends Capability
        */
       def addParamArgRefinements(core: Type, initCs: CaptureSet): (Type, CaptureSet) =
         var refined: Type = core
         var allCaptures: CaptureSet =
-          if core.derivesFromMutable then CaptureSet.fresh()
+          if core.derivesFromMutable then initCs ++ CaptureSet.fresh()
           else if core.derivesFromCapability then initCs ++ Fresh.Cap().readOnly.singletonCaptureSet
           else initCs
         for (getterName, argType) <- mt.paramNames.lazyZip(argTypes) do
@@ -1488,7 +1502,7 @@ class CheckCaptures extends Recheck, SymTransformer:
     /** If actual is a capturing type T^C extending Mutable, and expected is an
      *  unboxed non-singleton value type not extending mutable, narrow the capture
      *  set `C` to `ro(C)`.
-     *  The unboxed condition ensures that the expected is not a type variable
+     *  The unboxed condition ensures that the expected type is not a type variable
      *  that's upper bounded by a read-only type. In this case it would not be sound
      *  to narrow to the read-only set, since that set can be propagated
      *  by the type variable instantiation.
@@ -1514,9 +1528,9 @@ class CheckCaptures extends Recheck, SymTransformer:
         actual
       else
         val improvedVAR = improveCaptures(actual.widen.dealiasKeepAnnots, actual)
-        val improvedRO = improveReadOnly(improvedVAR, expected)
+        val improved = improveReadOnly(improvedVAR, expected)
         val adapted = adaptBoxed(
-            improvedRO.withReachCaptures(actual), expected, tree,
+            improved.withReachCaptures(actual), expected, tree,
             covariant = true, alwaysConst = false, boxErrors)
         if adapted eq improvedVAR // no .rd improvement, no box-adaptation
         then actual               // might as well use actual instead of improved widened
@@ -1563,17 +1577,19 @@ class CheckCaptures extends Recheck, SymTransformer:
 
         /** Check that overrides don't change the @use or @consume status of their parameters */
         override def additionalChecks(member: Symbol, other: Symbol)(using Context): Unit =
-          def fail(msg: String) =
-            report.error(
-              OverrideError(msg, self, member, other, self.memberInfo(member), self.memberInfo(other)),
-              if member.owner == clazz then member.srcPos else clazz.srcPos)
           for
             (params1, params2) <- member.rawParamss.lazyZip(other.rawParamss)
             (param1, param2) <- params1.lazyZip(params2)
           do
             def checkAnnot(cls: ClassSymbol) =
               if param1.hasAnnotation(cls) != param2.hasAnnotation(cls) then
-                fail(i"has a parameter ${param1.name} with different @${cls.name} status than the corresponding parameter in the overridden definition")
+                report.error(
+                  OverrideError(
+                      i"has a parameter ${param1.name} with different @${cls.name} status than the corresponding parameter in the overridden definition",
+                      self, member, other, self.memberInfo(member), self.memberInfo(other)
+                    ),
+                  if member.owner == clazz then member.srcPos else clazz.srcPos)
+
             checkAnnot(defn.UseAnnot)
             checkAnnot(defn.ConsumeAnnot)
       end OverridingPairsCheckerCC

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

@@ -252,7 +252,7 @@ object Existential:
       tp1.derivedAnnotatedType(toCap(parent), ann)
     case _ => tp
 
-  /** Map existentials at the top-level and in all nested result types to `cap`
+  /** Map existentials at the top-level and in all nested result types to `Fresh.Cap`
    */
   def toCapDeeply(tp: Type)(using Context): Type = tp.dealiasKeepAnnots match
     case Existential(boundVar, unpacked) =>

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

@@ -16,11 +16,16 @@ import util.SimpleIdentitySet.empty
 import CaptureSet.{Refs, emptySet, NarrowingCapabilityMap}
 import dotty.tools.dotc.util.SimpleIdentitySet
 
-/** Handling fresh in CC:
-
-*/
+/** A module for handling Fresh types. Fresh.Cap instances are top type that keep
+ *  track of what they hide when capabilities get widened by subsumption to fresh.
+ *  The module implements operations to convert between regular caps.cap and
+ *  Fresh.Cap instances. Fresh.Cap is encoded as `caps.cap @freshCapability(...)` where
+ *  `freshCapability(...)` is a special kind of annotation of type `Fresh.Annot`
+ *  that contains a hidden set.
+ */
 object Fresh:
 
+  /** The annotation of a Fresh.Cap instance */
   case class Annot(hidden: CaptureSet.HiddenSet) extends Annotation:
     override def symbol(using Context) = defn.FreshCapabilityAnnot
     override def tree(using Context) = New(symbol.typeRef, Nil)
@@ -32,13 +37,17 @@ object Fresh:
       case _ => false
   end Annot
 
+  /** The initial elements (either 0 or 1) of a hidden set created for given `owner`.
+   *  If owner `x` is a trackable this is `x*` if reach` is true, or `x` otherwise.
+   */
   private def ownerToHidden(owner: Symbol, reach: Boolean)(using Context): Refs =
     val ref = owner.termRef
     if reach then
       if ref.isTrackableRef then SimpleIdentitySet(ref.reach) else emptySet
     else
       if ref.isTracked then SimpleIdentitySet(ref) else emptySet
 
+  /** An extractor for "fresh" capabilities */
   object Cap:
 
     def apply(initialHidden: Refs = emptySet)(using Context): CaptureRef =

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

@@ -411,7 +411,7 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
     def currentOwner = role.dclSym.orElse(ctx.owner)
     for hiddenRef <- prune(refsToCheck, tpe, role) do
       val proot = hiddenRef.pathRootOrShared
-      if !proot.widen.derivesFrom(defn.Caps_SharedCapability) then
+      if !proot.widen.derivesFromSharedCapability then
         proot match
           case ref: TermRef =>
             val refSym = ref.symbol
@@ -448,7 +448,7 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
     role match
       case _: TypeRole.Argument | _: TypeRole.Qualifier =>
         for ref <- refsToCheck do
-          if !ref.pathRootOrShared.derivesFrom(defn.Caps_SharedCapability) then
+          if !ref.pathRootOrShared.derivesFromSharedCapability then
             consumed.put(ref, pos)
       case _ =>
   end checkConsumedRefs

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

@@ -345,10 +345,18 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
           parent
         case _ => tp
 
+      /** Check that types extending SharedCapability don't have a `cap` in their capture set.
+       *  TODO This is not enough.
+       *  We need to also track that we cannot get exclusive capabilities in paths
+       *  where some prefix derives from SharedCapability. Also, can we just
+       *  exclude `cap`, or do we have to extend this to all exclusive capabilties?
+       *  The problem is that we know what is exclusive in general only after capture
+       *  checking, not before.
+       */
       def checkSharedOK(tp: Type): tp.type =
         tp match
           case CapturingType(parent, refs)
-          if refs.isUniversal && parent.derivesFrom(defn.Caps_SharedCapability) =>
+          if refs.isUniversal && parent.derivesFromSharedCapability =>
             fail(em"$tp extends SharedCapability, so it cannot capture `cap`")
           case _ =>
         tp

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

@@ -1118,8 +1118,6 @@ class Definitions {
   @tu lazy val SilentAnnots: Set[Symbol] =
     Set(InlineParamAnnot, ErasedParamAnnot, RefineOverrideAnnot)
 
-  @tu lazy val ccParamOnlyAnnotations: Set[Symbol] = Set(UseAnnot, ConsumeAnnot)
-
   // A list of annotations that are commonly used to indicate that a field/method argument or return
   // type is not null. These annotations are used by the nullification logic in JavaNullInterop to
   // improve the precision of type nullification.

compiler/src/dotty/tools/dotc/typer/Checking.scala

@@ -606,7 +606,7 @@ object Checking {
     if sym.isWrappedToplevelDef && !sym.isType && sym.flags.is(Infix, butNot = Extension) then
       fail(ModifierNotAllowedForDefinition(Flags.Infix, s"A top-level ${sym.showKind} cannot be infix."))
     if sym.isUpdateMethod && !sym.owner.derivesFrom(defn.Caps_Mutable) then
-      fail(em"Update methods can only be used as members of classes deriving from the `Mutable` trait")
+      fail(em"Update methods can only be used as members of classes extending the `Mutable` trait")
     checkApplicable(Erased,
       !sym.is(Lazy, butNot = Given)
       && !sym.isMutableVarOrAccessor