Skip to content

Commit d7e4f94

Browse files
oderskyodersky
authored
Fix capture checking of dependent functions (#16264)
Fixes #15921. Capture checking can be unsound for dependent functions. Minimized example: ```scala trait Cap { def use(): Unit } def main() = { val f: (io: {*} Cap) -> {} () -> Unit = io => () => io.use() // should be an error val g: ({*} Cap) -> {} () -> Unit = io => () => io.use() // error, as expected } ``` In the above example, we issue an error for `g`, but not for `f`, which is unsound. The root cause of this issue is that in the `Typer` phase, we only create `InferredTypeTree` for the result type of function values when the expected type of the function literal is non-dependent; and later during `Setup` of the capture checking phase, we only create capture set variables and update the information of function symbols when its result type tree is an `InferredTypeTree`. To be more specific, the function literal `io => () => io.use()` in both `f` and `g` would be expaneded into the following tree in `Typer`: ```scala def $anonfun(io: {*} Cap): {} () -> Unit = { { def $anonfun(): Unit = { io.use() } closure($anonfun) } } closure($anonfun) ``` For `g`, where the expected type of the function literal is non-dependent, we would create capture set variables in `Setup` for the return type `{} () -> Unit` and update the symbol info of the outer `$anonfun`. For `f`, we would not do these things because `{} () -> Unit` is not an `InferredTypeTree`. This PR fixes this issue by typing the `DependentTypeTree` as an `InferredTypeTree` in the typer. ~Currently, although this PR fixes the soundness problem, it brings completeness issues, where sometimes we propagate the universal capability to some capture sets incorrectly, which prevents some positive test cases from being accepted. I am still investigating this issue and thus mark this PR as a draft for now.~ The completeness problem is fixed by two additional refinements: - preciser propagation of captured references through mapped instance (see [dd88672](dd88672)), - healing ill-formed type parameter capture sets (see [0e7d33a](0e7d33a)).
2 parents b4f8eef + c4240fb commit d7e4f94

File tree

12 files changed

+193
-45
lines changed

12 files changed

+193
-45
lines changed

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -546,7 +546,7 @@ object CaptureSet:
546546
else CompareResult.fail(this)
547547
}
548548
.andAlso {
549-
if (origin ne source) && mapIsIdempotent then
549+
if (origin ne source) && (origin ne initial) && mapIsIdempotent then
550550
// `tm` is idempotent, propagate back elems from image set.
551551
// This is sound, since we know that for `r in newElems: tm(r) = r`, hence
552552
// `r` is _one_ possible solution in `source` that would make an `r` appear in this set.

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

Lines changed: 87 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -606,11 +606,28 @@ class CheckCaptures extends Recheck, SymTransformer:
606606

607607
/** Massage `actual` and `expected` types using the methods below before checking conformance */
608608
override def checkConformsExpr(actual: Type, expected: Type, tree: Tree)(using Context): Unit =
609-
val expected1 = addOuterRefs(expected, actual)
609+
val expected1 = alignDependentFunction(addOuterRefs(expected, actual), actual.stripCapturing)
610610
val actual1 = adaptBoxed(actual, expected1, tree.srcPos)
611611
//println(i"check conforms $actual1 <<< $expected1")
612612
super.checkConformsExpr(actual1, expected1, tree)
613613

614+
private def toDepFun(args: List[Type], resultType: Type, isContextual: Boolean, isErased: Boolean)(using Context): Type =
615+
MethodType.companion(isContextual = isContextual, isErased = isErased)(args, resultType)
616+
.toFunctionType(isJava = false, alwaysDependent = true)
617+
618+
/** Turn `expected` into a dependent function when `actual` is dependent. */
619+
private def alignDependentFunction(expected: Type, actual: Type)(using Context): Type =
620+
def recur(expected: Type): Type = expected.dealias match
621+
case expected @ CapturingType(eparent, refs) =>
622+
CapturingType(recur(eparent), refs, boxed = expected.isBoxed)
623+
case expected @ defn.FunctionOf(args, resultType, isContextual, isErased)
624+
if defn.isNonRefinedFunction(expected) && defn.isFunctionType(actual) && !defn.isNonRefinedFunction(actual) =>
625+
val expected1 = toDepFun(args, resultType, isContextual, isErased)
626+
expected1
627+
case _ =>
628+
expected
629+
recur(expected)
630+
614631
/** For the expected type, implement the rule outlined in #14390:
615632
* - when checking an expression `a: Ca Ta` against an expected type `Ce Te`,
616633
* - where the capture set `Ce` contains Cls.this,
@@ -875,12 +892,79 @@ class CheckCaptures extends Recheck, SymTransformer:
875892
capt.println(i"checked $root with $selfType")
876893
end checkSelfTypes
877894

895+
/** Heal ill-formed capture sets in the type parameter.
896+
*
897+
* We can push parameter refs into a capture set in type parameters
898+
* that this type parameter can't see.
899+
* For example, when capture checking the following expression:
900+
*
901+
* def usingLogFile[T](op: (f: {*} File) => T): T = ...
902+
*
903+
* usingLogFile[box ?1 () -> Unit] { (f: {*} File) => () => { f.write(0) } }
904+
*
905+
* We may propagate `f` into ?1, making ?1 ill-formed.
906+
* This also causes soundness issues, since `f` in ?1 should be widened to `*`,
907+
* giving rise to an error that `*` cannot be included in a boxed capture set.
908+
*
909+
* To solve this, we still allow ?1 to capture parameter refs like `f`, but
910+
* compensate this by pushing the widened capture set of `f` into ?1.
911+
* This solves the soundness issue caused by the ill-formness of ?1.
912+
*/
913+
private def healTypeParam(tree: Tree)(using Context): Unit =
914+
val checker = new TypeTraverser:
915+
private def isAllowed(ref: CaptureRef): Boolean = ref match
916+
case ref: TermParamRef => allowed.contains(ref)
917+
case _ => true
918+
919+
// Widen the given term parameter refs x₁ : C₁ S₁ , ⋯ , xₙ : Cₙ Sₙ to their capture sets C₁ , ⋯ , Cₙ.
920+
//
921+
// If in these capture sets there are any capture references that are term parameter references we should avoid,
922+
// we will widen them recursively.
923+
private def widenParamRefs(refs: List[TermParamRef]): List[CaptureSet] =
924+
@scala.annotation.tailrec
925+
def recur(todos: List[TermParamRef], acc: List[CaptureSet]): List[CaptureSet] =
926+
todos match
927+
case Nil => acc
928+
case ref :: rem =>
929+
val cs = ref.captureSetOfInfo
930+
val nextAcc = cs.filter(isAllowed(_)) :: acc
931+
val nextRem: List[TermParamRef] = (cs.elems.toList.filter(!isAllowed(_)) ++ rem).asInstanceOf
932+
recur(nextRem, nextAcc)
933+
recur(refs, Nil)
934+
935+
private def healCaptureSet(cs: CaptureSet): Unit =
936+
val toInclude = widenParamRefs(cs.elems.toList.filter(!isAllowed(_)).asInstanceOf)
937+
toInclude.foreach(checkSubset(_, cs, tree.srcPos))
938+
939+
private var allowed: SimpleIdentitySet[TermParamRef] = SimpleIdentitySet.empty
940+
941+
def traverse(tp: Type) =
942+
tp match
943+
case CapturingType(parent, refs) =>
944+
healCaptureSet(refs)
945+
traverse(parent)
946+
case tp @ RefinedType(parent, rname, rinfo: MethodType) if defn.isFunctionType(tp) =>
947+
traverse(rinfo)
948+
case tp: TermLambda =>
949+
val saved = allowed
950+
try
951+
tp.paramRefs.foreach(allowed += _)
952+
traverseChildren(tp)
953+
finally allowed = saved
954+
case _ =>
955+
traverseChildren(tp)
956+
957+
if tree.isInstanceOf[InferredTypeTree] then
958+
checker.traverse(tree.knownType)
959+
end healTypeParam
960+
878961
/** Perform the following kinds of checks
879962
* - Check all explicitly written capturing types for well-formedness using `checkWellFormedPost`.
880963
* - Check that externally visible `val`s or `def`s have empty capture sets. If not,
881964
* suggest an explicit type. This is so that separate compilation (where external
882965
* symbols have empty capture sets) gives the same results as joint compilation.
883966
* - Check that arguments of TypeApplys and AppliedTypes conform to their bounds.
967+
* - Heal ill-formed capture sets of type parameters. See `healTypeParam`.
884968
*/
885969
def postCheck(unit: tpd.Tree)(using Context): Unit =
886970
unit.foreachSubTree {
@@ -933,6 +1017,8 @@ class CheckCaptures extends Recheck, SymTransformer:
9331017
}
9341018
checkBounds(normArgs, tl)
9351019
case _ =>
1020+
1021+
args.foreach(healTypeParam(_))
9361022
case _ =>
9371023
}
9381024
if !ctx.reporter.errorsReported then

