Revise capability hierarchy and fix classifiers

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

@@ -152,10 +152,39 @@ object Capabilities:
     val hiddenSet = CaptureSet.HiddenSet(owner, this: @unchecked)
       // fails initialization check without the @unchecked
 
+    /** Is this fresh cap (definitely) classified? If that's the case, the
+     *  classifier cannot be changed anymore.
+     *  We need to distinguish `FreshCap`s that can still be classified from
+     *  ones that cannot. Once a `FreshCap` is part of a constant capture set,
+     *  it gets classified by the type that prefixes the set and that classification
+     *  cannot be changed anymore. But other `FreshCap`s are created as members of
+     *  variable sets and then their classification status is open and can be
+     *  constrained further.
+     */
+    private[Capabilities] var isClassified = false
+
     override def equals(that: Any) = that match
       case that: FreshCap => this eq that
       case _ => false
 
+    /** Is this fresh cap at the right level to be able to subsume `ref`?
+     */
+    def acceptsLevelOf(ref: Capability)(using Context): Boolean =
+      if ccConfig.useFreshLevels && !CCState.collapseFresh then
+        val refOwner = ref.levelOwner
+        refOwner.isStaticOwner || ccOwner.isContainedIn(refOwner)
+      else ref.core match
+        case ResultCap(_) | _: ParamRef => false
+        case _ => true
+
+    /** Classify this FreshCap as `cls`, provided `isClassified` is still false.
+     *  @param  freeze  Deterermines future `isClassified` state.
+     */
+    def adoptClassifier(cls: ClassSymbol, freeze: Boolean)(using Context): Unit =
+      if !isClassified then
+        hiddenSet.adoptClassifier(cls)
+        if freeze then isClassified = true
+
     def descr(using Context) =
       val originStr = origin match
         case Origin.InDecl(sym) if sym.exists =>
@@ -477,7 +506,7 @@ object Capabilities:
 
     def derivesFromCapability(using Context): Boolean = derivesFromCapTrait(defn.Caps_Capability)
     def derivesFromMutable(using Context): Boolean = derivesFromCapTrait(defn.Caps_Mutable)
-    def derivesFromSharable(using Context): Boolean = derivesFromCapTrait(defn.Caps_Sharable)
+    def derivesFromShared(using Context): Boolean = derivesFromCapTrait(defn.Caps_SharedCapability)
 
     /** The capture set consisting of exactly this reference */
     def singletonCaptureSet(using Context): CaptureSet.Const =
@@ -495,7 +524,11 @@ object Capabilities:
         def isProvisional = this.core match
           case core: TypeProxy => !core.underlying.exists || core.underlying.isProvisional
           case _ => false
-        if !isCaptureChecking || ctx.mode.is(Mode.IgnoreCaptures) || isProvisional then
+        if !ccConfig.cacheCaptureSetOfInfo
+            || !isCaptureChecking
+            || ctx.mode.is(Mode.IgnoreCaptures)
+            || isProvisional
+        then
           myCaptureSet = null
         else
           myCaptureSet = computed
@@ -524,7 +557,8 @@ object Capabilities:
           case Reach(_) =>
             captureSetOfInfo.transClassifiers
           case self: CoreCapability =>
-            joinClassifiers(toClassifiers(self.classifier), captureSetOfInfo.transClassifiers)
+            if self.derivesFromCapability then toClassifiers(self.classifier)
+            else captureSetOfInfo.transClassifiers
         if myClassifiers != UnknownClassifier then
           classifiersValid == currentId
       myClassifiers
@@ -534,7 +568,8 @@ object Capabilities:
       cls == defn.AnyClass
       || this.match
         case self: FreshCap =>
-          self.hiddenSet.tryClassifyAs(cls)
+          if self.isClassified then self.hiddenSet.classifier.derivesFrom(cls)
+          else self.hiddenSet.tryClassifyAs(cls)
         case self: RootCapability =>
           true
         case Restricted(_, cls1) =>
@@ -547,8 +582,8 @@ object Capabilities:
         case Reach(_) =>
           captureSetOfInfo.tryClassifyAs(cls)
         case self: CoreCapability =>
-          self.classifier.isSubClass(cls)
-          && captureSetOfInfo.tryClassifyAs(cls)
+          if self.derivesFromCapability then self.derivesFrom(cls)
+          else captureSetOfInfo.tryClassifyAs(cls)
 
     def isKnownClassifiedAs(cls: ClassSymbol)(using Context): Boolean =
       transClassifiers match
@@ -677,7 +712,7 @@ object Capabilities:
               case _ => true
 
           vs.ifNotSeen(this)(x.hiddenSet.elems.exists(_.subsumes(y)))
