diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
index aad6ca8ddeac..6543d316f03e 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
@@ -221,19 +221,22 @@ extension (tp: Type)
     case tp: SingletonCaptureRef => tp.captureSetOfInfo
     case _ => CaptureSet.ofType(tp, followResult = false)
 
-  /** The deep capture set of a type.
-   *  For singleton capabilities `x` and reach capabilities `x*`, this is `{x*}`, provided
-   *  the underlying capture set resulting from traversing the type is non-empty.
-   *  For other types this is the union of all covariant capture sets embedded
-   *  in the type, as computed by `CaptureSet.ofTypeDeeply`.
+  /** The deep capture set of a type. This is by default the union of all
+   *  covariant capture sets embedded in the widened type, as computed by
+   *  `CaptureSet.ofTypeDeeply`. If that set is nonempty, and the type is
+   *  a singleton capability `x` or a reach capability `x*`, the deep capture
+   *  set can be narrowed to`{x*}`.
    */
   def deepCaptureSet(using Context): CaptureSet =
-    val dcs = CaptureSet.ofTypeDeeply(tp)
-    if dcs.isAlwaysEmpty then dcs
+    val dcs = CaptureSet.ofTypeDeeply(tp.widen.stripCapturing)
+    if dcs.isAlwaysEmpty then tp.captureSet
     else tp match
-      case tp @ ReachCapability(_) => tp.singletonCaptureSet
-      case tp: SingletonCaptureRef => tp.reach.singletonCaptureSet
-      case _ => dcs
+      case tp @ ReachCapability(_) =>
+        tp.singletonCaptureSet
+      case tp: SingletonCaptureRef if tp.isTrackableRef =>
+        tp.reach.singletonCaptureSet
+      case _ =>
+        tp.captureSet ++ dcs
 
   /** A type capturing `ref` */
   def capturing(ref: CaptureRef)(using Context): Type =
@@ -273,6 +276,29 @@ extension (tp: Type)
     case _ =>
       tp
 
+  /** The first element of this path type */
+  final def pathRoot(using Context): Type = tp.dealiasKeepAnnots match
+    case tp1: NamedType if tp1.symbol.owner.isClass => tp1.prefix.pathRoot
+    case ReachCapability(tp1) => tp1.pathRoot
+    case _ => tp
+
+  /** If this part starts with `C.this`, the class `C`.
+   *  Otherwise, if it starts with a reference `r`, `r`'s owner.
+   *  Otherwise NoSymbol.
+   */
+  final def pathOwner(using Context): Symbol = pathRoot match
+    case tp1: NamedType => tp1.symbol.owner
+    case tp1: ThisType => tp1.cls
+    case _ => NoSymbol
+
+  final def isParamPath(using Context): Boolean = tp.dealias match
+    case tp1: NamedType =>
+      tp1.prefix match
+        case _: ThisType | NoPrefix =>
+          tp1.symbol.is(Param) || tp1.symbol.is(ParamAccessor)
+        case prefix => prefix.isParamPath
+    case _ => false
+
   /** If this is a unboxed capturing type with nonempty capture set, its boxed version.
    *  Or, if type is a TypeBounds of capturing types, the version where the bounds are boxed.
    *  The identity for all other types.
@@ -468,29 +494,23 @@ extension (tp: Type)
     end CheckContraCaps
 
     object narrowCaps extends TypeMap:
-      /** Has the variance been flipped at this point? */
-      private var isFlipped: Boolean = false
-
       def apply(t: Type) =
-        val saved = isFlipped
-        try
-          if variance <= 0 then isFlipped = true
-          t.dealias match
-            case t1 @ CapturingType(p, cs) if cs.isUniversal && !isFlipped =>
-              t1.derivedCapturingType(apply(p), ref.reach.singletonCaptureSet)
-            case t1 @ FunctionOrMethod(args, res @ Existential(_, _))
-            if args.forall(_.isAlwaysPure) =>
-              // Also map existentials in results to reach capabilities if all
-              // preceding arguments are known to be always pure
-              apply(t1.derivedFunctionOrMethod(args, Existential.toCap(res)))
-            case Existential(_, _) =>
-              t
-            case _ => t match
-              case t @ CapturingType(p, cs) =>
-                t.derivedCapturingType(apply(p), cs) // don't map capture set variables
-              case t =>
-                mapOver(t)
-        finally isFlipped = saved
+        if variance <= 0 then t
+        else t.dealiasKeepAnnots match
+          case t @ CapturingType(p, cs) if cs.isUniversal =>
+            t.derivedCapturingType(apply(p), ref.reach.singletonCaptureSet)
+          case t @ AnnotatedType(parent, ann) =>
+            // Don't map annotations, which includes capture sets
+            t.derivedAnnotatedType(this(parent), ann)
+          case t @ FunctionOrMethod(args, res @ Existential(_, _))
+          if args.forall(_.isAlwaysPure) =>
+            // Also map existentials in results to reach capabilities if all
+            // preceding arguments are known to be always pure
+            apply(t.derivedFunctionOrMethod(args, Existential.toCap(res)))
+          case Existential(_, _) =>
+            t
+          case _ =>
+            mapOver(t)
     end narrowCaps
 
     ref match
@@ -639,8 +659,8 @@ object CapsOfApply:
 class AnnotatedCapability(annot: Context ?=> ClassSymbol):
   def apply(tp: Type)(using Context) =
     AnnotatedType(tp, Annotation(annot, util.Spans.NoSpan))
-  def unapply(tree: AnnotatedType)(using Context): Option[SingletonCaptureRef] = tree match
-    case AnnotatedType(parent: SingletonCaptureRef, ann) if ann.symbol == annot => Some(parent)
+  def unapply(tree: AnnotatedType)(using Context): Option[CaptureRef] = tree match
+    case AnnotatedType(parent: CaptureRef, ann) if ann.symbol == annot => Some(parent)
     case _ => None
 
 /** An extractor for `ref @annotation.internal.reachCapability`, which is used to express
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index 81b4287961ba..835e413463bd 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -1064,7 +1064,7 @@ object CaptureSet:
     case ref: (TermRef | TermParamRef) if ref.isMaxCapability =>
       if ref.isTrackableRef then ref.singletonCaptureSet
       else CaptureSet.universal
-    case ReachCapability(ref1) => deepCaptureSet(ref1.widen)
+    case ReachCapability(ref1) => ref1.widen.deepCaptureSet
       .showing(i"Deep capture set of $ref: ${ref1.widen} = $result", capt)
     case _ => ofType(ref.underlying, followResult = true)
 
@@ -1115,17 +1115,25 @@ object CaptureSet:
 
   /** The deep capture set of a type is the union of all covariant occurrences of
    *  capture sets. Nested existential sets are approximated with `cap`.
+   *  NOTE: The traversal logic needs to be in sync with narrowCaps in CaptureOps, which
+   *  replaces caps with reach capabilties.
    */
   def ofTypeDeeply(tp: Type)(using Context): CaptureSet =
     val collect = new TypeAccumulator[CaptureSet]:
-      def apply(cs: CaptureSet, t: Type) = t.dealias match
-        case t @ CapturingType(p, cs1) =>
-          val cs2 = apply(cs, p)
-          if variance > 0 then cs2 ++ cs1 else cs2
-        case t @ Existential(_, _) =>
-          apply(cs, Existential.toCap(t))
-        case _ =>
-          foldOver(cs, t)
+      def apply(cs: CaptureSet, t: Type) =
+        if variance <= 0 then cs
+        else t.dealias match
+          case t @ CapturingType(p, cs1) =>
+            this(cs, p) ++ cs1
+          case t @ AnnotatedType(parent, ann) =>
+            this(cs, parent)
+          case t @ FunctionOrMethod(args, res @ Existential(_, _))
+          if args.forall(_.isAlwaysPure) =>
+            this(cs, Existential.toCap(res))
+          case t @ Existential(_, _) =>
+            cs
+          case _ =>
+            foldOver(cs, t)
     collect(CaptureSet.empty, tp)
 
   type AssumedContains = immutable.Map[TypeRef, SimpleIdentitySet[CaptureRef]]
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 4d905a5df4ab..44c9a0f6a531 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -328,20 +328,22 @@ class CheckCaptures extends Recheck, SymTransformer:
         then CaptureSet.Var(sym.owner, level = sym.ccLevel)
         else CaptureSet.empty)
 
-    /** For all nested environments up to `limit` or a closed environment perform `op`,
-     *  but skip environmenrts directly enclosing environments of kind ClosureResult.
+    /** The next environment enclosing `env` that needs to be charged
+     *  with free references.
+     *  Skips environments directly enclosing environments of kind ClosureResult.
+     *  @param included Whether an environment is included in the range of
+     *                  environments to charge. Once `included` is false, no
+     *                  more environments need to be charged.
      */
-    def forallOuterEnvsUpTo(limit: Symbol)(op: Env => Unit)(using Context): Unit =
-      def recur(env: Env, skip: Boolean): Unit =
-        if env.isOpen && env.owner != limit then
-          if !skip then op(env)
-          if !env.isOutermost then
-            var nextEnv = env.outer
-            if env.owner.isConstructor then
-              if nextEnv.owner != limit && !nextEnv.isOutermost then
-                nextEnv = nextEnv.outer
-            recur(nextEnv, skip = env.kind == EnvKind.ClosureResult)
-      recur(curEnv, skip = false)
+    def nextEnvToCharge(env: Env, included: Env => Boolean)(using Context): Env =
+      var nextEnv = env.outer
+      if env.owner.isConstructor then
+        if included(nextEnv) then nextEnv = nextEnv.outer
+      if env.kind == EnvKind.ClosureResult then
+        // skip this one
+        nextEnvToCharge(nextEnv, included)
+      else
+        nextEnv
 
     /** A description where this environment comes from */
     private def provenance(env: Env)(using Context): String =
@@ -355,7 +357,6 @@ class CheckCaptures extends Recheck, SymTransformer:
       else
         i"\nof the enclosing ${owner.showLocated}"
 
-
     /** Include `sym` in the capture sets of all enclosing environments nested in the
      *  the environment in which `sym` is defined.
      */
