Canonicalize capture variable subtype comparisons (#22299)

bracevac · web-flow · commit b709262c2275 · 2025-01-22T21:14:07.000+01:00
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. Supersedes #22183 and #22289. This solution is overall cleaner and does not require adding a new bit to the TypeComparer's ApproxState. TODOs/Issues/Questions: - [x] Fix extension method in test [cc-poly-varargs.scala](https://github.com/dotty-staging/dotty/blob/capture-subtyping-canon/tests/pos-custom-args/captures/cc-poly-varargs.scala). Currently causes an infinite regress. - [x] Fix the aftermath * tests/neg-custom-args/captures/lazylists-exceptions.scala * tests/neg-custom-args/captures/exceptions.scala * tests/neg-custom-args/captures/real-try.scala * tests/run-custom-args/captures/colltest5 - [x] Some negative cases in test [capture-vars-subtyping.scala](https://github.com/dotty-staging/dotty/blob/capture-subtyping-canon/tests/neg-custom-args/captures/capture-vars-subtyping.scala) pass: `D <: E` fails, but its canonicalized form `CapSet^{D^} <: CapSet^{E^}` now succeeds. Potential problem in the subcapturing implementation. - [x] ~Extend to intersection/unions `def f[C^, D^, E <: C | D, F <: C & D](...) = ...` etc.~ Lacking good uses cases, not planned right now. - [X] ~If we have `C^` declared in the current context, should there be a difference between `C` vs. `C^` for subsequent mentions? We currently do, but seems a bit too subtle for users.~ Will be addressed by a new scheme for declaring capture variables using context bounds.
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala b/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,15 @@ 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) =>
+        /*
+          If `this` is a capture set variable `C^`, then it is possible that it can be
+          reached from term variables in a reachability chain through the context.
+          For instance, in `def test[C^](src: Foo^{C^}) = { val x: Foo^{src} = src; val y: Foo^{x} = x; y }`
+          we expect that `C^` subsumes `x` and `y` in the body of the method
+          (cf. test case cc-poly-varargs.scala for a more involved example).
+         */
+        test(info)
       case _ => false
 
     (this eq y)
@@ -149,7 +157,11 @@ 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) =>
+          /* The second condition in the guard is for `this` being a `CapSet^{a,b...}` and etablishing a
+             potential reachability chain through `y`'s capture to a binding with
+             `this`'s capture set (cf. `CapturingType` case in `def viaInfo` above for more context).
+           */
           refs.elems.forall(this.subsumes)
         case _ => false
     || this.match
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/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) =>
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/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)
@@ -1572,6 +1578,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
diff --git a/tests/neg-custom-args/captures/capture-vars-subtyping.scala b/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 --git a/tests/pos-custom-args/captures/cc-poly-varargs.scala b/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)