‎compiler/src/dotty/tools/dotc/typer/Typer.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2938,7 +2938,7 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
29382938
case tree: untpd.TypedSplice => typedTypedSplice(tree)
29392939
case tree: untpd.UnApply => typedUnApply(tree, pt)
29402940
case tree: untpd.Tuple => typedTuple(tree, pt)
2941-
case tree: untpd.DependentTypeTree => completeTypeTree(untpd.TypeTree(), pt, tree)
2941+
case tree: untpd.DependentTypeTree => completeTypeTree(untpd.InferredTypeTree(), pt, tree)
29422942
case tree: untpd.InfixOp => typedInfixOp(tree, pt)
29432943
case tree: untpd.ParsedTry => typedTry(tree, pt)
29442944
case tree @ untpd.PostfixOp(qual, Ident(nme.WILDCARD)) => typedAsFunction(tree, pt)

‎tests/pos-custom-args/captures/boxmap.scala renamed to ‎tests/neg-custom-args/boxmap.scala

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,5 +15,7 @@ def lazymap[A <: Top, B <: Top](b: Box[A])(f: A => B): {f} (() -> Box[B]) =
1515
def test[A <: Top, B <: Top] =
1616
def lazymap[A <: Top, B <: Top](b: Box[A])(f: A => B) =
1717
() => b[Box[B]]((x: A) => box(f(x)))
18-
val x: (b: Box[A]) -> (f: A => B) -> (() -> Box[B]) = lazymap[A, B]
18+
val x0: (b: Box[A]) -> (f: A => B) -> (() -> Box[B]) = lazymap[A, B] // error
19+
val x: (b: Box[A]) -> (f: A => B) -> {b, f} (() -> Box[B]) = lazymap[A, B] // works
20+
val y: (b: Box[A]) -> (f: A => B) -> {*} (() -> Box[B]) = lazymap[A, B] // works
1921
()

