From 921e9e0faa63d31386d060a4c1f895e0a8857d33 Mon Sep 17 00:00:00 2001
From: noti0na1 <noti0na1@users.noreply.github.com>
Date: Thu, 21 Nov 2024 20:10:41 +0100
Subject: [PATCH 01/13] Make capture parameters and members bounded by CapSet
 by default

---
 compiler/src/dotty/tools/dotc/ast/untpd.scala | 10 ++++++---
 .../dotty/tools/dotc/parsing/Parsers.scala    |  9 +++++---
 .../captures/capset-bound2.scala              | 13 ++++++++++++
 .../captures/capset-members.scala             | 21 +++++++++++++++++++
 4 files changed, 47 insertions(+), 6 deletions(-)
 create mode 100644 tests/neg-custom-args/captures/capset-bound2.scala
 create mode 100644 tests/neg-custom-args/captures/capset-members.scala

diff --git a/compiler/src/dotty/tools/dotc/ast/untpd.scala b/compiler/src/dotty/tools/dotc/ast/untpd.scala
index e8e3646bd087..b91c7a712f4c 100644
--- a/compiler/src/dotty/tools/dotc/ast/untpd.scala
+++ b/compiler/src/dotty/tools/dotc/ast/untpd.scala
@@ -527,10 +527,14 @@ object untpd extends Trees.Instance[Untyped] with UntypedTreeInfo {
   def makeCapsOf(tp: RefTree)(using Context): Tree =
     TypeApply(Select(scalaDot(nme.caps), nme.capsOf), tp :: Nil)
 
-  def makeCapsBound()(using Context): Tree =
-    makeRetaining(
+  // `type C^` and `[C^]` becomes:
+  // `type C >: CapSet <: CapSet^{cap}` and `[C >: CapSet <: CapSet^{cap}]`
+  def makeCapsBound()(using Context): TypeBoundsTree =
+    TypeBoundsTree(
       Select(scalaDot(nme.caps), tpnme.CapSet),
-      Nil, tpnme.retainsCap)
+      makeRetaining(
+        Select(scalaDot(nme.caps), tpnme.CapSet),
+        Nil, tpnme.retainsCap))
 
   def makeConstructor(tparams: List[TypeDef], vparamss: List[List[ValDef]], rhs: Tree = EmptyTree)(using Context): DefDef =
     DefDef(nme.CONSTRUCTOR, joinParams(tparams, vparamss), TypeTree(), rhs)
diff --git a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
index 220053e277a5..a67bb72333e9 100644
--- a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
+++ b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
@@ -2240,7 +2240,7 @@ object Parsers {
       atSpan(in.offset):
         if in.isIdent(nme.UPARROW) && Feature.ccEnabled then
           in.nextToken()
-          TypeBoundsTree(EmptyTree, makeCapsBound())
+          makeCapsBound()
         else
           TypeBoundsTree(bound(SUPERTYPE), bound(SUBTYPE))
 
@@ -4057,8 +4057,11 @@ object Parsers {
               || sourceVersion.isAtLeast(`3.6`) && in.isColon =>
             makeTypeDef(typeAndCtxBounds(tname))
           case _ =>
-            syntaxErrorOrIncomplete(ExpectedTypeBoundOrEquals(in.token))
-            return EmptyTree // return to avoid setting the span to EmptyTree
+            if in.isIdent(nme.UPARROW) && Feature.ccEnabled then
+              makeTypeDef(typeAndCtxBounds(tname))
+            else
+              syntaxErrorOrIncomplete(ExpectedTypeBoundOrEquals(in.token))
+              return EmptyTree // return to avoid setting the span to EmptyTree
         }
       }
     }
diff --git a/tests/neg-custom-args/captures/capset-bound2.scala b/tests/neg-custom-args/captures/capset-bound2.scala
new file mode 100644
index 000000000000..679606f0e43c
--- /dev/null
+++ b/tests/neg-custom-args/captures/capset-bound2.scala
@@ -0,0 +1,13 @@
+import caps.*
+
+class IO
+
+def f[C^](io: IO^{C^}) = ???
+
+def test =
+  f[CapSet](???)
+  f[CapSet^{}](???)
+  f[CapSet^](???)
+  f[Nothing](???) // error
+  f[String](???) // error
+  
\ No newline at end of file
diff --git a/tests/neg-custom-args/captures/capset-members.scala b/tests/neg-custom-args/captures/capset-members.scala
new file mode 100644
index 000000000000..bcc92835b95f
--- /dev/null
+++ b/tests/neg-custom-args/captures/capset-members.scala
@@ -0,0 +1,21 @@
+import caps.*
+
+trait Abstract[X^]:
+  type C >: X <: CapSet^
+  def boom(): Unit^{C^}
+
+class Concrete extends Abstract[CapSet^{}]:
+  type C = CapSet^{}
+  def boom() = ()
+
+class Concrete2 extends Abstract[CapSet^{}]:
+  type C = CapSet^{} & CapSet^{}
+  def boom() = ()
+
+class Concrete3 extends Abstract[CapSet^{}]:
+  type C = CapSet^{} | CapSet^{}
+  def boom() = ()
+
+class Concrete4 extends Abstract[CapSet^{}]:
+  type C = Nothing // error
+  def boom() = ()

From c996062deea19cf9932d050ffae009a114a15895 Mon Sep 17 00:00:00 2001
From: noti0na1 <noti0na1@users.noreply.github.com>
Date: Sun, 24 Nov 2024 23:22:33 +0100
Subject: [PATCH 02/13] Correct rules for CapSet; update definition for
 Contains; fix tests

---
 .../src/dotty/tools/dotc/cc/CaptureRef.scala  | 23 +++++++++++++++----
 library/src/scala/caps.scala                  |  4 ++--
 .../captures/capture-poly.scala               |  2 +-
 tests/neg-custom-args/captures/i22005.scala   |  8 +++++++
 .../neg-custom-args/captures/use-capset.check | 16 ++++++-------
 .../neg-custom-args/captures/use-capset.scala |  2 --
 tests/neg/cc-poly-2.check                     |  7 ------
 tests/neg/cc-poly-2.scala                     |  2 +-
 tests/pos/cc-poly-source-capability.scala     |  5 ++--
 9 files changed, 42 insertions(+), 27 deletions(-)
 create mode 100644 tests/neg-custom-args/captures/i22005.scala

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
index 199114880c2b..a11e272685d9 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
@@ -100,7 +100,8 @@ trait CaptureRef extends TypeProxy, ValueType:
    *   x: x1.type /\ x1 subsumes y  ==>  x subsumes y
    *   TODO: Document path cases
    */
-  final def subsumes(y: CaptureRef)(using Context): Boolean =
+  // import reporting.trace
+  final def subsumes(y: CaptureRef)(using Context): Boolean = // trace.force(i"subsumes $this, $y"):
 
     def subsumingRefs(x: Type, y: Type): Boolean = x match
       case x: CaptureRef => y match
@@ -135,14 +136,28 @@ trait CaptureRef extends TypeProxy, ValueType:
               case _ => false
           || viaInfo(y.info)(subsumingRefs(this, _))
         case MaybeCapability(y1) => this.stripMaybe.subsumes(y1)
