From 11c2d53bc1d8f9ad776f0a5175a6594450f330e0 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Tue, 22 Jul 2025 10:52:42 +0200
Subject: [PATCH 1/6] Improve naming and comments around "disallow roots"

---
 .../src/dotty/tools/dotc/cc/CaptureSet.scala  | 12 ++---
 .../dotty/tools/dotc/cc/CheckCaptures.scala   | 51 ++++++++++---------
 2 files changed, 32 insertions(+), 31 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index bdb7a774ca51..147924dc95ba 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -453,11 +453,11 @@ sealed abstract class CaptureSet extends Showable:
       case elem: FreshCap => elem.ccOwner.isContainedIn(rootLimit)
       case _ => false
 
-  /** Invoke `handler` if this set has (or later aquires) a root capability.
-   *  Excluded are Fresh instances unless their ccOwner is contained in `upto`.
+  /** Invoke `handler` if this set has (or later aquires) a bad root capability.
+   *  Fresh instances count as good as long as their ccOwner is outside `upto`.
    *  If `upto` is NoSymbol, all Fresh instances are admitted.
    */
-  def disallowRootCapability(upto: Symbol)(handler: () => Context ?=> Unit)(using Context): this.type =
+  def disallowBadRoots(upto: Symbol)(handler: () => Context ?=> Unit)(using Context): this.type =
     if elems.exists(isBadRoot(upto, _)) then handler()
     this
 
@@ -817,10 +817,10 @@ object CaptureSet:
       || isConst
       || varState.canRecord && { includeDep(cs); true }
 
-    override def disallowRootCapability(upto: Symbol)(handler: () => Context ?=> Unit)(using Context): this.type =
+    override def disallowBadRoots(upto: Symbol)(handler: () => Context ?=> Unit)(using Context): this.type =
       rootLimit = upto
       rootAddedHandler = handler
-      super.disallowRootCapability(upto)(handler)
+      super.disallowBadRoots(upto)(handler)
 
     override def ensureWellformed(handler: Capability => (Context) ?=> Unit)(using Context): this.type =
       newElemAddedHandler = handler
@@ -922,7 +922,7 @@ object CaptureSet:
    *  Test case: Without that tweak, logger.scala would not compile.
    */
   class RefiningVar(owner: Symbol)(using Context) extends Var(owner):
-    override def disallowRootCapability(upto: Symbol)(handler: () => Context ?=> Unit)(using Context) = this
+    override def disallowBadRoots(upto: Symbol)(handler: () => Context ?=> Unit)(using Context) = this
 
   /** A variable that is derived from some other variable via a map or filter. */
   abstract class DerivedVar(owner: Symbol, initialElems: Refs)(using @constructorOnly ctx: Context)
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index c0c42bbdb32f..b9911f04ef04 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -123,11 +123,11 @@ object CheckCaptures:
         report.error(em"$elem: $tpe is not a legal element of a capture set", ann.srcPos)
     ann.retainedSet.retainedElementsRaw.foreach(check)
 
-  /** Under the sealed policy, report an error if some part of `tp` contains the
-   *  root capability in its capture set or if it refers to a type parameter that
-   *  could possibly be instantiated with cap in a way that's visible at the type.
+  /** Disallow bad roots anywhere in type `tp``.
+   *  @param  upto  controls up to which owner local fresh capabilities should be disallowed.
+   *                See disallowBadRoots for details.
    */
-  private def disallowRootCapabilitiesIn(tp: Type, upto: Symbol, what: String, have: String, addendum: String, pos: SrcPos)(using Context) =
+  private def disallowBadRootsIn(tp: Type, upto: Symbol, what: => String, have: => String, addendum: => String, pos: SrcPos)(using Context) =
     val check = new TypeTraverser:
 
       private val seen = new EqHashSet[TypeRef]
@@ -154,7 +154,7 @@ object CheckCaptures:
           case CapturingType(parent, refs) =>
             if variance >= 0 then
               val openScopes = openExistentialScopes
-              refs.disallowRootCapability(upto): () =>
+              refs.disallowBadRoots(upto): () =>
                 def part =
                   if t eq tp then ""
                   else
@@ -182,7 +182,7 @@ object CheckCaptures:
           case t =>
             traverseChildren(t)
     check.traverse(tp)
-  end disallowRootCapabilitiesIn
+  end disallowBadRootsIn
 
   trait CheckerAPI:
     /** Complete symbol info of a val or a def */
@@ -493,7 +493,7 @@ class CheckCaptures extends Recheck, SymTransformer:
               case c1: CoreCapability =>
                 CaptureSet.ofType(c1.widen, followResult = false)
           capt.println(i"Widen reach $c to $underlying in ${env.owner}")
-          underlying.disallowRootCapability(NoSymbol): () =>
+          underlying.disallowBadRoots(NoSymbol): () =>
             report.error(em"Local capability $c in ${env.ownerString} cannot have `cap` as underlying capture set", tree.srcPos)
           recur(underlying, env, lastEnv)
 
@@ -537,8 +537,9 @@ class CheckCaptures extends Recheck, SymTransformer:
           	// Under deferredReaches, don't propagate out of methods inside terms.
           	// The use set of these methods will be charged when that method is called.
 
-      recur(cs, curEnv, null)
-      useInfos += ((tree, cs, curEnv))
+      if !cs.isAlwaysEmpty then
+        recur(cs, curEnv, null)
+        useInfos += ((tree, cs, curEnv))
     end markFree
 
     /** If capability `c` refers to a parameter that is not @use declared, report an error.
@@ -574,16 +575,16 @@ class CheckCaptures extends Recheck, SymTransformer:
         case _ =>
           tp
 
-    /** Under the sealed policy, disallow the root capability in type arguments.
-     *  Type arguments come either from a TypeApply node or from an AppliedType
+    /** Type arguments come either from a TypeApply node or from an AppliedType
      *  which represents a trait parent in a template.
-     *  Also, if a corresponding formal type parameter is declared or implied @use,
-     *  charge the deep capture set of the argument to the environent.
+     *   - Disallow global cap and result caps in such arguments.
+     *   - If a corresponding formal type parameter is declared or implied @use,
+     *     charge the deep capture set of the argument to the environent.
      *  @param  fn   the type application, of type TypeApply or TypeTree
      *  @param  sym  the constructor symbol (could be a method or a val or a class)
      *  @param  args the type arguments
      */
-    def disallowCapInTypeArgs(fn: Tree, sym: Symbol, args: List[Tree])(using Context): Unit =
+    def markFreeTypeArgs(fn: Tree, sym: Symbol, args: List[Tree])(using Context): Unit =
       def isExempt = sym.isTypeTestOrCast || defn.capsErasedValueMethods.contains(sym)
       if !isExempt then
         val paramNames = atPhase(thisPhase.prev):
@@ -596,17 +597,17 @@ class CheckCaptures extends Recheck, SymTransformer:
 
         for case (arg: TypeTree, pname) <- args.lazyZip(paramNames) do
           def where = if sym.exists then i" in an argument of $sym" else ""
-          val (addendum, errTree) =
+          def addendum =
             if arg.isInferred
-            then (i"\nThis is often caused by a local capability$where\nleaking as part of its result.", fn)
-            else if arg.span.exists then ("", arg)
-            else ("", fn)
-          disallowRootCapabilitiesIn(arg.nuType, NoSymbol,
+            then i"\nThis is often caused by a local capability$where\nleaking as part of its result."
+            else ""
+          def errTree = if !arg.isInferred && arg.span.exists then arg else fn
+          disallowBadRootsIn(arg.nuType, NoSymbol,
             i"Type variable $pname of $sym", "be instantiated to", addendum, errTree.srcPos)
 
           val param = fn.symbol.paramNamed(pname)
           if param.isUseParam then markFree(arg.nuType.deepCaptureSet, errTree)
-    end disallowCapInTypeArgs
+    end markFreeTypeArgs
 
     /** Rechecking idents involves:
      *   - adding call captures for idents referring to methods
@@ -875,7 +876,7 @@ class CheckCaptures extends Recheck, SymTransformer:
         case fun @ Select(qual, nme.apply) => qual.symbol.orElse(fun.symbol)
         case fun => fun.symbol
       def methDescr = if meth.exists then i"$meth's type " else ""
-      disallowCapInTypeArgs(tree.fun, meth, tree.args)
+      markFreeTypeArgs(tree.fun, meth, tree.args)
       val funType = super.recheckTypeApply(tree, pt)
       val res = resultToFresh(funType, Origin.ResultInstance(funType, meth))
       includeCallCaptures(tree.symbol, res, tree)
@@ -997,7 +998,7 @@ class CheckCaptures extends Recheck, SymTransformer:
                 i"\n\nNote that $sym does not count as local since it is captured by $enclStr"
               case _ =>
                 ""
-            disallowRootCapabilitiesIn(
+            disallowBadRootsIn(
               tree.tpt.nuType, NoSymbol, i"Mutable $sym", "have type", addendum, sym.srcPos)
           checkInferredResult(super.recheckValDef(tree, sym), tree)
       finally
@@ -1180,7 +1181,7 @@ class CheckCaptures extends Recheck, SymTransformer:
         for case tpt: TypeTree <- impl.parents do
           tpt.tpe match
             case AppliedType(fn, args) =>
-              disallowCapInTypeArgs(tpt, fn.typeSymbol, args.map(TypeTree(_)))
+              markFreeTypeArgs(tpt, fn.typeSymbol, args.map(TypeTree(_)))
             case _ =>
         ccState.inNestedLevelUnless(cls.is(Module)):
           super.recheckClassDef(tree, impl, cls)
@@ -1213,7 +1214,7 @@ class CheckCaptures extends Recheck, SymTransformer:
         recheck(tree.expr, pt)
       val tp = recheckTryRest(bodyType, tree.cases, tree.finalizer, pt)
       if Feature.enabled(Feature.saferExceptions) then
-        disallowRootCapabilitiesIn(tp, ctx.owner,
+        disallowBadRootsIn(tp, ctx.owner,
           "The result of `try`", "have type",
           "\nThis is often caused by a locally generated exception capability leaking as part of its result.",
           tree.srcPos)
@@ -1985,7 +1986,7 @@ class CheckCaptures extends Recheck, SymTransformer:
               if !(pos.span.isSynthetic && ctx.reporter.errorsReported)
                 && !arg.typeSymbol.name.is(WildcardParamName)
               then
-                CheckCaptures.disallowRootCapabilitiesIn(arg, NoSymbol,
+                CheckCaptures.disallowBadRootsIn(arg, NoSymbol,
                   "Array", "have element type", "",
                   pos)
               traverseChildren(t)

From b0e25eb8e3b1effa917a1412ffc14668634cdf6a Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Tue, 22 Jul 2025 12:39:03 +0200
Subject: [PATCH 2/6] Don't improve according to VAR rule for reach-caps

We used to improve c.x if type Box[T^{cs}] to c.x*. But this risks getting a follow-on
error that a usage leaks into an enclosing method. For instance, if we have

    def foo(c: Box[T^{io}]) =
      println(c.x)

we want to leave the capset of `c.x` as `{io}` instead of improving to `c.x*`
and running into an error later.
---
 .../src/dotty/tools/dotc/cc/CheckCaptures.scala    |  8 +++-----
 tests/neg-custom-args/captures/sep-box.check       | 14 +++++++-------
 2 files changed, 10 insertions(+), 12 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index b9911f04ef04..94449d60541a 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -1581,11 +1581,9 @@ class CheckCaptures extends Recheck, SymTransformer:
     private def improveCaptures(widened: Type, prefix: Type)(using Context): Type = prefix match
       case ref: Capability if ref.isTracked =>
         widened match
-          case widened @ CapturingType(p, refs) if ref.singletonCaptureSet.mightSubcapture(refs) =>
-            val improvedCs =
-              if widened.isBoxed then ref.reach.singletonCaptureSet
-              else ref.singletonCaptureSet
-            widened.derivedCapturingType(p, improvedCs)
+          case widened @ CapturingType(p, refs)
+          if ref.singletonCaptureSet.mightSubcapture(refs) && !widened.isBoxed =>
+            widened.derivedCapturingType(p, ref.singletonCaptureSet)
               .showing(i"improve $widened to $result", capt)
           case _ => widened
       case _ => widened
diff --git a/tests/neg-custom-args/captures/sep-box.check b/tests/neg-custom-args/captures/sep-box.check
index a0fe7340b93b..590c0b01c757 100644
--- a/tests/neg-custom-args/captures/sep-box.check
+++ b/tests/neg-custom-args/captures/sep-box.check
@@ -1,16 +1,16 @@
 -- Error: tests/neg-custom-args/captures/sep-box.scala:41:9 ------------------------------------------------------------
 41 |  par(h1.value, h2.value) // error
    |      ^^^^^^^^
-   |Separation failure: argument of type  Ref^{h1.value*}
+   |Separation failure: argument of type  Ref^{xs*}
    |to method par: (x: Ref^, y: Ref^): Unit
    |corresponds to capture-polymorphic formal parameter x of type  Ref^
-   |and hides capabilities  {h1.value*}.
-   |Some of these overlap with the captures of the second argument with type  Ref^{h2.value*}.
+   |and hides capabilities  {xs*}.
+   |Some of these overlap with the captures of the second argument with type  Ref^{xs*}.
    |
-   |  Hidden set of current argument        : {h1.value*}
-   |  Hidden footprint of current argument  : {h1.value*, xs*}
-   |  Capture set of second argument        : {h2.value*}
-   |  Footprint set of second argument      : {h2.value*, xs*}
+   |  Hidden set of current argument        : {xs*}
+   |  Hidden footprint of current argument  : {xs*}
+   |  Capture set of second argument        : {xs*}
+   |  Footprint set of second argument      : {xs*}
    |  The two sets overlap at               : {xs*}
    |
    |where:    ^ refers to a fresh root capability classified as Mutable created in method test when checking argument to parameter x of method par

From b1603227467b7881e22706e210221a8875dd3eb6 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Tue, 22 Jul 2025 23:50:20 +0200
Subject: [PATCH 3/6] First stab at useless checking

Several TODOs need follow-up
---
 .../src/dotty/tools/dotc/cc/CaptureOps.scala  | 40 ++++++++++++++-----
 .../dotty/tools/dotc/cc/CheckCaptures.scala   |  1 +
 compiler/src/dotty/tools/dotc/cc/Setup.scala  | 18 +++++++--
 .../src/dotty/tools/dotc/cc/ccConfig.scala    |  7 ++--
 .../dotty/tools/dotc/core/Definitions.scala   | 12 +++---
 .../tools/dotc/printing/PlainPrinter.scala    |  1 +
 .../src/dotty/tools/dotc/typer/Typer.scala    |  6 ++-
 .../dotty/tools/dotc/CompilationTests.scala   |  6 +--
 library/src/scala/caps/package.scala          | 16 ++++++--
 project/Build.scala                           |  4 +-
 .../captures/unsound-reach-7.scala            |  0
 .../captures/use-override.scala               |  0
 .../neg-custom-args/captures/bad-uses-2.scala |  4 +-
 .../captures/cc-annot-value-classes.scala     |  4 +-
 .../captures/cc-poly-source.scala             |  2 +-
 .../captures/classifiers-secondclass.scala    |  8 ++--
 tests/neg-custom-args/captures/dcs-tvar.check |  8 +++-
 tests/neg-custom-args/captures/dcs-tvar.scala |  2 +-
 .../captures/delayedRunops.check              | 30 +++++++-------
 .../captures/delayedRunops.scala              |  5 +--
 .../captures/gears-problem-1.scala            |  4 +-
 .../captures/gears-problem.check              | 20 +++++-----
 .../captures/gears-problem.scala              |  8 ++--
 tests/neg-custom-args/captures/i20503.scala   |  2 +-
 tests/neg-custom-args/captures/i21347.check   | 13 +++---
 tests/neg-custom-args/captures/i21347.scala   |  4 +-
 tests/neg-custom-args/captures/i21614.check   |  6 +--
 tests/neg-custom-args/captures/i21614.scala   |  4 +-
 tests/neg-custom-args/captures/i23303.scala   |  4 +-
 .../captures/leak-problem-2.scala             |  2 +-
 .../captures/leak-problem-unboxed.scala       | 12 +++---
 .../captures/leak-problem.scala               |  4 +-
 tests/neg-custom-args/captures/reaches.check  |  2 +-
 tests/neg-custom-args/captures/reaches.scala  | 18 ++++-----
 .../captures/sep-consume.check                | 12 ------
 .../captures/sep-consume.scala                |  7 ++--
 .../captures/spread-problem.check             | 18 ++++-----
 .../captures/spread-problem.scala             |  2 +-
 .../captures/unbox-overrides.check            | 27 ++++++++-----
 .../captures/unbox-overrides.scala            | 20 +++++-----
 .../captures/use-alternatives.scala           | 25 ++++++++++++
 .../neg-custom-args/captures/use-capset.check | 20 +++++-----
 .../neg-custom-args/captures/use-capset.scala |  8 ++--
 tests/new/test.scala                          |  4 +-
 .../captures/capset-problem.scala             | 17 ++++++++
 .../captures/capset-uses.scala                | 11 +++++
 .../captures/cc-poly-source-capability.scala  | 17 ++++----
 .../captures/cc-use-iterable.scala            |  4 +-
 .../pos-custom-args/captures/dep-reach.scala  |  6 +--
 .../captures/gears-problem-poly.scala         |  8 ++--
 tests/pos-custom-args/captures/i15749.scala   | 22 +++++-----
 tests/pos-custom-args/captures/i15749a.scala  |  6 +--
 tests/pos-custom-args/captures/i18699.scala   |  6 +--
 .../captures/reach-capability.scala           |  4 +-
 .../captures/reach-problem.scala              |  2 +-
 tests/pos-custom-args/captures/reaches.scala  |  8 ++--
 .../pos-custom-args/captures/sep-pairs.scala  | 19 +++++++--
 .../captures/use-alternatives.scala           | 18 +--------
 .../stdlibExperimentalDefinitions.scala       |  1 +
 59 files changed, 334 insertions(+), 235 deletions(-)
 rename tests/{ => invalid}/neg-custom-args/captures/unsound-reach-7.scala (100%)
 rename tests/{ => invalid}/neg-custom-args/captures/use-override.scala (100%)
 create mode 100644 tests/neg-custom-args/captures/use-alternatives.scala
 create mode 100644 tests/pos-custom-args/captures/capset-problem.scala
 create mode 100644 tests/pos-custom-args/captures/capset-uses.scala

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
index cd8615f0f8d5..06f6331e2be0 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
@@ -99,9 +99,17 @@ extension (tp: Type)
     case AnnotatedType(tp1, ann) if tp1.derivesFrom(defn.Caps_CapSet) && ann.symbol.isRetains =>
       ann.tree.retainedSet.retainedElementsRaw
     case tp =>
-      // Nothing is a special type to represent the empty set
-      if tp.isNothingType then Nil
-      else tp :: Nil // should be checked by wellformedness
+      tp.dealiasKeepAnnots match
+        case tp: TypeRef if tp.symbol == defn.Caps_CapSet =>
+          // This can happen in cases where we try to type an eta expansion `$x => f($x)`
+          // from a polymorphic target type using capture sets. In that case the parameter type
+          // of $x is not treated as inferred is approximated to CapSet. An example is
+          // capset-problem.scala. We handle these cases by appromxating to the empty set.
+          Nil
+        case _ =>
+          // Nothing is a special type to represent the empty set
+          if tp.isNothingType then Nil
+          else tp :: Nil // should be checked by wellformedness
 
   /** A list of capabilities of a retained set. */
   def retainedElements(using Context): List[Capability] =
@@ -571,18 +579,30 @@ extension (sym: Symbol)
   def hasTrackedParts(using Context): Boolean =
     !CaptureSet.ofTypeDeeply(sym.info).isAlwaysEmpty
 
-  /** `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.
+  /** Until 3.7:
+   *    `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.
+   *  From 3.8:
+   *    `sym` is a capset parameter without a `@reserve` annotation that
+   *      - belongs to a class in a class, or
+   *      - belongs to a method where it appears in a the deep capture set of a following term parameter of the same method.
    */
   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)