@@ -364,9 +365,12 @@ class CheckCaptures extends Recheck, SymTransformer:
 
     def markFree(sym: Symbol, ref: TermRef, pos: SrcPos)(using Context): Unit =
       if sym.exists && ref.isTracked then
-        forallOuterEnvsUpTo(sym.enclosure): env =>
-          capt.println(i"Mark $sym with cs ${ref.captureSet} free in ${env.owner}")
-          checkElem(ref, env.captured, pos, provenance(env))
+        def recur(env: Env): Unit =
+          if env.isOpen && env.owner != sym.enclosure then
+            capt.println(i"Mark $sym with cs ${ref.captureSet} free in ${env.owner}")
+            checkElem(ref, env.captured, pos, provenance(env))
+            recur(nextEnvToCharge(env, _.owner != sym.enclosure))
+        recur(curEnv)
 
     /** Make sure (projected) `cs` is a subset of the capture sets of all enclosing
      *  environments. At each stage, only include references from `cs` that are outside
@@ -381,92 +385,66 @@ class CheckCaptures extends Recheck, SymTransformer:
         else
           !sym.isContainedIn(env.owner)
 
-      def checkSubsetEnv(cs: CaptureSet, env: Env)(using Context): Unit =
-        // Only captured references that are visible from the environment
-        // should be included.
-        val included = cs.filter: c =>
-          c.stripReach match
-            case ref: NamedType =>
-              val refSym = ref.symbol
-              val refOwner = refSym.owner
-              val isVisible = isVisibleFromEnv(refOwner, env)
-              if isVisible && !ref.isRootCapability then
-                ref match
-                  case ref: TermRef if ref.prefix `ne` NoPrefix =>
-                    // If c is a path of a class defined outside the environment,
-                    // we check the capture set of its info.
-                    checkSubsetEnv(ref.captureSetOfInfo, env)
-                  case _ =>
-              if !isVisible
-                  && (c.isReach || ref.isType)
-                  && (!ccConfig.useSealed || refSym.is(Param))
-                  && refOwner == env.owner
-              then
-                if refSym.hasAnnotation(defn.UnboxAnnot) then
-                  capt.println(i"exempt: $ref in $refOwner")
-                else
-                  // Reach capabilities that go out of scope have to be approximated
-                  // by their underlying capture set, which cannot be universal.
-                  // Reach capabilities of @unboxed parameters are exempted.
-                  val cs = CaptureSet.ofInfo(c)
-                  cs.disallowRootCapability: () =>
-                    report.error(em"Local reach capability $c leaks into capture scope of ${env.ownerString}", pos)
-                  checkSubset(cs, env.captured, pos, provenance(env))
-              isVisible
-            case ref: ThisType => isVisibleFromEnv(ref.cls, env)
-            case _ => false
-        checkSubset(included, env.captured, pos, provenance(env))
-        capt.println(i"Include call or box capture $included from $cs in ${env.owner} --> ${env.captured}")
-
-      if !cs.isAlwaysEmpty then
-        forallOuterEnvsUpTo(ctx.owner.topLevelClass): env =>
-          checkSubsetEnv(cs, env)
+      def checkUseDeclared(c: CaptureRef, env: Env) =
+        c.pathRoot match
+          case ref: NamedType if !ref.symbol.hasAnnotation(defn.UseAnnot) =>
+            val what = if ref.isType then "Capture set parameter" else "Local reach capability"
+            report.error(
+              em"""$what $c leaks into capture scope of ${env.ownerString}.
+                  |To allow this, the ${ref.symbol} should be declared with a @use annotation""", pos)
+          case _ =>
+
+      def recur(cs: CaptureSet, env: Env)(using Context): Unit =
+        if env.isOpen && !env.owner.isStaticOwner && !cs.isAlwaysEmpty then
+          // Only captured references that are visible from the environment
+          // should be included.
+          val included = cs.filter: c =>
+            val isVisible = c.pathRoot match
+              case ref: NamedType => isVisibleFromEnv(ref.symbol.owner, env)
+              case ref: ThisType => isVisibleFromEnv(ref.cls, env)
+              case ref =>
+                false
+            if !isVisible then
+              c match
+                case ReachCapability(c1) =>
+                  if c1.isParamPath then
+                    checkUseDeclared(c, env)
+                  else
+                    // When a reach capabilty x* where `x` is not a parameter goes out
+                    // of scope, we need to continue with `x`'s underlying deep capture set.
+                    // It is an error if that set contains cap.
+                    // The same is not an issue for normal capabilities since in a local
+                    // definition `val x = e`, the capabilities of `e` have already been charged.
+                    // Note: It's not true that the underlying capture set of a reach capability
+                    // is always cap. Reach capabilities over paths depend on the prefix, which
+                    // might turn a cap into something else.
+                    // The path-use.scala neg test contains an example.
+                    val underlying = CaptureSet.ofTypeDeeply(c1.widen)
+                    capt.println(i"Widen reach $c to $underlying in ${env.owner}")
+                    underlying.disallowRootCapability: () =>
+                      report.error(em"Local reach capability $c leaks into capture scope of ${env.ownerString}", pos)
+                    recur(underlying, env)
+                case c: TypeRef if c.isParamPath =>
+                  checkUseDeclared(c, env)
+                case _ =>
+            isVisible
+          checkSubset(included, env.captured, pos, provenance(env))
+          capt.println(i"Include call or box capture $included from $cs in ${env.owner} --> ${env.captured}")
+          recur(included, nextEnvToCharge(env, !_.owner.isStaticOwner))
+      recur(cs, curEnv)
     end markFree
 
     /** Include references captured by the called method in the current environment stack */
-    def includeCallCaptures(sym: Symbol, pos: SrcPos)(using Context): Unit =
-      if sym.exists && curEnv.isOpen then markFree(capturedVars(sym), pos)
-
-    private val prefixCalls = util.EqHashSet[GenericApply]()
-    private val unboxedArgs = util.EqHashSet[Tree]()
-
-    def handleCall(meth: Symbol, call: GenericApply, eval: () => Type)(using Context): Type =
-      if prefixCalls.remove(call) then return eval()
-
-      val unboxedParamNames =
-        meth.rawParamss.flatMap: params =>
-          params.collect:
-            case param if param.hasAnnotation(defn.UnboxAnnot) =>
-              param.name
-        .toSet
-
-      def markUnboxedArgs(call: GenericApply): Unit = call.fun.tpe.widen match
-        case MethodType(pnames) =>
-          for (pname, arg) <- pnames.lazyZip(call.args) do
-            if unboxedParamNames.contains(pname) then
-              unboxedArgs.add(arg)
-        case _ =>
-
-      def markPrefixCalls(tree: Tree): Unit = tree match
-        case tree: GenericApply =>
-          prefixCalls.add(tree)
-          markUnboxedArgs(tree)
-          markPrefixCalls(tree.fun)
-        case _ =>
-
-      markUnboxedArgs(call)
-      markPrefixCalls(call.fun)
-      val res = eval()
-      includeCallCaptures(meth, call.srcPos)
-      res
-    end handleCall
+    def includeCallCaptures(sym: Symbol, resType: Type, pos: SrcPos)(using Context): Unit = resType match
+      case _: MethodOrPoly => // wait until method is fully applied
+      case _ =>
+        if sym.exists && curEnv.isOpen then markFree(capturedVars(sym), pos)
 
     override def recheckIdent(tree: Ident, pt: Type)(using Context): Type =
-      if tree.symbol.is(Method) then
-        if tree.symbol.info.isParameterless then
-          // there won't be an apply; need to include call captures now
-          includeCallCaptures(tree.symbol, tree.srcPos)
-      else if !tree.symbol.isStatic then
+      val sym = tree.symbol
+      if sym.is(Method) then
+        includeCallCaptures(sym, sym.info, tree.srcPos)
+      else if !sym.isStatic then
         //debugShowEnvs()
         def addSelects(ref: TermRef, pt: Type): TermRef = pt match
           case pt: PathSelectionProto if ref.isTracked =>
@@ -474,11 +452,11 @@ class CheckCaptures extends Recheck, SymTransformer:
             // class SerializationProxy in stdlib-cc/../LazyListIterable.scala has an example where this matters.
             addSelects(ref.select(pt.sym).asInstanceOf[TermRef], pt.pt)
           case _ => ref
-        val ref = tree.symbol.termRef
+        val ref = sym.termRef
         val pathRef = addSelects(ref, pt)
         //if pathRef ne ref then
         //  println(i"add selects $ref --> $pathRef")
-        markFree(tree.symbol, if false then ref else pathRef, tree.srcPos)
+        markFree(sym, if false then ref else pathRef, tree.srcPos)
       super.recheckIdent(tree, pt)
 
     override def selectionProto(tree: Select, pt: Type)(using Context): Type =
@@ -536,6 +514,16 @@ class CheckCaptures extends Recheck, SymTransformer:
           selType
     }//.showing(i"recheck sel $tree, $qualType = $result")
 
+    /** Copy all @use annotations on method parameter symbols to the corresponding paramInfo types.
+     */
+    override def prepareFunction(funtpe: MethodType, meth: Symbol)(using Context): MethodType =
+      val paramInfosWithUses = funtpe.paramInfos.zipWithConserve(funtpe.paramNames): (formal, pname) =>
+        val paramOpt = meth.rawParamss.nestedFind(_.name == pname)
+        paramOpt.flatMap(_.getAnnotation(defn.UseAnnot)) match
+          case Some(ann) => AnnotatedType(formal, ann)
+          case _ => formal
+      funtpe.derivedLambdaType(paramInfos = paramInfosWithUses)
+
     override def recheckApply(tree: Apply, pt: Type)(using Context): Type =
       val meth = tree.fun.symbol
 
@@ -570,15 +558,19 @@ class CheckCaptures extends Recheck, SymTransformer:
             tp.derivedCapturingType(forceBox(parent), refs)
         mapArgUsing(forceBox)
       else
-        handleCall(meth, tree, () => super.recheckApply(tree, pt))
+        val res = super.recheckApply(tree, pt)
+        includeCallCaptures(meth, res, tree.srcPos)
+        res
     end recheckApply
 
     protected override
     def recheckArg(arg: Tree, formal: Type)(using Context): Type =
       val argType = recheck(arg, formal)
