diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
index 349711ef21b0..4c31c7e44d0d 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
@@ -232,9 +232,7 @@ extension (tp: Type)
       case tp @ ReachCapability(_) =>
         tp.singletonCaptureSet
       case ReadOnlyCapability(ref) =>
-        val refDcs = ref.deepCaptureSet(includeTypevars)
-        if refDcs.isConst then CaptureSet(refDcs.elems.map(_.readOnly))
-        else refDcs // this case should not happen for correct programs
+        ref.deepCaptureSet(includeTypevars)
       case tp: SingletonCaptureRef if tp.isTrackableRef =>
         tp.reach.singletonCaptureSet
       case _ =>
@@ -281,24 +279,12 @@ extension (tp: Type)
     case _ =>
       tp
 
-  /** 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.
-   */
+  /** The first element of this path type */
   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: NamedType if tp1.symbol.maybeOwner.isClass && !tp1.symbol.is(TypeParam) =>
+      tp1.prefix.pathRoot
     case tp1 => tp1
 
-  /** The first element of a path type, but stop at references extending
-   *  SharedCapability.
-   */
-  final def pathRootOrShared(using Context): Type =
-    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
-      case tp1 => tp1
-
   /** If this part starts with `C.this`, the class `C`.
    *  Otherwise, if it starts with a reference `r`, `r`'s owner.
    *  Otherwise NoSymbol.
@@ -431,7 +417,6 @@ 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
@@ -471,11 +456,6 @@ 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)
@@ -493,10 +473,6 @@ 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)
@@ -508,7 +484,7 @@ extension (tp: Type)
     case _ =>
       ReadOnlyCapability(tp)
 
-  /** If `x` is a capture ref, replace all no-flip covariant occurrences of `cap`
+  /** If `x` is a capture ref, replacxe all no-flip covariant occurrences of `cap`
    *  in type `tp` with `x*`.
    */
   def withReachCaptures(ref: Type)(using Context): Type =
@@ -758,7 +734,7 @@ object MaybeCapability extends AnnotatedCapability(defn.MaybeCapabilityAnnot):
   protected def unwrappable(using Context) = Set()
 
 /** An extractor for `ref @readOnlyCapability`, which is used to express
- *  the read-only capability `ref.rd` as a type.
+ *  the rad-only capability `ref.rd` as a type.
  */
 object ReadOnlyCapability extends AnnotatedCapability(defn.ReadOnlyCapabilityAnnot):
   protected def unwrappable(using Context) = Set(defn.MaybeCapabilityAnnot)
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
index a2ceb1f20372..f95722274258 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
@@ -100,14 +100,12 @@ 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 of the generic root capabilities `cap` or `cap.rd` ? */
+  /** Is this reference one 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 a capability that does not derive from another capability?
-   *  Includes read-only versions of maximal capabilities.
-   */
+  /** 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)
@@ -115,14 +113,10 @@ trait CaptureRef extends TypeProxy, ValueType:
     case ReadOnlyCapability(tp1) => tp1.isMaxCapability
     case _ => false
 
-  /** An exclusive capability is a capability that derives
-   *  indirectly from a maximal capability without going through
-   *  a read-only capability first.
-   */
   final def isExclusive(using Context): Boolean =
     !isReadOnly && (isMaxCapability || captureSetOfInfo.isExclusive)
 
-  // With the support of paths, we don't need to normalize the `TermRef`s anymore.
+  // 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 =>
@@ -165,6 +159,8 @@ 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 =
 
@@ -242,8 +238,8 @@ trait CaptureRef extends TypeProxy, ValueType:
         case _ => false
   end subsumes
 
-  /** This is a maximal capability that subsumes `y` in given context and VarState.
-   *  @param canAddHidden  If true we allow maximal capabilities to subsume all other capabilities.
+  /** 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
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index 55fda0f22a08..52a7cd87f647 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -227,7 +227,11 @@ sealed abstract class CaptureSet extends Showable:
     elems.forall(that.mightAccountFor)
     && !that.elems.forall(this.mightAccountFor)
 
-  /** The subcapturing test, taking an explicit VarState. */
+  /** The subcapturing test.
+   *  @param frozen   if true, no new variables or dependent sets are allowed to
+   *                  be added when making this test. An attempt to add either
+   *                  will result in failure.
+   */
   final def subCaptures(that: CaptureSet, vs: VarState)(using Context): CompareResult =
     subCaptures(that)(using ctx, vs)
 
@@ -388,7 +392,7 @@ sealed abstract class CaptureSet extends Showable:
   override def toText(printer: Printer): Text =
     printer.toTextCaptureSet(this) ~~ description
 
-  /** Apply function `f` to the elements. Typically used for printing.
+  /** Apply function `f` to the elements. Typcially used for printing.
    *  Overridden in HiddenSet so that we don't run into infinite recursions
    */
   def processElems[T](f: Refs => T): T = f(elems)
@@ -403,10 +407,10 @@ object CaptureSet:
   /** If set to `true`, capture stack traces that tell us where sets are created */
   private final val debugSets = false
 
-  val emptyRefs: Refs = SimpleIdentitySet.empty
+  val emptySet = SimpleIdentitySet.empty
 
   /** The empty capture set `{}` */
-  val empty: CaptureSet.Const = Const(emptyRefs)
+  val empty: CaptureSet.Const = Const(emptySet)
 
   /** The universal capture set `{cap}` */
   def universal(using Context): CaptureSet =
@@ -462,7 +466,7 @@ object CaptureSet:
    *  nulls, this provides more lenient checking against compilation units that
    *  were not yet compiled with capture checking on.
    */
-  object Fluid extends Const(emptyRefs):
+  object Fluid extends Const(emptySet):
     override def isAlwaysEmpty = false
     override def addThisElem(elem: CaptureRef)(using Context, VarState) = CompareResult.OK
     override def accountsFor(x: CaptureRef)(using Context, VarState): Boolean = true
@@ -471,7 +475,7 @@ object CaptureSet:
   end Fluid
 
   /** The subclass of captureset variables with given initial elements */
-  class Var(override val owner: Symbol = NoSymbol, initialElems: Refs = emptyRefs, val level: Level = undefinedLevel, underBox: Boolean = false)(using @constructorOnly ictx: Context) extends CaptureSet:
+  class Var(override val owner: Symbol = NoSymbol, initialElems: Refs = emptySet, val level: Level = undefinedLevel, underBox: Boolean = false)(using @constructorOnly ictx: Context) extends CaptureSet:
 
     /** A unique identification number for diagnostics */
     val id =
@@ -489,7 +493,7 @@ object CaptureSet:
     /** The sets currently known to be dependent sets (i.e. new additions to this set
      *  are propagated to these dependent sets.)
      */
-    var deps: Deps = SimpleIdentitySet.empty
+    var deps: Deps = emptySet
 
     def isConst = isSolved
     def isAlwaysEmpty = isSolved && elems.isEmpty
@@ -632,8 +636,7 @@ object CaptureSet:
      */
     def solve()(using Context): Unit =
       if !isConst then
