Refine subsumes rule; fix test

scala · Nov 26, 2024 · 4abda8b · 4abda8b
1 parent a8c624e
commit 4abda8b
Show file tree

Hide file tree

Showing 2 changed files with 28 additions and 17 deletions.
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
@@ -93,15 +93,21 @@ trait CaptureRef extends TypeProxy, ValueType:
   final def invalidateCaches() =
     myCaptureSetRunId = NoRunId
 
-  /** x subsumes x
-   *   this subsumes this.f
+  /**  x subsumes x
+   *   x subsumes x.f
+   *   x =:= y ==> x subsumes y
    *   x subsumes y  ==>  x* subsumes y, x subsumes y?
    *   x subsumes y  ==>  x* subsumes y*, x? subsumes y?
    *   x: x1.type /\ x1 subsumes y  ==>  x subsumes y
-   *   TODO: Document path cases
+   *   X = CapSet^cx, exists rx in cx, rx subsumes y ==>  X subsumes y
+   *   Y = CapSet^cy, forall ry in cy, x subsumes ry ==>  x subsumes Y
+   *   X: CapSet^c1...CapSet^c2, (CapSet^c1) subsumes y  ==> X subsumes y
+   *   Y: CapSet^c1...CapSet^c2, x subsumes (CapSet^c2) ==> x subsumes Y
+   *   Contains[X, y]  ==>  X subsumes y
+   *
+   *   TODO: Document cases with more comments.
    */
-  // import reporting.trace
-  final def subsumes(y: CaptureRef)(using Context): Boolean = // trace.force(i"subsumes $this, $y"):
+  final def subsumes(y: CaptureRef)(using Context): Boolean =
 
     def subsumingRefs(x: Type, y: Type): Boolean = x match
       case x: CaptureRef => y match
@@ -136,11 +142,13 @@ trait CaptureRef extends TypeProxy, ValueType:
               case _ => false
           || viaInfo(y.info)(subsumingRefs(this, _))
         case MaybeCapability(y1) => this.stripMaybe.subsumes(y1)
-        case y: TypeRef if y.symbol.info.derivesFrom(defn.Caps_CapSet) =>
+        case y: TypeRef if y.derivesFrom(defn.Caps_CapSet) =>
           y.info match
-            case _: TypeAlias => y.captureSetOfInfo.elems.forall(this.subsumes)
             case TypeBounds(_, hi: CaptureRef) => this.subsumes(hi)
             case _ => y.captureSetOfInfo.elems.forall(this.subsumes)
+        case AnnotatedType(parent, ann)
+        if ann.symbol.isRetains && parent.derivesFrom(defn.Caps_CapSet) =>
+          ann.tree.toCaptureSet.elems.forall(this.subsumes)
         case _ => false
     || this.match
         case ReachCapability(x1) => x1.subsumes(y.stripReach)
@@ -149,8 +157,6 @@ trait CaptureRef extends TypeProxy, ValueType:
         case x: TypeRef if assumedContainsOf(x).contains(y) => true
         case x: TypeRef if x.derivesFrom(defn.Caps_CapSet) =>
           x.info match
-            case _: TypeAlias =>
-              x.captureSetOfInfo.elems.exists(_.subsumes(y))
             case TypeBounds(lo: CaptureRef, _) =>
               lo.subsumes(y)
             case _ =>

diff --git a/tests/pos-custom-args/captures/cc-poly-varargs.scala b/tests/pos-custom-args/captures/cc-poly-varargs.scala
@@ -1,17 +1,22 @@
-trait Cancellable
+abstract class Source[+T, Cap^]:
+  def transformValuesWith[U](f: (T -> U)^{Cap^}): Source[U, Cap]^{this, f} = ???
 
-abstract class Source[+T, Cap^]
-
-extension[T, Cap^](src: Source[T, Cap]^)
-  def transformValuesWith[U](f: (T -> U)^{Cap^}): Source[U, Cap]^{src, f} = ???
+// TODO: The extension version of `transformValuesWith` doesn't work currently.
+// extension[T, Cap^](src: Source[T, Cap]^)
+//   def transformValuesWith[U](f: (T -> U)^{Cap^}): Source[U, Cap]^{src, f} = ???
 
 def race[T, Cap^](sources: Source[T, Cap]^{Cap^}*): Source[T, Cap]^{Cap^} = ???
 
-def either[T1, T2, Cap^](src1: Source[T1, Cap]^{Cap^}, src2: Source[T2, Cap]^{Cap^}): Source[Either[T1, T2], Cap]^{Cap^} =
+def either[T1, T2, Cap^](
+    src1: Source[T1, Cap]^{Cap^},
+    src2: Source[T2, Cap]^{Cap^}): Source[Either[T1, T2], Cap]^{Cap^} =
   val left = src1.transformValuesWith(Left(_))
   val right = src2.transformValuesWith(Right(_))
-  race(left, right)
-
+  race[Either[T1, T2], Cap](left, right)
+  // An explcit type argument is required here because the second argument is
+  // inferred as `CapSet^{Cap^}` instead of `Cap`.
+  // Although `CapSet^{Cap^}` subsums `Cap` in terms of capture set,
+  // `Cap` is not a subtype of `CapSet^{Cap^}` in terms of subtyping.