Skip to content

Commit f2f1156

Browse files
authored
Two fixes to capture checking (#17524)
- It changes `isParamDependent` to consider `CaptureDependency` as well, so that when applying a capture dependent function the capture sets in the types of the remaining parameters will be correctly substituted. For example: ```scala def foo[X](x: Foo[X]^, op: () ->{x} Unit): Unit = ??? foo(a, useA) ``` After rechecking `a` in the argument list, the expected type of the second argument, `useA`, should become `() -> {a} Unit`. This example previously does not work. - It fixes #17517. It fixes the healing of capture sets, which happens at the end of the capture checking phase, in which we traverse the capture checked tree and try to heal the ill-formed capture sets in type arguments. Here we say a capture set `C` in a type argument is ill-formed if it contains `TermParamRef` bound by other lambdas. For example: ```scala def usingLogger[sealed T](f: OutputStream^)(op: Logger^{f} => T): T = ??? usingLogger[() ->?1 Unit](file)(l => () => l.log("test")) ``` `l` will be propagated to `?1` as a result of capture checking, which makes `?1` ill-formed and we should widen `l` to `file`. The problem is that we heal the capture sets one-after-another but the healing of a later capture set may propagate more `TermParamRef`s to a healed one. For example: ``` usingFile[() ->?2 Unit]( // should be error "foo", file => { usingLogger[() ->?1 Unit](file)(l => () => l.log("test")) } ) ``` After capture checking both `?1` and `?2` will be `{l}`. When traversing the tree we first heal `?2`, wherein we widen `l` to `file`, but `file` is a `TermRef` here and we do nothing. Then, only later when we heal `?1`, we also widen `l` to `file` but this will end up propagating a `TermParamRef` of `file` to `?2`, which we should have widened as well. But `?2` is already healed and is not inspected again. This PR solves this issue by installing a handler when healing the capture sets which will try to heal the new elements propagated later in the healing process.
2 parents c205a89 + 6870649 commit f2f1156

File tree

8 files changed

+60
-12
lines changed

8 files changed

+60
-12
lines changed

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

Lines changed: 14 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -275,6 +275,11 @@ sealed abstract class CaptureSet extends Showable:
275275
if isUniversal then handler()
276276
this
277277

278+
/** Invoke handler on the elements to check wellformedness of the capture set */
279+
def ensureWellformed(handler: List[CaptureRef] => Context ?=> Unit)(using Context): this.type =
280+
handler(elems.toList)
281+
this
282+
278283
/** An upper approximation of this capture set, i.e. a constant set that is
279284
* subcaptured by this set. If the current set is a variable
280285
* it is the intersection of all upper approximations of known supersets
@@ -375,6 +380,9 @@ object CaptureSet:
375380
/** A handler to be invoked if the root reference `cap` is added to this set */
376381
var rootAddedHandler: () => Context ?=> Unit = () => ()
377382

383+
/** A handler to be invoked when new elems are added to this set */
384+
var newElemAddedHandler: List[CaptureRef] => Context ?=> Unit = _ => ()
385+
378386
var description: String = ""
379387

380388
/** Record current elements in given VarState provided it does not yet
@@ -405,7 +413,8 @@ object CaptureSet:
405413
if !isConst && recordElemsState() then
406414
elems ++= newElems
407415
if isUniversal then rootAddedHandler()
408-
// assert(id != 2 || elems.size != 2, this)
416+
newElemAddedHandler(newElems.toList)
417+
// assert(id != 5 || elems.size != 3, this)
409418
(CompareResult.OK /: deps) { (r, dep) =>
410419
r.andAlso(dep.tryInclude(newElems, this))
411420
}
@@ -425,6 +434,10 @@ object CaptureSet:
425434
rootAddedHandler = handler
426435
super.disallowRootCapability(handler)
427436

437+
override def ensureWellformed(handler: List[CaptureRef] => (Context) ?=> Unit)(using Context): this.type =
438+
newElemAddedHandler = handler
439+
super.ensureWellformed(handler)
440+
428441
private var computingApprox = false
429442

430443
/** Roughly: the intersection of all constant known supersets of this set.

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

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -976,8 +976,11 @@ class CheckCaptures extends Recheck, SymTransformer:
976976
recur(refs, Nil)
977977

978978
private def healCaptureSet(cs: CaptureSet): Unit =
979-
val toInclude = widenParamRefs(cs.elems.toList.filter(!isAllowed(_)).asInstanceOf)
980-
toInclude.foreach(checkSubset(_, cs, tree.srcPos))
979+
def avoidance(elems: List[CaptureRef])(using Context): Unit =
980+
val toInclude = widenParamRefs(elems.filter(!isAllowed(_)).asInstanceOf)
981+
//println(i"HEAL $cs by widening to $toInclude")
982+
toInclude.foreach(checkSubset(_, cs, tree.srcPos))
983+
cs.ensureWellformed(avoidance)
981984

982985
private var allowed: SimpleIdentitySet[TermParamRef] = SimpleIdentitySet.empty
983986

compiler/src/dotty/tools/dotc/core/Types.scala

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3880,7 +3880,8 @@ object Types {
38803880
/** Does one of the parameter types contain references to earlier parameters
38813881
* of this method type which cannot be eliminated by de-aliasing?
38823882
*/
3883-
def isParamDependent(using Context): Boolean = paramDependencyStatus == TrueDeps
3883+
def isParamDependent(using Context): Boolean =
3884+
paramDependencyStatus == TrueDeps || paramDependencyStatus == CaptureDeps
38843885

38853886
/** Is there a dependency involving a reference in a capture set, but
38863887
* otherwise no true result dependency?
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
-- Error: tests/neg-custom-args/captures/usingLogFile-alt.scala:18:2 ---------------------------------------------------
2+
18 | usingFile( // error
3+
| ^^^^^^^^^
4+
| Sealed type variable T cannot be instantiated to box () => Unit since
5+
| that type captures the root capability `cap`.
6+
| This is often caused by a local capability in the body of method usingFile
7+
| leaking as part of its result.
Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
// Reported in issue #17517
2+
3+
import language.experimental.captureChecking
4+
import java.io.*
5+
6+
object Test:
7+
class Logger(f: OutputStream^):
8+
def log(msg: String): Unit = ???
9+
10+
def usingFile[sealed T](name: String, op: OutputStream^ => T): T =
11+
val f = new FileOutputStream(name)
12+
val result = op(f)
13+
f.close()
14+
result
15+
16+
def usingLogger[sealed T](f: OutputStream^)(op: Logger^{f} => T): T = ???
17+
18+
usingFile( // error
19+
"foo",
20+
file => {
21+
usingLogger(file)(l => () => l.log("test"))
22+
}
23+
)

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

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -45,10 +45,3 @@
4545
| that type captures the root capability `cap`.
4646
| This is often caused by a local capability in the body of method usingFile
4747
| leaking as part of its result.
48-
-- Error: tests/neg-custom-args/captures/usingLogFile.scala:72:6 -------------------------------------------------------
49-
72 | usingLogger(_, l => () => l.log("test"))) // error
50-
| ^^^^^^^^^^^
51-
| Sealed type variable T cannot be instantiated to box () => Unit since
52-
| that type captures the root capability `cap`.
53-
| This is often caused by a local capability in the body of method usingLogger
54-
| leaking as part of its result.

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -69,5 +69,5 @@ object Test4:
6969

7070
def test =
7171
val later = usingFile("logfile", // error
72-
usingLogger(_, l => () => l.log("test"))) // error
72+
usingLogger(_, l => () => l.log("test"))) // ok, since we can widen `l` to `file` instead of to `cap`
7373
later()
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
import language.experimental.captureChecking
2+
3+
trait Foo[T]
4+
def test(): Unit =
5+
val a: Foo[Int]^ = ???
6+
val useA: () ->{a} Unit = ???
7+
def foo[X](x: Foo[X]^, op: () ->{x} Unit): Unit = ???
8+
foo(a, useA)

0 commit comments

Comments
 (0)