From c07f6fa75cb42d787ce5f3c811dcc477c8c9619d Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Tue, 9 Sep 2025 09:22:06 +0200
Subject: [PATCH 1/7] Don't allow instantiated ResultCaps to subsume anything

We map them to fresh caps but their hidden sets should not accept new elements.
---
 compiler/src/dotty/tools/dotc/cc/Capability.scala  | 8 +++++++-
 compiler/src/dotty/tools/dotc/cc/CaptureSet.scala  | 7 +++++--
 tests/neg-custom-args/captures/frozen-result.scala | 9 +++++++++
 3 files changed, 21 insertions(+), 3 deletions(-)
 create mode 100644 tests/neg-custom-args/captures/frozen-result.scala

diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala
index 77c67dff5a00..0476553558ef 100644
--- a/compiler/src/dotty/tools/dotc/cc/Capability.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala
@@ -1033,7 +1033,13 @@ object Capabilities:
       override def mapCapability(c: Capability, deep: Boolean) = c match
         case c @ ResultCap(binder) =>
           if localBinders.contains(binder) then c // keep bound references
-          else seen.getOrElseUpdate(c, FreshCap(origin)) // map free references to FreshCap
+          else
+            // Create a fresh skolem that does not subsume anything
+            def freshSkolem =
+              val c = FreshCap(origin)
+              c.hiddenSet.markSolved(provisional = false)
+              c
+            seen.getOrElseUpdate(c, freshSkolem) // map free references to FreshCap
         case _ => super.mapCapability(c, deep)
     end subst
 
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index 9eec54ef3dd0..8c26011a538e 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -1206,6 +1206,7 @@ object CaptureSet:
       if alias ne this then alias.add(elem)
       else
         def addToElems() =
+          assert(!isConst)
           includeElem(elem)
           deps.foreach: dep =>
             assert(dep != this)
@@ -1378,8 +1379,10 @@ object CaptureSet:
      *  but the special state VarState.Separate overrides this.
      */
     def addHidden(hidden: HiddenSet, elem: Capability)(using Context): Boolean =
-      hidden.add(elem)(using ctx, this)
-      true
+      if hidden.isConst then false
+      else
+        hidden.add(elem)(using ctx, this)
+        true
 
     /** If root1 and root2 belong to the same binder but have different originalBinders
      *  it means that one of the roots was mapped to the binder of the other by a
diff --git a/tests/neg-custom-args/captures/frozen-result.scala b/tests/neg-custom-args/captures/frozen-result.scala
new file mode 100644
index 000000000000..e82d751c0ab9
--- /dev/null
+++ b/tests/neg-custom-args/captures/frozen-result.scala
@@ -0,0 +1,9 @@
+class B
+
+def Test(consume b1: B^, consume b2: B^) =
+  def f(): B^ = B()
+  var x: B^ = f()
+  x = b1 // error separation but should be OK, see #23889
+  var y = f()
+  y = b2 // error
+

From dcba1d841462171b4de6511bb85f24dc1055a5c1 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sat, 13 Sep 2025 13:49:14 +0200
Subject: [PATCH 2/7] Debug hooks for capture set inference

Allows us to diagnose when a specific variable is created or obtains
new elements.
---
 .../src/dotty/tools/dotc/cc/Capability.scala  |  1 +
 .../src/dotty/tools/dotc/cc/CaptureSet.scala  | 24 ++++++++++++++++---
 .../tools/dotc/printing/PlainPrinter.scala    |  6 +++--
 3 files changed, 26 insertions(+), 5 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala
index 0476553558ef..e50422aa5a3f 100644
--- a/compiler/src/dotty/tools/dotc/cc/Capability.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala
@@ -168,6 +168,7 @@ object Capabilities:
       case _ => false
 
     /** Is this fresh cap at the right level to be able to subsume `ref`?
+     *  Only outer freshes can be subsumed.
      */
     def acceptsLevelOf(ref: Capability)(using Context): Boolean =
       if ccConfig.useFreshLevels && !CCState.collapseFresh then
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index 8c26011a538e..652768433a15 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -394,7 +394,13 @@ sealed abstract class CaptureSet extends Showable:
           if mappedElems == elems then this
           else Const(mappedElems)
         else if ccState.mapFutureElems then
-          def unfused = BiMapped(asVar, tm, mappedElems)
+          def unfused =
+            if debugVars then
+              try BiMapped(asVar, tm, mappedElems)
+              catch case ex: AssertionError =>
+                println(i"error while mapping $this")
+                throw ex
+            else BiMapped(asVar, tm, mappedElems)
           this match
             case self: BiMapped => self.bimap.fuse(tm) match
               case Some(fused: BiTypeMap) => BiMapped(self.source, fused, mappedElems)
@@ -652,8 +658,12 @@ object CaptureSet:
     override def toString = "<fluid>"
   end Fluid
 
+  /** If true emit info when var with id debugTarget is created or gets a new element */
+  inline val debugVars = false
+  inline val debugTarget = 22
+
   /** The subclass of captureset variables with given initial elements */
-  class Var(initialOwner: Symbol = NoSymbol, initialElems: Refs = emptyRefs, val level: Level = undefinedLevel, underBox: Boolean = false)(using @constructorOnly ictx: Context) extends CaptureSet:
+  class Var(initialOwner: Symbol = NoSymbol, initialElems: Refs = emptyRefs, val level: Level = undefinedLevel, underBox: Boolean = false)(using /*@constructorOnly*/ ictx: Context) extends CaptureSet:
 
     override def owner = initialOwner
 
@@ -678,8 +688,14 @@ object CaptureSet:
     /** The elements currently known to be in the set */
     protected var myElems: Refs = initialElems
 
+    if debugVars && id == debugTarget then
+      println(i"###INIT ELEMS of $id to $initialElems")
+
     def elems: Refs = myElems
-    def elems_=(refs: Refs): Unit = myElems = refs
+    def elems_=(refs: Refs): Unit =
+      if debugVars && id == debugTarget then
+        println(i"###SET ELEMS of $id to $refs")
+      myElems = refs
 
     /** The sets currently known to be dependent sets (i.e. new additions to this set
      *  are propagated to these dependent sets.)
@@ -762,6 +778,8 @@ object CaptureSet:
 
     protected def includeElem(elem: Capability)(using Context): Unit =
       if !elems.contains(elem) then
+        if debugVars && id == debugTarget then
+          println(i"###INCLUDE $elem in $this")
         elems += elem
         TypeComparer.logUndoAction: () =>
           elems -= elem
diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
index 4a23f00f3c53..042a15f5ba0b 100644
--- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
@@ -172,13 +172,15 @@ class PlainPrinter(_ctx: Context) extends Printer {
     then cs.toString
     else if cs == CaptureSet.Fluid then "<fluid>"
     else
+      val idTxt = Str(s"#${cs.asVar.id}").provided(showUniqueIds && !cs.isConst)
       val core: Text =
-        if !cs.isConst && cs.elems.isEmpty then cs.asVar.repr.show
+        if !cs.isConst && cs.elems.isEmpty
+        then cs.asVar.repr.show ~ idTxt
         else
           Str("'").provided(ccVerbose && !cs.isConst)
            ~ "{" ~ Text(cs.processElems(_.toList.map(toTextCapability)), ", ") ~ "}"
            ~ Str(".reader").provided(ccVerbose && cs.mutability == Mutability.Reader)
-           ~ Str(s"#${cs.asVar.id}").provided(showUniqueIds && !cs.isConst)
+           ~ idTxt
       core ~ cs.optionalInfo
 
   private def toTextRetainedElem(ref: Type): Text = ref match

From 5530b460eec8370d025757e4f005dba956d87c41 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Tue, 16 Sep 2025 16:27:42 +0200
Subject: [PATCH 3/7] Switch level checking for capsets to owner-based scheme

The previous scheme was too coarse since it treated all vaks in a method the same.
---
 .../src/dotty/tools/dotc/cc/Capability.scala  |  6 ++
 .../src/dotty/tools/dotc/cc/CaptureSet.scala  | 28 +++++++-
 .../dotty/tools/dotc/cc/CheckCaptures.scala   | 46 +++++++++----
 tests/neg-custom-args/captures/boundary.check | 19 +++++-
 tests/neg-custom-args/captures/boundary.scala |  2 +-
 tests/neg-custom-args/captures/branding.scala |  6 +-
 .../captures/capset-members4.scala            | 10 +--
 tests/neg-custom-args/captures/i15772.check   |  8 +--
 tests/neg-custom-args/captures/i15922.scala   |  4 +-
 tests/neg-custom-args/captures/i21614.check   | 19 ++++--
 tests/neg-custom-args/captures/i21614.scala   |  2 +-
 tests/neg-custom-args/captures/i23207.check   |  8 +--
 .../captures/lazylists-exceptions.check       | 18 ++---
 .../captures/lazylists-exceptions.scala       |  4 +-
 tests/neg-custom-args/captures/leaky.check    |  8 +--
 tests/neg-custom-args/captures/real-try.check | 68 +++++++++----------
 tests/neg-custom-args/captures/real-try.scala | 12 ++--
 .../captures/sep-counter.check                |  6 +-
 .../neg-custom-args/captures/sep-pairs.check  |  6 +-
 tests/neg-custom-args/captures/vars.check     |  6 +-
 20 files changed, 177 insertions(+), 109 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala
index e50422aa5a3f..d4b1a41755ef 100644
--- a/compiler/src/dotty/tools/dotc/cc/Capability.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala
@@ -484,6 +484,12 @@ object Capabilities:
       case self: FreshCap => self.hiddenSet.owner
       case _ /* : GlobalCap | ResultCap | ParamRef */ => NoSymbol
 
