From 1284bc4a2c62b1a3bdf80beb6b8149fa345f09f5 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Mon, 1 Dec 2025 18:52:18 +0100
Subject: [PATCH 1/6] Test for a new collection class hierarchy respecting
 mutability

---
 .../captures/mut-collections.scala            | 51 +++++++++++++++++++
 1 file changed, 51 insertions(+)
 create mode 100644 tests/pos-custom-args/captures/mut-collections.scala

diff --git a/tests/pos-custom-args/captures/mut-collections.scala b/tests/pos-custom-args/captures/mut-collections.scala
new file mode 100644
index 000000000000..e1f6ebd7c040
--- /dev/null
+++ b/tests/pos-custom-args/captures/mut-collections.scala
@@ -0,0 +1,51 @@
+package colltestMut
+import caps.*
+import collection.*, mutable.*, immutable.*
+
+object collection:
+  trait Iterable[A]:
+    this: Iterable[A]^ =>
+    type C[X] <: Iterable[X]^
+    def map[B](f: A => B): C[B]^{f} = ???
+
+  trait View[A] extends Iterable[A]:
+    this: View[A]^ =>
+    type C[X] = View[X]^{this}
+
+  trait Seq[A] extends Iterable[A]:
+    this: Seq[A]^ =>
+    override def map[B](f: A => B): C[B] = ???
+
+object immutable:
+  import collection.*
+  trait Seq[A] extends Iterable[A], Pure:
+    type C[X] <: Seq[X]
+
+  class List[A] extends Seq[A]:
+    type C[X] = List[X]
+
+
+object mutable:
+  import collection.*
+  trait Seq[A] extends collection.Seq[A]:
+    this: Seq[A]^ =>
+    type C[X] <: Seq[X]^
+
+  trait Buffer[A] extends Seq[A], Mutable:
+    this: Buffer[A]^ =>
+    type C[X] = Buffer[X]^
+
+class IO extends SharedCapability
+class Ref extends Mutable
+
+object Test:
+  def test(io: IO, ref: Ref, f: Int => Int) =
+    val xs1: List[Int] = ???
+    val ys1 = xs1.map(f)
+    val xs2: Buffer[Int]^ = ???
+    val ys2 = xs2.map(f)
+    val xs3: Buffer[Int]^ = ???
+    val zs3 = freeze(xs3)
+    val xs4: Buffer[Int]^ = ???
+    val vs4: View[Int]^{xs4} = ???
+    val ys4 = vs4.map(f)

From 18a6b91adc154e84b475555a93cbf0034b709c56 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Tue, 2 Dec 2025 17:53:19 +0100
Subject: [PATCH 2/6] Show synthesizd tree for type mismatch errors in CC

In capture checking, a type mismatch might happen for a synthesized tree
(say from implicit search). It can be helpful to show this tree. Before
capture checking a helpful message is less likely since we don't synthesize
implicit trees that then don't match under the standard typing rules.
---
 compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala     | 2 +-
 compiler/src/dotty/tools/dotc/typer/ErrorReporting.scala | 9 ++++++++-
 tests/neg-custom-args/captures/boundary.check            | 2 ++
 3 files changed, 11 insertions(+), 2 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 051b4d8f3b5b..72d1e11bb13c 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -1581,7 +1581,7 @@ class CheckCaptures extends Recheck, SymTransformer:
      *  where local capture roots are instantiated to root variables.
      */
     override def checkConformsExpr(actual: Type, expected: Type, tree: Tree, notes: List[Note])(using Context): Type =
-      try testAdapted(actual, expected, tree, notes: List[Note])(err.typeMismatch)
+      try testAdapted(actual, expected, tree, notes)(err.typeMismatch)
       catch case ex: AssertionError =>
         println(i"error while checking $tree: $actual against $expected")
         throw ex
diff --git a/compiler/src/dotty/tools/dotc/typer/ErrorReporting.scala b/compiler/src/dotty/tools/dotc/typer/ErrorReporting.scala
index 76e55cda279f..89818820d575 100644
--- a/compiler/src/dotty/tools/dotc/typer/ErrorReporting.scala
+++ b/compiler/src/dotty/tools/dotc/typer/ErrorReporting.scala
@@ -14,6 +14,7 @@ import config.Feature
 import reporting.*
 import Message.Note
 import collection.mutable
+import cc.isCaptureChecking
 
 object ErrorReporting {
 
@@ -190,7 +191,13 @@ object ErrorReporting {
         case _ =>
           Nil
 
-      errorTree(tree, TypeMismatch(treeTp, expectedTp, Some(tree), notes ++ missingElse))
+      def badTreeNote =
+        val span = tree.span
+        if tree.span.isZeroExtent && isCaptureChecking then
+          Note(i"\n\nThe error occurred for a synthesized tree:  $tree") :: Nil
+        else Nil
+
+      errorTree(tree, TypeMismatch(treeTp, expectedTp, Some(tree), notes ++ missingElse ++ badTreeNote))
     }
 
     /** A subtype log explaining why `found` does not conform to `expected` */
diff --git a/tests/neg-custom-args/captures/boundary.check b/tests/neg-custom-args/captures/boundary.check
index 0c440125a403..f7d2a06b32f0 100644
--- a/tests/neg-custom-args/captures/boundary.check
+++ b/tests/neg-custom-args/captures/boundary.check
@@ -45,6 +45,8 @@
    |
    |  Note that capability cap is not included in capture set {cap²}.
    |
+   |  The error occurred for a synthesized tree:  _
+   |
    |  where:    ^ and cap² refer to the universal root capability
    |            ^² and cap refer to a fresh root capability created in package <empty>
  6 |      boundary[Unit]: l2 ?=>

From 7a7a18f26c62847180e9dcf1ac2647ae75468872 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Wed, 3 Dec 2025 11:38:06 +0100
Subject: [PATCH 3/6] Make Arrays mutable types under separation checking

---
 .../src/dotty/tools/dotc/cc/CaptureOps.scala  |  43 ++++-
 .../src/dotty/tools/dotc/cc/CaptureSet.scala  |  28 ++-
 .../dotty/tools/dotc/cc/CheckCaptures.scala   |  24 +--
 .../src/dotty/tools/dotc/cc/Mutability.scala  |   2 +
 compiler/src/dotty/tools/dotc/cc/Setup.scala  |  13 +-
 .../src/dotty/tools/dotc/cc/ccConfig.scala    |   5 +-
 .../tools/dotc/core/SymDenotations.scala      |   2 +-
 library/src/scala/caps/package.scala          |   2 +-
 .../captures/existential-mapping.check        |   4 +-
 .../captures/freeze-double-flip.check         |   2 +-
 tests/neg-custom-args/captures/freeze.check   |   2 +-
 tests/neg-custom-args/captures/freeze.scala   |   2 +-
 .../captures/mut-widen-empty.check            |  12 ++
 .../captures/mut-widen-empty.scala            |   8 +-
 tests/new/test.scala                          |  45 ++---
 .../captures/capt-depfun2.scala               |   6 +-
 tests/pos-custom-args/captures/freeze.scala   |  18 +-
 .../pos-custom-args/captures/mut-arrays.scala |   9 +
 tests/pos-custom-args/captures/ro-array.scala |   2 +-
 .../captures/sealed-value-class.scala         |   6 +-
 tests/pos-custom-args/captures/steppers.scala |  13 +-
 .../colltest5/CollectionStrawManCC5_1.scala   |  10 +-
 .../captures/minicheck-mutable.scala          | 181 ++++++++++++++++++
 23 files changed, 345 insertions(+), 94 deletions(-)
 create mode 100644 tests/pos-custom-args/captures/mut-arrays.scala
 create mode 100644 tests/run-custom-args/captures/minicheck-mutable.scala

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
index af9a2abc7a9d..217c49f78a8b 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
@@ -394,11 +394,18 @@ extension (tp: Type)
     case _ =>
       false
 
-  def derivesFromCapability(using Context): Boolean = derivesFromCapTrait(defn.Caps_Capability)
-  def derivesFromStateful(using Context): Boolean = derivesFromCapTrait(defn.Caps_Stateful)
-  def derivesFromShared(using Context): Boolean = derivesFromCapTrait(defn.Caps_SharedCapability)
-  def derivesFromUnscoped(using Context): Boolean = derivesFromCapTrait(defn.Caps_Unscoped)
-  def derivesFromMutable(using Context): Boolean = derivesFromCapTrait(defn.Caps_Mutable)
+  def derivesFromCapability(using Context): Boolean =
+    derivesFromCapTrait(defn.Caps_Capability) || isArrayUnderStrictMut
+  def derivesFromStateful(using Context): Boolean =
+    derivesFromCapTrait(defn.Caps_Stateful) || isArrayUnderStrictMut
+  def derivesFromShared(using Context): Boolean =
+    derivesFromCapTrait(defn.Caps_SharedCapability)
+  def derivesFromUnscoped(using Context): Boolean =
+    derivesFromCapTrait(defn.Caps_Unscoped) || isArrayUnderStrictMut
+  def derivesFromMutable(using Context): Boolean =
+    derivesFromCapTrait(defn.Caps_Mutable) || isArrayUnderStrictMut
+
+  def isArrayUnderStrictMut(using Context): Boolean = tp.classSymbol.isArrayUnderStrictMut
 
   /** Drop @retains annotations everywhere */
   def dropAllRetains(using Context): Type = // TODO we should drop retains from inferred types before unpickling
@@ -488,7 +495,8 @@ extension (tp: Type)
       tp
 
   def inheritedClassifier(using Context): ClassSymbol =
-    tp.classSymbols.map(_.classifier).foldLeft(defn.AnyClass)(leastClassifier)
+    if tp.isArrayUnderStrictMut then defn.Caps_Unscoped
+    else tp.classSymbols.map(_.classifier).foldLeft(defn.AnyClass)(leastClassifier)
 
 extension (tp: MethodType)
   /** A method marks an existential scope unless it is the prefix of a curried method */
@@ -553,10 +561,13 @@ extension (sym: Symbol)
    *   - or it is a value class
    *   - or it is an exception
    *   - or it is one of Nothing, Null, or String
+   *  Arrays are not pure under strict mutability even though their self type is declared pure
+   *  in Arrays.scala.
    */
   def isPureClass(using Context): Boolean = sym match
     case cls: ClassSymbol =>
-      cls.pureBaseClass.isDefined || defn.pureSimpleClasses.contains(cls)
+      (cls.pureBaseClass.isDefined || defn.pureSimpleClasses.contains(cls))
+      && !cls.isArrayUnderStrictMut
     case _ =>
       false
 
@@ -588,8 +599,8 @@ extension (sym: Symbol)
     && !defn.isPolymorphicAfterErasure(sym)
     && !defn.isTypeTestOrCast(sym)
 
-  /** It's a parameter accessor that is not annotated @constructorOnly or @uncheckedCaptures
-   *  and that is not a consume accessor.
+  /** It's a parameter accessor for a parameter that that is not annotated
+   *  @constructorOnly or @uncheckedCaptures and that is not a consume parameter.
    */
   def isRefiningParamAccessor(using Context): Boolean =
     sym.is(ParamAccessor)
@@ -600,6 +611,17 @@ extension (sym: Symbol)
       && !param.hasAnnotation(defn.ConsumeAnnot)
     }
 
+  /** It's a parameter accessor that is tracked for capture checking. Excluded are
+   *  accessors for parameters annotated with constructorOnly or @uncheckedCaptures.
+   */
+  def isTrackedParamAccessor(using Context): Boolean =
+    sym.is(ParamAccessor)
+    && {
+      val param = sym.owner.primaryConstructor.paramNamed(sym.name)
+      !param.hasAnnotation(defn.ConstructorOnlyAnnot)
+      && !param.hasAnnotation(defn.UntrackedCapturesAnnot)
+    }
+
   def hasTrackedParts(using Context): Boolean =
     !CaptureSet.ofTypeDeeply(sym.info).isAlwaysEmpty
 
@@ -642,6 +664,9 @@ extension (sym: Symbol)
     else if sym.name.is(TryOwnerName) then i"an enclosing try expression"
     else sym.show
 