-        val approx = upperApprox(empty)
-          .map(Fresh.FromCap(NoSymbol).inverse)    // Fresh.Cap --> cap
+        val approx = upperApprox(empty).map(Fresh.FromCap(NoSymbol).inverse)
           .showing(i"solve $this = $result", capt)
         //println(i"solving var $this $approx ${approx.isConst} deps = ${deps.toList}")
         val newElems = approx.elems -- elems
@@ -923,16 +926,16 @@ object CaptureSet:
     cs1.elems.filter(cs2.mightAccountFor) ++ cs2.elems.filter(cs1.mightAccountFor)
 
   /** A capture set variable used to record the references hidden by a Fresh.Cap instance */
-  class HiddenSet(initialHidden: Refs = emptyRefs)(using @constructorOnly ictx: Context)
+  class HiddenSet(initialHidden: Refs = emptySet)(using @constructorOnly ictx: Context)
   extends Var(initialElems = initialHidden):
 
     /** Apply function `f` to `elems` while setting `elems` to empty for the
-     *  duration. This is used to escape infinite recursions if two Fresh.Caps
+     *  duration. This is used to escape infinite recursions if two Frash.Caps
      *  refer to each other in their hidden sets.
      */
     override def processElems[T](f: Refs => T): T =
       val savedElems = elems
-      elems = emptyRefs
+      elems = emptySet
       try f(savedElems)
       finally elems = savedElems
   end HiddenSet
@@ -1136,7 +1139,6 @@ 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
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 7380996b3aed..df6eb2d385cc 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -519,7 +519,8 @@ 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 && curEnv.isOpen then markFree(capturedVars(sym), tree)
+        if sym.exists then
+          if 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
@@ -555,21 +556,16 @@ 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 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`.
+        // 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`.
         def addSelects(ref: TermRef, pt: Type): CaptureRef = pt match
           case pt: PathSelectionProto if ref.isTracked =>
             if pt.sym.isReadOnlyMethod then
@@ -586,8 +582,7 @@ 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 capability path or is a a read-only method, we return
-     *  a PathSelectionProto.
+     *  could be part of a capabaility path, we return a PathSelectionProto.
      */
     override def selectionProto(tree: Select, pt: Type)(using Context): Type =
       val sym = tree.symbol
@@ -621,9 +616,6 @@ class CheckCaptures extends Recheck, SymTransformer:
           }
         case _ => denot
 
-      // Don't allow update methods to be called unless the qualifier captures
-      // an exclusive reference. TODO This should probably 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,
@@ -659,8 +651,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 and @consume
-     *  annotations on method parameter symbols to the corresponding paramInfo types.
+    /** Hook for massaging a function before it is applied. Copies all @use annotations
+     *  on method parameter symbols to the corresponding paramInfo types.
      */
     override def prepareFunction(funtpe: MethodType, meth: Symbol)(using Context): MethodType =
       val paramInfosWithUses =
@@ -690,8 +682,7 @@ class CheckCaptures extends Recheck, SymTransformer:
         includeCallCaptures(meth, res, tree)
         res
 
-    /** Recheck argument against a "freshened" version of `formal` where toplevel `cap`
-     *  occurrences are replaced by `Fresh.Cap`. Also, if formal parameter carries a `@use`,
+    /** Recheck argument, and, 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 =
@@ -782,21 +773,16 @@ 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: @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.
+       *  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.
        *
        *  Second half: union of initial capture set and all capture sets of arguments
-       *  to tracked parameters. The initial capture set `initCs` is augmented with
-       *   - Fresh.Cap    if `core` extends Mutable
-       *   - Fresh.Cap.rd if `core` extends Capability
+       *  to tracked parameters.
        */
       def addParamArgRefinements(core: Type, initCs: CaptureSet): (Type, CaptureSet) =
         var refined: Type = core
         var allCaptures: CaptureSet =
-          if core.derivesFromMutable then initCs ++ CaptureSet.fresh()
+          if core.derivesFromMutable then CaptureSet.fresh()
           else if core.derivesFromCapability then initCs ++ Fresh.Cap().readOnly.singletonCaptureSet
           else initCs
         for (getterName, argType) <- mt.paramNames.lazyZip(argTypes) do
@@ -1502,7 +1488,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 type is not a type variable
+     *  The unboxed condition ensures that the expected 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.
@@ -1528,9 +1514,9 @@ class CheckCaptures extends Recheck, SymTransformer:
         actual
       else
         val improvedVAR = improveCaptures(actual.widen.dealiasKeepAnnots, actual)
-        val improved = improveReadOnly(improvedVAR, expected)
+        val improvedRO = improveReadOnly(improvedVAR, expected)
         val adapted = adaptBoxed(
-            improved.withReachCaptures(actual), expected, tree,
+            improvedRO.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
@@ -1577,19 +1563,17 @@ 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
-                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)
-
+                fail(i"has a parameter ${param1.name} with different @${cls.name} status than the corresponding parameter in the overridden definition")
             checkAnnot(defn.UseAnnot)
             checkAnnot(defn.ConsumeAnnot)
       end OverridingPairsCheckerCC
@@ -1839,7 +1823,7 @@ class CheckCaptures extends Recheck, SymTransformer:
       end checker
 
       checker.traverse(unit)(using ctx.withOwner(defn.RootClass))
-      if ccConfig.useSepChecks then SepCheck(this).traverse(unit)
+      if ccConfig.useSepChecks then SepChecker(this).traverse(unit)
       if !ctx.reporter.errorsReported then
         // We dont report errors here if previous errors were reported, because other
         // errors often result in bad applied types, but flagging these bad types gives
diff --git a/compiler/src/dotty/tools/dotc/cc/Existential.scala b/compiler/src/dotty/tools/dotc/cc/Existential.scala
index f115adfa6421..39f6fcf14fd9 100644
--- a/compiler/src/dotty/tools/dotc/cc/Existential.scala
+++ b/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 `Fresh.Cap`
+  /** Map existentials at the top-level and in all nested result types to `cap`
    */
   def toCapDeeply(tp: Type)(using Context): Type = tp.dealiasKeepAnnots match
     case Existential(boundVar, unpacked) =>
diff --git a/compiler/src/dotty/tools/dotc/cc/Fresh.scala b/compiler/src/dotty/tools/dotc/cc/Fresh.scala
index 48b20f18f027..889f05ce8308 100644
--- a/compiler/src/dotty/tools/dotc/cc/Fresh.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Fresh.scala
@@ -13,19 +13,14 @@ import NameKinds.ExistentialBinderName
 import NameOps.isImpureFunction
 import reporting.Message
 import util.SimpleIdentitySet.empty
-import CaptureSet.{Refs, emptyRefs, NarrowingCapabilityMap}
+import CaptureSet.{Refs, emptySet, NarrowingCapabilityMap}
 import dotty.tools.dotc.util.SimpleIdentitySet
 
-/** 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.
- */
+/** Handling fresh in CC:
+
+*/
 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)
@@ -37,20 +32,16 @@ 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 emptyRefs
+      if ref.isTrackableRef then SimpleIdentitySet(ref.reach) else emptySet
     else