+        case y: TypeRef if y.symbol.info.derivesFrom(defn.Caps_CapSet) =>
+          y.info match
+            case _: TypeAlias => y.captureSetOfInfo.elems.forall(this.subsumes)
+            case TypeBounds(_, hi: CaptureRef) => this.subsumes(hi)
+            case _ => y.captureSetOfInfo.elems.forall(this.subsumes)
         case _ => false
     || this.match
         case ReachCapability(x1) => x1.subsumes(y.stripReach)
         case x: TermRef => viaInfo(x.info)(subsumingRefs(_, y))
         case x: TermParamRef => subsumesExistentially(x, y)
-        case x: TypeRef if x.symbol.info.derivesFrom(defn.Caps_CapSet) =>
-          x.captureSetOfInfo.elems.exists(_.subsumes(y))
-        case x: TypeRef => assumedContainsOf(x).contains(y)
+        case x: TypeRef if assumedContainsOf(x).contains(y) => true
+        case x: TypeRef if x.derivesFrom(defn.Caps_CapSet) =>
+          x.info match
+            case _: TypeAlias =>
+              x.captureSetOfInfo.elems.exists(_.subsumes(y))
+            case TypeBounds(lo: CaptureRef, _) =>
+              lo.subsumes(y)
+            case _ =>
+              x.captureSetOfInfo.elems.exists(_.subsumes(y))
+        case AnnotatedType(parent, ann)
+        if ann.symbol.isRetains && parent.derivesFrom(defn.Caps_CapSet) =>
+          ann.tree.toCaptureSet.elems.exists(_.subsumes(y))
         case _ => false
   end subsumes
 
diff --git a/library/src/scala/caps.scala b/library/src/scala/caps.scala
index 53c4ae7dc0dd..da099c4afab6 100644
--- a/library/src/scala/caps.scala
+++ b/library/src/scala/caps.scala
@@ -22,12 +22,12 @@ import annotation.{experimental, compileTimeOnly, retainsCap}
   /** A type constraint expressing that the capture set `C` needs to contain
    *  the capability `R`
    */
-  sealed trait Contains[C <: CapSet @retainsCap, R <: Singleton]
+  sealed trait Contains[+C >: CapSet <: CapSet @retainsCap, R <: Singleton]
 
   /** The only implementation of `Contains`. The constraint that `{R} <: C` is
    *  added separately by the capture checker.
    */
-  given containsImpl[C <: CapSet @retainsCap, R <: Singleton]: Contains[C, R]()
+  given containsImpl[C >: CapSet <: CapSet @retainsCap, R <: Singleton]: Contains[C, R]()
 
   /** A wrapper indicating a type variable in a capture argument list of a
    *  @retains annotation. E.g. `^{x, Y^}` is represented as `@retains(x, capsOf[Y])`.
diff --git a/tests/neg-custom-args/captures/capture-poly.scala b/tests/neg-custom-args/captures/capture-poly.scala
index a3a7a4c2a3d7..0a0d773a3f64 100644
--- a/tests/neg-custom-args/captures/capture-poly.scala
+++ b/tests/neg-custom-args/captures/capture-poly.scala
@@ -3,7 +3,7 @@ import caps.*
 trait Foo extends Capability
 
 trait CaptureSet:
-  type C <: CapSet^
+  type C^
 
 def capturePoly[C^](a: Foo^{C^}): Foo^{C^} = a
 def capturePoly2(c: CaptureSet)(a: Foo^{c.C^}): Foo^{c.C^} = a
diff --git a/tests/neg-custom-args/captures/i22005.scala b/tests/neg-custom-args/captures/i22005.scala
new file mode 100644
index 000000000000..a9dca999e42b
--- /dev/null
+++ b/tests/neg-custom-args/captures/i22005.scala
@@ -0,0 +1,8 @@
+import caps.*
+
+class IO
+class File(io: IO^)
+
+class Handler[C^]:
+  def f(file: File^): File^{C^} = file // error
+  def g(file: File^{C^}): File^ = file // ok
diff --git a/tests/neg-custom-args/captures/use-capset.check b/tests/neg-custom-args/captures/use-capset.check
index cb330daf67f8..74afaa05890f 100644
--- a/tests/neg-custom-args/captures/use-capset.check
+++ b/tests/neg-custom-args/captures/use-capset.check
@@ -1,19 +1,19 @@
--- Error: tests/neg-custom-args/captures/use-capset.scala:7:50 ---------------------------------------------------------
-7 |private def g[C^] = (xs: List[Object^{C^}]) => xs.head // error
+-- Error: tests/neg-custom-args/captures/use-capset.scala:5:50 ---------------------------------------------------------
+5 |private def g[C^] = (xs: List[Object^{C^}]) => xs.head // error
   |                                               ^^^^^^^
   |                                               Capture set parameter C leaks into capture scope of method g.
   |                                               To allow this, the type C should be declared with a @use annotation
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:13:22 -----------------------------------
-13 |  val _: () -> Unit = h // error: should be ->{io}
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:11:22 -----------------------------------
+11 |  val _: () -> Unit = h // error: should be ->{io}
    |                      ^
    |                      Found:    (h : () ->{io} Unit)
    |                      Required: () -> Unit
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:15:50 -----------------------------------
-15 |  val _: () -> List[Object^{io}] -> Object^{io} = h2 // error, should be ->{io}
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:13:50 -----------------------------------
+13 |  val _: () -> List[Object^{io}] -> Object^{io} = h2 // error, should be ->{io}
    |                                                  ^^
-   |                                          Found:    (h2 : () ->? (x$0: List[box Object^]^{}) ->{io} Object^{io})
-   |                                          Required: () -> List[box Object^{io}] -> Object^{io}
+   |                                      Found:    (h2 : () ->? (x$0: List[box Object^{io}]^{}) ->{io} Object^{io})
+   |                                      Required: () -> List[box Object^{io}] -> Object^{io}
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/use-capset.scala b/tests/neg-custom-args/captures/use-capset.scala
index 6010e955f867..74288d616396 100644
--- a/tests/neg-custom-args/captures/use-capset.scala
+++ b/tests/neg-custom-args/captures/use-capset.scala
@@ -1,7 +1,5 @@
 import caps.{use, CapSet}
 
-
-
 def f[C^](@use xs: List[Object^{C^}]): Unit = ???
 
 private def g[C^] = (xs: List[Object^{C^}]) => xs.head // error
diff --git a/tests/neg/cc-poly-2.check b/tests/neg/cc-poly-2.check
index 0615ce19b5ea..7a2882775a75 100644
--- a/tests/neg/cc-poly-2.check
+++ b/tests/neg/cc-poly-2.check
@@ -1,10 +1,3 @@
--- [E007] Type Mismatch Error: tests/neg/cc-poly-2.scala:13:15 ---------------------------------------------------------
-13 |    f[Nothing](d) // error
-   |               ^
-   |               Found:    (d : Test.D^)
-   |               Required: Test.D
-   |
-   | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg/cc-poly-2.scala:14:19 ---------------------------------------------------------
 14 |    f[CapSet^{c1}](d) // error
    |                   ^
diff --git a/tests/neg/cc-poly-2.scala b/tests/neg/cc-poly-2.scala
index c5e5df6540da..809fa8ae077c 100644
--- a/tests/neg/cc-poly-2.scala
+++ b/tests/neg/cc-poly-2.scala
@@ -10,7 +10,7 @@ object Test:
 
   def test(c1: C, c2: C) =
     val d: D^ = D()
-    f[Nothing](d) // error
+    // f[Nothing](d) // already rule out at typer
     f[CapSet^{c1}](d) // error
     val x = f(d)
     val _: D^{c1} = x // error
diff --git a/tests/pos/cc-poly-source-capability.scala b/tests/pos/cc-poly-source-capability.scala
index 363f261dadc1..6f6bdd91d20a 100644
--- a/tests/pos/cc-poly-source-capability.scala
+++ b/tests/pos/cc-poly-source-capability.scala
@@ -20,13 +20,14 @@ import caps.use
 
   def test1(async1: Async, @use others: List[Async]) =
     val src = Source[CapSet^{async1, others*}]
+    val _: Set[Listener^{async1, others*}] = src.allListeners
     val lst1 = listener(async1)
     val lsts = others.map(listener)
     val _: List[Listener^{others*}] = lsts
     src.register{lst1}
     src.register(listener(async1))
-    lsts.foreach(src.register)
-    others.map(listener).foreach(src.register)
+    lsts.foreach(src.register(_)) // TODO: why we need to use _ explicitly here?
+    others.map(listener).foreach(src.register(_))
     val ls = src.allListeners
     val _: Set[Listener^{async1, others*}] = ls
 

From 8a15af3976715da2504f62862f176a1146df6aef Mon Sep 17 00:00:00 2001
From: noti0na1 <noti0na1@users.noreply.github.com>
Date: Tue, 26 Nov 2024 01:57:42 +0100
Subject: [PATCH 03/13] Refine subsumes rule; fix test

---
 .../src/dotty/tools/dotc/cc/CaptureRef.scala  | 24 ++++++++++++-------
 .../captures/cc-poly-varargs.scala            | 21 +++++++++-------
 2 files changed, 28 insertions(+), 17 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
index a11e272685d9..ec3e1908e1b5 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
@@ -93,15 +93,21 @@ trait CaptureRef extends TypeProxy, ValueType:
   final def invalidateCaches() =
     myCaptureSetRunId = NoRunId
 
-  /** x subsumes x
-   *   this subsumes this.f
+  /**  x subsumes x
+   *   x subsumes x.f
+   *   x =:= y ==> x subsumes y
    *   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
+   *   X = CapSet^cx, exists rx in cx, rx subsumes y ==>  X subsumes y
+   *   Y = CapSet^cy, forall ry in cy, x subsumes ry ==>  x subsumes Y
+   *   X: CapSet^c1...CapSet^c2, (CapSet^c1) subsumes y  ==> X subsumes y
+   *   Y: CapSet^c1...CapSet^c2, x subsumes (CapSet^c2) ==> x subsumes Y
+   *   Contains[X, y]  ==>  X subsumes y
+   *
+   *   TODO: Document cases with more comments.
    */