-          || levelOK
+          || x.acceptsLevelOf(y)
               && ( y.tryClassifyAs(x.hiddenSet.classifier)
                    || { capt.println(i"$y cannot be classified as $x"); false }
               )
@@ -686,7 +721,7 @@ object Capabilities:
         case x: ResultCap =>
           val result = y match
             case y: ResultCap => vs.unify(x, y)
-            case _ => y.derivesFromSharable
+            case _ => y.derivesFromShared
           if !result then
             TypeComparer.addErrorNote(CaptureSet.ExistentialSubsumesFailure(x, y))
           result
@@ -696,7 +731,7 @@ object Capabilities:
             case _: ResultCap => false
             case _: FreshCap if CCState.collapseFresh => true
             case _ =>
-              y.derivesFromSharable
+              y.derivesFromShared
               || canAddHidden && vs != VarState.HardSeparate && CCState.capIsRoot
         case Restricted(x1, cls) =>
           y.isKnownClassifiedAs(cls) && x1.maxSubsumes(y, canAddHidden)

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

@@ -378,7 +378,8 @@ 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_Sharable)
+  def derivesFromShared(using Context): Boolean = derivesFromCapTrait(defn.Caps_SharedCapability)
+  def derivesFromExclusive(using Context): Boolean = derivesFromCapTrait(defn.Caps_ExclusiveCapability)
 
   /** Drop @retains annotations everywhere */
   def dropAllRetains(using Context): Type = // TODO we should drop retains from inferred types before unpickling
@@ -401,9 +402,12 @@ extension (tp: Type)
           if variance <= 0 then t
           else t.dealias match
             case t @ CapturingType(p, cs) if cs.containsCapOrFresh =>
-              change = true
               val reachRef = if cs.isReadOnly then ref.reach.readOnly else ref.reach
-              t.derivedCapturingType(apply(p), reachRef.singletonCaptureSet)
+              if reachRef.singletonCaptureSet.mightSubcapture(cs) then
+                change = true
+                t.derivedCapturingType(apply(p), reachRef.singletonCaptureSet)
+              else
+                t
             case t @ AnnotatedType(parent, ann) =>
               // Don't map annotations, which includes capture sets
               t.derivedAnnotatedType(this(parent), ann)
@@ -599,6 +603,11 @@ extension (sym: Symbol)
     if sym.is(Method) && sym.owner.isClass then isReadOnlyMethod
     else sym.owner.isInReadOnlyMethod
 
+  def qualString(prefix: String)(using Context): String =
+    if !sym.exists then ""
+    else if sym.isAnonymousFunction then i" $prefix enclosing function"
+    else i" $prefix $sym"
+
 extension (tp: AnnotatedType)
   /** Is this a boxed capturing type? */
   def isBoxed(using Context): Boolean = tp.annot match
@@ -647,7 +656,9 @@ object OnlyCapability:
 
   def unapply(tree: AnnotatedType)(using Context): Option[(Type, ClassSymbol)] = tree match
     case AnnotatedType(parent: Type, ann) if ann.hasSymbol(defn.OnlyCapabilityAnnot) =>
-      Some((parent, ann.tree.tpe.argTypes.head.classSymbol.asClass))
+      ann.tree.tpe.argTypes.head.classSymbol match
+        case cls: ClassSymbol => Some((parent, cls))
+        case _ => None
     case _ => None
 end OnlyCapability
 

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

@@ -263,13 +263,19 @@ sealed abstract class CaptureSet extends Showable:
    */
   def mightAccountFor(x: Capability)(using Context): Boolean =
     reporting.trace(i"$this mightAccountFor $x, ${x.captureSetOfInfo}?", show = true):
