diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
index 25516da531fe..4c3747a47779 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,19 +279,17 @@ 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 => tp1
 
   /** The first element of a path type, but stop at references extending
-   *  SharedCapability.
+   *  SharableCapability
    */
   final def pathRootOrShared(using Context): Type =
-    if tp.derivesFromSharedCapability then tp
+    if tp.derivesFrom(defn.Caps_SharedCapability) 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
@@ -431,7 +427,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 +466,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 +483,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)
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
index 9987b0e91121..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,10 +113,6 @@ 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 goinh through
-   *  a read-only capability first.
-   */
   final def isExclusive(using Context): Boolean =
     !isReadOnly && (isMaxCapability || captureSetOfInfo.isExclusive)
 
@@ -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 =
 
@@ -243,7 +239,7 @@ trait CaptureRef extends TypeProxy, ValueType:
   end subsumes
 
   /** This is a maximal capabaility that subsumes `y` in given context and VarState.
-   *  @param canAddHidden  If true we allow maximal capabilities to subsume all other capabilities.
+   *  @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 1c03cb0b12ad..52a7cd87f647 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -636,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
@@ -1140,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 738281a6a76e..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
-      // contain an exclusive referenece. TODO This should probabkly rolled into
-      // qualifier logic once we have it.
       if tree.symbol.isUpdateMethod && !qualType.captureSet.isExclusive then
         report.error(
             em"""cannot call update ${tree.symbol} from $qualType,
@@ -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
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 ac275bd660e8..889f05ce8308 100644
--- a/compiler/src/dotty/tools/dotc/cc/Fresh.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Fresh.scala
@@ -16,16 +16,11 @@ import util.SimpleIdentitySet.empty
 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,9 +32,6 @@ 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
@@ -47,7 +39,6 @@ object Fresh:
     else
       if ref.isTracked then SimpleIdentitySet(ref) else emptySet
 
-  /** An extractor for "fresh" capabilities */
   object Cap:
 
     def apply(initialHidden: Refs = emptySet)(using Context): CaptureRef =
diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
index 608f39b1aa79..1aee9c467450 100644
--- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
+++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
@@ -411,7 +411,7 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
     def currentOwner = role.dclSym.orElse(ctx.owner)
     for hiddenRef <- prune(refsToCheck, tpe, role) do
       val proot = hiddenRef.pathRootOrShared
-      if !proot.widen.derivesFromSharedCapability then
+      if !proot.widen.derivesFrom(defn.Caps_SharedCapability) then
         proot match
           case ref: TermRef =>
             val refSym = ref.symbol
@@ -448,7 +448,7 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
     role match
       case _: TypeRole.Argument | _: TypeRole.Qualifier =>
         for ref <- refsToCheck do
-          if !ref.pathRootOrShared.derivesFromSharedCapability then
+          if !ref.pathRootOrShared.derivesFrom(defn.Caps_SharedCapability) then
             consumed.put(ref, pos)
       case _ =>
   end checkConsumedRefs
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.*