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..db17022efe92 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
@@ -194,7 +194,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 =>
@@ -639,8 +640,8 @@ object CapsOfApply:
 class AnnotatedCapability(annot: Context ?=> ClassSymbol):
   def apply(tp: Type)(using Context) =
     AnnotatedType(tp, Annotation(annot, util.Spans.NoSpan))
-  def unapply(tree: AnnotatedType)(using Context): Option[SingletonCaptureRef] = tree match
-    case AnnotatedType(parent: SingletonCaptureRef, ann) if ann.symbol == annot => Some(parent)
+  def unapply(tree: AnnotatedType)(using Context): Option[CaptureRef] = tree match
+    case AnnotatedType(parent: CaptureRef, ann) if ann.symbol == annot => Some(parent)
     case _ => None
 
 /** An extractor for `ref @annotation.internal.reachCapability`, which is used to express
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
index f00c6869cd80..bbaf0c7d2fa0 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
@@ -61,18 +61,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 +98,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..81b4287961ba 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) =>
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index b05ab8542137..738150691807 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,57 +360,67 @@ 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 refSym.hasAnnotation(defn.UnboxAnnot) then
+                  capt.println(i"exempt: $ref in $refOwner")
+                else
+                  // Reach capabilities that go out of scope have to be approximated
+                  // by their underlying capture set, which cannot be universal.
+                  // Reach capabilities of @unboxed parameters are exempted.
+                  val cs = CaptureSet.ofInfo(c)
+                  cs.disallowRootCapability: () =>
+                    report.error(em"Local reach capability $c leaks into capture scope of ${env.ownerString}", pos)
+                  checkSubset(cs, env.captured, pos, provenance(env))
+              isVisible
+            case ref: ThisType => isVisibleFromEnv(ref.cls, env)
+            case _ => false
+        checkSubset(included, env.captured, pos, provenance(env))
+        capt.println(i"Include call or box capture $included from $cs in ${env.owner} --> ${env.captured}")
+
       if !cs.isAlwaysEmpty then
         forallOuterEnvsUpTo(ctx.owner.topLevelClass): env =>
-          // 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 */
@@ -457,11 +466,26 @@ class CheckCaptures extends Recheck, SymTransformer:
         if tree.symbol.info.isParameterless then
           // there won't be an apply; need to include call captures now
           includeCallCaptures(tree.symbol, tree.srcPos)
-      else
+      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 +512,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
@@ -553,7 +581,8 @@ class CheckCaptures extends Recheck, SymTransformer:
         markFree(argType.deepCaptureSet, arg.srcPos)
       argType
 
-    /** A specialized implementation of the apply rule.
+    /** CURRENTLY DISABLED:
+     *  A specialized implementation of the apply rule.
      *
      *  E |- q: Tq^Cq
      *  E |- q.f: Ta^Ca ->Cf Tr^Cr
@@ -576,6 +605,7 @@ class CheckCaptures extends Recheck, SymTransformer:
     protected override
     def recheckApplication(tree: Apply, qualType: Type, funType: MethodType, argTypes: List[Type])(using Context): Type =
       val appType = Existential.toCap(super.recheckApplication(tree, qualType, funType, argTypes))
+      return appType
       val qualCaptures = qualType.captureSet
       val argCaptures =
         for (arg, argType) <- tree.args.lazyZip(argTypes) yield
@@ -1061,7 +1091,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 +1132,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 +1150,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
 
@@ -1310,7 +1368,7 @@ class CheckCaptures extends Recheck, SymTransformer:
         *  @param sym  symbol of the field definition that is being checked
         */
         override def checkSubType(actual: Type, expected: Type)(using Context): Boolean =
-          val expected1 = alignDependentFunction(addOuterRefs(expected, actual), actual.stripCapturing)
+          val expected1 = alignDependentFunction(addOuterRefs(expected, actual, srcPos), actual.stripCapturing)
           val actual1 =
             val saved = curEnv
             try
diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala
index 22e7899eeea1..76ae41649517 100644
--- a/compiler/src/dotty/tools/dotc/cc/Setup.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -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/parsing/Parsers.scala b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
index 8a173faa3cec..96f09a0d6214 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
      */
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/scala2-library-cc/src/scala/collection/Iterator.scala b/scala2-library-cc/src/scala/collection/Iterator.scala
index 4d1b0ed4ff95..368f13fb4b76 100644
--- a/scala2-library-cc/src/scala/collection/Iterator.scala
+++ b/scala2-library-cc/src/scala/collection/Iterator.scala
@@ -588,6 +588,8 @@ trait Iterator[+A] extends IterableOnce[A] with IterableOnceOps[A, Iterator, Ite
     def next() = f(self.next())
   }
 
+  // CC TODO This is unsafe. We will need to use a capture set variable:
+  //    def flatMap[B][C^](f: A => IterableOnce[B]^{C^}): Iterator[B]^{this, f, C^}
   def flatMap[B](f: A => IterableOnce[B]^): Iterator[B]^{this, f} = new AbstractIterator[B] {
     private[this] var cur: Iterator[B]^{f} = Iterator.empty
     /** Trillium logic boolean: -1 = unknown, 0 = false, 1 = true */
@@ -595,7 +597,7 @@ trait Iterator[+A] extends IterableOnce[A] with IterableOnceOps[A, Iterator, Ite
 
     private[this] def nextCur(): Unit = {
       cur = null
-      cur = f(self.next()).iterator
+      cur = f(self.next()).iterator.asInstanceOf // CC cast needed once apply special handling is dropped
       _hasNext = -1
     }
 
@@ -1215,7 +1217,7 @@ object Iterator extends IterableFactory[Iterator] {
   }
 
   private[this] final class ConcatIteratorCell[A](head: => IterableOnce[A]^, var tail: ConcatIteratorCell[A]) {
-    def headIterator: Iterator[A]^{this} = head.iterator // CC todo: can't use {head} as capture set, gives "cannot establish a reference"
+    def headIterator: Iterator[A]^{this.head*} = head.iterator // CC todo: can't use {head} as capture set, gives "cannot establish a reference"
   }
 
   /** Creates a delegating iterator capped by a limit count. Negative limit means unbounded.
diff --git a/scala2-library-cc/src/scala/collection/View.scala b/scala2-library-cc/src/scala/collection/View.scala
index 31c544a46beb..3545a3e1b72b 100644
--- a/scala2-library-cc/src/scala/collection/View.scala
+++ b/scala2-library-cc/src/scala/collection/View.scala
@@ -57,7 +57,7 @@ object View extends IterableFactory[View] {
     * @tparam A View element type
     */
   def fromIteratorProvider[A](it: () => Iterator[A]^): View[A]^{it} = new AbstractView[A] {
-    def iterator: Iterator[A]^{it} = it()
+    def iterator: Iterator[A]^{it} = it().asInstanceOf // CC TODO asInstanceOf needed once we drop special handling of apply
   }
 
   /**
@@ -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..2291a4d89eb3 100644
--- a/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala
+++ b/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala
@@ -1041,7 +1041,7 @@ object LazyListIterable extends IterableFactory[LazyListIterable] {
       var itHasNext       = false
       var rest            = restRef           // var rest = restRef.elem
       while (!itHasNext && !rest.isEmpty) {
-        it        = f(rest.head).iterator
+        it        = f(rest.head).iterator.asInstanceOf // CC TODO asInstanceOf needed once we drop special handling of apply
         itHasNext = it.hasNext
         if (!itHasNext) {                     // wait to advance `rest` because `it.next()` can throw
           rest    = rest.tail
@@ -1155,7 +1155,7 @@ object LazyListIterable extends IterableFactory[LazyListIterable] {
   /** Creates a State from an Iterator, with another State appended after the Iterator
     * is empty.
     */
-  private def stateFromIteratorConcatSuffix[A](it: Iterator[A]^)(suffix: => State[A]^): State[A]^{it, suffix} =
+  private def stateFromIteratorConcatSuffix[A, C^](it: Iterator[A]^)(suffix: => State[A]^{C^}): State[A]^{it, suffix, C^} =
     if (it.hasNext) sCons(it.next(), newLL(stateFromIteratorConcatSuffix(it)(suffix)))
     else suffix
 
@@ -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/scala2-library-cc/src/scala/collection/mutable/Buffer.scala b/scala2-library-cc/src/scala/collection/mutable/Buffer.scala
index 27e5a8997d48..591583ae90d4 100644
--- a/scala2-library-cc/src/scala/collection/mutable/Buffer.scala
+++ b/scala2-library-cc/src/scala/collection/mutable/Buffer.scala
@@ -184,7 +184,9 @@ trait IndexedBuffer[A] extends IndexedSeq[A]
     var i = 0
     val s = size
     val newElems = new Array[(IterableOnce[A]^{f})](s)
-    while (i < s) { newElems(i) = f(this(i)); i += 1 }
+    while i < s do
+      newElems(i) = f(this(i)).asInstanceOf // CC TODO asInstanceOf needed once we drop special handling of apply
+      i += 1
     clear()
     i = 0
     while (i < s) { ++=(newElems(i)); i += 1 }
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/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/inner-classes.scala b/tests/neg-custom-args/captures/inner-classes.scala
index fd500e607970..0f509faa3e31 100644
--- a/tests/neg-custom-args/captures/inner-classes.scala
+++ b/tests/neg-custom-args/captures/inner-classes.scala
@@ -19,7 +19,7 @@ object test:
     final class LazyCons[+T](val x: T, val xs: () => LazyList[T]^) extends LazyList[T]: // error
       def isEmpty = false
       def head = x
-      def tail: LazyList[T]^{this} = xs()
+      def tail: LazyList[T]^{this} = xs().asInstanceOf
     end LazyCons
 
     new LazyCons(1, () => LazyNil)
diff --git a/tests/neg-custom-args/captures/lazylist.check b/tests/neg-custom-args/captures/lazylist.check
index f0fbd1a025b5..5853c0bad1c2 100644
--- a/tests/neg-custom-args/captures/lazylist.check
+++ b/tests/neg-custom-args/captures/lazylist.check
@@ -1,7 +1,7 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylist.scala:17:15 -------------------------------------
 17 |  def tail = xs() // error
    |             ^^^^
-   |             Found:    lazylists.LazyList[T]^{LazyCons.this.xs}
+   |             Found:    lazylists.LazyList[T]^{LazyCons.this.xs*}
    |             Required: lazylists.LazyList[T]
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/leaking-iterators.scala b/tests/neg-custom-args/captures/leaking-iterators.scala
index ad5958e91e5b..40c551cc075e 100644
--- a/tests/neg-custom-args/captures/leaking-iterators.scala
+++ b/tests/neg-custom-args/captures/leaking-iterators.scala
@@ -36,8 +36,8 @@ trait Iterator[+A] extends IterableOnce[A]:
   def ++[B >: A](xs: IterableOnce[B]^): Iterator[B]^{this, xs}
 end Iterator
 
-private final class ConcatIteratorCell[A](head: => IterableOnce[A]^):
-  def headIterator: Iterator[A]^{this} = head.iterator
+private final class ConcatIteratorCell[A, C^](head: => IterableOnce[A]^{C^}):
+  def headIterator: Iterator[A]^{this, C^} = head.iterator
 
 def usingLogFile[R](op: FileOutputStream^ => R): R =
   val logFile = FileOutputStream("log")
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.check b/tests/neg-custom-args/captures/reaches.check
index f00fea09ed8c..62ebeeb529a2 100644
--- a/tests/neg-custom-args/captures/reaches.check
+++ b/tests/neg-custom-args/captures/reaches.check
@@ -32,7 +32,7 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:62:27 --------------------------------------
 62 |    val f1: File^{id*} = id(f) // error, since now id(f): File^
    |                         ^^^^^
-   |                         Found:    File^{f}
+   |                         Found:    File^
    |                         Required: File^{id*}
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/refine-withFile.scala b/tests/neg-custom-args/captures/refine-withFile.scala
index 823b62711d05..6cb1431f79d6 100644
--- a/tests/neg-custom-args/captures/refine-withFile.scala
+++ b/tests/neg-custom-args/captures/refine-withFile.scala
@@ -5,4 +5,4 @@ val useFile: [R] -> (path: String) -> (op: File^ -> R) -> R = ???
 def main(): Unit =
   val f: [R] -> (path: String) -> (op: File^ -> R) -> R = useFile
   val g: [R] -> (path: String) -> (op: File^{f*} -> R) -> R = f  // error
-  val leaked = g[File^{f*}]("test")(f => f)  // boom
+  val leaked = g[File^{f*}]("test")(f => f)  // error
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/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/i19470.check b/tests/neg/i19470.check
index fdb336bef7e5..ed9d795b0957 100644
--- a/tests/neg/i19470.check
+++ b/tests/neg/i19470.check
@@ -1,7 +1,7 @@
 -- [E007] Type Mismatch Error: tests/neg/i19470.scala:9:12 -------------------------------------------------------------
 9 |    List(foo(f())) // error
   |         ^^^^^^^^
-  |         Found:    Inv[box IO^{f?}]
+  |         Found:    Inv[box IO^{f*?}]
   |         Required: box Inv[box IO^?]^?
   |
   | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/lazylists-exceptions.check b/tests/pending/neg-customargs/captures/lazylists-exceptions.check
similarity index 100%
rename from tests/neg-custom-args/captures/lazylists-exceptions.check
rename to tests/pending/neg-customargs/captures/lazylists-exceptions.check
diff --git a/tests/neg-custom-args/captures/lazylists-exceptions.scala b/tests/pending/neg-customargs/captures/lazylists-exceptions.scala
similarity index 96%
rename from tests/neg-custom-args/captures/lazylists-exceptions.scala
rename to tests/pending/neg-customargs/captures/lazylists-exceptions.scala
index 295147f7f3c5..937d562f3324 100644
--- a/tests/neg-custom-args/captures/lazylists-exceptions.scala
+++ b/tests/pending/neg-customargs/captures/lazylists-exceptions.scala
@@ -1,3 +1,4 @@
+// Needs better use handling
 import language.experimental.saferExceptions
 
 trait LazyList[+A]:
diff --git a/tests/pos-custom-args/captures/lazylists-exceptions.scala b/tests/pending/pos-custom-args/captures/lazylists-exceptions.scala
similarity index 92%
rename from tests/pos-custom-args/captures/lazylists-exceptions.scala
rename to tests/pending/pos-custom-args/captures/lazylists-exceptions.scala
index afc6616108bc..7da43a485a85 100644
--- a/tests/pos-custom-args/captures/lazylists-exceptions.scala
+++ b/tests/pending/pos-custom-args/captures/lazylists-exceptions.scala
@@ -12,9 +12,9 @@ object LzyNil extends LzyList[Nothing]:
   def head = ???
   def tail = ???
 
-final class LzyCons[+A](hd: A, tl: () => LzyList[A]^) extends LzyList[A]:
+def LzyCons[A, C^](hd: A, tl: () => LzyList[A]^{C^}): LzyList[A]^{tl, C^} = new LzyList[A]:
   private var forced = false
-  private var cache: LzyList[A @uncheckedCaptures]^{this} = uninitialized
+  private var cache: LzyList[A @uncheckedCaptures]^{this, C^} = uninitialized
   private def force =
     if !forced then { cache = tl(); forced = true }
     cache
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/iterators.scala b/tests/pos-custom-args/captures/iterators.scala
index 89e1eb91b4f4..8db6702e8a26 100644
--- a/tests/pos-custom-args/captures/iterators.scala
+++ b/tests/pos-custom-args/captures/iterators.scala
@@ -13,8 +13,8 @@ abstract class Iterator[T]:
     def next = f(thisIterator.next)
 end Iterator
 
-private[this] final class ConcatIteratorCell[A](head: => IterableOnce[A]^):
-  def headIterator: Iterator[A]^{this} = head.iterator
+private[this] final class ConcatIteratorCell[A, C^](head: => IterableOnce[A]^{C^}):
+  def headIterator: Iterator[A]^{this, C^} = head.iterator
 
 class C
 type Cap = C^
diff --git a/tests/pos-custom-args/captures/lazylists1.scala b/tests/pos-custom-args/captures/lazylists1.scala
index 62b34f442221..2afc6d2a41cc 100644
--- a/tests/pos-custom-args/captures/lazylists1.scala
+++ b/tests/pos-custom-args/captures/lazylists1.scala
@@ -14,7 +14,7 @@ object LazyNil extends LazyList[Nothing]:
   def tail = ???
   def concat[B](other: LazyList[B]^): LazyList[B]^{other} = other
 
-final class LazyCons[+A](x: A)(xs: () => LazyList[A]^) extends LazyList[A]:
+def LazyCons[A, C^](x: A)(xs: () => LazyList[A]^{C^}): LazyList[A]^{xs, C^} = new LazyList[A]:
   def isEmpty = false
   def head = x
   def tail: LazyList[A]^{this} = xs()
@@ -30,10 +30,10 @@ def test(cap1: Cap, cap2: Cap) =
   def f(x: String): String = if cap1 == cap1 then "" else "a"
   def g(x: String): String = if cap2 == cap2 then "" else "a"
 
-  val xs = new LazyCons("")(() => if f("") == f("") then LazyNil else LazyNil)
+  val xs = LazyCons("")(() => if f("") == f("") then LazyNil else LazyNil)
   val xsc: LazyList[String]^{cap1} = xs
   val ys = xs.map(g)
   val ysc: LazyList[String]^{cap1, cap2} = ys
-  val zs = new LazyCons("")(() => if g("") == g("") then LazyNil else LazyNil)
+  val zs = LazyCons("")(() => if g("") == g("") then LazyNil else LazyNil)
   val as = xs.concat(zs)
   val asc: LazyList[String]^{xs, zs} = as
diff --git a/tests/pos-custom-args/captures/logger-tracked.scala b/tests/pos-custom-args/captures/logger-tracked.scala
index 053731de444d..88f79f5b5066 100644
--- a/tests/pos-custom-args/captures/logger-tracked.scala
+++ b/tests/pos-custom-args/captures/logger-tracked.scala
@@ -26,14 +26,14 @@ object LazyNil extends LazyList[Nothing]:
   def head = ???
   def tail = ???
 
-final class LazyCons[+T](val x: T, val xs: () => LazyList[T]^) extends LazyList[T]:
-  def isEmpty = false
-  def head = x
-  def tail: LazyList[T]^{this} = xs()
-end LazyCons
+def LazyCons[T, C^](x: T, xs: () => LazyList[T]^{C^}): LazyList[T]^{xs, C^} =
+  new LazyList[T]:
+    def isEmpty = false
+    def head = x
+    def tail: LazyList[T]^{this} = xs()
 
 extension [A](x: A)
-  def #::(xs1: => LazyList[A]^): LazyList[A]^{xs1} =
+  def #::[C^](xs1: => LazyList[A]^{C^}): LazyList[A]^{xs1, C^} =
     LazyCons(x, () => xs1)
 
 extension [A](xs: LazyList[A]^)
diff --git a/tests/pos-custom-args/captures/logger.scala b/tests/pos-custom-args/captures/logger.scala
index 81eeb521fee5..7150655f2daf 100644
--- a/tests/pos-custom-args/captures/logger.scala
+++ b/tests/pos-custom-args/captures/logger.scala
@@ -26,14 +26,14 @@ object LazyNil extends LazyList[Nothing]:
   def head = ???
   def tail = ???
 
-final class LazyCons[+T](val x: T, val xs: () => LazyList[T]^) extends LazyList[T]:
-  def isEmpty = false
-  def head = x
-  def tail: LazyList[T]^{this} = xs()
-end LazyCons
+def LazyCons[T, C^](x: T, xs: () => LazyList[T]^{C^}): LazyList[T]^{xs, C^} =
+  new LazyList[T]:
+    def isEmpty = false
+    def head = x
+    def tail: LazyList[T]^{this} = xs()
 
 extension [A](x: A)
-  def #::(xs1: => LazyList[A]^): LazyList[A]^{xs1} =
+  def #::[C^](xs1: => LazyList[A]^{C^}): LazyList[A]^{xs1, C^} =
     LazyCons(x, () => xs1)
 
 extension [A](xs: LazyList[A]^)
diff --git a/tests/pos-custom-args/captures/nested-classes-2.scala b/tests/pos-custom-args/captures/nested-classes-2.scala
index 744635ee949b..fb44a8d394fa 100644
--- a/tests/pos-custom-args/captures/nested-classes-2.scala
+++ b/tests/pos-custom-args/captures/nested-classes-2.scala
@@ -11,7 +11,7 @@ def test1(x: (() => Unit)): Unit =
 
 def test2(x1: (() => Unit), x2: (() => Unit) => Unit) =
   class C1(x1: (() => Unit), xx2: (() => Unit) => Unit):
-    def c2(y1: (() => Unit), y2: (() => Unit) => Unit): C2^ = C2(y1, y2)
+    def c2(y1: (() => Unit), y2: (() => Unit) => Unit): C2^{y1, y2} = C2(y1, y2)
     class C2(y1: (() => Unit), y2: (() => Unit) => Unit):
       val a: (() => Unit) => (() => Unit) = f(y1)
       a(x1)            //OK, but should be error
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/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala b/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala
index 5443758afa72..99a4452ad23e 100644
--- a/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala
+++ b/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala
@@ -433,8 +433,8 @@ object CollectionStrawMan5 {
   }
 
   object View {
-    def fromIterator[A](it: => Iterator[A]^): View[A]^{it} = new View[A]:
-        def iterator: Iterator[A]^{this} = it
+    def fromIterator[A, CI^](it: => Iterator[A]^{CI^}): View[A]^{it, CI^} = new View[A]:
+        def iterator: Iterator[A]^{this, CI^} = it
 
     case object Empty extends View[Nothing] {
       def iterator: Iterator[Nothing] = Iterator.empty
@@ -555,7 +555,15 @@ object CollectionStrawMan5 {
       private var myCurrent: Iterator[B]^{this, f} = Iterator.empty
       private def current = {
         while (!myCurrent.hasNext && self.hasNext)
-          myCurrent = f(self.next()).iterator
+          myCurrent = f(self.next()).iterator.asInstanceOf
+            // TODO: This is actually unsafe, we need to use a capture set variable for `flatMap`, like this:
+            //   def flatMap[B, C^](f: A => IterableOnce[B]^{C^}): Iterator[B]^{this, f, C^}
+            // but if we do this we get:
+            //   Local reach capability C leaks into capture scope of method flatMap
+            // The problem is we can do this only if we upgrade use reasoning. The C capability
+            // is not used at the call of flatMap. It's used later in the iterator.
+            // So the correct type of `flatMap` that expresses this should be:
+            //   def flatMap[B, C^](deferred f: A => IterableOnce[B]^{C^}): Iterator[B]^{this, f, C^}
         myCurrent
       }
       def hasNext = current.hasNext