From cb24fa952eef0b67e3a5e1d0e6f83b2050aee02e Mon Sep 17 00:00:00 2001
From: noti0na1 <noti0na1@users.noreply.github.com>
Date: Wed, 5 Mar 2025 16:44:14 +0100
Subject: [PATCH 01/17] Remove unnecessary `^` in capture set syntax.

---
 compiler/src/dotty/tools/dotc/core/Mode.scala | 10 ++++++-
 .../dotty/tools/dotc/parsing/Parsers.scala    | 10 ++-----
 .../dotty/tools/dotc/typer/Applications.scala |  5 +++-
 .../src/dotty/tools/dotc/typer/Typer.scala    | 12 ++++++++
 .../captures/capset-bound.scala               |  2 +-
 .../captures/capset-bound2.scala              |  3 +-
 .../captures/capset-members.scala             |  3 +-
 .../captures/capture-parameters.scala         |  9 +++---
 .../captures/capture-poly.scala               |  8 ++---
 .../captures/capture-vars-subtyping.scala     | 26 ++++++++--------
 .../captures/capture-vars-subtyping2.scala    | 30 +++++++++----------
 .../neg-custom-args/captures/cc-poly-1.scala  |  2 +-
 .../neg-custom-args/captures/cc-poly-2.scala  |  2 +-
 .../captures/cc-poly-source.scala             |  6 ++--
 tests/neg-custom-args/captures/i21313.scala   |  2 +-
 tests/neg-custom-args/captures/i21347.scala   |  2 +-
 tests/neg-custom-args/captures/i21868.scala   |  4 +--
 tests/neg-custom-args/captures/i21868b.scala  |  6 ++--
 .../captures/polyCaptures.check               |  4 +--
 .../captures/polyCaptures.scala               |  6 ++--
 .../neg-custom-args/captures/use-capset.check | 10 +++----
 .../neg-custom-args/captures/use-capset.scala |  6 ++--
 .../pos-custom-args/captures/cc-poly-1.scala  |  6 ++--
 .../captures/cc-poly-source-capability.scala  |  6 ++--
 .../captures/cc-poly-varargs.scala            |  8 ++---
 .../captures/gears-problem-poly.scala         |  8 ++---
 tests/pos-custom-args/captures/i21313.scala   |  8 ++---
 tests/pos-custom-args/captures/i21347.scala   |  2 +-
 tests/pos-custom-args/captures/i21507.scala   |  8 ++---
 .../pos-custom-args/captures/setup/a_1.scala  |  2 +-
 .../pos-custom-args/captures/setup/b_1.scala  |  2 +-
 .../pos-custom-args/captures/setup/b_2.scala  |  2 +-
 32 files changed, 117 insertions(+), 103 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/Mode.scala b/compiler/src/dotty/tools/dotc/core/Mode.scala
