Skip to content
Prev Previous commit
Next Next commit
Align deep capture sets with reach capabilities
Count in dcs exactly those locations where a cap gets replaced by a reach capability.
  • Loading branch information
odersky committed Oct 30, 2024
commit e1b31c1b752d6149d8b8aa0e4202248d958694d7
26 changes: 17 additions & 9 deletions compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
Original file line number Diff line number Diff line change
Expand Up @@ -1064,7 +1064,7 @@ object CaptureSet:
case ref: (TermRef | TermParamRef) if ref.isMaxCapability =>
if ref.isTrackableRef then ref.singletonCaptureSet
else CaptureSet.universal
case ReachCapability(ref1) => deepCaptureSet(ref1.widen)
case ReachCapability(ref1) => ref1.widen.deepCaptureSet
.showing(i"Deep capture set of $ref: ${ref1.widen} = $result", capt)
case _ => ofType(ref.underlying, followResult = true)

Expand Down Expand Up @@ -1115,17 +1115,25 @@ object CaptureSet:

/** The deep capture set of a type is the union of all covariant occurrences of
* capture sets. Nested existential sets are approximated with `cap`.
* NOTE: The traversal logic needs to be in sync with narrowCaps in CaptureOps, which
* replaces caps with reach capabilties.
*/
def ofTypeDeeply(tp: Type)(using Context): CaptureSet =
val collect = new TypeAccumulator[CaptureSet]:
def apply(cs: CaptureSet, t: Type) = t.dealias match
case t @ CapturingType(p, cs1) =>
val cs2 = apply(cs, p)
if variance > 0 then cs2 ++ cs1 else cs2
case t @ Existential(_, _) =>
apply(cs, Existential.toCap(t))
case _ =>
foldOver(cs, t)
def apply(cs: CaptureSet, t: Type) =
if variance <= 0 then cs
else t.dealias match
case t @ CapturingType(p, cs1) =>
this(cs, p) ++ cs1
case t @ AnnotatedType(parent, ann) =>
this(cs, parent)
case t @ FunctionOrMethod(args, res @ Existential(_, _))
if args.forall(_.isAlwaysPure) =>
this(cs, Existential.toCap(res))
case t @ Existential(_, _) =>
cs
case _ =>
foldOver(cs, t)
collect(CaptureSet.empty, tp)

type AssumedContains = immutable.Map[TypeRef, SimpleIdentitySet[CaptureRef]]
Expand Down
10 changes: 9 additions & 1 deletion tests/neg-custom-args/captures/reaches.check
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@
| ^^^^^^^^^^^^^^^^^^^
| Local reach capability id* leaks into capture scope of method test
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:62:27 --------------------------------------
62 | val f1: File^{id*} = id(f) // error, since now id(f): File^
62 | val f1: File^{id*} = id(f) // error, since now id(f): File^ // error
| ^^^^^
| Found: File^{f}
| Required: File^{id*}
Expand All @@ -50,3 +50,11 @@
| Type argument () -> Unit does not conform to lower bound () => Unit
|
| longer explanation available when compiling with `-explain`
-- Error: tests/neg-custom-args/captures/reaches.scala:61:31 -----------------------------------------------------------
61 | val leaked = usingFile[File^{id*}]: f => // error
| ^^^
| id* cannot be tracked since its capture set is empty
-- Error: tests/neg-custom-args/captures/reaches.scala:62:18 -----------------------------------------------------------
62 | val f1: File^{id*} = id(f) // error, since now id(f): File^ // error
| ^^^
| id* cannot be tracked since its capture set is empty
4 changes: 2 additions & 2 deletions tests/neg-custom-args/captures/reaches.scala
Original file line number Diff line number Diff line change
Expand Up @@ -58,8 +58,8 @@ def attack2 =
val id: File^ -> File^ = x => x
// val id: File^ -> EX C.File^C

val leaked = usingFile[File^{id*}]: f =>
val f1: File^{id*} = id(f) // error, since now id(f): File^
val leaked = usingFile[File^{id*}]: f => // error
val f1: File^{id*} = id(f) // error, since now id(f): File^ // error
f1

class List[+A]:
Expand Down
9 changes: 5 additions & 4 deletions tests/neg-custom-args/captures/refine-reach-shallow.scala
Original file line number Diff line number Diff line change
Expand Up @@ -5,14 +5,15 @@ def test1(): Unit =
val g: IO^ => IO^{f*} = f // error
def test2(): Unit =
val f: [R] -> (IO^ => R) -> R = ???
val g: [R] -> (IO^{f*} => R) -> R = f // error
val ff = f
val g: [R] -> (IO^{f*} => R) -> R = f // error // error
def test3(): Unit =
val f: [R] -> (IO^ -> R) -> R = ???
val g: [R] -> (IO^{f*} -> R) -> R = f // error
val g: [R] -> (IO^{f*} -> R) -> R = f // error // error
def test4(): Unit =
val xs: List[IO^] = ???
val ys: List[IO^{xs*}] = xs // ok
def test5(): Unit =
val f: [R] -> (IO^ -> R) -> IO^ = ???
val g: [R] -> (IO^ -> R) -> IO^{f*} = f // error
val h: [R] -> (IO^{f*} -> R) -> IO^ = f // error
val g: [R] -> (IO^ -> R) -> IO^{f*} = f // error // error
val h: [R] -> (IO^{f*} -> R) -> IO^ = f // error // error
4 changes: 2 additions & 2 deletions tests/neg-custom-args/captures/refine-withFile.scala
Original file line number Diff line number Diff line change
Expand Up @@ -4,5 +4,5 @@ trait File
val useFile: [R] -> (path: String) -> (op: File^ -> R) -> R = ???
def main(): Unit =
val f: [R] -> (path: String) -> (op: File^ -> R) -> R = useFile
val g: [R] -> (path: String) -> (op: File^{f*} -> R) -> R = f // error
val leaked = g[File^{f*}]("test")(f => f) // boom
val g: [R] -> (path: String) -> (op: File^{f*} -> R) -> R = f // error // error
val leaked = g[File^{f*}]("test")(f => f) // error