+  def isArrayUnderStrictMut(using Context): Boolean =
+    sym == defn.ArrayClass && ccConfig.strictMutability
+
 extension (tp: AnnotatedType)
   /** Is this a boxed capturing type? */
   def isBoxed(using Context): Boolean = tp.annot match
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index d67e344830b1..b042abaa4c75 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -666,13 +666,33 @@ object CaptureSet:
       then i" under-approximating the result of mapping $ref to $mapped"
       else ""
 
-  private def capImpliedByCapability(parent: Type)(using Context): Capability =
-    if parent.derivesFromStateful then GlobalCap.readOnly else GlobalCap
+  private def capImpliedByCapability(parent: Type, sym: Symbol, variance: Int)(using Context): Capability =
+    // Since standard library classes are not compiled with separation checking,
+    // they treat Array as a Pure class. That means, no effort is made to distinguish
+    // between exclusive and read-only arrays. To compensate in code compiled under
+    // strict mutability, we treat contravariant arrays in signatures of stdlib
+    // members as read-only (so all arrays may be passed to them), and co- and
+    // invariant arrays as exclusive.
+    // TODO This scheme should also apply whenever code under strict mutability interfaces
+    // with code compiled without. To do that we will need to store in the Tasty format
+    // a flag whether code was compiled with separation checking on. This will have
+    // to wait until 3.10.
+    def isArrayFromScalaPackage =
+      parent.classSymbol == defn.ArrayClass
+      && ccConfig.strictMutability
+      && variance >= 0
+      && sym.isContainedIn(defn.ScalaPackageClass)
+    if parent.derivesFromStateful && !isArrayFromScalaPackage
+    then GlobalCap.readOnly
+    else GlobalCap
 
   /* The same as {cap} but generated implicitly for references of Capability subtypes.
+   *  @param parent   the type to which the capture set will be attached
+   *  @param sym      the symbol carrying that type
+   *  @param variance the variance in which `parent` appears in the type of `sym`
    */
-  class CSImpliedByCapability(parent: Type)(using @constructorOnly ctx: Context)
-  extends Const(SimpleIdentitySet(capImpliedByCapability(parent)))
+  class CSImpliedByCapability(parent: Type, sym: Symbol, variance: Int)(using @constructorOnly ctx: Context)
+  extends Const(SimpleIdentitySet(capImpliedByCapability(parent, sym, variance)))
 
   /** A special capture set that gets added to the types of symbols that were not
    *  themselves capture checked, in order to admit arbitrary corresponding capture
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 72d1e11bb13c..3e9313ab518f 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -1410,9 +1410,7 @@ class CheckCaptures extends Recheck, SymTransformer:
 
         // (3) Capture set of self type includes capture sets of parameters
         for param <- cls.paramGetters do
-          if !param.hasAnnotation(defn.ConstructorOnlyAnnot)
-              && !param.hasAnnotation(defn.UntrackedCapturesAnnot)
-          then
+          if param.isTrackedParamAccessor then
             withCapAsRoot: // OK? We need this here since self types use `cap` instead of `fresh`
               checkSubset(param.termRef.captureSet, thisSet, param.srcPos)
 
@@ -2148,26 +2146,6 @@ class CheckCaptures extends Recheck, SymTransformer:
         checker.traverse(tree.nuType)
     end checkTypeParam
 
-    /** Under the unsealed policy: Arrays are like vars, check that their element types
-     *  do not contains `cap` (in fact it would work also to check on array creation
-     *  like we do under sealed).
-     */
-    def checkArraysAreSealedIn(tp: Type, pos: SrcPos)(using Context): Unit =
-      val check = new TypeTraverser:
-        def traverse(t: Type): Unit =
-          t match
-            case AppliedType(tycon, arg :: Nil) if tycon.typeSymbol == defn.ArrayClass =>
-              if !(pos.span.isSynthetic && ctx.reporter.errorsReported)
-                && !arg.typeSymbol.name.is(WildcardParamName)
-              then
-                disallowBadRootsIn(arg, NoSymbol, "Array", "have element type", "", pos)
-              traverseChildren(t)
-            case defn.RefinedFunctionOf(rinfo: MethodType) =>
-              traverse(rinfo)
-            case _ =>
-              traverseChildren(t)
-      check.traverse(tp)
-
     /** Check that no uses refer to reach capabilities of parameters of enclosing
      *  methods or classes.
      */
diff --git a/compiler/src/dotty/tools/dotc/cc/Mutability.scala b/compiler/src/dotty/tools/dotc/cc/Mutability.scala
index e788d32dba9b..9c4b3fb40961 100644
--- a/compiler/src/dotty/tools/dotc/cc/Mutability.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Mutability.scala
@@ -10,6 +10,7 @@ import config.Printers.capt
 import config.Feature
 import ast.tpd.Tree
 import typer.ProtoTypes.LhsProto
+import StdNames.nme
 
 /** Handling mutability and read-only access
  */
@@ -59,6 +60,7 @@ object Mutability:
               && !sym.field.hasAnnotation(defn.UntrackedCapturesAnnot)
             else true
            )
+      || ccConfig.strictMutability && sym.name == nme.update && sym == defn.Array_update
 
     /** A read-only member is a lazy val or a method that is not an update method. */
     def isReadOnlyMember(using Context): Boolean =
diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala
index 5c8c581f729c..2feb716d62ba 100644
--- a/compiler/src/dotty/tools/dotc/cc/Setup.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -165,9 +165,14 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
     if !pastRecheck && Feature.ccEnabledSomewhere then
       val sym = symd.symbol
       def mappedInfo =
-        if toBeUpdated.contains(sym)
-        then symd.info // don't transform symbols that will anyway be updated
-        else transformExplicitType(symd.info, sym)
+        if toBeUpdated.contains(sym) then
+          symd.info // don't transform symbols that will anyway be updated
+        else if sym.isArrayUnderStrictMut then
+          val cinfo: ClassInfo = sym.info.asInstanceOf
+          cinfo.derivedClassInfo(
+            declaredParents = cinfo.declaredParents :+ defn.Caps_Mutable.typeRef)
+        else
+          transformExplicitType(symd.info, sym)
       if Synthetics.needsTransform(symd) then
         Synthetics.transform(symd, mappedInfo)
       else if isPreCC(sym) then
@@ -425,7 +430,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
         then
           normalizeCaptures(mapOver(t)) match
             case t1 @ CapturingType(_, _) => t1
-            case t1 => CapturingType(t1, CaptureSet.CSImpliedByCapability(t1), boxed = false)
+            case t1 => CapturingType(t1, CaptureSet.CSImpliedByCapability(t1, sym, variance), boxed = false)
         else normalizeCaptures(mapFollowingAliases(t))
 
       def innerApply(t: Type) =