-      CCState.withCollapsedFresh: // OK here since we opportunistically choose an alternative which gets checked later
+      CCState.withCollapsedFresh:
+        // withCollapsedFresh should be dropped. The problem is that since our level checking
+        // does not deal with classes well, we get false negatives here. Observed in the line
+        //
+        //     stateFromIteratorConcatSuffix(it)(flatMapImpl(rest, f).state))))
+        //
+        // in cc-lib's LazyListIterable.scala.
         TypeComparer.noNotes:
           elems.exists(_.subsumes(x)(using ctx)(using VarState.ClosedUnrecorded))
       || !x.isTerminalCapability
         && {
-          val elems = x.captureSetOfInfo.elems
-          !elems.isEmpty && elems.forall(mightAccountFor)
+          val xelems = x.captureSetOfInfo.elems
+          !xelems.isEmpty && xelems.forall(mightAccountFor)
         }
 
   /** A more optimistic version of subCaptures used to choose one of two typing rules
@@ -436,9 +442,18 @@ sealed abstract class CaptureSet extends Showable:
   def adoptClassifier(cls: ClassSymbol)(using Context): Unit =
     for elem <- elems do
       elem.stripReadOnly match
-        case fresh: FreshCap => fresh.hiddenSet.adoptClassifier(cls)
+        case fresh: FreshCap => fresh.adoptClassifier(cls, freeze = isConst)
         case _ =>
 
+  /** All capabilities of this set except those Termrefs and FreshCaps that
+   *  are bound by `mt`.
+   */
+  def freeInResult(mt: MethodicType)(using Context): CaptureSet =
+    filter:
+      case TermParamRef(binder, _) => binder ne mt
+      case ResultCap(binder) => binder ne mt
+      case _ => true
+
   /** A bad root `elem` is inadmissible as a member of this set. What is a bad roots depends
    *  on the value of `rootLimit`.
    *  If the limit is null, all capture roots are good.
@@ -611,9 +626,13 @@ object CaptureSet:
       then i" under-approximating the result of mapping $ref to $mapped"
       else ""
 
+  private def capImpliedByCapability(parent: Type)(using Context): Capability =
+    if parent.derivesFromExclusive then GlobalCap.readOnly else GlobalCap
+
   /* The same as {cap.rd} but generated implicitly for references of Capability subtypes.
    */
-  case class CSImpliedByCapability() extends Const(SimpleIdentitySet(GlobalCap.readOnly))
+  class CSImpliedByCapability(parent: Type)(using @constructorOnly ctx: Context)
+  extends Const(SimpleIdentitySet(capImpliedByCapability(parent)))
 
   /** A special capture set that gets added to the types of symbols that were not
    *  themselves capture checked, in order to admit arbitrary corresponding capture
@@ -692,6 +711,9 @@ object CaptureSet:
      */
     private[CaptureSet] var rootLimit: Symbol | Null = null
 
+    def isBadRoot(elem: Capability)(using Context): Boolean =
+      isBadRoot(rootLimit, elem)
+
     private var myClassifier: ClassSymbol = defn.AnyClass
     def classifier: ClassSymbol = myClassifier
 
@@ -743,13 +765,14 @@ object CaptureSet:
       else if !levelOK(elem) then
         failWith(IncludeFailure(this, elem, levelError = true))    // or `elem` is not visible at the level of the set.
       else if !elem.tryClassifyAs(classifier) then
+        //println(i"cannot classify $elem as $classifier, ${elem.asInstanceOf[CoreCapability].classifier}")
         failWith(IncludeFailure(this, elem))
       else
         // id == 108 then assert(false, i"trying to add $elem to $this")
         assert(elem.isWellformed, elem)
         assert(!this.isInstanceOf[HiddenSet] || summon[VarState].isSeparating, summon[VarState])
         includeElem(elem)
-        if isBadRoot(rootLimit, elem) then
+        if isBadRoot(elem) then
           rootAddedHandler()
         val normElem = if isMaybeSet then elem else elem.stripMaybe
         // assert(id != 5 || elems.size != 3, this)
@@ -778,7 +801,7 @@ object CaptureSet:
             case _ => foldOver(b, t)
       find(false, binder)
 
-    private def levelOK(elem: Capability)(using Context): Boolean = elem match
+    def levelOK(elem: Capability)(using Context): Boolean = elem match
       case _: FreshCap =>
         !level.isDefined
         || ccState.symLevel(elem.ccOwner) <= level
@@ -1246,7 +1269,13 @@ object CaptureSet:
    *  when a subsumes check decides that an existential variable `ex` cannot be
    *  instantiated to the other capability `other`.
    */
-  case class ExistentialSubsumesFailure(val ex: ResultCap, val other: Capability) extends ErrorNote
+  case class ExistentialSubsumesFailure(val ex: ResultCap, val other: Capability) extends ErrorNote:
+    def description(using Context): String =
+      def reason =
+        if other.isTerminalCapability then ""
+        else " since that capability is not a `Sharable` capability"
+      i"""the existential capture root in ${ex.originalBinder.resType}
+         |cannot subsume the capability $other$reason."""
 
   /** Failure indicating that `elem` cannot be included in `cs` */
   case class IncludeFailure(cs: CaptureSet, elem: Capability, levelError: Boolean = false) extends ErrorNote, Showable:
@@ -1258,6 +1287,38 @@ object CaptureSet:
       res.myTrace = cs1 :: this.myTrace
       res
 
