Implement fresh capabilities

These are represented as Fresh.Cap(hidden) where hidden is the set of
capabilities subsumed by a fresh. The underlying representation is as
an annotated type `T @annotation.internal.freshCapability`.

Require -source `3.7` for caps to be converted to Fresh.Cap

Also:

 - Refacture and document CaputureSet
 - Make SimpleIdentitySets showable
 - Refactor VarState
    - Drop Frozen enum
    - Make VarState subclasses inner classes of companion object
    - Rename them
    - Give implicit parameter VarState of subCapture method a default value
 - Fix printing of capturesets containing cap and some other capability
 - Revise handing of @uncheckedAnnotation

Author: odersky

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

@@ -16,9 +16,14 @@ import config.Feature
 import collection.mutable
 import CCState.*
 import reporting.Message
+import CaptureSet.VarState
 
+/** Attachment key for capturing type trees */
 private val Captures: Key[CaptureSet] = Key()
 
+/** Context property to print Fresh.Cap as "fresh" instead of "cap" */
+val PrintFresh: Key[Unit] = Key()
+
 object ccConfig:
 
   /** If true, allow mapping capture set variables under captureChecking with maps that are neither
@@ -47,6 +52,10 @@ object ccConfig:
   def useSealed(using Context) =
     Feature.sourceVersion.stable != SourceVersion.`3.5`
 
+  /** If true, turn on separation checking */
+  def useFresh(using Context): Boolean =
+    Feature.sourceVersion.stable.isAtLeast(SourceVersion.`future`)
+
 end ccConfig
 
 /** Are we at checkCaptures phase? */
@@ -193,10 +202,7 @@ extension (tp: Type)
     case tp: TypeParamRef =>
       tp.derivesFrom(defn.Caps_CapSet)
     case AnnotatedType(parent, annot) =>
-      (annot.symbol == defn.ReachCapabilityAnnot
-      || annot.symbol == defn.MaybeCapabilityAnnot
-      || annot.symbol == defn.ReadOnlyCapabilityAnnot
-      ) && parent.isTrackableRef
+      defn.capabilityWrapperAnnots.contains(annot.symbol) && parent.isTrackableRef
     case _ =>
       false
 
@@ -244,7 +250,7 @@ extension (tp: Type)
    *  the two capture sets are combined.
    */
   def capturing(cs: CaptureSet)(using Context): Type =
-    if (cs.isAlwaysEmpty || cs.isConst && cs.subCaptures(tp.captureSet, frozen = true).isOK)
+    if (cs.isAlwaysEmpty || cs.isConst && cs.subCaptures(tp.captureSet, VarState.Separate).isOK)
         && !cs.keepAlways
     then tp
     else tp match
@@ -421,6 +427,10 @@ extension (tp: Type)
           mapOver(t)
     tm(tp)
 
+  def hasUseAnnot(using Context): Boolean = tp match
+    case AnnotatedType(_, ann) => ann.symbol == defn.UseAnnot
+    case _ => false
+
   /** If `x` is a capture ref, its maybe capability `x?`, represented internally
    *  as `x @maybeCapability`. `x?` stands for a capability `x` that might or might
    *  not be part of a capture set. We have `{} <: {x?} <: {x}`. Maybe capabilities
@@ -512,6 +522,24 @@ extension (tp: Type)
           tp
       case _ =>
         tp
+  end withReachCaptures
+
+  /** Does this type contain no-flip covariant occurrences of `cap`? */
+  def containsCap(using Context): Boolean =
+    val acc = new TypeAccumulator[Boolean]:
+      def apply(x: Boolean, t: Type) =
+        x
+        || variance > 0 && t.dealiasKeepAnnots.match
+          case t @ CapturingType(p, cs) if cs.containsCap =>
+            true
+          case t @ AnnotatedType(parent, ann) =>
+            // Don't traverse annotations, which includes capture sets
+            this(x, parent)
+          case Existential(_, _) =>
+            false
+          case _ =>
+            foldOver(x, t)
+    acc(false, tp)
 
   def level(using Context): Level =
     tp match
@@ -690,7 +718,7 @@ abstract class AnnotatedCapability(annot: Context ?=> ClassSymbol):
       case _ =>
     AnnotatedType(tp, Annotation(annot, util.Spans.NoSpan))
   def unapply(tree: AnnotatedType)(using Context): Option[CaptureRef] = tree match
-    case AnnotatedType(parent: CaptureRef, ann) if ann.symbol == annot => Some(parent)
+    case AnnotatedType(parent: CaptureRef, ann) if ann.hasSymbol(annot) => Some(parent)
     case _ => None
   protected def unwrappable(using Context): Set[Symbol]
 

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

