diff --git a/compiler/src/dotty/tools/dotc/ast/untpd.scala b/compiler/src/dotty/tools/dotc/ast/untpd.scala
index 60309d4d83bd..b86734afcc0a 100644
--- a/compiler/src/dotty/tools/dotc/ast/untpd.scala
+++ b/compiler/src/dotty/tools/dotc/ast/untpd.scala
@@ -525,8 +525,8 @@ object untpd extends Trees.Instance[Untyped] with UntypedTreeInfo {
   def makeRetaining(parent: Tree, refs: List[Tree], annotName: TypeName)(using Context): Annotated =
     Annotated(parent, New(scalaAnnotationDot(annotName), List(refs)))
 
-  def makeCapsOf(id: Ident)(using Context): Tree =
-    TypeApply(Select(scalaDot(nme.caps), nme.capsOf), id :: Nil)
+  def makeCapsOf(tp: Tree)(using Context): Tree =
+    TypeApply(Select(scalaDot(nme.caps), nme.capsOf), tp :: Nil)
 
   def makeCapsBound()(using Context): Tree =
     makeRetaining(
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
index 29c6528e36de..0bc9297b55bd 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
@@ -79,6 +79,15 @@ def depFun(args: List[Type], resultType: Type, isContextual: Boolean, paramNames
 /** An exception thrown if a @retains argument is not syntactically a CaptureRef */
 class IllegalCaptureRef(tpe: Type)(using Context) extends Exception(tpe.show)
 
+/** The type of a function to be called when a `caps.$use[T]` is encountered in a subtype
+ *  comparison.
+ *  @param tpUnderUse   the type under the caps.$use[...]
+ *  @param other        the type it is compared with
+ *  @param fromBelow    If true it's `other <: tpUnderUse` otherwise it's `tpUnderUse <: other`
+ *  @param op           The subtype test to possibly perform as a continuation
+ */
+type UseHandler = (toUnderUse: Type, other: Type, fromBelow: Boolean) => (op: () => Boolean) => Boolean
+
 /** Capture checking state, which is known to other capture checking components */
 class CCState:
 
@@ -92,6 +101,16 @@ class CCState:
    */
   val approxWarnings: mutable.ListBuffer[Message] = mutable.ListBuffer()
 
+  /** The operation to perform `recordUse` is called. This is typically the case
+   *  when a subtype check is performed between a part of a function argument
+   *  and a corresponding part of a formal parameter that was labelled @use.
+   *  Such annotations are mapped to `caps.$use[T]` applications, which are handled
+   *  as compiletime ops.
+   *  The parameter to the handler is typically the deep capture set of the argument.
+   *  The result of the handler is the result to be returned from the subtype check.
+   */
+  private var useHandler: UseHandler = (tpUnderUse, other, fromBelow) => op => op()
+
   private var curLevel: Level = outermostLevel
   private val symLevel: mutable.Map[Symbol, Int] = mutable.Map()
 
@@ -108,6 +127,19 @@ object CCState:
    */
   def currentLevel(using Context): Level = ccState.curLevel
 
+  /** Perform operation `op` with a given useHandler to be called when `caps.$use[T]` types
+   *  are encountered.
+   */
+  inline def withUseHandler[T](handler: UseHandler)(inline op: T)(using Context): T =
+    val ccs = ccState
+    val saved = ccs.useHandler
+    ccs.useHandler = handler
+    try op finally ccs.useHandler = saved
+
+  /** Call the current use handler with given arguments. This might then call `op`. */
+  def underUse[T](tpUnderUse: Type, other: Type, fromBelow: Boolean)(op: => Boolean)(using Context): Boolean =
+    ccState.useHandler(tpUnderUse, other, fromBelow)(() => op)
+
   inline def inNestedLevel[T](inline op: T)(using Context): T =
     val ccs = ccState
     val saved = ccs.curLevel
@@ -194,7 +226,8 @@ extension (tp: Type)
       true
     case tp: TermRef =>
       ((tp.prefix eq NoPrefix)
-      || tp.symbol.is(ParamAccessor) && tp.prefix.isThisTypeOf(tp.symbol.owner)
+      || tp.symbol.isField && !tp.symbol.isStatic && (
+        tp.prefix.isThisTypeOf(tp.symbol.owner) || tp.prefix.isTrackableRef)
       || tp.isRootCapability
       ) && !tp.symbol.isOneOf(UnstableValueFlags)
     case tp: TypeRef =>
@@ -204,6 +237,7 @@ extension (tp: Type)
     case AnnotatedType(parent, annot) =>
       (annot.symbol == defn.ReachCapabilityAnnot
       || annot.symbol == defn.MaybeCapabilityAnnot
+      || annot.symbol == defn.UseAnnot
       ) && parent.isTrackableRef
     case _ =>
       false
@@ -230,7 +264,7 @@ extension (tp: Type)
   def deepCaptureSet(using Context): CaptureSet =
     val dcs = CaptureSet.ofTypeDeeply(tp)
     if dcs.isAlwaysEmpty then dcs
-    else tp match
+    else tp.stripUse match
       case tp @ ReachCapability(_) => tp.singletonCaptureSet
       case tp: SingletonCaptureRef => tp.reach.singletonCaptureSet
       case _ => dcs
@@ -421,6 +455,14 @@ extension (tp: Type)
     case tp: CaptureRef if tp.isTrackableRef =>
       if tp.isMaybe then tp else MaybeCapability(tp)
 
+  def isUnderUse(using Context): Boolean = tp match
+    case AnnotatedType(_: CaptureRef, annot) => annot.symbol == defn.UseAnnot
+    case _ => false
+
+  def stripUse(using Context): Type = tp match
+    case AnnotatedType(tp1: CaptureRef, annot) if annot.symbol == defn.UseAnnot => tp1
+    case _ => tp
+
   /** If `ref` is a trackable capture ref, and `tp` has only covariant occurrences of a
    *  universal capture set, replace all these occurrences by `{ref*}`. This implements
    *  the new aspect of the (Var) rule, which can now be stated as follows:
@@ -470,26 +512,34 @@ extension (tp: Type)
     object narrowCaps extends TypeMap:
       /** Has the variance been flipped at this point? */
       private var isFlipped: Boolean = false
+      private var underUse = 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(_, _))
+          t.dealiasKeepAnnots match
+            case t @ CapturingType(p, cs) if cs.isUniversal && !isFlipped =>
+              var reach = ref.reach
+              if underUse then reach = reach.underUse
+              t.derivedCapturingType(apply(p), reach.singletonCaptureSet)
+            case t @ AnnotatedType(parent, ann) =>
+              if ann.symbol == defn.UseAnnot then
+                val saved = underUse
+                underUse = true
+                try mapOver(t)
+                finally underUse = saved
+              else
+                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(t1.derivedFunctionOrMethod(args, Existential.toCap(res)))
+              this(t.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)
+            case _ =>
+              mapOver(t)
         finally isFlipped = saved
     end narrowCaps
 
@@ -639,8 +689,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(tp: AnnotatedType)(using Context): Option[CaptureRef] = tp.stripUse 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/CaptureRef.scala b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
index f00c6869cd80..8097eee2fe7a 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
@@ -13,6 +13,7 @@ import CCState.*
 import Periods.NoRunId
 import compiletime.uninitialized
 import StdNames.nme
+import Annotations.Annotation
 
 /** A trait for references in CaptureSets. These can be NamedTypes, ThisTypes or ParamRefs,
  *  as well as two kinds of AnnotatedTypes representing reach and maybe capabilities.
@@ -29,24 +30,31 @@ trait CaptureRef extends TypeProxy, ValueType:
     this.isTrackableRef && (isMaxCapability || !captureSetOfInfo.isAlwaysEmpty)
 
   /** Is this a reach reference of the form `x*`? */
-  final def isReach(using Context): Boolean = this match
+  final def isReach(using Context): Boolean = this.stripUse match
     case AnnotatedType(_, annot) => annot.symbol == defn.ReachCapabilityAnnot
     case _ => false
 
+  final def isUnderUse(using Context): Boolean = this match
+    case AnnotatedType(_, annot) => annot.symbol == defn.UseAnnot
+    case _ => false
+
+  def underUse(using Context): CaptureRef =
+    AnnotatedType(this, Annotation(defn.UseAnnot, util.Spans.NoSpan))
+
   /** Is this a maybe reference of the form `x?`? */
-  final def isMaybe(using Context): Boolean = this match
+  final def isMaybe(using Context): Boolean = this.stripUse match
     case AnnotatedType(_, annot) => annot.symbol == defn.MaybeCapabilityAnnot
     case _ => false
 
   final def stripReach(using Context): CaptureRef =
     if isReach then
-      val AnnotatedType(parent: CaptureRef, _) = this: @unchecked
+      val AnnotatedType(parent: CaptureRef, _) = this.stripUse: @unchecked
       parent
     else this
 
   final def stripMaybe(using Context): CaptureRef =
     if isMaybe then
-      val AnnotatedType(parent: CaptureRef, _) = this: @unchecked
+      val AnnotatedType(parent: CaptureRef, _) = this.stripUse: @unchecked
       parent
     else this
 
@@ -61,18 +69,19 @@ trait CaptureRef extends TypeProxy, ValueType:
     case tp: TermParamRef => tp.underlying.derivesFrom(defn.Caps_Exists)
     case _ => false
 
-  /** Normalize reference so that it can be compared with `eq` for equality */
-  final def normalizedRef(using Context): CaptureRef = this match
-    case tp @ AnnotatedType(parent: CaptureRef, annot) if tp.isTrackableRef =>
-      tp.derivedAnnotatedType(parent.normalizedRef, annot)
-    case tp: TermRef if tp.isTrackableRef =>
-      tp.symbol.termRef
-    case _ => this
+  // With the support of pathes, we don't need to normalize the `TermRef`s anymore.
+  // /** Normalize reference so that it can be compared with `eq` for equality */
+  // final def normalizedRef(using Context): CaptureRef = this match
+  //   case tp @ AnnotatedType(parent: CaptureRef, annot) if tp.isTrackableRef =>
+  //     tp.derivedAnnotatedType(parent.normalizedRef, annot)
+  //   case tp: TermRef if tp.isTrackableRef =>
+  //     tp.symbol.termRef
+  //   case _ => this
 
   /** The capture set consisting of exactly this reference */
   final def singletonCaptureSet(using Context): CaptureSet.Const =
     if mySingletonCaptureSet == null then
-      mySingletonCaptureSet = CaptureSet(this.normalizedRef)
+      mySingletonCaptureSet = CaptureSet(this)
     mySingletonCaptureSet.uncheckedNN
 
   /** The capture set of the type underlying this reference */
@@ -97,27 +106,45 @@ trait CaptureRef extends TypeProxy, ValueType:
    *   x subsumes y  ==>  x* subsumes y, x subsumes y?
    *   x subsumes y  ==>  x* subsumes y*, x? subsumes y?
    *   x: x1.type /\ x1 subsumes y  ==>  x subsumes y
+   *   TODO: Document path cases
    */
   final def subsumes(y: CaptureRef)(using Context): Boolean =
+
+    def subsumingRefs(x: Type, y: Type): Boolean = x match
+      case x: CaptureRef => y match
+        case y: CaptureRef => x.subsumes(y)
+        case _ => false
+      case _ => false
+
+    def viaInfo(info: Type)(test: Type => Boolean): Boolean = info.match
+      case info: SingletonCaptureRef => test(info)
+      case info: AndType => test(info.tp1) || test(info.tp2)
+      case info: OrType => test(info.tp1) && test(info.tp2)
+      case _ => false
+
     (this eq y)
     || this.isRootCapability
     || y.match
         case y: TermRef =>
-          (y.prefix eq this)
-          || y.info.match
-              case y1: SingletonCaptureRef => this.subsumes(y1)
+            y.prefix.match
+              case ypre: CaptureRef =>
+                this.subsumes(ypre)
+                || this.match
+                    case x @ TermRef(xpre: CaptureRef, _) if x.symbol == y.symbol =>
+                      subsumingRefs(xpre, ypre) && subsumingRefs(ypre, xpre)
+                    case _ =>
+                      false
               case _ => false
+          || viaInfo(y.info)(subsumingRefs(this, _))
         case MaybeCapability(y1) => this.stripMaybe.subsumes(y1)
         case _ => false
     || this.match
         case ReachCapability(x1) => x1.subsumes(y.stripReach)
-        case x: TermRef =>
-          x.info match
-            case x1: SingletonCaptureRef => x1.subsumes(y)
-            case _ => false
+        case x: TermRef => viaInfo(x.info)(subsumingRefs(_, y))
         case x: TermParamRef => subsumesExistentially(x, y)
         case x: TypeRef => assumedContainsOf(x).contains(y)
         case _ => false
+  end subsumes
 
   def assumedContainsOf(x: TypeRef)(using Context): SimpleIdentitySet[CaptureRef] =
     CaptureSet.assumedContains.getOrElse(x, SimpleIdentitySet.empty)
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index 44d5e2cf4b88..2b5df937484a 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -374,7 +374,7 @@ object CaptureSet:
 
   def apply(elems: CaptureRef*)(using Context): CaptureSet.Const =
     if elems.isEmpty then empty
-    else Const(SimpleIdentitySet(elems.map(_.normalizedRef.ensuring(_.isTrackableRef))*))
+    else Const(SimpleIdentitySet(elems.map(_.ensuring(_.isTrackableRef))*))
 
   def apply(elems: Refs)(using Context): CaptureSet.Const =
     if elems.isEmpty then empty else Const(elems)
@@ -508,7 +508,11 @@ object CaptureSet:
         !noUniversal
       else elem match
         case elem: TermRef if level.isDefined =>
-          elem.symbol.ccLevel <= level
+          elem.prefix match
+            case prefix: CaptureRef =>
+              levelOK(prefix)
+            case _ =>
+              elem.symbol.ccLevel <= level
         case elem: ThisType if level.isDefined =>
           elem.cls.ccLevel.nextInner <= level
         case ReachCapability(elem1) =>
@@ -1078,7 +1082,8 @@ object CaptureSet:
           empty
         case CapturingType(parent, refs) =>
           recur(parent) ++ refs
-        case tp @ AnnotatedType(parent, ann) if ann.hasSymbol(defn.ReachCapabilityAnnot) =>
+        case tp @ AnnotatedType(parent, ann)
+        if ann.hasSymbol(defn.ReachCapabilityAnnot) =>
           parent match
             case parent: SingletonCaptureRef if parent.isTrackableRef =>
               tp.singletonCaptureSet
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index b05ab8542137..dd128848532d 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -13,7 +13,7 @@ import Trees.*
 import typer.RefChecks.{checkAllOverrides, checkSelfAgainstParents, OverridingPairsChecker}
 import typer.Checking.{checkBounds, checkAppliedTypesIn}
 import typer.ErrorReporting.{Addenda, NothingToAdd, err}
-import typer.ProtoTypes.{AnySelectionProto, LhsProto}
+import typer.ProtoTypes.{LhsProto, WildcardSelectionProto}
 import util.{SimpleIdentitySet, EqHashMap, EqHashSet, SrcPos, Property}
 import transform.{Recheck, PreRecheck, CapturedVars}
 import Recheck.*
@@ -122,10 +122,6 @@ object CheckCaptures:
    *  This check is performed at Typer.
    */
   def checkWellformed(parent: Tree, ann: Tree)(using Context): Unit =
-    parent.tpe match
-      case _: SingletonType =>
-        report.error(em"Singleton type $parent cannot have capture set", parent.srcPos)
-      case _ =>
     def check(elem: Tree, pos: SrcPos): Unit = elem.tpe match
       case ref: CaptureRef =>
         if !ref.isTrackableRef then
@@ -187,6 +183,9 @@ object CheckCaptures:
   /** Attachment key for bodies of closures, provided they are values */
   val ClosureBodyValue = Property.Key[Unit]
 
+  /** A prototype that indicates selection with an immutable value */
+  class PathSelectionProto(val sym: Symbol, val pt: Type)(using Context) extends WildcardSelectionProto
+
 class CheckCaptures extends Recheck, SymTransformer:
   thisPhase =>
 
@@ -361,107 +360,103 @@ class CheckCaptures extends Recheck, SymTransformer:
      *  the environment in which `sym` is defined.
      */
     def markFree(sym: Symbol, pos: SrcPos)(using Context): Unit =
-      if sym.exists then
-        val ref = sym.termRef
-        if 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))
+      markFree(sym, sym.termRef, pos)
+
+    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))
 
     /** 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
      *  the environment's owner
      */
     def markFree(cs: CaptureSet, pos: SrcPos)(using Context): Unit =
