Skip to content

Commit f6f996c

Browse files
oderskyodersky
committed
Add implied captures in function types
This is an attempt to fix the problem explified in the `delayedRunops*.scala` tests. We can treat it as a baseline that fixes the immediate problem of the interaction of reach capabilities and type variables. There might be better ways to do this by using a proper adapation rule for function types instead of adding implied captures post-hoc.
1 parent c6e3910 commit f6f996c

22 files changed

+200
-30
lines changed

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

+8
Original file line numberDiff line numberDiff line change
@@ -527,6 +527,14 @@ extension (tp: Type)
527527
case _ =>
528528
tp
529529

530+
/** Add implied captures as defined by `CaptureSet.addImplied`. */
531+
def withImpliedCaptures(using Context): Type =
532+
if tp.isValueType && !tp.isAlwaysPure then
533+
val implied = CaptureSet.addImplied()(CaptureSet.empty, tp)
534+
if !implied.isAlwaysEmpty then capt.println(i"Add implied $implied to $tp")
535+
tp.capturing(implied)
536+
else tp
537+
530538
def level(using Context): Level =
531539
tp match
532540
case tp: TermRef => tp.symbol.ccLevel

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

+33
Original file line numberDiff line numberDiff line change
@@ -1068,6 +1068,39 @@ object CaptureSet:
10681068
.showing(i"Deep capture set of $ref: ${ref1.widen} = $result", capt)
10691069
case _ => ofType(ref.underlying, followResult = true)
10701070

1071+
/** Add captures implied by a type. This means: if we have a contravarint, boxed
1072+
* capability in a function parameter and the capability is either `cap`, or a
1073+
* reach capability, or a capture set variable, add the same capability to the enclosing
1074+
* function arrow. For instance `List[() ->{ops*} Unit] -> Unit` would become
1075+
* `List[() ->{ops*} Unit] ->{ops*} Unit`. This is needed to make
1076+
* the `delayedRunops*.scala` tests produce errors.
1077+
* TODO: Investigate whether we can roll this into a widening rule like
1078+
*
1079+
* List[() ->{cap} Unit] -> Unit <: List[() ->{ops*} Unit] ->{ops*} Unit
1080+
*
1081+
* but not
1082+
*
1083+
* List[() ->{cap} Unit] -> Unit <: List[() ->{ops*} Unit] -> Unit
1084+
*
1085+
* It would mean that a reach capability can no longer be a subtype of `cap`.
1086+
*/
1087+
class addImplied(using Context) extends TypeAccumulator[CaptureSet]:
1088+
var boundVars: Set[CaptureRef] = Set.empty
1089+
def isImplied(tp: CaptureRef) =
1090+
(tp.isRootCapability || tp.isReach || tp.derivesFrom(defn.Caps_CapSet))
1091+
&& !boundVars.contains(tp.stripReach)
1092+
def apply(cs: CaptureSet, t: Type) = t match
1093+
case t @ CapturingType(parent, cs1) =>
1094+
val cs2 = this(cs, parent)
1095+
if variance <= 0 && t.isBoxed then cs2 ++ cs1.filter(isImplied)
1096+
else cs2
1097+
case t: MethodOrPoly =>
1098+
val saved = boundVars
1099+
boundVars ++= t.paramRefs.asInstanceOf[List[CaptureRef]]
1100+
try foldOver(cs, t) finally boundVars = saved
1101+
case _ =>
1102+
foldOver(cs, t)
1103+
10711104
/** Capture set of a type */
10721105
def ofType(tp: Type, followResult: Boolean)(using Context): CaptureSet =
10731106
def recur(tp: Type): CaptureSet = trace(i"ofType $tp, ${tp.getClass} $followResult", show = true):

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -1292,7 +1292,7 @@ class CheckCaptures extends Recheck, SymTransformer:
12921292
else
12931293
val widened = improveCaptures(actual.widen.dealiasKeepAnnots, actual)
12941294
val adapted = adaptBoxed(
1295-
widened.withReachCaptures(actual), expected, pos,
1295+
widened.withReachCaptures(actual).withImpliedCaptures, expected, pos,
12961296
covariant = true, alwaysConst = false, boxErrors)
12971297
if adapted eq widened then actual
12981298
else adapted.showing(i"adapt boxed $actual vs $expected = $adapted", capt)

Diff for: ‎scala2-library-cc/src/scala/collection/SeqView.scala

+1-1
Original file line numberDiff line numberDiff line change
@@ -212,7 +212,7 @@ object SeqView {
212212
override def sorted[B1 >: A](implicit ord1: Ordering[B1]): SeqView[A]^{this} =
213213
if (ord1 == Sorted.this.ord) outer.unsafeAssumePure
214214
else if (ord1.isReverseOf(Sorted.this.ord)) this
215-
else new Sorted(elems, len, ord1)
215+
else new Sorted(elems, len, ord1).asInstanceOf // !!! asInstanceOf needed after adding addImplied widening
216216
}
217217

