Skip to content

Commit

Permalink
Add implied captures in function types
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
odersky committed Oct 21, 2024
1 parent c6e3910 commit f6f996c
Show file tree
Hide file tree
Showing 22 changed files with 200 additions and 30 deletions.
8 changes: 8 additions & 0 deletions compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
Original file line number Diff line number Diff line change
Expand Up @@ -527,6 +527,14 @@ extension (tp: Type)
case _ =>
tp

/** Add implied captures as defined by `CaptureSet.addImplied`. */
def withImpliedCaptures(using Context): Type =
if tp.isValueType && !tp.isAlwaysPure then
val implied = CaptureSet.addImplied()(CaptureSet.empty, tp)
if !implied.isAlwaysEmpty then capt.println(i"Add implied $implied to $tp")
tp.capturing(implied)
else tp

def level(using Context): Level =
tp match
case tp: TermRef => tp.symbol.ccLevel
Expand Down
33 changes: 33 additions & 0 deletions compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
Original file line number Diff line number Diff line change
Expand Up @@ -1068,6 +1068,39 @@ object CaptureSet:
.showing(i"Deep capture set of $ref: ${ref1.widen} = $result", capt)
case _ => ofType(ref.underlying, followResult = true)

/** Add captures implied by a type. This means: if we have a contravarint, boxed
* capability in a function parameter and the capability is either `cap`, or a
* reach capability, or a capture set variable, add the same capability to the enclosing
* function arrow. For instance `List[() ->{ops*} Unit] -> Unit` would become
* `List[() ->{ops*} Unit] ->{ops*} Unit`. This is needed to make
* the `delayedRunops*.scala` tests produce errors.
* TODO: Investigate whether we can roll this into a widening rule like
*
* List[() ->{cap} Unit] -> Unit <: List[() ->{ops*} Unit] ->{ops*} Unit
*
* but not
*
* List[() ->{cap} Unit] -> Unit <: List[() ->{ops*} Unit] -> Unit
*
* It would mean that a reach capability can no longer be a subtype of `cap`.
*/
class addImplied(using Context) extends TypeAccumulator[CaptureSet]:
var boundVars: Set[CaptureRef] = Set.empty
def isImplied(tp: CaptureRef) =
(tp.isRootCapability || tp.isReach || tp.derivesFrom(defn.Caps_CapSet))
&& !boundVars.contains(tp.stripReach)
def apply(cs: CaptureSet, t: Type) = t match
case t @ CapturingType(parent, cs1) =>
val cs2 = this(cs, parent)
if variance <= 0 && t.isBoxed then cs2 ++ cs1.filter(isImplied)
else cs2
case t: MethodOrPoly =>
val saved = boundVars
boundVars ++= t.paramRefs.asInstanceOf[List[CaptureRef]]
try foldOver(cs, t) finally boundVars = saved
case _ =>
foldOver(cs, t)

/** Capture set of a type */
def ofType(tp: Type, followResult: Boolean)(using Context): CaptureSet =
def recur(tp: Type): CaptureSet = trace(i"ofType $tp, ${tp.getClass} $followResult", show = true):
Expand Down
2 changes: 1 addition & 1 deletion compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
Original file line number Diff line number Diff line change
Expand Up @@ -1292,7 +1292,7 @@ class CheckCaptures extends Recheck, SymTransformer:
else
val widened = improveCaptures(actual.widen.dealiasKeepAnnots, actual)
val adapted = adaptBoxed(
widened.withReachCaptures(actual), expected, pos,
widened.withReachCaptures(actual).withImpliedCaptures, expected, pos,
covariant = true, alwaysConst = false, boxErrors)
if adapted eq widened then actual
else adapted.showing(i"adapt boxed $actual vs $expected = $adapted", capt)
Expand Down
2 changes: 1 addition & 1 deletion scala2-library-cc/src/scala/collection/SeqView.scala
Original file line number Diff line number Diff line change
Expand Up @@ -212,7 +212,7 @@ object SeqView {
override def sorted[B1 >: A](implicit ord1: Ordering[B1]): SeqView[A]^{this} =
if (ord1 == Sorted.this.ord) outer.unsafeAssumePure
else if (ord1.isReverseOf(Sorted.this.ord)) this
else new Sorted(elems, len, ord1)
else new Sorted(elems, len, ord1).asInstanceOf // !!! asInstanceOf needed after adding addImplied widening
}