-  // import reporting.trace
-  final def subsumes(y: CaptureRef)(using Context): Boolean = // trace.force(i"subsumes $this, $y"):
+  final def subsumes(y: CaptureRef)(using Context): Boolean =
 
     def subsumingRefs(x: Type, y: Type): Boolean = x match
       case x: CaptureRef => y match
@@ -136,11 +142,13 @@ trait CaptureRef extends TypeProxy, ValueType:
               case _ => false
           || viaInfo(y.info)(subsumingRefs(this, _))
         case MaybeCapability(y1) => this.stripMaybe.subsumes(y1)
-        case y: TypeRef if y.symbol.info.derivesFrom(defn.Caps_CapSet) =>
+        case y: TypeRef if y.derivesFrom(defn.Caps_CapSet) =>
           y.info match
-            case _: TypeAlias => y.captureSetOfInfo.elems.forall(this.subsumes)
             case TypeBounds(_, hi: CaptureRef) => this.subsumes(hi)
             case _ => y.captureSetOfInfo.elems.forall(this.subsumes)
+        case AnnotatedType(parent, ann)
+        if ann.symbol.isRetains && parent.derivesFrom(defn.Caps_CapSet) =>
+          ann.tree.toCaptureSet.elems.forall(this.subsumes)
         case _ => false
     || this.match
         case ReachCapability(x1) => x1.subsumes(y.stripReach)
@@ -149,8 +157,6 @@ trait CaptureRef extends TypeProxy, ValueType:
         case x: TypeRef if assumedContainsOf(x).contains(y) => true
         case x: TypeRef if x.derivesFrom(defn.Caps_CapSet) =>
           x.info match
-            case _: TypeAlias =>
-              x.captureSetOfInfo.elems.exists(_.subsumes(y))
             case TypeBounds(lo: CaptureRef, _) =>
               lo.subsumes(y)
             case _ =>
diff --git a/tests/pos-custom-args/captures/cc-poly-varargs.scala b/tests/pos-custom-args/captures/cc-poly-varargs.scala
index ac76c47d6dd5..0d2478f37bdf 100644
--- a/tests/pos-custom-args/captures/cc-poly-varargs.scala
+++ b/tests/pos-custom-args/captures/cc-poly-varargs.scala
@@ -1,17 +1,22 @@
-trait Cancellable
+abstract class Source[+T, Cap^]:
+  def transformValuesWith[U](f: (T -> U)^{Cap^}): Source[U, Cap]^{this, f} = ???
 
-abstract class Source[+T, Cap^]
-
-extension[T, Cap^](src: Source[T, Cap]^)
-  def transformValuesWith[U](f: (T -> U)^{Cap^}): Source[U, Cap]^{src, f} = ???
+// TODO: The extension version of `transformValuesWith` doesn't work currently.
+// extension[T, Cap^](src: Source[T, Cap]^)
+//   def transformValuesWith[U](f: (T -> U)^{Cap^}): Source[U, Cap]^{src, f} = ???
 
 def race[T, Cap^](sources: Source[T, Cap]^{Cap^}*): Source[T, Cap]^{Cap^} = ???
 
-def either[T1, T2, Cap^](src1: Source[T1, Cap]^{Cap^}, src2: Source[T2, Cap]^{Cap^}): Source[Either[T1, T2], Cap]^{Cap^} =
+def either[T1, T2, Cap^](
+    src1: Source[T1, Cap]^{Cap^},
+    src2: Source[T2, Cap]^{Cap^}): Source[Either[T1, T2], Cap]^{Cap^} =
   val left = src1.transformValuesWith(Left(_))
   val right = src2.transformValuesWith(Right(_))
-  race(left, right)
-
+  race[Either[T1, T2], Cap](left, right)
+  // An explcit type argument is required here because the second argument is
+  // inferred as `CapSet^{Cap^}` instead of `Cap`.
+  // Although `CapSet^{Cap^}` subsums `Cap` in terms of capture set,
+  // `Cap` is not a subtype of `CapSet^{Cap^}` in terms of subtyping.
 
 
 

From 092b358a9b6903cc2732affaf89c6e3bcb2c66f9 Mon Sep 17 00:00:00 2001
From: noti0na1 <noti0na1@users.noreply.github.com>
Date: Tue, 26 Nov 2024 15:30:40 +0100
Subject: [PATCH 04/13] Add constraint to capsOf

---
 .../src/dotty/tools/dotc/cc/CaptureSet.scala  |  4 ++-
 compiler/src/dotty/tools/dotc/cc/Setup.scala  |  5 ++-
 library/src/scala/caps.scala                  |  2 +-
 .../captures/capset-members.scala             |  4 +--
 tests/neg-custom-args/captures/i21868.scala   | 17 +++++-----
 tests/neg-custom-args/captures/i21868b.scala  | 33 +++++++++++++++++++
 .../captures/cc-poly-varargs.scala            | 10 ++----
 7 files changed, 53 insertions(+), 22 deletions(-)
 create mode 100644 tests/neg-custom-args/captures/i21868b.scala

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index 5be4f6a2d1cd..1750e98f708a 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -161,7 +161,9 @@ sealed abstract class CaptureSet extends Showable:
     def debugInfo(using Context) = i"$this accountsFor $x, which has capture set ${x.captureSetOfInfo}"
     def test(using Context) = reporting.trace(debugInfo):
       elems.exists(_.subsumes(x))