-            && param.info.deepCaptureSet.elems.exists:
-                case c: TypeRef => c.symbol == sym
-                case _ => false
+        && !sym.info.hasAnnotation(defn.ReserveAnnot)
+        && (sym.owner.isClass
+            || sym.owner.rawParamss.nestedExists: param =>
+                param.is(TermParam)
+                && (!ccConfig.allowUse || param.hasAnnotation(defn.UseAnnot))
+                && param.info.deepCaptureSet.elems.exists:
+                    case c: TypeRef => c.symbol == sym
+                    case _ => false
+            || {
+              //println(i"not is use param $sym")
+              false
+            })
 
   /** `sym` or its info is annotated with `@consume`. */
   def isConsumeParam(using Context): Boolean =
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 94449d60541a..b417e017f8c7 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -1802,6 +1802,7 @@ class CheckCaptures extends Recheck, SymTransformer:
 
             checkAnnot(defn.UseAnnot)
             checkAnnot(defn.ConsumeAnnot)
+            checkAnnot(defn.ReserveAnnot)
       end OverridingPairsCheckerCC
 
       def traverse(t: Tree)(using Context) =
diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala
index 1a9d86c7d645..d043f81ba7dd 100644
--- a/compiler/src/dotty/tools/dotc/cc/Setup.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -752,7 +752,8 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
     end postProcess
 
     /** Check that @use and @consume annotations only appear on parameters and not on
-     *  anonymous function parameters
+     *  anonymous function parameters. Check that @use annotations don't appear
+     *  at all from 3.8 on.
      */
     def checkProperUseOrConsume(tree: Tree)(using Context): Unit = tree match
       case tree: MemberDef =>
