Skip to content

Commit

Permalink
Drop special handling in recheckApplication
Browse files Browse the repository at this point in the history
In recheckApplication we implemented a rule that computed the capture set of an
application `f(a)` by being the "better" of either the capture set of `f` union
capture set of `a` or the capture set of the result type of `f(a)`. This relies
on capture monotinicity, which we try to get away from. Also, it's semantically
dubious if the type of the argument `a` is a type variable that can be instantiated
to a capturing type as in the following example:
```scala
trait Iterator[+A]
  ...
  def flatMap[B](f: A => IterableOnce[B]^): Iterator[B]^{this, f}
```
Here, we account for every capability in `IterableOnce[B]^` already in `f`. But
those capabilities could also come from `A` if `A` is instantiated in the
actual function argument to a capturing type.

There was extensive breakage once the special handling was dropped. One example is
the `flatMap` definition above. We leave that as a potential soundness hold for now,
but the right way to fix `flatMap` would be by adding a capture set variable:
```scala
def flatMap[B, C^](f: A => IterableOnce[B]^{C^}): Iterator[B]^{this, f, C^}
```
The problem is that this currently cannot be done in a way that allows flatMap to be called
as before, passing a single type argument for `B`. We'd have to change the system to either
allow curried type parameters or optional type parameters for capture sets.

Another issue is that now more reach capabilities are registered as used by the enclosing method.
An example is lazylist-exceptions.scala, which has been moved to pending. Here, the use is spurious
because it happens inside an anonymous class creation on the right hand side of the method.
With refined use checking, the use would not propagate to the method, so the reach capability should
not be leaking. But to get there we need to implement refined use checking first.
  • Loading branch information
odersky committed Sep 27, 2024
1 parent 152710b commit cfb8314
Show file tree
Hide file tree
Showing 23 changed files with 90 additions and 41 deletions.
4 changes: 2 additions & 2 deletions compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
Original file line number Diff line number Diff line change
Expand Up @@ -640,8 +640,8 @@ object CapsOfApply:
class AnnotatedCapability(annot: Context ?=> ClassSymbol):
def apply(tp: Type)(using Context) =
AnnotatedType(tp, Annotation(annot, util.Spans.NoSpan))
def unapply(tree: AnnotatedType)(using Context): Option[SingletonCaptureRef] = tree match
case AnnotatedType(parent: SingletonCaptureRef, ann) if ann.symbol == annot => Some(parent)
def unapply(tree: AnnotatedType)(using Context): Option[CaptureRef] = tree match
case AnnotatedType(parent: CaptureRef, ann) if ann.symbol == annot => Some(parent)
case _ => None

/** An extractor for `ref @annotation.internal.reachCapability`, which is used to express
Expand Down
9 changes: 6 additions & 3 deletions compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
Original file line number Diff line number Diff line change
Expand Up @@ -581,7 +581,8 @@ class CheckCaptures extends Recheck, SymTransformer:
markFree(argType.deepCaptureSet, arg.srcPos)
argType

/** A specialized implementation of the apply rule.
/** CURRENTLY DISABLED:
* A specialized implementation of the apply rule.
*
* E |- q: Tq^Cq
* E |- q.f: Ta^Ca ->Cf Tr^Cr
Expand All @@ -604,6 +605,7 @@ class CheckCaptures extends Recheck, SymTransformer:
protected override
def recheckApplication(tree: Apply, qualType: Type, funType: MethodType, argTypes: List[Type])(using Context): Type =
val appType = Existential.toCap(super.recheckApplication(tree, qualType, funType, argTypes))
return appType
val qualCaptures = qualType.captureSet
val argCaptures =
for (arg, argType) <- tree.args.lazyZip(argTypes) yield
Expand Down Expand Up @@ -1150,10 +1152,11 @@ class CheckCaptures extends Recheck, SymTransformer:
eref match
case eref: ThisType if isPureContext(ctx.owner, eref.cls) =>
def isOuterRef(aref: Type): Boolean = aref match
case aref: TermRef =>
case aref: NamedType =>
val owner = aref.symbol.owner
if owner.isClass then isOuterRef(aref.prefix)
else eref.cls.isProperlyContainedIn(owner)
else
eref.cls.isProperlyContainedIn(owner)
case aref: ThisType => eref.cls.isProperlyContainedIn(aref.cls)
case _ => false
erefs ++ arefs.filter(isOuterRef)
Expand Down
6 changes: 4 additions & 2 deletions scala2-library-cc/src/scala/collection/Iterator.scala
Original file line number Diff line number Diff line change
Expand Up @@ -588,14 +588,16 @@ trait Iterator[+A] extends IterableOnce[A] with IterableOnceOps[A, Iterator, Ite
def next() = f(self.next())
}

// CC TODO This is unsafe. We will need to use a capture set variable:
// def flatMap[B][C^](f: A => IterableOnce[B]^{C^}): Iterator[B]^{this, f, C^}
def flatMap[B](f: A => IterableOnce[B]^): Iterator[B]^{this, f} = new AbstractIterator[B] {
private[this] var cur: Iterator[B]^{f} = Iterator.empty
/** Trillium logic boolean: -1 = unknown, 0 = false, 1 = true */
private[this] var _hasNext: Int = -1