-      || !x.isMaxCapability && x.captureSetOfInfo.subCaptures(this, frozen = true).isOK
+      || !x.isMaxCapability
+        && !x.derivesFrom(defn.Caps_CapSet)
+        && x.captureSetOfInfo.subCaptures(this, frozen = true).isOK
     comparer match
       case comparer: ExplainingTypeComparer => comparer.traceIndented(debugInfo)(test)
       case _ => test
diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala
index dfb9ec70bdba..9757e1af3cdb 100644
--- a/compiler/src/dotty/tools/dotc/cc/Setup.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -117,6 +117,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
    *  The info of these symbols is made fluid.
    */
   def isPreCC(sym: Symbol)(using Context): Boolean =
+    // TODO: check type members as well
     sym.isTerm && sym.maybeOwner.isClass
     && !sym.is(Module)
     && !sym.owner.is(CaptureChecked)
@@ -866,7 +867,9 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
           if others.accountsFor(ref) then
             report.warning(em"redundant capture: $dom already accounts for $ref", pos)
 
-        if ref.captureSetOfInfo.elems.isEmpty && !ref.derivesFrom(defn.Caps_Capability) then
+        if ref.captureSetOfInfo.elems.isEmpty
+            && !ref.derivesFrom(defn.Caps_Capability)
+            && !ref.derivesFrom(defn.Caps_CapSet) then
           val deepStr = if ref.isReach then " deep" else ""
           report.error(em"$ref cannot be tracked since its$deepStr capture set is empty", pos)
         check(parent.captureSet, parent)
diff --git a/library/src/scala/caps.scala b/library/src/scala/caps.scala
index da099c4afab6..c35b3b55e813 100644
--- a/library/src/scala/caps.scala
+++ b/library/src/scala/caps.scala
@@ -33,7 +33,7 @@ import annotation.{experimental, compileTimeOnly, retainsCap}
    *  @retains annotation. E.g. `^{x, Y^}` is represented as `@retains(x, capsOf[Y])`.
    */
   @compileTimeOnly("Should be be used only internally by the Scala compiler")