-      if ref.isTracked then SimpleIdentitySet(ref) else emptyRefs
+      if ref.isTracked then SimpleIdentitySet(ref) else emptySet
 
-  /** An extractor for "fresh" capabilities */
   object Cap:
 
-    def apply(initialHidden: Refs = emptyRefs)(using Context): CaptureRef =
+    def apply(initialHidden: Refs = emptySet)(using Context): CaptureRef =
       if ccConfig.useSepChecks then
         AnnotatedType(defn.captureRoot.termRef, Annot(CaptureSet.HiddenSet(initialHidden)))
       else
@@ -67,7 +58,6 @@ object Fresh:
       case _ => None
   end Cap
 
-  /** Map each occurrence of cap to a different Sep.Cap instance */
   class FromCap(owner: Symbol)(using Context) extends BiTypeMap, FollowAliasesMap:
     thisMap =>
 
diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
index b2318eb798dd..1fe57e80461b 100644
--- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
+++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
@@ -7,26 +7,14 @@ import collection.mutable
 import core.*
 import Symbols.*, Types.*, Flags.*
 import Contexts.*, Names.*, Flags.*, Symbols.*, Decorators.*
-import CaptureSet.{Refs, emptyRefs, HiddenSet}
+import CaptureSet.{Refs, emptySet, HiddenSet}
 import config.Printers.capt
 import StdNames.nme
 import util.{SimpleIdentitySet, EqHashMap, SrcPos}
 import tpd.*
 import reflect.ClassTag
 
-/** The separation checker is  a tree traverser that is run after capture checking.
- *  It checks tree nodes for various separation conditions, explained in the
- *  methods below. Rough summary:
- *
- *   - Hidden sets of arguments must not be referred to in the same application
- *   - Hidden sets of (result-) types must not be referred to alter in the same scope.
- *   - Returned hidden sets can only refer to @consume parameters.
- *   - If returned hidden sets refer to an encloding this, the reference must be
- *     from a @consume method.
- *   - Consumed entities cannot be used subsequently.
- *   - Entitites cannot be consumed in a loop.
- */
-object SepCheck:
+object SepChecker:
 
   /** Enumerates kinds of captures encountered so far */
   enum Captures:
@@ -62,7 +50,7 @@ object SepCheck:
       case TypeRole.Argument(_) =>
         "the argument's adapted type"
       case TypeRole.Qualifier(_, meth) =>
-        i"the type of the prefix to a call of $meth"
+        i"the type of the qualifier to a call of $meth"
   end TypeRole
 
   /** A class for segmented sets of consumed references.
@@ -138,18 +126,19 @@ object SepCheck:
         else ConstConsumedSet(refs.slice(start, size), locs.slice(start, size))
       finally
         size = start
+
   end MutConsumedSet
 
   val EmptyConsumedSet = ConstConsumedSet(Array(), Array())
 
-class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
+class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
   import checker.*
-  import SepCheck.*
+  import SepChecker.*
 
   /** The set of capabilities that are hidden by a polymorphic result type
    *  of some previous definition.
    */
-  private var defsShadow: Refs = emptyRefs
+  private var defsShadow: Refs = emptySet
 
   /** A map from definitions to their internal result types.
    *  Populated during separation checking traversal.
@@ -161,29 +150,17 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
    */
   private var previousDefs: List[mutable.ListBuffer[ValOrDefDef]] = Nil
 
-  /** The set of references that were consumed so far in the current method */
   private var consumed: MutConsumedSet = MutConsumedSet()
 
-  /** Run `op`` with a fresh, initially empty consumed set. */
   private def withFreshConsumed(op: => Unit): Unit =
     val saved = consumed
     consumed = MutConsumedSet()
     op
     consumed = saved
 
-  /** Infos aboput Labeled expressions enclosing the current traversal point.
-   *  For each labeled expression, it's label name, and a list buffer containing
-   *  all consumed sets of return expressions referring to that label.
-   */
   private var openLabeled: List[(Name, mutable.ListBuffer[ConsumedSet])] = Nil
 
   extension (refs: Refs)
-
-    /** The footprint of a set of references `refs` the smallest set `F` such that
-     *   - no maximal capability is in `F`
-     *   - all non-maximal capabilities in `refs` are in `F`
-     *   - if `f in F` then the footprint of `f`'s info is also in `F`.
-     */
     private def footprint(using Context): Refs =
       def recur(elems: Refs, newElems: List[CaptureRef]): Refs = newElems match
         case newElem :: newElems1 =>
@@ -194,18 +171,6 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
       val elems: Refs = refs.filter(!_.isMaxCapability)
       recur(elems, elems.toList)
 
-    /** The overlap of two footprint sets F1 and F2. This contains all exclusive references `r`
-     *  such that one of the following is true:
-     *   1.
-     *      - one of the sets contains `r`
-     *      - the other contains a capability `s` or `s.rd` where `s` _covers_ `r`
-     *   2.
-     *      - one of the sets contains `r.rd`
-     *      - the other contains a capability `s` where `s` _covers_ `r`
-     *
-     *  A capability `s` covers `r` if `r` can be seen as a path extension of `s`. E.g.
-     *  if `s = x.a` and `r = x.a.b.c` then `s` covers `a`.
-     */
     private def overlapWith(other: Refs)(using Context): Refs =
       val refs1 = refs
       val refs2 = other
@@ -217,7 +182,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
        */
       def common(refs1: Refs, refs2: Refs) =
         refs1.filter: ref =>
-          ref.isExclusive && refs2.exists(_.stripReadOnly.covers(ref))
+          ref.isExclusive && refs2.exists(ref2 => ref2.stripReadOnly.covers(ref))
         ++
         refs1
           .filter:
@@ -225,7 +190,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
               // We can get away testing only references with at least one field selection
               // here since stripped readOnly references that equal a reference in refs2
               // are added by the first clause of the symmetric call to common.
-              !ref.isCap && refs2.exists(_.covers(prefix))
+              !ref.isCap && refs2.exists(ref2 => ref2.covers(prefix))
             case _ =>
               false
           .map(_.stripReadOnly)
@@ -233,26 +198,19 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
       common(refs, other) ++ common(other, refs)
     end overlapWith
 
-    /** The non-maximal elements hidden directly or indirectly by a maximal
-     *  capability in `refs`. E g. if `R = {x, <cap hiding <y, <cap hiding z>>}` then
-     *  its hidden set is `{y, z}`.
-     */
     private def hidden(using Context): Refs =
       val seen: util.EqHashSet[CaptureRef] = new util.EqHashSet
-
-      def hiddenByElem(elem: CaptureRef): Refs = elem match
-        case Fresh.Cap(hcs) => hcs.elems.filter(!_.isRootCapability) ++ recur(hcs.elems)
-        case ReadOnlyCapability(ref1) => hiddenByElem(ref1).map(_.readOnly)
-        case _ => emptyRefs
-
-      def recur(refs: Refs): Refs =
-        (emptyRefs /: refs): (elems, elem) =>
-          if seen.add(elem) then elems ++ hiddenByElem(elem) else elems
-
+      def recur(cs: Refs): Refs =
+        (emptySet /: cs): (elems, elem) =>
+          if seen.add(elem) then elems ++ hiddenByElem(elem, recur)
+          else elems
       recur(refs)
     end hidden
 
