Canonicalize capture variable subtype comparisons

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

@@ -298,6 +298,43 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
       }
     }
 
+     //TODO move the following functions somewhere more appropriate
+    /**
+     * Is the type `tp` a `CapSet` type, i.e., a capture variable?
+     *
+     * @param tp The type to check
+     * @param includeCapSet Whether to include the bare `CapSet` type itself in the check, false at the top level
+     */
+    def isCapSet(tp: Type, includeCapSet: Boolean = false): Boolean = tp match {
+      case tp: TypeRef => (includeCapSet && (tp.symbol eq defn.Caps_CapSet)) || {
+        tp.underlying match
+          case TypeBounds(lo, hi) => isCapSet(lo, true) && isCapSet(hi, true)
+          case TypeAlias(alias)   => isCapSet(alias) // TODO: test cases involving type aliases
+          case _                  => false
+      }
+      case tp: SingletonType => isCapSet(tp.underlying)
+      case CapturingType(parent, _) => isCapSet(parent, true)
+      case _ => false
+    }
+
+    /**
+     * Assumes that isCapSet(tp) is true.
+     */
+    def canonicalizeToCapSet(tp: Type): Type = tp match
+      case ct @ CapturingType(_,_) => ct
+      case tp: TypeRef if tp.symbol eq defn.Caps_CapSet => CapturingType(tp, CaptureSet.empty)
+      case tp: SingletonType => canonicalizeToCapSet(tp.underlying)
+      case tp: CaptureRef => CapturingType(defn.Caps_CapSet.typeRef, CaptureSet(tp))
+
+
+    /** 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.
+     */
+    def tryHandleCaptureVars: Boolean =
+      isCaptureCheckingOrSetup && isCapSet(tp1) && isCapSet(tp2) && recur(canonicalizeToCapSet(tp1), canonicalizeToCapSet(tp2)) // TODO: we could probably just call subcapturing right away here and terminate early
+
     def firstTry: Boolean = tp2 match {
       case tp2: NamedType =>
         def compareNamed(tp1: Type, tp2: NamedType): Boolean =
@@ -346,6 +383,7 @@ 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
+                || tryHandleCaptureVars
                 || thirdTryNamed(tp2)
             case _ =>
               secondTry
@@ -858,9 +896,10 @@ 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] && tryHandleCaptureVars then return true
             if refs1.isAlwaysEmpty then recur(tp1, parent2)
             else
               // The singletonOK branch is because we sometimes have a larger capture set in a singleton

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

@@ -0,0 +1,47 @@
+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
+
+
+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

@@ -12,8 +12,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)