diff --git a/compiler/src/dotty/tools/dotc/cc/ccConfig.scala b/compiler/src/dotty/tools/dotc/cc/ccConfig.scala
index 5ea8b17d8aaf..9823f68ba8b0 100644
--- a/compiler/src/dotty/tools/dotc/cc/ccConfig.scala
+++ b/compiler/src/dotty/tools/dotc/cc/ccConfig.scala
@@ -61,9 +61,12 @@ object ccConfig:
   def newScheme(using ctx: Context): Boolean =
     Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.7`)
 
+  /** Allow @use annotations */
   def allowUse(using Context): Boolean =
     Feature.sourceVersion.stable.isAtMost(SourceVersion.`3.7`)
 
-
+  /** Treat arrays as mutable types. Enabled under separation checking */
+  def strictMutability(using Context): Boolean =
+    Feature.enabled(Feature.separationChecking)
 
 end ccConfig
diff --git a/compiler/src/dotty/tools/dotc/core/SymDenotations.scala b/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
index 3b198ea4dbaa..5e6dd471e304 100644
--- a/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
+++ b/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
@@ -1886,7 +1886,7 @@ object SymDenotations {
       myBaseTypeCache.nn
     }
 
-    private def invalidateBaseDataCache() = {
+    def invalidateBaseDataCache() = {
       baseDataCache.invalidate()
       baseDataCache = BaseData.None
     }
diff --git a/library/src/scala/caps/package.scala b/library/src/scala/caps/package.scala
index b0975da27607..772af102e942 100644
--- a/library/src/scala/caps/package.scala
+++ b/library/src/scala/caps/package.scala
@@ -195,7 +195,7 @@ end internal
  *  result of pure operation `op`, turning them into immutable types.
  */
 @experimental
-def freeze(@internal.consume x: Mutable): x.type = x
+def freeze(@internal.consume x: Mutable | Array[?]): x.type = x
 
 @experimental
 object unsafe:
diff --git a/tests/neg-custom-args/captures/existential-mapping.check b/tests/neg-custom-args/captures/existential-mapping.check
index 67f4afc25373..10f43e941e2e 100644
--- a/tests/neg-custom-args/captures/existential-mapping.check
+++ b/tests/neg-custom-args/captures/existential-mapping.check
@@ -1,10 +1,10 @@
 -- Error: tests/neg-custom-args/captures/existential-mapping.scala:46:10 -----------------------------------------------
 46 |  val z2: (x: A^) => Array[C^] = ??? // error
    |          ^^^^^^^^^^^^^^^^^^^^
-   |          Array[C^] captures the root capability `cap` in invariant position.
+   |          Array[C^]^{cap.rd} captures the root capability `cap` in invariant position.
    |          This capability cannot be converted to an existential in the result type of a function.
    |
-   |          where:    ^ refers to the universal root capability
+   |          where:    ^ and cap refer to the universal root capability
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:9:25 ---------------------------
 9 |  val _:  (x: C^) -> C = x1 // error
   |                         ^^
diff --git a/tests/neg-custom-args/captures/freeze-double-flip.check b/tests/neg-custom-args/captures/freeze-double-flip.check
index 949044982689..dfdc95e19519 100644
--- a/tests/neg-custom-args/captures/freeze-double-flip.check
+++ b/tests/neg-custom-args/captures/freeze-double-flip.check
@@ -2,6 +2,6 @@
 15 |    (x: Ref^) => (op: Ref^ => IRef) => op(x) // error
    |    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |    Found:    Ref^ -> (Ref^ => IRef) -> IRef
-   |    Required: scala.caps.Mutable
+   |    Required: scala.caps.Mutable | Array[?]
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/freeze.check b/tests/neg-custom-args/captures/freeze.check
index da865c0c8b43..9e0bbc2a8e36 100644
--- a/tests/neg-custom-args/captures/freeze.check
+++ b/tests/neg-custom-args/captures/freeze.check
@@ -2,6 +2,6 @@
 11 |  val b = freeze((a, a)) // error
    |                 ^^^^^^
    |                 Found:    (Arr[String], Arr[String])
-   |                 Required: scala.caps.Mutable
+   |                 Required: scala.caps.Mutable | Array[?]
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/freeze.scala b/tests/neg-custom-args/captures/freeze.scala
index 8f1a168fe2d2..81542f438c8e 100644
--- a/tests/neg-custom-args/captures/freeze.scala
+++ b/tests/neg-custom-args/captures/freeze.scala
@@ -1,7 +1,7 @@
 import caps.*
 
 class Arr[T: reflect.ClassTag](len: Int) extends Mutable:
-  private val arr: Array[T] = new Array[T](len)
+  private val arr: Array[T]^ = new Array[T](len)
   def get(i: Int): T = arr(i)
   update def update(i: Int, x: T): Unit = arr(i) = x
 
diff --git a/tests/neg-custom-args/captures/mut-widen-empty.check b/tests/neg-custom-args/captures/mut-widen-empty.check
index b3ab5df59979..2a23fdeab58a 100644
--- a/tests/neg-custom-args/captures/mut-widen-empty.check
+++ b/tests/neg-custom-args/captures/mut-widen-empty.check
@@ -10,3 +10,15 @@
    |              where:    ^ and cap refer to a fresh root capability classified as Unscoped in the type of value c
    |
    | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mut-widen-empty.scala:18:26 ------------------------------
+18 |  val c: Array[String]^ = b  // error
+   |                          ^
+   |              Found:    (b : Array[String]^{})
+   |              Required: Array[String]^
+   |
+   |              Note that {cap} is an exclusive capture set of the stateful type Array[String]^,
+   |              it cannot subsume a read-only capture set of the stateful type Array[String]^{}.
+   |
+   |              where:    ^ and cap refer to a fresh root capability classified as Unscoped in the type of value c
+   |
+   | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/mut-widen-empty.scala b/tests/neg-custom-args/captures/mut-widen-empty.scala
index 9e10c040a046..8ff95f210e10 100644
--- a/tests/neg-custom-args/captures/mut-widen-empty.scala
+++ b/tests/neg-custom-args/captures/mut-widen-empty.scala
@@ -1,7 +1,7 @@
 import caps.*
 
 class Arr[T: reflect.ClassTag](len: Int) extends Mutable:
-  private val arr: Array[T] = new Array[T](len)
+  private val arr: Array[T]^ = new Array[T](len)
   def get(i: Int): T = arr(i)
   update def update(i: Int, x: T): Unit = arr(i) = x
 
@@ -12,3 +12,9 @@ def test2 =
   val c: Arr[String]^ = b  // error
   c(2) = "a"   // boom!
 
+def test3 =
+  val a = new Array[String](2)
+  val b: Array[String]^{} = ???
+  val c: Array[String]^ = b  // error
+  c(2) = "a"   // boom!
+
diff --git a/tests/new/test.scala b/tests/new/test.scala
index 4541893e0ffb..b9be7bc5b47b 100644
--- a/tests/new/test.scala
+++ b/tests/new/test.scala
@@ -1,27 +1,18 @@
-import caps.*
-
-class Ref[T](init: T) extends caps.Stateful, Unscoped:
-  var x = init
-  def get: T = x
-  update def put(y: T): Unit = x = y
-
-class File:
-  def read(): String = ???
-
-def withFile[T](op: (f: File^) => T): T =
-  op(new File)
-
-def withFileAndRef[T](op: (f: File^, r: Ref[String]^) => T): T =
-  op(File(), Ref(""))
-
-def Test =
-/*
-  withFileAndRef: (f, r: Ref[String]^) =>
-    r.put(f.read())
-*/
-
-  withFileAndRef: (f, r) =>
-    r.put(f.read())
-
-
-
+import caps.unsafe.untrackedCaptures
+
+class ArrayBuffer[A] private (@untrackedCaptures initElems: Array[AnyRef]^, initLength: Int):
+  private var elems: Array[AnyRef]^ = initElems
+  private var start = 0
+  private var end = initLength
+
+  def +=(elem: A): this.type =
+    elems(end) = elem.asInstanceOf[AnyRef]
+    this
+
+  override def toString =
+    val slice = elems.slice(start, end)
+    val wrapped = wrapRefArray(slice)
+    //val wrapped2 = collection.mutable.ArraySeq.ofRef(slice)
+    val str = wrapped.mkString(", ")
+    str
+    //s"ArrayBuffer(${elems.slice(start, end).mkString(", ")})"
diff --git a/tests/pos-custom-args/captures/capt-depfun2.scala b/tests/pos-custom-args/captures/capt-depfun2.scala
index 4451deb27c76..0affafa8bb48 100644
--- a/tests/pos-custom-args/captures/capt-depfun2.scala
+++ b/tests/pos-custom-args/captures/capt-depfun2.scala
@@ -3,9 +3,11 @@ import annotation.retains
 class C
 type Cap = C @retains[caps.cap.type]
 
+class Arr[T]
+
 class STR
 def f(consume y: Cap, consume z: Cap) =
   def g(): C @retains[y.type | z.type] = ???
-  val ac: ((x: Cap) -> Array[STR @retains[x.type]]) = ???
-  val dc: Array[? >: STR <: STR^]^{y, z} = ac(g()) // needs to be inferred
+  val ac: ((x: Cap) => Arr[STR @retains[x.type]]^{x}) = ???
+  val dc: Arr[? >: STR <: STR^]^{y, z} = ac(g()) // needs to be inferred
   val ec = ac(y)
diff --git a/tests/pos-custom-args/captures/freeze.scala b/tests/pos-custom-args/captures/freeze.scala
index b979cb5cf193..3fe7f22e9d5f 100644
--- a/tests/pos-custom-args/captures/freeze.scala
+++ b/tests/pos-custom-args/captures/freeze.scala
@@ -2,7 +2,7 @@ import language.experimental.captureChecking
 import caps.*
 
 class Arr[T: reflect.ClassTag](len: Int) extends Mutable:
-  private val arr: Array[T] = new Array[T](len)
+  private val arr: Array[T]^ = new Array[T](len)
   def get(i: Int): T = arr(i)
   update def update(i: Int, x: T): Unit = arr(i) = x
 
@@ -23,3 +23,19 @@ def test3 =
   val _: Arr[String]^{} = b
   b
 
+def test4 =
+  val a = freeze:
+    val a = new Array[String](2)
+    a(0) = "1"
+    a(1) = "2"
+    a
+  val _: Array[String]^{} = a
+
+def test5 =
+  val a = new Array[String](2)
+  a(0) = "1"
+  a(1) = "2"
+  val b = freeze(a)
+  val _: Array[String]^{} = b
+  b
+
diff --git a/tests/pos-custom-args/captures/mut-arrays.scala b/tests/pos-custom-args/captures/mut-arrays.scala
new file mode 100644
index 000000000000..270a37a49c23
--- /dev/null
+++ b/tests/pos-custom-args/captures/mut-arrays.scala
@@ -0,0 +1,9 @@
+
+
+def Test =
+  val a1 = new Array[Int](3)
+  val a2 = Array.fill(3)(0)
+  val a3 = a1 ++ a2
+
+  def f = () => a1(0) = 2
+  def g = () => a1(0)
diff --git a/tests/pos-custom-args/captures/ro-array.scala b/tests/pos-custom-args/captures/ro-array.scala
index bcc4aa1be1c5..708331ca547d 100644
--- a/tests/pos-custom-args/captures/ro-array.scala
+++ b/tests/pos-custom-args/captures/ro-array.scala
@@ -2,7 +2,7 @@ import caps.*
 object Test
 
 class Arr[T: reflect.ClassTag](a: Async, len: Int) extends Stateful:
-  private val arr: Array[T] = new Array[T](len)
+  private val arr: Array[T]^ = new Array[T](len)
   def get(i: Int): T = arr(i)
   update def set(i: Int, x: T): Unit = arr(i) = x
 
diff --git a/tests/pos-custom-args/captures/sealed-value-class.scala b/tests/pos-custom-args/captures/sealed-value-class.scala
index 7d2a223be91f..a4850255315b 100644
--- a/tests/pos-custom-args/captures/sealed-value-class.scala
+++ b/tests/pos-custom-args/captures/sealed-value-class.scala
@@ -1,3 +1,3 @@
-class Ops[A](xs: Array[A]) extends AnyVal:
-
-  def f(p: A => Boolean): Array[A] = xs
+class Ops[A](xs: Array[A]^) extends AnyVal:
+  this: Ops[A]^ =>
+  def f(p: A => Boolean): Array[A]^{this} = xs
diff --git a/tests/pos-custom-args/captures/steppers.scala b/tests/pos-custom-args/captures/steppers.scala
index 0d99e305bb22..756bb9def891 100644
--- a/tests/pos-custom-args/captures/steppers.scala
+++ b/tests/pos-custom-args/captures/steppers.scala
@@ -1,25 +1,26 @@
+import caps.unsafe.untrackedCaptures
 
 trait Stepper[+A]
 
 object Stepper:
   trait EfficientSplit
 
-sealed trait StepperShape[-T, S <: Stepper[_]^] extends caps.Pure
+sealed trait StepperShape[-T, S <: Stepper[?]^] extends caps.Pure
 
 trait IterableOnce[+A] extends Any:
-  def stepper[S <: Stepper[_]^{this}](implicit shape: StepperShape[A, S]): S = ???
+  def stepper[S <: Stepper[?]^{this}](implicit shape: StepperShape[A, S]): S = ???
 
 sealed abstract class ArraySeq[T] extends IterableOnce[T], caps.Pure:
-  def array: Array[_]
+  val array: Array[?]
 
   def sorted[B >: T](implicit ord: Ordering[B]): ArraySeq[T] =
-    val arr = array.asInstanceOf[Array[T]].sorted(ord.asInstanceOf[Ordering[Any]]).asInstanceOf[Array[T]]
+    val arr = array.asInstanceOf[Array[T]].sorted(using ord.asInstanceOf[Ordering[Any]]).asInstanceOf[Array[T]]
     ArraySeq.make(arr).asInstanceOf[ArraySeq[T]]
 
 object ArraySeq:
 
   def make[T](x: Array[T]): ArraySeq[T] = ???
 
-  final class ofRef[T <: AnyRef](val array: Array[T]) extends ArraySeq[T], caps.Pure:
-    override def stepper[S <: Stepper[_]](implicit shape: StepperShape[T, S]): S & Stepper.EfficientSplit = ???
+  final class ofRef[T <: AnyRef](@untrackedCaptures val array: Array[T]) extends ArraySeq[T], caps.Pure:
+    override def stepper[S <: Stepper[?]](implicit shape: StepperShape[T, S]): S & Stepper.EfficientSplit = ???
 
diff --git a/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala b/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala
index 2de3ba603507..a5488b28d420 100644
--- a/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala
+++ b/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala
@@ -6,7 +6,7 @@ import scala.reflect.ClassTag
 import annotation.unchecked.{uncheckedVariance, uncheckedCaptures}
 import annotation.tailrec
 import caps.cap
-import caps.unsafe.unsafeAssumeSeparate
+import caps.unsafe.{unsafeAssumeSeparate, untrackedCaptures}
 
 import language.experimental.captureChecking
 
@@ -295,12 +295,12 @@ object CollectionStrawMan5 {
   }
 
   /** Concrete collection type: ArrayBuffer */
-  class ArrayBuffer[A] private (initElems: Array[AnyRef], initLength: Int)
+  class ArrayBuffer[A] private (@untrackedCaptures initElems: Array[AnyRef]^, initLength: Int)
   extends Seq[A] with SeqLike[A] with Builder[A, ArrayBuffer[A]] {
-    this: ArrayBuffer[A] =>
+    //this: ArrayBuffer[A] =>
     type C[X] = ArrayBuffer[X]
     def this() = this(new Array[AnyRef](16), 0)
-    private var elems: Array[AnyRef] = initElems
+    private var elems: Array[AnyRef]^ = initElems
     private var start = 0
     private var end = initLength
     def apply(n: Int) = elems(start + n).asInstanceOf[A]
@@ -358,7 +358,7 @@ object CollectionStrawMan5 {
       }
   }
 
-  class ArrayBufferView[A](val elems: Array[AnyRef], val start: Int, val end: Int) extends RandomAccessView[A] {
+  class ArrayBufferView[A](@untrackedCaptures val elems: Array[AnyRef]^, val start: Int, val end: Int) extends RandomAccessView[A] {
     this: ArrayBufferView[A] =>
     def apply(n: Int) = elems(start + n).asInstanceOf[A]
   }
diff --git a/tests/run-custom-args/captures/minicheck-mutable.scala b/tests/run-custom-args/captures/minicheck-mutable.scala
new file mode 100644
index 000000000000..ca2050955f7c
--- /dev/null
+++ b/tests/run-custom-args/captures/minicheck-mutable.scala
@@ -0,0 +1,181 @@
+// A mini typechecker to experiment with arena allocated contexts
+import compiletime.uninitialized
+import annotation.{experimental, tailrec, constructorOnly}
+import collection.mutable
+import caps.*
+import caps.unsafe.{untrackedCaptures, unsafeDiscardUses}
+
+case class Symbol(name: String, initOwner: Symbol | Null) extends caps.Pure:
+  def owner = initOwner.nn
+  @untrackedCaptures private var myInfo: Type = uninitialized
+  def infoOrCompleter: Type = myInfo
+  def info: Type =
+    infoOrCompleter match
+      case completer: LazyType =>
+        myInfo = NoType
+        completer.complete()
+        info
+      case NoType =>
+        throw TypeError(s"cyclic reference involving $name")
+      case tp =>
+        tp
+  def info_=(tp: Type) = myInfo = tp
+  def exists: Boolean = true
+  def orElse(alt: => Symbol): Symbol = this
+
+object NoSymbol extends Symbol("", null):
+  override def owner = assert(false, "NoSymbol.owner")
+  override def infoOrCompleter = NoType
+  override def exists: Boolean = false
+  override def orElse(alt: => Symbol): Symbol = alt
+
+abstract class Type extends caps.Pure:
+  def exists = true
+  def show: String
+case class IntType()(using @constructorOnly c: Context) extends Type:
+  def show = "Int"
+case class StringType()(using @constructorOnly c: Context) extends Type:
+  def show = "String"
+case object NoType extends Type:
+  override def exists = false
+  def show = "<none>"
+
+abstract class LazyType(using Context) extends Type:
+  def complete(): Unit = doComplete()
+  def doComplete()(using Context): Unit
+  def show = "?"
+
+enum Tree:
+  case Let(bindings: List[Binding], res: Tree)
+  case Ref(name: String)
+  case Add(x: Tree, y: Tree)
+  case Length(x: Tree)
+  case Lit(value: Any)
+
+case class Binding(name: String, rhs: Tree)
+
+class Scope:
+  private val elems = mutable.Map[String, Symbol]()
+  def enter(sym: Symbol)(using Context, Reporter^): Unit =
+    if elems.contains(sym.name) then
+      report.error(s"duplicate definition: ${sym.name}")
+    elems(sym.name) = sym
+  def lookup(name: String): Symbol =
+    elems.getOrElse(name, NoSymbol)
+  def elements: Iterator[Symbol] = elems.valuesIterator
+
+object EmptyScope extends Scope
+
+class TypeError(val msg: String) extends Exception
+
+class Reporter extends Stateful:
+  var errorCount = 0
+  update def error(msg: -> String)(using Context) =
+    errorCount += 1
+    println(s"ERROR: $msg")
+
+abstract class Context:
+  def outer: Context
+  def owner: Symbol
+  def scope: Scope
+
+class FreshContext(using val outer: Context)
+    (val owner: Symbol = outer.owner, val scope: Scope = outer.scope) extends Context
+
+object NoContext extends Context:
+  def outer = ???
+  def owner = NoSymbol
+  def scope = EmptyScope
+
+def ctx(using c: Context): Context = c
+def report(using r: Reporter^): r.type = r
+
+def withOwner[T](owner: Symbol)(op: Context ?=> T)(using Context): T =
+  op(using FreshContext(owner = owner))
+
+def withScope[T](scope: Scope)(op: Context ?=> T)(using Context): T =
+  op(using FreshContext(scope = scope))
+
+def typed(tree: Tree, expected: Type = NoType)(using Context, Reporter^): Type =
+  try
+    val tp = typedUnadapted(tree, expected)
+    if expected.exists && tp != expected then
+      report.error:
+        s"""Type error
+          |  found   : $tp
+          |  expected: $expected
+          |  for     : $tree""".stripMargin
+    tp
+  catch case ex: TypeError =>
+    report.error(ex.msg)
+    NoType
+
+import Tree.*
+def typedUnadapted(tree: Tree, expected: Type = NoType)(using ctx: Context, rep: Reporter^): Type = tree match
+  case Let(bindings, res) =>
+    withScope(Scope()):
+      for Binding(name, rhs) <- bindings do
+        val sym = Symbol(name, ctx.owner)
+        sym.info = new LazyType:
+          override def doComplete()(using Context) =
+            sym.info = withOwner(sym):
+              typed(rhs)(using ctx, unsafeDiscardUses(rep))
+        ctx.scope.enter(sym)
+      for sym <- ctx.scope.elements do sym.info
+      typed(res, expected)
+  case Ref(name: String) =>
+    def findIn(c: Context): Symbol =
+      val sym = c.scope.lookup(name)
+      if sym.exists || (c eq NoContext) then sym
+      else findIn(c.outer)
+    findIn(ctx).info
+  case Add(x: Tree, y: Tree) =>
+    typed(x, IntType())
+    typed(y, IntType())
+    IntType()
+  case Length(x: Tree) =>
+    typed(x, StringType())
+    IntType()
+  case Lit(value: Any) =>
+    value match
+      case value: Int => IntType()
+      case value: String => StringType()
+      case _ =>
+        report.error(s"Int or String literal expected by $value found")
+        NoType
+
+object sugar:
+  extension (tree: Tree)
+    infix def where(bindings: Binding*) = Let(bindings.toList, tree)
+    def + (other: Tree) = Add(tree, other)
+
+  extension (name: String)
+    def := (rhs: Tree) = Binding(name, rhs)
+
+import sugar.*
+
+val prog =
+  Ref("x") + Length(Ref("s")) where (
+    "x" := Lit(1) + Length(Ref("s")),
+    "s" := Lit("abc"))
+
+val bad = Ref("x") + Ref("s") where (
+    "x" := Lit(1),
+    "s" := Lit("abc"))
+
+val cyclic =
+  Ref("x") + Length(Ref("s")) where (
+    "x" := Lit(1) + Ref("x"),
+    "s" := Lit("abc"))
+
+def compile(tree: Tree)(using Context) =
+  val reporter = Reporter()
+  val tp = typed(tree)(using ctx, reporter)
+  if reporter.errorCount == 0 then
+    println(s"OK $tp")
+
+@main def Test =
+  given Context = NoContext
+  compile(prog)
+  compile(bad)
+  compile(cyclic)

From d27544a0ce28436b52b8fb3f72d2542a178e5fe5 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Thu, 4 Dec 2025 13:30:34 +0100
Subject: [PATCH 4/6] Put consume and untrackedCaptures annotations also on
 parameter accessors

---
 library/src/scala/caps/package.scala | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/library/src/scala/caps/package.scala b/library/src/scala/caps/package.scala
index 772af102e942..b63c9b4cd6fe 100644
--- a/library/src/scala/caps/package.scala
+++ b/library/src/scala/caps/package.scala
@@ -4,6 +4,7 @@ package caps
 import language.experimental.captureChecking
 
 import annotation.{experimental, compileTimeOnly, retainsCap}
+import annotation.meta.*
 
 /**
  * Base trait for classes that represent capabilities in the
@@ -157,6 +158,7 @@ object internal:
   /** An annotation to reflect that a parameter or method carries the `consume`
    *  soft modifier.
    */
+  @getter @param
   final class consume extends annotation.StaticAnnotation
 
   /** An internal annotation placed on a refinement created by capture checking.
@@ -193,6 +195,8 @@ end internal
 
 /** A wrapper that strips all covariant capture sets from Mutable types in the
  *  result of pure operation `op`, turning them into immutable types.
+ *  Array[?] is also included since it counts as a Mutable type for
+ *  separation checking.
  */
 @experimental
 def freeze(@internal.consume x: Mutable | Array[?]): x.type = x
@@ -220,6 +224,7 @@ object unsafe:
    * @note This should go into annotations. For now it is here, so that we
    *  can experiment with it quickly between minor releases
    */
+  @getter @param
   final class untrackedCaptures extends annotation.StaticAnnotation
 
   extension [T](x: T)

From 3edb4bf74b893d033ce8377dfc8dd3dacd0eb945 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Thu, 4 Dec 2025 17:45:41 +0100
Subject: [PATCH 5/6] Enforce mutable field restrictions under separation
 checking.

Fields are only allowed in stateful classes unless marked with @untrackedCaptures.
---
 .../dotty/tools/dotc/cc/CheckCaptures.scala   |  2 +-
 .../src/dotty/tools/dotc/cc/ccConfig.scala    | 10 ++---
 .../captures/cc-poly-source.scala             |  2 +-
 .../captures/class-level-attack.check         | 18 ++++----
 .../captures/class-level-attack.scala         | 10 ++---
 .../captures/filevar-expanded.scala           |  2 +-
 .../captures/filevar-multi-ios.scala          |  4 +-
 tests/neg-custom-args/captures/filevar.scala  |  2 +-
 tests/neg-custom-args/captures/i21920.scala   |  2 +-
 tests/neg-custom-args/captures/i24137.check   | 22 ----------
 .../captures/i24309-region-orig.scala         |  2 +-
 tests/neg-custom-args/captures/levels.scala   |  8 ++--
 tests/neg-custom-args/captures/reaches.check  | 14 +++---
 tests/neg-custom-args/captures/reaches.scala  |  4 +-
 .../captures/reference-cc.scala               |  6 +--
 tests/neg-custom-args/captures/ro-buf.scala   | 43 +++++++++++++++++++
 .../captures/scope-extrude-mut.scala          |  2 +-
 .../captures/stack-alloc.scala                | 25 +++++------
 tests/neg-custom-args/captures/vars.scala     |  2 +-
 tests/new/test.scala                          | 19 +-------
 tests/pos-custom-args/captures/buffers.scala  |  2 +-
 tests/pos-custom-args/captures/cc-cast.scala  |  2 +-
 .../captures/cc-poly-source-capability.scala  |  3 +-
 .../captures/drop-refinement.scala            |  7 +--
 .../captures/filevar-tracked.scala            |  2 +-
 tests/pos-custom-args/captures/filevar.scala  |  2 +-
 tests/pos-custom-args/captures/i21507.scala   |  3 +-
 tests/pos-custom-args/captures/i22723.scala   |  2 +-
 .../captures/i24137.scala                     |  8 ++--
 .../captures/i24309-region.scala              |  3 +-
 .../pos-custom-args/captures/iterators.scala  |  3 +-
 .../captures/lazylists-exceptions.scala       |  5 ++-
 tests/pos-custom-args/captures/reaches.scala  |  4 +-
 .../captures/secondary-constructors.scala     |  3 +-
 .../captures/stack-alloc.scala                | 23 +++++-----
 tests/pos-custom-args/captures/test.scala     |  4 +-
 .../captures/trickyTrailingUpArrow.scala      |  2 +-
 .../captures/unsafe-captures.scala            |  4 +-
 tests/pos-custom-args/captures/vars.scala     |  2 +-
 tests/pos-custom-args/captures/vars1.scala    |  2 +-
 .../colltest5/CollectionStrawManCC5_1.scala   | 26 +++++------
 .../run-custom-args/captures/minicheck.scala  | 17 ++++----
 42 files changed, 171 insertions(+), 157 deletions(-)
 delete mode 100644 tests/neg-custom-args/captures/i24137.check
 create mode 100644 tests/neg-custom-args/captures/ro-buf.scala
 rename tests/{neg-custom-args => pos-custom-args}/captures/i24137.scala (57%)

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 3e9313ab518f..683428cbdabe 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -1170,7 +1170,7 @@ class CheckCaptures extends Recheck, SymTransformer:
                   ""
               disallowBadRootsIn(
                 tree.tpt.nuType, NoSymbol, i"Mutable $sym", "have type", addendum, sym.srcPos)
-            if ccConfig.noUnsafeMutableFields
+            if ccConfig.strictMutability
                 && sym.owner.isClass
                 && !sym.owner.derivesFrom(defn.Caps_Stateful)
                 && !sym.hasAnnotation(defn.UntrackedCapturesAnnot) then
diff --git a/compiler/src/dotty/tools/dotc/cc/ccConfig.scala b/compiler/src/dotty/tools/dotc/cc/ccConfig.scala
index 9823f68ba8b0..4140f80ae43b 100644
--- a/compiler/src/dotty/tools/dotc/cc/ccConfig.scala
+++ b/compiler/src/dotty/tools/dotc/cc/ccConfig.scala
@@ -48,11 +48,6 @@ object ccConfig:
    */
   inline val useSpanCapset = false
 
-  /** If true force all mutable fields to be in Stateful classes, unless they
-   *  are annotated with @untrackedCaptures
-   */
-  inline val noUnsafeMutableFields = false
-
   /** If true, do level checking for FreshCap instances */
   def useFreshLevels(using Context): Boolean =
     Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.7`)