-      if unboxedArgs.contains(arg) then
-        capt.println(i"charging deep capture set of $arg: ${argType} = ${argType.deepCaptureSet}")
-        markFree(argType.deepCaptureSet, arg.srcPos)
+      formal match
+        case AnnotatedType(formal1, ann) if ann.symbol == defn.UseAnnot =>
+          capt.println(i"charging deep capture set of $arg: ${argType} = ${argType.deepCaptureSet}")
+          markFree(argType.deepCaptureSet, arg.srcPos)
+        case _ =>
       argType
 
     /** A specialized implementation of the apply rule.
@@ -589,13 +581,13 @@ class CheckCaptures extends Recheck, SymTransformer:
      *  ---------------------
      *  E |- f(a): Tr^C
      *
-     *  If the function `f` does not have an `@unboxed` parameter, then
+     *  If the function `f` does not have an `@use` parameter, then
      *  any unboxing it does would be charged to the environment of the function
      *  so they have to appear in Cq. Since any capabilities of the result of the
      *  application must already be present in the application, an upper
      *  approximation of the result capture set is Cq \union Ca, where `Ca`
      *  is the capture set of the argument.
-     *  If the function `f` does have an `@unboxed` parameter, then it could in addition
+     *  If the function `f` does have an `@use` parameter, then it could in addition
      *  unbox reach capabilities over its formal parameter. Therefore, the approximation
      *  would be `Cq \union dcs(Ca)` instead.
      *  If the approximation is known to subcapture the declared result Cr, we pick it for C
@@ -606,10 +598,10 @@ class CheckCaptures extends Recheck, SymTransformer:
       val appType = Existential.toCap(super.recheckApplication(tree, qualType, funType, argTypes))
       val qualCaptures = qualType.captureSet
       val argCaptures =
-        for (arg, argType) <- tree.args.lazyZip(argTypes) yield
-          if unboxedArgs.remove(arg) // need to ensure the remove happens, that's why argCaptures is computed even if not needed.
-          then argType.deepCaptureSet
-          else argType.captureSet
+        for (argType, formal) <- argTypes.lazyZip(funType.paramInfos) yield
+          formal match
+            case AnnotatedType(_, ann) if ann.symbol == defn.UseAnnot => argType.deepCaptureSet
+            case _ => argType.captureSet
       appType match
         case appType @ CapturingType(appType1, refs)
         if qualType.exists
@@ -704,8 +696,10 @@ class CheckCaptures extends Recheck, SymTransformer:
               i"Sealed type variable $pname", "be instantiated to",
               i"This is often caused by a local capability$where\nleaking as part of its result.",
               tree.srcPos)
-      try handleCall(meth, tree, () => Existential.toCap(super.recheckTypeApply(tree, pt)))
-      finally checkContains(tree)
+      val res = Existential.toCap(super.recheckTypeApply(tree, pt))
+      includeCallCaptures(meth, res, tree.srcPos)
+      checkContains(tree)
+      res
     end recheckTypeApply
 
     /** Faced with a tree of form `caps.contansImpl[CS, r.type]`, check that `R` is a tracked
@@ -1156,22 +1150,12 @@ class CheckCaptures extends Recheck, SymTransformer:
         (erefs /: erefs.elems): (erefs, eref) =>
           eref match
             case eref: ThisType if isPureContext(ctx.owner, eref.cls) =>
-
-              def pathRoot(aref: Type): Type = aref match
-                case aref: NamedType if aref.symbol.owner.isClass => pathRoot(aref.prefix)
-                case _ => aref
-
-              def isOuterRef(aref: Type): Boolean = pathRoot(aref) match
-                case aref: NamedType => eref.cls.isProperlyContainedIn(aref.symbol.owner)
-                case aref: ThisType => eref.cls.isProperlyContainedIn(aref.cls)
-                case _ => false
-
-              val outerRefs = arefs.filter(isOuterRef)
-
+              val outerRefs = arefs.filter: aref =>
+                eref.cls.isProperlyContainedIn(aref.pathOwner)
               // Include implicitly added outer references in the capture set of the class of `eref`.
               for outerRef <- outerRefs.elems do
                 if !erefs.elems.contains(outerRef)
-                    && !pathRoot(outerRef).isInstanceOf[ThisType]
+                    && !outerRef.pathRoot.isInstanceOf[ThisType]
                     // we don't need to add outer ThisTypes as these are anyway added as path
                     // prefixes at the use site. And this exemption is required since capture sets
                     // of non-local classes are always empty, so we can't add an outer this to them.
@@ -1328,6 +1312,12 @@ class CheckCaptures extends Recheck, SymTransformer:
 
     /** If actual is a tracked CaptureRef `a` and widened is a capturing type T^C,
      *  improve `T^C` to `T^{a}`, following the VAR rule of CC.
+     *  TODO: We probably should do this also for other top-level occurrences of captures
+     *  E.g.
+     *    class Foo { def a: C^{io}; val def: C^{async} }
+     *    val foo: Foo^{io, async}
+     *  Then
+     *    foo: Foo { def a: C^{foo}; def b: C^{foo} }^{foo}
      */
     private def improveCaptures(widened: Type, actual: Type)(using Context): Type = actual match
       case ref: CaptureRef if ref.isTracked =>
@@ -1389,16 +1379,16 @@ class CheckCaptures extends Recheck, SymTransformer:
 
         override def checkInheritedTraitParameters: Boolean = false
 
-        /** Check that overrides don't change the @unbox status of their parameters */
+        /** Check that overrides don't change the @use status of their parameters */
         override def additionalChecks(member: Symbol, other: Symbol)(using Context): Unit =
           for
             (params1, params2) <- member.rawParamss.lazyZip(other.rawParamss)
             (param1, param2) <- params1.lazyZip(params2)
           do