+    def description(using Context): String =
+      def why =
+        val reasons = cs.elems.toList.collect:
+          case c: FreshCap if !c.acceptsLevelOf(elem) =>
+            i"$elem${elem.levelOwner.qualString("in")} is not visible from $c${c.ccOwner.qualString("in")}"
+          case c: FreshCap if !elem.tryClassifyAs(c.hiddenSet.classifier) =>
+            i"$c is classified as ${c.hiddenSet.classifier} but $elem is not"
+        if reasons.isEmpty then ""
+        else reasons.mkString("\nbecause ", "\nand ", "")
+      cs match
+        case cs: Var =>
+          if !cs.levelOK(elem) then
+            val levelStr = elem match
+              case ref: TermRef => i", defined in ${ref.symbol.maybeOwner}"
+              case _ => ""
+            i"""capability ${elem}$levelStr
+                |cannot be included in outer capture set $cs"""
+          else if !elem.tryClassifyAs(cs.classifier) then
+            i"""capability ${elem} is not classified as ${cs.classifier}, therefore it
+                |cannot be included in capture set $cs of ${cs.classifier} elements"""
+          else if cs.isBadRoot(elem) then
+            elem match
+              case elem: FreshCap =>
+                i"""local capability $elem created in ${elem.ccOwner}
+                  |cannot be included in outer capture set $cs"""
+              case _ =>
+                i"universal capability $elem cannot be included in capture set $cs"
+          else
+            i"capability $elem cannot be included in capture set $cs"
+        case _ =>
+          i"capability $elem is not included in capture set $cs$why"
+
     override def toText(printer: Printer): Text =
       inContext(printer.printerContext):
         if levelError then
@@ -1274,7 +1335,11 @@ object CaptureSet:
    *  @param  lo    the lower type of the orginal type comparison, or NoType if not known
    *  @param  hi    the upper type of the orginal type comparison, or NoType if not known
    */
-  case class MutAdaptFailure(cs: CaptureSet, lo: Type = NoType, hi: Type = NoType) extends ErrorNote
+  case class MutAdaptFailure(cs: CaptureSet, lo: Type = NoType, hi: Type = NoType) extends ErrorNote:
+    def description(using Context): String =
+      def ofType(tp: Type) = if tp.exists then i"of the mutable type $tp" else "of a mutable type"
+      i"""$cs is an exclusive capture set ${ofType(hi)},
+          |it cannot subsume a read-only capture set ${ofType(lo)}."""
 
   /** A VarState serves as a snapshot mechanism that can undo
    *  additions of elements or super sets if an operation fails
@@ -1487,14 +1552,10 @@ object CaptureSet:
       // `ref` will not seem subsumed by other capabilities in a `++`.
       universal
     case c: CoreCapability =>
-      ofType(c.underlying, followResult = false)
+      ofType(c.underlying, followResult = true)
 
   /** Capture set of a type
    *  @param followResult  If true, also include capture sets of function results.
-   *                       This mode is currently not used. It could be interesting
-   *                       when we change the system so that the capture set of a function
-   *                       is the union of the capture sets if its span.
-   *                       In this case we should use `followResult = true` in the call in ofInfo above.
    */
   def ofType(tp: Type, followResult: Boolean)(using Context): CaptureSet =
     def recur(tp: Type): CaptureSet = trace(i"ofType $tp, ${tp.getClass} $followResult", show = true):
@@ -1510,13 +1571,9 @@ object CaptureSet:
           recur(parent) ++ refs
         case tp @ AnnotatedType(parent, ann) if ann.symbol.isRetains =>
           recur(parent) ++ ann.tree.toCaptureSet
-        case tpd @ defn.RefinedFunctionOf(rinfo: MethodType) if followResult =>
+        case tpd @ defn.RefinedFunctionOf(rinfo: MethodOrPoly) if followResult =>
           ofType(tpd.parent, followResult = false)            // pick up capture set from parent type
-          ++ recur(rinfo.resType)                             // add capture set of result
-              .filter:
-                case TermParamRef(binder, _) => binder ne rinfo
-                case ResultCap(binder) => binder ne rinfo
-                case _ => true
+          ++ recur(rinfo.resType).freeInResult(rinfo)         // add capture set of result
         case tpd @ AppliedType(tycon, args) =>
           if followResult && defn.isNonRefinedFunction(tpd) then
             recur(args.last)

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

@@ -40,7 +40,6 @@ object CapturingType:
         apply(parent1, refs ++ refs1, boxed)
       case _ =>
         if parent.derivesFromMutable then refs.setMutable()
-        val classifier = parent.classifier
         refs.adoptClassifier(parent.classifier)
         AnnotatedType(parent, CaptureAnnotation(refs, boxed)(defn.RetainsAnnot))