218218
@volatile private[this] var evaluated = false

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

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/delayedRunops2.scala:10:35 -------------------------------
2+
10 | app[List[() ->{ops*} Unit], Unit](ops, runOps) // error
3+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
4+
| Found: () ->{ops*} Unit
5+
| Required: () -> Unit
6+
|
7+
| longer explanation available when compiling with `-explain`
8+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/delayedRunops2.scala:18:36 -------------------------------
9+
18 | app2[List[() => Unit], Unit](ops, runOps: List[() => Unit] -> Unit) // error
10+
| ^^^^^^
11+
| Found: (ops: List[box () ->? Unit]^?) ->? Unit
12+
| Required: (ops: List[box () => Unit]) -> Unit
13+
|
14+
| longer explanation available when compiling with `-explain`

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

+22
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
import language.experimental.captureChecking
2+
3+
def runOps(ops: List[() => Unit]): Unit =
4+
ops.foreach(op => op())
5+
6+
def app[T, U](x: T, op: T => U): () ->{op} U =
7+
() => op(x)
8+
9+
def unsafeRunOps(ops: List[() => Unit]): () ->{} Unit =
10+
app[List[() ->{ops*} Unit], Unit](ops, runOps) // error
11+
12+
def app2[T, U](x: T, op: T => U): () ->{op} U =
13+
() =>
14+
def y: T = x
15+
op(y)
16+
17+
def unsafeRunOps2(ops: List[() => Unit]): () -> Unit =
18+
app2[List[() => Unit], Unit](ops, runOps: List[() => Unit] -> Unit) // error
19+
20+
21+
22+

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

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/delayedRunops3.scala:10:41 -------------------------------
2+
10 | app[List[() ->{ops*} Unit], Unit](ops, runOps) // error
3+
| ^^^^^^
4+
| Found: (ops: List[box () ->? Unit]^?) ->? Unit
5+
| Required: (ops: List[box () ->{ops²*} Unit]) -> Unit
6+
|
7+
| where: ops is a reference to a value parameter
8+
| ops² is a parameter in method unsafeRunOps
9+
|
10+
| longer explanation available when compiling with `-explain`

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

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
import language.experimental.captureChecking
2+
3+
def runOps(ops: List[() => Unit]): Unit =
4+
ops.foreach(op => op())
5+
6+
def app[T, U](x: T, op: T -> U): () ->{} U =
7+
() => op(x)
8+
9+
def unsafeRunOps(ops: List[() => Unit]): () ->{} Unit =
10+
app[List[() ->{ops*} Unit], Unit](ops, runOps) // error
11+
12+
13+
14+

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

+21
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/delayedRunops4.scala:11:4 --------------------------------
2+
11 | runOps[C]: List[() ->{C^} Unit] ->{C^} Unit) // error
3+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
4+
| Found: List[box () ->{C^} Unit] ->{C^} Unit
5+
| Required: List[box () ->{C^} Unit] -> Unit
6+
|
7+
| longer explanation available when compiling with `-explain`
8+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/delayedRunops4.scala:15:43 -------------------------------
9+
15 | app[List[() ->{C^} Unit], Unit](ops, rops[C]) // error
10+
| ^^^^^^^
11+
| Found: (ops: List[box () ->{C^} Unit]) ->{C^} Unit
12+
| Required: (ops: List[box () ->{C^} Unit]) -> Unit
13+
|
14+
| longer explanation available when compiling with `-explain`
15+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/delayedRunops4.scala:18:39 -------------------------------
16+
18 | app[List[() ->{C^} Unit], Unit](ops, runOps) // error
17+
| ^^^^^^
18+
| Found: (ops: List[box () ->? Unit]^?) ->? Unit
19+
| Required: (ops: List[box () ->{C^} Unit]) -> Unit
20+
|
21+
| longer explanation available when compiling with `-explain`

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

+24
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
import language.experimental.captureChecking
2+
3+
def runOps[C^](ops: List[() ->{C^} Unit]): Unit =
4+
ops.foreach(op => op())
5+
6+
def app[T, U](x: T, op: T -> U): () ->{} U =
7+
() => op(x)
8+
9+
def unsafeRunOps[C^](ops: List[() ->{C^} Unit]): () ->{} Unit =
10+
app[List[() ->{C^} Unit], Unit](ops,
11+
runOps[C]: List[() ->{C^} Unit] ->{C^} Unit) // error
12+
13+
def unsafeRunOps2[C^](ops: List[() ->{C^} Unit]): () ->{} Unit =
14+
def rops[D^]: (ops: List[() ->{D^} Unit]) -> Unit = ???
15+
app[List[() ->{C^} Unit], Unit](ops, rops[C]) // error
16+
17+
def unsafeRunOps3[C^](ops: List[() ->{C^} Unit]): () ->{} Unit =
18+
app[List[() ->{C^} Unit], Unit](ops, runOps) // error
19+
20+
21+
22+
23+
24+

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

