Canonicalize capture variable subtype comparisons

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

@@ -170,6 +170,32 @@ extension (tree: Tree)
 
 extension (tp: Type)
 
+  /**
+   * 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
+   */
+  final def isCapSet(includeCapSet: Boolean = false)(using Context): Boolean = tp match
+    case tp: TypeRef => (includeCapSet && (tp.symbol eq defn.Caps_CapSet)) || {
+      tp.underlying match
+        case TypeBounds(lo, hi) => lo.isCapSet(true) && hi.isCapSet(true)
+        case TypeAlias(alias)   => alias.isCapSet() // TODO: test cases involving type aliases
+        case _                  => false
+    }
+    case tp: SingletonType => tp.underlying.isCapSet()
+    case CapturingType(parent, _) => parent.isCapSet(true)
+    case _ => false
+
+  /**
+   * The capture set of a capture variable. Assumes that tp.isCapSet() is true.
+   */
+  final def captureSetOfCapSet(using Context): CaptureSet = tp match
+    case CapturingType(_,c) => c
+    case tp: TypeRef if tp.symbol eq defn.Caps_CapSet => CaptureSet.empty
+    case tp: SingletonType => tp.underlying.captureSetOfCapSet
+    case tp: CaptureRef => CaptureSet(tp)
+
   /** Is this type a CaptureRef that can be tracked?
    *  This is true for
    *    - all ThisTypes and all TermParamRef,

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

@@ -1071,6 +1071,9 @@ object CaptureSet:
     case ReachCapability(ref1) =>
       ref1.widen.deepCaptureSet(includeTypevars = true)
         .showing(i"Deep capture set of $ref: ${ref1.widen} = ${result}", capt)
+    case tp : TypeRef if tp.isCapSet() => tp.underlying match
+      case TypeBounds(lo, hi) if hi.isCapSet() => hi.captureSetOfCapSet
+      case _ => ofType(ref.underlying, followResult = true)
     case _ => ofType(ref.underlying, followResult = true)
 
   /** Capture set of a type */

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.isCapSet() && tp2.isCapSet()) then -1
+      else if (subCaptures(tp1.captureSetOfCapSet, tp2.captureSetOfCapSet, 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

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

@@ -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)