From 65424938592b28dad3454682213e83b0fc3d6140 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sat, 11 May 2024 13:08:22 +0200
Subject: [PATCH 01/14] Distinguish maximal from root capabilities

A maximal capability is one that derives from `caps.Cap`.

Also: drop the given caps.Cap. It's not clear why there needs to be a given for it.
---
 compiler/src/dotty/tools/dotc/cc/CaptureSet.scala | 10 +++++-----
 compiler/src/dotty/tools/dotc/core/Types.scala    |  9 ++++++++-
 library/src/scala/caps.scala                      |  2 --
 tests/neg-custom-args/captures/filevar.scala      |  2 +-
 tests/neg-custom-args/captures/i15923.scala       |  2 +-
 tests/neg-custom-args/captures/stack-alloc.scala  |  2 +-
 tests/neg-custom-args/captures/usingLogFile.scala |  2 +-
 7 files changed, 17 insertions(+), 12 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index d1a5a07f6a0f..5a60506cc49a 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -115,7 +115,7 @@ sealed abstract class CaptureSet extends Showable:
    *  capture set.
    */
   protected final def addNewElem(elem: CaptureRef)(using Context, VarState): CompareResult =
-    if elem.isRootCapability || summon[VarState] == FrozenState then
+    if elem.isMaxCapability || summon[VarState] == FrozenState then
       addThisElem(elem)
     else
       addThisElem(elem).orElse:
@@ -167,11 +167,11 @@ sealed abstract class CaptureSet extends Showable:
     if comparer.isInstanceOf[ExplainingTypeComparer] then // !!! DEBUG
       reporting.trace.force(i"$this accountsFor $x, ${x.captureSetOfInfo}?", show = true):
         elems.exists(_.subsumes(x))
-        || !x.isRootCapability && x.captureSetOfInfo.subCaptures(this, frozen = true).isOK
+        || !x.isMaxCapability && x.captureSetOfInfo.subCaptures(this, frozen = true).isOK
     else
       reporting.trace(i"$this accountsFor $x, ${x.captureSetOfInfo}?", show = true):
         elems.exists(_.subsumes(x))
-        || !x.isRootCapability && x.captureSetOfInfo.subCaptures(this, frozen = true).isOK
+        || !x.isMaxCapability && x.captureSetOfInfo.subCaptures(this, frozen = true).isOK
 
   /** A more optimistic version of accountsFor, which does not take variable supersets
    *  of the `x` reference into account. A set might account for `x` if it accounts
@@ -183,7 +183,7 @@ sealed abstract class CaptureSet extends Showable:
   def mightAccountFor(x: CaptureRef)(using Context): Boolean =
     reporting.trace(i"$this mightAccountFor $x, ${x.captureSetOfInfo}?", show = true) {
       elems.exists(_.subsumes(x))
-      || !x.isRootCapability
+      || !x.isMaxCapability
         && {
           val elems = x.captureSetOfInfo.elems
           !elems.isEmpty && elems.forall(mightAccountFor)
@@ -1032,7 +1032,7 @@ object CaptureSet:
 
   /** The capture set of the type underlying CaptureRef */
   def ofInfo(ref: CaptureRef)(using Context): CaptureSet = ref match