-  def capsOf[CS]: Any = ???
+  def capsOf[CS >: CapSet <: CapSet @retainsCap]: Any = ???
 
   /** Reach capabilities x* which appear as terms in @retains annotations are encoded
    *  as `caps.reachCapability(x)`. When converted to CaptureRef types in capture sets
diff --git a/tests/neg-custom-args/captures/capset-members.scala b/tests/neg-custom-args/captures/capset-members.scala
index bcc92835b95f..2be4b4e32263 100644
--- a/tests/neg-custom-args/captures/capset-members.scala
+++ b/tests/neg-custom-args/captures/capset-members.scala
@@ -16,6 +16,6 @@ class Concrete3 extends Abstract[CapSet^{}]:
   type C = CapSet^{} | CapSet^{}
   def boom() = ()
 
-class Concrete4 extends Abstract[CapSet^{}]:
-  type C = Nothing // error
+class Concrete4 extends Abstract[CapSet^]:
+  type C = CapSet // error
   def boom() = ()
diff --git a/tests/neg-custom-args/captures/i21868.scala b/tests/neg-custom-args/captures/i21868.scala
index 929e770a21c6..4a617f98d07a 100644
--- a/tests/neg-custom-args/captures/i21868.scala
+++ b/tests/neg-custom-args/captures/i21868.scala
@@ -1,14 +1,13 @@
 import caps.*
 
 trait AbstractWrong:
-    type C <: CapSet
-    def boom(): Unit^{C^} // error
+  type C <: CapSet
+  def f(): Unit^{C^} // error
 
-trait Abstract:
-    type C <: CapSet^
-    def boom(): Unit^{C^}
-
-class Concrete extends Abstract:
-    type C = Nothing
-    def boom() = () // error
+trait Abstract1:
+  type C^
+  def f(): Unit^{C^}
 
+class Abstract2:
+  type C >: CapSet <: CapSet^
+  def f(): Unit^{C^}
\ No newline at end of file
diff --git a/tests/neg-custom-args/captures/i21868b.scala b/tests/neg-custom-args/captures/i21868b.scala
new file mode 100644
index 000000000000..feb21894908f
--- /dev/null
+++ b/tests/neg-custom-args/captures/i21868b.scala
@@ -0,0 +1,33 @@
+import caps.*
+
+class IO
+
+class File
+
+trait Abstract:
+  type C >: CapSet <: CapSet^
+  def f(file: File^{C^}): Unit
+
+class Concrete1 extends Abstract:
+  type C = CapSet
+  def f(file: File) = ()
+
+class Concrete2(io: IO^) extends Abstract:
+  type C = CapSet^{io}
+  def f(file: File^{io}) = ()
+
+class Concrete3(io: IO^) extends Abstract:
+  type C = CapSet^{io}
+  def f(file: File) = () // error
+
+trait Abstract2(io: IO^):
+  type C >: CapSet <: CapSet^{io}
+  def f(file: File^{C^}): Unit
+
+class Concrete4(io: IO^) extends Abstract2(io):
+  type C = CapSet
+  def f(file: File) = ()
+
+class Concrete5(io1: IO^, io2: IO^) extends Abstract2(io1):
+  type C = CapSet^{io2} // error
+  def f(file: File^{io2}) = ()
\ No newline at end of file
diff --git a/tests/pos-custom-args/captures/cc-poly-varargs.scala b/tests/pos-custom-args/captures/cc-poly-varargs.scala
index 0d2478f37bdf..168cc4d0275f 100644
--- a/tests/pos-custom-args/captures/cc-poly-varargs.scala
+++ b/tests/pos-custom-args/captures/cc-poly-varargs.scala
@@ -13,13 +13,7 @@ def either[T1, T2, Cap^](
   val left = src1.transformValuesWith(Left(_))
   val right = src2.transformValuesWith(Right(_))
   race[Either[T1, T2], Cap](left, right)
-  // An explcit type argument is required here because the second argument is
-  // inferred as `CapSet^{Cap^}` instead of `Cap`.
+  // Explcit type arguments are required here because the second argument
+  // is inferred as `CapSet^{Cap^}` instead of `Cap`.
   // Although `CapSet^{Cap^}` subsums `Cap` in terms of capture set,
   // `Cap` is not a subtype of `CapSet^{Cap^}` in terms of subtyping.
-
-
-
-
-
-

From acde5c0e06615c5f082e8225f77ddcbd7101e289 Mon Sep 17 00:00:00 2001
From: noti0na1 <noti0na1@users.noreply.github.com>
Date: Tue, 26 Nov 2024 16:31:22 +0100
Subject: [PATCH 05/13] Update test

---
 .../neg-custom-args/captures/capset-members.scala |  6 +++++-
 .../captures/capture-parameters.scala             |  9 +++++++++
 tests/neg-custom-args/captures/i21868b.scala      | 15 ++++++++++++++-
 3 files changed, 28 insertions(+), 2 deletions(-)
 create mode 100644 tests/neg-custom-args/captures/capture-parameters.scala

diff --git a/tests/neg-custom-args/captures/capset-members.scala b/tests/neg-custom-args/captures/capset-members.scala
index 2be4b4e32263..7f975abbbc72 100644
--- a/tests/neg-custom-args/captures/capset-members.scala
+++ b/tests/neg-custom-args/captures/capset-members.scala
@@ -16,6 +16,10 @@ class Concrete3 extends Abstract[CapSet^{}]:
   type C = CapSet^{} | CapSet^{}
   def boom() = ()
 
-class Concrete4 extends Abstract[CapSet^]:
+class Concrete4(a: AnyRef^) extends Abstract[CapSet^{a}]:
   type C = CapSet // error
   def boom() = ()
+
+class Concrete5(a: AnyRef^) extends Abstract[CapSet^{a}]:
+  type C = CapSet^{} | CapSet^{a}
+  def boom() = ()
diff --git a/tests/neg-custom-args/captures/capture-parameters.scala b/tests/neg-custom-args/captures/capture-parameters.scala
new file mode 100644
index 000000000000..d59305ae0cb8
--- /dev/null
+++ b/tests/neg-custom-args/captures/capture-parameters.scala
@@ -0,0 +1,9 @@
+import caps.*
+
+class C
+
+def test[X^, Y^, Z >: X <: Y](x: C^{X^}, y: C^{Y^}, z: C^{Z^}) =
+  val x2z: C^{Z^} = x
+  val z2y: C^{Y^} = z
+  val x2y: C^{Y^} = x // error
+  
\ No newline at end of file
diff --git a/tests/neg-custom-args/captures/i21868b.scala b/tests/neg-custom-args/captures/i21868b.scala
index feb21894908f..cbecb485472e 100644
--- a/tests/neg-custom-args/captures/i21868b.scala
+++ b/tests/neg-custom-args/captures/i21868b.scala
@@ -1,3 +1,4 @@
+import language.experimental.modularity
 import caps.*
 
 class IO
@@ -20,7 +21,7 @@ class Concrete3(io: IO^) extends Abstract:
   type C = CapSet^{io}
   def f(file: File) = () // error
 
-trait Abstract2(io: IO^):
+trait Abstract2(tracked val io: IO^):
   type C >: CapSet <: CapSet^{io}
   def f(file: File^{C^}): Unit
 
@@ -29,5 +30,17 @@ class Concrete4(io: IO^) extends Abstract2(io):
   def f(file: File) = ()
 
 class Concrete5(io1: IO^, io2: IO^) extends Abstract2(io1):
+  type C = CapSet^{io2} // error
+  def f(file: File^{io2}) = ()
+
+trait Abstract3[X^]:
+  type C >: CapSet <: X
+  def f(file: File^{C^}): Unit
+
+class Concrete6(io: IO^) extends Abstract3[CapSet^{io}]:
+  type C = CapSet
+  def f(file: File) = ()
+
+class Concrete7(io1: IO^, io2: IO^) extends Abstract3[CapSet^{io1}]:
   type C = CapSet^{io2} // error
   def f(file: File^{io2}) = ()
\ No newline at end of file

From ed7eed681f406df43a3f8522cf08eaead8cb4497 Mon Sep 17 00:00:00 2001
From: noti0na1 <noti0na1@users.noreply.github.com>
Date: Tue, 26 Nov 2024 22:26:15 +0100
Subject: [PATCH 06/13] Apply suggestions from code review
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Oliver Bračevac <bracevac@users.noreply.github.com>
---
 tests/neg/cc-poly-2.scala                            | 2 +-
 tests/pos-custom-args/captures/cc-poly-varargs.scala | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/tests/neg/cc-poly-2.scala b/tests/neg/cc-poly-2.scala
index 809fa8ae077c..c9249ba59437 100644
--- a/tests/neg/cc-poly-2.scala
+++ b/tests/neg/cc-poly-2.scala
@@ -10,7 +10,7 @@ object Test:
 
   def test(c1: C, c2: C) =
     val d: D^ = D()
-    // f[Nothing](d) // already rule out at typer
+    // f[Nothing](d) // already ruled out at typer
     f[CapSet^{c1}](d) // error
     val x = f(d)
     val _: D^{c1} = x // error
diff --git a/tests/pos-custom-args/captures/cc-poly-varargs.scala b/tests/pos-custom-args/captures/cc-poly-varargs.scala
index 168cc4d0275f..7f04ed987b28 100644
--- a/tests/pos-custom-args/captures/cc-poly-varargs.scala
+++ b/tests/pos-custom-args/captures/cc-poly-varargs.scala
@@ -13,7 +13,7 @@ def either[T1, T2, Cap^](
   val left = src1.transformValuesWith(Left(_))
   val right = src2.transformValuesWith(Right(_))
   race[Either[T1, T2], Cap](left, right)
-  // Explcit type arguments are required here because the second argument
+  // Explicit type arguments are required here because the second argument
   // is inferred as `CapSet^{Cap^}` instead of `Cap`.
-  // Although `CapSet^{Cap^}` subsums `Cap` in terms of capture set,
+  // Although `CapSet^{Cap^}` subsumes `Cap` in terms of capture sets,
   // `Cap` is not a subtype of `CapSet^{Cap^}` in terms of subtyping.

From bf8dcccf74a8e63e2d0fa723eea5687814f27a23 Mon Sep 17 00:00:00 2001
From: noti0na1 <noti0na1@users.noreply.github.com>
Date: Wed, 27 Nov 2024 05:42:03 +0100
Subject: [PATCH 07/13] Fix test

---
 .../tools/dotc/cc/CaptureAnnotation.scala     |  1 +
 .../src/dotty/tools/dotc/cc/CaptureRef.scala  | 12 +++++-----
 .../captures/capset-members.scala             | 22 ++++++++++---------
 tests/neg-custom-args/captures/i21868b.scala  | 13 +++++++----
 4 files changed, 28 insertions(+), 20 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureAnnotation.scala b/compiler/src/dotty/tools/dotc/cc/CaptureAnnotation.scala
index e437a8ad5d5f..f0018cc93d7e 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureAnnotation.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureAnnotation.scala
@@ -42,6 +42,7 @@ case class CaptureAnnotation(refs: CaptureSet, boxed: Boolean)(cls: Symbol) exte
       case cr: TermRef => ref(cr)
       case cr: TermParamRef => untpd.Ident(cr.paramName).withType(cr)
       case cr: ThisType => This(cr.cls)
+      // TODO: Will crash if the type is an annotated type, for example `cap?`
     }
     val arg = repeated(elems, TypeTree(defn.AnyType))
     New(symbol.typeRef, arg :: Nil)
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
index ec3e1908e1b5..6bfb83e07921 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
@@ -94,15 +94,15 @@ trait CaptureRef extends TypeProxy, ValueType:
     myCaptureSetRunId = NoRunId
 
   /**  x subsumes x
-   *   x subsumes x.f
-   *   x =:= y ==> x subsumes y
+   *   x =:= y       ==>  x subsumes y
+   *   x subsumes y  ==>  x subsumes y.f
    *   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
-   *   X = CapSet^cx, exists rx in cx, rx subsumes y ==>  X subsumes y
-   *   Y = CapSet^cy, forall ry in cy, x subsumes ry ==>  x subsumes Y
-   *   X: CapSet^c1...CapSet^c2, (CapSet^c1) subsumes y  ==> X subsumes y
-   *   Y: CapSet^c1...CapSet^c2, x subsumes (CapSet^c2) ==> x subsumes Y
+   *   X = CapSet^cx, exists rx in cx, rx subsumes y     ==>  X subsumes y
+   *   Y = CapSet^cy, forall ry in cy, x subsumes ry     ==>  x subsumes Y
+   *   X: CapSet^c1...CapSet^c2, (CapSet^c1) subsumes y  ==>  X subsumes y
+   *   Y: CapSet^c1...CapSet^c2, x subsumes (CapSet^c2)  ==>  x subsumes Y
    *   Contains[X, y]  ==>  X subsumes y
    *
    *   TODO: Document cases with more comments.
diff --git a/tests/neg-custom-args/captures/capset-members.scala b/tests/neg-custom-args/captures/capset-members.scala
index 7f975abbbc72..984df756f48d 100644
--- a/tests/neg-custom-args/captures/capset-members.scala
+++ b/tests/neg-custom-args/captures/capset-members.scala
@@ -2,24 +2,26 @@ import caps.*
 
 trait Abstract[X^]:
   type C >: X <: CapSet^
-  def boom(): Unit^{C^}
+  // Don't test the return type using Unit, because it is a pure type.
+  def boom(): AnyRef^{C^}
 
 class Concrete extends Abstract[CapSet^{}]:
   type C = CapSet^{}
-  def boom() = ()
+  // TODO: Why do we get error without the return type here?
+  def boom(): AnyRef = new Object
 
 class Concrete2 extends Abstract[CapSet^{}]:
-  type C = CapSet^{} & CapSet^{}
-  def boom() = ()
+  type C = CapSet^{}
+  def boom(): AnyRef^ = new Object // error
 
 class Concrete3 extends Abstract[CapSet^{}]:
-  type C = CapSet^{} | CapSet^{}
-  def boom() = ()
+  def boom(): AnyRef = new Object
 
 class Concrete4(a: AnyRef^) extends Abstract[CapSet^{a}]:
   type C = CapSet // error
-  def boom() = ()
+  def boom(): AnyRef^{a} = a // error
 
-class Concrete5(a: AnyRef^) extends Abstract[CapSet^{a}]:
-  type C = CapSet^{} | CapSet^{a}
-  def boom() = ()
+class Concrete5(a: AnyRef^, b: AnyRef^) extends Abstract[CapSet^{a}]:
+  // TODO: Crash with the type member
+  // type C = CapSet^{a}
+  def boom(): AnyRef^{b} = b // error
diff --git a/tests/neg-custom-args/captures/i21868b.scala b/tests/neg-custom-args/captures/i21868b.scala
index cbecb485472e..bf512c411c19 100644
--- a/tests/neg-custom-args/captures/i21868b.scala
+++ b/tests/neg-custom-args/captures/i21868b.scala
@@ -29,9 +29,10 @@ class Concrete4(io: IO^) extends Abstract2(io):
   type C = CapSet
   def f(file: File) = ()
 
-class Concrete5(io1: IO^, io2: IO^) extends Abstract2(io1):
-  type C = CapSet^{io2} // error
-  def f(file: File^{io2}) = ()
+// TODO: Should be an error
+// class Concrete5(io1: IO^, io2: IO^) extends Abstract2(io1):
+//   type C = CapSet^{io2}
+//   def f(file: File^{io2}) = ()
 
 trait Abstract3[X^]:
   type C >: CapSet <: X
@@ -43,4 +44,8 @@ class Concrete6(io: IO^) extends Abstract3[CapSet^{io}]:
 
 class Concrete7(io1: IO^, io2: IO^) extends Abstract3[CapSet^{io1}]:
   type C = CapSet^{io2} // error
-  def f(file: File^{io2}) = ()
\ No newline at end of file
+  def f(file: File^{io2}) = ()
+
+class Concrete8(io1: IO^, io2: IO^) extends Abstract3[CapSet^{io1}]:
+  type C = CapSet^{io1}
+  def f(file: File^{io2}) = () // error
\ No newline at end of file

From 1fb05b2a82df1553a194502473b4f9a3232af470 Mon Sep 17 00:00:00 2001
From: noti0na1 <noti0na1@users.noreply.github.com>
Date: Wed, 27 Nov 2024 13:59:08 +0100
Subject: [PATCH 08/13] Fix crash error

---
 compiler/src/dotty/tools/dotc/cc/CaptureRef.scala   | 10 ++++------
 tests/neg-custom-args/captures/capset-members.scala |  7 +++++--
 tests/neg-custom-args/captures/i21868b.scala        | 12 +++++++++---
 3 files changed, 18 insertions(+), 11 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
index 6bfb83e07921..c4990b4413a8 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
@@ -146,9 +146,8 @@ trait CaptureRef extends TypeProxy, ValueType:
           y.info match
             case TypeBounds(_, hi: CaptureRef) => this.subsumes(hi)
             case _ => y.captureSetOfInfo.elems.forall(this.subsumes)
-        case AnnotatedType(parent, ann)
-        if ann.symbol.isRetains && parent.derivesFrom(defn.Caps_CapSet) =>
-          ann.tree.toCaptureSet.elems.forall(this.subsumes)
+        case CapturingType(parent, refs) if parent.derivesFrom(defn.Caps_CapSet) =>
+          refs.elems.forall(this.subsumes)
         case _ => false
     || this.match
         case ReachCapability(x1) => x1.subsumes(y.stripReach)
@@ -161,9 +160,8 @@ trait CaptureRef extends TypeProxy, ValueType:
               lo.subsumes(y)
             case _ =>
               x.captureSetOfInfo.elems.exists(_.subsumes(y))
-        case AnnotatedType(parent, ann)
-        if ann.symbol.isRetains && parent.derivesFrom(defn.Caps_CapSet) =>
-          ann.tree.toCaptureSet.elems.exists(_.subsumes(y))
+        case CapturingType(parent, refs) if parent.derivesFrom(defn.Caps_CapSet) =>
+          refs.elems.exists(_.subsumes(y))
         case _ => false
   end subsumes
 
diff --git a/tests/neg-custom-args/captures/capset-members.scala b/tests/neg-custom-args/captures/capset-members.scala
index 984df756f48d..540216852a43 100644
--- a/tests/neg-custom-args/captures/capset-members.scala
+++ b/tests/neg-custom-args/captures/capset-members.scala
@@ -22,6 +22,9 @@ class Concrete4(a: AnyRef^) extends Abstract[CapSet^{a}]:
   def boom(): AnyRef^{a} = a // error
 
 class Concrete5(a: AnyRef^, b: AnyRef^) extends Abstract[CapSet^{a}]:
-  // TODO: Crash with the type member
-  // type C = CapSet^{a}
+  type C = CapSet^{a}
   def boom(): AnyRef^{b} = b // error
+
+class Concrete6(a: AnyRef^, b: AnyRef^) extends Abstract[CapSet^{a}]:
+  def boom(): AnyRef^{b} = b // error
+  
\ No newline at end of file
diff --git a/tests/neg-custom-args/captures/i21868b.scala b/tests/neg-custom-args/captures/i21868b.scala
index bf512c411c19..490b5964b05b 100644
--- a/tests/neg-custom-args/captures/i21868b.scala
+++ b/tests/neg-custom-args/captures/i21868b.scala
@@ -30,9 +30,15 @@ class Concrete4(io: IO^) extends Abstract2(io):
   def f(file: File) = ()
 
 // TODO: Should be an error
-// class Concrete5(io1: IO^, io2: IO^) extends Abstract2(io1):
-//   type C = CapSet^{io2}
-//   def f(file: File^{io2}) = ()
+class Concrete5(io1: IO^, io2: IO^) extends Abstract2(io1):
+  // Similar to Concrete8, this type member should have overriding error.
+  // Parent class is Abstract2 { val io = Concrete5.this.io1 }
+  // Abstract2.this.C >: CapSet <: CapSet^{Concrete5.this.io1}
+  // Concrete5.this.C = CapSet^{Concrete5.this.io2}
+  // CapSet^{Concrete5.this.io2} !<:< CapSet^{Concrete5.this.io1}
+  // Hence, Concrete5.this.C !<:< Abstract2.this.C
+  type C = CapSet^{io2}
+  def f(file: File^{io2}) = ()
 
 trait Abstract3[X^]:
   type C >: CapSet <: X

From 82c5512009912b9b6535d0e5cf816695220a46f0 Mon Sep 17 00:00:00 2001
From: noti0na1 <noti0na1@users.noreply.github.com>
Date: Thu, 28 Nov 2024 01:15:14 +0100
Subject: [PATCH 09/13] Fix overriding check

---
 compiler/src/dotty/tools/dotc/cc/Setup.scala        |  1 -
 compiler/src/dotty/tools/dotc/typer/RefChecks.scala |  7 +++++--
 tests/neg-custom-args/captures/i21868b.scala        | 10 +---------
 3 files changed, 6 insertions(+), 12 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala
index 9757e1af3cdb..c5c362dbe8dc 100644
--- a/compiler/src/dotty/tools/dotc/cc/Setup.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -117,7 +117,6 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
    *  The info of these symbols is made fluid.
    */
   def isPreCC(sym: Symbol)(using Context): Boolean =
