From de1c3b7e020a441697140729d4cb4cf0e1dc0ebd Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Thu, 4 Sep 2025 11:25:51 +0200
Subject: [PATCH 01/12] Fixes to capture annotations in stdlib

These problems were discovered once we started recording uses of this references.
The recording is not yet part of this commit because it requires downstream bugfixes
in the compiler.
---
 library/src/scala/collection/Iterator.scala          | 12 ++++++------
 library/src/scala/collection/LazyZipOps.scala        |  2 +-
 library/src/scala/collection/SeqView.scala           |  4 ++--
 library/src/scala/collection/Stepper.scala           |  6 +++---
 library/src/scala/collection/View.scala              |  4 ++--
 .../scala/collection/convert/StreamExtensions.scala  |  1 +
 library/src/scala/collection/mutable/HashTable.scala |  2 +-
 .../captures/colltest5/CollectionStrawManCC5_1.scala |  2 +-
 8 files changed, 17 insertions(+), 16 deletions(-)

diff --git a/library/src/scala/collection/Iterator.scala b/library/src/scala/collection/Iterator.scala
index 6a6132990f76..2b8b9d45d6e4 100644
--- a/library/src/scala/collection/Iterator.scala
+++ b/library/src/scala/collection/Iterator.scala
@@ -418,7 +418,7 @@ trait Iterator[+A] extends IterableOnce[A] with IterableOnceOps[A, Iterator, Ite
 
   @deprecated("Call scanRight on an Iterable instead.", "2.13.0")
   def scanRight[B](z: B)(op: (A, B) => B): Iterator[B]^{this, op} = ArrayBuffer.from(this).scanRight(z)(op).iterator
- 
+
   /** Finds index of the first element satisfying some predicate after or at some start index.
     *
     *  $mayNotTerminateInf
@@ -494,9 +494,9 @@ trait Iterator[+A] extends IterableOnce[A] with IterableOnceOps[A, Iterator, Ite
       while (p(hd) == isFlipped) {
         if (!self.hasNext) return false
         hd = self.next()
-      } 
+      }
       hdDefined = true
-      true 
+      true
     }
 
     def next() =
@@ -874,7 +874,7 @@ trait Iterator[+A] extends IterableOnce[A] with IterableOnceOps[A, Iterator, Ite
     */
   def duplicate: (Iterator[A]^{this}, Iterator[A]^{this}) = {
     val gap = new scala.collection.mutable.Queue[A]
-    var ahead: Iterator[A] = null
+    var ahead: Iterator[A]^ = null
     class Partner extends AbstractIterator[A] {
       override def knownSize: Int = self.synchronized {
         val thisSize = self.knownSize
@@ -890,7 +890,7 @@ trait Iterator[+A] extends IterableOnce[A] with IterableOnceOps[A, Iterator, Ite
         if (gap.isEmpty) ahead = this
         if (this eq ahead) {
           val e = self.next()
-          gap enqueue e
+          gap.enqueue(e)
           e
         } else gap.dequeue()
       }
@@ -918,7 +918,7 @@ trait Iterator[+A] extends IterableOnce[A] with IterableOnceOps[A, Iterator, Ite
     */
   def patch[B >: A](from: Int, patchElems: Iterator[B]^, replaced: Int): Iterator[B]^{this, patchElems} =
     new AbstractIterator[B] {
-      private[this] var origElems = self
+      private[this] var origElems: Iterator[B]^ = self
       // > 0  => that many more elems from `origElems` before switching to `patchElems`
       //   0  => need to drop elems from `origElems` and start using `patchElems`
       //  -1  => have dropped elems from `origElems`, will be using `patchElems` until it's empty
diff --git a/library/src/scala/collection/LazyZipOps.scala b/library/src/scala/collection/LazyZipOps.scala
index 9a7dc3173926..5849de61448b 100644
--- a/library/src/scala/collection/LazyZipOps.scala
+++ b/library/src/scala/collection/LazyZipOps.scala
@@ -389,7 +389,7 @@ final class LazyZip4[+El1, +El2, +El3, +El4, C1] private[collection](src: C1,
   }
 
   private def toIterable: View[(El1, El2, El3, El4)]^{this} = new AbstractView[(El1, El2, El3, El4)] {
-    def iterator: AbstractIterator[(El1, El2, El3, El4)] = new AbstractIterator[(El1, El2, El3, El4)] {
+    def iterator: AbstractIterator[(El1, El2, El3, El4)]^{this} = new AbstractIterator[(El1, El2, El3, El4)] {
       private[this] val elems1 = coll1.iterator
       private[this] val elems2 = coll2.iterator
       private[this] val elems3 = coll3.iterator
diff --git a/library/src/scala/collection/SeqView.scala b/library/src/scala/collection/SeqView.scala
index 960de6f1d752..3928a20aef70 100644
--- a/library/src/scala/collection/SeqView.scala
+++ b/library/src/scala/collection/SeqView.scala
@@ -202,10 +202,10 @@ object SeqView {
     override def knownSize: Int = len
     override def isEmpty: Boolean = len == 0
     override def to[C1](factory: Factory[A, C1]): C1 = _sorted.to(factory)
-    override def reverse: SeqView[A] = new ReverseSorted
+    override def reverse: SeqView[A]^{this} = new ReverseSorted
     // we know `_sorted` is either tiny or has efficient random access,
     //  so this is acceptable for `reversed`
-    override protected def reversed: Iterable[A] = new ReverseSorted
+    override protected def reversed: Iterable[A]^{this} = new ReverseSorted
 
     override def sorted[B1 >: A](implicit ord1: Ordering[B1]): SeqView[A]^{this} =
       if (ord1 == this.ord) this
diff --git a/library/src/scala/collection/Stepper.scala b/library/src/scala/collection/Stepper.scala
index 7c4b5821aef9..7685c2304c7c 100644
--- a/library/src/scala/collection/Stepper.scala
+++ b/library/src/scala/collection/Stepper.scala
@@ -260,7 +260,7 @@ trait IntStepper extends Stepper[Int] {
 
   def spliterator[B >: Int]: Spliterator.OfInt^{this} = new IntStepper.IntStepperSpliterator(this)
 
-  def javaIterator[B >: Int]: PrimitiveIterator.OfInt = new PrimitiveIterator.OfInt {
+  def javaIterator[B >: Int]: PrimitiveIterator.OfInt^{this} = new PrimitiveIterator.OfInt {
     def hasNext: Boolean = hasStep
     def nextInt(): Int = nextStep()
   }
@@ -298,7 +298,7 @@ trait DoubleStepper extends Stepper[Double] {
 
   def spliterator[B >: Double]: Spliterator.OfDouble^{this} = new DoubleStepper.DoubleStepperSpliterator(this)
 
-  def javaIterator[B >: Double]: PrimitiveIterator.OfDouble = new PrimitiveIterator.OfDouble {
+  def javaIterator[B >: Double]: PrimitiveIterator.OfDouble^{this} = new PrimitiveIterator.OfDouble {
     def hasNext: Boolean = hasStep
     def nextDouble(): Double = nextStep()
   }
@@ -337,7 +337,7 @@ trait LongStepper extends Stepper[Long] {
 
   def spliterator[B >: Long]: Spliterator.OfLong^{this} = new LongStepper.LongStepperSpliterator(this)
 
-  def javaIterator[B >: Long]: PrimitiveIterator.OfLong = new PrimitiveIterator.OfLong {
+  def javaIterator[B >: Long]: PrimitiveIterator.OfLong^{this} = new PrimitiveIterator.OfLong {
     def hasNext: Boolean = hasStep
     def nextLong(): Long = nextStep()
   }
diff --git a/library/src/scala/collection/View.scala b/library/src/scala/collection/View.scala
index 6b862aece4ea..78a3f49b1f24 100644
--- a/library/src/scala/collection/View.scala
+++ b/library/src/scala/collection/View.scala
@@ -172,7 +172,7 @@ object View extends IterableFactory[View] {
 
   @SerialVersionUID(3L)
   class LeftPartitionMapped[A, A1, A2](underlying: SomeIterableOps[A]^, f: A => Either[A1, A2]) extends AbstractView[A1] {
-    def iterator: AbstractIterator[A1] = new AbstractIterator[A1] {
+    def iterator: AbstractIterator[A1]^{this} = new AbstractIterator[A1] {
       private[this] val self = underlying.iterator
       private[this] var hd: A1 = _
       private[this] var hdDefined: Boolean = false
@@ -197,7 +197,7 @@ object View extends IterableFactory[View] {
 
   @SerialVersionUID(3L)
   class RightPartitionMapped[A, A1, A2](underlying: SomeIterableOps[A]^, f: A => Either[A1, A2]) extends AbstractView[A2] {
-      def iterator: AbstractIterator[A2] = new AbstractIterator[A2] {
+      def iterator: AbstractIterator[A2]^{this} = new AbstractIterator[A2] {
         private[this] val self = underlying.iterator
         private[this] var hd: A2 = _
         private[this] var hdDefined: Boolean = false
diff --git a/library/src/scala/collection/convert/StreamExtensions.scala b/library/src/scala/collection/convert/StreamExtensions.scala
index 5e70ed1b4fd0..28b762b425f0 100644
--- a/library/src/scala/collection/convert/StreamExtensions.scala
+++ b/library/src/scala/collection/convert/StreamExtensions.scala
@@ -30,6 +30,7 @@ import scala.jdk._
   * [[scala.jdk.javaapi.StreamConverters]].
   */
 trait StreamExtensions {
+  this: StreamExtensions =>
   // collections
 
   implicit class IterableHasSeqStream[A](cc: IterableOnce[A]) {
diff --git a/library/src/scala/collection/mutable/HashTable.scala b/library/src/scala/collection/mutable/HashTable.scala
index 738adce7dfaa..5d0d1f35bdca 100644
--- a/library/src/scala/collection/mutable/HashTable.scala
+++ b/library/src/scala/collection/mutable/HashTable.scala
@@ -211,7 +211,7 @@ private[collection] trait HashTable[A, B, Entry >: Null <: HashEntry[A, Entry]]
 
   /** An iterator returning all entries.
    */
-  def entriesIterator: Iterator[Entry] = new AbstractIterator[Entry] {
+  def entriesIterator: Iterator[Entry]^{this} = new AbstractIterator[Entry] {
     val iterTable = table
     var idx       = lastPopulatedIndex
     var es        = iterTable(idx)
diff --git a/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala b/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala
index ea0bdc240e0c..1143cdb30d5e 100644
--- a/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala
+++ b/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala
@@ -423,7 +423,7 @@ object CollectionStrawMan5 {
     def start: Int
     def end: Int
     def apply(i: Int): A
-    def iterator: Iterator[A] = new Iterator[A] {
+    def iterator: Iterator[A]^{this} = new Iterator[A] {
       private var current = start
       def hasNext = current < end
       def next(): A = {

From a4e1546a8c8f01efd2a2c5c7c827f1602f65b99c Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Thu, 4 Sep 2025 11:38:13 +0200
Subject: [PATCH 02/12] Check use sets of non-static inner classes

These fell through the cracks before since we only considered named outer refs.
But inner classes can have outer this references check needd to be tracked in
use sets.
---
 compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 74c243a20684..a4ff27f29466 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -407,12 +407,12 @@ class CheckCaptures extends Recheck, SymTransformer:
           else i"references $cs1$cs1description are not all",
           cs1, cs2, pos, provenance)
 
-    /** If `sym` is a class or method nested inside a term, a capture set variable representing
-     *  the captured variables of the environment associated with `sym`.
+    /** If `sym` is a method or a non-static inner class, a capture set variable
+     *  representing the captured variables of the environment associated with `sym`.
      */
     def capturedVars(sym: Symbol)(using Context): CaptureSet =
       myCapturedVars.getOrElseUpdate(sym,
-        if sym.ownersIterator.exists(_.isTerm)
+        if sym.isTerm || !sym.owner.isStaticOwner
         then CaptureSet.Var(sym.owner, level = ccState.symLevel(sym))
         else CaptureSet.empty)
 

From 182a26ab156f728abb1660650437c33e6e701b21 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Thu, 4 Sep 2025 11:44:30 +0200
Subject: [PATCH 03/12] markFree of a constructor should never continue with
 the enclosing class

Previously there was a boundary condition where this could be the case for outermost
classes.
---
 .../src/dotty/tools/dotc/cc/CheckCaptures.scala   | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index a4ff27f29466..8823b302f290 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -420,12 +420,9 @@ class CheckCaptures extends Recheck, SymTransformer:
 
     /** The next environment enclosing `env` that needs to be charged
      *  with free references.
-     *  @param included Whether an environment is included in the range of
-     *                  environments to charge. Once `included` is false, no
-     *                  more environments need to be charged.
      */
-    def nextEnvToCharge(env: Env, included: Env => Boolean)(using Context): Env =
-      if env.owner.isConstructor && included(env.outer) then env.outer.outer
+    def nextEnvToCharge(env: Env)(using Context): Env | Null =
+      if env.owner.isConstructor then env.outer.outer0
       else env.outer
 
     /** A description where this environment comes from */
@@ -535,7 +532,9 @@ class CheckCaptures extends Recheck, SymTransformer:
           checkSubset(included, env.captured, tree.srcPos, provenance(env))
           capt.println(i"Include call or box capture $included from $cs in ${env.owner} --> ${env.captured}")
           if !isOfNestedMethod(env) then
-            recur(included, nextEnvToCharge(env, !_.owner.isStaticOwner), env)
+            val nextEnv = nextEnvToCharge(env)
+            if nextEnv != null && !nextEnv.owner.isStaticOwner then
+              recur(included, nextEnv, env)
           	// Under deferredReaches, don't propagate out of methods inside terms.
           	// The use set of these methods will be charged when that method is called.
 
@@ -2021,7 +2020,9 @@ class CheckCaptures extends Recheck, SymTransformer:
           if env.kind == EnvKind.Boxed then env.owner
           else if isOfNestedMethod(env) then env.owner.owner
           else if env.owner.isStaticOwner then NoSymbol
-          else boxedOwner(nextEnvToCharge(env, alwaysTrue))
+          else
+            val nextEnv = nextEnvToCharge(env)
+            if nextEnv == null then NoSymbol else boxedOwner(nextEnv)
 
         def checkUseUnlessBoxed(c: Capability, croot: NamedType) =
           if !boxedOwner(env).isContainedIn(croot.symbol.owner) then

From d71358f21b720189bdc4a891e763d4d2e61fe2e9 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Thu, 4 Sep 2025 11:49:22 +0200
Subject: [PATCH 04/12] Don't include use sets of class constructors in use
 sets of enclosing classes

---
 compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala | 2 +-
 tests/neg-custom-args/captures/real-try.check        | 2 +-
 tests/neg-custom-args/captures/unsound-reach-4.check | 2 +-
 tests/neg-custom-args/captures/unsound-reach.check   | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 8823b302f290..f35381a75bf0 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -865,7 +865,7 @@ class CheckCaptures extends Recheck, SymTransformer:
           val (refined, cs) = addParamArgRefinements(core, initCs)
           refined.capturing(cs)
 
-      augmentConstructorType(resType, capturedVars(cls) ++ capturedVars(constr))
+      augmentConstructorType(resType, capturedVars(cls))
         .showing(i"constr type $mt with $argTypes%, % in $constr = $result", capt)
     end refineConstructorInstance
 
diff --git a/tests/neg-custom-args/captures/real-try.check b/tests/neg-custom-args/captures/real-try.check
index bca841e11094..3fde3af88fd9 100644
--- a/tests/neg-custom-args/captures/real-try.check
+++ b/tests/neg-custom-args/captures/real-try.check
@@ -43,7 +43,7 @@
 -- Error: tests/neg-custom-args/captures/real-try.scala:32:10 ----------------------------------------------------------
 32 |  val b = try // error
    |          ^
-   |   The result of `try` cannot have type Cell[() => Unit]^'s2 since
+   |   The result of `try` cannot have type Cell[() => Unit] since
    |   the part () => Unit of that type captures the root capability `cap`.
    |   This is often caused by a locally generated exception capability leaking as part of its result.
    |
diff --git a/tests/neg-custom-args/captures/unsound-reach-4.check b/tests/neg-custom-args/captures/unsound-reach-4.check
index 573e9a31d068..cddcc58e38b4 100644
--- a/tests/neg-custom-args/captures/unsound-reach-4.check
+++ b/tests/neg-custom-args/captures/unsound-reach-4.check
@@ -8,7 +8,7 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/unsound-reach-4.scala:20:29 ------------------------------
 20 |  val backdoor: Foo[File^] = new Bar // error (follow-on, since the parent Foo[File^] of bar is illegal).
    |                             ^^^^^^^
-   |                             Found:    Bar^'s1
+   |                             Found:    Bar
    |                             Required: Foo[File^]
    |
    |                             Note that capability cap is not included in capture set {cap²}
diff --git a/tests/neg-custom-args/captures/unsound-reach.check b/tests/neg-custom-args/captures/unsound-reach.check
index 7f713586b6ec..0313ebe37b88 100644
--- a/tests/neg-custom-args/captures/unsound-reach.check
+++ b/tests/neg-custom-args/captures/unsound-reach.check
@@ -15,7 +15,7 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/unsound-reach.scala:18:31 --------------------------------
 18 |    val backdoor: Foo[File^] = new Bar   // error (follow-on, since the parent Foo[File^] of bar is illegal).
    |                               ^^^^^^^
-   |                               Found:    Bar^'s1
+   |                               Found:    Bar
    |                               Required: Foo[File^]
    |
    |                               Note that capability cap is not included in capture set {cap²}

From 668ceb1c691db93ccaaf27a2df0a49ff44b98bc1 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Thu, 4 Sep 2025 11:53:02 +0200
Subject: [PATCH 05/12] Don't assume `this` is visible in constructors

A constructor should never capture `this`, the object it constructs.
---
 compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index f35381a75bf0..c5f3353e2366 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -466,10 +466,13 @@ class CheckCaptures extends Recheck, SymTransformer:
       // if `sym` is not defined inside the owner of the environment.
       inline def isVisibleFromEnv(sym: Symbol, env: Env) =
         sym.exists && {
+          val effectiveOwner =
+            if env.owner.isConstructor then env.owner.owner
+            else env.owner
           if env.kind == EnvKind.NestedInOwner then
-            !sym.isProperlyContainedIn(env.owner)
+            !sym.isProperlyContainedIn(effectiveOwner)
           else
-            !sym.isContainedIn(env.owner)
+            !sym.isContainedIn(effectiveOwner)
         }
 
       /** Avoid locally defined capability by charging the underlying type

From 137d3b91ba583f0bf02a6aaefc102adb0d6199ee Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Thu, 4 Sep 2025 12:17:57 +0200
Subject: [PATCH 06/12] Record uses of this

Was shockingly missing before.
---
 .../dotty/tools/dotc/cc/CheckCaptures.scala   | 47 ++++++++++++-------
 .../dotty/tools/dotc/transform/Recheck.scala  | 10 +++-
 .../neg-custom-args/captures/class-caps.check | 22 +++++++++
 .../neg-custom-args/captures/class-caps.scala | 39 +++++++++++++++
 .../captures/constr-uses.scala                | 13 +++++
 .../captures/nested-classes.scala             |  1 +
 .../captures/secondary-constructors.scala     | 13 +++++
 7 files changed, 126 insertions(+), 19 deletions(-)
 create mode 100644 tests/neg-custom-args/captures/class-caps.check
 create mode 100644 tests/neg-custom-args/captures/class-caps.scala
 create mode 100644 tests/pos-custom-args/captures/constr-uses.scala
 create mode 100644 tests/pos-custom-args/captures/secondary-constructors.scala

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index c5f3353e2366..5942f5874712 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -455,7 +455,10 @@ class CheckCaptures extends Recheck, SymTransformer:
       markFree(sym, sym.termRef, tree)
 
     def markFree(sym: Symbol, ref: Capability, tree: Tree)(using Context): Unit =
-      if sym.exists && ref.isTracked then markFree(ref.singletonCaptureSet, tree)
+      if sym.exists then markFree(ref, tree)
+
+    def markFree(ref: Capability, tree: Tree)(using Context): Unit =
+      if ref.isTracked then markFree(ref.singletonCaptureSet, tree)
 
     /** Make sure the (projected) `cs` is a subset of the capture sets of all enclosing
      *  environments. At each stage, only include references from `cs` that are outside
@@ -628,25 +631,33 @@ class CheckCaptures extends Recheck, SymTransformer:
         // If ident refers to a parameterless method, charge its cv to the environment
         includeCallCaptures(sym, sym.info, tree)
       else if !sym.isStatic then
-        // Otherwise charge its symbol, but add all selections and also any `.rd`
-        // modifier implied by the expected type `pt`.
-        // Example: If we have `x` and the expected type says we select that with `.a.b`
-        // where `b` is a read-only method, we charge `x.a.b.rd` instead of `x`.
-        def addSelects(ref: TermRef, pt: Type): Capability = pt match
-          case pt: PathSelectionProto if ref.isTracked =>
-            if pt.sym.isReadOnlyMethod then
-              ref.readOnly
-            else
-              // if `ref` is not tracked then the selection could not give anything new
-              // class SerializationProxy in stdlib-cc/../LazyListIterable.scala has an example where this matters.
-              addSelects(ref.select(pt.sym).asInstanceOf[TermRef], pt.pt)
-          case _ => ref
-        var pathRef: Capability = addSelects(sym.termRef, pt)
-        if pathRef.derivesFromMutable && pt.isValueType && !pt.isMutableType then
-          pathRef = pathRef.readOnly
-        markFree(sym, pathRef, tree)
+        markFree(sym, pathRef(sym.termRef, pt), tree)
       mapResultRoots(super.recheckIdent(tree, pt), tree.symbol)
 
+    override def recheckThis(tree: This, pt: Type)(using Context): Type =
+      markFree(pathRef(tree.tpe.asInstanceOf[ThisType], pt), tree)
+      super.recheckThis(tree, pt)
+
+    /** Add all selections and also any `.rd modifier implied by the expected
+     *  type `pt` to `base`. Example:
+     *  If we have `x` and the expected type says we select that with `.a.b`
+     *  where `b` is a read-only method, we charge `x.a.b.rd` instead of `x`.
+     */
+    private def pathRef(base: TermRef | ThisType, pt: Type)(using Context): Capability =
+      def addSelects(ref: TermRef | ThisType, pt: Type): Capability = pt match
+        case pt: PathSelectionProto if ref.isTracked =>
+          if pt.sym.isReadOnlyMethod then
+            ref.readOnly
+          else
+            // if `ref` is not tracked then the selection could not give anything new
+            // class SerializationProxy in stdlib-cc/../LazyListIterable.scala has an example where this matters.
+            addSelects(ref.select(pt.sym).asInstanceOf[TermRef], pt.pt)
+        case _ => ref
+      val ref: Capability = addSelects(base, pt)
+      if ref.derivesFromMutable && pt.isValueType && !pt.isMutableType
+      then ref.readOnly
+      else ref
+
     /** The expected type for the qualifier of a selection. If the selection
      *  could be part of a capability path or is a a read-only method, we return
      *  a PathSelectionProto.
diff --git a/compiler/src/dotty/tools/dotc/transform/Recheck.scala b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
index fff8f3e94762..ffe28254fb08 100644
--- a/compiler/src/dotty/tools/dotc/transform/Recheck.scala
+++ b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
@@ -248,6 +248,12 @@ abstract class Recheck extends Phase, SymTransformer:
     def recheckSelection(tree: Select, qualType: Type, name: Name, pt: Type)(using Context): Type =
       recheckSelection(tree, qualType, name, sharpen = identity[Denotation])
 
+    def recheckThis(tree: This, pt: Type)(using Context): Type =
+      tree.tpe
+
+    def recheckSuper(tree: Super, pt: Type)(using Context): Type =
+      tree.tpe
+
     def recheckBind(tree: Bind, pt: Type)(using Context): Type = tree match
       case Bind(name, body) =>
         recheck(body, pt)
@@ -540,7 +546,9 @@ abstract class Recheck extends Phase, SymTransformer:
       def recheckUnnamed(tree: Tree, pt: Type): Type = tree match
         case tree: Apply => recheckApply(tree, pt)
         case tree: TypeApply => recheckTypeApply(tree, pt)
-        case _: New | _: This | _: Super | _: Literal => tree.tpe
+        case tree: This => recheckThis(tree, pt)
+        case tree: Super => recheckSuper(tree, pt)
+        case _: New | _: Literal => tree.tpe
         case tree: Typed => recheckTyped(tree)
         case tree: Assign => recheckAssign(tree)
         case tree: Block => recheckBlock(tree, pt)
diff --git a/tests/neg-custom-args/captures/class-caps.check b/tests/neg-custom-args/captures/class-caps.check
new file mode 100644
index 000000000000..ef6462eefbb3
--- /dev/null
+++ b/tests/neg-custom-args/captures/class-caps.check
@@ -0,0 +1,22 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/class-caps.scala:18:46 -----------------------------------
+18 |  def addWritesToConsole: (Int, Int) -> Int = (a, b) => // error
+   |                                              ^
+   |                                       Found:    (a: Int, b: Int) ->{Test.this.console} Int
+   |                                       Required: (Int, Int) -> Int
+   |
+   |                                       Note that capability Test.this.console is not included in capture set {}.
+19 |    log(s"adding a ($a) to b ($b)")(using console)
+20 |    a + b
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/class-caps.scala:28:46 -----------------------------------
+28 |  def addWritesToConsole: (Int, Int) -> Int = (a, b) => // error
+   |                                              ^
+   |                                      Found:    (a: Int, b: Int) ->{Test1.this.console} Int
+   |                                      Required: (Int, Int) -> Int
+   |
+   |                                      Note that capability Test1.this.console is not included in capture set {}.
+29 |    log(s"adding a ($a) to b ($b)")(using console)
+30 |    a + b
+   |
+   | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/class-caps.scala b/tests/neg-custom-args/captures/class-caps.scala
new file mode 100644
index 000000000000..f49356c8aecb
--- /dev/null
+++ b/tests/neg-custom-args/captures/class-caps.scala
@@ -0,0 +1,39 @@
+//> using scala 3.nightly
+
+import scala.language.experimental.captureChecking
+import scala.caps.*
+
+class Console() extends SharedCapability:
+  def println(s: String): Unit = System.out.println(s"console: $s")
+
+def log(s: String)(using c: Console): Unit =
+  summon[Console].println(s)
+
+class Test:
+  this: Test^ =>
+  val addPure: (Int, Int) -> Int = (a, b) => a + b // same as before
+
+  val console: Console^ = Console() // provide capability locally
+
+  def addWritesToConsole: (Int, Int) -> Int = (a, b) => // error
+    log(s"adding a ($a) to b ($b)")(using console)
+    a + b
+
+
+class Test1:
+  val addPure: (Int, Int) -> Int = (a, b) => a + b // same as before
+
+  val console: Console^ = Console() // provide capability locally
+
+  def addWritesToConsole: (Int, Int) -> Int = (a, b) => // error
+    log(s"adding a ($a) to b ($b)")(using console)
+    a + b
+
+object Test2:
+  val addPure: (Int, Int) -> Int = (a, b) => a + b // same as before
+
+  val console: Console^ = Console() // provide capability locally
+
+  def addWritesToConsole: (Int, Int) -> Int = (a, b) => // ok since `console` is static (maybe flag this?)
+    log(s"adding a ($a) to b ($b)")(using console)
+    a + b
diff --git a/tests/pos-custom-args/captures/constr-uses.scala b/tests/pos-custom-args/captures/constr-uses.scala
new file mode 100644
index 000000000000..cf32cfcfe4e3
--- /dev/null
+++ b/tests/pos-custom-args/captures/constr-uses.scala
@@ -0,0 +1,13 @@
+abstract class Test:
+  this: Test^ =>
+  def outer: Int
+
+  class Inner(x: Int):
+    def this() = this(outer)
+
+  val i = Inner()
+  val _: Inner = i
+
+  val f = () => Inner()
+  val _: () ->{this} Inner = f
+
diff --git a/tests/pos-custom-args/captures/nested-classes.scala b/tests/pos-custom-args/captures/nested-classes.scala
index e9227889f10e..bb422ceabd8f 100644
--- a/tests/pos-custom-args/captures/nested-classes.scala
+++ b/tests/pos-custom-args/captures/nested-classes.scala
@@ -5,6 +5,7 @@ class IO extends caps.SharedCapability
 class Blah
 class Pkg(using io: IO):
   class Foo:
+    this: Foo^{Pkg.this} =>
     def m(foo: Blah^{io}) = ???
 class Pkg2(using io: IO):
   class Foo:
diff --git a/tests/pos-custom-args/captures/secondary-constructors.scala b/tests/pos-custom-args/captures/secondary-constructors.scala
new file mode 100644
index 000000000000..abc923a3a8a3
--- /dev/null
+++ b/tests/pos-custom-args/captures/secondary-constructors.scala
@@ -0,0 +1,13 @@
+package scala
+package collection
+package immutable
+
+final class LazyListIterable[+A]():
+  this: LazyListIterable[A]^ =>
+  var _head: Any = 0
+  private def this(head: A, tail: LazyListIterable[A]^) =
+    this()
+    _head = head
+
+object LazyListIterable:
+  @inline private def eagerCons[A](hd: A, tl: LazyListIterable[A]^): LazyListIterable[A]^{tl} = new LazyListIterable[A](hd, tl)
\ No newline at end of file

From b7387d1766cf8d96170dc726081c32f2395173ea Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Thu, 4 Sep 2025 18:37:49 +0200
Subject: [PATCH 07/12] Refine treatment of fields

 - Charge the use set of the initializer to the class constructor
 - Charge the declared capture set to the class
---
 .../dotty/tools/dotc/cc/CheckCaptures.scala   | 31 +++++++++++++++++--
 .../dotty/tools/dotc/transform/Recheck.scala  |  5 ++-
 .../captures/class-constr.scala               |  6 ++--
 .../captures/exception-definitions.check      | 10 +++---
 .../captures/exception-definitions.scala      |  6 ++--
 .../captures/method-uses.scala                |  6 ++--
 tests/neg-custom-args/captures/uses.check     | 22 ++++++-------
 tests/neg-custom-args/captures/uses.scala     |  4 +--
 .../captures/nested-traits.scala              |  7 +++++
 9 files changed, 67 insertions(+), 30 deletions(-)
 create mode 100644 tests/pos-custom-args/captures/nested-traits.scala

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 5942f5874712..a7ecf18f387e 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -464,7 +464,7 @@ class CheckCaptures extends Recheck, SymTransformer:
      *  environments. At each stage, only include references from `cs` that are outside
      *  the environment's owner
      */
-    def markFree(cs: CaptureSet, tree: Tree)(using Context): Unit =
+    def markFree(cs: CaptureSet, tree: Tree, addUseInfo: Boolean = true)(using Context): Unit =
       // A captured reference with the symbol `sym` is visible from the environment
       // if `sym` is not defined inside the owner of the environment.
       inline def isVisibleFromEnv(sym: Symbol, env: Env) =
@@ -546,7 +546,7 @@ class CheckCaptures extends Recheck, SymTransformer:
 
       if !cs.isAlwaysEmpty then
         recur(cs, curEnv, null)
-        useInfos += ((tree, cs, curEnv))
+        if addUseInfo then useInfos += ((tree, cs, curEnv))
     end markFree
 
     /** If capability `c` refers to a parameter that is not implicitly or explicitly
@@ -988,6 +988,8 @@ class CheckCaptures extends Recheck, SymTransformer:
      *   - Interpolate contravariant capture set variables in result type.
      */
     override def recheckValDef(tree: ValDef, sym: Symbol)(using Context): Type =
+      val savedEnv = curEnv
+      val runInConstructor = !sym.isOneOf(Param | ParamAccessor | Lazy | NonMember)
       try
         if sym.is(Module) then sym.info // Modules are checked by checking the module class
         else
@@ -1006,6 +1008,8 @@ class CheckCaptures extends Recheck, SymTransformer:
                 ""
             disallowBadRootsIn(
               tree.tpt.nuType, NoSymbol, i"Mutable $sym", "have type", addendum, sym.srcPos)
+          if runInConstructor then
+            pushConstructorEnv()
           checkInferredResult(super.recheckValDef(tree, sym), tree)
       finally
         if !sym.is(Param) then
@@ -1015,6 +1019,11 @@ class CheckCaptures extends Recheck, SymTransformer:
           // function is compiled since we do not propagate expected types into blocks.
           interpolateIfInferred(tree.tpt, sym)
 
+        if runInConstructor && savedEnv.owner.isClass then
+          curEnv = savedEnv
+          markFree(tree.tpt.nuType.captureSet, tree, addUseInfo = false)
+    end recheckValDef
+
     /** Recheck method definitions:
      *   - check body in a nested environment that tracks uses, in  a nested level,
      *     and in a nested context that knows abaout Contains parameters so that we
@@ -1241,6 +1250,24 @@ class CheckCaptures extends Recheck, SymTransformer:
       recheckFinish(result, arg, pt)
     */
 
+    /** If environment is owned by a class, run in a new environment owned by
+     *  its primary constructor instead.
+     */
+    def pushConstructorEnv()(using Context): Unit =
+      if curEnv.owner.isClass then
+        val constr = curEnv.owner.primaryConstructor
+        if constr.exists then
+          val constrSet = capturedVars(constr)
+          if capturedVars(constr) ne CaptureSet.empty then
+            curEnv = Env(constr, EnvKind.Regular, constrSet, curEnv)
+
+    override def recheckStat(stat: Tree)(using Context): Unit =
+      val saved = curEnv
+      if !stat.isInstanceOf[MemberDef] then
+        pushConstructorEnv()
+      try recheck(stat)
+      finally curEnv = saved
+
     /** The main recheck method does some box adapation for all nodes:
      *   - If expected type `pt` is boxed and the tree is a lambda or a reference,
      *     don't propagate free variables.
diff --git a/compiler/src/dotty/tools/dotc/transform/Recheck.scala b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
index ffe28254fb08..d6fd49336e9d 100644
--- a/compiler/src/dotty/tools/dotc/transform/Recheck.scala
+++ b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
@@ -493,12 +493,15 @@ abstract class Recheck extends Phase, SymTransformer:
       recheckStats(tree.stats)
       NoType
 
+    def recheckStat(stat: Tree)(using Context): Unit =
+      recheck(stat)
+
     def recheckStats(stats: List[Tree])(using Context): Unit =
       @tailrec def traverse(stats: List[Tree])(using Context): Unit = stats match
         case (imp: Import) :: rest =>
           traverse(rest)(using ctx.importContext(imp, imp.symbol))
         case stat :: rest =>
-          recheck(stat)
+          recheckStat(stat)
           traverse(rest)
         case _ =>
       traverse(stats)
diff --git a/tests/neg-custom-args/captures/class-constr.scala b/tests/neg-custom-args/captures/class-constr.scala
index e86263fb0714..ab150868bef1 100644
--- a/tests/neg-custom-args/captures/class-constr.scala
+++ b/tests/neg-custom-args/captures/class-constr.scala
@@ -19,6 +19,6 @@ def test(a: Cap, b: Cap) =
       println(b)
       2
   val d = () => new D()
-  val d_ok1: () ->{a, b} D^{a, b} = d
-  val d_ok2: () -> D^{a, b} = d  // because of function shorthand
-  val d_ok3: () ->{a, b} D^{b} = d // error, but should work
+  val d_ok1: () ->{a, b} D^{a, b} = d // ok
+  val d_ok2: () ->{a} D^{b} = d  // ok
+  val d_ok3: () -> D^{a, b} = d // error
diff --git a/tests/neg-custom-args/captures/exception-definitions.check b/tests/neg-custom-args/captures/exception-definitions.check
index be5ea4304bf5..9429628b4bde 100644
--- a/tests/neg-custom-args/captures/exception-definitions.check
+++ b/tests/neg-custom-args/captures/exception-definitions.check
@@ -2,11 +2,11 @@
 3 |  self: Err^ => // error
   |        ^^^^
   |        Err is a pure type, it makes no sense to add a capture set to it
--- Error: tests/neg-custom-args/captures/exception-definitions.scala:7:12 ----------------------------------------------
+-- Error: tests/neg-custom-args/captures/exception-definitions.scala:7:8 -----------------------------------------------
 7 |    val x = c  // error
-  |            ^
-  |            reference (c : Any^) is not included in the allowed capture set {} of the self type of class Err2
+  |    ^^^^^^^^^
+  |    reference (c : Object^) is not included in the allowed capture set {} of the self type of class Err2
 -- Error: tests/neg-custom-args/captures/exception-definitions.scala:8:13 ----------------------------------------------
-8 |  class Err3(c: Any^) extends Exception // error
+8 |  class Err3(c: Object^) extends Exception // error
   |             ^
-  |       reference (Err3.this.c : Any^) is not included in the allowed capture set {} of the self type of class Err3
+  |    reference (Err3.this.c : Object^) is not included in the allowed capture set {} of the self type of class Err3
diff --git a/tests/neg-custom-args/captures/exception-definitions.scala b/tests/neg-custom-args/captures/exception-definitions.scala
index fbc9f3fd1d33..4c3370464ffe 100644
--- a/tests/neg-custom-args/captures/exception-definitions.scala
+++ b/tests/neg-custom-args/captures/exception-definitions.scala
@@ -2,11 +2,11 @@
 class Err extends Exception:
   self: Err^ => // error
 
-def test(c: Any^) =
+def test(c: Object^) =
   class Err2 extends Exception:
     val x = c  // error
-  class Err3(c: Any^) extends Exception // error
+  class Err3(c: Object^) extends Exception // error
 
-class Err4(c: Any^) extends AnyVal // was error, now ok
+class Err4(c: Object^) extends AnyVal // was error, now ok
 
 
diff --git a/tests/neg-custom-args/captures/method-uses.scala b/tests/neg-custom-args/captures/method-uses.scala
index da8f226685c0..576e227e5d74 100644
--- a/tests/neg-custom-args/captures/method-uses.scala
+++ b/tests/neg-custom-args/captures/method-uses.scala
@@ -11,7 +11,7 @@ def test(xs: List[() => Unit]) =
 
   foo // error
   bar() // error
-  Foo() // OK, but could be error
+  Foo() // error
 
 def test2(xs: List[() => Unit]) =
   def foo = xs.head // error, ok under deferredReaches
@@ -23,8 +23,8 @@ def test3(xs: List[() => Unit]): () ->{xs*} Unit = () =>
   def test4(xs: List[() => Unit]) = () => xs.head // error, ok under deferredReaches
 
   def test5(xs: List[() => Unit]) = new:
-    println(xs.head) // error, ok under deferredReaches
+    println(xs.head) // error, ok under deferredReaches // error
 
   def test6(xs: List[() => Unit]) =
-    val x= new { println(xs.head) } // error
+    val x= new { println(xs.head) } // error // error
     x
diff --git a/tests/neg-custom-args/captures/uses.check b/tests/neg-custom-args/captures/uses.check
index 08c79dd8fb5f..5ada150ddf79 100644
--- a/tests/neg-custom-args/captures/uses.check
+++ b/tests/neg-custom-args/captures/uses.check
@@ -1,21 +1,21 @@
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/uses.scala:8:17 ------------------------------------------
-8 |  val _: D^{y} = d // error, should be ok
-  |                 ^
-  |                 Found:    (d : D^{x, y})
-  |                 Required: D^{y}
-  |
-  |                 Note that capability x is not included in capture set {y}.
-  |
-  | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/uses.scala:9:13 ------------------------------------------
 9 |  val _: D = d // error
   |             ^
-  |             Found:    (d : D^{x, y})
+  |             Found:    (d : D^{y})
   |             Required: D
   |
-  |             Note that capability x is not included in capture set {}.
+  |             Note that capability y is not included in capture set {}.
   |
   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/uses.scala:13:22 -----------------------------------------
+13 |  val _: () -> Unit = f // error
+   |                      ^
+   |                      Found:    (f : () ->{x} Unit)
+   |                      Required: () -> Unit
+   |
+   |                      Note that capability x is not included in capture set {}.
+   |
+   | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/uses.scala:18:34 -----------------------------------------
 18 |  val _: () ->{x} () ->{y} Unit = g // error, should be ok
    |                                  ^
diff --git a/tests/neg-custom-args/captures/uses.scala b/tests/neg-custom-args/captures/uses.scala
index b872c7b03ec7..28d85b64687d 100644
--- a/tests/neg-custom-args/captures/uses.scala
+++ b/tests/neg-custom-args/captures/uses.scala
@@ -5,12 +5,12 @@ def test(x: C^, y: C^) =
     def foo() = println(y)
   }
   val d = D()
-  val _: D^{y} = d // error, should be ok
+  val _: D^{y} = d
   val _: D = d // error
 
   val f = () => println(D())
   val _: () ->{x} Unit = f // ok
-  val _: () -> Unit = f // should be error
+  val _: () -> Unit = f // error
 
   def g = () =>
     println(x)
diff --git a/tests/pos-custom-args/captures/nested-traits.scala b/tests/pos-custom-args/captures/nested-traits.scala
new file mode 100644
index 000000000000..b532feedeeee
--- /dev/null
+++ b/tests/pos-custom-args/captures/nested-traits.scala
@@ -0,0 +1,7 @@
+trait MapOps[K]:
+  this: MapOps[K]^ =>
+  def keysIterator: Iterator[K]
+
+  trait GenKeySet[K]:
+    this: collection.Set[K] =>
+    private[MapOps] val allKeys = MapOps.this.keysIterator.toSet
\ No newline at end of file

From 5c613919e9e1b2f3688c92213e1fc2b12abe5da9 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Thu, 4 Sep 2025 19:10:55 +0200
Subject: [PATCH 08/12] Issue a warning when a global value is declared with a
 capture set

---
 .../src/dotty/tools/dotc/cc/CheckCaptures.scala     | 13 ++++++++++++-
 tests/neg-custom-args/captures/class-caps.check     |  6 ++++++
 .../captures/nonsensical-for-pure.check             |  6 ++++++
 tests/pos-custom-args/captures/i23421.scala         |  2 +-
 4 files changed, 25 insertions(+), 2 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index a7ecf18f387e..86b34d302144 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -1019,9 +1019,20 @@ class CheckCaptures extends Recheck, SymTransformer:
           // function is compiled since we do not propagate expected types into blocks.
           interpolateIfInferred(tree.tpt, sym)
 
+        def declaredCaptures = tree.tpt.nuType.captureSet
         if runInConstructor && savedEnv.owner.isClass then
           curEnv = savedEnv
-          markFree(tree.tpt.nuType.captureSet, tree, addUseInfo = false)
+          markFree(declaredCaptures, tree, addUseInfo = false)
+
+        if sym.owner.isStaticOwner && !declaredCaptures.elems.isEmpty then
+          def where =
+            if sym.effectiveOwner.is(Package) then "top-level definition"
+            else i"member of static ${sym.owner}"
+          report.warning(
+            em"""$sym has a non-empty capture set but will not be added as
+                |a capability to computed capture sets since it is globally accessible
+                |as a $where. Global values cannot be capabilities.""",
+            tree.namePos)
     end recheckValDef
 
     /** Recheck method definitions:
diff --git a/tests/neg-custom-args/captures/class-caps.check b/tests/neg-custom-args/captures/class-caps.check
index ef6462eefbb3..362eee3e6170 100644
--- a/tests/neg-custom-args/captures/class-caps.check
+++ b/tests/neg-custom-args/captures/class-caps.check
@@ -20,3 +20,9 @@
 30 |    a + b
    |
    | longer explanation available when compiling with `-explain`
+-- Warning: tests/neg-custom-args/captures/class-caps.scala:35:6 -------------------------------------------------------
+35 |  val console: Console^ = Console() // provide capability locally
+   |      ^^^^^^^
+   |      value console has a non-empty capture set but will not be added as
+   |      a capability to computed capture sets since it is globally accessible
+   |      as a member of static object Test2. Global values cannot be capabilities.
diff --git a/tests/neg-custom-args/captures/nonsensical-for-pure.check b/tests/neg-custom-args/captures/nonsensical-for-pure.check
index 6860446c4177..2df943df4262 100644
--- a/tests/neg-custom-args/captures/nonsensical-for-pure.check
+++ b/tests/neg-custom-args/captures/nonsensical-for-pure.check
@@ -2,3 +2,9 @@
 1 |val x: Int^ = 2  // error
   |       ^^^^
   |       Int is a pure type, it makes no sense to add a capture set to it
+-- Warning: tests/neg-custom-args/captures/nonsensical-for-pure.scala:1:4 ----------------------------------------------
+1 |val x: Int^ = 2  // error
+  |    ^
+  |    value x has a non-empty capture set but will not be added as
+  |    a capability to computed capture sets since it is globally accessible
+  |    as a top-level definition. Global values cannot be capabilities.
diff --git a/tests/pos-custom-args/captures/i23421.scala b/tests/pos-custom-args/captures/i23421.scala
index ef5e7564073e..87458e6faeac 100644
--- a/tests/pos-custom-args/captures/i23421.scala
+++ b/tests/pos-custom-args/captures/i23421.scala
@@ -12,5 +12,5 @@ object Collection:
 trait Foo:
   val thunks: Collection[() => Unit] // that's fine
 
-object FooImpl1 extends Foo:
+class FooImpl1 extends Foo:
   val thunks: Collection[() => Unit] = Collection.empty // was error, now ok

From 4e8f7d9eac84230f5aa89b3df47e863b294b0cb3 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Thu, 4 Sep 2025 22:46:59 +0200
Subject: [PATCH 09/12] No warning for caps.cap

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

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 86b34d302144..21567d694bc9 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -1024,7 +1024,7 @@ class CheckCaptures extends Recheck, SymTransformer:
           curEnv = savedEnv
           markFree(declaredCaptures, tree, addUseInfo = false)
 
-        if sym.owner.isStaticOwner && !declaredCaptures.elems.isEmpty then
+        if sym.owner.isStaticOwner && !declaredCaptures.elems.isEmpty && sym != defn.captureRoot then
           def where =
             if sym.effectiveOwner.is(Package) then "top-level definition"
             else i"member of static ${sym.owner}"

From ce2e51ed47bc79e1357078c85b626dcd961ca913 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Fri, 5 Sep 2025 18:34:20 +0200
Subject: [PATCH 10/12] Propagate expected type into blocks

The level checking should do the proper avoidance so that local symbols
would not leak into type variables of the expected type.
---
 .../dotty/tools/dotc/transform/Recheck.scala  | 14 +++----
 .../neg-custom-args/captures/capt-test.scala  |  4 +-
 tests/neg-custom-args/captures/capt1.check    | 26 +++++-------
 tests/neg-custom-args/captures/capt1.scala    | 12 +++---
 tests/neg-custom-args/captures/eta.check      |  9 ++++
 tests/neg-custom-args/captures/eta.scala      |  2 +-
 .../captures/heal-tparam-cs.check             |  5 +--
 tests/neg-custom-args/captures/i23207.check   | 21 ++++++----
 tests/neg-custom-args/captures/i23207.scala   |  7 ++--
 .../neg-custom-args/captures/lazylists2.check | 42 ++++++++-----------
 .../neg-custom-args/captures/lazylists2.scala | 14 +++----
 tests/neg-custom-args/captures/leaky.check    | 37 ++++++----------
 tests/neg-custom-args/captures/leaky.scala    | 12 +++---
 .../captures/reference-cc.check               | 18 ++++----
 .../captures/sep-counter.check                |  6 +--
 .../neg-custom-args/captures/sep-pairs.check  |  4 +-
 .../captures/simple-using.check               |  4 +-
 tests/neg-custom-args/captures/try.check      | 34 ++++++---------
 tests/neg-custom-args/captures/try.scala      | 16 +++----
 .../captures/usingLogFile.check               |  8 ++--
 tests/neg-custom-args/captures/vars.check     |  5 +--
 21 files changed, 138 insertions(+), 162 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/transform/Recheck.scala b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
index d6fd49336e9d..34e3773ba147 100644
--- a/compiler/src/dotty/tools/dotc/transform/Recheck.scala
+++ b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
@@ -376,25 +376,21 @@ abstract class Recheck extends Phase, SymTransformer:
       recheck(tree.rhs, lhsType.widen)
       defn.UnitType
 
-    private def recheckBlock(stats: List[Tree], expr: Tree)(using Context): Type =
+    private def recheckBlock(stats: List[Tree], expr: Tree, pt: Type)(using Context): Type =
       recheckStats(stats)
-      val exprType = recheck(expr)
+      val exprType = recheck(expr, pt)
       TypeOps.avoid(exprType, localSyms(stats).filterConserve(_.isTerm))
 
     def recheckBlock(tree: Block, pt: Type)(using Context): Type = tree match
-      case Block(Nil, expr: Block) => recheckBlock(expr, pt)
       case Block((mdef : DefDef) :: Nil, closure: Closure) =>
         recheckClosureBlock(mdef, closure.withSpan(tree.span), pt)
-      case Block(stats, expr) => recheckBlock(stats, expr)
-        // The expected type `pt` is not propagated. Doing so would allow variables in the
-        // expected type to contain references to local symbols of the block, so the
-        // local symbols could escape that way.
+      case Block(stats, expr) => recheckBlock(stats, expr, pt)
 
     def recheckClosureBlock(mdef: DefDef, expr: Closure, pt: Type)(using Context): Type =
-      recheckBlock(mdef :: Nil, expr)
+      recheckBlock(mdef :: Nil, expr, pt)
 
     def recheckInlined(tree: Inlined, pt: Type)(using Context): Type =
-      recheckBlock(tree.bindings, tree.expansion)(using inlineContext(tree))
+      recheckBlock(tree.bindings, tree.expansion, pt)(using inlineContext(tree))
 
     def recheckIf(tree: If, pt: Type)(using Context): Type =
       recheck(tree.cond, defn.BooleanType)
diff --git a/tests/neg-custom-args/captures/capt-test.scala b/tests/neg-custom-args/captures/capt-test.scala
index 3d5ebd3ee6ff..ea2a77d5c2ac 100644
--- a/tests/neg-custom-args/captures/capt-test.scala
+++ b/tests/neg-custom-args/captures/capt-test.scala
@@ -20,8 +20,8 @@ def handle[E <: Exception,  R <: Top](op: (CT[E] @retains[caps.cap.type]) => R)(
   catch case ex: E => handler(ex)
 
 def test: Unit =
-  val b = handle[Exception, () => Nothing] { // error // error
-    (x: CanThrow[Exception]) => () => raise(new Exception)(using x)
+  val b = handle[Exception, () => Nothing] { // error
+    (x: CanThrow[Exception]) => () => raise(new Exception)(using x)  // error
   } {
     (ex: Exception) => ???
   }
diff --git a/tests/neg-custom-args/captures/capt1.check b/tests/neg-custom-args/captures/capt1.check
index a7d322c74395..6af772cd2a0b 100644
--- a/tests/neg-custom-args/captures/capt1.check
+++ b/tests/neg-custom-args/captures/capt1.check
@@ -16,35 +16,31 @@
   |  Note that capability x is not included in capture set {}.
   |
   | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:15:2 -----------------------------------------
-15 |  def f(y: Int) = if x == null then y else y  // error
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:16:2 -----------------------------------------
+16 |  f  // error
    |  ^
    |  Found:    (y: Int) ->{x} Int
    |  Required: Matchable
    |
    |  Note that capability x is not included in capture set {}.
-16 |  f
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:22:2 -----------------------------------------
-22 |  class F(y: Int) extends A:   // error
-   |  ^
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:24:2 -----------------------------------------
+24 |  F(22)  // error
+   |  ^^^^^
    |  Found:    A^{x}
    |  Required: A
    |
    |  Note that capability x is not included in capture set {}.
-23 |    def m() = if x == null then y else y
-24 |  F(22)
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:27:2 -----------------------------------------
-27 |  new A: // error
-   |  ^
-   |  Found:    A^{x}
-   |  Required: A
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:28:40 ----------------------------------------
+28 |    def m() = if x == null then y else y  // error
+   |                                        ^
+   |                                        Found:    A^{x}
+   |                                        Required: A
    |
-   |  Note that capability x is not included in capture set {}.
-28 |    def m() = if x == null then y else y
+   |                                        Note that capability x is not included in capture set {}.
    |
    | longer explanation available when compiling with `-explain`
 -- Error: tests/neg-custom-args/captures/capt1.scala:36:16 -------------------------------------------------------------
diff --git a/tests/neg-custom-args/captures/capt1.scala b/tests/neg-custom-args/captures/capt1.scala
index b8df78a869a1..1a1eddb7a2fb 100644
--- a/tests/neg-custom-args/captures/capt1.scala
+++ b/tests/neg-custom-args/captures/capt1.scala
@@ -12,20 +12,20 @@ def h1(x: C @retains[caps.cap.type], y: C): Any =
   () => f()  // ok
 
 def h2(x: C @retains[caps.cap.type]): Matchable =
-  def f(y: Int) = if x == null then y else y  // error
-  f
+  def f(y: Int) = if x == null then y else y
+  f  // error
 
 class A
 type Cap = C @retains[caps.cap.type]
 
 def h3(x: Cap): A =
-  class F(y: Int) extends A:   // error
+  class F(y: Int) extends A:
     def m() = if x == null then y else y
-  F(22)
+  F(22)  // error
 
 def h4(x: Cap, y: Int): A =
-  new A: // error
-    def m() = if x == null then y else y
+  new A:
+    def m() = if x == null then y else y  // error
 
 def f1(c: Cap): () ->{c} c.type = () => c // ok
 
diff --git a/tests/neg-custom-args/captures/eta.check b/tests/neg-custom-args/captures/eta.check
index dfce53accd4d..4bd409c35cca 100644
--- a/tests/neg-custom-args/captures/eta.check
+++ b/tests/neg-custom-args/captures/eta.check
@@ -7,3 +7,12 @@
   |         Note that capability f is not included in capture set {}.
   |
   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/eta.scala:7:7 --------------------------------------------
+7 |       () => { stowaway.apply().apply() }  // error (was ok)
+  |       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+  |       Found:    () ->{stowaway} Unit
+  |       Required: () -> Unit
+  |
+  |       Note that capability stowaway is not included in capture set {}.
+  |
+  | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/eta.scala b/tests/neg-custom-args/captures/eta.scala
index d192d7baedf8..ad4f24342b91 100644
--- a/tests/neg-custom-args/captures/eta.scala
+++ b/tests/neg-custom-args/captures/eta.scala
@@ -4,4 +4,4 @@
          g  // error
        val stowaway: () -> Proc^{f} =
          bar( () => f )  // was error now OK
-       () => { stowaway.apply().apply() }
\ No newline at end of file
+       () => { stowaway.apply().apply() }  // error (was ok)
\ No newline at end of file
diff --git a/tests/neg-custom-args/captures/heal-tparam-cs.check b/tests/neg-custom-args/captures/heal-tparam-cs.check
index efc0a3f168b2..d23ebe064866 100644
--- a/tests/neg-custom-args/captures/heal-tparam-cs.check
+++ b/tests/neg-custom-args/captures/heal-tparam-cs.check
@@ -1,6 +1,6 @@
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/heal-tparam-cs.scala:10:23 -------------------------------
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/heal-tparam-cs.scala:10:25 -------------------------------
 10 |  val test1 = localCap { c => // error
-   |                       ^
+   |                         ^
    |Found:    (c: Capp^'s1) ->'s2 () ->{c} Unit
    |Required: (c: Capp^) => () ->'s3 Unit
    |
@@ -9,7 +9,6 @@
    |where:    => refers to a fresh root capability created in value test1 when checking argument to parameter op of method localCap
    |          ^  refers to the universal root capability
 11 |    () => { c.use() }
-12 |  }
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/heal-tparam-cs.scala:15:13 -------------------------------
diff --git a/tests/neg-custom-args/captures/i23207.check b/tests/neg-custom-args/captures/i23207.check
index 6300857c612f..626655686d87 100644
--- a/tests/neg-custom-args/captures/i23207.check
+++ b/tests/neg-custom-args/captures/i23207.check
@@ -16,16 +16,21 @@
    |             Note that capability b is not included in capture set {}.
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i23207.scala:23:2 ----------------------------------------
-23 |  class B extends A:   // error, now we see the error for the whole block since there are no nested errors
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i23207.scala:19:2 ----------------------------------------
+19 |  c // error
    |  ^
-   |  Found:    A^{io}
+   |  Found:    A^{c}
    |  Required: A
    |
-   |  Note that capability io is not included in capture set {}.
-24 |    val hide: AnyRef^{io} = io
-25 |  val b = new B
-26 |  val c = b.getBox.x
-27 |  c
+   |  Note that capability c is not included in capture set {}.
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i23207.scala:27:2 ----------------------------------------
+27 |  c  // error
+   |  ^
+   |  Found:    A^{c}
+   |  Required: A
+   |
+   |  Note that capability c is not included in capture set {}.
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/i23207.scala b/tests/neg-custom-args/captures/i23207.scala
index 36402944d393..bfd1e3004c33 100644
--- a/tests/neg-custom-args/captures/i23207.scala
+++ b/tests/neg-custom-args/captures/i23207.scala
@@ -16,13 +16,12 @@ def leak(io: AnyRef^): A =
   val c = b.getBox.x
   val _: B^{b} = c // ok
   val _: A = c // error
-  c // no error here since we don't propagate expected type into the last expression of a block
-    // and the whole block's span overlaps with previous errors
+  c // error
 
 def leak2(io: AnyRef^): A =
-  class B extends A:   // error, now we see the error for the whole block since there are no nested errors
+  class B extends A:
     val hide: AnyRef^{io} = io
 
   val b = new B
   val c = b.getBox.x
-  c
+  c  // error
diff --git a/tests/neg-custom-args/captures/lazylists2.check b/tests/neg-custom-args/captures/lazylists2.check
index 027853498cf3..adbb35ad07e8 100644
--- a/tests/neg-custom-args/captures/lazylists2.check
+++ b/tests/neg-custom-args/captures/lazylists2.check
@@ -1,29 +1,19 @@
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylists2.scala:18:4 ------------------------------------
-18 |    final class Mapped extends LazyList[B]:  // error
-   |    ^
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylists2.scala:24:4 ------------------------------------
+24 |    new Mapped  // error
+   |    ^^^^^^^^^^
    |    Found:    LazyList[B^'s1]^{f, xs}
    |    Required: LazyList[B]^{f}
    |
    |    Note that capability xs is not included in capture set {f}.
-19 |      this: (Mapped^{xs, f}) =>
-20 |      def isEmpty = false
-21 |      def head: B = f(xs.head)
-22 |      def tail: LazyList[B]^{this} = xs.tail.map(f)
-23 |    new Mapped
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylists2.scala:27:4 ------------------------------------
-27 |    final class Mapped extends LazyList[B]:  // error
-   |    ^
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylists2.scala:33:4 ------------------------------------
+33 |    new Mapped  // error
+   |    ^^^^^^^^^^
    |    Found:    LazyList[B^'s2]^{f, xs}
    |    Required: LazyList[B]^{xs}
    |
    |    Note that capability f is not included in capture set {xs}.
-28 |      this: Mapped^{xs, f} =>
-29 |      def isEmpty = false
-30 |      def head: B = f(xs.head)
-31 |      def tail: LazyList[B]^{this} = xs.tail.map(f)
-32 |    new Mapped
    |
    | longer explanation available when compiling with `-explain`
 -- Error: tests/neg-custom-args/captures/lazylists2.scala:40:20 --------------------------------------------------------
@@ -34,18 +24,13 @@
 41 |      def tail: LazyList[B]^{this}= xs.tail.map(f) // error
    |                                                ^
    |         reference (f : A => B) is not included in the allowed capture set {xs} of the self type of class Mapped
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylists2.scala:45:4 ------------------------------------
-45 |    final class Mapped extends LazyList[B]:  // error
-   |    ^
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylists2.scala:51:4 ------------------------------------
+51 |    new Mapped  // error
+   |    ^^^^^^^^^^
    |    Found:    LazyList[B^'s3]^{f, xs}
    |    Required: LazyList[B]^{xs}
    |
    |    Note that capability f is not included in capture set {xs}.
-46 |      this: (Mapped^{xs, f}) =>
-47 |      def isEmpty = false
-48 |      def head: B = f(xs.head)
-49 |      def tail: LazyList[B]^{xs, f} = xs.tail.map(f)
-50 |    new Mapped
    |
    | longer explanation available when compiling with `-explain`
 -- Error: tests/neg-custom-args/captures/lazylists2.scala:60:10 --------------------------------------------------------
@@ -53,3 +38,12 @@
    |    ^
    |    references {f, xs} are not all included in the allowed capture set {} of the self type of class Mapped2
 61 |      this: Mapped =>
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylists2.scala:62:4 ------------------------------------
+62 |    new Mapped2 // error
+   |    ^^^^^^^^^^^
+   |    Found:    LazyList[B^'s4]^{f, xs}
+   |    Required: LazyList[B]
+   |
+   |    Note that capability f is not included in capture set {}.
+   |
+   | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/lazylists2.scala b/tests/neg-custom-args/captures/lazylists2.scala
index f6c1cf95a8ed..504ec6d64e06 100644
--- a/tests/neg-custom-args/captures/lazylists2.scala
+++ b/tests/neg-custom-args/captures/lazylists2.scala
@@ -15,22 +15,22 @@ object LazyNil extends LazyList[Nothing]:
 
 extension [A](xs: LazyList[A]^)
   def map[B](f: A => B): LazyList[B]^{f} =
-    final class Mapped extends LazyList[B]:  // error
+    final class Mapped extends LazyList[B]:
       this: (Mapped^{xs, f}) =>
 
       def isEmpty = false
       def head: B = f(xs.head)
       def tail: LazyList[B]^{this} = xs.tail.map(f)
-    new Mapped
+    new Mapped  // error
 
   def map2[B](f: A => B): LazyList[B]^{xs} =
-    final class Mapped extends LazyList[B]:  // error
+    final class Mapped extends LazyList[B]:
       this: Mapped^{xs, f} =>
 
       def isEmpty = false
       def head: B = f(xs.head)
       def tail: LazyList[B]^{this} = xs.tail.map(f)
-    new Mapped
+    new Mapped  // error
 
   def map3[B](f: A => B): LazyList[B]^{xs} =
     final class Mapped extends LazyList[B]:
@@ -42,13 +42,13 @@ extension [A](xs: LazyList[A]^)
     new Mapped
 
   def map4[B](f: A => B): LazyList[B]^{xs} =
-    final class Mapped extends LazyList[B]:  // error
+    final class Mapped extends LazyList[B]:
       this: (Mapped^{xs, f}) =>
 
       def isEmpty = false
       def head: B = f(xs.head)
       def tail: LazyList[B]^{xs, f} = xs.tail.map(f)
-    new Mapped
+    new Mapped  // error
 
   def map5[B](f: A => B): LazyList[B] =
     class Mapped extends LazyList[B]:
@@ -59,6 +59,6 @@ extension [A](xs: LazyList[A]^)
       def tail: LazyList[B]^{this} = xs.tail.map(f)
     class Mapped2 extends Mapped:  // error
       this: Mapped =>
-    new Mapped2
+    new Mapped2 // error
 
 
diff --git a/tests/neg-custom-args/captures/leaky.check b/tests/neg-custom-args/captures/leaky.check
index c441ac5f102e..b6fb368aa757 100644
--- a/tests/neg-custom-args/captures/leaky.check
+++ b/tests/neg-custom-args/captures/leaky.check
@@ -1,38 +1,27 @@
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/leaky.scala:14:2 -----------------------------------------
-14 |  val f: Any ->{a} Any = _ =>  // error
-   |  ^
-   |  Found:    test.runnable.Transform{val fun: Any ->{a} Any}^{a}
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/leaky.scala:17:11 ----------------------------------------
+17 |  Transform(f)  // error
+   |  ^^^^^^^^^^^^
+   |  Found:    test.runnable.Transform{val fun: (f : Any ->{a} Any)}^{f}
    |  Required: test.runnable.Transform
    |
-   |  Note that capability a is not included in capture set {}.
-15 |    a.print()
-16 |    ()
-17 |  Transform(f)
+   |  Note that capability f is not included in capture set {}.
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/leaky.scala:20:2 -----------------------------------------
-20 |  val f: Any ->{a} Any = _ => // error
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/leaky.scala:24:2 -----------------------------------------
+24 |  x  // error
    |  ^
-   |  Found:    test.runnable.Transform{val fun: Any ->{a} Any}^{a}
+   |  Found:    test.runnable.Transform{val fun: Any ->{f} Any}^{x}
    |  Required: test.runnable.Transform
    |
-   |  Note that capability a is not included in capture set {}.
-21 |    a.print()
-22 |    ()
-23 |  val x = Transform(f)
-24 |  x
+   |  Note that capability x is not included in capture set {}.
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/leaky.scala:27:2 -----------------------------------------
-27 |  val f: Any ->{a} Any = _ =>  // error
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/leaky.scala:31:2 -----------------------------------------
+31 |  x  // error
    |  ^
-   |  Found:    test.runnable.Transform{val fun: Any ->{a} Any}^{a}
+   |  Found:    test.runnable.Transform{val fun: Any ->{f} Any}^{x}
    |  Required: test.runnable.Transform
    |
-   |  Note that capability a is not included in capture set {}.
-28 |    a.print()
-29 |    ()
-30 |  val x = Transform.app(f)
-31 |  x
+   |  Note that capability x is not included in capture set {}.
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/leaky.scala b/tests/neg-custom-args/captures/leaky.scala
index b614c8e09bdc..4fd98d3f6b62 100644
--- a/tests/neg-custom-args/captures/leaky.scala
+++ b/tests/neg-custom-args/captures/leaky.scala
@@ -11,24 +11,24 @@ object Transform:
     Transform(f)
 
 def leak(a: A): Transform^{} =
-  val f: Any ->{a} Any = _ =>  // error
+  val f: Any ->{a} Any = _ =>
     a.print()
     ()
-  Transform(f)
+  Transform(f)  // error
 
 def leak1(a: A): Transform^{} =
-  val f: Any ->{a} Any = _ => // error
+  val f: Any ->{a} Any = _ =>
     a.print()
     ()
   val x = Transform(f)
-  x
+  x  // error
 
 def leak2(a: A): Transform^{} =
-  val f: Any ->{a} Any = _ =>  // error
+  val f: Any ->{a} Any = _ =>
     a.print()
     ()
   val x = Transform.app(f)
-  x
+  x  // error
 
 def withA[T](body: A => T): T = body(A())
 
diff --git a/tests/neg-custom-args/captures/reference-cc.check b/tests/neg-custom-args/captures/reference-cc.check
index dea3e1a5b5e1..d557a37039b8 100644
--- a/tests/neg-custom-args/captures/reference-cc.check
+++ b/tests/neg-custom-args/captures/reference-cc.check
@@ -3,9 +3,9 @@
    |                    ^
    |                    reference (c : Cap) is not included in the allowed capture set {}
    |                    of the enclosing class A
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reference-cc.scala:44:27 ---------------------------------
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reference-cc.scala:44:29 ---------------------------------
 44 |  val later = usingLogFile { file => () => file.write(0) } // error
-   |                           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   |                             ^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |Found:    (file: java.io.FileOutputStream^'s1) ->'s2 () ->{file} Unit
    |Required: java.io.FileOutputStream^ => () ->'s3 Unit
    |
@@ -31,15 +31,13 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reference-cc.scala:58:8 ----------------------------------
 58 |    try () => xs.map(f).sum  // error TODO improve error message
    |        ^^^^^^^^^^^^^^^^^^^
-   |Found:    () => Double
-   |Required: () =>² Double
+   |Found:    () ->{canThrow$1} Double
+   |Required: () => Double
    |
-   |Note that capability cap is not included in capture set {cap²}
-   |because cap in method try$1 is not visible from cap² in enclosing function.
+   |Note that capability canThrow$1 is not included in capture set {cap}
+   |because (canThrow$1 : CanThrow[LimitExceeded]) in method try$1 is not visible from cap in enclosing function.
    |
-   |where:    =>   refers to a fresh root capability classified as Control in the type of given instance canThrow$1
-   |          =>²  refers to a fresh root capability created in anonymous function of type (using erased x$1: CanThrow[LimitExceeded]): () => Double when instantiating expected result type () ->{cap³} Double of function literal
-   |          cap  is a fresh root capability classified as Control in the type of given instance canThrow$1
-   |          cap² is a fresh root capability created in anonymous function of type (using erased x$1: CanThrow[LimitExceeded]): () => Double when instantiating expected result type () ->{cap³} Double of function literal
+   |where:    =>  refers to a fresh root capability created in anonymous function of type (using erased x$1: CanThrow[LimitExceeded]): () => Double when instantiating expected result type () ->{cap²} Double of function literal
+   |          cap is a fresh root capability created in anonymous function of type (using erased x$1: CanThrow[LimitExceeded]): () => Double when instantiating expected result type () ->{cap²} Double of function literal
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/sep-counter.check b/tests/neg-custom-args/captures/sep-counter.check
index f46d3fa03dfc..c9d2b1895aee 100644
--- a/tests/neg-custom-args/captures/sep-counter.check
+++ b/tests/neg-custom-args/captures/sep-counter.check
@@ -2,9 +2,9 @@
 12 |  def mkCounter(): Pair[Ref^, Ref^] =  // error
    |                   ^^^^^^^^^^^^^^^^
    | Separation failure in method mkCounter's result type Pair[Ref^, Ref^²].
-   | One part,  Ref^, hides capabilities  {cap}.
-   | Another part,  Ref^²,  captures capabilities  {cap}.
-   | The two sets overlap at  cap of method mkCounter.
+   | One part,  Ref^, hides capabilities  {c, cap}.
+   | Another part,  Ref^²,  captures capabilities  {c, cap}.
+   | The two sets overlap at  {c}.
    |
    | where:    ^   refers to a fresh root capability classified as Mutable in the result type of method mkCounter
    |           ^²  refers to a fresh root capability classified as Mutable in the result type of method mkCounter
diff --git a/tests/neg-custom-args/captures/sep-pairs.check b/tests/neg-custom-args/captures/sep-pairs.check
index 3835730bea45..43429b08a3bc 100644
--- a/tests/neg-custom-args/captures/sep-pairs.check
+++ b/tests/neg-custom-args/captures/sep-pairs.check
@@ -12,8 +12,8 @@
 13 |def bad: Pair[Ref^, Ref^] =  // error: overlap at r1*, r0
    |         ^^^^^^^^^^^^^^^^
    |         Separation failure in method bad's result type Pair[Ref^, Ref^²].
-   |         One part,  Ref^, hides capabilities  {cap, cap², r1*, r0}.
-   |         Another part,  Ref^²,  captures capabilities  {cap, cap², r1*, r0}.
+   |         One part,  Ref^, hides capabilities  {r1*, cap, cap², r0}.
+   |         Another part,  Ref^²,  captures capabilities  {r1*, cap, cap², r0}.
    |         The two sets overlap at  {r1*, r0}.
    |
    |         where:    ^    refers to a fresh root capability classified as Mutable in the result type of method bad
diff --git a/tests/neg-custom-args/captures/simple-using.check b/tests/neg-custom-args/captures/simple-using.check
index 3c3ca24ebb47..54aa8a464ae4 100644
--- a/tests/neg-custom-args/captures/simple-using.check
+++ b/tests/neg-custom-args/captures/simple-using.check
@@ -1,6 +1,6 @@
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/simple-using.scala:8:15 ----------------------------------
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/simple-using.scala:8:17 ----------------------------------
 8 |  usingLogFile { f => () => f.write(2) } // error
-  |               ^^^^^^^^^^^^^^^^^^^^^^^^^
+  |                 ^^^^^^^^^^^^^^^^^^^^^
   |Found:    (f: java.io.FileOutputStream^'s1) ->'s2 () ->{f} Unit
   |Required: java.io.FileOutputStream^ => () ->'s3 Unit
   |
diff --git a/tests/neg-custom-args/captures/try.check b/tests/neg-custom-args/captures/try.check
index 7a42adb8bbdc..60029abb8202 100644
--- a/tests/neg-custom-args/captures/try.check
+++ b/tests/neg-custom-args/captures/try.check
@@ -1,13 +1,13 @@
 -- Error: tests/neg-custom-args/captures/try.scala:23:28 ---------------------------------------------------------------
-23 |  val a = handle[Exception, CanThrow[Exception]] { // error // error
+23 |  val a = handle[Exception, CanThrow[Exception]] { // error
    |                            ^^^^^^^^^^^^^^^^^^^
    |                            Type variable R of method handle cannot be instantiated to CT[Exception]^ since
    |                            that type captures the root capability `cap`.
    |
    |                            where:    ^ refers to the universal root capability
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:23:49 ------------------------------------------
-23 |  val a = handle[Exception, CanThrow[Exception]] { // error // error
-   |                                                 ^
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:24:4 -------------------------------------------
+24 |    (x: CanThrow[Exception]) => x // error
+   |    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |Found:    (x: CT[Exception]^) ->'s1 CT[Exception]^{x}
    |Required: CT[Exception]^ => CT[Exception]^²
    |
@@ -18,13 +18,11 @@
    |          ^   refers to the universal root capability
    |          ^²  refers to a fresh root capability created in value a when checking argument to parameter op of method handle
    |          cap is a fresh root capability created in value a when checking argument to parameter op of method handle
-24 |    (x: CanThrow[Exception]) => x
-25 |  }{
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:29:43 ------------------------------------------
-29 |  val b = handle[Exception, () -> Nothing] { // error
-   |                                           ^
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:30:4 -------------------------------------------
+30 |    (x: CanThrow[Exception]) => () => raise(new Exception)(using x) // error
+   |    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |Found:    (x: CT[Exception]^) ->'s2 () ->{x} Nothing
    |Required: CT[Exception]^ => () -> Nothing
    |
@@ -32,13 +30,11 @@
    |
    |where:    => refers to a fresh root capability created in value b when checking argument to parameter op of method handle
    |          ^  refers to the universal root capability
-30 |    (x: CanThrow[Exception]) => () => raise(new Exception)(using x)
-31 |  } {
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:35:18 ------------------------------------------
-35 |  val xx = handle {  // error
-   |                  ^
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:36:4 -------------------------------------------
+36 |    (x: CanThrow[Exception]) => // error
+   |    ^
    |Found:    (x: CT[Exception]^) ->'s3 () ->{x} Int
    |Required: CT[Exception]^ => () ->'s4 Int
    |
@@ -46,16 +42,14 @@
    |
    |where:    => refers to a fresh root capability created in value xx when checking argument to parameter op of method handle
    |          ^  refers to the universal root capability
-36 |    (x: CanThrow[Exception]) =>
 37 |      () =>
 38 |        raise(new Exception)(using x)
 39 |        22
-40 |  } {
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:47:31 ------------------------------------------
-47 |val global: () -> Int = handle { // error
-   |                               ^
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:48:2 -------------------------------------------
+48 |  (x: CanThrow[Exception]) =>  // error
+   |  ^
    |Found:    (x: CT[Exception]^) ->'s5 () ->{x} Int
    |Required: CT[Exception]^ => () ->'s6 Int
    |
@@ -63,10 +57,8 @@
    |
    |where:    => refers to a fresh root capability created in value global when checking argument to parameter op of method handle
    |          ^  refers to the universal root capability
-48 |  (x: CanThrow[Exception]) =>
 49 |    () =>
 50 |      raise(new Exception)(using x)
 51 |      22
-52 |} {
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/try.scala b/tests/neg-custom-args/captures/try.scala
index 8168504617ac..7656fd3e45ee 100644
--- a/tests/neg-custom-args/captures/try.scala
+++ b/tests/neg-custom-args/captures/try.scala
@@ -20,20 +20,20 @@ def handle[E <: Exception,  R <: Top](op: CT[E]^ => R)(handler: E => R): R =
   catch case ex: E => handler(ex)
 
 def test =
-  val a = handle[Exception, CanThrow[Exception]] { // error // error
-    (x: CanThrow[Exception]) => x
+  val a = handle[Exception, CanThrow[Exception]] { // error
+    (x: CanThrow[Exception]) => x // error
   }{
     (ex: Exception) => ???
   }
 
-  val b = handle[Exception, () -> Nothing] { // error
-    (x: CanThrow[Exception]) => () => raise(new Exception)(using x)
+  val b = handle[Exception, () -> Nothing] {
+    (x: CanThrow[Exception]) => () => raise(new Exception)(using x) // error
   } {
     (ex: Exception) => ???
   }
 
-  val xx = handle {  // error
-    (x: CanThrow[Exception]) =>
+  val xx = handle {
+    (x: CanThrow[Exception]) => // error
       () =>
         raise(new Exception)(using x)
         22
@@ -44,8 +44,8 @@ def test =
   yy // OK
 
 
-val global: () -> Int = handle { // error
-  (x: CanThrow[Exception]) =>
+val global: () -> Int = handle {
+  (x: CanThrow[Exception]) =>  // error
     () =>
       raise(new Exception)(using x)
       22
diff --git a/tests/neg-custom-args/captures/usingLogFile.check b/tests/neg-custom-args/captures/usingLogFile.check
index 82f0857c061b..b4ef40afd587 100644
--- a/tests/neg-custom-args/captures/usingLogFile.check
+++ b/tests/neg-custom-args/captures/usingLogFile.check
@@ -1,6 +1,6 @@
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/usingLogFile.scala:22:27 ---------------------------------
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/usingLogFile.scala:22:29 ---------------------------------
 22 |  val later = usingLogFile { f => () => f.write(0) } // error
-   |                           ^^^^^^^^^^^^^^^^^^^^^^^^^
+   |                             ^^^^^^^^^^^^^^^^^^^^^
    |Found:    (f: java.io.FileOutputStream^'s1) ->'s2 () ->{f} Unit
    |Required: java.io.FileOutputStream^ => () ->'s3 Unit
    |
@@ -10,9 +10,9 @@
    |          ^  refers to the universal root capability
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/usingLogFile.scala:27:36 ---------------------------------
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/usingLogFile.scala:27:38 ---------------------------------
 27 |  private val later2 = usingLogFile { f => Cell(() => f.write(0)) } // error
-   |                                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   |                                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |Found:    (f: java.io.FileOutputStream^'s4) ->'s5 Test2.Cell[() ->{f} Unit]^'s6
    |Required: java.io.FileOutputStream^ => Test2.Cell[() ->'s7 Unit]^'s8
    |
diff --git a/tests/neg-custom-args/captures/vars.check b/tests/neg-custom-args/captures/vars.check
index 52b1e5559322..2029a61cb00e 100644
--- a/tests/neg-custom-args/captures/vars.check
+++ b/tests/neg-custom-args/captures/vars.check
@@ -27,9 +27,9 @@
    |        Note that capability cap3 is not included in capture set {cap1, cap2}.
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/vars.scala:36:8 ------------------------------------------
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/vars.scala:36:10 -----------------------------------------
 36 |  local { cap3 => // error
-   |        ^
+   |          ^
    |Found:    (cap3: CC^) ->'s1 String => String
    |Required: CC^ -> String =>² String
    |
@@ -42,6 +42,5 @@
    |          cap² is a fresh root capability created in method test of parameter parameter cap3² of method $anonfun
 37 |    def g(x: String): String = if cap3 == cap3 then "" else "a"
 38 |    g
-39 |  }
    |
    | longer explanation available when compiling with `-explain`

From 0abc0d3cb44f010ea4b20df2caf9971606610043 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sat, 6 Sep 2025 20:01:41 +0200
Subject: [PATCH 11/12] Don't automatically add the owner of a FreshCap to its
 hidden set

This can lead to unsoundness. For instance:

    class C extends SharedCapability
    val b: C => C

Then `b` is the owner of the FreshCap implicitly added to the result C,
yet it should not be added to the hidden set, since `b` itself is not
a SharedCapability.
---
 compiler/src/dotty/tools/dotc/cc/Setup.scala | 21 +-------------------
 1 file changed, 1 insertion(+), 20 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala
index aa9b9f399634..b925442e8feb 100644
--- a/compiler/src/dotty/tools/dotc/cc/Setup.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -459,7 +459,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
       if sym.isType then stripImpliedCaptureSet(tp2)
       else tp2
     if freshen then
-      capToFresh(tp3, Origin.InDecl(sym)).tap(addOwnerAsHidden(_, sym))
+      capToFresh(tp3, Origin.InDecl(sym))
     else tp3
   end transformExplicitType
 
@@ -473,25 +473,6 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
   extension (sym: Symbol) def nextInfo(using Context): Type =
     atPhase(thisPhase.next)(sym.info)
 
-  private def addOwnerAsHidden(tp: Type, owner: Symbol)(using Context): Unit =
-    val ref = owner.termRef
-    def add = new TypeTraverser:
-      var reach = false
-      def traverse(t: Type): Unit = t match
-        case t @ CapturingType(parent, refs) =>
-          val saved = reach
-          reach |= t.isBoxed
-          try
-            traverse(parent)
-            for case fresh: FreshCap <- refs.elems.iterator do // TODO: what about fresh.rd elems?
-              if reach then fresh.hiddenSet.elems += ref.reach
-              else if ref.isTracked then fresh.hiddenSet.elems += ref
-          finally reach = saved
-        case _ =>
-          traverseChildren(t)
-    if ref.isTrackableRef then add.traverse(tp)
-  end addOwnerAsHidden
-
   /** A traverser that adds knownTypes and updates symbol infos */
   def setupTraverser(checker: CheckerAPI) = new TreeTraverserWithPreciseImportContexts:
     import checker.*

From fb45ece52380fca626a302fecdf5c18680a41fd2 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sat, 6 Sep 2025 20:05:55 +0200
Subject: [PATCH 12/12] By default don't include span captures in the
 underlying capset

What is the underlying capture set of a function? CC says the capture set
on the first arrow but we experimented with the capture of the span of the
function instead. This however causes a lot of complications if we want to push
it to a logical conclusion. So we now make it configurable and by default
span capture set is not used.
---
 .../src/dotty/tools/dotc/cc/CaptureSet.scala  |  2 +-
 .../dotty/tools/dotc/cc/CheckCaptures.scala   |  2 +-
 .../src/dotty/tools/dotc/cc/ccConfig.scala    |  5 ++
 library/src/scala/collection/Iterator.scala   |  1 -
 tests/neg-custom-args/captures/eta.check      |  9 ---
 tests/neg-custom-args/captures/eta.scala      |  2 +-
 .../captures/scoped-caps.check                | 61 ++++++-------------
 .../captures/scoped-caps.scala                |  5 +-
 .../captures/scoped-caps2.check               | 16 +----
 .../captures/scoped-caps2.scala               |  4 +-
 tests/neg-custom-args/captures/sep-use2.check | 12 ++--
 .../captures/scoped-caps.scala}               |  4 +-
 12 files changed, 41 insertions(+), 82 deletions(-)
 rename tests/{neg-custom-args/captures/test22.scala => pos-custom-args/captures/scoped-caps.scala} (61%)

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index 0ababe60e743..9eec54ef3dd0 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -1565,7 +1565,7 @@ object CaptureSet:
       // `ref` will not seem subsumed by other capabilities in a `++`.
       universal
     case c: CoreCapability =>
-      ofType(c.underlying, followResult = true)
+      ofType(c.underlying, followResult = ccConfig.useSpanCapset)
 
   /** Capture set of a type
    *  @param followResult  If true, also include capture sets of function results.
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 21567d694bc9..d931cb7df870 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -496,7 +496,7 @@ class CheckCaptures extends Recheck, SymTransformer:
             case _ => c.core match
               case c1: RootCapability => c1.singletonCaptureSet
               case c1: CoreCapability =>
-                CaptureSet.ofType(c1.widen, followResult = true)
+                CaptureSet.ofType(c1.widen, followResult = ccConfig.useSpanCapset)
           capt.println(i"Widen reach $c to $underlying in ${env.owner}")
           underlying.disallowBadRoots(NoSymbol): () =>
             report.error(em"Local capability $c${env.owner.qualString("in")} cannot have `cap` as underlying capture set", tree.srcPos)
diff --git a/compiler/src/dotty/tools/dotc/cc/ccConfig.scala b/compiler/src/dotty/tools/dotc/cc/ccConfig.scala
index 9626d182fa81..57ff55fb5c6e 100644
--- a/compiler/src/dotty/tools/dotc/cc/ccConfig.scala
+++ b/compiler/src/dotty/tools/dotc/cc/ccConfig.scala
@@ -43,6 +43,11 @@ object ccConfig:
    */
   inline val postCheckCapturesets = false
 
+  /** If true take as the underlying capture set of a capability of function type
+   *  the capture set along the span, including capture sets of function results.
+   */
+  inline val useSpanCapset = false
+
   /** If true, do level checking for FreshCap instances */
   def useFreshLevels(using Context): Boolean =
     Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.7`)
diff --git a/library/src/scala/collection/Iterator.scala b/library/src/scala/collection/Iterator.scala
index 2b8b9d45d6e4..4ddef7dcb18f 100644
--- a/library/src/scala/collection/Iterator.scala
+++ b/library/src/scala/collection/Iterator.scala
@@ -9,7 +9,6 @@
  * See the NOTICE file distributed with this work for
  * additional information regarding copyright ownership.
  */
-
 package scala.collection
 
 import scala.language.`2.13`
diff --git a/tests/neg-custom-args/captures/eta.check b/tests/neg-custom-args/captures/eta.check
index 4bd409c35cca..dfce53accd4d 100644
--- a/tests/neg-custom-args/captures/eta.check
+++ b/tests/neg-custom-args/captures/eta.check
@@ -7,12 +7,3 @@
   |         Note that capability f is not included in capture set {}.
   |
   | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/eta.scala:7:7 --------------------------------------------
-7 |       () => { stowaway.apply().apply() }  // error (was ok)
-  |       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-  |       Found:    () ->{stowaway} Unit
-  |       Required: () -> Unit
-  |
-  |       Note that capability stowaway is not included in capture set {}.
-  |
-  | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/eta.scala b/tests/neg-custom-args/captures/eta.scala
index ad4f24342b91..d192d7baedf8 100644
--- a/tests/neg-custom-args/captures/eta.scala
+++ b/tests/neg-custom-args/captures/eta.scala
@@ -4,4 +4,4 @@
          g  // error
        val stowaway: () -> Proc^{f} =
          bar( () => f )  // was error now OK
-       () => { stowaway.apply().apply() }  // error (was ok)
\ No newline at end of file
+       () => { stowaway.apply().apply() }
\ No newline at end of file
diff --git a/tests/neg-custom-args/captures/scoped-caps.check b/tests/neg-custom-args/captures/scoped-caps.check
index e9a421dfc044..141e8ac4a9c6 100644
--- a/tests/neg-custom-args/captures/scoped-caps.check
+++ b/tests/neg-custom-args/captures/scoped-caps.check
@@ -49,14 +49,17 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:12:20 ----------------------------------
 12 |  val _: A^ -> B^ = x => g(x)      // error: g is no longer pure, since it contains the ^ of B
    |                    ^^^^^^^^^
-   |                    Found:    (x: A^) ->{g} B^²
+   |                    Found:    (x: A^) ->'s1 B^²
    |                    Required: A^ -> B^³
    |
-   |                    Note that capability g is not included in capture set {}.
+   |                    Note that capability cap is not included in capture set {cap²}
+   |                    because cap is not visible from cap² in value _$5.
    |
-   |                    where:    ^  refers to the universal root capability
-   |                              ^² refers to a root capability associated with the result type of (x: A^): B^²
-   |                              ^³ refers to a fresh root capability in the type of value _$5
+   |                    where:    ^    refers to the universal root capability
+   |                              ^²   refers to a root capability associated with the result type of (x: A^): B^²
+   |                              ^³   refers to a fresh root capability in the type of value _$5
+   |                              cap  is a root capability associated with the result type of (x: A^): B^²
+   |                              cap² is a fresh root capability in the type of value _$5
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:16:24 ----------------------------------
@@ -75,61 +78,35 @@
    |                                 cap is a root capability associated with the result type of (x: S^): B^²
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:17:24 ----------------------------------
-17 |  val _: (x: S) -> B^ = (x: S) => h(x)  // error: eta expansion fails
-   |                        ^^^^^^^^^^^^^^
-   |                        Found:    (x: S^) ->{h} B^²
-   |                        Required: (x: S^) -> B^³
-   |
-   |                        Note that capability h is not included in capture set {}.
-   |
-   |                        where:    ^  refers to the universal root capability
-   |                                  ^² refers to a root capability associated with the result type of (x: S^): B^²
-   |                                  ^³ refers to a root capability associated with the result type of (x: S^): B^³
-   |
-   | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:21:23 ----------------------------------
-21 |  val _: (x: S) -> S = (x: S) => h2(x)  // error: eta conversion fails since `h2` is now impure (result type S is a capability)
-   |                       ^^^^^^^^^^^^^^^
-   |                       Found:    (x: S^) ->{h2} S^²
-   |                       Required: (x: S^) -> S^³
-   |
-   |                       Note that capability h2 is not included in capture set {}.
-   |
-   |                       where:    ^  refers to the universal root capability
-   |                                 ^² refers to a root capability associated with the result type of (x: S^): S^²
-   |                                 ^³ refers to a root capability associated with the result type of (x: S^): S^³
-   |
-   | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:27:19 ----------------------------------
-27 |  val _: S -> B^ = j               // error
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:26:19 ----------------------------------
+26 |  val _: S -> B^ = j               // error
    |                   ^
    |                   Found:    (j : (x: S) -> B^)
    |                   Required: S^² -> B^³
    |
    |                   Note that capability cap is not included in capture set {cap²}
-   |                   because cap is not visible from cap² in value _$14.
+   |                   because cap is not visible from cap² in value _$13.
    |
    |                   where:    ^    refers to a root capability associated with the result type of (x: S^²): B^
    |                             ^²   refers to the universal root capability
-   |                             ^³   refers to a fresh root capability in the type of value _$14
+   |                             ^³   refers to a fresh root capability in the type of value _$13
    |                             cap  is a root capability associated with the result type of (x: S^²): B^
-   |                             cap² is a fresh root capability in the type of value _$14
+   |                             cap² is a fresh root capability in the type of value _$13
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:28:19 ----------------------------------
-28 |  val _: S -> B^ = x => j(x)       // error
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:27:19 ----------------------------------
+27 |  val _: S -> B^ = x => j(x)       // error
    |                   ^^^^^^^^^
-   |                   Found:    (x: S^) ->'s1 B^²
+   |                   Found:    (x: S^) ->'s2 B^²
    |                   Required: S^ -> B^³
    |
    |                   Note that capability cap is not included in capture set {cap²}
-   |                   because cap is not visible from cap² in value _$15.
+   |                   because cap is not visible from cap² in value _$14.
    |
    |                   where:    ^    refers to the universal root capability
    |                             ^²   refers to a root capability associated with the result type of (x: S^): B^²
-   |                             ^³   refers to a fresh root capability in the type of value _$15
+   |                             ^³   refers to a fresh root capability in the type of value _$14
    |                             cap  is a root capability associated with the result type of (x: S^): B^²
-   |                             cap² is a fresh root capability in the type of value _$15
+   |                             cap² is a fresh root capability in the type of value _$14
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/scoped-caps.scala b/tests/neg-custom-args/captures/scoped-caps.scala
index d285b7ef79f5..1f985040c2ca 100644
--- a/tests/neg-custom-args/captures/scoped-caps.scala
+++ b/tests/neg-custom-args/captures/scoped-caps.scala
@@ -14,12 +14,11 @@ def test(io: Object^): Unit =
 
   val h: S -> B^ = ???
   val _: (x: S) -> B^ = h          // error: direct conversion fails
-  val _: (x: S) -> B^ = (x: S) => h(x)  // error: eta expansion fails
+  val _: (x: S) -> B^ = (x: S) => h(x)  // eta expansion is ok
 
   val h2: S -> S = ???
   val _: (x: S) -> S = h2               // direct conversion OK for shared S
-  val _: (x: S) -> S = (x: S) => h2(x)  // error: eta conversion fails since `h2` is now impure (result type S is a capability)
-  val _: (x: S) ->{h2} S = (x: S) => h2(x) // eta expansion OK
+  val _: (x: S) -> S = (x: S) => h2(x)  // eta conversion is also OK
 
   val j: (x: S) -> B^ = ???
   val _: (x: S) -> B^ = j
diff --git a/tests/neg-custom-args/captures/scoped-caps2.check b/tests/neg-custom-args/captures/scoped-caps2.check
index 1a885b4689d3..ad4acc726fc4 100644
--- a/tests/neg-custom-args/captures/scoped-caps2.check
+++ b/tests/neg-custom-args/captures/scoped-caps2.check
@@ -7,7 +7,7 @@
   |                   Note that the existential capture root in C^
   |                   cannot subsume the capability cap..
   |
-  |                   Note that capability cap is not included in capture set {cap²}.
+  |                   Note that capability cap² is not included in capture set {cap³}.
   |
   |                   where:    =>   refers to a fresh root capability in the type of value b
   |                             =>²  refers to a fresh root capability in the type of value _$1
@@ -15,6 +15,7 @@
   |                             ^²   refers to a root capability associated with the result type of (x: C^): C^²
   |                             cap  is a fresh root capability classified as SharedCapability in the type of value b
   |                             cap² is a fresh root capability in the type of value b
+  |                             cap³ is a fresh root capability in the type of value _$1
   |
   | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps2.scala:6:18 ----------------------------------
@@ -65,19 +66,6 @@
    |                  cap² is a fresh root capability classified as SharedCapability in the type of value _$6
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps2.scala:15:23 ---------------------------------
-15 |  val _: (x: C) -> C = (x: C) => b(x) // error
-   |                       ^^^^^^^^^^^^^^
-   |                       Found:    (x: C^) ->{b} C^²
-   |                       Required: (x: C^) -> C^³
-   |
-   |                       Note that capability b is not included in capture set {}.
-   |
-   |                       where:    ^  refers to the universal root capability
-   |                                 ^² refers to a root capability associated with the result type of (x: C^): C^²
-   |                                 ^³ refers to a root capability associated with the result type of (x: C^): C^³
-   |
-   | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps2.scala:16:29 ---------------------------------
 16 |  val _: C -> C = (x: C) => a(x) // error
    |                            ^^^^
diff --git a/tests/neg-custom-args/captures/scoped-caps2.scala b/tests/neg-custom-args/captures/scoped-caps2.scala
index 527debb57378..751ad9bdc9c0 100644
--- a/tests/neg-custom-args/captures/scoped-caps2.scala
+++ b/tests/neg-custom-args/captures/scoped-caps2.scala
@@ -4,7 +4,7 @@ def test1(c: C) =
   val b: C => C = ???
   val _: (x: C) => C = b // error
   val _: C => C = a // error
-  val _: (x: C) => C = (x: C) => b(x) // OK
+  val _: (x: C) => C = (x: C) => (b(x): C) // OK
   val _: C => C = (x: C) => a(x) // error
 
 def test2(c: C) =
@@ -12,6 +12,6 @@ def test2(c: C) =
   val b: C -> C = ???
   val _: (x: C) -> C = b // OK
   val _: C -> C = a // error
-  val _: (x: C) -> C = (x: C) => b(x) // error
+  val _: (x: C) -> C = (x: C) => b(x) // ok
   val _: C -> C = (x: C) => a(x) // error
 
diff --git a/tests/neg-custom-args/captures/sep-use2.check b/tests/neg-custom-args/captures/sep-use2.check
index 8fec0e3bdd83..2be46304db34 100644
--- a/tests/neg-custom-args/captures/sep-use2.check
+++ b/tests/neg-custom-args/captures/sep-use2.check
@@ -47,15 +47,15 @@
 24 |    { f(c) } // error
    |        ^
    |Separation failure: argument of type  (c : Object^)
-   |to a function of type Object^ ->{c} Object^{f*}
+   |to a function of type Object^ ->{f} Object^{f*}
    |corresponds to capture-polymorphic formal parameter v1 of type  Object^²
    |and hides capabilities  {c}.
    |Some of these overlap with the captures of the function prefix.
    |
    |  Hidden set of current argument        : {c}
    |  Hidden footprint of current argument  : {c}
-   |  Capture set of function prefix        : {c, f*}
-   |  Footprint set of function prefix      : {c, f*}
+   |  Capture set of function prefix        : {f*}
+   |  Footprint set of function prefix      : {f*, c}
    |  The two sets overlap at               : {c}
    |
    |where:    ^  refers to a fresh root capability in the type of parameter c
@@ -69,15 +69,15 @@
 28 |    { f(c) } // error
    |        ^
    |Separation failure: argument of type  (c : Object^)
-   |to a function of type Object^ ->{c} Object^{f*}
+   |to a function of type Object^ ->{f} Object^{f*}
    |corresponds to capture-polymorphic formal parameter v1 of type  Object^²
    |and hides capabilities  {c}.
    |Some of these overlap with the captures of the function prefix.
    |
    |  Hidden set of current argument        : {c}
    |  Hidden footprint of current argument  : {c}
-   |  Capture set of function prefix        : {c, f*}
-   |  Footprint set of function prefix      : {c, f*}
+   |  Capture set of function prefix        : {f*}
+   |  Footprint set of function prefix      : {f*, c}
    |  The two sets overlap at               : {c}
    |
    |where:    ^  refers to a fresh root capability in the type of parameter c
diff --git a/tests/neg-custom-args/captures/test22.scala b/tests/pos-custom-args/captures/scoped-caps.scala
similarity index 61%
rename from tests/neg-custom-args/captures/test22.scala
rename to tests/pos-custom-args/captures/scoped-caps.scala
index 6b83ac278648..f266cc65a30b 100644
--- a/tests/neg-custom-args/captures/test22.scala
+++ b/tests/pos-custom-args/captures/scoped-caps.scala
@@ -5,8 +5,8 @@ class S extends caps.SharedCapability
 def test(io: Object^): Unit =
   val h2: S -> S = ???
   val _: (x: S) -> S = h2               // direct conversion OK for shared S
-  val _: (x: S) -> S = (x: S) => h2(x)  // error: eta conversion fails since `h2` is now impure (result type S is a capability)
-  val _: (x: S) ->{h2} S =
+  val _: (x: S) -> S = (x: S) => h2(x)  // eta expansion also ok
+  val _: (x: S) -> S =
     (x: S) =>
       val y = h2(x) // eta expansion OK
       y