@@ -766,11 +767,22 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
               && !(sym.is(Method) && sym.owner.isClass)
             then
               report.error(
-                em"""@consume cannot be used here. Only memeber methods and their term parameters
+                em"""@consume cannot be used here. Only member methods and their term parameters
                     |can have @consume annotations.""",
                 tree.srcPos)
           else if annotCls == defn.UseAnnot then
-            if !isMethodParam then
+            if !ccConfig.allowUse then
+              if sym.is(TypeParam) then
+                report.error(
+                  em"""@use is redundant here and should no longer be written explicitly.
+                      |Capset variables are always implicitly used, unless they are annotated with @caps.preserve.""",
+                  tree.srcPos)
+              else
+                report.error(
+                  em"""@use is no longer supported. Instead of @use you can introduce capset
+                      |variables for the polymorphic parts of parameter types.""",
+                  tree.srcPos)
+            else if !isMethodParam then
               report.error(
                 em"@use cannot be used here. Only method parameters can have @use annotations.",
                 tree.srcPos)
diff --git a/compiler/src/dotty/tools/dotc/cc/ccConfig.scala b/compiler/src/dotty/tools/dotc/cc/ccConfig.scala
index 4cc2264c12cb..0e1e02d39c5a 100644
--- a/compiler/src/dotty/tools/dotc/cc/ccConfig.scala
+++ b/compiler/src/dotty/tools/dotc/cc/ccConfig.scala
@@ -50,12 +50,11 @@ object ccConfig:
   def useFreshLevels(using Context): Boolean =
     Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.7`)
 
-  /** If true, turn on separation checking */
-  def useSepChecks(using Context): Boolean =
-    Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.8`)
-
   /** Not used currently. Handy for trying out new features */
   def newScheme(using ctx: Context): Boolean =
     Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.7`)
 
+  def allowUse(using Context): Boolean =
+    Feature.sourceVersion.stable.isAtMost(SourceVersion.`3.7`)
+
 end ccConfig
diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala
index 386bae0f68c2..0e3ea5bb7a47 100644
--- a/compiler/src/dotty/tools/dotc/core/Definitions.scala
+++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala
@@ -1074,8 +1074,9 @@ class Definitions {
   @tu lazy val UncheckedVarianceAnnot: ClassSymbol = requiredClass("scala.annotation.unchecked.uncheckedVariance")
   @tu lazy val UncheckedCapturesAnnot: ClassSymbol = requiredClass("scala.annotation.unchecked.uncheckedCaptures")
   @tu lazy val UntrackedCapturesAnnot: ClassSymbol = requiredClass("scala.caps.unsafe.untrackedCaptures")
-  @tu lazy val UseAnnot:  ClassSymbol = requiredClass("scala.caps.use")
-  @tu lazy val ConsumeAnnot:  ClassSymbol = requiredClass("scala.caps.consume")
+  @tu lazy val UseAnnot: ClassSymbol = requiredClass("scala.caps.use")
+  @tu lazy val ConsumeAnnot: ClassSymbol = requiredClass("scala.caps.consume")
+  @tu lazy val ReserveAnnot: ClassSymbol = requiredClass("scala.caps.reserve")
   @tu lazy val RefineOverrideAnnot:  ClassSymbol = requiredClass("scala.caps.internal.refineOverride")
   @tu lazy val VolatileAnnot: ClassSymbol = requiredClass("scala.volatile")
   @tu lazy val LanguageFeatureMetaAnnot: ClassSymbol = requiredClass("scala.annotation.meta.languageFeature")
@@ -1476,7 +1477,7 @@ class Definitions {
   def patchStdLibClass(denot: ClassDenotation)(using Context): Unit =
     // Do not patch the stdlib files if we explicitly disable it
     // This is only to be used during the migration of the stdlib
-    if ctx.settings.YnoStdlibPatches.value then 
+    if ctx.settings.YnoStdlibPatches.value then
       return
 
     def patch2(denot: ClassDenotation, patchCls: Symbol): Unit =
@@ -2111,8 +2112,9 @@ class Definitions {
     CapsModule, CapsModule.moduleClass, PureClass,
     Caps_Capability, // TODO: Remove when Capability is stabilized
     RequiresCapabilityAnnot,
-    captureRoot, Caps_CapSet, Caps_ContainsTrait, Caps_ContainsModule, Caps_ContainsModule.moduleClass, UseAnnot,
-    Caps_Mutable, Caps_Sharable, Caps_Control, Caps_Classifier, ConsumeAnnot,
+    captureRoot, Caps_CapSet, Caps_ContainsTrait, Caps_ContainsModule, Caps_ContainsModule.moduleClass,
+    Caps_Mutable, Caps_Sharable, Caps_Control, Caps_Classifier,
+    ConsumeAnnot, UseAnnot, ReserveAnnot,
     CapsUnsafeModule, CapsUnsafeModule.moduleClass,
     CapsInternalModule, CapsInternalModule.moduleClass,
     RetainsAnnot, RetainsCapAnnot, RetainsByNameAnnot)
diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
index 03bffc65fbc7..877a2ba309da 100644
--- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
@@ -137,6 +137,7 @@ class PlainPrinter(_ctx: Context) extends Printer {
     keywordText("erased ").provided(isErased)
     ~ specialAnnotText(defn.UseAnnot, arg)
     ~ specialAnnotText(defn.ConsumeAnnot, arg)
+    ~ specialAnnotText(defn.ReserveAnnot, arg)
     ~ homogenizeArg(arg).match
         case arg: TypeBounds => "?" ~ toText(arg)
         case arg => toText(arg)
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index 10a061ab8fc4..2840dcbcac52 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -602,7 +602,11 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
   def typedIdent(tree: untpd.Ident, pt: Type)(using Context): Tree =
     record("typedIdent")
     val name = tree.name
-    def kind = if (name.isTermName) "" else "type "
+    def kind =
+      if name.isTermName then
+        if ctx.mode.is(Mode.InCaptureSet) then "capability "
+        else ""
+      else "type "
     typr.println(s"typed ident $kind$name in ${ctx.owner}")
     if ctx.mode.is(Mode.Pattern) then
       if name == nme.WILDCARD then
diff --git a/compiler/test/dotty/tools/dotc/CompilationTests.scala b/compiler/test/dotty/tools/dotc/CompilationTests.scala
index c49efceff73f..f1e73c314fc7 100644
--- a/compiler/test/dotty/tools/dotc/CompilationTests.scala
+++ b/compiler/test/dotty/tools/dotc/CompilationTests.scala
@@ -37,7 +37,7 @@ class CompilationTests {
       compileFilesInDir("tests/pos-special/sourcepath/outer", defaultOptions.and("-sourcepath", "tests/pos-special/sourcepath")),
       compileFile("tests/pos-special/sourcepath/outer/nested/Test4.scala", defaultOptions.and("-sourcepath", "tests/pos-special/sourcepath")),
       compileFilesInDir("tests/pos-scala2", defaultOptions.and("-source", "3.0-migration")),
-      compileFilesInDir("tests/pos-custom-args/captures", defaultOptions.and("-language:experimental.captureChecking", "-language:experimental.separationChecking")),
+      compileFilesInDir("tests/pos-custom-args/captures", defaultOptions.and("-language:experimental.captureChecking", "-language:experimental.separationChecking", "-source", "3.8")),
       compileFile("tests/pos-special/utf8encoded.scala", defaultOptions.and("-encoding", "UTF8")),
       compileFile("tests/pos-special/utf16encoded.scala", defaultOptions.and("-encoding", "UTF16")),
       compileDir("tests/pos-special/i18589", defaultOptions.and("-Wsafe-init").without("-Ycheck:all")),
@@ -149,7 +149,7 @@ class CompilationTests {
     aggregateTests(
       compileFilesInDir("tests/neg", defaultOptions, FileFilter.exclude(TestSources.negScala2LibraryTastyExcludelisted)),
       compileFilesInDir("tests/neg-deep-subtype", allowDeepSubtypes),
-      compileFilesInDir("tests/neg-custom-args/captures", defaultOptions.and("-language:experimental.captureChecking", "-language:experimental.separationChecking")),
+      compileFilesInDir("tests/neg-custom-args/captures", defaultOptions.and("-language:experimental.captureChecking", "-language:experimental.separationChecking", "-source", "3.8")),
       compileFile("tests/neg-custom-args/sourcepath/outer/nested/Test1.scala", defaultOptions.and("-sourcepath", "tests/neg-custom-args/sourcepath")),
       compileDir("tests/neg-custom-args/sourcepath2/hi", defaultOptions.and("-sourcepath", "tests/neg-custom-args/sourcepath2", "-Xfatal-warnings")),
       compileList("duplicate source", List(
@@ -172,7 +172,7 @@ class CompilationTests {
     aggregateTests(
       compileFilesInDir("tests/run", defaultOptions.and("-Wsafe-init")),
       compileFilesInDir("tests/run-deep-subtype", allowDeepSubtypes),
-      compileFilesInDir("tests/run-custom-args/captures", allowDeepSubtypes.and("-language:experimental.captureChecking", "-language:experimental.separationChecking")),
+      compileFilesInDir("tests/run-custom-args/captures", allowDeepSubtypes.and("-language:experimental.captureChecking", "-language:experimental.separationChecking", "-source", "3.8")),
       // Run tests for legacy lazy vals.
       compileFilesInDir("tests/run", defaultOptions.and("-Wsafe-init", "-Ylegacy-lazy-vals", "-Ycheck-constraint-deps"), FileFilter.include(TestSources.runLazyValsAllowlist)),
     ).checkRuns()
diff --git a/library/src/scala/caps/package.scala b/library/src/scala/caps/package.scala
index 2f466af166e3..9633643ed777 100644
--- a/library/src/scala/caps/package.scala
+++ b/library/src/scala/caps/package.scala
@@ -70,15 +70,25 @@ object Contains:
   @experimental
   given containsImpl[C >: CapSet <: CapSet @retainsCap, R <: Singleton]: Contains[C, R]()
 
-/** An annotation on parameters `x` stating that the method's body makes
- *  use of the reach capability `x*`. Consequently, when calling the method
- *  we need to charge the deep capture set of the actual argiment to the
+/** An annotation on capset parameters `C` stating that the method's body does not
+ *  have `C` in its use-set. `C` might be accessed under a box in the method
+ *  or in the result type of the method. Consequently, when calling the method
+ *  we do not need to charge the capture set of the actual argiment to the
  *  environment.
  *
  *  Note: This should go into annotations. For now it is here, so that we
  *  can experiment with it quickly between minor releases
  */
 @experimental
+final class reserve extends annotation.StaticAnnotation
+
+/** Allowed only for source versions up to 3.7:
+ *  An annotation on parameters `x` stating that the method's body makes
+ *  use of the reach capability `x*`. Consequently, when calling the method
+ *  we need to charge the deep capture set of the actual argiment to the
+ *  environment.
+ */
+@experimental
 final class use extends annotation.StaticAnnotation
 
 /** An annotations on parameters and update methods.
diff --git a/project/Build.scala b/project/Build.scala
index 6fe56c8735b1..e8233f70f51a 100644
--- a/project/Build.scala
+++ b/project/Build.scala
@@ -1452,7 +1452,7 @@ object Build {
       moduleName    := "scala-library",
       version       := dottyVersion,
       versionScheme := Some("semver-spec"),
-      // sbt defaults to scala 2.12.x and metals will report issues as it doesn't consider the project a scala 3 project 
+      // sbt defaults to scala 2.12.x and metals will report issues as it doesn't consider the project a scala 3 project
       // (not the actual version we use to compile the project)
       scalaVersion  := referenceVersion,
       crossPaths    := false, // org.scala-lang:scala-library doesn't have a crosspath
@@ -1606,7 +1606,7 @@ object Build {
     settings(scala2LibraryBootstrappedSettings).
     settings(
       moduleName := "scala2-library-cc",
-      scalacOptions += "-language:experimental.separationChecking" // for separation checking
+      scalacOptions ++= List("-language:experimental.separationChecking", "-source", "3.8") // for @use changes
     )
 
   lazy val scala2LibraryBootstrappedSettings = Seq(
diff --git a/tests/neg-custom-args/captures/unsound-reach-7.scala b/tests/invalid/neg-custom-args/captures/unsound-reach-7.scala
similarity index 100%
rename from tests/neg-custom-args/captures/unsound-reach-7.scala
rename to tests/invalid/neg-custom-args/captures/unsound-reach-7.scala
diff --git a/tests/neg-custom-args/captures/use-override.scala b/tests/invalid/neg-custom-args/captures/use-override.scala
similarity index 100%
rename from tests/neg-custom-args/captures/use-override.scala
rename to tests/invalid/neg-custom-args/captures/use-override.scala
diff --git a/tests/neg-custom-args/captures/bad-uses-2.scala b/tests/neg-custom-args/captures/bad-uses-2.scala
index 2b4d6eebb2f0..d8bc3eca93e6 100644
--- a/tests/neg-custom-args/captures/bad-uses-2.scala
+++ b/tests/neg-custom-args/captures/bad-uses-2.scala
@@ -3,11 +3,11 @@ class TestUse:
   @use def F = ???  // error
   @use val x = ???  // error
   @use type T       // error
-  def foo[@use T](@use c: T): Unit = ??? // OK
+  def foo[@use T](@use c: T): Unit = ??? // error // error
 
 class TestConsume:
   @consume def F = ???  // ok
   @consume val x = ???  // error
   @consume type T       // error
-  def foo[@consume T](@use c: T): Unit = ??? // error
+  def foo[@consume T](@use c: T): Unit = ??? // error // error
 
diff --git a/tests/neg-custom-args/captures/cc-annot-value-classes.scala b/tests/neg-custom-args/captures/cc-annot-value-classes.scala
index 745b1c85b8b1..f5b6681a1c0b 100644
--- a/tests/neg-custom-args/captures/cc-annot-value-classes.scala
+++ b/tests/neg-custom-args/captures/cc-annot-value-classes.scala
@@ -2,11 +2,11 @@ import language.experimental.captureChecking
 import caps.*
 
 class Runner(val x: Int) extends AnyVal:
-  def runOps(@use ops: List[() => Unit]): Unit =
+  def runOps[C^](ops: List[() ->{C} Unit]): Unit =
     ops.foreach(_())  // ok
 
 class RunnerAlt(val x: Int):
-  def runOps(@use ops: List[() => Unit]): Unit =
+  def runOps[C^](ops: List[() ->{C} Unit]): Unit =
     ops.foreach(_())  // ok, of course
 
 class RunnerAltAlt(val x: Int) extends AnyVal:
diff --git a/tests/neg-custom-args/captures/cc-poly-source.scala b/tests/neg-custom-args/captures/cc-poly-source.scala
index 915903d670e8..4ef03750e7cb 100644
--- a/tests/neg-custom-args/captures/cc-poly-source.scala
+++ b/tests/neg-custom-args/captures/cc-poly-source.scala
@@ -25,7 +25,7 @@ import caps.use
     val ls = src.allListeners
     val _: Set[Listener^{lbl1, lbl2}] = ls
 
-  def test2(@use lbls: List[Label^]) =
+  def test2[C^](lbls: List[Label^{C}]) =
     def makeListener(lbl: Label^): Listener^{lbl} = ???
     val listeners = lbls.map(makeListener) // error
       // we get an error here because we no longer allow contravariant cap
diff --git a/tests/neg-custom-args/captures/classifiers-secondclass.scala b/tests/neg-custom-args/captures/classifiers-secondclass.scala
index c4378df5f9a5..cfd9e6bebbd4 100644
--- a/tests/neg-custom-args/captures/classifiers-secondclass.scala
+++ b/tests/neg-custom-args/captures/classifiers-secondclass.scala
@@ -28,7 +28,7 @@ object Levels:
 
   // Unfortunately, we do not have @use lambdas yet
   trait UseFunction[U]:
-    def apply(@use f: File^): U
+    def apply[C^](f: File^{C}): U
 
   def withFile[U](name: String)(block: UseFunction[U]): U = block(File(name)) // unrestricted use of files & other capabilities
   def parReduce[U](xs: Seq[U])(op: (U, U) ->{cap.only[Read]} U): U = xs.reduce(op) // only Read-classified allowed
@@ -36,7 +36,7 @@ object Levels:
   @main def test =
     withFile("foo.txt"):
       new UseFunction[Unit]:
-        def apply(@use f: File^): Unit =
+        def apply[C^](f: File^{C}): Unit =
           f.read() // ok
           parReduce(1 to 1000): (a, b) =>
             a * b * f.read()    // ok
@@ -48,10 +48,10 @@ object Levels:
   def testMulti =
     withFile("foo.txt"):
       new UseFunction[Unit]:
-        def apply(@use f: File^): Unit =
+        def apply[C^](f: File^{C}): Unit =
           withFile("bar.txt"):
             new UseFunction[Unit]:
-              def apply(@use g: File^): Unit =
+              def apply[C^](g: File^{C}): Unit =
                 f.read() // ok
                 g.read() // ok
                 parReduce(1 to 1000): (a, b) =>
diff --git a/tests/neg-custom-args/captures/dcs-tvar.check b/tests/neg-custom-args/captures/dcs-tvar.check
index 65fc12f82ba0..aaf27ddaae65 100644
--- a/tests/neg-custom-args/captures/dcs-tvar.check
+++ b/tests/neg-custom-args/captures/dcs-tvar.check
@@ -1,14 +1,18 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/dcs-tvar.scala:6:2 ---------------------------------------
 6 |  () => runOps(xs) // error
   |  ^^^^^^^^^^^^^^^^
-  |  Found:    () ->{xs*} Unit
+  |  Found:    () => Unit
   |  Required: () -> Unit
   |
+  |  where:    => refers to a fresh root capability in the type of type T
+  |
   | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/dcs-tvar.scala:9:2 ---------------------------------------
 9 |  () => runOps(xs) // error
   |  ^^^^^^^^^^^^^^^^
-  |  Found:    () ->{xs*} Unit
+  |  Found:    () => Unit
   |  Required: () -> Unit
   |
+  |  where:    => refers to a fresh root capability in the type of type U
+  |
   | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/dcs-tvar.scala b/tests/neg-custom-args/captures/dcs-tvar.scala
index 381c08b4d351..9f61f4ad16cd 100644
--- a/tests/neg-custom-args/captures/dcs-tvar.scala
+++ b/tests/neg-custom-args/captures/dcs-tvar.scala
@@ -1,6 +1,6 @@
 import caps.use
 
-def runOps(@use xs: List[() => Unit]): Unit = ???
+def runOps[C^](xs: List[() ->{C} Unit]): Unit = ???
 
 def f[T <: List[() => Unit]](xs: T): () -> Unit =
   () => runOps(xs) // error
diff --git a/tests/neg-custom-args/captures/delayedRunops.check b/tests/neg-custom-args/captures/delayedRunops.check
index 5554a32bc10e..b565acb66427 100644
--- a/tests/neg-custom-args/captures/delayedRunops.check
+++ b/tests/neg-custom-args/captures/delayedRunops.check
@@ -1,27 +1,27 @@
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/delayedRunops.scala:15:4 ---------------------------------
-15 |    () => // error
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/delayedRunops.scala:14:4 ---------------------------------
+14 |    () => // error
    |    ^
    |    Found:    () ->{ops*} Unit
    |    Required: () -> Unit
-16 |      val ops1 = ops
-17 |      runOps(ops1)
+15 |      val ops1 = ops
+16 |      runOps(ops1)
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/delayedRunops.scala:27:4 ---------------------------------
-27 |    () => // error
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/delayedRunops.scala:26:4 ---------------------------------
+26 |    () => // error
    |    ^
    |    Found:    () ->{ops*} Unit
    |    Required: () -> Unit
-28 |      val ops1: List[() ->{ops*} Unit] = ops
-29 |      runOps(ops1)
+27 |      val ops1: List[() ->{ops*} Unit] = ops
+28 |      runOps(ops1)
    |
    | longer explanation available when compiling with `-explain`
--- Error: tests/neg-custom-args/captures/delayedRunops.scala:23:13 -----------------------------------------------------
-23 |      runOps(ops1)  // error
-   |             ^^^^
-   |             Local reach capability ops* leaks into capture scope of method delayedRunOps2.
-   |             To allow this, the parameter ops should be declared with a @use annotation
--- Error: tests/neg-custom-args/captures/delayedRunops.scala:22:16 -----------------------------------------------------
-22 |      val ops1: List[() => Unit] = ops // error
+-- Error: tests/neg-custom-args/captures/delayedRunops.scala:22:6 ------------------------------------------------------
+22 |      runOps(ops1)  // error
+   |      ^^^^^^
+   |      Local reach capability ops* leaks into capture scope of method delayedRunOps2.
+   |      To allow this, the parameter ops should be declared with a @use annotation
+-- Error: tests/neg-custom-args/captures/delayedRunops.scala:21:16 -----------------------------------------------------
+21 |      val ops1: List[() => Unit] = ops // error
    |                ^^^^^^^^^^^^^^^^
    |                Separation failure: value ops1's type List[() => Unit] hides non-local parameter ops
diff --git a/tests/neg-custom-args/captures/delayedRunops.scala b/tests/neg-custom-args/captures/delayedRunops.scala
index a4cb0129d912..a9ad226d4da1 100644
--- a/tests/neg-custom-args/captures/delayedRunops.scala
+++ b/tests/neg-custom-args/captures/delayedRunops.scala
@@ -2,12 +2,11 @@ import language.experimental.captureChecking
 
 import caps.{use, consume}
 
-  // ok
-  def runOps(@use ops: List[() => Unit]): Unit =
+  def runOps[C^](ops: List[() ->{C} Unit]): Unit =
     ops.foreach(op => op())
 
   // ok
-  def delayedRunOps(@use ops: List[() => Unit]): () ->{ops*} Unit = // @use should not be necessary in the future
+  def delayedRunOps[C^](ops: List[() ->{C} Unit]): () ->{C} Unit = // @use should not be necessary in the future
     () => runOps(ops)
 
   // unsound: impure operation pretended pure
diff --git a/tests/neg-custom-args/captures/gears-problem-1.scala b/tests/neg-custom-args/captures/gears-problem-1.scala
index 515aecd468f6..6023ed9da104 100644
--- a/tests/neg-custom-args/captures/gears-problem-1.scala
+++ b/tests/neg-custom-args/captures/gears-problem-1.scala
@@ -17,9 +17,9 @@ class Result[+T, +E]:
 case class Err[+E](e: E) extends Result[Nothing, E]
 case class Ok[+T](x: T) extends Result[T, Nothing]
 
-extension [T](@use fs: Seq[Future[T]^])
+extension [T, C^](fs: Seq[Future[T]^{C}])
   def awaitAll =
     val collector//: Collector[T]{val futures: Seq[Future[T]^{fs*}]}
        = Collector(fs)
     // val ch = collector.results // also errors
-    val fut: Future[T]^{fs*} = collector.results.read().get // error
+    val fut: Future[T]^{C} = collector.results.read().get // error
diff --git a/tests/neg-custom-args/captures/gears-problem.check b/tests/neg-custom-args/captures/gears-problem.check
index 0fc5f8c3f163..1e9c30dd30e7 100644
--- a/tests/neg-custom-args/captures/gears-problem.check
+++ b/tests/neg-custom-args/captures/gears-problem.check
@@ -1,15 +1,15 @@
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/gears-problem.scala:19:62 --------------------------------
-19 |    val fut: Future[T]^{fs*} = collector.results.read().right.get // error
-   |                               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-   |                               Found:    Future[T]^{collector.futures*}
-   |                               Required: Future[T]^{fs*}
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/gears-problem.scala:19:60 --------------------------------
+19 |    val fut: Future[T]^{C} = collector.results.read().right.get // error
+   |                             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   |                             Found:    Future[T]^{collector.futures*}
+   |                             Required: Future[T]^{C}
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/gears-problem.scala:24:34 --------------------------------
-24 |    val fut2: Future[T]^{fs*} = r.get // error
-   |                                ^^^^^
-   |                                Found:    Future[T^{}]^{collector.futures*}
-   |                                Required: Future[T]^{fs*}
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/gears-problem.scala:24:32 --------------------------------
+24 |    val fut2: Future[T]^{C} = r.get // error
+   |                              ^^^^^
+   |                              Found:    Future[T^{}]^{collector.futures*}
+   |                              Required: Future[T]^{C}
    |
    | longer explanation available when compiling with `-explain`
 there were 4 deprecation warnings; re-run with -deprecation for details
diff --git a/tests/neg-custom-args/captures/gears-problem.scala b/tests/neg-custom-args/captures/gears-problem.scala
index 8dcdaabb2100..e73a4d31a388 100644
--- a/tests/neg-custom-args/captures/gears-problem.scala
+++ b/tests/neg-custom-args/captures/gears-problem.scala
@@ -11,14 +11,14 @@ class Collector[T](val futures: Seq[Future[T]^]):
   val results: Channel[Future[T]^{futures*}] = ???
 end Collector
 
-extension [T](@use fs: Seq[Future[T]^])
+extension [T, C^](fs: Seq[Future[T]^{C}])
   def awaitAll =
-    val collector: Collector[T]{val futures: Seq[Future[T]^{fs*}]}
+    val collector: Collector[T]{val futures: Seq[Future[T]^{C}]}
        = Collector(fs)
     // val ch = collector.results // also errors
-    val fut: Future[T]^{fs*} = collector.results.read().right.get // error
+    val fut: Future[T]^{C} = collector.results.read().right.get // error
 
     val ch = collector.results
     val item = ch.read()
     val r = item.right
-    val fut2: Future[T]^{fs*} = r.get // error
\ No newline at end of file
+    val fut2: Future[T]^{C} = r.get // error
\ No newline at end of file
diff --git a/tests/neg-custom-args/captures/i20503.scala b/tests/neg-custom-args/captures/i20503.scala
index 828b6ce71137..e563ed6785cc 100644
--- a/tests/neg-custom-args/captures/i20503.scala
+++ b/tests/neg-custom-args/captures/i20503.scala
@@ -8,7 +8,7 @@ class List[+A]:
   def foreach[U](f: A => U): Unit = ???
   def nonEmpty: Boolean = ???
 
-def runOps(@use ops: List[() => Unit]): Unit =
+def runOps[C^](ops: List[() ->{C} Unit]): Unit =
   // See i20156, due to limitation in expressiveness of current system,
   // we could map over the list of impure elements. OK with existentials.
   ops.foreach(op => op())
diff --git a/tests/neg-custom-args/captures/i21347.check b/tests/neg-custom-args/captures/i21347.check
index e1845d9778d5..6985c58afd18 100644
--- a/tests/neg-custom-args/captures/i21347.check
+++ b/tests/neg-custom-args/captures/i21347.check
@@ -1,9 +1,10 @@
--- Error: tests/neg-custom-args/captures/i21347.scala:4:15 -------------------------------------------------------------
-4 |  ops.foreach: op => // error
-  |               ^
-  |               Capture set parameter C leaks into capture scope of method runOps.
-  |               To allow this, the type C should be declared with a @use annotation
-5 |    op()
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21347.scala:8:2 -----------------------------------------
+8 |  () => runOps(f :: Nil) // error
+  |  ^^^^^^^^^^^^^^^^^^^^^^
+  |  Found:    () ->{f} Unit
+  |  Required: () -> Unit
+  |
+  | longer explanation available when compiling with `-explain`
 -- Error: tests/neg-custom-args/captures/i21347.scala:11:15 ------------------------------------------------------------
 11 |  ops.foreach: op => // error
    |               ^
diff --git a/tests/neg-custom-args/captures/i21347.scala b/tests/neg-custom-args/captures/i21347.scala
index 2e37511f053c..35c4428277d6 100644
--- a/tests/neg-custom-args/captures/i21347.scala
+++ b/tests/neg-custom-args/captures/i21347.scala
@@ -1,11 +1,11 @@
 import language.experimental.captureChecking
 
 def runOps[C^](ops: List[() ->{C} Unit]): Unit =
-  ops.foreach: op => // error
+  ops.foreach: op =>
     op()
 
 def boom(f: () => Unit): () -> Unit =
-  () => runOps(f :: Nil) // now ok
+  () => runOps(f :: Nil) // error
 
 def runOpsAlt(ops: List[() => Unit]): Unit =
   ops.foreach: op => // error
diff --git a/tests/neg-custom-args/captures/i21614.check b/tests/neg-custom-args/captures/i21614.check
index 9535ce2e5b96..df2112e15bb0 100644
--- a/tests/neg-custom-args/captures/i21614.check
+++ b/tests/neg-custom-args/captures/i21614.check
@@ -10,13 +10,13 @@
 -- [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^?) ->{files*} Logger{val f: File^{_$1}}^{cap.rd, _$1}
-   |Required: File^{files*} => Logger{val f: File^?}^?
+   |Found:    (_$1: File^?) ->{C} Logger{val f: File^{_$1}}^{cap.rd, _$1}
+   |Required: File^{C} => Logger{val f: File^?}^?
    |
    |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^?): Logger{val f: File^{_$1}}^{cap.rd, _$1}
    |
-   |Note that reference <cap of (_$1: File^{files*}): Logger{val f: File^?}^?>.rd
+   |Note that reference <cap of (_$1: File^{C}): Logger{val f: File^?}^?>.rd
    |cannot be included in outer capture set ?
    |
    | 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 f5bab90f543b..fa20ced08a69 100644
--- a/tests/neg-custom-args/captures/i21614.scala
+++ b/tests/neg-custom-args/captures/i21614.scala
@@ -8,8 +8,8 @@ trait List[+T]:
 trait File extends Capability
 class Logger(f: File^) extends Capability // <- will work if we remove the extends clause
 
-def mkLoggers1[F <: File^](@use files: List[F]): List[Logger^] =
+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)?
 
-def mkLoggers2(@use files: List[File^]): List[Logger^] =
+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/i23303.scala b/tests/neg-custom-args/captures/i23303.scala
index 81bb45af315c..51cd05f53107 100644
--- a/tests/neg-custom-args/captures/i23303.scala
+++ b/tests/neg-custom-args/captures/i23303.scala
@@ -10,8 +10,8 @@ class Test:
 
 
 class Test2:
-  class Runner(@use ops: List[() => Unit]):
+  class Runner[C^](ops: List[() ->{C} Unit]):
     def execute: Unit = ops.foreach(f => f()) //ok
 
-  private def Runner2(@use ops: List[() => Unit]) =
+  private def Runner2[C^](ops: List[() ->{C} Unit]) =
     () => ops.foreach(f => f()) // ok
diff --git a/tests/neg-custom-args/captures/leak-problem-2.scala b/tests/neg-custom-args/captures/leak-problem-2.scala
index 8ca298dbdd1e..8c68cdc848ef 100644
--- a/tests/neg-custom-args/captures/leak-problem-2.scala
+++ b/tests/neg-custom-args/captures/leak-problem-2.scala
@@ -2,7 +2,7 @@ import language.experimental.captureChecking
 
 trait Source[+T]
 
-def race[T](@caps.use sources: Seq[Source[T]^]): Source[T]^{sources*} = ???
+def race[T, C^](sources: Seq[Source[T]^{C}]): Source[T]^{C} = ???
 
 def raceTwo[T](src1: Source[T]^, src2: Source[T]^): Source[T]^{}
   = race(Seq(src1, src2)) // error
diff --git a/tests/neg-custom-args/captures/leak-problem-unboxed.scala b/tests/neg-custom-args/captures/leak-problem-unboxed.scala
index 6d4c4b4c94aa..00d953b1ce09 100644
--- a/tests/neg-custom-args/captures/leak-problem-unboxed.scala
+++ b/tests/neg-custom-args/captures/leak-problem-unboxed.scala
@@ -9,18 +9,20 @@ def usingAsync[X](op: Async^ => X): X = ???
 
 case class Box[+T](get: T)
 
-def useBoxedAsync(@use x: Box[Async^]): Unit =
+def useBoxedAsync[C^](x: Box[Async^{C}]): Unit =
   val t0 = x
   val t1 = t0.get // ok
   t1.read()
 
-def useBoxedAsync1(@use x: Box[Async^]): Unit = x.get.read() // ok
+def useBoxedAsync1[C^](x: Box[Async^{C}]): Unit = x.get.read() // ok
 
 def test(): Unit =
 
-  val f: Box[Async^] => Unit = (x:  Box[Async^]) => useBoxedAsync(x) // error
-  val t1: Box[Async^] => Unit = useBoxedAsync(_) // error
-  val t2: Box[Async^] => Unit = useBoxedAsync // error
+  val f: Box[Async^] => Unit = (x: Box[Async^]) => useBoxedAsync(x) // error
+  val t0: Box[Async^] => Unit = x => useBoxedAsync(x) // TODO hould be error!
+
+  val t1: Box[Async^] => Unit = useBoxedAsync(_) // TODO should be error!
+  val t2: Box[Async^] => Unit = useBoxedAsync // TODO should be error!
   val t3 = useBoxedAsync(_) // was error, now ok
   val t4 = useBoxedAsync // was error, now ok
 
diff --git a/tests/neg-custom-args/captures/leak-problem.scala b/tests/neg-custom-args/captures/leak-problem.scala
index 9a9534052d30..bf1957014c3e 100644
--- a/tests/neg-custom-args/captures/leak-problem.scala
+++ b/tests/neg-custom-args/captures/leak-problem.scala
@@ -17,12 +17,12 @@ def useBoxedAsync(x: Box[Async^]): Unit =
 def useBoxedAsync1(x: Box[Async^]): Unit = x.get.read() // error
 
 def test(): Unit =
-  def useBoxedAsync(@use x: Box[Async^]): Unit =
+  def useBoxedAsync[C^](x: Box[Async^{C}]): Unit =
     val t0 = x
     val t1 = t0.get
     t1.read()
 
-  def useBoxedAsync1(@use x: Box[Async^]): Unit = x.get.read()
+  def useBoxedAsync1[C^](x: Box[Async^{C}]): Unit = x.get.read()
 
   val xs: Box[Async^] = ???
   val xsLambda = () => useBoxedAsync(xs) // was error now ok
diff --git a/tests/neg-custom-args/captures/reaches.check b/tests/neg-custom-args/captures/reaches.check
index 70c2b8f2a82b..64b3a3c9a736 100644
--- a/tests/neg-custom-args/captures/reaches.check
+++ b/tests/neg-custom-args/captures/reaches.check
@@ -104,7 +104,7 @@
 91 |  ps.map((x, y) => compose1(x, y)) // error
    |          ^^^^^^^^^^^^^^^^^^^^^^^
    |Found:    (x$1: (A^ ->? A^?, A^ ->? A^?)^?) ->? A^? ->? A^?
-   |Required: ((A ->{ps*} A, A ->{ps*} A)) => A^? ->? A^?
+   |Required: ((A ->{C} A, A ->{C} A)) => A^? ->? A^?
    |
    |where:    => refers to a fresh root capability created in method mapCompose2 when checking argument to parameter f of method map
    |          ^  refers to the universal root capability
diff --git a/tests/neg-custom-args/captures/reaches.scala b/tests/neg-custom-args/captures/reaches.scala
index b811b1405590..663fcd2bba28 100644
--- a/tests/neg-custom-args/captures/reaches.scala
+++ b/tests/neg-custom-args/captures/reaches.scala
@@ -12,22 +12,22 @@ class Ref[T](init: T):
   def get: T = x
   def set(y: T) = { x = y }
 
-def runAll0(@use xs: List[Proc]): Unit =
-  var cur: List[() ->{xs*} Unit] = xs
+def runAll0[C^](xs: List[() ->{C} Unit]): Unit =
+  var cur: List[() ->{C} Unit] = xs
   while cur.nonEmpty do
-    val next: () ->{xs*} Unit = cur.head
+    val next: () ->{C} Unit = cur.head
     next()
-    cur = cur.tail: List[() ->{xs*} Unit]
+    cur = cur.tail: List[() ->{C} Unit]
 
   usingFile: f => // error
     cur = (() => f.write()) :: Nil
 
-def runAll1(@use xs: List[Proc]): Unit =
-  val cur = Ref[List[() ->{xs*} Unit]](xs)  // OK, by revised VAR
+def runAll1[C^](xs: List[() ->{C} Unit]): Unit =
+  val cur = Ref[List[() ->{C} Unit]](xs)  // OK, by revised VAR
   while cur.get.nonEmpty do
-    val next: () ->{xs*} Unit = cur.get.head
+    val next: () ->{C} Unit = cur.get.head
     next()
-    cur.set(cur.get.tail: List[() ->{xs*} Unit])
+    cur.set(cur.get.tail: List[() ->{C} Unit])
 
   usingFile: f => // error
     cur.set:
@@ -87,5 +87,5 @@ def compose1[A, B, C](f: A => B, g: B => C): A ->{f, g} C =
 def mapCompose[A](ps: List[(A => A, A => A)]): List[A ->{ps*} A] =
   ps.map((x, y) => compose1(x, y)) // error
 
-def mapCompose2[A](@use ps: List[(A => A, A => A)]): List[A ->{ps*} A] =
+def mapCompose2[A, C^](ps: List[(A ->{C} A, A ->{C} A)]): List[A ->{C} A] =
   ps.map((x, y) => compose1(x, y)) // error
diff --git a/tests/neg-custom-args/captures/sep-consume.check b/tests/neg-custom-args/captures/sep-consume.check
index 9aeaf0a59cc5..e44d3235afd6 100644
--- a/tests/neg-custom-args/captures/sep-consume.check
+++ b/tests/neg-custom-args/captures/sep-consume.check
@@ -18,15 +18,3 @@
 26 |  def foo = bad(f) // error
    |                ^
    | Separation failure: argument to @consume parameter with type (f : () ->{x.rd} Unit) refers to non-local value f
--- Error: tests/neg-custom-args/captures/sep-consume.scala:34:12 -------------------------------------------------------
-34 |  println(p.fst.get) // error
-   |          ^^^^^
-   |          Separation failure: Illegal access to p.fst*, which was passed to a
-   |          @consume parameter or was used as a prefix to a @consume method on line 33
-   |          and therefore is no longer available.
--- Error: tests/neg-custom-args/captures/sep-consume.scala:40:12 -------------------------------------------------------
-40 |  println(p.fst.get) // error
-   |          ^^^^^
-   |          Separation failure: Illegal access to p.fst*, which was passed to a
-   |          @consume parameter or was used as a prefix to a @consume method on line 39
-   |          and therefore is no longer available.
diff --git a/tests/neg-custom-args/captures/sep-consume.scala b/tests/neg-custom-args/captures/sep-consume.scala
index 3d167e0674d9..7b633b814e88 100644
--- a/tests/neg-custom-args/captures/sep-consume.scala
+++ b/tests/neg-custom-args/captures/sep-consume.scala
@@ -27,15 +27,16 @@ def test3(@consume x: Ref^): Unit =
   foo()
   foo()
 
+/*
 def test4(@consume @use p: Pair[Ref^, Ref^]): Unit =
   val x: Ref^{p.fst*} = p.fst
   val y: Ref^{p.snd*} = p.snd
   badp(Pair(x, y))
-  println(p.fst.get) // error
+  println(p.fst.get)
 
 def badp(@consume p: Pair[Ref^, Ref^]): Unit = ()
 
 def test5(@consume @use p: Pair[Ref^, Ref^]): Unit =
   badp(p) // ok
-  println(p.fst.get) // error
-
+  println(p.fst.get)
+*/
diff --git a/tests/neg-custom-args/captures/spread-problem.check b/tests/neg-custom-args/captures/spread-problem.check
index 91022f920486..031c87629838 100644
--- a/tests/neg-custom-args/captures/spread-problem.check
+++ b/tests/neg-custom-args/captures/spread-problem.check
@@ -1,14 +1,12 @@
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/spread-problem.scala:8:6 ---------------------------------
+-- Error: tests/neg-custom-args/captures/spread-problem.scala:8:7 ------------------------------------------------------
 8 |  race(Seq(src1, src2)*) // error
-  |  ^^^^^^^^^^^^^^^^^^^^^^
-  |  Found:    Source[T^?]^{src1, src2}
-  |  Required: Source[T]
-  |
-  | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/spread-problem.scala:11:6 --------------------------------
+  |       ^^^^^^^^^^^^^^^^
+  |       Sequence argument type annotation `*` cannot be used here:
+  |       the corresponding parameter has type Seq[Source[T]^{C}] which is not a repeated parameter type
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/spread-problem.scala:11:7 --------------------------------
 11 |  race(src1, src2) // error
-   |  ^^^^^^^^^^^^^^^^
-   |  Found:    Source[T^?]^{src1, src2}
-   |  Required: Source[T]
+   |       ^^^^^^^^^^
+   |       Found:    (Source[T]^, Source[T]^)
+   |       Required: Seq[Source[T]^]
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/spread-problem.scala b/tests/neg-custom-args/captures/spread-problem.scala
index 75f3a615cde8..f921e3feeadd 100644
--- a/tests/neg-custom-args/captures/spread-problem.scala
+++ b/tests/neg-custom-args/captures/spread-problem.scala
@@ -2,7 +2,7 @@ import language.experimental.captureChecking
 
 trait Source[+T]
 
-def race[T](@caps.use sources: (Source[T]^)*): Source[T]^{sources*} = ???
+def race[T, C^](sources: Seq[Source[T]^{C}]): Source[T]^{C} = ???
 
 def raceTwo[T](src1: Source[T]^, src2: Source[T]^): Source[T]^{} =
   race(Seq(src1, src2)*) // error
diff --git a/tests/neg-custom-args/captures/unbox-overrides.check b/tests/neg-custom-args/captures/unbox-overrides.check
index a531b546a62a..883ab56c59a5 100644
--- a/tests/neg-custom-args/captures/unbox-overrides.check
+++ b/tests/neg-custom-args/captures/unbox-overrides.check
@@ -1,21 +1,30 @@
 -- [E164] Declaration Error: tests/neg-custom-args/captures/unbox-overrides.scala:8:6 ----------------------------------
-8 |  def foo(x: C): C        // error
+8 |  def foo[C^]: Object^{C}  // error
   |      ^
-  |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
+  |error overriding method foo in trait A of type [C >: scala.caps.CapSet <: scala.caps.CapSet^]: Object^{C};
+  |  method foo of type [C >: scala.caps.CapSet <: scala.caps.CapSet^²]: Object^{C} has a parameter C with different @reserve status than the corresponding parameter in the overridden definition
+  |
+  |where:    ^  refers to a fresh root capability in the type of type C²
+  |          ^² refers to a fresh root capability in the type of type C³
   |
   | longer explanation available when compiling with `-explain`
 -- [E164] Declaration Error: tests/neg-custom-args/captures/unbox-overrides.scala:9:6 ----------------------------------
-9 |  def bar(@use x: C): C // error
+9 |  def bar[@reserve C^]: Object^{C} // error
   |      ^
-  |error overriding method bar in trait A of type (x: C): C;
-  |  method bar of type (@use x: C): C has a parameter x with different @use status than the corresponding parameter in the overridden definition
+  |error overriding method bar in trait A of type [C >: scala.caps.CapSet <: scala.caps.CapSet^]: Object^{C};
+  |  method bar of type [C >: scala.caps.CapSet <: scala.caps.CapSet^²]: Object^{C} has a parameter C with different @reserve status than the corresponding parameter in the overridden definition
+  |
+  |where:    ^  refers to a fresh root capability in the type of type C²
+  |          ^² refers to a fresh root capability in the type of type C³
   |
   | 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
+15 |abstract class C extends A, B2 // error
    |               ^
-   |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
+   |error overriding method foo in trait A of type [C >: scala.caps.CapSet <: scala.caps.CapSet^]: Object^{C};
+   |  method foo in trait B2 of type [C >: scala.caps.CapSet <: scala.caps.CapSet^²]: Object^{C} has a parameter C with different @reserve status than the corresponding parameter in the overridden definition
+   |
+   |where:    ^  refers to a fresh root capability in the type of type C²
+   |          ^² refers to a fresh root capability in the type of type C³
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/unbox-overrides.scala b/tests/neg-custom-args/captures/unbox-overrides.scala
index 6164ca274eaf..9d44d7da3afe 100644
--- a/tests/neg-custom-args/captures/unbox-overrides.scala
+++ b/tests/neg-custom-args/captures/unbox-overrides.scala
@@ -1,15 +1,15 @@
-import caps.use
+import caps.reserve
 
-trait A[X]:
-  def foo(@use x: X): X
-  def bar(x: X): X
+trait A:
+  def foo[@reserve C^]: Object^{C}
+  def bar[C^]: Object^{C}
 
-trait B extends A[C]:
-  def foo(x: C): C        // error
-  def bar(@use x: C): C // error
+trait B extends A:
+  def foo[C^]: Object^{C}  // error
+  def bar[@reserve C^]: Object^{C} // error
 
 trait B2:
-  def foo(x: C): C
-  def bar(@use x: C): C
+  def foo[C^]: Object^{C}
+  def bar[@reserve C^]: Object^{C}
 
-abstract class C extends A[C], B2 // error
+abstract class C extends A, B2 // error
diff --git a/tests/neg-custom-args/captures/use-alternatives.scala b/tests/neg-custom-args/captures/use-alternatives.scala
new file mode 100644
index 000000000000..7a6845e66e1a
--- /dev/null
+++ b/tests/neg-custom-args/captures/use-alternatives.scala
@@ -0,0 +1,25 @@
+import language.experimental.captureChecking
+import caps.{cap, use}
+
+def foo1(@use xs: List[() => Unit]): Unit = // error
+  var x: () ->{xs*} Unit = xs.head
+  var ys = xs
+  while ys.nonEmpty do
+    ys = ys.tail
+    x = ys.head
+
+def foo2(@use xs: List[() => Unit]): Unit = // error
+  def inner[@use C^](xs: List[() ->{C} Unit]): Unit = // error
+    var x: () ->{C} Unit = xs.head
+    var ys = xs
+    while ys.nonEmpty do
+      ys = ys.tail
+      x = ys.head
+  inner(xs)
+
+def foo3[@use C^](xs: List[() ->{C} Unit]): Unit = // error
+  var x: () ->{C} Unit = xs.head
+  var ys = xs
+  while ys.nonEmpty do
+    ys = ys.tail
+    x = ys.head
diff --git a/tests/neg-custom-args/captures/use-capset.check b/tests/neg-custom-args/captures/use-capset.check
index fc65636b1302..6fd8a3cfe325 100644
--- a/tests/neg-custom-args/captures/use-capset.check
+++ b/tests/neg-custom-args/captures/use-capset.check
@@ -1,19 +1,19 @@
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:11:22 -----------------------------------
-11 |  val _: () -> Unit = h // error: should be ->{io}
-   |                      ^
-   |                      Found:    (h : () ->{io} Unit)
-   |                      Required: () -> Unit
-   |
-   | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:13:50 -----------------------------------
-13 |  val _: () -> List[Object^{io}] -> Object^{io} = h2 // error, should be ->{io}
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:9:22 ------------------------------------
+9 |  val _: () -> Unit = h // error: should be ->{io}
+  |                      ^
+  |                      Found:    (h : () ->{io} Unit)
+  |                      Required: () -> Unit
+  |
+  | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:11:50 -----------------------------------
+11 |  val _: () -> List[Object^{io}] -> Object^{io} = h2 // error, should be ->{io}
    |                                                  ^^
    |                                                Found:    (h2 : () ->{} List[Object^{io}]^{} ->{io} Object^{io})
    |                                                Required: () -> List[Object^{io}] -> Object^{io}
    |
    | longer explanation available when compiling with `-explain`
 -- Error: tests/neg-custom-args/captures/use-capset.scala:5:49 ---------------------------------------------------------
-5 |private def g[C^] = (xs: List[Object^{C}]) => xs.head // error
+5 |private def g[C^] = (xs: List[Object^{C}]) => xs.head // error TODO: allow this
   |                                              ^^^^^^^
   |                                              Capture set parameter C leaks into capture scope of method g.
   |                                              To allow this, the type C should be declared with a @use annotation
diff --git a/tests/neg-custom-args/captures/use-capset.scala b/tests/neg-custom-args/captures/use-capset.scala
index 2d489a5061d8..49798ff31308 100644
--- a/tests/neg-custom-args/captures/use-capset.scala
+++ b/tests/neg-custom-args/captures/use-capset.scala
@@ -1,12 +1,10 @@
 import caps.{use, CapSet}
 
-def f[C^](@use xs: List[Object^{C}]): Unit = ???
+def f[C^](xs: List[Object^{C}]): Unit = ???
 
-private def g[C^] = (xs: List[Object^{C}]) => xs.head // error
+private def g[C^] = (xs: List[Object^{C}]) => xs.head // error TODO: allow this
 
-private def g2[@use C^] = (xs: List[Object^{C}]) => xs.head // ok
-
-def test(io: Object^)(@use xs: List[Object^{io}]): Unit =
+def test(io: Object^)(xs: List[Object^{io}]): Unit =
   val h = () => f(xs)
   val _: () -> Unit = h // error: should be ->{io}
   val h2 = () => g[{io}]
diff --git a/tests/new/test.scala b/tests/new/test.scala
index de3073216898..2904592cc6b2 100644
--- a/tests/new/test.scala
+++ b/tests/new/test.scala
@@ -1,3 +1 @@
-
-
-def foo[T: Singleton](x: T) = x
+def test[T] = println(T)
diff --git a/tests/pos-custom-args/captures/capset-problem.scala b/tests/pos-custom-args/captures/capset-problem.scala
new file mode 100644
index 000000000000..61dc9f6c9944
--- /dev/null
+++ b/tests/pos-custom-args/captures/capset-problem.scala
@@ -0,0 +1,17 @@
+import language.experimental.captureChecking
+import caps.use
+
+// Some capabilities that should be used locally
+trait Async
+
+case class Box[+T](get: T)
+
+def useBoxedAsync[C^](x: Box[Async^{C}]): Unit = ???
+def foo[C](x: Box[C]): Unit = ???
+
+def test(): Unit =
+
+  val t3 = useBoxedAsync(_)
+  val _: Box[Async^{}] -> Unit = t3
+  val t4 = foo(_)
+  val _: Box[Any] -> Unit = t4
\ No newline at end of file
diff --git a/tests/pos-custom-args/captures/capset-uses.scala b/tests/pos-custom-args/captures/capset-uses.scala
new file mode 100644
index 000000000000..1bfc3d2c7038
--- /dev/null
+++ b/tests/pos-custom-args/captures/capset-uses.scala
@@ -0,0 +1,11 @@
+import caps.use
+
+def foo[C^](x: List[() ->{C} Unit]): Unit =
+  println(x.head)
+
+def bar[C^](x: List[() ->{C} Unit]): Unit = ()
+
+def test(io: Object^) =
+  val xs: List[() ->{io} Unit] = ???
+  val f = () => foo[{io}](xs)
+  val g = () => bar[{io}](xs)
diff --git a/tests/pos-custom-args/captures/cc-poly-source-capability.scala b/tests/pos-custom-args/captures/cc-poly-source-capability.scala
index 7d06edd36415..9a30b49ef428 100644
--- a/tests/pos-custom-args/captures/cc-poly-source-capability.scala
+++ b/tests/pos-custom-args/captures/cc-poly-source-capability.scala
@@ -7,7 +7,7 @@ import caps.use
 
   class Async extends Sharable
 
-  def listener(async: Async): Listener^{async} = ???
+  def listener[C^](async: Async^{C}): Listener^{async} = ???
 
   class Listener
 
@@ -18,17 +18,16 @@ import caps.use
 
     def allListeners: Set[Listener^{X}] = listeners
 
-  def test1(async1: Async, @use others: List[Async]) =
-    val src = Source[{async1, others*}]
-    val _: Set[Listener^{async1, others*}] = src.allListeners
+  def test1[C^](async1: Async, others: List[Async^{C}]) =
+    val src = Source[{async1, C}]
+    val _: Set[Listener^{async1, C}] = src.allListeners
     val lst1 = listener(async1)
-    val lsts = others.map(listener)
-    val _: List[Listener^{others*}] = lsts
+    val lsts = others.map(listener[C])
+    val _: List[Listener^{C}] = lsts
     src.register{lst1}
     src.register(listener(async1))
     lsts.foreach(src.register(_)) // TODO: why we need to use _ explicitly here?
-    others.map(listener).foreach(src.register(_))
+    others.map(listener[C]).foreach(src.register(_)) // TODO: drop [C] and you get illegal capture reference: CapSet
     val ls = src.allListeners
-    val _: Set[Listener^{async1, others*}] = ls
-
+    val _: Set[Listener^{async1, C}] = ls
 
diff --git a/tests/pos-custom-args/captures/cc-use-iterable.scala b/tests/pos-custom-args/captures/cc-use-iterable.scala
index 84c497c0f6ce..610568847452 100644
--- a/tests/pos-custom-args/captures/cc-use-iterable.scala
+++ b/tests/pos-custom-args/captures/cc-use-iterable.scala
@@ -1,10 +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*}
+  def flatMap[U, C^](f: T => IterableOnce[U]^{C}): Iterable[U]^{this, C}
 
 
 class IterableOnceExtensionMethods[T](val it: IterableOnce[T]) extends AnyVal:
-  def flatMap[U](@caps.use f: T => IterableOnce[U]^): IterableOnce[U]^{f*} = it match
+  def flatMap[U, C^](f: T => IterableOnce[U]^{C}): IterableOnce[U]^{C} = it match
     case it: Iterable[T] => it.flatMap(f)
 
diff --git a/tests/pos-custom-args/captures/dep-reach.scala b/tests/pos-custom-args/captures/dep-reach.scala
index 1ee6fc3d17f9..8c06240657e0 100644
--- a/tests/pos-custom-args/captures/dep-reach.scala
+++ b/tests/pos-custom-args/captures/dep-reach.scala
@@ -1,10 +1,10 @@
 import caps.use
 object Test:
   class C
-  type Proc = () => Unit
+  type Proc[CS^] = () ->{CS} Unit
 
   def f(c: C^, d: C^): () ->{c, d} Unit =
-    def foo(@use xs: Proc*): () ->{xs*} Unit =
+    def foo[CS^](xs: Proc[CS]*): () ->{CS} Unit =
       xs.head
     val a: () ->{c} Unit = () => ()
     val b: () ->{d} Unit = () => ()
@@ -13,7 +13,7 @@ object Test:
 
   def g(c: C^, d: C^): () ->{c, d} Unit =
 
-    def foo(@use xs: Seq[() => Unit]): () ->{xs*} Unit =
+    def foo[CS^](xs: Seq[() ->{CS} Unit]): () ->{CS} Unit =
       xs.head
 
     val a: () ->{c} Unit = () => ()
diff --git a/tests/pos-custom-args/captures/gears-problem-poly.scala b/tests/pos-custom-args/captures/gears-problem-poly.scala
index 0b6fe3a9a0e9..df625b132215 100644
--- a/tests/pos-custom-args/captures/gears-problem-poly.scala
+++ b/tests/pos-custom-args/captures/gears-problem-poly.scala
@@ -17,13 +17,11 @@ class Result[+T, +E]:
 case class Err[+E](e: E) extends Result[Nothing, E]
 case class Ok[+T](x: T) extends Result[T, Nothing]
 
-extension [T, C^](@use fs: Seq[Future[T]^{C}])
+extension [T, C^](fs: Seq[Future[T]^{C}])
   def awaitAllPoly =
     val collector = Collector(fs)
     val fut: Future[T]^{C} = collector.results.read().get
-
-extension [T](@use fs: Seq[Future[T]^])
   def awaitAll = fs.awaitAllPoly
 
-def awaitExplicit[T](@use fs: Seq[Future[T]^]): Unit =
-  awaitAllPoly[T, {fs*}](fs)
+def awaitExplicit[T, C^](fs: Seq[Future[T]^{C}]): Unit =
+  awaitAllPoly[T, C](fs)
diff --git a/tests/pos-custom-args/captures/i15749.scala b/tests/pos-custom-args/captures/i15749.scala
index dd92aced77a5..8b4c77602439 100644
--- a/tests/pos-custom-args/captures/i15749.scala
+++ b/tests/pos-custom-args/captures/i15749.scala
@@ -1,16 +1,20 @@
 import caps.use
-class Unit
-object unit extends Unit
+class U
+object u extends U
 
 type Top = Any^
 
-type LazyVal[T] = Unit => T
+type LazyVal[T, C^] = U ->{C} T
 
 class Foo[T](val x: T)
 
-// Foo[□ Unit => T]
-type BoxedLazyVal[T] = Foo[LazyVal[T]]
-
-def force[A](@use v: BoxedLazyVal[A]): A =
-  // Γ ⊢ v.x : □ {cap} Unit -> A
-  v.x(unit)  // should be error: (unbox v.x)(unit), where (unbox v.x) should be untypable, now ok
\ No newline at end of file
+// Foo[□ U => T]
+type BoxedLazyVal[T, C^] = Foo[LazyVal[T, C]]
+/*
+def force[A, C^](v: BoxedLazyVal[A, C]): A =
+  // Γ ⊢ v.x : □ {cap} U -> A
+  v.x(u)  // should be error: (unbox v.x)(u), where (unbox v.x) should be untypable, now ok
+*/
+def force[A, C^](v: Foo[U ->{C} A]): A =
+  // Γ ⊢ v.x : □ {cap} U -> A
+  v.x(u)  // should be error: (unbox v.x)(u), where (unbox v.x) should be untypable, now ok
\ No newline at end of file
diff --git a/tests/pos-custom-args/captures/i15749a.scala b/tests/pos-custom-args/captures/i15749a.scala
index c008d20a155c..19e919798fd9 100644
--- a/tests/pos-custom-args/captures/i15749a.scala
+++ b/tests/pos-custom-args/captures/i15749a.scala
@@ -14,10 +14,10 @@ def test =
   def wrapper[T](x: T): Wrapper[T] = Wrapper:
     [X] => (op: T ->{cap} X) => op(x)
 
-  def strictMap[A <: Top,  B <: Top](mx: Wrapper[A])(f: A ->{cap, mx*} B): Wrapper[B] =
+  def strictMap[A <: Top, B <: Top, C^](mx: Wrapper[A])(f: A ->{cap, C} B): Wrapper[B] =
     mx.value((x: A) => wrapper(f(x)))
 
   def force[A](thunk: Unit ->{cap} A): A = thunk(u)
 
-  def forceWrapper[A](@use mx: Wrapper[Unit ->{cap} A]): Wrapper[A] =
-    strictMap[Unit ->{mx*} A, A](mx)(t => force[A](t)) // was error when Wrapper was an alias type
+  def forceWrapper[A, C^](mx: Wrapper[Unit ->{C} A]): Wrapper[A] =
+    strictMap[Unit ->{C} A, A, C](mx)(t => force[A](t)) // was error when Wrapper was an alias type
diff --git a/tests/pos-custom-args/captures/i18699.scala b/tests/pos-custom-args/captures/i18699.scala
index 5a0a9357f774..91a27c7474c0 100644
--- a/tests/pos-custom-args/captures/i18699.scala
+++ b/tests/pos-custom-args/captures/i18699.scala
@@ -4,6 +4,6 @@ import caps.use
 trait Cap:
   def use: Int = 42
 
-def test2(@use cs: List[Cap^]): Unit =
-  val t0: Cap^{cs*} = cs.head  // error
-  var t1: Cap^{cs*} = cs.head  // error
+def test2[C^](cs: List[Cap^{C}]): Unit =
+  val t0: Cap^{C} = cs.head
+  var t1: Cap^{C} = cs.head
diff --git a/tests/pos-custom-args/captures/reach-capability.scala b/tests/pos-custom-args/captures/reach-capability.scala
index 77bd91957fa0..681997a6d20e 100644
--- a/tests/pos-custom-args/captures/reach-capability.scala
+++ b/tests/pos-custom-args/captures/reach-capability.scala
@@ -12,7 +12,7 @@ import caps.use
 
   class Listener
 
-  def test2(@use lbls: List[Label]) =
-    def makeListener(lbl: Label): Listener^{lbl} = ???
+  def test2[C^](lbls: List[Label^{C}]) =
+    def makeListener(lbl: Label^{C}): Listener^{lbl} = ???
     val listeners = lbls.map(makeListener) // should work
 
diff --git a/tests/pos-custom-args/captures/reach-problem.scala b/tests/pos-custom-args/captures/reach-problem.scala
index f36a4af14ad2..7027899f7f06 100644
--- a/tests/pos-custom-args/captures/reach-problem.scala
+++ b/tests/pos-custom-args/captures/reach-problem.scala
@@ -5,7 +5,7 @@ class Box[T](items: Seq[T^]):
   def getOne: T^{items*} = ???
 
 object Box:
-  def getOne[T](@use items: Seq[T^]): T^{items*} =
+  def getOne[T, C^](items: Seq[T^{C}]): T^{items*} =
     val bx = Box(items)
     bx.getOne
 /*
diff --git a/tests/pos-custom-args/captures/reaches.scala b/tests/pos-custom-args/captures/reaches.scala
index 131dce862b02..cf9751a3211e 100644
--- a/tests/pos-custom-args/captures/reaches.scala
+++ b/tests/pos-custom-args/captures/reaches.scala
@@ -23,12 +23,12 @@ extension [A](x: A) def :: (xs: List[A]): List[A] = ???
 
 object Nil extends List[Nothing]
 
-def runAll(@use xs: List[Proc]): Unit =
-  var cur: List[() ->{xs*} Unit] = xs  // OK, by revised VAR
+def runAll[C^](xs: List[() ->{C} Unit]): Unit =
+  var cur: List[() ->{C} Unit] = xs  // OK, by revised VAR
   while cur.nonEmpty do
-    val next: () ->{xs*} Unit = cur.head
+    val next: () ->{C} Unit = cur.head
     next()
-    cur = cur.tail: List[() ->{xs*} Unit]
+    cur = cur.tail: List[() ->{C} Unit]
 
 def id1(x: Proc): () ->{x} Unit = x
 def id2(xs: List[Proc]): List[() ->{xs*} Unit] = xs
diff --git a/tests/pos-custom-args/captures/sep-pairs.scala b/tests/pos-custom-args/captures/sep-pairs.scala
index 494996c12161..86d16dea82b1 100644
--- a/tests/pos-custom-args/captures/sep-pairs.scala
+++ b/tests/pos-custom-args/captures/sep-pairs.scala
@@ -14,8 +14,21 @@ def mkPair: Pair[Ref^, Ref^] =
   val p_exact: Pair[Ref^{r1}, Ref^{r2}] = Pair(r1, r2)
   p_exact
 
-def copyPair(@consume @use p: Pair[Ref^, Ref^]): Pair[Ref^, Ref^] =
-  val x: Ref^{p.fst*} = p.fst
-  val y: Ref^{p.snd*} = p.snd
+def copyPair[C^, D^](@consume p: Pair[Ref^{C}, Ref^{D}]): Pair[Ref^{C}, Ref^{D}] =
+  val x: Ref^{C} = p.fst
+  val y: Ref^{D} = p.snd
+  Pair[Ref^{C}, Ref^{D}](x, y)
+
+/* TODO: The following variants don't work
+
+def copyPair[C^, D^](@consume p: Pair[Ref^{C}, Ref^{D}]): Pair[Ref^{C}, Ref^{D}] =
+  val x: Ref^{C} = p.fst
+  val y: Ref^{D} = p.snd
+  Pair(x, y)
+
+def copyPair[C^, D^](@consume p: Pair[Ref^{C}, Ref^{D}]): Pair[Ref^, Ref^] =
+  val x: Ref^{C} = p.fst
+  val y: Ref^{D} = p.snd
   Pair(x, y)
 
+*/
\ No newline at end of file
diff --git a/tests/pos-custom-args/captures/use-alternatives.scala b/tests/pos-custom-args/captures/use-alternatives.scala
index b4fd896210d4..73a3fb725035 100644
--- a/tests/pos-custom-args/captures/use-alternatives.scala
+++ b/tests/pos-custom-args/captures/use-alternatives.scala
@@ -1,23 +1,7 @@
 import language.experimental.captureChecking
 import caps.{cap, use}
 
-def foo1(@use xs: List[() => Unit]): Unit =
-  var x: () ->{xs*} Unit = xs.head
-  var ys = xs
-  while ys.nonEmpty do
-    ys = ys.tail
-    x = ys.head
-
-def foo2(@use xs: List[() => Unit]): Unit =
-  def inner[@use C^](xs: List[() ->{C} Unit]): Unit =
-    var x: () ->{C} Unit = xs.head
-    var ys = xs
-    while ys.nonEmpty do
-      ys = ys.tail
-      x = ys.head
-  inner(xs)
-
-def foo3[@use C^](xs: List[() ->{C} Unit]): Unit =
+def foo[C^](xs: List[() ->{C} Unit]): Unit =
   var x: () ->{C} Unit = xs.head
   var ys = xs
   while ys.nonEmpty do
diff --git a/tests/run-tasty-inspector/stdlibExperimentalDefinitions.scala b/tests/run-tasty-inspector/stdlibExperimentalDefinitions.scala
index f95c25635d9f..814cc35648b3 100644
--- a/tests/run-tasty-inspector/stdlibExperimentalDefinitions.scala
+++ b/tests/run-tasty-inspector/stdlibExperimentalDefinitions.scala
@@ -49,6 +49,7 @@ val experimentalDefinitionInLibrary = Set(
   "scala.caps.unsafe",
   "scala.caps.unsafe$",
   "scala.caps.use",
+  "scala.caps.reserve",
 
   //// New feature: into
   "scala.Conversion$.into",

From 3e7d84a66af919f84a170b988aabcf9a2f4c38cc Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Wed, 23 Jul 2025 12:59:26 +0200
Subject: [PATCH 4/6] Prevent leaking FreshCaps created for parameters

---
 .../src/dotty/tools/dotc/cc/Capability.scala  |  9 +++++++--
 .../src/dotty/tools/dotc/cc/CaptureSet.scala  |  2 +-
 .../dotty/tools/dotc/cc/CheckCaptures.scala   | 20 ++++++++++++-------
 compiler/src/dotty/tools/dotc/cc/Setup.scala  | 11 +++++-----
 .../captures/leak-problem-unboxed.scala       | 20 ++++++++++++-------
 5 files changed, 40 insertions(+), 22 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala
index c3c743a7c8f5..618025d42b1c 100644
--- a/compiler/src/dotty/tools/dotc/cc/Capability.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala
@@ -152,6 +152,8 @@ object Capabilities:
     val hiddenSet = CaptureSet.HiddenSet(owner, this: @unchecked)
       // fails initialization check without the @unchecked
 
+    //assert(rootId != 6, origin)
+
     override def equals(that: Any) = that match
       case that: FreshCap => this eq that
       case _ => false
@@ -808,6 +810,7 @@ object Capabilities:
     case LambdaActual(restp: Type)
     case OverriddenType(member: Symbol)
     case DeepCS(ref: TypeRef)
+    case Parameter(param: Symbol)
     case Unknown
 
     def explanation(using Context): String = this match
@@ -841,6 +844,8 @@ object Capabilities:
         i" when instantiating upper bound of member overridden by $member"
       case DeepCS(ref: TypeRef) =>
         i" when computing deep capture set of $ref"
+      case Parameter(param) =>
+        i" of parameter $param of ${param.owner}"
       case Unknown =>
         ""
   end Origin
@@ -907,8 +912,8 @@ object Capabilities:
       CapToFresh(origin)(tp)
 
   /** Maps fresh to cap */
-  def freshToCap(tp: Type)(using Context): Type =
-    CapToFresh(Origin.Unknown).inverse(tp)
+  def freshToCap(param: Symbol, tp: Type)(using Context): Type =
+    CapToFresh(Origin.Parameter(param)).inverse(tp)
 
   /** Map top-level free existential variables one-to-one to Fresh instances */
   def resultToFresh(tp: Type, origin: Origin)(using Context): Type =
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index 147924dc95ba..2a56400d1eeb 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -698,7 +698,7 @@ object CaptureSet:
     private def narrowClassifier(cls: ClassSymbol)(using Context): Unit =
       val newClassifier = leastClassifier(classifier, cls)
       if newClassifier == defn.NothingClass then
-        println(i"conflicting classifications for $this, was $classifier, now $cls")
+        capt.println(i"conflicting classifications for $this, was $classifier, now $cls")
       myClassifier = newClassifier
 
     override def adoptClassifier(cls: ClassSymbol)(using Context): Unit =
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index b417e017f8c7..755d8a6d3f9b 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -68,8 +68,7 @@ object CheckCaptures:
         cur = cur.outer
         res
 
-    def ownerString(using Context): String =
-      if owner.isAnonymousFunction then "enclosing function" else owner.show
+    def ownerString(using Context): String = ownerStr(owner)
   end Env
 
   /** Similar normal substParams, but this is an approximating type map that
@@ -184,6 +183,9 @@ object CheckCaptures:
     check.traverse(tp)
   end disallowBadRootsIn
 
+  private def ownerStr(owner: Symbol)(using Context): String =
+    if owner.isAnonymousFunction then "enclosing function" else owner.show
+
   trait CheckerAPI:
     /** Complete symbol info of a val or a def */
     def completeDef(tree: ValOrDefDef, sym: Symbol, completer: LazyType)(using Context): Type
@@ -548,10 +550,8 @@ class CheckCaptures extends Recheck, SymTransformer:
       c.paramPathRoot match
         case ref: NamedType if !ref.symbol.isUseParam =>
           val what = if ref.isType then "Capture set parameter" else "Local reach capability"
-          val owner = ref.symbol.owner
-          val ownerStr = if owner.isAnonymousFunction then "enclosing function" else owner.show
           report.error(
-            em"""$what $c leaks into capture scope of $ownerStr.
+            em"""$what $c leaks into capture scope of ${ownerStr(ref.symbol.owner)}.
                 |To allow this, the ${ref.symbol} should be declared with a @use annotation""", pos)
         case _ =>
 