index 6fd76e37977d..e0ab4571667c 100644
--- a/compiler/src/dotty/tools/dotc/core/Mode.scala
+++ b/compiler/src/dotty/tools/dotc/core/Mode.scala
@@ -91,8 +91,16 @@ object Mode {
    */
   val ImplicitExploration: Mode = newMode(12, "ImplicitExploration")
 
+  /** We are currently inside a capture set.
+   *  A term name could be a capture variable, so we need to
+   *  check that it is valid to use as type name.
+   *  Since this mode is only used during annotation typing,
+   *  we can reuse the value of `ImplicitExploration` to save bits.
+   */
+  val InCaptureSet: Mode = newMode(13, "InCaptureSet")
+
   /** We are currently unpickling Scala2 info */
-  val Scala2Unpickling: Mode = newMode(13, "Scala2Unpickling")
+  val Scala2Unpickling: Mode = newMode(14, "Scala2Unpickling")
 
   /** Signifies one of two possible situations:
    *   1. We are currently checking bounds to be non-empty, so we should not
diff --git a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
index c24dbce1b6ac..1f756008d632 100644
--- a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
+++ b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
@@ -1600,8 +1600,8 @@ object Parsers {
       case _ => None
     }
 
-    /** CaptureRef  ::=  { SimpleRef `.` } SimpleRef [`*`] [`.` rd]
-     *                |  [ { SimpleRef `.` } SimpleRef `.` ] id `^`
+    /** CaptureRef  ::=  { SimpleRef `.` } SimpleRef [`*`]
+     *                |  [ { SimpleRef `.` } SimpleRef `.` ] id
      */
     def captureRef(): Tree =
 
@@ -1620,12 +1620,6 @@ object Parsers {
             in.nextToken()
             derived(reachRef, nme.CC_READONLY)
           else reachRef
-        else if isIdent(nme.UPARROW) then
-          in.nextToken()
-          atSpan(startOffset(ref)):
-            convertToTypeId(ref) match
-              case ref: RefTree => makeCapsOf(ref)
-              case ref => ref
         else ref
 
       recur(simpleRef())
diff --git a/compiler/src/dotty/tools/dotc/typer/Applications.scala b/compiler/src/dotty/tools/dotc/typer/Applications.scala
index 71fc250d0710..381643a1cfbd 100644
--- a/compiler/src/dotty/tools/dotc/typer/Applications.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Applications.scala
@@ -36,6 +36,7 @@ import annotation.threadUnsafe
 
 import scala.util.control.NonFatal
 import dotty.tools.dotc.inlines.Inlines
+import dotty.tools.dotc.cc.isRetains
 
 object Applications {
   import tpd.*
@@ -1115,7 +1116,9 @@ trait Applications extends Compatibility {
             val fun2 = Applications.retypeSignaturePolymorphicFn(fun1, methType)
             simpleApply(fun2, proto)
           case funRef: TermRef =>
-            val app = ApplyTo(tree, fun1, funRef, proto, pt)
+            // println(i"typedApply: $funRef, ${tree.args}, ${funRef.symbol.maybeOwner.isRetains}")
+            val applyCtx = if funRef.symbol.maybeOwner.isRetains then ctx.addMode(Mode.InCaptureSet) else ctx
+            val app = ApplyTo(tree, fun1, funRef, proto, pt)(using applyCtx)
             convertNewGenericArray(
               widenEnumCase(
                 postProcessByNameArgs(funRef, app).computeNullable(),
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index 6b7b840e7606..3ca3afef3315 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -715,6 +715,10 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
         && ctx.owner.owner.unforcedDecls.lookup(tree.name).exists
     then // we are in the arguments of a this(...) constructor call
       errorTree(tree, em"$tree is not accessible from constructor arguments")
+    else if ctx.mode.is(Mode.InCaptureSet) then
+      // If we are in a capture set and the identifier is not a term name,
+      // try to type it with the same name but as a type
+      typed(untpd.makeCapsOf(untpd.cpy.Ident(tree)(name.toTypeName)), pt)
     else
       errorTree(tree, MissingIdent(tree, kind, name, pt))
   end typedIdent
@@ -920,6 +924,13 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
         typedCBSelect(tree0, pt, qual)
       else EmptyTree
 
+    // Otherwise, if we are in a capture set, try to type it as a capture variable
+    // reference (as selecting a type name).
+    def trySelectTypeInCaptureSet() =
+      if ctx.mode.is(Mode.InCaptureSet) && tree0.name.isTypeName then
+        typedSelectWithAdapt(untpd.cpy.Select(tree0)(qual, tree0.name.toTypeName), pt, qual)
+      else EmptyTree
+
     // Otherwise, report an error
     def reportAnError() =
       assignType(tree,
@@ -941,6 +952,7 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
       .orElse(tryDynamic())
       .orElse(trySelectable())
       .orElse(tryCBCompanion())
+      .orElse(trySelectTypeInCaptureSet())
       .orElse(reportAnError())
   end typedSelectWithAdapt
 
diff --git a/tests/neg-custom-args/captures/capset-bound.scala b/tests/neg-custom-args/captures/capset-bound.scala
index c00f61240dea..80ee3804776f 100644
--- a/tests/neg-custom-args/captures/capset-bound.scala
+++ b/tests/neg-custom-args/captures/capset-bound.scala
@@ -5,7 +5,7 @@ class IO
 case class File(io: IO^)
 
 def test(io1: IO^, io2: IO^) =
-  def f[C >: CapSet^{io1} <: CapSet^](file: File^{C^}) = ???
+  def f[C >: CapSet^{io1} <: CapSet^](file: File^{C}) = ???
   val f1: File^{io1} = ???
   val f2: File^{io2} = ???
   val f3: File^{io1, io2} = ???
diff --git a/tests/neg-custom-args/captures/capset-bound2.scala b/tests/neg-custom-args/captures/capset-bound2.scala
index 679606f0e43c..4cee6b244de7 100644
--- a/tests/neg-custom-args/captures/capset-bound2.scala
+++ b/tests/neg-custom-args/captures/capset-bound2.scala
@@ -2,7 +2,7 @@ import caps.*
 
 class IO
 
-def f[C^](io: IO^{C^}) = ???
+def f[C^](io: IO^{C}) = ???
 
 def test =
   f[CapSet](???)
@@ -10,4 +10,3 @@ def test =
   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
index 540216852a43..44720b68ff84 100644
--- a/tests/neg-custom-args/captures/capset-members.scala
+++ b/tests/neg-custom-args/captures/capset-members.scala
@@ -3,7 +3,7 @@ import caps.*
 trait Abstract[X^]:
   type C >: X <: CapSet^
   // Don't test the return type using Unit, because it is a pure type.
-  def boom(): AnyRef^{C^}
+  def boom(): AnyRef^{C}
 
 class Concrete extends Abstract[CapSet^{}]:
   type C = CapSet^{}
@@ -27,4 +27,3 @@ class Concrete5(a: AnyRef^, b: AnyRef^) extends Abstract[CapSet^{a}]:
 
 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/capture-parameters.scala b/tests/neg-custom-args/captures/capture-parameters.scala
index d59305ae0cb8..d9288a062ded 100644
--- a/tests/neg-custom-args/captures/capture-parameters.scala
+++ b/tests/neg-custom-args/captures/capture-parameters.scala
@@ -2,8 +2,7 @@ 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
+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
diff --git a/tests/neg-custom-args/captures/capture-poly.scala b/tests/neg-custom-args/captures/capture-poly.scala
index 88989b418726..9276eab0342f 100644
--- a/tests/neg-custom-args/captures/capture-poly.scala
+++ b/tests/neg-custom-args/captures/capture-poly.scala
@@ -5,8 +5,8 @@ trait Foo extends Capability
 trait CaptureSet:
   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
+def capturePoly[C^](a: Foo^{C}): Foo^{C} = a
+def capturePoly2(c: CaptureSet)(a: Foo^{c.C}): Foo^{c.C} = a
 
 def test =
   val x: Foo^ = ???
@@ -15,8 +15,8 @@ def test =
   object X extends CaptureSet:
     type C = CapSet^{x}
 
-  val z1: Foo^{X.C^} = x
-  val z2: Foo^{X.C^} = y // error
+  val z1: Foo^{X.C} = x
+  val z2: Foo^{X.C} = y // error
 
   val z3: Foo^{x} = capturePoly(x)
   val z4: Foo^{x} = capturePoly(y) // error
diff --git a/tests/neg-custom-args/captures/capture-vars-subtyping.scala b/tests/neg-custom-args/captures/capture-vars-subtyping.scala
index 1986a0aa33fc..c0356bb0873f 100644
--- a/tests/neg-custom-args/captures/capture-vars-subtyping.scala
+++ b/tests/neg-custom-args/captures/capture-vars-subtyping.scala
@@ -3,32 +3,32 @@ import caps.*
 
 def test[C^] =
   val a: C = ???
-  val b: CapSet^{C^} = a
+  val b: CapSet^{C} = a
   val c: C = b
-  val d: CapSet^{C^, c} = a
+  val d: CapSet^{C, c} = a
 
 // TODO: make "CapSet-ness" of type variables somehow contagious?
 // Then we don't have to spell out the bounds explicitly...
 def testTrans[C^, D >: CapSet <: C, E >: CapSet <: D, F >: C <: CapSet^] =
   val d1: D = ???
-  val d2: CapSet^{D^} = d1
+  val d2: CapSet^{D} = d1
   val d3: D = d2
   val e1: E = ???
-  val e2: CapSet^{E^} = e1
+  val e2: CapSet^{E} = e1
   val e3: E = e2
   val d4: D = e1
   val c1: C = d1
   val c2: C = e1
   val f1: F = c1
-  val d_e_f1: CapSet^{D^,E^,F^} = d1
-  val d_e_f2: CapSet^{D^,E^,F^} = e1
-  val d_e_f3: CapSet^{D^,E^,F^} = f1
+  val d_e_f1: CapSet^{D,E,F} = d1
+  val d_e_f2: CapSet^{D,E,F} = e1
+  val d_e_f3: CapSet^{D,E,F} = f1
   val f2: F = d_e_f1
   val c3: C = d_e_f1 // error
   val c4: C = f1     // error
   val e4: E = f1     // error
   val e5: E = d1     // error
-  val c5: CapSet^{C^} = e1
+  val c5: CapSet^{C} = e1
 
 
 trait A[+T]
@@ -37,12 +37,12 @@ trait B[-C]
 
 def testCong[C^, D^] =
   val a: A[C] = ???
-  val b: A[CapSet^{C^}] = a
-  val c: A[CapSet^{D^}] = a // error
-  val d: A[CapSet^{C^,D^}] = a
+  val b: A[CapSet^{C}] = a
+  val c: A[CapSet^{D}] = a // error
+  val d: A[CapSet^{C,D}] = a
   val e: A[C] = d // error
   val f: B[C] = ???
-  val g: B[CapSet^{C^}] = f
+  val g: B[CapSet^{C}] = f
   val h: B[C] = g
-  val i: B[CapSet^{C^,D^}] = h // error
+  val i: B[CapSet^{C,D}] = h // error
   val j: B[C] = i
diff --git a/tests/neg-custom-args/captures/capture-vars-subtyping2.scala b/tests/neg-custom-args/captures/capture-vars-subtyping2.scala
index 205451ee41ed..0a3d776227cb 100644
--- a/tests/neg-custom-args/captures/capture-vars-subtyping2.scala
+++ b/tests/neg-custom-args/captures/capture-vars-subtyping2.scala
@@ -10,32 +10,32 @@ trait BoundsTest:
 
   def testTransMixed[A^,
                     B >: CapSet <: A,
-                    C >: CapSet <: CapSet^{B^},
+                    C >: CapSet <: CapSet^{B},
                     D >: CapSet <: C,
-                    E >: CapSet <: CapSet^{D^},
-                    F >: CapSet <: CapSet^{A^,b},
-                    X >: CapSet <: CapSet^{F^,D^},
-                    Y >: CapSet^{F^} <: CapSet^{F^,A^,b},
-                    Z >: CapSet^{b} <: CapSet^{b,Y^}] =
+                    E >: CapSet <: CapSet^{D},
+                    F >: CapSet <: CapSet^{A,b},
+                    X >: CapSet <: CapSet^{F,D},
+                    Y >: CapSet^{F} <: CapSet^{F,A,b},
+                    Z >: CapSet^{b} <: CapSet^{b,Y}] =
     val e: E = ???
-    val e2: CapSet^{E^} = e
+    val e2: CapSet^{E} = e
     val ed: D = e
-    val ed2: CapSet^{D^} = e
+    val ed2: CapSet^{D} = e
     val ec: C = e
-    val ec2: CapSet^{C^} = e
+    val ec2: CapSet^{C} = e
     val eb: B = e
-    val eb2: CapSet^{B^} = e
+    val eb2: CapSet^{B} = e
     val ea: A = e
-    val ea2: CapSet^{A^} = e
+    val ea2: CapSet^{A} = e
     val ex: X = e            // error
-    val ex2: CapSet^{X^} = e // error
+    val ex2: CapSet^{X} = e // error
     val f: F = ???
-    val f2: CapSet^{F^} = f
+    val f2: CapSet^{F} = f
     val y: Y = f
-    val y2: CapSet^{Y^} = f
+    val y2: CapSet^{Y} = f
     val cb: CapSet^{b} = ???
     val z: Z = cb
-    val z2: CapSet^{Z^} = cb
+    val z2: CapSet^{Z} = cb
 
   def callTransMixed =
     val x, y, z: Bar^ = ???
diff --git a/tests/neg-custom-args/captures/cc-poly-1.scala b/tests/neg-custom-args/captures/cc-poly-1.scala
index 580b124bc8f3..b205b9b25246 100644
--- a/tests/neg-custom-args/captures/cc-poly-1.scala
+++ b/tests/neg-custom-args/captures/cc-poly-1.scala
@@ -6,7 +6,7 @@ object Test:
   class C extends Capability
   class D
 
-  def f[X^](x: D^{X^}): D^{X^} = x
+  def f[X^](x: D^{X}): D^{X} = x
 
   def test(c1: C, c2: C) =
     f[Any](D()) // error
diff --git a/tests/neg-custom-args/captures/cc-poly-2.scala b/tests/neg-custom-args/captures/cc-poly-2.scala
index c9249ba59437..8fb590f4f769 100644
--- a/tests/neg-custom-args/captures/cc-poly-2.scala
+++ b/tests/neg-custom-args/captures/cc-poly-2.scala
@@ -6,7 +6,7 @@ object Test:
   class C extends Capability
   class D
 
-  def f[X^](x: D^{X^}): D^{X^} = x
+  def f[X^](x: D^{X}): D^{X} = x
 
   def test(c1: C, c2: C) =
     val d: D^ = D()
diff --git a/tests/neg-custom-args/captures/cc-poly-source.scala b/tests/neg-custom-args/captures/cc-poly-source.scala
index e08ea36a6fc9..ec98c40a4fa9 100644
--- a/tests/neg-custom-args/captures/cc-poly-source.scala
+++ b/tests/neg-custom-args/captures/cc-poly-source.scala
@@ -10,11 +10,11 @@ import caps.use
   class Listener
 
   class Source[X^]:
-    private var listeners: Set[Listener^{X^}] = Set.empty
-    def register(x: Listener^{X^}): Unit =
+    private var listeners: Set[Listener^{X}] = Set.empty
+    def register(x: Listener^{X}): Unit =
       listeners += x
 
-    def allListeners: Set[Listener^{X^}] = listeners
+    def allListeners: Set[Listener^{X}] = listeners
 
   def test1(lbl1: Label^, lbl2: Label^) =
     val src = Source[CapSet^{lbl1, lbl2}]
diff --git a/tests/neg-custom-args/captures/i21313.scala b/tests/neg-custom-args/captures/i21313.scala
index 01bedb10aefd..4b6d16c4da88 100644
--- a/tests/neg-custom-args/captures/i21313.scala
+++ b/tests/neg-custom-args/captures/i21313.scala
@@ -6,7 +6,7 @@ trait Async:
 def foo(x: Async) = x.await(???) // error
 
 trait Source[+T, Cap^]:
-  final def await(using ac: Async^{Cap^}) = ac.await[T, Cap](this) // Contains[Cap, ac] is assured because {ac} <: Cap.
+  final def await(using ac: Async^{Cap}) = ac.await[T, Cap](this) // Contains[Cap, ac] is assured because {ac} <: Cap.
 
 def test(using ac1: Async^, ac2: Async^, x: String) =
   val src1 = new Source[Int, CapSet^{ac1}] {}
diff --git a/tests/neg-custom-args/captures/i21347.scala b/tests/neg-custom-args/captures/i21347.scala
index 54fe859caedd..2e37511f053c 100644
--- a/tests/neg-custom-args/captures/i21347.scala
+++ b/tests/neg-custom-args/captures/i21347.scala
@@ -1,6 +1,6 @@
 import language.experimental.captureChecking
 
-def runOps[C^](ops: List[() ->{C^} Unit]): Unit =
+def runOps[C^](ops: List[() ->{C} Unit]): Unit =
   ops.foreach: op => // error
     op()
 
diff --git a/tests/neg-custom-args/captures/i21868.scala b/tests/neg-custom-args/captures/i21868.scala
index 876b68ac90a4..de6a9b64b78b 100644
--- a/tests/neg-custom-args/captures/i21868.scala
+++ b/tests/neg-custom-args/captures/i21868.scala
@@ -2,11 +2,11 @@ import caps.*
 
 trait AbstractWrong:
   type C <: CapSet
-  def f(): Unit^{C^} // error
+  def f(): Unit^{C} // error
 
 trait Abstract1:
   type C >: CapSet <: CapSet^
-  def f(): Unit^{C^}
+  def f(): Unit^{C}
 
 // class Abstract2:
 //   type C^
diff --git a/tests/neg-custom-args/captures/i21868b.scala b/tests/neg-custom-args/captures/i21868b.scala
index 70f4e9c9d59c..5cff4e3fac2e 100644
--- a/tests/neg-custom-args/captures/i21868b.scala
+++ b/tests/neg-custom-args/captures/i21868b.scala
@@ -7,7 +7,7 @@ class File
 
 trait Abstract:
   type C >: CapSet <: CapSet^
-  def f(file: File^{C^}): Unit
+  def f(file: File^{C}): Unit
 
 class Concrete1 extends Abstract:
   type C = CapSet
@@ -23,7 +23,7 @@ class Concrete3(io: IO^) extends Abstract:
 
 trait Abstract2(tracked val io: IO^):
   type C >: CapSet <: CapSet^{io}
-  def f(file: File^{C^}): Unit
+  def f(file: File^{C}): Unit
 
 class Concrete4(io: IO^) extends Abstract2(io):
   type C = CapSet
@@ -35,7 +35,7 @@ class Concrete5(io1: IO^, io2: IO^) extends Abstract2(io1):
 
 trait Abstract3[X^]:
   type C >: CapSet <: X
-  def f(file: File^{C^}): Unit
+  def f(file: File^{C}): Unit
 
 class Concrete6(io: IO^) extends Abstract3[CapSet^{io}]:
   type C = CapSet
diff --git a/tests/neg-custom-args/captures/polyCaptures.check b/tests/neg-custom-args/captures/polyCaptures.check
index 8173828b7bc8..08ebaf1c63ee 100644
--- a/tests/neg-custom-args/captures/polyCaptures.check
+++ b/tests/neg-custom-args/captures/polyCaptures.check
@@ -1,8 +1,8 @@
 -- Error: tests/neg-custom-args/captures/polyCaptures.scala:4:22 -------------------------------------------------------
-4 |val runOpsCheck: [C^] -> (ops: List[() ->{C^} Unit]) ->{C^} Unit = runOps  // error
+4 |val runOpsCheck: [C^] -> (ops: List[() ->{C} Unit]) ->{C} Unit = runOps  // error
   |                      ^
   |          Implementation restriction: polymorphic function types cannot wrap function types that have capture sets
 -- Error: tests/neg-custom-args/captures/polyCaptures.scala:5:23 -------------------------------------------------------
-5 |val runOpsCheck2: [C^] => (ops: List[() ->{C^} Unit]) ->{C^} Unit = runOps // error
+5 |val runOpsCheck2: [C^] => (ops: List[() ->{C} Unit]) ->{C} Unit = runOps // error
   |                       ^
   |          Implementation restriction: polymorphic function types cannot wrap function types that have capture sets
diff --git a/tests/neg-custom-args/captures/polyCaptures.scala b/tests/neg-custom-args/captures/polyCaptures.scala
index 776af95e5dcf..eb8e50f0b997 100644
--- a/tests/neg-custom-args/captures/polyCaptures.scala
+++ b/tests/neg-custom-args/captures/polyCaptures.scala
@@ -1,7 +1,7 @@
 class Box[X](val elem: X)
 
-val runOps = [C^] => (b: Box[() ->{C^} Unit]) => b.elem()
-val runOpsCheck: [C^] -> (ops: List[() ->{C^} Unit]) ->{C^} Unit = runOps  // error
-val runOpsCheck2: [C^] => (ops: List[() ->{C^} Unit]) ->{C^} Unit = runOps // error
+val runOps = [C^] => (b: Box[() ->{C} Unit]) => b.elem()
+val runOpsCheck: [C^] -> (ops: List[() ->{C} Unit]) ->{C} Unit = runOps  // error
+val runOpsCheck2: [C^] => (ops: List[() ->{C} Unit]) ->{C} Unit = runOps // error
 
 
diff --git a/tests/neg-custom-args/captures/use-capset.check b/tests/neg-custom-args/captures/use-capset.check
index 4897698e336d..70b63e87d792 100644
--- a/tests/neg-custom-args/captures/use-capset.check
+++ b/tests/neg-custom-args/captures/use-capset.check
@@ -1,8 +1,8 @@
--- 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
+-- Error: tests/neg-custom-args/captures/use-capset.scala:5:49 ---------------------------------------------------------
+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:11:22 -----------------------------------
 11 |  val _: () -> Unit = h // error: should be ->{io}
    |                      ^
diff --git a/tests/neg-custom-args/captures/use-capset.scala b/tests/neg-custom-args/captures/use-capset.scala
index 74288d616396..4f2c239247e6 100644
--- a/tests/neg-custom-args/captures/use-capset.scala
+++ b/tests/neg-custom-args/captures/use-capset.scala
@@ -1,10 +1,10 @@
 import caps.{use, CapSet}
 
-def f[C^](@use xs: List[Object^{C^}]): Unit = ???
+def f[C^](@use xs: List[Object^{C}]): Unit = ???
 
-private def g[C^] = (xs: List[Object^{C^}]) => xs.head // error
+private def g[C^] = (xs: List[Object^{C}]) => xs.head // error
 
-private def g2[@use C^] = (xs: List[Object^{C^}]) => xs.head // ok
+private def g2[@use C^] = (xs: List[Object^{C}]) => xs.head // ok
 
 def test(io: Object^)(@use xs: List[Object^{io}]): Unit =
   val h = () => f(xs)
diff --git a/tests/pos-custom-args/captures/cc-poly-1.scala b/tests/pos-custom-args/captures/cc-poly-1.scala
index ed32d94f7a99..e423d94d4000 100644
--- a/tests/pos-custom-args/captures/cc-poly-1.scala
+++ b/tests/pos-custom-args/captures/cc-poly-1.scala
@@ -7,9 +7,9 @@ import caps.{CapSet, Capability}
   class C extends Capability
   class D
 
-  def f[X^](x: D^{X^}): D^{X^} = x
-  def g[X^](x: D^{X^}, y: D^{X^}): D^{X^} = x
-  def h[X^](): D^{X^} = ???
+  def f[X^](x: D^{X}): D^{X} = x
+  def g[X^](x: D^{X}, y: D^{X}): D^{X} = x
+  def h[X^](): D^{X} = ???
 
   def test(c1: C, c2: C) =
     val d: D^{c1, c2} = D()
diff --git a/tests/pos-custom-args/captures/cc-poly-source-capability.scala b/tests/pos-custom-args/captures/cc-poly-source-capability.scala
index 6f987658923c..1208649193af 100644
--- a/tests/pos-custom-args/captures/cc-poly-source-capability.scala
+++ b/tests/pos-custom-args/captures/cc-poly-source-capability.scala
@@ -12,11 +12,11 @@ import caps.use
   class Listener
 
   class Source[X^]:
-    private var listeners: Set[Listener^{X^}] = Set.empty
-    def register(x: Listener^{X^}): Unit =
+    private var listeners: Set[Listener^{X}] = Set.empty
+    def register(x: Listener^{X}): Unit =
       listeners += x
 
-    def allListeners: Set[Listener^{X^}] = listeners
+    def allListeners: Set[Listener^{X}] = listeners
 
   def test1(async1: Async, @use others: List[Async]) =
     val src = Source[CapSet^{async1, others*}]
diff --git a/tests/pos-custom-args/captures/cc-poly-varargs.scala b/tests/pos-custom-args/captures/cc-poly-varargs.scala
index 8bd0dc89bc7a..13e4b276df5a 100644
--- a/tests/pos-custom-args/captures/cc-poly-varargs.scala
+++ b/tests/pos-custom-args/captures/cc-poly-varargs.scala
@@ -1,13 +1,13 @@
 abstract class Source[+T, Cap^]
 
 extension[T, Cap^](src: Source[T, Cap]^)
-  def transformValuesWith[U](f: (T -> U)^{Cap^}): Source[U, Cap]^{src, f} = ???
+  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 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^} =
+    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)
diff --git a/tests/pos-custom-args/captures/gears-problem-poly.scala b/tests/pos-custom-args/captures/gears-problem-poly.scala
index fdbcf37a35a6..f7632bce4124 100644
--- a/tests/pos-custom-args/captures/gears-problem-poly.scala
+++ b/tests/pos-custom-args/captures/gears-problem-poly.scala
@@ -7,8 +7,8 @@ trait Future[+T]:
 trait Channel[+T]:
   def read(): Ok[T]
 
-class Collector[T, C^](val futures: Seq[Future[T]^{C^}]):
-  val results: Channel[Future[T]^{C^}] = ???
+class Collector[T, C^](val futures: Seq[Future[T]^{C}]):
+  val results: Channel[Future[T]^{C}] = ???
 end Collector
 
 class Result[+T, +E]:
@@ -17,10 +17,10 @@ class Result[+T, +E]:
 case class Err[+E](e: E) extends Result[Nothing, E]
 case class Ok[+T](x: T) extends Result[T, Nothing]
 
-extension [T, C^](@use fs: Seq[Future[T]^{C^}])
+extension [T, C^](@use fs: Seq[Future[T]^{C}])
   def awaitAllPoly =
     val collector = Collector(fs)
-    val fut: Future[T]^{C^} = collector.results.read().get
+    val fut: Future[T]^{C} = collector.results.read().get
 
 extension [T](@use fs: Seq[Future[T]^])
   def awaitAll = fs.awaitAllPoly
diff --git a/tests/pos-custom-args/captures/i21313.scala b/tests/pos-custom-args/captures/i21313.scala
index b388b6487cb5..e55bf9c7ce62 100644
--- a/tests/pos-custom-args/captures/i21313.scala
+++ b/tests/pos-custom-args/captures/i21313.scala
@@ -3,17 +3,17 @@ import caps.CapSet
 trait Async:
   def await[T, Cap^](using caps.Contains[Cap, this.type])(src: Source[T, Cap]^): T =
     val x: Async^{this} = ???
-    val y: Async^{Cap^} = x
+    val y: Async^{Cap} = x
     val ac: Async^ = ???
     def f(using caps.Contains[Cap, ac.type]) =
       val x2: Async^{this} = ???
-      val y2: Async^{Cap^} = x2
+      val y2: Async^{Cap} = x2
       val x3: Async^{ac} = ???
-      val y3: Async^{Cap^} = x3
+      val y3: Async^{Cap} = x3
     ???
 
 trait Source[+T, Cap^]:
-  final def await(using ac: Async^{Cap^}) = ac.await[T, Cap](this) // Contains[Cap, ac] is assured because {ac} <: Cap.
+  final def await(using ac: Async^{Cap}) = ac.await[T, Cap](this) // Contains[Cap, ac] is assured because {ac} <: Cap.
 
 def test(using ac1: Async^, ac2: Async^, x: String) =
   val src1 = new Source[Int, CapSet^{ac1}] {}
diff --git a/tests/pos-custom-args/captures/i21347.scala b/tests/pos-custom-args/captures/i21347.scala
index a965b7e4f26b..9dbb8b154cfb 100644
--- a/tests/pos-custom-args/captures/i21347.scala
+++ b/tests/pos-custom-args/captures/i21347.scala
@@ -4,7 +4,7 @@ import language.experimental.captureChecking
 
 class Box[Cap^] {}
 
-def run[Cap^](f: Box[Cap]^{Cap^} => Unit): Box[Cap]^{Cap^} = ???
+def run[Cap^](f: Box[Cap]^{Cap} => Unit): Box[Cap]^{Cap} = ???
 
 def main() =
   val b = run(_ => ())
diff --git a/tests/pos-custom-args/captures/i21507.scala b/tests/pos-custom-args/captures/i21507.scala
index bb80dafb3b45..4267795d3a41 100644
--- a/tests/pos-custom-args/captures/i21507.scala
+++ b/tests/pos-custom-args/captures/i21507.scala
@@ -1,10 +1,10 @@
 import language.experimental.captureChecking
 
 trait Box[Cap^]:
-  def store(f: (() -> Unit)^{Cap^}): Unit
+  def store(f: (() -> Unit)^{Cap}): Unit
 
-def run[Cap^](f: Box[Cap]^{Cap^} => Unit): Box[Cap]^{Cap^} =
+def run[Cap^](f: Box[Cap]^{Cap} => Unit): Box[Cap]^{Cap} =
   new Box[Cap]:
-    private var item: () ->{Cap^} Unit = () => ()
-    def store(f: () ->{Cap^} Unit): Unit =
+    private var item: () ->{Cap} Unit = () => ()
+    def store(f: () ->{Cap} Unit): Unit =
       item = f  // was error, now ok
diff --git a/tests/pos-custom-args/captures/setup/a_1.scala b/tests/pos-custom-args/captures/setup/a_1.scala
index 21afde8be3ea..3a6ec7ffa773 100644
--- a/tests/pos-custom-args/captures/setup/a_1.scala
+++ b/tests/pos-custom-args/captures/setup/a_1.scala
@@ -3,4 +3,4 @@ import language.experimental.captureChecking
 import scala.caps.CapSet
 
 trait A:
-  def f[C^](x: AnyRef^{C^}): Unit
+  def f[C^](x: AnyRef^{C}): Unit
diff --git a/tests/pos-custom-args/captures/setup/b_1.scala b/tests/pos-custom-args/captures/setup/b_1.scala
index d5ba925970ba..70c72723c84c 100644
--- a/tests/pos-custom-args/captures/setup/b_1.scala
+++ b/tests/pos-custom-args/captures/setup/b_1.scala
@@ -2,4 +2,4 @@ import language.experimental.captureChecking
 import scala.caps.CapSet
 
 class B extends A:
-  def f[C^](x: AnyRef^{C^}): Unit = ???
+  def f[C^](x: AnyRef^{C}): Unit = ???
diff --git a/tests/pos-custom-args/captures/setup/b_2.scala b/tests/pos-custom-args/captures/setup/b_2.scala
index d5ba925970ba..70c72723c84c 100644
--- a/tests/pos-custom-args/captures/setup/b_2.scala
+++ b/tests/pos-custom-args/captures/setup/b_2.scala
@@ -2,4 +2,4 @@ import language.experimental.captureChecking
 import scala.caps.CapSet
 
 class B extends A:
-  def f[C^](x: AnyRef^{C^}): Unit = ???
+  def f[C^](x: AnyRef^{C}): Unit = ???

From b305a5a04f1f8eaf5041e0e33527a9196a109913 Mon Sep 17 00:00:00 2001
From: noti0na1 <noti0na1@users.noreply.github.com>
Date: Wed, 5 Mar 2025 16:52:00 +0100
Subject: [PATCH 02/17] Tight the condition for retrying `InCaptureSet`

---
 compiler/src/dotty/tools/dotc/typer/Typer.scala | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index 3ca3afef3315..6ecc9d9cdaa5 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -715,7 +715,7 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
         && ctx.owner.owner.unforcedDecls.lookup(tree.name).exists
     then // we are in the arguments of a this(...) constructor call
       errorTree(tree, em"$tree is not accessible from constructor arguments")
-    else if ctx.mode.is(Mode.InCaptureSet) then
+    else if name.isTermName && ctx.mode.is(Mode.InCaptureSet) then
       // If we are in a capture set and the identifier is not a term name,
       // try to type it with the same name but as a type
       typed(untpd.makeCapsOf(untpd.cpy.Ident(tree)(name.toTypeName)), pt)
@@ -927,7 +927,7 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
     // Otherwise, if we are in a capture set, try to type it as a capture variable
     // reference (as selecting a type name).
     def trySelectTypeInCaptureSet() =
-      if ctx.mode.is(Mode.InCaptureSet) && tree0.name.isTypeName then
+      if tree0.name.isTermName && ctx.mode.is(Mode.InCaptureSet) then
         typedSelectWithAdapt(untpd.cpy.Select(tree0)(qual, tree0.name.toTypeName), pt, qual)
       else EmptyTree
 

From 8b9ecf48c66d025212fec7f14dab5312fff2af0a Mon Sep 17 00:00:00 2001
From: noti0na1 <noti0na1@users.noreply.github.com>
Date: Wed, 5 Mar 2025 16:55:04 +0100
Subject: [PATCH 03/17] Forget to reuse the bit

---
 compiler/src/dotty/tools/dotc/core/Mode.scala | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/Mode.scala b/compiler/src/dotty/tools/dotc/core/Mode.scala
index e0ab4571667c..571a786e9106 100644
--- a/compiler/src/dotty/tools/dotc/core/Mode.scala
+++ b/compiler/src/dotty/tools/dotc/core/Mode.scala
@@ -97,10 +97,10 @@ object Mode {
    *  Since this mode is only used during annotation typing,
    *  we can reuse the value of `ImplicitExploration` to save bits.
    */
-  val InCaptureSet: Mode = newMode(13, "InCaptureSet")
+  val InCaptureSet: Mode = ImplicitExploration
 
   /** We are currently unpickling Scala2 info */
-  val Scala2Unpickling: Mode = newMode(14, "Scala2Unpickling")
+  val Scala2Unpickling: Mode = newMode(13, "Scala2Unpickling")
 
   /** Signifies one of two possible situations:
    *   1. We are currently checking bounds to be non-empty, so we should not

From a36ca952f539f7ebcadd4fbecaa9f04f0175d093 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Oliver=20Bra=C4=8Devac?= <bracevac@users.noreply.github.com>
Date: Mon, 10 Mar 2025 00:45:35 +0100
Subject: [PATCH 04/17] Change syntax of cap parameters and members

`cap` is now a soft modifier and we abolish
separate cap lists.
---
 compiler/src/dotty/tools/dotc/ast/untpd.scala |  15 +-
 .../src/dotty/tools/dotc/core/Flags.scala     |   3 +
 .../src/dotty/tools/dotc/core/StdNames.scala  |   1 +
 .../dotty/tools/dotc/parsing/Parsers.scala    | 191 +++++++++++++++---
 .../dotty/tools/dotc/parsing/Scanners.scala   |   3 +-
 .../tools/dotc/reporting/ErrorMessageID.scala |   1 +
 .../dotty/tools/dotc/reporting/messages.scala |  17 ++
 .../captures/capset-members.scala             |  26 +--
 .../captures/capset-members2.check            |   4 +
 .../captures/capset-members2.scala            |   5 +
 .../captures/capset-members3.check            |   6 +
 .../captures/capset-members3.scala            |   5 +
 tests/pending/cap-paramlists8.scala           |  10 +
 .../captures/cap-paramlists.scala             |  23 +++
 .../captures/cap-paramlists2.scala            |   6 +
 .../captures/cap-paramlists3.scala            |  10 +
 .../captures/cap-paramlists4.scala            |   6 +
 .../captures/cap-paramlists5.scala            |   9 +
 .../captures/cap-paramlists6.scala            |  10 +
 .../captures/cap-paramlists7.scala            |  10 +
 .../captures/capset-members.scala             |  25 +++
 21 files changed, 334 insertions(+), 52 deletions(-)
 create mode 100644 tests/neg-custom-args/captures/capset-members2.check
 create mode 100644 tests/neg-custom-args/captures/capset-members2.scala
 create mode 100644 tests/neg-custom-args/captures/capset-members3.check
 create mode 100644 tests/neg-custom-args/captures/capset-members3.scala
 create mode 100644 tests/pending/cap-paramlists8.scala
 create mode 100644 tests/pos-custom-args/captures/cap-paramlists.scala
 create mode 100644 tests/pos-custom-args/captures/cap-paramlists2.scala
 create mode 100644 tests/pos-custom-args/captures/cap-paramlists3.scala
 create mode 100644 tests/pos-custom-args/captures/cap-paramlists4.scala
 create mode 100644 tests/pos-custom-args/captures/cap-paramlists5.scala
 create mode 100644 tests/pos-custom-args/captures/cap-paramlists6.scala
 create mode 100644 tests/pos-custom-args/captures/cap-paramlists7.scala
 create mode 100644 tests/pos-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 145c61584fcc..35a459dba67c 100644
--- a/compiler/src/dotty/tools/dotc/ast/untpd.scala
+++ b/compiler/src/dotty/tools/dotc/ast/untpd.scala
@@ -236,6 +236,8 @@ object untpd extends Trees.Instance[Untyped] with UntypedTreeInfo {
 
     case class Tracked()(implicit @constructorOnly src: SourceFile) extends Mod(Flags.Tracked)
 
+    case class CaptureParam()(implicit @constructorOnly src: SourceFile) extends Mod(Flags.CaptureParam)
+
     /** Used under pureFunctions to mark impure function types `A => B` in `FunctionWithMods` */
     case class Impure()(implicit @constructorOnly src: SourceFile) extends Mod(Flags.Impure)
   }
@@ -534,12 +536,13 @@ object untpd extends Trees.Instance[Untyped] with UntypedTreeInfo {
     TypeApply(capsInternalDot(nme.capsOf), tp :: Nil)
 
   // Capture set variable `[C^]` becomes: `[C >: CapSet <: CapSet^{cap}]`
-  def makeCapsBound()(using Context): TypeBoundsTree =
-    TypeBoundsTree(
-      Select(scalaDot(nme.caps), tpnme.CapSet),
-      makeRetaining(
-        Select(scalaDot(nme.caps), tpnme.CapSet),
-        Nil, tpnme.retainsCap))
+  def makeCapsBound(refsL: List[Tree] = Nil, refsU: List[Tree] = Nil)(using Context): TypeBoundsTree =
+    val lower = refsL match
+      case Nil => Select(scalaDot(nme.caps), tpnme.CapSet)
+      case refsL => makeRetaining(Select(scalaDot(nme.caps), tpnme.CapSet), refsL, tpnme.retains)
+    val upper =
+      makeRetaining(Select(scalaDot(nme.caps), tpnme.CapSet), refsU, if refsU.isEmpty then tpnme.retainsCap else tpnme.retains)
+    TypeBoundsTree(lower, upper)
 
   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/core/Flags.scala b/compiler/src/dotty/tools/dotc/core/Flags.scala
index 57bf870c6b64..9b34bb8fc8e3 100644
--- a/compiler/src/dotty/tools/dotc/core/Flags.scala
+++ b/compiler/src/dotty/tools/dotc/core/Flags.scala
@@ -380,6 +380,9 @@ object Flags {
   /** Tracked modifier for class parameter / a class with some tracked parameters */
   val (Tracked @ _, _, Dependent @ _) = newFlags(46, "tracked")
 
+  /** Cap modifier for capture-set parameters and capture-set members */
+  val (_, _, CaptureParam @ _) = newFlags(47, "cap")
+
   // ------------ Flags following this one are not pickled ----------------------------------
 
   /** Symbol is not a member of its owner */
diff --git a/compiler/src/dotty/tools/dotc/core/StdNames.scala b/compiler/src/dotty/tools/dotc/core/StdNames.scala
index c33c795571e6..29f843a64cb2 100644
--- a/compiler/src/dotty/tools/dotc/core/StdNames.scala
+++ b/compiler/src/dotty/tools/dotc/core/StdNames.scala
@@ -444,6 +444,7 @@ object StdNames {
     val bytes: N                = "bytes"
     val canEqual_ : N           = "canEqual"
     val canEqualAny : N         = "canEqualAny"
+    val cap: N                  = "cap"
     val caps: N                 = "caps"
     val capsOf: N               = "capsOf"
     val captureChecking: N      = "captureChecking"
diff --git a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
index 1f756008d632..c6afa0e6b9ce 100644
--- a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
+++ b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
@@ -35,6 +35,7 @@ import config.SourceVersion.*
 import config.SourceVersion
 import dotty.tools.dotc.config.MigrationVersion
 import dotty.tools.dotc.util.chaining.*
+import dotty.tools.dotc.config.Feature.ccEnabled
 
 object Parsers {
 
@@ -220,6 +221,10 @@ object Parsers {
     def isErased = isIdent(nme.erased) && in.erasedEnabled
     // Are we seeing an `erased` soft keyword that will not be an identifier?
     def isErasedKw = isErased && in.isSoftModifierInParamModifierPosition
+    // Are we seeing a `cap` soft keyword for declaring a capture-set member or at the beginning a capture-variable parameter list?
+    def isCapKw = Feature.ccEnabled && isIdent(nme.cap)
+    // 'cap type' ?
+    def isCapTypeKw = isCapKw && in.lookahead.token == TYPE
     def isSimpleLiteral =
       simpleLiteralTokens.contains(in.token)
       || isIdent(nme.raw.MINUS) && numericLitTokens.contains(in.lookahead.token)
@@ -1917,7 +1922,7 @@ object Parsers {
         refinedTypeRest(atSpan(startOffset(t)) {
           RefinedTypeTree(rejectWildcardType(t), refinement(indentOK = true))
         })
-      else if Feature.ccEnabled && in.isIdent(nme.UPARROW) && isCaptureUpArrow then
+      else if Feature.ccEnabled && in.isIdent(nme.UPARROW) && isCaptureUpArrow then // TODO remove
         atSpan(t.span.start):
           in.nextToken()
           if in.token == LBRACE
@@ -1972,7 +1977,8 @@ object Parsers {
 
     def typeBlockStats(): List[Tree] =
       val tdefs = new ListBuffer[Tree]
-      while in.token == TYPE do tdefs += typeBlockStat()
+      while (in.token == TYPE) do
+        tdefs += typeBlockStat()
       tdefs.toList
 
     /**  TypeBlockStat ::= ‘type’ {nl} TypeDef
@@ -2173,11 +2179,14 @@ object Parsers {
      *    NamesAndTypes     ::=  NameAndType {‘,’ NameAndType}
      *    NameAndType       ::=  id ':' Type
      */
-    def argTypes(namedOK: Boolean, wildOK: Boolean, tupleOK: Boolean): List[Tree] =
-      def argType() =
-        val t = typ()
+    def argTypes(namedOK: Boolean, wildOK: Boolean, tupleOK: Boolean): List[Tree] = //TOOD grammar doc
+      def withWildCard(gen: => Tree) =
+        val t = gen
         if wildOK then t else rejectWildcardType(t)
 
+      def argType() = withWildCard(typ())
+      def argOrCapType() = withWildCard(if in.token == LBRACE then concreteCapsType(captureSet()) else typ())
+
       def namedArgType() =
         atSpan(in.offset):
           val name = ident()
@@ -2188,14 +2197,14 @@ object Parsers {
         atSpan(in.offset):
           val name = ident()
           acceptColon()
-          NamedArg(name, argType())
+          NamedArg(name, argType()) // TODO allow capsets here?
 
-      if namedOK && isIdent && in.lookahead.token == EQUALS then
-        commaSeparated(() => namedArgType())
+      if namedOK && isIdent && in.lookahead.token == EQUALS then // TOOD support for named cap args
+          commaSeparated(() => namedArgType())
       else if tupleOK && isIdent && in.lookahead.isColon && sourceVersion.enablesNamedTuples then
         commaSeparated(() => namedElem())
       else
-        commaSeparated(() => argType())
+        commaSeparated(() => argOrCapType())
     end argTypes
 
     def paramTypeOf(core: () => Tree): Tree =
@@ -2254,7 +2263,7 @@ object Parsers {
         inBraces(refineStatSeq())
 
     /** TypeBounds ::= [`>:' Type] [`<:' Type]
-     *              |  `^`                     -- under captureChecking
+     *              |  `^`                     -- under captureChecking TODO remove
      */
     def typeBounds(): TypeBoundsTree =
       atSpan(in.offset):
@@ -2264,10 +2273,29 @@ object Parsers {
         else
           TypeBoundsTree(bound(SUPERTYPE), bound(SUBTYPE))
 
+    /** CaptureSetBounds ::= [`>:' CaptureSetOrRef ] [`<:' CaptureSetOrRef ] --- under captureChecking
+     */
+    def captureSetBounds(): TypeBoundsTree =
+      atSpan(in.offset):
+          TypeBoundsTree(capsBound(SUPERTYPE), capsBound(SUBTYPE))
+
     private def bound(tok: Int): Tree =
       if (in.token == tok) { in.nextToken(); toplevelTyp() }
       else EmptyTree
 
+    private def capsBound(refs: List[Tree], isLowerBound: Boolean = false): Tree =
+      if isLowerBound && refs.isEmpty then // lower bounds with empty capture sets become a pure CapSet
+        Select(scalaDot(nme.caps), tpnme.CapSet)
+      else
+        makeRetaining(Select(scalaDot(nme.caps), tpnme.CapSet), refs, if refs.isEmpty then tpnme.retainsCap else tpnme.retains)
+
+    private def capsBound(tok: Int): Tree =
+      if (in.token == tok) then
+        in.nextToken()
+        capsBound(captureSet(), isLowerBound = tok == SUPERTYPE)
+      else
+        capsBound(Nil, isLowerBound = tok == SUPERTYPE)
+
     /** TypeAndCtxBounds  ::=  TypeBounds [`:` ContextBounds]
      */
     def typeAndCtxBounds(pname: TypeName): Tree = {
@@ -2277,6 +2305,15 @@ object Parsers {
       else atSpan((t.span union cbs.head.span).start) { ContextBounds(t, cbs) }
     }
 
+    /** CaptureSetAndCtxBounds  ::=  CaptureSetBounds [`:` ContextBounds]   -- under captureChecking
+     */
+    def captureSetAndCtxBounds(pname: TypeName): Tree = {
+      val t = captureSetBounds()
+      val cbs = contextBounds(pname)
+      if (cbs.isEmpty) t
+      else atSpan((t.span union cbs.head.span).start) { ContextBounds(t, cbs) }
+    }
+
     /** ContextBound      ::=  Type [`as` id] */
     def contextBound(pname: TypeName): Tree =
       val t = toplevelTyp(inContextBound = true)
@@ -2796,7 +2833,10 @@ object Parsers {
           in.nextToken()
           simpleExprRest(selectorOrMatch(t), location, canApply = true)
         case LBRACKET =>
-          val tapp = atSpan(startOffset(t), in.offset) { TypeApply(t, typeArgs(namedOK = true, wildOK = false)) }
+          val tapp = atSpan(startOffset(t), in.offset) {
+            val args = typeArgs(namedOK = true, wildOK = false)
+            TypeApply(t, args)
+          }
           simpleExprRest(tapp, location, canApply = true)
         case LPAREN | LBRACE | INDENT if canApply =>
           val app = atSpan(startOffset(t), in.offset) { mkApply(t, argumentExprs()) }
@@ -3320,6 +3360,7 @@ object Parsers {
           case nme.tracked => Mod.Tracked()
           case nme.erased if in.erasedEnabled => Mod.Erased()
           case nme.mut if Feature.ccEnabled => Mod.Mut()
+          case nme.cap => Mod.CaptureParam()
         }
     }
 
@@ -3388,7 +3429,7 @@ object Parsers {
      *                  |  opaque
      *  LocalModifier  ::= abstract | final | sealed | open | implicit | lazy | erased |
      *                     inline | transparent | infix |
-     *                     mut                              -- under cc
+     *                     mut | cap                             -- under cc
      */
     def modifiers(allowed: BitSet = modifierTokens, start: Modifiers = Modifiers()): Modifiers = {
       @tailrec
@@ -3477,7 +3518,6 @@ object Parsers {
       recur(numLeadParams, firstClause = true, prevIsTypeClause = false)
     end typeOrTermParamClauses
 
-
     /** ClsTypeParamClause::=  ‘[’ ClsTypeParam {‘,’ ClsTypeParam} ‘]’
      *  ClsTypeParam      ::=  {Annotation} [‘+’ | ‘-’]
      *                         id [HkTypeParamClause] TypeAndCtxBounds
@@ -3502,6 +3542,43 @@ object Parsers {
         in.nextToken()
         ok
 
+      def ensureNoHKParams() = // for cap params
+        if in.token == LBRACKET then
+          syntaxError(em"'cap' parameters cannot have type parameters")
+          in.nextToken()
+
+      def ensureNoVariance() = // for cap params
+        if isIdent(nme.raw.PLUS) || isIdent(nme.raw.MINUS) then
+          syntaxError(em"no `+/-` variance annotation allowed here")
+          in.nextToken()
+
+      def typeOrCapParam(): TypeDef =
+        if isCapKw then
+          in.nextToken()
+          capParam()
+        else typeParam()
+
+      def capParam(): TypeDef = {
+        val start = in.offset
+        var mods = annotsAsMods() | Param
+        if paramOwner.isClass then
+          mods |= PrivateLocal
+        ensureNoVariance() // TODO: in the future, we might want to support variances on capture params, ruled out for now
+        atSpan(start, nameStart) {
+          val name =
+            if paramOwner.acceptsWildcard && in.token == USCORE then
+              in.nextToken()
+              WildcardParamName.fresh().toTypeName
+            else ident().toTypeName
+          ensureNoHKParams()
+          val bounds =
+            if paramOwner.acceptsCtxBounds then captureSetAndCtxBounds(name)
+            else if sourceVersion.enablesNewGivens && paramOwner == ParamOwner.Type then captureSetAndCtxBounds(name)
+            else captureSetBounds()
+          TypeDef(name, bounds).withMods(mods)
+        }
+      }
+
       def typeParam(): TypeDef = {
         val start = in.offset
         var mods = annotsAsMods() | Param
@@ -3525,11 +3602,14 @@ object Parsers {
           TypeDef(name, lambdaAbstract(hkparams, bounds)).withMods(mods)
         }
       }
-      commaSeparated(() => typeParam())
+      commaSeparated(() => typeOrCapParam())
     }
 
     def typeParamClauseOpt(paramOwner: ParamOwner): List[TypeDef] =
-      if (in.token == LBRACKET) typeParamClause(paramOwner) else Nil
+      if (in.token == LBRACKET)
+        typeParamClause(paramOwner)
+      else
+        Nil
 
     /** ContextTypes   ::=  FunArgType {‘,’ FunArgType}
      */
@@ -3871,25 +3951,29 @@ object Parsers {
      *             | var VarDef
      *             | def DefDef
      *             | type {nl} TypeDef
+     *             | cap type {nl} CapDef     -- under capture checking
      *             | TmplDef
      *  EnumCase ::= `case' (id ClassConstr [`extends' ConstrApps]] | ids)
      */
-    def defOrDcl(start: Int, mods: Modifiers): Tree = in.token match {
-      case VAL =>
-        in.nextToken()
-        patDefOrDcl(start, mods)
-      case VAR =>
-        val mod = atSpan(in.skipToken()) { Mod.Var() }
-        val mod1 = addMod(mods, mod)
-        patDefOrDcl(start, mod1)
-      case DEF =>
-        defDefOrDcl(start, in.skipToken(mods))
-      case TYPE =>
-        typeDefOrDcl(start, in.skipToken(mods))
-      case CASE if inEnum =>
-        enumCase(start, mods)
-      case _ =>
-        tmplDef(start, mods)
+    def defOrDcl(start: Int, mods: Modifiers): Tree =
+      in.token match {
+        case VAL =>
+          in.nextToken()
+          patDefOrDcl(start, mods)
+        case VAR =>
+          val mod = atSpan(in.skipToken()) { Mod.Var() }
+          val mod1 = addMod(mods, mod)
+          patDefOrDcl(start, mod1)
+        case DEF =>
+          defDefOrDcl(start, in.skipToken(mods))
+        case TYPE if mods.is(CaptureParam) =>
+          capDefOrDcl(start, in.skipToken(mods))
+        case TYPE =>
+          typeDefOrDcl(start, in.skipToken(mods))
+        case CASE if inEnum =>
+          enumCase(start, mods)
+        case _ =>
+          tmplDef(start, mods)
     }
 
     /** PatDef  ::=  ids [‘:’ Type] [‘=’ Expr]
@@ -4098,6 +4182,43 @@ object Parsers {
       }
     }
 
+    private def concreteCapsType(refs: List[Tree]): Tree =
+      makeRetaining(Select(scalaDot(nme.caps), tpnme.CapSet), refs, tpnme.retains)
+
+    /** CapDef ::=  id CaptureSetAndCtxBounds [‘=’ CaptureSetOrRef]    -- under capture checking
+     */
+    def capDefOrDcl(start: Offset, mods: Modifiers): Tree =
+      newLinesOpt()
+      atSpan(start, nameStart) {
+        val nameIdent = typeIdent()
+        val tname = nameIdent.name.asTypeName
+        if in.token == LBRACKET then syntaxError(em"'cap type' declarations cannot have type parameters")
+
+        def makeCapDef(refs: List[Tree] | Tree): Tree = {
+          val tdef = TypeDef(nameIdent.name.toTypeName,
+                             refs.match
+                                case refs: List[Tree] => concreteCapsType(refs)
+                                case bounds: Tree => bounds)
+
+          if (nameIdent.isBackquoted)
+            tdef.pushAttachment(Backquoted, ())
+          finalizeDef(tdef, mods, start)
+        }
+
+        in.token.match
+          case EQUALS =>
+            in.nextToken()
+            makeCapDef(captureSet())
+          case SUBTYPE | SUPERTYPE | SEMI | NEWLINE | NEWLINES | COMMA | RBRACE | OUTDENT | EOF =>
+            makeCapDef(captureSetAndCtxBounds(tname))
+          case _ if (staged & StageKind.QuotedPattern) != 0
+              || sourceVersion.enablesNewGivens && in.isColon =>
+            makeCapDef(captureSetAndCtxBounds(tname))
+          case _ =>
+            syntaxErrorOrIncomplete(ExpectedCaptureBoundOrEquals(in.token))
+            return EmptyTree // return to avoid setting the span to EmptyTree
+      }
+
     /** TmplDef ::=  ([‘case’] ‘class’ | ‘trait’) ClassDef
      *            |  [‘case’] ‘object’ ObjectDef
      *            |  ‘enum’ EnumDef
@@ -4691,6 +4812,7 @@ object Parsers {
      *                     |  ‘var’ VarDef
      *                     |  ‘def’ DefDef
      *                     |  ‘type’ {nl} TypeDef
+     *                     |  ‘cap’ ‘type’ {nl} CapDef -- under capture checking
      *  (in reality we admit class defs and vars and filter them out afterwards in `checkLegal`)
      */
     def refineStatSeq(): List[Tree] = {
@@ -4716,9 +4838,14 @@ object Parsers {
             fail(em"this kind of definition cannot be a refinement")
 
       while
+        val mods =
+          if isCapTypeKw then // allow `cap type` in refinements
+            in.nextToken()
+            addMod(Modifiers(), Mod.CaptureParam())
+          else Modifiers()
         val dclFound = isDclIntro
         if dclFound then
-          stats ++= checkLegal(defOrDcl(in.offset, Modifiers()))
+          stats ++= checkLegal(defOrDcl(in.offset, mods))
         var what = "declaration"
         if inFunReturnType then what += " (possible cause: missing `=` in front of current method body)"
         statSepOrEnd(stats, noPrevStat = !dclFound, what)
diff --git a/compiler/src/dotty/tools/dotc/parsing/Scanners.scala b/compiler/src/dotty/tools/dotc/parsing/Scanners.scala
index f7050cec41fd..a1969fc2e9c1 100644
--- a/compiler/src/dotty/tools/dotc/parsing/Scanners.scala
+++ b/compiler/src/dotty/tools/dotc/parsing/Scanners.scala
@@ -1212,7 +1212,8 @@ object Scanners {
       && (softModifierNames.contains(name)
         || name == nme.erased && erasedEnabled
         || name == nme.tracked && trackedEnabled
-        || name == nme.mut && Feature.ccEnabled)
+        || name == nme.mut && Feature.ccEnabled
+        || name == nme.cap && Feature.ccEnabled)
 
     def isSoftModifierInModifierPosition: Boolean =
       isSoftModifier && inModifierPosition()
diff --git a/compiler/src/dotty/tools/dotc/reporting/ErrorMessageID.scala b/compiler/src/dotty/tools/dotc/reporting/ErrorMessageID.scala
index 8f8f4676f43b..264ce47cb8ef 100644
--- a/compiler/src/dotty/tools/dotc/reporting/ErrorMessageID.scala
+++ b/compiler/src/dotty/tools/dotc/reporting/ErrorMessageID.scala
@@ -222,6 +222,7 @@ enum ErrorMessageID(val isActive: Boolean = true) extends java.lang.Enum[ErrorMe
   case EnumMayNotBeValueClassesID // errorNumber: 206
   case IllegalUnrollPlacementID // errorNumber: 207
   case ExtensionHasDefaultID // errorNumber: 208
+  case ExpectedCaptureBoundOrEqualsID // errorNumber: 209
 
   def errorNumber = ordinal - 1
 
diff --git a/compiler/src/dotty/tools/dotc/reporting/messages.scala b/compiler/src/dotty/tools/dotc/reporting/messages.scala
index dcd7ed10987b..800b9469d8d8 100644
--- a/compiler/src/dotty/tools/dotc/reporting/messages.scala
+++ b/compiler/src/dotty/tools/dotc/reporting/messages.scala
@@ -1917,6 +1917,23 @@ class ExpectedTypeBoundOrEquals(found: Token)(using Context)
         |"""
 }
 
+class ExpectedCaptureBoundOrEquals(found: Token)(using Context)
+  extends SyntaxMsg(ExpectedCaptureBoundOrEqualsID) {
+  def msg(using Context) = i"${hl("=")}, ${hl(">:")}, or ${hl("<:")} expected, but ${Tokens.showToken(found)} found"
+
+  def explain(using Context) =
+    i"""Capture parameters and abstract captures may be constrained by a capture bound.
+        |Such capture bounds limit the concrete values of the capture variables and possibly
+        |reveal more information about the members of such captures.
+        |
+        |A lower type bound ${hl("B >: A")} expresses that the capture variable ${hl("B")}
+        |refers to a super capture of capture ${hl("A")}.
+        |
+        |An upper capture bound ${hl("T <: A")} declares that capture variable ${hl("T")}
+        |refers to a subcapture of ${hl("A")}.
+        |"""
+}
+
 class ClassAndCompanionNameClash(cls: Symbol, other: Symbol)(using Context)
   extends NamingMsg(ClassAndCompanionNameClashID) {
   def msg(using Context) =
diff --git a/tests/neg-custom-args/captures/capset-members.scala b/tests/neg-custom-args/captures/capset-members.scala
index 44720b68ff84..9d197a206e95 100644
--- a/tests/neg-custom-args/captures/capset-members.scala
+++ b/tests/neg-custom-args/captures/capset-members.scala
@@ -1,29 +1,29 @@
 import caps.*
 
-trait Abstract[X^]:
-  type C >: X <: CapSet^
+trait Abstract[cap X]:
+  cap type C >: {X}
   // 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^{}
+class Concrete extends Abstract[{}]:
+  cap type C = {}
   // TODO: Why do we get error without the return type here?
   def boom(): AnyRef = new Object
 
-class Concrete2 extends Abstract[CapSet^{}]:
-  type C = CapSet^{}
+class Concrete2 extends Abstract[{}]:
+  cap type C = {}
   def boom(): AnyRef^ = new Object // error
 
-class Concrete3 extends Abstract[CapSet^{}]:
+class Concrete3 extends Abstract[{}]:
   def boom(): AnyRef = new Object
 
-class Concrete4(a: AnyRef^) extends Abstract[CapSet^{a}]:
-  type C = CapSet // error
+class Concrete4(a: AnyRef^) extends Abstract[{a}]:
+  cap type C = {} // error
   def boom(): AnyRef^{a} = a // error
 
-class Concrete5(a: AnyRef^, b: AnyRef^) extends Abstract[CapSet^{a}]:
-  type C = CapSet^{a}
+class Concrete5(a: AnyRef^, b: AnyRef^) extends Abstract[{a}]:
+  cap type C = {a}
   def boom(): AnyRef^{b} = b // error
 
-class Concrete6(a: AnyRef^, b: AnyRef^) extends Abstract[CapSet^{a}]:
-  def boom(): AnyRef^{b} = b // error
+class Concrete6(a: AnyRef^, b: AnyRef^) extends Abstract[{a}]:
+  def boom(): AnyRef^{b} = b // error
\ No newline at end of file
diff --git a/tests/neg-custom-args/captures/capset-members2.check b/tests/neg-custom-args/captures/capset-members2.check
new file mode 100644
index 000000000000..6e67ce3d39a3
--- /dev/null
+++ b/tests/neg-custom-args/captures/capset-members2.check
@@ -0,0 +1,4 @@
+-- Error: tests/neg-custom-args/captures/capset-members2.scala:4:12 ----------------------------------------------------
+4 |  cap type C[T] // error
+  |            ^
+  |            'cap type' declarations cannot have type parameters
diff --git a/tests/neg-custom-args/captures/capset-members2.scala b/tests/neg-custom-args/captures/capset-members2.scala
new file mode 100644
index 000000000000..ab8fab3716d8
--- /dev/null
+++ b/tests/neg-custom-args/captures/capset-members2.scala
@@ -0,0 +1,5 @@
+import caps.*
+
+trait Foo:
+  cap type C[T] // error
+
diff --git a/tests/neg-custom-args/captures/capset-members3.check b/tests/neg-custom-args/captures/capset-members3.check
new file mode 100644
index 000000000000..74d3cf82f78e
--- /dev/null
+++ b/tests/neg-custom-args/captures/capset-members3.check
@@ -0,0 +1,6 @@
+-- [E209] Syntax Error: tests/neg-custom-args/captures/capset-members3.scala:4:13 --------------------------------------
+4 |  cap type C _ // error
+  |             ^
+  |             =, >:, or <: expected, but '_' found
+  |
+  | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/capset-members3.scala b/tests/neg-custom-args/captures/capset-members3.scala
new file mode 100644
index 000000000000..02e377a8d553
--- /dev/null
+++ b/tests/neg-custom-args/captures/capset-members3.scala
@@ -0,0 +1,5 @@
+import caps.*
+
+trait Foo:
+  cap type C _ // error
+
diff --git a/tests/pending/cap-paramlists8.scala b/tests/pending/cap-paramlists8.scala
new file mode 100644
index 000000000000..5151629283f6
--- /dev/null
+++ b/tests/pending/cap-paramlists8.scala
@@ -0,0 +1,10 @@
+import language.experimental.captureChecking
+
+trait Ctx[T]
+
+def test =
+  val x: Any^ = ???
+  val y: Any^ = ???
+  object O:
+    val z: Any^ = ???
+  val baz3 = (i: Int) => [cap C, cap D <: {C}, cap E <: {C,x}] => () => [cap F >: {x,y} <: {C,E} : Ctx] => (x: Int) => 1
\ No newline at end of file
diff --git a/tests/pos-custom-args/captures/cap-paramlists.scala b/tests/pos-custom-args/captures/cap-paramlists.scala
new file mode 100644
index 000000000000..c81bcd5b5440
--- /dev/null
+++ b/tests/pos-custom-args/captures/cap-paramlists.scala
@@ -0,0 +1,23 @@
+import language.experimental.captureChecking
+
+trait Ctx[T]
+
+def test =
+  val x: Any^ = ???
+  val y: Any^ = ???
+  object O:
+    val z: Any^ = ???
+  def foo[cap A >: {y} <: {x},
+          cap B,
+          cap C <: {x},
+          cap D : Ctx,
+          cap E <: {C},
+          cap F <: {C},
+          cap G <: {x, y},
+          cap H >: {x} <: {x,y} : Ctx, T, U]()[cap I <: {y, G, H},
+                                               cap J <: {O.z},
+                                               cap K <: {x, O.z},
+                                               cap L <: {x, y, O.z},
+                                               cap M >: {x, y, O.z} <: {C} : Ctx,
+                                               cap N >: {x} <: {x},
+                                               cap O >: {O.z} <: {O.z}] = ???
\ No newline at end of file
diff --git a/tests/pos-custom-args/captures/cap-paramlists2.scala b/tests/pos-custom-args/captures/cap-paramlists2.scala
new file mode 100644
index 000000000000..284fa9c6b3d9
--- /dev/null
+++ b/tests/pos-custom-args/captures/cap-paramlists2.scala
@@ -0,0 +1,6 @@
+import language.experimental.captureChecking
+
+trait Bar:
+  cap type C
+
+def useFoo[cap D](x: Bar { cap type C = {D} } ): Any^{x.C} = ???
\ No newline at end of file
diff --git a/tests/pos-custom-args/captures/cap-paramlists3.scala b/tests/pos-custom-args/captures/cap-paramlists3.scala
new file mode 100644
index 000000000000..ebd3bc171a57
--- /dev/null
+++ b/tests/pos-custom-args/captures/cap-paramlists3.scala
@@ -0,0 +1,10 @@
+import language.experimental.captureChecking
+
+trait Ctx[T]
+
+def test =
+  val x: Any^ = ???
+  val y: Any^ = ???
+  object O:
+    val z: Any^ = ???
+  val bar = [cap C, cap D <: {C}, cap E <: {C,x}, cap F >: {x,y} <: {C,E}] => (x: Int) => 1
\ No newline at end of file
diff --git a/tests/pos-custom-args/captures/cap-paramlists4.scala b/tests/pos-custom-args/captures/cap-paramlists4.scala
new file mode 100644
index 000000000000..16ef9b2ee935
--- /dev/null
+++ b/tests/pos-custom-args/captures/cap-paramlists4.scala
@@ -0,0 +1,6 @@
+import language.experimental.captureChecking
+
+trait Foo[cap U, cap V, cap W]:
+  cap type C = {caps.cap}
+  cap type D = {caps.cap}
+  cap type E >: {V,W} <: {U}
\ No newline at end of file
diff --git a/tests/pos-custom-args/captures/cap-paramlists5.scala b/tests/pos-custom-args/captures/cap-paramlists5.scala
new file mode 100644
index 000000000000..d2599787d5a2
--- /dev/null
+++ b/tests/pos-custom-args/captures/cap-paramlists5.scala
@@ -0,0 +1,9 @@
+import language.experimental.captureChecking
+import language.experimental.namedTypeArguments
+
+def test2 =
+  val x: Any^ = ???
+  def foo[cap A, cap B >: {A}, T](x: Int) = 1
+  foo[{x}, {x}, Int](0)
+ // foo[cap A = {x}, cap B = {x}](0)
+ // foo[cap A = {x}](0)
\ No newline at end of file
diff --git a/tests/pos-custom-args/captures/cap-paramlists6.scala b/tests/pos-custom-args/captures/cap-paramlists6.scala
new file mode 100644
index 000000000000..f230890e8374
--- /dev/null
+++ b/tests/pos-custom-args/captures/cap-paramlists6.scala
@@ -0,0 +1,10 @@
+import language.experimental.captureChecking
+
+trait Ctx[T]
+
+def test =
+  val x: Any^ = ???
+  val y: Any^ = ???
+  object O:
+    val z: Any^ = ???
+  val baz  = () => [cap C, cap D <: {C}, cap E <: {C,x}, cap F >: {x,y} <: {C,E} : Ctx] => (x: Int) => 1
\ No newline at end of file
diff --git a/tests/pos-custom-args/captures/cap-paramlists7.scala b/tests/pos-custom-args/captures/cap-paramlists7.scala
new file mode 100644
index 000000000000..9a46787e7e34
--- /dev/null
+++ b/tests/pos-custom-args/captures/cap-paramlists7.scala
@@ -0,0 +1,10 @@
+import language.experimental.captureChecking
+
+trait Ctx[T]
+
+def test =
+  val x: Any^ = ???
+  val y: Any^ = ???
+  object O:
+    val z: Any^ = ???
+  val baz2 = (i: Int) => [cap C, cap D <: {C}, cap E <: {C,x}, cap F >: {x,y} <: {C,E} : Ctx] => (x: Int) => 1
\ No newline at end of file
diff --git a/tests/pos-custom-args/captures/capset-members.scala b/tests/pos-custom-args/captures/capset-members.scala
new file mode 100644
index 000000000000..eed7f4a2fa15
--- /dev/null
+++ b/tests/pos-custom-args/captures/capset-members.scala
@@ -0,0 +1,25 @@
+import language.experimental.captureChecking
+
+trait Ctx[T]
+
+def test =
+  val x: Any^ = ???
+  val y: Any^ = ???
+  object O:
+    val z: Any^ = ???
+  trait CaptureSet:
+    cap type A >: {y} <: {x}
+    cap type B = {x}
+    cap type C <: {x}
+    cap type D : Ctx
+    cap type E <: {C}
+    cap type F <: {C}
+    cap type G <: {x, y}
+    cap type H >: {x} <: {x,y} : Ctx
+    cap type I = {y, G, H}
+    cap type J = {O.z}
+    cap type K = {x, O.z}
+    cap type L <: {x, y, O.z}
+    cap type M >: {x, y, O.z} <: {C}
+    cap type N >: {x} <: {x}
+    cap type O >: {O.z} <: {O.z}
\ No newline at end of file

From 82ed8f99daf8805b62209144bb55f125a221d27a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Oliver=20Bra=C4=8Devac?= <bracevac@users.noreply.github.com>
Date: Tue, 1 Apr 2025 18:22:01 +0200
Subject: [PATCH 05/17] Fix parsing of argTypes

---
 .../dotty/tools/dotc/parsing/Parsers.scala    | 27 ++++++++++++++-----
 tests/neg-custom-args/captures/i22005.scala   |  6 ++---
 .../captures/cap-paramlists5.scala            | 11 +++++---
 3 files changed, 31 insertions(+), 13 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
index c6afa0e6b9ce..a48ea9b8c1d4 100644
--- a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
+++ b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
@@ -35,7 +35,6 @@ import config.SourceVersion.*
 import config.SourceVersion
 import dotty.tools.dotc.config.MigrationVersion
 import dotty.tools.dotc.util.chaining.*
-import dotty.tools.dotc.config.Feature.ccEnabled
 
 object Parsers {
 
@@ -225,6 +224,15 @@ object Parsers {
     def isCapKw = Feature.ccEnabled && isIdent(nme.cap)
     // 'cap type' ?
     def isCapTypeKw = isCapKw && in.lookahead.token == TYPE
+    // Are the next two tokens 'cap type'?
+    def isCapTypeKwNext = {
+      if Feature.ccEnabled then
+        val lookahead = in.LookaheadScanner()
+        lookahead.nextToken()
+        val res = lookahead.isIdent(nme.cap) && lookahead.lookahead.token == TYPE
+        res
+      else false
+    }
     def isSimpleLiteral =
       simpleLiteralTokens.contains(in.token)
       || isIdent(nme.raw.MINUS) && numericLitTokens.contains(in.lookahead.token)
@@ -232,6 +240,7 @@ object Parsers {
     def isNumericLit = numericLitTokens contains in.token
     def isTemplateIntro = templateIntroTokens contains in.token
     def isDclIntro = dclIntroTokens contains in.token
+    def isDclIntroNext = dclIntroTokens contains in.lookahead.token
     def isStatSeqEnd = in.isNestedEnd || in.token == EOF || in.token == RPAREN
     def mustStartStat = mustStartStatTokens contains in.token
 
@@ -1922,7 +1931,7 @@ object Parsers {
         refinedTypeRest(atSpan(startOffset(t)) {
           RefinedTypeTree(rejectWildcardType(t), refinement(indentOK = true))
         })
-      else if Feature.ccEnabled && in.isIdent(nme.UPARROW) && isCaptureUpArrow then // TODO remove
+      else if Feature.ccEnabled && in.isIdent(nme.UPARROW) && isCaptureUpArrow then
         atSpan(t.span.start):
           in.nextToken()
           if in.token == LBRACE
@@ -2179,13 +2188,19 @@ object Parsers {
      *    NamesAndTypes     ::=  NameAndType {‘,’ NameAndType}
      *    NameAndType       ::=  id ':' Type
      */
-    def argTypes(namedOK: Boolean, wildOK: Boolean, tupleOK: Boolean): List[Tree] = //TOOD grammar doc
-      def withWildCard(gen: => Tree) =
+    def argTypes(namedOK: Boolean, wildOK: Boolean, tupleOK: Boolean): List[Tree] = //TODO grammar doc
+      inline def wildCardCheck(inline gen: Tree): Tree =
         val t = gen
         if wildOK then t else rejectWildcardType(t)
 
-      def argType() = withWildCard(typ())
-      def argOrCapType() = withWildCard(if in.token == LBRACE then concreteCapsType(captureSet()) else typ())
+      def argType() = wildCardCheck:
+        typ()
+
+      def argOrCapType() = wildCardCheck:
+        if Feature.ccEnabled && in.token == LBRACE && !isDclIntroNext && !isCapTypeKwNext then // is this a capture set and not a refinement type?
+          // This case is ambiguous w.r.t. an Object literal {}. But since CC is enabled, we probably expect it to designate the empty set
+          concreteCapsType(captureSet())
+        else typ()
 
       def namedArgType() =
         atSpan(in.offset):
diff --git a/tests/neg-custom-args/captures/i22005.scala b/tests/neg-custom-args/captures/i22005.scala
index 689246d6f835..4d70badcaf5e 100644
--- a/tests/neg-custom-args/captures/i22005.scala
+++ b/tests/neg-custom-args/captures/i22005.scala
@@ -4,6 +4,6 @@ import caps.*
 class IO
 class File(io: IO^)
 
-class Handler[C^]:
-  def f(file: File^): File^{C^} = file // error
-  def g(@consume file: File^{C^}): File^ = file // ok
+class Handler[cap C]:
+  def f(file: File^): File^{C} = file // error
+  def g(@consume file: File^{C}): File^ = file // ok
diff --git a/tests/pos-custom-args/captures/cap-paramlists5.scala b/tests/pos-custom-args/captures/cap-paramlists5.scala
index d2599787d5a2..0460bf85b287 100644
--- a/tests/pos-custom-args/captures/cap-paramlists5.scala
+++ b/tests/pos-custom-args/captures/cap-paramlists5.scala
@@ -3,7 +3,10 @@ import language.experimental.namedTypeArguments
 
 def test2 =
   val x: Any^ = ???
-  def foo[cap A, cap B >: {A}, T](x: Int) = 1
-  foo[{x}, {x}, Int](0)
- // foo[cap A = {x}, cap B = {x}](0)
- // foo[cap A = {x}](0)
\ No newline at end of file
+  def foo[cap A, cap B >: {A}, T, U](x: Int) = 1
+  //foo[{x}, {x}, Int](0) // TODO will not work for {x} in first arg
+  foo[{}, {}, { def bar: Int }, { cap type D = {x} }](0)
+  trait Foo { cap type D }
+  foo[{}, {}, Foo, Foo](0)
+  // foo[cap A = {x}, cap B = {x}](0)
+  // foo[cap A = {x}](0)
\ No newline at end of file

From 468da8729db850ec7eb977bec0195cdce9bf9146 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Oliver=20Bra=C4=8Devac?= <bracevac@users.noreply.github.com>
Date: Tue, 1 Apr 2025 19:29:30 +0200
Subject: [PATCH 06/17] Migrate tests to new syntax

Neg test use-capset revealed that type param
clauses are incorrectly parsed when a capset
parameter has an annotation.
---
 .../dotty/tools/dotc/parsing/Parsers.scala    | 25 ++++++++---------
 .../captures/capset-bound2.scala              |  8 +++---
 .../captures/capture-parameters.scala         |  2 +-
 .../captures/capture-poly.scala               |  6 ++--
 .../captures/capture-vars-subtyping.scala     | 16 +++++------
 .../captures/capture-vars-subtyping2.scala    | 24 ++++++++--------
 .../neg-custom-args/captures/cc-poly-1.scala  |  2 +-
 .../neg-custom-args/captures/cc-poly-2.check  | 10 +++----
 .../neg-custom-args/captures/cc-poly-2.scala  |  4 +--
 .../captures/cc-poly-source.scala             |  6 ++--
 tests/neg-custom-args/captures/i21313.scala   | 10 +++----
 tests/neg-custom-args/captures/i21347.scala   |  2 +-
 tests/neg-custom-args/captures/i21868b.scala  | 28 +++++++++----------
 .../captures/polyCaptures.check               | 12 ++++----
 .../captures/polyCaptures.scala               |  6 ++--
 .../neg-custom-args/captures/use-capset.check | 18 ++++++------
 .../neg-custom-args/captures/use-capset.scala | 11 ++++----
 .../pos-custom-args/captures/cc-poly-1.scala  |  8 +++---
 .../captures/cc-poly-source-capability.scala  |  4 +--
 .../captures/cc-poly-varargs.scala            | 14 +++++-----
 .../captures/gears-problem-poly.scala         |  8 +++---
 tests/pos-custom-args/captures/i21313.scala   | 13 +++++----
 tests/pos-custom-args/captures/i21347.scala   |  4 +--
 tests/pos-custom-args/captures/i21507.scala   |  6 ++--
 tests/pos-custom-args/captures/polycap.scala  |  8 +++---
 .../pos-custom-args/captures/setup/a_1.scala  |  3 +-
 .../pos-custom-args/captures/setup/b_1.scala  |  3 +-
 .../pos-custom-args/captures/setup/b_2.scala  |  3 +-
 28 files changed, 130 insertions(+), 134 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
index a48ea9b8c1d4..562031223751 100644
--- a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
+++ b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
@@ -2278,15 +2278,10 @@ object Parsers {
         inBraces(refineStatSeq())
 
     /** TypeBounds ::= [`>:' Type] [`<:' Type]
-     *              |  `^`                     -- under captureChecking TODO remove
      */
     def typeBounds(): TypeBoundsTree =
       atSpan(in.offset):
-        if in.isIdent(nme.UPARROW) && Feature.ccEnabled then
-          in.nextToken()
-          makeCapsBound()
-        else
-          TypeBoundsTree(bound(SUPERTYPE), bound(SUBTYPE))
+        TypeBoundsTree(bound(SUPERTYPE), bound(SUBTYPE))
 
     /** CaptureSetBounds ::= [`>:' CaptureSetOrRef ] [`<:' CaptureSetOrRef ] --- under captureChecking
      */
@@ -3568,14 +3563,16 @@ object Parsers {
           in.nextToken()
 
       def typeOrCapParam(): TypeDef =
+        val start = in.offset
+        val mods = annotsAsMods() | Param
         if isCapKw then
           in.nextToken()
-          capParam()
-        else typeParam()
+          capParam(start, mods)
+        else typeParam(start, mods)
 
-      def capParam(): TypeDef = {
-        val start = in.offset
-        var mods = annotsAsMods() | Param
+      def capParam(startOffset: Int, mods0: Modifiers): TypeDef = { // TODO grammar doc
+        val start = startOffset
+        var mods = mods0
         if paramOwner.isClass then
           mods |= PrivateLocal
         ensureNoVariance() // TODO: in the future, we might want to support variances on capture params, ruled out for now
@@ -3594,9 +3591,9 @@ object Parsers {
         }
       }
 
-      def typeParam(): TypeDef = {
-        val start = in.offset
-        var mods = annotsAsMods() | Param
+      def typeParam(startOffset: Int, mods0: Modifiers): TypeDef = {
+        val start = startOffset
+        var mods = mods0
         if paramOwner.isClass then
           mods |= PrivateLocal
         if isIdent(nme.raw.PLUS) && checkVarianceOK() then
diff --git a/tests/neg-custom-args/captures/capset-bound2.scala b/tests/neg-custom-args/captures/capset-bound2.scala
index 4cee6b244de7..5148fdf748b2 100644
--- a/tests/neg-custom-args/captures/capset-bound2.scala
+++ b/tests/neg-custom-args/captures/capset-bound2.scala
@@ -2,11 +2,11 @@ import caps.*
 
 class IO
 
-def f[C^](io: IO^{C}) = ???
+def f[cap C](io: IO^{C}) = ???
 
 def test =
-  f[CapSet](???)
-  f[CapSet^{}](???)
-  f[CapSet^](???)
+  f[{}](???)
+  f[{}](???)
+  f[{cap}](???)
   f[Nothing](???) // error
   f[String](???) // error
diff --git a/tests/neg-custom-args/captures/capture-parameters.scala b/tests/neg-custom-args/captures/capture-parameters.scala
index d9288a062ded..ba01ae55d3a8 100644
--- a/tests/neg-custom-args/captures/capture-parameters.scala
+++ b/tests/neg-custom-args/captures/capture-parameters.scala
@@ -2,7 +2,7 @@ import caps.*
 
 class C
 
-def test[X^, Y^, Z >: X <: Y](x: C^{X}, y: C^{Y}, z: C^{Z}) =
+def test[cap X, cap Y, cap 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
diff --git a/tests/neg-custom-args/captures/capture-poly.scala b/tests/neg-custom-args/captures/capture-poly.scala
index 9276eab0342f..ef4860d8090a 100644
--- a/tests/neg-custom-args/captures/capture-poly.scala
+++ b/tests/neg-custom-args/captures/capture-poly.scala
@@ -3,9 +3,9 @@ import caps.*
 trait Foo extends Capability
 
 trait CaptureSet:
-  type C >: CapSet <: CapSet^
+  cap type C
 
-def capturePoly[C^](a: Foo^{C}): Foo^{C} = a
+def capturePoly[cap C](a: Foo^{C}): Foo^{C} = a
 def capturePoly2(c: CaptureSet)(a: Foo^{c.C}): Foo^{c.C} = a
 
 def test =
@@ -13,7 +13,7 @@ def test =
   val y: Foo^ = ???
 
   object X extends CaptureSet:
-    type C = CapSet^{x}
+    cap type C = {x}
 
   val z1: Foo^{X.C} = x
   val z2: Foo^{X.C} = y // error
diff --git a/tests/neg-custom-args/captures/capture-vars-subtyping.scala b/tests/neg-custom-args/captures/capture-vars-subtyping.scala
index c0356bb0873f..b9ee56c10a41 100644
--- a/tests/neg-custom-args/captures/capture-vars-subtyping.scala
+++ b/tests/neg-custom-args/captures/capture-vars-subtyping.scala
@@ -1,7 +1,7 @@
 import language.experimental.captureChecking
 import caps.*
 
-def test[C^] =
+def test[cap C] =
   val a: C = ???
   val b: CapSet^{C} = a
   val c: C = b
@@ -9,7 +9,7 @@ def test[C^] =
 
 // TODO: make "CapSet-ness" of type variables somehow contagious?
 // Then we don't have to spell out the bounds explicitly...
-def testTrans[C^, D >: CapSet <: C, E >: CapSet <: D, F >: C <: CapSet^] =
+def testTrans[cap C, cap D <: {C}, cap E <: {D}, cap F >: {C}] =
   val d1: D = ???
   val d2: CapSet^{D} = d1
   val d3: D = d2
@@ -35,14 +35,14 @@ trait A[+T]
 
 trait B[-C]
 
-def testCong[C^, D^] =
+def testCong[cap C, cap D] =
   val a: A[C] = ???
-  val b: A[CapSet^{C}] = a
-  val c: A[CapSet^{D}] = a // error
-  val d: A[CapSet^{C,D}] = a
+  val b: A[{C}] = a
+  val c: A[{D}] = a // error
+  val d: A[{C,D}] = a
   val e: A[C] = d // error
   val f: B[C] = ???
-  val g: B[CapSet^{C}] = f
+  val g: B[{C}] = f
   val h: B[C] = g
-  val i: B[CapSet^{C,D}] = h // error
+  val i: B[{C,D}] = h // error
   val j: B[C] = i
diff --git a/tests/neg-custom-args/captures/capture-vars-subtyping2.scala b/tests/neg-custom-args/captures/capture-vars-subtyping2.scala
index 0a3d776227cb..b3232cbaafbb 100644
--- a/tests/neg-custom-args/captures/capture-vars-subtyping2.scala
+++ b/tests/neg-custom-args/captures/capture-vars-subtyping2.scala
@@ -8,15 +8,15 @@ trait BoundsTest:
 
   val b: Bar^ = ???
 
-  def testTransMixed[A^,
-                    B >: CapSet <: A,
-                    C >: CapSet <: CapSet^{B},
-                    D >: CapSet <: C,
-                    E >: CapSet <: CapSet^{D},
-                    F >: CapSet <: CapSet^{A,b},
-                    X >: CapSet <: CapSet^{F,D},
-                    Y >: CapSet^{F} <: CapSet^{F,A,b},
-                    Z >: CapSet^{b} <: CapSet^{b,Y}] =
+  def testTransMixed[cap A,
+                     cap B <: {A},
+                     cap C <: {B},
+                     cap D <: {C},
+                     cap E <: {D},
+                     cap F <: {A,b},
+                     cap X <: {F,D},
+                     cap Y >: {F} <: {F,A,b},
+                     cap Z >: {b} <: {b,Y}] =
     val e: E = ???
     val e2: CapSet^{E} = e
     val ed: D = e
@@ -39,6 +39,6 @@ trait BoundsTest:
 
   def callTransMixed =
     val x, y, z: Bar^ = ???
-    testTransMixed[CapSet^{x,y,z}, CapSet^{x,y,z}, CapSet^{x,y,z}, CapSet^{x,y,z}, CapSet^{x,y,z}, CapSet^{x,y,z}, CapSet^{x,y,z}, CapSet^{x,y,z}, CapSet^{b,x,y,z}]
-    testTransMixed[CapSet^{x,y,z}, CapSet^{x,y}, CapSet^{x,y}, CapSet^{x}, CapSet^{}, CapSet^{b,x}, CapSet^{b}, CapSet^{b,x}, CapSet^{b}]
-    testTransMixed[CapSet^{x,y,z}, CapSet^{x,y}, CapSet^{x,y}, CapSet^{x}, CapSet^{}, CapSet^{b,x}, CapSet^{b}, CapSet^{b,x}, CapSet^{b,x,y,z}] // error
+    testTransMixed[{x,y,z}, {x,y,z}, {x,y,z}, {x,y,z}, {x,y,z}, {x,y,z}, {x,y,z}, {x,y,z}, {b,x,y,z}]
+    testTransMixed[{x,y,z}, {x,y}, {x,y}, {x}, {}, {b,x}, {b}, {b,x}, {b}]
+    testTransMixed[{x,y,z}, {x,y}, {x,y}, {x}, {}, {b,x}, {b}, {b,x}, {b,x,y,z}] // error
diff --git a/tests/neg-custom-args/captures/cc-poly-1.scala b/tests/neg-custom-args/captures/cc-poly-1.scala
index b205b9b25246..fa05a447af0b 100644
--- a/tests/neg-custom-args/captures/cc-poly-1.scala
+++ b/tests/neg-custom-args/captures/cc-poly-1.scala
@@ -6,7 +6,7 @@ object Test:
   class C extends Capability
   class D
 
-  def f[X^](x: D^{X}): D^{X} = x
+  def f[cap X](x: D^{X}): D^{X} = x
 
   def test(c1: C, c2: C) =
     f[Any](D()) // error
diff --git a/tests/neg-custom-args/captures/cc-poly-2.check b/tests/neg-custom-args/captures/cc-poly-2.check
index 90568de385b3..f2f31ab85f39 100644
--- a/tests/neg-custom-args/captures/cc-poly-2.check
+++ b/tests/neg-custom-args/captures/cc-poly-2.check
@@ -1,8 +1,8 @@
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-poly-2.scala:14:19 ------------------------------------
-14 |    f[CapSet^{c1}](d) // error
-   |                   ^
-   |                   Found:    (d : Test.D^)
-   |                   Required: Test.D^{c1}
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-poly-2.scala:14:12 ------------------------------------
+14 |    f[{c1}](d) // error
+   |            ^
+   |            Found:    (d : Test.D^)
+   |            Required: Test.D^{c1}
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-poly-2.scala:16:20 ------------------------------------
diff --git a/tests/neg-custom-args/captures/cc-poly-2.scala b/tests/neg-custom-args/captures/cc-poly-2.scala
index 8fb590f4f769..323e2d1333a2 100644
--- a/tests/neg-custom-args/captures/cc-poly-2.scala
+++ b/tests/neg-custom-args/captures/cc-poly-2.scala
@@ -6,11 +6,11 @@ object Test:
   class C extends Capability
   class D
 
-  def f[X^](x: D^{X}): D^{X} = x
+  def f[cap X](x: D^{X}): D^{X} = x
 
   def test(c1: C, c2: C) =
     val d: D^ = D()
     // f[Nothing](d) // already ruled out at typer
-    f[CapSet^{c1}](d) // error
+    f[{c1}](d) // error
     val x = f(d)
     val _: D^{c1} = x // error
diff --git a/tests/neg-custom-args/captures/cc-poly-source.scala b/tests/neg-custom-args/captures/cc-poly-source.scala
index ec98c40a4fa9..0a42b7bbba8f 100644
--- a/tests/neg-custom-args/captures/cc-poly-source.scala
+++ b/tests/neg-custom-args/captures/cc-poly-source.scala
@@ -9,7 +9,7 @@ import caps.use
 
   class Listener
 
-  class Source[X^]:
+  class Source[cap X]:
     private var listeners: Set[Listener^{X}] = Set.empty
     def register(x: Listener^{X}): Unit =
       listeners += x
@@ -17,7 +17,7 @@ import caps.use
     def allListeners: Set[Listener^{X}] = listeners
 
   def test1(lbl1: Label^, lbl2: Label^) =
-    val src = Source[CapSet^{lbl1, lbl2}]
+    val src = Source[{lbl1, lbl2}]
     def l1: Listener^{lbl1} = ???
     val l2: Listener^{lbl2} = ???
     src.register{l1}
@@ -31,7 +31,7 @@ import caps.use
       // we get an error here because we no longer allow contravariant cap
       // to subsume other capabilities. The problem can be solved by declaring
       // Label a SharedCapability, see cc-poly-source-capability.scala
-    val src = Source[CapSet^{lbls*}]
+    val src = Source[{lbls*}]
     for l <- listeners do
       src.register(l)
     val ls = src.allListeners
diff --git a/tests/neg-custom-args/captures/i21313.scala b/tests/neg-custom-args/captures/i21313.scala
index 4b6d16c4da88..7ca612d07e7e 100644
--- a/tests/neg-custom-args/captures/i21313.scala
+++ b/tests/neg-custom-args/captures/i21313.scala
@@ -1,15 +1,15 @@
 import caps.CapSet
 
 trait Async:
-  def await[T, Cap^](using caps.Contains[Cap, this.type])(src: Source[T, Cap]^): T
+  def await[T, cap Cap](using caps.Contains[{Cap}, this.type])(src: Source[T, {Cap}]^): T
 
 def foo(x: Async) = x.await(???) // error
 
-trait Source[+T, Cap^]:
-  final def await(using ac: Async^{Cap}) = ac.await[T, Cap](this) // Contains[Cap, ac] is assured because {ac} <: Cap.
+trait Source[+T, cap Cap]:
+  final def await(using ac: Async^{Cap}) = ac.await[T, {Cap}](this) // Contains[Cap, ac] is assured because {ac} <: Cap.
 
 def test(using ac1: Async^, ac2: Async^, x: String) =
-  val src1 = new Source[Int, CapSet^{ac1}] {}
+  val src1 = new Source[Int, {ac1}] {}
   ac1.await(src1) // ok
-  val src2 = new Source[Int, CapSet^{ac2}] {}
+  val src2 = new Source[Int, {ac2}] {}
   ac1.await(src2) // error
diff --git a/tests/neg-custom-args/captures/i21347.scala b/tests/neg-custom-args/captures/i21347.scala
index 2e37511f053c..9328130963ee 100644
--- a/tests/neg-custom-args/captures/i21347.scala
+++ b/tests/neg-custom-args/captures/i21347.scala
@@ -1,6 +1,6 @@
 import language.experimental.captureChecking
 
-def runOps[C^](ops: List[() ->{C} Unit]): Unit =
+def runOps[cap C](ops: List[() ->{C} Unit]): Unit =
   ops.foreach: op => // error
     op()
 
diff --git a/tests/neg-custom-args/captures/i21868b.scala b/tests/neg-custom-args/captures/i21868b.scala
index 5cff4e3fac2e..2c4420321c74 100644
--- a/tests/neg-custom-args/captures/i21868b.scala
+++ b/tests/neg-custom-args/captures/i21868b.scala
@@ -6,44 +6,44 @@ class IO
 class File
 
 trait Abstract:
-  type C >: CapSet <: CapSet^
+  cap type C
   def f(file: File^{C}): Unit
 
 class Concrete1 extends Abstract:
-  type C = CapSet
+  cap type C = {}
   def f(file: File) = ()
 
 class Concrete2(io: IO^) extends Abstract:
-  type C = CapSet^{io}
+  cap type C = {io}
   def f(file: File^{io}) = ()
 
 class Concrete3(io: IO^) extends Abstract:
-  type C = CapSet^{io}
+  cap type C = {io}
   def f(file: File) = () // error
 
 trait Abstract2(tracked val io: IO^):
-  type C >: CapSet <: CapSet^{io}
+  cap type C <: {io}
   def f(file: File^{C}): Unit
 
 class Concrete4(io: IO^) extends Abstract2(io):
-  type C = CapSet
+  cap type C = {}
   def f(file: File) = ()
 
 class Concrete5(io1: IO^, io2: IO^) extends Abstract2(io1):
-  type C = CapSet^{io2} // error
+  cap type C = {io2} // error
   def f(file: File^{io2}) = ()
 
-trait Abstract3[X^]:
-  type C >: CapSet <: X
+trait Abstract3[cap X]:
+  cap type C <: {X}
   def f(file: File^{C}): Unit
 
-class Concrete6(io: IO^) extends Abstract3[CapSet^{io}]:
-  type C = CapSet
+class Concrete6(io: IO^) extends Abstract3[{io}]:
+  cap type C = {}
   def f(file: File) = ()
 
-class Concrete7(io1: IO^, io2: IO^) extends Abstract3[CapSet^{io1}]:
-  type C = CapSet^{io2} // error
+class Concrete7(io1: IO^, io2: IO^) extends Abstract3[{io1}]:
+  cap type C = {io2} // error
   def f(file: File^{io2}) = ()
 
-class Concrete8(io1: IO^, io2: IO^) extends Abstract3[CapSet^{io1}]:
+class Concrete8(io1: IO^, io2: IO^) extends Abstract3[{io1}]:
   def f(file: File^{io2}) = () // error
\ No newline at end of file
diff --git a/tests/neg-custom-args/captures/polyCaptures.check b/tests/neg-custom-args/captures/polyCaptures.check
index 08ebaf1c63ee..57812e629e70 100644
--- a/tests/neg-custom-args/captures/polyCaptures.check
+++ b/tests/neg-custom-args/captures/polyCaptures.check
@@ -1,8 +1,8 @@
--- Error: tests/neg-custom-args/captures/polyCaptures.scala:4:22 -------------------------------------------------------
-4 |val runOpsCheck: [C^] -> (ops: List[() ->{C} Unit]) ->{C} Unit = runOps  // error
-  |                      ^
+-- Error: tests/neg-custom-args/captures/polyCaptures.scala:4:25 -------------------------------------------------------
+4 |val runOpsCheck: [cap C] -> (ops: List[() ->{C} Unit]) ->{C} Unit = runOps  // error
+  |                         ^
   |          Implementation restriction: polymorphic function types cannot wrap function types that have capture sets
--- Error: tests/neg-custom-args/captures/polyCaptures.scala:5:23 -------------------------------------------------------
-5 |val runOpsCheck2: [C^] => (ops: List[() ->{C} Unit]) ->{C} Unit = runOps // error
-  |                       ^
+-- Error: tests/neg-custom-args/captures/polyCaptures.scala:5:26 -------------------------------------------------------
+5 |val runOpsCheck2: [cap C] => (ops: List[() ->{C} Unit]) ->{C} Unit = runOps // error
+  |                          ^
   |          Implementation restriction: polymorphic function types cannot wrap function types that have capture sets
diff --git a/tests/neg-custom-args/captures/polyCaptures.scala b/tests/neg-custom-args/captures/polyCaptures.scala
index eb8e50f0b997..d92ac36c9987 100644
--- a/tests/neg-custom-args/captures/polyCaptures.scala
+++ b/tests/neg-custom-args/captures/polyCaptures.scala
@@ -1,7 +1,7 @@
 class Box[X](val elem: X)
 
-val runOps = [C^] => (b: Box[() ->{C} Unit]) => b.elem()
-val runOpsCheck: [C^] -> (ops: List[() ->{C} Unit]) ->{C} Unit = runOps  // error
-val runOpsCheck2: [C^] => (ops: List[() ->{C} Unit]) ->{C} Unit = runOps // error
+val runOps = [cap C] => (b: Box[() ->{C} Unit]) => b.elem()
+val runOpsCheck: [cap C] -> (ops: List[() ->{C} Unit]) ->{C} Unit = runOps  // error
+val runOpsCheck2: [cap C] => (ops: List[() ->{C} Unit]) ->{C} Unit = runOps // error
 
 
diff --git a/tests/neg-custom-args/captures/use-capset.check b/tests/neg-custom-args/captures/use-capset.check
index 70b63e87d792..0e25f526f12f 100644
--- a/tests/neg-custom-args/captures/use-capset.check
+++ b/tests/neg-custom-args/captures/use-capset.check
@@ -1,17 +1,17 @@
--- Error: tests/neg-custom-args/captures/use-capset.scala:5:49 ---------------------------------------------------------
-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:11:22 -----------------------------------
-11 |  val _: () -> Unit = h // error: should be ->{io}
+-- Error: tests/neg-custom-args/captures/use-capset.scala:6:52 ---------------------------------------------------------
+6 |private def g[cap 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:12:22 -----------------------------------
+12 |  val _: () -> Unit = h // error: should be ->{io}
    |                      ^
    |                      Found:    (h : () ->{io} Unit)
    |                      Required: () -> Unit
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:13:50 -----------------------------------
-13 |  val _: () -> List[Object^{io}] -> Object^{io} = h2 // error, should be ->{io}
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:14:50 -----------------------------------
+14 |  val _: () -> List[Object^{io}] -> Object^{io} = h2 // error, should be ->{io}
    |                                                  ^^
    |                                             Found:    (h2 : () ->? List[box Object^{io}]^{} ->{io} Object^{io})
    |                                             Required: () -> List[box Object^{io}] -> Object^{io}
diff --git a/tests/neg-custom-args/captures/use-capset.scala b/tests/neg-custom-args/captures/use-capset.scala
index 4f2c239247e6..80a93d861219 100644
--- a/tests/neg-custom-args/captures/use-capset.scala
+++ b/tests/neg-custom-args/captures/use-capset.scala
@@ -1,14 +1,15 @@
-import caps.{use, CapSet}
+import language.experimental.captureChecking
+import caps.use
 
-def f[C^](@use xs: List[Object^{C}]): Unit = ???
+def f[cap C](@use xs: List[Object^{C}]): Unit = ???
 
-private def g[C^] = (xs: List[Object^{C}]) => xs.head // error
+private def g[cap C] = (xs: List[Object^{C}]) => xs.head // error
 
-private def g2[@use C^] = (xs: List[Object^{C}]) => xs.head // ok
+private def g2[@use cap C] = (xs: List[Object^{C}]) => xs.head // ok
 
 def test(io: Object^)(@use xs: List[Object^{io}]): Unit =
   val h = () => f(xs)
   val _: () -> Unit = h // error: should be ->{io}
-  val h2 = () => g[CapSet^{io}]
+  val h2 = () => g[{io}]
   val _: () -> List[Object^{io}] -> Object^{io} = h2 // error, should be ->{io}
 
diff --git a/tests/pos-custom-args/captures/cc-poly-1.scala b/tests/pos-custom-args/captures/cc-poly-1.scala
index e423d94d4000..4e1a7f383db2 100644
--- a/tests/pos-custom-args/captures/cc-poly-1.scala
+++ b/tests/pos-custom-args/captures/cc-poly-1.scala
@@ -7,13 +7,13 @@ import caps.{CapSet, Capability}
   class C extends Capability
   class D
 
-  def f[X^](x: D^{X}): D^{X} = x
-  def g[X^](x: D^{X}, y: D^{X}): D^{X} = x
-  def h[X^](): D^{X} = ???
+  def f[cap X](x: D^{X}): D^{X} = x
+  def g[cap X](x: D^{X}, y: D^{X}): D^{X} = x
+  def h[cap X](): D^{X} = ???
 
   def test(c1: C, c2: C) =
     val d: D^{c1, c2} = D()
-    val x = f[CapSet^{c1, c2}](d)
+    val x = f[{c1, c2}](d)
     val _: D^{c1, c2} = x
     val d1: D^{c1} = D()
     val d2: D^{c2} = D()
diff --git a/tests/pos-custom-args/captures/cc-poly-source-capability.scala b/tests/pos-custom-args/captures/cc-poly-source-capability.scala
index 1208649193af..9dbcf85f9500 100644
--- a/tests/pos-custom-args/captures/cc-poly-source-capability.scala
+++ b/tests/pos-custom-args/captures/cc-poly-source-capability.scala
@@ -11,7 +11,7 @@ import caps.use
 
   class Listener
 
-  class Source[X^]:
+  class Source[cap X]:
     private var listeners: Set[Listener^{X}] = Set.empty
     def register(x: Listener^{X}): Unit =
       listeners += x
@@ -19,7 +19,7 @@ import caps.use
     def allListeners: Set[Listener^{X}] = listeners
 
   def test1(async1: Async, @use others: List[Async]) =
-    val src = Source[CapSet^{async1, others*}]
+    val src = Source[{async1, others*}]
     val _: Set[Listener^{async1, others*}] = src.allListeners
     val lst1 = listener(async1)
     val lsts = others.map(listener)
diff --git a/tests/pos-custom-args/captures/cc-poly-varargs.scala b/tests/pos-custom-args/captures/cc-poly-varargs.scala
index 13e4b276df5a..31a9699ec773 100644
--- a/tests/pos-custom-args/captures/cc-poly-varargs.scala
+++ b/tests/pos-custom-args/captures/cc-poly-varargs.scala
@@ -1,13 +1,13 @@
-abstract class Source[+T, Cap^]
+abstract class Source[+T, cap Cap]
 
-extension[T, Cap^](src: Source[T, Cap]^)
-  def transformValuesWith[U](f: (T -> U)^{Cap}): Source[U, Cap]^{src, f} = ???
+extension[T, cap 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 race[T, cap 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 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)
diff --git a/tests/pos-custom-args/captures/gears-problem-poly.scala b/tests/pos-custom-args/captures/gears-problem-poly.scala
index f7632bce4124..a56ef8577cb9 100644
--- a/tests/pos-custom-args/captures/gears-problem-poly.scala
+++ b/tests/pos-custom-args/captures/gears-problem-poly.scala
@@ -1,5 +1,5 @@
 import language.experimental.captureChecking
-import caps.{use, CapSet}
+import caps.{use}
 
 trait Future[+T]:
   def await: T
@@ -7,7 +7,7 @@ trait Future[+T]:
 trait Channel[+T]:
   def read(): Ok[T]
 
-class Collector[T, C^](val futures: Seq[Future[T]^{C}]):
+class Collector[T, cap C](val futures: Seq[Future[T]^{C}]):
   val results: Channel[Future[T]^{C}] = ???
 end Collector
 
@@ -17,7 +17,7 @@ class Result[+T, +E]:
 case class Err[+E](e: E) extends Result[Nothing, E]
 case class Ok[+T](x: T) extends Result[T, Nothing]
 
-extension [T, C^](@use fs: Seq[Future[T]^{C}])
+extension [T, cap C](@use fs: Seq[Future[T]^{C}])
   def awaitAllPoly =
     val collector = Collector(fs)
     val fut: Future[T]^{C} = collector.results.read().get
@@ -26,4 +26,4 @@ extension [T](@use fs: Seq[Future[T]^])
   def awaitAll = fs.awaitAllPoly
 
 def awaitExplicit[T](@use fs: Seq[Future[T]^]): Unit =
-  awaitAllPoly[T, CapSet^{fs*}](fs)
+  awaitAllPoly[T, {fs*}](fs)
diff --git a/tests/pos-custom-args/captures/i21313.scala b/tests/pos-custom-args/captures/i21313.scala
index e55bf9c7ce62..5255510981cc 100644
--- a/tests/pos-custom-args/captures/i21313.scala
+++ b/tests/pos-custom-args/captures/i21313.scala
@@ -1,20 +1,21 @@
-import caps.CapSet
+import language.experimental.captureChecking
 
 trait Async:
-  def await[T, Cap^](using caps.Contains[Cap, this.type])(src: Source[T, Cap]^): T =
+  def await[T, cap Cap](using caps.Contains[Cap, this.type])(src: Source[T, {Cap}]^): T =
+    // FIXME: this is an irregularity: it works if we write caps.Contains[Cap, this.type], but we should expect to write caps.Contains[{Cap}, this.type]!
     val x: Async^{this} = ???
     val y: Async^{Cap} = x
     val ac: Async^ = ???
-    def f(using caps.Contains[Cap, ac.type]) =
+    def f(using caps.Contains[Cap, ac.type]) = // FIXME: dito
       val x2: Async^{this} = ???
       val y2: Async^{Cap} = x2
       val x3: Async^{ac} = ???
       val y3: Async^{Cap} = x3
     ???
 
-trait Source[+T, Cap^]:
-  final def await(using ac: Async^{Cap}) = ac.await[T, Cap](this) // Contains[Cap, ac] is assured because {ac} <: Cap.
+trait Source[+T, cap Cap]:
+  final def await(using ac: Async^{Cap}) = ac.await[T, {Cap}](this) // Contains[Cap, ac] is assured because {ac} <: Cap.
 
 def test(using ac1: Async^, ac2: Async^, x: String) =
-  val src1 = new Source[Int, CapSet^{ac1}] {}
+  val src1 = new Source[Int, {ac1}] {}
   ac1.await(src1)
diff --git a/tests/pos-custom-args/captures/i21347.scala b/tests/pos-custom-args/captures/i21347.scala
index 9dbb8b154cfb..7e6298200b29 100644
--- a/tests/pos-custom-args/captures/i21347.scala
+++ b/tests/pos-custom-args/captures/i21347.scala
@@ -2,9 +2,9 @@
 
 import language.experimental.captureChecking
 
-class Box[Cap^] {}
+class Box[cap Cap] {}
 
-def run[Cap^](f: Box[Cap]^{Cap} => Unit): Box[Cap]^{Cap} = ???
+def run[cap Cap](f: Box[{Cap}]^{Cap} => Unit): Box[{Cap}]^{Cap} = ???
 
 def main() =
   val b = run(_ => ())
diff --git a/tests/pos-custom-args/captures/i21507.scala b/tests/pos-custom-args/captures/i21507.scala
index 4267795d3a41..285086a26554 100644
--- a/tests/pos-custom-args/captures/i21507.scala
+++ b/tests/pos-custom-args/captures/i21507.scala
@@ -1,10 +1,10 @@
 import language.experimental.captureChecking
 
-trait Box[Cap^]:
+trait Box[cap Cap]:
   def store(f: (() -> Unit)^{Cap}): Unit
 
-def run[Cap^](f: Box[Cap]^{Cap} => Unit): Box[Cap]^{Cap} =
-  new Box[Cap]:
+def run[cap Cap](f: Box[{Cap}]^{Cap} => Unit): Box[{Cap}]^{Cap} =
+  new Box[{Cap}]:
     private var item: () ->{Cap} Unit = () => ()
     def store(f: () ->{Cap} Unit): Unit =
       item = f  // was error, now ok
diff --git a/tests/pos-custom-args/captures/polycap.scala b/tests/pos-custom-args/captures/polycap.scala
index 684f46454595..31f32176e707 100644
--- a/tests/pos-custom-args/captures/polycap.scala
+++ b/tests/pos-custom-args/captures/polycap.scala
@@ -1,11 +1,11 @@
 import language.experimental.captureChecking
 
-class Source[+T, Cap^]
+class Source[+T, cap Cap]
 
-def completed[T, Cap^](result: T): Source[T, Cap] =
+def completed[T, cap Cap](result: T): Source[T, {Cap}] =
   //val fut = new Source[T, Cap]()
-  val fut2 = new Source[T, Cap]()
-  fut2: Source[T, Cap]
+  val fut2 = new Source[T, {Cap}]()
+  fut2: Source[T, {Cap}]
 
 
 
diff --git a/tests/pos-custom-args/captures/setup/a_1.scala b/tests/pos-custom-args/captures/setup/a_1.scala
index 3a6ec7ffa773..2d5c0869624d 100644
--- a/tests/pos-custom-args/captures/setup/a_1.scala
+++ b/tests/pos-custom-args/captures/setup/a_1.scala
@@ -1,6 +1,5 @@
 // a.scala
 import language.experimental.captureChecking
-import scala.caps.CapSet
 
 trait A:
-  def f[C^](x: AnyRef^{C}): Unit
+  def f[cap C](x: AnyRef^{C}): Unit
diff --git a/tests/pos-custom-args/captures/setup/b_1.scala b/tests/pos-custom-args/captures/setup/b_1.scala
index 70c72723c84c..fd5718224d3d 100644
--- a/tests/pos-custom-args/captures/setup/b_1.scala
+++ b/tests/pos-custom-args/captures/setup/b_1.scala
@@ -1,5 +1,4 @@
 import language.experimental.captureChecking
-import scala.caps.CapSet
 
 class B extends A:
-  def f[C^](x: AnyRef^{C}): Unit = ???
+  def f[cap C](x: AnyRef^{C}): Unit = ???
diff --git a/tests/pos-custom-args/captures/setup/b_2.scala b/tests/pos-custom-args/captures/setup/b_2.scala
index 70c72723c84c..fd5718224d3d 100644
--- a/tests/pos-custom-args/captures/setup/b_2.scala
+++ b/tests/pos-custom-args/captures/setup/b_2.scala
@@ -1,5 +1,4 @@
 import language.experimental.captureChecking
-import scala.caps.CapSet
 
 class B extends A:
-  def f[C^](x: AnyRef^{C}): Unit = ???
+  def f[cap C](x: AnyRef^{C}): Unit = ???

From 781656a65e9b3544b8c1063265c91b65099c7e54 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Oliver=20Bra=C4=8Devac?= <bracevac@users.noreply.github.com>
Date: Tue, 1 Apr 2025 19:53:19 +0200
Subject: [PATCH 07/17] Mark cap params with flag

---
 compiler/src/dotty/tools/dotc/parsing/Parsers.scala | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
index 562031223751..55dba4a45fb6 100644
--- a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
+++ b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
@@ -3564,8 +3564,9 @@ object Parsers {
 
       def typeOrCapParam(): TypeDef =
         val start = in.offset
-        val mods = annotsAsMods() | Param
+        var mods = annotsAsMods() | Param
         if isCapKw then
+          mods |= CaptureParam
           in.nextToken()
           capParam(start, mods)
         else typeParam(start, mods)

From bbac2450f8fb3abb38075cc28f6b296b9f584961 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Oliver=20Bra=C4=8Devac?= <bracevac@users.noreply.github.com>
Date: Wed, 2 Apr 2025 01:27:55 +0200
Subject: [PATCH 08/17] Support for named cap arguments

---
 .../dotty/tools/dotc/parsing/Parsers.scala    | 79 +++++++++++--------
 .../captures/capture-vars-subtyping.scala     |  2 -
 .../captures/cap-paramlists5.scala            | 10 ++-
 3 files changed, 53 insertions(+), 38 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
index 55dba4a45fb6..06e9369b1a61 100644
--- a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
+++ b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
@@ -229,8 +229,14 @@ object Parsers {
       if Feature.ccEnabled then
         val lookahead = in.LookaheadScanner()
         lookahead.nextToken()
-        val res = lookahead.isIdent(nme.cap) && lookahead.lookahead.token == TYPE
-        res
+        lookahead.isIdent(nme.cap) && lookahead.lookahead.token == TYPE
+      else false
+    }
+    def isCapAssignmentNext = {
+      if isCapKw then
+        val lookahead = in.LookaheadScanner()
+        lookahead.nextToken()
+        lookahead.isIdent && lookahead.lookahead.token == EQUALS
       else false
     }
     def isSimpleLiteral =
@@ -1614,7 +1620,7 @@ object Parsers {
       case _ => None
     }
 
-    /** CaptureRef  ::=  { SimpleRef `.` } SimpleRef [`*`]
+    /** CaptureRef  ::=  { SimpleRef `.` } SimpleRef [`*`] [`.` rd]
      *                |  [ { SimpleRef `.` } SimpleRef `.` ] id
      */
     def captureRef(): Tree =
@@ -1894,7 +1900,7 @@ object Parsers {
       if in.token == LPAREN then funParamClause() :: funParamClauses() else Nil
 
     /** InfixType ::= RefinedType {id [nl] RefinedType}
-     *             |  RefinedType `^`   // under capture checking
+     *             |  RefinedType `^`   -- under captureChecking
      */
     def infixType(inContextBound: Boolean = false): Tree = infixTypeRest(inContextBound)(refinedType())
 
@@ -2182,44 +2188,47 @@ object Parsers {
       atSpan(startOffset(t), startOffset(id)) { Select(t, id.name) }
     }
 
-    /**   ArgTypes          ::=  Type {`,' Type}
-     *                        |  NamedTypeArg {`,' NamedTypeArg}
-     *    NamedTypeArg      ::=  id `=' Type
+    /**   ArgTypes          ::=  TypeArg {‘,’ TypeArg}
+     *                        |  NamedTypeArg {‘,’ NamedTypeArg}
+     *    TypeArg           ::=  Type
+     *                       |   CaptureSet                       -- under captureChecking
+     *    NamedTypeArg      ::=  id ‘=’  Type
+     *                        |  ‘cap’ id ‘=’ CaptureSet          -- under captureChecking
      *    NamesAndTypes     ::=  NameAndType {‘,’ NameAndType}
-     *    NameAndType       ::=  id ':' Type
+     *    NameAndType       ::=  id ‘:’ Type
      */
-    def argTypes(namedOK: Boolean, wildOK: Boolean, tupleOK: Boolean): List[Tree] = //TODO grammar doc
+    def argTypes(namedOK: Boolean, wildOK: Boolean, tupleOK: Boolean): List[Tree] =
       inline def wildCardCheck(inline gen: Tree): Tree =
         val t = gen
         if wildOK then t else rejectWildcardType(t)
 
-      def argType() = wildCardCheck:
-        typ()
+      def argType() = wildCardCheck(typ())
 
-      def argOrCapType() = wildCardCheck:
+      def typeArg() = wildCardCheck:
         if Feature.ccEnabled && in.token == LBRACE && !isDclIntroNext && !isCapTypeKwNext then // is this a capture set and not a refinement type?
           // This case is ambiguous w.r.t. an Object literal {}. But since CC is enabled, we probably expect it to designate the empty set
           concreteCapsType(captureSet())
         else typ()
 
-      def namedArgType() =
+      def namedTypeArg() =
         atSpan(in.offset):
+          val isCap = if isCapKw then { in.nextToken(); true } else false
           val name = ident()
           accept(EQUALS)
-          NamedArg(name.toTypeName, argType())
+          NamedArg(name.toTypeName, if isCap then concreteCapsType(captureSet()) else argType())
 
-      def namedElem() =
+      def nameAndType() =
         atSpan(in.offset):
           val name = ident()
           acceptColon()
-          NamedArg(name, argType()) // TODO allow capsets here?
+          NamedArg(name, argType())
 
-      if namedOK && isIdent && in.lookahead.token == EQUALS then // TOOD support for named cap args
-          commaSeparated(() => namedArgType())
+      if namedOK && (isIdent && in.lookahead.token == EQUALS || isCapAssignmentNext) then
+        commaSeparated(() => namedTypeArg())
       else if tupleOK && isIdent && in.lookahead.isColon && sourceVersion.enablesNamedTuples then
-        commaSeparated(() => namedElem())
+        commaSeparated(() => nameAndType())
       else
-        commaSeparated(() => argOrCapType())
+        commaSeparated(() => typeArg())
     end argTypes
 
     def paramTypeOf(core: () => Tree): Tree =
@@ -3439,7 +3448,7 @@ object Parsers {
      *                  |  opaque
      *  LocalModifier  ::= abstract | final | sealed | open | implicit | lazy | erased |
      *                     inline | transparent | infix |
-     *                     mut | cap                             -- under cc
+     *                     mut | cap                             -- under captureChecking
      */
     def modifiers(allowed: BitSet = modifierTokens, start: Modifiers = Modifiers()): Modifiers = {
       @tailrec
@@ -3529,20 +3538,24 @@ object Parsers {
     end typeOrTermParamClauses
 
     /** ClsTypeParamClause::=  ‘[’ ClsTypeParam {‘,’ ClsTypeParam} ‘]’
-     *  ClsTypeParam      ::=  {Annotation} [‘+’ | ‘-’]
-     *                         id [HkTypeParamClause] TypeAndCtxBounds
+     *  ClsTypeParam      ::=   {Annotation} [‘+’ | ‘-’]
+     *                          id [HkTypeParamClause] TypeAndCtxBounds
+     *                        | {Annotation} ‘cap’ id CaptureSetAndCtxBounds         -- under captureChecking
      *
      *  DefTypeParamClause::=  ‘[’ DefTypeParam {‘,’ DefTypeParam} ‘]’
-     *  DefTypeParam      ::=  {Annotation}
-     *                         id [HkTypeParamClause] TypeAndCtxBounds
+     *  DefTypeParam      ::=   {Annotation}
+     *                          id [HkTypeParamClause] TypeAndCtxBounds
+     *                        | {Annotation} ‘cap’ id CaptureSetAndCtxBounds         -- under captureChecking
      *
      *  TypTypeParamClause::=  ‘[’ TypTypeParam {‘,’ TypTypeParam} ‘]’
-     *  TypTypeParam      ::=  {Annotation}
-     *                         (id | ‘_’) [HkTypeParamClause] TypeAndCtxBounds
+     *  TypTypeParam      ::=   {Annotation}
+     *                          (id | ‘_’) [HkTypeParamClause] TypeAndCtxBounds
+     *                        | {Annotation} ‘cap’ (id | ‘_’) CaptureSetAndCtxBounds -- under captureChecking
      *
      *  HkTypeParamClause ::=  ‘[’ HkTypeParam {‘,’ HkTypeParam} ‘]’
-     *  HkTypeParam       ::=  {Annotation} [‘+’ | ‘-’]
-     *                         (id | ‘_’) [HkTypePamClause] TypeBounds
+     *  HkTypeParam       ::=   {Annotation} [‘+’ | ‘-’]
+     *                          (id | ‘_’) [HkTypePamClause] TypeBounds
+     *                        | {Annotation} ‘cap’ (id | ‘_’) CaptureSetBounds       -- under captureChecking
      */
     def typeParamClause(paramOwner: ParamOwner): List[TypeDef] = inBracketsWithCommas {
 
@@ -3571,7 +3584,7 @@ object Parsers {
           capParam(start, mods)
         else typeParam(start, mods)
 
-      def capParam(startOffset: Int, mods0: Modifiers): TypeDef = { // TODO grammar doc
+      def capParam(startOffset: Int, mods0: Modifiers): TypeDef = {
         val start = startOffset
         var mods = mods0
         if paramOwner.isClass then
@@ -3964,7 +3977,7 @@ object Parsers {
      *             | var VarDef
      *             | def DefDef
      *             | type {nl} TypeDef
-     *             | cap type {nl} CapDef     -- under capture checking
+     *             | cap type {nl} CapDef     -- under captureChecking
      *             | TmplDef
      *  EnumCase ::= `case' (id ClassConstr [`extends' ConstrApps]] | ids)
      */
@@ -4198,7 +4211,7 @@ object Parsers {
     private def concreteCapsType(refs: List[Tree]): Tree =
       makeRetaining(Select(scalaDot(nme.caps), tpnme.CapSet), refs, tpnme.retains)
 
-    /** CapDef ::=  id CaptureSetAndCtxBounds [‘=’ CaptureSetOrRef]    -- under capture checking
+    /** CapDef ::=  id CaptureSetAndCtxBounds [‘=’ CaptureSetOrRef]    -- under captureChecking
      */
     def capDefOrDcl(start: Offset, mods: Modifiers): Tree =
       newLinesOpt()
@@ -4825,7 +4838,7 @@ object Parsers {
      *                     |  ‘var’ VarDef
      *                     |  ‘def’ DefDef
      *                     |  ‘type’ {nl} TypeDef
-     *                     |  ‘cap’ ‘type’ {nl} CapDef -- under capture checking
+     *                     |  ‘cap’ ‘type’ {nl} CapDef -- under captureChecking
      *  (in reality we admit class defs and vars and filter them out afterwards in `checkLegal`)
      */
     def refineStatSeq(): List[Tree] = {
diff --git a/tests/neg-custom-args/captures/capture-vars-subtyping.scala b/tests/neg-custom-args/captures/capture-vars-subtyping.scala
index b9ee56c10a41..fc3e9fe27ff5 100644
--- a/tests/neg-custom-args/captures/capture-vars-subtyping.scala
+++ b/tests/neg-custom-args/captures/capture-vars-subtyping.scala
@@ -7,8 +7,6 @@ def test[cap C] =
   val c: C = b
   val d: CapSet^{C, c} = a
 
-// TODO: make "CapSet-ness" of type variables somehow contagious?
-// Then we don't have to spell out the bounds explicitly...
 def testTrans[cap C, cap D <: {C}, cap E <: {D}, cap F >: {C}] =
   val d1: D = ???
   val d2: CapSet^{D} = d1
diff --git a/tests/pos-custom-args/captures/cap-paramlists5.scala b/tests/pos-custom-args/captures/cap-paramlists5.scala
index 0460bf85b287..28c00e0468da 100644
--- a/tests/pos-custom-args/captures/cap-paramlists5.scala
+++ b/tests/pos-custom-args/captures/cap-paramlists5.scala
@@ -4,9 +4,13 @@ import language.experimental.namedTypeArguments
 def test2 =
   val x: Any^ = ???
   def foo[cap A, cap B >: {A}, T, U](x: Int) = 1
-  //foo[{x}, {x}, Int](0) // TODO will not work for {x} in first arg
+  foo[{x}, {x}, Int, String](0)
   foo[{}, {}, { def bar: Int }, { cap type D = {x} }](0)
   trait Foo { cap type D }
   foo[{}, {}, Foo, Foo](0)
-  // foo[cap A = {x}, cap B = {x}](0)
-  // foo[cap A = {x}](0)
\ No newline at end of file
+  foo[cap A = {x}, cap B = {x}](0)
+  foo[cap A = {x}](0)
+  foo[T = Int](0)
+  foo[T = Int, cap A = {x}](1)
+  foo[cap A = {x}, T = Int](1)
+  foo[cap B = {}, U = String, cap A = {}](1)
\ No newline at end of file

From 2afdef4dc639ab05e2c2578e9b14939303ba4419 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Oliver=20Bra=C4=8Devac?= <bracevac@users.noreply.github.com>
Date: Wed, 2 Apr 2025 01:49:52 +0200
Subject: [PATCH 09/17] Clean up comments

---
 .../src/dotty/tools/dotc/parsing/Parsers.scala | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
index 06e9369b1a61..73b6f10ec5c5 100644
--- a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
+++ b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
@@ -1620,7 +1620,7 @@ object Parsers {
       case _ => None
     }
 
-    /** CaptureRef  ::=  { SimpleRef `.` } SimpleRef [`*`] [`.` rd]
+    /** CaptureRef  ::=  { SimpleRef `.` } SimpleRef [`*`] [`.` rd]  -- under captureChecking
      *                |  [ { SimpleRef `.` } SimpleRef `.` ] id
      */
     def captureRef(): Tree =
@@ -2292,7 +2292,7 @@ object Parsers {
       atSpan(in.offset):
         TypeBoundsTree(bound(SUPERTYPE), bound(SUBTYPE))
 
-    /** CaptureSetBounds ::= [`>:' CaptureSetOrRef ] [`<:' CaptureSetOrRef ] --- under captureChecking
+    /** CaptureSetBounds ::= [`>:' CaptureSet ] [`<:' CaptureSet ] --- under captureChecking
      */
     def captureSetBounds(): TypeBoundsTree =
       atSpan(in.offset):
@@ -3973,13 +3973,13 @@ object Parsers {
       () => atSpan(in.offset) { importSelection(simpleRef()) }
     end importExpr
 
-    /** Def      ::= val PatDef
-     *             | var VarDef
-     *             | def DefDef
-     *             | type {nl} TypeDef
-     *             | cap type {nl} CapDef     -- under captureChecking
+    /** Def      ::= ‘val’ PatDef
+     *             | ‘var’ VarDef
+     *             | ‘def’ DefDef
+     *             | ‘type’ {nl} TypeDef
+     *             | ‘cap’ ‘type’ {nl} CapDef     -- under captureChecking
      *             | TmplDef
-     *  EnumCase ::= `case' (id ClassConstr [`extends' ConstrApps]] | ids)
+     *  EnumCase ::= ‘case’ (id ClassConstr [‘extends’ ConstrApps]] | ids)
      */
     def defOrDcl(start: Int, mods: Modifiers): Tree =
       in.token match {
@@ -4211,7 +4211,7 @@ object Parsers {
     private def concreteCapsType(refs: List[Tree]): Tree =
       makeRetaining(Select(scalaDot(nme.caps), tpnme.CapSet), refs, tpnme.retains)
 
-    /** CapDef ::=  id CaptureSetAndCtxBounds [‘=’ CaptureSetOrRef]    -- under captureChecking
+    /** CapDef ::=  id CaptureSetAndCtxBounds [‘=’ CaptureSet]    -- under captureChecking
      */
     def capDefOrDcl(start: Offset, mods: Modifiers): Tree =
       newLinesOpt()

From cebba7c5da19ba1e7249d786e31a8fa077ed4e6a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Oliver=20Bra=C4=8Devac?= <bracevac@users.noreply.github.com>
Date: Wed, 2 Apr 2025 15:43:17 +0200
Subject: [PATCH 10/17] Another test for capset members

---
 .../captures/capset-members2.scala               | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
 create mode 100644 tests/pos-custom-args/captures/capset-members2.scala

diff --git a/tests/pos-custom-args/captures/capset-members2.scala b/tests/pos-custom-args/captures/capset-members2.scala
new file mode 100644
index 000000000000..4c5decc1fed1
--- /dev/null
+++ b/tests/pos-custom-args/captures/capset-members2.scala
@@ -0,0 +1,16 @@
+import language.experimental.captureChecking
+
+trait Ctx[T]
+
+def test =
+  val x: Any^ = ???
+  val y: Any^ = ???
+  object O:
+    val z: Any^ = ???
+
+  abstract class Foo[cap A, T]:
+    cap type C <: {A}
+  abstract class Bar extends Foo[{x,y,O.z}, String]:
+    override cap type C <: {x,y}
+  class Baz extends Bar:
+    final override cap type C = {y}
\ No newline at end of file

From f23b9dc94495bcb18ab69c94aa0c34e3b2e73b09 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Oliver=20Bra=C4=8Devac?= <bracevac@users.noreply.github.com>
Date: Wed, 2 Apr 2025 15:43:42 +0200
Subject: [PATCH 11/17] Grammar documentation

---
 .../dotty/tools/dotc/parsing/Parsers.scala    | 31 ++++++++++---------
 docs/_docs/internals/syntax.md                | 28 +++++++++++++++--
 2 files changed, 41 insertions(+), 18 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
index 73b6f10ec5c5..07a5bace0cd0 100644
--- a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
+++ b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
@@ -220,11 +220,11 @@ object Parsers {
     def isErased = isIdent(nme.erased) && in.erasedEnabled
     // Are we seeing an `erased` soft keyword that will not be an identifier?
     def isErasedKw = isErased && in.isSoftModifierInParamModifierPosition
-    // Are we seeing a `cap` soft keyword for declaring a capture-set member or at the beginning a capture-variable parameter list?
+    // Are we seeing a `cap` soft keyword for declaring a capture-set member or a capture-variable parameter?
     def isCapKw = Feature.ccEnabled && isIdent(nme.cap)
-    // 'cap type' ?
+    // Are we seeing 'cap type' ?
     def isCapTypeKw = isCapKw && in.lookahead.token == TYPE
-    // Are the next two tokens 'cap type'?
+    // Are the next two tokens after the current 'cap type'?
     def isCapTypeKwNext = {
       if Feature.ccEnabled then
         val lookahead = in.LookaheadScanner()
@@ -232,6 +232,7 @@ object Parsers {
         lookahead.isIdent(nme.cap) && lookahead.lookahead.token == TYPE
       else false
     }
+    // Are we seeing a named cap parameter assignment? `'cap' id '='` (under namedTypeArguments)
     def isCapAssignmentNext = {
       if isCapKw then
         val lookahead = in.LookaheadScanner()
@@ -1620,8 +1621,8 @@ object Parsers {
       case _ => None
     }
 
-    /** CaptureRef  ::=  { SimpleRef `.` } SimpleRef [`*`] [`.` rd]  -- under captureChecking
-     *                |  [ { SimpleRef `.` } SimpleRef `.` ] id
+    /** CaptureRef  ::=  { SimpleRef ‘.’ } SimpleRef [‘*’] [‘.’ ‘rd’] -- under captureChecking
+     *                |  [ { SimpleRef ‘.’ } SimpleRef ‘.’ ] id
      */
     def captureRef(): Tree =
 
@@ -1645,7 +1646,7 @@ object Parsers {
       recur(simpleRef())
     end captureRef
 
-    /**  CaptureSet ::=  `{` CaptureRef {`,` CaptureRef} `}`    -- under captureChecking
+    /**  CaptureSet ::=  ‘{’ CaptureRef {‘,’ CaptureRef} ‘}’    -- under captureChecking
      */
     def captureSet(): List[Tree] = inBraces {
       if in.token == RBRACE then Nil else commaSeparated(captureRef)
@@ -1663,9 +1664,9 @@ object Parsers {
      *                   |  InfixType
      *  FunType        ::=  (MonoFunType | PolyFunType)
      *  MonoFunType    ::=  FunTypeArgs (‘=>’ | ‘?=>’) Type
-     *                   |  (‘->’ | ‘?->’ ) [CaptureSet] Type           -- under pureFunctions
+     *                   |  (‘->’ | ‘?->’ ) [CaptureSet] Type           -- under pureFunctions and captureChecking
      *  PolyFunType    ::=  TypTypeParamClause '=>' Type
-     *                   |  TypTypeParamClause ‘->’ [CaptureSet] Type   -- under pureFunctions
+     *                   |  TypTypeParamClause ‘->’ [CaptureSet] Type   -- under pureFunctions and captureChecking
      *  FunTypeArgs    ::=  InfixType
      *                   |  `(' [ FunArgType {`,' FunArgType } ] `)'
      *                   |  '(' [ TypedFunParam {',' TypedFunParam } ')'
@@ -2192,8 +2193,8 @@ object Parsers {
      *                        |  NamedTypeArg {‘,’ NamedTypeArg}
      *    TypeArg           ::=  Type
      *                       |   CaptureSet                       -- under captureChecking
-     *    NamedTypeArg      ::=  id ‘=’  Type
-     *                        |  ‘cap’ id ‘=’ CaptureSet          -- under captureChecking
+     *    NamedTypeArg      ::=  id ‘=’  Type                     -- under namedTypeArguments
+     *                        |  ‘cap’ id ‘=’ CaptureSet          -- under namedTypeArguments and captureChecking
      *    NamesAndTypes     ::=  NameAndType {‘,’ NameAndType}
      *    NameAndType       ::=  id ‘:’ Type
      */
@@ -2272,7 +2273,7 @@ object Parsers {
           PostfixOp(t, Ident(tpnme.raw.STAR))
       else t
 
-    /** TypeArgs      ::= `[' Type {`,' Type} `]'
+    /** TypeArgs      ::= `[' TypeArg {`,' TypeArg} `]'
      *  NamedTypeArgs ::= `[' NamedTypeArg {`,' NamedTypeArg} `]'
      */
     def typeArgs(namedOK: Boolean, wildOK: Boolean): List[Tree] =
@@ -3540,22 +3541,22 @@ object Parsers {
     /** ClsTypeParamClause::=  ‘[’ ClsTypeParam {‘,’ ClsTypeParam} ‘]’
      *  ClsTypeParam      ::=   {Annotation} [‘+’ | ‘-’]
      *                          id [HkTypeParamClause] TypeAndCtxBounds
-     *                        | {Annotation} ‘cap’ id CaptureSetAndCtxBounds         -- under captureChecking
+     *                      |   {Annotation} ‘cap’ id CaptureSetAndCtxBounds         -- under captureChecking
      *
      *  DefTypeParamClause::=  ‘[’ DefTypeParam {‘,’ DefTypeParam} ‘]’
      *  DefTypeParam      ::=   {Annotation}
      *                          id [HkTypeParamClause] TypeAndCtxBounds
-     *                        | {Annotation} ‘cap’ id CaptureSetAndCtxBounds         -- under captureChecking
+     *                      |   {Annotation} ‘cap’ id CaptureSetAndCtxBounds         -- under captureChecking
      *
      *  TypTypeParamClause::=  ‘[’ TypTypeParam {‘,’ TypTypeParam} ‘]’
      *  TypTypeParam      ::=   {Annotation}
      *                          (id | ‘_’) [HkTypeParamClause] TypeAndCtxBounds
-     *                        | {Annotation} ‘cap’ (id | ‘_’) CaptureSetAndCtxBounds -- under captureChecking
+     *                      |   {Annotation} ‘cap’ (id | ‘_’) CaptureSetAndCtxBounds -- under captureChecking
      *
      *  HkTypeParamClause ::=  ‘[’ HkTypeParam {‘,’ HkTypeParam} ‘]’
      *  HkTypeParam       ::=   {Annotation} [‘+’ | ‘-’]
      *                          (id | ‘_’) [HkTypePamClause] TypeBounds
-     *                        | {Annotation} ‘cap’ (id | ‘_’) CaptureSetBounds       -- under captureChecking
+     *                      |   {Annotation} ‘cap’ (id | ‘_’) CaptureSetBounds       -- under captureChecking
      */
     def typeParamClause(paramOwner: ParamOwner): List[TypeDef] = inBracketsWithCommas {
 
diff --git a/docs/_docs/internals/syntax.md b/docs/_docs/internals/syntax.md
index 665b4f5144ba..d34ed4d58e1f 100644
--- a/docs/_docs/internals/syntax.md
+++ b/docs/_docs/internals/syntax.md
@@ -141,7 +141,7 @@ type      val       var       while     with      yield
 ### Soft keywords
 
 ```
-as  derives  end  erased  extension  infix  inline  opaque  open  throws tracked transparent  using  |  *  +  -
+as  cap  derives  end  erased  extension  infix  inline  mut  opaque  open  throws tracked transparent  using  |  *  +  -
 ```
 
 See the [separate section on soft keywords](../reference/soft-modifier.md) for additional
@@ -182,7 +182,9 @@ Type              ::=  FunType
                     |  MatchType
                     |  InfixType
 FunType           ::=  FunTypeArgs (‘=>’ | ‘?=>’) Type                          Function(ts, t) | FunctionWithMods(ts, t, mods, erasedParams)
-                    |  TypTypeParamClause '=>' Type                             PolyFunction(ps, t)
+                    |  FunTypeArgs (‘->’ | ‘?->’) [CaptureSet] Type             -- under pureFunctions and captureChecking
+                    |  TypTypeParamClause ‘=>’ Type                             PolyFunction(ps, t)
+                    |  TypTypeParamClause ‘->’ [CaptureSet] Type                -- under pureFunctions and captureChecking
 FunTypeArgs       ::=  InfixType
                     |  ‘(’ [ FunArgTypes ] ‘)’
                     |  FunParamClause
@@ -190,7 +192,9 @@ FunParamClause    ::=  ‘(’ TypedFunParam {‘,’ TypedFunParam } ‘)’
 TypedFunParam     ::=  [`erased`] id ‘:’ Type
 MatchType         ::=  InfixType `match` <<< TypeCaseClauses >>>
 InfixType         ::=  RefinedType {id [nl] RefinedType}                        InfixOp(t1, op, t2)
+                    |  RefinedType ‘^’                                          -- under captureChecking
 RefinedType       ::=  AnnotType {[nl] Refinement}                              RefinedTypeTree(t, ds)
+                    |  AnnotType {[nl] Refinement} [‘^’ CaptureSet]             -- under captureChecking
 AnnotType         ::=  SimpleType {Annotation}                                  Annotated(t, annot)
 AnnotType1        ::=  SimpleType1 {Annotation}                                 Annotated(t, annot)
 
@@ -210,8 +214,10 @@ Singleton         ::=  SimpleRef
                     |  Singleton ‘.’ id
 FunArgType        ::=  Type
                     |  ‘=>’ Type                                                PrefixOp(=>, t)
+                    |  ‘->’ [CaptureSet] Type                                   -- under captureChecking
 FunArgTypes       ::=  FunArgType { ‘,’ FunArgType }
 ParamType         ::=  [‘=>’] ParamValueType
+                    |  ‘->’ [CaptureSet] ParamValueType                         -- under captureChecking
 ParamValueType    ::=  Type [‘*’]                                               PostfixOp(t, "*")
                     |  IntoType
                     |  ‘(’ IntoType ‘)’ ‘*’                                     PostfixOp(t, "*")
@@ -219,7 +225,7 @@ IntoType          ::=  [‘into’] IntoTargetType
                     |  ‘(’ IntoType ‘)’
 IntoTargetType    ::=  Type
                     |  FunTypeArgs (‘=>’ | ‘?=>’) IntoType
-TypeArgs          ::=  ‘[’ Types ‘]’                                            ts
+TypeArgs          ::=  ‘[’ TypeArg {‘,’ TypeArg} ‘]’                            ts
 Refinement        ::=  :<<< [RefineDcl] {semi [RefineDcl]} >>>                  ds
 TypeBounds        ::=  [‘>:’ Type] [‘<:’ Type]                                  TypeBoundsTree(lo, hi)
 TypeAndCtxBounds  ::=  TypeBounds [‘:’ ContextBounds]                           ContextBounds(typeBounds, tps)
@@ -228,8 +234,15 @@ ContextBounds     ::=  ContextBound
                     |  '{' ContextBound {',' ContextBound} '}'
 ContextBound      ::=  Type ['as' id]
 Types             ::=  Type {‘,’ Type}
+TypeArg           ::=  Type
+                    |  CaptureSet                                               -- under captureChecking
 NamesAndTypes     ::=  NameAndType {‘,’ NameAndType}
 NameAndType       ::=  id ':' Type
+CaptureSet             ::=  ‘{’ CaptureRef {‘,’ CaptureRef} ‘}’                 -- under captureChecking
+CaptureRef             ::=  { SimpleRef ‘.’ } SimpleRef [‘*’] [‘.’ ‘rd’]        -- under captureChecking
+                         |  [ { SimpleRef ‘.’ } SimpleRef ‘.’ ] id              -- under captureChecking
+CaptureSetBounds       ::=  [‘>:’ CaptureSet ] [‘<:’ CaptureSet ]               -- under captureChecking
+CaptureSetAndCtxBounds ::=  CaptureSetBounds [‘:’ ContextBounds]                -- under captureChecking
 ```
 
 ### Expressions
@@ -365,16 +378,20 @@ ArgumentPatterns  ::=  ‘(’ [Patterns] ‘)’
 ClsTypeParamClause::=  ‘[’ ClsTypeParam {‘,’ ClsTypeParam} ‘]’
 ClsTypeParam      ::=  {Annotation} [‘+’ | ‘-’]                                 TypeDef(Modifiers, name, tparams, bounds)
                        id [HkTypeParamClause] TypeAndCtxBounds                  Bound(below, above, context)
+                    |  {Annotation} ‘cap’ id CaptureSetAndCtxBounds             -- under captureChecking
 
 DefTypeParamClause::=  [nl] ‘[’ DefTypeParam {‘,’ DefTypeParam} ‘]’
 DefTypeParam      ::=  {Annotation} id [HkTypeParamClause] TypeAndCtxBounds
+                    |  {Annotation} ‘cap’ id CaptureSetAndCtxBounds             -- under captureChecking
 
 TypTypeParamClause::=  ‘[’ TypTypeParam {‘,’ TypTypeParam} ‘]’
 TypTypeParam      ::=  {Annotation} (id | ‘_’) [HkTypeParamClause] TypeBounds
+                    |  {Annotation} ‘cap’ id CaptureSetAndCtxBounds             -- under captureChecking
 
 HkTypeParamClause ::=  ‘[’ HkTypeParam {‘,’ HkTypeParam} ‘]’
 HkTypeParam       ::=  {Annotation} [‘+’ | ‘-’] (id  | ‘_’) [HkTypeParamClause]
                        TypeBounds
+                    |  {Annotation} ‘cap’ id CaptureSetAndCtxBounds             -- under captureChecking
 
 ClsParamClauses   ::=  {ClsParamClause} [[nl] ‘(’ [‘implicit’] ClsParams ‘)’]
 ClsParamClause    ::=  [nl] ‘(’ ClsParams ‘)’
@@ -419,6 +436,8 @@ LocalModifier     ::=  ‘abstract’
                     |  ‘infix’
                     |  ‘erased’
                     |  ‘tracked’
+                    |  ‘mut’                                                      -- under captureChecking
+                    |  ‘cap’                                                      -- under captureChecking
 
 AccessModifier    ::=  (‘private’ | ‘protected’) [AccessQualifier]
 AccessQualifier   ::=  ‘[’ id ‘]’
@@ -448,6 +467,7 @@ RefineDcl         ::=  ‘val’ ValDcl
                     |  ‘var’ ValDcl
                     |  ‘def’ DefDcl
                     |  ‘type’ {nl} TypeDef
+                    |  ‘cap’ ‘type’ {nl} CapDef                                 -- under captureChecking
 ValDcl            ::=  ids ‘:’ Type
 DefDcl            ::=  DefSig ‘:’ Type
 
@@ -455,6 +475,7 @@ Def               ::=  ‘val’ PatDef
                     |  ‘var’ PatDef
                     |  ‘def’ DefDef
                     |  ‘type’ {nl} TypeDef
+                    |  ‘cap’ ‘type’ {nl} CapDef                                 -- under captureChecking
                     |  TmplDef
 PatDef            ::=  ids [‘:’ Type] [‘=’ Expr]
                     |  Pattern2 [‘:’ Type] [‘=’ Expr]                           PatDef(_, pats, tpe?, expr)
@@ -463,6 +484,7 @@ DefDef            ::=  DefSig [‘:’ Type] [‘=’ Expr]
 DefSig            ::=  id [DefParamClauses] [DefImplicitClause]
 TypeDef           ::=  id [HkTypeParamClause] {FunParamClause} TypeAndCtxBounds   TypeDefTree(_, name, tparams, bound
                        [‘=’ Type]
+CapDef            ::=  id CaptureSetAndCtxBounds [‘=’ CaptureSet]               -- under captureChecking
 
 TmplDef           ::=  ([‘case’] ‘class’ | ‘trait’) ClassDef
                     |  [‘case’] ‘object’ ObjectDef

From c2834c72a19b6be996e89411c0eceed2d5a20af5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Oliver=20Bra=C4=8Devac?= <bracevac@users.noreply.github.com>
Date: Fri, 4 Apr 2025 17:37:16 +0200
Subject: [PATCH 12/17] Fixes and polishings

---
 .../dotty/tools/dotc/reporting/messages.scala |  2 +-
 docs/_docs/internals/syntax.md                |  2 +-
 .../captures/capset-bound.scala               | 16 +++++------
 .../captures/capset-members4.scala            | 27 +++++++++++++++++++
 .../captures/capture-vars-subtyping2.scala    |  8 +++---
 tests/neg-custom-args/captures/i21313.scala   |  2 +-
 tests/neg-custom-args/captures/i21868.scala   |  2 +-
 7 files changed, 43 insertions(+), 16 deletions(-)
 create mode 100644 tests/neg-custom-args/captures/capset-members4.scala

diff --git a/compiler/src/dotty/tools/dotc/reporting/messages.scala b/compiler/src/dotty/tools/dotc/reporting/messages.scala
index 800b9469d8d8..291ee431b34b 100644
--- a/compiler/src/dotty/tools/dotc/reporting/messages.scala
+++ b/compiler/src/dotty/tools/dotc/reporting/messages.scala
@@ -1926,7 +1926,7 @@ class ExpectedCaptureBoundOrEquals(found: Token)(using Context)
         |Such capture bounds limit the concrete values of the capture variables and possibly
         |reveal more information about the members of such captures.
         |
-        |A lower type bound ${hl("B >: A")} expresses that the capture variable ${hl("B")}
+        |A lower capture bound ${hl("B >: A")} expresses that the capture variable ${hl("B")}
         |refers to a super capture of capture ${hl("A")}.
         |
         |An upper capture bound ${hl("T <: A")} declares that capture variable ${hl("T")}
diff --git a/docs/_docs/internals/syntax.md b/docs/_docs/internals/syntax.md
index d34ed4d58e1f..d99c169fe7b7 100644
--- a/docs/_docs/internals/syntax.md
+++ b/docs/_docs/internals/syntax.md
@@ -194,7 +194,7 @@ MatchType         ::=  InfixType `match` <<< TypeCaseClauses >>>
 InfixType         ::=  RefinedType {id [nl] RefinedType}                        InfixOp(t1, op, t2)
                     |  RefinedType ‘^’                                          -- under captureChecking
 RefinedType       ::=  AnnotType {[nl] Refinement}                              RefinedTypeTree(t, ds)
-                    |  AnnotType {[nl] Refinement} [‘^’ CaptureSet]             -- under captureChecking
+                    |  AnnotType {[nl] Refinement} ‘^’ CaptureSet               -- under captureChecking
 AnnotType         ::=  SimpleType {Annotation}                                  Annotated(t, annot)
 AnnotType1        ::=  SimpleType1 {Annotation}                                 Annotated(t, annot)
 
diff --git a/tests/neg-custom-args/captures/capset-bound.scala b/tests/neg-custom-args/captures/capset-bound.scala
index 80ee3804776f..d20847729a77 100644
--- a/tests/neg-custom-args/captures/capset-bound.scala
+++ b/tests/neg-custom-args/captures/capset-bound.scala
@@ -5,14 +5,14 @@ class IO
 case class File(io: IO^)
 
 def test(io1: IO^, io2: IO^) =
-  def f[C >: CapSet^{io1} <: CapSet^](file: File^{C}) = ???
+  def f[cap C >: {io1}](file: File^{C}) = ???
   val f1: File^{io1} = ???
   val f2: File^{io2} = ???
   val f3: File^{io1, io2} = ???
-  f[CapSet^{io1}](f1)
-  f[CapSet^{io1}](f2) // error
-  f[CapSet^{io1}](f3) // error
-  f[CapSet^{io2}](f2) // error
-  f[CapSet^{io1, io2}](f1)
-  f[CapSet^{io1, io2}](f2)
-  f[CapSet^{io1, io2}](f3)
\ No newline at end of file
+  f[{io1}](f1)
+  f[{io1}](f2) // error
+  f[{io1}](f3) // error
+  f[{io2}](f2) // error
+  f[{io1, io2}](f1)
+  f[{io1, io2}](f2)
+  f[{io1, io2}](f3)
\ No newline at end of file
diff --git a/tests/neg-custom-args/captures/capset-members4.scala b/tests/neg-custom-args/captures/capset-members4.scala
new file mode 100644
index 000000000000..0da33199fbcb
--- /dev/null
+++ b/tests/neg-custom-args/captures/capset-members4.scala
@@ -0,0 +1,27 @@
+import language.experimental.captureChecking
+import language.experimental.modularity
+import caps.*
+
+def test =
+  val x: Any^ = ???
+  val y: Any^ = ???
+  val z: Any^ = ???
+  def onlyWithZ[cap C](using c: Contains[C, z.type]) = ???
+
+  trait IncludesZ[cap C]:
+    val c: Contains[C, z.type]
+
+  trait Foo:
+    cap type C >: {x} <: {x,y,z} : IncludesZ
+
+  val foo: Foo = ???
+/*   new Foo {
+    override given IncludesZ[C]: // FIXME: doesn't work yet
+      val c: Contains[C, z.type] = summon
+    cap type C = {x,z}
+  } */
+  onlyWithZ(using foo.C.c)
+  onlyWithZ[{z}]
+  onlyWithZ[{x,z}]
+  onlyWithZ[{x,y,z}]
+  onlyWithZ[{x,y}] // error
\ No newline at end of file
diff --git a/tests/neg-custom-args/captures/capture-vars-subtyping2.scala b/tests/neg-custom-args/captures/capture-vars-subtyping2.scala
index b3232cbaafbb..93d080e83a70 100644
--- a/tests/neg-custom-args/captures/capture-vars-subtyping2.scala
+++ b/tests/neg-custom-args/captures/capture-vars-subtyping2.scala
@@ -16,7 +16,7 @@ trait BoundsTest:
                      cap F <: {A,b},
                      cap X <: {F,D},
                      cap Y >: {F} <: {F,A,b},
-                     cap Z >: {b} <: {b,Y}] =
+                     cap Z >: {b} <: {b,Y}, T <: List[Bar^{Z}]] =
     val e: E = ???
     val e2: CapSet^{E} = e
     val ed: D = e
@@ -39,6 +39,6 @@ trait BoundsTest:
 
   def callTransMixed =
     val x, y, z: Bar^ = ???
-    testTransMixed[{x,y,z}, {x,y,z}, {x,y,z}, {x,y,z}, {x,y,z}, {x,y,z}, {x,y,z}, {x,y,z}, {b,x,y,z}]
-    testTransMixed[{x,y,z}, {x,y}, {x,y}, {x}, {}, {b,x}, {b}, {b,x}, {b}]
-    testTransMixed[{x,y,z}, {x,y}, {x,y}, {x}, {}, {b,x}, {b}, {b,x}, {b,x,y,z}] // error
+    testTransMixed[{x,y,z}, {x,y,z}, {x,y,z}, {x,y,z}, {x,y,z}, {x,y,z}, {x,y,z}, {x,y,z}, {b,x,y,z}, List[Bar^{b}]]
+    testTransMixed[{x,y,z}, {x,y}, {x,y}, {x}, {}, {b,x}, {b}, {b,x}, {b}, List[Bar^{b}]]
+    testTransMixed[{x,y,z}, {x,y}, {x,y}, {x}, {}, {b,x}, {b}, {b,x}, {b,x,y,z}, List[Bar^{}]] // error
diff --git a/tests/neg-custom-args/captures/i21313.scala b/tests/neg-custom-args/captures/i21313.scala
index 7ca612d07e7e..e81790b60dff 100644
--- a/tests/neg-custom-args/captures/i21313.scala
+++ b/tests/neg-custom-args/captures/i21313.scala
@@ -1,7 +1,7 @@
 import caps.CapSet
 
 trait Async:
-  def await[T, cap Cap](using caps.Contains[{Cap}, this.type])(src: Source[T, {Cap}]^): T
+  def await[T, cap Cap](using caps.Contains[Cap, this.type])(src: Source[T, {Cap}]^): T
 
 def foo(x: Async) = x.await(???) // error
 
diff --git a/tests/neg-custom-args/captures/i21868.scala b/tests/neg-custom-args/captures/i21868.scala
index de6a9b64b78b..d726fb1fc716 100644
--- a/tests/neg-custom-args/captures/i21868.scala
+++ b/tests/neg-custom-args/captures/i21868.scala
@@ -5,7 +5,7 @@ trait AbstractWrong:
   def f(): Unit^{C} // error
 
 trait Abstract1:
-  type C >: CapSet <: CapSet^
+  cap type C
   def f(): Unit^{C}
 
 // class Abstract2:

From 48e87da198fa0b27184f37f7309cb2256a18d64f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Oliver=20Bra=C4=8Devac?= <bracevac@users.noreply.github.com>
Date: Fri, 4 Apr 2025 18:05:04 +0200
Subject: [PATCH 13/17] Add lexical control delimiter test for captures

---
 .../src/dotty/tools/dotc/parsing/Parsers.scala | 10 +++++++---
 .../captures/lexical-control.scala             | 18 ++++++++++++++++++
 2 files changed, 25 insertions(+), 3 deletions(-)
 create mode 100644 tests/neg-custom-args/captures/lexical-control.scala

diff --git a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
index 07a5bace0cd0..c74975ccae20 100644
--- a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
+++ b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
@@ -1648,9 +1648,13 @@ object Parsers {
 
     /**  CaptureSet ::=  ‘{’ CaptureRef {‘,’ CaptureRef} ‘}’    -- under captureChecking
      */
-    def captureSet(): List[Tree] = inBraces {
-      if in.token == RBRACE then Nil else commaSeparated(captureRef)
-    }
+    def captureSet(): List[Tree] =
+      if in.token != LBRACE then
+        syntaxError(em"expected '{' to start capture set", in.offset)
+        Nil
+      else inBraces {
+        if in.token == RBRACE then Nil else commaSeparated(captureRef)
+      }
 
     def capturesAndResult(core: () => Tree): Tree =
       if Feature.ccEnabled && in.token == LBRACE && canStartCaptureSetContentsTokens.contains(in.lookahead.token)
diff --git a/tests/neg-custom-args/captures/lexical-control.scala b/tests/neg-custom-args/captures/lexical-control.scala
new file mode 100644
index 000000000000..fd7d56dc7ea7
--- /dev/null
+++ b/tests/neg-custom-args/captures/lexical-control.scala
@@ -0,0 +1,18 @@
+import language.experimental.captureChecking
+import caps.*
+
+trait Label extends Capability:
+  cap type Fv // the capability set occurring freely in the `block` passed to `boundary` below.
+
+def boundary[T, cap C](block: Label{cap type Fv = {C} } ->{C} T): T = ??? // link label and block capture set
+def suspend[U](label: Label)(handler: () ->{label.Fv} U): U = ??? // note the path
+
+def test =
+  val x = 1
+  boundary: outer =>
+    val y = 2
+    boundary: inner =>
+      val z = 3
+      suspend(outer): () =>
+        println(inner) // error  (leaks the inner label)
+        x + y + z
\ No newline at end of file

From aab2aa23cdc96a6f611c843ccc3f850377bd5cc9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Oliver=20Bra=C4=8Devac?= <bracevac@users.noreply.github.com>
Date: Sun, 6 Apr 2025 20:30:14 +0200
Subject: [PATCH 14/17] Fix test

---
 .../captures/lexical-control.scala                | 15 ++++++++++++---
 1 file changed, 12 insertions(+), 3 deletions(-)

diff --git a/tests/neg-custom-args/captures/lexical-control.scala b/tests/neg-custom-args/captures/lexical-control.scala
index fd7d56dc7ea7..ecbae49d4542 100644
--- a/tests/neg-custom-args/captures/lexical-control.scala
+++ b/tests/neg-custom-args/captures/lexical-control.scala
@@ -5,7 +5,7 @@ trait Label extends Capability:
   cap type Fv // the capability set occurring freely in the `block` passed to `boundary` below.
 
 def boundary[T, cap C](block: Label{cap type Fv = {C} } ->{C} T): T = ??? // link label and block capture set
-def suspend[U](label: Label)(handler: () ->{label.Fv} U): U = ??? // note the path
+def suspend[U](label: Label)[cap D <: {label.Fv}](handler: () ->{D} U): U = ??? // note the path
 
 def test =
   val x = 1
@@ -13,6 +13,15 @@ def test =
     val y = 2
     boundary: inner =>
       val z = 3
-      suspend(outer): () =>
-        println(inner) // error  (leaks the inner label)
+      val w = suspend(outer) {() => z} // ok
+      val v = suspend(inner) {() => y} // ok
+      val u = suspend(inner): () =>
+        suspend(outer) {() => y} // ok
+        suspend(outer) {() => y} // ok
+        y
+      suspend(outer) { () => // error
+        suspend(outer) {() => y }
+      }
+      suspend(outer): () => // error  (leaks the inner label)
+        println(inner)
         x + y + z
\ No newline at end of file

From 0e6958fe648d4d12665c8cf1652c9b9dcc7ace71 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Oliver=20Bra=C4=8Devac?= <bracevac@users.noreply.github.com>
Date: Wed, 9 Apr 2025 01:31:36 +0200
Subject: [PATCH 15/17] Update language reference to new capset syntax

Plus added a test demonstrating branding
and uses of upper and lower bounds.
---
 docs/_docs/reference/experimental/cc.md       | 134 +++++++++++++++---
 tests/neg-custom-args/captures/branding.scala |  39 +++++
 2 files changed, 155 insertions(+), 18 deletions(-)
 create mode 100644 tests/neg-custom-args/captures/branding.scala

diff --git a/docs/_docs/reference/experimental/cc.md b/docs/_docs/reference/experimental/cc.md
index ff480ffb638b..2a1f9ba20933 100644
--- a/docs/_docs/reference/experimental/cc.md
+++ b/docs/_docs/reference/experimental/cc.md
@@ -726,34 +726,38 @@ Reach capabilities take the form `x*` where `x` is syntactically a regular capab
 It is sometimes convenient to write operations that are parameterized with a capture set of capabilities. For instance consider a type of event sources
 `Source` on which `Listener`s can be registered. Listeners can hold certain capabilities, which show up as a parameter to `Source`:
 ```scala
-  class Source[X^]:
-    private var listeners: Set[Listener^{X^}] = Set.empty
-    def register(x: Listener^{X^}): Unit =
-      listeners += x
+class Source[cap X]:
+  private var listeners: Set[Listener^{X}] = Set.empty
+  def register(x: Listener^{X}): Unit =
+    listeners += x
 
-    def allListeners: Set[Listener^{X^}] = listeners
+  def allListeners: Set[Listener^{X}] = listeners
 ```
-The type variable `X^` can be instantiated with a set of capabilities. It can occur in capture sets in its scope. For instance, in the example above
-we see a variable `listeners` that has as type a `Set` of `Listeners` capturing `X^`. The `register` method takes a listener of this type
+The type variable `cap X` (with `cap` being a soft modifier) can be instantiated with a set of capabilities. It can occur in capture sets in its scope. For instance, in the example above
+we see a variable `listeners` that has as type a `Set` of `Listeners` capturing `X`. The `register` method takes a listener of this type
 and assigns it to the variable.
 
-Capture set variables `X^` are represented as regular type variables with a
-special upper bound `CapSet`. For instance, `Source` could be equivalently
+Capture-set variables `cap X` are represented as regular type variables within the special interval
+ `>: CapSet <: CapSet^`. For instance, `Source` could be equivalently
 defined as follows:
 ```scala
-  class Source[X <: CapSet^]:
-    ...
+class Source[X >: CapSet <: CapSet^]:
+  ...
 ```
-`CapSet` is a sealed trait in the `caps` object. It cannot be instantiated or inherited, so its only purpose is to identify capture set type variables and types. Capture set variables can be inferred like regular type variables. When they should be instantiated explicitly one uses a capturing
-type `CapSet`. For instance:
+`CapSet` is a sealed trait in the `caps` object. It cannot be instantiated or inherited, so its only
+purpose is to identify capture-set type variables and types. This representation based on `CapSet` is subject to change and
+its direct use is discouraged.
+
+Capture-set variables can be inferred like regular type variables. When they should be instantiated
+explicitly one supplies a concrete capture set. For instance:
 ```scala
-  class Async extends caps.Capability
+class Async extends caps.Capability
 
-  def listener(async: Async): Listener^{async} = ???
+def listener(async: Async): Listener^{async} = ???
 
-  def test1(async1: Async, others: List[Async]) =
-    val src = Source[CapSet^{async1, others*}]
-    ...
+def test1(async1: Async, others: List[Async]) =
+  val src = Source[{async1, others*}]
+  ...
 ```
 Here, `src` is created as a `Source` on which listeners can be registered that refer to the `async` capability or to any of the capabilities in list `others`. So we can continue the example code above as follows:
 ```scala
@@ -761,6 +765,100 @@ Here, `src` is created as a `Source` on which listeners can be registered that r
   others.map(listener).foreach(src.register)
   val ls: Set[Listener^{async, others*}] = src.allListeners
 ```
+A common use-case for explicit capture parameters is describing changes to the captures of mutable fields, such as concatenating
+effectful iterators:
+```scala
+class ConcatIterator[A, cap C](var iterators: mutable.List[IterableOnce[A]^{C}]):
+  def concat(it: IterableOnce[A]^): ConcatIterator[A, {this.C, it}]^{this, it} =
+    iterators ++= it                             //            ^
+    this                                         // track contents of `it` in the result
+```
+In such a scenario, we also should ensure that any pre-existing alias of a `ConcatIterator` object should become
+inaccessible after invoking its `concat` method. This is achieved with mutation and separation tracking which are
+currently in development.
+
+Finally, analogously to type parameters, we can lower- and upper-bound capability parameters where the bounds consist of concrete capture sets:
+```scala
+  // We can close over anything subsumed branded by the 'trusted' capability, but nothing else
+  def runSecure[cap C >: {trusted} <: {trusted}](block: () ->{C} Unit): Unit = ...
+
+  // This is a 'brand" capability to mark what can be mentioned in trusted code
+  object trusted extends caps.Capability
+
+  // These capabilities are trusted:
+  val trustedLogger: Logger^{trusted}
+  val trustedChannel: Channel[String]^{trusted}
+  // These aren't:
+  val untrustedLogger: Logger^
+  val untrustedChannel: Channel[String]^
+
+  runSecure: () =>
+    trustedLogger.log("Hello from trusted code") // ok
+
+  runSecure: () =>
+    trustedChannel.send("I can send")            // ok
+    trustedLogger.log(trustedChannel.recv())     // ok
+
+  runSecure: () => "I am pure and that's ok"     // ok
+
+  runSecure: () =>
+    untrustedLogger.log("I can't be used")       // error
+    untrustedChannel.send("I can't be used")     // error
+```
+The idea is that every capability derived from the marker capability `trusted` (and only those) are eligible to be used in the `block` closure
+passed to `runSecure`. We can enforce this by an explicit capability parameter `C` constraining the possible captures of `block` to the interval `>: {trusted} <: {trusted}`
+
+## Capability Members
+
+Just as parametrization by types can be equally expressed with type members, we could
+also define the `Source[cap X]` class above could using a _capability member_:
+```scala
+class Source:
+  cap type X
+  private var listeners: Set[Listener^{this.X}] = Set.empty
+  ... // as before
+```
+Here, we can refer to capability members using paths in capture sets (such as `{this.X}`). Similarly to type members,
+capability members can be upper- and lower-bounded with capture sets:
+```scala
+trait Thread:
+  cap type Cap
+  def run(block: () ->{this.Cap} -> Unit): Unit
+
+trait GPUThread extends Thread:
+  cap type Cap >: {cudaMalloc, cudaFree} <: {caps.cap}
+```
+
+
+We conclude with a more advanced example, showing how capability members and paths to these members can prevent leakage
+of labels for lexically-delimited control operators:
+```scala
+trait Label extends Capability:
+  cap type Fv // the capability set occurring freely in the `block` passed to `boundary` below.
+
+def boundary[T, cap C](block: Label{cap type Fv = {C} } ->{C} T): T = ??? // ensure free caps of label and block match
+def suspend[U](label: Label)[cap D <: {label.Fv}](handler: () ->{D} U): U = ??? // may only capture the free capabilities of label
+
+def test =
+  val x = 1
+  boundary: outer =>
+    val y = 2
+    boundary: inner =>
+      val z = 3
+      val w = suspend(outer) {() => z} // ok
+      val v = suspend(inner) {() => y} // ok
+      val u = suspend(inner): () =>
+        suspend(outer) {() => w + v} // ok
+        y
+      suspend(outer): () =>
+        println(inner) // error (would leak the inner label)
+        x + y + z
+```
+A key property is that `suspend` (think `shift` from delimited continuations) targeting a specific label (such as `outer`) should not accidentally close over labels from a nested `boundary` (such as `inner`), because they would escape their defining scope this way.
+By leveraging capability polymorphism, capability members, and path-dependent capabilities, we can prevent such leaks from occurring at compile time:
+
+* `Label`s store the free capabilities `C` of the `block` passed to `boundary` in their capability member `Fv`.
+* When suspending on a given label, the suspension handler can capture at most the capabilities that occur freely at the `boundary` that introduced the label. That prevents mentioning nested bound labels.
 
 ## Compilation Options
 
diff --git a/tests/neg-custom-args/captures/branding.scala b/tests/neg-custom-args/captures/branding.scala
new file mode 100644
index 000000000000..dcdac7a4ee82
--- /dev/null
+++ b/tests/neg-custom-args/captures/branding.scala
@@ -0,0 +1,39 @@
+import language.experimental.captureChecking
+import caps.*
+
+
+def main() =
+  trait Channel[T] extends caps.Capability:
+    def send(msg: T): Unit
+    def recv(): T
+
+  trait Logger extends caps.Capability:
+    def log(msg: String): Unit
+
+  // we can close over anything subsumed by the 'trusted' brand capability, but nothing else
+  def runSecure[cap C >: {trusted} <: {trusted}](block: () ->{C} Unit): Unit = block()
+
+  // This is a 'brand" capability to mark what can be mentioned in trusted code
+  object trusted extends caps.Capability
+
+  val trustedLogger: Logger^{trusted} = ???
+  val trustedChannel: Channel[String]^{trusted} = ???
+
+  val untrustedLogger: Logger^ = ???
+  val untrustedChannel: Channel[String]^ = ???
+
+  runSecure: () =>
+    trustedLogger.log("Hello from trusted code") // ok
+
+  runSecure: () =>
+    trustedChannel.send("I can send")
+    trustedLogger.log(trustedChannel.recv()) // ok
+
+  runSecure: () =>
+    "I am pure"                             // ok
+
+  runSecure: () => // error
+    untrustedLogger.log("I can't be used here")
+
+  runSecure: () => // error
+    untrustedChannel.send("I can't be used here")
\ No newline at end of file

From 0817e43f8a8d01e4cee3ffaefd6ce0e3daed85b3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Oliver=20Bra=C4=8Devac?= <bracevac@users.noreply.github.com>
Date: Wed, 9 Apr 2025 14:53:40 +0200
Subject: [PATCH 16/17] Polishings

---
 docs/_docs/reference/experimental/cc.md       | 13 +++++--
 .../neg-custom-args/captures/branding2.scala  | 39 +++++++++++++++++++
 2 files changed, 49 insertions(+), 3 deletions(-)
 create mode 100644 tests/neg-custom-args/captures/branding2.scala

diff --git a/docs/_docs/reference/experimental/cc.md b/docs/_docs/reference/experimental/cc.md
index 2a1f9ba20933..72b509f9be19 100644
--- a/docs/_docs/reference/experimental/cc.md
+++ b/docs/_docs/reference/experimental/cc.md
@@ -779,7 +779,8 @@ currently in development.
 
 Finally, analogously to type parameters, we can lower- and upper-bound capability parameters where the bounds consist of concrete capture sets:
 ```scala
-  // We can close over anything subsumed branded by the 'trusted' capability, but nothing else
+def main() =
+  // We can close over anything branded by the 'trusted' capability, but nothing else
   def runSecure[cap C >: {trusted} <: {trusted}](block: () ->{C} Unit): Unit = ...
 
   // This is a 'brand" capability to mark what can be mentioned in trusted code
@@ -806,7 +807,12 @@ Finally, analogously to type parameters, we can lower- and upper-bound capabilit
     untrustedChannel.send("I can't be used")     // error
 ```
 The idea is that every capability derived from the marker capability `trusted` (and only those) are eligible to be used in the `block` closure
-passed to `runSecure`. We can enforce this by an explicit capability parameter `C` constraining the possible captures of `block` to the interval `>: {trusted} <: {trusted}`
+passed to `runSecure`. We can enforce this by an explicit capability parameter `C` constraining the possible captures of `block` to the interval `>: {trusted} <: {trusted}`.
+
+Note that since capabilities of function types are covariant, we could have equivalently specified `runSecure`'s signature using implicit capture polymorphism to achieve the same behavior:
+```scala
+def runSecure(block: () ->{trusted} Unit): Unit
+```
 
 ## Capability Members
 
@@ -828,7 +834,8 @@ trait Thread:
 trait GPUThread extends Thread:
   cap type Cap >: {cudaMalloc, cudaFree} <: {caps.cap}
 ```
-
+Since `caps.cap` is the top element for subcapturing, we could have also left out the
+upper bound: `cap type Cap >: {cudaMalloc, cudaFree}`.
 
 We conclude with a more advanced example, showing how capability members and paths to these members can prevent leakage
 of labels for lexically-delimited control operators:
diff --git a/tests/neg-custom-args/captures/branding2.scala b/tests/neg-custom-args/captures/branding2.scala
new file mode 100644
index 000000000000..eb27d863c745
--- /dev/null
+++ b/tests/neg-custom-args/captures/branding2.scala
@@ -0,0 +1,39 @@
+import language.experimental.captureChecking
+import caps.*
+
+
+def main() =
+  trait Channel[T] extends caps.Capability:
+    def send(msg: T): Unit
+    def recv(): T
+
+  trait Logger extends caps.Capability:
+    def log(msg: String): Unit
+
+  // we can close over anything subsumed by the 'trusted' brand capability, but nothing else
+  def runSecure(block: () ->{trusted} Unit): Unit = block()
+
+  // This is a 'brand" capability to mark what can be mentioned in trusted code
+  object trusted extends caps.Capability
+
+  val trustedLogger: Logger^{trusted} = ???
+  val trustedChannel: Channel[String]^{trusted} = ???
+
+  val untrustedLogger: Logger^ = ???
+  val untrustedChannel: Channel[String]^ = ???
+
+  runSecure: () =>
+    trustedLogger.log("Hello from trusted code") // ok
+
+  runSecure: () =>
+    trustedChannel.send("I can send")
+    trustedLogger.log(trustedChannel.recv()) // ok
+
+  runSecure: () =>
+    "I am pure" : Unit                             // ok
+
+  runSecure: () =>
+    untrustedLogger.log("I can't be used here") // error
+
+  runSecure: () =>
+    untrustedChannel.send("I can't be used here") // error
\ No newline at end of file

From 1de50f6a75e059021afad7dbdea2e3fdff20d455 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Oliver=20Bra=C4=8Devac?= <bracevac@users.noreply.github.com>
Date: Fri, 11 Apr 2025 18:23:31 +0200
Subject: [PATCH 17/17] Update cc.md

---
 docs/_docs/reference/experimental/cc.md | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

diff --git a/docs/_docs/reference/experimental/cc.md b/docs/_docs/reference/experimental/cc.md
index 72b509f9be19..cfb3097205cf 100644
--- a/docs/_docs/reference/experimental/cc.md
+++ b/docs/_docs/reference/experimental/cc.md
@@ -737,15 +737,22 @@ The type variable `cap X` (with `cap` being a soft modifier) can be instantiated
 we see a variable `listeners` that has as type a `Set` of `Listeners` capturing `X`. The `register` method takes a listener of this type
 and assigns it to the variable.
 
-Capture-set variables `cap X` are represented as regular type variables within the special interval
- `>: CapSet <: CapSet^`. For instance, `Source` could be equivalently
+Capture-set variables `cap X` without user-annotated bounds by default range over the interval `>: {} <: {caps.cap}` which is the universe of capture sets instead of regular types.
+
+Under the hood, such capture-set variables are represented as regular type variables within the special interval
+ `>: CapSet <: CapSet^`.
+For instance, `Source` from above could be equivalently
 defined as follows:
 ```scala
 class Source[X >: CapSet <: CapSet^]:
   ...
 ```
 `CapSet` is a sealed trait in the `caps` object. It cannot be instantiated or inherited, so its only
-purpose is to identify capture-set type variables and types. This representation based on `CapSet` is subject to change and
+purpose is to identify type variables which are capture sets. In non-capture-checked
+usage contexts, the type system will treat `CapSet^{a}` and `CapSet^{a,b}` as the type `CapSet`, whereas
+with capture checking enabled, it will take the annotated capture sets into account,
+so that `CapSet^{a}` and `CapSet^{a,b}` are distinct.
+This representation based on `CapSet` is subject to change and
 its direct use is discouraged.
 
 Capture-set variables can be inferred like regular type variables. When they should be instantiated