-            if param1.hasAnnotation(defn.UnboxAnnot) != param2.hasAnnotation(defn.UnboxAnnot) then
+            if param1.hasAnnotation(defn.UseAnnot) != param2.hasAnnotation(defn.UseAnnot) then
               report.error(
                 OverrideError(
-                    i"has a parameter ${param1.name} with different @unbox status than the corresponding parameter in the overridden definition",
+                    i"has a parameter ${param1.name} with different @use status than the corresponding parameter in the overridden definition",
                     self, member, other, self.memberInfo(member), self.memberInfo(other)
                   ),
                 if member.owner == clazz then member.srcPos else clazz.srcPos
diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala
index 76ae41649517..665bdb446c86 100644
--- a/compiler/src/dotty/tools/dotc/cc/Setup.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -523,13 +523,16 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
               // substitute `x.f.type`, `x` becomes a `TermParamRef`. But the new method
               // type is still under initialization and `paramInfos` is still `null`,
               // so the new `NamedType` will not have a denoation.
+              def adaptedInfo(psym: Symbol, info: mt.PInfo): mt.PInfo = mt.companion match
+                case mtc: MethodTypeCompanion => mtc.adaptParamInfo(psym, info).asInstanceOf[mt.PInfo]
+                case _ => info
               mt.companion(mt.paramNames)(
                 mt1 =>
                   if !paramSignatureChanges && !mt.isParamDependent && prevLambdas.isEmpty then
                     mt.paramInfos
                   else
                     val subst = SubstParams(psyms :: prevPsymss, mt1 :: prevLambdas)
-                    psyms.map(psym => subst(psym.nextInfo).asInstanceOf[mt.PInfo]),
+                    psyms.map(psym => adaptedInfo(psym, subst(psym.nextInfo).asInstanceOf[mt.PInfo])),
                 mt1 =>
                   integrateRT(mt.resType, psymss.tail, resType, psyms :: prevPsymss, mt1 :: prevLambdas)
               )
@@ -751,7 +754,8 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
             report.warning(em"redundant capture: $dom already accounts for $ref", pos)
 
         if ref.captureSetOfInfo.elems.isEmpty && !ref.derivesFrom(defn.Caps_Capability) then
-          report.error(em"$ref cannot be tracked since its capture set is empty", pos)
+          val deepStr = if ref.isReach then " deep" else ""
+          report.error(em"$ref cannot be tracked since its$deepStr capture set is empty", pos)
         check(parent.captureSet, parent)
 
         val others =
diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala
index 0195a4ddbf34..1e36cb6f22db 100644
--- a/compiler/src/dotty/tools/dotc/core/Definitions.scala
+++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala
@@ -1057,12 +1057,12 @@ class Definitions {
   @tu lazy val ExperimentalAnnot: ClassSymbol = requiredClass("scala.annotation.experimental")
   @tu lazy val ThrowsAnnot: ClassSymbol = requiredClass("scala.throws")
   @tu lazy val TransientAnnot: ClassSymbol = requiredClass("scala.transient")
-  @tu lazy val UnboxAnnot:  ClassSymbol = requiredClass("scala.caps.unbox")
   @tu lazy val UncheckedAnnot: ClassSymbol = requiredClass("scala.unchecked")
   @tu lazy val UncheckedStableAnnot: ClassSymbol = requiredClass("scala.annotation.unchecked.uncheckedStable")
   @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.untrackedCaptures")
+  @tu lazy val UseAnnot:  ClassSymbol = requiredClass("scala.caps.use")
   @tu lazy val VolatileAnnot: ClassSymbol = requiredClass("scala.volatile")
   @tu lazy val BeanGetterMetaAnnot: ClassSymbol = requiredClass("scala.annotation.meta.beanGetter")
   @tu lazy val BeanSetterMetaAnnot: ClassSymbol = requiredClass("scala.annotation.meta.beanSetter")
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index 8a9d44cb8d25..ab25d0ae8389 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -4178,24 +4178,28 @@ object Types extends TypeUtils {
      *   - wrap types of parameters that have an @allowConversions annotation with Into[_]
      */
     def fromSymbols(params: List[Symbol], resultType: Type)(using Context): MethodType =
+      apply(params.map(_.name.asTermName))(
+         tl => params.map(p => tl.integrate(params, adaptParamInfo(p))),
+         tl => tl.integrate(params, resultType))
+
+    /** Adapt info of parameter symbol to be integhrated into corresponding MethodType
+     *  using the scheme described in `fromSymbols`.
+     */
+    def adaptParamInfo(param: Symbol, pinfo: Type)(using Context): Type =
       def addAnnotation(tp: Type, cls: ClassSymbol, param: Symbol): Type = tp match
         case ExprType(resType) => ExprType(addAnnotation(resType, cls, param))
         case _ => AnnotatedType(tp, Annotation(cls, param.span))
-
-      def paramInfo(param: Symbol) =
-        var paramType = param.info
-          .annotatedToRepeated
-          .mapIntoAnnot(defn.IntoAnnot, defn.IntoParamAnnot)
-        if param.is(Inline) then
-          paramType = addAnnotation(paramType, defn.InlineParamAnnot, param)
-        if param.is(Erased) then
-          paramType = addAnnotation(paramType, defn.ErasedParamAnnot, param)
-        paramType
-
-      apply(params.map(_.name.asTermName))(
-         tl => params.map(p => tl.integrate(params, paramInfo(p))),
-         tl => tl.integrate(params, resultType))
-    end fromSymbols
+      var paramType = pinfo
+        .annotatedToRepeated
+        .mapIntoAnnot(defn.IntoAnnot, defn.IntoParamAnnot)
+      if param.is(Inline) then
+        paramType = addAnnotation(paramType, defn.InlineParamAnnot, param)
+      if param.is(Erased) then
+        paramType = addAnnotation(paramType, defn.ErasedParamAnnot, param)
+      paramType
+
+    def adaptParamInfo(param: Symbol)(using Context): Type =
+      adaptParamInfo(param, param.info)
 
     def apply(paramNames: List[TermName])(paramInfosExp: MethodType => List[Type], resultTypeExp: MethodType => Type)(using Context): MethodType =
       checkValid(unique(new CachedMethodType(paramNames)(paramInfosExp, resultTypeExp, self)))
diff --git a/compiler/src/dotty/tools/dotc/transform/Recheck.scala b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
index 8df9e5966920..33f8eeb42eff 100644
--- a/compiler/src/dotty/tools/dotc/transform/Recheck.scala
+++ b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
@@ -99,7 +99,7 @@ object Recheck:
    *   - in function and method parameter types
    *   - under annotations
    */
-  def normalizeByName(tp: Type)(using Context): Type = tp.dealias match
+  def normalizeByName(tp: Type)(using Context): Type = tp.dealiasKeepAnnots match
     case tp: ExprType =>
       mapExprType(tp)
     case tp: PolyType =>
@@ -291,7 +291,7 @@ abstract class Recheck extends Phase, SymTransformer:
     protected def instantiate(mt: MethodType, argTypes: List[Type], sym: Symbol)(using Context): Type =
       mt.instantiate(argTypes)
 
-    /** A hook to massage the type of an applied method; currently not overridden */
+    /** A hook to massage the type of an applied method */
     protected def prepareFunction(funtpe: MethodType, meth: Symbol)(using Context): MethodType = funtpe
 
     protected def recheckArg(arg: Tree, formal: Type)(using Context): Type =
@@ -336,7 +336,7 @@ abstract class Recheck extends Phase, SymTransformer:
               assert(formals.isEmpty)
               Nil
           val argTypes = recheckArgs(tree.args, formals, fntpe.paramRefs)
-          recheckApplication(tree, qualType, fntpe1, argTypes)
+          recheckApplication(tree, qualType, fntpe, argTypes)
             //.showing(i"typed app $tree : $fntpe with ${tree.args}%, % : $argTypes%, % = $result")
         case tp =>
           assert(false, i"unexpected type of ${tree.fun}: $tp")
diff --git a/library/src/scala/caps.scala b/library/src/scala/caps.scala
index 9911ef920116..6c7610e410c0 100644
--- a/library/src/scala/caps.scala
+++ b/library/src/scala/caps.scala
@@ -55,7 +55,7 @@ import annotation.{experimental, compileTimeOnly, retainsCap}
   /** This should go into annotations. For now it is here, so that we
    *  can experiment with it quickly between minor releases
    */
-  final class unbox extends annotation.StaticAnnotation
+  final class use extends annotation.StaticAnnotation
 
   object unsafe:
 
diff --git a/scala2-library-cc/src/scala/collection/Iterator.scala b/scala2-library-cc/src/scala/collection/Iterator.scala
index 4d1b0ed4ff95..22632d738199 100644
--- a/scala2-library-cc/src/scala/collection/Iterator.scala
+++ b/scala2-library-cc/src/scala/collection/Iterator.scala
@@ -1159,7 +1159,8 @@ object Iterator extends IterableFactory[Iterator] {
         // If we advanced the current iterator to a ConcatIterator, merge it into this one
         @tailrec def merge(): Unit =
           if (current.isInstanceOf[ConcatIterator[_]]) {
-            val c = current.asInstanceOf[ConcatIterator[A]]
+            val c: ConcatIterator[A] { val from: Iterator[A] }
+               = current.asInstanceOf
             current = c.current.asInstanceOf // !!! CC unsafe op
             currentHasNextChecked = c.currentHasNextChecked
             if (c.tail != null) {
diff --git a/tests/neg-custom-args/captures/delayedRunops.check b/tests/neg-custom-args/captures/delayedRunops.check
new file mode 100644
index 000000000000..68da4672acf5
--- /dev/null
+++ b/tests/neg-custom-args/captures/delayedRunops.check
@@ -0,0 +1,14 @@
+-- Error: tests/neg-custom-args/captures/delayedRunops.scala:16:13 -----------------------------------------------------
+16 |      runOps(ops1)  // error
+   |             ^^^^
+   |             reference ops* is not included in the allowed capture set {}
+   |             of an enclosing function literal with expected type () -> Unit
+-- Error: tests/neg-custom-args/captures/delayedRunops.scala:22:13 -----------------------------------------------------
+22 |      runOps(ops1)  // error
+   |             ^^^^
+   |             Local reach capability ops1* leaks into capture scope of enclosing function
+-- Error: tests/neg-custom-args/captures/delayedRunops.scala:28:13 -----------------------------------------------------
+28 |      runOps(ops1)  // error
+   |             ^^^^
+   |             reference ops* is not included in the allowed capture set {}
+   |             of an enclosing function literal with expected type () -> Unit
diff --git a/tests/neg-custom-args/captures/delayedRunops.scala b/tests/neg-custom-args/captures/delayedRunops.scala
new file mode 100644
index 000000000000..191118fa19c9
--- /dev/null
+++ b/tests/neg-custom-args/captures/delayedRunops.scala
@@ -0,0 +1,28 @@
+import language.experimental.captureChecking
+import caps.use
+
+  // ok
+  def runOps(@use ops: List[() => Unit]): Unit =
+    ops.foreach(op => op())
+
+  // ok
+  def delayedRunOps(@use ops: List[() => Unit]): () ->{ops*} Unit = // @use should not be necessary in the future
+    () => runOps(ops)
+
+  // unsound: impure operation pretended pure
+  def delayedRunOps1(ops: List[() => Unit]): () ->{} Unit =
+    () =>
+      val ops1 = ops
+      runOps(ops1)  // error
+
+  // unsound: impure operation pretended pure
+  def delayedRunOps2(ops: List[() => Unit]): () ->{} Unit =
+    () =>
+      val ops1: List[() => Unit] = ops
+      runOps(ops1)  // error
+
+  // unsound: impure operation pretended pure
+  def delayedRunOps3(ops: List[() => Unit]): () ->{} Unit =
+    () =>
+      val ops1: List[() ->{ops*} Unit] = ops
+      runOps(ops1)  // error
diff --git a/tests/neg-custom-args/captures/i15749a.scala b/tests/neg-custom-args/captures/i15749a.scala
index 57fca27fae66..d3c1fce13322 100644
--- a/tests/neg-custom-args/captures/i15749a.scala
+++ b/tests/neg-custom-args/captures/i15749a.scala
@@ -1,5 +1,5 @@
 import caps.cap
-import caps.unbox
+import caps.use
 
 class Unit
 object u extends Unit
@@ -18,7 +18,7 @@ def test =
 
   def force[A](thunk: Unit ->{cap} A): A = thunk(u)
 
-  def forceWrapper[A](@unbox mx: Wrapper[Unit ->{cap} A]): Wrapper[A] =
+  def forceWrapper[A](@use mx: Wrapper[Unit ->{cap} A]): Wrapper[A] =
     // Γ ⊢ mx: Wrapper[□ {cap} Unit => A]
     // `force` should be typed as ∀(□ {cap} Unit -> A) A, but it can not
     strictMap[Unit ->{mx*} A, A](mx)(t => force[A](t)) // error // should work
diff --git a/tests/neg-custom-args/captures/i16114.check b/tests/neg-custom-args/captures/i16114.check
new file mode 100644
index 000000000000..6d81d8d63747
--- /dev/null
+++ b/tests/neg-custom-args/captures/i16114.check
@@ -0,0 +1,55 @@
+-- Error: tests/neg-custom-args/captures/i16114.scala:18:12 ------------------------------------------------------------
+18 |      expect[Cap^] {  // error
+   |      ^^^^^^^^^^^^
+   |      Sealed type variable T cannot be instantiated to box Cap^ since
+   |      that type captures the root capability `cap`.
+   |      This is often caused by a local capability in an argument of method expect
+   |      leaking as part of its result.
+-- Error: tests/neg-custom-args/captures/i16114.scala:20:8 -------------------------------------------------------------
+20 |        fs  // error (limitation)
+   |        ^^
+   |        (fs : Cap^) cannot be referenced here; it is not included in the allowed capture set {io}
+   |        of an enclosing function literal with expected type Unit ->{io} Unit
+-- Error: tests/neg-custom-args/captures/i16114.scala:24:12 ------------------------------------------------------------
+24 |      expect[Cap^] { // error
+   |      ^^^^^^^^^^^^
+   |      Sealed type variable T cannot be instantiated to box Cap^ since
+   |      that type captures the root capability `cap`.
+   |      This is often caused by a local capability in an argument of method expect
+   |      leaking as part of its result.
+-- Error: tests/neg-custom-args/captures/i16114.scala:26:8 -------------------------------------------------------------
+26 |        io  // error (limitation)
+   |        ^^
+   |        (io : Cap^) cannot be referenced here; it is not included in the allowed capture set {fs}
+   |        of an enclosing function literal with expected type Unit ->{fs} Unit
+-- Error: tests/neg-custom-args/captures/i16114.scala:30:12 ------------------------------------------------------------
+30 |      expect[Cap^] {  // error
+   |      ^^^^^^^^^^^^
+   |      Sealed type variable T cannot be instantiated to box Cap^ since
+   |      that type captures the root capability `cap`.
+   |      This is often caused by a local capability in an argument of method expect
+   |      leaking as part of its result.
+-- Error: tests/neg-custom-args/captures/i16114.scala:36:12 ------------------------------------------------------------
+36 |      expect[Cap^](io) // error
+   |      ^^^^^^^^^^^^
+   |      Sealed type variable T cannot be instantiated to box Cap^ since
+   |      that type captures the root capability `cap`.
+   |      This is often caused by a local capability in an argument of method expect
+   |      leaking as part of its result.
+-- Error: tests/neg-custom-args/captures/i16114.scala:39:12 ------------------------------------------------------------
+39 |      expect[Cap^] { // error
+   |      ^^^^^^^^^^^^
+   |      Sealed type variable T cannot be instantiated to box Cap^ since
+   |      that type captures the root capability `cap`.
+   |      This is often caused by a local capability in an argument of method expect
+   |      leaking as part of its result.
+-- Error: tests/neg-custom-args/captures/i16114.scala:40:8 -------------------------------------------------------------
+40 |        io.use()    // error
+   |        ^^
+   |        (io : Cap^) cannot be referenced here; it is not included in the allowed capture set {}
+   |        of an enclosing function literal with expected type Unit -> Unit
+-- Error: tests/neg-custom-args/captures/i16114.scala:41:8 -------------------------------------------------------------
+41 |        io          // error
+   |        ^^
+   |        (io : Cap^) cannot be referenced here; it is not included in the allowed capture set {}
+   |        of an enclosing function literal with expected type Unit -> Unit
diff --git a/tests/neg-custom-args/captures/i21347.check b/tests/neg-custom-args/captures/i21347.check
index c680a54d3efc..e1845d9778d5 100644
--- a/tests/neg-custom-args/captures/i21347.check
+++ b/tests/neg-custom-args/captures/i21347.check
@@ -1,15 +1,12 @@
 -- Error: tests/neg-custom-args/captures/i21347.scala:4:15 -------------------------------------------------------------
 4 |  ops.foreach: op => // error
   |               ^
-  |               Local reach capability C leaks into capture scope of method runOps
+  |               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()
--- Error: tests/neg-custom-args/captures/i21347.scala:8:14 -------------------------------------------------------------
-8 |  () => runOps(f :: Nil) // error
-  |        ^^^^^^^^^^^^^^^^
-  |        reference (caps.cap : caps.Capability) is not included in the allowed capture set {}
-  |        of an enclosing function literal with expected type () -> Unit
 -- Error: tests/neg-custom-args/captures/i21347.scala:11:15 ------------------------------------------------------------
 11 |  ops.foreach: op => // error
    |               ^
-   |               Local reach capability ops* leaks into capture scope of method runOpsAlt
+   |               Local reach capability ops* leaks into capture scope of method runOpsAlt.
+   |               To allow this, the parameter ops should be declared with a @use annotation
 12 |    op()
diff --git a/tests/neg-custom-args/captures/i21347.scala b/tests/neg-custom-args/captures/i21347.scala
index 41887be6a78a..54fe859caedd 100644
--- a/tests/neg-custom-args/captures/i21347.scala
+++ b/tests/neg-custom-args/captures/i21347.scala
@@ -5,7 +5,7 @@ def runOps[C^](ops: List[() ->{C^} Unit]): Unit =
     op()
 
 def boom(f: () => Unit): () -> Unit =
-  () => runOps(f :: Nil) // error
+  () => runOps(f :: Nil) // now ok
 
 def runOpsAlt(ops: List[() => Unit]): Unit =
   ops.foreach: op => // error
diff --git a/tests/neg-custom-args/captures/i21442.check b/tests/neg-custom-args/captures/i21442.check
index a3bbf65c5988..30becfea0215 100644
--- a/tests/neg-custom-args/captures/i21442.check
+++ b/tests/neg-custom-args/captures/i21442.check
@@ -1,7 +1,8 @@
 -- Error: tests/neg-custom-args/captures/i21442.scala:9:13 -------------------------------------------------------------
 9 |  val io = x.unbox // error: local reach capability {x*} leaks
   |           ^^^^^^^
-  |           Local reach capability x* leaks into capture scope of method foo
+  |           Local reach capability x* leaks into capture scope of method foo.
+  |           To allow this, the parameter x should be declared with a @use annotation
 -- Error: tests/neg-custom-args/captures/i21442.scala:17:14 ------------------------------------------------------------
 17 |  val io = x1.unbox // error
    |           ^^^^^^^^
diff --git a/tests/neg-custom-args/captures/i21614.scala b/tests/neg-custom-args/captures/i21614.scala
index a5ed25d818a5..69aef446e9e2 100644
--- a/tests/neg-custom-args/captures/i21614.scala
+++ b/tests/neg-custom-args/captures/i21614.scala
@@ -1,12 +1,12 @@
 import language.experimental.captureChecking
 import caps.Capability
-import caps.unbox
+import caps.use
 
 trait File extends Capability
 class Logger(f: File^) extends Capability // <- will work if we remove the extends clause
 
-def mkLoggers1[F <: File^](@unbox files: List[F]): List[Logger^] =
+def mkLoggers1[F <: File^](@use files: List[F]): List[Logger^] =
   files.map((f: F) => new Logger(f)) // error, Q: can we make this pass (see #19076)?
 
-def mkLoggers2(@unbox files: List[File^]): List[Logger^] =
+def mkLoggers2(@use files: List[File^]): List[Logger^] =
   files.map(new Logger(_)) // error, Q: can we improve the error message?
diff --git a/tests/neg-custom-args/captures/i21646.scala b/tests/neg-custom-args/captures/i21646.scala
new file mode 100644
index 000000000000..42c493a9ea80
--- /dev/null
+++ b/tests/neg-custom-args/captures/i21646.scala
@@ -0,0 +1,13 @@
+import language.experimental.captureChecking
+import caps.Capability
+
+trait File extends Capability
+
+class Resource[T <: Capability](gen: T):
+  def use[U](f: T => U): U =
+    f(gen) // error
+
+@main def run =
+  val myFile: File = ???
+  val r = Resource(myFile) // error
+  ()
diff --git a/tests/neg-custom-args/captures/leak-problem-2.scala b/tests/neg-custom-args/captures/leak-problem-2.scala
index 08a3a6c2d9ca..8ca298dbdd1e 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.unbox sources: Seq[Source[T]^]): Source[T]^{sources*} = ???
+def race[T](@caps.use sources: Seq[Source[T]^]): Source[T]^{sources*} = ???
 
 def raceTwo[T](src1: Source[T]^, src2: Source[T]^): Source[T]^{}
   = race(Seq(src1, src2)) // error
diff --git a/tests/neg-custom-args/captures/path-use.check b/tests/neg-custom-args/captures/path-use.check
new file mode 100644
index 000000000000..e09ee232dd17
--- /dev/null
+++ b/tests/neg-custom-args/captures/path-use.check
@@ -0,0 +1,4 @@
+-- Error: tests/neg-custom-args/captures/path-use.scala:18:32 ----------------------------------------------------------
+18 |  val g = () => println(c.procs.head) // error, local reach capability c.procs* leaks
+   |                        ^^^^^^^^^^^^
+   |                        Local reach capability c.procs* leaks into capture scope of method test
diff --git a/tests/neg-custom-args/captures/path-use.scala b/tests/neg-custom-args/captures/path-use.scala
new file mode 100644
index 000000000000..31feb4c0adf4
--- /dev/null
+++ b/tests/neg-custom-args/captures/path-use.scala
@@ -0,0 +1,25 @@
+import language.experimental.namedTuples
+
+class IO
+
+class C(val f: IO^):
+  val procs: List[Proc] = ???
+
+type Proc = () => Unit
+
+def test(io: IO^) =
+  val c = C(io)
+  val f = () => println(c.f)
+  val _: () ->{c.f} Unit = f
+
+  val x = c.procs
+  val _: List[() ->{c.procs*} Unit] = x
+
+  val g = () => println(c.procs.head) // error, local reach capability c.procs* leaks
+  val _: () ->{c.procs*} Unit = g
+
+  val cc: C { val f: IO^{io}; val procs: List[() ->{io} Unit] }^{io} =
+    ???
+
+  val gg = () => println(cc.procs.head) // OK, since cc.procs* has {io} as underlying capture set
+  val _: () ->{io} Unit = gg
diff --git a/tests/neg-custom-args/captures/reaches.check b/tests/neg-custom-args/captures/reaches.check
index f00fea09ed8c..0121f0cf7a55 100644
--- a/tests/neg-custom-args/captures/reaches.check
+++ b/tests/neg-custom-args/captures/reaches.check
@@ -30,7 +30,7 @@
    |    ^^^^^^^^^^^^^^^^^^^
    |    Local reach capability id* leaks into capture scope of method test
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:62:27 --------------------------------------
-62 |    val f1: File^{id*} = id(f) // error, since now id(f): File^
+62 |    val f1: File^{id*} = id(f) // error, since now id(f): File^ // error
    |                         ^^^^^
    |                         Found:    File^{f}
    |                         Required: File^{id*}
@@ -39,14 +39,24 @@
 -- Error: tests/neg-custom-args/captures/reaches.scala:79:10 -----------------------------------------------------------
 79 |  ps.map((x, y) => compose1(x, y)) // error // error
    |          ^
-   |          Local reach capability ps* leaks into capture scope of method mapCompose
+   |          Local reach capability ps* leaks into capture scope of method mapCompose.
+   |          To allow this, the parameter ps should be declared with a @use annotation
 -- Error: tests/neg-custom-args/captures/reaches.scala:79:13 -----------------------------------------------------------
 79 |  ps.map((x, y) => compose1(x, y)) // error // error
    |             ^
-   |             Local reach capability ps* leaks into capture scope of method mapCompose
+   |             Local reach capability ps* leaks into capture scope of method mapCompose.
+   |             To allow this, the parameter ps should be declared with a @use annotation
 -- [E057] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:53:51 --------------------------------------
 53 |  val id: Id[Proc, Proc] = new Id[Proc, () -> Unit] // error
    |                                                   ^
    |                                             Type argument () -> Unit does not conform to lower bound () => Unit
    |
    | longer explanation available when compiling with `-explain`
+-- Error: tests/neg-custom-args/captures/reaches.scala:61:31 -----------------------------------------------------------
+61 |  val leaked = usingFile[File^{id*}]: f => // error
+   |                               ^^^
+   |                               id* cannot be tracked since its deep capture set is empty
+-- Error: tests/neg-custom-args/captures/reaches.scala:62:18 -----------------------------------------------------------
+62 |    val f1: File^{id*} = id(f) // error, since now id(f): File^ // error
+   |                  ^^^
+   |                  id* cannot be tracked since its deep capture set is empty
diff --git a/tests/neg-custom-args/captures/reaches.scala b/tests/neg-custom-args/captures/reaches.scala
index c33ba80a668b..066c40031553 100644
--- a/tests/neg-custom-args/captures/reaches.scala
+++ b/tests/neg-custom-args/captures/reaches.scala
@@ -1,4 +1,4 @@
-import caps.unbox
+import caps.use
 class File:
   def write(): Unit = ???
 
@@ -11,7 +11,7 @@ class Ref[T](init: T):
   def get: T = x
   def set(y: T) = { x = y }
 
-def runAll0(@unbox xs: List[Proc]): Unit =
+def runAll0(@use xs: List[Proc]): Unit =
   var cur: List[() ->{xs*} Unit] = xs
   while cur.nonEmpty do
     val next: () ->{xs*} Unit = cur.head
@@ -21,7 +21,7 @@ def runAll0(@unbox xs: List[Proc]): Unit =
   usingFile: f =>
     cur = (() => f.write()) :: Nil // error
 
-def runAll1(@unbox xs: List[Proc]): Unit =
+def runAll1(@use xs: List[Proc]): Unit =
   val cur = Ref[List[() ->{xs*} Unit]](xs)  // OK, by revised VAR
   while cur.get.nonEmpty do
     val next: () ->{xs*} Unit = cur.get.head
@@ -58,8 +58,8 @@ def attack2 =
   val id: File^ -> File^ = x => x
     // val id: File^ -> EX C.File^C
 
-  val leaked = usingFile[File^{id*}]: f =>
-    val f1: File^{id*} = id(f) // error, since now id(f): File^
+  val leaked = usingFile[File^{id*}]: f => // error
+    val f1: File^{id*} = id(f) // error, since now id(f): File^ // error
     f1
 
 class List[+A]:
@@ -78,5 +78,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 // error
 
-def mapCompose2[A](@unbox ps: List[(A => A, A => A)]): List[A ->{ps*} A] =
+def mapCompose2[A](@use ps: List[(A => A, A => A)]): List[A ->{ps*} A] =
   ps.map((x, y) => compose1(x, y))
diff --git a/tests/neg-custom-args/captures/real-try.check b/tests/neg-custom-args/captures/real-try.check
index 7f8ab50bc222..1e1644d38d23 100644
--- a/tests/neg-custom-args/captures/real-try.check
+++ b/tests/neg-custom-args/captures/real-try.check
@@ -1,7 +1,7 @@
--- [E190] Potential Issue Warning: tests/neg-custom-args/captures/real-try.scala:38:4 ----------------------------------
-38 |  b.x
-   |  ^^^
-   |  Discarded non-Unit value of type () -> Unit. You may want to use `()`.
+-- [E190] Potential Issue Warning: tests/neg-custom-args/captures/real-try.scala:38:2 ----------------------------------
+38 |  b
+   |  ^
+   |  Discarded non-Unit value of type Cell[() -> Unit]. You may want to use `()`.
    |
    | longer explanation available when compiling with `-explain`
 -- Error: tests/neg-custom-args/captures/real-try.scala:14:2 -----------------------------------------------------------
diff --git a/tests/neg-custom-args/captures/real-try.scala b/tests/neg-custom-args/captures/real-try.scala
index 51f1a0fdea5a..8e60d4fe7326 100644
--- a/tests/neg-custom-args/captures/real-try.scala
+++ b/tests/neg-custom-args/captures/real-try.scala
@@ -35,4 +35,4 @@ def test(): Unit =
     case _: Ex1 => ???
     case _: Ex2 => ???
 
-  b.x
+  b
diff --git a/tests/neg-custom-args/captures/refine-reach-shallow.scala b/tests/neg-custom-args/captures/refine-reach-shallow.scala
index 525d33fdb7c5..f78c99f919af 100644
--- a/tests/neg-custom-args/captures/refine-reach-shallow.scala
+++ b/tests/neg-custom-args/captures/refine-reach-shallow.scala
@@ -5,14 +5,15 @@ def test1(): Unit =
   val g: IO^ => IO^{f*} = f  // error
 def test2(): Unit =
   val f: [R] -> (IO^ => R) -> R = ???
-  val g: [R] -> (IO^{f*} => R) -> R = f  // error
+  val ff = f
+  val g: [R] -> (IO^{f*} => R) -> R = f  // error // error
 def test3(): Unit =
   val f: [R] -> (IO^ -> R) -> R = ???
-  val g: [R] -> (IO^{f*} -> R) -> R = f  // error
+  val g: [R] -> (IO^{f*} -> R) -> R = f  // error // error
 def test4(): Unit =
   val xs: List[IO^] = ???
   val ys: List[IO^{xs*}] = xs  // ok
 def test5(): Unit =
   val f: [R] -> (IO^ -> R) -> IO^ = ???
-  val g: [R] -> (IO^ -> R) -> IO^{f*} = f  // error
-  val h: [R] -> (IO^{f*} -> R) -> IO^ = f  // error
+  val g: [R] -> (IO^ -> R) -> IO^{f*} = f  // error // error
+  val h: [R] -> (IO^{f*} -> R) -> IO^ = f  // error // error
diff --git a/tests/neg-custom-args/captures/refine-withFile.scala b/tests/neg-custom-args/captures/refine-withFile.scala
index 823b62711d05..e7958ab66fc8 100644
--- a/tests/neg-custom-args/captures/refine-withFile.scala
+++ b/tests/neg-custom-args/captures/refine-withFile.scala
@@ -4,5 +4,5 @@ trait File
 val useFile: [R] -> (path: String) -> (op: File^ -> R) -> R = ???
 def main(): Unit =
   val f: [R] -> (path: String) -> (op: File^ -> R) -> R = useFile
-  val g: [R] -> (path: String) -> (op: File^{f*} -> R) -> R = f  // error
-  val leaked = g[File^{f*}]("test")(f => f)  // boom
+  val g: [R] -> (path: String) -> (op: File^{f*} -> R) -> R = f  // error // error
+  val leaked = g[File^{f*}]("test")(f => f)  // error
diff --git a/tests/neg-custom-args/captures/spread-problem.scala b/tests/neg-custom-args/captures/spread-problem.scala
index 579c7817b9c1..75f3a615cde8 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.unbox sources: (Source[T]^)*): Source[T]^{sources*} = ???
+def race[T](@caps.use sources: (Source[T]^)*): Source[T]^{sources*} = ???
 
 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 b9a3be7bffbc..dbffc164b5c5 100644
--- a/tests/neg-custom-args/captures/unbox-overrides.check
+++ b/tests/neg-custom-args/captures/unbox-overrides.check
@@ -2,20 +2,20 @@
 8 |  def foo(x: C): C        // error
   |      ^
   |error overriding method foo in trait A of type (x: C): C;
-  |  method foo of type (x: C): C has a parameter x with different @unbox status than the corresponding parameter in the overridden definition
+  |  method foo of type (x: C): C has a parameter x with different @use status than the corresponding parameter in the overridden definition
   |
   | longer explanation available when compiling with `-explain`
 -- [E164] Declaration Error: tests/neg-custom-args/captures/unbox-overrides.scala:9:6 ----------------------------------
-9 |  def bar(@unbox x: C): C // error
+9 |  def bar(@use x: C): C // error
   |      ^
   |error overriding method bar in trait A of type (x: C): C;
-  |  method bar of type (x: C): C has a parameter x with different @unbox status than the corresponding parameter in the overridden definition
+  |  method bar of type (x: C): C has a parameter x with different @use status than the corresponding parameter in the overridden definition
   |
   | longer explanation available when compiling with `-explain`
 -- [E164] Declaration Error: tests/neg-custom-args/captures/unbox-overrides.scala:15:15 --------------------------------
 15 |abstract class C extends A[C], B2 // error
    |               ^
    |error overriding method foo in trait A of type (x: C): C;
-   |  method foo in trait B2 of type (x: C): C has a parameter x with different @unbox status than the corresponding parameter in the overridden definition
+   |  method foo in trait B2 of type (x: C): C has a parameter x with different @use status than the corresponding parameter in the overridden definition
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/unbox-overrides.scala b/tests/neg-custom-args/captures/unbox-overrides.scala
index 5abb5013bfbe..6164ca274eaf 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.unbox
+import caps.use
 
 trait A[X]:
-  def foo(@unbox x: X): X
+  def foo(@use x: X): X
   def bar(x: X): X
 
 trait B extends A[C]:
   def foo(x: C): C        // error
-  def bar(@unbox x: C): C // error
+  def bar(@use x: C): C // error
 
 trait B2:
   def foo(x: C): C
-  def bar(@unbox x: C): C
+  def bar(@use x: C): C
 
 abstract class C extends A[C], B2 // error
diff --git a/tests/neg-custom-args/captures/unsound-reach-3.scala b/tests/neg-custom-args/captures/unsound-reach-3.scala
index 0063216e957e..985beb7ae55d 100644
--- a/tests/neg-custom-args/captures/unsound-reach-3.scala
+++ b/tests/neg-custom-args/captures/unsound-reach-3.scala
@@ -16,8 +16,8 @@ def bad(): Unit =
   val boom: Foo[File^{backdoor*}] = backdoor
 
   var escaped: File^{backdoor*} = null
-  withFile("hello.txt"): f => // error
-    escaped = boom.use(f)
+  withFile("hello.txt"): f =>
+    escaped = boom.use(f) // error
       // boom.use: (x: File^) -> File^{backdoor*}, it is a selection so reach capabilities are allowed
       // f: File^, so there is no reach capabilities
 
diff --git a/tests/neg-custom-args/captures/unsound-reach-4.check b/tests/neg-custom-args/captures/unsound-reach-4.check
index d359b298555e..ed8e29cdf511 100644
--- a/tests/neg-custom-args/captures/unsound-reach-4.check
+++ b/tests/neg-custom-args/captures/unsound-reach-4.check
@@ -1,6 +1,4 @@
--- Error: tests/neg-custom-args/captures/unsound-reach-4.scala:21:25 ---------------------------------------------------
-21 |  withFile("hello.txt"): f =>  // error
-   |                         ^
-   |                         Reach capability backdoor* and universal capability cap cannot both
-   |                         appear in the type (f: File^) ->{backdoor*} Unit of this expression
-22 |    escaped = boom.use(f)
+-- Error: tests/neg-custom-args/captures/unsound-reach-4.scala:22:22 ---------------------------------------------------
+22 |    escaped = boom.use(f)  // error
+   |              ^^^^^^^^^^^
+   |              Local reach capability backdoor* leaks into capture scope of method bad
diff --git a/tests/neg-custom-args/captures/unsound-reach-4.scala b/tests/neg-custom-args/captures/unsound-reach-4.scala
index bc66085614f2..14050b4afff2 100644
--- a/tests/neg-custom-args/captures/unsound-reach-4.scala
+++ b/tests/neg-custom-args/captures/unsound-reach-4.scala
@@ -18,5 +18,5 @@ def bad(): Unit =
   val boom: Foo[File^{backdoor*}] = backdoor
 
   var escaped: File^{backdoor*} = null
-  withFile("hello.txt"): f =>  // error
-    escaped = boom.use(f)
+  withFile("hello.txt"): f =>
+    escaped = boom.use(f)  // error
diff --git a/tests/neg-custom-args/captures/uses.check b/tests/neg-custom-args/captures/uses.check
new file mode 100644
index 000000000000..de583d75db06
--- /dev/null
+++ b/tests/neg-custom-args/captures/uses.check
@@ -0,0 +1,28 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/uses.scala:8:17 ------------------------------------------
+8 |  val _: D^{y} = d // error, should be ok
+  |                 ^
+  |                 Found:    (d : D^{x, y})
+  |                 Required: D^{y}
+  |
+  | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/uses.scala:9:13 ------------------------------------------
+9 |  val _: D = d // error
+  |             ^
+  |             Found:    (d : D^{x, y})
+  |             Required: D
+  |
+  | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/uses.scala:18:34 -----------------------------------------
+18 |  val _: () ->{x} () ->{y} Unit = g // error, should be ok
+   |                                  ^
+   |                                  Found:    () ->{x, y} (ex$7: caps.Exists) -> () ->{y} Unit
+   |                                  Required: () ->{x} () ->{y} Unit
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/uses.scala:19:28 -----------------------------------------
+19 |  val _: () -> () -> Unit = g // error
+   |                            ^
+   |                            Found:    () ->{x, y} (ex$7: caps.Exists) -> () ->{y} Unit
+   |                            Required: () -> () -> Unit
+   |
+   | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/uses.scala b/tests/neg-custom-args/captures/uses.scala
new file mode 100644
index 000000000000..b872c7b03ec7
--- /dev/null
+++ b/tests/neg-custom-args/captures/uses.scala
@@ -0,0 +1,20 @@
+class C
+def test(x: C^, y: C^) =
+  class D {
+    println(x)
+    def foo() = println(y)
+  }
+  val d = D()
+  val _: D^{y} = d // error, should be ok
+  val _: D = d // error
+
+  val f = () => println(D())
+  val _: () ->{x} Unit = f // ok
+  val _: () -> Unit = f // should be error
+
+  def g = () =>
+    println(x)
+    () => println(y)
+  val _: () ->{x} () ->{y} Unit = g // error, should be ok
+  val _: () -> () -> Unit = g // error
+
diff --git a/tests/neg-custom-args/captures/wf-reach-1.check b/tests/neg-custom-args/captures/wf-reach-1.check
new file mode 100644
index 000000000000..6a3ac9771a11
--- /dev/null
+++ b/tests/neg-custom-args/captures/wf-reach-1.check
@@ -0,0 +1,4 @@
+-- Error: tests/neg-custom-args/captures/wf-reach-1.scala:2:17 ---------------------------------------------------------
+2 |  val y: Object^{x*} = ??? // error
+  |                 ^^
+  |                 x* cannot be tracked since its deep capture set is empty
diff --git a/tests/neg-custom-args/captures/wf-reach-1.scala b/tests/neg-custom-args/captures/wf-reach-1.scala
new file mode 100644
index 000000000000..c8901c7ae4a8
--- /dev/null
+++ b/tests/neg-custom-args/captures/wf-reach-1.scala
@@ -0,0 +1,2 @@
+def test(x: List[() -> Unit]) =
+  val y: Object^{x*} = ??? // error
diff --git a/tests/neg-custom-args/captures/widen-reach.check b/tests/neg-custom-args/captures/widen-reach.check
index 06d21ff445d8..abc065a1e2bc 100644
--- a/tests/neg-custom-args/captures/widen-reach.check
+++ b/tests/neg-custom-args/captures/widen-reach.check
@@ -1,11 +1,13 @@
 -- Error: tests/neg-custom-args/captures/widen-reach.scala:13:26 -------------------------------------------------------
 13 |  val y2: IO^ -> IO^ = y1.foo      // error
    |                       ^^^^^^
-   |                       Local reach capability x* leaks into capture scope of method test
+   |                       Local reach capability x* leaks into capture scope of method test.
+   |                       To allow this, the parameter x should be declared with a @use annotation
 -- Error: tests/neg-custom-args/captures/widen-reach.scala:14:30 -------------------------------------------------------
 14 |  val y3: IO^ -> IO^{x*} = y1.foo  // error
    |                           ^^^^^^
-   |                           Local reach capability x* leaks into capture scope of method test
+   |                           Local reach capability x* leaks into capture scope of method test.
+   |                           To allow this, the parameter x should be declared with a @use annotation
 -- [E164] Declaration Error: tests/neg-custom-args/captures/widen-reach.scala:9:6 --------------------------------------
 9 |  val foo: IO^ -> IO^ = x => x // error
   |      ^
diff --git a/tests/neg/i20503.scala b/tests/neg/i20503.scala
index 3fb0573f6c2f..828b6ce71137 100644
--- a/tests/neg/i20503.scala
+++ b/tests/neg/i20503.scala
@@ -1,5 +1,5 @@
 import language.experimental.captureChecking
-import caps.unbox
+import caps.use
 
 class List[+A]:
   def head: A = ???
@@ -8,7 +8,7 @@ class List[+A]:
   def foreach[U](f: A => U): Unit = ???
   def nonEmpty: Boolean = ???
 
-def runOps(@unbox ops: List[() => Unit]): Unit =
+def runOps(@use ops: List[() => 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/leak-problem-unboxed.scala b/tests/neg/leak-problem-unboxed.scala
index 7de3d84bfcca..aedd7c889112 100644
--- a/tests/neg/leak-problem-unboxed.scala
+++ b/tests/neg/leak-problem-unboxed.scala
@@ -1,5 +1,5 @@
 import language.experimental.captureChecking
-import caps.unbox
+import caps.use
 
 // Some capabilities that should be used locally
 trait Async:
@@ -9,12 +9,12 @@ def usingAsync[X](op: Async^ => X): X = ???
 
 case class Box[+T](get: T)
 
-def useBoxedAsync(@unbox x: Box[Async^]): Unit =
+def useBoxedAsync(@use x: Box[Async^]): Unit =
   val t0 = x
   val t1 = t0.get // ok
   t1.read()
 
-def useBoxedAsync1(@unbox x: Box[Async^]): Unit = x.get.read() // ok
+def useBoxedAsync1(@use x: Box[Async^]): Unit = x.get.read() // ok
 
 def test(): Unit =
 
diff --git a/tests/neg/leak-problem.scala b/tests/neg/leak-problem.scala
index 354d54d86707..c842280c0587 100644
--- a/tests/neg/leak-problem.scala
+++ b/tests/neg/leak-problem.scala
@@ -1,4 +1,5 @@
 import language.experimental.captureChecking
+import caps.use
 
 // Some capabilities that should be used locally
 trait Async:
@@ -16,12 +17,28 @@ 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 =
+    val t0 = x
+    val t1 = t0.get
+    t1.read()
+
+  def useBoxedAsync1(@use x: Box[Async^]): Unit = x.get.read()
+
+  val xs: Box[Async^] = ???
+  val xsLambda = () => useBoxedAsync(xs) // error
+  val _: () ->{xs*} Unit = xsLambda
+  val _: () -> Unit = xsLambda // error
+
   val useBoxedAsync2 = (x: Box[Async^]) =>
     val t0 = x
     val t1 = x.get // error
     t1.read()
 
-  val f: Box[Async^] => Unit = (x:  Box[Async^]) => useBoxedAsync(x)
+  val xsLambda2 = () => useBoxedAsync2(xs)
+  val _: () ->{xs*} Unit = xsLambda2
+  val _: () -> Unit = xsLambda2
+
+  val f: Box[Async^] => Unit = (x:  Box[Async^]) => useBoxedAsync(x) // error
 
   def boom(x: Async^): () ->{f} Unit =
     () => f(Box(x))
diff --git a/tests/pos-custom-args/captures/Buffer.scala b/tests/pos-custom-args/captures/Buffer.scala
index 2412e5b388ca..9ecd51ffa62a 100644
--- a/tests/pos-custom-args/captures/Buffer.scala
+++ b/tests/pos-custom-args/captures/Buffer.scala
@@ -10,7 +10,7 @@ trait Buffer[A]:
     val s = 10
      // capture checking: we need the copy since we box/unbox on g* on the next line
       // TODO: This looks fishy, need to investigate
-      // Alternative would be to mark `f` as @unbox. It's not inferred
+      // Alternative would be to mark `f` as @use. It's not inferred
       // since `^ appears in a function result, not under a box.
     val newElems = new Array[(IterableOnce[A]^{f})](s)
     var i = 0
diff --git a/tests/pos-custom-args/captures/dep-reach.scala b/tests/pos-custom-args/captures/dep-reach.scala
index c81197aa738d..1ee6fc3d17f9 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.unbox
+import caps.use
 object Test:
   class C
   type Proc = () => Unit
 
   def f(c: C^, d: C^): () ->{c, d} Unit =
-    def foo(@unbox xs: Proc*): () ->{xs*} Unit =
+    def foo(@use xs: Proc*): () ->{xs*} 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(@unbox xs: Seq[() => Unit]): () ->{xs*} Unit =
+    def foo(@use xs: Seq[() => Unit]): () ->{xs*} Unit =
       xs.head
 
     val a: () ->{c} Unit = () => ()
diff --git a/tests/pos-custom-args/captures/erased-methods.scala b/tests/pos-custom-args/captures/erased-methods.scala
new file mode 100644
index 000000000000..911c779e08e5
--- /dev/null
+++ b/tests/pos-custom-args/captures/erased-methods.scala
@@ -0,0 +1,20 @@
+import language.experimental.saferExceptions
+import language.experimental.erasedDefinitions
+import language.experimental.captureChecking
+
+class Ex1 extends Exception("Ex1")
+class Ex2 extends Exception("Ex2")
+class Ex3 extends Exception("Ex3")
+
+def foo8a(i: Int) =
+  (erased xx1: CanThrow[Ex2]^) ?=> throw new Ex2
+
+def foo9a(i: Int)
+  : (erased x$0: CanThrow[Ex3]^)
+    ?=> (erased x$1: CanThrow[Ex2]^)
+    ?=> (erased x$2: CanThrow[Ex1]^)
+    ?=> Unit
+  = (erased x$1: CanThrow[Ex3]^)
+     ?=> (erased x$2: CanThrow[Ex2]^)
+     ?=> (erased x$3: CanThrow[Ex1]^)
+     ?=> throw new Ex3
diff --git a/tests/pos/gears-probem.scala b/tests/pos-custom-args/captures/gears-problem.scala
similarity index 89%
rename from tests/pos/gears-probem.scala
rename to tests/pos-custom-args/captures/gears-problem.scala
index 2e445c985de2..c6ef72bc421e 100644
--- a/tests/pos/gears-probem.scala
+++ b/tests/pos-custom-args/captures/gears-problem.scala
@@ -1,4 +1,5 @@
 import language.experimental.captureChecking
+import caps.use
 
 trait Future[+T]:
   def await: T
@@ -10,7 +11,7 @@ class Collector[T](val futures: Seq[Future[T]^]):
   val results: Channel[Future[T]^{futures*}] = ???
 end Collector
 
-extension [T](fs: Seq[Future[T]^])
+extension [T](@use fs: Seq[Future[T]^])
   def awaitAll =
     val collector: Collector[T]{val futures: Seq[Future[T]^{fs*}]}
        = Collector(fs)
diff --git a/tests/pos-custom-args/captures/path-use.scala b/tests/pos-custom-args/captures/path-use.scala
index 5eb2b60fd218..629fa04315a7 100644
--- a/tests/pos-custom-args/captures/path-use.scala
+++ b/tests/pos-custom-args/captures/path-use.scala
@@ -1,4 +1,5 @@
 import language.experimental.namedTuples
+import caps.use
 
 class IO
 
@@ -8,12 +9,14 @@ class C(val f: IO^):
 type Proc = () => Unit
 
 def test(io: IO^) =
-  val c = C(io)
-  val f = () => println(c.f)
-  val _: () ->{c.f} Unit = f
+  def test1(@use c: C { val f: IO^{io}}^{io}) =
+    val f = () => println(c.f)
+    val _: () ->{c.f} Unit = f
 
-  val x = c.procs
-  val _: List[() ->{c.procs*} Unit] = x
+    val x = c.procs
+    val _: List[() ->{c.procs*} Unit] = x
+
+    val g = () => println(c.procs.head)
+    val _: () ->{c.procs*} Unit = g
+  test1(C(io))
 
-  val g = () => println(c.procs.head)
-  val _: () ->{c.procs*} Unit = g
diff --git a/tests/pos-custom-args/captures/reaches.scala b/tests/pos-custom-args/captures/reaches.scala
index ab0da9b67d18..cbe88e60020b 100644
--- a/tests/pos-custom-args/captures/reaches.scala
+++ b/tests/pos-custom-args/captures/reaches.scala
@@ -1,4 +1,4 @@
-import caps.unbox
+import caps.use
 
 class C
 def f(xs: List[C^]) =
@@ -22,7 +22,7 @@ extension [A](x: A) def :: (xs: List[A]): List[A] = ???
 
 object Nil extends List[Nothing]
 
-def runAll(@unbox xs: List[Proc]): Unit =
+def runAll(@use xs: List[Proc]): Unit =
   var cur: List[() ->{xs*} Unit] = xs  // OK, by revised VAR
   while cur.nonEmpty do
     val next: () ->{xs*} Unit = cur.head
diff --git a/tests/pos/Buffer.scala b/tests/pos/Buffer.scala
index 2412e5b388ca..9ecd51ffa62a 100644
--- a/tests/pos/Buffer.scala
+++ b/tests/pos/Buffer.scala
@@ -10,7 +10,7 @@ trait Buffer[A]:
     val s = 10
      // capture checking: we need the copy since we box/unbox on g* on the next line
       // TODO: This looks fishy, need to investigate
-      // Alternative would be to mark `f` as @unbox. It's not inferred
+      // Alternative would be to mark `f` as @use. It's not inferred
       // since `^ appears in a function result, not under a box.
     val newElems = new Array[(IterableOnce[A]^{f})](s)
     var i = 0
diff --git a/tests/pos/cc-poly-source-capability.scala b/tests/pos/cc-poly-source-capability.scala
index 3b6c0bde1398..363f261dadc1 100644
--- a/tests/pos/cc-poly-source-capability.scala
+++ b/tests/pos/cc-poly-source-capability.scala
@@ -1,7 +1,7 @@
 import language.experimental.captureChecking
 import annotation.experimental
 import caps.{CapSet, Capability}
-import caps.unbox
+import caps.use
 
 @experimental object Test:
 
@@ -18,7 +18,7 @@ import caps.unbox
 
     def allListeners: Set[Listener^{X^}] = listeners
 
-  def test1(async1: Async, @unbox others: List[Async]) =
+  def test1(async1: Async, @use others: List[Async]) =
     val src = Source[CapSet^{async1, others*}]
     val lst1 = listener(async1)
     val lsts = others.map(listener)
diff --git a/tests/pos/cc-poly-source.scala b/tests/pos/cc-poly-source.scala
index 4cfbbaa06936..2de5c6d67340 100644
--- a/tests/pos/cc-poly-source.scala
+++ b/tests/pos/cc-poly-source.scala
@@ -1,7 +1,7 @@
 import language.experimental.captureChecking
 import annotation.experimental
 import caps.{CapSet, Capability}
-import caps.unbox
+import caps.use
 
 @experimental object Test:
 
@@ -25,7 +25,7 @@ import caps.unbox
     val ls = src.allListeners
     val _: Set[Listener^{lbl1, lbl2}] = ls
 
-  def test2(@unbox lbls: List[Label^]) =
+  def test2(@use lbls: List[Label^]) =
     def makeListener(lbl: Label^): Listener^{lbl} = ???
     val listeners = lbls.map(makeListener)
     val src = Source[CapSet^{lbls*}]
diff --git a/tests/pos/gears-probem-1.scala b/tests/pos/gears-probem-1.scala
index ab71616b72fc..d363515afece 100644
--- a/tests/pos/gears-probem-1.scala
+++ b/tests/pos/gears-probem-1.scala
@@ -1,5 +1,5 @@
 import language.experimental.captureChecking
-import caps.unbox
+import caps.use
 
 trait Future[+T]:
   def await: T
@@ -17,7 +17,7 @@ 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](@unbox fs: Seq[Future[T]^])
+extension [T](@use fs: Seq[Future[T]^])
   def awaitAll =
     val collector//: Collector[T]{val futures: Seq[Future[T]^{fs*}]}
        = Collector(fs)
diff --git a/tests/pos/i18699.scala b/tests/pos/i18699.scala
index 1937d7dca8c5..5a0a9357f774 100644
--- a/tests/pos/i18699.scala
+++ b/tests/pos/i18699.scala
@@ -1,9 +1,9 @@
 import language.experimental.captureChecking
-import caps.unbox
+import caps.use
 
 trait Cap:
   def use: Int = 42
 
-def test2(@unbox cs: List[Cap^]): Unit =
+def test2(@use cs: List[Cap^]): Unit =
   val t0: Cap^{cs*} = cs.head  // error
   var t1: Cap^{cs*} = cs.head  // error
diff --git a/tests/pos/reach-capability.scala b/tests/pos/reach-capability.scala
index 50ea479ec3c1..08e82a1dabe9 100644
--- a/tests/pos/reach-capability.scala
+++ b/tests/pos/reach-capability.scala
@@ -1,7 +1,7 @@
 import language.experimental.captureChecking
 import annotation.experimental
 import caps.Capability
-import caps.unbox
+import caps.use
 
 @experimental object Test2:
 
@@ -12,7 +12,7 @@ import caps.unbox
 
   class Listener
 
-  def test2(@unbox lbls: List[Label]) =
+  def test2(@use lbls: List[Label]) =
     def makeListener(lbl: Label): Listener^{lbl} = ???
     val listeners = lbls.map(makeListener) // should work
 
diff --git a/tests/pos/reach-problem.scala b/tests/pos/reach-problem.scala
index d6b7b79011a6..f36a4af14ad2 100644
--- a/tests/pos/reach-problem.scala
+++ b/tests/pos/reach-problem.scala
@@ -1,11 +1,11 @@
 import language.experimental.captureChecking
-import caps.unbox
+import caps.use
 
 class Box[T](items: Seq[T^]):
   def getOne: T^{items*} = ???
 
 object Box:
-  def getOne[T](@unbox items: Seq[T^]): T^{items*} =
+  def getOne[T](@use items: Seq[T^]): T^{items*} =
     val bx = Box(items)
     bx.getOne
 /*