From ff30b1069e95f20f636cbe659482582e79de5751 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Fri, 30 May 2025 17:55:47 +0200
Subject: [PATCH 01/14] Don't decorate types in New with capture sets

---
 compiler/src/dotty/tools/dotc/cc/Setup.scala | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala
index 1357df42915e..de79eab11834 100644
--- a/compiler/src/dotty/tools/dotc/cc/Setup.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -422,7 +422,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
           case _ =>
         tp
 
-      /** Map references to capability classes C to C^,
+      /** Map references to capability classes C to C^{cap.rd},
        *  normalize captures and map to dependent functions.
        */
       def defaultApply(t: Type) =
@@ -618,6 +618,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
             traverse(body)
           catches.foreach(traverse)
           traverse(finalizer)
+        case tree: New =>
         case _ =>
           traverseChildren(tree)
       postProcess(tree)

From 82702ecea0005c9f2401c68d05ae59abfb035cc9 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Fri, 30 May 2025 18:51:11 +0200
Subject: [PATCH 02/14] Tweak improveReadOnly

Widen to cap.rd only if parent type does not extend Mutable.
---
 compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala   | 2 +-
 tests/neg-custom-args/captures/scope-extrude-mut.check | 7 ++++---
 2 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 20824f7eac80..da7d956f3524 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -1571,7 +1571,7 @@ class CheckCaptures extends Recheck, SymTransformer:
       case actual @ CapturingType(parent, refs)
       if parent.derivesFrom(defn.Caps_Mutable)
           && expected.isValueType
-          && !expected.isMutableType
+          && !expected.derivesFromMutable
           && !expected.isSingleton
           && !expected.isBoxedCapturing =>
         actual.derivedCapturingType(parent, refs.readOnly)
diff --git a/tests/neg-custom-args/captures/scope-extrude-mut.check b/tests/neg-custom-args/captures/scope-extrude-mut.check
index 1e01ddf834f8..70e6abc6a2ff 100644
--- a/tests/neg-custom-args/captures/scope-extrude-mut.check
+++ b/tests/neg-custom-args/captures/scope-extrude-mut.check
@@ -1,9 +1,10 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scope-extrude-mut.scala:9:8 ------------------------------
 9 |    a = a1  // error
   |        ^^
-  |        Found:    A^{a1.rd}
-  |        Required: A^
+  |        Found:    (a1 : A^)
+  |        Required: A^²
   |
-  |        where:    ^ refers to a fresh root capability in the type of variable a
+  |        where:    ^  refers to a fresh root capability created in value a1 when constructing mutable A
+  |                  ^² refers to a fresh root capability in the type of variable a
   |
   | longer explanation available when compiling with `-explain`

From c09443117c06c020931ef1662f3eb2c97c7ca520 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sat, 31 May 2025 11:03:01 +0200
Subject: [PATCH 03/14] Be more precise for the inCaptureCheckingOrSetup test

---
 compiler/src/dotty/tools/dotc/cc/CCState.scala    |  5 ++++-
 compiler/src/dotty/tools/dotc/cc/CaptureOps.scala | 15 +++++++++++----
 .../src/dotty/tools/dotc/cc/CheckCaptures.scala   |  1 +
 .../src/dotty/tools/dotc/core/TypeComparer.scala  |  4 ++--
 4 files changed, 18 insertions(+), 7 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CCState.scala b/compiler/src/dotty/tools/dotc/cc/CCState.scala
index 5feae257b97e..c425c5bb4266 100644
--- a/compiler/src/dotty/tools/dotc/cc/CCState.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CCState.scala
@@ -70,7 +70,7 @@ class CCState:
 
   // ------ Iteration count of capture checking run
 
-  private var iterCount = 1
+  private var iterCount = 0
 
   def iterationId = iterCount
 
@@ -78,6 +78,9 @@ class CCState:
     iterCount += 1
     try op finally iterCount -= 1
 
+  def start(): Unit =
+    iterCount = 1
+
   // ------ Global counters -----------------------
 
   /** Next CaptureSet.Var id */
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
index 21f25f8b7719..40fc6eb8f1de 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
@@ -22,11 +22,18 @@ private val Captures: Key[CaptureSet] = Key()
 def isCaptureChecking(using Context): Boolean =
   ctx.phaseId == Phases.checkCapturesPhase.id
 
-/** Are we at checkCaptures or Setup phase? */
+/** Are we in the CheckCaptures or Setup phase? */
 def isCaptureCheckingOrSetup(using Context): Boolean =
-  val ccId = Phases.checkCapturesPhase.id
-  val ctxId = ctx.phaseId
-  ctxId == ccId || ctxId == ccId - 1
+  val ccPhase = Phases.checkCapturesPhase
+  ccPhase.exists
+  && {
+    val ccId = ccPhase.id
+    val ctxId = ctx.phaseId
+    ctxId == ccId
+    || ctxId == ccId - 1 && ccState.iterationId > 0
+      // Note: just checking phase id is not enough since Setup would
+      // also be the phase after pattern matcher.
+  }
 
 /** A dependent function type with given arguments and result type
  *  TODO Move somewhere else where we treat all function type related ops together.
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index da7d956f3524..004a384430bc 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -1751,6 +1751,7 @@ class CheckCaptures extends Recheck, SymTransformer:
     private val setup: SetupAPI = thisPhase.prev.asInstanceOf[Setup]
 
     override def checkUnit(unit: CompilationUnit)(using Context): Unit =
+      ccState.start()
       setup.setupUnit(unit.tpdTree, this)
       collectCapturedMutVars.traverse(unit.tpdTree)
 
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 210e7f12b4b4..99cca6baf10c 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -1010,7 +1010,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
           if isCaptureCheckingOrSetup then
             tp1
               .match
-                case tp1: Capability if tp1.isTracked =>
+                case tp1: Capability if isCaptureCheckingOrSetup && tp1.isTracked =>
                   CapturingType(tp1w.stripCapturing, tp1.singletonCaptureSet)
                 case _ =>
                   tp1w
@@ -2110,7 +2110,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
    * since `T >: Int` is subsumed by both alternatives in the first match clause.
    *
    * However, the following should not:
-   * 
+   *
    *   def foo[T](e: Expr[T]): T = e match
    *     case I1(_) | B(_) => 42
    *

From 50f1e83cc465c4ff23899f2604b4af849edd7ba8 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Thu, 5 Jun 2025 17:35:40 +0200
Subject: [PATCH 04/14] Add undo infrastructure in TypeComparer

---
 .../dotty/tools/dotc/core/TypeComparer.scala  | 20 +++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 99cca6baf10c..5c3aeda29168 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -53,6 +53,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
     needsGc = false
     maxErrorLevel = -1
     errorNotes = Nil
+    logSize = 0
     if Config.checkTypeComparerReset then checkReset()
 
   private var pendingSubTypes: util.MutableSet[(Type, Type)] | Null = null
@@ -62,6 +63,9 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
   private var maxErrorLevel: Int = -1
   protected var errorNotes: List[(Int, ErrorNote)] = Nil
 
+  private val undoLog = mutable.ArrayBuffer[() => Unit]()
+  private var logSize = 0
+
   private var needsGc = false
 
   private var canCompareAtoms: Boolean = true // used for internal consistency checking
@@ -1579,15 +1583,25 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
       && tp1.derivesFrom(defn.Caps_CapSet)
       && tp2.derivesFrom(defn.Caps_CapSet)
 
+    def rollBack(prevSize: Int): Unit =
+      var i = prevSize
+      while i < undoLog.size do
+        undoLog(i)()
+        i += 1
+      undoLog.takeInPlace(prevSize)
+
     // begin recur
     if tp2 eq NoType then false
     else if tp1 eq tp2 then true
     else
       val savedCstr = constraint
       val savedGadt = ctx.gadt
+      val savedLogSize = logSize
       inline def restore() =
         state.constraint = savedCstr
         ctx.gadtState.restore(savedGadt)
+        if undoLog.size != savedLogSize then
+          rollBack(savedLogSize)
       val savedSuccessCount = successCount
       try
         val result = inNestedLevel:
@@ -2885,6 +2899,9 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
     (tp1.isBoxedCapturing == tp2.isBoxedCapturing)
     || refs1.subCaptures(CaptureSet.empty, makeVarState())
 
+  protected def logUndoAction(action: () => Unit) =
+    undoLog += action
+
   // ----------- Diagnostics --------------------------------------------------
 
   /** A hook for showing subtype traces. Overridden in ExplainingTypeComparer */