private[this] def nextCur(): Unit = {
cur = null
cur = f(self.next()).iterator
cur = f(self.next()).iterator.asInstanceOf // CC cast needed once apply special handling is dropped
_hasNext = -1
}

Expand Down Expand Up @@ -1215,7 +1217,7 @@ object Iterator extends IterableFactory[Iterator] {
}

private[this] final class ConcatIteratorCell[A](head: => IterableOnce[A]^, var tail: ConcatIteratorCell[A]) {
def headIterator: Iterator[A]^{this} = head.iterator // CC todo: can't use {head} as capture set, gives "cannot establish a reference"
def headIterator: Iterator[A]^{this.head*} = head.iterator // CC todo: can't use {head} as capture set, gives "cannot establish a reference"
}

/** Creates a delegating iterator capped by a limit count. Negative limit means unbounded.
Expand Down
2 changes: 1 addition & 1 deletion scala2-library-cc/src/scala/collection/View.scala
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,7 @@ object View extends IterableFactory[View] {
* @tparam A View element type
*/
def fromIteratorProvider[A](it: () => Iterator[A]^): View[A]^{it} = new AbstractView[A] {
def iterator: Iterator[A]^{it} = it()
def iterator: Iterator[A]^{it} = it().asInstanceOf // CC TODO asInstanceOf needed once we drop special handling of apply
}

/**
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -1041,7 +1041,7 @@ object LazyListIterable extends IterableFactory[LazyListIterable] {
var itHasNext = false
var rest = restRef // var rest = restRef.elem
while (!itHasNext && !rest.isEmpty) {
it = f(rest.head).iterator
it = f(rest.head).iterator.asInstanceOf // CC TODO asInstanceOf needed once we drop special handling of apply
itHasNext = it.hasNext
if (!itHasNext) { // wait to advance `rest` because `it.next()` can throw
rest = rest.tail
Expand Down Expand Up @@ -1155,7 +1155,7 @@ object LazyListIterable extends IterableFactory[LazyListIterable] {
/** Creates a State from an Iterator, with another State appended after the Iterator
* is empty.
*/
private def stateFromIteratorConcatSuffix[A](it: Iterator[A]^)(suffix: => State[A]^): State[A]^{it, suffix} =
private def stateFromIteratorConcatSuffix[A, C^](it: Iterator[A]^)(suffix: => State[A]^{C^}): State[A]^{it, suffix, C^} =
if (it.hasNext) sCons(it.next(), newLL(stateFromIteratorConcatSuffix(it)(suffix)))
else suffix

Expand Down
4 changes: 3 additions & 1 deletion scala2-library-cc/src/scala/collection/mutable/Buffer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -184,7 +184,9 @@ trait IndexedBuffer[A] extends IndexedSeq[A]
var i = 0
val s = size
val newElems = new Array[(IterableOnce[A]^{f})](s)
while (i < s) { newElems(i) = f(this(i)); i += 1 }
while i < s do
newElems(i) = f(this(i)).asInstanceOf // CC TODO asInstanceOf needed once we drop special handling of apply
i += 1
clear()
i = 0
while (i < s) { ++=(newElems(i)); i += 1 }
Expand Down
13 changes: 13 additions & 0 deletions tests/neg-custom-args/captures/i21646.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
import language.experimental.captureChecking
import caps.Capability

trait File extends Capability

class Resource[T <: Capability](gen: T):
def use[U](f: T => U): U =
f(gen) // error

@main def run =
val myFile: File = ???
val r = Resource(myFile) // error
()
2 changes: 1 addition & 1 deletion tests/neg-custom-args/captures/inner-classes.scala
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ object test:
final class LazyCons[+T](val x: T, val xs: () => LazyList[T]^) extends LazyList[T]: // error
def isEmpty = false
def head = x
def tail: LazyList[T]^{this} = xs()
def tail: LazyList[T]^{this} = xs().asInstanceOf
end LazyCons