@@ -925,7 +925,7 @@ class CheckCaptures extends Recheck, SymTransformer:
             assert(params.hasSameLengthAs(argTypes), i"$mdef vs $pt, ${params}")
             for (argType, param) <- argTypes.lazyZip(params) do
               val paramTpt = param.asInstanceOf[ValDef].tpt
-              val paramType = freshToCap(paramTpt.nuType)
+              val paramType = freshToCap(param.symbol, paramTpt.nuType)
               checkConformsExpr(argType, paramType, param)
                 .showing(i"compared expected closure formal $argType against $param with ${paramTpt.nuType}", capt)
             if ccConfig.preTypeClosureResults && !(isEtaExpansion(mdef) && ccConfig.handleEtaExpansionsSpecially) then
@@ -2030,7 +2030,13 @@ class CheckCaptures extends Recheck, SymTransformer:
               case c: DerivedCapability =>
                 checkElem(c.underlying)
               case c: FreshCap =>
-                check(c.hiddenSet)
+                c.origin match
+                  case Origin.Parameter(param) =>
+                    report.error(
+                      em"Local $c created in type of $param leaks into capture scope of ${ownerStr(param.owner)}",
+                      tree.srcPos)
+                  case _ =>
+                    check(c.hiddenSet)
               case _ =>
 
         check(uses)
diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala
index d043f81ba7dd..00791b9083af 100644
--- a/compiler/src/dotty/tools/dotc/cc/Setup.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -646,17 +646,18 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
         def ownerChanges =
           ctx.owner.name.is(TryOwnerName)
 
-        def paramsToCap(mt: Type)(using Context): Type = mt match
+        def paramsToCap(psymss: List[List[Symbol]], mt: Type)(using Context): Type = mt match
           case mt: MethodType =>
             try
               mt.derivedLambdaType(
-                paramInfos = mt.paramInfos.map(freshToCap),
-                resType = paramsToCap(mt.resType))
+                paramInfos =
+                  psymss.head.lazyZip(mt.paramInfos).map(freshToCap),
+                resType = paramsToCap(psymss.tail, mt.resType))
             catch case ex: AssertionError =>
               println(i"error while mapping params ${mt.paramInfos} of $sym")
               throw ex
           case mt: PolyType =>
-            mt.derivedLambdaType(resType = paramsToCap(mt.resType))
+            mt.derivedLambdaType(resType = paramsToCap(psymss.tail, mt.resType))
           case _ => mt
 
         // If there's a change in the signature or owner, update the info of `sym`
@@ -668,7 +669,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
                 toResultInResults(sym, report.error(_, tree.srcPos)):
                   if sym.is(Method) then
                     inContext(ctx.withOwner(sym)):