@@ -65,7 +60,10 @@ object ccConfig:
   def allowUse(using Context): Boolean =
     Feature.sourceVersion.stable.isAtMost(SourceVersion.`3.7`)
 
-  /** Treat arrays as mutable types. Enabled under separation checking */
+  /** Treat arrays as mutable types and force all mutable fields to be in Stateful
+   *  classes, unless they are annotated with @untrackedCaptures.
+   *  Enabled under separation checking
+   */
   def strictMutability(using Context): Boolean =
     Feature.enabled(Feature.separationChecking)
 
diff --git a/tests/neg-custom-args/captures/cc-poly-source.scala b/tests/neg-custom-args/captures/cc-poly-source.scala
index 47673621c358..fcbcde7f43e5 100644
--- a/tests/neg-custom-args/captures/cc-poly-source.scala
+++ b/tests/neg-custom-args/captures/cc-poly-source.scala
@@ -10,7 +10,7 @@ import caps.use
   class Listener
 
   class Source[X^]:
-    private var listeners: Set[Listener^{X}] = Set.empty
+    @caps.unsafe.untrackedCaptures private var listeners: Set[Listener^{X}] = Set.empty
     def register(x: Listener^{X}): Unit =
       listeners += x
 
diff --git a/tests/neg-custom-args/captures/class-level-attack.check b/tests/neg-custom-args/captures/class-level-attack.check
index d9eefddb0fc6..7cb7dc336c82 100644
--- a/tests/neg-custom-args/captures/class-level-attack.check
+++ b/tests/neg-custom-args/captures/class-level-attack.check
@@ -1,13 +1,13 @@
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/class-level-attack.scala:17:26 ---------------------------
-17 |  def set(x: IO^) = r.put(x)  // error
-   |                          ^
-   |                          Found:    IO^{x}
-   |                          Required: IO^
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/class-level-attack.scala:17:33 ---------------------------
+17 |  update def set(x: IO^) = r.put(x)  // error
+   |                                 ^
+   |                                Found:    IO^{x}
+   |                                Required: IO^
    |
