Canonicalize capture variable subtype comparisons

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

@@ -108,7 +108,6 @@ trait CaptureRef extends TypeProxy, ValueType:
    *   TODO: Document cases with more comments.
    */
   final def subsumes(y: CaptureRef)(using Context): Boolean =
-
     def subsumingRefs(x: Type, y: Type): Boolean = x match
       case x: CaptureRef => y match
         case y: CaptureRef => x.subsumes(y)
@@ -119,6 +118,7 @@ trait CaptureRef extends TypeProxy, ValueType:
       case info: SingletonCaptureRef => test(info)
       case info: AndType => viaInfo(info.tp1)(test) || viaInfo(info.tp2)(test)
       case info: OrType => viaInfo(info.tp1)(test) && viaInfo(info.tp2)(test)
+      case info @ CapturingType(_,_) if this.derivesFrom(defn.Caps_CapSet) => test(info)
       case _ => false
 
     (this eq y)
@@ -149,7 +149,7 @@ trait CaptureRef extends TypeProxy, ValueType:
           y.info match
             case TypeBounds(_, hi: CaptureRef) => this.subsumes(hi)
             case _ => y.captureSetOfInfo.elems.forall(this.subsumes)
-        case CapturingType(parent, refs) if parent.derivesFrom(defn.Caps_CapSet) =>
+        case CapturingType(parent, refs) if parent.derivesFrom(defn.Caps_CapSet) || this.derivesFrom(defn.Caps_CapSet) =>
           refs.elems.forall(this.subsumes)
         case _ => false
     || this.match

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

@@ -1085,10 +1085,9 @@ object CaptureSet:
           tp.captureSet
         case tp: TermParamRef =>
           tp.captureSet
-        case _: TypeRef =>
-          empty
-        case _: TypeParamRef =>
-          empty
+        case tp: (TypeRef | TypeParamRef) =>
+          if tp.derivesFrom(defn.Caps_CapSet) then tp.captureSet
+          else empty
         case CapturingType(parent, refs) =>
           recur(parent) ++ refs
         case tp @ AnnotatedType(parent, ann) if ann.hasSymbol(defn.ReachCapabilityAnnot) =>

compiler/src/dotty/tools/dotc/core/TypeComparer.scala

@@ -439,7 +439,10 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
             if (recur(info1.alias, tp2)) return true
             if (tp1.prefix.isStable) return tryLiftedToThis1
           case _ =>
-            if (tp1 eq NothingType) || isBottom(tp1) then return true
+            if isCaptureVarComparison then
+              return subCaptures(tp1.captureSet, tp2.captureSet, frozenConstraint).isOK
+            if (tp1 eq NothingType) || isBottom(tp1) then
+              return true
         }
         thirdTry
       case tp1: TypeParamRef =>
@@ -587,6 +590,9 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
             || narrowGADTBounds(tp2, tp1, approx, isUpper = false))
           && (isBottom(tp1) || GADTusage(tp2.symbol))
 
+        if isCaptureVarComparison then
+          return subCaptures(tp1.captureSet, tp2.captureSet, frozenConstraint).isOK
+
         isSubApproxHi(tp1, info2.lo) && (trustBounds || isSubApproxHi(tp1, info2.hi))
         || compareGADT
         || tryLiftedToThis2
@@ -858,7 +864,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
         }
         compareTypeBounds
       case CapturingType(parent2, refs2) =>
-        def compareCapturing =
+        def compareCapturing: Boolean =
           val refs1 = tp1.captureSet
           try
             if refs1.isAlwaysEmpty then recur(tp1, parent2)
@@ -1580,6 +1586,11 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
       (tp2a ne tp2) && recur(tp1, tp2a) && { opaquesUsed = true; true }
     }
 
+    def isCaptureVarComparison: Boolean =
+      isCaptureCheckingOrSetup
+      && tp1.derivesFrom(defn.Caps_CapSet)
+      && tp2.derivesFrom(defn.Caps_CapSet)
+
     // begin recur
     if tp2 eq NoType then false
     else if tp1 eq tp2 then true

tests/neg-custom-args/captures/capture-vars-subtyping.scala

@@ -0,0 +1,48 @@
+import language.experimental.captureChecking
+import caps.*
+
+def test[C^] =
+  val a: C = ???
+  val b: CapSet^{C^} = a
+  val c: C = b
+  val d: CapSet^{C^, c} = a
+
+// TODO: make "CapSet-ness" of type variables somehow contagious?
+// Then we don't have to spell out the bounds explicitly...
+def testTrans[C^, D >: CapSet <: C, E >: CapSet <: D, F >: C <: CapSet^] =
+  val d1: D = ???
+  val d2: CapSet^{D^} = d1
+  val d3: D = d2
+  val e1: E = ???
+  val e2: CapSet^{E^} = e1
+  val e3: E = e2
+  val d4: D = e1
+  val c1: C = d1
+  val c2: C = e1
+  val f1: F = c1
+  val d_e_f1: CapSet^{D^,E^,F^} = d1
+  val d_e_f2: CapSet^{D^,E^,F^} = e1
+  val d_e_f3: CapSet^{D^,E^,F^} = f1
+  val f2: F = d_e_f1
+  val c3: C = d_e_f1 // error
+  val c4: C = f1     // error
+  val e4: E = f1     // error
+  val e5: E = d1     // error
+  val c5: CapSet^{C^} = e1
+
+
+trait A[+T]
+
+trait B[-C]
+
+def testCong[C^, D^] =
+  val a: A[C] = ???
+  val b: A[CapSet^{C^}] = a
+  val c: A[CapSet^{D^}] = a // error
+  val d: A[CapSet^{C^,D^}] = a
+  val e: A[C] = d // error
+  val f: B[C] = ???
+  val g: B[CapSet^{C^}] = f
+  val h: B[C] = g
+  val i: B[CapSet^{C^,D^}] = h // error
+  val j: B[C] = i

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

@@ -1,9 +1,7 @@
-abstract class Source[+T, Cap^]:
-  def transformValuesWith[U](f: (T -> U)^{Cap^}): Source[U, Cap]^{this, f} = ???
+abstract class Source[+T, Cap^]
 
-// 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} = ???
+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^} = ???
 
@@ -12,8 +10,4 @@ def either[T1, T2, Cap^](
     src2: Source[T2, Cap]^{Cap^}): Source[Either[T1, T2], Cap]^{Cap^} =
   val left = src1.transformValuesWith(Left(_))
   val right = src2.transformValuesWith(Right(_))
-  race[Either[T1, T2], Cap](left, right)
-  // Explicit type arguments are required here because the second argument
-  // is inferred as `CapSet^{Cap^}` instead of `Cap`.
-  // Although `CapSet^{Cap^}` subsumes `Cap` in terms of capture sets,
-  // `Cap` is not a subtype of `CapSet^{Cap^}` in terms of subtyping.
+  race(left, right)