-                      paramsToCap(methodType(paramSymss, localReturnType))
+                      paramsToCap(paramSymss, methodType(paramSymss, localReturnType))
                   else tree.tpt.nuType
               if tree.tpt.isInstanceOf[InferredTypeTree]
                   && !sym.is(Param) && !sym.is(ParamAccessor)
diff --git a/tests/neg-custom-args/captures/leak-problem-unboxed.scala b/tests/neg-custom-args/captures/leak-problem-unboxed.scala
index 00d953b1ce09..b00a226937a2 100644
--- a/tests/neg-custom-args/captures/leak-problem-unboxed.scala
+++ b/tests/neg-custom-args/captures/leak-problem-unboxed.scala
@@ -1,5 +1,4 @@
 import language.experimental.captureChecking
-import caps.use
 
 // Some capabilities that should be used locally
 trait Async:
@@ -19,16 +18,23 @@ def useBoxedAsync1[C^](x: Box[Async^{C}]): Unit = x.get.read() // ok
 def test(): Unit =
 
   val f: Box[Async^] => Unit = (x: Box[Async^]) => useBoxedAsync(x) // error
-  val t0: Box[Async^] => Unit = x => useBoxedAsync(x) // TODO hould be error!
+  val f0: Box[Async^] => Unit = x => useBoxedAsync(x) // // error
 