-   |                          Note that capability x is not included in capture set {cap}
-   |                          because (x : IO^²) in method set is not visible from cap in value r.
+   |                                Note that capability x is not included in capture set {cap}
+   |                                because (x : IO^²) in method set is not visible from cap in value r.
    |
-   |                          where:    ^ and cap refer to a fresh root capability in the type of value r
-   |                                    ^²        refers to a fresh root capability in the type of parameter x
+   |                                where:    ^ and cap refer to a fresh root capability in the type of value r
+   |                                          ^²        refers to a fresh root capability in the type of parameter x
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/class-level-attack.scala b/tests/neg-custom-args/captures/class-level-attack.scala
index b48aca8c0c5f..2f2cfb85872f 100644
--- a/tests/neg-custom-args/captures/class-level-attack.scala
+++ b/tests/neg-custom-args/captures/class-level-attack.scala
@@ -3,18 +3,18 @@ import caps.*
 
 class IO
 
-class Ref[X](init: X):
+class Ref[X](init: X) extends caps.Stateful:
   var x = init
   def get: X = x
-  def put(y: X): Unit = x = y
+  update def put(y: X): Unit = x = y
 
-class C(io: IO^):
-  val r: Ref[IO^] = Ref[IO^](io)
+class C(io: IO^) extends caps.Stateful:
+  val r: Ref[IO^]^ = Ref[IO^](io)
     //Type variable X of constructor Ref cannot be instantiated to box IO^ since
     //that type captures the root capability `cap`.
     // where: ^ refers to the universal root capability
   val r2: Ref[IO^] = Ref(io)
-  def set(x: IO^) = r.put(x)  // error
+  update def set(x: IO^) = r.put(x)  // error
 
 def outer(outerio: IO^) =
   val c = C(outerio)
diff --git a/tests/neg-custom-args/captures/filevar-expanded.scala b/tests/neg-custom-args/captures/filevar-expanded.scala
index 461a617bde0d..e1dad4941a26 100644
--- a/tests/neg-custom-args/captures/filevar-expanded.scala
+++ b/tests/neg-custom-args/captures/filevar-expanded.scala
@@ -23,7 +23,7 @@ object test2:
   class File:
     def write(x: String): Unit = ???
 
-  class Service(tracked val io: IO^):
+  class Service(tracked val io: IO^) extends caps.Stateful:
     var file: File^{io} = uninitialized
     def log = file.write("log")
 
diff --git a/tests/neg-custom-args/captures/filevar-multi-ios.scala b/tests/neg-custom-args/captures/filevar-multi-ios.scala
index 848d7c268b9c..df6800b8f287 100644
--- a/tests/neg-custom-args/captures/filevar-multi-ios.scala
+++ b/tests/neg-custom-args/captures/filevar-multi-ios.scala
@@ -8,7 +8,7 @@ class File:
 
 object test1:
 
-  class Service(val io: IO, val io2: IO):
+  class Service(val io: IO, val io2: IO) extends caps.Stateful:
     var file: File^{io} = uninitialized
     var file2: File^{io2} = uninitialized
     def log = file.write("log")
@@ -25,7 +25,7 @@ object test1:
 
 object test2:
 
-  class Service(tracked val io: IO, tracked val io2: IO):
+  class Service(tracked val io: IO, tracked val io2: IO) extends caps.Stateful:
     var file: File^{io} = uninitialized
     var file2: File^{io2} = uninitialized
     def log = file.write("log")
diff --git a/tests/neg-custom-args/captures/filevar.scala b/tests/neg-custom-args/captures/filevar.scala
index 047c41c6af05..537bed3af2b1 100644
--- a/tests/neg-custom-args/captures/filevar.scala
+++ b/tests/neg-custom-args/captures/filevar.scala
@@ -4,7 +4,7 @@ import compiletime.uninitialized
 class File:
   def write(x: String): Unit = ???
 
-class Service:
+class Service extends caps.Stateful:
   var file: File^ = uninitialized  //OK, was  error under sealed
   def log = file.write("log") // OK, was error under unsealed
 
diff --git a/tests/neg-custom-args/captures/i21920.scala b/tests/neg-custom-args/captures/i21920.scala
index 6bdff6dd65fb..e9ef3e17530d 100644
--- a/tests/neg-custom-args/captures/i21920.scala
+++ b/tests/neg-custom-args/captures/i21920.scala
@@ -11,7 +11,7 @@ final class Cell[A](head: () => IterableOnce[A]^):
   def headIterator: Iterator[A]^{this} = head().iterator
 
 class File private ():
-  private var closed = false
+  @caps.unsafe.untrackedCaptures private var closed = false
 
   def close() = closed = true
 
diff --git a/tests/neg-custom-args/captures/i24137.check b/tests/neg-custom-args/captures/i24137.check
deleted file mode 100644
index 60919d7b7591..000000000000
--- a/tests/neg-custom-args/captures/i24137.check
+++ /dev/null
@@ -1,22 +0,0 @@
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i24137.scala:16:21 ---------------------------------------
-16 |  val _: B^{async} = b  // error, but could be OK if we have a way to mark
-   |                     ^
-   |                     Found:    (b : B{val elem1: A^{a}; val elem2: A^{a}}^{cap, a})
-   |                     Required: B^{async}
-   |
-   |                     Note that capability b is not included in capture set {async}.
-   |
-   |                     where:    cap is a fresh root capability in the type of value b
-   |
-   | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i24137.scala:18:23 ---------------------------------------
-18 |  val b1: B^{async} = B(a, a) // error but could also be OK
-   |                      ^^^^^^^
-   |                      Found:    B{val elem1: (a : A^{async}); val elem2: (a : A^{async})}^{cap, a}
-   |                      Required: B^{async}
-   |
-   |                      Note that capability cap is not included in capture set {async}.
-   |
-   |                      where:    cap is a fresh root capability created in value b1 when constructing instance B
-   |
-   | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/i24309-region-orig.scala b/tests/neg-custom-args/captures/i24309-region-orig.scala
index d12eb1f98c39..48972fa7e657 100644
--- a/tests/neg-custom-args/captures/i24309-region-orig.scala
+++ b/tests/neg-custom-args/captures/i24309-region-orig.scala
@@ -1,6 +1,6 @@
 import language.experimental.captureChecking
 import caps.*
-class Ref(private var x: Int):
+class Ref(@caps.unsafe.untrackedCaptures private var x: Int):
   def get = x
   def set(y: Int) = x = y
 trait Region extends SharedCapability:
diff --git a/tests/neg-custom-args/captures/levels.scala b/tests/neg-custom-args/captures/levels.scala
index d15984ed25c2..163224102562 100644
--- a/tests/neg-custom-args/captures/levels.scala
+++ b/tests/neg-custom-args/captures/levels.scala
@@ -2,16 +2,16 @@ class CC
 
 def test1(cap1: CC^) =
 
-  class Ref[T](init: T):
+  class Ref[T](init: T) extends caps.Stateful:
     private var v: T = init
-    def setV(x: T): Unit = v = x
+    update def setV(x: T): Unit = v = x
     def getV: T = v
 
 def test2(cap1: CC^) =
 
-  class Ref[T](init: T):
+  class Ref[T](init: T) extends caps.Stateful:
     private var v: T = init
-    def setV(x: T): Unit = v = x
+    update def setV(x: T): Unit = v = x
     def getV: T = v
 
   val _ = Ref[String => String]((x: String) => x)
diff --git a/tests/neg-custom-args/captures/reaches.check b/tests/neg-custom-args/captures/reaches.check
index 7a0018962776..09310e74fbfd 100644
--- a/tests/neg-custom-args/captures/reaches.check
+++ b/tests/neg-custom-args/captures/reaches.check
@@ -15,7 +15,7 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:30:13 --------------------------------------
 30 |  usingFile: f => // error
    |             ^