‎tests/neg-custom-args/captures/byname.check

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@
88
10 | h(f2()) // error
99
| ^^^^
1010
| Found: {cap1} (x$0: Int) -> Int
11-
| Required: {cap2} Int -> Int
11+
| Required: {cap2} (x$0: Int) -> Int
1212
|
1313
| longer explanation available when compiling with `-explain`
1414
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/byname.scala:19:5 ----------------------------------------

‎tests/neg-custom-args/captures/cc-depfun.scala

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
trait Cap { def use(): Unit }
2+
3+
def main() = {
4+
val f: (io: {*} Cap) -> {} () -> Unit =
5+
io => () => io.use() // error
6+
7+
val g: ({*} Cap) -> {} () -> Unit =
8+
io => () => io.use() // error
9+
}

‎tests/neg-custom-args/captures/heal-tparam-cs.scala

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
import language.experimental.captureChecking
2+
3+
trait Cap { def use(): Unit }
4+
5+
def localCap[T](op: (cap: {*} Cap) => T): T = ???
6+
7+
def main(io: {*} Cap, net: {*} Cap): Unit = {
8+
val test1 = localCap { cap => // error
9+
() => { cap.use() }
10+
}
11+
12+
val test2: (cap: {*} Cap) -> {cap} () -> Unit =
13+
localCap { cap => // should work
14+
(cap1: {*} Cap) => () => { cap1.use() }
15+
}
16+
17+
val test3: (cap: {io} Cap) -> {io} () -> Unit =
18+
localCap { cap => // should work
19+
(cap1: {io} Cap) => () => { cap1.use() }
20+
}
21+
22+
val test4: (cap: {io} Cap) -> {net} () -> Unit =
23+
localCap { cap => // error
24+
(cap1: {io} Cap) => () => { cap1.use() }
25+
}
26+
27+
def localCap2[T](op: (cap: {io} Cap) => T): T = ???
28+
29+
val test5: {io} () -> Unit =
30+
localCap2 { cap => // ok
31+
() => { cap.use() }
32+
}
33+
}

