Skip to content

Commit 7693722

Browse files
committed
Align deep capture sets with reach capabilities
Count in dcs exactly those locations where a cap gets replaced by a reach capability.
1 parent d749137 commit 7693722

File tree

5 files changed

+35
-18
lines changed

5 files changed

+35
-18
lines changed

compiler/src/dotty/tools/dotc/cc/CaptureSet.scala

Lines changed: 17 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1064,7 +1064,7 @@ object CaptureSet:
10641064
case ref: (TermRef | TermParamRef) if ref.isMaxCapability =>
10651065
if ref.isTrackableRef then ref.singletonCaptureSet
10661066
else CaptureSet.universal
1067-
case ReachCapability(ref1) => deepCaptureSet(ref1.widen)
1067+
case ReachCapability(ref1) => ref1.widen.deepCaptureSet
10681068
.showing(i"Deep capture set of $ref: ${ref1.widen} = $result", capt)
10691069
case _ => ofType(ref.underlying, followResult = true)
10701070

@@ -1115,17 +1115,25 @@ object CaptureSet:
11151115

11161116
/** The deep capture set of a type is the union of all covariant occurrences of
11171117
* capture sets. Nested existential sets are approximated with `cap`.
1118+
* NOTE: The traversal logic needs to be in sync with narrowCaps in CaptureOps, which
1119+
* replaces caps with reach capabilties.
11181120
*/
11191121
def ofTypeDeeply(tp: Type)(using Context): CaptureSet =
11201122
val collect = new TypeAccumulator[CaptureSet]:
1121-
def apply(cs: CaptureSet, t: Type) = t.dealias match
1122-
case t @ CapturingType(p, cs1) =>
1123-
val cs2 = apply(cs, p)
1124-
if variance > 0 then cs2 ++ cs1 else cs2
1125-
case t @ Existential(_, _) =>
1126-
apply(cs, Existential.toCap(t))
1127-
case _ =>
1128-
foldOver(cs, t)
1123+
def apply(cs: CaptureSet, t: Type) =
1124+
if variance <= 0 then cs
1125+
else t.dealias match
1126+
case t @ CapturingType(p, cs1) =>
1127+
this(cs, p) ++ cs1
1128+
case t @ AnnotatedType(parent, ann) =>
1129+
this(cs, parent)
1130+
case t @ FunctionOrMethod(args, res @ Existential(_, _))
1131+
if args.forall(_.isAlwaysPure) =>
1132+
this(cs, Existential.toCap(res))
1133+
case t @ Existential(_, _) =>
1134+
cs
1135+
case _ =>
1136+
foldOver(cs, t)
11291137
collect(CaptureSet.empty, tp)
11301138

11311139
type AssumedContains = immutable.Map[TypeRef, SimpleIdentitySet[CaptureRef]]

tests/neg-custom-args/captures/reaches.check

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@
3030
| ^^^^^^^^^^^^^^^^^^^
3131
| Local reach capability id* leaks into capture scope of method test
3232
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:62:27 --------------------------------------
33-
62 | val f1: File^{id*} = id(f) // error, since now id(f): File^
33+
62 | val f1: File^{id*} = id(f) // error, since now id(f): File^ // error
3434
| ^^^^^
3535
| Found: File^{f}
3636
| Required: File^{id*}
@@ -50,3 +50,11 @@
5050
| Type argument () -> Unit does not conform to lower bound () => Unit
5151
|
5252
| longer explanation available when compiling with `-explain`
53+
-- Error: tests/neg-custom-args/captures/reaches.scala:61:31 -----------------------------------------------------------
54+
61 | val leaked = usingFile[File^{id*}]: f => // error
55+
| ^^^
56+
| id* cannot be tracked since its capture set is empty
57+
-- Error: tests/neg-custom-args/captures/reaches.scala:62:18 -----------------------------------------------------------
58+
62 | val f1: File^{id*} = id(f) // error, since now id(f): File^ // error
59+
| ^^^
60+
| id* cannot be tracked since its capture set is empty

tests/neg-custom-args/captures/reaches.scala

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -58,8 +58,8 @@ def attack2 =
5858
val id: File^ -> File^ = x => x
5959
// val id: File^ -> EX C.File^C
6060

61-
val leaked = usingFile[File^{id*}]: f =>
62-
val f1: File^{id*} = id(f) // error, since now id(f): File^
61+
val leaked = usingFile[File^{id*}]: f => // error
62+
val f1: File^{id*} = id(f) // error, since now id(f): File^ // error
6363
f1
6464

6565
class List[+A]:

tests/neg-custom-args/captures/refine-reach-shallow.scala

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -5,14 +5,15 @@ def test1(): Unit =
55
val g: IO^ => IO^{f*} = f // error
66
def test2(): Unit =
77
val f: [R] -> (IO^ => R) -> R = ???
8-
val g: [R] -> (IO^{f*} => R) -> R = f // error
8+
val ff = f
9+
val g: [R] -> (IO^{f*} => R) -> R = f // error // error
910
def test3(): Unit =
1011
val f: [R] -> (IO^ -> R) -> R = ???
11-
val g: [R] -> (IO^{f*} -> R) -> R = f // error
12+
val g: [R] -> (IO^{f*} -> R) -> R = f // error // error
1213
def test4(): Unit =
1314
val xs: List[IO^] = ???
1415
val ys: List[IO^{xs*}] = xs // ok
1516
def test5(): Unit =
1617
val f: [R] -> (IO^ -> R) -> IO^ = ???
17-
val g: [R] -> (IO^ -> R) -> IO^{f*} = f // error
18-
val h: [R] -> (IO^{f*} -> R) -> IO^ = f // error
18+
val g: [R] -> (IO^ -> R) -> IO^{f*} = f // error // error
19+
val h: [R] -> (IO^{f*} -> R) -> IO^ = f // error // error

tests/neg-custom-args/captures/refine-withFile.scala

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,5 +4,5 @@ trait File
44
val useFile: [R] -> (path: String) -> (op: File^ -> R) -> R = ???
55
def main(): Unit =
66
val f: [R] -> (path: String) -> (op: File^ -> R) -> R = useFile
7-
val g: [R] -> (path: String) -> (op: File^{f*} -> R) -> R = f // error
8-
val leaked = g[File^{f*}]("test")(f => f) // boom
7+
val g: [R] -> (path: String) -> (op: File^{f*} -> R) -> R = f // error // error
8+
val leaked = g[File^{f*}]("test")(f => f) // error

0 commit comments

Comments
 (0)