-    /** Subtract all elements that are covered by some element in `others` from this set. */
+    private def containsHidden(using Context): Boolean =
+      refs.exists: ref =>
+        !hiddenByElem(ref, _ => emptySet).isEmpty
+
     private def deduct(others: Refs)(using Context): Refs =
       refs.filter: ref =>
         !others.exists(_.covers(ref))
@@ -263,36 +221,27 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
       if ref.isTrackableRef then refs.deduct(CaptureSet(ref, ref.reach).elems.footprint)
       else refs
 
-    /** Deduct the footprint of all captures of trees in `deps` from `refs` */
+    /** Deduct the footprint of all captures of `deps` from `refs` */
     private def deductCapturesOf(deps: List[Tree])(using Context): Refs =
       deps.foldLeft(refs): (refs, dep) =>
         refs.deduct(captures(dep).footprint)
   end extension
 
-  /** The deep capture set of an argument or prefix widened to the formal parameter, if
+  private def hiddenByElem(ref: CaptureRef, recur: Refs => Refs)(using Context): Refs = ref match
+    case Fresh.Cap(hcs) => hcs.elems.filter(!_.isRootCapability) ++ recur(hcs.elems)
+    case ReadOnlyCapability(ref1) => hiddenByElem(ref1, recur).map(_.readOnly)
+    case _ => emptySet
+
+  /** The captures of an argument or prefix widened to the formal parameter, if
    *  the latter contains a cap.
    */
   private def formalCaptures(arg: Tree)(using Context): Refs =
     arg.formalType.orElse(arg.nuType).deepCaptureSet.elems
 
-   /** The deep capture set if the type of `tree` */
+   /** The captures of a node */
   private def captures(tree: Tree)(using Context): Refs =
    tree.nuType.deepCaptureSet.elems
 
-  // ---- Error reporting TODO Once these are stabilized, move to messages -----
-
-  /** Report a separation failure in an application `fn(args)`
-   *  @param fn          the function
-   *  @param args        the flattened argument lists
-   *  @param argIdx      the index of the failing argument in `args`, starting at 0
-   *  @param overlap     the overlap causing the failure
-   *  @param hiddenInArg the hidxden set of the type of the failing argument
-   *  @param footprints  a sequence of partial footprints, and the index of the
-   *                     last argument they cover.
-   *  @param deps        cross argument dependencies: maps argument trees to
-   *                     those other arguments that where mentioned by coorresponding
-   *                     formal parameters.
-   */
   private def sepApplyError(fn: Tree, args: List[Tree], argIdx: Int,
       overlap: Refs, hiddenInArg: Refs, footprints: List[(Refs, Int)],
       deps: collection.Map[Tree, List[Tree]])(using Context): Unit =
@@ -335,7 +284,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
     def hiddenCaptures = formalCaptures(arg).hidden
     def clashFootprint = clashCaptures.footprint
     def hiddenFootprint = hiddenCaptures.footprint
