Refine rules for capture parameters and members

compiler/src/dotty/tools/dotc/ast/untpd.scala

@@ -527,10 +527,14 @@ object untpd extends Trees.Instance[Untyped] with UntypedTreeInfo {
   def makeCapsOf(tp: RefTree)(using Context): Tree =
     TypeApply(Select(scalaDot(nme.caps), nme.capsOf), tp :: Nil)
 
-  def makeCapsBound()(using Context): Tree =
-    makeRetaining(
+  // `type C^` and `[C^]` becomes:
+  // `type C >: CapSet <: CapSet^{cap}` and `[C >: CapSet <: CapSet^{cap}]`
+  def makeCapsBound()(using Context): TypeBoundsTree =
+    TypeBoundsTree(
       Select(scalaDot(nme.caps), tpnme.CapSet),
-      Nil, tpnme.retainsCap)
+      makeRetaining(
+        Select(scalaDot(nme.caps), tpnme.CapSet),
+        Nil, tpnme.retainsCap))
 
   def makeConstructor(tparams: List[TypeDef], vparamss: List[List[ValDef]], rhs: Tree = EmptyTree)(using Context): DefDef =
     DefDef(nme.CONSTRUCTOR, joinParams(tparams, vparamss), TypeTree(), rhs)

compiler/src/dotty/tools/dotc/cc/CaptureRef.scala

@@ -93,12 +93,19 @@ trait CaptureRef extends TypeProxy, ValueType:
   final def invalidateCaches() =
     myCaptureSetRunId = NoRunId
 
-  /** x subsumes x
-   *   this subsumes this.f
+  /**  x subsumes x
+   *   x subsumes x.f
+   *   x =:= y ==> x subsumes y
    *   x subsumes y  ==>  x* subsumes y, x subsumes y?
    *   x subsumes y  ==>  x* subsumes y*, x? subsumes y?
    *   x: x1.type /\ x1 subsumes y  ==>  x subsumes y
-   *   TODO: Document path cases
+   *   X = CapSet^cx, exists rx in cx, rx subsumes y ==>  X subsumes y
+   *   Y = CapSet^cy, forall ry in cy, x subsumes ry ==>  x subsumes Y
+   *   X: CapSet^c1...CapSet^c2, (CapSet^c1) subsumes y  ==> X subsumes y
+   *   Y: CapSet^c1...CapSet^c2, x subsumes (CapSet^c2) ==> x subsumes Y
+   *   Contains[X, y]  ==>  X subsumes y
+   *
+   *   TODO: Document cases with more comments.
    */
   final def subsumes(y: CaptureRef)(using Context): Boolean =
 
@@ -135,14 +142,28 @@ trait CaptureRef extends TypeProxy, ValueType:
               case _ => false
           || viaInfo(y.info)(subsumingRefs(this, _))
         case MaybeCapability(y1) => this.stripMaybe.subsumes(y1)
+        case y: TypeRef if y.derivesFrom(defn.Caps_CapSet) =>
+          y.info match
+            case TypeBounds(_, hi: CaptureRef) => this.subsumes(hi)
+            case _ => y.captureSetOfInfo.elems.forall(this.subsumes)
+        case AnnotatedType(parent, ann)
+        if ann.symbol.isRetains && parent.derivesFrom(defn.Caps_CapSet) =>
+          ann.tree.toCaptureSet.elems.forall(this.subsumes)
         case _ => false
     || this.match
         case ReachCapability(x1) => x1.subsumes(y.stripReach)
         case x: TermRef => viaInfo(x.info)(subsumingRefs(_, y))
         case x: TermParamRef => subsumesExistentially(x, y)
-        case x: TypeRef if x.symbol.info.derivesFrom(defn.Caps_CapSet) =>
-          x.captureSetOfInfo.elems.exists(_.subsumes(y))
-        case x: TypeRef => assumedContainsOf(x).contains(y)
+        case x: TypeRef if assumedContainsOf(x).contains(y) => true
+        case x: TypeRef if x.derivesFrom(defn.Caps_CapSet) =>
+          x.info match
+            case TypeBounds(lo: CaptureRef, _) =>
+              lo.subsumes(y)
+            case _ =>
+              x.captureSetOfInfo.elems.exists(_.subsumes(y))
+        case AnnotatedType(parent, ann)
+        if ann.symbol.isRetains && parent.derivesFrom(defn.Caps_CapSet) =>
+          ann.tree.toCaptureSet.elems.exists(_.subsumes(y))
         case _ => false
   end subsumes
 

compiler/src/dotty/tools/dotc/cc/CaptureSet.scala

@@ -161,7 +161,9 @@ sealed abstract class CaptureSet extends Showable:
     def debugInfo(using Context) = i"$this accountsFor $x, which has capture set ${x.captureSetOfInfo}"
     def test(using Context) = reporting.trace(debugInfo):
       elems.exists(_.subsumes(x))
-      || !x.isMaxCapability && x.captureSetOfInfo.subCaptures(this, frozen = true).isOK
+      || !x.isMaxCapability
+        && !x.derivesFrom(defn.Caps_CapSet)
+        && x.captureSetOfInfo.subCaptures(this, frozen = true).isOK
     comparer match
       case comparer: ExplainingTypeComparer => comparer.traceIndented(debugInfo)(test)
       case _ => test

compiler/src/dotty/tools/dotc/cc/Setup.scala

@@ -117,6 +117,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
    *  The info of these symbols is made fluid.
    */
   def isPreCC(sym: Symbol)(using Context): Boolean =
+    // TODO: check type members as well
     sym.isTerm && sym.maybeOwner.isClass
     && !sym.is(Module)
     && !sym.owner.is(CaptureChecked)
@@ -866,7 +867,9 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
           if others.accountsFor(ref) then
             report.warning(em"redundant capture: $dom already accounts for $ref", pos)
 
-        if ref.captureSetOfInfo.elems.isEmpty && !ref.derivesFrom(defn.Caps_Capability) then
+        if ref.captureSetOfInfo.elems.isEmpty
+            && !ref.derivesFrom(defn.Caps_Capability)
+            && !ref.derivesFrom(defn.Caps_CapSet) then
           val deepStr = if ref.isReach then " deep" else ""
           report.error(em"$ref cannot be tracked since its$deepStr capture set is empty", pos)
         check(parent.captureSet, parent)

compiler/src/dotty/tools/dotc/parsing/Parsers.scala

@@ -2240,7 +2240,7 @@ object Parsers {
       atSpan(in.offset):
         if in.isIdent(nme.UPARROW) && Feature.ccEnabled then
           in.nextToken()
-          TypeBoundsTree(EmptyTree, makeCapsBound())
+          makeCapsBound()
         else
           TypeBoundsTree(bound(SUPERTYPE), bound(SUBTYPE))
 
@@ -4057,8 +4057,11 @@ object Parsers {
               || sourceVersion.isAtLeast(`3.6`) && in.isColon =>
             makeTypeDef(typeAndCtxBounds(tname))
           case _ =>
-            syntaxErrorOrIncomplete(ExpectedTypeBoundOrEquals(in.token))
-            return EmptyTree // return to avoid setting the span to EmptyTree
+            if in.isIdent(nme.UPARROW) && Feature.ccEnabled then
+              makeTypeDef(typeAndCtxBounds(tname))
+            else
+              syntaxErrorOrIncomplete(ExpectedTypeBoundOrEquals(in.token))
+              return EmptyTree // return to avoid setting the span to EmptyTree
         }
       }
     }