+    final def visibility(using Context): Symbol = this match
+      case self: FreshCap => ccOwner.enclosingMethodOrClass
+      case _ =>
+        val vis = ccOwner
+        if vis.is(Param) then vis.owner else vis
+
     /** The symbol that represents the level closest-enclosing ccOwner.
      *  Symbols representing levels are
      *   - class symbols, but not inner (non-static) module classes
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index 652768433a15..4fa037c31617 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -660,7 +660,7 @@ object CaptureSet:
 
   /** If true emit info when var with id debugTarget is created or gets a new element */
   inline val debugVars = false
-  inline val debugTarget = 22
+  inline val debugTarget = 1745
 
   /** The subclass of captureset variables with given initial elements */
   class Var(initialOwner: Symbol = NoSymbol, initialElems: Refs = emptyRefs, val level: Level = undefinedLevel, underBox: Boolean = false)(using /*@constructorOnly*/ ictx: Context) extends CaptureSet:
@@ -690,6 +690,7 @@ object CaptureSet:
 
     if debugVars && id == debugTarget then
       println(i"###INIT ELEMS of $id to $initialElems")
+      assert(false)
 
     def elems: Refs = myElems
     def elems_=(refs: Refs): Unit =
@@ -832,7 +833,7 @@ object CaptureSet:
             case _ => foldOver(b, t)
       find(false, binder)
 
-    def levelOK(elem: Capability)(using Context): Boolean = elem match
+    def levelOKold(elem: Capability)(using Context): Boolean = elem match
       case _: FreshCap =>
         !level.isDefined
         || ccState.symLevel(elem.ccOwner) <= level
@@ -865,6 +866,29 @@ object CaptureSet:
       case _ =>
         true
 
+    def levelOKnew(elem: Capability)(using Context): Boolean = elem match
+      case elem @ ResultCap(binder) =>
+        rootLimit == null && (this.isInstanceOf[BiMapped] || isPartOf(binder.resType))
+      case GlobalCap =>
+        rootLimit == null
+      case elem: ParamRef =>
+        this.isInstanceOf[BiMapped] || isPartOf(elem.binder.resType)
+      case _ =>
+        if owner.exists then
+          val elemVis = elem.visibility
+          !elemVis.isProperlyContainedIn(owner)
+        else true
+
+    inline val debugLevelChecking = false
+
+    def levelOK(elem: Capability)(using Context): Boolean =
+      val now = levelOKnew(elem)
+      if debugLevelChecking then
+        val was = levelOKold(elem)
+        if was != now then
+          println(i"LEVEL DIFF for $this / $getClass in ${owner.ownersIterator.toList} and elem $elem in ${elem.ccOwner}, was $was")
+      now
+
     def addDependent(cs: CaptureSet)(using Context, VarState): Boolean =
       (cs eq this)
       || cs.isUniversal
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index d931cb7df870..3f5e1b276253 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -28,6 +28,7 @@ import reporting.{trace, Message, OverrideError}
 import Annotations.Annotation
 import Capabilities.*
 import util.common.alwaysTrue
+import scala.annotation.constructorOnly
 
 /** The capture checker */
 object CheckCaptures:
@@ -56,7 +57,13 @@ object CheckCaptures:
       kind: EnvKind,
       captured: CaptureSet,
       outer0: Env | Null,
-      nestedClosure: Symbol = NoSymbol):
+      nestedClosure: Symbol = NoSymbol)(using @constructorOnly ictx: Context):
+
+    assert(definesEnv(owner))
+    captured match
+      case captured: CaptureSet.Var => assert(captured.owner == owner,
+        i"owner discrepancy env owner = $owner but its captureset $captured has owner ${captured.owner}")
+      case _ =>
 
     def outer = outer0.nn
 
@@ -71,6 +78,9 @@ object CheckCaptures:
         res
   end Env
 
+  def definesEnv(sym: Symbol)(using Context): Boolean =
+    sym.is(Method) || sym.isClass
+
   /** Similar normal substParams, but this is an approximating type map that
    *  maps parameters in contravariant capture sets to the empty set.
    */
@@ -364,21 +374,28 @@ class CheckCaptures extends Recheck, SymTransformer:
       assert(cs1.subCaptures(cs2), i"$cs1 is not a subset of $cs2")
 
     /** If `res` is not CompareResult.OK, report an error */
-    def checkOK(res: TypeComparer.CompareResult, prefix: => String, added: Capability | CaptureSet, target: CaptureSet, pos: SrcPos, provenance: => String = "")(using Context): Unit =
+    def checkOK(res: TypeComparer.CompareResult,
+        prefix: => String,
+        added: Capability | CaptureSet,
+        target: CaptureSet,
+        pos: SrcPos,
+        provenance: => String = "")(using Context): Unit =
       res match
         case TypeComparer.CompareResult.Fail(notes) =>
-          val ((res: IncludeFailure) :: Nil, otherNotes) =
-            notes.partition(_.isInstanceOf[IncludeFailure]): @unchecked
+          val (includeFailures, otherNotes) = notes.partition(_.isInstanceOf[IncludeFailure])
+          val realTarget = includeFailures match
+            case (fail: IncludeFailure) :: _ => fail.cs
+            case _ => target
           def msg(provisional: Boolean) =
             def toAdd: String = errorNotes(otherNotes).toAdd.mkString
             def descr: String =
-              val d = res.cs.description
+              val d = realTarget.description
               if d.isEmpty then provenance else ""
             def kind = if provisional then "previously estimated\n" else "allowed "
-            em"$prefix included in the ${kind}capture set ${res.cs}$descr$toAdd"
+            em"$prefix included in the ${kind}capture set $realTarget$descr$toAdd"
           target match
             case target: CaptureSet.Var