-    case ref: TermRef if ref.isRootCapability => ref.singletonCaptureSet
+    case ref: (TermRef | TermParamRef) if ref.isMaxCapability => ref.singletonCaptureSet
     case ReachCapability(ref1) => deepCaptureSet(ref1.widen)
       .showing(i"Deep capture set of $ref: ${ref1.widen} = $result", capt)
     case _ => ofType(ref.underlying, followResult = true)
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index cad06e973741..f1f90ea5a41c 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -2269,7 +2269,7 @@ object Types extends TypeUtils {
      *  set of the underlying type is not always empty.
      */
     final def isTracked(using Context): Boolean =
-      isTrackableRef && (isRootCapability || !captureSetOfInfo.isAlwaysEmpty)
+      isTrackableRef && (isMaxCapability || !captureSetOfInfo.isAlwaysEmpty)
 
     /** Is this a reach reference of the form `x*`? */
     def isReach(using Context): Boolean = false // overridden in AnnotatedType
@@ -2283,6 +2283,9 @@ object Types extends TypeUtils {
     /** Is this reference the generic root capability `cap` ? */
     def isRootCapability(using Context): Boolean = false
 
+    /** Is this reference capability that does not derive from another capability ? */
+    def isMaxCapability(using Context): Boolean = false
+
     /** Normalize reference so that it can be compared with `eq` for equality */
     def normalizedRef(using Context): CaptureRef = this
 
@@ -3020,6 +3023,9 @@ object Types extends TypeUtils {
     override def isRootCapability(using Context): Boolean =
       name == nme.CAPTURE_ROOT && symbol == defn.captureRoot
 
+    override def isMaxCapability(using Context): Boolean =
+      widen.derivesFrom(defn.Caps_Cap) && symbol.isStableMember
+
     override def normalizedRef(using Context): CaptureRef =
       if isTrackableRef then symbol.termRef else this
   }
@@ -4819,6 +4825,7 @@ object Types extends TypeUtils {
     def kindString: String = "Term"
     def copyBoundType(bt: BT): Type = bt.paramRefs(paramNum)
     override def isTrackableRef(using Context) = true
+    override def isMaxCapability(using Context) = widen.derivesFrom(defn.Caps_Cap)
   }
 
   private final class TermParamRefImpl(binder: TermLambda, paramNum: Int) extends TermParamRef(binder, paramNum)
diff --git a/library/src/scala/caps.scala b/library/src/scala/caps.scala
index c7fc8e7ba584..9e21b4af1f1e 100644
--- a/library/src/scala/caps.scala
+++ b/library/src/scala/caps.scala
@@ -13,8 +13,6 @@ import annotation.experimental
   /** The universal capture reference */
   val cap: Cap = Cap()
 
-  given Cap = cap
-
   /** Reach capabilities x* which appear as terms in @retains annotations are encoded
    *  as `caps.reachCapability(x)`. When converted to CaptureRef types in capture sets
    *  they are  represented as `x.type @annotation.internal.reachCapability`.
diff --git a/tests/neg-custom-args/captures/filevar.scala b/tests/neg-custom-args/captures/filevar.scala
index 59b8415d6e0f..bcf2d7beccbf 100644
--- a/tests/neg-custom-args/captures/filevar.scala
+++ b/tests/neg-custom-args/captures/filevar.scala
@@ -9,7 +9,7 @@ class Service:
   def log = file.write("log")
 
 def withFile[T](op: (l: caps.Cap) ?-> (f: File^{l}) => T): T =
-  op(new File)
+  op(using caps.cap)(new File)
 
 def test =
   withFile: f =>
diff --git a/tests/neg-custom-args/captures/i15923.scala b/tests/neg-custom-args/captures/i15923.scala
index 754fd0687037..89688449bdac 100644
--- a/tests/neg-custom-args/captures/i15923.scala
+++ b/tests/neg-custom-args/captures/i15923.scala
@@ -5,7 +5,7 @@ def mkId[X](x: X): Id[X] = [T] => (op: X => T) => op(x)
 def bar() = {
   def withCap[X](op: (lcap: caps.Cap) ?-> Cap^{lcap} => X): X = {
     val cap: Cap = new Cap { def use() = { println("cap is used"); 0 } }
-    val result = op(cap)
+    val result = op(using caps.cap)(cap)
     result
   }
 
diff --git a/tests/neg-custom-args/captures/stack-alloc.scala b/tests/neg-custom-args/captures/stack-alloc.scala
index befafbf13003..1b93d2e5129d 100644
--- a/tests/neg-custom-args/captures/stack-alloc.scala
+++ b/tests/neg-custom-args/captures/stack-alloc.scala
@@ -9,7 +9,7 @@ def withFreshPooled[T](op: (lcap: caps.Cap) ?-> Pooled^{lcap} => T): T =
   if nextFree >= stack.size then stack.append(new Pooled)
   val pooled = stack(nextFree)
   nextFree = nextFree + 1
-  val ret = op(pooled)
+  val ret = op(using caps.cap)(pooled)
   nextFree = nextFree - 1
   ret
 
diff --git a/tests/neg-custom-args/captures/usingLogFile.scala b/tests/neg-custom-args/captures/usingLogFile.scala
index 67e6f841e7ce..25b853913af9 100644
--- a/tests/neg-custom-args/captures/usingLogFile.scala
+++ b/tests/neg-custom-args/captures/usingLogFile.scala
@@ -5,7 +5,7 @@ object Test1:
 
   def usingLogFile[T](op: (local: caps.Cap) ?-> FileOutputStream => T): T =
     val logFile = FileOutputStream("log")
-    val result = op(logFile)
+    val result = op(using caps.cap)(logFile)
     logFile.close()
     result
 

From 8dc27b131be9ac1878ae4e738c35d2c831871ba3 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sat, 11 May 2024 23:08:05 +0200
Subject: [PATCH 02/14] Handle tracked class parameters

The current handling of class type refinements is unsound. We cannot simply
use a variable for the capture set of a class argument. What we need to do
instead is treat class arguments as tracked.

In this commit we at least allow explicitly declared tracked arguments. This needed
two modifications:

 - Don't additionally add a capture set for tracked arguments
 - Handle the case where a capture reference is of a singleton type which
   is another capture reference.

As a next step we should treat all class arguments as implicitly tracked.
---
 compiler/src/dotty/tools/dotc/cc/CaptureSet.scala |  5 +++++
 compiler/src/dotty/tools/dotc/cc/Setup.scala      |  4 +++-
 compiler/src/dotty/tools/dotc/core/Types.scala    | 11 +++++++++--
 3 files changed, 17 insertions(+), 3 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index 5a60506cc49a..3c2dab7c46e0 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -147,6 +147,7 @@ sealed abstract class CaptureSet extends Showable:
    *   this subsumes this.f
    *   x subsumes y  ==>  x* subsumes y, x subsumes y?
    *   x subsumes y  ==>  x* subsumes y*, x? subsumes y?
+   *   x: x1.type /\ x1 subsumes y  ==>  x subsumes y
    */
   extension (x: CaptureRef)
      private def subsumes(y: CaptureRef)(using Context): Boolean =
@@ -158,6 +159,10 @@ sealed abstract class CaptureSet extends Showable:
           case _ => false
       || x.match
           case ReachCapability(x1) => x1.subsumes(y.stripReach)
+          case x: TermRef =>
+            x.info match
+              case x1: CaptureRef => x1.subsumes(y)
+              case _ => false
           case _ => false
 
   /** {x} <:< this   where <:< is subcapturing, but treating all variables
diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala
index e6953dbf67b7..d909bccc8070 100644
--- a/compiler/src/dotty/tools/dotc/cc/Setup.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -196,7 +196,9 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
             case cls: ClassSymbol
             if !defn.isFunctionClass(cls) && cls.is(CaptureChecked) =>
               cls.paramGetters.foldLeft(tp) { (core, getter) =>
-                if atPhase(thisPhase.next)(getter.termRef.isTracked) then
+                if atPhase(thisPhase.next)(getter.termRef.isTracked)
+                    && !getter.is(Tracked)
+                then
                   val getterType =
                     mapInferred(refine = false)(tp.memberInfo(getter)).strippedDealias
                   RefinedType(core, getter.name,
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index f1f90ea5a41c..22a985c6c174 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -6172,8 +6172,15 @@ object Types extends TypeUtils {
     def inverse: BiTypeMap
 
     /** A restriction of this map to a function on tracked CaptureRefs */
-    def forward(ref: CaptureRef): CaptureRef = this(ref) match
-      case result: CaptureRef if result.isTrackableRef => result
+    def forward(ref: CaptureRef): CaptureRef =
+      val result = this(ref)
+      def ensureTrackable(tp: Type): CaptureRef = tp match
+        case tp: CaptureRef =>
+          if tp.isTrackableRef then tp
+          else ensureTrackable(tp.underlying)
+        case _ =>
+          assert(false, i"not a trackable captureRef ref: $result, ${result.underlyingIterator.toList}")
+      ensureTrackable(result)
 
     /** A restriction of the inverse to a function on tracked CaptureRefs */
     def backward(ref: CaptureRef): CaptureRef = inverse(ref) match

From edf62ef80156e485345ab52f4de3f4c16f32e90a Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sat, 11 May 2024 23:08:50 +0200
Subject: [PATCH 03/14] Drop @capability annotations

Replace with references that inherit trait `Capability`.
---
 .../src/dotty/tools/dotc/cc/CaptureOps.scala  | 19 ++++-
 .../src/dotty/tools/dotc/cc/CaptureSet.scala  |  3 +-
 .../dotty/tools/dotc/cc/CheckCaptures.scala   | 10 ++-
 compiler/src/dotty/tools/dotc/cc/Setup.scala  |  6 +-
 .../dotty/tools/dotc/core/Definitions.scala   |  5 +-
 .../src/dotty/tools/dotc/core/Types.scala     |  7 +-
 library/src/scala/CanThrow.scala              |  4 +-
 library/src/scala/annotation/capability.scala |  4 +-
 library/src/scala/caps.scala                  | 11 ++-
 tests/disabled/pos/lazylist.scala             |  2 +-
 .../captures/box-unsoundness.scala            |  1 -
 tests/neg-custom-args/captures/byname.check   |  2 +-
 tests/neg-custom-args/captures/byname.scala   |  2 +-
 .../captures/capt-box-env.scala               |  2 +-
 tests/neg-custom-args/captures/capt-box.scala |  2 +-
 tests/neg-custom-args/captures/capt-wf2.scala |  2 +-
 .../captures/caseclass/Test_2.scala           |  2 +-
 tests/neg-custom-args/captures/cc-this.scala  |  2 +-
 tests/neg-custom-args/captures/cc-this2.check |  2 +-
 tests/neg-custom-args/captures/cc-this3.scala |  2 +-
 tests/neg-custom-args/captures/cc-this5.check |  2 +-
 tests/neg-custom-args/captures/cc-this5.scala |  4 +-
 .../captures/class-constr.scala               |  2 +-
 .../captures/effect-swaps-explicit.check      | 29 +++++++
 .../captures/effect-swaps-explicit.scala      | 76 +++++++++++++++++++
 .../captures/effect-swaps.check               | 15 ++--
 .../captures/effect-swaps.scala               | 14 +++-
 .../captures/exception-definitions.check      |  2 +-
 .../captures/extending-cap-classes.scala      | 15 ----
 tests/neg-custom-args/captures/filevar.scala  |  2 +-
 tests/neg-custom-args/captures/i15923.scala   |  2 +-
 tests/neg-custom-args/captures/i16725.scala   |  7 +-
 .../captures/inner-classes.scala              |  2 +-
 .../captures/stack-alloc.scala                |  2 +-
 tests/neg-custom-args/captures/try3.scala     |  2 +-
 .../captures/usingLogFile.scala               |  2 +-
 tests/neg/unsound-reach.check                 | 10 +--
 tests/neg/unsound-reach.scala                 | 16 ++--
 tests/pos-custom-args/captures/boxed1.scala   |  2 +-
 .../captures/capt-capability.scala            | 16 ++--
 .../pos-custom-args/captures/caseclass.scala  |  2 +-
 tests/pos-custom-args/captures/cc-this.scala  |  2 +-
 .../captures/eta-expansions.scala             |  2 +-
 .../captures/filevar-tracked.scala            | 38 ++++++++++
 tests/pos-custom-args/captures/filevar.scala  | 13 ++--
 tests/pos-custom-args/captures/i16116.scala   |  3 +-
 tests/pos-custom-args/captures/i16226.scala   |  2 +-
 tests/pos-custom-args/captures/i19751.scala   |  2 +-
 tests/pos-custom-args/captures/lazyref.scala  |  2 +-
 tests/pos-custom-args/captures/lists.scala    |  4 +-
 .../captures/logger-tracked.scala             | 68 +++++++++++++++++
 tests/pos-custom-args/captures/logger.scala   |  9 ++-
 .../captures/nested-classes-tracked.scala     | 22 ++++++
 .../captures/nested-classes.scala             |  9 ++-
 .../captures/null-logger.scala                |  2 +-
 tests/pos-custom-args/captures/pairs.scala    |  6 +-
 tests/pos-custom-args/captures/reaches.scala  |  2 +-
 tests/pos-custom-args/captures/try3.scala     |  2 +-
 tests/pos-custom-args/captures/vars.scala     |  2 +-
 tests/pos/dotty-experimental.scala            |  2 +-
 tests/pos/i20237.scala                        |  2 +-
 tests/pos/into-bigint.scala                   |  4 +-
 62 files changed, 382 insertions(+), 130 deletions(-)
 create mode 100644 tests/neg-custom-args/captures/effect-swaps-explicit.check
 create mode 100644 tests/neg-custom-args/captures/effect-swaps-explicit.scala
 delete mode 100644 tests/neg-custom-args/captures/extending-cap-classes.scala
 create mode 100644 tests/pos-custom-args/captures/filevar-tracked.scala
 create mode 100644 tests/pos-custom-args/captures/logger-tracked.scala
 create mode 100644 tests/pos-custom-args/captures/nested-classes-tracked.scala

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
index 5c9946f6134a..9b899030bc02 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
@@ -203,6 +203,23 @@ extension (tp: Type)
     case _ =>
       false
 
+  /** Does type derive from caps.Capability?, which means it references of this
+   *  type are maximal capabilities?
+   */
+  def derivesFromCapability(using Context): Boolean = tp.dealias match
+    case tp: (TypeRef | AppliedType) =>
+      val sym = tp.typeSymbol
+      if sym.isClass then sym.derivesFrom(defn.Caps_Capability)
+      else tp.superType.derivesFromCapability
+    case tp: TypeProxy =>
+      tp.superType.derivesFromCapability
+    case tp: AndType =>
+      tp.tp1.derivesFromCapability || tp.tp2.derivesFromCapability
+    case tp: OrType =>
+      tp.tp1.derivesFromCapability && tp.tp2.derivesFromCapability
+    case _ =>
+      false
+
   /** Drop @retains annotations everywhere */
   def dropAllRetains(using Context): Type = // TODO we should drop retains from inferred types before unpickling
     val tm = new TypeMap:
@@ -408,7 +425,7 @@ extension (sym: Symbol)
   /** The owner of the current level. Qualifying owners are
    *   - methods other than constructors and anonymous functions
    *   - anonymous functions, provided they either define a local
-   *     root of type caps.Cap, or they are the rhs of a val definition.
+   *     root of type caps.Capability, or they are the rhs of a val definition.
    *   - classes, if they are not staticOwners
    *   - _root_
    */
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index 3c2dab7c46e0..06ba36bd5e24 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -1051,7 +1051,8 @@ object CaptureSet:
         case tp: TermParamRef =>
           tp.captureSet
         case tp: TypeRef =>
-          if tp.typeSymbol == defn.Caps_Cap then universal else empty
+          if tp.derivesFromCapability then universal // TODO: maybe return another value that indicates that the underltinf ref is maximal?
+          else empty
         case _: TypeParamRef =>
           empty
         case CapturingType(parent, refs) =>
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index a5bb8792af2c..cd0f21129ac9 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -537,8 +537,8 @@ class CheckCaptures extends Recheck, SymTransformer:
          */
         def addParamArgRefinements(core: Type, initCs: CaptureSet): (Type, CaptureSet) =
           var refined: Type = core
-          var allCaptures: CaptureSet = if setup.isCapabilityClassRef(core)
-            then CaptureSet.universal else initCs
+          var allCaptures: CaptureSet =
+            if core.derivesFromCapability then CaptureSet.universal else initCs
           for (getterName, argType) <- mt.paramNames.lazyZip(argTypes) do
             val getter = cls.info.member(getterName).suchThat(_.is(ParamAccessor)).symbol
             if getter.termRef.isTracked && !getter.is(Private) then
@@ -572,8 +572,10 @@ class CheckCaptures extends Recheck, SymTransformer:
         val TypeApply(fn, args) = tree
         val polyType = atPhase(thisPhase.prev):
           fn.tpe.widen.asInstanceOf[TypeLambda]
+        def isExempt(sym: Symbol) =
+          sym.isTypeTestOrCast || sym == defn.Compiletime_erasedValue
         for case (arg: TypeTree, formal, pname) <- args.lazyZip(polyType.paramRefs).lazyZip((polyType.paramNames)) do
-          if !tree.symbol.isTypeTestOrCast then
+          if !isExempt(tree.symbol) then
             def where = if fn.symbol.exists then i" in an argument of ${fn.symbol}" else ""
             disallowRootCapabilitiesIn(arg.knownType, NoSymbol,
               i"Sealed type variable $pname", "be instantiated to",
@@ -1305,7 +1307,7 @@ class CheckCaptures extends Recheck, SymTransformer:
                 case ref: TermParamRef
                 if !allowed.contains(ref) && !seen.contains(ref) =>
                   seen += ref
-                  if ref.underlying.isRef(defn.Caps_Cap) then
+                  if ref.underlying.isRef(defn.Caps_Capability) then
                     report.error(i"escaping local reference $ref", tree.srcPos)
                   else
                     val widened = ref.captureSetOfInfo
diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala
index d909bccc8070..1a8c65c89a43 100644
--- a/compiler/src/dotty/tools/dotc/cc/Setup.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -77,9 +77,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
   def isCapabilityClassRef(tp: Type)(using Context): Boolean = tp.dealiasKeepAnnots match
     case _: TypeRef | _: AppliedType =>
       val sym = tp.classSymbol
-      def checkSym: Boolean =
-        sym.hasAnnotation(defn.CapabilityAnnot)
-        || sym.info.parents.exists(hasUniversalCapability)
+      def checkSym: Boolean = sym.info.parents.exists(hasUniversalCapability)
       sym.isClass && capabilityClassMap.getOrElseUpdate(sym, checkSym)
     case _ => false
 
@@ -594,7 +592,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
         if sym.isClass then
           !sym.isPureClass
         else
-          sym != defn.Caps_Cap && instanceCanBeImpure(tp.superType)
+          sym != defn.Caps_Capability && instanceCanBeImpure(tp.superType)
       case tp: (RefinedOrRecType | MatchType) =>
         instanceCanBeImpure(tp.underlying)
       case tp: AndType =>
diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala
index 11a4a8473e79..52535f26c692 100644
--- a/compiler/src/dotty/tools/dotc/core/Definitions.scala
+++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala
@@ -991,7 +991,7 @@ class Definitions {
 
   @tu lazy val CapsModule: Symbol = requiredModule("scala.caps")
     @tu lazy val captureRoot: TermSymbol = CapsModule.requiredValue("cap")
-    @tu lazy val Caps_Cap: TypeSymbol = CapsModule.requiredType("Cap")
+    @tu lazy val Caps_Capability: TypeSymbol = CapsModule.requiredType("Capability")
     @tu lazy val Caps_reachCapability: TermSymbol = CapsModule.requiredMethod("reachCapability")
     @tu lazy val CapsUnsafeModule: Symbol = requiredModule("scala.caps.unsafe")
     @tu lazy val Caps_unsafeAssumePure: Symbol = CapsUnsafeModule.requiredMethod("unsafeAssumePure")
@@ -1014,7 +1014,6 @@ class Definitions {
   @tu lazy val BeanPropertyAnnot: ClassSymbol = requiredClass("scala.beans.BeanProperty")
   @tu lazy val BooleanBeanPropertyAnnot: ClassSymbol = requiredClass("scala.beans.BooleanBeanProperty")
   @tu lazy val BodyAnnot: ClassSymbol = requiredClass("scala.annotation.internal.Body")
-  @tu lazy val CapabilityAnnot: ClassSymbol = requiredClass("scala.annotation.capability")
   @tu lazy val ChildAnnot: ClassSymbol = requiredClass("scala.annotation.internal.Child")
   @tu lazy val ContextResultCountAnnot: ClassSymbol = requiredClass("scala.annotation.internal.ContextResultCount")
   @tu lazy val ProvisionalSuperClassAnnot: ClassSymbol = requiredClass("scala.annotation.internal.ProvisionalSuperClass")
@@ -2033,7 +2032,7 @@ class Definitions {
    */
   @tu lazy val ccExperimental: Set[Symbol] = Set(
     CapsModule, CapsModule.moduleClass, PureClass,
-    CapabilityAnnot, RequiresCapabilityAnnot,
+    RequiresCapabilityAnnot,
     RetainsAnnot, RetainsCapAnnot, RetainsByNameAnnot)
 
   /** Experimental language features defined in `scala.runtime.stdLibPatches.language.experimental`.
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index 22a985c6c174..7a5a92e836fd 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -3024,7 +3024,8 @@ object Types extends TypeUtils {
       name == nme.CAPTURE_ROOT && symbol == defn.captureRoot
 
     override def isMaxCapability(using Context): Boolean =
-      widen.derivesFrom(defn.Caps_Cap) && symbol.isStableMember
+      import cc.*
+      this.derivesFromCapability && symbol.isStableMember
 
     override def normalizedRef(using Context): CaptureRef =
       if isTrackableRef then symbol.termRef else this
@@ -4825,7 +4826,9 @@ object Types extends TypeUtils {
     def kindString: String = "Term"
     def copyBoundType(bt: BT): Type = bt.paramRefs(paramNum)
     override def isTrackableRef(using Context) = true
-    override def isMaxCapability(using Context) = widen.derivesFrom(defn.Caps_Cap)
+    override def isMaxCapability(using Context) =
+      import cc.*
+      this.derivesFromCapability
   }
 
   private final class TermParamRefImpl(binder: TermLambda, paramNum: Int) extends TermParamRef(binder, paramNum)
diff --git a/library/src/scala/CanThrow.scala b/library/src/scala/CanThrow.scala
index c7f23a393715..91c94229c43c 100644
--- a/library/src/scala/CanThrow.scala
+++ b/library/src/scala/CanThrow.scala
@@ -6,9 +6,9 @@ import annotation.{implicitNotFound, experimental, capability}
  *  experimental.saferExceptions feature, a `throw Ex()` expression will require
  *  a given of class `CanThrow[Ex]` to be available.
  */
-@experimental @capability
+@experimental
 @implicitNotFound("The capability to throw exception ${E} is missing.\nThe capability can be provided by one of the following:\n - Adding a using clause `(using CanThrow[${E}])` to the definition of the enclosing method\n - Adding `throws ${E}` clause after the result type of the enclosing method\n - Wrapping this piece of code with a `try` block that catches ${E}")
-erased class CanThrow[-E <: Exception]
+erased class CanThrow[-E <: Exception] extends caps.Capability
 
 @experimental
 object unsafeExceptions:
diff --git a/library/src/scala/annotation/capability.scala b/library/src/scala/annotation/capability.scala
index 4696ed6a015e..d3453e3c8168 100644
--- a/library/src/scala/annotation/capability.scala
+++ b/library/src/scala/annotation/capability.scala
@@ -11,4 +11,6 @@ import annotation.experimental
  *  THere, the capture set of any instance of `CanThrow` is assumed to be
  *  `{*}`.
  */
-@experimental final class capability extends StaticAnnotation
+@experimental
+@deprecated("To make a class a capability, let it derive from the `Capability` trait instead")
+final class capability extends StaticAnnotation
diff --git a/library/src/scala/caps.scala b/library/src/scala/caps.scala
index 9e21b4af1f1e..215ad2cb5697 100644
--- a/library/src/scala/caps.scala
+++ b/library/src/scala/caps.scala
@@ -4,14 +4,17 @@ import annotation.experimental
 
 @experimental object caps:
 
-  class Cap // should be @erased
+  trait Capability // should be @erased
+
+  /** The universal capture reference */
+  val cap: Capability = new Capability() {}
 
   /** The universal capture reference (deprecated) */
   @deprecated("Use `cap` instead")
-  val `*`: Cap = cap
+  val `*`: Capability = cap
 
-  /** The universal capture reference */
-  val cap: Cap = Cap()
+  @deprecated("Use `Capability` instead")
+  type Cap = Capability
 
   /** Reach capabilities x* which appear as terms in @retains annotations are encoded
    *  as `caps.reachCapability(x)`. When converted to CaptureRef types in capture sets
diff --git a/tests/disabled/pos/lazylist.scala b/tests/disabled/pos/lazylist.scala
index c24f8677b91f..e56eb484894c 100644
--- a/tests/disabled/pos/lazylist.scala
+++ b/tests/disabled/pos/lazylist.scala
@@ -34,7 +34,7 @@ object LazyNil extends LazyList[Nothing]:
 def map[A, B](xs: {*} LazyList[A], f: {*} A => B): {f, xs} LazyList[B] =
   xs.map(f)
 
-@annotation.capability class Cap
+class Cap extends caps.Capability
 
 def test(cap1: Cap, cap2: Cap, cap3: Cap) =
   def f[T](x: LazyList[T]): LazyList[T] = if cap1 == cap1 then x else LazyNil
diff --git a/tests/neg-custom-args/captures/box-unsoundness.scala b/tests/neg-custom-args/captures/box-unsoundness.scala
index d1331f16df1f..8c1c22bc7fa6 100644
--- a/tests/neg-custom-args/captures/box-unsoundness.scala
+++ b/tests/neg-custom-args/captures/box-unsoundness.scala
@@ -1,4 +1,3 @@
-//@annotation.capability
 class CanIO { def use(): Unit = () }
 def use[X](x: X): (op: X -> Unit) -> Unit = op => op(x)
 def test(io: CanIO^): Unit =
diff --git a/tests/neg-custom-args/captures/byname.check b/tests/neg-custom-args/captures/byname.check
index e06a3a1f8268..2b48428e97bc 100644
--- a/tests/neg-custom-args/captures/byname.check
+++ b/tests/neg-custom-args/captures/byname.check
@@ -1,7 +1,7 @@
 -- Error: tests/neg-custom-args/captures/byname.scala:19:5 -------------------------------------------------------------
 19 |  h(g()) // error
    |    ^^^
-   |    reference (cap2 : Cap^) is not included in the allowed capture set {cap1}
+   |    reference (cap2 : Cap) is not included in the allowed capture set {cap1}
    |    of an enclosing function literal with expected type () ?->{cap1} I
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/byname.scala:4:2 -----------------------------------------
  4 |  def f() = if cap1 == cap1 then g else g // error
diff --git a/tests/neg-custom-args/captures/byname.scala b/tests/neg-custom-args/captures/byname.scala
index 279122f54735..0ed3a09cb414 100644
--- a/tests/neg-custom-args/captures/byname.scala
+++ b/tests/neg-custom-args/captures/byname.scala
@@ -1,4 +1,4 @@
-@annotation.capability class Cap
+class Cap extends caps.Capability
 
 def test(cap1: Cap, cap2: Cap) =
   def f() = if cap1 == cap1 then g else g // error
diff --git a/tests/neg-custom-args/captures/capt-box-env.scala b/tests/neg-custom-args/captures/capt-box-env.scala
index 605b446d5262..bfe1874d073b 100644
--- a/tests/neg-custom-args/captures/capt-box-env.scala
+++ b/tests/neg-custom-args/captures/capt-box-env.scala
@@ -1,4 +1,4 @@
-@annotation.capability class Cap
+class Cap extends caps.Capability
 
 class Pair[+A, +B](x: A, y: B):
     def fst: A = x
diff --git a/tests/neg-custom-args/captures/capt-box.scala b/tests/neg-custom-args/captures/capt-box.scala
index 634470704fc5..291882bed36d 100644
--- a/tests/neg-custom-args/captures/capt-box.scala
+++ b/tests/neg-custom-args/captures/capt-box.scala
@@ -1,4 +1,4 @@
-@annotation.capability class Cap
+class Cap extends caps.Capability
 
 def test(x: Cap) =
 
diff --git a/tests/neg-custom-args/captures/capt-wf2.scala b/tests/neg-custom-args/captures/capt-wf2.scala
index 6c65e0dc77f7..8bb04a230fdd 100644
--- a/tests/neg-custom-args/captures/capt-wf2.scala
+++ b/tests/neg-custom-args/captures/capt-wf2.scala
@@ -1,4 +1,4 @@
-@annotation.capability class C
+class C extends caps.Capability
 
 def test(c: C) =
   var x: Any^{c} = ???
diff --git a/tests/neg-custom-args/captures/caseclass/Test_2.scala b/tests/neg-custom-args/captures/caseclass/Test_2.scala
index bffc0a295bdc..9d97d5537c72 100644
--- a/tests/neg-custom-args/captures/caseclass/Test_2.scala
+++ b/tests/neg-custom-args/captures/caseclass/Test_2.scala
@@ -1,4 +1,4 @@
-@annotation.capability class C
+class C extends caps.Capability
 def test(c: C) =
   val pure: () -> Unit = () => ()
   val impure: () => Unit = pure
diff --git a/tests/neg-custom-args/captures/cc-this.scala b/tests/neg-custom-args/captures/cc-this.scala
index 4c05be702c51..e4336ed457af 100644
--- a/tests/neg-custom-args/captures/cc-this.scala
+++ b/tests/neg-custom-args/captures/cc-this.scala
@@ -1,4 +1,4 @@
-@annotation.capability class Cap
+class Cap extends caps.Capability
 
 def eff(using Cap): Unit = ()
 
diff --git a/tests/neg-custom-args/captures/cc-this2.check b/tests/neg-custom-args/captures/cc-this2.check
index bd9a1085d262..6cb3010d6174 100644
--- a/tests/neg-custom-args/captures/cc-this2.check
+++ b/tests/neg-custom-args/captures/cc-this2.check
@@ -2,7 +2,7 @@
 -- Error: tests/neg-custom-args/captures/cc-this2/D_2.scala:3:8 --------------------------------------------------------
 3 |  this: D^ => // error
   |        ^^
-  |reference (caps.cap : caps.Cap) captured by this self type is not included in the allowed capture set {} of pure base class class C
+  |reference (caps.cap : caps.Capability) captured by this self type is not included in the allowed capture set {} of pure base class class C
 -- [E058] Type Mismatch Error: tests/neg-custom-args/captures/cc-this2/D_2.scala:2:6 -----------------------------------
 2 |class D extends C: // error
   |      ^
diff --git a/tests/neg-custom-args/captures/cc-this3.scala b/tests/neg-custom-args/captures/cc-this3.scala
index 25af19dd6c4a..0a36cde8173b 100644
--- a/tests/neg-custom-args/captures/cc-this3.scala
+++ b/tests/neg-custom-args/captures/cc-this3.scala
@@ -1,4 +1,4 @@
-@annotation.capability class Cap
+class Cap extends caps.Capability
 
 def eff(using Cap): Unit = ()
 
diff --git a/tests/neg-custom-args/captures/cc-this5.check b/tests/neg-custom-args/captures/cc-this5.check
index 8affe7005e2e..1329734ce37d 100644
--- a/tests/neg-custom-args/captures/cc-this5.check
+++ b/tests/neg-custom-args/captures/cc-this5.check
@@ -1,7 +1,7 @@
 -- Error: tests/neg-custom-args/captures/cc-this5.scala:16:20 ----------------------------------------------------------
 16 |    def f = println(c)  // error
    |                    ^
-   |                    (c : Cap^) cannot be referenced here; it is not included in the allowed capture set {}
+   |                    (c : Cap) cannot be referenced here; it is not included in the allowed capture set {}
    |                    of the enclosing class A
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-this5.scala:21:15 -------------------------------------
 21 |    val x: A = this // error
diff --git a/tests/neg-custom-args/captures/cc-this5.scala b/tests/neg-custom-args/captures/cc-this5.scala
index e84c2a41f55c..4c9a8a706670 100644
--- a/tests/neg-custom-args/captures/cc-this5.scala
+++ b/tests/neg-custom-args/captures/cc-this5.scala
@@ -1,7 +1,7 @@
 class C:
   val x: C = this
 
-@annotation.capability class Cap
+class Cap extends caps.Capability
 
 def foo(c: Cap) =
   object D extends C:   // error
@@ -17,5 +17,5 @@ def test(c: Cap) =
 
 def test2(c: Cap) =
   class A:
-    def f = println(c) 
+    def f = println(c)
     val x: A = this // error
diff --git a/tests/neg-custom-args/captures/class-constr.scala b/tests/neg-custom-args/captures/class-constr.scala
index 9afb6972ccfa..619fa9fa0341 100644
--- a/tests/neg-custom-args/captures/class-constr.scala
+++ b/tests/neg-custom-args/captures/class-constr.scala
@@ -1,6 +1,6 @@
 import annotation.{capability, constructorOnly}
 
-@capability class Cap
+class Cap extends caps.Capability
 
 class C(x: Cap, @constructorOnly y: Cap)
 
diff --git a/tests/neg-custom-args/captures/effect-swaps-explicit.check b/tests/neg-custom-args/captures/effect-swaps-explicit.check
new file mode 100644
index 000000000000..47559ab97568
--- /dev/null
+++ b/tests/neg-custom-args/captures/effect-swaps-explicit.check
@@ -0,0 +1,29 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps-explicit.scala:64:8 -------------------------
+63 |      Result:
+64 |        Future: // error, type mismatch
+   |      ^
+   |      Found:    Result.Ok[box Future[box T^?]^{fr, contextual$1}]
+   |      Required: Result[Future[T], Nothing]
+65 |          fr.await.ok
+   |--------------------------------------------------------------------------------------------------------------------
+   |Inline stack trace
+   |- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
+   |This location contains code that was inlined from effect-swaps-explicit.scala:41
+41 |    boundary(Ok(body))
+   |             ^^^^^^^^
+    --------------------------------------------------------------------------------------------------------------------
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps-explicit.scala:74:10 ------------------------
+74 |          Future: fut ?=> // error: type mismatch
+   |          ^
+   |          Found:    Future[box T^?]^{fr, lbl}
+   |          Required: Future[box T^?]^?
+75 |            fr.await.ok
+   |
+   | longer explanation available when compiling with `-explain`
+-- Error: tests/neg-custom-args/captures/effect-swaps-explicit.scala:68:15 ---------------------------------------------
+68 |        Result.make: //lbl ?=> // error, escaping label from Result
+   |        ^^^^^^^^^^^
+   |local reference contextual$9 from (using contextual$9: boundary.Label[Result[box Future[box T^?]^{fr, contextual$9}, box E^?]]^):
+   |  box Future[box T^?]^{fr, contextual$9} leaks into outer capture set of type parameter T of method make in object Result
diff --git a/tests/neg-custom-args/captures/effect-swaps-explicit.scala b/tests/neg-custom-args/captures/effect-swaps-explicit.scala
new file mode 100644
index 000000000000..814199706721
--- /dev/null
+++ b/tests/neg-custom-args/captures/effect-swaps-explicit.scala
@@ -0,0 +1,76 @@
+import annotation.capability
+
+object boundary:
+
+  final class Label[-T] // extends caps.Capability
+
+  /** Abort current computation and instead return `value` as the value of
+   *  the enclosing `boundary` call that created `label`.
+   */
+  def break[T](value: T)(using label: Label[T]^): Nothing = ???
+
+  def apply[T](body: Label[T]^ ?=> T): T = ???
+end boundary
+
+import boundary.{Label, break}
+
+trait Async extends caps.Capability
+object Async:
+  def blocking[T](body: Async ?=> T): T = ???
+
+class Future[+T]:
+  this: Future[T]^ =>
+  def await(using Async): T = ???
+object Future:
+  def apply[T](op: Async ?=> T)(using Async): Future[T]^{op} = ???
+
+enum Result[+T, +E]:
+  case Ok[+T](value: T) extends Result[T, Nothing]
+  case Err[+E](error: E) extends Result[Nothing, E]
+
+
+object Result:
+  extension [T, E](r: Result[T, E]^)(using Label[Err[E]]^)
+
+    /** `_.ok` propagates Err to current Label */
+    def ok: T = r match
+      case Ok(value) => value
+      case Err(value) => break[Err[E]](Err(value))
+
+  transparent inline def apply[T, E](inline body: Label[Result[T, E]]^ ?=> T): Result[T, E] =
+    boundary(Ok(body))
+
+  // same as apply, but not an inline method
+  def make[T, E](body: Label[Result[T, E]]^ ?=> T): Result[T, E] =
+    boundary(Ok(body))
+
+end Result
+
+def test[T, E](using Async) =
+  import Result.*
+  Async.blocking: async ?=>
+    val good1: List[Future[Result[T, E]]] => Future[Result[List[T], E]] = frs =>
+      Future:
+        Result:
+          frs.map(_.await.ok) // OK
+
+    val good2: Result[Future[T], E] => Future[Result[T, E]] = rf =>
+      Future:
+        Result:
+          rf.ok.await  // OK, Future argument has type Result[T]
+
+    def fail3(fr: Future[Result[T, E]]^) =
+      Result:
+        Future: // error, type mismatch
+          fr.await.ok
+
+    def fail4[T, E](fr: Future[Result[T, E]]^) =
+        Result.make: //lbl ?=> // error, escaping label from Result
+          Future: fut ?=>
+            fr.await.ok
+
+    def fail5[T, E](fr: Future[Result[T, E]]^) =
+        Result.make[Future[T], E]: lbl ?=>
+          Future: fut ?=> // error: type mismatch
+            fr.await.ok
+
diff --git a/tests/neg-custom-args/captures/effect-swaps.check b/tests/neg-custom-args/captures/effect-swaps.check
index bda3509645d1..f16019c15513 100644
--- a/tests/neg-custom-args/captures/effect-swaps.check
+++ b/tests/neg-custom-args/captures/effect-swaps.check
@@ -1,6 +1,6 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps.scala:64:8 ----------------------------------
 63 |      Result:
-64 |        Future: // error, escaping label from Result
+64 |        Future: // error, type mismatch
    |      ^
    |      Found:    Result.Ok[box Future[box T^?]^{fr, contextual$1}]
    |      Required: Result[Future[T], Nothing]
@@ -14,8 +14,11 @@
     --------------------------------------------------------------------------------------------------------------------
    |
    | longer explanation available when compiling with `-explain`
--- Error: tests/neg-custom-args/captures/effect-swaps.scala:68:15 ------------------------------------------------------
-68 |        Result.make: //lbl ?=> // error, escaping label from Result
-   |        ^^^^^^^^^^^
-   |local reference contextual$9 from (using contextual$9: boundary.Label[Result[box Future[box T^?]^{fr, contextual$9}, box E^?]]^):
-   |  box Future[box T^?]^{fr, contextual$9} leaks into outer capture set of type parameter T of method make in object Result
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps.scala:74:10 ---------------------------------
+74 |          Future: fut ?=> // error: type mismatch
+   |          ^
+   |          Found:    Future[box T^?]^{fr, lbl}
+   |          Required: Future[box T^?]^?
+75 |            fr.await.ok
+   |
+   | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/effect-swaps.scala b/tests/neg-custom-args/captures/effect-swaps.scala
index 1d72077bb8da..af44501371a9 100644
--- a/tests/neg-custom-args/captures/effect-swaps.scala
+++ b/tests/neg-custom-args/captures/effect-swaps.scala
@@ -2,7 +2,7 @@ import annotation.capability
 
 object boundary:
 
-  @capability final class Label[-T]
+  final class Label[-T] extends caps.Capability
 
   /** Abort current computation and instead return `value` as the value of
    *  the enclosing `boundary` call that created `label`.
@@ -14,7 +14,7 @@ end boundary
 
 import boundary.{Label, break}
 
-@capability trait Async
+trait Async extends caps.Capability
 object Async:
   def blocking[T](body: Async ?=> T): T = ???
 
@@ -61,10 +61,16 @@ def test[T, E](using Async) =
 
     def fail3(fr: Future[Result[T, E]]^) =
       Result:
-        Future: // error, escaping label from Result
+        Future: // error, type mismatch
           fr.await.ok
 
     def fail4[T, E](fr: Future[Result[T, E]]^) =
-        Result.make: //lbl ?=> // error, escaping label from Result
+        Result.make: //lbl ?=> // should be error, escaping label from Result but infers Result[Any, Any]
           Future: fut ?=>
             fr.await.ok
+
+    def fail5[T, E](fr: Future[Result[T, E]]^) =
+        Result.make[Future[T], E]: lbl ?=>
+          Future: fut ?=> // error: type mismatch
+            fr.await.ok
+
diff --git a/tests/neg-custom-args/captures/exception-definitions.check b/tests/neg-custom-args/captures/exception-definitions.check
index 72b88f252e59..7f915ebd9833 100644
--- a/tests/neg-custom-args/captures/exception-definitions.check
+++ b/tests/neg-custom-args/captures/exception-definitions.check
@@ -1,7 +1,7 @@
 -- Error: tests/neg-custom-args/captures/exception-definitions.scala:3:8 -----------------------------------------------
 3 |  self: Err^ => // error
   |        ^^^^
-  |reference (caps.cap : caps.Cap) captured by this self type is not included in the allowed capture set {} of pure base class class Throwable
+  |reference (caps.cap : caps.Capability) captured by this self type is not included in the allowed capture set {} of pure base class class Throwable
 -- Error: tests/neg-custom-args/captures/exception-definitions.scala:7:12 ----------------------------------------------
 7 |    val x = c  // error
   |            ^
diff --git a/tests/neg-custom-args/captures/extending-cap-classes.scala b/tests/neg-custom-args/captures/extending-cap-classes.scala
deleted file mode 100644
index 17497e415a1e..000000000000
--- a/tests/neg-custom-args/captures/extending-cap-classes.scala
+++ /dev/null
@@ -1,15 +0,0 @@
-import annotation.capability
-
-class C1
-@capability class C2 extends C1
-class C3 extends C2
-
-def test =
-  val x1: C1 = new C1
-  val x2: C1 = new C2 // error
-  val x3: C1 = new C3 // error
-
-  val y1: C2 = new C2
-  val y2: C2 = new C3
-  
-  val z1: C3 = new C3
\ No newline at end of file
diff --git a/tests/neg-custom-args/captures/filevar.scala b/tests/neg-custom-args/captures/filevar.scala
index bcf2d7beccbf..0d9cbed164e3 100644
--- a/tests/neg-custom-args/captures/filevar.scala
+++ b/tests/neg-custom-args/captures/filevar.scala
@@ -8,7 +8,7 @@ class Service:
   var file: File^ = uninitialized  // error
   def log = file.write("log")
 
-def withFile[T](op: (l: caps.Cap) ?-> (f: File^{l}) => T): T =
+def withFile[T](op: (l: caps.Capability) ?-> (f: File^{l}) => T): T =
   op(using caps.cap)(new File)
 
 def test =
diff --git a/tests/neg-custom-args/captures/i15923.scala b/tests/neg-custom-args/captures/i15923.scala
index 89688449bdac..e71f01996938 100644
--- a/tests/neg-custom-args/captures/i15923.scala
+++ b/tests/neg-custom-args/captures/i15923.scala
@@ -3,7 +3,7 @@ type Id[X] = [T] -> (op: X => T) -> T
 def mkId[X](x: X): Id[X] = [T] => (op: X => T) => op(x)
 
 def bar() = {
-  def withCap[X](op: (lcap: caps.Cap) ?-> Cap^{lcap} => X): X = {
+  def withCap[X](op: (lcap: caps.Capability) ?-> Cap^{lcap} => X): X = {
     val cap: Cap = new Cap { def use() = { println("cap is used"); 0 } }
     val result = op(using caps.cap)(cap)
     result
diff --git a/tests/neg-custom-args/captures/i16725.scala b/tests/neg-custom-args/captures/i16725.scala
index ff06b3be78a7..853b3e96ca5c 100644
--- a/tests/neg-custom-args/captures/i16725.scala
+++ b/tests/neg-custom-args/captures/i16725.scala
@@ -1,6 +1,5 @@
 import language.experimental.captureChecking
-@annotation.capability
-class IO:
+class IO extends caps.Capability:
   def brewCoffee(): Unit = ???
 def usingIO[T](op: IO => T): T = ???
 
@@ -8,8 +7,8 @@ type Wrapper[T] = [R] -> (f: T => R) -> R
 def mk[T](x: T): Wrapper[T] = [R] => f => f(x)
 def useWrappedIO(wrapper: Wrapper[IO]): () -> Unit =
   () =>
-    wrapper: io => // error
+    wrapper: io =>
       io.brewCoffee()
 def main(): Unit =
-  val escaped = usingIO(io => useWrappedIO(mk(io)))
+  val escaped = usingIO(io => useWrappedIO(mk(io))) // error // error
   escaped()  // boom
diff --git a/tests/neg-custom-args/captures/inner-classes.scala b/tests/neg-custom-args/captures/inner-classes.scala
index 181b830e4996..fd500e607970 100644
--- a/tests/neg-custom-args/captures/inner-classes.scala
+++ b/tests/neg-custom-args/captures/inner-classes.scala
@@ -1,6 +1,6 @@
 object test:
 
-  @annotation.capability class FileSystem
+  class FileSystem extends caps.Capability
 
   def foo(fs: FileSystem) =
 
diff --git a/tests/neg-custom-args/captures/stack-alloc.scala b/tests/neg-custom-args/captures/stack-alloc.scala
index 1b93d2e5129d..80e7e4169720 100644
--- a/tests/neg-custom-args/captures/stack-alloc.scala
+++ b/tests/neg-custom-args/captures/stack-alloc.scala
@@ -5,7 +5,7 @@ class Pooled
 val stack = mutable.ArrayBuffer[Pooled]()
 var nextFree = 0
 
-def withFreshPooled[T](op: (lcap: caps.Cap) ?-> Pooled^{lcap} => T): T =
+def withFreshPooled[T](op: (lcap: caps.Capability) ?-> Pooled^{lcap} => T): T =
   if nextFree >= stack.size then stack.append(new Pooled)
   val pooled = stack(nextFree)
   nextFree = nextFree + 1
diff --git a/tests/neg-custom-args/captures/try3.scala b/tests/neg-custom-args/captures/try3.scala
index 004cda6a399c..880d20ef16a0 100644
--- a/tests/neg-custom-args/captures/try3.scala
+++ b/tests/neg-custom-args/captures/try3.scala
@@ -4,7 +4,7 @@ class CT[E]
 type CanThrow[E] = CT[E]^
 type Top  = Any^
 
-def handle[E <: Exception, T <: Top](op: (lcap: caps.Cap) ?-> CT[E]^{lcap} ?=> T)(handler: E => T): T =
+def handle[E <: Exception, T <: Top](op: (lcap: caps.Capability) ?-> CT[E]^{lcap} ?=> T)(handler: E => T): T =
   val x: CT[E] = ???
   try op(using caps.cap)(using x)
   catch case ex: E => handler(ex)
diff --git a/tests/neg-custom-args/captures/usingLogFile.scala b/tests/neg-custom-args/captures/usingLogFile.scala
index 25b853913af9..b25e4e75a784 100644
--- a/tests/neg-custom-args/captures/usingLogFile.scala
+++ b/tests/neg-custom-args/captures/usingLogFile.scala
@@ -3,7 +3,7 @@ import annotation.capability
 
 object Test1:
 
-  def usingLogFile[T](op: (local: caps.Cap) ?-> FileOutputStream => T): T =
+  def usingLogFile[T](op: (local: caps.Capability) ?-> FileOutputStream => T): T =
     val logFile = FileOutputStream("log")
     val result = op(using caps.cap)(logFile)
     logFile.close()
diff --git a/tests/neg/unsound-reach.check b/tests/neg/unsound-reach.check
index fd5c401416d1..8cabbe1571a0 100644
--- a/tests/neg/unsound-reach.check
+++ b/tests/neg/unsound-reach.check
@@ -1,5 +1,5 @@
--- Error: tests/neg/unsound-reach.scala:18:9 ---------------------------------------------------------------------------
-18 |    boom.use(f): (f1: File^{backdoor*}) => // error
-   |    ^^^^^^^^
-   |    Reach capability backdoor* and universal capability cap cannot both
-   |    appear in the type (x: File^)(op: box File^{backdoor*} => Unit): Unit of this expression
+-- Error: tests/neg/unsound-reach.scala:18:13 --------------------------------------------------------------------------
+18 |        boom.use(f): (f1: File^{backdoor*}) => // error
+   |        ^^^^^^^^
+   |        Reach capability backdoor* and universal capability cap cannot both
+   |        appear in the type (x: File^)(op: box File^{backdoor*} => Unit): Unit of this expression
diff --git a/tests/neg/unsound-reach.scala b/tests/neg/unsound-reach.scala
index 468730168019..48a74f86d311 100644
--- a/tests/neg/unsound-reach.scala
+++ b/tests/neg/unsound-reach.scala
@@ -5,16 +5,16 @@ trait File:
 def withFile[R](path: String)(op: File^ => R): R = ???
 
 trait Foo[+X]:
-  def use(x: File^)(op: X => Unit): Unit
+    def use(x: File^)(op: X => Unit): Unit
 class Bar extends Foo[File^]:
-  def use(x: File^)(op: File^ => Unit): Unit = op(x)
+    def use(x: File^)(op: File^ => Unit): Unit = op(x)
 
 def bad(): Unit =
-  val backdoor: Foo[File^] = new Bar
-  val boom: Foo[File^{backdoor*}] = backdoor
+    val backdoor: Foo[File^] = new Bar
+    val boom: Foo[File^{backdoor*}] = backdoor
 
-  var escaped: File^{backdoor*} = null
-  withFile("hello.txt"): f =>
-    boom.use(f): (f1: File^{backdoor*}) => // error
-      escaped = f1
+    var escaped: File^{backdoor*} = null
+    withFile("hello.txt"): f =>
+        boom.use(f): (f1: File^{backdoor*}) => // error
+            escaped = f1
 
diff --git a/tests/pos-custom-args/captures/boxed1.scala b/tests/pos-custom-args/captures/boxed1.scala
index 8c6b63ef0134..e2ff69c305d2 100644
--- a/tests/pos-custom-args/captures/boxed1.scala
+++ b/tests/pos-custom-args/captures/boxed1.scala
@@ -1,6 +1,6 @@
 class Box[T](val x: T)
 
-@annotation.capability class Cap
+class Cap extends caps.Capability
 
 def foo(x: => Int): Unit = ()
 
diff --git a/tests/pos-custom-args/captures/capt-capability.scala b/tests/pos-custom-args/captures/capt-capability.scala
index 830d341c7bca..64892218ee41 100644
--- a/tests/pos-custom-args/captures/capt-capability.scala
+++ b/tests/pos-custom-args/captures/capt-capability.scala
@@ -1,7 +1,7 @@
 import annotation.capability
+import caps.Capability
 
-@capability class Cap
-def f1(c: Cap): () ->{c} c.type = () => c // ok
+def f1(c: Capability): () ->{c} c.type = () => c // ok
 
 def f2: Int =
   val g: Boolean => Int = ???
@@ -15,15 +15,15 @@ def f3: Int =
   x
 
 def foo() =
-  val x: Cap = ???
-  val y: Cap = x
-  val x2: () ->{x} Cap = ???
-  val y2: () ->{x} Cap = x2
+  val x: Capability = ???
+  val y: Capability = x
+  val x2: () ->{x} Capability = ???
+  val y2: () ->{x} Capability = x2
 
-  val z1: () => Cap = f1(x)
+  val z1: () => Capability = f1(x)
   def h[X](a: X)(b: X) = a
 
   val z2 =
-    if x == null then () => x else () => Cap()
+    if x == null then () => x else () => new Capability() {}
   val _ = x
 
diff --git a/tests/pos-custom-args/captures/caseclass.scala b/tests/pos-custom-args/captures/caseclass.scala
index ffbf878dca49..0aa656eaf9cb 100644
--- a/tests/pos-custom-args/captures/caseclass.scala
+++ b/tests/pos-custom-args/captures/caseclass.scala
@@ -1,4 +1,4 @@
-@annotation.capability class C
+class C extends caps.Capability
 object test1:
   case class Ref(x: String^)
 
diff --git a/tests/pos-custom-args/captures/cc-this.scala b/tests/pos-custom-args/captures/cc-this.scala
index 12c62e99d186..d9705df76c55 100644
--- a/tests/pos-custom-args/captures/cc-this.scala
+++ b/tests/pos-custom-args/captures/cc-this.scala
@@ -1,4 +1,4 @@
-@annotation.capability class Cap
+class Cap extends caps.Capability
 
 def eff(using Cap): Unit = ()
 
diff --git a/tests/pos-custom-args/captures/eta-expansions.scala b/tests/pos-custom-args/captures/eta-expansions.scala
index 1aac7ded1b50..b4e38cdf0856 100644
--- a/tests/pos-custom-args/captures/eta-expansions.scala
+++ b/tests/pos-custom-args/captures/eta-expansions.scala
@@ -1,4 +1,4 @@
-@annotation.capability class Cap
+class Cap extends caps.Capability
 
 def test(d: Cap) =
   def map2(xs: List[Int])(f: Int => Int): List[Int] = xs.map(f)
diff --git a/tests/pos-custom-args/captures/filevar-tracked.scala b/tests/pos-custom-args/captures/filevar-tracked.scala
new file mode 100644
index 000000000000..6fb7000ad4c2
--- /dev/null
+++ b/tests/pos-custom-args/captures/filevar-tracked.scala
@@ -0,0 +1,38 @@
+import language.experimental.captureChecking
+import language.experimental.modularity
+import annotation.capability
+import compiletime.uninitialized
+
+object test1:
+  class File:
+    def write(x: String): Unit = ???
+
+  class Service(f: File^):
+    def log = f.write("log")
+
+  def withFile[T](op: (f: File^) => T): T =
+    op(new File)
+
+  def test =
+    withFile: f =>
+      val o = Service(f)
+      o.log
+
+object test2:
+  class IO extends caps.Capability
+
+  class File:
+    def write(x: String): Unit = ???
+
+  class Service(tracked val io: IO):
+    var file: File^{io} = uninitialized
+    def log = file.write("log")
+
+  def withFile[T](io2: IO)(op: (f: File^{io2}) => T): T =
+    op(new File)
+
+  def test(io3: IO) =
+    withFile(io3): f =>
+      val o = Service(io3)
+      o.file = f
+      o.log
diff --git a/tests/pos-custom-args/captures/filevar.scala b/tests/pos-custom-args/captures/filevar.scala
index a6cc7ca9ff47..c5571ca88849 100644
--- a/tests/pos-custom-args/captures/filevar.scala
+++ b/tests/pos-custom-args/captures/filevar.scala
@@ -1,4 +1,5 @@
 import language.experimental.captureChecking
+import language.experimental.modularity
 import annotation.capability
 import compiletime.uninitialized
 
@@ -18,20 +19,20 @@ object test1:
       o.log
 
 object test2:
-  @capability class IO
+  class IO
 
   class File:
     def write(x: String): Unit = ???
 
-  class Service(io: IO):
+  class Service(io: IO^):
     var file: File^{io} = uninitialized
     def log = file.write("log")
 
-  def withFile[T](io: IO)(op: (f: File^{io}) => T): T =
+  def withFile[T](io2: IO^)(op: (f: File^{io2}) => T): T =
     op(new File)
 
-  def test(io: IO) =
-    withFile(io): f =>
-      val o = Service(io)
+  def test(io3: IO^) =
+    withFile(io3): f =>
+      val o = Service(io3)
       o.file = f
       o.log
diff --git a/tests/pos-custom-args/captures/i16116.scala b/tests/pos-custom-args/captures/i16116.scala
index 0311e744f146..979bfdbe4328 100644
--- a/tests/pos-custom-args/captures/i16116.scala
+++ b/tests/pos-custom-args/captures/i16116.scala
@@ -15,8 +15,7 @@ object CpsMonad {
 @experimental
 object Test {
 
-  @capability
-  class CpsTransform[F[_]] {
+  class CpsTransform[F[_]] extends caps.Capability {
      def await[T](ft: F[T]): T^{ this } = ???
   }
 
diff --git a/tests/pos-custom-args/captures/i16226.scala b/tests/pos-custom-args/captures/i16226.scala
index 4cd7f0ceea81..071eefbd3420 100644
--- a/tests/pos-custom-args/captures/i16226.scala
+++ b/tests/pos-custom-args/captures/i16226.scala
@@ -1,4 +1,4 @@
-@annotation.capability class Cap
+class Cap extends caps.Capability
 
 class LazyRef[T](val elem: () => T):
   val get: () ->{elem} T = elem
diff --git a/tests/pos-custom-args/captures/i19751.scala b/tests/pos-custom-args/captures/i19751.scala
index b6023cc0ff87..30bd8677f024 100644
--- a/tests/pos-custom-args/captures/i19751.scala
+++ b/tests/pos-custom-args/captures/i19751.scala
@@ -3,7 +3,7 @@ import annotation.capability
 import caps.cap
 
 trait Ptr[A]
-@capability trait Scope:
+trait Scope extends caps.Capability:
   def allocate(size: Int): Ptr[Unit]^{this}
 
 
diff --git a/tests/pos-custom-args/captures/lazyref.scala b/tests/pos-custom-args/captures/lazyref.scala
index 3dae51b491b4..2e3a0030bcdc 100644
--- a/tests/pos-custom-args/captures/lazyref.scala
+++ b/tests/pos-custom-args/captures/lazyref.scala
@@ -1,4 +1,4 @@
-@annotation.capability class Cap
+class Cap extends caps.Capability
 
 class LazyRef[T](val elem: () => T):
   val get: () ->{elem} T = elem
diff --git a/tests/pos-custom-args/captures/lists.scala b/tests/pos-custom-args/captures/lists.scala
index 99505f0bb7a2..5f4991c6be54 100644
--- a/tests/pos-custom-args/captures/lists.scala
+++ b/tests/pos-custom-args/captures/lists.scala
@@ -18,7 +18,7 @@ object NIL extends LIST[Nothing]:
 def map[A, B](f: A => B)(xs: LIST[A]): LIST[B] =
   xs.map(f)
 
-@annotation.capability class Cap
+class Cap extends caps.Capability
 
 def test(c: Cap, d: Cap, e: Cap) =
   def f(x: Cap): Unit = if c == x then ()
@@ -30,7 +30,7 @@ def test(c: Cap, d: Cap, e: Cap) =
     CONS(z, ys)
   val zsc: LIST[Cap ->{d, y} Unit] = zs
   val z1 = zs.head
-  val z1c: Cap^ ->{y, d} Unit = z1
+  val z1c: Cap ->{y, d} Unit = z1
   val ys1 = zs.tail
   val y1 = ys1.head
 
diff --git a/tests/pos-custom-args/captures/logger-tracked.scala b/tests/pos-custom-args/captures/logger-tracked.scala
new file mode 100644
index 000000000000..1949e25b00d9
--- /dev/null
+++ b/tests/pos-custom-args/captures/logger-tracked.scala
@@ -0,0 +1,68 @@
+import annotation.capability
+import language.experimental.saferExceptions
+import language.experimental.modularity
+
+class FileSystem extends caps.Capability
+
+class Logger(using tracked val fs: FileSystem):
+  def log(s: String): Unit = ???
+
+def test(using fs: FileSystem) =
+  val l: Logger^{fs} = Logger(using fs)
+  l.log("hello world!")
+  val xs: LazyList[Int]^{l} =
+    LazyList.from(1)
+      .map { i =>
+        l.log(s"computing elem # $i")
+        i * i
+      }
+
+trait LazyList[+A]:
+  def isEmpty: Boolean
+  def head: A
+  def tail: LazyList[A]^{this}
+
+object LazyNil extends LazyList[Nothing]:
+  def isEmpty: Boolean = true
+  def head = ???
+  def tail = ???
+
+final class LazyCons[+T](val x: T, val xs: () => LazyList[T]^) extends LazyList[T]:
+  def isEmpty = false
+  def head = x
+  def tail: LazyList[T]^{this} = xs()
+end LazyCons
+
+extension [A](x: A)
+  def #::(xs1: => LazyList[A]^): LazyList[A]^{xs1} =
+    LazyCons(x, () => xs1)
+
+extension [A](xs: LazyList[A]^)
+  def map[B](f: A => B): LazyList[B]^{xs, f} =
+    if xs.isEmpty then LazyNil
+    else f(xs.head) #:: xs.tail.map(f)
+
+object LazyList:
+  def from(start: Int): LazyList[Int] =
+    start #:: from(start + 1)
+
+class Pair[+A, +B](x: A, y: B):
+  def fst: A = x
+  def snd: B = y
+
+def test2(ct: CanThrow[Exception], fs: FileSystem) =
+  def x: Int ->{ct} String = ???
+  def y: Logger^{fs} = ???
+  def p = Pair[Int ->{ct} String, Logger^{fs}](x, y)
+  def p3 = Pair(x, y)
+  def f = () => p.fst
+
+
+/*
+  val l1: Int => String = ???
+  val l2: Object^{c} = ???
+  val pd = () => Pair(l1, l2)
+  val p2: Pair[Int => String, Object]^{c} = pd()
+  val hd = () => p2.fst
+
+*/
\ No newline at end of file
diff --git a/tests/pos-custom-args/captures/logger.scala b/tests/pos-custom-args/captures/logger.scala
index d95eeaae74cf..75ea3ac3fbc0 100644
--- a/tests/pos-custom-args/captures/logger.scala
+++ b/tests/pos-custom-args/captures/logger.scala
@@ -1,12 +1,13 @@
 import annotation.capability
 import language.experimental.saferExceptions
+import language.experimental.modularity
 
-@capability class FileSystem
+class FileSystem // does not work with extends caps.Capability
 
-class Logger(using fs: FileSystem):
+class Logger(using fs: FileSystem^):
   def log(s: String): Unit = ???
 
-def test(using fs: FileSystem) =
+def test(using fs: FileSystem^) =
   val l: Logger^{fs} = Logger(using fs)
   l.log("hello world!")
   val xs: LazyList[Int]^{l} =
@@ -49,7 +50,7 @@ class Pair[+A, +B](x: A, y: B):
   def fst: A = x
   def snd: B = y
 
-def test2(ct: CanThrow[Exception], fs: FileSystem) =
+def test2(ct: CanThrow[Exception], fs: FileSystem^) =
   def x: Int ->{ct} String = ???
   def y: Logger^{fs} = ???
   def p = Pair[Int ->{ct} String, Logger^{fs}](x, y)
diff --git a/tests/pos-custom-args/captures/nested-classes-tracked.scala b/tests/pos-custom-args/captures/nested-classes-tracked.scala
new file mode 100644
index 000000000000..1c81441f321b
--- /dev/null
+++ b/tests/pos-custom-args/captures/nested-classes-tracked.scala
@@ -0,0 +1,22 @@
+import language.experimental.captureChecking
+import language.experimental.modularity
+import annotation.{capability, constructorOnly}
+
+class IO extends caps.Capability
+class Blah
+class Pkg(using tracked val io: IO):
+  class Foo:
+    def m(foo: Blah^{io}) = ???
+class Pkg2(using tracked val io: IO):
+  class Foo:
+    def m(foo: Blah^{io}): Any = io; ???
+
+def main(using io: IO) =
+  val pkg = Pkg()
+  val f = pkg.Foo()
+  f.m(???)
+  val pkg2 = Pkg2()
+  val f2 = pkg2.Foo()
+  f2.m(???)
+
+
diff --git a/tests/pos-custom-args/captures/nested-classes.scala b/tests/pos-custom-args/captures/nested-classes.scala
index b16fc4365183..4a0da34faf5c 100644
--- a/tests/pos-custom-args/captures/nested-classes.scala
+++ b/tests/pos-custom-args/captures/nested-classes.scala
@@ -1,16 +1,17 @@
 import language.experimental.captureChecking
+import language.experimental.modularity
 import annotation.{capability, constructorOnly}
 
-@capability class IO
+class IO // does not work with extends caps.Capability
 class Blah
-class Pkg(using @constructorOnly io: IO):
+class Pkg(using io: IO^):
   class Foo:
     def m(foo: Blah^{io}) = ???
-class Pkg2(using io: IO):
+class Pkg2(using io: IO^):
   class Foo:
     def m(foo: Blah^{io}): Any = io; ???
 
-def main(using io: IO) =
+def main(using io: IO^) =
   val pkg = Pkg()
   val f = pkg.Foo()
   f.m(???)
diff --git a/tests/pos-custom-args/captures/null-logger.scala b/tests/pos-custom-args/captures/null-logger.scala
index 0b32d045778c..958002ad0358 100644
--- a/tests/pos-custom-args/captures/null-logger.scala
+++ b/tests/pos-custom-args/captures/null-logger.scala
@@ -1,7 +1,7 @@
 import annotation.capability
 import annotation.constructorOnly
 
-@capability class FileSystem
+class FileSystem extends caps.Capability
 
 class NullLogger(using @constructorOnly fs: FileSystem)
 
diff --git a/tests/pos-custom-args/captures/pairs.scala b/tests/pos-custom-args/captures/pairs.scala
index e15a76970c29..da7f30185ad3 100644
--- a/tests/pos-custom-args/captures/pairs.scala
+++ b/tests/pos-custom-args/captures/pairs.scala
@@ -1,6 +1,6 @@
 //class CC
 //type Cap = CC^
-@annotation.capability class Cap
+class Cap extends caps.Capability
 
 object Generic:
 
@@ -13,6 +13,6 @@ object Generic:
     def g(x: Cap): Unit = if d == x then ()
     val p = Pair(f, g)
     val x1 = p.fst
-    val x1c: Cap^ ->{c} Unit = x1
+    val x1c: Cap ->{c} Unit = x1
     val y1 = p.snd
-    val y1c: Cap^ ->{d} Unit = y1
+    val y1c: Cap ->{d} Unit = y1
diff --git a/tests/pos-custom-args/captures/reaches.scala b/tests/pos-custom-args/captures/reaches.scala
index f17c25712c39..f82c792c8445 100644
--- a/tests/pos-custom-args/captures/reaches.scala
+++ b/tests/pos-custom-args/captures/reaches.scala
@@ -48,7 +48,7 @@ def compose2[A, B, C](f: A => B, g: B => C): A => C =
 def mapCompose[A](ps: List[(A => A, A => A)]): List[A ->{ps*} A] =
   ps.map((x, y) => compose1(x, y)) // Does not work if map takes an impure function, see reaches in neg
 
-@annotation.capability class IO
+class IO extends caps.Capability
 
 def test(io: IO) =
   val a: () ->{io} Unit = () => ()
diff --git a/tests/pos-custom-args/captures/try3.scala b/tests/pos-custom-args/captures/try3.scala
index b44ea57ccae4..305069d3ae9f 100644
--- a/tests/pos-custom-args/captures/try3.scala
+++ b/tests/pos-custom-args/captures/try3.scala
@@ -2,7 +2,7 @@ import language.experimental.erasedDefinitions
 import annotation.capability
 import java.io.IOException
 
-@annotation.capability class CanThrow[-E]
+class CanThrow[-E] extends caps.Capability
 
 def handle[E <: Exception, T](op: CanThrow[E] ?=> T)(handler: E => T): T =
   val x: CanThrow[E] = ???
diff --git a/tests/pos-custom-args/captures/vars.scala b/tests/pos-custom-args/captures/vars.scala
index a335be96fed1..5c9598fab508 100644
--- a/tests/pos-custom-args/captures/vars.scala
+++ b/tests/pos-custom-args/captures/vars.scala
@@ -1,4 +1,4 @@
-@annotation.capability class Cap
+class Cap extends caps.Capability
 
 def test(cap1: Cap, cap2: Cap) =
   def f(x: String): String = if cap1 == cap1 then "" else "a"
diff --git a/tests/pos/dotty-experimental.scala b/tests/pos/dotty-experimental.scala
index ee9a84a1b497..813c9b5920c1 100644
--- a/tests/pos/dotty-experimental.scala
+++ b/tests/pos/dotty-experimental.scala
@@ -3,6 +3,6 @@
 import language.experimental.captureChecking
 object test {
 
-  val x: caps.Cap = caps.cap
+  val x: caps.Capability = caps.cap
 
 }
diff --git a/tests/pos/i20237.scala b/tests/pos/i20237.scala
index da3e902b78b4..0a5eb6d9a332 100644
--- a/tests/pos/i20237.scala
+++ b/tests/pos/i20237.scala
@@ -1,7 +1,7 @@
 import language.experimental.captureChecking
 import scala.annotation.capability
 
-@capability class Cap:
+class Cap extends caps.Capability:
   def use[T](body: Cap ?=> T) = body(using this)
 
 class Box[T](body: Cap ?=> T):
diff --git a/tests/pos/into-bigint.scala b/tests/pos/into-bigint.scala
index d7ecee40b3ba..409b5e79da2c 100644
--- a/tests/pos/into-bigint.scala
+++ b/tests/pos/into-bigint.scala
@@ -14,8 +14,8 @@ object BigInt:
 @main def Test =
   val x = BigInt(2)
   val y = 3
-  val a1 = x + y
-  val a2 = y * x
+  val a1 = x + y // uses conversion on `y`
+  val a2 = y * x // uses conversion on `y`
   val a3 = x * x
   val a4 = y + y
 

From 9ed37a93c7ef53d61c9a99d2535bb5468121f033 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Tue, 14 May 2024 18:29:48 +0200
Subject: [PATCH 04/14] Drop convention on classes inheriting from universal
 capturing types

Drop convention that classes inheriting from universal capturing types are capability classes. Capture sets of parents
are instead ignored.

The convention led to algebraic anomalies. For instance if

    class C extends A => B, Serializable

then C <: (A => B) & Serializable, which has an empty capture set. Yet we treat every occurrence of C as
implicitly carrying `cap`.
---
 compiler/src/dotty/tools/dotc/cc/Setup.scala  | 29 +------------------
 .../dotty/tools/dotc/transform/Recheck.scala  |  1 -
 .../captures/extending-impure-function.scala  |  0
 3 files changed, 1 insertion(+), 29 deletions(-)
 rename tests/{neg-custom-args => pos-custom-args}/captures/extending-impure-function.scala (100%)

diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala
index 1a8c65c89a43..bdbc00674563 100644
--- a/compiler/src/dotty/tools/dotc/cc/Setup.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -23,7 +23,6 @@ trait SetupAPI:
   def setupUnit(tree: Tree, recheckDef: DefRecheck)(using Context): Unit
   def isPreCC(sym: Symbol)(using Context): Boolean
   def postCheck()(using Context): Unit
-  def isCapabilityClassRef(tp: Type)(using Context): Boolean
 
 object Setup:
 
@@ -68,29 +67,6 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
     && !sym.owner.is(CaptureChecked)
     && !defn.isFunctionSymbol(sym.owner)
 
-  private val capabilityClassMap = new util.HashMap[Symbol, Boolean]
-
-  /** Check if the class is capability, which means:
-   *  1. the class has a capability annotation,
-   *  2. or at least one of its parent type has universal capability.
-   */
-  def isCapabilityClassRef(tp: Type)(using Context): Boolean = tp.dealiasKeepAnnots match
-    case _: TypeRef | _: AppliedType =>
-      val sym = tp.classSymbol
-      def checkSym: Boolean = sym.info.parents.exists(hasUniversalCapability)
-      sym.isClass && capabilityClassMap.getOrElseUpdate(sym, checkSym)
-    case _ => false
-
-  private def hasUniversalCapability(tp: Type)(using Context): Boolean = tp.dealiasKeepAnnots match
-    case CapturingType(parent, refs) =>
-      refs.isUniversal || hasUniversalCapability(parent)
-    case AnnotatedType(parent, ann) =>
-      if ann.symbol.isRetains then
-        try ann.tree.toCaptureSet.isUniversal || hasUniversalCapability(parent)
-        catch case ex: IllegalCaptureRef => false
-      else hasUniversalCapability(parent)
-    case tp => isCapabilityClassRef(tp)
-
   private def fluidify(using Context) = new TypeMap with IdempotentCaptRefMap:
     def apply(t: Type): Type = t match
       case t: MethodType =>
@@ -317,10 +293,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
           case t: TypeVar =>
             this(t.underlying)
           case t =>
-            // Map references to capability classes C to C^
-            if isCapabilityClassRef(t)
-            then CapturingType(t, defn.expandedUniversalSet, boxed = false)
-            else recur(t)
+            recur(t)
     end expandAliases
 
     val tp1 = expandAliases(tp) // TODO: Do we still need to follow aliases?
diff --git a/compiler/src/dotty/tools/dotc/transform/Recheck.scala b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
index f809fbd176ce..e40c8346ed82 100644
--- a/compiler/src/dotty/tools/dotc/transform/Recheck.scala
+++ b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
@@ -33,7 +33,6 @@ object Recheck:
    *  Scala2ModuleVar cannot be also ParamAccessors.
    */
   val ResetPrivate = Scala2ModuleVar
-  val ResetPrivateParamAccessor = ResetPrivate | ParamAccessor
 
   /** Attachment key for rechecked types of TypeTrees */
   val RecheckedType = Property.Key[Type]
diff --git a/tests/neg-custom-args/captures/extending-impure-function.scala b/tests/pos-custom-args/captures/extending-impure-function.scala
similarity index 100%
rename from tests/neg-custom-args/captures/extending-impure-function.scala
rename to tests/pos-custom-args/captures/extending-impure-function.scala

From d49b314fcaf96bc6a1e67198abdb66eb7ef56910 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Tue, 14 May 2024 20:56:42 +0200
Subject: [PATCH 05/14] Add fewer parameter refinements.

Only enrich classes with capture refinements for a parameter if the deep capture set of the parameter's type is nonempty.
---
 compiler/src/dotty/tools/dotc/cc/Setup.scala | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala
index bdbc00674563..67977b027137 100644
--- a/compiler/src/dotty/tools/dotc/cc/Setup.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -57,7 +57,20 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
   private val toBeUpdated = new mutable.HashSet[Symbol]
 
   private def newFlagsFor(symd: SymDenotation)(using Context): FlagSet =
-    if symd.isAllOf(PrivateParamAccessor) && symd.owner.is(CaptureChecked) && !symd.hasAnnotation(defn.ConstructorOnlyAnnot)
+
+    object containsCovarRetains extends TypeAccumulator[Boolean]:
+      def apply(x: Boolean, tp: Type): Boolean =
+        if x then true
+        else if tp.derivesFromCapability && variance >= 0 then true
+        else tp match
+          case AnnotatedType(_, ann) if ann.symbol.isRetains && variance >= 0 => true
+          case _ => foldOver(x, tp)
+      def apply(tp: Type): Boolean = apply(false, tp)
+
+    if symd.isAllOf(PrivateParamAccessor)
+        && symd.owner.is(CaptureChecked)
+        && !symd.hasAnnotation(defn.ConstructorOnlyAnnot)
+        //&& containsCovarRetains(symd.symbol.originDenotation.info)
     then symd.flags &~ Private | Recheck.ResetPrivate
     else symd.flags
 

From f91b6c13fb9ac5e68fe3e80a88b8f127d9354126 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Wed, 15 May 2024 15:42:19 +0200
Subject: [PATCH 06/14] Drop ResetPrivate flag

---
 compiler/src/dotty/tools/dotc/cc/Setup.scala               | 4 ++--
 .../src/dotty/tools/dotc/transform/OverridingPairs.scala   | 4 +++-
 compiler/src/dotty/tools/dotc/transform/Recheck.scala      | 7 -------
 3 files changed, 5 insertions(+), 10 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala
index 67977b027137..0175d40c186c 100644
--- a/compiler/src/dotty/tools/dotc/cc/Setup.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -70,8 +70,8 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
     if symd.isAllOf(PrivateParamAccessor)
         && symd.owner.is(CaptureChecked)
         && !symd.hasAnnotation(defn.ConstructorOnlyAnnot)
-        //&& containsCovarRetains(symd.symbol.originDenotation.info)
-    then symd.flags &~ Private | Recheck.ResetPrivate
+        && containsCovarRetains(symd.symbol.originDenotation.info)
+    then symd.flags &~ Private
     else symd.flags
 
   def isPreCC(sym: Symbol)(using Context): Boolean =
diff --git a/compiler/src/dotty/tools/dotc/transform/OverridingPairs.scala b/compiler/src/dotty/tools/dotc/transform/OverridingPairs.scala
index 4020291dded0..6529eed77fa0 100644
--- a/compiler/src/dotty/tools/dotc/transform/OverridingPairs.scala
+++ b/compiler/src/dotty/tools/dotc/transform/OverridingPairs.scala
@@ -34,7 +34,9 @@ object OverridingPairs:
      */
     protected def exclude(sym: Symbol): Boolean =
       !sym.memberCanMatchInheritedSymbols
-      || isCaptureChecking && sym.is(Recheck.ResetPrivate)
+      || isCaptureChecking && atPhase(ctx.phase.prev)(sym.is(Private))
+        // for capture checking we drop the private flag of certain parameter accessors
+        // but these still need no overriding checks
 
     /** The parents of base that are checked when deciding whether an overriding
      *  pair has already been treated in a parent class.
diff --git a/compiler/src/dotty/tools/dotc/transform/Recheck.scala b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
index e40c8346ed82..79dfe3393578 100644
--- a/compiler/src/dotty/tools/dotc/transform/Recheck.scala
+++ b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
@@ -27,13 +27,6 @@ import annotation.tailrec
 object Recheck:
   import tpd.*
 
-  /** A flag used to indicate that a ParamAccessor has been temporarily made not-private
-   *  Only used at the start of the Recheck phase, reset at its end.
-   *  The flag repurposes the Scala2ModuleVar flag. No confusion is possible since
-   *  Scala2ModuleVar cannot be also ParamAccessors.
-   */
-  val ResetPrivate = Scala2ModuleVar
-
   /** Attachment key for rechecked types of TypeTrees */
   val RecheckedType = Property.Key[Type]
 

From 5cf37578ad957721321359e9416912dd59a173b9 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Fri, 17 May 2024 13:31:21 +0200
Subject: [PATCH 07/14] Turn nested environment capture sets into constants at
 the end of box adaptation

This change lets more ref trees with underlying function types keep their singleton
types.
---
 .../src/dotty/tools/dotc/cc/CaptureSet.scala  |  2 +-
 .../dotty/tools/dotc/cc/CheckCaptures.scala   |  4 +--
 .../dotty/tools/dotc/core/TypeComparer.scala  | 28 ++++++++++++++-----
 tests/neg-custom-args/captures/byname.check   |  6 ++--
 tests/neg-custom-args/captures/eta.check      |  2 +-
 tests/neg-custom-args/captures/i15772.check   |  2 +-
 .../neg-custom-args/captures/outer-var.check  |  4 +--
 7 files changed, 31 insertions(+), 17 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index 06ba36bd5e24..1a81e2bc1014 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -1080,7 +1080,7 @@ object CaptureSet:
         case _ =>
           empty
     recur(tp)
-      .showing(i"capture set of $tp = $result", captDebug)
+      //.showing(i"capture set of $tp = $result", captDebug)
 
   private def deepCaptureSet(tp: Type)(using Context): CaptureSet =
     val collect = new TypeAccumulator[CaptureSet]:
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index cd0f21129ac9..30d05a744e31 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -1006,7 +1006,7 @@ class CheckCaptures extends Recheck, SymTransformer:
             if (ares1 eq ares) && (aargs1 eq aargs) then actual
             else reconstruct(aargs1, ares1)
 
-          (resTp, curEnv.captured)
+          (resTp, CaptureSet(curEnv.captured.elems))
       end adaptFun
 
       /** Adapt type function type `actual` to the expected type.
@@ -1028,7 +1028,7 @@ class CheckCaptures extends Recheck, SymTransformer:
             if ares1 eq ares then actual
             else reconstruct(ares1)
 
-          (resTp, curEnv.captured)
+          (resTp, CaptureSet(curEnv.captured.elems))
       end adaptTypeFun
 
       def adaptInfo(actual: Type, expected: Type, covariant: Boolean): String =
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index e0ab30907314..c4f34753bb7f 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -842,13 +842,27 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
           val refs1 = tp1.captureSet
           try
             if refs1.isAlwaysEmpty then recur(tp1, parent2)
-            else subCaptures(refs1, refs2, frozenConstraint).isOK
-              && sameBoxed(tp1, tp2, refs1)
-              && (recur(tp1.widen.stripCapturing, parent2)
-                 || tp1.isInstanceOf[SingletonType] && recur(tp1, parent2)
-                    // this alternative is needed in case the right hand side is a
-                    // capturing type that contains the lhs as an alternative of a union type.
-                 )
+            else
+              // The singletonOK branch is because we sometimes have a larger capture set in a singleton
+              // than in its underlying type. An example is `f: () -> () ->{x} T`, which might be
+              // the type of a closure. In that case the capture set of `f.type` is `{x}` but the
+              // capture set of the underlying type is `{}`. So without the `singletonOK` test, a singleton
+              // might not be a subtype of its underlying type. Examples where this arises is
+              // capt-capibility.scala and function-combinators.scala
+              val singletonOK = tp1 match
+                case tp1: SingletonType
+                if subCaptures(tp1.underlying.captureSet, refs2, frozen = true).isOK =>
+                  recur(tp1.widen, tp2)
+                case _ =>
+                  false
+              singletonOK
+              || subCaptures(refs1, refs2, frozenConstraint).isOK
+                  && sameBoxed(tp1, tp2, refs1)
+                  && (recur(tp1.widen.stripCapturing, parent2)
+                     || tp1.isInstanceOf[SingletonType] && recur(tp1, parent2)
+                        // this alternative is needed in case the right hand side is a
+                        // capturing type that contains the lhs as an alternative of a union type.
+                    )
           catch case ex: AssertionError =>
             println(i"assertion failed while compare captured $tp1 <:< $tp2")
             throw ex
diff --git a/tests/neg-custom-args/captures/byname.check b/tests/neg-custom-args/captures/byname.check
index 2b48428e97bc..b9e5c81b721d 100644
--- a/tests/neg-custom-args/captures/byname.check
+++ b/tests/neg-custom-args/captures/byname.check
@@ -6,13 +6,13 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/byname.scala:4:2 -----------------------------------------
  4 |  def f() = if cap1 == cap1 then g else g // error
    |  ^
-   |  Found:    (x$0: Int) ->{cap2} Int
-   |  Required: (x$0: Int) -> Int
+   |  Found:    ((x$0: Int) ->{cap2} Int)^{}
+   |  Required: Int -> Int
    |
    |  Note that the expected type Int ->{} Int
    |  is the previously inferred result type of method test
    |  which is also the type seen in separately compiled sources.
-   |  The new inferred type (x$0: Int) ->{cap2} Int
+   |  The new inferred type ((x$0: Int) ->{cap2} Int)^{}
    |  must conform to this type.
  5 |  def g(x: Int) = if cap2 == cap2 then 1 else x
  6 |  def g2(x: Int) = if cap1 == cap1 then 1 else x
diff --git a/tests/neg-custom-args/captures/eta.check b/tests/neg-custom-args/captures/eta.check
index 91dfdf06d3cd..9850e54a7fdf 100644
--- a/tests/neg-custom-args/captures/eta.check
+++ b/tests/neg-custom-args/captures/eta.check
@@ -1,7 +1,7 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/eta.scala:4:9 --------------------------------------------
 4 |         g  // error
   |         ^
-  |         Found:    () ->? A
+  |         Found:    (g : () -> A)
   |         Required: () -> Proc^{f}
   |
   | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/i15772.check b/tests/neg-custom-args/captures/i15772.check
index cce58da1b93b..0f8f0bf6eac5 100644
--- a/tests/neg-custom-args/captures/i15772.check
+++ b/tests/neg-custom-args/captures/i15772.check
@@ -35,7 +35,7 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15772.scala:44:2 ----------------------------------------
 44 |  x: (() -> Unit) // error
    |  ^
-   |  Found:    () ->{x} Unit
+   |  Found:    (x : () ->{filesList, sayHello} Unit)
    |  Required: () -> Unit
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/outer-var.check b/tests/neg-custom-args/captures/outer-var.check
index c250280961d9..b9f1f57be769 100644
--- a/tests/neg-custom-args/captures/outer-var.check
+++ b/tests/neg-custom-args/captures/outer-var.check
@@ -1,7 +1,7 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/outer-var.scala:11:8 -------------------------------------
 11 |    x = q           // error
    |        ^
-   |        Found:    () ->{q} Unit
+   |        Found:    (q : Proc)
    |        Required: () ->{p, q²} Unit
    |
    |        where:    q  is a parameter in method inner
@@ -28,7 +28,7 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/outer-var.scala:14:8 -------------------------------------
 14 |    y = q           // error
    |        ^
-   |        Found:    () ->{q} Unit
+   |        Found:    (q : Proc)
    |        Required: () ->{p} Unit
    |
    |        Note that reference (q : Proc), defined in method inner

From 1a5469ce3e8f169193d78d2592e56354e01b9f1a Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sun, 19 May 2024 10:36:57 +0200
Subject: [PATCH 08/14] Two fixes to make tests pass as before

 - Avoid creating capture sets of untrackable references
 - Refine disallowRootCapability to consider only explicit captures
---
 .../src/dotty/tools/dotc/cc/CaptureSet.scala  |  4 ++-
 .../dotty/tools/dotc/cc/CheckCaptures.scala   |  6 ++--
 tests/neg-custom-args/captures/capt1.check    |  2 +-
 tests/neg-custom-args/captures/i16725.scala   |  2 +-
 .../captures/filevar-expanded.scala           | 36 +++++++++++++++++++
 tests/pos-custom-args/captures/filevar.scala  | 10 +++---
 tests/pos-custom-args/captures/logger.scala   |  8 ++---
 .../captures/nested-classes.scala             | 12 +++----
 8 files changed, 59 insertions(+), 21 deletions(-)
 create mode 100644 tests/pos-custom-args/captures/filevar-expanded.scala

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index 1a81e2bc1014..5422706f7c40 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -1037,7 +1037,9 @@ object CaptureSet:
 
   /** The capture set of the type underlying CaptureRef */
   def ofInfo(ref: CaptureRef)(using Context): CaptureSet = ref match
-    case ref: (TermRef | TermParamRef) if ref.isMaxCapability => ref.singletonCaptureSet
+    case ref: (TermRef | TermParamRef) if ref.isMaxCapability =>
+      if ref.isTrackableRef then ref.singletonCaptureSet
+      else CaptureSet.universal
     case ReachCapability(ref1) => deepCaptureSet(ref1.widen)
       .showing(i"Deep capture set of $ref: ${ref1.widen} = $result", capt)
     case _ => ofType(ref.underlying, followResult = true)
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 30d05a744e31..bde97a6d0387 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -157,15 +157,17 @@ object CheckCaptures:
                 case _ =>
           case AnnotatedType(_, ann) if ann.symbol == defn.UncheckedCapturesAnnot =>
             ()
-          case t =>
+          case CapturingType(parent, refs) =>
             if variance >= 0 then
-              t.captureSet.disallowRootCapability: () =>
+              refs.disallowRootCapability: () =>
                 def part = if t eq tp then "" else i"the part $t of "
                 report.error(
                   em"""$what cannot $have $tp since
                       |${part}that type captures the root capability `cap`.
                       |$addendum""",
                   pos)
+            traverse(parent)
+          case t =>
             traverseChildren(t)
     check.traverse(tp)
   end disallowRootCapabilitiesIn
diff --git a/tests/neg-custom-args/captures/capt1.check b/tests/neg-custom-args/captures/capt1.check
index 74b9db728983..0e99d1876d3c 100644
--- a/tests/neg-custom-args/captures/capt1.check
+++ b/tests/neg-custom-args/captures/capt1.check
@@ -49,6 +49,6 @@
 34 |  val z3 = h[(() -> Cap) @retains(x)](() => x)(() => C())  // error
    |           ^^^^^^^^^^^^^^^^^^^^^^^^^^
    |           Sealed type variable X cannot be instantiated to box () ->{x} Cap since
-   |           the part C^ of that type captures the root capability `cap`.
+   |           the part Cap of that type captures the root capability `cap`.
    |           This is often caused by a local capability in an argument of method h
    |           leaking as part of its result.
diff --git a/tests/neg-custom-args/captures/i16725.scala b/tests/neg-custom-args/captures/i16725.scala
index 853b3e96ca5c..733c2c562bbc 100644
--- a/tests/neg-custom-args/captures/i16725.scala
+++ b/tests/neg-custom-args/captures/i16725.scala
@@ -10,5 +10,5 @@ def useWrappedIO(wrapper: Wrapper[IO]): () -> Unit =
     wrapper: io =>
       io.brewCoffee()
 def main(): Unit =
-  val escaped = usingIO(io => useWrappedIO(mk(io))) // error // error
+  val escaped = usingIO(io => useWrappedIO(mk(io))) // error
   escaped()  // boom
diff --git a/tests/pos-custom-args/captures/filevar-expanded.scala b/tests/pos-custom-args/captures/filevar-expanded.scala
new file mode 100644
index 000000000000..13051994f346
--- /dev/null
+++ b/tests/pos-custom-args/captures/filevar-expanded.scala
@@ -0,0 +1,36 @@
+import language.experimental.captureChecking
+import compiletime.uninitialized
+
+object test1:
+  class File:
+    def write(x: String): Unit = ???
+
+  class Service(f: File^):
+    def log = f.write("log")
+
+  def withFile[T](op: (f: File^) => T): T =
+    op(new File)
+
+  def test =
+    withFile: f =>
+      val o = Service(f)
+      o.log
+
+object test2:
+  class IO
+
+  class File:
+    def write(x: String): Unit = ???
+
+  class Service(io: IO^):
+    var file: File^{io} = uninitialized
+    def log = file.write("log")
+
+  def withFile[T](io2: IO^)(op: (f: File^{io2}) => T): T =
+    op(new File)
+
+  def test(io3: IO^) =
+    withFile(io3): f =>
+      val o = Service(io3)
+      o.file = f
+      o.log
diff --git a/tests/pos-custom-args/captures/filevar.scala b/tests/pos-custom-args/captures/filevar.scala
index c5571ca88849..9ab34fe617b5 100644
--- a/tests/pos-custom-args/captures/filevar.scala
+++ b/tests/pos-custom-args/captures/filevar.scala
@@ -1,6 +1,4 @@
 import language.experimental.captureChecking
-import language.experimental.modularity
-import annotation.capability
 import compiletime.uninitialized
 
 object test1:
@@ -19,19 +17,19 @@ object test1:
       o.log
 
 object test2:
-  class IO
+  class IO extends caps.Capability
 
   class File:
     def write(x: String): Unit = ???
 
-  class Service(io: IO^):
+  class Service(io: IO):
     var file: File^{io} = uninitialized
     def log = file.write("log")
 
-  def withFile[T](io2: IO^)(op: (f: File^{io2}) => T): T =
+  def withFile[T](io2: IO)(op: (f: File^{io2}) => T): T =
     op(new File)
 
-  def test(io3: IO^) =
+  def test(io3: IO) =
     withFile(io3): f =>
       val o = Service(io3)
       o.file = f
diff --git a/tests/pos-custom-args/captures/logger.scala b/tests/pos-custom-args/captures/logger.scala
index 75ea3ac3fbc0..04aee89a227e 100644
--- a/tests/pos-custom-args/captures/logger.scala
+++ b/tests/pos-custom-args/captures/logger.scala
@@ -2,12 +2,12 @@ import annotation.capability
 import language.experimental.saferExceptions
 import language.experimental.modularity
 
-class FileSystem // does not work with extends caps.Capability
+class FileSystem extends caps.Capability
 
-class Logger(using fs: FileSystem^):
+class Logger(using fs: FileSystem):
   def log(s: String): Unit = ???
 
-def test(using fs: FileSystem^) =
+def test(using fs: FileSystem) =
   val l: Logger^{fs} = Logger(using fs)
   l.log("hello world!")
   val xs: LazyList[Int]^{l} =
@@ -50,7 +50,7 @@ class Pair[+A, +B](x: A, y: B):
   def fst: A = x
   def snd: B = y
 
-def test2(ct: CanThrow[Exception], fs: FileSystem^) =
+def test2(ct: CanThrow[Exception], fs: FileSystem) =
   def x: Int ->{ct} String = ???
   def y: Logger^{fs} = ???
   def p = Pair[Int ->{ct} String, Logger^{fs}](x, y)
diff --git a/tests/pos-custom-args/captures/nested-classes.scala b/tests/pos-custom-args/captures/nested-classes.scala
index 4a0da34faf5c..4a76a88c03ff 100644
--- a/tests/pos-custom-args/captures/nested-classes.scala
+++ b/tests/pos-custom-args/captures/nested-classes.scala
@@ -2,21 +2,21 @@ import language.experimental.captureChecking
 import language.experimental.modularity
 import annotation.{capability, constructorOnly}
 
-class IO // does not work with extends caps.Capability
+class IO extends caps.Capability
 class Blah
-class Pkg(using io: IO^):
+class Pkg(using io: IO):
   class Foo:
     def m(foo: Blah^{io}) = ???
-class Pkg2(using io: IO^):
+class Pkg2(using io: IO):
   class Foo:
     def m(foo: Blah^{io}): Any = io; ???
 
-def main(using io: IO^) =
+def main(using io: IO) =
   val pkg = Pkg()
   val f = pkg.Foo()
-  f.m(???)
+  val x1 = f.m(???)
   val pkg2 = Pkg2()
   val f2 = pkg2.Foo()
-  f2.m(???)
+  val x2 = f2.m(???)
 
 

From 4a1ca2ee430c0a012b19a5116ac6fcc477e212bf Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sun, 19 May 2024 10:37:22 +0200
Subject: [PATCH 09/14] Add assertions that all references in capture sets are
 trackable

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

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index 5422706f7c40..697b6f707309 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -388,7 +388,7 @@ object CaptureSet:
 
   def apply(elems: CaptureRef*)(using Context): CaptureSet.Const =
     if elems.isEmpty then empty
-    else Const(SimpleIdentitySet(elems.map(_.normalizedRef)*))
+    else Const(SimpleIdentitySet(elems.map(_.normalizedRef.ensuring(_.isTrackableRef))*))
 
   def apply(elems: Refs)(using Context): CaptureSet.Const =
     if elems.isEmpty then empty else Const(elems)
@@ -496,6 +496,7 @@ object CaptureSet:
         CompareResult.LevelError(this, elem)
       else
         //if id == 34 then assert(!elem.isUniversalRootCapability)
+        assert(elem.isTrackableRef, elem)
         elems += elem
         if elem.isRootCapability then
           rootAddedHandler()

From 31266d12e8669eba9cda9dc756507d8a1a3c2871 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sun, 26 May 2024 16:21:48 +0200
Subject: [PATCH 10/14] Make capture sets of expressions deriving Capability
 explicit

When an expression has a type that derives from caps.Capability, add an
explicit capture set.

Also: Address other review comments
---
 .../src/dotty/tools/dotc/cc/CaptureOps.scala  |  4 +--
 .../src/dotty/tools/dotc/cc/CaptureSet.scala  |  6 +++-
 .../dotty/tools/dotc/cc/CheckCaptures.scala   | 29 +++++++++++++++----
 library/src/scala/caps.scala                  |  2 +-
 .../captures/effect-swaps-explicit.check      | 22 +++++++-------
 .../captures/effect-swaps-explicit.scala      |  2 --
 .../captures/effect-swaps.check               | 18 ++++++------
 .../captures/effect-swaps.scala               |  2 --
 .../captures/extending-cap-classes.check      | 21 ++++++++++++++
 .../captures/extending-cap-classes.scala      | 14 +++++++++
 .../captures/usingLogFile.check               | 12 ++++----
 .../captures/usingLogFile.scala               |  1 -
 .../captures/capt-capability.scala            |  1 -
 .../captures/filevar-tracked.scala            |  1 -
 tests/pos-custom-args/captures/i19751.scala   |  1 -
 .../captures/logger-tracked.scala             |  1 -
 tests/pos-custom-args/captures/logger.scala   |  1 -
 .../captures/null-logger.scala                |  1 -
 tests/pos-custom-args/captures/try3.scala     |  1 -
 .../dotc/core/Definitions.scala               |  1 -
 tests/pos/i20237.scala                        |  1 -
 21 files changed, 92 insertions(+), 50 deletions(-)
 create mode 100644 tests/neg-custom-args/captures/extending-cap-classes.check
 create mode 100644 tests/neg-custom-args/captures/extending-cap-classes.scala

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
index 9b899030bc02..8276a0987003 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
@@ -203,8 +203,8 @@ extension (tp: Type)
     case _ =>
       false
 
-  /** Does type derive from caps.Capability?, which means it references of this
-   *  type are maximal capabilities?
+  /** Tests whether the type derives from `caps.Capability`, which means
+   *  references of this type are maximal capabilities.
    */
   def derivesFromCapability(using Context): Boolean = tp.dealias match
     case tp: (TypeRef | AppliedType) =>
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index 697b6f707309..f78ed1a91bd6 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -154,7 +154,11 @@ sealed abstract class CaptureSet extends Showable:
       (x eq y)
       || x.isRootCapability
       || y.match
-          case y: TermRef => y.prefix eq x
+          case y: TermRef =>
+            (y.prefix eq x)
+            || y.info.match
+                case y1: CaptureRef => x.subsumes(y1)
+                case _ => false
           case MaybeCapability(y1) => x.stripMaybe.subsumes(y1)
           case _ => false
       || x.match
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index bde97a6d0387..5daa56b9cc07 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -1037,7 +1037,7 @@ class CheckCaptures extends Recheck, SymTransformer:
         val arrow = if covariant then "~~>" else "<~~"
         i"adapting $actual $arrow $expected"
 
-      def adapt(actual: Type, expected: Type, covariant: Boolean): Type = trace(adaptInfo(actual, expected, covariant), recheckr, show = true) {
+      def adapt(actual: Type, expected: Type, covariant: Boolean): Type = trace(adaptInfo(actual, expected, covariant), recheckr, show = true):
         if expected.isInstanceOf[WildcardType] then actual
         else
           // Decompose the actual type into the inner shape type, the capture set and the box status
@@ -1117,7 +1117,22 @@ class CheckCaptures extends Recheck, SymTransformer:
               adaptedType(!boxed)
           else
             adaptedType(boxed)
-      }
+      end adapt
+
+      /** If result derives from caps.Capability, yet is not a capturing type itself,
+       *  make its capture set explicit.
+       */
+      def makeCaptureSetExplicit(result: Type) = result match
+        case CapturingType(_, _) => result
+        case _ =>
+          if result.derivesFromCapability then
+            val cap: CaptureRef = actual match
+              case ref: CaptureRef if ref.isTracked =>
+                ref
+              case _ =>
+                defn.captureRoot.termRef // TODO: skolemize?
+            CapturingType(result, cap.singletonCaptureSet)
+          else result
 
       if expected == LhsProto || expected.isSingleton && actual.isSingleton then
         actual
@@ -1133,10 +1148,12 @@ class CheckCaptures extends Recheck, SymTransformer:
               case _ =>
           case _ =>
         val adapted = adapt(actualw.withReachCaptures(actual), expected, covariant = true)
-        if adapted ne actualw then
-          capt.println(i"adapt boxed $actual vs $expected ===> $adapted")
-          adapted
-        else actual
+        makeCaptureSetExplicit:
+          if adapted ne actualw then
+            capt.println(i"adapt boxed $actual vs $expected ===> $adapted")
+            adapted
+          else
+            actual
     end adaptBoxed
 
     /** Check overrides again, taking capture sets into account.
diff --git a/library/src/scala/caps.scala b/library/src/scala/caps.scala
index 215ad2cb5697..808bdba34e3f 100644
--- a/library/src/scala/caps.scala
+++ b/library/src/scala/caps.scala
@@ -4,7 +4,7 @@ import annotation.experimental
 
 @experimental object caps:
 
-  trait Capability // should be @erased
+  trait Capability extends Any
 
   /** The universal capture reference */
   val cap: Capability = new Capability() {}
diff --git a/tests/neg-custom-args/captures/effect-swaps-explicit.check b/tests/neg-custom-args/captures/effect-swaps-explicit.check
index 47559ab97568..8c4d1f315fd8 100644
--- a/tests/neg-custom-args/captures/effect-swaps-explicit.check
+++ b/tests/neg-custom-args/captures/effect-swaps-explicit.check
@@ -1,29 +1,29 @@
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps-explicit.scala:64:8 -------------------------
-63 |      Result:
-64 |        Future: // error, type mismatch
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps-explicit.scala:62:8 -------------------------
+61 |      Result:
+62 |        Future: // error, type mismatch
    |      ^
    |      Found:    Result.Ok[box Future[box T^?]^{fr, contextual$1}]
    |      Required: Result[Future[T], Nothing]
-65 |          fr.await.ok
+63 |          fr.await.ok
    |--------------------------------------------------------------------------------------------------------------------
    |Inline stack trace
    |- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
-   |This location contains code that was inlined from effect-swaps-explicit.scala:41
-41 |    boundary(Ok(body))
+   |This location contains code that was inlined from effect-swaps-explicit.scala:39
+39 |    boundary(Ok(body))
    |             ^^^^^^^^
     --------------------------------------------------------------------------------------------------------------------
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps-explicit.scala:74:10 ------------------------
-74 |          Future: fut ?=> // error: type mismatch
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps-explicit.scala:72:10 ------------------------
+72 |          Future: fut ?=> // error: type mismatch
    |          ^
    |          Found:    Future[box T^?]^{fr, lbl}
    |          Required: Future[box T^?]^?
-75 |            fr.await.ok
+73 |            fr.await.ok
    |
    | longer explanation available when compiling with `-explain`
--- Error: tests/neg-custom-args/captures/effect-swaps-explicit.scala:68:15 ---------------------------------------------
-68 |        Result.make: //lbl ?=> // error, escaping label from Result
+-- Error: tests/neg-custom-args/captures/effect-swaps-explicit.scala:66:15 ---------------------------------------------
+66 |        Result.make: //lbl ?=> // error, escaping label from Result
    |        ^^^^^^^^^^^
    |local reference contextual$9 from (using contextual$9: boundary.Label[Result[box Future[box T^?]^{fr, contextual$9}, box E^?]]^):
    |  box Future[box T^?]^{fr, contextual$9} leaks into outer capture set of type parameter T of method make in object Result
diff --git a/tests/neg-custom-args/captures/effect-swaps-explicit.scala b/tests/neg-custom-args/captures/effect-swaps-explicit.scala
index 814199706721..052beaab01b2 100644
--- a/tests/neg-custom-args/captures/effect-swaps-explicit.scala
+++ b/tests/neg-custom-args/captures/effect-swaps-explicit.scala
@@ -1,5 +1,3 @@
-import annotation.capability
-
 object boundary:
 
   final class Label[-T] // extends caps.Capability
diff --git a/tests/neg-custom-args/captures/effect-swaps.check b/tests/neg-custom-args/captures/effect-swaps.check
index f16019c15513..ef5a95d333bf 100644
--- a/tests/neg-custom-args/captures/effect-swaps.check
+++ b/tests/neg-custom-args/captures/effect-swaps.check
@@ -1,24 +1,24 @@
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps.scala:64:8 ----------------------------------
-63 |      Result:
-64 |        Future: // error, type mismatch
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps.scala:62:8 ----------------------------------
+61 |      Result:
+62 |        Future: // error, type mismatch
    |      ^
    |      Found:    Result.Ok[box Future[box T^?]^{fr, contextual$1}]
    |      Required: Result[Future[T], Nothing]
-65 |          fr.await.ok
+63 |          fr.await.ok
    |--------------------------------------------------------------------------------------------------------------------
    |Inline stack trace
    |- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
-   |This location contains code that was inlined from effect-swaps.scala:41
-41 |    boundary(Ok(body))
+   |This location contains code that was inlined from effect-swaps.scala:39
+39 |    boundary(Ok(body))
    |             ^^^^^^^^
     --------------------------------------------------------------------------------------------------------------------
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps.scala:74:10 ---------------------------------
-74 |          Future: fut ?=> // error: type mismatch
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps.scala:72:10 ---------------------------------
+72 |          Future: fut ?=> // error: type mismatch
    |          ^
    |          Found:    Future[box T^?]^{fr, lbl}
    |          Required: Future[box T^?]^?
-75 |            fr.await.ok
+73 |            fr.await.ok
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/effect-swaps.scala b/tests/neg-custom-args/captures/effect-swaps.scala
index af44501371a9..d4eed2bae2f2 100644
--- a/tests/neg-custom-args/captures/effect-swaps.scala
+++ b/tests/neg-custom-args/captures/effect-swaps.scala
@@ -1,5 +1,3 @@
-import annotation.capability
-
 object boundary:
 
   final class Label[-T] extends caps.Capability
diff --git a/tests/neg-custom-args/captures/extending-cap-classes.check b/tests/neg-custom-args/captures/extending-cap-classes.check
new file mode 100644
index 000000000000..3bdddfd9dd3c
--- /dev/null
+++ b/tests/neg-custom-args/captures/extending-cap-classes.check
@@ -0,0 +1,21 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/extending-cap-classes.scala:7:15 -------------------------
+7 |  val x2: C1 = new C2 // error
+  |               ^^^^^^
+  |               Found:    C2^
+  |               Required: C1
+  |
+  | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/extending-cap-classes.scala:8:15 -------------------------
+8 |  val x3: C1 = new C3 // error
+  |               ^^^^^^
+  |               Found:    C3^
+  |               Required: C1
+  |
+  | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/extending-cap-classes.scala:13:15 ------------------------
+13 |  val z2: C1 = y2 // error
+   |               ^^
+   |               Found:    (y2 : C2)^{y2}
+   |               Required: C1
+   |
+   | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/extending-cap-classes.scala b/tests/neg-custom-args/captures/extending-cap-classes.scala
new file mode 100644
index 000000000000..6f5a8f48c30a
--- /dev/null
+++ b/tests/neg-custom-args/captures/extending-cap-classes.scala
@@ -0,0 +1,14 @@
+class C1
+class C2 extends C1, caps.Capability
+class C3 extends C2
+
+def test =
+  val x1: C1 = new C1
+  val x2: C1 = new C2 // error
+  val x3: C1 = new C3 // error
+
+  val y2: C2 = new C2
+  val y3: C3 = new C3
+
+  val z2: C1 = y2 // error
+
diff --git a/tests/neg-custom-args/captures/usingLogFile.check b/tests/neg-custom-args/captures/usingLogFile.check
index bf5c1dc4f83a..068d8be78c70 100644
--- a/tests/neg-custom-args/captures/usingLogFile.check
+++ b/tests/neg-custom-args/captures/usingLogFile.check
@@ -1,12 +1,12 @@
--- Error: tests/neg-custom-args/captures/usingLogFile.scala:23:14 ------------------------------------------------------
-23 |  val later = usingLogFile { f => () => f.write(0) } // error
+-- Error: tests/neg-custom-args/captures/usingLogFile.scala:22:14 ------------------------------------------------------
+22 |  val later = usingLogFile { f => () => f.write(0) } // error
    |              ^^^^^^^^^^^^
    |       local reference f leaks into outer capture set of type parameter T of method usingLogFile in object Test2
--- Error: tests/neg-custom-args/captures/usingLogFile.scala:28:23 ------------------------------------------------------
-28 |  private val later2 = usingLogFile { f => Cell(() => f.write(0)) } // error
+-- Error: tests/neg-custom-args/captures/usingLogFile.scala:27:23 ------------------------------------------------------
+27 |  private val later2 = usingLogFile { f => Cell(() => f.write(0)) } // error
    |                       ^^^^^^^^^^^^
    |       local reference f leaks into outer capture set of type parameter T of method usingLogFile in object Test2
--- Error: tests/neg-custom-args/captures/usingLogFile.scala:44:16 ------------------------------------------------------
-44 |    val later = usingFile("out", f => (y: Int) => xs.foreach(x => f.write(x + y))) // error
+-- Error: tests/neg-custom-args/captures/usingLogFile.scala:43:16 ------------------------------------------------------
+43 |    val later = usingFile("out", f => (y: Int) => xs.foreach(x => f.write(x + y))) // error
    |                ^^^^^^^^^
    |          local reference f leaks into outer capture set of type parameter T of method usingFile in object Test3
diff --git a/tests/neg-custom-args/captures/usingLogFile.scala b/tests/neg-custom-args/captures/usingLogFile.scala
index b25e4e75a784..2b46a5401f46 100644
--- a/tests/neg-custom-args/captures/usingLogFile.scala
+++ b/tests/neg-custom-args/captures/usingLogFile.scala
@@ -1,5 +1,4 @@
 import java.io.*
-import annotation.capability
 
 object Test1:
 
diff --git a/tests/pos-custom-args/captures/capt-capability.scala b/tests/pos-custom-args/captures/capt-capability.scala
index 64892218ee41..03b5cb1bbabf 100644
--- a/tests/pos-custom-args/captures/capt-capability.scala
+++ b/tests/pos-custom-args/captures/capt-capability.scala
@@ -1,4 +1,3 @@
-import annotation.capability
 import caps.Capability
 
 def f1(c: Capability): () ->{c} c.type = () => c // ok
diff --git a/tests/pos-custom-args/captures/filevar-tracked.scala b/tests/pos-custom-args/captures/filevar-tracked.scala
index 6fb7000ad4c2..dc8d0b18908b 100644
--- a/tests/pos-custom-args/captures/filevar-tracked.scala
+++ b/tests/pos-custom-args/captures/filevar-tracked.scala
@@ -1,6 +1,5 @@
 import language.experimental.captureChecking
 import language.experimental.modularity
-import annotation.capability
 import compiletime.uninitialized
 
 object test1:
diff --git a/tests/pos-custom-args/captures/i19751.scala b/tests/pos-custom-args/captures/i19751.scala
index 30bd8677f024..b41017f4f3e7 100644
--- a/tests/pos-custom-args/captures/i19751.scala
+++ b/tests/pos-custom-args/captures/i19751.scala
@@ -1,5 +1,4 @@
 import language.experimental.captureChecking
-import annotation.capability
 import caps.cap
 
 trait Ptr[A]
diff --git a/tests/pos-custom-args/captures/logger-tracked.scala b/tests/pos-custom-args/captures/logger-tracked.scala
index 1949e25b00d9..053731de444d 100644
--- a/tests/pos-custom-args/captures/logger-tracked.scala
+++ b/tests/pos-custom-args/captures/logger-tracked.scala
@@ -1,4 +1,3 @@
-import annotation.capability
 import language.experimental.saferExceptions
 import language.experimental.modularity
 
diff --git a/tests/pos-custom-args/captures/logger.scala b/tests/pos-custom-args/captures/logger.scala
index 04aee89a227e..81eeb521fee5 100644
--- a/tests/pos-custom-args/captures/logger.scala
+++ b/tests/pos-custom-args/captures/logger.scala
@@ -1,4 +1,3 @@
-import annotation.capability
 import language.experimental.saferExceptions
 import language.experimental.modularity
 
diff --git a/tests/pos-custom-args/captures/null-logger.scala b/tests/pos-custom-args/captures/null-logger.scala
index 958002ad0358..d532b5f74b38 100644
--- a/tests/pos-custom-args/captures/null-logger.scala
+++ b/tests/pos-custom-args/captures/null-logger.scala
@@ -1,4 +1,3 @@
-import annotation.capability
 import annotation.constructorOnly
 
 class FileSystem extends caps.Capability
diff --git a/tests/pos-custom-args/captures/try3.scala b/tests/pos-custom-args/captures/try3.scala
index 305069d3ae9f..a1a1bab8724a 100644
--- a/tests/pos-custom-args/captures/try3.scala
+++ b/tests/pos-custom-args/captures/try3.scala
@@ -1,5 +1,4 @@
 import language.experimental.erasedDefinitions
-import annotation.capability
 import java.io.IOException
 
 class CanThrow[-E] extends caps.Capability
diff --git a/tests/pos-with-compiler-cc/dotc/core/Definitions.scala b/tests/pos-with-compiler-cc/dotc/core/Definitions.scala
index 603088dd8f26..8faf208e36d0 100644
--- a/tests/pos-with-compiler-cc/dotc/core/Definitions.scala
+++ b/tests/pos-with-compiler-cc/dotc/core/Definitions.scala
@@ -985,7 +985,6 @@ class Definitions {
   @tu lazy val BeanPropertyAnnot: ClassSymbol = requiredClass("scala.beans.BeanProperty")
   @tu lazy val BooleanBeanPropertyAnnot: ClassSymbol = requiredClass("scala.beans.BooleanBeanProperty")
   @tu lazy val BodyAnnot: ClassSymbol = requiredClass("scala.annotation.internal.Body")
-  @tu lazy val CapabilityAnnot: ClassSymbol = requiredClass("scala.annotation.capability")
   @tu lazy val ChildAnnot: ClassSymbol = requiredClass("scala.annotation.internal.Child")
   @tu lazy val ContextResultCountAnnot: ClassSymbol = requiredClass("scala.annotation.internal.ContextResultCount")
   @tu lazy val ProvisionalSuperClassAnnot: ClassSymbol = requiredClass("scala.annotation.internal.ProvisionalSuperClass")
diff --git a/tests/pos/i20237.scala b/tests/pos/i20237.scala
index 0a5eb6d9a332..973f5d2025e3 100644
--- a/tests/pos/i20237.scala
+++ b/tests/pos/i20237.scala
@@ -1,5 +1,4 @@
 import language.experimental.captureChecking
-import scala.annotation.capability
 
 class Cap extends caps.Capability:
   def use[T](body: Cap ?=> T) = body(using this)

From 917d576b829cecd3109167ac52fdc08863807dae Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Sat, 25 May 2024 12:53:02 +0200
Subject: [PATCH 11/14] Existential capabilities design draft

---
 .../src/dotty/tools/dotc/cc/Existential.scala | 217 ++++++++++++++++++
 .../dotty/tools/dotc/core/TypeComparer.scala  |  57 ++++-
 2 files changed, 267 insertions(+), 7 deletions(-)
 create mode 100644 compiler/src/dotty/tools/dotc/cc/Existential.scala

diff --git a/compiler/src/dotty/tools/dotc/cc/Existential.scala b/compiler/src/dotty/tools/dotc/cc/Existential.scala
new file mode 100644
index 000000000000..7a191ae3769a
--- /dev/null
+++ b/compiler/src/dotty/tools/dotc/cc/Existential.scala
@@ -0,0 +1,217 @@
+package dotty.tools
+package dotc
+package cc
+
+import core.*
+import Types.*, Symbols.*, Contexts.*, Annotations.*, Flags.*
+import CaptureSet.IdempotentCaptRefMap
+import StdNames.nme
+
+/**
+
+Handling existentials in CC:
+
+In adapt:
+
+  - If an EX is toplevel in expected type, replace with a fresh capture set variable
+  - If an EX is toplevel in actual type, find a trackable replacement `x` as follows:
+      + If actual type is a trackable ref, pick that
+      + Otherwise, create a fresh skolem val symbol with currently enclosing
+        method as owner, and use its termRef
+    Then,
+      + If the EX-bound variable appears only at toplevel, replace it with `x`
+      + Otherwise, replace it with a fresh reach capability `x*`.
+
+In avoidance of a type T:
+
+  - Replace all co-variant occurrences of locals variables in T (including locally
+    created EX-skolems) with single fresh EX-bound variable, which wraps T.
+  - Contravariant occurrences of local variables are approximated by the empty capture set,
+    as was the case before.
+  - Invariant occurrences of local variables produce errors, as was the case before.
+  - Check that no existentially quantified local variable appears under a box.
+
+The reason it is done this way is that it produces the smallest existential type
+wrt the existential type ordering shown below. For instance, consider the type
+
+      (A^{x}, B^{y})
+
+where `x` and `y` are local. We widen to
+
+      EX a.(A^{a}, B^{a})
+
+rather than
+
+      EX a.EX b.(A^{a}, A^{b})
+
+In the subtype ordering of existentials the first of these types is a subtype of
+the other, but not _vice versa_.
+
+In cv-computation (markFree):
+
+  - Reach capabilities x* of a parameter x cannot appear in the capture set of
+    the owning method. They have to be widened to dcs(x), or, where this is not
+    possible, it's an error.
+
+In well-formedness checking of explicitly written type T:
+
+  - If T is not the type of a parameter, check that no EX-bound variable appears
+    under a box.
+
+Subtype rules
+
+  - new alphabet: existentially bound variables `a`.
+  - they can be stored in environments Gamma.
+  - they are alpha-renable, usual hygiene conditions apply
+
+      Gamma |- EX a.T <: U
+        if Gamma, a |- T <: U
+
+      Gamma |- T <: EX a.U
+        if a in Gamma, T <: U
+
+  Note that this is a fairly restrictive ordering. A more permissive ordering would
+  allow us to instantiate EX-quantified variables to sets of other EX-quantified
+  variables since in the end all we need to do is ensure subcapturing of sets. But
+  that would be algorithmically more complicated.
+
+Representation:
+
+  EX a.T[a] is  represented as
+
+      r @ RecType(T[TermRef[r.recThis, caps.cap]]
+
+Subtype checking algorithm, general scheme:
+
+  Maintain two structures in TypeComparer:
+
+    openExistentials: List[RecThis]
+    assocExistentials: Map[RecThis, List[RecThis]]
+
+  `openExistentials` corresponds to the list of existential variables stored in the environment.
+  `assocExistentials` maps existential variables bound by existentials appearing on the right
+  of a subtype judgement to a list of possible associations. Initally this is openExistentials
+  at the time when the existential on the right was dropped. It can become a single existential
+  when the existentially bound key variable is unified with one of the variables in the
+  environment.
+
+Subtype checking algorithm, steps to add for tp1 <:< tp2:
+
+  If tp1 is an existential EX a.tp1a:
+
+      val saved = openExistentials
+      openExistentials = tp1.recThis :: openExistentials
+      try tp1a <:< tp2
+      finally openExistentials = saved
+
+  If tp2 is an existential EX a.tp2a:
+
+      val saved = assocExistentials
+      assocExistentials = assocExistentials + (tp2.recThis -> openExistentials
+      try tp1 <:< tp2a
+      finally assocExistentials = saved
+
+  If tp1 and tp2 are existentially bound variables `TermRef(pre1/pre2: RecThis, cap)`:
+
+      assocExistentials(pre2).contains(pre1) &&
+      { assocExistentials(pre2) = List(pre1); true }
+
+Existential source syntax:
+
+  Existential types are ususally not written in source, since we still allow the `^`
+  syntax that can express most of them more concesely (see below for translation rules).
+  But we should also allow to write existential types explicity, even if it ends up mainly
+  for debugging. To express them, we add the following trait definition in the caps object:
+
+      trait Exists[X]
+
+  A typical expression of an existential is then
+
+      Exists[(x: Capability) => A ->{x} B]
+
+  Existential types are expanded at Typer to the RecType syntax presented above. It is checked
+  that the type argument is a dependent function type with one argument of type `Capability` and
+  that this argument is used only in capture sets of the result type.
+
+  Existential types can only appear at the top-level of _legal existential scopes_. These are:
+
+    - The type of a binding: i.e a type of a parameter or val, a result type of a def, or
+      a self type of a class.
+    - The type of a type ascription in an expression or pattern
+    - The argument and result types of a function.
+
+Expansion of ^:
+
+  We drop `cap` as a capture reference, but keep the unqualified `^` syntax.
+  This now expands to existentials. The translation treats each legal existential scope
+  separately. If existential scopes nest, the inner ones are translated first.
+
+  The expansion algorithm is then defined as follows:
+
+    1. In an existential scope, replace every occurrence of ^ with a fresh existentially
+        bound variable and quantify over all variables such introduced.
+
+    2. After this step, type aliases are expanded. If aliases have aliases in arguments,
+        the outer alias is expanded before the aliases in the arguments. Each time an alias
+        is expanded that reveals a `^`, apply step (1).
+
+    3. The algorithm ends when no more alieases remain to be expanded.
+
+  ^ captures outside an existential scope or the right hand side of a type alias (e.g. in
+  a class parent) are not allowed.
+
+  Examples:
+
+    - `A => B` is an alias type that expands to `(A -> B)^`, which expands to `EX c. A ->{c} B`.
+
+    - `Iterator[A => B]` expands to `EX c. Iterator[A ->{c} B]`
+
+    - `A -> B^` expands to `A -> EX c.B^{c}`.
+
+    - If we define `type Fun[T] = A -> T`, then `Fun[B^]` expands to `EX c.Fun[B^{c}]`, which
+      dealiases to `EX c.A -> B^{c}`.
+
+    - If we define
+
+        type F = A -> Fun[B^]
+
+      then the type alias expands to
+
+        type F = A -> EX c.A -> B^{c}
+
+      since the result type of the RHS is a legal existential scope.
+*/
+object Existential:
+
+  private class PackMap(sym: Symbol, rt: RecType)(using Context) extends DeepTypeMap, IdempotentCaptRefMap:
+    def apply(tp: Type): Type = tp match
+      case ref: TermRef if ref.symbol == sym => TermRef(rt.recThis, defn.captureRoot)
+      case _ => mapOver(tp)
+
+  /** Unpack current type from an existential `rt` so that all references bound by `rt`
+   *  are recplaced by `ref`.
+   */
+  private class OpenMap(rt: RecType, ref: Type)(using Context) extends DeepTypeMap, IdempotentCaptRefMap:
+    def apply(tp: Type): Type =
+      if isExBound(tp, rt) then ref else mapOver(tp)
+
+  /** Is `tp` a reference to the bound variable of `rt`? */
+  private def isExBound(tp: Type, rt: Type)(using Context) = tp match
+    case tp @ TermRef(RecThis(rt1), _) => (rt1 eq rt) && tp.symbol == defn.captureRoot
+    case _ => false
+
+  /** Open existential, replacing the bund variable by `ref` */
+  def open(rt: RecType, ref: Type)(using Context): Type = OpenMap(rt, ref)(rt.parent)
+
+  /** Create an existential type `ex c.<tp>` so that all references to `sym` in `tp`
+   *  become references to the existentially bound variable `c`.
+   */
+  def fromSymbol(tp: Type, sym: Symbol)(using Context): RecType =
+    RecType(PackMap(sym, _)(tp))
+
+  def unapply(rt: RecType)(using Context): Option[Type] =
+    if isCaptureChecking && rt.parent.existsPart(isExBound(_, rt))
+    then Some(rt.parent)
+    else None
+
+end Existential
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index c4f34753bb7f..1cd4d8f4c83b 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -46,6 +46,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
     monitored = false
     GADTused = false
     opaquesUsed = false
+    openedExistentials = Nil
+    assocExistentials = Map.empty
     recCount = 0
     needsGc = false
     if Config.checkTypeComparerReset then checkReset()
@@ -64,6 +66,18 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
   /** Indicates whether the subtype check used opaque types */
   private var opaquesUsed: Boolean = false
 
+  /** In capture checking: The existential types that are open because they
+   *  appear in an existential type on the left in an enclosing comparison.
+   */
+  private var openedExistentials: List[RecThis] = Nil
+
+  /** In capture checking: A map from existential types that are appear
+   *  in an existential type on the right in an enclosing comparison.
+   *  Each existential gets mapped to the opened existentials to which it
+   *  may resolve at this point.
+   */
+  private var assocExistentials: Map[RecThis, List[RecThis]] = Map.empty
+
   private var myInstance: TypeComparer = this
   def currentInstance: TypeComparer = myInstance
 
@@ -325,14 +339,17 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
                 isSubPrefix(tp1.prefix, tp2.prefix) ||
                 thirdTryNamed(tp2)
               else
-                (  (tp1.name eq tp2.name)
+                (tp1.name eq tp2.name)
                 && !sym1.is(Private)
-                && tp2.isPrefixDependentMemberRef
-                && isSubPrefix(tp1.prefix, tp2.prefix)
-                && tp1.signature == tp2.signature
-                && !(sym1.isClass && sym2.isClass)  // class types don't subtype each other
-                ) ||
-                thirdTryNamed(tp2)
+                && (
+                  tp2.isPrefixDependentMemberRef
+                    && isSubPrefix(tp1.prefix, tp2.prefix)
+                    && tp1.signature == tp2.signature
+                    && !(sym1.isClass && sym2.isClass)  // class types don't subtype each other
+                  || tp1.name == nme.CAPTURE_ROOT
+                    && existentialsConform(tp1, tp2)
+                )
+                || thirdTryNamed(tp2)
             case _ =>
               secondTry
         end compareNamed
@@ -416,6 +433,18 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
         secondTry
     }
 
+    def existentialsConform(tp1: NamedType, tp2: NamedType) = (tp1, tp2) match
+      case (TermRef(rt1: RecThis, _), TermRef(rt2: RecThis, _)) =>
+        def link(rt1: RecThis, rt2: RecThis) =
+          assocExistentials.get(rt2).exists(_.contains(rt1))
+          && {
+            assocExistentials = assocExistentials.updated(rt2, rt1 :: Nil)
+            true
+          }
+        link(rt2, rt1) || link(rt1, rt2)
+      case _ =>
+        false
+
     def secondTry: Boolean = tp1 match {
       case tp1: NamedType =>
         tp1.info match {
@@ -546,6 +575,13 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
         if reduced.exists then
           recur(reduced, tp2) && recordGadtUsageIf { MatchType.thatReducesUsingGadt(tp1) }
         else thirdTry
+      case tp1 @ cc.Existential(tp1unpacked) =>
+        val saved = openedExistentials
+        try
+          openedExistentials = tp1.recThis :: openedExistentials
+          recur(tp1unpacked, tp2)
+        finally
+          openedExistentials = saved
       case _: FlexType =>
         true
       case _ =>
@@ -696,6 +732,13 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
         end compareRefined
 
         compareRefined
+      case tp2 @ cc.Existential(tp2unpacked) =>
+        val saved = assocExistentials
+        try
+          assocExistentials = assocExistentials.updated(tp2.recThis, openedExistentials)
+          recur(tp1, tp2unpacked)
+        finally
+          assocExistentials = saved
       case tp2: RecType =>
         def compareRec = tp1.safeDealias match {
           case tp1: RecType =>

From 322501b0b8e519da37cca2e66bfe64d58beb6e14 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Tue, 28 May 2024 16:19:54 +0200
Subject: [PATCH 12/14] Implement subtyping between existential types

---
 .../src/dotty/tools/dotc/cc/CaptureSet.scala  |   3 +
 .../dotty/tools/dotc/cc/CheckCaptures.scala   |   5 +-
 .../src/dotty/tools/dotc/cc/Existential.scala |  75 +++++++----
 .../dotty/tools/dotc/core/Definitions.scala   |  13 +-
 .../dotty/tools/dotc/core/TypeComparer.scala  | 123 ++++++++++--------
 library/src/scala/caps.scala                  |   6 +
 tests/neg/cc-existentials.scala               |  25 ++++
 7 files changed, 167 insertions(+), 83 deletions(-)
 create mode 100644 tests/neg/cc-existentials.scala

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index f78ed1a91bd6..a61a767eb873 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -14,6 +14,7 @@ import printing.{Showable, Printer}
 import printing.Texts.*
 import util.{SimpleIdentitySet, Property}
 import typer.ErrorReporting.Addenda
+import TypeComparer.linkOK
 import util.common.alwaysTrue
 import scala.collection.mutable
 
@@ -159,6 +160,7 @@ sealed abstract class CaptureSet extends Showable:
             || y.info.match
                 case y1: CaptureRef => x.subsumes(y1)
                 case _ => false
+          case y: TermParamRef => linkOK(y, x)
           case MaybeCapability(y1) => x.stripMaybe.subsumes(y1)
           case _ => false
       || x.match
@@ -167,6 +169,7 @@ sealed abstract class CaptureSet extends Showable:
             x.info match
               case x1: CaptureRef => x1.subsumes(y)
               case _ => false
+          case x: TermParamRef => linkOK(x, y)
           case _ => false
 
   /** {x} <:< this   where <:< is subcapturing, but treating all variables
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 5daa56b9cc07..45ccacacbbea 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -907,8 +907,7 @@ class CheckCaptures extends Recheck, SymTransformer:
         case expected @ defn.FunctionOf(args, resultType, isContextual)
         if defn.isNonRefinedFunction(expected) =>
           actual match
-            case RefinedType(parent, nme.apply, rinfo: MethodType)
-            if defn.isFunctionNType(actual) =>
+            case defn.RefinedFunctionOf(rinfo: MethodType) =>
               depFun(args, resultType, isContextual, rinfo.paramNames)
             case _ => expected
         case _ => expected
@@ -999,7 +998,7 @@ class CheckCaptures extends Recheck, SymTransformer:
           val (eargs, eres) = expected.dealias.stripCapturing match
             case defn.FunctionOf(eargs, eres, _) => (eargs, eres)
             case expected: MethodType => (expected.paramInfos, expected.resType)
-            case expected @ RefinedType(_, _, rinfo: MethodType) if defn.isFunctionNType(expected) => (rinfo.paramInfos, rinfo.resType)
+            case defn.RefinedFunctionOf(rinfo: MethodType) => (rinfo.paramInfos, rinfo.resType)
             case _ => (aargs.map(_ => WildcardType), WildcardType)
           val aargs1 = aargs.zipWithConserve(eargs) { (aarg, earg) => adapt(aarg, earg, !covariant) }
           val ares1 = adapt(ares, eres, covariant)
diff --git a/compiler/src/dotty/tools/dotc/cc/Existential.scala b/compiler/src/dotty/tools/dotc/cc/Existential.scala
index 7a191ae3769a..aefaa12ca6c7 100644
--- a/compiler/src/dotty/tools/dotc/cc/Existential.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Existential.scala
@@ -6,6 +6,9 @@ import core.*
 import Types.*, Symbols.*, Contexts.*, Annotations.*, Flags.*
 import CaptureSet.IdempotentCaptRefMap
 import StdNames.nme
+import ast.tpd.*
+import Decorators.*
+import typer.ErrorReporting.errorType
 
 /**
 
@@ -77,20 +80,29 @@ Subtype rules
 
 Representation:
 
-  EX a.T[a] is  represented as
+  EX a.T[a] is represented as a dependent function type
 
-      r @ RecType(T[TermRef[r.recThis, caps.cap]]
+      (a: Exists) => T[a]]
+
+  where Exists is defined in caps like this:
+
+      sealed trait Exists extends Capability
+
+  The defn.RefinedFunctionOf extractor will exclude existential types from
+  its results, so only normal refined functions match.
+
+  Let `boundvar(ex)` be the TermParamRef defined by the extistential type `ex`.
 
 Subtype checking algorithm, general scheme:
 
   Maintain two structures in TypeComparer:
 
-    openExistentials: List[RecThis]
-    assocExistentials: Map[RecThis, List[RecThis]]
+    openExistentials: List[TermParamRef]
+    assocExistentials: Map[TermParamRef, List[TermParamRef]]
 
   `openExistentials` corresponds to the list of existential variables stored in the environment.
   `assocExistentials` maps existential variables bound by existentials appearing on the right
-  of a subtype judgement to a list of possible associations. Initally this is openExistentials
+  of a subtype judgement to a list of possible associations. Initially this is openExistentials
   at the time when the existential on the right was dropped. It can become a single existential
   when the existentially bound key variable is unified with one of the variables in the
   environment.
@@ -100,38 +112,31 @@ Subtype checking algorithm, steps to add for tp1 <:< tp2:
   If tp1 is an existential EX a.tp1a:
 
       val saved = openExistentials
-      openExistentials = tp1.recThis :: openExistentials
+      openExistentials = boundvar(tp1) :: openExistentials
       try tp1a <:< tp2
       finally openExistentials = saved
 
   If tp2 is an existential EX a.tp2a:
 
       val saved = assocExistentials
-      assocExistentials = assocExistentials + (tp2.recThis -> openExistentials
+      assocExistentials = assocExistentials + (boundvar(tp2) -> openExistentials
       try tp1 <:< tp2a
       finally assocExistentials = saved
 
-  If tp1 and tp2 are existentially bound variables `TermRef(pre1/pre2: RecThis, cap)`:
+  If tp1 and tp2 are existentially bound variables:
 
-      assocExistentials(pre2).contains(pre1) &&
-      { assocExistentials(pre2) = List(pre1); true }
+      assocExistentials(tpi).contains(tpj) &&
+      { assocExistentials(tpi) = List(tpj); true }
 
 Existential source syntax:
 
   Existential types are ususally not written in source, since we still allow the `^`
   syntax that can express most of them more concesely (see below for translation rules).
   But we should also allow to write existential types explicity, even if it ends up mainly
-  for debugging. To express them, we add the following trait definition in the caps object:
-
-      trait Exists[X]
-
-  A typical expression of an existential is then
+  for debugging. To express them, we use the encoding with `Exists`, so a typical
+  expression of an existential would be
 
-      Exists[(x: Capability) => A ->{x} B]
-
-  Existential types are expanded at Typer to the RecType syntax presented above. It is checked
-  that the type argument is a dependent function type with one argument of type `Capability` and
-  that this argument is used only in capture sets of the result type.
+      (x: Exists) => A ->{x} B
 
   Existential types can only appear at the top-level of _legal existential scopes_. These are:
 
@@ -183,6 +188,23 @@ Expansion of ^:
 */
 object Existential:
 
+  def fromDepFun(arg: Tree)(using Context): Type = arg.tpe match
+    case RefinedType(parent, nme.apply, info: MethodType) if defn.isNonRefinedFunction(parent) =>
+      info match
+        case info @ MethodType(_ :: Nil)
+        if info.paramInfos.head.derivesFrom(defn.Caps_Capability) =>
+          apply(ref => info.resultType.substParams(info, ref :: Nil))
+        case _ =>
+          errorType(em"Malformed existential: dependent function must have a singgle parameter of type caps.Capability", arg.srcPos)
+    case _ =>
+      errorType(em"Malformed existential: dependent function type expected", arg.srcPos)
+
+  def apply(fn: TermRef => Type)(using Context): RecType =
+    RecType(rt => fn(exBoundRef(rt)))
+
+  def exBoundRef(rt: RecType)(using Context): TermRef =
+    TermRef(rt.recThis, defn.captureRoot)
+
   private class PackMap(sym: Symbol, rt: RecType)(using Context) extends DeepTypeMap, IdempotentCaptRefMap:
     def apply(tp: Type): Type = tp match
       case ref: TermRef if ref.symbol == sym => TermRef(rt.recThis, defn.captureRoot)
@@ -209,9 +231,14 @@ object Existential:
   def fromSymbol(tp: Type, sym: Symbol)(using Context): RecType =
     RecType(PackMap(sym, _)(tp))
 
-  def unapply(rt: RecType)(using Context): Option[Type] =
-    if isCaptureChecking && rt.parent.existsPart(isExBound(_, rt))
-    then Some(rt.parent)
-    else None
+  def isExistentialMethod(mt: MethodType)(using Context): Boolean = mt.paramInfos match
+    case (info: TypeRef) :: rest => info.symbol == defn.Caps_Exists && rest.isEmpty
+    case _ => false
 
+  def unapply(tp: RefinedType)(using Context): Option[(TermParamRef, Type)] =
+    tp.refinedInfo match
+      case mt: MethodType
+      if isExistentialMethod(mt) && defn.isNonRefinedFunction(tp.parent) =>
+        Some(mt.paramRefs.head, mt.resultType)
+      case _ => None
 end Existential
diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala
index 52535f26c692..1ef1c7254b24 100644
--- a/compiler/src/dotty/tools/dotc/core/Definitions.scala
+++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala
@@ -15,7 +15,7 @@ import Comments.{Comment, docCtx}
 import util.Spans.NoSpan
 import config.Feature
 import Symbols.requiredModuleRef
-import cc.{CaptureSet, RetainingType}
+import cc.{CaptureSet, RetainingType, Existential}
 import ast.tpd.ref
 
 import scala.annotation.tailrec
@@ -993,6 +993,7 @@ class Definitions {
     @tu lazy val captureRoot: TermSymbol = CapsModule.requiredValue("cap")
     @tu lazy val Caps_Capability: TypeSymbol = CapsModule.requiredType("Capability")
     @tu lazy val Caps_reachCapability: TermSymbol = CapsModule.requiredMethod("reachCapability")
+    @tu lazy val Caps_Exists = requiredClass("scala.caps.Exists")
     @tu lazy val CapsUnsafeModule: Symbol = requiredModule("scala.caps.unsafe")
     @tu lazy val Caps_unsafeAssumePure: Symbol = CapsUnsafeModule.requiredMethod("unsafeAssumePure")
     @tu lazy val Caps_unsafeBox: Symbol = CapsUnsafeModule.requiredMethod("unsafeBox")
@@ -1189,11 +1190,17 @@ class Definitions {
 
     /** Matches a refined `PolyFunction`/`FunctionN[...]`/`ContextFunctionN[...]`.
      *  Extracts the method type type and apply info.
+     *  Will NOT math an existential type encoded as a dependent function.
      */
     def unapply(tpe: RefinedType)(using Context): Option[MethodOrPoly] =
       tpe.refinedInfo match
-        case mt: MethodOrPoly
-        if tpe.refinedName == nme.apply && isFunctionType(tpe.parent) => Some(mt)
+        case mt: MethodType
+        if tpe.refinedName == nme.apply
+            && isFunctionType(tpe.parent)
+            && !Existential.isExistentialMethod(mt) => Some(mt)
+        case mt: PolyType
+        if tpe.refinedName == nme.apply
+            && isFunctionType(tpe.parent) => Some(mt)
         case _ => None
 
   end RefinedFunctionOf
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 1cd4d8f4c83b..866d685a53dc 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -69,14 +69,14 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
   /** In capture checking: The existential types that are open because they
    *  appear in an existential type on the left in an enclosing comparison.
    */
-  private var openedExistentials: List[RecThis] = Nil
+  private var openedExistentials: List[TermParamRef] = Nil
 
   /** In capture checking: A map from existential types that are appear
    *  in an existential type on the right in an enclosing comparison.
    *  Each existential gets mapped to the opened existentials to which it
    *  may resolve at this point.
    */
-  private var assocExistentials: Map[RecThis, List[RecThis]] = Map.empty
+  private var assocExistentials: Map[TermParamRef, List[TermParamRef]] = Map.empty
 
   private var myInstance: TypeComparer = this
   def currentInstance: TypeComparer = myInstance
@@ -341,14 +341,10 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
               else
                 (tp1.name eq tp2.name)
                 && !sym1.is(Private)
-                && (
-                  tp2.isPrefixDependentMemberRef
-                    && isSubPrefix(tp1.prefix, tp2.prefix)
-                    && tp1.signature == tp2.signature
-                    && !(sym1.isClass && sym2.isClass)  // class types don't subtype each other
-                  || tp1.name == nme.CAPTURE_ROOT
-                    && existentialsConform(tp1, tp2)
-                )
+                && tp2.isPrefixDependentMemberRef
+                && isSubPrefix(tp1.prefix, tp2.prefix)
+                && tp1.signature == tp2.signature
+                && !(sym1.isClass && sym2.isClass)  // class types don't subtype each other
                 || thirdTryNamed(tp2)
             case _ =>
               secondTry
@@ -361,7 +357,9 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
       case tp2: ProtoType =>
         isMatchedByProto(tp2, tp1)
       case tp2: BoundType =>
-        tp2 == tp1 || secondTry
+        tp2 == tp1
+        || existentialVarsConform(tp1, tp2)
+        || secondTry
       case tp2: TypeVar =>
         recur(tp1, typeVarInstance(tp2))
       case tp2: WildcardType =>
@@ -433,18 +431,6 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
         secondTry
     }
 
-    def existentialsConform(tp1: NamedType, tp2: NamedType) = (tp1, tp2) match
-      case (TermRef(rt1: RecThis, _), TermRef(rt2: RecThis, _)) =>
-        def link(rt1: RecThis, rt2: RecThis) =
-          assocExistentials.get(rt2).exists(_.contains(rt1))
-          && {
-            assocExistentials = assocExistentials.updated(rt2, rt1 :: Nil)
-            true
-          }
-        link(rt2, rt1) || link(rt1, rt2)
-      case _ =>
-        false
-
     def secondTry: Boolean = tp1 match {
       case tp1: NamedType =>
         tp1.info match {
@@ -575,13 +561,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
         if reduced.exists then
           recur(reduced, tp2) && recordGadtUsageIf { MatchType.thatReducesUsingGadt(tp1) }
         else thirdTry
-      case tp1 @ cc.Existential(tp1unpacked) =>
-        val saved = openedExistentials
-        try
-          openedExistentials = tp1.recThis :: openedExistentials
-          recur(tp1unpacked, tp2)
-        finally
-          openedExistentials = saved
+      case Existential(boundVar, tp1unpacked) =>
+        compareExistentialLeft(boundVar, tp1unpacked, tp2)
       case _: FlexType =>
         true
       case _ =>
@@ -663,6 +644,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
         thirdTryNamed(tp2)
       case tp2: TypeParamRef =>
         compareTypeParamRef(tp2)
+      case Existential(boundVar, tp2unpacked) =>
+        compareExistentialRight(tp1, boundVar, tp2unpacked)
       case tp2: RefinedType =>
         def compareRefinedSlow: Boolean =
           val name2 = tp2.refinedName
@@ -732,13 +715,6 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
         end compareRefined
 
         compareRefined
-      case tp2 @ cc.Existential(tp2unpacked) =>
-        val saved = assocExistentials
-        try
-          assocExistentials = assocExistentials.updated(tp2.recThis, openedExistentials)
-          recur(tp1, tp2unpacked)
-        finally
-          assocExistentials = saved
       case tp2: RecType =>
         def compareRec = tp1.safeDealias match {
           case tp1: RecType =>
@@ -1462,20 +1438,21 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
           canConstrain(param2) && canInstantiate(param2) ||
           compareLower(bounds(param2), tyconIsTypeRef = false)
         case tycon2: TypeRef =>
-          isMatchingApply(tp1) ||
-          byGadtBounds ||
-          defn.isCompiletimeAppliedType(tycon2.symbol) && compareCompiletimeAppliedType(tp2, tp1, fromBelow = true) || {
-            tycon2.info match {
-              case info2: TypeBounds =>
-                compareLower(info2, tyconIsTypeRef = true)
-              case info2: ClassInfo =>
-                tycon2.name.startsWith("Tuple") &&
-                  defn.isTupleNType(tp2) && recur(tp1, tp2.toNestedPairs) ||
-                tryBaseType(info2.cls)
-              case _ =>
-                fourthTry
-            }
-          } || tryLiftedToThis2
+          isMatchingApply(tp1)
+          || byGadtBounds
+          || defn.isCompiletimeAppliedType(tycon2.symbol)
+              && compareCompiletimeAppliedType(tp2, tp1, fromBelow = true)
+          || tycon2.info.match
+                case info2: TypeBounds =>
+                  compareLower(info2, tyconIsTypeRef = true)
+                case info2: ClassInfo =>
+                  tycon2.name.startsWith("Tuple")
+                  && defn.isTupleNType(tp2)
+                  && recur(tp1, tp2.toNestedPairs)
+                  || tryBaseType(info2.cls)
+                case _ =>
+                  fourthTry
+          || tryLiftedToThis2
 
         case tv: TypeVar =>
           if tv.isInstantiated then
@@ -1512,12 +1489,12 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
               inFrozenGadt { isSubType(bounds1.hi.applyIfParameterized(args1), tp2, approx.addLow) }
             } && recordGadtUsageIf(true)
 
-
           !sym.isClass && {
             defn.isCompiletimeAppliedType(sym) && compareCompiletimeAppliedType(tp1, tp2, fromBelow = false) ||
             { recur(tp1.superTypeNormalized, tp2) && recordGadtUsageIf(MatchType.thatReducesUsingGadt(tp1)) } ||
             tryLiftedToThis1
-          } || byGadtBounds
+          }
+          || byGadtBounds
         case tycon1: TypeProxy =>
           recur(tp1.superTypeNormalized, tp2)
         case _ =>
@@ -2818,6 +2795,43 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
       false
   }
 
+  private def compareExistentialLeft(boundVar: TermParamRef, tp1unpacked: Type, tp2: Type)(using Context): Boolean =
+    val saved = openedExistentials
+    try
+      openedExistentials = boundVar :: openedExistentials
+      recur(tp1unpacked, tp2)
+    finally
+      openedExistentials = saved
+
+  private def compareExistentialRight(tp1: Type, boundVar: TermParamRef, tp2unpacked: Type)(using Context): Boolean =
+    val saved = assocExistentials
+    try
+      //println(i"assoc $boundVar = $openedExistentials")
+      assocExistentials = assocExistentials.updated(boundVar, openedExistentials)
+      recur(tp1, tp2unpacked)
+    finally
+      assocExistentials = saved
+
+  def linkOK(tp1: TermParamRef, tp2: CaptureRef)(using Context): Boolean =
+    assocExistentials.get(tp1).exists(_.contains(tp2))
+    && {
+      assocExistentials = assocExistentials.updated(tp1, tp2.asInstanceOf[TermParamRef] :: Nil)
+      true
+    }
+
+  /** Are tp1, tp2 termRefs that can be linked? This should never be called
+   *  normally, since exietential variables appear only in capture sets
+   *  which are in annotations that are ignored during normal typing. The real
+   *  work is done in CaptureSet#subsumes which calls linkOK directly.
+   */
+  private def existentialVarsConform(tp1: Type, tp2: Type) = tp1 match
+    case tp1: TermParamRef =>
+      tp2 match
+        case tp2: TermParamRef =>
+          linkOK(tp1, tp2) || linkOK(tp2, tp1)
+        case _ => false
+    case _ => false
+
   protected def subCaptures(refs1: CaptureSet, refs2: CaptureSet, frozen: Boolean)(using Context): CaptureSet.CompareResult =
     refs1.subCaptures(refs2, frozen)
 
@@ -3283,6 +3297,9 @@ object TypeComparer {
   def lub(tp1: Type, tp2: Type, canConstrain: Boolean = false, isSoft: Boolean = true)(using Context): Type =
     comparing(_.lub(tp1, tp2, canConstrain = canConstrain, isSoft = isSoft))
 
+  def linkOK(tp1: TermParamRef, tp2: CaptureRef)(using Context) =
+    comparing(_.linkOK(tp1, tp2))
+
   /** The least upper bound of a list of types */
   final def lub(tps: List[Type])(using Context): Type =
     tps.foldLeft(defn.NothingType: Type)(lub(_,_))
diff --git a/library/src/scala/caps.scala b/library/src/scala/caps.scala
index 808bdba34e3f..840601f1622d 100644
--- a/library/src/scala/caps.scala
+++ b/library/src/scala/caps.scala
@@ -22,6 +22,12 @@ import annotation.experimental
    */
   extension (x: Any) def reachCapability: Any = x
 
+  /** A trait to allow expressing existential types such as
+   *
+   *      (x: Exists) => A ->{x} B
+   */
+  sealed trait Exists extends Capability
+
   object unsafe:
 
     extension [T](x: T)
diff --git a/tests/neg/cc-existentials.scala b/tests/neg/cc-existentials.scala
new file mode 100644
index 000000000000..27e434079fe0
--- /dev/null
+++ b/tests/neg/cc-existentials.scala
@@ -0,0 +1,25 @@
+import language.experimental.captureChecking
+import caps.{Exists, Capability}
+
+class C
+
+type EX1 = (c: Exists) => (C^{c}, C^{c})
+
+type EX2 = (c1: Exists) => (c2: Exists) => (C^{c1}, C^{c2})
+
+type EX3 = (c: Exists) => () => C^{c}
+
+type EX4 = () => (c: Exists) => C^{c}
+
+def Test =
+  val ex1: EX1 = ???
+  val ex2: EX2 = ???
+  val _: EX1 = ex1
+  val _: EX2 = ex1
+  val _: EX1 = ex2  // error
+
+  val ex3: EX3 = ???
+  val ex4: EX4 = ???
+  val _: EX4 = ex3
+  val _: EX4 = ex4
+  val _: EX3 = ex4 // error

From 555089a692efcd8c2f7c6023c8a7fb45cc9d157e Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Thu, 30 May 2024 16:33:43 +0200
Subject: [PATCH 13/14] Open expected and actual existentials (draft)

---
 .../dotty/tools/dotc/cc/CheckCaptures.scala   | 34 +++++---
 .../src/dotty/tools/dotc/cc/Existential.scala | 77 ++++++++++++++++---
 compiler/src/dotty/tools/dotc/cc/Setup.scala  |  7 +-
 .../src/dotty/tools/dotc/core/NameKinds.scala |  1 +
 .../src/dotty/tools/dotc/core/Types.scala     |  7 +-
 .../tools/dotc/printing/RefinedPrinter.scala  |  4 +-
 .../dotty/tools/dotc/transform/Recheck.scala  |  6 +-
 ...tentials.scala => cc-ex-conformance.scala} |  8 +-
 tests/pos/cc-ex-unpack.scala                  | 18 +++++
 9 files changed, 132 insertions(+), 30 deletions(-)
 rename tests/neg/{cc-existentials.scala => cc-ex-conformance.scala} (61%)
 create mode 100644 tests/pos/cc-ex-unpack.scala

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 45ccacacbbea..da5a80d520d3 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -696,6 +696,13 @@ class CheckCaptures extends Recheck, SymTransformer:
             interpolateVarsIn(tree.tpt)
           curEnv = saved
 
+    override def recheckRHS(rhs: Tree, pt: Type)(using Context): Type =
+      def avoidMap = new TypeOps.AvoidMap:
+        def toAvoid(tp: NamedType) =
+          tp.isTerm && tp.symbol.owner == ctx.owner && !tp.symbol.is(Param)
+      val tp = recheck(rhs, pt)
+      if ctx.owner.is(Method) then avoidMap(tp) else tp
+
     /** If val or def definition with inferred (result) type is visible
      *  in other compilation units, check that the actual inferred type
      *  conforms to the expected type where all inferred capture sets are dropped.
@@ -812,7 +819,8 @@ class CheckCaptures extends Recheck, SymTransformer:
      *  Otherwise, if the result type is boxed, simulate an unboxing by
      *  adding all references in the boxed capture set to the current environment.
      */
-    override def recheck(tree: Tree, pt: Type = WildcardType)(using Context): Type =
+    override def recheck(tree: Tree, pt0: Type = WildcardType)(using Context): Type =
+      val pt = Existential.openExpected(pt0)
       val saved = curEnv
       tree match
         case _: RefTree | closureDef(_) if pt.isBoxedCapturing =>
@@ -878,23 +886,24 @@ class CheckCaptures extends Recheck, SymTransformer:
      *  where local capture roots are instantiated to root variables.
      */
     override def checkConformsExpr(actual: Type, expected: Type, tree: Tree, addenda: Addenda)(using Context): Type =
-      var expected1 = alignDependentFunction(expected, actual.stripCapturing)
-      val actualBoxed = adaptBoxed(actual, expected1, tree.srcPos)
+      val actualUnpacked = Existential.skolemize(actual)
+      var expected1 = alignDependentFunction(expected, actualUnpacked.stripCapturing)
+      val actualBoxed = adaptBoxed(actualUnpacked, expected1, tree.srcPos)
       //println(i"check conforms $actualBoxed <<< $expected1")
 
-      if actualBoxed eq actual then
+      if actualBoxed eq actualUnpacked then
         // Only `addOuterRefs` when there is no box adaptation
-        expected1 = addOuterRefs(expected1, actual)
+        expected1 = addOuterRefs(expected1, actualUnpacked)
       if isCompatible(actualBoxed, expected1) then
         if debugSuccesses then tree match
             case Ident(_) =>
-              println(i"SUCCESS $tree:\n${TypeComparer.explained(_.isSubType(actual, expected))}")
+              println(i"SUCCESS $tree:\n${TypeComparer.explained(_.isSubType(actualUnpacked, expected))}")
             case _ =>
         actualBoxed
       else
         capt.println(i"conforms failed for ${tree}: $actual vs $expected")
         err.typeMismatch(tree.withType(actualBoxed), expected1, addenda ++ CaptureSet.levelErrors)
-        actual
+        actualUnpacked
     end checkConformsExpr
 
     /** Turn `expected` into a dependent function when `actual` is dependent. */
@@ -1121,7 +1130,7 @@ class CheckCaptures extends Recheck, SymTransformer:
       /** If result derives from caps.Capability, yet is not a capturing type itself,
        *  make its capture set explicit.
        */
-      def makeCaptureSetExplicit(result: Type) = result match
+      def makeCaptureSetExplicit(actual: Type, result: Type) = result match
         case CapturingType(_, _) => result
         case _ =>
           if result.derivesFromCapability then
@@ -1147,16 +1156,17 @@ class CheckCaptures extends Recheck, SymTransformer:
               case _ =>
           case _ =>
         val adapted = adapt(actualw.withReachCaptures(actual), expected, covariant = true)
-        makeCaptureSetExplicit:
+        makeCaptureSetExplicit(actual,
           if adapted ne actualw then
             capt.println(i"adapt boxed $actual vs $expected ===> $adapted")
             adapted
           else
-            actual
+            actual)
     end adaptBoxed
 
     /** Check overrides again, taking capture sets into account.
     *  TODO: Can we avoid doing overrides checks twice?
+    *
     *  We need to do them here since only at this phase CaptureTypes are relevant
     *  But maybe we can then elide the check during the RefChecks phase under captureChecking?
     */
@@ -1167,12 +1177,12 @@ class CheckCaptures extends Recheck, SymTransformer:
         *  @param sym  symbol of the field definition that is being checked
         */
         override def checkSubType(actual: Type, expected: Type)(using Context): Boolean =
-          val expected1 = alignDependentFunction(addOuterRefs(expected, actual), actual.stripCapturing)
+          val expected1 = alignDependentFunction(addOuterRefs(Existential.strip(expected), actual), actual.stripCapturing)
           val actual1 =
             val saved = curEnv
             try
               curEnv = Env(clazz, EnvKind.NestedInOwner, capturedVars(clazz), outer0 = curEnv)
-              val adapted = adaptBoxed(actual, expected1, srcPos, alwaysConst = true)
+              val adapted = adaptBoxed(Existential.strip(actual), expected1, srcPos, alwaysConst = true)
               actual match
                 case _: MethodType =>
                   // We remove the capture set resulted from box adaptation for method types,
diff --git a/compiler/src/dotty/tools/dotc/cc/Existential.scala b/compiler/src/dotty/tools/dotc/cc/Existential.scala
index aefaa12ca6c7..81d53e7f0101 100644
--- a/compiler/src/dotty/tools/dotc/cc/Existential.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Existential.scala
@@ -9,6 +9,7 @@ import StdNames.nme
 import ast.tpd.*
 import Decorators.*
 import typer.ErrorReporting.errorType
+import NameKinds.exSkolemName
 
 /**
 
@@ -23,7 +24,7 @@ In adapt:
         method as owner, and use its termRef
     Then,
       + If the EX-bound variable appears only at toplevel, replace it with `x`
-      + Otherwise, replace it with a fresh reach capability `x*`.
+      + Otherwise, replace it with `x*`.
 
 In avoidance of a type T:
 
@@ -145,6 +146,21 @@ Existential source syntax:
     - The type of a type ascription in an expression or pattern
     - The argument and result types of a function.
 
+  Restrictions on Existential Types:
+
+    - An existential capture ref must be the only member of its set. This is
+      intended to model the idea that existential variables effectibely range
+      over capture sets, not capture references. But so far out calculus
+      and implementation does not yet acoommodate first-class capture sets.
+    - Existential capture refs must appear co-variantly in their bound type
+
+  So the following would all be illegal:
+
+      EX x.C^{x, io}            // error: multiple members
+      EX x.() => EX y.C^{x, y}  // error: multiple members
+      EX x.C^{x} ->{x} D        // error: contra-variant occurrence
+      EX x.Set[C^{x}]           // error: invariant occurrence
+
 Expansion of ^:
 
   We drop `cap` as a capture reference, but keep the unqualified `^` syntax.
@@ -188,6 +204,55 @@ Expansion of ^:
 */
 object Existential:
 
+  type Carrier = RefinedType
+
+  def openExpected(pt: Type)(using Context): Type = pt.dealias match
+    case Existential(boundVar, unpacked) =>
+      val tm = new IdempotentCaptRefMap:
+        val cvar = CaptureSet.Var(ctx.owner)
+        def apply(t: Type) = mapOver(t) match
+          case t @ CapturingType(parent, refs) if refs.elems.contains(boundVar) =>
+            assert(refs.isConst && refs.elems.size == 1, i"malformed existential $t")
+            t.derivedCapturingType(parent, cvar)
+          case t =>
+            t
+      openExpected(tm(unpacked))
+    case _ => pt
+
+  def strip(tp: Type)(using Context) = tp match
+    case Existential(_, tpunpacked) => tpunpacked
+    case _ => tp
+
+  def skolemize(tp: Type)(using Context) = tp.widenDealias match
+    case Existential(boundVar, unpacked) =>
+      val skolem = tp match
+        case tp: CaptureRef if tp.isTracked => tp
+        case _ => newSkolemSym(boundVar.underlying).termRef
+      val tm = new IdempotentCaptRefMap:
+        var deep = false
+        private inline def deepApply(t: Type): Type =
+          val saved = deep
+          deep = true
+          try apply(t) finally deep = saved
+        def apply(t: Type) =
+          if t eq boundVar then
+            if deep then skolem.reach else skolem
+          else t match
+            case defn.FunctionOf(args, res, contextual) =>
+              val res1 = deepApply(res)
+              if res1 ne res then defn.FunctionOf(args, res1, contextual)
+              else t
+            case defn.RefinedFunctionOf(mt) =>
+              mt.derivedLambdaType(resType = deepApply(mt.resType))
+            case _ =>
+              mapOver(t)
+      tm(unpacked)
+    case _ => tp
+  end skolemize
+
+  def newSkolemSym(tp: Type)(using Context): TermSymbol =
+    newSymbol(ctx.owner.enclosingMethodOrClass, exSkolemName.fresh(), Synthetic, tp)
+/*
   def fromDepFun(arg: Tree)(using Context): Type = arg.tpe match
     case RefinedType(parent, nme.apply, info: MethodType) if defn.isNonRefinedFunction(parent) =>
       info match
@@ -198,13 +263,7 @@ object Existential:
           errorType(em"Malformed existential: dependent function must have a singgle parameter of type caps.Capability", arg.srcPos)
     case _ =>
       errorType(em"Malformed existential: dependent function type expected", arg.srcPos)
-
-  def apply(fn: TermRef => Type)(using Context): RecType =
-    RecType(rt => fn(exBoundRef(rt)))
-
-  def exBoundRef(rt: RecType)(using Context): TermRef =
-    TermRef(rt.recThis, defn.captureRoot)
-
+*/
   private class PackMap(sym: Symbol, rt: RecType)(using Context) extends DeepTypeMap, IdempotentCaptRefMap:
     def apply(tp: Type): Type = tp match
       case ref: TermRef if ref.symbol == sym => TermRef(rt.recThis, defn.captureRoot)
@@ -235,7 +294,7 @@ object Existential:
     case (info: TypeRef) :: rest => info.symbol == defn.Caps_Exists && rest.isEmpty
     case _ => false
 
-  def unapply(tp: RefinedType)(using Context): Option[(TermParamRef, Type)] =
+  def unapply(tp: Carrier)(using Context): Option[(TermParamRef, Type)] =
     tp.refinedInfo match
       case mt: MethodType
       if isExistentialMethod(mt) && defn.isNonRefinedFunction(tp.parent) =>
diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala
index 0175d40c186c..fffc50ec809e 100644
--- a/compiler/src/dotty/tools/dotc/cc/Setup.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -237,6 +237,8 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
             val rinfo1 = apply(rinfo)
             if rinfo1 ne rinfo then rinfo1.toFunctionType(alwaysDependent = true)
             else tp
+          case Existential(_, unpacked) =>
+            apply(unpacked)
           case tp: MethodType =>
             tp.derivedLambdaType(
               paramInfos = mapNested(tp.paramInfos),
@@ -252,7 +254,10 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
       end apply
     end mapInferred
 
-    mapInferred(refine = true)(tp)
+    try mapInferred(refine = true)(tp)
+    catch case ex: AssertionError =>
+      println(i"error while maop inferred $tp")
+      throw ex
   end transformInferredType
 
   private def transformExplicitType(tp: Type, tptToCheck: Option[Tree] = None)(using Context): Type =
diff --git a/compiler/src/dotty/tools/dotc/core/NameKinds.scala b/compiler/src/dotty/tools/dotc/core/NameKinds.scala
index 74d440562824..49579aaf5d5b 100644
--- a/compiler/src/dotty/tools/dotc/core/NameKinds.scala
+++ b/compiler/src/dotty/tools/dotc/core/NameKinds.scala
@@ -332,6 +332,7 @@ object NameKinds {
   val InlineScrutineeName: UniqueNameKind    = new UniqueNameKind("$scrutinee")
   val InlineBinderName: UniqueNameKind       = new UniqueNameKind("$proxy")
   val MacroNames: UniqueNameKind             = new UniqueNameKind("$macro$")
+  val exSkolemName: UniqueNameKind           = new UniqueNameKind("$exSkolem")
 
   val UniqueExtMethName: UniqueNameKind = new UniqueNameKindWithUnmangle("$extension")
 
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index 7a5a92e836fd..1302e9aeb1da 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -3318,7 +3318,12 @@ object Types extends TypeUtils {
     private def badInst =
       throw new AssertionError(s"bad instantiation: $this")
 
-    def checkInst(using Context): this.type = this // debug hook
+    def checkInst(using Context): this.type =
+      if refinedName == nme.apply then
+        parent.dealias.stripAnnots match
+          case RefinedType(_, nme.apply, _) => assert(false, this) // debug hook
+          case _ =>
+      this
 
     final def derivedRefinedType
         (parent: Type = this.parent, refinedName: Name = this.refinedName, refinedInfo: Type = this.refinedInfo)
diff --git a/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala b/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala
index 0c6e36c8f18f..9852dfc1170d 100644
--- a/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala
@@ -564,7 +564,9 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
       case SingletonTypeTree(ref) =>
         toTextLocal(ref) ~ "." ~ keywordStr("type")
       case RefinedTypeTree(tpt, refines) =>
-        toTextLocal(tpt) ~ " " ~ blockText(refines)
+        if defn.isFunctionSymbol(tpt.symbol) && tree.hasType && !printDebug
+        then changePrec(GlobalPrec) { toText(tree.typeOpt) }
+        else toTextLocal(tpt) ~ blockText(refines)
       case AppliedTypeTree(tpt, args) =>
         if (tpt.symbol == defn.orType && args.length == 2)
           changePrec(OrTypePrec) { toText(args(0)) ~ " | " ~ atPrec(OrTypePrec + 1) { toText(args(1)) } }
diff --git a/compiler/src/dotty/tools/dotc/transform/Recheck.scala b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
index 79dfe3393578..7ef9beba9a96 100644
--- a/compiler/src/dotty/tools/dotc/transform/Recheck.scala
+++ b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
@@ -249,14 +249,16 @@ abstract class Recheck extends Phase, SymTransformer:
     def recheckValDef(tree: ValDef, sym: Symbol)(using Context): Type =
       val resType = recheck(tree.tpt)
       if tree.rhs.isEmpty then resType
-      else recheck(tree.rhs, resType)
+      else recheckRHS(tree.rhs, resType)
 
     def recheckDefDef(tree: DefDef, sym: Symbol)(using Context): Type =
       inContext(linkConstructorParams(sym).withOwner(sym)):
         val resType = recheck(tree.tpt)
         if tree.rhs.isEmpty || sym.isInlineMethod || sym.isEffectivelyErased
         then resType
-        else recheck(tree.rhs, resType)
+        else recheckRHS(tree.rhs, resType)
+
+    def recheckRHS(rhs: Tree, pt: Type)(using Context): Type = recheck(rhs, pt)
 
     def recheckTypeDef(tree: TypeDef, sym: Symbol)(using Context): Type =
       recheck(tree.rhs)
diff --git a/tests/neg/cc-existentials.scala b/tests/neg/cc-ex-conformance.scala
similarity index 61%
rename from tests/neg/cc-existentials.scala
rename to tests/neg/cc-ex-conformance.scala
index 27e434079fe0..63cb15bb8c74 100644
--- a/tests/neg/cc-existentials.scala
+++ b/tests/neg/cc-ex-conformance.scala
@@ -3,13 +3,13 @@ import caps.{Exists, Capability}
 
 class C
 
-type EX1 = (c: Exists) => (C^{c}, C^{c})
+type EX1 = () => (c: Exists) => (C^{c}, C^{c})
 
-type EX2 = (c1: Exists) => (c2: Exists) => (C^{c1}, C^{c2})
+type EX2 = () => (c1: Exists) => (c2: Exists) => (C^{c1}, C^{c2})
 
-type EX3 = (c: Exists) => () => C^{c}
+type EX3 = () => (c: Exists) => () => C^{c}
 
-type EX4 = () => (c: Exists) => C^{c}
+type EX4 = () => () => (c: Exists) => C^{c}
 
 def Test =
   val ex1: EX1 = ???
diff --git a/tests/pos/cc-ex-unpack.scala b/tests/pos/cc-ex-unpack.scala
new file mode 100644
index 000000000000..ae9b4ea5d805
--- /dev/null
+++ b/tests/pos/cc-ex-unpack.scala
@@ -0,0 +1,18 @@
+import language.experimental.captureChecking
+import caps.{Exists, Capability}
+
+class C
+
+type EX1 = (c: Exists) -> (C^{c}, C^{c})
+
+type EX2 = () -> (c1: Exists) -> (c2: Exists) -> (C^{c1}, C^{c2})
+
+type EX3 = () -> (c: Exists) -> () -> C^{c}
+
+type EX4 = () -> () -> (c: Exists) -> C^{c}
+
+def Test =
+  def f =
+    val ex1: EX1 = ???
+    val c1 = ex1
+    c1

From a17c6a9e651ef95bb9e1c0185730bc0b0d81c973 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Fri, 31 May 2024 22:55:29 +0200
Subject: [PATCH 14/14] More robust level handling

---
 .../src/dotty/tools/dotc/cc/CaptureOps.scala  | 49 +++++++++-
 .../src/dotty/tools/dotc/cc/CaptureSet.scala  | 57 +++++------
 .../dotty/tools/dotc/cc/CheckCaptures.scala   | 36 ++++---
 .../src/dotty/tools/dotc/cc/Existential.scala | 39 ++++----
 compiler/src/dotty/tools/dotc/cc/Setup.scala  | 96 +++++++++++--------
 .../tools/dotc/printing/PlainPrinter.scala    |  2 +-
 .../dotty/tools/dotc/transform/Recheck.scala  |  2 +-
 tests/neg-custom-args/captures/levels.check   |  2 +-
 .../neg-custom-args/captures/outer-var.check  |  2 +-
 tests/neg-custom-args/captures/reaches.check  |  2 +-
 tests/neg-custom-args/captures/vars.check     |  4 +-
 tests/printing/dependent-annot.check          |  7 +-
 12 files changed, 176 insertions(+), 122 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
index 8276a0987003..867c44818e3c 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
@@ -14,6 +14,7 @@ import tpd.*
 import StdNames.nme
 import config.Feature
 import collection.mutable
+import CCState.*
 
 private val Captures: Key[CaptureSet] = Key()
 
@@ -64,11 +65,47 @@ class CCState:
    */
   var levelError: Option[CaptureSet.CompareResult.LevelError] = None
 
+  private var curLevel: Level = outermostLevel
+  private val symLevel: mutable.Map[Symbol, Int] = mutable.Map()
+
+object CCState:
+
+  opaque type Level = Int
+
+  val undefinedLevel: Level = -1
+
+  val outermostLevel: Level = 0
+
+  /** The level of the current environment. Levels start at 0 and increase for
+   *  each nested function or class. -1 means the level is undefined.
+   */
+  def currentLevel(using Context): Level = ccState.curLevel
+
+  inline def inNestedLevel[T](inline op: T)(using Context): T =
+    val ccs = ccState
+    val saved = ccs.curLevel
+    ccs.curLevel = ccs.curLevel.nextInner
+    try op finally ccs.curLevel = saved
+
+  inline def inNestedLevelUnless[T](inline p: Boolean)(inline op: T)(using Context): T =
+    val ccs = ccState
+    val saved = ccs.curLevel
+    if !p then ccs.curLevel = ccs.curLevel.nextInner
+    try op finally ccs.curLevel = saved
+
+  extension (x: Level)
+    def isDefined: Boolean = x >= 0
+    def <= (y: Level) = (x: Int) <= y
+    def nextInner: Level = if isDefined then x + 1 else x
+
+  extension (sym: Symbol)(using Context)
+    def ccLevel: Level = ccState.symLevel.getOrElse(sym, -1)
+    def recordLevel() = ccState.symLevel(sym) = currentLevel
 end CCState
 
 /** The currently valid CCState */
 def ccState(using Context) =
-  Phases.checkCapturesPhase.asInstanceOf[CheckCaptures].ccState
+  Phases.checkCapturesPhase.asInstanceOf[CheckCaptures].ccState1
 
 class NoCommonRoot(rs: Symbol*)(using Context) extends Exception(
   i"No common capture root nested in ${rs.mkString(" and ")}"
@@ -339,6 +376,12 @@ extension (tp: Type)
       case _ =>
         tp
 
+  def level(using Context): Level =
+    tp match
+    case tp: TermRef => tp.symbol.ccLevel
+    case tp: ThisType => tp.cls.ccLevel.nextInner
+    case _ => undefinedLevel
+
 extension (cls: ClassSymbol)
 
   def pureBaseClass(using Context): Option[Symbol] =
@@ -423,9 +466,7 @@ extension (sym: Symbol)
     || sym.is(Method, butNot = Accessor)
 
   /** The owner of the current level. Qualifying owners are
-   *   - methods other than constructors and anonymous functions
-   *   - anonymous functions, provided they either define a local
-   *     root of type caps.Capability, or they are the rhs of a val definition.
+   *   - methods, other than accessors
    *   - classes, if they are not staticOwners
    *   - _root_
    */
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index a61a767eb873..a5ad8855bdc9 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -17,6 +17,7 @@ import typer.ErrorReporting.Addenda
 import TypeComparer.linkOK
 import util.common.alwaysTrue
 import scala.collection.mutable
+import CCState.*
 
 /** A class for capture sets. Capture sets can be constants or variables.
  *  Capture sets support inclusion constraints <:< where <:< is subcapturing.
@@ -56,10 +57,14 @@ sealed abstract class CaptureSet extends Showable:
    */
   def isAlwaysEmpty: Boolean
 
-  /** An optional level limit, or NoSymbol if none exists. All elements of the set
-   *  must be in scopes visible from the level limit.
+  /** An optional level limit, or undefinedLevel if none exists. All elements of the set
+   *  must be at levels equal or smaller than the level of the set, if it is defined.
    */
-  def levelLimit: Symbol
+  def level: Level
+
+  /** An optional owner, or NoSymbol if none exists. Used for diagnstics
+   */
+  def owner: Symbol
 
   /** Is this capture set definitely non-empty? */
   final def isNotEmpty: Boolean = !elems.isEmpty
@@ -242,9 +247,7 @@ sealed abstract class CaptureSet extends Showable:
     if this.subCaptures(that, frozen = true).isOK then that
     else if that.subCaptures(this, frozen = true).isOK then this
     else if this.isConst && that.isConst then Const(this.elems ++ that.elems)
-    else Var(
-        this.levelLimit.maxNested(that.levelLimit, onConflict = (sym1, sym2) => sym1),
-        this.elems ++ that.elems)
+    else Var(initialElems = this.elems ++ that.elems)
       .addAsDependentTo(this).addAsDependentTo(that)
 
   /** The smallest superset (via <:<) of this capture set that also contains `ref`.
@@ -414,7 +417,9 @@ object CaptureSet:
 
     def withDescription(description: String): Const = Const(elems, description)
 
-    def levelLimit = NoSymbol
+    def level = undefinedLevel
+
+    def owner = NoSymbol
 
     override def toString = elems.toString
   end Const
@@ -434,7 +439,7 @@ object CaptureSet:
   end Fluid
 
   /** The subclass of captureset variables with given initial elements */
-  class Var(directOwner: Symbol, initialElems: Refs = emptySet)(using @constructorOnly ictx: Context) extends CaptureSet:
+  class Var(override val owner: Symbol = NoSymbol, initialElems: Refs = emptySet, val level: Level = undefinedLevel, underBox: Boolean = false)(using @constructorOnly ictx: Context) extends CaptureSet:
 
     /** A unique identification number for diagnostics */
     val id =
@@ -443,9 +448,6 @@ object CaptureSet:
 
     //assert(id != 40)
 
-    override val levelLimit =
-      if directOwner.exists then directOwner.levelOwner else NoSymbol
-
     /** A variable is solved if it is aproximated to a from-then-on constant set. */
     private var isSolved: Boolean = false
 
@@ -519,12 +521,10 @@ object CaptureSet:
     private def levelOK(elem: CaptureRef)(using Context): Boolean =
       if elem.isRootCapability then !noUniversal
       else elem match
-        case elem: TermRef if levelLimit.exists =>
-          var sym = elem.symbol
-          if sym.isLevelOwner then sym = sym.owner
-          levelLimit.isContainedIn(sym.levelOwner)
-        case elem: ThisType if levelLimit.exists =>
-          levelLimit.isContainedIn(elem.cls.levelOwner)
+        case elem: TermRef if level.isDefined =>
+          elem.symbol.ccLevel <= level
+        case elem: ThisType if level.isDefined =>
+          elem.cls.ccLevel.nextInner <= level
         case ReachCapability(elem1) =>
           levelOK(elem1)
         case MaybeCapability(elem1) =>
@@ -602,8 +602,8 @@ object CaptureSet:
       val debugInfo =
         if !isConst && ctx.settings.YccDebug.value then ids else ""
       val limitInfo =
-        if ctx.settings.YprintLevel.value && levelLimit.exists
-        then i"<in $levelLimit>"
+        if ctx.settings.YprintLevel.value && level.isDefined
+        then i"<at level ${level.toString}>"
         else ""
       debugInfo ++ limitInfo
 
@@ -622,13 +622,6 @@ object CaptureSet:
     override def toString = s"Var$id$elems"
   end Var
 
-  /** Variables that represent refinements of class parameters can have the universal
-   *  capture set, since they represent only what is the result of the constructor.
-   *  Test case: Without that tweak, logger.scala would not compile.
-   */
-  class RefiningVar(directOwner: Symbol)(using Context) extends Var(directOwner):
-    override def disallowRootCapability(handler: () => Context ?=> Unit)(using Context) = this
-
   /** A variable that is derived from some other variable via a map or filter. */
   abstract class DerivedVar(owner: Symbol, initialElems: Refs)(using @constructorOnly ctx: Context)
   extends Var(owner, initialElems):
@@ -657,7 +650,7 @@ object CaptureSet:
    */
   class Mapped private[CaptureSet]
     (val source: Var, tm: TypeMap, variance: Int, initial: CaptureSet)(using @constructorOnly ctx: Context)
-  extends DerivedVar(source.levelLimit, initial.elems):
+  extends DerivedVar(source.owner, initial.elems):
     addAsDependentTo(initial)  // initial mappings could change by propagation
 
     private def mapIsIdempotent = tm.isInstanceOf[IdempotentCaptRefMap]
@@ -754,7 +747,7 @@ object CaptureSet:
    */
   final class BiMapped private[CaptureSet]
     (val source: Var, bimap: BiTypeMap, initialElems: Refs)(using @constructorOnly ctx: Context)
-  extends DerivedVar(source.levelLimit, initialElems):
+  extends DerivedVar(source.owner, initialElems):
 
     override def tryInclude(elem: CaptureRef, origin: CaptureSet)(using Context, VarState): CompareResult =
       if origin eq source then
@@ -788,7 +781,7 @@ object CaptureSet:
   /** A variable with elements given at any time as { x <- source.elems | p(x) } */
   class Filtered private[CaptureSet]
     (val source: Var, p: Context ?=> CaptureRef => Boolean)(using @constructorOnly ctx: Context)
-  extends DerivedVar(source.levelLimit, source.elems.filter(p)):
+  extends DerivedVar(source.owner, source.elems.filter(p)):
 
     override def tryInclude(elem: CaptureRef, origin: CaptureSet)(using Context, VarState): CompareResult =
       if accountsFor(elem) then
@@ -818,7 +811,7 @@ object CaptureSet:
   extends Filtered(source, !other.accountsFor(_))
 
   class Intersected(cs1: CaptureSet, cs2: CaptureSet)(using Context)
-  extends Var(cs1.levelLimit.minNested(cs2.levelLimit), elemIntersection(cs1, cs2)):
+  extends Var(initialElems = elemIntersection(cs1, cs2)):
     addAsDependentTo(cs1)
     addAsDependentTo(cs2)
     deps += cs1
@@ -908,7 +901,7 @@ object CaptureSet:
             if ctx.settings.YccDebug.value then printer.toText(trace, ", ")
             else blocking.show
           case LevelError(cs: CaptureSet, elem: CaptureRef) =>
-            Str(i"($elem at wrong level for $cs in ${cs.levelLimit})")
+            Str(i"($elem at wrong level for $cs at level ${cs.level.toString})")
 
     /** The result is OK */
     def isOK: Boolean = this == OK
@@ -1151,6 +1144,6 @@ object CaptureSet:
           i"""
             |
             |Note that reference ${ref}$levelStr
-            |cannot be included in outer capture set $cs which is associated with ${cs.levelLimit}"""
+            |cannot be included in outer capture set $cs"""
 
 end CaptureSet
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index da5a80d520d3..6381a0259b45 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -19,6 +19,7 @@ import transform.{Recheck, PreRecheck, CapturedVars}
 import Recheck.*
 import scala.collection.mutable
 import CaptureSet.{withCaptureSetsExplained, IdempotentCaptRefMap, CompareResult}
+import CCState.*
 import StdNames.nme
 import NameKinds.{DefaultGetterName, WildcardParamName, UniqueNameKind}
 import reporting.trace
@@ -191,7 +192,7 @@ class CheckCaptures extends Recheck, SymTransformer:
     if Feature.ccEnabled then
       super.run
 
-  val ccState = new CCState
+  val ccState1 = new CCState // Dotty problem: Rename to ccState ==> Crash in ExplicitOuter
 
   class CaptureChecker(ictx: Context) extends Rechecker(ictx):
 
@@ -311,7 +312,7 @@ class CheckCaptures extends Recheck, SymTransformer:
     def capturedVars(sym: Symbol)(using Context): CaptureSet =
       myCapturedVars.getOrElseUpdate(sym,
         if sym.ownersIterator.exists(_.isTerm)
-        then CaptureSet.Var(sym.owner)
+        then CaptureSet.Var(sym.owner, level = sym.ccLevel)
         else CaptureSet.empty)
 
     /** For all nested environments up to `limit` or a closed environment perform `op`,
@@ -585,6 +586,9 @@ class CheckCaptures extends Recheck, SymTransformer:
               tree.srcPos)
       super.recheckTypeApply(tree, pt)
 
+    override def recheckBlock(tree: Block, pt: Type)(using Context): Type =
+      inNestedLevel(super.recheckBlock(tree, pt))
+
     override def recheckClosure(tree: Closure, pt: Type, forceDependent: Boolean)(using Context): Type =
       val cs = capturedVars(tree.meth.symbol)
       capt.println(i"typing closure $tree with cvs $cs")
@@ -688,13 +692,14 @@ class CheckCaptures extends Recheck, SymTransformer:
         val localSet = capturedVars(sym)
         if !localSet.isAlwaysEmpty then
           curEnv = Env(sym, EnvKind.Regular, localSet, curEnv)
-        try checkInferredResult(super.recheckDefDef(tree, sym), tree)
-        finally
-          if !sym.isAnonymousFunction then
-            // Anonymous functions propagate their type to the enclosing environment
-            // so it is not in general sound to interpolate their types.
-            interpolateVarsIn(tree.tpt)
-          curEnv = saved
+        inNestedLevel:
+          try checkInferredResult(super.recheckDefDef(tree, sym), tree)
+          finally
+            if !sym.isAnonymousFunction then
+              // Anonymous functions propagate their type to the enclosing environment
+              // so it is not in general sound to interpolate their types.
+              interpolateVarsIn(tree.tpt)
+            curEnv = saved
 
     override def recheckRHS(rhs: Tree, pt: Type)(using Context): Type =
       def avoidMap = new TypeOps.AvoidMap:
@@ -771,7 +776,8 @@ class CheckCaptures extends Recheck, SymTransformer:
           checkSubset(thisSet,
             CaptureSet.empty.withDescription(i"of pure base class $pureBase"),
             selfType.srcPos, cs1description = " captured by this self type")
-        super.recheckClassDef(tree, impl, cls)
+        inNestedLevelUnless(cls.is(Module)):
+          super.recheckClassDef(tree, impl, cls)
       finally
         curEnv = saved
 
@@ -824,9 +830,9 @@ class CheckCaptures extends Recheck, SymTransformer:
       val saved = curEnv
       tree match
         case _: RefTree | closureDef(_) if pt.isBoxedCapturing =>
-          curEnv = Env(curEnv.owner, EnvKind.Boxed, CaptureSet.Var(curEnv.owner), curEnv)
+          curEnv = Env(curEnv.owner, EnvKind.Boxed, CaptureSet.Var(curEnv.owner, level = currentLevel), curEnv)
         case _ if tree.hasAttachment(ClosureBodyValue) =>
-          curEnv = Env(curEnv.owner, EnvKind.ClosureResult, CaptureSet.Var(curEnv.owner), curEnv)
+          curEnv = Env(curEnv.owner, EnvKind.ClosureResult, CaptureSet.Var(curEnv.owner, level = currentLevel), curEnv)
         case _ =>
       val res =
         try
@@ -990,7 +996,11 @@ class CheckCaptures extends Recheck, SymTransformer:
 
       inline def inNestedEnv[T](boxed: Boolean)(op: => T): T =
         val saved = curEnv
-        curEnv = Env(curEnv.owner, EnvKind.NestedInOwner, CaptureSet.Var(curEnv.owner), if boxed then null else curEnv)
+        curEnv = Env(
+          curEnv.owner,
+          EnvKind.NestedInOwner,
+          CaptureSet.Var(curEnv.owner, level = currentLevel),
+          if boxed then null else curEnv)
         try op
         finally curEnv = saved
 
diff --git a/compiler/src/dotty/tools/dotc/cc/Existential.scala b/compiler/src/dotty/tools/dotc/cc/Existential.scala
index 81d53e7f0101..1b37d2de39ba 100644
--- a/compiler/src/dotty/tools/dotc/cc/Existential.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Existential.scala
@@ -17,7 +17,7 @@ Handling existentials in CC:
 
 In adapt:
 
-  - If an EX is toplevel in expected type, replace with a fresh capture set variable
+  - If an EX is toplevel in expected type, replace with `cap`.
   - If an EX is toplevel in actual type, find a trackable replacement `x` as follows:
       + If actual type is a trackable ref, pick that
       + Otherwise, create a fresh skolem val symbol with currently enclosing
@@ -26,30 +26,31 @@ In adapt:
       + If the EX-bound variable appears only at toplevel, replace it with `x`
       + Otherwise, replace it with `x*`.
 
-In avoidance of a type T:
+Delayed packing:
 
-  - Replace all co-variant occurrences of locals variables in T (including locally
-    created EX-skolems) with single fresh EX-bound variable, which wraps T.
-  - Contravariant occurrences of local variables are approximated by the empty capture set,
-    as was the case before.
-  - Invariant occurrences of local variables produce errors, as was the case before.
-  - Check that no existentially quantified local variable appears under a box.
+ - When typing a `def` (including an anonymoys function), convert all covariant
+   toplevel `cap`s to a fresh existential variable wrapping the result type.
 
-The reason it is done this way is that it produces the smallest existential type
-wrt the existential type ordering shown below. For instance, consider the type
+Level checking and avoidance:
 
-      (A^{x}, B^{y})
+  - Environments, capture refs, and capture set variables carry levels
 
-where `x` and `y` are local. We widen to
+    + levels start at 0
+    + The level of a block or template statement sequence is one higher than the level of
+      its environment
+    + The level of a TermRef is the level of the environment where its symbol is defined.
+    + The level of a ThisType is the level of the statements of the class to which it beloongs.
+    + The level of a TermParamRef is currently -1 (i.e. TermParamRefs are not yet checked using this system)
+    + The level of a capture set variable is the level of the environment where it is created.
 
-      EX a.(A^{a}, B^{a})
+  - Variables also carry info whether they accept `cap` or not. Variables introduced under a box
+    don't, the others do.
 
-rather than
-
-      EX a.EX b.(A^{a}, A^{b})
-
-In the subtype ordering of existentials the first of these types is a subtype of
-the other, but not _vice versa_.
+  - Capture set variables do not accept elements of level higher than the variable's level
+  - We use avoidance to heal such cases: If the level-incorrect ref appears
+    + covariantly: widen to underlying capture set, reject if that is cap and the variable does not allow it
+    + contravariantly: narrow to {}
+    + invarianty: reject with error
 
 In cv-computation (markFree):
 
diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala
index fffc50ec809e..699499e5b41c 100644
--- a/compiler/src/dotty/tools/dotc/cc/Setup.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -16,6 +16,7 @@ import Synthetics.isExcluded
 import util.Property
 import printing.{Printer, Texts}, Texts.{Text, Str}
 import collection.mutable
+import CCState.*
 
 /** Operations accessed from CheckCaptures */
 trait SetupAPI:
@@ -189,7 +190,10 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
                   val getterType =
                     mapInferred(refine = false)(tp.memberInfo(getter)).strippedDealias
                   RefinedType(core, getter.name,
-                      CapturingType(getterType, CaptureSet.RefiningVar(ctx.owner)))
+                      CapturingType(getterType,
+                      new CaptureSet.Var(ctx.owner):
+                        override def disallowRootCapability(handler: () => Context ?=> Unit)(using Context) = this
+                      ))
                     .showing(i"add capture refinement $tp --> $result", capt)
                 else
                   core
@@ -407,14 +411,17 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
           if isExcluded(meth) then
             return
 
-          inContext(ctx.withOwner(meth)):
-            paramss.foreach(traverse)
-            transformResultType(tpt, meth)
-            traverse(tree.rhs)
-            //println(i"TYPE of ${tree.symbol.showLocated} = ${tpt.knownType}")
+          meth.recordLevel()
+          inNestedLevel:
+            inContext(ctx.withOwner(meth)):
+              paramss.foreach(traverse)
+              transformResultType(tpt, meth)
+              traverse(tree.rhs)
+              //println(i"TYPE of ${tree.symbol.showLocated} = ${tpt.knownType}")
 
         case tree @ ValDef(_, tpt: TypeTree, _) =>
           val sym = tree.symbol
+          sym.recordLevel()
           val defCtx = if sym.isOneOf(TermParamOrAccessor) then ctx else ctx.withOwner(sym)
           inContext(defCtx):
             transformResultType(tpt, sym)
@@ -431,13 +438,19 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
                 transformTT(arg, boxed = true, exact = false) // type arguments in type applications are boxed
 
         case tree: TypeDef if tree.symbol.isClass =>
-          inContext(ctx.withOwner(tree.symbol)):
-            traverseChildren(tree)
+          val sym = tree.symbol
+          sym.recordLevel()
+          inNestedLevelUnless(sym.is(Module)):
+            inContext(ctx.withOwner(sym))
+              traverseChildren(tree)
 
         case tree @ SeqLiteral(elems, tpt: TypeTree) =>
           traverse(elems)
           tpt.rememberType(box(transformInferredType(tpt.tpe)))
 
+        case tree: Block =>
+          inNestedLevel(traverseChildren(tree))
+
         case _ =>
           traverseChildren(tree)
       postProcess(tree)
@@ -536,36 +549,37 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
       case tree: TypeDef =>
         tree.symbol match
           case cls: ClassSymbol =>
-            val cinfo @ ClassInfo(prefix, _, ps, decls, selfInfo) = cls.classInfo
-            def innerModule = cls.is(ModuleClass) && !cls.isStatic
-            val selfInfo1 =
-              if (selfInfo ne NoType) && !innerModule then
-                // if selfInfo is explicitly given then use that one, except if
-                // self info applies to non-static modules, these still need to be inferred
-                selfInfo
-              else if cls.isPureClass then
-                // is cls is known to be pure, nothing needs to be added to self type
-                selfInfo
-              else if !cls.isEffectivelySealed && !cls.baseClassHasExplicitSelfType then
-                // assume {cap} for completely unconstrained self types of publicly extensible classes
-                CapturingType(cinfo.selfType, CaptureSet.universal)
-              else
-                // Infer the self type for the rest, which is all classes without explicit
-                // self types (to which we also add nested module classes), provided they are
-                // neither pure, nor are publicily extensible with an unconstrained self type.
-                CapturingType(cinfo.selfType, CaptureSet.Var(cls))
-            val ps1 = inContext(ctx.withOwner(cls)):
-              ps.mapConserve(transformExplicitType(_))
-            if (selfInfo1 ne selfInfo) || (ps1 ne ps) then
-              val newInfo = ClassInfo(prefix, cls, ps1, decls, selfInfo1)
-              updateInfo(cls, newInfo)
-              capt.println(i"update class info of $cls with parents $ps selfinfo $selfInfo to $newInfo")
-              cls.thisType.asInstanceOf[ThisType].invalidateCaches()
-              if cls.is(ModuleClass) then
-                // if it's a module, the capture set of the module reference is the capture set of the self type
-                val modul = cls.sourceModule
-                updateInfo(modul, CapturingType(modul.info, selfInfo1.asInstanceOf[Type].captureSet))
-                modul.termRef.invalidateCaches()
+            inNestedLevelUnless(cls.is(Module)):
+              val cinfo @ ClassInfo(prefix, _, ps, decls, selfInfo) = cls.classInfo
+              def innerModule = cls.is(ModuleClass) && !cls.isStatic
+              val selfInfo1 =
+                if (selfInfo ne NoType) && !innerModule then
+                  // if selfInfo is explicitly given then use that one, except if
+                  // self info applies to non-static modules, these still need to be inferred
+                  selfInfo
+                else if cls.isPureClass then
+                  // is cls is known to be pure, nothing needs to be added to self type
+                  selfInfo
+                else if !cls.isEffectivelySealed && !cls.baseClassHasExplicitSelfType then
+                  // assume {cap} for completely unconstrained self types of publicly extensible classes
+                  CapturingType(cinfo.selfType, CaptureSet.universal)
+                else
+                  // Infer the self type for the rest, which is all classes without explicit
+                  // self types (to which we also add nested module classes), provided they are
+                  // neither pure, nor are publicily extensible with an unconstrained self type.
+                  CapturingType(cinfo.selfType, CaptureSet.Var(cls, level = currentLevel))
+              val ps1 = inContext(ctx.withOwner(cls)):
+                ps.mapConserve(transformExplicitType(_))
+              if (selfInfo1 ne selfInfo) || (ps1 ne ps) then
+                val newInfo = ClassInfo(prefix, cls, ps1, decls, selfInfo1)
+                updateInfo(cls, newInfo)
+                capt.println(i"update class info of $cls with parents $ps selfinfo $selfInfo to $newInfo")
+                cls.thisType.asInstanceOf[ThisType].invalidateCaches()
+                if cls.is(ModuleClass) then
+                  // if it's a module, the capture set of the module reference is the capture set of the self type
+                  val modul = cls.sourceModule
+                  updateInfo(modul, CapturingType(modul.info, selfInfo1.asInstanceOf[Type].captureSet))
+                  modul.termRef.invalidateCaches()
           case _ =>
       case _ =>
     end postProcess
@@ -677,11 +691,11 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
   /** Add a capture set variable to `tp` if necessary, or maybe pull out
    *  an embedded capture set variable from a part of `tp`.
    */
-  def addVar(tp: Type, owner: Symbol)(using Context): Type =
+  private def addVar(tp: Type, owner: Symbol)(using Context): Type =
     decorate(tp,
       addedSet = _.dealias.match
-        case CapturingType(_, refs) => CaptureSet.Var(owner, refs.elems)
-        case _ => CaptureSet.Var(owner))
+        case CapturingType(_, refs) => CaptureSet.Var(owner, refs.elems, level = currentLevel)
+        case _ => CaptureSet.Var(owner, level = currentLevel))
 
   def setupUnit(tree: Tree, recheckDef: DefRecheck)(using Context): Unit =
     setupTraverser(recheckDef).traverse(tree)(using ctx.withPhase(thisPhase))
diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
index c06b43cafe17..71ebb7054000 100644
--- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
@@ -15,7 +15,7 @@ import util.SourcePosition
 import scala.util.control.NonFatal
 import scala.annotation.switch
 import config.{Config, Feature}
-import cc.{CapturingType, RetainingType, CaptureSet, ReachCapability, MaybeCapability, isBoxed, levelOwner, retainedElems, isRetainsLike}
+import cc.{CapturingType, RetainingType, CaptureSet, ReachCapability, MaybeCapability, isBoxed, retainedElems, isRetainsLike}
 
 class PlainPrinter(_ctx: Context) extends Printer {
 
diff --git a/compiler/src/dotty/tools/dotc/transform/Recheck.scala b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
index 7ef9beba9a96..fd3ed913d2aa 100644
--- a/compiler/src/dotty/tools/dotc/transform/Recheck.scala
+++ b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
@@ -266,7 +266,7 @@ abstract class Recheck extends Phase, SymTransformer:
 
     def recheckClassDef(tree: TypeDef, impl: Template, sym: ClassSymbol)(using Context): Type =
       recheck(impl.constr)
-      impl.parentsOrDerived.foreach(recheck(_))
+      impl.parents.foreach(recheck(_))
       recheck(impl.self)
       recheckStats(impl.body)
       sym.typeRef
diff --git a/tests/neg-custom-args/captures/levels.check b/tests/neg-custom-args/captures/levels.check
index a5f8d73ccf7a..479a231a0404 100644
--- a/tests/neg-custom-args/captures/levels.check
+++ b/tests/neg-custom-args/captures/levels.check
@@ -12,6 +12,6 @@
    |           Required: box (x$0: String) ->? String
    |
    |           Note that reference (cap3 : CC^), defined in method scope
-   |           cannot be included in outer capture set ? of value r which is associated with method test2
+   |           cannot be included in outer capture set ? of value r
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/outer-var.check b/tests/neg-custom-args/captures/outer-var.check
index b9f1f57be769..d57d615cda64 100644
--- a/tests/neg-custom-args/captures/outer-var.check
+++ b/tests/neg-custom-args/captures/outer-var.check
@@ -32,7 +32,7 @@
    |        Required: () ->{p} Unit
    |
    |        Note that reference (q : Proc), defined in method inner
-   |        cannot be included in outer capture set {p} of variable y which is associated with method test
+   |        cannot be included in outer capture set {p} of variable y
    |
    | longer explanation available when compiling with `-explain`
 -- Error: tests/neg-custom-args/captures/outer-var.scala:16:53 ---------------------------------------------------------
diff --git a/tests/neg-custom-args/captures/reaches.check b/tests/neg-custom-args/captures/reaches.check
index a1c5a56369e9..ccd9e891380b 100644
--- a/tests/neg-custom-args/captures/reaches.check
+++ b/tests/neg-custom-args/captures/reaches.check
@@ -12,7 +12,7 @@
    |       Required: box List[box () ->{xs*} Unit]^?
    |
    |       Note that reference (f : File^), defined in method $anonfun
-   |       cannot be included in outer capture set {xs*} of value cur which is associated with method runAll1
+   |       cannot be included in outer capture set {xs*} of value cur
    |
    | longer explanation available when compiling with `-explain`
 -- Error: tests/neg-custom-args/captures/reaches.scala:35:6 ------------------------------------------------------------
diff --git a/tests/neg-custom-args/captures/vars.check b/tests/neg-custom-args/captures/vars.check
index 22d13d8e26e7..e2d817f2d8bd 100644
--- a/tests/neg-custom-args/captures/vars.check
+++ b/tests/neg-custom-args/captures/vars.check
@@ -4,7 +4,7 @@
    |             reference (cap3 : Cap) is not included in the allowed capture set {cap1} of variable a
    |
    |             Note that reference (cap3 : Cap), defined in method scope
-   |             cannot be included in outer capture set {cap1} of variable a which is associated with method test
+   |             cannot be included in outer capture set {cap1} of variable a
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/vars.scala:23:8 ------------------------------------------
 23 |    a = g      // error
    |        ^
@@ -12,7 +12,7 @@
    |        Required: (x$0: String) ->{cap1} String
    |
    |        Note that reference (cap3 : Cap), defined in method scope
-   |        cannot be included in outer capture set {cap1} of variable a which is associated with method test
+   |        cannot be included in outer capture set {cap1} of variable a
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/vars.scala:25:12 -----------------------------------------
diff --git a/tests/printing/dependent-annot.check b/tests/printing/dependent-annot.check
index a8a7e8b0bfee..f2dd0f702884 100644
--- a/tests/printing/dependent-annot.check
+++ b/tests/printing/dependent-annot.check
@@ -11,12 +11,7 @@ package <empty> {
     def f(y: C, z: C): Unit =
       {
         def g(): C @ann([y,z : Any]*) = ???
-        val ac:
-          (C => Array[String])
-            {
-              def apply(x: C): Array[String @ann([x : Any]*)]
-            }
-         = ???
+        val ac: (x: C) => Array[String @ann([x : Any]*)] = ???
         val dc: Array[String] = ac.apply(g())
         ()
       }