@@ -13,6 +13,7 @@ import CCState.*
 import Periods.NoRunId
 import compiletime.uninitialized
 import StdNames.nme
+import CaptureSet.VarState
 
 /** A trait for references in CaptureSets. These can be NamedTypes, ThisTypes or ParamRefs,
  *  as well as three kinds of AnnotatedTypes representing readOnly, reach, and maybe capabilities.
@@ -78,15 +79,24 @@ trait CaptureRef extends TypeProxy, ValueType:
     case tp: TermRef => tp.name == nme.CAPTURE_ROOT && tp.symbol == defn.captureRoot
     case _ => false
 
+  /** Is this reference a Fresh.Cap instance? */
+  final def isFresh(using Context): Boolean = this match
+    case Fresh.Cap(_) => true
+    case _ => false
+
+  /** 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` ? */
   final def isRootCapability(using Context): Boolean = this match
-    case ReadOnlyCapability(tp1) => tp1.isCap
-    case _ => isCap
+    case ReadOnlyCapability(tp1) => tp1.isCapOrFresh
+    case _ => isCapOrFresh
 
   /** Is this reference capability that does not derive from another capability ? */
   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
 
@@ -137,34 +147,36 @@ trait CaptureRef extends TypeProxy, ValueType:
    *   Y: CapSet^c1...CapSet^c2, x subsumes (CapSet^c2)  ==>  x subsumes Y
    *   Contains[X, y]  ==>  X subsumes y
    *
-   *   TODO: Document cases with more comments.
+   *   TODO: Move to CaptureSet
    */
-  final def subsumes(y: CaptureRef)(using Context): Boolean =
+  final def subsumes(y: CaptureRef)(using ctx: Context, vs: VarState = VarState.Separate): 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
+    def viaInfo(info: Type)(test: Type => Boolean): Boolean = info.dealias match
       case info: SingletonCaptureRef => test(info)
+      case CapturingType(parent, _) =>
+        if this.derivesFrom(defn.Caps_CapSet) then test(info)
+          /*
+            If `this` is a capture set variable `C^`, then it is possible that it can be
+            reached from term variables in a reachability chain through the context.
+            For instance, in `def test[C^](src: Foo^{C^}) = { val x: Foo^{src} = src; val y: Foo^{x} = x; y }`
+            we expect that `C^` subsumes `x` and `y` in the body of the method
+            (cf. test case cc-poly-varargs.scala for a more involved example).
+          */
+        else viaInfo(parent)(test)
       case info: AndType => viaInfo(info.tp1)(test) || viaInfo(info.tp2)(test)
       case info: OrType => viaInfo(info.tp1)(test) && viaInfo(info.tp2)(test)
-      case info @ CapturingType(_,_) if this.derivesFrom(defn.Caps_CapSet) =>
-        /*
-          If `this` is a capture set variable `C^`, then it is possible that it can be
-          reached from term variables in a reachability chain through the context.
-          For instance, in `def test[C^](src: Foo^{C^}) = { val x: Foo^{src} = src; val y: Foo^{x} = x; y }`
-          we expect that `C^` subsumes `x` and `y` in the body of the method
-          (cf. test case cc-poly-varargs.scala for a more involved example).
-         */
-        test(info)
       case _ => false
 
     (this eq y)
-    || this.isCap
+    || maxSubsumes(y, canAddHidden = !vs.isOpen)
     || y.match
-        case y: TermRef if !y.isRootCapability =>
+        case y: TermRef if !y.isCap =>
             y.prefix.match
               case ypre: CaptureRef =>
                 this.subsumes(ypre)
@@ -213,6 +225,27 @@ trait CaptureRef extends TypeProxy, ValueType:
         case _ => false
   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.
+   *                       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
+   *                       accepts additions we first run `maxSubsumes` with `canAddHidden = false`
+   *                       so that new variables get added to the sets. If that fails, we run
+   *                       the test again with canAddHidden = true as a last effort before we
+   *                       fail a comparison.
+   */
+  def maxSubsumes(y: CaptureRef, canAddHidden: Boolean)(using ctx: Context, vs: VarState = VarState.Separate): Boolean =
+    this.match
+      case Fresh.Cap(hidden) =>
+        vs.ifNotSeen(this)(hidden.elems.exists(_.subsumes(y)))
+        || !y.stripReadOnly.isCap && canAddHidden && vs.addHidden(hidden, y)
+      case _ =>
+        this.isCap && canAddHidden
+        || y.match
+            case ReadOnlyCapability(y1) => this.stripReadOnly.maxSubsumes(y1, canAddHidden)
+            case _ => false
+
   def assumedContainsOf(x: TypeRef)(using Context): SimpleIdentitySet[CaptureRef] =
     CaptureSet.assumedContains.getOrElse(x, SimpleIdentitySet.empty)