From 4b0f18c2370fcbe087129f287aeca5347f5fad33 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Fri, 6 Jun 2025 14:31:21 +0200
Subject: [PATCH 01/14] Add use annotations in parameter info type for use
 parameters

---
 compiler/src/dotty/tools/dotc/cc/CaptureOps.scala | 1 +
 compiler/src/dotty/tools/dotc/core/Types.scala    | 2 ++
 2 files changed, 3 insertions(+)

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
index 3dd847f19b56..74e09948106f 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
@@ -495,6 +495,7 @@ extension (sym: Symbol)
    */
   def isUseParam(using Context): Boolean =
     sym.hasAnnotation(defn.UseAnnot)
+    || sym.info.hasAnnotation(defn.UseAnnot)
     || sym.is(TypeParam)
         && sym.owner.rawParamss.nestedExists: param =>
             param.is(TermParam) && param.hasAnnotation(defn.UseAnnot)
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index b06bd5c00a28..0a97593eef89 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -4234,6 +4234,8 @@ object Types extends TypeUtils {
         paramType = addAnnotation(paramType, defn.InlineParamAnnot, param)
       if param.is(Erased) then
         paramType = addAnnotation(paramType, defn.ErasedParamAnnot, param)
+      if param.isUseParam then
+        paramType = addAnnotation(paramType, defn.UseAnnot, param)
       paramType
 
     def adaptParamInfo(param: Symbol)(using Context): Type =

From 921a930d148a16b942815ede75cd664a42e0a160 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Fri, 6 Jun 2025 14:48:42 +0200
Subject: [PATCH 02/14] Add testcases for use annotations and value classes

---
 .../captures/cc-annot-value-classes.scala      | 18 ++++++++++++++++++
 .../captures/cc-use-iterable.scala             | 10 ++++++++++
 2 files changed, 28 insertions(+)
 create mode 100644 tests/neg-custom-args/captures/cc-annot-value-classes.scala
 create mode 100644 tests/pos-custom-args/captures/cc-use-iterable.scala

diff --git a/tests/neg-custom-args/captures/cc-annot-value-classes.scala b/tests/neg-custom-args/captures/cc-annot-value-classes.scala
new file mode 100644
index 000000000000..745b1c85b8b1
--- /dev/null
+++ b/tests/neg-custom-args/captures/cc-annot-value-classes.scala
@@ -0,0 +1,18 @@
+import language.experimental.captureChecking
+import caps.*
+
+class Runner(val x: Int) extends AnyVal:
+  def runOps(@use ops: List[() => Unit]): Unit =
+    ops.foreach(_())  // ok
+
+class RunnerAlt(val x: Int):
+  def runOps(@use ops: List[() => Unit]): Unit =
+    ops.foreach(_())  // ok, of course
+
+class RunnerAltAlt(val x: Int) extends AnyVal:
+  def runOps(ops: List[() => Unit]): Unit =
+    ops.foreach(_())  // error, as expected
+
+class RunnerAltAltAlt(val x: Int):
+  def runOps(ops: List[() => Unit]): Unit =
+    ops.foreach(_())  // error, as expected
diff --git a/tests/pos-custom-args/captures/cc-use-iterable.scala b/tests/pos-custom-args/captures/cc-use-iterable.scala
new file mode 100644
index 000000000000..84c497c0f6ce
--- /dev/null
+++ b/tests/pos-custom-args/captures/cc-use-iterable.scala
@@ -0,0 +1,10 @@
+import language.experimental.captureChecking
+trait IterableOnce[+T]
+trait Iterable[+T] extends IterableOnce[T]:
+  def flatMap[U](@caps.use f: T => IterableOnce[U]^): Iterable[U]^{this, f*}
+
+
+class IterableOnceExtensionMethods[T](val it: IterableOnce[T]) extends AnyVal:
+  def flatMap[U](@caps.use f: T => IterableOnce[U]^): IterableOnce[U]^{f*} = it match
+    case it: Iterable[T] => it.flatMap(f)
+

From b867b3fee761ec866acf70a226ba032e267328dc Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Fri, 6 Jun 2025 17:07:44 +0200
Subject: [PATCH 03/14] Copy `@consume` annotations to the type

---
 .../src/dotty/tools/dotc/cc/CaptureOps.scala     | 10 +++++++++-
 .../src/dotty/tools/dotc/cc/CheckCaptures.scala  |  7 +++++--
 compiler/src/dotty/tools/dotc/cc/SepCheck.scala  |  6 +++---
 compiler/src/dotty/tools/dotc/core/Types.scala   |  5 ++++-
 .../captures/cc-annot-value-classes2.scala       | 16 ++++++++++++++++
 5 files changed, 37 insertions(+), 7 deletions(-)
 create mode 100644 tests/neg-custom-args/captures/cc-annot-value-classes2.scala

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
index 74e09948106f..feae2cc9fa4f 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
@@ -395,6 +395,9 @@ extension (tp: Type)
     RefinedType(tp, name,
       AnnotatedType(rinfo, Annotation(defn.RefineOverrideAnnot, util.Spans.NoSpan)))
 
+  def dropUseAndConsumeAnnots(using Context): Type =
+    tp.dropAnnot(defn.UseAnnot).dropAnnot(defn.ConsumeAnnot)
+
 extension (tp: MethodType)
   /** A method marks an existential scope unless it is the prefix of a curried method */
   def marksExistentialScope(using Context): Boolean =
@@ -490,7 +493,7 @@ extension (sym: Symbol)
   def hasTrackedParts(using Context): Boolean =
     !CaptureSet.ofTypeDeeply(sym.info).isAlwaysEmpty
 
-  /** `sym` is annotated @use or it is a type parameter with a matching
+  /** `sym` itself or its info is annotated @use or it is a type parameter with a matching
    *  @use-annotated term parameter that contains `sym` in its deep capture set.
    */
   def isUseParam(using Context): Boolean =
@@ -503,6 +506,11 @@ extension (sym: Symbol)
                 case c: TypeRef => c.symbol == sym
                 case _ => false
 
+  /** `sym` or its info is annotated with `@consume`. */
+  def isConsumeParam(using Context): Boolean =
+    sym.hasAnnotation(defn.ConsumeAnnot)
+    || sym.info.hasAnnotation(defn.ConsumeAnnot)
+
   def isUpdateMethod(using Context): Boolean =
     sym.isAllOf(Mutable | Method, butNot = Accessor)
 
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 1bdd7ce92129..44082346e3cc 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -716,7 +716,7 @@ class CheckCaptures extends Recheck, SymTransformer:
         funtpe.paramInfos.zipWithConserve(funtpe.paramNames): (formal, pname) =>
           val param = meth.paramNamed(pname)
           def copyAnnot(tp: Type, cls: ClassSymbol) = param.getAnnotation(cls) match
-            case Some(ann) => AnnotatedType(tp, ann)
+            case Some(ann) if !tp.hasAnnotation(cls) => AnnotatedType(tp, ann)
             case _ => tp
           copyAnnot(copyAnnot(formal, defn.UseAnnot), defn.ConsumeAnnot)
       funtpe.derivedLambdaType(paramInfos = paramInfosWithUses)
@@ -1616,7 +1616,10 @@ class CheckCaptures extends Recheck, SymTransformer:
       if noWiden(actual, expected) then
         actual
       else
-        val improvedVAR = improveCaptures(actual.widen.dealiasKeepAnnots, actual)
+        // Compute the widened type. Drop `@use` and `@consume` annotations from the type,
+        // since they obscures the capturing type.
+        val widened = actual.widen.dealiasKeepAnnots.dropUseAndConsumeAnnots
+        val improvedVAR = improveCaptures(widened, actual)
         val improved = improveReadOnly(improvedVAR, expected)
         val adapted = adaptBoxed(
             improved.withReachCaptures(actual), expected, tree,
diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
index 6dad0e9a2ff7..a402e58624f2 100644
--- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
+++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
@@ -620,7 +620,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
             if currentOwner.enclosingMethodOrClass.isProperlyContainedIn(refSym.maybeOwner.enclosingMethodOrClass) then
               report.error(em"""Separation failure: $descr non-local $refSym""", pos)
             else if refSym.is(TermParam)
-              && !refSym.hasAnnotation(defn.ConsumeAnnot)
+              && !refSym.isConsumeParam
               && currentOwner.isContainedIn(refSym.owner)
             then
               badParams += refSym
@@ -899,7 +899,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
     if !isUnsafeAssumeSeparate(tree) then trace(i"checking separate $tree"):
       checkUse(tree)
       tree match
-        case tree @ Select(qual, _) if tree.symbol.is(Method) && tree.symbol.hasAnnotation(defn.ConsumeAnnot) =>
+        case tree @ Select(qual, _) if tree.symbol.is(Method) && tree.symbol.isConsumeParam =>
           traverseChildren(tree)
           checkConsumedRefs(
               captures(qual).footprint(), qual.nuType,
@@ -962,4 +962,4 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
             consumeInLoopError(ref, pos)
         case _ =>
           traverseChildren(tree)
-end SepCheck
\ No newline at end of file
+end SepCheck
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index 0a97593eef89..e10a5221e8e7 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -4234,8 +4234,11 @@ object Types extends TypeUtils {
         paramType = addAnnotation(paramType, defn.InlineParamAnnot, param)
       if param.is(Erased) then
         paramType = addAnnotation(paramType, defn.ErasedParamAnnot, param)
-      if param.isUseParam then
+      // Copy `@use` and `@consume` annotations from parameter symbols to the type.
+      if param.hasAnnotation(defn.UseAnnot) then
         paramType = addAnnotation(paramType, defn.UseAnnot, param)
+      if param.hasAnnotation(defn.ConsumeAnnot) then
+        paramType = addAnnotation(paramType, defn.ConsumeAnnot, param)
       paramType
 
     def adaptParamInfo(param: Symbol)(using Context): Type =
diff --git a/tests/neg-custom-args/captures/cc-annot-value-classes2.scala b/tests/neg-custom-args/captures/cc-annot-value-classes2.scala
new file mode 100644
index 000000000000..5821f9664f6b
--- /dev/null
+++ b/tests/neg-custom-args/captures/cc-annot-value-classes2.scala
@@ -0,0 +1,16 @@
+import language.experimental.captureChecking
+import caps.*
+trait Ref extends Mutable
+def kill(@consume x: Ref^): Unit = ()
+
+class C1:
+  def myKill(@consume x: Ref^): Unit = kill(x)  // ok
+
+class C2(val dummy: Int) extends AnyVal:
+  def myKill(@consume x: Ref^): Unit = kill(x)  // ok, too
+
+class C3:
+  def myKill(x: Ref^): Unit = kill(x)  // error
+
+class C4(val dummy: Int) extends AnyVal:
+  def myKill(x: Ref^): Unit = kill(x)  // error, too

From 531d165fb494f6595db469792f1fa50654a36370 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Sat, 7 Jun 2025 13:55:29 +0200
Subject: [PATCH 04/14] Properly print `@use` and `@consume` parameters

---
 compiler/src/dotty/tools/dotc/core/Definitions.scala      | 2 +-
 compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala | 6 +++++-
 tests/neg-custom-args/captures/unbox-overrides.check      | 6 +++---
 tests/neg-custom-args/captures/unsound-reach-4.check      | 4 ++--
 4 files changed, 11 insertions(+), 7 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala
index 83c85adb0f43..9626e5ccb7c5 100644
--- a/compiler/src/dotty/tools/dotc/core/Definitions.scala
+++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala
@@ -1117,7 +1117,7 @@ class Definitions {
 
   // Set of annotations that are not printed in types except under -Yprint-debug
   @tu lazy val SilentAnnots: Set[Symbol] =
-    Set(InlineParamAnnot, ErasedParamAnnot, RefineOverrideAnnot, SilentIntoAnnot)
+    Set(InlineParamAnnot, ErasedParamAnnot, RefineOverrideAnnot, SilentIntoAnnot, UseAnnot, ConsumeAnnot)
 
   // A list of annotations that are commonly used to indicate that a field/method argument or return
   // type is not null. These annotations are used by the nullification logic in JavaNullInterop to
diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
index 750e4b646e0d..a7f0f59aba3b 100644
--- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
@@ -379,7 +379,11 @@ class PlainPrinter(_ctx: Context) extends Printer {
   protected def paramsText(lam: LambdaType): Text = {
     def paramText(ref: ParamRef) =
       val erased = ref.underlying.hasAnnotation(defn.ErasedParamAnnot)
-      keywordText("erased ").provided(erased) ~ ParamRefNameString(ref) ~ hashStr(lam) ~ toTextRHS(ref.underlying, isParameter = true)
+      def maybeAnnotsText(sym: ClassSymbol): Text =
+        Str(s"@${sym.name} ").provided(ref.underlying.hasAnnotation(sym))
+      keywordText("erased ").provided(erased)
+        ~ maybeAnnotsText(defn.UseAnnot) ~ maybeAnnotsText(defn.ConsumeAnnot)
+        ~ ParamRefNameString(ref) ~ hashStr(lam) ~ toTextRHS(ref.underlying, isParameter = true)
     Text(lam.paramRefs.map(paramText), ", ")
   }
 
diff --git a/tests/neg-custom-args/captures/unbox-overrides.check b/tests/neg-custom-args/captures/unbox-overrides.check
index dbffc164b5c5..a531b546a62a 100644
--- a/tests/neg-custom-args/captures/unbox-overrides.check
+++ b/tests/neg-custom-args/captures/unbox-overrides.check
@@ -1,7 +1,7 @@
 -- [E164] Declaration Error: tests/neg-custom-args/captures/unbox-overrides.scala:8:6 ----------------------------------
 8 |  def foo(x: C): C        // error
   |      ^
-  |error overriding method foo in trait A of type (x: C): C;
+  |error overriding method foo in trait A of type (@use x: C): C;
   |  method foo of type (x: C): C has a parameter x with different @use status than the corresponding parameter in the overridden definition
   |
   | longer explanation available when compiling with `-explain`
@@ -9,13 +9,13 @@
 9 |  def bar(@use x: C): C // error
   |      ^
   |error overriding method bar in trait A of type (x: C): C;
-  |  method bar of type (x: C): C has a parameter x with different @use status than the corresponding parameter in the overridden definition
+  |  method bar of type (@use x: C): C has a parameter x with different @use status than the corresponding parameter in the overridden definition
   |
   | longer explanation available when compiling with `-explain`
 -- [E164] Declaration Error: tests/neg-custom-args/captures/unbox-overrides.scala:15:15 --------------------------------
 15 |abstract class C extends A[C], B2 // error
    |               ^
-   |error overriding method foo in trait A of type (x: C): C;
+   |error overriding method foo in trait A of type (@use x: C): C;
    |  method foo in trait B2 of type (x: C): C has a parameter x with different @use status than the corresponding parameter in the overridden definition
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/unsound-reach-4.check b/tests/neg-custom-args/captures/unsound-reach-4.check
index 0e9acbea1afa..361b1158305d 100644
--- a/tests/neg-custom-args/captures/unsound-reach-4.check
+++ b/tests/neg-custom-args/captures/unsound-reach-4.check
@@ -18,9 +18,9 @@
 17 |  def use(@consume x: F): File^ = x // error @consume override
    |      ^
    |      error overriding method use in trait Foo of type (x: File^): box File^;
-   |        method use of type (x: File^): File^² has incompatible type
+   |        method use of type (@consume x: File^): File^² has incompatible type
    |
    |      where:    ^  refers to the universal root capability
-   |                ^² refers to a root capability associated with the result type of (x: File^): File^²
+   |                ^² refers to a root capability associated with the result type of (@consume x: File^): File^²
    |
    | longer explanation available when compiling with `-explain`

From 0dd57f21de060a4efe9b368356cf7c63a21db3ac Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Sat, 7 Jun 2025 14:11:44 +0200
Subject: [PATCH 05/14] Improve printing `@use` and `@consume`

---
 .../src/dotty/tools/dotc/printing/PlainPrinter.scala | 12 +++++++++---
 .../captures/leak-problem-unboxed.scala              | 10 +++++-----
 2 files changed, 14 insertions(+), 8 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
index a7f0f59aba3b..e1ae2ec32de2 100644
--- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
@@ -134,6 +134,8 @@ class PlainPrinter(_ctx: Context) extends Printer {
 
   protected def argText(arg: Type, isErased: Boolean = false): Text =
     keywordText("erased ").provided(isErased)
+    ~ specialAnnotText(defn.UseAnnot, arg)
+    ~ specialAnnotText(defn.ConsumeAnnot, arg)
     ~ homogenizeArg(arg).match
         case arg: TypeBounds => "?" ~ toText(arg)
         case arg => toText(arg)
@@ -376,13 +378,17 @@ class PlainPrinter(_ctx: Context) extends Printer {
     try "(" ~ toTextRef(tp) ~ " : " ~ toTextGlobal(tp.underlying) ~ ")"
     finally elideCapabilityCaps = saved
 
+  /** Print the annotation that are meant to be on the parameter symbol but was moved
+   * to parameter types. Examples are `@use` and `@consume`. */
+  protected def specialAnnotText(sym: ClassSymbol, tp: Type): Text =
+    Str(s"@${sym.name} ").provided(tp.hasAnnotation(sym))
+
   protected def paramsText(lam: LambdaType): Text = {
     def paramText(ref: ParamRef) =
       val erased = ref.underlying.hasAnnotation(defn.ErasedParamAnnot)
-      def maybeAnnotsText(sym: ClassSymbol): Text =
-        Str(s"@${sym.name} ").provided(ref.underlying.hasAnnotation(sym))
       keywordText("erased ").provided(erased)
-        ~ maybeAnnotsText(defn.UseAnnot) ~ maybeAnnotsText(defn.ConsumeAnnot)
+        ~ specialAnnotText(defn.UseAnnot, ref.underlying)
+        ~ specialAnnotText(defn.ConsumeAnnot, ref.underlying)
         ~ ParamRefNameString(ref) ~ hashStr(lam) ~ toTextRHS(ref.underlying, isParameter = true)
     Text(lam.paramRefs.map(paramText), ", ")
   }
diff --git a/tests/neg-custom-args/captures/leak-problem-unboxed.scala b/tests/neg-custom-args/captures/leak-problem-unboxed.scala
index aedd7c889112..6d4c4b4c94aa 100644
--- a/tests/neg-custom-args/captures/leak-problem-unboxed.scala
+++ b/tests/neg-custom-args/captures/leak-problem-unboxed.scala
@@ -19,14 +19,14 @@ def useBoxedAsync1(@use x: Box[Async^]): Unit = x.get.read() // ok
 def test(): Unit =
 
   val f: Box[Async^] => Unit = (x:  Box[Async^]) => useBoxedAsync(x) // error
-  val _: Box[Async^] => Unit = useBoxedAsync(_) // error
-  val _: Box[Async^] => Unit = useBoxedAsync // error
-  val _ = useBoxedAsync(_) // error
-  val _ = useBoxedAsync // error
+  val t1: Box[Async^] => Unit = useBoxedAsync(_) // error
+  val t2: Box[Async^] => Unit = useBoxedAsync // error
+  val t3 = useBoxedAsync(_) // was error, now ok
+  val t4 = useBoxedAsync // was error, now ok
 
   def boom(x: Async^): () ->{f} Unit =
     () => f(Box(x))
 
   val leaked = usingAsync[() ->{f} Unit](boom)
 
-  leaked()  // scope violation
\ No newline at end of file
+  leaked()  // scope violation

From 1cf238f209dbc7bcedfd9c3e86d82b4a16e4995b Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Sun, 8 Jun 2025 14:15:55 +0200
Subject: [PATCH 06/14] Drop redundant copying logic

---
 .../src/dotty/tools/dotc/cc/CheckCaptures.scala     | 13 -------------
 1 file changed, 13 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 44082346e3cc..29107037f441 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -708,19 +708,6 @@ class CheckCaptures extends Recheck, SymTransformer:
           selType
     }//.showing(i"recheck sel $tree, $qualType = $result")
 
-    /** Hook for massaging a function before it is applied. Copies all @use and @consume
-     *  annotations on method parameter symbols to the corresponding paramInfo types.
-     */
-    override def prepareFunction(funtpe: MethodType, meth: Symbol)(using Context): MethodType =
-      val paramInfosWithUses =
-        funtpe.paramInfos.zipWithConserve(funtpe.paramNames): (formal, pname) =>
-          val param = meth.paramNamed(pname)
-          def copyAnnot(tp: Type, cls: ClassSymbol) = param.getAnnotation(cls) match
-            case Some(ann) if !tp.hasAnnotation(cls) => AnnotatedType(tp, ann)
-            case _ => tp
-          copyAnnot(copyAnnot(formal, defn.UseAnnot), defn.ConsumeAnnot)
-      funtpe.derivedLambdaType(paramInfos = paramInfosWithUses)
-
     /** Recheck applications, with special handling of unsafeAssumePure.
      *  More work is done in `recheckApplication`, `recheckArg` and `instantiate` below.
      */

From 9bdf3a7f8889d1a43367f3c0c946f7fb9be41d01 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Sun, 8 Jun 2025 14:19:12 +0200
Subject: [PATCH 07/14] Documenting where the annotations were added

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

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 29107037f441..d92ed29b8a6f 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -735,7 +735,8 @@ class CheckCaptures extends Recheck, SymTransformer:
       val argType = recheck(arg, freshenedFormal)
         .showing(i"recheck arg $arg vs $freshenedFormal = $result", capt)
       if formal.hasAnnotation(defn.UseAnnot) || formal.hasAnnotation(defn.ConsumeAnnot) then
-        // The @use and/or @consume annotation is added to `formal` by `prepareFunction`
+        // The @use and/or @consume annotation is added to `formal` when creating methods types.
+        // See [[MethodTypeCompanion.adaptParamInfo]].
         capt.println(i"charging deep capture set of $arg: ${argType} = ${argType.deepCaptureSet}")
         markFree(argType.deepCaptureSet, arg)
       if formal.containsCap then

From 69ddc4b5bcaf072a4f5e90277cee79b45770a2a2 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Thu, 29 May 2025 13:35:10 +0200
Subject: [PATCH 08/14] Add a debugging helper

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

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
index feae2cc9fa4f..d8d2a5a039c8 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
@@ -369,6 +369,7 @@ extension (tp: Type)
       val tp1 = narrowCaps(tp)
       if narrowCaps.change then
         capt.println(i"narrow $tp of $ref to $tp1")
+        //println(i"reach refinement $tp at $ref to $tp1 (${ctx.compilationUnit})")
         tp1
       else
         tp

From 70d1cc6f17bb5e1d0037e0e6c0b30dbd18d9d670 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Thu, 29 May 2025 14:44:15 +0200
Subject: [PATCH 09/14] Allow `this` to subsume `this.f` if `f` is a use
 parameter

---
 .../src/dotty/tools/dotc/cc/Capability.scala  | 48 +++++++++++--------
 .../captures/cc-class-this-reach1.scala       |  8 ++++
 2 files changed, 37 insertions(+), 19 deletions(-)
 create mode 100644 tests/neg-custom-args/captures/cc-class-this-reach1.scala

diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala
index 95f8f180b339..a25a3eb461a7 100644
--- a/compiler/src/dotty/tools/dotc/cc/Capability.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala
@@ -473,27 +473,28 @@ object Capabilities:
         case info: OrType => viaInfo(info.tp1)(test) && viaInfo(info.tp2)(test)
         case _ => false
 
+      def trySubpath(y: TermRef): Boolean =
+        y.prefix.match
+          case ypre: Capability =>
+            this.subsumes(ypre)
+            || this.match
+                case x @ TermRef(xpre: Capability, _) if x.symbol == y.symbol =>
+                  // To show `{x.f} <:< {y.f}`, it is important to prove `x` and `y`
+                  // are equvalent, which means `x =:= y` in terms of subtyping,
+                  // not just `{x} =:= {y}` in terms of subcapturing.
+                  // It is possible to construct two singleton types `x` and `y`,
+                  // which subsume each other, but are not equal references.
+                  // See `tests/neg-custom-args/captures/path-prefix.scala` for example.
+                  withMode(Mode.IgnoreCaptures):
+                    TypeComparer.isSameRef(xpre, ypre)
+                case _ =>
+                  false
+          case _ => false
+
       try (this eq y)
       || maxSubsumes(y, canAddHidden = !vs.isOpen)
       || y.match
-        case y: TermRef =>
-            y.prefix.match
-              case ypre: Capability =>
-                this.subsumes(ypre)
-                || this.match
-                    case x @ TermRef(xpre: Capability, _) if x.symbol == y.symbol =>
-                      // To show `{x.f} <:< {y.f}`, it is important to prove `x` and `y`
-                      // are equvalent, which means `x =:= y` in terms of subtyping,
-                      // not just `{x} =:= {y}` in terms of subcapturing.
-                      // It is possible to construct two singleton types `x` and `y`,
-                      // which subsume each other, but are not equal references.
-                      // See `tests/neg-custom-args/captures/path-prefix.scala` for example.
-                      withMode(Mode.IgnoreCaptures):
-                        TypeComparer.isSameRef(xpre, ypre)
-                    case _ =>
-                      false
-              case _ => false
-          || viaInfo(y.info)(subsumingRefs(this, _))
+        case y: TermRef => trySubpath(y) || viaInfo(y.info)(subsumingRefs(this, _))
         case Maybe(y1) => this.stripMaybe.subsumes(y1)
         case ReadOnly(y1) => this.stripReadOnly.subsumes(y1)
         case y: TypeRef if y.derivesFrom(defn.Caps_CapSet) =>
@@ -507,6 +508,15 @@ object Capabilities:
               this.subsumes(hi)
             case _ =>
               y.captureSetOfInfo.elems.forall(this.subsumes)
+        case Reach(y1: TermRef) =>
+          val sym = y1.symbol
+          def isUseClassParam: Boolean =
+            sym.owner match
+              case classSym: ClassSymbol =>
+                val paramSym = classSym.primaryConstructor.paramNamed(sym.name)
+                paramSym.isUseParam
+              case _ => false
+          isUseClassParam && trySubpath(y1)
         case _ => false
       || this.match
           case Reach(x1) => x1.subsumes(y.stripReach)
@@ -858,4 +868,4 @@ object Capabilities:
       case tp1 => tp1
   end toResultInResults
 
-end Capabilities
\ No newline at end of file
+end Capabilities
diff --git a/tests/neg-custom-args/captures/cc-class-this-reach1.scala b/tests/neg-custom-args/captures/cc-class-this-reach1.scala
new file mode 100644
index 000000000000..1eff58a6202b
--- /dev/null
+++ b/tests/neg-custom-args/captures/cc-class-this-reach1.scala
@@ -0,0 +1,8 @@
+import language.experimental.captureChecking
+import caps.*
+trait Runner:
+  def run: () ->{this} Unit
+class Runner1(f: List[() => Unit]) extends Runner:
+  def run: () ->{f*} Unit = f.head // error
+class Runner2(@use f: List[() => Unit]) extends Runner:
+  def run: () ->{f*} Unit = f.head // ok

From 2b81ca94e0b11de4f2594a7c378940355115f968 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Thu, 29 May 2025 15:26:59 +0200
Subject: [PATCH 10/14] Capture check stdlib under new scheme

---
 scala2-library-cc/src/scala/collection/Iterable.scala     | 4 ++--
 scala2-library-cc/src/scala/collection/IterableOnce.scala | 5 ++---
 scala2-library-cc/src/scala/collection/Iterator.scala     | 8 ++++----
 scala2-library-cc/src/scala/collection/Map.scala          | 4 ++--
 scala2-library-cc/src/scala/collection/SortedMap.scala    | 2 +-
 .../src/scala/collection/StrictOptimizedIterableOps.scala | 2 +-
 .../src/scala/collection/StrictOptimizedMapOps.scala      | 2 +-
 scala2-library-cc/src/scala/collection/View.scala         | 4 ++--
 scala2-library-cc/src/scala/collection/WithFilter.scala   | 2 +-
 .../src/scala/collection/immutable/LazyListIterable.scala | 4 ++--
 .../src/scala/collection/immutable/List.scala             | 2 +-
 .../src/scala/collection/immutable/TreeSeqMap.scala       | 2 +-
 12 files changed, 20 insertions(+), 21 deletions(-)

diff --git a/scala2-library-cc/src/scala/collection/Iterable.scala b/scala2-library-cc/src/scala/collection/Iterable.scala
index 6556f31d378d..73b6a47134e7 100644
--- a/scala2-library-cc/src/scala/collection/Iterable.scala
+++ b/scala2-library-cc/src/scala/collection/Iterable.scala
@@ -682,7 +682,7 @@ trait IterableOps[+A, +CC[_], +C] extends Any with IterableOnce[A] with Iterable
 
   def map[B](f: A => B): CC[B]^{this, f} = iterableFactory.from(new View.Map(this, f))
 
-  def flatMap[B](f: A => IterableOnce[B]^): CC[B]^{this, f} = iterableFactory.from(new View.FlatMap(this, f))
+  def flatMap[B](@caps.use f: A => IterableOnce[B]^): CC[B]^{this, f*} = iterableFactory.from(new View.FlatMap(this, f))
 
   def flatten[B](implicit asIterable: A -> IterableOnce[B]): CC[B]^{this} = flatMap(asIterable)
 
@@ -902,7 +902,7 @@ object IterableOps {
     def map[B](f: A => B): CC[B]^{this, f} =
       self.iterableFactory.from(new View.Map(filtered, f))
 
-    def flatMap[B](f: A => IterableOnce[B]^): CC[B]^{this, f} =
+    def flatMap[B](@caps.use f: A => IterableOnce[B]^): CC[B]^{this, f*} =
       self.iterableFactory.from(new View.FlatMap(filtered, f))
 
     def foreach[U](f: A => U): Unit = filtered.foreach(f)
diff --git a/scala2-library-cc/src/scala/collection/IterableOnce.scala b/scala2-library-cc/src/scala/collection/IterableOnce.scala
index 7ea62a9e1a65..803d97e963c7 100644
--- a/scala2-library-cc/src/scala/collection/IterableOnce.scala
+++ b/scala2-library-cc/src/scala/collection/IterableOnce.scala
@@ -246,10 +246,9 @@ final class IterableOnceExtensionMethods[A](private val it: IterableOnce[A]) ext
   }
 
   @deprecated("Use .iterator.flatMap instead or consider requiring an Iterable", "2.13.0")
-  def flatMap[B](f: A => IterableOnce[B]^): IterableOnce[B]^{f} = it match {
+  def flatMap[B](@caps.use f: A => IterableOnce[B]^): IterableOnce[B]^{f*} = it match
     case it: Iterable[A] => it.flatMap(f)
     case _ => it.iterator.flatMap(f)
-  }
 
   @deprecated("Use .iterator.sameElements instead", "2.13.0")
   def sameElements[B >: A](that: IterableOnce[B]): Boolean = it.iterator.sameElements(that)
@@ -439,7 +438,7 @@ trait IterableOnceOps[+A, +CC[_], +C] extends Any { this: IterableOnce[A]^ =>
    *  @return       a new $coll resulting from applying the given collection-valued function
    *                `f` to each element of this $coll and concatenating the results.
    */
-  def flatMap[B](f: A => IterableOnce[B]^): CC[B]^{this, f}
+  def flatMap[B](@caps.use f: A => IterableOnce[B]^): CC[B]^{this, f*}
 
   /** Converts this $coll of iterable collections into
    *  a $coll formed by the elements of these iterable
diff --git a/scala2-library-cc/src/scala/collection/Iterator.scala b/scala2-library-cc/src/scala/collection/Iterator.scala
index 91a22caa288c..3409ede38a37 100644
--- a/scala2-library-cc/src/scala/collection/Iterator.scala
+++ b/scala2-library-cc/src/scala/collection/Iterator.scala
@@ -588,7 +588,7 @@ trait Iterator[+A] extends IterableOnce[A] with IterableOnceOps[A, Iterator, Ite
     def next() = f(self.next())
   }
 
-  def flatMap[B](f: A => IterableOnce[B]^): Iterator[B]^{this, f} = new AbstractIterator[B] {
+  def flatMap[B](@caps.use f: A => IterableOnce[B]^): Iterator[B]^{this, f*} = new AbstractIterator[B] {
     private[this] var cur: Iterator[B]^{f} = Iterator.empty
     /** Trillium logic boolean: -1 = unknown, 0 = false, 1 = true */
     private[this] var _hasNext: Int = -1
@@ -623,7 +623,7 @@ trait Iterator[+A] extends IterableOnce[A] with IterableOnceOps[A, Iterator, Ite
     }
   }
 
-  def flatten[B](implicit ev: A -> IterableOnce[B]): Iterator[B]^{this} =
+  def flatten[B](implicit ev: A -> IterableOnce[B]): Iterator[B]^{this, ev*} =
     flatMap[B](ev)
 
   def concat[B >: A](xs: => IterableOnce[B]^): Iterator[B]^{this, xs} = new Iterator.ConcatIterator[B](self).concat(xs)
@@ -982,7 +982,7 @@ object Iterator extends IterableFactory[Iterator] {
   /** Creates a target $coll from an existing source collection
     *
     * @param source Source collection
-    * @tparam A the type of the collection’s elements
+    * @tparam A the type of the collection's elements
     * @return a new $coll with the elements of `source`
     */
   override def from[A](source: IterableOnce[A]^): Iterator[A]^{source} = source.iterator
@@ -1003,7 +1003,7 @@ object Iterator extends IterableFactory[Iterator] {
 
   /**
     * @return A builder for $Coll objects.
-    * @tparam A the type of the ${coll}’s elements
+    * @tparam A the type of the ${coll}'s elements
     */
   def newBuilder[A]: Builder[A, Iterator[A]] =
     new ImmutableBuilder[A, Iterator[A]](empty[A]) {
diff --git a/scala2-library-cc/src/scala/collection/Map.scala b/scala2-library-cc/src/scala/collection/Map.scala
index 7ba393ecd242..3734ecf5bc83 100644
--- a/scala2-library-cc/src/scala/collection/Map.scala
+++ b/scala2-library-cc/src/scala/collection/Map.scala
@@ -321,7 +321,7 @@ trait MapOps[K, +V, +CC[_, _] <: IterableOps[_, AnyConstr, _], +C]
     *  @return       a new $coll resulting from applying the given collection-valued function
     *                `f` to each element of this $coll and concatenating the results.
     */
-  def flatMap[K2, V2](f: ((K, V)) => IterableOnce[(K2, V2)]^): CC[K2, V2] = mapFactory.from(new View.FlatMap(this, f))
+  def flatMap[K2, V2](@caps.use f: ((K, V)) => IterableOnce[(K2, V2)]^): CC[K2, V2] = mapFactory.from(new View.FlatMap(this, f))
 
   /** Returns a new $coll containing the elements from the left hand operand followed by the elements from the
     *  right hand operand. The element type of the $coll is the most specific superclass encompassing
@@ -383,7 +383,7 @@ object MapOps {
     def map[K2, V2](f: ((K, V)) => (K2, V2)): CC[K2, V2]^{this, f} =
       self.mapFactory.from(new View.Map(filtered, f))
 
-    def flatMap[K2, V2](f: ((K, V)) => IterableOnce[(K2, V2)]^): CC[K2, V2]^{this, f} =
+    def flatMap[K2, V2](@caps.use f: ((K, V)) => IterableOnce[(K2, V2)]^): CC[K2, V2]^{this, f*} =
       self.mapFactory.from(new View.FlatMap(filtered, f))
 
     override def withFilter(q: ((K, V)) => Boolean): WithFilter[K, V, IterableCC, CC]^{this, q} =
diff --git a/scala2-library-cc/src/scala/collection/SortedMap.scala b/scala2-library-cc/src/scala/collection/SortedMap.scala
index 876a83b2709c..546f10b452a6 100644
--- a/scala2-library-cc/src/scala/collection/SortedMap.scala
+++ b/scala2-library-cc/src/scala/collection/SortedMap.scala
@@ -208,7 +208,7 @@ object SortedMapOps {
     def map[K2 : Ordering, V2](f: ((K, V)) => (K2, V2)): CC[K2, V2] =
       self.sortedMapFactory.from(new View.Map(filtered, f))
 
-    def flatMap[K2 : Ordering, V2](f: ((K, V)) => IterableOnce[(K2, V2)]^): CC[K2, V2] =
+    def flatMap[K2 : Ordering, V2](@caps.use f: ((K, V)) => IterableOnce[(K2, V2)]^): CC[K2, V2] =
       self.sortedMapFactory.from(new View.FlatMap(filtered, f))
 
     override def withFilter(q: ((K, V)) => Boolean): WithFilter[K, V, IterableCC, MapCC, CC]^{this, q} =
diff --git a/scala2-library-cc/src/scala/collection/StrictOptimizedIterableOps.scala b/scala2-library-cc/src/scala/collection/StrictOptimizedIterableOps.scala
index 5b504a2469b5..4dae50afea6e 100644
--- a/scala2-library-cc/src/scala/collection/StrictOptimizedIterableOps.scala
+++ b/scala2-library-cc/src/scala/collection/StrictOptimizedIterableOps.scala
@@ -104,7 +104,7 @@ trait StrictOptimizedIterableOps[+A, +CC[_], +C]
     b.result()
   }
 
-  override def flatMap[B](f: A => IterableOnce[B]^): CC[B] =
+  override def flatMap[B](@caps.use f: A => IterableOnce[B]^): CC[B] =
     strictOptimizedFlatMap(iterableFactory.newBuilder, f)
 
   /**
diff --git a/scala2-library-cc/src/scala/collection/StrictOptimizedMapOps.scala b/scala2-library-cc/src/scala/collection/StrictOptimizedMapOps.scala
index a9c5e0af43b3..a26ab590e91f 100644
--- a/scala2-library-cc/src/scala/collection/StrictOptimizedMapOps.scala
+++ b/scala2-library-cc/src/scala/collection/StrictOptimizedMapOps.scala
@@ -29,7 +29,7 @@ trait StrictOptimizedMapOps[K, +V, +CC[_, _] <: IterableOps[_, AnyConstr, _], +C
   override def map[K2, V2](f: ((K, V)) => (K2, V2)): CC[K2, V2] =
     strictOptimizedMap(mapFactory.newBuilder, f)
 
-  override def flatMap[K2, V2](f: ((K, V)) => IterableOnce[(K2, V2)]^): CC[K2, V2] =
+  override def flatMap[K2, V2](@caps.use f: ((K, V)) => IterableOnce[(K2, V2)]^): CC[K2, V2] =
     strictOptimizedFlatMap(mapFactory.newBuilder, f)
 
   override def concat[V2 >: V](suffix: IterableOnce[(K, V2)]^): CC[K, V2] =
diff --git a/scala2-library-cc/src/scala/collection/View.scala b/scala2-library-cc/src/scala/collection/View.scala
index 72a073836e77..a376895b06a7 100644
--- a/scala2-library-cc/src/scala/collection/View.scala
+++ b/scala2-library-cc/src/scala/collection/View.scala
@@ -309,8 +309,8 @@ object View extends IterableFactory[View] {
 
   /** A view that flatmaps elements of the underlying collection. */
   @SerialVersionUID(3L)
-  class FlatMap[A, B](underlying: SomeIterableOps[A]^, f: A => IterableOnce[B]^) extends AbstractView[B] {
-    def iterator: Iterator[B]^{underlying, f} = underlying.iterator.flatMap(f)
+  class FlatMap[A, B](underlying: SomeIterableOps[A]^, @caps.use f: A => IterableOnce[B]^) extends AbstractView[B] {
+    def iterator: Iterator[B]^{underlying, f*} = underlying.iterator.flatMap(f)
     override def knownSize: Int = if (underlying.knownSize == 0) 0 else super.knownSize
     override def isEmpty: Boolean = iterator.isEmpty
   }
diff --git a/scala2-library-cc/src/scala/collection/WithFilter.scala b/scala2-library-cc/src/scala/collection/WithFilter.scala
index a2255a8cc0c5..3dfe920461c7 100644
--- a/scala2-library-cc/src/scala/collection/WithFilter.scala
+++ b/scala2-library-cc/src/scala/collection/WithFilter.scala
@@ -45,7 +45,7 @@ abstract class WithFilter[+A, +CC[_]] extends Serializable {
     *                of the filtered outer $coll and
     *                concatenating the results.
     */
-  def flatMap[B](f: A => IterableOnce[B]^): CC[B]^{this, f}
+  def flatMap[B](@caps.use f: A => IterableOnce[B]^): CC[B]^{this, f*}
 
   /** Applies a function `f` to all elements of the `filtered` outer $coll.
     *
diff --git a/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala b/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala
index 726b011c6929..e4e77e60127b 100644
--- a/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala
+++ b/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala
@@ -592,7 +592,7 @@ final class LazyListIterable[+A] private(@untrackedCaptures lazyState: () => Laz
     */
   // optimisations are not for speed, but for functionality
   // see tickets #153, #498, #2147, and corresponding tests in run/ (as well as run/stream_flatmap_odds.scala)
-  override def flatMap[B](f: A => IterableOnce[B]^): LazyListIterable[B]^{this, f} =
+  override def flatMap[B](@caps.use f: A => IterableOnce[B]^): LazyListIterable[B]^{this, f} =
     if (knownIsEmpty) LazyListIterable.empty
     else LazyListIterable.flatMapImpl(this, f)
 
@@ -1307,7 +1307,7 @@ object LazyListIterable extends IterableFactory[LazyListIterable] {
     extends collection.WithFilter[A, LazyListIterable] {
     private[this] val filtered = lazyList.filter(p)
     def map[B](f: A => B): LazyListIterable[B]^{this, f} = filtered.map(f)
-    def flatMap[B](f: A => IterableOnce[B]^): LazyListIterable[B]^{this, f} = filtered.flatMap(f)
+    def flatMap[B](@caps.use f: A => IterableOnce[B]^): LazyListIterable[B]^{this, f} = filtered.flatMap(f)
     def foreach[U](f: A => U): Unit = filtered.foreach(f)
     def withFilter(q: A => Boolean): collection.WithFilter[A, LazyListIterable]^{this, q} = new WithFilter(filtered, q)
   }
diff --git a/scala2-library-cc/src/scala/collection/immutable/List.scala b/scala2-library-cc/src/scala/collection/immutable/List.scala
index 913de8b0be08..ad4edf1b3989 100644
--- a/scala2-library-cc/src/scala/collection/immutable/List.scala
+++ b/scala2-library-cc/src/scala/collection/immutable/List.scala
@@ -286,7 +286,7 @@ sealed abstract class List[+A]
     }
   }
 
-  final override def flatMap[B](f: A => IterableOnce[B]^): List[B] = {
+  final override def flatMap[B](@caps.use f: A => IterableOnce[B]^): List[B] = {
     var rest = this
     var h: ::[B] = null
     var t: ::[B] = null
diff --git a/scala2-library-cc/src/scala/collection/immutable/TreeSeqMap.scala b/scala2-library-cc/src/scala/collection/immutable/TreeSeqMap.scala
index dc59d21b8b19..6fbeea560e07 100644
--- a/scala2-library-cc/src/scala/collection/immutable/TreeSeqMap.scala
+++ b/scala2-library-cc/src/scala/collection/immutable/TreeSeqMap.scala
@@ -234,7 +234,7 @@ final class TreeSeqMap[K, +V] private (
     bdr.result()
   }
 
-  override def flatMap[K2, V2](f: ((K, V)) => IterableOnce[(K2, V2)]^): TreeSeqMap[K2, V2] = {
+  override def flatMap[K2, V2](@caps.use f: ((K, V)) => IterableOnce[(K2, V2)]^): TreeSeqMap[K2, V2] = {
     val bdr = newBuilder[K2, V2](orderedBy)
     val iter = ordering.iterator
     while (iter.hasNext) {

From 5bd8efa90af3c6b0741a699cc72459ae52cb8e3c Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Thu, 29 May 2025 16:53:53 +0200
Subject: [PATCH 11/14] Hack: use monotonicity trick only for
 empty-parameter-list functions

like () ?=> T, () => T
---
 compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala | 1 +
 1 file changed, 1 insertion(+)

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index d92ed29b8a6f..acbb9911f531 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -777,6 +777,7 @@ class CheckCaptures extends Recheck, SymTransformer:
         case appType @ CapturingType(appType1, refs)
         if qualType.exists
             && !tree.fun.symbol.isConstructor
+            && funType.paramInfos.isEmpty
             && qualCaptures.mightSubcapture(refs)
             && argCaptures.forall(_.mightSubcapture(refs)) =>
           val callCaptures = argCaptures.foldLeft(qualCaptures)(_ ++ _)

From 4cc0cf5cf159027fc5ed7dc32394e593745c41fb Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Thu, 29 May 2025 16:54:21 +0200
Subject: [PATCH 12/14] Finish capture checking standard library

---
 scala2-library-cc/src/scala/collection/Iterator.scala     | 2 +-
 .../src/scala/collection/immutable/LazyListIterable.scala | 8 ++++----
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/scala2-library-cc/src/scala/collection/Iterator.scala b/scala2-library-cc/src/scala/collection/Iterator.scala
index 3409ede38a37..275e0651da3d 100644
--- a/scala2-library-cc/src/scala/collection/Iterator.scala
+++ b/scala2-library-cc/src/scala/collection/Iterator.scala
@@ -589,7 +589,7 @@ trait Iterator[+A] extends IterableOnce[A] with IterableOnceOps[A, Iterator, Ite
   }
 
   def flatMap[B](@caps.use f: A => IterableOnce[B]^): Iterator[B]^{this, f*} = new AbstractIterator[B] {
-    private[this] var cur: Iterator[B]^{f} = Iterator.empty
+    private[this] var cur: Iterator[B]^{f*} = Iterator.empty
     /** Trillium logic boolean: -1 = unknown, 0 = false, 1 = true */
     private[this] var _hasNext: Int = -1
 
diff --git a/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala b/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala
index e4e77e60127b..1f3782f8f768 100644
--- a/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala
+++ b/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala
@@ -592,7 +592,7 @@ final class LazyListIterable[+A] private(@untrackedCaptures lazyState: () => Laz
     */
   // optimisations are not for speed, but for functionality
   // see tickets #153, #498, #2147, and corresponding tests in run/ (as well as run/stream_flatmap_odds.scala)
-  override def flatMap[B](@caps.use f: A => IterableOnce[B]^): LazyListIterable[B]^{this, f} =
+  override def flatMap[B](@caps.use f: A => IterableOnce[B]^): LazyListIterable[B]^{this, f*} =
     if (knownIsEmpty) LazyListIterable.empty
     else LazyListIterable.flatMapImpl(this, f)
 
@@ -1061,11 +1061,11 @@ object LazyListIterable extends IterableFactory[LazyListIterable] {
     }
   }
 
-  private def flatMapImpl[A, B](ll: LazyListIterable[A]^, f: A => IterableOnce[B]^): LazyListIterable[B]^{ll, f} = {
+  private def flatMapImpl[A, B](ll: LazyListIterable[A]^, f: A => IterableOnce[B]^): LazyListIterable[B]^{ll, f*} = {
     // DO NOT REFERENCE `ll` ANYWHERE ELSE, OR IT WILL LEAK THE HEAD
     var restRef: LazyListIterable[A]^{ll} = ll  // restRef is captured by closure arg to newLL, so A is not recognized as parametric
     newLL {
-      var it: Iterator[B]^{ll, f} = null
+      var it: Iterator[B]^{ll, f*} = null
       var itHasNext       = false
       var rest            = restRef           // var rest = restRef.elem
       while (!itHasNext && !rest.isEmpty) {
@@ -1307,7 +1307,7 @@ object LazyListIterable extends IterableFactory[LazyListIterable] {
     extends collection.WithFilter[A, LazyListIterable] {
     private[this] val filtered = lazyList.filter(p)
     def map[B](f: A => B): LazyListIterable[B]^{this, f} = filtered.map(f)
-    def flatMap[B](@caps.use f: A => IterableOnce[B]^): LazyListIterable[B]^{this, f} = filtered.flatMap(f)
+    def flatMap[B](@caps.use f: A => IterableOnce[B]^): LazyListIterable[B]^{this, f*} = filtered.flatMap(f)
     def foreach[U](f: A => U): Unit = filtered.foreach(f)
     def withFilter(q: A => Boolean): collection.WithFilter[A, LazyListIterable]^{this, q} = new WithFilter(filtered, q)
   }

From 4c20f079119dbff66babb9ba5af4abcac24b09ca Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Mon, 2 Jun 2025 11:39:02 +0200
Subject: [PATCH 13/14] Charge deep capture set for use class params

---
 compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala | 6 +++++-
 tests/neg-custom-args/captures/cc-class-reach.scala  | 7 +++++++
 2 files changed, 12 insertions(+), 1 deletion(-)
 create mode 100644 tests/neg-custom-args/captures/cc-class-reach.scala

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index acbb9911f531..c719d57da896 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -834,10 +834,14 @@ class CheckCaptures extends Recheck, SymTransformer:
             initCs ++ FreshCap(Origin.NewCapability(core)).readOnly.singletonCaptureSet
           else initCs
         for (getterName, argType) <- mt.paramNames.lazyZip(argTypes) do
+          val paramSym = cls.primaryConstructor.paramNamed(getterName)
           val getter = cls.info.member(getterName).suchThat(_.isRefiningParamAccessor).symbol
           if !getter.is(Private) && getter.hasTrackedParts then
             refined = refined.refinedOverride(getterName, argType.unboxed) // Yichen you might want to check this
-            allCaptures ++= argType.captureSet
+            if paramSym.isUseParam then
+              allCaptures ++= argType.deepCaptureSet
+            else
+              allCaptures ++= argType.captureSet
         (refined, allCaptures)
 
       /** Augment result type of constructor with refinements and captures.
diff --git a/tests/neg-custom-args/captures/cc-class-reach.scala b/tests/neg-custom-args/captures/cc-class-reach.scala
new file mode 100644
index 000000000000..860eb782b427
--- /dev/null
+++ b/tests/neg-custom-args/captures/cc-class-reach.scala
@@ -0,0 +1,7 @@
+import language.experimental.captureChecking
+import caps.*
+class Runner(@use xs: List[() => Unit]):
+  def execute: Unit = xs.foreach(op => op())
+def test1(@use ops: List[() => Unit]): Unit =
+  val runner: Runner^{} = Runner(ops)  // error
+

From 419efc747640eafa3b6a819fca95b5693d852d4b Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Mon, 2 Jun 2025 13:27:55 +0200
Subject: [PATCH 14/14] Fix two CC errors in stdlib

They turns out not to be bugs. We cannot safely widen `{asIterable*}` to
`{}` in these cases.
---
 scala2-library-cc/src/scala/collection/Iterable.scala           | 2 +-
 .../src/scala/collection/immutable/LazyListIterable.scala       | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/scala2-library-cc/src/scala/collection/Iterable.scala b/scala2-library-cc/src/scala/collection/Iterable.scala
index 73b6a47134e7..1fc40a019c4d 100644
--- a/scala2-library-cc/src/scala/collection/Iterable.scala
+++ b/scala2-library-cc/src/scala/collection/Iterable.scala
@@ -684,7 +684,7 @@ trait IterableOps[+A, +CC[_], +C] extends Any with IterableOnce[A] with Iterable
 
   def flatMap[B](@caps.use f: A => IterableOnce[B]^): CC[B]^{this, f*} = iterableFactory.from(new View.FlatMap(this, f))
 
-  def flatten[B](implicit asIterable: A -> IterableOnce[B]): CC[B]^{this} = flatMap(asIterable)
+  def flatten[B](implicit asIterable: A -> IterableOnce[B]): CC[B]^{this, asIterable*} = flatMap(asIterable)
 
   def collect[B](pf: PartialFunction[A, B]^): CC[B]^{this, pf} =
     iterableFactory.from(new View.Collect(this, pf))
diff --git a/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala b/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala
index 1f3782f8f768..5ab128cb01d7 100644
--- a/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala
+++ b/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala
@@ -600,7 +600,7 @@ final class LazyListIterable[+A] private(@untrackedCaptures lazyState: () => Laz
     *
     * $preservesLaziness
     */
-  override def flatten[B](implicit asIterable: A -> IterableOnce[B]): LazyListIterable[B]^{this} = flatMap(asIterable)
+  override def flatten[B](implicit asIterable: A -> IterableOnce[B]): LazyListIterable[B]^{this, asIterable*} = flatMap(asIterable)
 
   /** @inheritdoc
     *