@volatile private[this] var evaluated = false
Expand Down
14 changes: 14 additions & 0 deletions tests/neg-custom-args/captures/delayedRunops2.check
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/delayedRunops2.scala:10:35 -------------------------------
10 | app[List[() ->{ops*} Unit], Unit](ops, runOps) // error
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
| Found: () ->{ops*} Unit
| Required: () -> Unit
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/delayedRunops2.scala:18:36 -------------------------------
18 | app2[List[() => Unit], Unit](ops, runOps: List[() => Unit] -> Unit) // error
| ^^^^^^
| Found: (ops: List[box () ->? Unit]^?) ->? Unit
| Required: (ops: List[box () => Unit]) -> Unit
|
| longer explanation available when compiling with `-explain`
22 changes: 22 additions & 0 deletions tests/neg-custom-args/captures/delayedRunops2.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
import language.experimental.captureChecking

def runOps(ops: List[() => Unit]): Unit =
ops.foreach(op => op())

def app[T, U](x: T, op: T => U): () ->{op} U =
() => op(x)

def unsafeRunOps(ops: List[() => Unit]): () ->{} Unit =
app[List[() ->{ops*} Unit], Unit](ops, runOps) // error

def app2[T, U](x: T, op: T => U): () ->{op} U =
() =>
def y: T = x
op(y)

def unsafeRunOps2(ops: List[() => Unit]): () -> Unit =
app2[List[() => Unit], Unit](ops, runOps: List[() => Unit] -> Unit) // error




10 changes: 10 additions & 0 deletions tests/neg-custom-args/captures/delayedRunops3.check
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/delayedRunops3.scala:10:41 -------------------------------
10 | app[List[() ->{ops*} Unit], Unit](ops, runOps) // error
| ^^^^^^
| Found: (ops: List[box () ->? Unit]^?) ->? Unit
| Required: (ops: List[box () ->{ops²*} Unit]) -> Unit
|
| where: ops is a reference to a value parameter
| ops² is a parameter in method unsafeRunOps
|
| longer explanation available when compiling with `-explain`
14 changes: 14 additions & 0 deletions tests/neg-custom-args/captures/delayedRunops3.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
import language.experimental.captureChecking

def runOps(ops: List[() => Unit]): Unit =
ops.foreach(op => op())

def app[T, U](x: T, op: T -> U): () ->{} U =
() => op(x)

def unsafeRunOps(ops: List[() => Unit]): () ->{} Unit =
app[List[() ->{ops*} Unit], Unit](ops, runOps) // error




21 changes: 21 additions & 0 deletions tests/neg-custom-args/captures/delayedRunops4.check
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/delayedRunops4.scala:11:4 --------------------------------
11 | runOps[C]: List[() ->{C^} Unit] ->{C^} Unit) // error
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
| Found: List[box () ->{C^} Unit] ->{C^} Unit
| Required: List[box () ->{C^} Unit] -> Unit
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/delayedRunops4.scala:15:43 -------------------------------
15 | app[List[() ->{C^} Unit], Unit](ops, rops[C]) // error
| ^^^^^^^
| Found: (ops: List[box () ->{C^} Unit]) ->{C^} Unit
| Required: (ops: List[box () ->{C^} Unit]) -> Unit
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/delayedRunops4.scala:18:39 -------------------------------
18 | app[List[() ->{C^} Unit], Unit](ops, runOps) // error
| ^^^^^^
| Found: (ops: List[box () ->? Unit]^?) ->? Unit
| Required: (ops: List[box () ->{C^} Unit]) -> Unit
|
| longer explanation available when compiling with `-explain`
24 changes: 24 additions & 0 deletions tests/neg-custom-args/captures/delayedRunops4.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
import language.experimental.captureChecking