@@ -3504,6 +3521,9 @@ object TypeComparer {
   def subCaptures(refs1: CaptureSet, refs2: CaptureSet, vs: CaptureSet.VarState)(using Context): Boolean =
     comparing(_.subCaptures(refs1, refs2, vs))
 
+  def logUndoAction(action: () => Unit)(using Context): Unit =
+    comparer.logUndoAction(action)
+
   def inNestedLevel(op: => Boolean)(using Context): Boolean =
     comparer.inNestedLevel(op)
 

From ec786404a7e1f9a5aed9f2702d526069c13a4df8 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Thu, 5 Jun 2025 17:43:41 +0200
Subject: [PATCH 05/14] Map capture set to read-only when comparing mutable
 with non-mutable

---
 .../dotty/tools/dotc/core/TypeComparer.scala  | 29 ++++++++++++-------
 1 file changed, 18 insertions(+), 11 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 5c3aeda29168..2dc96a53d3f7 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -546,7 +546,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
       case tp1 @ CapturingType(parent1, refs1) =>
         def compareCapturing =
           if tp2.isAny then true
-          else if subCaptures(refs1, tp2.captureSet) && sameBoxed(tp1, tp2, refs1)
+          else if compareCaptures(tp1, refs1, tp2, tp2.captureSet)
             || !ctx.mode.is(Mode.CheckBoundsOrSelfType) && tp1.isAlwaysPure
           then
             val tp2a =
@@ -673,12 +673,12 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
                 && isSubInfo(info1.resultType, info2.resultType.subst(info2, info1))
               case (info1 @ CapturingType(parent1, refs1), info2: Type)
               if info2.stripCapturing.isInstanceOf[MethodOrPoly] =>
-                subCaptures(refs1, info2.captureSet) && sameBoxed(info1, info2, refs1)
+                compareCaptures(info1, refs1, info2, info2.captureSet)
                   && isSubInfo(parent1, info2)
               case (info1: Type, CapturingType(parent2, refs2))
               if info1.stripCapturing.isInstanceOf[MethodOrPoly] =>
                 val refs1 = info1.captureSet
-                (refs1.isAlwaysEmpty || subCaptures(refs1, refs2)) && sameBoxed(info1, info2, refs1)
+                (refs1.isAlwaysEmpty || compareCaptures(info1, refs1, info2, refs2))
                   && isSubInfo(info1, parent2)
               case _ =>
                 isSubType(info1, info2)
@@ -877,8 +877,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
                 case _ =>
                   false
               singletonOK
-              || subCaptures(refs1, refs2)
-                  && sameBoxed(tp1, tp2, refs1)
+              || compareCaptures(tp1, refs1, tp2, refs2)
                   && (recur(tp1.widen.stripCapturing, parent2)
                      || tp1.isInstanceOf[SingletonType] && recur(tp1, parent2)
                         // this alternative is needed in case the right hand side is a
@@ -2891,13 +2890,21 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
       println(i"fail while subCaptures $refs1 <:< $refs2")
       throw ex
 
-  /** Is the boxing status of tp1 and tp2 the same, or alternatively, is
-   *  the capture sets `refs1` of `tp1` a subcapture of the empty set?
-   *  In the latter case, boxing status does not matter.
+  /**
+   *  - Compare capture sets using subCaptures. If the lower type derives from Mutable and the
+   *    upper type does not, make the lower set read-only.
+   *  - Test whether the boxing status of tp1 and tp2 the same, or alternatively,
+   *    whether the capture set `refs1` of `tp1` is subcapture of the empty set?
+   *    In the latter case, boxing status does not matter.
    */
-  protected def sameBoxed(tp1: Type, tp2: Type, refs1: CaptureSet)(using Context): Boolean =
-    (tp1.isBoxedCapturing == tp2.isBoxedCapturing)
-    || refs1.subCaptures(CaptureSet.empty, makeVarState())
+  protected def compareCaptures(tp1: Type, refs1: CaptureSet, tp2: Type, refs2: CaptureSet): Boolean =
+    val refs1Adapted =
+      if tp1.derivesFromMutable && !tp2.derivesFromMutable
+      then refs1.readOnly
+      else refs1
+    subCaptures(refs1Adapted, refs2)
+    && (tp1.isBoxedCapturing == tp2.isBoxedCapturing)
+        || refs1.subCaptures(CaptureSet.empty, makeVarState())
 
   protected def logUndoAction(action: () => Unit) =
     undoLog += action

From dd79eb2352f830e19b8432ad93ff89cb04b86e1a Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Thu, 5 Jun 2025 18:05:26 +0200
Subject: [PATCH 06/14] Add missing CaptureSet.ofType case for RetainingTypes

---
 .../src/dotty/tools/dotc/cc/CaptureSet.scala  |  2 ++
 .../src/scala/collection/Iterable.scala       | 15 ++++++++++---
 .../captures/capture-vars-subtyping.scala     |  1 +
 .../captures/capture-vars-subtyping2.scala    |  3 ++-
 tests/neg-custom-args/captures/lazyref.check  | 12 +++++-----
 .../captures/sep-curried-redux.scala          | 18 +++++++++++++++
 .../captures/SizeCompareOps-redux.scala       | 22 +++++++++++++++++++
 7 files changed, 63 insertions(+), 10 deletions(-)
 create mode 100644 tests/neg-custom-args/captures/sep-curried-redux.scala
 create mode 100644 tests/pending/pos-custom-args/captures/SizeCompareOps-redux.scala

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index 22236a3853ef..70c0b2e72f5a 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -1360,6 +1360,8 @@ object CaptureSet:
           else empty
         case CapturingType(parent, refs) =>
           recur(parent) ++ refs
+        case tp @ AnnotatedType(parent, ann) if ann.symbol.isRetains =>
+          recur(parent) ++ ann.tree.toCaptureSet
         case tpd @ defn.RefinedFunctionOf(rinfo: MethodType) if followResult =>
           ofType(tpd.parent, followResult = false)            // pick up capture set from parent type
           ++ recur(rinfo.resType)                             // add capture set of result
diff --git a/scala2-library-cc/src/scala/collection/Iterable.scala b/scala2-library-cc/src/scala/collection/Iterable.scala
index 6556f31d378d..6b6a03f88965 100644
--- a/scala2-library-cc/src/scala/collection/Iterable.scala
+++ b/scala2-library-cc/src/scala/collection/Iterable.scala
@@ -17,6 +17,7 @@ import scala.annotation.unchecked.uncheckedVariance
 import scala.collection.mutable.Builder
 import scala.collection.View.{LeftPartitionMapped, RightPartitionMapped}
 import language.experimental.captureChecking
+import scala.caps.unsafe.unsafeAssumePure
 
 /** Base trait for generic collections.
   *
@@ -302,7 +303,8 @@ trait IterableOps[+A, +CC[_], +C] extends Any with IterableOnce[A] with Iterable
     * this.sizeIs > size     // this.sizeCompare(size) > 0
     * }}}
     */
-  @inline final def sizeIs: IterableOps.SizeCompareOps^{this} = new IterableOps.SizeCompareOps(this)
+  @inline final def sizeIs: IterableOps.SizeCompareOps^{this} = new IterableOps.SizeCompareOps(this.unsafeAssumePure)
+    // CC Problem: unsafeAssumePure needed since we had to change the argument signatire of SizeCompareOps
 
   /** Compares the size of this $coll to the size of another `Iterable`.
     *
@@ -866,8 +868,15 @@ object IterableOps {
     * These operations are implemented in terms of
     * [[scala.collection.IterableOps.sizeCompare(Int) `sizeCompare(Int)`]].
     */
-  final class SizeCompareOps private[collection](val it: IterableOps[_, AnyConstr, _]^) extends AnyVal {
-    this: SizeCompareOps^{it} =>
+  final class SizeCompareOps private[collection](val it: IterableOps[_, AnyConstr, _]/*^*/) extends AnyVal {
+    this: SizeCompareOps/*^*/ =>
+    // CC Problem: if we add the logically needed `^`s to the `it` parameter and the
+    // self type, separation checking fails in the compiler-generated equals$extends
+    // method of the value class. There seems to be something wrong how pattern
+    // matching interacts with separation checking. A minimized test case
+    // is pending/pos-custom-args/captures/SizeCompareOps-redux.scala.
+    // Without the `^`s, the `sizeIs` method needs an unsafeAssumePure.
+
     /** Tests if the size of the collection is less than some value. */
     @inline def <(size: Int): Boolean = it.sizeCompare(size) < 0
     /** Tests if the size of the collection is less than or equal to some value. */
diff --git a/tests/neg-custom-args/captures/capture-vars-subtyping.scala b/tests/neg-custom-args/captures/capture-vars-subtyping.scala
index 9a32abe0b6e3..68b26dcf564d 100644
--- a/tests/neg-custom-args/captures/capture-vars-subtyping.scala
+++ b/tests/neg-custom-args/captures/capture-vars-subtyping.scala
@@ -1,4 +1,5 @@
 import language.experimental.captureChecking
+import language.`3.7` // no separation checking, TODO enable
 import caps.*
 
 def test[C^] =
diff --git a/tests/neg-custom-args/captures/capture-vars-subtyping2.scala b/tests/neg-custom-args/captures/capture-vars-subtyping2.scala
index ccf646f34dca..235bfb5e1cf0 100644
--- a/tests/neg-custom-args/captures/capture-vars-subtyping2.scala
+++ b/tests/neg-custom-args/captures/capture-vars-subtyping2.scala
@@ -25,7 +25,8 @@ trait BoundsTest:
     val ec2: CapSet^{C} = e
     val eb: B = e
     val eb2: CapSet^{B} = e
-    val ea: A = e
+    locally:
+      val ea: A = e
     val ea2: CapSet^{A} = e
     val ex: X = e            // error
     val ex2: CapSet^{X} = e // error
diff --git a/tests/neg-custom-args/captures/lazyref.check b/tests/neg-custom-args/captures/lazyref.check
index 9c2f1a2d1a50..dde9e6fd2bac 100644
--- a/tests/neg-custom-args/captures/lazyref.check
+++ b/tests/neg-custom-args/captures/lazyref.check
@@ -39,7 +39,7 @@
    |             ^^^^
    |             Separation failure: Illegal access to {cap1} which is hidden by the previous definition
    |             of value ref2 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
-   |             This type hides capabilities  {cap1}
+   |             This type hides capabilities  {LazyRef.this.elem, cap1}
    |
    |             where:    => refers to a fresh root capability in the type of value elem
 -- Error: tests/neg-custom-args/captures/lazyref.scala:26:9 ------------------------------------------------------------
@@ -47,7 +47,7 @@
    |         ^^^^
    |         Separation failure: Illegal access to {cap1} which is hidden by the previous definition
    |         of value ref3 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
-   |         This type hides capabilities  {ref2*, cap1}
+   |         This type hides capabilities  {LazyRef.this.elem, ref2*, cap1}
    |
    |         where:    => refers to a fresh root capability in the type of value elem
 -- Error: tests/neg-custom-args/captures/lazyref.scala:26:17 -----------------------------------------------------------
@@ -55,7 +55,7 @@
    |                 ^^^^
    |                 Separation failure: Illegal access to {cap2} which is hidden by the previous definition
    |                 of value ref3 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
-   |                 This type hides capabilities  {ref2*, cap1}
+   |                 This type hides capabilities  {LazyRef.this.elem, ref2*, cap1}
    |
    |                 where:    => refers to a fresh root capability in the type of value elem
 -- Error: tests/neg-custom-args/captures/lazyref.scala:27:11 -----------------------------------------------------------
@@ -63,7 +63,7 @@
    |           ^^^^
    |           Separation failure: Illegal access to {cap1, ref1} which is hidden by the previous definition
    |           of value ref3 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
-   |           This type hides capabilities  {ref2*, cap1}
+   |           This type hides capabilities  {LazyRef.this.elem, ref2*, cap1}
    |
    |           where:    => refers to a fresh root capability in the type of value elem
 -- Error: tests/neg-custom-args/captures/lazyref.scala:28:11 -----------------------------------------------------------
@@ -71,7 +71,7 @@
    |           ^^^^
    |           Separation failure: Illegal access to {cap1, cap2, ref1} which is hidden by the previous definition
    |           of value ref3 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
-   |           This type hides capabilities  {ref2*, cap1}
+   |           This type hides capabilities  {LazyRef.this.elem, ref2*, cap1}
    |
    |           where:    => refers to a fresh root capability in the type of value elem
 -- Error: tests/neg-custom-args/captures/lazyref.scala:29:9 ------------------------------------------------------------
@@ -79,6 +79,6 @@
    |         ^
    |         Separation failure: Illegal access to {cap2} which is hidden by the previous definition
    |         of value ref3 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
-   |         This type hides capabilities  {ref2*, cap1}
+   |         This type hides capabilities  {LazyRef.this.elem, ref2*, cap1}
    |
    |         where:    => refers to a fresh root capability in the type of value elem
diff --git a/tests/neg-custom-args/captures/sep-curried-redux.scala b/tests/neg-custom-args/captures/sep-curried-redux.scala
new file mode 100644
index 000000000000..31b349b09f94
--- /dev/null
+++ b/tests/neg-custom-args/captures/sep-curried-redux.scala
@@ -0,0 +1,18 @@
+import language.experimental.captureChecking
+import caps.*
+
+class Ref[T](init: T) extends Mutable:
+  private var value: T = init
+  def get: T = value
+  mut def set(newValue: T): Unit = value = newValue
+
+// a library function that assumes that a and b MUST BE separate
+def swap[T](a: Ref[Int]^, b: Ref[Int]^): Unit = ???
+
+def test4(): Unit =
+  val a: Ref[Int]^ = Ref(0)
+  val foo: (x: Ref[Int]^) -> (y: Ref[Int]^) ->{x} Unit =
+    x => y => swap(x, y)
+  val f = foo(a)
+  f(a) // error
+
diff --git a/tests/pending/pos-custom-args/captures/SizeCompareOps-redux.scala b/tests/pending/pos-custom-args/captures/SizeCompareOps-redux.scala
new file mode 100644
index 000000000000..f694699fded1
--- /dev/null
+++ b/tests/pending/pos-custom-args/captures/SizeCompareOps-redux.scala
@@ -0,0 +1,22 @@
+package collection
+trait IterableOps[+A, +CC[_], +C] extends Any:
+  def sizeCompare(size: Int): Int
+
+object IterableOps:
+
+  type AnyConstr[X] = Any
+
+  final class SizeCompareOps private[collection](val it: IterableOps[_, AnyConstr, _]^) extends AnyVal:
+    this: SizeCompareOps^{it} =>
+    /** Tests if the size of the collection is less than some value. */
+    @inline def <(size: Int): Boolean = it.sizeCompare(size) < 0
+    /** Tests if the size of the collection is less than or equal to some value. */
+    @inline def <=(size: Int): Boolean = it.sizeCompare(size) <= 0
+    /** Tests if the size of the collection is equal to some value. */
+    @inline def ==(size: Int): Boolean = it.sizeCompare(size) == 0
+    /** Tests if the size of the collection is not equal to some value. */
+    @inline def !=(size: Int): Boolean = it.sizeCompare(size) != 0
+    /** Tests if the size of the collection is greater than or equal to some value. */
+    @inline def >=(size: Int): Boolean = it.sizeCompare(size) >= 0
+    /** Tests if the size of the collection is greater than some value. */
+    @inline def >(size: Int): Boolean = it.sizeCompare(size) > 0

From 8ecb4aa549370f7cd71b1f026942961229a3754a Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Fri, 6 Jun 2025 12:26:19 +0200
Subject: [PATCH 07/14] Simplify footprint in SepChecks

---
 .../dotty/tools/dotc/cc/CheckCaptures.scala   |  4 +-
 .../src/dotty/tools/dotc/cc/SepCheck.scala    | 54 ++++++++++---------
 .../captures/sep-counter.check                |  2 +-
 3 files changed, 33 insertions(+), 27 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 004a384430bc..d3ae08e4559c 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -1231,7 +1231,8 @@ class CheckCaptures extends Recheck, SymTransformer:
       val saved = curEnv
       tree match
         case _: RefTree | closureDef(_) if pt.isBoxedCapturing =>
-          curEnv = Env(curEnv.owner, EnvKind.Boxed, CaptureSet.Var(curEnv.owner, level = ccState.currentLevel), curEnv)
+          curEnv = Env(curEnv.owner, EnvKind.Boxed,
+            CaptureSet.Var(curEnv.owner, level = ccState.currentLevel), curEnv)
         case _ =>
       val res =
         try
@@ -1575,6 +1576,7 @@ class CheckCaptures extends Recheck, SymTransformer:
           && !expected.isSingleton
           && !expected.isBoxedCapturing =>
         actual.derivedCapturingType(parent, refs.readOnly)
+          .showing(i"improv ro $actual vs $expected = $result", capt)
       case _ =>
         actual
 
diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
index a402e58624f2..4a391bf2c62f 100644
--- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
+++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
@@ -165,12 +165,11 @@ object SepCheck:
   extension (refs: Refs)
 
     /** The footprint of a set of references `refs` the smallest set `F` such that
-     *   1. if includeMax is false then no maximal capability is in `F`
-     *   2. all capabilities in `refs` satisfying (1) are in `F`
-     *   3. if `f in F` then the footprint of `f`'s info is also in `F`.
+     *   1. all capabilities in `refs` satisfying (1) are in `F`
+     *   2. if `f in F` then the footprint of `f`'s info is also in `F`.
      */
-    private def footprint(includeMax: Boolean = false)(using Context): Refs =
-      def retain(ref: Capability) = includeMax || !ref.isTerminalCapability
+    private def footprint(using Context): Refs =
+      def retain(ref: Capability) = !ref.isTerminalCapability
       def recur(elems: Refs, newElems: List[Capability]): Refs = newElems match
         case newElem :: newElems1 =>
           val superElems = newElem.captureSetOfInfo.elems.filter: superElem =>
@@ -326,15 +325,14 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
         i"$other"
 
   def overlapStr(hiddenSet: Refs, clashSet: Refs)(using Context): String =
-    val hiddenFootprint = hiddenSet.footprint()
-    val clashFootprint = clashSet.footprint()
+    val hiddenFootprint = hiddenSet.footprint
+    val clashFootprint = clashSet.footprint
     // The overlap of footprints, or, of this empty the set of shared peaks.
     // We prefer footprint overlap since it tends to be more informative.
     val overlap = hiddenFootprint.overlapWith(clashFootprint)
     if !overlap.isEmpty then i"${CaptureSet(overlap)}"
     else
-      val sharedPeaks = hiddenSet.footprint(includeMax = true).sharedWith:
-        clashSet.footprint(includeMax = true)
+      val sharedPeaks = hiddenSet.peaks.sharedWith(clashSet.peaks)
       assert(!sharedPeaks.isEmpty, i"no overlap for $hiddenSet vs $clashSet")
       sharedPeaksStr(sharedPeaks)
 
@@ -386,9 +384,9 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
           |Some of these overlap with the captures of the ${clashArgStr.trim}$clashTypeStr.
           |
           |  Hidden set of current argument        : ${CaptureSet(hiddenSet)}
-          |  Hidden footprint of current argument  : ${CaptureSet(hiddenSet.footprint())}
+          |  Hidden footprint of current argument  : ${CaptureSet(hiddenSet.footprint)}
           |  Capture set of $clashArgStr        : ${CaptureSet(clashSet)}
-          |  Footprint set of $clashArgStr      : ${CaptureSet(clashSet.footprint())}
+          |  Footprint set of $clashArgStr      : ${CaptureSet(clashSet.footprint)}
           |  The two sets overlap at               : ${overlapStr(hiddenSet, clashSet)}""",
       polyArg.srcPos)
 
@@ -679,7 +677,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
       val captured = genPart.deepCaptureSet.elems
       val hiddenSet = captured.hiddenSet.pruned
       val clashSet = otherPart.deepCaptureSet.elems
-      val deepClashSet = (clashSet.footprint() ++ clashSet.hiddenSet).pruned
+      val deepClashSet = (clashSet.footprint ++ clashSet.hiddenSet).pruned
       report.error(
         em"""Separation failure in ${role.description} $tpe.
             |One part,  $genPart, hides capabilities  ${CaptureSet(hiddenSet)}.
@@ -782,11 +780,11 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
                                     // "see through them" when we look at hidden sets.
         then
           val refs = tpe.deepCaptureSet.elems
-          val toCheck = refs.hiddenSet.footprint().deduct(refs.footprint())
+          val toCheck = refs.hiddenSet.footprint.deduct(refs.footprint)
           checkConsumedRefs(toCheck, tpe, role, i"${role.description} $tpe hides", pos)
       case TypeRole.Argument(arg) =>
         if tpe.hasAnnotation(defn.ConsumeAnnot) then
-          val capts = captures(arg).footprint()
+          val capts = captures(arg).footprint
           checkConsumedRefs(capts, tpe, role, i"argument to @consume parameter with type ${arg.nuType} refers to", pos)
       case _ =>
 
@@ -881,7 +879,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
   def checkValOrDefDef(tree: ValOrDefDef)(using Context): Unit =
     if !tree.symbol.isOneOf(TermParamOrAccessor) && !isUnsafeAssumeSeparate(tree.rhs) then
       checkType(tree.tpt, tree.symbol)
-      capt.println(i"sep check def ${tree.symbol}: ${tree.tpt} with ${captures(tree.tpt).hiddenSet.footprint()}")
+      capt.println(i"sep check def ${tree.symbol}: ${tree.tpt} with ${captures(tree.tpt).hiddenSet.footprint}")
       pushDef(tree, captures(tree.tpt).hiddenSet.deductSymRefs(tree.symbol))
 
   def inSection[T](op: => T)(using Context): T =
@@ -894,6 +892,13 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
 
   def traverseSection[T](tree: Tree)(using Context) = inSection(traverseChildren(tree))
 
+  /** Should separatiion checking be disabled for the body of this method?
+   */
+  def skippable(sym: Symbol)(using Context): Boolean =
+    sym.isInlineMethod
+      // We currently skip inline method bodies since these seem to generan
+      // spurious recheck completions. Test case is i20237.scala
+
   /** Traverse `tree` and perform separation checks everywhere */
   def traverse(tree: Tree)(using Context): Unit =
     if !isUnsafeAssumeSeparate(tree) then trace(i"checking separate $tree"):
@@ -902,7 +907,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
         case tree @ Select(qual, _) if tree.symbol.is(Method) && tree.symbol.isConsumeParam =>
           traverseChildren(tree)
           checkConsumedRefs(
-              captures(qual).footprint(), qual.nuType,
+              captures(qual).footprint, qual.nuType,
               TypeRole.Qualifier(qual, tree.symbol),
               i"call prefix of @consume ${tree.symbol} refers to", qual.srcPos)
         case tree: GenericApply =>
@@ -916,15 +921,14 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
           traverseChildren(tree)
           checkValOrDefDef(tree)
         case tree: DefDef =>
-          if tree.symbol.isInlineMethod then
-            // We currently skip inline method since these seem to generate
-            // spurious recheck completions. Test case is i20237.scala
-            capt.println(i"skipping sep check of inline def ${tree.symbol}")
-          else inSection:
-            consumed.segment:
-              for params <- tree.paramss; case param: ValDef <- params do
-                pushDef(param, emptyRefs)
-              traverseChildren(tree)
+          if skippable(tree.symbol) then
+            capt.println(i"skipping sep check of ${tree.symbol}")
+          else
+            inSection:
+              consumed.segment:
+                for params <- tree.paramss; case param: ValDef <- params do
+                  pushDef(param, emptyRefs)
+                traverseChildren(tree)
           checkValOrDefDef(tree)
         case If(cond, thenp, elsep) =>
           traverse(cond)
diff --git a/tests/neg-custom-args/captures/sep-counter.check b/tests/neg-custom-args/captures/sep-counter.check
index ee38eba5eab9..112f23b6ecd3 100644
--- a/tests/neg-custom-args/captures/sep-counter.check
+++ b/tests/neg-custom-args/captures/sep-counter.check
@@ -4,7 +4,7 @@
    |                   Separation failure in method mkCounter's result type Pair[box Ref^, box Ref^²].
    |                   One part,  box Ref^, hides capabilities  {cap}.
    |                   Another part,  box Ref^²,  captures capabilities  {cap}.
-   |                   The two sets overlap at  cap of value c.
+   |                   The two sets overlap at  cap of method mkCounter.
    |
    |                   where:    ^   refers to a fresh root capability in the result type of method mkCounter
    |                             ^²  refers to a fresh root capability in the result type of method mkCounter

From 1c14c77a141dacc769ddc84d74a76d2875bb5016 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Fri, 6 Jun 2025 13:02:52 +0200
Subject: [PATCH 08/14] Turn assert in RetainingType into test

We used to have the case where a RetainingType needs to be tested after
a CapturingType. It would be better to reverse that order: If a RetainingType
is possible test this first, and then test a CapturingType. If we just test for
CapturingType we should crash if it's a RetainingType. That way we can express
expectations that a retaining type was transformed.

This commit does the first half: RetainingType unapply now can handle a CapturingType
(and respond with a None). We still need to do the second half, that a CapturingType
unapply does not handle a RetainingType.
---
 compiler/src/dotty/tools/dotc/cc/CapturingType.scala |  7 +++++--
 compiler/src/dotty/tools/dotc/cc/RetainingType.scala | 10 ++++------
 2 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CapturingType.scala b/compiler/src/dotty/tools/dotc/cc/CapturingType.scala
index 9f9b923b2c88..6380609d8543 100644
--- a/compiler/src/dotty/tools/dotc/cc/CapturingType.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CapturingType.scala
@@ -52,11 +52,11 @@ object CapturingType:
     else decomposeCapturingType(tp)
 
   /** Decompose `tp` as a capturing type without taking IgnoreCaptures into account */
-  def decomposeCapturingType(tp: Type)(using Context): Option[(Type, CaptureSet)] = tp match
+  def decomposeCapturingType(using Context)(tp: Type, alsoRetains: Boolean = isCaptureChecking): Option[(Type, CaptureSet)] = tp match
     case AnnotatedType(parent, ann: CaptureAnnotation)
     if isCaptureCheckingOrSetup =>
       Some((parent, ann.refs))
-    case AnnotatedType(parent, ann) if ann.symbol.isRetains && isCaptureChecking =>
+    case AnnotatedType(parent, ann) if ann.symbol.isRetains && alsoRetains =>
       // There are some circumstances where we cannot map annotated types
       // with retains annotations to capturing types, so this second recognizer
       // path still has to exist. One example is when checking capture sets
@@ -68,6 +68,9 @@ object CapturingType:
       // type `C^{f}` which does not have a capture annotation yet. The transformed
       // type would be in a copy of the dependent function type, but it is useless
       // since we need to check the original reference.
+      //
+      // TODO In other situations we expect that the type is already transformed to a
+      // CapturingType and we should crash if this not the case.
       try Some((parent, ann.tree.toCaptureSet))
       catch case ex: IllegalCaptureRef => None
     case _ =>
diff --git a/compiler/src/dotty/tools/dotc/cc/RetainingType.scala b/compiler/src/dotty/tools/dotc/cc/RetainingType.scala
index 8bdd6a7301a8..6fde63a0d3ac 100644
--- a/compiler/src/dotty/tools/dotc/cc/RetainingType.scala
+++ b/compiler/src/dotty/tools/dotc/cc/RetainingType.scala
@@ -8,7 +8,8 @@ import ast.tpd.*
 import Annotations.Annotation
 import Decorators.i
 
-/** A builder and extractor for annotated types with @retains or @retainsByName annotations.
+/** A builder and extractor for annotated types with @retains or @retainsByName annotations
+ *  excluding CapturingTypes.
  */
 object RetainingType:
 
@@ -21,11 +22,8 @@ object RetainingType:
     val sym = tp.annot.symbol
     if sym.isRetainsLike then
       tp.annot match
-        case _: CaptureAnnotation =>
-          assert(ctx.mode.is(Mode.IgnoreCaptures), s"bad retains $tp at ${ctx.phase}")
-          None
-        case ann =>
-          Some((tp.parent, ann.tree.retainedSet))
+        case _: CaptureAnnotation => None
+        case ann => Some((tp.parent, ann.tree.retainedSet))
     else
       None
 end RetainingType

From 4344f05c3e185a54f11d4a4e92bd2f51106eff71 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Fri, 6 Jun 2025 19:50:53 +0200
Subject: [PATCH 09/14] Fix backwards propagation in intersections

---
 compiler/src/dotty/tools/dotc/cc/CaptureSet.scala | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index 70c0b2e72f5a..b15734335f2e 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -930,11 +930,15 @@ object CaptureSet:
     deps += cs2
 
     override def tryInclude(elem: Capability, origin: CaptureSet)(using Context, VarState): Boolean =
-      val present =
+      val inIntersection =
         if origin eq cs1 then cs2.accountsFor(elem)
         else if origin eq cs2 then cs1.accountsFor(elem)
         else true
-      !present || accountsFor(elem) || addNewElem(elem)
+      !inIntersection
+      || accountsFor(elem)
+      || addNewElem(elem)
+        && ((origin eq cs1) || cs1.tryInclude(elem, this))
+        && ((origin eq cs2) || cs2.tryInclude(elem, this))
 
     override def computeApprox(origin: CaptureSet)(using Context): CaptureSet =
       if (origin eq cs1) || (origin eq cs2) then

From 650874b4f54ea1aefad8a32431c37973bef0006c Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sat, 7 Jun 2025 19:30:43 +0200
Subject: [PATCH 10/14] Introduce mutability qualifiers

---
 .../src/dotty/tools/dotc/cc/Capability.scala  |   6 +
 .../src/dotty/tools/dotc/cc/CaptureSet.scala  | 111 +++++++++++++++++-
 .../dotty/tools/dotc/cc/CapturingType.scala   |   6 +
 .../src/dotty/tools/dotc/cc/ccConfig.scala    |   4 +-
 .../tools/dotc/printing/PlainPrinter.scala    |   5 +-
 tests/pos-custom-args/captures/matrix.scala   |  37 ++++++
 6 files changed, 164 insertions(+), 5 deletions(-)
 create mode 100644 tests/pos-custom-args/captures/matrix.scala

diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala
index ca15fb397a42..f99b27854bac 100644
--- a/compiler/src/dotty/tools/dotc/cc/Capability.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala
@@ -330,6 +330,12 @@ object Capabilities:
     final def isExclusive(using Context): Boolean =
       !isReadOnly && (isTerminalCapability || captureSetOfInfo.isExclusive)
 
+    /** Similar to isExlusive, but also includes capabilties with capture
+     *  set variables in their info whose status is still open.
+     */
+    final def maybeExclusive(using Context): Boolean =
+      !isReadOnly && (isTerminalCapability || captureSetOfInfo.maybeExclusive)
+
     final def isWellformed(using Context): Boolean = this match
       case self: CoreCapability => self.isTrackableRef
       case _ => true
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index b15734335f2e..6a5f650440a3 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -44,12 +44,24 @@ import Capabilities.*
  */
 sealed abstract class CaptureSet extends Showable:
   import CaptureSet.*
+  import Mutability.*
 
   /** The elements of this capture set. For capture variables,
    *  the elements known so far.
    */
   def elems: Refs
 
+  protected var myMut : Mutability = Ignored
+
+  /** The access kind of this CaptureSet. */
+  def mutability(using Context): Mutability = myMut
+
+  def mutability_=(x: Mutability): Unit =
+    myMut = x
+
+  /** Mark this capture set as belonging to a Mutable type. */
+  def setMutable()(using Context): Unit
+
   /** Is this capture set constant (i.e. not an unsolved capture variable)?
    *  Solved capture variables count as constant.
    */
@@ -127,6 +139,13 @@ sealed abstract class CaptureSet extends Showable:
   final def isExclusive(using Context): Boolean =
     elems.exists(_.isExclusive)
 
+  /** Similar to isExlusive, but also includes capture set variables
+   *  with unknown status.
+   */
+  final def maybeExclusive(using Context): Boolean = reporting.trace(i"mabe exclusive $this"):
+    if isConst then elems.exists(_.maybeExclusive)
+    else mutability != ReadOnly
+
   final def keepAlways: Boolean = this.isInstanceOf[EmptyWithProvenance]
 
   def failWith(fail: TypeComparer.ErrorNote)(using Context): false =
@@ -164,6 +183,9 @@ sealed abstract class CaptureSet extends Showable:
       // through this method.
       newElems.forall(tryInclude(_, origin))
 
+  protected def mutableToReader(origin: CaptureSet)(using Context): Boolean =
+    if mutability == Mutable then toReader() else true
+
   /** Add an element to this capture set, assuming it is not already accounted for,
    *  and omitting any mapping or filtering.
    *
@@ -188,6 +210,8 @@ sealed abstract class CaptureSet extends Showable:
    */
   protected def addThisElem(elem: Capability)(using Context, VarState): Boolean
 
+  protected def toReader()(using Context): Boolean
+
   protected def addIfHiddenOrFail(elem: Capability)(using ctx: Context, vs: VarState): Boolean =
     elems.exists(_.maxSubsumes(elem, canAddHidden = true))
     || failWith(IncludeFailure(this, elem))
@@ -258,7 +282,12 @@ sealed abstract class CaptureSet extends Showable:
 
   /** The subcapturing test, using a given VarState */
   final def subCaptures(that: CaptureSet)(using ctx: Context, vs: VarState = VarState()): Boolean =
-    if that.tryInclude(elems, this) then
+    val this1 = this.adaptMutability(that)
+    if this1 == null then false
+    else if this1 ne this then
+      capt.println(i"WIDEN ro $this with ${this.mutability} <:< $that with ${that.mutability} to $this1")
+      this1.subCaptures(that, vs)
+    else if that.tryInclude(elems, this) then
       addDependent(that)
     else
       varState.rollBack()
@@ -271,6 +300,14 @@ sealed abstract class CaptureSet extends Showable:
        this.subCaptures(that, VarState.Separate)
     && that.subCaptures(this, VarState.Separate)
 
+  def adaptMutability(that: CaptureSet)(using Context): CaptureSet | Null =
+    val m1 = this.mutability
+    val m2 = that.mutability
+    if m1 == Mutable && m2 == Reader then this.readOnly
+    else if m1 == Reader && m2 == Mutable then
+      if that.toReader() then this else null
+    else this
+
   /** The smallest capture set (via <:<) that is a superset of both
    *  `this` and `that`
    */
@@ -372,7 +409,10 @@ sealed abstract class CaptureSet extends Showable:
 
   def maybe(using Context): CaptureSet = map(MaybeMap())
 
-  def readOnly(using Context): CaptureSet = map(ReadOnlyMap())
+  def readOnly(using Context): CaptureSet =
+    val res = map(ReadOnlyMap())
+    if mutability != Ignored then res.mutability = Reader
+    res
 
   /** A bad root `elem` is inadmissible as a member of this set. What is a bad roots depends
    *  on the value of `rootLimit`.
@@ -445,6 +485,25 @@ object CaptureSet:
   type Vars = SimpleIdentitySet[Var]
   type Deps = SimpleIdentitySet[CaptureSet]
 
+  enum Mutability:
+    case Mutable, Reader, Ignored
+
+    def | (that: Mutability): Mutability =
+      if this == that then this
+      else if this == Ignored || that == Ignored then Ignored
+      else if this == Reader || that == Reader then Reader
+      else Mutable
+
+    def & (that: Mutability): Mutability =
+      if this == that then this
+      else if this == Ignored then that
+      else if that == Ignored then this
+      else if this == Reader then that
+      else this
+
+  end Mutability
+  import Mutability.*
+
   /** If set to `true`, capture stack traces that tell us where sets are created */
   private final val debugSets = false
 
@@ -496,6 +555,8 @@ object CaptureSet:
         false
       }
 
+    def toReader()(using Context) = false
+
     def addDependent(cs: CaptureSet)(using Context, VarState) = true
 
     def upperApprox(origin: CaptureSet)(using Context): CaptureSet = this
@@ -506,6 +567,17 @@ object CaptureSet:
 
     def owner = NoSymbol
 
+    private var isComplete = true
+
+    def setMutable()(using Context): Unit =
+      isComplete = false // delay computation of Mutability status
+
+    override def mutability(using Context): Mutability =
+      if !isComplete then
+        myMut = if maybeExclusive then Mutable else Reader
+        isComplete = true
+      myMut
+
     override def toString = elems.toString
   end Const
 
@@ -524,6 +596,7 @@ object CaptureSet:
   object Fluid extends Const(emptyRefs):
     override def isAlwaysEmpty(using Context) = false
     override def addThisElem(elem: Capability)(using Context, VarState) = true
+    override def toReader()(using Context) = true
     override def accountsFor(x: Capability)(using Context)(using VarState): Boolean = true
     override def mightAccountFor(x: Capability)(using Context): Boolean = true
     override def toString = "<fluid>"
@@ -563,6 +636,9 @@ object CaptureSet:
      */
     var deps: Deps = SimpleIdentitySet.empty
 
+    def setMutable()(using Context): Unit =
+      mutability = Mutable
+
     def isConst(using Context) = solved >= ccState.iterationId
     def isAlwaysEmpty(using Context) = isConst && elems.isEmpty
     def isProvisionallySolved(using Context): Boolean = solved > 0 && solved != Int.MaxValue
@@ -640,6 +716,13 @@ object CaptureSet:
             case note: IncludeFailure => note.addToTrace(this)
         res
 
+    final def toReader()(using Context) =
+      if isConst then false // TODO add error note when failing?
+      else
+        mutability = Reader
+        TypeComparer.logUndoAction(() => mutability = Mutable)
+        deps.forall(_.mutableToReader(this))
+
     private def isPartOf(binder: Type)(using Context): Boolean =
       val find = new TypeAccumulator[Boolean]:
         def apply(b: Boolean, t: Type) =
@@ -744,6 +827,8 @@ object CaptureSet:
     def markSolved(provisional: Boolean)(using Context): Unit =
       solved = if provisional then ccState.iterationId else Int.MaxValue
       deps.foreach(_.propagateSolved(provisional))
+      if mutability == Mutable && !maybeExclusive then mutability = Reader
+
 
     var skippedMaps: Set[TypeMap] = Set.empty
 
@@ -803,8 +888,14 @@ object CaptureSet:
     /** The variable from which this variable is derived */
     def source: Var
 
+    mutability = source.mutability
+
     addAsDependentTo(source)
 
+    override def mutableToReader(origin: CaptureSet)(using Context): Boolean =
+      super.mutableToReader(origin)
+      && ((origin eq source) || source.mutableToReader(this))
+
     override def propagateSolved(provisional: Boolean)(using Context) =
       if source.isConst && !isConst then markSolved(provisional)
 
@@ -904,6 +995,7 @@ object CaptureSet:
   extends Var(initialElems = cs1.elems ++ cs2.elems):
     addAsDependentTo(cs1)
     addAsDependentTo(cs2)
+    mutability = cs1.mutability | cs2.mutability
 
     override def tryInclude(elem: Capability, origin: CaptureSet)(using Context, VarState): Boolean =
       if accountsFor(elem) then true
@@ -918,6 +1010,15 @@ object CaptureSet:
           else res
         else res
 
+    override def mutableToReader(origin: CaptureSet)(using Context): Boolean =
+      super.mutableToReader(origin)
+      && {
+        if (origin eq cs1) || (origin eq cs2) then true
+        else if cs1.isConst && cs1.mutability == Mutable then cs2.mutableToReader(this)
+        else if cs2.isConst && cs2.mutability == Mutable then cs1.mutableToReader(this)
+        else true
+      }
+
     override def propagateSolved(provisional: Boolean)(using Context) =
       if cs1.isConst && cs2.isConst && !isConst then markSolved(provisional)
   end Union
@@ -928,6 +1029,7 @@ object CaptureSet:
     addAsDependentTo(cs2)
     deps += cs1
     deps += cs2
+    mutability = cs1.mutability & cs2.mutability
 
     override def tryInclude(elem: Capability, origin: CaptureSet)(using Context, VarState): Boolean =
       val inIntersection =
@@ -940,6 +1042,11 @@ object CaptureSet:
         && ((origin eq cs1) || cs1.tryInclude(elem, this))
         && ((origin eq cs2) || cs2.tryInclude(elem, this))
 
+    override def mutableToReader(origin: CaptureSet)(using Context): Boolean =
+      super.mutableToReader(origin)
+      && ((origin eq cs1) || cs1.mutableToReader(this))
+      && ((origin eq cs2) || cs2.mutableToReader(this))
+
     override def computeApprox(origin: CaptureSet)(using Context): CaptureSet =
       if (origin eq cs1) || (origin eq cs2) then
         // it's a combination of origin with some other set, so not a superset of `origin`,
diff --git a/compiler/src/dotty/tools/dotc/cc/CapturingType.scala b/compiler/src/dotty/tools/dotc/cc/CapturingType.scala
index 6380609d8543..58bee8132b98 100644
--- a/compiler/src/dotty/tools/dotc/cc/CapturingType.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CapturingType.scala
@@ -39,6 +39,7 @@ object CapturingType:
       case parent @ CapturingType(parent1, refs1) if boxed || !parent.isBoxed =>
         apply(parent1, refs ++ refs1, boxed)
       case _ =>
+        if parent.derivesFromMutable then refs.setMutable()
         AnnotatedType(parent, CaptureAnnotation(refs, boxed)(defn.RetainsAnnot))
 
   /** An extractor for CapturingTypes. Capturing types are recognized if
@@ -84,4 +85,9 @@ object CapturingType:
 
 end CapturingType
 
+object CapturingOrRetainsType:
+   def unapply(tp: AnnotatedType)(using Context): Option[(Type, CaptureSet)] =
+    if ctx.mode.is(Mode.IgnoreCaptures) then None
+    else CapturingType.decomposeCapturingType(tp, alsoRetains = true)
+
 
diff --git a/compiler/src/dotty/tools/dotc/cc/ccConfig.scala b/compiler/src/dotty/tools/dotc/cc/ccConfig.scala
index fec13d9627fb..7836d7fd54a7 100644
--- a/compiler/src/dotty/tools/dotc/cc/ccConfig.scala
+++ b/compiler/src/dotty/tools/dotc/cc/ccConfig.scala
@@ -55,7 +55,7 @@ object ccConfig:
     Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.8`)
 
   /** Not used currently. Handy for trying out new features */
-  def newScheme(using Context): Boolean =
-    Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.7`)
+  def newScheme(using ctx: Context): Boolean =
+    ctx.settings.XdropComments.value
 
 end ccConfig
diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
index 3b4ad409efc2..c8b2d0ad7add 100644
--- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
@@ -17,6 +17,7 @@ import scala.annotation.switch
 import config.{Config, Feature}
 import ast.tpd
 import cc.*
+import CaptureSet.Mutability
 import Capabilities.*
 
 class PlainPrinter(_ctx: Context) extends Printer {
@@ -173,7 +174,9 @@ class PlainPrinter(_ctx: Context) extends Printer {
       val core: Text =
         if !cs.isConst && cs.elems.isEmpty then "?"
         else "{" ~ Text(cs.processElems(_.toList.map(toTextCapability)), ", ") ~ "}"
-           //     ~ Str("?").provided(!cs.isConst)
+           ~ Str(".reader").provided(ccVerbose && cs.mutability == Mutability.Reader)
+           ~ Str("?").provided(ccVerbose && !cs.isConst)
+           ~ Str(s"#${cs.asVar.id}").provided(showUniqueIds && !cs.isConst)
       core ~ cs.optionalInfo
 
   private def toTextRetainedElem(ref: Type): Text = ref match
diff --git a/tests/pos-custom-args/captures/matrix.scala b/tests/pos-custom-args/captures/matrix.scala
new file mode 100644
index 000000000000..89c2ca36380e
--- /dev/null
+++ b/tests/pos-custom-args/captures/matrix.scala
@@ -0,0 +1,37 @@
+import caps.Mutable
+import caps.cap
+import language.`3.7` // fails separation checking right now
+
+trait Rdr[T]:
+  def get: T
+
+class Ref[T](init: T) extends Rdr[T], Mutable:
+  private var current = init
+  def get: T = current
+  mut def put(x: T): Unit = current = x
+
+abstract class IMatrix:
+  def apply(i: Int, j: Int): Double
+
+class Matrix(nrows: Int, ncols: Int) extends IMatrix, Mutable:
+  val arr = Array.fill(nrows, ncols)(0.0)
+  def apply(i: Int, j: Int): Double = arr(i)(j)
+  mut def update(i: Int, j: Int, x: Double): Unit = arr(i)(j) = x
+
+
+def mul(x: Matrix, y: Matrix, z: Matrix^): Unit = ???
+def mul1(x: Matrix^{cap.rd}, y: Matrix^{cap.rd}, z: Matrix^): Unit = ???
+
+def Test(c: Object^): Unit =
+  val m1 = Matrix(10, 10)
+  val m2 = Matrix(10, 10)
+  mul(m1, m2, m2) // error: will fail separation checking
+  mul(m1, m1, m2) // should be ok
+
+  mul1(m1, m2, m2) // error: will fail separation checking
+  mul(m1, m1, m2) // should be ok
+
+  def f2(): Matrix^ = Matrix(10, 10)
+
+  val i1: IMatrix^{cap.rd} = m1
+  val i2: IMatrix^{cap.rd} = f2()

From 750c7f0ef96af44acac586897984d0aafbf8efb0 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Mon, 9 Jun 2025 10:30:29 +0200
Subject: [PATCH 11/14] Generalize read-only adaptation

 - Also adapt in type arguments, refinements, and function results
 - Also adapt to readonly if target is a mutable, read-only type
---
 .../src/dotty/tools/dotc/cc/CaptureSet.scala  | 10 ++-
 .../dotty/tools/dotc/cc/CheckCaptures.scala   | 82 +++++++++++++++++--
 tests/neg-custom-args/captures/matrix.check   | 32 ++++++++
 tests/neg-custom-args/captures/matrix.scala   | 36 ++++++++
 .../captures/ro-mut-conformance.check         | 14 ++++
 .../captures/ro-mut-conformance.scala         | 11 +++
 .../pos-custom-args/captures/deep-adapt.scala | 23 ++++++
 tests/pos-custom-args/captures/matrix.scala   |  4 -
 8 files changed, 195 insertions(+), 17 deletions(-)
 create mode 100644 tests/neg-custom-args/captures/matrix.check
 create mode 100644 tests/neg-custom-args/captures/matrix.scala
 create mode 100644 tests/neg-custom-args/captures/ro-mut-conformance.check
 create mode 100644 tests/neg-custom-args/captures/ro-mut-conformance.scala
 create mode 100644 tests/pos-custom-args/captures/deep-adapt.scala

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index 6a5f650440a3..7f258613fdac 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -136,6 +136,8 @@ sealed abstract class CaptureSet extends Showable:
   final def isReadOnly(using Context): Boolean =
     elems.forall(_.isReadOnly)
 
+  final def isAlwaysReadOnly(using Context): Boolean = isConst && isReadOnly
+
   final def isExclusive(using Context): Boolean =
     elems.exists(_.isExclusive)
 
@@ -1385,8 +1387,8 @@ object CaptureSet:
     def apply(t: Type) = mapOver(t)
 
     override def fuse(next: BiTypeMap)(using Context) = next match
-      case next: Inverse if next.inverse.getClass == getClass => assert(false); Some(IdentityTypeMap)
-      case next: NarrowingCapabilityMap if next.getClass == getClass => assert(false)
+      case next: Inverse if next.inverse.getClass == getClass => Some(IdentityTypeMap)
+      case next: NarrowingCapabilityMap if next.getClass == getClass => Some(this)
       case _ => None
 
     class Inverse extends BiTypeMap:
@@ -1395,8 +1397,8 @@ object CaptureSet:
       def inverse = NarrowingCapabilityMap.this
       override def toString = NarrowingCapabilityMap.this.toString ++ ".inverse"
       override def fuse(next: BiTypeMap)(using Context) = next match
-        case next: NarrowingCapabilityMap if next.inverse.getClass == getClass => assert(false); Some(IdentityTypeMap)
-        case next: NarrowingCapabilityMap if next.getClass == getClass => assert(false)
+        case next: NarrowingCapabilityMap if next.inverse.getClass == getClass => Some(IdentityTypeMap)
+        case next: NarrowingCapabilityMap if next.getClass == getClass => Some(this)
         case _ => None
 
     lazy val inverse = Inverse()
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index d3ae08e4559c..a80fe614aac1 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -1568,17 +1568,81 @@ class CheckCaptures extends Recheck, SymTransformer:
      *  to narrow to the read-only set, since that set can be propagated
      *  by the type variable instantiation.
      */
-    private def improveReadOnly(actual: Type, expected: Type)(using Context): Type = actual match
-      case actual @ CapturingType(parent, refs)
-      if parent.derivesFrom(defn.Caps_Mutable)
-          && expected.isValueType
-          && !expected.derivesFromMutable
-          && !expected.isSingleton
-          && !expected.isBoxedCapturing =>
-        actual.derivedCapturingType(parent, refs.readOnly)
-          .showing(i"improv ro $actual vs $expected = $result", capt)
+    private def improveReadOnly(actual: Type, expected: Type)(using Context): Type = reporting.trace(i"improv ro $actual vs $expected"):
+      actual.dealiasKeepAnnots match
+      case actual @ CapturingType(parent, refs) =>
+        val parent1 = improveReadOnly(parent, expected)
+        val refs1 =
+          if parent1.derivesFrom(defn.Caps_Mutable)
+              && expected.isValueType
+              && (!expected.derivesFromMutable || expected.captureSet.isAlwaysReadOnly)
+              && !expected.isSingleton
+              && actual.isBoxedCapturing == expected.isBoxedCapturing
+          then refs.readOnly
+          else refs
+        actual.derivedCapturingType(parent1, refs1)
+      case actual @ FunctionOrMethod(aargs, ares) =>
+        expected.dealias.stripCapturing match
+          case FunctionOrMethod(eargs, eres) =>
+            actual.derivedFunctionOrMethod(aargs, improveReadOnly(ares, eres))
+          case _ =>
+            actual
+      case actual @ AppliedType(atycon, aargs) =>
+        def improveArgs(aargs: List[Type], eargs: List[Type], formals: List[ParamInfo]): List[Type] =
+          aargs match
+            case aargs @ (aarg :: aargs1) =>
+              val aarg1 =
+                if formals.head.paramVariance.is(Covariant)
+                then improveReadOnly(aarg, eargs.head)
+                else aarg
+              aargs.derivedCons(aarg1, improveArgs(aargs1, eargs.tail, formals.tail))
+            case Nil =>
+              aargs
+        val expected1 = expected.dealias.stripCapturing
+        val esym = expected1.typeSymbol
+        expected1 match
+          case AppliedType(etycon, eargs) =>
+            if atycon.typeSymbol == esym then
+              actual.derivedAppliedType(atycon,
+                improveArgs(aargs, eargs, etycon.typeParams))
+            else if esym.isClass then
+              // This case is tricky: Try to lift actual to the base type with class `esym`,
+              // improve the resulting arguments, and figure out if anything can be
+              // deduced from that for the original arguments.
+              actual.baseType(esym) match
+                case base @ AppliedType(_, bargs) =>
+                  // If any of the base type arguments can be improved, check
+                  // whether they are the same as an original argument, and in this
+                  // case improve the original argument.
+                  val iargs = improveArgs(bargs, eargs, etycon.typeParams)
+                  if iargs ne bargs then
+                    val updates =
+                      for
+                        (barg, iarg) <- bargs.lazyZip(iargs)
+                        if barg ne iarg
+                        aarg <- aargs.find(_ eq barg)
+                      yield (aarg, iarg)
+                    if updates.nonEmpty then AppliedType(atycon, aargs.map(updates.toMap))
+                    else actual
+                  else actual
+                case _ => actual
+            else actual
+          case _ =>
+            actual
+      case actual @ RefinedType(aparent, aname, ainfo) =>
+        expected.dealias.stripCapturing match
+          case RefinedType(eparent, ename, einfo) if aname == ename =>
+            actual.derivedRefinedType(
+              improveReadOnly(aparent, eparent),
+              aname,
+              improveReadOnly(ainfo, einfo))
+          case _ =>
+            actual
+      case actual @ AnnotatedType(parent, ann) =>
+        actual.derivedAnnotatedType(improveReadOnly(parent, expected), ann)
       case _ =>
         actual
+    end improveReadOnly
 
     /* Currently not needed since it forms part of `adapt`
     private def improve(actual: Type, prefix: Type)(using Context): Type =
diff --git a/tests/neg-custom-args/captures/matrix.check b/tests/neg-custom-args/captures/matrix.check
new file mode 100644
index 000000000000..6a58b62dc2a3
--- /dev/null
+++ b/tests/neg-custom-args/captures/matrix.check
@@ -0,0 +1,32 @@
+-- Error: tests/neg-custom-args/captures/matrix.scala:27:10 ------------------------------------------------------------
+27 |  mul(m1, m2, m2) // error: will fail separation checking
+   |          ^^
+   |Separation failure: argument of type  Matrix^{m2.rd}
+   |to method mul: (x: Matrix^{cap.rd}, y: Matrix^{cap.rd}, z: Matrix^): Unit
+   |corresponds to capture-polymorphic formal parameter y of type  Matrix^{cap.rd}
+   |and hides capabilities  {m2.rd}.
+   |Some of these overlap with the captures of the third argument with type  (m2 : Matrix^).
+   |
+   |  Hidden set of current argument        : {m2.rd}
+   |  Hidden footprint of current argument  : {m2.rd}
+   |  Capture set of third argument         : {m2}
+   |  Footprint set of third argument       : {m2}
+   |  The two sets overlap at               : {m2}
+   |
+   |where:    cap is a fresh root capability created in method Test when checking argument to parameter y of method mul
+-- Error: tests/neg-custom-args/captures/matrix.scala:30:11 ------------------------------------------------------------
+30 |  mul1(m1, m2, m2) // error: will fail separation checking
+   |           ^^
+   |Separation failure: argument of type  Matrix^{m2.rd}
+   |to method mul1: (x: Matrix^{cap.rd}, y: Matrix^{cap.rd}, z: Matrix^): Unit
+   |corresponds to capture-polymorphic formal parameter y of type  Matrix^{cap.rd}
+   |and hides capabilities  {m2.rd}.
+   |Some of these overlap with the captures of the third argument with type  (m2 : Matrix^).
+   |
+   |  Hidden set of current argument        : {m2.rd}
+   |  Hidden footprint of current argument  : {m2.rd}
+   |  Capture set of third argument         : {m2}
+   |  Footprint set of third argument       : {m2}
+   |  The two sets overlap at               : {m2}
+   |
+   |where:    cap is a fresh root capability created in method Test when checking argument to parameter y of method mul1
diff --git a/tests/neg-custom-args/captures/matrix.scala b/tests/neg-custom-args/captures/matrix.scala
new file mode 100644
index 000000000000..a333d41a98dc
--- /dev/null
+++ b/tests/neg-custom-args/captures/matrix.scala
@@ -0,0 +1,36 @@
+import caps.Mutable
+import caps.cap
+
+trait Rdr[T]:
+  def get: T
+
+class Ref[T](init: T) extends Rdr[T], Mutable:
+  private var current = init
+  def get: T = current
+  mut def put(x: T): Unit = current = x
+
+abstract class IMatrix:
+  def apply(i: Int, j: Int): Double
+
+class Matrix(nrows: Int, ncols: Int) extends IMatrix, Mutable:
+  val arr = Array.fill(nrows, ncols)(0.0)
+  def apply(i: Int, j: Int): Double = arr(i)(j)
+  mut def update(i: Int, j: Int, x: Double): Unit = arr(i)(j) = x
+
+
+def mul(x: Matrix, y: Matrix, z: Matrix^): Unit = ???
+def mul1(x: Matrix^{cap.rd}, y: Matrix^{cap.rd}, z: Matrix^): Unit = ???
+
+def Test(c: Object^): Unit =
+  val m1 = Matrix(10, 10)
+  val m2 = Matrix(10, 10)
+  mul(m1, m2, m2) // error: will fail separation checking
+  mul(m1, m1, m2) // should be ok
+
+  mul1(m1, m2, m2) // error: will fail separation checking
+  mul(m1, m1, m2) // should be ok
+
+  def f2(): Matrix^ = Matrix(10, 10)
+
+  val i1: IMatrix^{cap.rd} = m1
+  val i2: IMatrix^{cap.rd} = f2()
diff --git a/tests/neg-custom-args/captures/ro-mut-conformance.check b/tests/neg-custom-args/captures/ro-mut-conformance.check
new file mode 100644
index 000000000000..4fc780ec8641
--- /dev/null
+++ b/tests/neg-custom-args/captures/ro-mut-conformance.check
@@ -0,0 +1,14 @@
+-- Error: tests/neg-custom-args/captures/ro-mut-conformance.scala:8:4 --------------------------------------------------
+8 |  a.set(42)  // error
+  |  ^^^^^
+  |  cannot call update method set from (a : Ref),
+  |  since its capture set {a} is read-only
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/ro-mut-conformance.scala:10:21 ---------------------------
+10 |  val t: Ref^{cap} = a  // error
+   |                     ^
+   |                     Found:    (a : Ref)
+   |                     Required: Ref^
+   |
+   |                     where:    ^ refers to a fresh root capability in the type of value t
+   |
+   | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/ro-mut-conformance.scala b/tests/neg-custom-args/captures/ro-mut-conformance.scala
new file mode 100644
index 000000000000..708aa4517504
--- /dev/null
+++ b/tests/neg-custom-args/captures/ro-mut-conformance.scala
@@ -0,0 +1,11 @@
+import language.experimental.captureChecking
+import caps.*
+class Ref extends Mutable:
+  private var _data: Int = 0
+  def get: Int = _data
+  mut def set(x: Int): Unit = _data = x
+def test1(a: Ref^{cap.rd}): Unit =
+  a.set(42)  // error
+def test2(a: Ref^{cap.rd}): Unit =
+  val t: Ref^{cap} = a  // error
+  t.set(42)
\ No newline at end of file
diff --git a/tests/pos-custom-args/captures/deep-adapt.scala b/tests/pos-custom-args/captures/deep-adapt.scala
new file mode 100644
index 000000000000..70dd0cc5d0dc
--- /dev/null
+++ b/tests/pos-custom-args/captures/deep-adapt.scala
@@ -0,0 +1,23 @@
+import caps.Mutable
+import caps.cap
+
+trait Rdr[T]:
+  def get: T
+
+class Ref[T](init: T) extends Rdr[T], Mutable:
+  private var current = init
+  def get: T = current
+  mut def put(x: T): Unit = current = x
+
+case class Pair[+A, +B](x: A, y: B)
+class Swap[+A, +B](x: A, y: B) extends Pair[B, A](y, x)
+
+def Test(c: Object^): Unit =
+  val refs = List(Ref(1), Ref(2))
+  val rdrs: List[Ref[Int]^{cap.rd}] = refs
+  val rdrs2: Seq[Ref[Int]^{cap.rd}] = refs
+
+  val swapped = Swap(Ref(1), Ref("hello"))
+  val _: Swap[Ref[Int]^{cap.rd}, Ref[String]^{cap.rd}] = swapped
+  val _: Pair[Ref[String]^{cap.rd}, Ref[Int]^{cap.rd}] @unchecked = swapped
+
diff --git a/tests/pos-custom-args/captures/matrix.scala b/tests/pos-custom-args/captures/matrix.scala
index 89c2ca36380e..8e7fb6663304 100644
--- a/tests/pos-custom-args/captures/matrix.scala
+++ b/tests/pos-custom-args/captures/matrix.scala
@@ -1,6 +1,5 @@
 import caps.Mutable
 import caps.cap
-import language.`3.7` // fails separation checking right now
 
 trait Rdr[T]:
   def get: T
@@ -25,10 +24,7 @@ def mul1(x: Matrix^{cap.rd}, y: Matrix^{cap.rd}, z: Matrix^): Unit = ???
 def Test(c: Object^): Unit =
   val m1 = Matrix(10, 10)
   val m2 = Matrix(10, 10)
-  mul(m1, m2, m2) // error: will fail separation checking
   mul(m1, m1, m2) // should be ok
-
-  mul1(m1, m2, m2) // error: will fail separation checking
   mul(m1, m1, m2) // should be ok
 
   def f2(): Matrix^ = Matrix(10, 10)

From 489f785408b83b7bad331457328fe551cab7d8aa Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Tue, 10 Jun 2025 12:29:51 +0200
Subject: [PATCH 12/14] Make capture-sets thread-safe again

---
 compiler/src/dotty/tools/dotc/cc/CaptureSet.scala | 14 ++++++++------
 compiler/src/dotty/tools/dotc/cc/Setup.scala      |  4 ++--
 2 files changed, 10 insertions(+), 8 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index 7f258613fdac..f7ed98471d10 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -512,17 +512,13 @@ object CaptureSet:
   val emptyRefs: Refs = SimpleIdentitySet.empty
 
   /** The empty capture set `{}` */
+  @sharable // sharable since the set is empty, so setMutable is a no-op
   val empty: CaptureSet.Const = Const(emptyRefs)
 
   /** The universal capture set `{cap}` */
   def universal(using Context): Const =
     Const(SimpleIdentitySet(GlobalCap))
 
-  /** The same as {cap.rd} but generated implicitly for
-   * references of Capability subtypes
-   */
-  val csImpliedByCapability = Const(SimpleIdentitySet(GlobalCap.readOnly))
-
   def fresh(origin: Origin)(using Context): Const =
     FreshCap(origin).singletonCaptureSet
 
@@ -572,7 +568,8 @@ object CaptureSet:
     private var isComplete = true
 
     def setMutable()(using Context): Unit =
-      isComplete = false // delay computation of Mutability status
+      if !elems.isEmpty then
+        isComplete = false // delay computation of Mutability status
 
     override def mutability(using Context): Mutability =
       if !isComplete then
@@ -589,12 +586,17 @@ object CaptureSet:
       then i" under-approximating the result of mapping $ref to $mapped"
       else ""
 
+  /* The same as {cap.rd} but generated implicitly for references of Capability subtypes.
+   */
+  case class CSImpliedByCapability() extends Const(SimpleIdentitySet(GlobalCap.readOnly))
+
   /** 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
    *  sets in subcapturing comparisons. Similar to platform types for explicit
    *  nulls, this provides more lenient checking against compilation units that
    *  were not yet compiled with capture checking on.
    */
+  @sharable // sharable since the set is empty, so setMutable is a no-op
   object Fluid extends Const(emptyRefs):
     override def isAlwaysEmpty(using Context) = false
     override def addThisElem(elem: Capability)(using Context, VarState) = true
diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala
index de79eab11834..51ff6948a947 100644
--- a/compiler/src/dotty/tools/dotc/cc/Setup.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -367,7 +367,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
      */
     def stripImpliedCaptureSet(tp: Type): Type = tp match
       case tp @ CapturingType(parent, refs)
-      if (refs eq CaptureSet.csImpliedByCapability) && !tp.isBoxedCapturing =>
+      if refs.isInstanceOf[CaptureSet.CSImpliedByCapability] && !tp.isBoxedCapturing =>
         parent
       case tp: AliasingBounds =>
         tp.derivedAlias(stripImpliedCaptureSet(tp.alias))
@@ -430,7 +430,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
           && !t.isSingleton
           && (!sym.isConstructor || (t ne tp.finalResultType))
             // Don't add ^ to result types of class constructors deriving from Capability
-        then CapturingType(t, CaptureSet.csImpliedByCapability, boxed = false)
+        then CapturingType(t, CaptureSet.CSImpliedByCapability(), boxed = false)
         else normalizeCaptures(mapFollowingAliases(t))
 
       def innerApply(t: Type) =

From cdc9cf41b364ef2991140bb7a7e6ba4c5541e2cf Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Tue, 10 Jun 2025 15:57:19 +0200
Subject: [PATCH 13/14] Adapt to mut->update renames

---
 tests/neg-custom-args/captures/matrix.scala             | 4 ++--
 tests/neg-custom-args/captures/ro-mut-conformance.scala | 2 +-
 tests/neg-custom-args/captures/sep-curried-redux.scala  | 2 +-
 tests/pos-custom-args/captures/deep-adapt.scala         | 2 +-
 tests/pos-custom-args/captures/matrix.scala             | 4 ++--
 5 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/tests/neg-custom-args/captures/matrix.scala b/tests/neg-custom-args/captures/matrix.scala
index a333d41a98dc..e473da7edc70 100644
--- a/tests/neg-custom-args/captures/matrix.scala
+++ b/tests/neg-custom-args/captures/matrix.scala
@@ -7,7 +7,7 @@ trait Rdr[T]:
 class Ref[T](init: T) extends Rdr[T], Mutable:
   private var current = init
   def get: T = current
-  mut def put(x: T): Unit = current = x
+  update def put(x: T): Unit = current = x
 
 abstract class IMatrix:
   def apply(i: Int, j: Int): Double
@@ -15,7 +15,7 @@ abstract class IMatrix:
 class Matrix(nrows: Int, ncols: Int) extends IMatrix, Mutable:
   val arr = Array.fill(nrows, ncols)(0.0)
   def apply(i: Int, j: Int): Double = arr(i)(j)
-  mut def update(i: Int, j: Int, x: Double): Unit = arr(i)(j) = x
+  update def update(i: Int, j: Int, x: Double): Unit = arr(i)(j) = x
 
 
 def mul(x: Matrix, y: Matrix, z: Matrix^): Unit = ???
diff --git a/tests/neg-custom-args/captures/ro-mut-conformance.scala b/tests/neg-custom-args/captures/ro-mut-conformance.scala
index 708aa4517504..0aecbb2b972e 100644
--- a/tests/neg-custom-args/captures/ro-mut-conformance.scala
+++ b/tests/neg-custom-args/captures/ro-mut-conformance.scala
@@ -3,7 +3,7 @@ import caps.*
 class Ref extends Mutable:
   private var _data: Int = 0
   def get: Int = _data
-  mut def set(x: Int): Unit = _data = x
+  update def set(x: Int): Unit = _data = x
 def test1(a: Ref^{cap.rd}): Unit =
   a.set(42)  // error
 def test2(a: Ref^{cap.rd}): Unit =
diff --git a/tests/neg-custom-args/captures/sep-curried-redux.scala b/tests/neg-custom-args/captures/sep-curried-redux.scala
index 31b349b09f94..a34164b106f1 100644
--- a/tests/neg-custom-args/captures/sep-curried-redux.scala
+++ b/tests/neg-custom-args/captures/sep-curried-redux.scala
@@ -4,7 +4,7 @@ import caps.*
 class Ref[T](init: T) extends Mutable:
   private var value: T = init
   def get: T = value
-  mut def set(newValue: T): Unit = value = newValue
+  update def set(newValue: T): Unit = value = newValue
 
 // a library function that assumes that a and b MUST BE separate
 def swap[T](a: Ref[Int]^, b: Ref[Int]^): Unit = ???
diff --git a/tests/pos-custom-args/captures/deep-adapt.scala b/tests/pos-custom-args/captures/deep-adapt.scala
index 70dd0cc5d0dc..2a27763f53fa 100644
--- a/tests/pos-custom-args/captures/deep-adapt.scala
+++ b/tests/pos-custom-args/captures/deep-adapt.scala
@@ -7,7 +7,7 @@ trait Rdr[T]:
 class Ref[T](init: T) extends Rdr[T], Mutable:
   private var current = init
   def get: T = current
-  mut def put(x: T): Unit = current = x
+  update def put(x: T): Unit = current = x
 
 case class Pair[+A, +B](x: A, y: B)
 class Swap[+A, +B](x: A, y: B) extends Pair[B, A](y, x)
diff --git a/tests/pos-custom-args/captures/matrix.scala b/tests/pos-custom-args/captures/matrix.scala
index 8e7fb6663304..11c314fa6e51 100644
--- a/tests/pos-custom-args/captures/matrix.scala
+++ b/tests/pos-custom-args/captures/matrix.scala
@@ -7,7 +7,7 @@ trait Rdr[T]:
 class Ref[T](init: T) extends Rdr[T], Mutable:
   private var current = init
   def get: T = current
-  mut def put(x: T): Unit = current = x
+  update def put(x: T): Unit = current = x
 
 abstract class IMatrix:
   def apply(i: Int, j: Int): Double
@@ -15,7 +15,7 @@ abstract class IMatrix:
 class Matrix(nrows: Int, ncols: Int) extends IMatrix, Mutable:
   val arr = Array.fill(nrows, ncols)(0.0)
   def apply(i: Int, j: Int): Double = arr(i)(j)
-  mut def update(i: Int, j: Int, x: Double): Unit = arr(i)(j) = x
+  update def update(i: Int, j: Int, x: Double): Unit = arr(i)(j) = x
 
 
 def mul(x: Matrix, y: Matrix, z: Matrix^): Unit = ???

From 0c9e2241826b62cbb3d6f4ab884083c4159ec95c Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Wed, 11 Jun 2025 09:37:33 +0200
Subject: [PATCH 14/14] Improve error message for failures of mutable capture
 sets

---
 compiler/src/dotty/tools/dotc/cc/CaptureSet.scala   | 13 +++++++++++--
 .../src/dotty/tools/dotc/cc/CheckCaptures.scala     |  7 ++++++-
 .../src/dotty/tools/dotc/core/TypeComparer.scala    |  8 +++++++-
 .../captures/ro-mut-conformance.check               |  3 +++
 4 files changed, 27 insertions(+), 4 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index f7ed98471d10..6684c6615bc8 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -553,7 +553,7 @@ object CaptureSet:
         false
       }
 
-    def toReader()(using Context) = false
+    def toReader()(using Context) = failWith(MutAdaptFailure(this))
 
     def addDependent(cs: CaptureSet)(using Context, VarState) = true
 
@@ -721,7 +721,7 @@ object CaptureSet:
         res
 
     final def toReader()(using Context) =
-      if isConst then false // TODO add error note when failing?
+      if isConst then failWith(MutAdaptFailure(this))
       else
         mutability = Reader
         TypeComparer.logUndoAction(() => mutability = Mutable)
@@ -1205,6 +1205,7 @@ object CaptureSet:
    */
   case class ExistentialSubsumesFailure(val ex: ResultCap, val other: Capability) extends ErrorNote
 
+  /** Failure indicating that `elem` cannot be included in `cs` */
   case class IncludeFailure(cs: CaptureSet, elem: Capability, levelError: Boolean = false) extends ErrorNote, Showable:
     private var myTrace: List[CaptureSet] = cs :: Nil
 
@@ -1224,6 +1225,14 @@ object CaptureSet:
           else i"$elem cannot be included in $cs"
   end IncludeFailure
 
+  /** Failure indicating that a read-only capture set of a mutable type cannot be
+   *  widened to an exclusive set.
+   *  @param  cs    the exclusive set in question
+   *  @param  lo    the lower type of the orginal type comparison, or NoType if not known
+   *  @param  hi    the upper type of the orginal type comparison, or NoType if not known
+   */
+  case class MutAdaptFailure(cs: CaptureSet, lo: Type = NoType, hi: Type = NoType) extends ErrorNote
+
   /** A VarState serves as a snapshot mechanism that can undo
    *  additions of elements or super sets if an operation fails
    */
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index a80fe614aac1..4d3cfc698a61 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -25,6 +25,7 @@ import NameKinds.{DefaultGetterName, WildcardParamName, UniqueNameKind}
 import reporting.{trace, Message, OverrideError}
 import Annotations.Annotation
 import Capabilities.*
+import dotty.tools.dotc.cc.CaptureSet.MutAdaptFailure
 
 /** The capture checker */
 object CheckCaptures:
@@ -1265,7 +1266,7 @@ class CheckCaptures extends Recheck, SymTransformer:
     private def errorNotes(notes: List[TypeComparer.ErrorNote])(using Context): Addenda =
       val printableNotes = notes.filter:
         case IncludeFailure(_, _, true) => true
-        case _: ExistentialSubsumesFailure => true
+        case _: ExistentialSubsumesFailure | _: MutAdaptFailure => true
         case _ => false
       if printableNotes.isEmpty then NothingToAdd
       else new Addenda:
@@ -1287,6 +1288,10 @@ class CheckCaptures extends Recheck, SymTransformer:
                 else " since that capability is not a SharedCapability"
               i"""the existential capture root in ${ex.originalBinder.resType}
                  |cannot subsume the capability $other$since"""
+            case MutAdaptFailure(cs, lo, hi) =>
+              def ofType(tp: Type) = if tp.exists then i"of the mutable type $tp" else "of a mutable type"
+              i"""$cs is an exclusive capture set ${ofType(hi)},
+                 |it cannot subsume a read-only capture set ${ofType(lo)}."""
           i"""
              |Note that ${msg.toString}"""
 
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 2dc96a53d3f7..97a32e66f30e 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -2902,7 +2902,13 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
       if tp1.derivesFromMutable && !tp2.derivesFromMutable
       then refs1.readOnly
       else refs1
-    subCaptures(refs1Adapted, refs2)
+    val subc = subCaptures(refs1Adapted, refs2)
+    if !subc then
+      errorNotes match
+        case (level, CaptureSet.MutAdaptFailure(cs, NoType, NoType)) :: rest =>
+          errorNotes = (level, CaptureSet.MutAdaptFailure(cs, tp1, tp2)) :: rest
+        case _ =>
+    subc
     && (tp1.isBoxedCapturing == tp2.isBoxedCapturing)
         || refs1.subCaptures(CaptureSet.empty, makeVarState())
 
diff --git a/tests/neg-custom-args/captures/ro-mut-conformance.check b/tests/neg-custom-args/captures/ro-mut-conformance.check
index 4fc780ec8641..0a3fe9f0318b 100644
--- a/tests/neg-custom-args/captures/ro-mut-conformance.check
+++ b/tests/neg-custom-args/captures/ro-mut-conformance.check
@@ -11,4 +11,7 @@
    |
    |                     where:    ^ refers to a fresh root capability in the type of value t
    |
+   |                     Note that {cap} is an exclusive capture set of the mutable type Ref^,
+   |                     it cannot subsume a read-only capture set of the mutable type (a : Ref).
+   |
    | longer explanation available when compiling with `-explain`