Ignore capture sets in certain cases of subtyping

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

@@ -543,6 +543,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
         res
 
       case tp1 @ CapturingType(parent1, refs1) =>
+        if (approx.lowIgnoreCaptures) then return recur(parent1, tp2)
         def compareCapturing =
           if tp2.isAny then true
           else if subCaptures(refs1, tp2.captureSet, frozenConstraint).isOK && sameBoxed(tp1, tp2, refs1)
@@ -936,7 +937,10 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
               || tp1.widen.underlyingClassRef(refinementOK = true).exists)
       then
         def checkBase =
-          isSubType(base, tp2, if tp1.isRef(cls2) then approx else approx.addLow)
+          var a = approx
+          if (!tp1.isRef(cls2)) then a = a.addLow
+          if (cls2 eq defn.Caps_CapSet) then a = a.addLowIgnoreCaptures //TODO is this the correct place to add this?
+          isSubType(base, tp2, a)
           && recordGadtUsageIf { MatchType.thatReducesUsingGadt(tp1) }
         if tp1.widenDealias.isInstanceOf[AndType] || base.isInstanceOf[OrType] then
           // If tp1 is a intersection, it could be that one of the original
@@ -3325,30 +3329,35 @@ object TypeComparer {
    *   - `None`    : They are still the same types
    *   - `LoApprox`: The left type is approximated (i.e widened)"
    *   - `HiApprox`: The right type is approximated (i.e narrowed)"
+   *   - `LoIgnoreCaptures`: (Capture checking): The captures of the left type are ignored in the comparison
    */
   object ApproxState:
     opaque type Repr = Int
 
     val None: Repr = 0
     private val LoApprox = 1
     private val HiApprox = 2
+    private val LoIgnoreCaptures = 4
 
     /** A special approximation state to indicate that this is the first time we
      *  compare (approximations of) this pair of types. It's converted to `None`
      *  in `isSubType`, but also leads to `leftRoot` being set there.
      */
-    val Fresh: Repr = 4
+    val Fresh: Repr = 8
 
     object Repr:
       extension (approx: Repr)
         def low: Boolean = (approx & LoApprox) != 0
         def high: Boolean = (approx & HiApprox) != 0
+        def lowIgnoreCaptures: Boolean = (approx & LoIgnoreCaptures) != 0
         def addLow: Repr = approx | LoApprox
         def addHigh: Repr = approx | HiApprox
+        def addLowIgnoreCaptures: Repr = approx | LoIgnoreCaptures
         def show: String =
           val lo = if low then " (left is approximated)" else ""
           val hi = if high then " (right is approximated)" else ""
-          lo ++ hi
+          val locapt = if lowIgnoreCaptures then " (left captures are ignored)" else ""
+          lo ++ hi ++ locapt
   end ApproxState
   type ApproxState = ApproxState.Repr
 

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)