-  val t1: Box[Async^] => Unit = useBoxedAsync(_) // TODO should be error!
-  val t2: Box[Async^] => Unit = useBoxedAsync // TODO should be error!
-  val t3 = useBoxedAsync(_) // was error, now ok
-  val t4 = useBoxedAsync // was error, now ok
+  val f1: Box[Async^] => Unit = useBoxedAsync(_) // error
+  val f2: Box[Async^] => Unit = useBoxedAsync // error
+  val f3 = useBoxedAsync(_) // was error, now ok, but bang below fails
+  val f4 = useBoxedAsync // was error, now ok, but bang2 below fails
 
   def boom(x: Async^): () ->{f} Unit =
     () => f(Box(x))
 
   val leaked = usingAsync[() ->{f} Unit](boom)
 
-  leaked()  // scope violation
+  leaked()  // was scope violation
+
+  def bang(x: Async^) =
+    () => f3(Box(x)) // error
+
+  def bang2(x: Async^) =
+    () => f3(Box(x)) // error
+

From 3c69f599210f4f08e2d61cae74e602bf9d2ebb3c Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Wed, 23 Jul 2025 13:11:04 +0200
Subject: [PATCH 5/6] Drop some TODOs in tests, explain others

---
 .../neg-custom-args/captures/use-capset.check  | 18 +++++++++---------
 .../neg-custom-args/captures/use-capset.scala  |  2 ++
 .../captures/cc-poly-source-capability.scala   |  2 +-
 tests/pos-custom-args/captures/sep-pairs.scala |  4 ++--
 4 files changed, 14 insertions(+), 12 deletions(-)

diff --git a/tests/neg-custom-args/captures/use-capset.check b/tests/neg-custom-args/captures/use-capset.check
index 6fd8a3cfe325..0aecd0f203ed 100644
--- a/tests/neg-custom-args/captures/use-capset.check
+++ b/tests/neg-custom-args/captures/use-capset.check
@@ -1,12 +1,12 @@
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:9:22 ------------------------------------
-9 |  val _: () -> Unit = h // error: should be ->{io}
-  |                      ^
-  |                      Found:    (h : () ->{io} Unit)
-  |                      Required: () -> Unit
-  |
-  | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:11:50 -----------------------------------
-11 |  val _: () -> List[Object^{io}] -> Object^{io} = h2 // error, should be ->{io}
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:11:22 -----------------------------------
+11 |  val _: () -> Unit = h // error: should be ->{io}
+   |                      ^
+   |                      Found:    (h : () ->{io} Unit)
+   |                      Required: () -> Unit
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:13:50 -----------------------------------
+13 |  val _: () -> List[Object^{io}] -> Object^{io} = h2 // error, should be ->{io}
    |                                                  ^^
    |                                                Found:    (h2 : () ->{} List[Object^{io}]^{} ->{io} Object^{io})
    |                                                Required: () -> List[Object^{io}] -> Object^{io}
diff --git a/tests/neg-custom-args/captures/use-capset.scala b/tests/neg-custom-args/captures/use-capset.scala
index 49798ff31308..c478a88b3086 100644
--- a/tests/neg-custom-args/captures/use-capset.scala
+++ b/tests/neg-custom-args/captures/use-capset.scala
@@ -3,6 +3,8 @@ import caps.{use, CapSet}
 def f[C^](xs: List[Object^{C}]): Unit = ???
 
 private def g[C^] = (xs: List[Object^{C}]) => xs.head // error TODO: allow this
