From bd324f619236193a22a1e892b7ae75e733e93f07 Mon Sep 17 00:00:00 2001 From: odersky Date: Thu, 6 Nov 2025 18:16:25 +0100 Subject: [PATCH 1/2] Freshen all explicit arguments of type applications Previously, we did not do that, which means that explicit arguments in TypeApply's could not contain `^`. This precaution shoul dnot longer be needed with level checking. --- compiler/src/dotty/tools/dotc/cc/Setup.scala | 2 +- .../captures/boundary-homebrew.check | 16 ++++ .../captures/boundary-homebrew.scala | 22 +++++ .../captures/boundschecks.scala | 2 +- .../neg-custom-args/captures/capt-test.scala | 2 +- tests/neg-custom-args/captures/capt1.check | 56 +++++++------ tests/neg-custom-args/captures/capt1.scala | 4 +- .../captures/class-level-attack.check | 7 -- .../captures/class-level-attack.scala | 2 +- tests/neg-custom-args/captures/i15049.scala | 2 +- tests/neg-custom-args/captures/i16114.check | 84 +++++++++++-------- tests/neg-custom-args/captures/i16114.scala | 20 ++--- tests/neg-custom-args/captures/i21401.check | 34 +------- tests/neg-custom-args/captures/i21401.scala | 6 +- tests/neg-custom-args/captures/levels.check | 7 -- tests/neg-custom-args/captures/levels.scala | 2 +- .../neg-custom-args/captures/outer-var.check | 7 -- .../neg-custom-args/captures/outer-var.scala | 2 +- tests/neg-custom-args/captures/reaches.check | 59 ++++++------- tests/neg-custom-args/captures/reaches.scala | 4 +- tests/neg-custom-args/captures/try.check | 9 +- tests/neg-custom-args/captures/try.scala | 2 +- .../captures/unsound-reach.check | 22 +++-- .../captures/unsound-reach.scala | 13 ++- tests/neg-custom-args/captures/withFile.scala | 4 +- .../captures/i23389.scala | 8 +- 26 files changed, 201 insertions(+), 197 deletions(-) create mode 100644 tests/neg-custom-args/captures/boundary-homebrew.check create mode 100644 tests/neg-custom-args/captures/boundary-homebrew.scala rename tests/{neg-custom-args => pos-custom-args}/captures/i23389.scala (90%) diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala index 38b60744c6f7..f12c4ecb1f1b 100644 --- a/compiler/src/dotty/tools/dotc/cc/Setup.scala +++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala @@ -501,7 +501,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: var transformed = if tree.isInferred then transformInferredType(tree.tpe) - else transformExplicitType(tree.tpe, sym, freshen = !boxed, tptToCheck = tree) + else transformExplicitType(tree.tpe, sym, freshen = true, tptToCheck = tree) if boxed then transformed = transformed.boxDeeply tree.setNuType( if sym.hasAnnotation(defn.UncheckedCapturesAnnot) then makeUnchecked(transformed) diff --git a/tests/neg-custom-args/captures/boundary-homebrew.check b/tests/neg-custom-args/captures/boundary-homebrew.check new file mode 100644 index 000000000000..387d1aea2d6b --- /dev/null +++ b/tests/neg-custom-args/captures/boundary-homebrew.check @@ -0,0 +1,16 @@ +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/boundary-homebrew.scala:19:19 ---------------------------- +19 | boundary[Int]: l2 ?=> // error + | ^ + |Capability cap outlives its scope: it leaks into outer capture set 's1 of parameter l1. + |The leakage occurred when trying to match the following types: + | + |Found: (l2: boundary.Label[Int]^'s2) ?->{l1} Int + |Required: (boundary.Label[Int]^) ?=> Int + | + |where: ?=> refers to a fresh root capability created in anonymous function of type (using l1²: boundary.Label[boundary.Label[Int]^]^): boundary.Label[Int]^ when checking argument to parameter body of method apply + | ^ refers to the universal root capability + | cap is a fresh root capability created in anonymous function of type (using l2: boundary.Label[Int]^'s2): Int of parameter parameter l2² of method $anonfun +20 | boundary.break(l2)(using l1) +21 | 15 + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/boundary-homebrew.scala b/tests/neg-custom-args/captures/boundary-homebrew.scala new file mode 100644 index 000000000000..d510464a35be --- /dev/null +++ b/tests/neg-custom-args/captures/boundary-homebrew.scala @@ -0,0 +1,22 @@ +import language.experimental.captureChecking +import caps.* + +object boundary: + class Label[-T] + case class Break[T](private[boundary] label: Label[T]^{}, result: T) extends Throwable + + def apply[T](body: Label[T]^ ?=> T): T = + val label = Label() + try + body(using label) + catch + case Break[T @unchecked](l, res) if l eq label => res + + def break[T](value: T)(using l: Label[T]) = throw Break(unsafe.unsafeAssumePure(l), value) + +def test = + boundary[boundary.Label[Int]^]: l1 ?=> + boundary[Int]: l2 ?=> // error + boundary.break(l2)(using l1) + 15 + ??? \ No newline at end of file diff --git a/tests/neg-custom-args/captures/boundschecks.scala b/tests/neg-custom-args/captures/boundschecks.scala index 766d89d2f37b..9f215b602355 100644 --- a/tests/neg-custom-args/captures/boundschecks.scala +++ b/tests/neg-custom-args/captures/boundschecks.scala @@ -11,7 +11,7 @@ object test { f[Tree^](t) // error f[Tree](t) // error val c1 = C(t) // error - val c2 = C[Tree^](t) // error + val c2 = C[Tree^](t) // error // error val c3 = C[Tree](t) // error val foo: C[Tree^] = ??? diff --git a/tests/neg-custom-args/captures/capt-test.scala b/tests/neg-custom-args/captures/capt-test.scala index ea2a77d5c2ac..f2ade7daf8c4 100644 --- a/tests/neg-custom-args/captures/capt-test.scala +++ b/tests/neg-custom-args/captures/capt-test.scala @@ -20,7 +20,7 @@ def handle[E <: Exception, R <: Top](op: (CT[E] @retains[caps.cap.type]) => R)( catch case ex: E => handler(ex) def test: Unit = - val b = handle[Exception, () => Nothing] { // error + val b = handle[Exception, () => Nothing] { (x: CanThrow[Exception]) => () => raise(new Exception)(using x) // error } { (ex: Exception) => ??? diff --git a/tests/neg-custom-args/captures/capt1.check b/tests/neg-custom-args/captures/capt1.check index 93b90d2d1279..906991c4019e 100644 --- a/tests/neg-custom-args/captures/capt1.check +++ b/tests/neg-custom-args/captures/capt1.check @@ -43,46 +43,50 @@ | Note that capability x is not included in capture set {}. | | longer explanation available when compiling with `-explain` --- Error: tests/neg-custom-args/captures/capt1.scala:36:16 ------------------------------------------------------------- -36 | val z2 = h[() -> Cap](() => x) // error // error - | ^^^^^^^^^ - | Type variable X of method h cannot be instantiated to () -> C^ since - | the part C^ of that type captures the root capability `cap`. - | - | where: ^ refers to the universal root capability -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:36:24 ---------------------------------------- -36 | val z2 = h[() -> Cap](() => x) // error // error +36 | val z2 = h[() -> Cap](() => x) // error | ^^^^^^^ - |Found: () ->'s2 C^ - |Required: () -> C^² + | Found: () ->'s2 C^ + | Required: () -> C^² | - |Note that capability cap is not included in capture set {cap²} - |because cap is not visible from cap² in value z2. + | Note that capability cap is not included in capture set {cap²} + | because cap is not visible from cap² in value z2. | - |where: ^ and cap refer to a root capability associated with the result type of (): C^ - | ^² and cap² refer to a fresh root capability created in value z2 when checking argument to parameter a of method h + | where: ^ and cap refer to a root capability associated with the result type of (): C^ + | ^² and cap² refer to a fresh root capability created in value z2 | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:37:5 ----------------------------------------- 37 | (() => C()) // error | ^^^^^^^^^ - |Found: () ->'s3 C^ - |Required: () -> C^² + | Found: () ->'s3 C^ + | Required: () -> C^² | - |Note that capability cap is not included in capture set {cap²} - |because cap is not visible from cap² in value z2. + | Note that capability cap is not included in capture set {cap²} + | because cap is not visible from cap² in value z2. | - |where: ^ and cap refer to a root capability associated with the result type of (): C^ - | ^² and cap² refer to a fresh root capability created in value z2 when checking argument to parameter b of method h + | where: ^ and cap refer to a root capability associated with the result type of (): C^ + | ^² and cap² refer to a fresh root capability created in value z2 | | longer explanation available when compiling with `-explain` --- Error: tests/neg-custom-args/captures/capt1.scala:38:13 ------------------------------------------------------------- +-- Error: tests/neg-custom-args/captures/capt1.scala:38:51 ------------------------------------------------------------- 38 | val z3 = h[(() -> Cap) @retains[x.type]](() => x)(() => C()) // error - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - | Type variable X of method h cannot be instantiated to () ->{x} C^ since - | the part C^ of that type captures the root capability `cap`. - | - | where: ^ refers to the universal root capability + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | Separation failure: Illegal access to {x} which is hidden by the previous definition + | of value z2 with type () ->{} C^. + | This type hides capabilities {cap, x} + | + | where: ^ refers to a fresh root capability in the type of value z2 + | cap is a fresh root capability created in value z2 +-- Error: tests/neg-custom-args/captures/capt1.scala:40:25 ------------------------------------------------------------- +40 | val z1: () => Cap = f1(x) // error + | ^ + | Separation failure: Illegal access to {x} which is hidden by the previous definition + | of value z3 with type () ->{x} C^. + | This type hides capabilities {cap, x} + | + | where: ^ refers to a fresh root capability in the type of value z3 + | cap is a fresh root capability created in value z3 -- Error: tests/neg-custom-args/captures/capt1.scala:43:7 -------------------------------------------------------------- 43 | if x == null then // error: separation | ^ diff --git a/tests/neg-custom-args/captures/capt1.scala b/tests/neg-custom-args/captures/capt1.scala index 1a1eddb7a2fb..01eda5e049f8 100644 --- a/tests/neg-custom-args/captures/capt1.scala +++ b/tests/neg-custom-args/captures/capt1.scala @@ -33,11 +33,11 @@ def foo() = val x: C @retains[caps.cap.type] = ??? def h[X](a: X)(b: X) = a - val z2 = h[() -> Cap](() => x) // error // error + val z2 = h[() -> Cap](() => x) // error (() => C()) // error val z3 = h[(() -> Cap) @retains[x.type]](() => x)(() => C()) // error - val z1: () => Cap = f1(x) + val z1: () => Cap = f1(x) // error val z4 = if x == null then // error: separation diff --git a/tests/neg-custom-args/captures/class-level-attack.check b/tests/neg-custom-args/captures/class-level-attack.check index d6fa9e5821a4..d9eefddb0fc6 100644 --- a/tests/neg-custom-args/captures/class-level-attack.check +++ b/tests/neg-custom-args/captures/class-level-attack.check @@ -1,10 +1,3 @@ --- Error: tests/neg-custom-args/captures/class-level-attack.scala:12:24 ------------------------------------------------ -12 | val r: Ref[IO^] = Ref[IO^](io) // error: - | ^^^ - | Type variable X of constructor Ref cannot be instantiated to IO^ since - | that type captures the root capability `cap`. - | - | where: ^ refers to the universal root capability -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/class-level-attack.scala:17:26 --------------------------- 17 | def set(x: IO^) = r.put(x) // error | ^ diff --git a/tests/neg-custom-args/captures/class-level-attack.scala b/tests/neg-custom-args/captures/class-level-attack.scala index b9847ea4045d..b48aca8c0c5f 100644 --- a/tests/neg-custom-args/captures/class-level-attack.scala +++ b/tests/neg-custom-args/captures/class-level-attack.scala @@ -9,7 +9,7 @@ class Ref[X](init: X): def put(y: X): Unit = x = y class C(io: IO^): - val r: Ref[IO^] = Ref[IO^](io) // error: + val r: Ref[IO^] = Ref[IO^](io) //Type variable X of constructor Ref cannot be instantiated to box IO^ since //that type captures the root capability `cap`. // where: ^ refers to the universal root capability diff --git a/tests/neg-custom-args/captures/i15049.scala b/tests/neg-custom-args/captures/i15049.scala index 7f8368631d4f..ff6b17c360de 100644 --- a/tests/neg-custom-args/captures/i15049.scala +++ b/tests/neg-custom-args/captures/i15049.scala @@ -7,4 +7,4 @@ class Foo: def Test: Unit = val f = new Foo f.withSession(s => s).request // error - f.withSession[Session^](t => t) // error // error + f.withSession[Session^](t => t) // error diff --git a/tests/neg-custom-args/captures/i16114.check b/tests/neg-custom-args/captures/i16114.check index 5e755d6770f1..8f4f707319f5 100644 --- a/tests/neg-custom-args/captures/i16114.check +++ b/tests/neg-custom-args/captures/i16114.check @@ -1,35 +1,49 @@ --- Error: tests/neg-custom-args/captures/i16114.scala:18:13 ------------------------------------------------------------ -18 | expect[Cap^] { // error - | ^^^^ - | Type variable T of method expect cannot be instantiated to Cap^ since - | that type captures the root capability `cap`. - | - | where: ^ refers to the universal root capability --- Error: tests/neg-custom-args/captures/i16114.scala:24:13 ------------------------------------------------------------ -24 | expect[Cap^] { // error - | ^^^^ - | Type variable T of method expect cannot be instantiated to Cap^ since - | that type captures the root capability `cap`. - | - | where: ^ refers to the universal root capability --- Error: tests/neg-custom-args/captures/i16114.scala:30:13 ------------------------------------------------------------ -30 | expect[Cap^] { // error - | ^^^^ - | Type variable T of method expect cannot be instantiated to Cap^ since - | that type captures the root capability `cap`. - | - | where: ^ refers to the universal root capability --- Error: tests/neg-custom-args/captures/i16114.scala:36:13 ------------------------------------------------------------ -36 | expect[Cap^](io) // error - | ^^^^ - | Type variable T of method expect cannot be instantiated to Cap^ since - | that type captures the root capability `cap`. - | - | where: ^ refers to the universal root capability --- Error: tests/neg-custom-args/captures/i16114.scala:39:13 ------------------------------------------------------------ -39 | expect[Cap^] { // error - | ^^^^ - | Type variable T of method expect cannot be instantiated to Cap^ since - | that type captures the root capability `cap`. - | - | where: ^ refers to the universal root capability +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i16114.scala:17:32 --------------------------------------- +17 | val op1: Unit ->{io} Unit = (x: Unit) => // error + | ^ + | Found: (x: Unit) ->{io, fs} Unit + | Required: Unit ->{io} Unit + | + | Note that capability fs is not included in capture set {io}. +18 | expect[Cap^] { +19 | io.use() +20 | fs +21 | } + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i16114.scala:23:32 --------------------------------------- +23 | val op2: Unit ->{fs} Unit = (x: Unit) => // error + | ^ + | Found: (x: Unit) ->{fs, io} Unit + | Required: Unit ->{fs} Unit + | + | Note that capability io is not included in capture set {fs}. +24 | expect[Cap^] { +25 | fs.use() +26 | io +27 | } + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i16114.scala:35:30 --------------------------------------- +35 | val op4: Unit ->{} Unit = (x: Unit) => // error + | ^ + | Found: (x: Unit) ->{io} Unit + | Required: Unit -> Unit + | + | Note that capability io is not included in capture set {}. +36 | expect[Cap^](io) + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i16114.scala:38:27 --------------------------------------- +38 | val op: Unit -> Unit = (x: Unit) => // error + | ^ + | Found: (x: Unit) ->{io} Unit + | Required: Unit -> Unit + | + | Note that capability io is not included in capture set {}. +39 | expect[Cap^] { +40 | io.use() +41 | io +42 | } + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/i16114.scala b/tests/neg-custom-args/captures/i16114.scala index dccd9564d8ca..18f984e3e92d 100644 --- a/tests/neg-custom-args/captures/i16114.scala +++ b/tests/neg-custom-args/captures/i16114.scala @@ -14,29 +14,29 @@ def withCap[T](op: Cap^ => T): T = { def main(fs: Cap^): Unit = { def badOp(io: Cap^): Unit ->{} Unit = { - val op1: Unit ->{io} Unit = (x: Unit) => - expect[Cap^] { // error + val op1: Unit ->{io} Unit = (x: Unit) => // error + expect[Cap^] { io.use() fs } - val op2: Unit ->{fs} Unit = (x: Unit) => - expect[Cap^] { // error + val op2: Unit ->{fs} Unit = (x: Unit) => // error + expect[Cap^] { fs.use() io } - val op3: Unit ->{io} Unit = (x: Unit) => - expect[Cap^] { // error + val op3: Unit ->{io} Unit = (x: Unit) => // ok + expect[Cap^] { io.use() io } - val op4: Unit ->{} Unit = (x: Unit) => // o k - expect[Cap^](io) // error + val op4: Unit ->{} Unit = (x: Unit) => // error + expect[Cap^](io) - val op: Unit -> Unit = (x: Unit) => - expect[Cap^] { // error + val op: Unit -> Unit = (x: Unit) => // error + expect[Cap^] { io.use() io } diff --git a/tests/neg-custom-args/captures/i21401.check b/tests/neg-custom-args/captures/i21401.check index ac8cecf98514..ca8140e9aa4d 100644 --- a/tests/neg-custom-args/captures/i21401.check +++ b/tests/neg-custom-args/captures/i21401.check @@ -1,19 +1,5 @@ --- Error: tests/neg-custom-args/captures/i21401.scala:13:14 ------------------------------------------------------------ -13 | op1(Boxed[IO^](x)) // error - | ^^^ - | Type variable T of object Boxed cannot be instantiated to IO^ since - | that type captures the root capability `cap`. - | - | where: ^ refers to the universal root capability --- Error: tests/neg-custom-args/captures/i21401.scala:15:18 ------------------------------------------------------------ -15 | val a = usingIO[IO^](x => x) // error // error - | ^^^ - | Type variable R of method usingIO cannot be instantiated to IO^ since - | that type captures the root capability `cap`. - | - | where: ^ refers to the universal root capability -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21401.scala:15:23 --------------------------------------- -15 | val a = usingIO[IO^](x => x) // error // error +15 | val a = usingIO[IO^](x => x) // error | ^^^^^^ |Found: (x: IO^'s1) ->'s2 IO^{x} |Required: IO^ => IO^² @@ -23,7 +9,7 @@ | |where: => refers to a fresh root capability created in value a when checking argument to parameter op of method usingIO | ^ refers to the universal root capability - | ^² and cap refer to a fresh root capability created in value a when checking argument to parameter op of method usingIO + | ^² and cap refer to a fresh root capability created in value a | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/i21401.scala:16:66 ------------------------------------------------------------ @@ -33,22 +19,8 @@ | the part IO^ of that type captures the root capability `cap`. | | where: ^ refers to the universal root capability --- Error: tests/neg-custom-args/captures/i21401.scala:17:29 ------------------------------------------------------------ -17 | val x: Boxed[IO^] = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x) // error // error // error - | ^^^^^^^^^^ - | Type variable R of value leaked cannot be instantiated to Boxed[IO^] since - | the part IO^ of that type captures the root capability `cap`. - | - | where: ^ refers to the universal root capability --- Error: tests/neg-custom-args/captures/i21401.scala:17:52 ------------------------------------------------------------ -17 | val x: Boxed[IO^] = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x) // error // error // error - | ^^^^^^^^^^^^^^^^^^^^^^^^ - | Type variable X of value leaked cannot be instantiated to Boxed[IO^] -> Boxed[IO^] since - | the part IO^ of that type captures the root capability `cap`. - | - | where: ^ refers to the universal root capability -- [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 // error // error +17 | val x: Boxed[IO^] = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x) // error | ^^^^^^ |Found: (x: Boxed[IO^]^'s3) ->'s4 Boxed[IO^²] |Required: Boxed[IO^] -> Boxed[IO^³] diff --git a/tests/neg-custom-args/captures/i21401.scala b/tests/neg-custom-args/captures/i21401.scala index af82fb88002d..da90a65d364a 100644 --- a/tests/neg-custom-args/captures/i21401.scala +++ b/tests/neg-custom-args/captures/i21401.scala @@ -10,10 +10,10 @@ type Res = [R, X <: Boxed[IO^] -> R] -> (op: X) -> R def mkRes(x: IO^): Res = [R, X <: Boxed[IO^] -> R] => (op: X) => val op1: Boxed[IO^] -> R = op - op1(Boxed[IO^](x)) // error + op1(Boxed[IO^](x)) def test2() = - val a = usingIO[IO^](x => x) // error // error + val a = usingIO[IO^](x => x) // error val leaked: [R, X <: Boxed[IO^] -> R] -> (op: X) -> R = usingIO[Res](mkRes) // error - val x: Boxed[IO^] = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x) // error // error // error + val x: Boxed[IO^] = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x) // error val y: IO^{x*} = x.unbox // was error y.println("boom") diff --git a/tests/neg-custom-args/captures/levels.check b/tests/neg-custom-args/captures/levels.check index a7650a8ad19f..43a96dda25ba 100644 --- a/tests/neg-custom-args/captures/levels.check +++ b/tests/neg-custom-args/captures/levels.check @@ -1,10 +1,3 @@ --- Error: tests/neg-custom-args/captures/levels.scala:17:21 ------------------------------------------------------------ -17 | val _ = Ref[String => String]((x: String) => x) // error - | ^^^^^^^^^^^^^^^^ - | Type variable T of constructor Ref cannot be instantiated to String => String since - | that type captures the root capability `cap`. - | - | where: => refers to the universal root capability -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/levels.scala:22:11 --------------------------------------- 22 | r.setV(g) // error | ^ diff --git a/tests/neg-custom-args/captures/levels.scala b/tests/neg-custom-args/captures/levels.scala index b28e87f03ef7..d15984ed25c2 100644 --- a/tests/neg-custom-args/captures/levels.scala +++ b/tests/neg-custom-args/captures/levels.scala @@ -14,7 +14,7 @@ def test2(cap1: CC^) = def setV(x: T): Unit = v = x def getV: T = v - val _ = Ref[String => String]((x: String) => x) // error + val _ = Ref[String => String]((x: String) => x) val r = Ref((x: String) => x) def scope(cap3: CC^) = diff --git a/tests/neg-custom-args/captures/outer-var.check b/tests/neg-custom-args/captures/outer-var.check index ae9f6f3619a0..4cb75e7415fe 100644 --- a/tests/neg-custom-args/captures/outer-var.check +++ b/tests/neg-custom-args/captures/outer-var.check @@ -44,10 +44,3 @@ | where: => refers to a fresh root capability in the type of parameter q | | longer explanation available when compiling with `-explain` --- Error: tests/neg-custom-args/captures/outer-var.scala:17:57 --------------------------------------------------------- -17 | var finalizeActions = collection.mutable.ListBuffer[() => Unit]() // error, was OK under unsealed - | ^^^^^^^^^^ - | Type variable A of object ListBuffer cannot be instantiated to () => Unit since - | that type captures the root capability `cap`. - | - | where: => refers to the universal root capability diff --git a/tests/neg-custom-args/captures/outer-var.scala b/tests/neg-custom-args/captures/outer-var.scala index eb82312d4b37..aec79f546df7 100644 --- a/tests/neg-custom-args/captures/outer-var.scala +++ b/tests/neg-custom-args/captures/outer-var.scala @@ -14,6 +14,6 @@ def test(p: Proc, q: () => Unit) = y = (q: Proc) // error y = q // error, was OK under unsealed - var finalizeActions = collection.mutable.ListBuffer[() => Unit]() // error, was OK under unsealed + var finalizeActions = collection.mutable.ListBuffer[() => Unit]() // now ok diff --git a/tests/neg-custom-args/captures/reaches.check b/tests/neg-custom-args/captures/reaches.check index 8c099c520d60..7a0018962776 100644 --- a/tests/neg-custom-args/captures/reaches.check +++ b/tests/neg-custom-args/captures/reaches.check @@ -27,46 +27,20 @@ 32 | (() => f.write()) :: Nil | | longer explanation available when compiling with `-explain` --- Error: tests/neg-custom-args/captures/reaches.scala:42:16 ----------------------------------------------------------- -42 | val cur = Ref[List[Proc]](xs) // error - | ^^^^^^^^^^ - | Type variable T of constructor Ref cannot be instantiated to List[() => Unit] since - | the part () => Unit of that type captures the root capability `cap`. - | - | where: => refers to the universal root capability --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:44:35 -------------------------------------- -44 | val next: () => Unit = cur.get.head // error - | ^^^^^^^^^^^^ - | Found: () => Unit - | Required: () =>² Unit +-- [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: Id[() => Unit, () -> Unit] + | Required: Id[() =>² Unit, () =>³ Unit] | | Note that capability cap is not included in capture set {cap²} - | because cap is not visible from cap² in value next. + | because cap is not visible from cap² in value id. | - | where: => and cap refer to the universal root capability - | =>² and cap² refer to a fresh root capability in the type of value next + | where: => and cap² refer to a fresh root capability created in value id + | =>² and cap refer to the universal root capability + | =>³ refers to a fresh root capability in the type of value id | | longer explanation available when compiling with `-explain` --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:46:20 -------------------------------------- -46 | cur.set(cur.get.tail: List[Proc]) // error - | ^^^^^^^^^^^^ - | Found: List[() => Unit] - | Required: List[() =>² Unit] - | - | Note that capability cap is not included in capture set {cap²} - | because cap is not visible from cap² in method runAll3. - | - | where: => and cap refer to the universal root capability - | =>² and cap² refer to a fresh root capability created in method runAll3 - | - | longer explanation available when compiling with `-explain` --- Error: tests/neg-custom-args/captures/reaches.scala:52:51 ----------------------------------------------------------- -52 | val id: Id[Proc, Proc] = new Id[Proc, () -> Unit] // error - | ^ - | Type variable A of constructor Id cannot be instantiated to () => Unit since - | that type captures the root capability `cap`. - | - | where: => refers to the universal root capability -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:57:27 -------------------------------------- 57 | val id: File^ -> File^ = x => x // error | ^^^^^^ @@ -121,6 +95,11 @@ | ^^^^^^^^ | Local reach capability xs* leaks into capture scope of method runAll2. | You could try to abstract the capabilities referred to by xs* in a capset variable. +-- Error: tests/neg-custom-args/captures/reaches.scala:44:35 ----------------------------------------------------------- +44 | val next: () => Unit = cur.get.head // error // error + | ^^^^^^^^^^^^ + | Local reach capability xs* leaks into capture scope of method runAll3. + | You could try to abstract the capabilities referred to by xs* in a capset variable. -- Error: tests/neg-custom-args/captures/reaches.scala:60:36 ----------------------------------------------------------- 60 | val leaked = usingFile[File^{id*}]: f => // error: separation | ^ @@ -129,3 +108,13 @@ | where: cap is a fresh root capability created in value id of parameter parameter x of method $anonfun 61 | val f1: File^{id*} = id(f) 62 | f1 +-- Error: tests/neg-custom-args/captures/reaches.scala:42:9 ------------------------------------------------------------ +42 | val cur = Ref[List[Proc]](xs) // error + | ^ + | Separation failure: value cur's inferred type Ref[List[() => Unit]^{}]^{} hides parameter xs. + | The parameter needs to be annotated with consume to allow this. +-- Error: tests/neg-custom-args/captures/reaches.scala:44:17 ----------------------------------------------------------- +44 | val next: () => Unit = cur.get.head // error // error + | ^^^^^^^^^^ + | Separation failure: value next's type () => Unit hides parameter xs. + | The parameter needs to be annotated with consume to allow this. diff --git a/tests/neg-custom-args/captures/reaches.scala b/tests/neg-custom-args/captures/reaches.scala index 2c700baccef5..bbbf3830c759 100644 --- a/tests/neg-custom-args/captures/reaches.scala +++ b/tests/neg-custom-args/captures/reaches.scala @@ -41,9 +41,9 @@ def runAll2(consume xs: List[Proc]): Unit = def runAll3(xs: List[Proc]): Unit = val cur = Ref[List[Proc]](xs) // error while cur.get.nonEmpty do - val next: () => Unit = cur.get.head // error + val next: () => Unit = cur.get.head // error // error next() - cur.set(cur.get.tail: List[Proc]) // error + cur.set(cur.get.tail: List[Proc]) class Id[-A, +B >: A](): def apply(a: A): B = a diff --git a/tests/neg-custom-args/captures/try.check b/tests/neg-custom-args/captures/try.check index 33b69e0e3fd6..d33c008aeb0a 100644 --- a/tests/neg-custom-args/captures/try.check +++ b/tests/neg-custom-args/captures/try.check @@ -1,10 +1,3 @@ --- Error: tests/neg-custom-args/captures/try.scala:23:28 --------------------------------------------------------------- -23 | val a = handle[Exception, CanThrow[Exception]] { // error - | ^^^^^^^^^^^^^^^^^^^ - | Type variable R of method handle cannot be instantiated to CT[Exception]^ since - | that type captures the root capability `cap`. - | - | where: ^ refers to the universal root capability -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:24:4 ------------------------------------------- 24 | (x: CanThrow[Exception]) => x // error | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ @@ -16,7 +9,7 @@ | |where: => refers to a fresh root capability created in value a when checking argument to parameter op of method handle | ^ refers to the universal root capability - | ^² and cap refer to a fresh root capability created in value a when checking argument to parameter op of method handle + | ^² and cap refer to a fresh root capability created in value a | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:30:4 ------------------------------------------- diff --git a/tests/neg-custom-args/captures/try.scala b/tests/neg-custom-args/captures/try.scala index 7656fd3e45ee..af8d2d2fdf70 100644 --- a/tests/neg-custom-args/captures/try.scala +++ b/tests/neg-custom-args/captures/try.scala @@ -20,7 +20,7 @@ def handle[E <: Exception, R <: Top](op: CT[E]^ => R)(handler: E => R): R = catch case ex: E => handler(ex) def test = - val a = handle[Exception, CanThrow[Exception]] { // error + val a = handle[Exception, CanThrow[Exception]] { (x: CanThrow[Exception]) => x // error }{ (ex: Exception) => ??? diff --git a/tests/neg-custom-args/captures/unsound-reach.check b/tests/neg-custom-args/captures/unsound-reach.check index b06515b42053..fa65c92ba8f5 100644 --- a/tests/neg-custom-args/captures/unsound-reach.check +++ b/tests/neg-custom-args/captures/unsound-reach.check @@ -5,15 +5,8 @@ | that type captures the root capability `cap`. | | where: ^ refers to the universal root capability --- Error: tests/neg-custom-args/captures/unsound-reach.scala:14:19 ----------------------------------------------------- -14 |class Bar2 extends Foo2[File^]: // error - | ^ - | Type variable X of constructor Foo2 cannot be instantiated to File^ since - | that type captures the root capability `cap`. - | - | where: ^ refers to the universal root capability -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/unsound-reach.scala:18:31 -------------------------------- -18 | val backdoor: Foo[File^] = new Bar // error (follow-on, since the parent Foo[File^] of bar is illegal). +18 | val backdoor: Foo[File^] = new Bar // error | ^^^^^^^ | Found: Bar | Required: Foo[File^] @@ -25,3 +18,16 @@ | cap is the universal root capability | | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/unsound-reach.scala:27:32 -------------------------------- +27 | val backdoor: Foo2[File^] = new Bar2 // error + | ^^^^^^^^ + | Found: Bar2 + | Required: Foo2[File^] + | + | Note that capability cap is not included in capture set {cap²} + | because cap is not visible from cap² in value backdoor. + | + | where: ^ and cap² refer to a fresh root capability in the type of value backdoor + | cap is the universal root capability + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/unsound-reach.scala b/tests/neg-custom-args/captures/unsound-reach.scala index a53b091c5918..bf58e06b56bd 100644 --- a/tests/neg-custom-args/captures/unsound-reach.scala +++ b/tests/neg-custom-args/captures/unsound-reach.scala @@ -11,11 +11,11 @@ class Bar extends Foo[File^]: // error abstract class Foo2[+X](): def use(x: File^)(op: X => Unit): Unit -class Bar2 extends Foo2[File^]: // error +class Bar2 extends Foo2[File^]: // no error, since we check only parent types, and Foo2[File^] is a constructor application def use(x: File^)(op: File^ => Unit): Unit = op(x) // OK using sealed checking def bad(): Unit = - val backdoor: Foo[File^] = new Bar // error (follow-on, since the parent Foo[File^] of bar is illegal). + val backdoor: Foo[File^] = new Bar // error val boom: Foo[File^{backdoor*}] = backdoor var escaped: File^{backdoor*} = null @@ -23,3 +23,12 @@ def bad(): Unit = boom.use(f): (f1: File^{backdoor*}) => // was error escaped = f1 +def bad2(): Unit = + val backdoor: Foo2[File^] = new Bar2 // error + val boom: Foo2[File^{backdoor*}] = backdoor + + var escaped: File^{backdoor*} = null + withFile("hello.txt"): f => + boom.use(f): (f1: File^{backdoor*}) => // was error + escaped = f1 + diff --git a/tests/neg-custom-args/captures/withFile.scala b/tests/neg-custom-args/captures/withFile.scala index 8e287d8631ba..1eb458f8db83 100644 --- a/tests/neg-custom-args/captures/withFile.scala +++ b/tests/neg-custom-args/captures/withFile.scala @@ -13,7 +13,7 @@ object Test2: private val later1 = usingLogFile { f => () => f.write() } // error private val later2 = usingLogFile { f => Box(f) } // error - private val later3 = usingLogFile[() => Unit]: // error + private val later3 = usingLogFile[() => Unit]: f => () => f.write() // error - private val later4 = usingLogFile[Box[File^]]: // error + private val later4 = usingLogFile[Box[File^]]: f => Box(f) // error diff --git a/tests/neg-custom-args/captures/i23389.scala b/tests/pos-custom-args/captures/i23389.scala similarity index 90% rename from tests/neg-custom-args/captures/i23389.scala rename to tests/pos-custom-args/captures/i23389.scala index 3962949e2088..54e5ef0ff24f 100644 --- a/tests/neg-custom-args/captures/i23389.scala +++ b/tests/pos-custom-args/captures/i23389.scala @@ -16,8 +16,8 @@ package test1: object FooImpl1 extends Foo: val thunks: Collection[() => Unit] = Collection.empty // was error, now ok - val thunks2: Collection[() => Unit] = Collection.empty[() => Unit] // error - val thunks3: Collection[() => Unit] = Collection.empty[() => Unit] // error + val thunks2: Collection[() => Unit] = Collection.empty[() => Unit] // was error, now ok + val thunks3: Collection[() => Unit] = Collection.empty[() => Unit] // was error, now ok package test2: @@ -32,5 +32,5 @@ package test2: object FooImpl1 extends Foo: val thunks: Collection[() => Unit] = Collection.empty // was error, now ok - val thunks2: Collection[() => Unit] = Collection.empty[() => Unit] // error - val thunks3: Collection[() => Unit] = Collection.empty[() => Unit] // error + val thunks2: Collection[() => Unit] = Collection.empty[() => Unit] // was error, now ok + val thunks3: Collection[() => Unit] = Collection.empty[() => Unit] // was error, now ok From 9180c55220719fdb34ec12290c8394abfad615e7 Mon Sep 17 00:00:00 2001 From: odersky Date: Thu, 6 Nov 2025 18:24:10 +0100 Subject: [PATCH 2/2] Also freshen type arguments in parent classes --- compiler/src/dotty/tools/dotc/cc/Setup.scala | 12 +++++------- tests/neg-custom-args/captures/hk-param.scala | 2 +- tests/neg-custom-args/captures/unsound-reach-4.check | 11 ++++++----- tests/neg-custom-args/captures/unsound-reach.check | 8 ++++---- 4 files changed, 16 insertions(+), 17 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala index f12c4ecb1f1b..bb29ed3b7947 100644 --- a/compiler/src/dotty/tools/dotc/cc/Setup.scala +++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala @@ -158,7 +158,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: def mappedInfo = if toBeUpdated.contains(sym) then symd.info // don't transform symbols that will anyway be updated - else transformExplicitType(symd.info, sym, freshen = true) + else transformExplicitType(symd.info, sym) if Synthetics.needsTransform(symd) then Synthetics.transform(symd, mappedInfo) else if isPreCC(sym) then @@ -340,7 +340,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: * 5. Schedule deferred well-formed tests for types with retains annotations. * 6. Perform normalizeCaptures */ - private def transformExplicitType(tp: Type, sym: Symbol, freshen: Boolean, tptToCheck: Tree = EmptyTree)(using Context): Type = + private def transformExplicitType(tp: Type, sym: Symbol, tptToCheck: Tree = EmptyTree)(using Context): Type = def fail(msg: Message) = if !tptToCheck.isEmpty then report.error(msg, tptToCheck.srcPos) @@ -474,9 +474,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: val tp3 = if sym.isType then stripImpliedCaptureSet(tp2) else tp2 - if freshen then - capToFresh(tp3, Origin.InDecl(sym)) - else tp3 + capToFresh(tp3, Origin.InDecl(sym)) end transformExplicitType /** Update info of `sym` for CheckCaptures phase only */ @@ -501,7 +499,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: var transformed = if tree.isInferred then transformInferredType(tree.tpe) - else transformExplicitType(tree.tpe, sym, freshen = true, tptToCheck = tree) + else transformExplicitType(tree.tpe, sym, tptToCheck = tree) if boxed then transformed = transformed.boxDeeply tree.setNuType( if sym.hasAnnotation(defn.UncheckedCapturesAnnot) then makeUnchecked(transformed) @@ -725,7 +723,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: // Compute new parent types val ps1 = inContext(ctx.withOwner(cls)): - ps.mapConserve(transformExplicitType(_, NoSymbol, freshen = false)) + ps.mapConserve(transformExplicitType(_, NoSymbol)) // Install new types and if it is a module class also update module object if (selfInfo1 ne selfInfo) || (ps1 ne ps) then diff --git a/tests/neg-custom-args/captures/hk-param.scala b/tests/neg-custom-args/captures/hk-param.scala index bfd4f82a0697..de50828c859c 100644 --- a/tests/neg-custom-args/captures/hk-param.scala +++ b/tests/neg-custom-args/captures/hk-param.scala @@ -1,6 +1,6 @@ /** Concrete collection type: View */ trait View[+A] extends Itable[A], ILike[A, [X] =>> View[X]^]: // error - override def fromIterable[B](c: Itable[B]^): View[B]^{c} = ??? + override def fromIterable[B](c: Itable[B]^): View[B]^{c} = ??? // error trait IPolyTransforms[+A, +C[A]] extends Any: def fromIterable[B](coll: Itable[B]^): C[B] diff --git a/tests/neg-custom-args/captures/unsound-reach-4.check b/tests/neg-custom-args/captures/unsound-reach-4.check index 441a6c25aec7..6e4271cf0057 100644 --- a/tests/neg-custom-args/captures/unsound-reach-4.check +++ b/tests/neg-custom-args/captures/unsound-reach-4.check @@ -12,19 +12,20 @@ | Required: Foo[File^] | | Note that capability cap is not included in capture set {cap²} - | because cap is not visible from cap² in value backdoor. + | because cap in class Bar is not visible from cap² in value backdoor. | | where: ^ and cap² refer to a fresh root capability in the type of value backdoor - | cap is the universal root capability + | cap is a fresh root capability created in class Bar | | longer explanation available when compiling with `-explain` -- [E164] Declaration Error: tests/neg-custom-args/captures/unsound-reach-4.scala:17:6 --------------------------------- 17 | def use(consume x: F): File^ = x // error consume override | ^ - | error overriding method use in trait Foo of type (x: File^): File^; - | method use of type (@consume x: File^): File^² has incompatible type + | error overriding method use in trait Foo of type (x: File^): File^²; + | method use of type (@consume x: File^): File^³ has incompatible type | | where: ^ refers to the universal root capability - | ^² refers to a root capability associated with the result type of (@consume x: File^): File^² + | ^² refers to a fresh root capability created in class Bar + | ^³ refers to a root capability associated with the result type of (@consume x: File^): File^³ | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/unsound-reach.check b/tests/neg-custom-args/captures/unsound-reach.check index fa65c92ba8f5..e426cec0c0ac 100644 --- a/tests/neg-custom-args/captures/unsound-reach.check +++ b/tests/neg-custom-args/captures/unsound-reach.check @@ -12,10 +12,10 @@ | Required: Foo[File^] | | Note that capability cap is not included in capture set {cap²} - | because cap is not visible from cap² in value backdoor. + | because cap in class Bar is not visible from cap² in value backdoor. | | where: ^ and cap² refer to a fresh root capability in the type of value backdoor - | cap is the universal root capability + | cap is a fresh root capability created in class Bar | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/unsound-reach.scala:27:32 -------------------------------- @@ -25,9 +25,9 @@ | Required: Foo2[File^] | | Note that capability cap is not included in capture set {cap²} - | because cap is not visible from cap² in value backdoor. + | because cap in class Bar2 is not visible from cap² in value backdoor. | | where: ^ and cap² refer to a fresh root capability in the type of value backdoor - | cap is the universal root capability + | cap is a fresh root capability created in class Bar2 | | longer explanation available when compiling with `-explain`