+      // A captured reference with the symbol `sym` is visible from the environment
+      // if `sym` is not defined inside the owner of the environment.
+      inline def isVisibleFromEnv(sym: Symbol, env: Env) =
+        if env.kind == EnvKind.NestedInOwner then
+          !sym.isProperlyContainedIn(env.owner)
+        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 ref.info.hasAnnotation(defn.UseAnnot)|| c.isUnderUse 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 are exempted if
+                  //  - they are under-use capabilties that were generated from a cap
+                  //    appearing under a @use, or
+                  //  - their reference has a type thar carries a @use annotation. In that
+                  //    case callers will charge the deep capture set of the argument.
+                  val cs = CaptureSet.ofInfo(c)
+                  cs.disallowRootCapability: () =>
+                    def kind = if c.isReach then "reach capability" else "capture set variable"
+                    report.error(em"Local $kind $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 =>
-          // Whether a symbol is defined inside the owner of the environment?
-          inline def isContainedInEnv(sym: Symbol) =
-            if env.kind == EnvKind.NestedInOwner then
-              sym.isProperlyContainedIn(env.owner)
-            else
-              sym.isContainedIn(env.owner)
-          // A captured reference with the symbol `sym` is visible from the environment
-          // if `sym` is not defined inside the owner of the environment
-          inline def isVisibleFromEnv(sym: Symbol) = !isContainedInEnv(sym)
-          // 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)
-                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)
-              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}")
+          checkSubsetEnv(cs, env)
     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
+        includeCallCaptures(tree.symbol, tree.symbol.info, tree.srcPos)
+      else if !tree.symbol.isStatic then
         //debugShowEnvs()
-        markFree(tree.symbol, tree.srcPos)
+        def addSelects(ref: TermRef, pt: Type): TermRef = pt match
+          case pt: PathSelectionProto if ref.isTracked =>
+            // if `ref` is not tracked then the selection could not give anything new
+            // class SerializationProxy in stdlib-cc/../LazyListIterable.scala has an example where this matters.
+            addSelects(ref.select(pt.sym).asInstanceOf[TermRef], pt.pt)
+          case _ => ref
+        val ref = tree.symbol.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)
       super.recheckIdent(tree, pt)
 
