diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala index 199114880c2b..a11e272685d9 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala @@ -100,7 +100,8 @@ trait CaptureRef extends TypeProxy, ValueType: * x: x1.type /\ x1 subsumes y ==> x subsumes y * TODO: Document path cases */ - final def subsumes(y: CaptureRef)(using Context): Boolean = + // import reporting.trace + final def subsumes(y: CaptureRef)(using Context): Boolean = // trace.force(i"subsumes $this, $y"): def subsumingRefs(x: Type, y: Type): Boolean = x match case x: CaptureRef => y match @@ -135,14 +136,28 @@ trait CaptureRef extends TypeProxy, ValueType: case _ => false || viaInfo(y.info)(subsumingRefs(this, _)) case MaybeCapability(y1) => this.stripMaybe.subsumes(y1) + case y: TypeRef if y.symbol.info.derivesFrom(defn.Caps_CapSet) => + y.info match + case _: TypeAlias => y.captureSetOfInfo.elems.forall(this.subsumes) + case TypeBounds(_, hi: CaptureRef) => this.subsumes(hi) + case _ => y.captureSetOfInfo.elems.forall(this.subsumes) case _ => false || this.match case ReachCapability(x1) => x1.subsumes(y.stripReach) case x: TermRef => viaInfo(x.info)(subsumingRefs(_, y)) case x: TermParamRef => subsumesExistentially(x, y) - case x: TypeRef if x.symbol.info.derivesFrom(defn.Caps_CapSet) => - x.captureSetOfInfo.elems.exists(_.subsumes(y)) - case x: TypeRef => assumedContainsOf(x).contains(y) + case x: TypeRef if assumedContainsOf(x).contains(y) => true + case x: TypeRef if x.derivesFrom(defn.Caps_CapSet) => + x.info match + case _: TypeAlias => + x.captureSetOfInfo.elems.exists(_.subsumes(y)) + case TypeBounds(lo: CaptureRef, _) => + lo.subsumes(y) + case _ => + x.captureSetOfInfo.elems.exists(_.subsumes(y)) + case AnnotatedType(parent, ann) + if ann.symbol.isRetains && parent.derivesFrom(defn.Caps_CapSet) => + ann.tree.toCaptureSet.elems.exists(_.subsumes(y)) case _ => false end subsumes diff --git a/library/src/scala/caps.scala b/library/src/scala/caps.scala index 53c4ae7dc0dd..da099c4afab6 100644 --- a/library/src/scala/caps.scala +++ b/library/src/scala/caps.scala @@ -22,12 +22,12 @@ import annotation.{experimental, compileTimeOnly, retainsCap} /** A type constraint expressing that the capture set `C` needs to contain * the capability `R` */ - sealed trait Contains[C <: CapSet @retainsCap, R <: Singleton] + sealed trait Contains[+C >: CapSet <: CapSet @retainsCap, R <: Singleton] /** The only implementation of `Contains`. The constraint that `{R} <: C` is * added separately by the capture checker. */ - given containsImpl[C <: CapSet @retainsCap, R <: Singleton]: Contains[C, R]() + given containsImpl[C >: CapSet <: CapSet @retainsCap, R <: Singleton]: Contains[C, R]() /** A wrapper indicating a type variable in a capture argument list of a * @retains annotation. E.g. `^{x, Y^}` is represented as `@retains(x, capsOf[Y])`. diff --git a/tests/neg-custom-args/captures/capture-poly.scala b/tests/neg-custom-args/captures/capture-poly.scala index a3a7a4c2a3d7..0a0d773a3f64 100644 --- a/tests/neg-custom-args/captures/capture-poly.scala +++ b/tests/neg-custom-args/captures/capture-poly.scala @@ -3,7 +3,7 @@ import caps.* trait Foo extends Capability trait CaptureSet: - type C <: CapSet^ + type C^ def capturePoly[C^](a: Foo^{C^}): Foo^{C^} = a def capturePoly2(c: CaptureSet)(a: Foo^{c.C^}): Foo^{c.C^} = a diff --git a/tests/neg-custom-args/captures/i22005.scala b/tests/neg-custom-args/captures/i22005.scala new file mode 100644 index 000000000000..a9dca999e42b --- /dev/null +++ b/tests/neg-custom-args/captures/i22005.scala @@ -0,0 +1,8 @@ +import caps.* + +class IO +class File(io: IO^) + +class Handler[C^]: + def f(file: File^): File^{C^} = file // error + def g(file: File^{C^}): File^ = file // ok diff --git a/tests/neg-custom-args/captures/use-capset.check b/tests/neg-custom-args/captures/use-capset.check index cb330daf67f8..74afaa05890f 100644 --- a/tests/neg-custom-args/captures/use-capset.check +++ b/tests/neg-custom-args/captures/use-capset.check @@ -1,19 +1,19 @@ --- Error: tests/neg-custom-args/captures/use-capset.scala:7:50 --------------------------------------------------------- -7 |private def g[C^] = (xs: List[Object^{C^}]) => xs.head // error +-- Error: tests/neg-custom-args/captures/use-capset.scala:5:50 --------------------------------------------------------- +5 |private def g[C^] = (xs: List[Object^{C^}]) => xs.head // error | ^^^^^^^ | Capture set parameter C leaks into capture scope of method g. | To allow this, the type C should be declared with a @use annotation --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:13:22 ----------------------------------- -13 | val _: () -> Unit = h // error: should be ->{io} +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:11:22 ----------------------------------- +11 | val _: () -> Unit = h // error: should be ->{io} | ^ | Found: (h : () ->{io} Unit) | Required: () -> Unit | | longer explanation available when compiling with `-explain` --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:15:50 ----------------------------------- -15 | val _: () -> List[Object^{io}] -> Object^{io} = h2 // error, should be ->{io} +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:13:50 ----------------------------------- +13 | val _: () -> List[Object^{io}] -> Object^{io} = h2 // error, should be ->{io} | ^^ - | Found: (h2 : () ->? (x$0: List[box Object^]^{}) ->{io} Object^{io}) - | Required: () -> List[box Object^{io}] -> Object^{io} + | Found: (h2 : () ->? (x$0: List[box Object^{io}]^{}) ->{io} Object^{io}) + | Required: () -> List[box Object^{io}] -> Object^{io} | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/use-capset.scala b/tests/neg-custom-args/captures/use-capset.scala index 6010e955f867..74288d616396 100644 --- a/tests/neg-custom-args/captures/use-capset.scala +++ b/tests/neg-custom-args/captures/use-capset.scala @@ -1,7 +1,5 @@ import caps.{use, CapSet} - - def f[C^](@use xs: List[Object^{C^}]): Unit = ??? private def g[C^] = (xs: List[Object^{C^}]) => xs.head // error diff --git a/tests/neg/cc-poly-2.check b/tests/neg/cc-poly-2.check index 0615ce19b5ea..7a2882775a75 100644 --- a/tests/neg/cc-poly-2.check +++ b/tests/neg/cc-poly-2.check @@ -1,10 +1,3 @@ --- [E007] Type Mismatch Error: tests/neg/cc-poly-2.scala:13:15 --------------------------------------------------------- -13 | f[Nothing](d) // error - | ^ - | Found: (d : Test.D^) - | Required: Test.D - | - | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg/cc-poly-2.scala:14:19 --------------------------------------------------------- 14 | f[CapSet^{c1}](d) // error | ^ diff --git a/tests/neg/cc-poly-2.scala b/tests/neg/cc-poly-2.scala index c5e5df6540da..809fa8ae077c 100644 --- a/tests/neg/cc-poly-2.scala +++ b/tests/neg/cc-poly-2.scala @@ -10,7 +10,7 @@ object Test: def test(c1: C, c2: C) = val d: D^ = D() - f[Nothing](d) // error + // f[Nothing](d) // already rule out at typer f[CapSet^{c1}](d) // error val x = f(d) val _: D^{c1} = x // error diff --git a/tests/pos/cc-poly-source-capability.scala b/tests/pos/cc-poly-source-capability.scala index 363f261dadc1..6f6bdd91d20a 100644 --- a/tests/pos/cc-poly-source-capability.scala +++ b/tests/pos/cc-poly-source-capability.scala @@ -20,13 +20,14 @@ import caps.use def test1(async1: Async, @use others: List[Async]) = val src = Source[CapSet^{async1, others*}] + val _: Set[Listener^{async1, others*}] = src.allListeners val lst1 = listener(async1) val lsts = others.map(listener) val _: List[Listener^{others*}] = lsts src.register{lst1} src.register(listener(async1)) - lsts.foreach(src.register) - others.map(listener).foreach(src.register) + lsts.foreach(src.register(_)) // TODO: why we need to use _ explicitly here? + others.map(listener).foreach(src.register(_)) val ls = src.allListeners val _: Set[Listener^{async1, others*}] = ls