Skip to content

Commit a8c624e

Browse files
noti0na1noti0na1
committed
Correct rules for CapSet; update definition for Contains; fix tests
1 parent 82c7e0a commit a8c624e

File tree

9 files changed

+42
-27
lines changed

9 files changed

+42
-27
lines changed

Diff for: ‎compiler/src/dotty/tools/dotc/cc/CaptureRef.scala

+19-4
Original file line numberDiff line numberDiff line change
@@ -100,7 +100,8 @@ trait CaptureRef extends TypeProxy, ValueType:
100100
* x: x1.type /\ x1 subsumes y ==> x subsumes y
101101
* TODO: Document path cases
102102
*/
103-
final def subsumes(y: CaptureRef)(using Context): Boolean =
103+
// import reporting.trace
104+
final def subsumes(y: CaptureRef)(using Context): Boolean = // trace.force(i"subsumes $this, $y"):
104105

105106
def subsumingRefs(x: Type, y: Type): Boolean = x match
106107
case x: CaptureRef => y match
@@ -135,14 +136,28 @@ trait CaptureRef extends TypeProxy, ValueType:
135136
case _ => false
136137
|| viaInfo(y.info)(subsumingRefs(this, _))
137138
case MaybeCapability(y1) => this.stripMaybe.subsumes(y1)
139+
case y: TypeRef if y.symbol.info.derivesFrom(defn.Caps_CapSet) =>
140+
y.info match
141+
case _: TypeAlias => y.captureSetOfInfo.elems.forall(this.subsumes)
142+
case TypeBounds(_, hi: CaptureRef) => this.subsumes(hi)
143+
case _ => y.captureSetOfInfo.elems.forall(this.subsumes)
138144
case _ => false
139145
|| this.match
140146
case ReachCapability(x1) => x1.subsumes(y.stripReach)
141147
case x: TermRef => viaInfo(x.info)(subsumingRefs(_, y))
142148
case x: TermParamRef => subsumesExistentially(x, y)
143-
case x: TypeRef if x.symbol.info.derivesFrom(defn.Caps_CapSet) =>
144-
x.captureSetOfInfo.elems.exists(_.subsumes(y))
145-
case x: TypeRef => assumedContainsOf(x).contains(y)
149+
case x: TypeRef if assumedContainsOf(x).contains(y) => true
150+
case x: TypeRef if x.derivesFrom(defn.Caps_CapSet) =>
151+
x.info match
152+
case _: TypeAlias =>
153+
x.captureSetOfInfo.elems.exists(_.subsumes(y))
154+
case TypeBounds(lo: CaptureRef, _) =>
155+
lo.subsumes(y)
156+
case _ =>
157+
x.captureSetOfInfo.elems.exists(_.subsumes(y))
158+
case AnnotatedType(parent, ann)
159+
if ann.symbol.isRetains && parent.derivesFrom(defn.Caps_CapSet) =>
160+
ann.tree.toCaptureSet.elems.exists(_.subsumes(y))
146161
case _ => false
147162
end subsumes
148163

Diff for: ‎library/src/scala/caps.scala

+2-2
Original file line numberDiff line numberDiff line change
@@ -22,12 +22,12 @@ import annotation.{experimental, compileTimeOnly, retainsCap}
2222
/** A type constraint expressing that the capture set `C` needs to contain
2323
* the capability `R`
2424
*/
25-
sealed trait Contains[C <: CapSet @retainsCap, R <: Singleton]
25+
sealed trait Contains[+C >: CapSet <: CapSet @retainsCap, R <: Singleton]
2626

2727
/** The only implementation of `Contains`. The constraint that `{R} <: C` is
2828
* added separately by the capture checker.
2929
*/
30-
given containsImpl[C <: CapSet @retainsCap, R <: Singleton]: Contains[C, R]()
30+
given containsImpl[C >: CapSet <: CapSet @retainsCap, R <: Singleton]: Contains[C, R]()
3131

