First steps into separation checking

 - Require -source future for separation checking being turned on
 - Add a type Frash.Cap for fresh maximal capabilities
 - Maintain hidden sets for these types to record what they subsume
 - 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

    - The previous meaning did not do enough in the presence of fresh.
      The new meaning is that all universal capture sets under a @uncheckedCaptures
      become <fluid> capture sets.

 - Print `Fresh.Cap` as `fresh` in error messages where both `cap` and `Fresh.Cap` are printed.
   This avoid confustion with `cap`. Similarly, print `A => B` as `A ->{fresh B` in that case.

 - Print pre-cc annotated capturing types with @retains annotations with `^`. The annotation is
   already rendered as a set in this case, but the `^` was missing.

 - Don't recheck `_` right hand sides of uninitialized variables. These were handled in ways
   that broke freshness checking. The new `uninitialied` scheme does not have this problem.

 - Convert cap to fresh in type arguments of asInstanceOf

 - Let cap and Fresh.Cap subsume other refs only if these others refs cannot
   be added separately to a capture set.

 - When creating an instance of a capability class, assume fresh.cap, not cap as capability.

 - Fix: Skip existentials in when accessing result type in augmentConstructorType
 - Refactor handling of rechecked types

   - Always store new types on rechecking
   - Store them in a hashmap which is associated with the rechecker of the
     current compilation unit
   - After rechecking is done, the map is forgotten, unless keepTypes is true.
     Under keepTypes, then map is kept in an attachment of the unit's root tree.

 - Change in nomenclature:

       knownType --> nuType
       rememberType --> setNuType
       hasRememberedType --> hasNuType

# Conflicts:
#	compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
#	compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
#	compiler/src/dotty/tools/dotc/cc/Existential.scala
#	project/MiMaFilters.scala
#	tests/neg-custom-args/captures/box-adapt-cases.check
#	tests/neg-custom-args/captures/box-adapt-cases.scala
#	tests/neg-custom-args/captures/existential-mapping.check
#	tests/neg-custom-args/captures/i19330.check
#	tests/neg-custom-args/captures/outer-var.check
#	tests/neg-custom-args/captures/vars.check

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

@@ -55,11 +55,6 @@ case class CaptureAnnotation(refs: CaptureSet, boxed: Boolean)(cls: Symbol) exte
     if (this.refs eq refs) && (this.boxed == boxed) then this
     else CaptureAnnotation(refs, boxed)(cls)
 
-  override def sameAnnotation(that: Annotation)(using Context): Boolean = that match
-    case CaptureAnnotation(refs, boxed) =>
-      this.refs == refs && this.boxed == boxed && this.symbol == that.symbol
-    case _ => false
-
   override def mapWith(tm: TypeMap)(using Context) =
     val elems = refs.elems.toList
     val elems1 = elems.mapConserve(tm)

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,26 +147,27 @@ 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, _) => 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 _ => 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)
@@ -201,6 +212,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)