def runOps[C^](ops: List[() ->{C^} Unit]): Unit =
ops.foreach(op => op())

def app[T, U](x: T, op: T -> U): () ->{} U =
() => op(x)

def unsafeRunOps[C^](ops: List[() ->{C^} Unit]): () ->{} Unit =
app[List[() ->{C^} Unit], Unit](ops,
runOps[C]: List[() ->{C^} Unit] ->{C^} Unit) // error

def unsafeRunOps2[C^](ops: List[() ->{C^} Unit]): () ->{} Unit =
def rops[D^]: (ops: List[() ->{D^} Unit]) -> Unit = ???
app[List[() ->{C^} Unit], Unit](ops, rops[C]) // error

def unsafeRunOps3[C^](ops: List[() ->{C^} Unit]): () ->{} Unit =
app[List[() ->{C^} Unit], Unit](ops, runOps) // error






7 changes: 7 additions & 0 deletions tests/neg-custom-args/captures/i21401.check
Original file line number Diff line number Diff line change
Expand Up @@ -13,3 +13,10 @@
| ^^^^^^^^^^^^^^^^^^^
| The expression's type Res is not allowed to capture the root capability `cap` in its part box IO^.
| This usually means that a capability persists longer than its allowed lifetime.
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21401.scala:17:67 ---------------------------------------
17 | val x: Boxed[IO^] = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x) // error after adding addImplied widening
| ^^^^^^
| Found: (x: Boxed[box IO^?]^?) ->? Boxed[box IO^?]^?
| Required: (x: Boxed[box IO^]) -> Boxed[box IO^]
|
| longer explanation available when compiling with `-explain`
2 changes: 1 addition & 1 deletion tests/neg-custom-args/captures/i21401.scala
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,6 @@ def mkRes(x: IO^): Res =
def test2() =
val a = usingIO[IO^](x => x) // error: The expression's type IO^ is not allowed to capture the root capability `cap`
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^
val x: Boxed[IO^] = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x)
val x: Boxed[IO^] = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x) // error after adding addImplied widening
val y: IO^{x*} = x.unbox
y.println("boom")
10 changes: 10 additions & 0 deletions tests/neg-custom-args/captures/outer-var.check
Original file line number Diff line number Diff line change
Expand Up @@ -28,3 +28,13 @@
| since at least one of their capture sets contains the root capability `cap`
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/outer-var.scala:16:65 ------------------------------------
16 | var finalizeActions = collection.mutable.ListBuffer[() => Unit]() // error under addImplied widening
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|Found: scala.collection.mutable.ListBuffer[box () => Unit]^
|Required: box scala.collection.mutable.ListBuffer[box () ->? Unit]^
|
|Note that scala.collection.mutable.ListBuffer[box () => Unit]^ cannot be box-converted to box scala.collection.mutable.ListBuffer[box () ->? Unit]^
|since at least one of their capture sets contains the root capability `cap`
|
| longer explanation available when compiling with `-explain`
2 changes: 1 addition & 1 deletion tests/neg-custom-args/captures/outer-var.scala
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,6 @@ def test(p: Proc, q: () => Unit) =
y = (q: Proc) // error
y = q // OK, was error under sealed

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