+    override def selectionProto(tree: Select, pt: Type)(using Context): Type =
+      val sym = tree.symbol
+      if !sym.isOneOf(UnstableValueFlags) && !sym.isStatic then PathSelectionProto(sym, pt)
+      else super.selectionProto(tree, pt)
+
     /** A specialized implementation of the selection rule.
      *
      *  E |- f: T{ m: R^Cr }^{f}
@@ -488,21 +483,25 @@ class CheckCaptures extends Recheck, SymTransformer:
         case _ => denot
 
       val selType = recheckSelection(tree, qualType, name, disambiguate)
-      val selCs = selType.widen.captureSet
-      if selCs.isAlwaysEmpty
-          || selType.widen.isBoxedCapturing
+      val selWiden = selType.widen
+
+      if pt == LhsProto
           || qualType.isBoxedCapturing
-          || pt == LhsProto
+          || selType.isTrackableRef
+          || selWiden.isBoxedCapturing
+          || selWiden.captureSet.isAlwaysEmpty
       then
         selType
       else
         val qualCs = qualType.captureSet
-        capt.println(i"pick one of $qualType, ${selType.widen}, $qualCs, $selCs in $tree")
+        val selCs = selType.captureSet
+        capt.println(i"pick one of $qualType, ${selType.widen}, $qualCs, $selCs ${selWiden.captureSet} in $tree")
+
         if qualCs.mightSubcapture(selCs)
             && !selCs.mightSubcapture(qualCs)
             && !pt.stripCapturing.isInstanceOf[SingletonType]
         then
-          selType.widen.stripCapturing.capturing(qualCs)
+          selWiden.stripCapturing.capturing(qualCs)
             .showing(i"alternate type for select $tree: $selType --> $result, $qualCs / $selCs", capt)
         else
           selType
@@ -542,17 +541,51 @@ 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)
+      accountForUses(arg, argType, formal)
       argType
 
+    /** At given variance, map occurrences of `T @use` to `caps.$use[T]`.
+     *  @param deep   If true also map result types of functions
+     */
+    class MapUses(deep: Boolean, atVariance: Int)(using Context) extends TypeMap:
+      var usesFound = false
+      def apply(t: Type) = t match
+        case t @ AnnotatedType(parent, ann) =>
+          if ann.symbol == defn.UseAnnot && variance == atVariance then
+            usesFound = true
+            defn.Caps_Use.typeRef.appliedTo(apply(parent))
+          else
+            t.derivedAnnotatedType(this(parent), ann)
+        case Existential(_, _) if !deep =>
+          t
+        case _ =>
+          mapOver(t)
+
+    /** If `formal` contains `@use` occurrences charge the deep capture set
+     *  of the corresponding `argType` parts to the enclosing environments.
+     */
+    def accountForUses(arg: Tree, argType: Type, formal: Type)(using Context): Unit =
+      val mapper = MapUses(deep = false, atVariance = 1)
+      val formal1 = mapper(formal)
+      if mapper.usesFound then
+        def useHandler(tpUnderUse: Type, other: Type, fromBelow: Boolean)(cmp: () => Boolean): Boolean =
+          if fromBelow then
+            val dcs = other.deepCaptureSet
+            capt.println(i"actual uses for $arg: $argType vs $formal = $dcs")
+            markFree(dcs, arg.srcPos)
+          cmp()
+        CCState.withUseHandler(useHandler):
+          checkConformsExpr(argType, formal1, arg, NothingToAdd)
+    end accountForUses
+
     /** A specialized implementation of the apply rule.
      *
      *  E |- q: Tq^Cq
@@ -561,15 +594,10 @@ class CheckCaptures extends Recheck, SymTransformer:
      *  ---------------------
      *  E |- f(a): Tr^C
      *
-     *  If the function `f` does not have an `@unboxed` 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
-     *  unbox reach capabilities over its formal parameter. Therefore, the approximation
-     *  would be `Cq \union dcs(Ca)` instead.
+     *  If the type of the function `f` does not mention any formal parameters
+     *  any capabilities of the result of the application must already be present in
+     *  the application. So an upper approximation of the result capture set is Cq \union Ca,
+     *  where `Ca` is the capture set of the argument.
      *  If the approximation is known to subcapture the declared result Cr, we pick it for C
      *  otherwise we pick Cr.
      */
@@ -577,11 +605,7 @@ class CheckCaptures extends Recheck, SymTransformer:
     def recheckApplication(tree: Apply, qualType: Type, funType: MethodType, argTypes: List[Type])(using Context): Type =
       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
+      val argCaptures = argTypes.map(_.captureSet)
       appType match
         case appType @ CapturingType(appType1, refs)
         if qualType.exists
@@ -676,8 +700,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
@@ -1061,7 +1087,7 @@ class CheckCaptures extends Recheck, SymTransformer:
 
       if actualBoxed eq actual then
         // Only `addOuterRefs` when there is no box adaptation
-        expected1 = addOuterRefs(expected1, actual)
+        expected1 = addOuterRefs(expected1, actual, tree.srcPos)
       if isCompatible(actualBoxed, expected1) then
         if debugSuccesses then tree match
             case Ident(_) =>
@@ -1102,8 +1128,12 @@ class CheckCaptures extends Recheck, SymTransformer:
      *     that are outside `Cls`. These are all accessed through `Cls.this`,
      *     so we can assume they are already accounted for by `Ce` and adding
      *     them explicitly to `Ce` changes nothing.
+     *   - To make up for this, we also add these variables to the capture set of `Cls`,
+     *     so that all instances of `Cls` will capture these outer references.
+     *  So in a sense we use `{Cls.this}` as a placeholder for certain outer captures.
+     *  that we needed to be subsumed by `Cls.this`.
      */
-    private def addOuterRefs(expected: Type, actual: Type)(using Context): Type =
+    private def addOuterRefs(expected: Type, actual: Type, pos: SrcPos)(using Context): Type =
 
       def isPure(info: Type): Boolean = info match
         case info: PolyType => isPure(info.resType)
@@ -1116,16 +1146,40 @@ class CheckCaptures extends Recheck, SymTransformer:
         else isPure(owner.info) && isPureContext(owner.owner, limit)
 
       // Augment expeced capture set `erefs` by all references in actual capture
-      // set `arefs` that are outside some `this.type` reference in `erefs`
+      // set `arefs` that are outside some `C.this.type` reference in `erefs` for an enclosing
+      // class `C`. If an added reference is not a ThisType itself, add it to the capture set
+      // (i.e. use set) of the `C`. This makes sure that any outer reference implicitly subsumed
+      // by `C.this` becomes a capture reference of every instance of `C`.
       def augment(erefs: CaptureSet, arefs: CaptureSet): CaptureSet =
         (erefs /: erefs.elems): (erefs, eref) =>
           eref match
             case eref: ThisType if isPureContext(ctx.owner, eref.cls) =>
-              erefs ++ arefs.filter {
-                case aref: TermRef => eref.cls.isProperlyContainedIn(aref.symbol.owner)
+
+              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)
+
+              // 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]
+                    // 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.
+                then
+                  def provenance =
+                    i""" of the enclosing class ${eref.cls}.
+                       |The reference was included since we tried to establish that $arefs <: $erefs"""
+                  checkElem(outerRef, capturedVars(eref.cls), pos, provenance)
+
+              erefs ++ outerRefs
             case _ =>
               erefs
 
@@ -1305,18 +1359,23 @@ class CheckCaptures extends Recheck, SymTransformer:
     */
     def checkOverrides = new TreeTraverser:
       class OverridingPairsCheckerCC(clazz: ClassSymbol, self: Type, srcPos: SrcPos)(using Context) extends OverridingPairsChecker(clazz, self):
-        /** Check subtype with box adaptation.
-        *  This function is passed to RefChecks to check the compatibility of overriding pairs.
-        *  @param sym  symbol of the field definition that is being checked
-        */
+        /** Check subtype with box adaptation and @use checking.
+         *  This function is passed to RefChecks to check the compatibility of overriding pairs.
+         *  @param sym  symbol of the field definition that is being checked
+         *  @use checking: Overrides must have fewer @uses than overridden members.
+         *  I.e. every @use in an parameter of an overriding method must correspond
+         *  to an enclosing @use in the parameter of the overridden method.
+         */
         override def checkSubType(actual: Type, expected: Type)(using Context): Boolean =
-          val expected1 = alignDependentFunction(addOuterRefs(expected, actual), actual.stripCapturing)
+          val mapUses = MapUses(deep = true, atVariance = -1)
+          val expected1 = alignDependentFunction(
+            addOuterRefs(mapUses(expected), actual, srcPos), actual.stripCapturing)
           val actual1 =
             val saved = curEnv
             try
               curEnv = Env(clazz, EnvKind.NestedInOwner, capturedVars(clazz), outer0 = curEnv)
               val adapted =
-                adaptBoxed(actual, expected1, srcPos, covariant = true, alwaysConst = true, null)
+                adaptBoxed(mapUses(actual), expected1, srcPos, covariant = true, alwaysConst = true, null)
               actual match
                 case _: MethodType =>
                   // We remove the capture set resulted from box adaptation for method types,
@@ -1326,27 +1385,22 @@ class CheckCaptures extends Recheck, SymTransformer:
                   adapted.stripCapturing
                 case _ => adapted
             finally curEnv = saved
-          actual1 frozen_<:< expected1
+
+          def lowerUseSeen: UseHandler = (tpUnderUse, other, fromBelow) => cmp =>
+            cmp()
+          def noLowerUseSeen: UseHandler = (tpUnderUse, other, fromBelow) => cmp =>
+            if fromBelow
+            then false // found a @use in overriding that is not covered by an enclosing @use in overridden
+            else CCState.withUseHandler(lowerUseSeen)(cmp())
+          CCState.withUseHandler(noLowerUseSeen):
+            TypeComparer.usingContravarianceForMethods:
+              actual1 frozen_<:< expected1
+        end checkSubType
 
         override def needsCheck(overriding: Symbol, overridden: Symbol)(using Context): Boolean =
           !setup.isPreCC(overriding) && !setup.isPreCC(overridden)
 
         override def checkInheritedTraitParameters: Boolean = false
-
-        /** Check that overrides don't change the @unbox 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
-              report.error(
-                OverrideError(
-                    i"has a parameter ${param1.name} with different @unbox 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
-              )
       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 22e7899eeea1..967ff9e827d9 100644
--- a/compiler/src/dotty/tools/dotc/cc/Setup.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -212,8 +212,8 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
 
       def apply(tp: Type) =
         val tp1 = tp match
-          case AnnotatedType(parent, annot) if annot.symbol.isRetains =>
-            // Drop explicit retains annotations
+          case AnnotatedType(parent, annot) if annot.symbol.isRetains || annot.symbol == defn.UseAnnot =>
+            // Drop inferred retains and @use annotations
             apply(parent)
           case tp @ AppliedType(tycon, args) =>
             val tycon1 = this(tycon)
@@ -518,6 +518,11 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
           info match
             case mt: MethodOrPoly =>
               val psyms = psymss.head
+              // TODO: the substitution does not work for param-dependent method types.
+              // For example, `(x: T, y: x.f.type) => Unit`. In this case, when we
+              // 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.
               mt.companion(mt.paramNames)(
                 mt1 =>
                   if !paramSignatureChanges && !mt.isParamDependent && prevLambdas.isEmpty then
diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala
index f95bb3cea351..af91e2296304 100644
--- a/compiler/src/dotty/tools/dotc/core/Definitions.scala
+++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala
@@ -1004,6 +1004,7 @@ class Definitions {
     @tu lazy val Caps_unsafeBoxFunArg: Symbol = CapsUnsafeModule.requiredMethod("unsafeBoxFunArg")
     @tu lazy val Caps_ContainsTrait: TypeSymbol = CapsModule.requiredType("Contains")
     @tu lazy val Caps_containsImpl: TermSymbol = CapsModule.requiredMethod("containsImpl")
+    @tu lazy val Caps_Use: TypeSymbol = CapsModule.requiredType("$use")
 
   /** The same as CaptureSet.universal but generated implicitly for references of Capability subtypes */
   @tu lazy val universalCSImpliedByCapability = CaptureSet(captureRoot.termRef)