-    // TODO: check type members as well
     sym.isTerm && sym.maybeOwner.isClass
     && !sym.is(Module)
     && !sym.owner.is(CaptureChecked)
diff --git a/compiler/src/dotty/tools/dotc/typer/RefChecks.scala b/compiler/src/dotty/tools/dotc/typer/RefChecks.scala
index 0ec9458cac5c..e03a2e3764c3 100644
--- a/compiler/src/dotty/tools/dotc/typer/RefChecks.scala
+++ b/compiler/src/dotty/tools/dotc/typer/RefChecks.scala
@@ -21,6 +21,7 @@ import config.MigrationVersion
 import config.Printers.refcheck
 import reporting.*
 import Constants.Constant
+import cc.stripCapturing
 
 object RefChecks {
   import tpd.*
@@ -83,8 +84,10 @@ object RefChecks {
    *  This one used to succeed only if forwarding parameters is on.
    *  (Forwarding tends to hide problems by binding parameter names).
    */
+
   private def upwardsThisType(cls: Symbol)(using Context) = cls.info match {
-    case ClassInfo(_, _, _, _, tp: Type) if (tp ne cls.typeRef) && !cls.isOneOf(FinalOrModuleClass) =>
+    case ClassInfo(_, _, _, _, tp: Type) if (tp.stripCapturing ne cls.typeRef) && !cls.isOneOf(FinalOrModuleClass) =>
+      // println(i"upwardsThisType($cls) = ${cls.typeRef}, ne $tp")
       SkolemType(cls.appliedRef).withName(nme.this_)
     case _ =>
       cls.thisType
@@ -439,7 +442,7 @@ object RefChecks {
         val (mtp, otp) = if compareTypes then (memberTp(self), otherTp(self)) else (NoType, NoType)
         OverrideError(core, self, member, other, mtp, otp)
 
-      def compatTypes(memberTp: Type, otherTp: Type): Boolean =
+      def compatTypes(memberTp: Type, otherTp: Type): Boolean = // race.force(i"compatTypes $memberTp <:< $otherTp"):
         try
           isOverridingPair(member, memberTp, other, otherTp,
             fallBack = warnOnMigration(
diff --git a/tests/neg-custom-args/captures/i21868b.scala b/tests/neg-custom-args/captures/i21868b.scala
index 490b5964b05b..70f4e9c9d59c 100644
--- a/tests/neg-custom-args/captures/i21868b.scala
+++ b/tests/neg-custom-args/captures/i21868b.scala
@@ -29,15 +29,8 @@ class Concrete4(io: IO^) extends Abstract2(io):
   type C = CapSet
   def f(file: File) = ()
 
-// TODO: Should be an error
 class Concrete5(io1: IO^, io2: IO^) extends Abstract2(io1):
-  // Similar to Concrete8, this type member should have overriding error.
-  // Parent class is Abstract2 { val io = Concrete5.this.io1 }
-  // Abstract2.this.C >: CapSet <: CapSet^{Concrete5.this.io1}
-  // Concrete5.this.C = CapSet^{Concrete5.this.io2}
-  // CapSet^{Concrete5.this.io2} !<:< CapSet^{Concrete5.this.io1}
-  // Hence, Concrete5.this.C !<:< Abstract2.this.C
-  type C = CapSet^{io2}
+  type C = CapSet^{io2} // error
   def f(file: File^{io2}) = ()
 
 trait Abstract3[X^]:
@@ -53,5 +46,4 @@ class Concrete7(io1: IO^, io2: IO^) extends Abstract3[CapSet^{io1}]:
   def f(file: File^{io2}) = ()
 
 class Concrete8(io1: IO^, io2: IO^) extends Abstract3[CapSet^{io1}]:
-  type C = CapSet^{io1}
   def f(file: File^{io2}) = () // error
\ No newline at end of file

From 0750d5c4433ca0dba5b508ef46723c063da6b2c1 Mon Sep 17 00:00:00 2001
From: noti0na1 <noti0na1@users.noreply.github.com>
Date: Fri, 29 Nov 2024 12:49:36 +0100
Subject: [PATCH 10/13] Update Stepper in the library

---
 scala2-library-cc/src/scala/collection/Stepper.scala | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/scala2-library-cc/src/scala/collection/Stepper.scala b/scala2-library-cc/src/scala/collection/Stepper.scala
index 2f8abee4cffb..1723a110ad8a 100644
--- a/scala2-library-cc/src/scala/collection/Stepper.scala
+++ b/scala2-library-cc/src/scala/collection/Stepper.scala
@@ -53,7 +53,7 @@ trait Stepper[@specialized(Double, Int, Long) +A] {
     *
     * See method `trySplit` in [[java.util.Spliterator]].
     */
-  def trySplit(): Stepper[A]
+  def trySplit(): Stepper[A]^{this}
 
   /** Returns an estimate of the number of elements of this Stepper, or [[Long.MaxValue]]. See
     * method `estimateSize` in [[java.util.Spliterator]].
@@ -71,7 +71,7 @@ trait Stepper[@specialized(Double, Int, Long) +A] {
     * a [[java.util.Spliterator.OfInt]] (which is a `Spliterator[Integer]`) in the subclass [[IntStepper]]
     * (which is a `Stepper[Int]`).
     */
-  def spliterator[B >: A]: Spliterator[_]
+  def spliterator[B >: A]: Spliterator[_]^{this}
 
   /** Returns a Java [[java.util.Iterator]] corresponding to this Stepper.
     *
@@ -79,7 +79,7 @@ trait Stepper[@specialized(Double, Int, Long) +A] {
     * a [[java.util.PrimitiveIterator.OfInt]] (which is a `Iterator[Integer]`) in the subclass
     * [[IntStepper]] (which is a `Stepper[Int]`).
     */
-  def javaIterator[B >: A]: JIterator[_]
+  def javaIterator[B >: A]: JIterator[_]^{this}
 
   /** Returns an [[Iterator]] corresponding to this Stepper. Note that Iterators corresponding to
     * primitive Steppers box the elements.

From 1ed08dee4a26d6ae1806a6d5368ef0160bbe3a8d Mon Sep 17 00:00:00 2001
From: noti0na1 <noti0na1@users.noreply.github.com>
Date: Fri, 29 Nov 2024 15:31:18 +0100
Subject: [PATCH 11/13] Clean comments

---
 compiler/src/dotty/tools/dotc/typer/RefChecks.scala | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/typer/RefChecks.scala b/compiler/src/dotty/tools/dotc/typer/RefChecks.scala
index e03a2e3764c3..7e53b38b5f98 100644
--- a/compiler/src/dotty/tools/dotc/typer/RefChecks.scala
+++ b/compiler/src/dotty/tools/dotc/typer/RefChecks.scala
@@ -84,10 +84,8 @@ object RefChecks {
    *  This one used to succeed only if forwarding parameters is on.
    *  (Forwarding tends to hide problems by binding parameter names).
    */
-
   private def upwardsThisType(cls: Symbol)(using Context) = cls.info match {
     case ClassInfo(_, _, _, _, tp: Type) if (tp.stripCapturing ne cls.typeRef) && !cls.isOneOf(FinalOrModuleClass) =>
-      // println(i"upwardsThisType($cls) = ${cls.typeRef}, ne $tp")
       SkolemType(cls.appliedRef).withName(nme.this_)
     case _ =>
       cls.thisType
@@ -442,7 +440,7 @@ object RefChecks {
         val (mtp, otp) = if compareTypes then (memberTp(self), otherTp(self)) else (NoType, NoType)
         OverrideError(core, self, member, other, mtp, otp)
 
-      def compatTypes(memberTp: Type, otherTp: Type): Boolean = // race.force(i"compatTypes $memberTp <:< $otherTp"):
+      def compatTypes(memberTp: Type, otherTp: Type): Boolean =
         try
           isOverridingPair(member, memberTp, other, otherTp,
             fallBack = warnOnMigration(

From c1a083547e0b0cf80f20561eb6216cb0168e891f Mon Sep 17 00:00:00 2001
From: noti0na1 <noti0na1@users.noreply.github.com>
Date: Sat, 30 Nov 2024 01:42:10 +0100
Subject: [PATCH 12/13] Drop syntax sugar for capture set member

---
 compiler/src/dotty/tools/dotc/cc/CaptureRef.scala   | 3 +++
 compiler/src/dotty/tools/dotc/parsing/Parsers.scala | 7 ++-----
 tests/neg-custom-args/captures/capture-poly.scala   | 2 +-
 tests/neg-custom-args/captures/i21868.scala         | 8 ++++----
 4 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
index c4990b4413a8..9bda9102cbb8 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
@@ -143,6 +143,9 @@ trait CaptureRef extends TypeProxy, ValueType:
           || viaInfo(y.info)(subsumingRefs(this, _))
         case MaybeCapability(y1) => this.stripMaybe.subsumes(y1)
         case y: TypeRef if y.derivesFrom(defn.Caps_CapSet) =>
+          // The upper and lower bounds don't have to be in the form of `CapSet^{...}`.
+          // They can be other capture set variables, which are bounded by `CapSet`,
+          // like `def test[X^, Y^, Z >: X <: Y]`.
           y.info match
             case TypeBounds(_, hi: CaptureRef) => this.subsumes(hi)
             case _ => y.captureSetOfInfo.elems.forall(this.subsumes)
diff --git a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
index a67bb72333e9..89f88faebc17 100644
--- a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
+++ b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
@@ -4057,11 +4057,8 @@ object Parsers {
               || sourceVersion.isAtLeast(`3.6`) && in.isColon =>
             makeTypeDef(typeAndCtxBounds(tname))
           case _ =>
-            if in.isIdent(nme.UPARROW) && Feature.ccEnabled then
-              makeTypeDef(typeAndCtxBounds(tname))
-            else
-              syntaxErrorOrIncomplete(ExpectedTypeBoundOrEquals(in.token))
-              return EmptyTree // return to avoid setting the span to EmptyTree
+            syntaxErrorOrIncomplete(ExpectedTypeBoundOrEquals(in.token))
+            return EmptyTree // return to avoid setting the span to EmptyTree
         }
       }
     }
diff --git a/tests/neg-custom-args/captures/capture-poly.scala b/tests/neg-custom-args/captures/capture-poly.scala
index 0a0d773a3f64..88989b418726 100644
--- a/tests/neg-custom-args/captures/capture-poly.scala
+++ b/tests/neg-custom-args/captures/capture-poly.scala
@@ -3,7 +3,7 @@ import caps.*
 trait Foo extends Capability
 
 trait CaptureSet:
-  type C^
+  type C >: CapSet <: CapSet^
 
 def capturePoly[C^](a: Foo^{C^}): Foo^{C^} = a
 def capturePoly2(c: CaptureSet)(a: Foo^{c.C^}): Foo^{c.C^} = a
diff --git a/tests/neg-custom-args/captures/i21868.scala b/tests/neg-custom-args/captures/i21868.scala
index 4a617f98d07a..876b68ac90a4 100644
--- a/tests/neg-custom-args/captures/i21868.scala
+++ b/tests/neg-custom-args/captures/i21868.scala
@@ -5,9 +5,9 @@ trait AbstractWrong:
   def f(): Unit^{C^} // error
 
 trait Abstract1:
-  type C^
+  type C >: CapSet <: CapSet^
   def f(): Unit^{C^}
 
-class Abstract2:
-  type C >: CapSet <: CapSet^
-  def f(): Unit^{C^}
\ No newline at end of file
+// class Abstract2:
+//   type C^
+//   def f(): Unit^{C^}
\ No newline at end of file

From 6866bd11544fd29ac3c12117184346134b54ca63 Mon Sep 17 00:00:00 2001
From: noti0na1 <noti0na1@users.noreply.github.com>
Date: Sat, 30 Nov 2024 01:45:07 +0100
Subject: [PATCH 13/13] Update comment

---
 compiler/src/dotty/tools/dotc/ast/untpd.scala | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/ast/untpd.scala b/compiler/src/dotty/tools/dotc/ast/untpd.scala
index b91c7a712f4c..2acfc4cf86e3 100644
--- a/compiler/src/dotty/tools/dotc/ast/untpd.scala
+++ b/compiler/src/dotty/tools/dotc/ast/untpd.scala
@@ -527,8 +527,7 @@ object untpd extends Trees.Instance[Untyped] with UntypedTreeInfo {
   def makeCapsOf(tp: RefTree)(using Context): Tree =
     TypeApply(Select(scalaDot(nme.caps), nme.capsOf), tp :: Nil)
 
-  // `type C^` and `[C^]` becomes:
-  // `type C >: CapSet <: CapSet^{cap}` and `[C >: CapSet <: CapSet^{cap}]`
+  // Capture set variable `[C^]` becomes: `[C >: CapSet <: CapSet^{cap}]`
   def makeCapsBound()(using Context): TypeBoundsTree =
     TypeBoundsTree(
       Select(scalaDot(nme.caps), tpnme.CapSet),