new LazyCons(1, () => LazyNil)
Expand Down
2 changes: 1 addition & 1 deletion tests/neg-custom-args/captures/lazylist.check
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylist.scala:17:15 -------------------------------------
17 | def tail = xs() // error
| ^^^^
| Found: lazylists.LazyList[T]^{LazyCons.this.xs}
| Found: lazylists.LazyList[T]^{LazyCons.this.xs*}
| Required: lazylists.LazyList[T]
|
| longer explanation available when compiling with `-explain`
Expand Down
4 changes: 2 additions & 2 deletions tests/neg-custom-args/captures/leaking-iterators.scala
Original file line number Diff line number Diff line change
Expand Up @@ -36,8 +36,8 @@ trait Iterator[+A] extends IterableOnce[A]:
def ++[B >: A](xs: IterableOnce[B]^): Iterator[B]^{this, xs}
end Iterator

private final class ConcatIteratorCell[A](head: => IterableOnce[A]^):
def headIterator: Iterator[A]^{this} = head.iterator
private final class ConcatIteratorCell[A, C^](head: => IterableOnce[A]^{C^}):
def headIterator: Iterator[A]^{this, C^} = head.iterator

def usingLogFile[R](op: FileOutputStream^ => R): R =
val logFile = FileOutputStream("log")
Expand Down
2 changes: 1 addition & 1 deletion tests/neg-custom-args/captures/reaches.check
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@
-- [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^
| ^^^^^
| Found: File^{f}
| Found: File^
| Required: File^{id*}
|
| longer explanation available when compiling with `-explain`
Expand Down
2 changes: 1 addition & 1 deletion tests/neg-custom-args/captures/refine-withFile.scala
Original file line number Diff line number Diff line change
Expand Up @@ -5,4 +5,4 @@ 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 leaked = g[File^{f*}]("test")(f => f) // error
20 changes: 20 additions & 0 deletions tests/neg-custom-args/captures/uses.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
class C
def test(x: C^, y: C^) =
class D {
println(x)
def foo() = println(y)
}
val d = D()
val _: D^{y} = d // error, should be ok
val _: D = d // error

val f = () => println(D())
val _: () ->{x} Unit = f // ok
val _: () -> Unit = f // should be error

def g = () =>
println(x)
() => println(y)
val _: () ->{x} () ->{y} Unit = g // error, should be ok
val _: () -> () -> Unit = g // error

2 changes: 1 addition & 1 deletion tests/neg/i19470.check
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
-- [E007] Type Mismatch Error: tests/neg/i19470.scala:9:12 -------------------------------------------------------------
9 | List(foo(f())) // error
| ^^^^^^^^
| Found: Inv[box IO^{f?}]
| Found: Inv[box IO^{f*?}]
| Required: box Inv[box IO^?]^?
|
| longer explanation available when compiling with `-explain`
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
// Needs better use handling
import language.experimental.saferExceptions

trait LazyList[+A]:
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -12,9 +12,9 @@ object LzyNil extends LzyList[Nothing]:
def head = ???
def tail = ???

final class LzyCons[+A](hd: A, tl: () => LzyList[A]^) extends LzyList[A]:
def LzyCons[A, C^](hd: A, tl: () => LzyList[A]^{C^}): LzyList[A]^{tl, C^} = new LzyList[A]:
private var forced = false
private var cache: LzyList[A @uncheckedCaptures]^{this} = uninitialized
private var cache: LzyList[A @uncheckedCaptures]^{this, C^} = uninitialized
private def force =
if !forced then { cache = tl(); forced = true }
cache
Expand Down
4 changes: 2 additions & 2 deletions tests/pos-custom-args/captures/iterators.scala
Original file line number Diff line number Diff line change
Expand Up @@ -13,8 +13,8 @@ abstract class Iterator[T]:
def next = f(thisIterator.next)
end Iterator

private[this] final class ConcatIteratorCell[A](head: => IterableOnce[A]^):
def headIterator: Iterator[A]^{this} = head.iterator
private[this] final class ConcatIteratorCell[A, C^](head: => IterableOnce[A]^{C^}):
def headIterator: Iterator[A]^{this, C^} = head.iterator

class C
type Cap = C^
Expand Down
6 changes: 3 additions & 3 deletions tests/pos-custom-args/captures/lazylists1.scala
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ object LazyNil extends LazyList[Nothing]:
def tail = ???
def concat[B](other: LazyList[B]^): LazyList[B]^{other} = other

final class LazyCons[+A](x: A)(xs: () => LazyList[A]^) extends LazyList[A]:
def LazyCons[A, C^](x: A)(xs: () => LazyList[A]^{C^}): LazyList[A]^{xs, C^} = new LazyList[A]:
def isEmpty = false
def head = x
def tail: LazyList[A]^{this} = xs()
Expand All @@ -30,10 +30,10 @@ def test(cap1: Cap, cap2: Cap) =
def f(x: String): String = if cap1 == cap1 then "" else "a"
def g(x: String): String = if cap2 == cap2 then "" else "a"

val xs = new LazyCons("")(() => if f("") == f("") then LazyNil else LazyNil)
val xs = LazyCons("")(() => if f("") == f("") then LazyNil else LazyNil)
val xsc: LazyList[String]^{cap1} = xs
val ys = xs.map(g)
val ysc: LazyList[String]^{cap1, cap2} = ys
val zs = new LazyCons("")(() => if g("") == g("") then LazyNil else LazyNil)
val zs = LazyCons("")(() => if g("") == g("") then LazyNil else LazyNil)
val as = xs.concat(zs)
val asc: LazyList[String]^{xs, zs} = as
12 changes: 6 additions & 6 deletions tests/pos-custom-args/captures/logger-tracked.scala
Original file line number Diff line number Diff line change
Expand Up @@ -26,14 +26,14 @@ object LazyNil extends LazyList[Nothing]:
def head = ???
def tail = ???

final class LazyCons[+T](val x: T, val xs: () => LazyList[T]^) extends LazyList[T]:
def isEmpty = false
def head = x
def tail: LazyList[T]^{this} = xs()
end LazyCons
def LazyCons[T, C^](x: T, xs: () => LazyList[T]^{C^}): LazyList[T]^{xs, C^} =
new LazyList[T]:
def isEmpty = false
def head = x
def tail: LazyList[T]^{this} = xs()

extension [A](x: A)
def #::(xs1: => LazyList[A]^): LazyList[A]^{xs1} =
def #::[C^](xs1: => LazyList[A]^{C^}): LazyList[A]^{xs1, C^} =
LazyCons(x, () => xs1)

extension [A](xs: LazyList[A]^)
Expand Down
12 changes: 6 additions & 6 deletions tests/pos-custom-args/captures/logger.scala
Original file line number Diff line number Diff line change
Expand Up @@ -26,14 +26,14 @@ object LazyNil extends LazyList[Nothing]:
def head = ???
def tail = ???

final class LazyCons[+T](val x: T, val xs: () => LazyList[T]^) extends LazyList[T]:
def isEmpty = false
def head = x
def tail: LazyList[T]^{this} = xs()
end LazyCons
def LazyCons[T, C^](x: T, xs: () => LazyList[T]^{C^}): LazyList[T]^{xs, C^} =
new LazyList[T]:
def isEmpty = false
def head = x
def tail: LazyList[T]^{this} = xs()

extension [A](x: A)
def #::(xs1: => LazyList[A]^): LazyList[A]^{xs1} =
def #::[C^](xs1: => LazyList[A]^{C^}): LazyList[A]^{xs1, C^} =
LazyCons(x, () => xs1)

extension [A](xs: LazyList[A]^)
Expand Down
2 changes: 1 addition & 1 deletion tests/pos-custom-args/captures/nested-classes-2.scala
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ def test1(x: (() => Unit)): Unit =

def test2(x1: (() => Unit), x2: (() => Unit) => Unit) =
class C1(x1: (() => Unit), xx2: (() => Unit) => Unit):
def c2(y1: (() => Unit), y2: (() => Unit) => Unit): C2^ = C2(y1, y2)
def c2(y1: (() => Unit), y2: (() => Unit) => Unit): C2^{y1, y2} = C2(y1, y2)
class C2(y1: (() => Unit), y2: (() => Unit) => Unit):
val a: (() => Unit) => (() => Unit) = f(y1)
a(x1) //OK, but should be error
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -433,8 +433,8 @@ object CollectionStrawMan5 {
}

object View {
def fromIterator[A](it: => Iterator[A]^): View[A]^{it} = new View[A]:
def iterator: Iterator[A]^{this} = it
def fromIterator[A, CI^](it: => Iterator[A]^{CI^}): View[A]^{it, CI^} = new View[A]:
def iterator: Iterator[A]^{this, CI^} = it

case object Empty extends View[Nothing] {
def iterator: Iterator[Nothing] = Iterator.empty
Expand Down Expand Up @@ -555,7 +555,15 @@ object CollectionStrawMan5 {
private var myCurrent: Iterator[B]^{this, f} = Iterator.empty
private def current = {
while (!myCurrent.hasNext && self.hasNext)
myCurrent = f(self.next()).iterator
myCurrent = f(self.next()).iterator.asInstanceOf
// TODO: This is actually unsafe, we need to use a capture set variable for `flatMap`, like this:
// def flatMap[B, C^](f: A => IterableOnce[B]^{C^}): Iterator[B]^{this, f, C^}
// but if we do this we get:
// Local reach capability C leaks into capture scope of method flatMap
// The problem is we can do this only if we upgrade use reasoning. The C capability
// is not used at the call of flatMap. It's used later in the iterator.
// So the correct type of `flatMap` that expresses this should be:
// def flatMap[B, C^](deferred f: A => IterableOnce[B]^{C^}): Iterator[B]^{this, f, C^}
myCurrent
}
def hasNext = current.hasNext
Expand Down

0 comments on commit cfb8314

Please sign in to comment.