@@ -1057,12 +1058,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")
@@ -1352,6 +1353,9 @@ class Definitions {
   final def isNamedTuple_From(sym: Symbol)(using Context): Boolean =
     sym.name == tpnme.From && sym.owner == NamedTupleModule.moduleClass
 
+  final def isUse(sym: Symbol)(using Context): Boolean =
+    sym.name == tpnme.USE && sym.owner == CapsModule.moduleClass
+
   private val compiletimePackageAnyTypes: Set[Name] = Set(
     tpnme.Equals, tpnme.NotEquals, tpnme.IsConst, tpnme.ToString
   )
@@ -1380,7 +1384,7 @@ class Definitions {
     tpnme.Plus, tpnme.Length, tpnme.Substring, tpnme.Matches, tpnme.CharAt
   )
   private val compiletimePackageOpTypes: Set[Name] =
-    Set(tpnme.S, tpnme.From)
+    Set(tpnme.S, tpnme.From, tpnme.USE)
     ++ compiletimePackageAnyTypes
     ++ compiletimePackageIntTypes
     ++ compiletimePackageLongTypes
@@ -1394,6 +1398,7 @@ class Definitions {
     && (
          isCompiletime_S(sym)
       || isNamedTuple_From(sym)
+      || isUse(sym)
       || sym.owner == CompiletimeOpsAnyModuleClass && compiletimePackageAnyTypes.contains(sym.name)
       || sym.owner == CompiletimeOpsIntModuleClass && compiletimePackageIntTypes.contains(sym.name)
       || sym.owner == CompiletimeOpsLongModuleClass && compiletimePackageLongTypes.contains(sym.name)
diff --git a/compiler/src/dotty/tools/dotc/core/StdNames.scala b/compiler/src/dotty/tools/dotc/core/StdNames.scala
index d3e198a7e7a7..e30cabcc9f4b 100644
--- a/compiler/src/dotty/tools/dotc/core/StdNames.scala
+++ b/compiler/src/dotty/tools/dotc/core/StdNames.scala
@@ -194,6 +194,7 @@ object StdNames {
     final val WILDCARD_STAR: N                  = "_*"
     final val REIFY_TREECREATOR_PREFIX: N       = "$treecreator"
     final val REIFY_TYPECREATOR_PREFIX: N       = "$typecreator"
+    final val USE: N                            = "$use"
 
     final val Any: N                 = "Any"
     final val AnyKind: N             = "AnyKind"
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 8fc6307c426c..9b161b2be661 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -51,6 +51,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
     assocExistentials = Nil
     recCount = 0
     needsGc = false
+    useContravariance = false
     if Config.checkTypeComparerReset then checkReset()
 
   private var pendingSubTypes: util.MutableSet[(Type, Type)] | Null = null
@@ -79,6 +80,12 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
    */
   private var assocExistentials: ExAssoc = Nil
 
+  /** Whether method type parameters should be compared contra-variantly.
+   *  This is usually false, but set to true for comparisons of methods in
+   *  refinements and for override checks in capture checking.
+   */
+  private var useContravariance = false
+
   private var myInstance: TypeComparer = this
   def currentInstance: TypeComparer = myInstance
 
@@ -667,7 +674,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
                 info1.paramNames.hasSameLengthAs(info2.paramNames)
                 && isSubInfo(info1.resultType, info2.resultType.subst(info2, info1))
               case (info1: MethodType, info2: MethodType) =>
-                matchingMethodParams(info1, info2, precise = false)
+                usingContravarianceForMethods(matchingMethodParams(info1, info2))
                 && isSubInfo(info1.resultType, info2.resultType.subst(info2, info1))
               case (info1 @ CapturingType(parent1, refs1), info2: Type)
               if info2.stripCapturing.isInstanceOf[MethodOrPoly] =>
@@ -812,10 +819,10 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
       case tp2: MethodType =>
         def compareMethod = tp1 match {
           case tp1: MethodType =>
-            (tp1.signature consistentParams tp2.signature) &&
-            matchingMethodParams(tp1, tp2) &&
-            (!tp2.isImplicitMethod || tp1.isImplicitMethod) &&
-            isSubType(tp1.resultType, tp2.resultType.subst(tp2, tp1))
+            (useContravariance || tp1.signature.consistentParams(tp2.signature))
+            && matchingMethodParams(tp1, tp2)
+            && (!tp2.isImplicitMethod || tp1.isImplicitMethod)
+            && isSubType(tp1.resultType, tp2.resultType.subst(tp2, tp1))
           case _ => false
         }
         compareMethod
@@ -823,7 +830,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
         def comparePoly = tp1 match {
           case tp1: PolyType =>
             comparingTypeLambdas(tp1, tp2) {
-              (tp1.signature consistentParams tp2.signature)
+              (useContravariance || (tp1.signature consistentParams tp2.signature))
               && matchingPolyParams(tp1, tp2)
               && isSubType(tp1.resultType, tp2.resultType.subst(tp2, tp1))
             }
@@ -1527,13 +1534,16 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
      *  with `other` via ">:>" if fromBelow is true, "<:<" otherwise.
      *  Delegates to compareS if `tycon` is scala.compiletime.S. Otherwise, constant folds if possible.
      */
-    def compareCompiletimeAppliedType(tp: AppliedType, other: Type, fromBelow: Boolean): Boolean = {
-      if (defn.isCompiletime_S(tp.tycon.typeSymbol)) compareS(tp, other, fromBelow)
-      else {
+    def compareCompiletimeAppliedType(tp: AppliedType, other: Type, fromBelow: Boolean): Boolean =
+      val tycon = tp.tycon.typeSymbol
+      if defn.isCompiletime_S(tycon) then
+        compareS(tp, other, fromBelow)
+      else if defn.isUse(tycon) then
+        CCState.underUse(tp.args.head, other, fromBelow):
+          if fromBelow then recur(other, tp.args.head) else recur(tp.args.head, other)
+      else
         val folded = tp.tryCompiletimeConstantFold
         if (fromBelow) recur(other, folded) else recur(folded, other)
-      }
-    }
 
     /** Like tp1 <:< tp2, but returns false immediately if we know that
      *  the case was covered previously during subtyping.
@@ -2154,7 +2164,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
             info1 match
               case info1: MethodType =>
                 val symInfo1 = symInfo.stripPoly
-                matchingMethodParams(info1, info2, precise = false)
+                usingContravarianceForMethods(matchingMethodParams(info1, info2))
                 && isSubInfo(info1.resultType, info2.resultType.subst(info2, info1), symInfo1.resultType)
                 && sigsOK(symInfo1, info2)
               case _ => inFrozenGadtIf(tp1IsSingleton) { isSubType(info1, info2) }
@@ -2277,18 +2287,18 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
   }
 
   /** Do the parameter types of `tp1` and `tp2` match in a way that allows `tp1`
-   *  to override `tp2` ? Two modes: precise or not.
-   *  If `precise` is set (which is the default) this is the case if they're pairwise `=:=`.
-   *  Otherwise parameters in `tp2` must be subtypes of corresponding parameters in `tp1`.
+   *  to override `tp2` ? Two modes, dependenging on `useContravariance`.
+   *  If `useContravariance` is off (which is the default) this is the case if they're pairwise `=:=`.
+   *  If `useContravariance` is on, parameters in `tp2` must be subtypes of corresponding parameters in `tp1`.
    */
-  def matchingMethodParams(tp1: MethodType, tp2: MethodType, precise: Boolean = true): Boolean = {
+  def matchingMethodParams(tp1: MethodType, tp2: MethodType): Boolean = {
     def loop(formals1: List[Type], formals2: List[Type]): Boolean = formals1 match {
       case formal1 :: rest1 =>
         formals2 match {
           case formal2 :: rest2 =>
             val formal2a = if (tp2.isParamDependent) formal2.subst(tp2, tp1) else formal2
             val paramsMatch =
-              if precise then
+              if !useContravariance then
                 isSameTypeWhenFrozen(formal1, formal2a)
               else if isCaptureCheckingOrSetup then
                 // allow to constrain capture set variables
@@ -2907,6 +2917,11 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
     (tp1.isBoxedCapturing == tp2.isBoxedCapturing)
     || refs1.subCaptures(CaptureSet.empty, frozenConstraint).isOK
 
+  protected def usingContravarianceForMethods[T](op: => T)(using Context) =
+    val saved = useContravariance
+    useContravariance = true
+    try op finally useContravariance = saved
+
   // ----------- Diagnostics --------------------------------------------------
 
   /** A hook for showing subtype traces. Overridden in ExplainingTypeComparer */
@@ -3452,6 +3467,9 @@ object TypeComparer {
 
   def subsumesExistentially(tp1: TermParamRef, tp2: CaptureRef)(using Context) =
     comparing(_.subsumesExistentially(tp1, tp2))
+
+  def usingContravarianceForMethods[T](op: => T)(using Context) =
+    comparing(_.usingContravarianceForMethods(op))
 }
 
 object MatchReducer:
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index aba8c3bb31fd..60bac8221e1d 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -1796,7 +1796,7 @@ object Types extends TypeUtils {
 
     /** Is this either not a method at all, or a parameterless method? */
     final def isParameterless(using Context): Boolean = stripPoly match {
-      case mt: MethodType => false
+      case mt: MethodOrPoly => false
       case _ => true
     }
 
diff --git a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
index 8a173faa3cec..cd481dba14ef 100644
--- a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
+++ b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
@@ -1548,21 +1548,23 @@ object Parsers {
       case _ => None
     }
 
-    /** CaptureRef  ::=  ident [`*` | `^`] | `this`
+    /** CaptureRef  ::=  (ident | `this`) [`*` | `^`]
      */
     def captureRef(): Tree =
-      if in.token == THIS then simpleRef()
-      else
-        val id = termIdent()
-        if isIdent(nme.raw.STAR) then
-          in.nextToken()
-          atSpan(startOffset(id)):
-            PostfixOp(id, Ident(nme.CC_REACH))
-        else if isIdent(nme.UPARROW) then
-          in.nextToken()
-          atSpan(startOffset(id)):
-            makeCapsOf(cpy.Ident(id)(id.name.toTypeName))
-        else id
+      val ref = singleton()
+      if isIdent(nme.raw.STAR) then
+        in.nextToken()
+        atSpan(startOffset(ref)):
+          PostfixOp(ref, Ident(nme.CC_REACH))
+      else if isIdent(nme.UPARROW) then
+        in.nextToken()
+        def toTypeSel(r: Tree): Tree = r match
+          case id: Ident => cpy.Ident(id)(id.name.toTypeName)
+          case Select(qual, id) => Select(qual, id.toTypeName)
+          case _ => r
+        atSpan(startOffset(ref)):
+          makeCapsOf(toTypeSel(ref))
+      else ref
 
     /**  CaptureSet ::=  `{` CaptureRef {`,` CaptureRef} `}`    -- under captureChecking
      */
@@ -1825,7 +1827,7 @@ object Parsers {
       if in.token == LPAREN then funParamClause() :: funParamClauses() else Nil
 
     /** InfixType ::= RefinedType {id [nl] RefinedType}
-     *             |  RefinedType `^`   // under capture checking
+     *             |  RefinedType `^` {Annotation}  // under capture checking
      */
     def infixType(): Tree = infixTypeRest(refinedType())
 
@@ -1836,7 +1838,7 @@ object Parsers {
                      && !(isIdent(nme.as) && in.featureEnabled(Feature.modularity))
                      && nextCanFollowOperator(canStartInfixTypeTokens))
 
-    /** RefinedType   ::=  WithType {[nl] Refinement} [`^` CaptureSet]
+    /** RefinedType   ::=  WithType {[nl] Refinement} [`^` CaptureSet {Annotation}]
      */
     val refinedTypeFn: Location => Tree = _ => refinedType()
 
@@ -1865,9 +1867,10 @@ object Parsers {
       else if Feature.ccEnabled && in.isIdent(nme.UPARROW) && isCaptureUpArrow then
         atSpan(t.span.start):
           in.nextToken()
-          if in.token == LBRACE
-          then makeRetaining(t, captureSet(), tpnme.retains)
-          else makeRetaining(t, Nil, tpnme.retainsCap)
+          annotTypeRest:
+            if in.token == LBRACE
+            then makeRetaining(t, captureSet(), tpnme.retains)
+            else makeRetaining(t, Nil, tpnme.retainsCap)
       else
         t
     }
diff --git a/compiler/src/dotty/tools/dotc/parsing/Tokens.scala b/compiler/src/dotty/tools/dotc/parsing/Tokens.scala
index b0a533b2f1df..a7f44fc8370e 100644
--- a/compiler/src/dotty/tools/dotc/parsing/Tokens.scala
+++ b/compiler/src/dotty/tools/dotc/parsing/Tokens.scala
@@ -232,7 +232,7 @@ object Tokens extends TokensCommon {
   final val canStartExprTokens2: TokenSet = canStartExprTokens3 | BitSet(DO)
 
   final val canStartInfixTypeTokens: TokenSet = literalTokens | identifierTokens | BitSet(
-    THIS, SUPER, USCORE, LPAREN, LBRACE, AT)
+    THIS, SUPER, USCORE, LPAREN, LBRACE)
 
   final val canStartTypeTokens: TokenSet = canStartInfixTypeTokens | BitSet(LBRACE)
 
diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
index b5ed3bdb4fa7..0c8358e07cfa 100644
--- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
@@ -15,7 +15,7 @@ import util.SourcePosition
 import scala.util.control.NonFatal
 import scala.annotation.switch
 import config.{Config, Feature}
-import cc.{CapturingType, RetainingType, CaptureSet, ReachCapability, MaybeCapability, isBoxed, retainedElems, isRetainsLike}
+import cc.*
 
 class PlainPrinter(_ctx: Context) extends Printer {
 
@@ -417,7 +417,8 @@ class PlainPrinter(_ctx: Context) extends Printer {
       case tp: TermRef if tp.symbol == defn.captureRoot => Str("cap")
       case tp: SingletonType => toTextRef(tp)
       case tp: (TypeRef | TypeParamRef) => toText(tp) ~ "^"
-      case ReachCapability(tp1) => toTextCaptureRef(tp1) ~ "*"
+      case ReachCapability(tp1) =>
+        toTextCaptureRef(tp1) ~ "*" ~ Str("@use").provided(tp.isUnderUse)
       case MaybeCapability(tp1) => toTextCaptureRef(tp1) ~ "?"
       case tp => toText(tp)
 
diff --git a/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala b/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala
index ea729e9549d5..f753088d67b0 100644
--- a/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala
@@ -27,7 +27,7 @@ import config.{Config, Feature}
 
 import dotty.tools.dotc.util.SourcePosition
 import dotty.tools.dotc.ast.untpd.{MemberDef, Modifiers, PackageDef, RefTree, Template, TypeDef, ValOrDefDef}
-import cc.{CaptureSet, CapturingType, toCaptureSet, IllegalCaptureRef, isRetains, ReachCapability, MaybeCapability}
+import cc.*
 import dotty.tools.dotc.parsing.JavaParsers
 
 class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
diff --git a/compiler/src/dotty/tools/dotc/transform/Recheck.scala b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
index 03f0001110d3..26a75215bab1 100644
--- a/compiler/src/dotty/tools/dotc/transform/Recheck.scala
+++ b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
@@ -12,7 +12,7 @@ import DenotTransformers.{DenotTransformer, IdentityDenotTransformer, SymTransfo
 import NamerOps.linkConstructorParams
 import NullOpsDecorator.stripNull
 import typer.ErrorReporting.err
-import typer.ProtoTypes.*
+import typer.ProtoTypes.{AnySelectionProto, LhsProto}
 import typer.TypeAssigner.seqLitType
 import typer.ConstFold
 import typer.ErrorReporting.{Addenda, NothingToAdd}
@@ -203,13 +203,12 @@ abstract class Recheck extends Phase, SymTransformer:
       tree.tpe
 
     def recheckSelect(tree: Select, pt: Type)(using Context): Type =
-      recheckSelection(tree, recheckSelectQualifier(tree), tree.name, pt)
+      recheckSelection(tree,
+        recheck(tree.qualifier, selectionProto(tree, pt)).widenIfUnstable,
+        tree.name, pt)
 
-    def recheckSelectQualifier(tree: Select)(using Context): Type =
-      val proto =
-        if tree.symbol == defn.Any_asInstanceOf then WildcardType
-        else AnySelectionProto
-      recheck(tree.qualifier, proto).widenIfUnstable
+    def selectionProto(tree: Select, pt: Type)(using Context): Type =
+      if tree.symbol == defn.Any_asInstanceOf then WildcardType else AnySelectionProto
 
     def recheckSelection(tree: Select, qualType: Type, name: Name,
         sharpen: Denotation => Denotation)(using Context): Type =
@@ -308,7 +307,7 @@ abstract class Recheck extends Phase, SymTransformer:
     def recheckApply(tree: Apply, pt: Type)(using Context): Type =
       val (funtpe0, qualType) = tree.fun match
         case fun: Select =>
-          val qualType = recheckSelectQualifier(fun)
+          val qualType = recheck(fun.qualifier, selectionProto(fun, WildcardType)).widenIfUnstable
           (recheckSelection(fun, qualType, fun.name, WildcardType), qualType)
         case _ =>
           (recheck(tree.fun), NoType)
diff --git a/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala b/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala
index a69a63d1ceef..53e0b456ed9a 100644
--- a/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala
+++ b/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala
@@ -324,6 +324,8 @@ object ProtoTypes {
       case tp: UnapplyFunProto => new UnapplySelectionProto(name, nameSpan)
       case tp => SelectionProto(name, IgnoredProto(tp), typer, privateOK = true, nameSpan)
 
+  class WildcardSelectionProto extends SelectionProto(nme.WILDCARD, WildcardType, NoViewsAllowed, true, NoSpan)
+
   /** A prototype for expressions [] that are in some unspecified selection operation
    *
    *    [].?: ?
@@ -332,9 +334,9 @@ object ProtoTypes {
    *  operation is further selection. In this case, the expression need not be a value.
    *  @see checkValue
    */
-  @sharable object AnySelectionProto extends SelectionProto(nme.WILDCARD, WildcardType, NoViewsAllowed, true, NoSpan)
+  @sharable object AnySelectionProto extends WildcardSelectionProto
 
-  @sharable object SingletonTypeProto extends SelectionProto(nme.WILDCARD, WildcardType, NoViewsAllowed, true, NoSpan)
+  @sharable object SingletonTypeProto extends WildcardSelectionProto
 
   /** A prototype for selections in pattern constructors */
   class UnapplySelectionProto(name: Name, nameSpan: Span) extends SelectionProto(name, WildcardType, NoViewsAllowed, true, nameSpan)
diff --git a/library/src/scala/caps.scala b/library/src/scala/caps.scala
index 9911ef920116..83dc3ae16423 100644
--- a/library/src/scala/caps.scala
+++ b/library/src/scala/caps.scala
@@ -55,7 +55,9 @@ 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
+
+  type $use[+T]
 
   object unsafe:
 
diff --git a/scala2-library-cc/src/scala/collection/View.scala b/scala2-library-cc/src/scala/collection/View.scala
index 31c544a46beb..132934dbe3bd 100644
--- a/scala2-library-cc/src/scala/collection/View.scala
+++ b/scala2-library-cc/src/scala/collection/View.scala
@@ -150,7 +150,10 @@ object View extends IterableFactory[View] {
   object Filter {
     def apply[A](underlying: Iterable[A]^, p: A => Boolean, isFlipped: Boolean): Filter[A]^{underlying, p} =
       underlying match {
-        case filter: Filter[A] if filter.isFlipped == isFlipped => new Filter(filter.underlying, a => filter.p(a) && p(a), isFlipped)
+        case filter: Filter[A] if filter.isFlipped == isFlipped =>
+          new Filter(filter.underlying, a => filter.p(a) && p(a), isFlipped)
+            .asInstanceOf[Filter[A]^{underlying, p}]
+              // !!! asInstanceOf needed once paths were added, see path-patmat-should-be-pos.scala for minimization
         case _ => new Filter(underlying, p, isFlipped)
       }
   }
diff --git a/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala b/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala
index 2f7b017a6729..28ce8da104aa 100644
--- a/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala
+++ b/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala
@@ -1366,7 +1366,9 @@ object LazyListIterable extends IterableFactory[LazyListIterable] {
         case SerializeEnd => initRead = true
         case a => init += a.asInstanceOf[A]
       }
-      val tail = in.readObject().asInstanceOf[LazyListIterable[A]]
+      val tail: LazyListIterable[A] = in.readObject().asInstanceOf[LazyListIterable[A]]
+        // Explicit type annotation needed so that tail.state below is dropped from capture set.
+        // Before paths were added, it was tail that was added, and the `asSeenFrom` to a pure type made it work.
       // scala/scala#10118: caution that no code path can evaluate `tail.state`
       // before the resulting LazyListIterable is returned
       val it = init.toList.iterator
diff --git a/tests/neg-custom-args/captures/class-contra.check b/tests/neg-custom-args/captures/class-contra.check
index 9fc009ac3d48..808118bd1795 100644
--- a/tests/neg-custom-args/captures/class-contra.check
+++ b/tests/neg-custom-args/captures/class-contra.check
@@ -1,10 +1,7 @@
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/class-contra.scala:12:39 ---------------------------------
-12 |  def fun(x: K{val f: T^{a}}) = x.setf(a) // error
-   |                                       ^
-   |   Found:    (a : T^{x, y})
-   |   Required: T^{}
-   |
-   |   Note that a capability (K.this.f : T^) in a capture set appearing in contravariant position
-   |   was mapped to (x.f : T^{a}) which is not a capability. Therefore, it was under-approximated to the empty set.
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/class-contra.scala:12:40 ---------------------------------
+12 |  def fun1(k: K{val f: T^{a}}) = k.setf(a) // error
+   |                                        ^
+   |                                        Found:    (a : T^{x, y})
+   |                                        Required: T^{k.f}
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/class-contra.scala b/tests/neg-custom-args/captures/class-contra.scala
index 210fd4e331f1..8ef8e7485a18 100644
--- a/tests/neg-custom-args/captures/class-contra.scala
+++ b/tests/neg-custom-args/captures/class-contra.scala
@@ -9,5 +9,6 @@ class T
 
 def test(x: Cap, y: Cap) =
   val a: T^{x, y} = ???
-  def fun(x: K{val f: T^{a}}) = x.setf(a) // error
+  def fun1(k: K{val f: T^{a}}) = k.setf(a) // error
+  def fun2(k: K{val f: a.type}) = k.setf(a)
   ()
\ No newline at end of file
diff --git a/tests/neg-custom-args/captures/explain-under-approx.check b/tests/neg-custom-args/captures/explain-under-approx.check
index 2d2b05b4b95a..c186fc6adb11 100644
--- a/tests/neg-custom-args/captures/explain-under-approx.check
+++ b/tests/neg-custom-args/captures/explain-under-approx.check
@@ -1,20 +1,14 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/explain-under-approx.scala:12:10 -------------------------
 12 |  col.add(Future(() => 25)) // error
    |          ^^^^^^^^^^^^^^^^
-   |       Found:    Future[Int]{val a: (async : Async^)}^{async}
-   |       Required: Future[Int]^{}
-   |
-   |       Note that a capability Collector.this.futs* in a capture set appearing in contravariant position
-   |       was mapped to col.futs* which is not a capability. Therefore, it was under-approximated to the empty set.
+   |          Found:    Future[Int]{val a: (async : Async^)}^{async}
+   |          Required: Future[Int]^{col.futs*}
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/explain-under-approx.scala:15:11 -------------------------
 15 |  col1.add(Future(() => 25)) // error
    |           ^^^^^^^^^^^^^^^^
-   |      Found:    Future[Int]{val a: (async : Async^)}^{async}
-   |      Required: Future[Int]^{}
-   |
-   |      Note that a capability Collector.this.futs* in a capture set appearing in contravariant position
-   |      was mapped to col1.futs* which is not a capability. Therefore, it was under-approximated to the empty set.
+   |           Found:    Future[Int]{val a: (async : Async^)}^{async}
+   |           Required: Future[Int]^{col1.futs*}
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/filevar-multi-ios.scala b/tests/neg-custom-args/captures/filevar-multi-ios.scala
new file mode 100644
index 000000000000..8ffc8d8e299c
--- /dev/null
+++ b/tests/neg-custom-args/captures/filevar-multi-ios.scala
@@ -0,0 +1,41 @@
+import language.experimental.modularity
+import compiletime.uninitialized
+
+class IO extends caps.Capability
+
+class File:
+  def write(x: String): Unit = ???
+
+object test1:
+
+  class Service(val io: IO, val io2: IO):
+    var file: File^{io} = uninitialized
+    var file2: File^{io2} = uninitialized
+    def log = file.write("log")
+
+  def withFile[T](io: IO)(op: File^{io} => T): T =
+    op(new File)
+
+  def test(io3: IO, io4: IO) =
+    withFile(io3): f =>
+      val o = Service(io3, io4)
+      o.file = f // error
+      o.file2 = f // error
+      o.log
+
+object test2:
+
+  class Service(tracked val io: IO, tracked val io2: IO):
+    var file: File^{io} = uninitialized
+    var file2: File^{io2} = uninitialized
+    def log = file.write("log")
+
+  def withFile[T](io: IO)(op: File^{io} => T): T =
+    op(new File)
+
+  def test(io3: IO, io4: IO) =
+    withFile(io3): f =>
+      val o = Service(io3, io4)
+      o.file = f
+      o.file2 = f // error
+      o.log
diff --git a/tests/neg-custom-args/captures/i15116.check b/tests/neg-custom-args/captures/i15116.check
index df05324866e1..0a16af9f6704 100644
--- a/tests/neg-custom-args/captures/i15116.check
+++ b/tests/neg-custom-args/captures/i15116.check
@@ -18,13 +18,17 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15116.scala:5:13 ----------------------------------------
 5 |  val x = Foo(m)   // error
   |          ^^^^^^
-  |          Found:    Foo{val m: String^{Baz.this}}^{Baz.this}
+  |          Found:    Foo{val m²: (Baz.this.m : String^)}^{Baz.this.m}
   |          Required: Foo
   |
+  |          where:    m  is a value in trait Baz
+  |                    m² is a value in class Foo
+  |
+  |
   |          Note that the expected type Foo
   |          is the previously inferred type of value x
   |          which is also the type seen in separately compiled sources.
-  |          The new inferred type Foo{val m: String^{Baz.this}}^{Baz.this}
+  |          The new inferred type Foo{val m: (Baz.this.m : String^)}^{Baz.this.m}
   |          must conform to this type.
   |
   | longer explanation available when compiling with `-explain`
@@ -48,13 +52,17 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15116.scala:9:13 ----------------------------------------
 9 |  val x = Foo(m)   // error
   |          ^^^^^^
-  |          Found:    Foo{val m: String^{Baz2.this}}^{Baz2.this}
+  |          Found:    Foo{val m²: (Baz2.this.m : String^)}^{Baz2.this.m}
   |          Required: Foo
   |
+  |          where:    m  is a value in trait Baz2
+  |                    m² is a value in class Foo
+  |
+  |
   |          Note that the expected type Foo
   |          is the previously inferred type of value x
   |          which is also the type seen in separately compiled sources.
-  |          The new inferred type Foo{val m: String^{Baz2.this}}^{Baz2.this}
+  |          The new inferred type Foo{val m: (Baz2.this.m : String^)}^{Baz2.this.m}
   |          must conform to this type.
   |
   | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/i15749a.scala b/tests/neg-custom-args/captures/i15749a.scala
index 57fca27fae66..a620bd1d7c0c 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](mx: Wrapper[Unit ->{cap} A] @use): 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/i21347.check b/tests/neg-custom-args/captures/i21347.check
index c680a54d3efc..0d9ed6993d3e 100644
--- a/tests/neg-custom-args/captures/i21347.check
+++ b/tests/neg-custom-args/captures/i21347.check
@@ -1,7 +1,7 @@
 -- 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
+  |               Local capture set variable C leaks into capture scope of method runOps
 5 |    op()
 -- Error: tests/neg-custom-args/captures/i21347.scala:8:14 -------------------------------------------------------------
 8 |  () => runOps(f :: Nil) // error
diff --git a/tests/neg-custom-args/captures/i21614.check b/tests/neg-custom-args/captures/i21614.check
index 14b468db4c8e..af6ddee624b6 100644
--- a/tests/neg-custom-args/captures/i21614.check
+++ b/tests/neg-custom-args/captures/i21614.check
@@ -8,7 +8,7 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:12:12 ---------------------------------------
 12 |  files.map(new Logger(_)) // error, Q: can we improve the error message?
    |            ^^^^^^^^^^^^^
-   |            Found:    Logger{val f: (_$1 : File^{files*})}^
+   |            Found:    Logger{val f: (_$1 : File^{files*@use})}^
    |            Required: Logger{val f: File^?}^?
    |
    |            Note that the universal capability `cap`
diff --git a/tests/neg-custom-args/captures/i21614.scala b/tests/neg-custom-args/captures/i21614.scala
index a5ed25d818a5..333c9368629e 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^](files: List[F @use]): 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(files: List[File^ @use]): 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..7c1b6e31d60c 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](sources: Seq[Source[T]^ @caps.use]): 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/outerRefsUses.scala b/tests/neg-custom-args/captures/outerRefsUses.scala
new file mode 100644
index 000000000000..cd03c8c41efd
--- /dev/null
+++ b/tests/neg-custom-args/captures/outerRefsUses.scala
@@ -0,0 +1,10 @@
+class IO
+def test(io: IO^) =
+  class C:
+    def foo() = () =>
+      val x: IO^{this} = io
+      ()
+  val c = new C
+  val _: C^{io} = c // ok
+  val _: C = c // error
+  ()
diff --git a/tests/neg-custom-args/captures/path-box.scala b/tests/neg-custom-args/captures/path-box.scala
new file mode 100644
index 000000000000..3213c236aaf5
--- /dev/null
+++ b/tests/neg-custom-args/captures/path-box.scala
@@ -0,0 +1,20 @@
+class A:
+  val m: A^ = ???
+  val self: this.type = this
+
+case class Box[+T](value: T)
+
+def testBox1(a: A^): Box[A^{a}] =
+  Box(a.m)
+
+def testBox2(a: A^): Box[A^{a.m}] =
+  Box(a.m)
+
+def testBox3(a: A^): Box[A^{a.m}] =
+  Box(a) // error
+
+def testBox4(a: A^): Box[A^{a.m}] =
+  Box(a.m.m.m)
+
+def testBox5(a: A^): Box[A^{a.m}] =
+  Box(a.m.m.self)
\ No newline at end of file
diff --git a/tests/neg-custom-args/captures/path-connection.scala b/tests/neg-custom-args/captures/path-connection.scala
new file mode 100644
index 000000000000..c65aa75b1ed2
--- /dev/null
+++ b/tests/neg-custom-args/captures/path-connection.scala
@@ -0,0 +1,48 @@
+import language.experimental.modularity
+
+trait Reader:
+  def read(): String
+
+trait Sender:
+  def send(msg: String): Unit
+
+class Connection extends Reader, Sender:
+  def read() = "hello"
+  def send(msg: String) = ()
+
+  val readOnly: Reader^ = new Reader:
+    def read() = Connection.this.read()
+
+class ReaderProxy(tracked val r: Reader^) extends Reader:
+  def read() = "(Proxy)" + r.read()
+
+class SenderProxy(tracked val s: Sender^) extends Sender:
+  def send(msg: String) = s.send("(Proxy) " + msg)
+
+// TODO: We have to put `c` in the different argument list to make it work.
+// See the comments in `integrateRT`.
+def testConnection(c: Connection^)(
+    handle1: Reader^{c.readOnly} => String,
+    handle2: Sender^{c} => Unit,
+    handle3: Reader^{c} => String,
+    ) =
+  val m1 = c.read()
+  c.send("hello")
+
+  val m2 = c.readOnly.read()
+
+  val m3a = handle1(c.readOnly)
+  val m3b = handle3(c.readOnly)
+
+  val m4a = handle1(c) // error
+  val m4b = handle3(c)
+
+  val m5a = handle1(new ReaderProxy(c.readOnly))
+  val m5b = handle3(new ReaderProxy(c.readOnly))
+
+  val m6a = handle1(new ReaderProxy(c)) // error
+  val m6b = handle3(new ReaderProxy(c))
+
+  handle2(c)
+
+  handle2(new SenderProxy(c))
\ No newline at end of file
diff --git a/tests/neg-custom-args/captures/path-illigal.scala b/tests/neg-custom-args/captures/path-illigal.scala
new file mode 100644
index 000000000000..f09db0087ef7
--- /dev/null
+++ b/tests/neg-custom-args/captures/path-illigal.scala
@@ -0,0 +1,7 @@
+class A:
+  val m: A^ = ???
+  var n: A^ = ???
+
+def test1(a: A^) =
+  val c1: A^{a.m} = a.m
+  val f1: A^{a.n} = a.n // error
\ No newline at end of file
diff --git a/tests/neg-custom-args/captures/path-patmat-should-be-pos.scala b/tests/neg-custom-args/captures/path-patmat-should-be-pos.scala
new file mode 100644
index 000000000000..aca6102204a3
--- /dev/null
+++ b/tests/neg-custom-args/captures/path-patmat-should-be-pos.scala
@@ -0,0 +1,26 @@
+class It[A]
+
+class Filter[A](val underlying: It[A]^, val p: A => Boolean) extends It[A]
+object Filter:
+  def apply[A](underlying: It[A]^, p: A => Boolean): Filter[A]^{underlying, p} =
+    underlying match
+      case filter: Filter[A]^ =>
+        val x = new Filter(filter.underlying, a => filter.p(a) && p(a))
+        x: Filter[A]^{underlying, p} // error
+          // !!! should work, it seems to be the case that the system does not recognize that
+          // underlying and filter are aliases.
+
+    // On the other hand, the following works:
+    locally:
+      val filter: underlying.type & Filter[A] = ???
+      val a: It[A]^{filter.underlying} = ???
+      val b: It[A]^{underlying} = a
+      val x = new Filter(filter.underlying, a => filter.p(a) && p(a))
+      x: Filter[A]^{underlying, p}
+
+    locally:
+      val filter: underlying.type & Filter[A]^ = ???
+      val a: It[A]^{filter.underlying} = ???
+      val b: It[A]^{underlying} = a
+      val x = new Filter(filter.underlying, a => filter.p(a) && p(a))
+      x: Filter[A]^{underlying, p}
diff --git a/tests/neg-custom-args/captures/path-simple.scala b/tests/neg-custom-args/captures/path-simple.scala
new file mode 100644
index 000000000000..93b6dacebe74
--- /dev/null
+++ b/tests/neg-custom-args/captures/path-simple.scala
@@ -0,0 +1,27 @@
+
+class A:
+  val m: A^ = ???
+  val self: this.type = this
+
+case class C(ca: A^)
+
+def test1(a: A^, b: A^) =
+  val c1: A^{a} = a.m
+  val c2: A^{a.m} = a.m
+  val c3: A^{b} = a.m // error
+
+  val d1: A^{a} = a.self
+  val d2: A^{a.self} = a.self
+  val d3: A^{a.self} = a
+
+  val e1: A^{a.m} = a.self.m
+  val e2: A^{a.self.m} = a.self.m
+  val e3: A^{a.self.m} = a.m
+
+def test2(a: A^) =
+  val b: a.type = a
+  val c1: C^{a} = new C(a)
+  val c2: C^{a} = new C(a.m)
+  val c3: C^{a.m} = new C(a.m)
+  val c4: C^{b} = new C(a)
+  val c5: C^{a} = new C(b)
\ No newline at end of file
diff --git a/tests/neg-custom-args/captures/reaches.scala b/tests/neg-custom-args/captures/reaches.scala
index c33ba80a668b..3ddddcc35e9b 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(xs: List[Proc] @use): 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(xs: List[Proc] @use): Unit =
   val cur = Ref[List[() ->{xs*} Unit]](xs)  // OK, by revised VAR
   while cur.get.nonEmpty do
     val next: () ->{xs*} Unit = cur.get.head
@@ -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](ps: List[(A => A, A => A)] @use): List[A ->{ps*} A] =
   ps.map((x, y) => compose1(x, y))
diff --git a/tests/neg-custom-args/captures/singletons.scala b/tests/neg-custom-args/captures/singletons.scala
index 194e6e850dcd..be0ee67ab1bc 100644
--- a/tests/neg-custom-args/captures/singletons.scala
+++ b/tests/neg-custom-args/captures/singletons.scala
@@ -1,6 +1,6 @@
 val x = () => ()
 
-val y1: x.type = x          // ok
-val y2: x.type^{} = x       // error: singleton type cannot have capture set
-val y3: x.type^{x} = x      // error: singleton type cannot have capture set // error
-val y4: x.type^ = x         // error: singleton type cannot have capture set
+val y1: x.type = x
+val y2: x.type^{} = x
+val y3: x.type^{x} = x // error
+val y4: x.type^ = x
diff --git a/tests/neg-custom-args/captures/spread-problem.scala b/tests/neg-custom-args/captures/spread-problem.scala
index 579c7817b9c1..92b1cb86c99d 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](sources: (Source[T]^ @caps.use)*): 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..20b3a05e25d0 100644
--- a/tests/neg-custom-args/captures/unbox-overrides.check
+++ b/tests/neg-custom-args/captures/unbox-overrides.check
@@ -1,21 +1,42 @@
--- [E164] Declaration Error: tests/neg-custom-args/captures/unbox-overrides.scala:8:6 ----------------------------------
-8 |  def foo(x: C): C        // error
-  |      ^
-  |error overriding method foo in trait A of type (x: C): C;
-  |  method foo of type (x: C): C has a parameter x with different @unbox 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(x: C @use): 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
+  |      error overriding method bar in trait A of type (x: C): C;
+  |        method bar of type (x: C @use): C has incompatible type
   |
   | 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
+-- [E164] Declaration Error: tests/neg-custom-args/captures/unbox-overrides.scala:16:6 ---------------------------------
+16 |  def foo(x: C @use): C // error
+   |      ^
+   |      error overriding method foo in trait B2 of type (x: C): C;
+   |        method foo of type (x: C @use): C has incompatible type
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E164] Declaration Error: tests/neg-custom-args/captures/unbox-overrides.scala:19:15 --------------------------------
+19 |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
+   |               error overriding method bar in trait A of type (x: C): C;
+   |                 method bar in trait B2 of type (x: C @use): C has incompatible type
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E164] Declaration Error: tests/neg-custom-args/captures/unbox-overrides.scala:26:6 ---------------------------------
+26 |  def foo[T](a: Int)(x: C @use): C // error
+   |      ^
+   |      error overriding method foo in trait Poly of type [T](a: Int)(x: C): C;
+   |        method foo of type [T](a: Int)(x: C @use): C has incompatible type
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E164] Declaration Error: tests/neg-custom-args/captures/unbox-overrides.scala:35:6 ---------------------------------
+35 |  def foo(x: (List[C], List[C]) @use): Unit  // error
+   |      ^
+   |      error overriding method foo in trait D1 of type (x: (List[C @use], List[C])): Unit;
+   |        method foo of type (x: (List[C], List[C]) @use): Unit has incompatible type
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E164] Declaration Error: tests/neg-custom-args/captures/unbox-overrides.scala:36:6 ---------------------------------
+36 |  def bar(x: (List[C], List[C]) @use): Unit  // error
+   |      ^
+   |      error overriding method bar in trait D1 of type (x: (List[C @use], List[C @use])): Unit;
+   |        method bar of type (x: (List[C], List[C]) @use): Unit has incompatible type
    |
    | 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..f18d71c24722 100644
--- a/tests/neg-custom-args/captures/unbox-overrides.scala
+++ b/tests/neg-custom-args/captures/unbox-overrides.scala
@@ -1,15 +1,48 @@
-import caps.unbox
+import caps.use
 
 trait A[X]:
-  def foo(@unbox x: X): X
+  def foo(x: X @use): 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 foo(x: C): C        // ok
+  def bar(x: C @use): C // error
 
 trait B2:
   def foo(x: C): C
-  def bar(@unbox x: C): C
+  def bar(x: C @use): C
+
+trait B3 extends B2:
+  def foo(x: C @use): C // error
+  def bar(x: C): C // ok
 
 abstract class C extends A[C], B2 // error
+
+trait Poly:
+  def foo[T](a: Int)(x: C): C
+  def bar[T](a: Int)(x: C @use): C
+
+trait Poly1 extends Poly:
+  def foo[T](a: Int)(x: C @use): C // error
+  def bar[T](a: Int)(x: C): C // ok
+
+trait D1:
+  def foo(x: (List[C @use], List[C])): Unit
+  def bar(x: (List[C @use], List[C @use])): Unit
+  def baz(x: (List[C], List[C]) @use): Unit
+
+trait D2 extends D1:
+  def foo(x: (List[C], List[C]) @use): Unit  // error
+  def bar(x: (List[C], List[C]) @use): Unit  // error
+  def baz(x: (List[C] @use, List[C] @use)): Unit  // ok
+
+trait E2:
+  def foo(x: (List[C], List[C]) @use): Unit
+  def bar(x: (List[C], List[C]) @use): Unit
+  def baz(x: (List[C] @use, List[C] @use)): Unit
+
+trait E3 extends E2:
+  def foo(x: (List[C] @use, List[C])): Unit  // ok
+  def bar(x: (List[C], List[C])): Unit  // ok
+  def baz(x: (List[C] @use, List[C] @use)): Unit  // ok
+
diff --git a/tests/neg-custom-args/captures/useAnnot.check b/tests/neg-custom-args/captures/useAnnot.check
new file mode 100644
index 000000000000..271a776e091a
--- /dev/null
+++ b/tests/neg-custom-args/captures/useAnnot.check
@@ -0,0 +1,4 @@
+-- Error: tests/neg-custom-args/captures/useAnnot.scala:13:26 ----------------------------------------------------------
+13 |  val _ = () => println(f(ioProcs))  // error
+   |                          ^^^^^^^
+   |                          Local reach capability ioProcs* leaks into capture scope of method Test2
diff --git a/tests/neg-custom-args/captures/useAnnot.scala b/tests/neg-custom-args/captures/useAnnot.scala
new file mode 100644
index 000000000000..deb0839bdbd3
--- /dev/null
+++ b/tests/neg-custom-args/captures/useAnnot.scala
@@ -0,0 +1,16 @@
+import caps.use
+
+type Proc = () => Unit
+
+def f(xs: List[Proc] @use) = ???
+def g(xs: List[Proc]) = ???
+
+def Test(ioProcs: List[Proc @use]) =
+  val ff = () => println(f(ioProcs))  // ok
+  ()
+
+def Test2(ioProcs: List[Proc]) =
+  val _ = () => println(f(ioProcs))  // error
+  val gg = () => println(g(ioProcs))  // ok
+  ()
+
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/i20503.scala b/tests/neg/i20503.scala
index 3fb0573f6c2f..562aea94e0f6 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(ops: List[(() => Unit) @use]): 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..f03a6b16ab10 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,20 +9,21 @@ def usingAsync[X](op: Async^ => X): X = ???
 
 case class Box[+T](get: T)
 
-def useBoxedAsync(@unbox x: Box[Async^]): Unit =
+def useBoxedAsync(x: Box[Async^ @use]): Unit =
   val t0 = x
   val t1 = t0.get // ok
   t1.read()
 
-def useBoxedAsync1(@unbox x: Box[Async^]): Unit = x.get.read() // ok
+def useBoxedAsync1(x: Box[Async^ @use]): Unit = x.get.read() // ok
 
 def test(): Unit =
 
   val f: Box[Async^] => Unit = (x:  Box[Async^]) => useBoxedAsync(x) // error
   val _: Box[Async^] => Unit = useBoxedAsync(_) // error
   val _: Box[Async^] => Unit = useBoxedAsync // error
-  val _ = useBoxedAsync(_) // error
-  val _ = useBoxedAsync // error
+  val _ = (x:  Box[Async^]) => useBoxedAsync(x) // error
+  val _ = useBoxedAsync(_) // was error, now OK since @use is inferred
+  val _ = useBoxedAsync // was error, now OK since @use is inferred
 
   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..a5f4bd6657e3 100644
--- a/tests/pos-custom-args/captures/Buffer.scala
+++ b/tests/pos-custom-args/captures/Buffer.scala
@@ -8,10 +8,8 @@ trait Buffer[A]:
   def flatMapInPlace(f: A => IterableOnce[A]^): this.type = {
     val g = f
     val s = 10
-     // capture checking: we need the copy since we box/unbox on g* on the next line
+      // 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
-      // since `^ appears in a function result, not under a box.
     val newElems = new Array[(IterableOnce[A]^{f})](s)
     var i = 0
     while i < s do
diff --git a/tests/pos-custom-args/captures/curried-uses.scala b/tests/pos-custom-args/captures/curried-uses.scala
new file mode 100644
index 000000000000..3e2b5378f845
--- /dev/null
+++ b/tests/pos-custom-args/captures/curried-uses.scala
@@ -0,0 +1,9 @@
+
+def test() =
+  val f: () => () => Unit = ???
+  val x = () =>
+    val z1: () => Unit = f()
+    val z2 = z1()
+    z2
+  val _: () ->{f} Unit = x
+  ()
diff --git a/tests/pos-custom-args/captures/dep-reach.scala b/tests/pos-custom-args/captures/dep-reach.scala
index c81197aa738d..b84ed2113b26 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(xs: Proc @use *): () ->{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(xs: Seq[(() => Unit) @use]): () ->{xs*} Unit =
       xs.head
 
     val a: () ->{c} Unit = () => ()
diff --git a/tests/pos-custom-args/captures/filevar-expanded.scala b/tests/pos-custom-args/captures/filevar-expanded.scala
index a883471e8d2e..58e7a0e67e0a 100644
--- a/tests/pos-custom-args/captures/filevar-expanded.scala
+++ b/tests/pos-custom-args/captures/filevar-expanded.scala
@@ -1,4 +1,5 @@
 import language.experimental.captureChecking
+import language.experimental.modularity
 import compiletime.uninitialized
 
 object test1:
@@ -22,7 +23,7 @@ object test2:
   class File:
     def write(x: String): Unit = ???
 
-  class Service(io: IO^):
+  class Service(tracked val io: IO^):
     var file: File^{io} = uninitialized
     def log = file.write("log")
 
diff --git a/tests/pos-custom-args/captures/filevar.scala b/tests/pos-custom-args/captures/filevar.scala
index 9ab34fe617b5..dc8d0b18908b 100644
--- a/tests/pos-custom-args/captures/filevar.scala
+++ b/tests/pos-custom-args/captures/filevar.scala
@@ -1,4 +1,5 @@
 import language.experimental.captureChecking
+import language.experimental.modularity
 import compiletime.uninitialized
 
 object test1:
@@ -22,7 +23,7 @@ object test2:
   class File:
     def write(x: String): Unit = ???
 
-  class Service(io: IO):
+  class Service(tracked val io: IO):
     var file: File^{io} = uninitialized
     def log = file.write("log")
 
diff --git a/tests/pos-custom-args/captures/path-use.scala b/tests/pos-custom-args/captures/path-use.scala
new file mode 100644
index 000000000000..5eb2b60fd218
--- /dev/null
+++ b/tests/pos-custom-args/captures/path-use.scala
@@ -0,0 +1,19 @@
+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)
+  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..8e21a1f2edd6 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(xs: List[Proc] @use): 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
deleted file mode 100644
index 2412e5b388ca..000000000000
--- a/tests/pos/Buffer.scala
+++ /dev/null
@@ -1,22 +0,0 @@
-import language.experimental.captureChecking
-
-// Extract of the problem in collection.mutable.Buffers
-trait Buffer[A]:
-
-  def apply(i: Int): A = ???
-
-  def flatMapInPlace(f: A => IterableOnce[A]^): this.type = {
-    val g = f
-    val s = 10
-     // capture checking: we need the copy since we box/unbox on g* on the next line
-      // TODO: This looks fishy, need to investigate
-      // Alternative would be to mark `f` as @unbox. It's not inferred
-      // since `^ appears in a function result, not under a box.
-    val newElems = new Array[(IterableOnce[A]^{f})](s)
-    var i = 0
-    while i < s do
-      val x = g(this(i))
-      newElems(i) = x
-      i += 1
-    this
-  }
\ No newline at end of file
diff --git a/tests/pos/cc-poly-source-capability.scala b/tests/pos/cc-poly-source-capability.scala
index 3b6c0bde1398..0ecea7a7932f 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, others: List[Async @use]) =
     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..aa516afea910 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(lbls: List[Label^ @use]) =
     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..45a6a8234737 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](fs: Seq[Future[T]^ @use])
   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..2cf9368a3176 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(cs: List[Cap^] @use): 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..19e3165efbf9 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(lbls: List[Label] @use) =
     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..a2388837d923 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](items: Seq[T^ @use]): T^{items*} =
     val bx = Box(items)
     bx.getOne
 /*