+7
Original file line numberDiff line numberDiff line change
@@ -13,3 +13,10 @@
1313
| ^^^^^^^^^^^^^^^^^^^
1414
| The expression's type Res is not allowed to capture the root capability `cap` in its part box IO^.
1515
| This usually means that a capability persists longer than its allowed lifetime.
16+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21401.scala:17:67 ---------------------------------------
17+
17 | val x: Boxed[IO^] = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x) // error after adding addImplied widening
18+
| ^^^^^^
19+
| Found: (x: Boxed[box IO^?]^?) ->? Boxed[box IO^?]^?
20+
| Required: (x: Boxed[box IO^]) -> Boxed[box IO^]
21+
|
22+
| longer explanation available when compiling with `-explain`

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,6 @@ def mkRes(x: IO^): Res =
1414
def test2() =
1515
val a = usingIO[IO^](x => x) // error: The expression's type IO^ is not allowed to capture the root capability `cap`
1616
val leaked: [R, X <: Boxed[IO^] -> R] -> (op: X) -> R = usingIO[Res](mkRes) // error: The expression's type Res is not allowed to capture the root capability `cap` in its part box IO^
17-
val x: Boxed[IO^] = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x)
17+
val x: Boxed[IO^] = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x) // error after adding addImplied widening
1818
val y: IO^{x*} = x.unbox
1919
y.println("boom")

Diff for: ‎tests/neg-custom-args/captures/outer-var.check

+10
Original file line numberDiff line numberDiff line change
@@ -28,3 +28,13 @@
2828
| since at least one of their capture sets contains the root capability `cap`
2929
|
3030
| longer explanation available when compiling with `-explain`
31+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/outer-var.scala:16:65 ------------------------------------
32+
16 | var finalizeActions = collection.mutable.ListBuffer[() => Unit]() // error under addImplied widening
33+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
34+
|Found: scala.collection.mutable.ListBuffer[box () => Unit]^
35+
|Required: box scala.collection.mutable.ListBuffer[box () ->? Unit]^
36+
|
37+
|Note that scala.collection.mutable.ListBuffer[box () => Unit]^ cannot be box-converted to box scala.collection.mutable.ListBuffer[box () ->? Unit]^
38+
|since at least one of their capture sets contains the root capability `cap`
39+
|
40+
| longer explanation available when compiling with `-explain`

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,6 @@ def test(p: Proc, q: () => Unit) =
1313
y = (q: Proc) // error
1414
y = q // OK, was error under sealed
1515

16-
var finalizeActions = collection.mutable.ListBuffer[() => Unit]() // OK, was error under sealed
16+
var finalizeActions = collection.mutable.ListBuffer[() => Unit]() // error under addImplied widening
1717

1818

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

+4-9
Original file line numberDiff line numberDiff line change
@@ -25,16 +25,11 @@
2525
| ^^^^^^^^^^^^
2626
| The expression's type box () => Unit is not allowed to capture the root capability `cap`.
2727
| This usually means that a capability persists longer than its allowed lifetime.
28-
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:52:2 ---------------------------------------
28+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:52:27 --------------------------------------
2929
52 | val id: Id[Proc, Proc] = new Id[Proc, () -> Unit] // error
30-
| ^
31-
| Found: box () => Unit
32-
| Required: () => Unit
33-
|
34-
| Note that box () => Unit cannot be box-converted to () => Unit
35-
| since at least one of their capture sets contains the root capability `cap`
36-
53 | usingFile: f =>
37-
54 | id(() => f.write())
30+
| ^^^^^^^^^^^^^^^^^^^^^^^^
31+
| Found: Id[box () => Unit, () -> Unit]^
32+
| Required: Id[box () => Unit, box () => Unit]
3833
|
3934
| longer explanation available when compiling with `-explain`
4035
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:61:27 --------------------------------------

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