+  // This fails currently since `C^` is not classified as used. To classify it we'd also have to look on the
+  // RHS. But this would change again if we go to non-monotonic currying.
 
 def test(io: Object^)(xs: List[Object^{io}]): Unit =
   val h = () => f(xs)
diff --git a/tests/pos-custom-args/captures/cc-poly-source-capability.scala b/tests/pos-custom-args/captures/cc-poly-source-capability.scala
index 9a30b49ef428..248693c2f7ae 100644
--- a/tests/pos-custom-args/captures/cc-poly-source-capability.scala
+++ b/tests/pos-custom-args/captures/cc-poly-source-capability.scala
@@ -27,7 +27,7 @@ import caps.use
     src.register{lst1}
     src.register(listener(async1))
     lsts.foreach(src.register(_)) // TODO: why we need to use _ explicitly here?
-    others.map(listener[C]).foreach(src.register(_)) // TODO: drop [C] and you get illegal capture reference: CapSet
+    others.map(listener[C]).foreach(src.register(_))
     val ls = src.allListeners
     val _: Set[Listener^{async1, C}] = ls
 
diff --git a/tests/pos-custom-args/captures/sep-pairs.scala b/tests/pos-custom-args/captures/sep-pairs.scala
index 86d16dea82b1..17cb8eb9aa6c 100644
--- a/tests/pos-custom-args/captures/sep-pairs.scala
+++ b/tests/pos-custom-args/captures/sep-pairs.scala
@@ -21,12 +21,12 @@ def copyPair[C^, D^](@consume p: Pair[Ref^{C}, Ref^{D}]): Pair[Ref^{C}, Ref^{D}]
 
 /* TODO: The following variants don't work
 
-def copyPair[C^, D^](@consume p: Pair[Ref^{C}, Ref^{D}]): Pair[Ref^{C}, Ref^{D}] =
+def copyPair1[C^, D^](@consume p: Pair[Ref^{C}, Ref^{D}]): Pair[Ref^{C}, Ref^{D}] =
   val x: Ref^{C} = p.fst
   val y: Ref^{D} = p.snd
   Pair(x, y)
 
-def copyPair[C^, D^](@consume p: Pair[Ref^{C}, Ref^{D}]): Pair[Ref^, Ref^] =
+def copyPair2[C^, D^](@consume p: Pair[Ref^{C}, Ref^{D}]): Pair[Ref^, Ref^] =
   val x: Ref^{C} = p.fst
   val y: Ref^{D} = p.snd
   Pair(x, y)

From e3dd109a73291a479042501366d3f1be14d0964d Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Wed, 23 Jul 2025 15:24:59 +0200
Subject: [PATCH 6/6] Fix error message for leaks

---
 .../src/dotty/tools/dotc/cc/CheckCaptures.scala    | 14 ++++++++++----
 .../dotty/tools/dotc/printing/PlainPrinter.scala   |  3 ++-
 tests/neg-custom-args/captures/delayedRunops.check |  2 +-
 tests/neg-custom-args/captures/i21347.check        |  2 +-
 tests/neg-custom-args/captures/i21442.check        |  4 ++--
 tests/neg-custom-args/captures/i23303.check        |  6 +++---
 tests/neg-custom-args/captures/localReaches.check  |  4 ++--
 tests/neg-custom-args/captures/reaches.check       |  2 +-
 .../neg-custom-args/captures/unsound-reach-6.check |  4 ++--
 tests/neg-custom-args/captures/use-capset.check    |  1 -
 tests/neg/localReaches.check                       |  4 ++--
 11 files changed, 26 insertions(+), 20 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 755d8a6d3f9b..86d361628953 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -544,15 +544,21 @@ class CheckCaptures extends Recheck, SymTransformer:
         useInfos += ((tree, cs, curEnv))
     end markFree
 
-    /** If capability `c` refers to a parameter that is not @use declared, report an error.
+    /** If capability `c` refers to a parameter that is not implicitly or explicitly
+     *  @use declared, report an error.
      */
     def checkUseDeclared(c: Capability, pos: SrcPos)(using Context): Unit =
       c.paramPathRoot match
         case ref: NamedType if !ref.symbol.isUseParam =>
           val what = if ref.isType then "Capture set parameter" else "Local reach capability"
+          def mitigation =
+            if ccConfig.allowUse
+            then i"\nTo allow this, the ${ref.symbol} should be declared with a @use annotation."
+            else if !ref.isType then i"\nYou could try to abstract the capabilities referred to by $c in a capset variable."
+            else ""
           report.error(
-            em"""$what $c leaks into capture scope of ${ownerStr(ref.symbol.owner)}.
-                |To allow this, the ${ref.symbol} should be declared with a @use annotation""", pos)
+            em"$what $c leaks into capture scope of ${ownerStr(ref.symbol.owner)}.$mitigation",
+            pos)
         case _ =>
 
     /** Include references captured by the called method in the current environment stack */
@@ -1785,7 +1791,7 @@ class CheckCaptures extends Recheck, SymTransformer:
 
         override def checkInheritedTraitParameters: Boolean = false
 
-        /** Check that overrides don't change the @use or @consume status of their parameters */
+        /** Check that overrides don't change the @use, @consume, or @reserve status of their parameters */
         override def additionalChecks(member: Symbol, other: Symbol)(using Context): Unit =
           for
             (params1, params2) <- member.rawParamss.lazyZip(other.rawParamss)
diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
index 877a2ba309da..70e31a03b13f 100644
--- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
@@ -379,7 +379,8 @@ class PlainPrinter(_ctx: Context) extends Printer {
     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`. */
+   * to parameter types. Examples are `@use` and `@consume`.
+   */
   protected def specialAnnotText(sym: ClassSymbol, tp: Type): Text =
     Str(s"@${sym.name} ").provided(tp.hasAnnotation(sym))
 
diff --git a/tests/neg-custom-args/captures/delayedRunops.check b/tests/neg-custom-args/captures/delayedRunops.check
index b565acb66427..04f874665c5b 100644
--- a/tests/neg-custom-args/captures/delayedRunops.check
+++ b/tests/neg-custom-args/captures/delayedRunops.check
@@ -20,7 +20,7 @@
 22 |      runOps(ops1)  // error
    |      ^^^^^^
    |      Local reach capability ops* leaks into capture scope of method delayedRunOps2.
-   |      To allow this, the parameter ops should be declared with a @use annotation
+   |      You could try to abstract the capabilities referred to by ops* in a capset variable.
 -- Error: tests/neg-custom-args/captures/delayedRunops.scala:21:16 -----------------------------------------------------
 21 |      val ops1: List[() => Unit] = ops // error
    |                ^^^^^^^^^^^^^^^^
diff --git a/tests/neg-custom-args/captures/i21347.check b/tests/neg-custom-args/captures/i21347.check
index 6985c58afd18..87595b29b184 100644
--- a/tests/neg-custom-args/captures/i21347.check
+++ b/tests/neg-custom-args/captures/i21347.check
@@ -9,5 +9,5 @@
 11 |  ops.foreach: op => // error
    |               ^
    |               Local reach capability ops* leaks into capture scope of method runOpsAlt.
-   |               To allow this, the parameter ops should be declared with a @use annotation
+   |               You could try to abstract the capabilities referred to by ops* in a capset variable.
 12 |    op()
diff --git a/tests/neg-custom-args/captures/i21442.check b/tests/neg-custom-args/captures/i21442.check
index 330c88d393dd..aa0a8e53ff7f 100644
--- a/tests/neg-custom-args/captures/i21442.check
+++ b/tests/neg-custom-args/captures/i21442.check
@@ -2,12 +2,12 @@
 10 |  val io = x.unbox // error: local reach capability {x*} leaks
    |           ^^^^^^^
    |           Local reach capability x.unbox* leaks into capture scope of method foo.
-   |           To allow this, the parameter x should be declared with a @use annotation
+   |           You could try to abstract the capabilities referred to by x.unbox* in a capset variable.
 -- Error: tests/neg-custom-args/captures/i21442.scala:18:14 ------------------------------------------------------------
 18 |  val io = x1.unbox // error
    |           ^^^^^^^^
    |           Local reach capability x* leaks into capture scope of method bar.
-   |           To allow this, the parameter x should be declared with a @use annotation
+   |           You could try to abstract the capabilities referred to by x* in a capset variable.
 -- Error: tests/neg-custom-args/captures/i21442.scala:17:10 ------------------------------------------------------------
 17 |  val x1: Boxed[IO^] = x // error
    |          ^^^^^^^^^^
diff --git a/tests/neg-custom-args/captures/i23303.check b/tests/neg-custom-args/captures/i23303.check
index 437cd471a42c..c3c3e272e218 100644
--- a/tests/neg-custom-args/captures/i23303.check
+++ b/tests/neg-custom-args/captures/i23303.check
@@ -1,10 +1,10 @@
 -- Error: tests/neg-custom-args/captures/i23303.scala:6:36 -------------------------------------------------------------
 6 |    def execute: Unit = ops.foreach(f => f()) // error
   |                                    ^^^^^^^^
-  |                                 Local reach capability Runner.this.ops* leaks into capture scope of class Runner.
-  |                                 To allow this, the value ops should be declared with a @use annotation
+  |                  Local reach capability Runner.this.ops* leaks into capture scope of class Runner.
+  |                  You could try to abstract the capabilities referred to by Runner.this.ops* in a capset variable.
 -- Error: tests/neg-custom-args/captures/i23303.scala:9:22 -------------------------------------------------------------
 9 |    () => ops.foreach(f => f()) // error
   |                      ^^^^^^^^
   |                      Local reach capability ops* leaks into capture scope of method Runner2.
-  |                      To allow this, the parameter ops should be declared with a @use annotation
+  |                      You could try to abstract the capabilities referred to by ops* in a capset variable.
diff --git a/tests/neg-custom-args/captures/localReaches.check b/tests/neg-custom-args/captures/localReaches.check
index 886fbbf7c3e9..1df4886e61d5 100644
--- a/tests/neg-custom-args/captures/localReaches.check
+++ b/tests/neg-custom-args/captures/localReaches.check
@@ -2,12 +2,12 @@
 24 |  var x: () ->{xs*} Unit = ys.head // error
    |                           ^^^^^^^
    |                           Local reach capability ops* leaks into capture scope of method localReach3.
-   |                           To allow this, the parameter ops should be declared with a @use annotation
+   |                           You could try to abstract the capabilities referred to by ops* in a capset variable.
 -- Error: tests/neg-custom-args/captures/localReaches.scala:27:11 ------------------------------------------------------
 27 |    x = ys.head  // error
    |        ^^^^^^^
    |        Local reach capability ops* leaks into capture scope of method localReach3.
-   |        To allow this, the parameter ops should be declared with a @use annotation
+   |        You could try to abstract the capabilities referred to by ops* in a capset variable.
 -- Error: tests/neg-custom-args/captures/localReaches.scala:14:10 ------------------------------------------------------
 14 |  val xs: List[() => Unit] = op :: Nil // error
    |          ^^^^^^^^^^^^^^^^
diff --git a/tests/neg-custom-args/captures/reaches.check b/tests/neg-custom-args/captures/reaches.check
index 64b3a3c9a736..e6c0c68d5dad 100644
--- a/tests/neg-custom-args/captures/reaches.check
+++ b/tests/neg-custom-args/captures/reaches.check
@@ -114,4 +114,4 @@
 39 |    val next: () => Unit = cur.head   // error
    |                           ^^^^^^^^
    |                           Local reach capability xs* leaks into capture scope of method runAll2.
-   |                           To allow this, the parameter xs should be declared with a @use annotation
+   |                           You could try to abstract the capabilities referred to by xs* in a capset variable.
diff --git a/tests/neg-custom-args/captures/unsound-reach-6.check b/tests/neg-custom-args/captures/unsound-reach-6.check
index 8308e2336d7c..8691cfd0d5e5 100644
--- a/tests/neg-custom-args/captures/unsound-reach-6.check
+++ b/tests/neg-custom-args/captures/unsound-reach-6.check
@@ -16,12 +16,12 @@
 7 |  println(xs.head) // error
   |          ^^^^^^^
   |          Local reach capability xs* leaks into capture scope of method f.
-  |          To allow this, the parameter xs should be declared with a @use annotation
+  |          You could try to abstract the capabilities referred to by xs* in a capset variable.
 -- Error: tests/neg-custom-args/captures/unsound-reach-6.scala:11:14 ---------------------------------------------------
 11 |    val z = f(ys)   // error @consume failure
    |              ^^
    |              Local reach capability ys* leaks into capture scope of method test.
-   |              To allow this, the parameter ys should be declared with a @use annotation
+   |              You could try to abstract the capabilities referred to by ys* in a capset variable.
 -- Error: tests/neg-custom-args/captures/unsound-reach-6.scala:19:14 ---------------------------------------------------
 19 |    val z = f(ys)  // error @consume failure
    |              ^^
diff --git a/tests/neg-custom-args/captures/use-capset.check b/tests/neg-custom-args/captures/use-capset.check
index 0aecd0f203ed..317abf53dabe 100644
--- a/tests/neg-custom-args/captures/use-capset.check
+++ b/tests/neg-custom-args/captures/use-capset.check
@@ -16,4 +16,3 @@
 5 |private def g[C^] = (xs: List[Object^{C}]) => xs.head // error TODO: allow this
   |                                              ^^^^^^^
   |                                              Capture set parameter C leaks into capture scope of method g.
-  |                                              To allow this, the type C should be declared with a @use annotation
diff --git a/tests/neg/localReaches.check b/tests/neg/localReaches.check
index 18510e3a3616..71a3057fa74b 100644
--- a/tests/neg/localReaches.check
+++ b/tests/neg/localReaches.check
@@ -2,9 +2,9 @@
 24 |  var x: () ->{xs*} Unit = ys.head // error
    |                           ^^^^^^^
    |                           Local reach capability ops* leaks into capture scope of method localReach3.
-   |                           To allow this, the parameter ops should be declared with a @use annotation
+   |                           To allow this, the parameter ops should be declared with a @use annotation.
 -- Error: tests/neg/localReaches.scala:27:11 ---------------------------------------------------------------------------
 27 |    x = ys.head  // error
    |        ^^^^^^^
    |        Local reach capability ops* leaks into capture scope of method localReach3.
-   |        To allow this, the parameter ops should be declared with a @use annotation
+   |        To allow this, the parameter ops should be declared with a @use annotation.