3232
/** A wrapper indicating a type variable in a capture argument list of a
3333
* @retains annotation. E.g. `^{x, Y^}` is represented as `@retains(x, capsOf[Y])`.

Diff for: ‎tests/neg-custom-args/captures/capture-poly.scala

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ import caps.*
33
trait Foo extends Capability
44

55
trait CaptureSet:
6-
type C <: CapSet^
6+
type C^
77

88
def capturePoly[C^](a: Foo^{C^}): Foo^{C^} = a
99
def capturePoly2(c: CaptureSet)(a: Foo^{c.C^}): Foo^{c.C^} = a

Diff for: ‎tests/neg-custom-args/captures/i22005.scala

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
import caps.*
2+
3+
class IO
4+
class File(io: IO^)
5+
6+
class Handler[C^]:
7+
def f(file: File^): File^{C^} = file // error
8+
def g(file: File^{C^}): File^ = file // ok

Diff for: ‎tests/neg-custom-args/captures/use-capset.check

+8-8
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,19 @@
1-
-- Error: tests/neg-custom-args/captures/use-capset.scala:7:50 ---------------------------------------------------------
2-
7 |private def g[C^] = (xs: List[Object^{C^}]) => xs.head // error
1+
-- Error: tests/neg-custom-args/captures/use-capset.scala:5:50 ---------------------------------------------------------
2+
5 |private def g[C^] = (xs: List[Object^{C^}]) => xs.head // error
33
| ^^^^^^^
44
| Capture set parameter C leaks into capture scope of method g.
55
| To allow this, the type C should be declared with a @use annotation
6-
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:13:22 -----------------------------------
7-
13 | val _: () -> Unit = h // error: should be ->{io}
6+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:11:22 -----------------------------------
7+
11 | val _: () -> Unit = h // error: should be ->{io}
88
| ^
99
| Found: (h : () ->{io} Unit)
1010
| Required: () -> Unit
1111
|
1212
| longer explanation available when compiling with `-explain`
13-
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:15:50 -----------------------------------
14-
15 | val _: () -> List[Object^{io}] -> Object^{io} = h2 // error, should be ->{io}
13+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:13:50 -----------------------------------
14+
13 | val _: () -> List[Object^{io}] -> Object^{io} = h2 // error, should be ->{io}
1515
| ^^
16-
| Found: (h2 : () ->? (x$0: List[box Object^]^{}) ->{io} Object^{io})
17-
| Required: () -> List[box Object^{io}] -> Object^{io}
16+
| Found: (h2 : () ->? (x$0: List[box Object^{io}]^{}) ->{io} Object^{io})
17+
| Required: () -> List[box Object^{io}] -> Object^{io}
1818
|
1919
| longer explanation available when compiling with `-explain`

Diff for: ‎tests/neg-custom-args/captures/use-capset.scala

-2
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,5 @@
11
import caps.{use, CapSet}
22

3-
4-
53
def f[C^](@use xs: List[Object^{C^}]): Unit = ???
64

75
private def g[C^] = (xs: List[Object^{C^}]) => xs.head // error

Diff for: ‎tests/neg/cc-poly-2.check

-7
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,3 @@
1-
-- [E007] Type Mismatch Error: tests/neg/cc-poly-2.scala:13:15 ---------------------------------------------------------
2-
13 | f[Nothing](d) // error
3-
| ^
4-
| Found: (d : Test.D^)
5-
| Required: Test.D
6-
|
7-
| longer explanation available when compiling with `-explain`
81
-- [E007] Type Mismatch Error: tests/neg/cc-poly-2.scala:14:19 ---------------------------------------------------------
92
14 | f[CapSet^{c1}](d) // error
103
| ^

Diff for: ‎tests/neg/cc-poly-2.scala

+1-1
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ object Test:
1010

1111
def test(c1: C, c2: C) =
1212
val d: D^ = D()
13-
f[Nothing](d) // error
13+
// f[Nothing](d) // already rule out at typer
1414
f[CapSet^{c1}](d) // error
1515
val x = f(d)
1616
val _: D^{c1} = x // error

Diff for: ‎tests/pos/cc-poly-source-capability.scala

+3-2
Original file line numberDiff line numberDiff line change
@@ -20,13 +20,14 @@ import caps.use
2020

2121
def test1(async1: Async, @use others: List[Async]) =
2222
val src = Source[CapSet^{async1, others*}]
23+
val _: Set[Listener^{async1, others*}] = src.allListeners
2324
val lst1 = listener(async1)
2425
val lsts = others.map(listener)
2526
val _: List[Listener^{others*}] = lsts
2627
src.register{lst1}
2728
src.register(listener(async1))
28-
lsts.foreach(src.register)
29-
others.map(listener).foreach(src.register)
29+
lsts.foreach(src.register(_)) // TODO: why we need to use _ explicitly here?
30+
others.map(listener).foreach(src.register(_))
3031
val ls = src.allListeners
3132
val _: Set[Listener^{async1, others*}] = ls
3233

0 commit comments

Comments
 (0)