diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 8414c3795f49..1d861e1ab9a9 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/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,6 +3329,7 @@ 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 @@ -3332,23 +3337,27 @@ object TypeComparer { 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 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..c0c31aba74db --- /dev/null +++ b/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 diff --git a/tests/pos-custom-args/captures/cc-poly-varargs.scala b/tests/pos-custom-args/captures/cc-poly-varargs.scala index 7f04ed987b28..aecd099a1479 100644 --- a/tests/pos-custom-args/captures/cc-poly-varargs.scala +++ b/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) \ No newline at end of file