Correct rules for CapSet; update definition for Contains; fix tests

Author: noti0na1

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

@@ -100,7 +100,8 @@ trait CaptureRef extends TypeProxy, ValueType:
    *   x: x1.type /\ x1 subsumes y  ==>  x subsumes y
    *   TODO: Document path cases
    */
-  final def subsumes(y: CaptureRef)(using Context): Boolean =
+  // import reporting.trace
+  final def subsumes(y: CaptureRef)(using Context): Boolean = // trace.force(i"subsumes $this, $y"):
 
     def subsumingRefs(x: Type, y: Type): Boolean = x match
       case x: CaptureRef => y match
@@ -135,14 +136,28 @@ trait CaptureRef extends TypeProxy, ValueType:
               case _ => false
           || viaInfo(y.info)(subsumingRefs(this, _))
         case MaybeCapability(y1) => this.stripMaybe.subsumes(y1)
+        case y: TypeRef if y.symbol.info.derivesFrom(defn.Caps_CapSet) =>
+          y.info match
+            case _: TypeAlias => y.captureSetOfInfo.elems.forall(this.subsumes)
+            case TypeBounds(_, hi: CaptureRef) => this.subsumes(hi)
+            case _ => y.captureSetOfInfo.elems.forall(this.subsumes)
         case _ => false
     || this.match
         case ReachCapability(x1) => x1.subsumes(y.stripReach)
         case x: TermRef => viaInfo(x.info)(subsumingRefs(_, y))
         case x: TermParamRef => subsumesExistentially(x, y)
-        case x: TypeRef if x.symbol.info.derivesFrom(defn.Caps_CapSet) =>
-          x.captureSetOfInfo.elems.exists(_.subsumes(y))
-        case x: TypeRef => assumedContainsOf(x).contains(y)
+        case x: TypeRef if assumedContainsOf(x).contains(y) => true
+        case x: TypeRef if x.derivesFrom(defn.Caps_CapSet) =>
+          x.info match
+            case _: TypeAlias =>
+              x.captureSetOfInfo.elems.exists(_.subsumes(y))
+            case TypeBounds(lo: CaptureRef, _) =>
+              lo.subsumes(y)
+            case _ =>
+              x.captureSetOfInfo.elems.exists(_.subsumes(y))
+        case AnnotatedType(parent, ann)
+        if ann.symbol.isRetains && parent.derivesFrom(defn.Caps_CapSet) =>
+          ann.tree.toCaptureSet.elems.exists(_.subsumes(y))
         case _ => false
   end subsumes
 

library/src/scala/caps.scala

@@ -22,12 +22,12 @@ import annotation.{experimental, compileTimeOnly, retainsCap}
   /** A type constraint expressing that the capture set `C` needs to contain
    *  the capability `R`
    */
-  sealed trait Contains[C <: CapSet @retainsCap, R <: Singleton]
+  sealed trait Contains[+C >: CapSet <: CapSet @retainsCap, R <: Singleton]
 
   /** The only implementation of `Contains`. The constraint that `{R} <: C` is
    *  added separately by the capture checker.
    */
-  given containsImpl[C <: CapSet @retainsCap, R <: Singleton]: Contains[C, R]()
+  given containsImpl[C >: CapSet <: CapSet @retainsCap, R <: Singleton]: Contains[C, R]()
 
   /** A wrapper indicating a type variable in a capture argument list of a
    *  @retains annotation. E.g. `^{x, Y^}` is represented as `@retains(x, capsOf[Y])`.

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/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/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