-   |Found:    (f: File^'s3) ->'s4 Unit
+   |Found:    (f: File^'s3) ->{cur} Unit
    |Required: File^ => Unit
    |
    |Note that capability cap cannot be included in capture set {C} of value cur.
@@ -44,7 +44,7 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:57:27 --------------------------------------
 57 |  val id: File^ -> File^ = x => x // error
    |                           ^^^^^^
-   |          Found:    (x: File^) ->'s5 File^²
+   |          Found:    (x: File^) ->'s4 File^²
    |          Required: File^ -> File^³
    |
    |          Note that capability cap is not included in capture set {cap²}
@@ -69,8 +69,8 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:85:10 --------------------------------------
 85 |  ps.map((x, y) => compose1(x, y)) // error
    |          ^^^^^^^^^^^^^^^^^^^^^^^
-   |Found:    (x$1: (A^ ->'s6 A^'s7, A^ ->'s8 A^'s9)^'s10) ->'s11 A^'s12 ->'s13 A^'s14
-   |Required: ((A ->{ps*} A, A ->{ps*} A)) => A^'s15 ->'s16 A^'s17
+   |Found:    (x$1: (A^ ->'s5 A^'s6, A^ ->'s7 A^'s8)^'s9) ->'s10 A^'s11 ->'s12 A^'s13
+   |Required: ((A ->{ps*} A, A ->{ps*} A)) => A^'s14 ->'s15 A^'s16
    |
    |Note that capability ps* cannot be included in capture set {} of value x.
    |
@@ -81,8 +81,8 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:88:10 --------------------------------------
 88 |  ps.map((x, y) => compose1(x, y)) // error
    |          ^^^^^^^^^^^^^^^^^^^^^^^
-   |Found:    (x$1: (A^ ->'s18 A^'s19, A^ ->'s20 A^'s21)^'s22) ->'s23 A^'s24 ->'s25 A^'s26
-   |Required: ((A ->{C} A, A ->{C} A)) => A^'s27 ->'s28 A^'s29
+   |Found:    (x$1: (A^ ->'s17 A^'s18, A^ ->'s19 A^'s20)^'s21) ->'s22 A^'s23 ->'s24 A^'s25
+   |Required: ((A ->{C} A, A ->{C} A)) => A^'s26 ->'s27 A^'s28
    |
    |Note that capability C cannot be included in capture set {} of value x.
    |
@@ -111,7 +111,7 @@
 -- Error: tests/neg-custom-args/captures/reaches.scala:42:9 ------------------------------------------------------------
 42 |  val cur = Ref[List[Proc]](xs) // error
    |         ^
-   |         Separation failure: value cur's inferred type Ref[List[() => Unit]^{}]^{} hides parameter xs.
+   |         Separation failure: value cur's inferred type Ref[List[() => Unit]^{}]^ hides parameter xs.
    |         The parameter needs to be annotated with consume to allow this.
 -- Error: tests/neg-custom-args/captures/reaches.scala:44:17 -----------------------------------------------------------
 44 |    val next: () => Unit = cur.get.head // error // error
diff --git a/tests/neg-custom-args/captures/reaches.scala b/tests/neg-custom-args/captures/reaches.scala
index bbbf3830c759..77ba64fbbc60 100644
--- a/tests/neg-custom-args/captures/reaches.scala
+++ b/tests/neg-custom-args/captures/reaches.scala
@@ -5,10 +5,10 @@ def usingFile[T](f: File^ => T): T = ???
 
 type Proc = () => Unit
 
-class Ref[T](init: T):
+class Ref[T](init: T) extends caps.Stateful:
   private var x: T = init
   def get: T = x
-  def set(y: T) = { x = y }
+  update def set(y: T) = { x = y }
 
 def runAll0[C^](xs: List[() ->{C} Unit]): Unit =
   var cur: List[() ->{C} Unit] = xs
diff --git a/tests/neg-custom-args/captures/reference-cc.scala b/tests/neg-custom-args/captures/reference-cc.scala
index 8426cd0ce303..ec7df82a3a69 100644
--- a/tests/neg-custom-args/captures/reference-cc.scala
+++ b/tests/neg-custom-args/captures/reference-cc.scala
@@ -2,7 +2,7 @@ import language.experimental.captureChecking
 import scala.compiletime.uninitialized
 import java.io.*
 import language.experimental.saferExceptions
-
+import caps.unsafe.untrackedCaptures
 
 def usingLogFile[T](op: FileOutputStream^ => T): T =
   val logFile = FileOutputStream("log")
@@ -24,8 +24,8 @@ object LzyNil extends LzyList[Nothing]:
   def tail = ???
 
 final class LzyCons[+A](hd: A, tl: () => LzyList[A]^) extends LzyList[A]:
-  private var forced = false
-  private var cache: LzyList[A]^{this} = uninitialized
+  @untrackedCaptures private var forced = false
+  @untrackedCaptures private var cache: LzyList[A]^{this} = uninitialized
   private def force =
     if !forced then { cache = tl(); forced = true }
     cache
diff --git a/tests/neg-custom-args/captures/ro-buf.scala b/tests/neg-custom-args/captures/ro-buf.scala
new file mode 100644
index 000000000000..fae4ccb964f5
--- /dev/null
+++ b/tests/neg-custom-args/captures/ro-buf.scala
@@ -0,0 +1,43 @@
+import caps.unsafe.*
+import caps.Stateful
+
+class Buf[A] extends Stateful:
+  this: Buf[A] =>
+  val elems: Array[A]^ = ???
+  def +=(elem: A): this.type =
+    elems(0) = elem // error
+    this
+
+  /** Concrete collection type: ArrayBuffer */
+  class ArrayBuffer[A] private (@untrackedCaptures initElems: Array[AnyRef]^, initLength: Int) {
+    this: ArrayBuffer[A] =>
+    def this() = this(new Array[AnyRef](16), 0)
+    @untrackedCaptures private var elems: Array[AnyRef]^ = initElems
+    @untrackedCaptures private var start = 0
+    @untrackedCaptures private var end = initLength
+    def apply(n: Int) = elems(start + n).asInstanceOf[A]
+    def iterator: Iterator[A] = ???
+    def length = end - start
+    def +=(elem: A): this.type = {
+      if (end == elems.length) {
+        if (start > 0) {
+          Array.copy(elems, start, elems, 0, length)
+          end -= start
+          start = 0
+        }
+        else {
+          val newelems = new Array[AnyRef](end * 2)
+          Array.copy(elems, 0, newelems, 0, end)
+          elems = newelems
+        }
+      }
+      elems(end) = elem.asInstanceOf[AnyRef] // error
+        // cannot call update method on Array[A] since it is read-only.
+        // elems is of type Array[A] since the self type is pure, so this
+        // has type ArrayBuffer[A], which means that this.elems os read-only.
+      end += 1
+      this
+    }
+    override def toString = s"ArrayBuffer(${elems.slice(start, end).mkString(", ")})"
+  }
+
diff --git a/tests/neg-custom-args/captures/scope-extrude-mut.scala b/tests/neg-custom-args/captures/scope-extrude-mut.scala
index e6a851f9f4c5..d48686886343 100644
--- a/tests/neg-custom-args/captures/scope-extrude-mut.scala
+++ b/tests/neg-custom-args/captures/scope-extrude-mut.scala
@@ -3,7 +3,7 @@ import language.experimental.captureChecking
 class A extends caps.Stateful:
   var x = 0
 
-class B:
+class B extends caps.Stateful:
   private var a: A^ = A()
   def b() =
     val a1 = A()
diff --git a/tests/neg-custom-args/captures/stack-alloc.scala b/tests/neg-custom-args/captures/stack-alloc.scala
index 80e7e4169720..f1e9465fd975 100644
--- a/tests/neg-custom-args/captures/stack-alloc.scala
+++ b/tests/neg-custom-args/captures/stack-alloc.scala
@@ -2,17 +2,18 @@ import scala.collection.mutable
 
 class Pooled
 
-val stack = mutable.ArrayBuffer[Pooled]()
-var nextFree = 0
+class Test extends caps.Stateful:
+  val stack = mutable.ArrayBuffer[Pooled]()
+  var nextFree = 0
 
-def withFreshPooled[T](op: (lcap: caps.Capability) ?-> Pooled^{lcap} => T): T =
-  if nextFree >= stack.size then stack.append(new Pooled)
-  val pooled = stack(nextFree)
-  nextFree = nextFree + 1
-  val ret = op(using caps.cap)(pooled)
-  nextFree = nextFree - 1
-  ret
+  update def withFreshPooled[T](op: (lcap: caps.Capability) ?-> Pooled^{lcap} => T): T =
+    if nextFree >= stack.size then stack.append(new Pooled)
+    val pooled = stack(nextFree)
+    nextFree = nextFree + 1
+    val ret = op(using caps.cap)(pooled)
+    nextFree = nextFree - 1
+    ret
 
-def test() =
-  val pooledClosure = withFreshPooled(pooled => () => pooled.toString) // error
-  pooledClosure()
\ No newline at end of file
+  update def test() =
+    val pooledClosure = withFreshPooled(pooled => () => pooled.toString) // error
+    pooledClosure()
\ No newline at end of file
diff --git a/tests/neg-custom-args/captures/vars.scala b/tests/neg-custom-args/captures/vars.scala
index eb9719cd2adf..640654534887 100644
--- a/tests/neg-custom-args/captures/vars.scala
+++ b/tests/neg-custom-args/captures/vars.scala
@@ -39,7 +39,7 @@ def test(cap1: Cap, cap2: Cap) =
   }
 
   class Ref:
-    var elem: String ->{cap1} String = null
+    @caps.unsafe.untrackedCaptures var elem: String ->{cap1} String = null
 
   val r = Ref()
   r.elem = f
diff --git a/tests/new/test.scala b/tests/new/test.scala
index b9be7bc5b47b..00174769a0f0 100644
--- a/tests/new/test.scala
+++ b/tests/new/test.scala
@@ -1,18 +1 @@
-import caps.unsafe.untrackedCaptures
-
-class ArrayBuffer[A] private (@untrackedCaptures initElems: Array[AnyRef]^, initLength: Int):
-  private var elems: Array[AnyRef]^ = initElems
-  private var start = 0
-  private var end = initLength
-
-  def +=(elem: A): this.type =
-    elems(end) = elem.asInstanceOf[AnyRef]
-    this
-
-  override def toString =
-    val slice = elems.slice(start, end)
-    val wrapped = wrapRefArray(slice)
-    //val wrapped2 = collection.mutable.ArraySeq.ofRef(slice)
-    val str = wrapped.mkString(", ")
-    str
-    //s"ArrayBuffer(${elems.slice(start, end).mkString(", ")})"
+object Test
diff --git a/tests/pos-custom-args/captures/buffers.scala b/tests/pos-custom-args/captures/buffers.scala
index 7fcf96291ccb..7ec4e25e6872 100644
--- a/tests/pos-custom-args/captures/buffers.scala
+++ b/tests/pos-custom-args/captures/buffers.scala
@@ -1,6 +1,6 @@
 import reflect.ClassTag
 
-class Buffer[A]
+class Buffer[A] extends caps.Mutable
 
 class ArrayBuffer[A: ClassTag] extends Buffer[A]:
   var elems: Array[A] = new Array[A](10)
diff --git a/tests/pos-custom-args/captures/cc-cast.scala b/tests/pos-custom-args/captures/cc-cast.scala
index cfd96d63bee7..370a19f9ea61 100644
--- a/tests/pos-custom-args/captures/cc-cast.scala
+++ b/tests/pos-custom-args/captures/cc-cast.scala
@@ -4,7 +4,7 @@ import compiletime.uninitialized
 def foo(x: Int => Int) = ()
 
 
-object Test:
+object Test extends caps.Mutable:
   def test(x: Object) =
     foo(x.asInstanceOf[Int => Int])
 
diff --git a/tests/pos-custom-args/captures/cc-poly-source-capability.scala b/tests/pos-custom-args/captures/cc-poly-source-capability.scala
index 96a2edd414be..1d12f55ac79c 100644
--- a/tests/pos-custom-args/captures/cc-poly-source-capability.scala
+++ b/tests/pos-custom-args/captures/cc-poly-source-capability.scala
@@ -2,6 +2,7 @@ import language.experimental.captureChecking
 import annotation.experimental
 import caps.{CapSet, SharedCapability}
 import caps.use
+import caps.unsafe.untrackedCaptures
 
 @experimental object Test:
 
@@ -12,7 +13,7 @@ import caps.use
   class Listener
 
   class Source[X^]:
-    private var listeners: Set[Listener^{X}] = Set.empty
+    @untrackedCaptures private var listeners: Set[Listener^{X}] = Set.empty
     def register(x: Listener^{X}): Unit =
       listeners += x
 
diff --git a/tests/pos-custom-args/captures/drop-refinement.scala b/tests/pos-custom-args/captures/drop-refinement.scala
index f7e922b88012..e9fce44d8489 100644
--- a/tests/pos-custom-args/captures/drop-refinement.scala
+++ b/tests/pos-custom-args/captures/drop-refinement.scala
@@ -12,7 +12,8 @@ private final class ConcatIterator[+A](val from: Iterator[A @uncheckedVariance]^
   }
 }
 
-private final class ConcatIteratorCell[A](head: => IterableOnce[A]^, var tail: ConcatIteratorCell[A]^) {
-  def headIterator: Iterator[A]^{this} = head.iterator
-}
+private final class ConcatIteratorCell[A](head: => IterableOnce[A]^, var tail: ConcatIteratorCell[A]^)
+extends caps.Stateful:
+  update def headIterator: Iterator[A]^{this} = head.iterator
+
 
diff --git a/tests/pos-custom-args/captures/filevar-tracked.scala b/tests/pos-custom-args/captures/filevar-tracked.scala
index 8c48017502b8..96d8575f5588 100644
--- a/tests/pos-custom-args/captures/filevar-tracked.scala
+++ b/tests/pos-custom-args/captures/filevar-tracked.scala
@@ -23,7 +23,7 @@ object test2:
   class File:
     def write(x: String): Unit = ???
 
-  class Service(tracked val io: IO):
+  class Service(tracked val io: IO) extends caps.Stateful:
     var file: File^{io} = uninitialized
     def log = file.write("log")
 
diff --git a/tests/pos-custom-args/captures/filevar.scala b/tests/pos-custom-args/captures/filevar.scala
index 8c48017502b8..96d8575f5588 100644
--- a/tests/pos-custom-args/captures/filevar.scala
+++ b/tests/pos-custom-args/captures/filevar.scala
@@ -23,7 +23,7 @@ object test2:
   class File:
     def write(x: String): Unit = ???
 
-  class Service(tracked val io: IO):
+  class Service(tracked val io: IO) extends caps.Stateful:
     var file: File^{io} = uninitialized
     def log = file.write("log")
 
diff --git a/tests/pos-custom-args/captures/i21507.scala b/tests/pos-custom-args/captures/i21507.scala
index 953c8a0b0dca..11ed5b165798 100644
--- a/tests/pos-custom-args/captures/i21507.scala
+++ b/tests/pos-custom-args/captures/i21507.scala
@@ -1,11 +1,12 @@
 import language.experimental.captureChecking
+import caps.unsafe.untrackedCaptures
 
 trait Box[Cap^]:
   def store(f: (() -> Unit)^{Cap}): Unit
 
 def run[Cap^](f: Box[{Cap}]^{Cap} => Unit): Box[{Cap}]^{Cap} =
   new Box[{Cap}] {
-    private var item: () ->{Cap} Unit = () => ()
+    @untrackedCaptures private var item: () ->{Cap} Unit = () => ()
     def store(f: () ->{Cap} Unit): Unit =
       item = f  // was error, now ok
   }
diff --git a/tests/pos-custom-args/captures/i22723.scala b/tests/pos-custom-args/captures/i22723.scala
index 7fc20f813f7c..a0fada648ea3 100644
--- a/tests/pos-custom-args/captures/i22723.scala
+++ b/tests/pos-custom-args/captures/i22723.scala
@@ -11,7 +11,7 @@ trait HasCap:
 object HasCap:
   def apply[T](body: HasCap^ ?=> T): T = ???
 
-class Box(using tracked val h: HasCap^):
+class Box(using tracked val h: HasCap^) extends caps.Stateful:
   var t: A^{h} = h.mkA
 
 def main() =
diff --git a/tests/neg-custom-args/captures/i24137.scala b/tests/pos-custom-args/captures/i24137.scala
similarity index 57%
rename from tests/neg-custom-args/captures/i24137.scala
rename to tests/pos-custom-args/captures/i24137.scala
index 033fa1b7d2f2..5a2699fd3d7a 100644
--- a/tests/neg-custom-args/captures/i24137.scala
+++ b/tests/pos-custom-args/captures/i24137.scala
@@ -1,10 +1,10 @@
 //< using options -Ycc-verbose
 import caps.{cap, Shared, SharedCapability}
-
+import caps.unsafe.untrackedCaptures
 open class A
 
 class B(elem1: A^{cap.only[Shared]}, elem2: A^{cap.only[Shared]}):
-  private var curElem: A^ = elem1 // problem is curElem contibutes cap to B().
+  @untrackedCaptures private var curElem: A^ = elem1 // problem is curElem contibutes cap to B().
   def next() =
     curElem = elem2
 
@@ -13,6 +13,6 @@ class Async extends caps.SharedCapability
 def test(async: Async) =
   val a: A^{async} = A()
   val b = B(a, a)
-  val _: B^{async} = b  // error, but could be OK if we have a way to mark
+  val _: B^{async} = b  // was error, but could be OK if we have a way to mark
                         // curElem above as not contributing anything
-  val b1: B^{async} = B(a, a) // error but could also be OK
+  val b1: B^{async} = B(a, a) // was error but could also be OK
diff --git a/tests/pos-custom-args/captures/i24309-region.scala b/tests/pos-custom-args/captures/i24309-region.scala
index 37d25702a6c8..61f79894419f 100644
--- a/tests/pos-custom-args/captures/i24309-region.scala
+++ b/tests/pos-custom-args/captures/i24309-region.scala
@@ -2,9 +2,10 @@ import language.experimental.captureChecking
 import language.experimental.separationChecking
 
 import caps.*
+import caps.unsafe.untrackedCaptures
 
 object Regions:
-  class Ref(private var x: Int):
+  class Ref(@untrackedCaptures private var x: Int):
     def get = x
     def set(y: Int) = x = y
 
diff --git a/tests/pos-custom-args/captures/iterators.scala b/tests/pos-custom-args/captures/iterators.scala
index 89e1eb91b4f4..4607b94eac60 100644
--- a/tests/pos-custom-args/captures/iterators.scala
+++ b/tests/pos-custom-args/captures/iterators.scala
@@ -1,4 +1,5 @@
 package cctest
+import caps.unsafe.untrackedCaptures
 
 trait IterableOnce[A]:
   def iterator: Iterator[A]^{this}
@@ -25,7 +26,7 @@ def map[T, U](it: Iterator[T]^, f: T^ => U): Iterator[U]^{it, f} = new Iterator:
 
 def test(c: Cap, d: Cap, e: Cap) =
   val it = new Iterator[Int]:
-    private var ctr = 0
+    @untrackedCaptures private var ctr = 0
     def hasNext = ctr < 10
     def next = { ctr += 1; ctr }
 
diff --git a/tests/pos-custom-args/captures/lazylists-exceptions.scala b/tests/pos-custom-args/captures/lazylists-exceptions.scala
index afc6616108bc..64ef984d301c 100644
--- a/tests/pos-custom-args/captures/lazylists-exceptions.scala
+++ b/tests/pos-custom-args/captures/lazylists-exceptions.scala
@@ -1,6 +1,7 @@
 import language.experimental.saferExceptions
 import scala.compiletime.uninitialized
 import scala.annotation.unchecked.uncheckedCaptures
+import caps.unsafe.untrackedCaptures
 
 trait LzyList[+A]:
   def isEmpty: Boolean
@@ -13,8 +14,8 @@ object LzyNil extends LzyList[Nothing]:
   def tail = ???
 
 final class LzyCons[+A](hd: A, tl: () => LzyList[A]^) extends LzyList[A]:
-  private var forced = false
-  private var cache: LzyList[A @uncheckedCaptures]^{this} = uninitialized
+  @untrackedCaptures private var forced = false
+  @untrackedCaptures private var cache: LzyList[A @uncheckedCaptures]^{this} = uninitialized
   private def force =
     if !forced then { cache = tl(); forced = true }
     cache
diff --git a/tests/pos-custom-args/captures/reaches.scala b/tests/pos-custom-args/captures/reaches.scala
index 348346ad1c3f..18d86b6f5def 100644
--- a/tests/pos-custom-args/captures/reaches.scala
+++ b/tests/pos-custom-args/captures/reaches.scala
@@ -5,10 +5,10 @@ def f(xs: List[C^]) =
 
 type Proc = () => Unit
 
-class Ref[T](init: T):
+class Ref[T](init: T) extends caps.Mutable:
   private var x: T = init
   def get: T = x
-  def set(y: T) = { x = y }
+  update def set(y: T) = { x = y }
 
 class List[+A]:
   def head: A = ???
diff --git a/tests/pos-custom-args/captures/secondary-constructors.scala b/tests/pos-custom-args/captures/secondary-constructors.scala
index abc923a3a8a3..8df0d1b4ecb5 100644
--- a/tests/pos-custom-args/captures/secondary-constructors.scala
+++ b/tests/pos-custom-args/captures/secondary-constructors.scala
@@ -1,10 +1,11 @@
 package scala
 package collection
 package immutable
+import caps.unsafe.untrackedCaptures
 
 final class LazyListIterable[+A]():
   this: LazyListIterable[A]^ =>
-  var _head: Any = 0
+  @untrackedCaptures var _head: Any = 0
   private def this(head: A, tail: LazyListIterable[A]^) =
     this()
     _head = head
diff --git a/tests/pos-custom-args/captures/stack-alloc.scala b/tests/pos-custom-args/captures/stack-alloc.scala
index 7013f978c281..d490e04d2fdc 100644
--- a/tests/pos-custom-args/captures/stack-alloc.scala
+++ b/tests/pos-custom-args/captures/stack-alloc.scala
@@ -2,16 +2,17 @@ import scala.collection.mutable
 
 class Pooled
 
-val stack = mutable.ArrayBuffer[Pooled]()
-var nextFree = 0
+class Test extends caps.Stateful:
+  val stack = mutable.ArrayBuffer[Pooled]()
+  var nextFree = 0
 
-def withFreshPooled[T](op: Pooled^ => T): T =
-  if nextFree >= stack.size then stack.append(new Pooled)
-  val pooled = stack(nextFree)
-  nextFree = nextFree + 1
-  val ret = op(pooled)
-  nextFree = nextFree - 1
-  ret
+  update def withFreshPooled[T](op: Pooled^ => T): T =
+    if nextFree >= stack.size then stack.append(new Pooled)
+    val pooled = stack(nextFree)
+    nextFree = nextFree + 1
+    val ret = op(pooled)
+    nextFree = nextFree - 1
+    ret
 
-def test() =
-  withFreshPooled(pooled => pooled.toString)
\ No newline at end of file
+  update def test() =
+    withFreshPooled(pooled => pooled.toString)
\ No newline at end of file
diff --git a/tests/pos-custom-args/captures/test.scala b/tests/pos-custom-args/captures/test.scala
index 979f3d34ec17..5a894670fa5c 100644
--- a/tests/pos-custom-args/captures/test.scala
+++ b/tests/pos-custom-args/captures/test.scala
@@ -3,9 +3,9 @@ type Cap = C^
 
 type Proc = () => Unit
 
-class Ref[T](p: T):
+class Ref[T](p: T) extends caps.Mutable:
   private var x: T = p
-  def set(x: T): Unit = this.x = x
+  update def set(x: T): Unit = this.x = x
   def get: T = x
 
 def test(c: () => Unit) =
diff --git a/tests/pos-custom-args/captures/trickyTrailingUpArrow.scala b/tests/pos-custom-args/captures/trickyTrailingUpArrow.scala
index 1ca4403a54b7..b0402ec80601 100644
--- a/tests/pos-custom-args/captures/trickyTrailingUpArrow.scala
+++ b/tests/pos-custom-args/captures/trickyTrailingUpArrow.scala
@@ -1,5 +1,5 @@
  class STR
- object Test:
+ object Test extends caps.Stateful:
   var x = 0
   type FreshContext = STR^
   x += 1
diff --git a/tests/pos-custom-args/captures/unsafe-captures.scala b/tests/pos-custom-args/captures/unsafe-captures.scala
index 5e0144331344..1a40b4174f6e 100644
--- a/tests/pos-custom-args/captures/unsafe-captures.scala
+++ b/tests/pos-custom-args/captures/unsafe-captures.scala
@@ -1,5 +1,7 @@
 import annotation.unchecked.uncheckedCaptures
-class LL[+A] private (private var lazyState: (() => LL.State[A]^) @uncheckedCaptures):
+import caps.unsafe.untrackedCaptures
+
+class LL[+A] private (@untrackedCaptures private var lazyState: (() => LL.State[A]^) @uncheckedCaptures):
   private val res = lazyState() // without unchecked captures we get a van't unbox cap error
 
 
diff --git a/tests/pos-custom-args/captures/vars.scala b/tests/pos-custom-args/captures/vars.scala
index 37044f7e7529..f1fc7c1aeb59 100644
--- a/tests/pos-custom-args/captures/vars.scala
+++ b/tests/pos-custom-args/captures/vars.scala
@@ -9,7 +9,7 @@ def test(cap1: Cap, cap2: Cap) =
   val z2 = () => { x = identity }
   val z2c: () ->{cap1} Unit = z2
 
-  class Ref:
+  class Ref extends caps.Stateful:
     var elem: String ->{cap1} String = null
 
   val r = Ref()
diff --git a/tests/pos-custom-args/captures/vars1.scala b/tests/pos-custom-args/captures/vars1.scala
index c8d887e38463..2fca64dad725 100644
--- a/tests/pos-custom-args/captures/vars1.scala
+++ b/tests/pos-custom-args/captures/vars1.scala
@@ -1,7 +1,7 @@
 import caps.unsafe.*
 import annotation.unchecked.uncheckedCaptures
 
-object Test:
+object Test extends caps.Mutable:
   type ErrorHandler = (Int, String) => Unit
 
   @uncheckedCaptures
diff --git a/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala b/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala
index a5488b28d420..b5d1cb771ddd 100644
--- a/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala
+++ b/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala
@@ -207,7 +207,7 @@ object CollectionStrawMan5 {
     def head: A
     def tail: List[A]
     def iterator = new Iterator[A] {
-      private var current = self
+      @untrackedCaptures private var current = self
       def hasNext = !current.isEmpty
       def next() = { val r = current.head; current = current.tail; r }
     }
@@ -230,7 +230,7 @@ object CollectionStrawMan5 {
       if (n > 0) tail.drop(n - 1) else this
   }
 
-  case class Cons[+A](x: A, private[collections] var next: List[A @uncheckedVariance @uncheckedCaptures]) // sound because `next` is used only locally
+  case class Cons[+A](x: A, @untrackedCaptures private[collections] var next: List[A @uncheckedVariance @uncheckedCaptures]) // sound because `next` is used only locally
   extends List[A] {
     override def isEmpty = false
     override def head = x
@@ -254,8 +254,8 @@ object CollectionStrawMan5 {
   /** Concrete collection type: ListBuffer */
   class ListBuffer[A] extends Seq[A] with SeqLike[A] with Builder[A, List[A]] {
     type C[X] = ListBuffer[X]
-    private var first, last: List[A] = Nil
-    private var aliased = false
+    @untrackedCaptures private var first, last: List[A] = Nil
+    @untrackedCaptures private var aliased = false
     def iterator = first.iterator
     def fromIterable[B](coll: Iterable[B]^): ListBuffer[B] = ListBuffer.fromIterable(coll)
     def apply(i: Int) = first.apply(i)
@@ -300,9 +300,9 @@ object CollectionStrawMan5 {
     //this: ArrayBuffer[A] =>
     type C[X] = ArrayBuffer[X]
     def this() = this(new Array[AnyRef](16), 0)
-    private var elems: Array[AnyRef]^ = initElems
-    private var start = 0
-    private var end = initLength
+    @untrackedCaptures private var elems: Array[AnyRef]^ = initElems
+    @untrackedCaptures private var start = 0
+    @untrackedCaptures private var end = initLength
     def apply(n: Int) = elems(start + n).asInstanceOf[A]
     def length = end - start
     override def knownLength = length
@@ -424,7 +424,7 @@ object CollectionStrawMan5 {
     def end: Int
     def apply(i: Int): A
     def iterator: Iterator[A]^{this} = new Iterator[A] {
-      private var current = start
+      @untrackedCaptures private var current = start
       def hasNext = current < end
       def next(): A = {
         val r = apply(current)
@@ -533,8 +533,8 @@ object CollectionStrawMan5 {
       -1
     }
     def filter(p: A ->{cap, this} Boolean): Iterator[A]^{this, p} = new Iterator[A] {
-      private var hd: A = compiletime.uninitialized
-      private var hdDefined: Boolean = false
+      @untrackedCaptures private var hd: A = compiletime.uninitialized
+      @untrackedCaptures private var hdDefined: Boolean = false
 
       def hasNext: Boolean = hdDefined || {
         while {
@@ -560,7 +560,7 @@ object CollectionStrawMan5 {
     }
 
     def flatMap[B](f: A => IterableOnce[B]^): Iterator[B]^{this, f} = new Iterator[B] {
-      private var myCurrent: Iterator[B]^{this, f} = Iterator.empty
+      @untrackedCaptures private var myCurrent: Iterator[B]^{this, f} = Iterator.empty
       private def current = {
         while (!myCurrent.hasNext && self.hasNext)
           myCurrent = f(self.next()).iterator
@@ -570,8 +570,8 @@ object CollectionStrawMan5 {
       def next() = current.next()
     }
     def ++[B >: A](xs: IterableOnce[B]^): Iterator[B]^{this, xs} = new Iterator[B] {
-      private var myCurrent: Iterator[B]^{self, xs} = self
-      private var first = true
+      @untrackedCaptures private var myCurrent: Iterator[B]^{self, xs} = self
+      @untrackedCaptures private var first = true
       private def current = {
         if (!myCurrent.hasNext && first) {
           myCurrent = xs.iterator
diff --git a/tests/run-custom-args/captures/minicheck.scala b/tests/run-custom-args/captures/minicheck.scala
index 5a16649b5fe5..95df61bbcea1 100644
--- a/tests/run-custom-args/captures/minicheck.scala
+++ b/tests/run-custom-args/captures/minicheck.scala
@@ -2,10 +2,11 @@
 import compiletime.uninitialized
 import annotation.{experimental, tailrec, constructorOnly}
 import collection.mutable
+import caps.unsafe.untrackedCaptures
 
 case class Symbol(name: String, initOwner: Symbol | Null) extends caps.Pure:
   def owner = initOwner.nn
-  private var myInfo: Type = uninitialized
+  @untrackedCaptures private var myInfo: Type = uninitialized
   def infoOrCompleter: Type = myInfo
   def info: Type =
     infoOrCompleter match
@@ -67,7 +68,7 @@ object EmptyScope extends Scope
 class TypeError(val msg: String) extends Exception
 
 class Run:
-  var errorCount = 0
+  @untrackedCaptures var errorCount = 0
 
 object report:
   def error(msg: -> String)(using Context) =
@@ -87,10 +88,10 @@ abstract class DetachedContext extends Ctx:
   def outer: DetachedContext
 
 class FreshCtx(val level: Int) extends DetachedContext:
-  var outer: FreshCtx = uninitialized
-  var owner: Symbol = uninitialized
-  var scope: Scope = uninitialized
-  var run: Run = uninitialized
+  @untrackedCaptures var outer: FreshCtx = uninitialized
+  @untrackedCaptures var owner: Symbol = uninitialized
+  @untrackedCaptures var scope: Scope = uninitialized
+  @untrackedCaptures var run: Run = uninitialized
   def initFrom(other: Context): this.type =
     outer = other.asInstanceOf[FreshCtx]
     owner = other.owner
@@ -113,8 +114,8 @@ type FreshContext = FreshCtx^
 inline def ctx(using c: Context): Ctx^{c} = c
 
 // !cc! it does not work if ctxStack is an Array[FreshContext] instead.
-var ctxStack = Array.tabulate(16)(new FreshCtx(_))
-var curLevel = 0
+@untrackedCaptures var ctxStack = Array.tabulate(16)(new FreshCtx(_))
+@untrackedCaptures var curLevel = 0
 
 private def freshContext(using Context): FreshContext =
   if curLevel == ctxStack.length then

From 4b03873b6c5fc82d281b16a3747206e950ff0416 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Thu, 4 Dec 2025 18:36:42 +0100
Subject: [PATCH 6/6] Update doc page

---
 .../capture-checking/mutability.md            | 29 +++++++++++++------
 library/src/scala/caps/package.scala          |  9 ++++--
 2 files changed, 26 insertions(+), 12 deletions(-)

diff --git a/docs/_docs/reference/experimental/capture-checking/mutability.md b/docs/_docs/reference/experimental/capture-checking/mutability.md
index 1ed6e457ba34..284b712ab2d2 100644
--- a/docs/_docs/reference/experimental/capture-checking/mutability.md
+++ b/docs/_docs/reference/experimental/capture-checking/mutability.md
@@ -239,6 +239,20 @@ class Arr[T](n: Int) extends Mutable:
 An example of a `Stateful` and `Unscoped` capability that is _not_ `Separate` would be a
 facade class that reveals some part of an underlying `Mutable` capability.
 
+## Arrays
+
+The class `scala.Array` is considered a `Mutable` class if [separation checking](./separation-checking.md) is enabled. In that context, class Array can be considered to be declared roughly as follows:
+```scala
+class Array[T] extends Mutable:
+  def length: Int
+  def apply(i: Int): T
+  update def update(i: Int, x: T): Unit
+```
+In fact, for technical reasons `Array` cannot extend `Mutable` or any other new traits beyond what is supported by the JVM. But for the purposes of capture and separation checking, it is still a considered a `Mutable` class.
+
+By contrast, none of the mutable collections in the Scala standard library extend currently `Stateful` or `Mutable`. So to experiment with mutable collections, an
+alternative class library has to be used.
+
 ## Read-only Capabilities
 
 If `x` is an exclusive capability of a type extending `Stateful`, `x.rd` is its associated _read-only_ capability.
@@ -388,7 +402,9 @@ ro.set(22)        // disallowed, since `ro` is read-only access
 
 ## Untracked Vars
 
-Sometimes, disallowing assignments to mutable fields from normal methods is too restrictive. For instance:
+Under [separation checking](./separation-checking.md), mutable fields are allowed to be declared only in `Stateful` classes. Updates to these fields can then only happen in update methods of these classes.
+
+But sometimes, disallowing assignments to mutable fields from normal methods is too restrictive. For instance:
 ```scala
 import caps.unsafe.untrackedCaptures
 
@@ -401,17 +417,12 @@ class Cache[T](eval: () -> T):
       known = true
     x
 ```
-Note that, even though `Cache` has mutable variables, it is not declared as a `Stateful` class. In this case, the mutable field `x` is used to store the result of a pure function `eval` and field `known` reflects whether `eval` was called. This is equivalent to just calling `eval()` directly but can be more efficient since the cached value is evaluated at most once. So from a semantic standpoint, it should not be necessary to make `force` an update method, even though it does assign to `x`.
+Note that `Cache` is not declared as a `Stateful` class, even though it has mutable fields. In this case, the mutable field `x` is used to store the result of a pure function `eval` and field `known` reflects whether `eval` was called. This is equivalent to just calling `eval()` directly but can be more efficient since the cached value is evaluated at most once. So from a semantic standpoint, it should not be necessary to make `Cache` a `Stateful` class with `force` as an update method, even though `force` does assign to `x`.
 
-We can avoid the need for update methods by annotating mutable fields with `@untrackedCaptures`. Assignments to untracked mutable field are then not checked for read-only restrictions. The `@untrackedCaptures` annotation can be imported from the `scala.caps.unsafe` object. It is up to the developer
+We can avoid the need for stateful classes and update methods by annotating mutable fields with `@untrackedCaptures`. Assignments to untracked mutable fields are then not checked for read-only restrictions. The `@untrackedCaptures` annotation can be imported from the `scala.caps.unsafe` object. It is up to the developer
 to use `@untrackedCaptures` responsibly so that it does not hide visible side effects on mutable state.
 
-Note that at the moment an assignment to a variable is restricted _only_ if the variable is a field of a `Stateful` class. Fields of other classes and local variables are currently not checked. So the `Cache` class above would in fact
-currently compile without the addition of `@untrackedCaptures`.
-
-But is planned to tighten the rules in the future so that mutable fields that are not annotated with `@untrackedCaptures` can be declared only in classes extending `Stateful`. This means that all assignments to mutable fields would be checked with the read-only restriction, and `@untrackedCapture`s would become essential as an escape hatch.
-
-By contrast, it is not planned to check assignments to local mutable variables, which are not fields of some class. So `@untrackedCaptures` is disallowed for such local variables.
+Note that the are no restrictions on assignments to local mutable variables, which are not fields of some class. So `@untrackedCaptures` is disallowed for such local variables.
 
 The `untrackedCaptures` annotation can also be used in some other contexts unrelated to mutable variables. These are described in its [doc comment](https://www.scala-lang.org/api/current/scala/caps/unsafe$$untrackedCaptures.html).
 
diff --git a/library/src/scala/caps/package.scala b/library/src/scala/caps/package.scala
index b63c9b4cd6fe..3e8bd69b0f4b 100644
--- a/library/src/scala/caps/package.scala
+++ b/library/src/scala/caps/package.scala
@@ -203,14 +203,14 @@ def freeze(@internal.consume x: Mutable | Array[?]): x.type = x
 
 @experimental
 object unsafe:
-  /** Two usages:
+  /** Three usages:
    *
    *   1. Marks the constructor parameter as untracked.
    *      The capture set of this parameter will not be included in
    *      the capture set of the constructed object.
    *
-   *   2. Marks a class field that has a cap in its capture set, so that
-   *      the cap is not contributed to the class instance.
+   *   2. Marks a class field that has a root capability in its capture set, so
+   *      that the root capability is not contributed to the class instance.
    *      Example:
    *
    *          class A { val b B^ = ... }; new A()
@@ -221,6 +221,9 @@ object unsafe:
    *
    *      has type A. The `b` field does not contribute its cap.
    *
+   *   3. Allows a field to be declarewd in a class that does not extend Stateful,
+   *      and suppresses checks for updates to the field.
+   *
    * @note This should go into annotations. For now it is here, so that we
    *  can experiment with it quickly between minor releases
    */