-            if res.cs.isProvisionallySolved =>
+            if realTarget.isProvisionallySolved =>
               report.warning(
                 msg(provisional = true)
                   .prepend(i"Another capture checking run needs to be scheduled because\n"),
@@ -413,7 +430,7 @@ class CheckCaptures extends Recheck, SymTransformer:
     def capturedVars(sym: Symbol)(using Context): CaptureSet =
       myCapturedVars.getOrElseUpdate(sym,
         if sym.isTerm || !sym.owner.isStaticOwner
-        then CaptureSet.Var(sym.owner, level = ccState.symLevel(sym))
+        then CaptureSet.Var(sym, level = ccState.symLevel(sym))
         else CaptureSet.empty)
 
 // ---- Record Uses with MarkFree ----------------------------------------------------
@@ -535,6 +552,7 @@ class CheckCaptures extends Recheck, SymTransformer:
               then avoidLocalCapability(c, env, lastEnv)
               else avoidLocalReachCapability(c, env)
             isVisible
+          //println(i"Include call or box capture $included from $cs in ${env.owner}/${env.captured}/${env.captured.owner}/${env.kind}")
           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
@@ -1151,11 +1169,13 @@ class CheckCaptures extends Recheck, SymTransformer:
           .map(e => (e.owner, e))
           .toMap
         def restoreEnvFor(sym: Symbol): Env =
-          val localSet = capturedVars(sym)
-          if localSet eq CaptureSet.empty then rootEnv
-          else envForOwner.get(sym) match
-            case Some(e) => e
-            case None => Env(sym, EnvKind.Regular, localSet, restoreEnvFor(sym.owner))
+          if definesEnv(sym) then
+            val localSet = capturedVars(sym)
+            if localSet eq CaptureSet.empty then rootEnv
+            else envForOwner.get(sym) match
+              case Some(e) => e
+              case None => Env(sym, EnvKind.Regular, localSet, restoreEnvFor(sym.owner))
+          else restoreEnvFor(sym.owner)
         curEnv = restoreEnvFor(sym.owner)
         capt.println(i"Complete $sym in ${curEnv.outersIterator.toList.map(_.owner)}")
         try recheckDef(tree, sym)
diff --git a/tests/neg-custom-args/captures/boundary.check b/tests/neg-custom-args/captures/boundary.check
index dd0b6716adc7..0cac2ec2f60d 100644
--- a/tests/neg-custom-args/captures/boundary.check
+++ b/tests/neg-custom-args/captures/boundary.check
@@ -12,7 +12,7 @@
    |          cap  is a fresh root capability classified as Control created in value local when constructing Capability instance scala.util.boundary.Label[Object^'s1]
    |          cap² is the universal root capability
  6 |      boundary[Unit]: l2 ?=>
- 7 |        boundary.break(l2)(using l1)
+ 7 |        boundary.break(l2)(using l1) // error
  8 |      ???
    |--------------------------------------------------------------------------------------------------------------------
    |Inline stack trace
@@ -23,6 +23,21 @@
     --------------------------------------------------------------------------------------------------------------------
    |
    | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/boundary.scala:7:33 --------------------------------------
+7 |        boundary.break(l2)(using l1) // error
+  |                                 ^^
+  |Found:    (local : scala.util.boundary.Label[Object^])
+  |Required: scala.util.boundary.Label[scala.util.boundary.Label[Unit]^²]^³
+  |
+  |Note that capability cap is not included in capture set {cap²}.
+  |
+  |where:    ^    refers to the universal root capability
+  |          ^²   refers to a fresh root capability classified as Control in the type of value local²
+  |          ^³   refers to a fresh root capability classified as Control created in package <empty> when checking argument to parameter label of method break
+  |          cap  is a fresh root capability classified as Control in the type of value local
+  |          cap² is a fresh root capability classified as Control created in package <empty> when checking argument to parameter label of method break
+  |
+  | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/boundary.scala:5:4 ---------------------------------------
  4 |  boundary[AnyRef^]:
  5 |    l1 ?=> // error // error
@@ -37,7 +52,7 @@
    |            cap  is a fresh root capability created in package <empty>
    |            cap² is the universal root capability
  6 |      boundary[Unit]: l2 ?=>
- 7 |        boundary.break(l2)(using l1)
+ 7 |        boundary.break(l2)(using l1) // error
  8 |      ???
    |--------------------------------------------------------------------------------------------------------------------
    |Inline stack trace
diff --git a/tests/neg-custom-args/captures/boundary.scala b/tests/neg-custom-args/captures/boundary.scala
index 9792a0e49fa3..adce5e0d68e2 100644
--- a/tests/neg-custom-args/captures/boundary.scala
+++ b/tests/neg-custom-args/captures/boundary.scala
@@ -4,5 +4,5 @@ object test:
   boundary[AnyRef^]:
     l1 ?=> // error // error
       boundary[Unit]: l2 ?=>
-        boundary.break(l2)(using l1)
+        boundary.break(l2)(using l1) // error
       ???
diff --git a/tests/neg-custom-args/captures/branding.scala b/tests/neg-custom-args/captures/branding.scala
index 9d5ad25e82bc..744fdf065d91 100644
--- a/tests/neg-custom-args/captures/branding.scala
+++ b/tests/neg-custom-args/captures/branding.scala
@@ -22,14 +22,14 @@ def main() =
   val untrustedLogger: Logger^ = ???
   val untrustedChannel: Channel[String]^ = ???
 
-  runSecure: () =>
+  runSecure: () => // error (???, arose after changing level checking)
     trustedLogger.log("Hello from trusted code") // ok
 
-  runSecure: () =>
+  runSecure: () => // error (???, arose after changing level checking)
     trustedChannel.send("I can send")
     trustedLogger.log(trustedChannel.recv()) // ok
 
-  runSecure: () =>
+  runSecure: () => // error (???, arose after changing level checking)
     "I am pure"                             // ok
 
   runSecure: () => // error
diff --git a/tests/neg-custom-args/captures/capset-members4.scala b/tests/neg-custom-args/captures/capset-members4.scala
index 698ef28c1fb4..338e0e99acb2 100644
--- a/tests/neg-custom-args/captures/capset-members4.scala
+++ b/tests/neg-custom-args/captures/capset-members4.scala
@@ -11,8 +11,8 @@ def test =
     type C^ >: {z,x} <: {x,y,z}
 
   val foo: Foo = ???
-  onlyWithZ[{foo.C}]
-  onlyWithZ[{z}]
-  onlyWithZ[{x,z}]
-  onlyWithZ[{x,y,z}]
-  onlyWithZ[{x,y}] // error
\ No newline at end of file
+  onlyWithZ[{foo.C}] // error
+  onlyWithZ[{z}]     // error
+  onlyWithZ[{x,z}]   // error
+  onlyWithZ[{x,y,z}] // error
+  onlyWithZ[{x,y}]   // error
\ No newline at end of file
diff --git a/tests/neg-custom-args/captures/i15772.check b/tests/neg-custom-args/captures/i15772.check
index b167580f548c..c7644791925b 100644
--- a/tests/neg-custom-args/captures/i15772.check
+++ b/tests/neg-custom-args/captures/i15772.check
@@ -5,8 +5,8 @@
 -- Error: tests/neg-custom-args/captures/i15772.scala:22:46 ------------------------------------------------------------
 22 |    val boxed1 : ((C^) => Unit) -> Unit = box1(c)  // error
    |                                          ^^^^^^^
-   |C^ => Unit cannot be box-converted to C{val arg: C^²}^{c} ->{cap, c} Unit
-   |since the additional capture set {c} resulting from box conversion is not allowed in C{val arg: C^²}^{c} => Unit
+   |C^ => Unit cannot be box-converted to C{val arg: C^²}^{c} ->{cap, x} Unit
+   |since the additional capture set {x} resulting from box conversion is not allowed in C{val arg: C^²}^{c} => Unit
    |
    |where:    =>  refers to the universal root capability
    |          ^   refers to the universal root capability
@@ -15,8 +15,8 @@
 -- Error: tests/neg-custom-args/captures/i15772.scala:29:35 ------------------------------------------------------------
 29 |    val boxed2 : Observe[C^] = box2(c)  // error
    |                               ^^^^^^^
-   |C^ => Unit cannot be box-converted to C{val arg: C^²}^{c} ->{cap, c} Unit
-   |since the additional capture set {c} resulting from box conversion is not allowed in C{val arg: C^²}^{c} => Unit
+   |C^ => Unit cannot be box-converted to C{val arg: C^²}^{c} ->{cap, x} Unit
+   |since the additional capture set {x} resulting from box conversion is not allowed in C{val arg: C^²}^{c} => Unit
    |
    |where:    =>  refers to the universal root capability
    |          ^   refers to the universal root capability
diff --git a/tests/neg-custom-args/captures/i15922.scala b/tests/neg-custom-args/captures/i15922.scala
index b8bcc346ef81..4fb4e140d2b7 100644
--- a/tests/neg-custom-args/captures/i15922.scala
+++ b/tests/neg-custom-args/captures/i15922.scala
@@ -13,6 +13,6 @@ def withCap[X](op: (Cap^) => X): X = {
 def leaking(c: Cap^): Id[Cap^{c}] = mkId(c)
 
 def test =
-  val ll = (c: Cap^) => leaking(c)
-  val bad1 = withCap(ll)       // error
+  val ll = (c: Cap^) => leaking(c)  // error
+  val bad1 = withCap(ll)
   val bad2 = withCap(leaking)  // error
diff --git a/tests/neg-custom-args/captures/i21614.check b/tests/neg-custom-args/captures/i21614.check
index f7938c16b9b5..89b9a4b216c1 100644
--- a/tests/neg-custom-args/captures/i21614.check
+++ b/tests/neg-custom-args/captures/i21614.check
@@ -1,5 +1,5 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:12:33 ---------------------------------------
-12 |  files.map((f: F) => new Logger(f)) // error, Q: can we make this pass (see #19076)?
+12 |  files.map((f: F) => new Logger(f)) // error // error, Q: can we make this pass (see #19076)?
    |                                 ^
    |Found:    (f : F)
    |Required: File^
@@ -11,16 +11,25 @@
    |          cap² is a fresh root capability classified as SharedCapability created in anonymous function of type (f²: F): Logger when checking argument to parameter f of constructor Logger
    |
    | longer explanation available when compiling with `-explain`
+-- Error: tests/neg-custom-args/captures/i21614.scala:12:8 -------------------------------------------------------------
+12 |  files.map((f: F) => new Logger(f)) // error // error, Q: can we make this pass (see #19076)?
+   |  ^^^^^^^^^
+   |Type variable U of method map cannot be instantiated to Logger{val f: File^'s1}^{cap.rd} since
+   |that type captures the root capability `cap`.
+   |This is often caused by a local capability in an argument of method map
+   |leaking as part of its result.
+   |
+   |where:    cap is a root capability associated with the result type of (f²: F^{files*}): Logger{val f: File^'s1}^'s2
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:15:12 ---------------------------------------
 15 |  files.map(new Logger(_)) // error, Q: can we improve the error message?
    |            ^^^^^^^^^^^^^
-   |Found:    (_$1: File^'s1) ->{C} Logger{val f: File^{_$1}}^{cap.rd, _$1}
-   |Required: File^{C} => Logger{val f: File^'s2}^'s3
+   |Found:    (_$1: File^'s3) ->{C} Logger{val f: File^{_$1}}^{cap.rd, _$1}
+   |Required: File^{C} => Logger{val f: File^'s4}^'s5
    |
    |Note that capability C is not classified as trait SharedCapability, therefore it
-   |cannot be included in capture set 's1 of parameter _$1 of SharedCapability elements.
+   |cannot be included in capture set 's3 of parameter _$1 of SharedCapability elements.
    |
    |where:    =>  refers to a fresh root capability created in method mkLoggers2 when checking argument to parameter f of method map
-   |          cap is a root capability associated with the result type of (_$1: File^'s1): Logger{val f: File^{_$1}}^{cap.rd, _$1}
+   |          cap is a root capability associated with the result type of (_$1: File^'s3): Logger{val f: File^{_$1}}^{cap.rd, _$1}
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/i21614.scala b/tests/neg-custom-args/captures/i21614.scala
index 11929f2414db..54e3ea863677 100644
--- a/tests/neg-custom-args/captures/i21614.scala
+++ b/tests/neg-custom-args/captures/i21614.scala
@@ -9,7 +9,7 @@ trait File extends SharedCapability
 class Logger(f: File^) extends SharedCapability // <- will work if we remove the extends clause
 
 def mkLoggers1[F <: File^](files: List[F]): List[Logger^] =
-  files.map((f: F) => new Logger(f)) // error, Q: can we make this pass (see #19076)?
+  files.map((f: F) => new Logger(f)) // error // error, Q: can we make this pass (see #19076)?
 
 def mkLoggers2[C^](files: List[File^{C}]): List[Logger^] =
   files.map(new Logger(_)) // error, Q: can we improve the error message?
diff --git a/tests/neg-custom-args/captures/i23207.check b/tests/neg-custom-args/captures/i23207.check
index 626655686d87..d76ae4d39af1 100644
--- a/tests/neg-custom-args/captures/i23207.check
+++ b/tests/neg-custom-args/captures/i23207.check
@@ -19,18 +19,18 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i23207.scala:19:2 ----------------------------------------
 19 |  c // error
    |  ^
-   |  Found:    A^{c}
+   |  Found:    A^{io}
    |  Required: A
    |
-   |  Note that capability c is not included in capture set {}.
+   |  Note that capability io 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}
+   |  Found:    A^{io}
    |  Required: A
    |
-   |  Note that capability c is not included in capture set {}.
+   |  Note that capability io is not included in capture set {}.
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/lazylists-exceptions.check b/tests/neg-custom-args/captures/lazylists-exceptions.check
index a60984fac608..0f31ab58cca6 100644
--- a/tests/neg-custom-args/captures/lazylists-exceptions.check
+++ b/tests/neg-custom-args/captures/lazylists-exceptions.check
@@ -1,13 +1,13 @@
--- Error: tests/neg-custom-args/captures/lazylists-exceptions.scala:36:2 -----------------------------------------------
-36 |  try // error
-   |  ^
-   |  The result of `try` cannot have type LazyList[Int]^ since
-   |  that type captures the root capability `cap`.
-   |  This is often caused by a locally generated exception capability leaking as part of its result.
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylists-exceptions.scala:37:17 -------------------------
+37 |    tabulate(10) { i =>  // error
+   |    ^
+   |    Found:    LazyList[Int]^{canThrow$1}
+   |    Required: LazyList[Int]^'s1
    |
-   |  where:    ^ refers to a fresh root capability classified as Control in the type of given instance canThrow$1
-37 |    tabulate(10) { i =>
+   |    Note that capability canThrow$1, defined in method try$1
+   |    cannot be included in outer capture set 's1 of method problem.
 38 |      if i > 9 then throw Ex1()
 39 |      i * i
 40 |    }
-41 |  catch case ex: Ex1 => LazyNil
+   |
+   | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/lazylists-exceptions.scala b/tests/neg-custom-args/captures/lazylists-exceptions.scala
index 295147f7f3c5..e09386712528 100644
--- a/tests/neg-custom-args/captures/lazylists-exceptions.scala
+++ b/tests/neg-custom-args/captures/lazylists-exceptions.scala
@@ -33,8 +33,8 @@ def tabulate[A](n: Int)(gen: Int => A): LazyList[A]^{gen} =
 class Ex1 extends Exception
 
 def problem =
-  try // error
-    tabulate(10) { i =>
+  try
+    tabulate(10) { i =>  // error
       if i > 9 then throw Ex1()
       i * i
     }
diff --git a/tests/neg-custom-args/captures/leaky.check b/tests/neg-custom-args/captures/leaky.check
index b6fb368aa757..463a941545cf 100644
--- a/tests/neg-custom-args/captures/leaky.check
+++ b/tests/neg-custom-args/captures/leaky.check
@@ -10,18 +10,18 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/leaky.scala:24:2 -----------------------------------------
 24 |  x  // error
    |  ^
-   |  Found:    test.runnable.Transform{val fun: Any ->{f} Any}^{x}
+   |  Found:    test.runnable.Transform{val fun: Any ->{a} Any}^{a}
    |  Required: test.runnable.Transform
    |
-   |  Note that capability x is not included in capture set {}.
+   |  Note that capability a is not included in capture set {}.
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/leaky.scala:31:2 -----------------------------------------
 31 |  x  // error
    |  ^
-   |  Found:    test.runnable.Transform{val fun: Any ->{f} Any}^{x}
+   |  Found:    test.runnable.Transform{val fun: Any ->{a} Any}^{a}
    |  Required: test.runnable.Transform
    |
-   |  Note that capability x is not included in capture set {}.
+   |  Note that capability a is not included in capture set {}.
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/real-try.check b/tests/neg-custom-args/captures/real-try.check
index 3fde3af88fd9..a665939ba1e9 100644
--- a/tests/neg-custom-args/captures/real-try.check
+++ b/tests/neg-custom-args/captures/real-try.check
@@ -16,39 +16,35 @@
 16 |  catch
 17 |    case _: Ex1 => ???
 18 |    case _: Ex2 => ???
--- Error: tests/neg-custom-args/captures/real-try.scala:20:10 ----------------------------------------------------------
-20 |  val x = try // error
-   |          ^
-   |   The result of `try` cannot have type () => Unit since
-   |   that type captures the root capability `cap`.
-   |   This is often caused by a locally generated exception capability leaking as part of its result.
-   |
-   |   where:    => refers to a fresh root capability classified as Control in the type of given instance canThrow$2
-21 |    () => foo(1)
-22 |  catch
-23 |    case _: Ex1 => ???
-24 |    case _: Ex2 => ???
--- Error: tests/neg-custom-args/captures/real-try.scala:26:10 ----------------------------------------------------------
-26 |  val y = try  // error
-   |          ^
-   |   The result of `try` cannot have type () => Cell[Unit]^'s1 since
-   |   that type captures the root capability `cap`.
-   |   This is often caused by a locally generated exception capability leaking as part of its result.
-   |
-   |   where:    => refers to a fresh root capability classified as Control in the type of given instance canThrow$3
-27 |    () => Cell(foo(1))
-28 |  catch
-29 |    case _: Ex1 => ???
-30 |    case _: Ex2 => ???
--- 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] 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.
-   |
-   |   where:    => refers to a fresh root capability classified as Control in the type of given instance canThrow$4
-33 |    Cell(() => foo(1))
-34 |  catch
-35 |    case _: Ex1 => ???
-36 |    case _: Ex2 => ???
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/real-try.scala:21:4 --------------------------------------
+21 |    () => foo(1) // error
+   |    ^^^^^^^^^^^^
+   |    Found:    () ->{canThrow$2} Unit
+   |    Required: () ->'s1 Unit
+   |
+   |    Note that capability canThrow$2, defined in method try$2
+   |    cannot be included in outer capture set 's1 of value x.
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/real-try.scala:27:4 --------------------------------------
+27 |    () => Cell(foo(1)) // error
+   |    ^^^^^^^^^^^^^^^^^^
+   |    Found:    () ->{canThrow$3} Cell[Unit]^'s2
+   |    Required: () ->'s3 Cell[Unit]^'s4
+   |
+   |    Note that capability canThrow$3, defined in method try$3
+   |    cannot be included in outer capture set 's3 of value y.
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/real-try.scala:33:8 --------------------------------------
+33 |    Cell(() => foo(1)) // error
+   |    ^^^^^^^^^^^^^^^^^^
+   |  Found:    Cell[() => Unit]
+   |  Required: Cell[() ->'s5 Unit]^'s6
+   |
+   |  Note that capability cap cannot be included in outer capture set 's5 of value b.
+   |
+   |  where:    =>  refers to a fresh root capability classified as Control in the type of given instance canThrow$4
+   |            cap is a fresh root capability classified as Control in the type of given instance canThrow$4
+   |
+   | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/real-try.scala b/tests/neg-custom-args/captures/real-try.scala
index 32e976f654a9..167db091ed4d 100644
--- a/tests/neg-custom-args/captures/real-try.scala
+++ b/tests/neg-custom-args/captures/real-try.scala
@@ -17,20 +17,20 @@ def test(): Unit =
     case _: Ex1 => ???
     case _: Ex2 => ???
 
-  val x = try // error
-    () => foo(1)
+  val x = try
+    () => foo(1) // error
   catch
     case _: Ex1 => ???
     case _: Ex2 => ???
 
-  val y = try  // error
-    () => Cell(foo(1))
+  val y = try
+    () => Cell(foo(1)) // error
   catch
     case _: Ex1 => ???
     case _: Ex2 => ???
 
-  val b = try // error
-    Cell(() => foo(1))
+  val b = try
+    Cell(() => foo(1)) // error
   catch
     case _: Ex1 => ???
     case _: Ex2 => ???
diff --git a/tests/neg-custom-args/captures/sep-counter.check b/tests/neg-custom-args/captures/sep-counter.check
index c9d2b1895aee..f46d3fa03dfc 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  {c, cap}.
-   | Another part,  Ref^²,  captures capabilities  {c, cap}.
-   | The two sets overlap at  {c}.
+   | One part,  Ref^, hides capabilities  {cap}.
+   | Another part,  Ref^²,  captures capabilities  {cap}.
+   | The two sets overlap at  cap of method mkCounter.
    |
    | 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 43429b08a3bc..79a9e8ddf108 100644
--- a/tests/neg-custom-args/captures/sep-pairs.check
+++ b/tests/neg-custom-args/captures/sep-pairs.check
@@ -12,9 +12,9 @@
 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  {r1*, cap, cap², r0}.
-   |         Another part,  Ref^²,  captures capabilities  {r1*, cap, cap², r0}.
-   |         The two sets overlap at  {r1*, r0}.
+   |         One part,  Ref^, hides capabilities  {cap, cap², r0}.
+   |         Another part,  Ref^²,  captures capabilities  {cap, cap², r0}.
+   |         The two sets overlap at  {r0}.
    |
    |         where:    ^    refers to a fresh root capability classified as Mutable in the result type of method bad
    |                   ^²   refers to a fresh root capability classified as Mutable in the result type of method bad
diff --git a/tests/neg-custom-args/captures/vars.check b/tests/neg-custom-args/captures/vars.check
index 2029a61cb00e..f0e82a9dfff6 100644
--- a/tests/neg-custom-args/captures/vars.check
+++ b/tests/neg-custom-args/captures/vars.check
@@ -4,8 +4,7 @@
    |        Found:    (x: String) ->{cap3} String
    |        Required: String ->{cap1} String
    |
-   |        Note that capability cap3, defined in method scope
-   |        cannot be included in outer capture set {cap1} of variable a.
+   |        Note that capability cap3 cannot be included in capture set {cap1} of variable a.
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/vars.scala:25:8 ------------------------------------------
@@ -14,8 +13,7 @@
    |        Found:    (x: String) ->{cap3} String
    |        Required: String ->{cap1} String
    |
-   |        Note that capability cap3, defined in method scope
-   |        cannot be included in outer capture set {cap1} of variable a.
+   |        Note that capability cap3 cannot be included in capture set {cap1} of variable a.
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/vars.scala:27:12 -----------------------------------------

From 39b6f470262d5553f9fa2823fcdabf40291d0f0a Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Tue, 16 Sep 2025 16:38:35 +0200
Subject: [PATCH 4/7] New tests

---
 .../captures/closure-avoidance.scala          | 30 +++++++++++++++++++
 .../captures/flatmapInPlace.scala             | 19 ++++++++++++
 .../pos-custom-args/captures/leveltest.scala  | 24 +++++++++++++++
 3 files changed, 73 insertions(+)
 create mode 100644 tests/neg-custom-args/captures/closure-avoidance.scala
 create mode 100644 tests/pos-custom-args/captures/flatmapInPlace.scala
 create mode 100644 tests/pos-custom-args/captures/leveltest.scala

diff --git a/tests/neg-custom-args/captures/closure-avoidance.scala b/tests/neg-custom-args/captures/closure-avoidance.scala
new file mode 100644
index 000000000000..78747d7a3239
--- /dev/null
+++ b/tests/neg-custom-args/captures/closure-avoidance.scala
@@ -0,0 +1,30 @@
+trait A
+trait B
+
+def test =
+  val f = (a: A^) =>
+    val b: B^ = ???
+    b
+
+  val f1: A^ => B^ = (a: A^) => // error -- can we make this work as for f2?
+    val b: B^ = ???
+    b
+
+  val f2: (x: A^) => B^ = (a: A^) =>
+    val b: B^ = ???
+    b   // ok
+
+  val g = (a: A^) =>
+    println("")
+    (??? : B^)
+
+  val test = g
+
+  val g1: A^ => B^ = (a: A^) => // error -- can we make this work as for g2?
+    println("")
+    (??? : B^)
+
+  val g2: (x: A^) => B^ = (a: A^) =>
+    println("")
+    (??? : B^) // ok
+
diff --git a/tests/pos-custom-args/captures/flatmapInPlace.scala b/tests/pos-custom-args/captures/flatmapInPlace.scala
new file mode 100644
index 000000000000..f2d37273a9bc
--- /dev/null
+++ b/tests/pos-custom-args/captures/flatmapInPlace.scala
@@ -0,0 +1,19 @@
+trait Buffer[A]:
+
+  def apply(i: Int): A = ???
+
+  def flatMapInPlace(f: A => IterableOnce[A]^): this.type = {
+    val g = f
+    val s = 10
+     // capture checking: we need the copy since we box/unbox on g* on the next line
+      // TODO: This looks fishy, need to investigate
+      // Alternative would be to mark `f` as @use. It's not inferred
+      // since `^ appears in a function result, not under a box.
+    val newElems = new Array[(IterableOnce[A]^{f})](s)
+    var i = 0
+    while i < s do
+      val x = g(this(i))
+      newElems(i) = x
+      i += 1
+    this
+  }
\ No newline at end of file
diff --git a/tests/pos-custom-args/captures/leveltest.scala b/tests/pos-custom-args/captures/leveltest.scala
new file mode 100644
index 000000000000..7c1c27edbe99
--- /dev/null
+++ b/tests/pos-custom-args/captures/leveltest.scala
@@ -0,0 +1,24 @@
+class Cap extends caps.ExclusiveCapability
+
+class A
+
+def T =
+  def test(x: A^): A^{x} = ???
+
+  def foo(): A^ = ???
+
+  val a: A^ = ???
+
+  val x = test(foo())
+  val _: A^ = x
+
+  val y = test(a) :: Nil
+  val _: List[A^{a}] = y
+
+  def z =
+    val b = test(a)
+    Nil.::(b)
+  val _: List[A^{a}] = z
+
+
+

From d5365c2b554fcbf436527bda8968c5c3cc6feb2b Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Tue, 16 Sep 2025 16:49:04 +0200
Subject: [PATCH 5/7] Remove old level checking code

Remove old level checking code and debug infra to compare old with new.
---
 .../src/dotty/tools/dotc/cc/CCState.scala     |  39 ------
 .../src/dotty/tools/dotc/cc/Capability.scala  |   1 -
 .../src/dotty/tools/dotc/cc/CaptureSet.scala  |  68 +---------
 .../dotty/tools/dotc/cc/CheckCaptures.scala   |  24 ++--
 compiler/src/dotty/tools/dotc/cc/Setup.scala  | 116 +++++++++---------
 5 files changed, 72 insertions(+), 176 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CCState.scala b/compiler/src/dotty/tools/dotc/cc/CCState.scala
index 26977691339a..061810c3cd42 100644
--- a/compiler/src/dotty/tools/dotc/cc/CCState.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CCState.scala
@@ -21,34 +21,6 @@ class CCState:
    */
   val approxWarnings: mutable.ListBuffer[Message] = mutable.ListBuffer()
 
-  // ------ Level handling ---------------------------
-
-  private var curLevel: Level = outermostLevel
-
-  /** The level of the current environment. Levels start at 0 and increase for
-   *  each nested function or class. -1 means the level is undefined.
-   */
-  def currentLevel(using Context): Level = curLevel
-
-  /** Perform `op` in the next inner level */
-  inline def inNestedLevel[T](inline op: T)(using Context): T =
-    val saved = curLevel
-    curLevel = curLevel.nextInner
-    try op finally curLevel = saved
-
-  /** Perform `op` in the next inner level unless `p` holds. */
-  inline def inNestedLevelUnless[T](inline p: Boolean)(inline op: T)(using Context): T =
-    val saved = curLevel
-    if !p then curLevel = curLevel.nextInner
-    try op finally curLevel = saved
-
-  /** A map recording the level of a symbol */
-  private val mySymLevel: mutable.Map[Symbol, Level] = mutable.Map()
-
-  def symLevel(sym: Symbol): Level = mySymLevel.getOrElse(sym, undefinedLevel)
-
-  def recordLevel(sym: Symbol)(using Context): Unit = mySymLevel(sym) = curLevel
-
   // ------ BiTypeMap adjustment -----------------------
 
   private var myMapFutureElems = true
@@ -117,17 +89,6 @@ class CCState:
 
 object CCState:
 
-  opaque type Level = Int
-
-  val undefinedLevel: Level = -1
-
-  val outermostLevel: Level = 0
-
-  extension (x: Level)
-    def isDefined: Boolean = x >= 0
-    def <= (y: Level) = (x: Int) <= y
-    def nextInner: Level = if isDefined then x + 1 else x
-
   /** If we are currently in capture checking or setup, and `mt` is a method
    *  type that is not a prefix of a curried method, perform `op` assuming
    *  a fresh enclosing existential scope `mt`, otherwise perform `op` directly.
diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala
index d4b1a41755ef..4528c0cdc579 100644
--- a/compiler/src/dotty/tools/dotc/cc/Capability.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala
@@ -16,7 +16,6 @@ import CaptureSet.VarState
 import Annotations.Annotation
 import Flags.*
 import config.Printers.capt
-import CCState.{Level, undefinedLevel}
 import annotation.constructorOnly
 import ast.tpd
 import printing.{Printer, Showable}
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index 4fa037c31617..e275fd76b774 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -76,11 +76,6 @@ sealed abstract class CaptureSet extends Showable:
   /** Is this set provisionally solved, so that another cc run might unfreeze it? */
   def isProvisionallySolved(using Context): Boolean
 
-  /** An optional level limit, or undefinedLevel if none exists. All elements of the set
-   *  must be at levels equal or smaller than the level of the set, if it is defined.
-   */
-  def level: Level
-
   /** An optional owner, or NoSymbol if none exists. Used for diagnstics
    */
   def owner: Symbol
@@ -607,8 +602,6 @@ object CaptureSet:
 
     def withDescription(description: String): Const = Const(elems, description)
 
-    def level = undefinedLevel
-
     def owner = NoSymbol
 
     def dropEmpties()(using Context) = this
@@ -663,7 +656,7 @@ object CaptureSet:
   inline val debugTarget = 1745
 
   /** The subclass of captureset variables with given initial elements */
-  class Var(initialOwner: Symbol = NoSymbol, initialElems: Refs = emptyRefs, val level: Level = undefinedLevel, underBox: Boolean = false)(using /*@constructorOnly*/ ictx: Context) extends CaptureSet:
+  class Var(initialOwner: Symbol = NoSymbol, initialElems: Refs = emptyRefs, underBox: Boolean = false)(using /*@constructorOnly*/ ictx: Context) extends CaptureSet:
 
     override def owner = initialOwner
 
@@ -833,40 +826,7 @@ object CaptureSet:
             case _ => foldOver(b, t)
       find(false, binder)
 
-    def levelOKold(elem: Capability)(using Context): Boolean = elem match
-      case _: FreshCap =>
-        !level.isDefined
-        || ccState.symLevel(elem.ccOwner) <= level
-        || {
-          capt.println(i"LEVEL ERROR $elem cannot be included in $this of $owner")
-          false
-        }
-      case elem @ ResultCap(binder) =>
-        rootLimit == null && (this.isInstanceOf[BiMapped] || isPartOf(binder.resType))
-      case GlobalCap =>
-        rootLimit == null
-      case elem: TermRef if level.isDefined =>
-        elem.prefix match
-          case prefix: Capability =>
-            levelOK(prefix)
-          case _ =>
-            ccState.symLevel(elem.symbol) <= level
-      case elem: ThisType if level.isDefined =>
-        ccState.symLevel(elem.cls).nextInner <= level
-      case elem: ParamRef if !this.isInstanceOf[BiMapped] =>
-        isPartOf(elem.binder.resType)
-        || {
-          capt.println(
-            i"""LEVEL ERROR $elem for $this
-                |elem binder = ${elem.binder}""")
-          false
-        }
-      case elem: DerivedCapability =>
-        levelOK(elem.underlying)
-      case _ =>
-        true
-
-    def levelOKnew(elem: Capability)(using Context): Boolean = elem match
+    def levelOK(elem: Capability)(using Context): Boolean = elem match
       case elem @ ResultCap(binder) =>
         rootLimit == null && (this.isInstanceOf[BiMapped] || isPartOf(binder.resType))
       case GlobalCap =>
@@ -879,16 +839,6 @@ object CaptureSet:
           !elemVis.isProperlyContainedIn(owner)
         else true
 
-    inline val debugLevelChecking = false
-
-    def levelOK(elem: Capability)(using Context): Boolean =
-      val now = levelOKnew(elem)
-      if debugLevelChecking then
-        val was = levelOKold(elem)
-        if was != now then
-          println(i"LEVEL DIFF for $this / $getClass in ${owner.ownersIterator.toList} and elem $elem in ${elem.ccOwner}, was $was")
-      now
-
     def addDependent(cs: CaptureSet)(using Context, VarState): Boolean =
       (cs eq this)
       || cs.isUniversal
@@ -968,15 +918,9 @@ object CaptureSet:
      */
     override def optionalInfo(using Context): String =
       for vars <- ctx.property(ShownVars) do vars += this
-      val debugInfo =
-        if !ctx.settings.YccDebug.value then ""
-        else if isConst then ids ++ "(solved)"
-        else ids
-      val limitInfo =
-        if ctx.settings.YprintLevel.value && level.isDefined
-        then i"<at level ${level.toString}>"
-        else ""
-      debugInfo ++ limitInfo
+      if !ctx.settings.YccDebug.value then ""
+      else if isConst then ids ++ "(solved)"
+      else ids
 
     /** Used for diagnostics and debugging: A string that traces the creation
      *  history of a variable by following source links. Each variable on the
@@ -1378,7 +1322,7 @@ object CaptureSet:
     override def toText(printer: Printer): Text =
       inContext(printer.printerContext):
         if levelError then
-          i"($elem at wrong level for $cs at level ${cs.level.toString})"
+          i"($elem at wrong level for $cs in ${cs.owner.showLocated})"
         else
           if ctx.settings.YccDebug.value
           then i"$elem cannot be included in $trace"
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 3f5e1b276253..d352baa071b9 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -430,7 +430,7 @@ class CheckCaptures extends Recheck, SymTransformer:
     def capturedVars(sym: Symbol)(using Context): CaptureSet =
       myCapturedVars.getOrElseUpdate(sym,
         if sym.isTerm || !sym.owner.isStaticOwner
-        then CaptureSet.Var(sym, level = ccState.symLevel(sym))
+        then CaptureSet.Var(sym)
         else CaptureSet.empty)
 
 // ---- Record Uses with MarkFree ----------------------------------------------------
@@ -1091,14 +1091,13 @@ class CheckCaptures extends Recheck, SymTransformer:
           if ac.isEmpty then ctx
           else ctx.withProperty(CaptureSet.AssumedContains, Some(ac))
 
-        ccState.inNestedLevel: // TODO: nestedLevel needed here?
-          try checkInferredResult(super.recheckDefDef(tree, sym)(using bodyCtx), tree)
-          finally
-            if !sym.isAnonymousFunction then
-              // Anonymous functions propagate their type to the enclosing environment
-              // so it is not in general sound to interpolate their types.
-              interpolateIfInferred(tree.tpt, sym)
-            curEnv = saved
+        try checkInferredResult(super.recheckDefDef(tree, sym)(using bodyCtx), tree)
+        finally
+          if !sym.isAnonymousFunction then
+            // Anonymous functions propagate their type to the enclosing environment
+            // so it is not in general sound to interpolate their types.
+            interpolateIfInferred(tree.tpt, sym)
+          curEnv = saved
     end recheckDefDef
 
     /** If val or def definition with inferred (result) type is visible
@@ -1228,8 +1227,7 @@ class CheckCaptures extends Recheck, SymTransformer:
             case AppliedType(fn, args) =>
               markFreeTypeArgs(tpt, fn.typeSymbol, args.map(TypeTree(_)))
             case _ =>
-        ccState.inNestedLevelUnless(cls.is(Module)):
-          super.recheckClassDef(tree, impl, cls)
+        super.recheckClassDef(tree, impl, cls)
       finally
         completed += cls
         curEnv = saved
@@ -1311,7 +1309,7 @@ class CheckCaptures extends Recheck, SymTransformer:
       tree match
         case _: RefTree | closureDef(_) if pt.isBoxedCapturing =>
           curEnv = Env(curEnv.owner, EnvKind.Boxed,
-            CaptureSet.Var(curEnv.owner, level = ccState.currentLevel), curEnv)
+            CaptureSet.Var(curEnv.owner), curEnv)
         case _ =>
       val res =
         try
@@ -1577,7 +1575,7 @@ class CheckCaptures extends Recheck, SymTransformer:
             curEnv = Env(
               curEnv.owner,
               if boxed then EnvKind.Boxed else EnvKind.NestedInOwner,
-              CaptureSet.Var(curEnv.owner, level = ccState.currentLevel),
+              CaptureSet.Var(curEnv.owner),
               if boxed then null else curEnv)
             try
               val (eargs, eres) = expected.dealias.stripCapturing match
diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala
index b925442e8feb..4864c837dd45 100644
--- a/compiler/src/dotty/tools/dotc/cc/Setup.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -520,16 +520,13 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
           if isExcluded(meth) then
             return
 
-          ccState.recordLevel(meth)
-          ccState.inNestedLevel:
-            inContext(ctx.withOwner(meth)):
-              paramss.foreach(traverse)
-              transformResultType(tpt, meth)
-              traverse(tree.rhs)
+          inContext(ctx.withOwner(meth)):
+            paramss.foreach(traverse)
+            transformResultType(tpt, meth)
+            traverse(tree.rhs)
 
         case tree @ ValDef(_, tpt: TypeTree, _) =>
           val sym = tree.symbol
-          ccState.recordLevel(sym)
           val defCtx = if sym.isOneOf(TermParamOrAccessor) then ctx else ctx.withOwner(sym)
           inContext(defCtx):
             transformResultType(tpt, sym)
@@ -546,10 +543,8 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
 
         case tree: TypeDef if tree.symbol.isClass =>
           val sym = tree.symbol
-          ccState.recordLevel(sym)
-          ccState.inNestedLevelUnless(sym.is(Module)):
-            inContext(ctx.withOwner(sym))
-              traverseChildren(tree)
+          inContext(ctx.withOwner(sym))
+            traverseChildren(tree)
 
         case tree @ TypeDef(_, rhs: TypeTree) =>
           transformTT(rhs, tree.symbol, boxed = false)
@@ -670,55 +665,54 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
         tree.symbol match
           case cls: ClassSymbol =>
             checkClassifiedInheritance(cls)
-            ccState.inNestedLevelUnless(cls.is(Module)):
-              val cinfo @ ClassInfo(prefix, _, ps, decls, selfInfo) = cls.classInfo
-
-              // Compute new self type
-              def isInnerModule = cls.is(ModuleClass) && !cls.isStatic
-              val selfInfo1 =
-                if (selfInfo ne NoType) && !isInnerModule then
-                  // if selfInfo is explicitly given then use that one, except if
-                  // self info applies to non-static modules, these still need to be inferred
-                  selfInfo
-                else if cls.isPureClass then
-                  // is cls is known to be pure, nothing needs to be added to self type
-                  selfInfo
-                else if !cls.isEffectivelySealed && !cls.baseClassHasExplicitNonUniversalSelfType then
-                  // assume {cap} for completely unconstrained self types of publicly extensible classes
-                  CapturingType(cinfo.selfType, CaptureSet.universal)
-                else
-                  // Infer the self type for the rest, which is all classes without explicit
-                  // self types (to which we also add nested module classes), provided they are
-                  // neither pure, nor are publicily extensible with an unconstrained self type.
-                  val cs = CaptureSet.Var(cls, level = ccState.currentLevel)
-                  if cls.derivesFrom(defn.Caps_Capability) then
-                    // If cls is a capability class, we need to add a fresh readonly capability to
-                    // ensure we cannot treat the class as pure.
-                    CaptureSet.fresh(Origin.InDecl(cls)).readOnly.subCaptures(cs)
-                  CapturingType(cinfo.selfType, cs)
-
-              // Compute new parent types
-              val ps1 = inContext(ctx.withOwner(cls)):
-                ps.mapConserve(transformExplicitType(_, NoSymbol, freshen = false))
-
-              // Install new types and if it is a module class also update module object
-              if (selfInfo1 ne selfInfo) || (ps1 ne ps) then
-                val newInfo = ClassInfo(prefix, cls, ps1, decls, selfInfo1)
-                updateInfo(cls, newInfo, cls.owner)
-                capt.println(i"update class info of $cls with parents $ps selfinfo $selfInfo to $newInfo")
-                cls.thisType.asInstanceOf[ThisType].invalidateCaches()
-                if cls.is(ModuleClass) then
-                  // if it's a module, the capture set of the module reference is the capture set of the self type
-                  val modul = cls.sourceModule
-                  val selfCaptures = selfInfo1 match
-                    case CapturingType(_, refs) => refs
-                    case _ => CaptureSet.empty
-                  // Note: Can't do val selfCaptures = selfInfo1.captureSet here.
-                  // This would potentially give stackoverflows when setup is run repeatedly.
-                  // One test case is pos-custom-args/captures/checkbounds.scala under
-                  // ccConfig.alwaysRepeatRun = true.
-                  updateInfo(modul, CapturingType(modul.info, selfCaptures), modul.owner)
-                  modul.termRef.invalidateCaches()
+            val cinfo @ ClassInfo(prefix, _, ps, decls, selfInfo) = cls.classInfo
+
+            // Compute new self type
+            def isInnerModule = cls.is(ModuleClass) && !cls.isStatic
+            val selfInfo1 =
+              if (selfInfo ne NoType) && !isInnerModule then
+                // if selfInfo is explicitly given then use that one, except if
+                // self info applies to non-static modules, these still need to be inferred
+                selfInfo
+              else if cls.isPureClass then
+                // is cls is known to be pure, nothing needs to be added to self type
+                selfInfo
+              else if !cls.isEffectivelySealed && !cls.baseClassHasExplicitNonUniversalSelfType then
+                // assume {cap} for completely unconstrained self types of publicly extensible classes
+                CapturingType(cinfo.selfType, CaptureSet.universal)
+              else
+                // Infer the self type for the rest, which is all classes without explicit
+                // self types (to which we also add nested module classes), provided they are
+                // neither pure, nor are publicily extensible with an unconstrained self type.
+                val cs = CaptureSet.Var(cls)
+                if cls.derivesFrom(defn.Caps_Capability) then
+                  // If cls is a capability class, we need to add a fresh readonly capability to
+                  // ensure we cannot treat the class as pure.
+                  CaptureSet.fresh(Origin.InDecl(cls)).readOnly.subCaptures(cs)
+                CapturingType(cinfo.selfType, cs)
+
+            // Compute new parent types
+            val ps1 = inContext(ctx.withOwner(cls)):
+              ps.mapConserve(transformExplicitType(_, NoSymbol, freshen = false))
+
+            // Install new types and if it is a module class also update module object
+            if (selfInfo1 ne selfInfo) || (ps1 ne ps) then
+              val newInfo = ClassInfo(prefix, cls, ps1, decls, selfInfo1)
+              updateInfo(cls, newInfo, cls.owner)
+              capt.println(i"update class info of $cls with parents $ps selfinfo $selfInfo to $newInfo")
+              cls.thisType.asInstanceOf[ThisType].invalidateCaches()
+              if cls.is(ModuleClass) then
+                // if it's a module, the capture set of the module reference is the capture set of the self type
+                val modul = cls.sourceModule
+                val selfCaptures = selfInfo1 match
+                  case CapturingType(_, refs) => refs
+                  case _ => CaptureSet.empty
+                // Note: Can't do val selfCaptures = selfInfo1.captureSet here.
+                // This would potentially give stackoverflows when setup is run repeatedly.
+                // One test case is pos-custom-args/captures/checkbounds.scala under
+                // ccConfig.alwaysRepeatRun = true.
+                updateInfo(modul, CapturingType(modul.info, selfCaptures), modul.owner)
+                modul.termRef.invalidateCaches()
           case _ =>
       case _ =>
     end postProcess
@@ -857,7 +851,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
 
   /** Add a capture set variable to `tp` if necessary. */
   private def addVar(tp: Type, owner: Symbol)(using Context): Type =
-    decorate(tp, CaptureSet.Var(owner, _, level = ccState.currentLevel))
+    decorate(tp, CaptureSet.Var(owner, _))
 
   /** A map that adds <fluid> capture sets at all contra- and invariant positions
    *  in a type where a capture set would be needed. This is used to make types

From badf8729fc02ccc93fd9b4bd5fb23f8061dfaca8 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Wed, 17 Sep 2025 12:20:06 +0200
Subject: [PATCH 6/7] Add comment

---
 compiler/src/dotty/tools/dotc/cc/Capability.scala | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala
index 4528c0cdc579..539af2731d67 100644
--- a/compiler/src/dotty/tools/dotc/cc/Capability.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala
@@ -168,6 +168,11 @@ object Capabilities:
 
     /** Is this fresh cap at the right level to be able to subsume `ref`?
      *  Only outer freshes can be subsumed.
+     *  TODO Can we merge this with levelOK? Right now we use two different schemes:
+     *   - For level checking capsets with levelOK: Check that the visibility of the element
+     *     os not properly contained in the captset owner.
+     *  - For level checking elements subsumed by FreshCaps: Check that the widened scope
+     *    (using levelOwner) of the elements contains the owner of the FreshCap.
      */
     def acceptsLevelOf(ref: Capability)(using Context): Boolean =
       if ccConfig.useFreshLevels && !CCState.collapseFresh then

From de35cbbbe565555eead3842fb4373db56479b1ad Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Fri, 19 Sep 2025 19:11:57 +0200
Subject: [PATCH 7/7] Tweaks to level checking

 - In levelOwner, don't skip constructors. These are significant now.
 - Skip non-static modules when computing the visibility of FreshCaps
---
 .../src/dotty/tools/dotc/cc/Capability.scala    | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala
index 539af2731d67..fb12ff6c68b1 100644
--- a/compiler/src/dotty/tools/dotc/cc/Capability.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala
@@ -489,7 +489,7 @@ object Capabilities:
       case _ /* : GlobalCap | ResultCap | ParamRef */ => NoSymbol
 
     final def visibility(using Context): Symbol = this match
-      case self: FreshCap => ccOwner.enclosingMethodOrClass
+      case self: FreshCap => adjustOwner(ccOwner)
       case _ =>
         val vis = ccOwner
         if vis.is(Param) then vis.owner else vis
@@ -500,13 +500,14 @@ object Capabilities:
      *   - method symbols, but not accessors or constructors
      */
     final def levelOwner(using Context): Symbol =
-      def adjust(owner: Symbol): Symbol =
-        if !owner.exists
-          || owner.isClass && (!owner.is(Flags.Module) || owner.isStatic)
-          || owner.is(Flags.Method, butNot = Flags.Accessor) && !owner.isConstructor
-        then owner
-        else adjust(owner.owner)
-      adjust(ccOwner)
+      adjustOwner(ccOwner)
+
+    private def adjustOwner(owner: Symbol)(using Context): Symbol =
+      if !owner.exists
+        || owner.isClass && (!owner.is(Flags.Module) || owner.isStatic)
+        || owner.is(Flags.Method, butNot = Flags.Accessor)
+      then owner
+      else adjustOwner(owner.owner)
 
     /** Tests whether the capability derives from capability class `cls`. */
     def derivesFromCapTrait(cls: ClassSymbol)(using Context): Boolean = this match