library/src/scala/caps.scala

@@ -22,18 +22,18 @@ import annotation.{experimental, compileTimeOnly, retainsCap}
   /** A type constraint expressing that the capture set `C` needs to contain
    *  the capability `R`
    */
-  sealed trait Contains[C <: CapSet @retainsCap, R <: Singleton]
+  sealed trait Contains[+C >: CapSet <: CapSet @retainsCap, R <: Singleton]
 
   /** The only implementation of `Contains`. The constraint that `{R} <: C` is
    *  added separately by the capture checker.
    */
-  given containsImpl[C <: CapSet @retainsCap, R <: Singleton]: Contains[C, R]()
+  given containsImpl[C >: CapSet <: CapSet @retainsCap, R <: Singleton]: Contains[C, R]()
 
   /** A wrapper indicating a type variable in a capture argument list of a
    *  @retains annotation. E.g. `^{x, Y^}` is represented as `@retains(x, capsOf[Y])`.
    */
   @compileTimeOnly("Should be be used only internally by the Scala compiler")
-  def capsOf[CS]: Any = ???
+  def capsOf[CS >: CapSet <: CapSet @retainsCap]: Any = ???
 
   /** Reach capabilities x* which appear as terms in @retains annotations are encoded
    *  as `caps.reachCapability(x)`. When converted to CaptureRef types in capture sets

tests/neg-custom-args/captures/capset-bound2.scala

@@ -0,0 +1,13 @@
+import caps.*
+
+class IO
+
+def f[C^](io: IO^{C^}) = ???
+
+def test =
+  f[CapSet](???)
+  f[CapSet^{}](???)
+  f[CapSet^](???)
+  f[Nothing](???) // error
+  f[String](???) // error
+

tests/neg-custom-args/captures/capset-members.scala

@@ -0,0 +1,25 @@
+import caps.*
+
+trait Abstract[X^]:
+  type C >: X <: CapSet^
+  def boom(): Unit^{C^}
+
+class Concrete extends Abstract[CapSet^{}]:
+  type C = CapSet^{}
+  def boom() = ()
+
+class Concrete2 extends Abstract[CapSet^{}]:
+  type C = CapSet^{} & CapSet^{}
+  def boom() = ()
+
+class Concrete3 extends Abstract[CapSet^{}]:
+  type C = CapSet^{} | CapSet^{}
+  def boom() = ()
+
+class Concrete4(a: AnyRef^) extends Abstract[CapSet^{a}]:
+  type C = CapSet // error
+  def boom() = ()
+
+class Concrete5(a: AnyRef^) extends Abstract[CapSet^{a}]:
+  type C = CapSet^{} | CapSet^{a}
+  def boom() = ()

tests/neg-custom-args/captures/capture-parameters.scala

@@ -0,0 +1,9 @@
+import caps.*
+
+class C
+
+def test[X^, Y^, Z >: X <: Y](x: C^{X^}, y: C^{Y^}, z: C^{Z^}) =
+  val x2z: C^{Z^} = x
+  val z2y: C^{Y^} = z
+  val x2y: C^{Y^} = x // error
+

tests/neg-custom-args/captures/capture-poly.scala

@@ -3,7 +3,7 @@ import caps.*
 trait Foo extends Capability
 
 trait CaptureSet:
-  type C <: CapSet^
+  type C^
 
 def capturePoly[C^](a: Foo^{C^}): Foo^{C^} = a
 def capturePoly2(c: CaptureSet)(a: Foo^{c.C^}): Foo^{c.C^} = a

tests/neg-custom-args/captures/i21868.scala

@@ -1,14 +1,13 @@
 import caps.*
 
 trait AbstractWrong:
-    type C <: CapSet
-    def boom(): Unit^{C^} // error
+  type C <: CapSet
+  def f(): Unit^{C^} // error
 
-trait Abstract:
-    type C <: CapSet^
-    def boom(): Unit^{C^}
-
-class Concrete extends Abstract:
-    type C = Nothing
-    def boom() = () // error
+trait Abstract1:
+  type C^
+  def f(): Unit^{C^}
 
+class Abstract2:
+  type C >: CapSet <: CapSet^
+  def f(): Unit^{C^}

tests/neg-custom-args/captures/i21868b.scala

@@ -0,0 +1,46 @@
+import language.experimental.modularity
+import caps.*
+
+class IO
+
+class File
+
+trait Abstract:
+  type C >: CapSet <: CapSet^
+  def f(file: File^{C^}): Unit
+
+class Concrete1 extends Abstract:
+  type C = CapSet
+  def f(file: File) = ()
+
+class Concrete2(io: IO^) extends Abstract:
+  type C = CapSet^{io}
+  def f(file: File^{io}) = ()
+
+class Concrete3(io: IO^) extends Abstract:
+  type C = CapSet^{io}
+  def f(file: File) = () // error
+
+trait Abstract2(tracked val io: IO^):
+  type C >: CapSet <: CapSet^{io}
+  def f(file: File^{C^}): Unit
+
+class Concrete4(io: IO^) extends Abstract2(io):
+  type C = CapSet
+  def f(file: File) = ()
+
+class Concrete5(io1: IO^, io2: IO^) extends Abstract2(io1):
+  type C = CapSet^{io2} // error
+  def f(file: File^{io2}) = ()
+
+trait Abstract3[X^]:
+  type C >: CapSet <: X
+  def f(file: File^{C^}): Unit
+
+class Concrete6(io: IO^) extends Abstract3[CapSet^{io}]:
+  type C = CapSet
+  def f(file: File) = ()
+
+class Concrete7(io1: IO^, io2: IO^) extends Abstract3[CapSet^{io1}]:
+  type C = CapSet^{io2} // error
+  def f(file: File^{io2}) = ()

tests/neg-custom-args/captures/i22005.scala

@@ -0,0 +1,8 @@
+import caps.*
+
+class IO
+class File(io: IO^)
+
+class Handler[C^]:
+  def f(file: File^): File^{C^} = file // error
+  def g(file: File^{C^}): File^ = file // ok

tests/neg-custom-args/captures/use-capset.check

@@ -1,19 +1,19 @@
--- Error: tests/neg-custom-args/captures/use-capset.scala:7:50 ---------------------------------------------------------
-7 |private def g[C^] = (xs: List[Object^{C^}]) => xs.head // error
+-- Error: tests/neg-custom-args/captures/use-capset.scala:5:50 ---------------------------------------------------------
+5 |private def g[C^] = (xs: List[Object^{C^}]) => xs.head // error
   |                                               ^^^^^^^
   |                                               Capture set parameter C leaks into capture scope of method g.
   |                                               To allow this, the type C should be declared with a @use annotation
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:13:22 -----------------------------------
-13 |  val _: () -> Unit = h // error: should be ->{io}
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:11:22 -----------------------------------
+11 |  val _: () -> Unit = h // error: should be ->{io}
    |                      ^
    |                      Found:    (h : () ->{io} Unit)
    |                      Required: () -> Unit
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:15:50 -----------------------------------
-15 |  val _: () -> List[Object^{io}] -> Object^{io} = h2 // error, should be ->{io}
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:13:50 -----------------------------------
+13 |  val _: () -> List[Object^{io}] -> Object^{io} = h2 // error, should be ->{io}
    |                                                  ^^
-   |                                          Found:    (h2 : () ->? (x$0: List[box Object^]^{}) ->{io} Object^{io})
-   |                                          Required: () -> List[box Object^{io}] -> Object^{io}
+   |                                      Found:    (h2 : () ->? (x$0: List[box Object^{io}]^{}) ->{io} Object^{io})
+   |                                      Required: () -> List[box Object^{io}] -> Object^{io}
    |
    | longer explanation available when compiling with `-explain`

tests/neg-custom-args/captures/use-capset.scala

@@ -1,7 +1,5 @@
 import caps.{use, CapSet}
 
-
-
 def f[C^](@use xs: List[Object^{C^}]): Unit = ???
 
 private def g[C^] = (xs: List[Object^{C^}]) => xs.head // error

tests/neg/cc-poly-2.check

@@ -1,10 +1,3 @@
--- [E007] Type Mismatch Error: tests/neg/cc-poly-2.scala:13:15 ---------------------------------------------------------
-13 |    f[Nothing](d) // error
-   |               ^
-   |               Found:    (d : Test.D^)
-   |               Required: Test.D
-   |
-   | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg/cc-poly-2.scala:14:19 ---------------------------------------------------------
 14 |    f[CapSet^{c1}](d) // error
    |                   ^

tests/neg/cc-poly-2.scala

@@ -10,7 +10,7 @@ object Test:
 
   def test(c1: C, c2: C) =
     val d: D^ = D()
-    f[Nothing](d) // error
+    // f[Nothing](d) // already rule out at typer
     f[CapSet^{c1}](d) // error
     val x = f(d)
     val _: D^{c1} = x // error

tests/pos-custom-args/captures/cc-poly-varargs.scala

@@ -1,20 +1,19 @@
-trait Cancellable
+abstract class Source[+T, Cap^]:
+  def transformValuesWith[U](f: (T -> U)^{Cap^}): Source[U, Cap]^{this, f} = ???
 
-abstract class Source[+T, Cap^]
-
-extension[T, Cap^](src: Source[T, Cap]^)
-  def transformValuesWith[U](f: (T -> U)^{Cap^}): Source[U, Cap]^{src, f} = ???
+// TODO: The extension version of `transformValuesWith` doesn't work currently.
+// extension[T, Cap^](src: Source[T, Cap]^)
+//   def transformValuesWith[U](f: (T -> U)^{Cap^}): Source[U, Cap]^{src, f} = ???
 
 def race[T, Cap^](sources: Source[T, Cap]^{Cap^}*): Source[T, Cap]^{Cap^} = ???
 
-def either[T1, T2, Cap^](src1: Source[T1, Cap]^{Cap^}, src2: Source[T2, Cap]^{Cap^}): Source[Either[T1, T2], Cap]^{Cap^} =
+def either[T1, T2, Cap^](
+    src1: Source[T1, Cap]^{Cap^},
+    src2: Source[T2, Cap]^{Cap^}): Source[Either[T1, T2], Cap]^{Cap^} =
   val left = src1.transformValuesWith(Left(_))
   val right = src2.transformValuesWith(Right(_))
-  race(left, right)
-
-
-
-
-
-
-
+  race[Either[T1, T2], Cap](left, right)
+  // Explcit type arguments are required here because the second argument
+  // is inferred as `CapSet^{Cap^}` instead of `Cap`.
+  // Although `CapSet^{Cap^}` subsums `Cap` in terms of capture set,
+  // `Cap` is not a subtype of `CapSet^{Cap^}` in terms of subtyping.

tests/pos/cc-poly-source-capability.scala

@@ -20,13 +20,14 @@ import caps.use
 
   def test1(async1: Async, @use others: List[Async]) =
     val src = Source[CapSet^{async1, others*}]
+    val _: Set[Listener^{async1, others*}] = src.allListeners
     val lst1 = listener(async1)
     val lsts = others.map(listener)
     val _: List[Listener^{others*}] = lsts
     src.register{lst1}
     src.register(listener(async1))
-    lsts.foreach(src.register)
-    others.map(listener).foreach(src.register)
+    lsts.foreach(src.register(_)) // TODO: why we need to use _ explicitly here?
+    others.map(listener).foreach(src.register(_))
     val ls = src.allListeners
     val _: Set[Listener^{async1, others*}] = ls