From bae5b972eb7cc4aff76703bb7a47bd2ac28d39dd Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Fri, 28 Oct 2022 13:40:22 +0200 Subject: [PATCH 01/16] type DependentTypeTree as an inferred type --- compiler/src/dotty/tools/dotc/typer/Typer.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala index 33638df54fb1..0a0e1403f208 100644 --- a/compiler/src/dotty/tools/dotc/typer/Typer.scala +++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala @@ -2930,7 +2930,7 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer case tree: untpd.TypedSplice => typedTypedSplice(tree) case tree: untpd.UnApply => typedUnApply(tree, pt) case tree: untpd.Tuple => typedTuple(tree, pt) - case tree: untpd.DependentTypeTree => completeTypeTree(untpd.TypeTree(), pt, tree) + case tree: untpd.DependentTypeTree => completeTypeTree(untpd.InferredTypeTree(), pt, tree) case tree: untpd.InfixOp => typedInfixOp(tree, pt) case tree: untpd.ParsedTry => typedTry(tree, pt) case tree @ untpd.PostfixOp(qual, Ident(nme.WILDCARD)) => typedAsFunction(tree, pt) From 8c9090855b4df790e9e5bf9253e4bc35416e74f8 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 31 Oct 2022 12:33:27 +0100 Subject: [PATCH 02/16] add testcase for #15921 --- tests/neg-custom-args/captures/i15921.scala | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 tests/neg-custom-args/captures/i15921.scala diff --git a/tests/neg-custom-args/captures/i15921.scala b/tests/neg-custom-args/captures/i15921.scala new file mode 100644 index 000000000000..291673746e33 --- /dev/null +++ b/tests/neg-custom-args/captures/i15921.scala @@ -0,0 +1,12 @@ +trait Stream { def close(): Unit = (); def write(x: Any): Unit = () } + +object Test { + def usingLogFile[T](op: (c: {*} Stream) => T): T = + val logFile = new Stream { } + val result = op(logFile) + logFile.close() + result + + val later = usingLogFile { f => () => f.write(0) } // error + later() // writing to closed file! +} From 18222b75b9db6d931bf57e11ab11ac152fdd759f Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 31 Oct 2022 13:16:01 +0100 Subject: [PATCH 03/16] tweak tests, add limitation errors After the fix of the soundness issue, sometimes we infer universal capabilities where it is not necessary. This results in completeness issues. --- .../captures => neg-custom-args}/boxmap.scala | 4 +++- .../captures/lazyref-pos.scala} | 2 +- tests/neg-custom-args/captures/lazyref.check | 8 ++++++++ tests/neg-custom-args/captures/lazyref.scala | 2 +- 4 files changed, 13 insertions(+), 3 deletions(-) rename tests/{pos-custom-args/captures => neg-custom-args}/boxmap.scala (66%) rename tests/{pos-custom-args/captures/lazyref.scala => neg-custom-args/captures/lazyref-pos.scala} (93%) diff --git a/tests/pos-custom-args/captures/boxmap.scala b/tests/neg-custom-args/boxmap.scala similarity index 66% rename from tests/pos-custom-args/captures/boxmap.scala rename to tests/neg-custom-args/boxmap.scala index 18baabd4e584..340f9cfe820f 100644 --- a/tests/pos-custom-args/captures/boxmap.scala +++ b/tests/neg-custom-args/boxmap.scala @@ -15,5 +15,7 @@ def lazymap[A <: Top, B <: Top](b: Box[A])(f: A => B): {f} (() -> Box[B]) = def test[A <: Top, B <: Top] = def lazymap[A <: Top, B <: Top](b: Box[A])(f: A => B) = () => b[Box[B]]((x: A) => box(f(x))) - val x: (b: Box[A]) -> (f: A => B) -> (() -> Box[B]) = lazymap[A, B] + val x0: (b: Box[A]) -> (f: A => B) -> (() -> Box[B]) = lazymap[A, B] // error + val x: (b: Box[A]) -> (f: A => B) -> {f} (() -> Box[B]) = lazymap[A, B] // error // limitation + val y: (b: Box[A]) -> (f: A => B) -> {*} (() -> Box[B]) = lazymap[A, B] // works () diff --git a/tests/pos-custom-args/captures/lazyref.scala b/tests/neg-custom-args/captures/lazyref-pos.scala similarity index 93% rename from tests/pos-custom-args/captures/lazyref.scala rename to tests/neg-custom-args/captures/lazyref-pos.scala index 0d988dc3e17b..8ff394934a04 100644 --- a/tests/pos-custom-args/captures/lazyref.scala +++ b/tests/neg-custom-args/captures/lazyref-pos.scala @@ -9,7 +9,7 @@ def map[A, B](ref: {*} LazyRef[A], f: A => B): {f, ref} LazyRef[B] = new LazyRef(() => f(ref.elem())) def mapc[A, B]: (ref: {*} LazyRef[A], f: A => B) => {f, ref} LazyRef[B] = - (ref1, f1) => map[A, B](ref1, f1) + (ref1, f1) => map[A, B](ref1, f1) // error // limitation def test(cap1: Cap, cap2: Cap) = def f(x: Int) = if cap1 == cap1 then x else 0 diff --git a/tests/neg-custom-args/captures/lazyref.check b/tests/neg-custom-args/captures/lazyref.check index fcd98d0d67bd..2a3b013af6fb 100644 --- a/tests/neg-custom-args/captures/lazyref.check +++ b/tests/neg-custom-args/captures/lazyref.check @@ -1,3 +1,11 @@ +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazyref.scala:13:2 --------------------------------------- +13 | (ref1, f1) => map[A, B](ref1, f1) // error // limitation + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | Found: ? (ref1: {*} LazyRef[? A]{elem: {*} () -> box ? A}, f1: {*} (x$0: ? A) -> ? B) -> + | {f1, ref1, *} LazyRef[? B]{elem: {*} () -> box ? B} + | Required: (ref: {*} LazyRef[A], f: A => B) -> {f, ref} LazyRef[B] + | + | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazyref.scala:19:28 -------------------------------------- 19 | val ref1c: LazyRef[Int] = ref1 // error | ^^^^ diff --git a/tests/neg-custom-args/captures/lazyref.scala b/tests/neg-custom-args/captures/lazyref.scala index 8395e5cb42cd..e7e1be9d1624 100644 --- a/tests/neg-custom-args/captures/lazyref.scala +++ b/tests/neg-custom-args/captures/lazyref.scala @@ -10,7 +10,7 @@ def map[A, B](ref: {*} LazyRef[A], f: A => B): {f, ref} LazyRef[B] = new LazyRef(() => f(ref.elem())) def mapc[A, B]: (ref: {*} LazyRef[A], f: A => B) -> {f, ref} LazyRef[B] = - (ref1, f1) => map[A, B](ref1, f1) + (ref1, f1) => map[A, B](ref1, f1) // error // limitation def test(cap1: Cap, cap2: Cap) = def f(x: Int) = if cap1 == cap1 then x else 0 From 7e695fddac47cc56234fe76c390689c182fad76d Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 31 Oct 2022 14:25:12 +0100 Subject: [PATCH 04/16] one more test case for capture checking dependent functions --- tests/neg-custom-args/captures/cc-depfun.scala | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 tests/neg-custom-args/captures/cc-depfun.scala diff --git a/tests/neg-custom-args/captures/cc-depfun.scala b/tests/neg-custom-args/captures/cc-depfun.scala new file mode 100644 index 000000000000..c4ef303f4712 --- /dev/null +++ b/tests/neg-custom-args/captures/cc-depfun.scala @@ -0,0 +1,9 @@ +trait Cap { def use(): Unit } + +def main() = { + val f: (io: {*} Cap) -> {} () -> Unit = + io => () => io.use() // error + + val g: ({*} Cap) -> {} () -> Unit = + io => () => io.use() // error +} From dd88672e122293a007401a83f467378baa7c93c9 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Thu, 10 Nov 2022 23:07:55 +0100 Subject: [PATCH 05/16] refine propagation for idempotent maps MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit For an idempotent map f and a set C, we do not need to propagate x ∈ f(C) back to C when x comes from f(y) for some y ∈ C. --- compiler/src/dotty/tools/dotc/cc/CaptureSet.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index 6bf6d7770d8b..02144d69b151 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala @@ -546,7 +546,7 @@ object CaptureSet: else CompareResult.fail(this) } .andAlso { - if (origin ne source) && mapIsIdempotent then + if (origin ne source) && (origin ne initial) && mapIsIdempotent then // `tm` is idempotent, propagate back elems from image set. // This is sound, since we know that for `r in newElems: tm(r) = r`, hence // `r` is _one_ possible solution in `source` that would make an `r` appear in this set. From f45e083c6f22c2fd0e0a7713889f37ffd7299b01 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Thu, 10 Nov 2022 23:13:09 +0100 Subject: [PATCH 06/16] make expected function type dependent when the actual type is dependent So that TypeComparer can propagate the capture sets correctly. --- .../dotty/tools/dotc/cc/CheckCaptures.scala | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 899914e872c8..874ad544d0d1 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -606,11 +606,27 @@ class CheckCaptures extends Recheck, SymTransformer: /** Massage `actual` and `expected` types using the methods below before checking conformance */ override def checkConformsExpr(actual: Type, expected: Type, tree: Tree)(using Context): Unit = - val expected1 = addOuterRefs(expected, actual) + val expected1 = makeFunctionDependent(addOuterRefs(expected, actual), actual.stripCapturing) val actual1 = adaptBoxed(actual, expected1, tree.srcPos) //println(i"check conforms $actual1 <<< $expected1") super.checkConformsExpr(actual1, expected1, tree) + private def toDepFun(args: List[Type], resultType: Type, isContextual: Boolean, isErased: Boolean)(using Context): Type = + MethodType.companion(isContextual = isContextual, isErased = isErased)(args, resultType) + .toFunctionType(isJava = false, alwaysDependent = true) + + private def makeFunctionDependent(expected: Type, actual: Type)(using Context): Type = + def recur(expected: Type): Type = expected.dealias match + case expected @ CapturingType(eparent, refs) => + CapturingType(recur(eparent), refs, boxed = expected.isBoxed) + case expected @ defn.FunctionOf(args, resultType, isContextual, isErased) + if defn.isNonRefinedFunction(expected) && defn.isFunctionType(actual) && !defn.isNonRefinedFunction(actual) => + val expected1 = toDepFun(args, resultType, isContextual, isErased) + expected1 + case _ => + expected + recur(expected) + /** For the expected type, implement the rule outlined in #14390: * - when checking an expression `a: Ca Ta` against an expected type `Ce Te`, * - where the capture set `Ce` contains Cls.this, From 62975d3d421f6568cfb3a43856396de9cc2a2358 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Thu, 10 Nov 2022 23:16:50 +0100 Subject: [PATCH 07/16] heal ill-formed capture sets in type parameters Given an applied function `f[cs A](g)`, where the type of `f` is `[T] -> (x: {*} C) -> T` and the type of `g` is dependent, e.g. `(x: {*} Cap) -> {x} A`, the reference `x` may be propagate to cs. But this makes `cs A` ill-formed since it is not allowed to mention `{x}`. This sometimes cause soundness problems. We heal this by pushing the capture set of `{x}` into cs. --- .../dotty/tools/dotc/cc/CheckCaptures.scala | 31 +++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 874ad544d0d1..d86b91beb7c4 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -891,6 +891,24 @@ class CheckCaptures extends Recheck, SymTransformer: capt.println(i"checked $root with $selfType") end checkSelfTypes + private def healTypeParamCaptureSet(cs: CaptureSet)(using Context) = { + def avoidParam(tpr: TermParamRef): List[CaptureSet] = + val refs = tpr.binder.paramInfos(tpr.paramNum).captureSet + refs.filter(!_.isInstanceOf[TermParamRef]) :: refs.elems.toList.flatMap { + case tpr: TermParamRef => avoidParam(tpr) + case _ => Nil + } + + val widenedSets = cs.elems.toList flatMap { + case tpr: TermParamRef => avoidParam(tpr) + case _ => Nil + } + + widenedSets foreach { cs1 => + cs1.subCaptures(cs, frozen = false) + } + } + /** Perform the following kinds of checks * - Check all explicitly written capturing types for well-formedness using `checkWellFormedPost`. * - Check that externally visible `val`s or `def`s have empty capture sets. If not, @@ -949,6 +967,19 @@ class CheckCaptures extends Recheck, SymTransformer: } checkBounds(normArgs, tl) case _ => + + args foreach { targ => + val tp = targ.knownType + val tm = new TypeMap with IdempotentCaptRefMap: + def apply(tp: Type): Type = + tp match + case CapturingType(parent, refs) => + healTypeParamCaptureSet(refs) + mapOver(tp) + case _ => + mapOver(tp) + tm(tp) + } case _ => } if !ctx.reporter.errorsReported then From 406f51b86fbb711fe8c0a4aed2d39550e21eb5ae Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Thu, 10 Nov 2022 23:20:19 +0100 Subject: [PATCH 08/16] tweak tests - remove limitation errors - update check files --- tests/neg-custom-args/captures/byname.check | 2 +- tests/neg-custom-args/captures/lazyref.check | 8 ---- tests/neg-custom-args/captures/lazyref.scala | 2 +- tests/neg-custom-args/captures/try.check | 32 +++++++------ tests/neg-custom-args/captures/try.scala | 4 +- .../captures/usingLogFile.check | 48 ++++++++++--------- tests/neg-custom-args/captures/vars.check | 2 +- .../captures/lazyref.scala} | 0 8 files changed, 48 insertions(+), 50 deletions(-) rename tests/{neg-custom-args/captures/lazyref-pos.scala => pos-custom-args/captures/lazyref.scala} (100%) diff --git a/tests/neg-custom-args/captures/byname.check b/tests/neg-custom-args/captures/byname.check index 486f94d599ac..90cf6c145c33 100644 --- a/tests/neg-custom-args/captures/byname.check +++ b/tests/neg-custom-args/captures/byname.check @@ -8,7 +8,7 @@ 10 | h(f2()) // error | ^^^^ | Found: {cap1} (x$0: Int) -> Int - | Required: {cap2} Int -> Int + | Required: {cap2} (x$0: Int) -> Int | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/byname.scala:19:5 ---------------------------------------- diff --git a/tests/neg-custom-args/captures/lazyref.check b/tests/neg-custom-args/captures/lazyref.check index 2a3b013af6fb..fcd98d0d67bd 100644 --- a/tests/neg-custom-args/captures/lazyref.check +++ b/tests/neg-custom-args/captures/lazyref.check @@ -1,11 +1,3 @@ --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazyref.scala:13:2 --------------------------------------- -13 | (ref1, f1) => map[A, B](ref1, f1) // error // limitation - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - | Found: ? (ref1: {*} LazyRef[? A]{elem: {*} () -> box ? A}, f1: {*} (x$0: ? A) -> ? B) -> - | {f1, ref1, *} LazyRef[? B]{elem: {*} () -> box ? B} - | Required: (ref: {*} LazyRef[A], f: A => B) -> {f, ref} LazyRef[B] - | - | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazyref.scala:19:28 -------------------------------------- 19 | val ref1c: LazyRef[Int] = ref1 // error | ^^^^ diff --git a/tests/neg-custom-args/captures/lazyref.scala b/tests/neg-custom-args/captures/lazyref.scala index e7e1be9d1624..8395e5cb42cd 100644 --- a/tests/neg-custom-args/captures/lazyref.scala +++ b/tests/neg-custom-args/captures/lazyref.scala @@ -10,7 +10,7 @@ def map[A, B](ref: {*} LazyRef[A], f: A => B): {f, ref} LazyRef[B] = new LazyRef(() => f(ref.elem())) def mapc[A, B]: (ref: {*} LazyRef[A], f: A => B) -> {f, ref} LazyRef[B] = - (ref1, f1) => map[A, B](ref1, f1) // error // limitation + (ref1, f1) => map[A, B](ref1, f1) def test(cap1: Cap, cap2: Cap) = def f(x: Int) = if cap1 == cap1 then x else 0 diff --git a/tests/neg-custom-args/captures/try.check b/tests/neg-custom-args/captures/try.check index c9cc7f7c1b56..d4bcc859d256 100644 --- a/tests/neg-custom-args/captures/try.check +++ b/tests/neg-custom-args/captures/try.check @@ -2,7 +2,7 @@ 23 | val a = handle[Exception, CanThrow[Exception]] { // error | ^ | Found: ? ({*} CT[Exception]) -> CanThrow[Exception] - | Required: CanThrow[Exception] => box {*} CT[Exception] + | Required: {*} CanThrow[Exception] -> box {*} CT[Exception] 24 | (x: CanThrow[Exception]) => x 25 | }{ | @@ -11,11 +11,25 @@ 29 | val b = handle[Exception, () -> Nothing] { // error | ^ | Found: ? (x: {*} CT[Exception]) -> {x} () -> Nothing - | Required: CanThrow[Exception] => () -> Nothing + | Required: {*} (x$0: CanThrow[Exception]) -> () -> Nothing 30 | (x: CanThrow[Exception]) => () => raise(new Exception)(using x) 31 | } { | | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:52:2 ------------------------------------------- +47 |val global: () -> Int = handle { +48 | (x: CanThrow[Exception]) => +49 | () => +50 | raise(new Exception)(using x) +51 | 22 +52 |} { // error + | ^ + | Found: {x$0} () -> Int + | Required: () -> Int +53 | (ex: Exception) => () => 22 +54 |} + | + | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/try.scala:40:4 ---------------------------------------------------------------- 35 | val xx = handle { 36 | (x: CanThrow[Exception]) => @@ -24,19 +38,7 @@ 39 | 22 40 | } { // error | ^ - | The expression's type box {*} () -> Int is not allowed to capture the root capability `*`. + | The expression's type box {x$0, *} () -> Int is not allowed to capture the root capability `*`. | This usually means that a capability persists longer than its allowed lifetime. 41 | (ex: Exception) => () => 22 42 | } --- Error: tests/neg-custom-args/captures/try.scala:52:2 ---------------------------------------------------------------- -47 |val global = handle { -48 | (x: CanThrow[Exception]) => -49 | () => -50 | raise(new Exception)(using x) -51 | 22 -52 |} { // error - | ^ - | The expression's type box {*} () -> Int is not allowed to capture the root capability `*`. - | This usually means that a capability persists longer than its allowed lifetime. -53 | (ex: Exception) => () => 22 -54 |} diff --git a/tests/neg-custom-args/captures/try.scala b/tests/neg-custom-args/captures/try.scala index df7930f76af8..9489766d41be 100644 --- a/tests/neg-custom-args/captures/try.scala +++ b/tests/neg-custom-args/captures/try.scala @@ -44,11 +44,11 @@ def test = yy // OK -val global = handle { +val global: () -> Int = handle { (x: CanThrow[Exception]) => () => raise(new Exception)(using x) 22 } { // error (ex: Exception) => () => 22 -} \ No newline at end of file +} diff --git a/tests/neg-custom-args/captures/usingLogFile.check b/tests/neg-custom-args/captures/usingLogFile.check index beb7ac23ed44..05fb385a64f7 100644 --- a/tests/neg-custom-args/captures/usingLogFile.check +++ b/tests/neg-custom-args/captures/usingLogFile.check @@ -1,13 +1,3 @@ --- Error: tests/neg-custom-args/captures/usingLogFile.scala:23:27 ------------------------------------------------------ -23 | val later = usingLogFile { f => () => f.write(0) } // error - | ^^^^^^^^^^^^^^^^^^^^^^^^^ - | {f} () -> Unit cannot be box-converted to box ? () -> Unit - | since one of their capture sets contains the root capability `*` --- Error: tests/neg-custom-args/captures/usingLogFile.scala:29:9 ------------------------------------------------------- -29 | later2.x() // error - | ^^^^^^^^ - | The expression's type box {*} () -> Unit is not allowed to capture the root capability `*`. - | This usually means that a capability persists longer than its allowed lifetime. -- Error: tests/neg-custom-args/captures/usingLogFile.scala:33:2 ------------------------------------------------------- 33 | later3() // error | ^^^^^^ @@ -18,18 +8,32 @@ | ^^^^^^^^ | The expression's type box {*} () -> Unit is not allowed to capture the root capability `*`. | This usually means that a capability persists longer than its allowed lifetime. --- Error: tests/neg-custom-args/captures/usingLogFile.scala:47:27 ------------------------------------------------------ +-- Error: tests/neg-custom-args/captures/usingLogFile.scala:23:6 ------------------------------------------------------- +23 | val later = usingLogFile { f => () => f.write(0) } // error + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | Non-local value later cannot have an inferred type + | {x$0} () -> Unit + | with non-empty capture set {x$0}. + | The type needs to be declared explicitly. +-- Error: tests/neg-custom-args/captures/usingLogFile.scala:29:9 ------------------------------------------------------- +29 | later2.x() // error + | ^^^^^^^^ + | The expression's type box {x$0, *} () -> Unit is not allowed to capture the root capability `*`. + | This usually means that a capability persists longer than its allowed lifetime. +-- Error: tests/neg-custom-args/captures/usingLogFile.scala:47:6 ------------------------------------------------------- 47 | val later = usingLogFile { f => () => f.write(0) } // error - | ^^^^^^^^^^^^^^^^^^^^^^^^^ - | {f} () -> Unit cannot be box-converted to box ? () -> Unit - | since one of their capture sets contains the root capability `*` --- Error: tests/neg-custom-args/captures/usingLogFile.scala:62:33 ------------------------------------------------------ + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | Non-local value later cannot have an inferred type + | {x$0} () -> Unit + | with non-empty capture set {x$0}. + | The type needs to be declared explicitly. +-- Error: tests/neg-custom-args/captures/usingLogFile.scala:62:25 ------------------------------------------------------ 62 | val later = usingFile("out", f => (y: Int) => xs.foreach(x => f.write(x + y))) // error - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - | {f} (x$0: Int) -> Unit cannot be box-converted to box ? (x$0: Int) -> Unit - | since one of their capture sets contains the root capability `*` --- Error: tests/neg-custom-args/captures/usingLogFile.scala:71:37 ------------------------------------------------------ + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | The expression's type box {x$0, *} (x$0: Int) -> Unit is not allowed to capture the root capability `*`. + | This usually means that a capability persists longer than its allowed lifetime. +-- Error: tests/neg-custom-args/captures/usingLogFile.scala:71:25 ------------------------------------------------------ 71 | val later = usingFile("logfile", usingLogger(_, l => () => l.log("test"))) // error - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - | {_$1} () -> Unit cannot be box-converted to box ? () -> Unit - | since one of their capture sets contains the root capability `*` + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | The expression's type box {x$0, *} () -> Unit is not allowed to capture the root capability `*`. + | This usually means that a capability persists longer than its allowed lifetime. diff --git a/tests/neg-custom-args/captures/vars.check b/tests/neg-custom-args/captures/vars.check index 8fe72a76493a..4b9ab5723ce6 100644 --- a/tests/neg-custom-args/captures/vars.check +++ b/tests/neg-custom-args/captures/vars.check @@ -25,7 +25,7 @@ -- Error: tests/neg-custom-args/captures/vars.scala:32:8 --------------------------------------------------------------- 32 | local { cap3 => // error | ^ - | The expression's type box {*} (x$0: String) -> String is not allowed to capture the root capability `*`. + | The expression's type box {x$0, *} (x$0: String) -> String is not allowed to capture the root capability `*`. | This usually means that a capability persists longer than its allowed lifetime. 33 | def g(x: String): String = if cap3 == cap3 then "" else "a" 34 | g diff --git a/tests/neg-custom-args/captures/lazyref-pos.scala b/tests/pos-custom-args/captures/lazyref.scala similarity index 100% rename from tests/neg-custom-args/captures/lazyref-pos.scala rename to tests/pos-custom-args/captures/lazyref.scala From 0e7d33ad838b5c521ed4e24131379607c4e9130e Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Sun, 13 Nov 2022 19:10:52 +0100 Subject: [PATCH 09/16] polish implementation --- .../dotty/tools/dotc/cc/CheckCaptures.scala | 103 +++++++++++++----- 1 file changed, 76 insertions(+), 27 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index d86b91beb7c4..321ecf236168 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -891,23 +891,82 @@ class CheckCaptures extends Recheck, SymTransformer: capt.println(i"checked $root with $selfType") end checkSelfTypes - private def healTypeParamCaptureSet(cs: CaptureSet)(using Context) = { - def avoidParam(tpr: TermParamRef): List[CaptureSet] = - val refs = tpr.binder.paramInfos(tpr.paramNum).captureSet - refs.filter(!_.isInstanceOf[TermParamRef]) :: refs.elems.toList.flatMap { - case tpr: TermParamRef => avoidParam(tpr) - case _ => Nil - } + /** Heal ill-formed capture sets in the type parameter. + * + * We can push parameter refs into a capture set in type parameters + * that this type parameter can't see. + * For example, when capture checking the following expression: + * + * def usingLogFile[T](op: (f: {*} File) => T): T = ... + * + * usingLogFile[box ?1 () -> Unit] { (f: {*} File) => () => { f.write(0) } } + * + * We may propagate `f` into ?1, making ?1 ill-formed. + * This also causes soundness issues, since `f` in ?1 should be widened to `*`, + * giving rise to an error that `*` cannot be included in a boxed capture set. + * + * To solve this, we still allow ?1 to capture parameter refs like `f`, but + * compensate this by pushing the widened capture set of `f` into ?1. + * This solves the soundness issue caused by the ill-formness of ?1. + */ + private def healTypeParam(tree: Tree)(using Context): Unit = + val tm = new TypeMap with IdempotentCaptRefMap: + private def isAllowed(ref: CaptureRef): Boolean = ref match + case ref: TermParamRef => allowed.contains(ref) + case _ => true + + private def widenParamRefs(refs: List[TermParamRef]): List[CaptureSet] = + @scala.annotation.tailrec + def recur(todos: List[TermParamRef], acc: List[CaptureSet]): List[CaptureSet] = + todos match + case Nil => acc + case ref :: rem => + val cs = ref.binder.paramInfos(ref.paramNum).captureSet + val nextAcc = cs.filter(isAllowed(_)) :: acc + val nextRem: List[TermParamRef] = (cs.elems.toList.filter(!isAllowed(_)) ++ rem).asInstanceOf + recur(nextRem, nextAcc) + recur(refs, Nil) + + private def healCaptureSet(cs: CaptureSet): Unit = + val toInclude = widenParamRefs(cs.elems.toList.filter(!isAllowed(_)).asInstanceOf) + toInclude foreach { cs1 => + // We omit the check of the result of capture set inclusion here, + // since there are only two possible kinds of errors. + // Both kinds will be detected in other places and tend to + // give better error messages. + // + // The two kinds of errors are: + // - Pushing `*` to a boxed capture set. + // This triggers error reporting registered as the `rootAddedHandler` + // in `CaptureSet`. + // - Failing to include a capture reference in a capture set. + // This is mostly due to the restriction placed by explicit type annotations, + // and should already be reported as a type mismatch during `checkConforms`. + cs1.subCaptures(cs, frozen = false) + } - val widenedSets = cs.elems.toList flatMap { - case tpr: TermParamRef => avoidParam(tpr) - case _ => Nil - } + private var allowed: SimpleIdentitySet[TermParamRef] = SimpleIdentitySet.empty + + def apply(tp: Type) = + tp match + case CapturingType(parent, refs) => + healCaptureSet(refs) + mapOver(tp) + case tp @ RefinedType(parent, rname, rinfo: MethodType) => + this(rinfo) + case tp: TermLambda => + val localParams: List[TermParamRef] = tp.paramRefs + val saved = allowed + try + localParams foreach { x => allowed = allowed + x } + mapOver(tp) + finally allowed = saved + case _ => + mapOver(tp) - widenedSets foreach { cs1 => - cs1.subCaptures(cs, frozen = false) - } - } + if tree.isInstanceOf[InferredTypeTree] then + tm(tree.knownType) + end healTypeParam /** Perform the following kinds of checks * - Check all explicitly written capturing types for well-formedness using `checkWellFormedPost`. @@ -915,6 +974,7 @@ class CheckCaptures extends Recheck, SymTransformer: * suggest an explicit type. This is so that separate compilation (where external * symbols have empty capture sets) gives the same results as joint compilation. * - Check that arguments of TypeApplys and AppliedTypes conform to their bounds. + * - Heal ill-formed capture sets of type parameters. See `healTypeParam`. */ def postCheck(unit: tpd.Tree)(using Context): Unit = unit.foreachSubTree { @@ -968,18 +1028,7 @@ class CheckCaptures extends Recheck, SymTransformer: checkBounds(normArgs, tl) case _ => - args foreach { targ => - val tp = targ.knownType - val tm = new TypeMap with IdempotentCaptRefMap: - def apply(tp: Type): Type = - tp match - case CapturingType(parent, refs) => - healTypeParamCaptureSet(refs) - mapOver(tp) - case _ => - mapOver(tp) - tm(tp) - } + args.foreach(healTypeParam(_)) case _ => } if !ctx.reporter.errorsReported then From 1afbf7441cac24c8bb1d6632e8cc779b0d5c4ee6 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Sun, 13 Nov 2022 19:10:59 +0100 Subject: [PATCH 10/16] test case for type parameter capture set healing --- .../captures/heal-tparam-cs.scala | 33 +++++++++++++++++++ 1 file changed, 33 insertions(+) create mode 100644 tests/neg-custom-args/captures/heal-tparam-cs.scala diff --git a/tests/neg-custom-args/captures/heal-tparam-cs.scala b/tests/neg-custom-args/captures/heal-tparam-cs.scala new file mode 100644 index 000000000000..3ff34d0a8a42 --- /dev/null +++ b/tests/neg-custom-args/captures/heal-tparam-cs.scala @@ -0,0 +1,33 @@ +import language.experimental.captureChecking + +trait Cap { def use(): Unit } + +def localCap[T](op: (cap: {*} Cap) => T): T = ??? + +def main(io: {*} Cap, net: {*} Cap): Unit = { + val test1 = localCap { cap => // error + () => { cap.use() } + } + + val test2: (cap: {*} Cap) -> {cap} () -> Unit = + localCap { cap => // should work + (cap1: {*} Cap) => () => { cap1.use() } + } + + val test3: (cap: {io} Cap) -> {io} () -> Unit = + localCap { cap => // should work + (cap1: {io} Cap) => () => { cap1.use() } + } + + val test4: (cap: {io} Cap) -> {net} () -> Unit = + localCap { cap => // error + (cap1: {io} Cap) => () => { cap1.use() } + } + + def localCap2[T](op: (cap: {io} Cap) => T): T = ??? + + val test5: {io} () -> Unit = + localCap2 { cap => // ok + () => { cap.use() } + } +} From abd085e9d5b06098bc4deb00ba497f7b36cb068a Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 14 Nov 2022 00:17:31 +0100 Subject: [PATCH 11/16] use a type traverser to heal capture sets --- .../src/dotty/tools/dotc/cc/CheckCaptures.scala | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 321ecf236168..68b62a574e84 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -910,7 +910,7 @@ class CheckCaptures extends Recheck, SymTransformer: * This solves the soundness issue caused by the ill-formness of ?1. */ private def healTypeParam(tree: Tree)(using Context): Unit = - val tm = new TypeMap with IdempotentCaptRefMap: + val checker = new TypeTraverser: private def isAllowed(ref: CaptureRef): Boolean = ref match case ref: TermParamRef => allowed.contains(ref) case _ => true @@ -947,25 +947,26 @@ class CheckCaptures extends Recheck, SymTransformer: private var allowed: SimpleIdentitySet[TermParamRef] = SimpleIdentitySet.empty - def apply(tp: Type) = + def traverse(tp: Type) = tp match case CapturingType(parent, refs) => healCaptureSet(refs) - mapOver(tp) + // mapOver(tp) + traverseChildren(parent) case tp @ RefinedType(parent, rname, rinfo: MethodType) => - this(rinfo) + traverseChildren(rinfo) case tp: TermLambda => val localParams: List[TermParamRef] = tp.paramRefs val saved = allowed try localParams foreach { x => allowed = allowed + x } - mapOver(tp) + traverseChildren(tp) finally allowed = saved case _ => - mapOver(tp) + traverseChildren(tp) if tree.isInstanceOf[InferredTypeTree] then - tm(tree.knownType) + checker.traverse(tree.knownType) end healTypeParam /** Perform the following kinds of checks From 80830e3bcd897c9214e1eb4cbdd31abeaff8f814 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 14 Nov 2022 00:17:49 +0100 Subject: [PATCH 12/16] tweak test cases --- tests/neg-custom-args/boxmap.scala | 2 +- tests/pos-custom-args/captures/lazyref.scala | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/neg-custom-args/boxmap.scala b/tests/neg-custom-args/boxmap.scala index 340f9cfe820f..e66b0a8ec808 100644 --- a/tests/neg-custom-args/boxmap.scala +++ b/tests/neg-custom-args/boxmap.scala @@ -16,6 +16,6 @@ def test[A <: Top, B <: Top] = def lazymap[A <: Top, B <: Top](b: Box[A])(f: A => B) = () => b[Box[B]]((x: A) => box(f(x))) val x0: (b: Box[A]) -> (f: A => B) -> (() -> Box[B]) = lazymap[A, B] // error - val x: (b: Box[A]) -> (f: A => B) -> {f} (() -> Box[B]) = lazymap[A, B] // error // limitation + val x: (b: Box[A]) -> (f: A => B) -> {b, f} (() -> Box[B]) = lazymap[A, B] // works val y: (b: Box[A]) -> (f: A => B) -> {*} (() -> Box[B]) = lazymap[A, B] // works () diff --git a/tests/pos-custom-args/captures/lazyref.scala b/tests/pos-custom-args/captures/lazyref.scala index 8ff394934a04..0d988dc3e17b 100644 --- a/tests/pos-custom-args/captures/lazyref.scala +++ b/tests/pos-custom-args/captures/lazyref.scala @@ -9,7 +9,7 @@ def map[A, B](ref: {*} LazyRef[A], f: A => B): {f, ref} LazyRef[B] = new LazyRef(() => f(ref.elem())) def mapc[A, B]: (ref: {*} LazyRef[A], f: A => B) => {f, ref} LazyRef[B] = - (ref1, f1) => map[A, B](ref1, f1) // error // limitation + (ref1, f1) => map[A, B](ref1, f1) def test(cap1: Cap, cap2: Cap) = def f(x: Int) = if cap1 == cap1 then x else 0 From fcf85adad0bb040391a0d7b3bb8be3c671d9be2f Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Sun, 20 Nov 2022 21:00:41 +0100 Subject: [PATCH 13/16] rename function and add doc --- compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 68b62a574e84..a17154dc493e 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -606,7 +606,7 @@ class CheckCaptures extends Recheck, SymTransformer: /** Massage `actual` and `expected` types using the methods below before checking conformance */ override def checkConformsExpr(actual: Type, expected: Type, tree: Tree)(using Context): Unit = - val expected1 = makeFunctionDependent(addOuterRefs(expected, actual), actual.stripCapturing) + val expected1 = alignDependentFunction(addOuterRefs(expected, actual), actual.stripCapturing) val actual1 = adaptBoxed(actual, expected1, tree.srcPos) //println(i"check conforms $actual1 <<< $expected1") super.checkConformsExpr(actual1, expected1, tree) @@ -615,7 +615,8 @@ class CheckCaptures extends Recheck, SymTransformer: MethodType.companion(isContextual = isContextual, isErased = isErased)(args, resultType) .toFunctionType(isJava = false, alwaysDependent = true) - private def makeFunctionDependent(expected: Type, actual: Type)(using Context): Type = + /** Turn `expected` into a dependent function when `actual` is dependent. */ + private def alignDependentFunction(expected: Type, actual: Type)(using Context): Type = def recur(expected: Type): Type = expected.dealias match case expected @ CapturingType(eparent, refs) => CapturingType(recur(eparent), refs, boxed = expected.isBoxed) From dfd077e032a19b36e043bd2048748e017479207f Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Sun, 20 Nov 2022 22:03:09 +0100 Subject: [PATCH 14/16] address review comments --- compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index a17154dc493e..8e4204d543e6 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -916,6 +916,10 @@ class CheckCaptures extends Recheck, SymTransformer: case ref: TermParamRef => allowed.contains(ref) case _ => true + // Widen the given term parameter refs x₁ : C₁ S₁ , ⋯ , xₙ : Cₙ Sₙ to their capture sets C₁ , ⋯ , Cₙ. + // + // If in these capture sets there are any capture references that are term parameter references we should avoid, + // we will widen them recursively. private def widenParamRefs(refs: List[TermParamRef]): List[CaptureSet] = @scala.annotation.tailrec def recur(todos: List[TermParamRef], acc: List[CaptureSet]): List[CaptureSet] = @@ -954,13 +958,12 @@ class CheckCaptures extends Recheck, SymTransformer: healCaptureSet(refs) // mapOver(tp) traverseChildren(parent) - case tp @ RefinedType(parent, rname, rinfo: MethodType) => + case tp @ RefinedType(parent, rname, rinfo: MethodType) if defn.isFunctionType(tp) => traverseChildren(rinfo) case tp: TermLambda => - val localParams: List[TermParamRef] = tp.paramRefs val saved = allowed try - localParams foreach { x => allowed = allowed + x } + tp.paramRefs.foreach(allowed += _) traverseChildren(tp) finally allowed = saved case _ => From f8895632a3013f14f6a56d1fe48ffa4e53371eab Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Sun, 20 Nov 2022 22:43:48 +0100 Subject: [PATCH 15/16] check the result of widened capture set inclusion --- .../dotty/tools/dotc/cc/CheckCaptures.scala | 21 +++---------------- 1 file changed, 3 insertions(+), 18 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 8e4204d543e6..2bc6fc7c9d16 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -934,21 +934,7 @@ class CheckCaptures extends Recheck, SymTransformer: private def healCaptureSet(cs: CaptureSet): Unit = val toInclude = widenParamRefs(cs.elems.toList.filter(!isAllowed(_)).asInstanceOf) - toInclude foreach { cs1 => - // We omit the check of the result of capture set inclusion here, - // since there are only two possible kinds of errors. - // Both kinds will be detected in other places and tend to - // give better error messages. - // - // The two kinds of errors are: - // - Pushing `*` to a boxed capture set. - // This triggers error reporting registered as the `rootAddedHandler` - // in `CaptureSet`. - // - Failing to include a capture reference in a capture set. - // This is mostly due to the restriction placed by explicit type annotations, - // and should already be reported as a type mismatch during `checkConforms`. - cs1.subCaptures(cs, frozen = false) - } + toInclude.foreach(checkSubset(_, cs, tree.srcPos)) private var allowed: SimpleIdentitySet[TermParamRef] = SimpleIdentitySet.empty @@ -956,10 +942,9 @@ class CheckCaptures extends Recheck, SymTransformer: tp match case CapturingType(parent, refs) => healCaptureSet(refs) - // mapOver(tp) - traverseChildren(parent) + traverse(parent) case tp @ RefinedType(parent, rname, rinfo: MethodType) if defn.isFunctionType(tp) => - traverseChildren(rinfo) + traverse(rinfo) case tp: TermLambda => val saved = allowed try From c4240fb6e1858cb29281c6ebae6106d61751ca9e Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Sun, 20 Nov 2022 22:47:20 +0100 Subject: [PATCH 16/16] use captureSetOfInfo --- compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 2bc6fc7c9d16..d518084039d3 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -926,7 +926,7 @@ class CheckCaptures extends Recheck, SymTransformer: todos match case Nil => acc case ref :: rem => - val cs = ref.binder.paramInfos(ref.paramNum).captureSet + val cs = ref.captureSetOfInfo val nextAcc = cs.filter(isAllowed(_)) :: acc val nextRem: List[TermParamRef] = (cs.elems.toList.filter(!isAllowed(_)) ++ rem).asInstanceOf recur(nextRem, nextAcc)