From a587261e224c3eacdd370c252a433cc717cb8359 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Oliver=20Bra=C4=8Devac?= Date: Tue, 21 Jan 2025 21:58:27 +0100 Subject: [PATCH 1/3] 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. --- .../src/dotty/tools/dotc/cc/CaptureRef.scala | 4 +- .../src/dotty/tools/dotc/cc/CaptureSet.scala | 8 ++-- .../dotty/tools/dotc/core/TypeComparer.scala | 24 +++++++++- .../captures/capture-vars-subtyping.scala | 48 +++++++++++++++++++ .../captures/cc-poly-varargs.scala | 14 ++---- 5 files changed, 80 insertions(+), 18 deletions(-) create mode 100644 tests/neg-custom-args/captures/capture-vars-subtyping.scala diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala index e5beb56c6c56..1e7b025826cb 100644 --- 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,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 --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index 7f4a34bab1f9..d7da8235ad80 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/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 --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index bb52d97ac04e..8927394a6c38 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/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 --git a/tests/neg-custom-args/captures/capture-vars-subtyping.scala b/tests/neg-custom-args/captures/capture-vars-subtyping.scala new file mode 100644 index 000000000000..1986a0aa33fc --- /dev/null +++ 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 index 7f04ed987b28..8bd0dc89bc7a 100644 --- 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) From 24ddd744c8c3a206ea88ee9ffb21a925fb176b09 Mon Sep 17 00:00:00 2001 From: odersky Date: Wed, 22 Jan 2025 15:17:44 +0100 Subject: [PATCH 2/3] Polishings Make tests in TypeComparer fit better with the rest --- .../src/dotty/tools/dotc/cc/CaptureSet.scala | 1 - .../dotty/tools/dotc/core/TypeComparer.scala | 35 +++++++------------ 2 files changed, 13 insertions(+), 23 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index d7da8235ad80..39c41c369864 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala @@ -18,7 +18,6 @@ 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. diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 8927394a6c38..4aca85cbb179 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -298,19 +298,6 @@ 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 = @@ -359,9 +346,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 - || {val cv = tryHandleCaptureVars - if (cv < 0) then thirdTryNamed(tp2) - else cv != 0 } + || thirdTryNamed(tp2) case _ => secondTry end compareNamed @@ -449,14 +434,15 @@ 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 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 => @@ -604,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 @@ -878,9 +867,6 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling 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 @@ -1600,6 +1586,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 From c3fcd7cd2772a6b75ae3bdb09c8a857efd66cf12 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Oliver=20Bra=C4=8Devac?= Date: Wed, 22 Jan 2025 17:47:23 +0100 Subject: [PATCH 3/3] Comments --- compiler/src/dotty/tools/dotc/cc/CaptureRef.scala | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala index 1e7b025826cb..2caba4cf7d89 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala @@ -118,7 +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) => test(info) + 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) @@ -150,6 +158,10 @@ trait CaptureRef extends TypeProxy, ValueType: case TypeBounds(_, hi: CaptureRef) => this.subsumes(hi) case _ => y.captureSetOfInfo.elems.forall(this.subsumes) 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