13 changes: 4 additions & 9 deletions tests/neg-custom-args/captures/reaches.check
Original file line number Diff line number Diff line change
Expand Up @@ -25,16 +25,11 @@
| ^^^^^^^^^^^^
| The expression's type box () => Unit is not allowed to capture the root capability `cap`.
| This usually means that a capability persists longer than its allowed lifetime.
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:52:2 ---------------------------------------
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:52:27 --------------------------------------
52 | val id: Id[Proc, Proc] = new Id[Proc, () -> Unit] // error
| ^
| Found: box () => Unit
| Required: () => Unit
|
| Note that box () => Unit cannot be box-converted to () => Unit
| since at least one of their capture sets contains the root capability `cap`
53 | usingFile: f =>
54 | id(() => f.write())
| ^^^^^^^^^^^^^^^^^^^^^^^^
| Found: Id[box () => Unit, () -> Unit]^
| Required: Id[box () => Unit, box () => Unit]
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:61:27 --------------------------------------
Expand Down
18 changes: 8 additions & 10 deletions tests/neg-custom-args/captures/reaches2.check
Original file line number Diff line number Diff line change
@@ -1,10 +1,8 @@
-- Error: tests/neg-custom-args/captures/reaches2.scala:8:10 -----------------------------------------------------------
8 | ps.map((x, y) => compose1(x, y)) // error // error
| ^
|reference ps* is not included in the allowed capture set {}
|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^?
-- Error: tests/neg-custom-args/captures/reaches2.scala:8:13 -----------------------------------------------------------
8 | ps.map((x, y) => compose1(x, y)) // error // error
| ^
|reference ps* is not included in the allowed capture set {}
|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^?
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches2.scala:8:10 --------------------------------------
8 | ps.map((x, y) => compose1(x, y)) // error
| ^^^^^^^^^^^^^^^^^^^^^^^
|Found: (x$1: (box (x$0: A^?) ->? (ex$18: caps.Exists) -> A^?, box (x$0: A^?) ->? (ex$19: caps.Exists) -> A^?)^?) ->?
| box (x$0: A^?) ->? A^?
|Required: (x$1: (box A ->{ps*} A, box A ->{ps*} A)) -> box (x$0: A^?) ->? A^?
|
| longer explanation available when compiling with `-explain`
2 changes: 1 addition & 1 deletion tests/neg-custom-args/captures/reaches2.scala
Original file line number Diff line number Diff line change
Expand Up @@ -5,5 +5,5 @@ def compose1[A, B, C](f: A => B, g: B => C): A ->{f, g} C =
z => g(f(z))

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

2 changes: 1 addition & 1 deletion tests/neg/leak-problem.scala
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ def test(): Unit =
t1.read()

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

val f: Box[Async^] => Unit = (x: Box[Async^]) => useBoxedAsync(x)
Expand Down
6 changes: 2 additions & 4 deletions tests/pos-custom-args/captures/i20503.scala
Original file line number Diff line number Diff line change
Expand Up @@ -8,10 +8,8 @@ class List[+A]:
def nonEmpty: Boolean = ???

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

def main(): Unit =
val f: List[() => Unit] -> Unit = (ops: List[() => Unit]) => runOps(ops) // now ok
val _: List[() => Unit] -> Unit = runOps // now ok
val f: List[() => Unit] => Unit = (ops: List[() => Unit]) => runOps(ops)
val _: List[() => Unit] => Unit = runOps
3 changes: 2 additions & 1 deletion tests/pos-custom-args/captures/unsafe-unbox.scala
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
import annotation.unchecked.uncheckedCaptures
def test =
val finalizeActionsInit = collection.mutable.ListBuffer[(() => Unit) @uncheckedCaptures]()
val finalizeActionsInit: (collection.mutable.ListBuffer[(() => Unit) @uncheckedCaptures]^) @uncheckedCaptures
= collection.mutable.ListBuffer()
var finalizeActions = finalizeActionsInit
val action = finalizeActions.remove(0)

Expand Down
9 changes: 9 additions & 0 deletions tests/pos/cc-poly-source-capability.scala
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,12 @@ import caps.{CapSet, Capability}

@experimental object Test:

class Set[T] extends Pure: // Define sets as `Pure` needed after adding addImplied widening
def +[T](x: T): Set[T] = ???

object Set:
def empty[T]: Set[T] = ???

class Async extends Capability

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



6 changes: 6 additions & 0 deletions tests/pos/cc-poly-source.scala
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,12 @@ import caps.{CapSet, Capability}

@experimental object Test:

class Set[T] extends Pure: // Define sets as `Pure` needed after adding addImplied widening
def +[T](x: T): Set[T] = ???

object Set:
def empty[T]: Set[T] = ???

class Label //extends Capability

class Listener
Expand Down

0 comments on commit f6f996c

Please sign in to comment.