-    def declaredFootprint = deps(arg).map(captures(_)).foldLeft(emptyRefs)(_ ++ _).footprint
+    def declaredFootprint = deps(arg).map(captures(_)).foldLeft(emptySet)(_ ++ _).footprint
     def footprintOverlap = hiddenFootprint.overlapWith(clashFootprint).deduct(declaredFootprint)
     report.error(
       em"""Separation failure: argument of type  ${arg.nuType}
@@ -353,13 +302,6 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
       arg.srcPos)
   end sepApplyError
 
-  /** Report a use/definition failure, where a previously hidden capability is
-   *  used again.
-   *  @param tree          the tree where the capability is used
-   *  @param used          the footprint of all uses of `tree`
-   *  @param globalOverlap the overlap between `used` and all capabilities hidden
-   *                       by previous definitions
-   */
   def sepUseError(tree: Tree, used: Refs, globalOverlap: Refs)(using Context): Unit =
     val individualChecks = for mdefs <- previousDefs.iterator; mdef <- mdefs.iterator yield
       val hiddenByDef = captures(mdef.tpt).hidden.footprint
@@ -381,11 +323,6 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
       tree.srcPos)
   end sepUseError
 
-  /** Report a failure where a previously consumed capability is used again,
-   *  @param ref     the capability that is used after being consumed
-   *  @param loc     the position where the capability was consumed
-   *  @param pos     the position where the capability was used again
-   */
   def consumeError(ref: CaptureRef, loc: SrcPos, pos: SrcPos)(using Context): Unit =
     report.error(
       em"""Separation failure: Illegal access to $ref, which was passed to a
@@ -393,43 +330,12 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
           |and therefore is no longer available.""",
       pos)
 
-  /** Report a failure where a capability is consumed in a loop.
-   *  @param ref     the capability
-   *  @param loc     the position where the capability was consumed
-   */
   def consumeInLoopError(ref: CaptureRef, pos: SrcPos)(using Context): Unit =
     report.error(
       em"""Separation failure: $ref appears in a loop, therefore it cannot
           |be passed to a @consume parameter or be used as a prefix of a @consume method call.""",
       pos)
 
-  // ------------ Checks -----------------------------------------------------
-
-  /** Check separation between different arguments and between function
-   *  prefix and arguments. A capability cannot be hidden by one of these arguments
-   *  and also be either explicitly referenced or hidden by the prefix or another
-   *  argument. "Hidden" means: the capability is in the deep capture set of the
-   *  argument and appears in the hidden set of the corresponding (capture-polymorphic)
-   *  formal parameter. Howeber, we do allow explicit references to a hidden
-   *  capability in later arguments, if the corresponding formal parameter mentions
-   *  the parameter where the capability was hidden. For instance in
-   *
-   *    def seq(x: () => Unit; y ->{cap, x} Unit): Unit
-   *    def f: () ->{io} Unit
-   *
-   *  we do allow `seq(f, f)` even though `{f, io}` is in the hidden set of the
-   *  first parameter `x`, since the second parameter explicitly mentions `x` in
-   *  its capture set.
-   *
-   *  Also check separation via checkType within individual arguments widened to their
-   *  formal paramater types.
-   *
-   *  @param fn        the applied function
-   *  @param args      the flattened argument lists
-   *  @param deps      cross argument dependencies: maps argument trees to
-   *                   those other arguments that where mentioned by coorresponding
-   *                   formal parameters.
-   */
   private def checkApply(fn: Tree, args: List[Tree], deps: collection.Map[Tree, List[Tree]])(using Context): Unit =
     val fnCaptures = methPart(fn) match
       case Select(qual, _) => qual.nuType.captureSet
@@ -439,18 +345,10 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
     val footprints = mutable.ListBuffer[(Refs, Int)]((footprint, 0))
     val indexedArgs = args.zipWithIndex
 
-    // First, compute all footprints of arguments to monomorphic pararameters,
-    // separately in `footprints`, and their union in `footprint`.
     for (arg, idx) <- indexedArgs do
       if !arg.needsSepCheck then
         footprint = footprint ++ captures(arg).footprint.deductCapturesOf(deps(arg))
         footprints += ((footprint, idx + 1))
-
-    // Then, for each argument to a polymorphic parameter:
-    //   - check formal type via checkType
-    //   - check that hidden set of argument does not overlap with current footprint
-    //   - add footprint of the deep capture set of actual type of argument
-    //     to global footprint(s)
     for (arg, idx) <- indexedArgs do
       if arg.needsSepCheck then
         val ac = formalCaptures(arg)
@@ -464,10 +362,6 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
         footprints += ((footprint, idx + 1))
   end checkApply
 
-  /** The def/use overlap between the references `hiddenByDef` hidden by
-   *  a previous definition and the `used` set of a tree with symbol `sym`.
-   *  Deduct any capabilities referred to or hidden by the (result-) type of `sym`.
-   */
   def defUseOverlap(hiddenByDef: Refs, used: Refs, sym: Symbol)(using Context): Refs =
     val overlap = hiddenByDef.overlapWith(used)
     resultType.get(sym) match
@@ -477,10 +371,6 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
       case _ =>
         overlap
 
-  /** 1. Check that the capabilities used at `tree` don't overlap with
-   *     capabilities hidden by a previous definition.
-   *  2. Also check that none of the used capabilities was consumed before.
-   */
   def checkUse(tree: Tree)(using Context) =
     val used = tree.markedFree
     if !used.elems.isEmpty then
@@ -492,41 +382,24 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
         val pos = consumed.get(ref)
         if pos != null then consumeError(ref, pos, tree.srcPos)
 
-  /** If `tp` denotes some version of a singleton type `x.type` the set `{x}`
-   *  otherwise the empty set.
-   */
   def explicitRefs(tp: Type): Refs = tp match
     case tp: (TermRef | ThisType) => SimpleIdentitySet(tp)
     case AnnotatedType(parent, _) => explicitRefs(parent)
     case AndType(tp1, tp2) => explicitRefs(tp1) ++ explicitRefs(tp2)
     case OrType(tp1, tp2) => explicitRefs(tp1) ** explicitRefs(tp2)
-    case _ => emptyRefs
+    case _ => emptySet
 
-  /** Deduct some elements from `refs` according to the role of the checked type `tpe`:
-   *   - If the the type apears as a (result-) type of a definition of `x`, deduct
-   *     `x` and `x*`.
-   *   - If `tpe` is morally a singleton type deduct it as well.
-   */
   def prune(refs: Refs, tpe: Type, role: TypeRole)(using Context): Refs =
     refs.deductSym(role.dclSym).deduct(explicitRefs(tpe))
 
-  /** Check validity of consumed references `refsToCheck`. The references are consumed
+  def checkType(tpt: Tree, sym: Symbol)(using Context): Unit =
+    checkType(tpt.nuType, tpt.srcPos,
+        TypeRole.Result(sym, inferred = tpt.isInstanceOf[InferredTypeTree]))
+
+  /** Check validity consumed references `refsToCheck`. The references are consumed
    *  because they are hidden in a Fresh.Cap result type or they are referred
    *  to in an argument to a @consume parameter or in a prefix of a @consume method --
-   *  which one applies is determined by the role parameter.
-   *
-   *  This entails the following checks:
-   *   - The reference must be defined in the same as method or class as
-   *     the access.
-   *   - If the reference is to a term parameter, that parameter must be
-   *     marked as @consume as well.
-   *   - If the reference is to a this type of the enclosing class, the
-   *     access must be in a @consume method.
-   *
-   *  References that extend SharedCapability are excluded from checking.
-   *  As a side effect, add all checked references with the given position `pos`
-   *  to the global `consumed` map.
-   *
+   *  which one applie is determined by the role parameter.
    *  @param refsToCheck   the referencves to check
    *  @param tpe           the type containing those references
    *  @param role          the role in which the type apears
@@ -537,9 +410,8 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
     val badParams = mutable.ListBuffer[Symbol]()
     def currentOwner = role.dclSym.orElse(ctx.owner)
     for hiddenRef <- prune(refsToCheck, tpe, role) do
-      val proot = hiddenRef.pathRootOrShared
-      if !proot.widen.derivesFromSharedCapability then
-        proot match
+      if !hiddenRef.derivesFrom(defn.Caps_SharedCapability) then
+        hiddenRef.pathRoot match
           case ref: TermRef =>
             val refSym = ref.symbol
             if currentOwner.enclosingMethodOrClass.isProperlyContainedIn(refSym.maybeOwner.enclosingMethodOrClass) then
@@ -575,26 +447,17 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
     role match
       case _: TypeRole.Argument | _: TypeRole.Qualifier =>
         for ref <- refsToCheck do
-          if !ref.pathRootOrShared.derivesFromSharedCapability then
+          if !ref.derivesFrom(defn.Caps_SharedCapability) then
             consumed.put(ref, pos)
       case _ =>
   end checkConsumedRefs
 
-  /** Check separation conditions of type `tpe` that appears in `role`.
-   *   1. Check that the parts of type `tpe` are mutually separated, as defined in
-   *      `checkParts` below.
-   *   2. Check that validity of all references consumed by the type as defined in
-   *      `checkLegalRefs` below
-   */
+  /** Check that all parts of type `tpe` are separated. */
   def checkType(tpe: Type, pos: SrcPos, role: TypeRole)(using Context): Unit =
 
-    /** Check that the parts of type `tpe` are mutually separated.
-     *  This means that references hidden in some part of the type may not
-     *  be explicitly referenced or hidden in some other part.
-     */
     def checkParts(parts: List[Type]): Unit =
-      var footprint: Refs = emptyRefs
-      var hiddenSet: Refs = emptyRefs
+      var footprint: Refs = emptySet
+      var hiddenSet: Refs = emptySet
       var checked = 0
       for part <- parts do
 
@@ -638,15 +501,11 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
       end for
     end checkParts
 
-    /** A traverser that collects part lists to check for separation conditions.
-     *  The accumulator of type `Captures` indicates what kind of captures were
-     *  encountered in previous parts.
-     */
     object traverse extends TypeAccumulator[Captures]:
 
       /** A stack of part lists to check. We maintain this since immediately
-       *  checking parts when traversing the type would check innermost to outermost.
-       *  But we want to check outermost parts first since this prioritizes errors
+       *  checking parts when traversing the type would check innermost to oputermost.
+       *  But we want to check outermost parts first since this prioritized errors
        *  that are more obvious.
        */
       var toCheck: List[List[Type]] = Nil
@@ -665,7 +524,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
               c.add(c1)
             case t @ CapturingType(parent, cs) =>
               val c1 = this(c, parent)
-              if cs.containsRootCapability then c1.add(Captures.Hidden)
+              if cs.elems.containsHidden then c1.add(Captures.Hidden)
               else if !cs.elems.isEmpty then c1.add(Captures.Explicit)
               else c1
             case t: TypeRef if t.symbol.isAbstractOrParamType =>
@@ -676,11 +535,6 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
             case t =>
               foldOver(c, t)
 
-    /** If `tpe` appears as a (result-) type of a definition, treat its
-     *  hidden set minus its explicitly declared footprint as consumed.
-     *  If `tpe` appears as an argument to a @consume parameter, treat
-     *  its footprint as consumed.
-     */
     def checkLegalRefs() = role match
       case TypeRole.Result(sym, _) =>
         if !sym.isAnonymousFunction // we don't check return types of anonymous functions
@@ -704,27 +558,11 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
       checkLegalRefs()
   end checkType
 
-  /** Check the (result-) type of a definition of symbol `sym` */
-  def checkType(tpt: Tree, sym: Symbol)(using Context): Unit =
-    checkType(tpt.nuType, tpt.srcPos,
-        TypeRole.Result(sym, inferred = tpt.isInstanceOf[InferredTypeTree]))
-
-  /** The list of all individual method types making up some potentially
-   *  curried method type.
-   */
   private def collectMethodTypes(tp: Type): List[TermLambda] = tp match
     case tp: MethodType => tp :: collectMethodTypes(tp.resType)
     case tp: PolyType => collectMethodTypes(tp.resType)
     case _ => Nil
 
-  /** The inter-parameter dependencies of the function reference `fn` applied
-   *  to the argument lists `argss`. For instance, if `f` has type
-   *
-   *    f(x: A, y: B^{cap, x}, z: C^{x, y}): D
-   *
-   *  then the dependencies of an application `f(a, b)` is a map that takes
-   *  `b` to `List(a)` and `c` to `List(a, b)`.
-   */
   private def dependencies(fn: Tree, argss: List[List[Tree]])(using Context): collection.Map[Tree, List[Tree]] =
     val mtpe =
       if fn.symbol.exists then fn.symbol.info
@@ -750,10 +588,6 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
       deps(arg) ++= referred
     deps
 
-  /** Decompose an application into a function prefix and a list of argument lists.
-   *  If some of the arguments need a separation check because they are capture polymorphic,
-   *  perform a separation check with `checkApply`
-   */
   private def traverseApply(tree: Tree, argss: List[List[Tree]])(using Context): Unit = tree match
     case Apply(fn, args) => traverseApply(fn, args :: argss)
     case TypeApply(fn, args) => traverseApply(fn, argss) // skip type arguments
@@ -761,16 +595,10 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
       if argss.nestedExists(_.needsSepCheck) then
         checkApply(tree, argss.flatten, dependencies(tree, argss))
 
-  /** Is `tree` an application of `caps.unsafe.unsafeAssumeSeparate`? */
   def isUnsafeAssumeSeparate(tree: Tree)(using Context): Boolean = tree match
     case tree: Apply => tree.symbol == defn.Caps_unsafeAssumeSeparate
     case _ => false
 
-  /** Check (result-) type of `tree` for separation conditions using `checkType`.
-   *  Excluded are parameters and definitions that have an =unsafeAssumeSeparate
-   *  application as right hand sides.
-   *  Hidden sets of checked definitions are added to `defsShadow`.
-   */
   def checkValOrDefDef(tree: ValOrDefDef)(using Context): Unit =
     if !tree.symbol.isOneOf(TermParamOrAccessor) && !isUnsafeAssumeSeparate(tree.rhs) then
       checkType(tree.tpt, tree.symbol)
@@ -780,7 +608,6 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
         resultType(tree.symbol) = tree.tpt.nuType
         previousDefs.head += tree
 
-  /** Traverse `tree` and perform separation checks everywhere */
   def traverse(tree: Tree)(using Context): Unit =
     if isUnsafeAssumeSeparate(tree) then return
     checkUse(tree)
@@ -846,4 +673,4 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
           consumeInLoopError(ref, pos)
       case _ =>
         traverseChildren(tree)
-end SepCheck
\ No newline at end of file
+end SepChecker
\ No newline at end of file
diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala
index 655cdf979859..6232ad640a40 100644
--- a/compiler/src/dotty/tools/dotc/cc/Setup.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -345,18 +345,10 @@ 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.derivesFromSharedCapability =>
+          if refs.isUniversal && parent.derivesFrom(defn.Caps_SharedCapability) =>
             fail(em"$tp extends SharedCapability, so it cannot capture `cap`")
           case _ =>
         tp
diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala
index a0634fa89b6a..b6cf6275f5f5 100644
--- a/compiler/src/dotty/tools/dotc/core/Definitions.scala
+++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala
@@ -1115,6 +1115,8 @@ 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.
diff --git a/compiler/src/dotty/tools/dotc/typer/Checking.scala b/compiler/src/dotty/tools/dotc/typer/Checking.scala
index eefa919d401d..be7cdf8e705e 100644
--- a/compiler/src/dotty/tools/dotc/typer/Checking.scala
+++ b/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 extending the `Mutable` trait")
+      fail(em"Update methods can only be used as members of classes deriving from the `Mutable` trait")
     checkApplicable(Erased,
       !sym.is(Lazy, butNot = Given)
       && !sym.isMutableVarOrAccessor
diff --git a/library/src/scala/caps.scala b/library/src/scala/caps.scala
index 4444bdf7e5b3..50497044fee8 100644
--- a/library/src/scala/caps.scala
+++ b/library/src/scala/caps.scala
@@ -72,22 +72,15 @@ import annotation.{experimental, compileTimeOnly, retainsCap}
    */
   final class use extends annotation.StaticAnnotation
 
-  /** An annotations on parameters and update methods.
-   *  On a parameter it states that any capabilties passed in the argument
-   *  are no longer available afterwards, unless they are of class `SharableCapabilitty`.
-   *  On an update method, it states that the `this` of the enclosing class is
-   *  consumed, which means that any capabilities of the method prefix are
-   *  no longer available afterwards.
-   */
-  final class consume extends annotation.StaticAnnotation
-
   /** An annotation placed on a refinement created by capture checking.
    *  Refinements with this annotation unconditionally override any
-   *  info from the parent type, so no intersection needs to be formed.
+   *  info vfrom the parent type, so no intersection needs to be formed.
    *  This could be useful for tracked parameters as well.
    */
   final class refineOverride extends annotation.StaticAnnotation
 
+  final class consume extends annotation.StaticAnnotation
+
   object unsafe:
 
     extension [T](x: T)
diff --git a/project/Build.scala b/project/Build.scala
index 463abab3f6fd..7411daf621f4 100644
--- a/project/Build.scala
+++ b/project/Build.scala
@@ -1225,7 +1225,7 @@ object Build {
     settings(scala2LibraryBootstrappedSettings).
     settings(
       moduleName := "scala2-library-cc",
-      scalacOptions += "-Ycheck:all",
+      scalacOptions += "-Ycheck:all"
     )
 
   lazy val scala2LibraryBootstrappedSettings = Seq(
diff --git a/scala2-library-cc/src/scala/collection/View.scala b/scala2-library-cc/src/scala/collection/View.scala
index 482884835cb1..b30fa5e508fe 100644
--- a/scala2-library-cc/src/scala/collection/View.scala
+++ b/scala2-library-cc/src/scala/collection/View.scala
@@ -153,9 +153,6 @@ object View extends IterableFactory[View] {
       underlying match {
         case filter: Filter[A]^{underlying} if filter.isFlipped == isFlipped =>
           unsafeAssumeSeparate:
-            // See filter-iterable.scala for a test where a variant of Filter
-            // works without the unsafeAssumeSeparate. But it requires significant
-            // changes compared to the version here. See also Filter in colltest5.CollectionStrawManCC5_1.
             new Filter(filter.underlying, a => filter.p(a) && p(a), isFlipped)
         case _ => new Filter(underlying, p, isFlipped)
       }
diff --git a/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala b/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala
index f12576033622..3cb57784ad95 100644
--- a/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala
+++ b/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala
@@ -24,7 +24,7 @@ import scala.language.implicitConversions
 import scala.runtime.Statics
 import language.experimental.captureChecking
 import annotation.unchecked.uncheckedCaptures
-import caps.{cap, untrackedCaptures}
+import caps.untrackedCaptures
 import caps.unsafe.unsafeAssumeSeparate
 
 /**  This class implements an immutable linked list. We call it "lazy"
@@ -880,7 +880,8 @@ final class LazyListIterable[+A] private(@untrackedCaptures lazyState: () => Laz
         // if cursor (eq scout) has state defined, it is empty; else unknown state
         if (!cursor.stateDefined) b.append(sep).append("<not computed>")
       } else {
-        @inline def same(a: LazyListIterable[A]^, b: LazyListIterable[A]^{cap, a}): Boolean = (a eq b) || (a.state eq b.state)
+        @inline def same(a: LazyListIterable[A]^, b: LazyListIterable[A]^): Boolean = (a eq b) || (a.state eq b.state)
+          // !!!CC with qualifiers, same should have cap.rd parameters
         // Cycle.
         // If we have a prefix of length P followed by a cycle of length C,
         // the scout will be at position (P%C) in the cycle when the cursor
@@ -892,7 +893,7 @@ final class LazyListIterable[+A] private(@untrackedCaptures lazyState: () => Laz
         // the start of the loop.
         var runner = this
         var k = 0
-        while (!same(runner, scout)) {
+        while (!unsafeAssumeSeparate(same(runner, scout))) {
           runner = runner.tail
           scout = scout.tail
           k += 1
@@ -902,11 +903,11 @@ final class LazyListIterable[+A] private(@untrackedCaptures lazyState: () => Laz
         // everything once.  If cursor is already at beginning, we'd better
         // advance one first unless runner didn't go anywhere (in which case
         // we've already looped once).
-        if (same(cursor, scout) && (k > 0)) {
+        if (unsafeAssumeSeparate(same(cursor, scout)) && (k > 0)) {
           appendCursorElement()
           cursor = cursor.tail
         }
-        while (!same(cursor, scout)) {
+        while (!unsafeAssumeSeparate(same(cursor, scout))) {
           appendCursorElement()
           cursor = cursor.tail
         }
@@ -1182,10 +1183,10 @@ object LazyListIterable extends IterableFactory[LazyListIterable] {
     *  @param f     the function that's repeatedly applied
     *  @return      the LazyListIterable returning the infinite sequence of values `start, f(start), f(f(start)), ...`
     */
-  def iterate[A](start: => A)(f: A ->{cap, start} A): LazyListIterable[A]^{start, f} =
+  def iterate[A](start: => A)(f: A => A): LazyListIterable[A]^{start, f} =
     newLL {
       val head = start
-      sCons(head, iterate(f(head))(f))
+      sCons(head, unsafeAssumeSeparate(iterate(f(head))(f)))
     }
 
   /**
diff --git a/scala2-library-cc/src/scala/collection/mutable/CheckedIndexedSeqView.scala b/scala2-library-cc/src/scala/collection/mutable/CheckedIndexedSeqView.scala
index 1c3f669f5358..7bfda7972762 100644
--- a/scala2-library-cc/src/scala/collection/mutable/CheckedIndexedSeqView.scala
+++ b/scala2-library-cc/src/scala/collection/mutable/CheckedIndexedSeqView.scala
@@ -14,11 +14,10 @@ package scala
 package collection
 package mutable
 import language.experimental.captureChecking
-import caps.cap
 
 private[mutable] trait CheckedIndexedSeqView[+A] extends IndexedSeqView[A] {
 
-  protected val mutationCount: () ->{cap.rd} Int
+  protected val mutationCount: () -> Int
 
   override def iterator: Iterator[A]^{this} = new CheckedIndexedSeqView.CheckedIterator(this, mutationCount())
   override def reverseIterator: Iterator[A]^{this} = new CheckedIndexedSeqView.CheckedReverseIterator(this, mutationCount())
@@ -43,7 +42,7 @@ private[mutable] object CheckedIndexedSeqView {
   import IndexedSeqView.SomeIndexedSeqOps
 
   @SerialVersionUID(3L)
-  private[mutable] class CheckedIterator[A](self: IndexedSeqView[A]^, mutationCount: ->{cap.rd} Int)
+  private[mutable] class CheckedIterator[A](self: IndexedSeqView[A]^, mutationCount: -> Int)
     extends IndexedSeqView.IndexedSeqViewIterator[A](self) {
     private[this] val expectedCount = mutationCount
     override def hasNext: Boolean = {
@@ -53,7 +52,7 @@ private[mutable] object CheckedIndexedSeqView {
   }
 
   @SerialVersionUID(3L)
-  private[mutable] class CheckedReverseIterator[A](self: IndexedSeqView[A]^, mutationCount: ->{cap.rd} Int)
+  private[mutable] class CheckedReverseIterator[A](self: IndexedSeqView[A]^, mutationCount: -> Int)
     extends IndexedSeqView.IndexedSeqViewReverseIterator[A](self) {
     private[this] val expectedCount = mutationCount
     override def hasNext: Boolean = {
@@ -63,43 +62,43 @@ private[mutable] object CheckedIndexedSeqView {
   }
 
   @SerialVersionUID(3L)
-  class Id[+A](underlying: SomeIndexedSeqOps[A]^)(protected val mutationCount: () ->{cap.rd} Int)
+  class Id[+A](underlying: SomeIndexedSeqOps[A]^)(protected val mutationCount: () -> Int)
     extends IndexedSeqView.Id(underlying) with CheckedIndexedSeqView[A]
 
   @SerialVersionUID(3L)
-  class Appended[+A](underlying: SomeIndexedSeqOps[A]^, elem: A)(protected val mutationCount: () ->{cap.rd} Int)
+  class Appended[+A](underlying: SomeIndexedSeqOps[A]^, elem: A)(protected val mutationCount: () -> Int)
     extends IndexedSeqView.Appended(underlying, elem) with CheckedIndexedSeqView[A]
 
   @SerialVersionUID(3L)
-  class Prepended[+A](elem: A, underlying: SomeIndexedSeqOps[A]^)(protected val mutationCount: () ->{cap.rd} Int)
+  class Prepended[+A](elem: A, underlying: SomeIndexedSeqOps[A]^)(protected val mutationCount: () -> Int)
     extends IndexedSeqView.Prepended(elem, underlying) with CheckedIndexedSeqView[A]
 
   @SerialVersionUID(3L)
-  class Concat[A](prefix: SomeIndexedSeqOps[A]^, suffix: SomeIndexedSeqOps[A]^)(protected val mutationCount: () ->{cap.rd} Int)
+  class Concat[A](prefix: SomeIndexedSeqOps[A]^, suffix: SomeIndexedSeqOps[A]^)(protected val mutationCount: () -> Int)
     extends IndexedSeqView.Concat[A](prefix, suffix) with CheckedIndexedSeqView[A]
 
   @SerialVersionUID(3L)
-  class Take[A](underlying: SomeIndexedSeqOps[A]^, n: Int)(protected val mutationCount: () ->{cap.rd} Int)
+  class Take[A](underlying: SomeIndexedSeqOps[A]^, n: Int)(protected val mutationCount: () -> Int)
     extends IndexedSeqView.Take(underlying, n) with CheckedIndexedSeqView[A]
 
   @SerialVersionUID(3L)
-  class TakeRight[A](underlying: SomeIndexedSeqOps[A]^, n: Int)(protected val mutationCount: () ->{cap.rd} Int)
+  class TakeRight[A](underlying: SomeIndexedSeqOps[A]^, n: Int)(protected val mutationCount: () -> Int)
     extends IndexedSeqView.TakeRight(underlying, n) with CheckedIndexedSeqView[A]
 
   @SerialVersionUID(3L)
-  class Drop[A](underlying: SomeIndexedSeqOps[A]^, n: Int)(protected val mutationCount: () ->{cap.rd} Int)
+  class Drop[A](underlying: SomeIndexedSeqOps[A]^, n: Int)(protected val mutationCount: () -> Int)
     extends IndexedSeqView.Drop[A](underlying, n) with CheckedIndexedSeqView[A]
 
   @SerialVersionUID(3L)
-  class DropRight[A](underlying: SomeIndexedSeqOps[A]^, n: Int)(protected val mutationCount: () ->{cap.rd} Int)
+  class DropRight[A](underlying: SomeIndexedSeqOps[A]^, n: Int)(protected val mutationCount: () -> Int)
     extends IndexedSeqView.DropRight[A](underlying, n) with CheckedIndexedSeqView[A]
 
   @SerialVersionUID(3L)
-  class Map[A, B](underlying: SomeIndexedSeqOps[A]^, f: A => B)(protected val mutationCount: () ->{cap.rd} Int)
+  class Map[A, B](underlying: SomeIndexedSeqOps[A]^, f: A => B)(protected val mutationCount: () -> Int)
     extends IndexedSeqView.Map(underlying, f) with CheckedIndexedSeqView[B]
 
   @SerialVersionUID(3L)
-  class Reverse[A](underlying: SomeIndexedSeqOps[A]^)(protected val mutationCount: () ->{cap.rd} Int)
+  class Reverse[A](underlying: SomeIndexedSeqOps[A]^)(protected val mutationCount: () -> Int)
     extends IndexedSeqView.Reverse[A](underlying) with CheckedIndexedSeqView[A] {
     override def reverse: IndexedSeqView[A] = underlying match {
       case x: IndexedSeqView[A] => x
@@ -108,7 +107,7 @@ private[mutable] object CheckedIndexedSeqView {
   }
 
   @SerialVersionUID(3L)
-  class Slice[A](underlying: SomeIndexedSeqOps[A]^, from: Int, until: Int)(protected val mutationCount: () ->{cap.rd} Int)
+  class Slice[A](underlying: SomeIndexedSeqOps[A]^, from: Int, until: Int)(protected val mutationCount: () -> Int)
     extends AbstractIndexedSeqView[A] with CheckedIndexedSeqView[A] {
     protected val lo = from max 0
     protected val hi = (until max 0) min underlying.length
diff --git a/tests/neg-custom-args/captures/mut-outside-mutable.check b/tests/neg-custom-args/captures/mut-outside-mutable.check
index bfc1b5161f0a..0407f35745b9 100644
--- a/tests/neg-custom-args/captures/mut-outside-mutable.check
+++ b/tests/neg-custom-args/captures/mut-outside-mutable.check
@@ -1,8 +1,8 @@
 -- Error: tests/neg-custom-args/captures/mut-outside-mutable.scala:5:10 ------------------------------------------------
 5 |  mut def foreach(op: T => Unit): Unit // error
   |          ^
-  |          Update methods can only be used as members of classes extending the `Mutable` trait
+  |          Update methods can only be used as members of classes deriving from the `Mutable` trait
 -- Error: tests/neg-custom-args/captures/mut-outside-mutable.scala:9:12 ------------------------------------------------
 9 |    mut def baz() = 1 // error
   |            ^
-  |            Update methods can only be used as members of classes extending the `Mutable` trait
+  |            Update methods can only be used as members of classes deriving from the `Mutable` trait
diff --git a/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala b/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala
index 54e5f7e2c6fd..e12890a9be9b 100644
--- a/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala
+++ b/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala
@@ -6,6 +6,7 @@ import scala.reflect.ClassTag
 import annotation.unchecked.{uncheckedVariance, uncheckedCaptures}
 import annotation.tailrec
 import caps.cap
+import caps.untrackedCaptures
 import caps.unsafe.unsafeAssumeSeparate
 
 /** A strawman architecture for new collections. It contains some
@@ -68,7 +69,10 @@ object CollectionStrawMan5 {
   /** Base trait for strict collections */
   trait Buildable[+A] extends Iterable[A] {
     protected def newBuilder: Builder[A, Repr] @uncheckedVariance
-    override def partition(p: A => Boolean): (Repr, Repr) =
+    override def partition(p: A => Boolean): (Repr, Repr) @untrackedCaptures =
+      // Without untrackedCaptures this fails SepChecks.checkType.
+      // But this is probably an error in the hiding logic.
+      // TODO remove @untrackedCaptures and investigate
       val l, r = newBuilder
       iterator.foreach(x => (if (p(x)) l else r) += x)
       (l.result, r.result)
@@ -116,7 +120,7 @@ object CollectionStrawMan5 {
     this: SeqLike[A] =>
     type C[X] <: Seq[X]
     def fromIterable[B](coll: Iterable[B]^): C[B]
-    override protected def fromLikeIterable(coll: Iterable[A] @uncheckedVariance ^): Repr =
+    override protected def fromLikeIterable(coll: Iterable[A] @uncheckedVariance ^ ): Repr =
       fromIterable(coll)
 
   trait IterableOps[+A] extends Any {
diff --git a/tests/run-custom-args/captures/colltest5/Test_2.scala b/tests/run-custom-args/captures/colltest5/Test_2.scala
index 2bde8cb5a885..2b3b27c94243 100644
--- a/tests/run-custom-args/captures/colltest5/Test_2.scala
+++ b/tests/run-custom-args/captures/colltest5/Test_2.scala
@@ -1,6 +1,7 @@
 import Predef.{augmentString as _, wrapString as _, *}
 import scala.reflect.ClassTag
 import caps.unsafe.unsafeAssumeSeparate
+import language.`3.7` // sepchecks on
 
 object Test {
   import colltest5.strawman.collections.*