+8-10
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,8 @@
1-
-- Error: tests/neg-custom-args/captures/reaches2.scala:8:10 -----------------------------------------------------------
2-
8 | ps.map((x, y) => compose1(x, y)) // error // error
3-
| ^
4-
|reference ps* is not included in the allowed capture set {}
5-
|of an enclosing function literal with expected type ((box A ->{ps*} A, box A ->{ps*} A)) -> box (x$0: A^?) ->? (ex$15: caps.Exists) -> A^?
6-
-- Error: tests/neg-custom-args/captures/reaches2.scala:8:13 -----------------------------------------------------------
7-
8 | ps.map((x, y) => compose1(x, y)) // error // error
8-
| ^
9-
|reference ps* is not included in the allowed capture set {}
10-
|of an enclosing function literal with expected type ((box A ->{ps*} A, box A ->{ps*} A)) -> box (x$0: A^?) ->? (ex$15: caps.Exists) -> A^?
1+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches2.scala:8:10 --------------------------------------
2+
8 | ps.map((x, y) => compose1(x, y)) // error
3+
| ^^^^^^^^^^^^^^^^^^^^^^^
4+
|Found: (x$1: (box (x$0: A^?) ->? (ex$18: caps.Exists) -> A^?, box (x$0: A^?) ->? (ex$19: caps.Exists) -> A^?)^?) ->?
5+
| box (x$0: A^?) ->? A^?
6+
|Required: (x$1: (box A ->{ps*} A, box A ->{ps*} A)) -> box (x$0: A^?) ->? A^?
7+
|
8+
| longer explanation available when compiling with `-explain`

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -5,5 +5,5 @@ def compose1[A, B, C](f: A => B, g: B => C): A ->{f, g} C =
55
z => g(f(z))
66

77
def mapCompose[A](ps: List[(A => A, A => A)]): List[A ->{ps*} A] =
8-
ps.map((x, y) => compose1(x, y)) // error // error
8+
ps.map((x, y) => compose1(x, y)) // error
99

Diff for: ‎tests/neg/leak-problem.scala

+1-1
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ def test(): Unit =
2727
t1.read()
2828

2929
val xsLambda2 = () => useBoxedAsync2(xs)
30-
val _: () ->{xs*} Unit = xsLambda2
30+
val _: () ->{useBoxedAsync2, xs*} Unit = xsLambda2 // useBoxedAsync2 needed after adding addImplied widening
3131
val _: () -> Unit = xsLambda2 // error
3232

3333
val f: Box[Async^] => Unit = (x: Box[Async^]) => useBoxedAsync(x)

Diff for: ‎tests/pos-custom-args/captures/i20503.scala

+2-4
Original file line numberDiff line numberDiff line change
@@ -8,10 +8,8 @@ class List[+A]:
88
def nonEmpty: Boolean = ???
99

1010
def runOps(ops: List[() => Unit]): Unit =
11-
// See i20156, due to limitation in expressiveness of current system,
12-
// we could map over the list of impure elements. OK with existentials.
1311
ops.foreach(op => op())
1412

1513
def main(): Unit =
16-
val f: List[() => Unit] -> Unit = (ops: List[() => Unit]) => runOps(ops) // now ok
17-
val _: List[() => Unit] -> Unit = runOps // now ok
14+
val f: List[() => Unit] => Unit = (ops: List[() => Unit]) => runOps(ops)
15+
val _: List[() => Unit] => Unit = runOps

Diff for: ‎tests/pos-custom-args/captures/unsafe-unbox.scala

+2-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
import annotation.unchecked.uncheckedCaptures
22
def test =
3-
val finalizeActionsInit = collection.mutable.ListBuffer[(() => Unit) @uncheckedCaptures]()
3+
val finalizeActionsInit: (collection.mutable.ListBuffer[(() => Unit) @uncheckedCaptures]^) @uncheckedCaptures
4+
= collection.mutable.ListBuffer()
45
var finalizeActions = finalizeActionsInit
56
val action = finalizeActions.remove(0)
67

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

+9
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,12 @@ import caps.{CapSet, Capability}
44

55
@experimental object Test:
66

7+
class Set[T] extends Pure: // Define sets as `Pure` needed after adding addImplied widening
8+
def +[T](x: T): Set[T] = ???
9+
10+
object Set:
11+
def empty[T]: Set[T] = ???
12+
713
class Async extends Capability
814

915
def listener(async: Async): Listener^{async} = ???
@@ -28,5 +34,8 @@ import caps.{CapSet, Capability}
2834
others.map(listener).foreach(src.register)
2935
val ls = src.allListeners
3036
val _: Set[Listener^{async1, others*}] = ls
37+
// {ls, others*} would be added by addImplied here since sets are invariant
38+
// But this is suppressed since Set is now declared to be pure.
39+
3140

3241

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

+6
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,12 @@ import caps.{CapSet, Capability}
44

55
@experimental object Test:
66

7+
class Set[T] extends Pure: // Define sets as `Pure` needed after adding addImplied widening
8+
def +[T](x: T): Set[T] = ???
9+
10+
object Set:
11+
def empty[T]: Set[T] = ???
12+
713
class Label //extends Capability
814

915
class Listener

0 commit comments

Comments
 (0)