‎tests/neg-custom-args/captures/i15921.scala

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
trait Stream { def close(): Unit = (); def write(x: Any): Unit = () }
2+
3+
object Test {
4+
def usingLogFile[T](op: (c: {*} Stream) => T): T =
5+
val logFile = new Stream { }
6+
val result = op(logFile)
7+
logFile.close()
8+
result
9+
10+
val later = usingLogFile { f => () => f.write(0) } // error
11+
later() // writing to closed file!
12+
}

‎tests/neg-custom-args/captures/try.check

Lines changed: 17 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
23 | val a = handle[Exception, CanThrow[Exception]] { // error
33
| ^
44
| Found: ? ({*} CT[Exception]) -> CanThrow[Exception]
5-
| Required: CanThrow[Exception] => box {*} CT[Exception]
5+
| Required: {*} CanThrow[Exception] -> box {*} CT[Exception]
66
24 | (x: CanThrow[Exception]) => x
77
25 | }{
88
|
@@ -11,11 +11,25 @@
1111
29 | val b = handle[Exception, () -> Nothing] { // error
1212
| ^
1313
| Found: ? (x: {*} CT[Exception]) -> {x} () -> Nothing
14-
| Required: CanThrow[Exception] => () -> Nothing
14+
| Required: {*} (x$0: CanThrow[Exception]) -> () -> Nothing
1515
30 | (x: CanThrow[Exception]) => () => raise(new Exception)(using x)
1616
31 | } {
1717
|
1818
| longer explanation available when compiling with `-explain`
19+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:52:2 -------------------------------------------
20+
47 |val global: () -> Int = handle {
21+
48 | (x: CanThrow[Exception]) =>
22+
49 | () =>
23+
50 | raise(new Exception)(using x)
24+
51 | 22
25+
52 |} { // error
26+
| ^
27+
| Found: {x$0} () -> Int
28+
| Required: () -> Int
29+
53 | (ex: Exception) => () => 22
30+
54 |}
31+
|
32+
| longer explanation available when compiling with `-explain`
1933
-- Error: tests/neg-custom-args/captures/try.scala:40:4 ----------------------------------------------------------------
2034
35 | val xx = handle {
2135
36 | (x: CanThrow[Exception]) =>
@@ -24,19 +38,7 @@
2438
39 | 22
2539
40 | } { // error
2640
| ^
27-
| The expression's type box {*} () -> Int is not allowed to capture the root capability `*`.
41+
| The expression's type box {x$0, *} () -> Int is not allowed to capture the root capability `*`.
2842
| This usually means that a capability persists longer than its allowed lifetime.
2943
41 | (ex: Exception) => () => 22
3044
42 | }
31-
-- Error: tests/neg-custom-args/captures/try.scala:52:2 ----------------------------------------------------------------
32-
47 |val global = handle {
33-
48 | (x: CanThrow[Exception]) =>
34-
49 | () =>
35-
50 | raise(new Exception)(using x)
36-
51 | 22
37-
52 |} { // error
38-
| ^
39-
| The expression's type box {*} () -> Int is not allowed to capture the root capability `*`.
40-
| This usually means that a capability persists longer than its allowed lifetime.
41-
53 | (ex: Exception) => () => 22
42-
54 |}

‎tests/neg-custom-args/captures/try.scala

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -44,11 +44,11 @@ def test =
4444
yy // OK
4545

4646

47-
val global = handle {
47+
val global: () -> Int = handle {
4848
(x: CanThrow[Exception]) =>
4949
() =>
5050
raise(new Exception)(using x)
5151
22
5252
} { // error
5353
(ex: Exception) => () => 22
54-
}
54+
}

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

Lines changed: 26 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,3 @@
1-
-- Error: tests/neg-custom-args/captures/usingLogFile.scala:23:27 ------------------------------------------------------
2-
23 | val later = usingLogFile { f => () => f.write(0) } // error
3-
| ^^^^^^^^^^^^^^^^^^^^^^^^^
4-
| {f} () -> Unit cannot be box-converted to box ? () -> Unit
5-
| since one of their capture sets contains the root capability `*`
6-
-- Error: tests/neg-custom-args/captures/usingLogFile.scala:29:9 -------------------------------------------------------
7-
29 | later2.x() // error
8-
| ^^^^^^^^
9-
| The expression's type box {*} () -> Unit is not allowed to capture the root capability `*`.
10-
| This usually means that a capability persists longer than its allowed lifetime.
111
-- Error: tests/neg-custom-args/captures/usingLogFile.scala:33:2 -------------------------------------------------------
122
33 | later3() // error
133
| ^^^^^^
@@ -18,18 +8,32 @@
188
| ^^^^^^^^
199
| The expression's type box {*} () -> Unit is not allowed to capture the root capability `*`.
2010
| This usually means that a capability persists longer than its allowed lifetime.
21-
-- Error: tests/neg-custom-args/captures/usingLogFile.scala:47:27 ------------------------------------------------------
11+
-- Error: tests/neg-custom-args/captures/usingLogFile.scala:23:6 -------------------------------------------------------
12+
23 | val later = usingLogFile { f => () => f.write(0) } // error
13+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
14+
| Non-local value later cannot have an inferred type
15+
| {x$0} () -> Unit
16+
| with non-empty capture set {x$0}.
17+
| The type needs to be declared explicitly.
18+
-- Error: tests/neg-custom-args/captures/usingLogFile.scala:29:9 -------------------------------------------------------
19+
29 | later2.x() // error
20+
| ^^^^^^^^
21+
| The expression's type box {x$0, *} () -> Unit is not allowed to capture the root capability `*`.
22+
| This usually means that a capability persists longer than its allowed lifetime.
23+
-- Error: tests/neg-custom-args/captures/usingLogFile.scala:47:6 -------------------------------------------------------
2224
47 | val later = usingLogFile { f => () => f.write(0) } // error
23-
| ^^^^^^^^^^^^^^^^^^^^^^^^^
24-
| {f} () -> Unit cannot be box-converted to box ? () -> Unit
25-
| since one of their capture sets contains the root capability `*`
26-
-- Error: tests/neg-custom-args/captures/usingLogFile.scala:62:33 ------------------------------------------------------
25+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
26+
| Non-local value later cannot have an inferred type
27+
| {x$0} () -> Unit
28+
| with non-empty capture set {x$0}.
29+
| The type needs to be declared explicitly.
30+
-- Error: tests/neg-custom-args/captures/usingLogFile.scala:62:25 ------------------------------------------------------
2731
62 | val later = usingFile("out", f => (y: Int) => xs.foreach(x => f.write(x + y))) // error
28-
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
29-
| {f} (x$0: Int) -> Unit cannot be box-converted to box ? (x$0: Int) -> Unit
30-
| since one of their capture sets contains the root capability `*`
31-
-- Error: tests/neg-custom-args/captures/usingLogFile.scala:71:37 ------------------------------------------------------
32+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
33+
| The expression's type box {x$0, *} (x$0: Int) -> Unit is not allowed to capture the root capability `*`.
34+
| This usually means that a capability persists longer than its allowed lifetime.
35+
-- Error: tests/neg-custom-args/captures/usingLogFile.scala:71:25 ------------------------------------------------------
3236
71 | val later = usingFile("logfile", usingLogger(_, l => () => l.log("test"))) // error
33-
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
34-
| {_$1} () -> Unit cannot be box-converted to box ? () -> Unit
35-
| since one of their capture sets contains the root capability `*`
37+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
38+
| The expression's type box {x$0, *} () -> Unit is not allowed to capture the root capability `*`.
39+
| This usually means that a capability persists longer than its allowed lifetime.

‎tests/neg-custom-args/captures/vars.check

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@
2525
-- Error: tests/neg-custom-args/captures/vars.scala:32:8 ---------------------------------------------------------------
2626
32 | local { cap3 => // error
2727
| ^
28-
| The expression's type box {*} (x$0: String) -> String is not allowed to capture the root capability `*`.
28+
| The expression's type box {x$0, *} (x$0: String) -> String is not allowed to capture the root capability `*`.
2929
| This usually means that a capability persists longer than its allowed lifetime.
3030
33 | def g(x: String): String = if cap3 == cap3 then "" else "a"
3131
34 | g

0 commit comments

Comments
 (0)