Canonicalize capture variable subtype comparisons

Fixes #22103

Subtype problems where at least one side is a type variable
representing a capture variable are canonicalized to
capturing type comparisons on the special `CapSet` for the
universe capture sets. For example, `C <: CapSet^{C^}`
becomes `CapSet^{C^} <: CapSet^{C^}`, and `A <: B` becomes
`CapSet^{A^} <: CapSet^{B^}` if both `A` and `B` are capture
variables.

Needs a patch in subsumes

Without the patch we get divergence in AvoidMap for cc-poly-varargs.
The underlying cause for the divergence is that we could not conclude
that the capture variable `Cap^` subsumes `left`
through `src1`, i.e., `left` reaches `Cap^`.
That caused `left` to appear circularly in its
own capture set and subsequently avoidance to loop
forever.

Author: bracevac

Diff for: 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

Diff for: compiler/src/dotty/tools/dotc/cc/CaptureSet.scala

@@ -18,6 +18,7 @@ import TypeComparer.subsumesExistentially
 import util.common.alwaysTrue
 import scala.collection.{mutable, immutable}
 import CCState.*
+import dotty.tools.dotc.core.TypeOps.AvoidMap
 
 /** A class for capture sets. Capture sets can be constants or variables.
  *  Capture sets support inclusion constraints <:< where <:< is subcapturing.
@@ -1085,10 +1086,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) =>

Diff for: compiler/src/dotty/tools/dotc/core/TypeComparer.scala

@@ -298,6 +298,19 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
       }
     }
 
+    /** In capture checking, implements the logic to compare type variables which represent
+     *  capture variables.
+     *
+     *  Note: should only be called in a context where tp1 or tp2 is a type variable representing a capture variable.
+     *
+     *  @return -1 if tp1 or tp2 is not a capture variables, 1 if both tp1 and tp2 are capture variables and tp1 is a subcapture of tp2,
+     *           0 if both tp1 and tp2 are capture variables but tp1 is not a subcapture of tp2.
+     */
+    inline def tryHandleCaptureVars: Int =
+      if !(isCaptureCheckingOrSetup && tp1.derivesFrom(defn.Caps_CapSet) && tp1.derivesFrom(defn.Caps_CapSet)) then -1
+      else if (subCaptures(tp1.captureSet, tp2.captureSet, frozenConstraint).isOK) then 1
+      else 0
+
     def firstTry: Boolean = tp2 match {
       case tp2: NamedType =>
         def compareNamed(tp1: Type, tp2: NamedType): Boolean =
@@ -346,7 +359,9 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
                 && isSubPrefix(tp1.prefix, tp2.prefix)
                 && tp1.signature == tp2.signature
                 && !(sym1.isClass && sym2.isClass)  // class types don't subtype each other
-                || thirdTryNamed(tp2)
+                || {val cv = tryHandleCaptureVars
+                    if (cv < 0) then thirdTryNamed(tp2)
+                    else cv != 0 }
             case _ =>
               secondTry
         end compareNamed
@@ -434,6 +449,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
 
     def secondTry: Boolean = tp1 match {
       case tp1: NamedType =>
+        val cv = tryHandleCaptureVars
+        if (cv >= 0) then return cv != 0
         tp1.info match {
           case info1: TypeAlias =>
             if (recur(info1.alias, tp2)) return true
@@ -858,9 +875,12 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
         }
         compareTypeBounds
       case CapturingType(parent2, refs2) =>
-        def compareCapturing =
+        def compareCapturing: Boolean =
           val refs1 = tp1.captureSet
           try
+            if tp1.isInstanceOf[TypeRef] then
+              val cv = tryHandleCaptureVars
+              if (cv >= 0) then return (cv != 0)
             if refs1.isAlwaysEmpty then recur(tp1, parent2)
             else
               // The singletonOK branch is because we sometimes have a larger capture set in a singleton

Diff for: 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

Diff for: 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)