From bb4ae9c5c3f43ddadb8664428d8f1c90452b0cea Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Tue, 24 Jun 2025 23:15:25 +0200 Subject: [PATCH 1/8] Minor improvements --- compiler/src/dotty/tools/dotc/cc/Capability.scala | 4 ++-- compiler/src/dotty/tools/dotc/cc/Setup.scala | 1 - 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala index 86bc8aa1ca66..f350a019de46 100644 --- a/compiler/src/dotty/tools/dotc/cc/Capability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala @@ -784,7 +784,7 @@ object Capabilities: abstract class CapMap extends BiTypeMap: override def mapOver(t: Type): Type = t match case t @ FunctionOrMethod(args, res) if variance > 0 && !t.isAliasFun => - t // `t` should be mapped in this case by a different call to `mapCap`. + t // `t` should be mapped in this case by a different call to `toResult`. See [[toResultInResults]]. case t: (LazyRef | TypeVar) => mapConserveSuper(t) case _ => @@ -882,4 +882,4 @@ object Capabilities: case tp1 => tp1 end toResultInResults -end Capabilities \ No newline at end of file +end Capabilities diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala index 752a1a469c39..6143a7131e32 100644 --- a/compiler/src/dotty/tools/dotc/cc/Setup.scala +++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala @@ -18,7 +18,6 @@ import reporting.Message import printing.{Printer, Texts}, Texts.{Text, Str} import collection.mutable import CCState.* -import dotty.tools.dotc.util.NoSourcePosition import CheckCaptures.CheckerAPI import NamerOps.methodType import NameKinds.{CanThrowEvidenceName, TryOwnerName} From c35fbe410fcc4ae2c9eec7ed051cc47ac60c327e Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Wed, 25 Jun 2025 15:10:36 +0200 Subject: [PATCH 2/8] Freshen invariant occurrences of `cap`s --- .../src/dotty/tools/dotc/cc/Capability.scala | 4 +++- .../neg-custom-args/captures/boundschecks3.check | 4 ++-- .../captures/box-adapt-cases.check | 11 ----------- .../captures/box-adapt-cases.scala | 2 +- .../captures/class-level-attack.check | 16 ++++++++++++++++ .../captures/class-level-attack.scala | 5 ++--- tests/neg-custom-args/captures/i16725.scala | 6 +++--- 7 files changed, 27 insertions(+), 21 deletions(-) create mode 100644 tests/neg-custom-args/captures/class-level-attack.check diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala index f350a019de46..d46a625b0d64 100644 --- a/compiler/src/dotty/tools/dotc/cc/Capability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala @@ -693,7 +693,7 @@ object Capabilities: thisMap => override def apply(t: Type) = - if variance <= 0 then t + if variance < 0 then t else t match case t @ CapturingType(_, _) => mapOver(t) @@ -703,6 +703,8 @@ object Capabilities: this(CapturingType(parent1, ann.tree.toCaptureSet)) else t.derivedAnnotatedType(parent1, ann) + case t @ FunctionOrMethod(_, _) if t.isAliasFun => + t // stop at dependent function types case _ => mapFollowingAliases(t) diff --git a/tests/neg-custom-args/captures/boundschecks3.check b/tests/neg-custom-args/captures/boundschecks3.check index 51881f2a454f..57bcf8cbc32a 100644 --- a/tests/neg-custom-args/captures/boundschecks3.check +++ b/tests/neg-custom-args/captures/boundschecks3.check @@ -3,7 +3,7 @@ | ^ | Type argument test.Tree^ does not conform to upper bound test.Tree in inferred type test.C[test.Tree^] | - | where: ^ refers to the universal root capability + | where: ^ refers to a fresh root capability in the type of value foo | | longer explanation available when compiling with `-explain` -- [E057] Type Mismatch Error: tests/neg-custom-args/captures/boundschecks3.scala:10:11 -------------------------------- @@ -11,7 +11,7 @@ | ^ | Type argument test.Tree^ does not conform to upper bound test.Tree in inferred type test.C[test.Tree^] | - | where: ^ refers to the universal root capability + | where: ^ refers to a fresh root capability in the type of type T | | longer explanation available when compiling with `-explain` -- [E057] Type Mismatch Error: tests/neg-custom-args/captures/boundschecks3.scala:11:11 -------------------------------- diff --git a/tests/neg-custom-args/captures/box-adapt-cases.check b/tests/neg-custom-args/captures/box-adapt-cases.check index fc161baf341f..330fd196023b 100644 --- a/tests/neg-custom-args/captures/box-adapt-cases.check +++ b/tests/neg-custom-args/captures/box-adapt-cases.check @@ -1,14 +1,3 @@ --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/box-adapt-cases.scala:8:10 ------------------------------- -8 | x.value(cap => cap.use()) // error, was OK - | ^^^^^^^^^^^^^^^^ - | Found: (cap: Cap^?) => Int - | Required: Cap^ =>² Int - | - | where: => refers to the universal root capability - | =>² refers to a fresh root capability created in method test1 - | ^ refers to the universal root capability - | - | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/box-adapt-cases.scala:15:10 ------------------------------ 15 | x.value(cap => cap.use()) // error | ^^^^^^^^^^^^^^^^ diff --git a/tests/neg-custom-args/captures/box-adapt-cases.scala b/tests/neg-custom-args/captures/box-adapt-cases.scala index 7db58318ed05..af79e1fcb6f6 100644 --- a/tests/neg-custom-args/captures/box-adapt-cases.scala +++ b/tests/neg-custom-args/captures/box-adapt-cases.scala @@ -5,7 +5,7 @@ def test1(): Unit = { class Id[X](val value: [T] -> (op: X => T) -> T) val x: Id[Cap^] = ??? - x.value(cap => cap.use()) // error, was OK + x.value(cap => cap.use()) } def test2(io: Cap^): Unit = { diff --git a/tests/neg-custom-args/captures/class-level-attack.check b/tests/neg-custom-args/captures/class-level-attack.check new file mode 100644 index 000000000000..a2f60535d86f --- /dev/null +++ b/tests/neg-custom-args/captures/class-level-attack.check @@ -0,0 +1,16 @@ +-- 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 + | ^ + | Found: IO^{x} + | Required: IO^ + | + | where: ^ refers to a fresh root capability in the type of value r + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/class-level-attack.scala b/tests/neg-custom-args/captures/class-level-attack.scala index 19d681198e8c..b9847ea4045d 100644 --- a/tests/neg-custom-args/captures/class-level-attack.scala +++ b/tests/neg-custom-args/captures/class-level-attack.scala @@ -13,9 +13,8 @@ class C(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 - val r2: Ref[IO^] = Ref(io) // error: - //Error: Ref[IO^{io}] does not conform to Ref[IO^] (since Refs are invariant) - def set(x: IO^) = r.put(x) + val r2: Ref[IO^] = Ref(io) + def set(x: IO^) = r.put(x) // error def outer(outerio: IO^) = val c = C(outerio) diff --git a/tests/neg-custom-args/captures/i16725.scala b/tests/neg-custom-args/captures/i16725.scala index 96cf44e72f3c..3422ae537c92 100644 --- a/tests/neg-custom-args/captures/i16725.scala +++ b/tests/neg-custom-args/captures/i16725.scala @@ -6,9 +6,9 @@ def usingIO[T](op: IO => T): T = ??? class Wrapper[T](val value: [R] -> (f: T => R) -> R) def mk[T](x: T): Wrapper[T] = Wrapper([R] => f => f(x)) def useWrappedIO(wrapper: Wrapper[IO]): () -> Unit = - () => - wrapper.value: io => // error + () => // error + wrapper.value: io => io.brewCoffee() def main(): Unit = - val escaped = usingIO(io => useWrappedIO(mk(io))) // error + val escaped = usingIO(io => useWrappedIO(mk(io))) escaped() // boom From 62ea061561fd58faa8dc31a3c78677955f2a5abd Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Wed, 25 Jun 2025 17:12:20 +0200 Subject: [PATCH 3/8] Add result caps for type-parameter-only `def`s --- compiler/src/dotty/tools/dotc/cc/Capability.scala | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala index d46a625b0d64..2678275a4bd0 100644 --- a/compiler/src/dotty/tools/dotc/cc/Capability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala @@ -21,7 +21,7 @@ import annotation.constructorOnly import ast.tpd import printing.{Printer, Showable} import printing.Texts.Text -import reporting.Message +import reporting.{Message, trace} import NameOps.isImpureFunction import annotation.internal.sharable @@ -881,6 +881,8 @@ object Capabilities: m(tp) match case tp1: ExprType if sym.is(Method, butNot = Accessor) => tp1.derivedExprType(toResult(tp1.resType, tp1, fail)) + case tp1: PolyType if !tp1.resType.isInstanceOf[MethodicType] => + tp1.derivedLambdaType(resType = toResult(tp1.resType, tp1, fail)) case tp1 => tp1 end toResultInResults From 8dd6fd4a48df7090bd9366aba826682973a299c4 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Wed, 25 Jun 2025 17:12:51 +0200 Subject: [PATCH 4/8] chore: drop one unused import --- compiler/src/dotty/tools/dotc/cc/CaptureSet.scala | 1 - 1 file changed, 1 deletion(-) diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index 47c96e604784..37ee3f68b9ad 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala @@ -14,7 +14,6 @@ import printing.{Showable, Printer} import printing.Texts.* import util.{SimpleIdentitySet, Property} import typer.ErrorReporting.Addenda -import util.common.alwaysTrue import scala.collection.{mutable, immutable} import TypeComparer.ErrorNote import CCState.* From 16e8d0d5d1ff0d76b898075d140d0f1c94bba0a8 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Wed, 25 Jun 2025 22:07:15 +0200 Subject: [PATCH 5/8] Document `toResultInResults` and add test cases --- .../src/dotty/tools/dotc/cc/Capability.scala | 12 +++++++++++- .../captures/cc-fresh-levels.check | 19 +++++++++++++++++++ .../captures/cc-fresh-levels.scala | 19 +++++++++++++++++++ .../captures/cc-def-fresh.scala | 10 ++++++++++ tests/pos-custom-args/captures/i23421.scala | 16 ++++++++++++++++ 5 files changed, 75 insertions(+), 1 deletion(-) create mode 100644 tests/neg-custom-args/captures/cc-fresh-levels.check create mode 100644 tests/neg-custom-args/captures/cc-fresh-levels.scala create mode 100644 tests/pos-custom-args/captures/cc-def-fresh.scala create mode 100644 tests/pos-custom-args/captures/i23421.scala diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala index 2678275a4bd0..ff01e0ddfc7b 100644 --- a/compiler/src/dotty/tools/dotc/cc/Capability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala @@ -851,7 +851,8 @@ object Capabilities: end toResult /** Map global roots in function results to result roots. Also, - * map roots in the types of parameterless def methods. + * map roots in the types of def methods that are parameterless + * or have only type parameters. */ def toResultInResults(sym: Symbol, fail: Message => Unit, keepAliases: Boolean = false)(tp: Type)(using Context): Type = val m = new TypeMap with FollowAliasesMap: @@ -880,8 +881,17 @@ object Capabilities: throw ex m(tp) match case tp1: ExprType if sym.is(Method, butNot = Accessor) => + // Map the result of parameterless `def` methods. tp1.derivedExprType(toResult(tp1.resType, tp1, fail)) case tp1: PolyType if !tp1.resType.isInstanceOf[MethodicType] => + // Map also the result type of method with only type parameters. + // This way, the `^` in the following method will be mapped to a `ResultCap`: + // ``` + // object Buffer: + // def empty[T]: Buffer[T]^ + // ``` + // This is more desirable than interpreting `^` as a `Fresh` at the level of `Buffer.empty` + // in most cases. tp1.derivedLambdaType(resType = toResult(tp1.resType, tp1, fail)) case tp1 => tp1 end toResultInResults diff --git a/tests/neg-custom-args/captures/cc-fresh-levels.check b/tests/neg-custom-args/captures/cc-fresh-levels.check new file mode 100644 index 000000000000..09d122f1d8a8 --- /dev/null +++ b/tests/neg-custom-args/captures/cc-fresh-levels.check @@ -0,0 +1,19 @@ +Flag -source set repeatedly +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-fresh-levels.scala:14:10 ------------------------------ +14 | r.put(x) // error + | ^ + | Found: IO^{x} + | Required: IO^ + | + | where: ^ refers to a fresh root capability in the type of value r + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-fresh-levels.scala:17:10 ------------------------------ +17 | r.put(innerIO) // error + | ^^^^^^^ + | Found: IO^{innerIO} + | Required: IO^ + | + | where: ^ refers to a fresh root capability in the type of value r + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/cc-fresh-levels.scala b/tests/neg-custom-args/captures/cc-fresh-levels.scala new file mode 100644 index 000000000000..c8f6e4d9bbac --- /dev/null +++ b/tests/neg-custom-args/captures/cc-fresh-levels.scala @@ -0,0 +1,19 @@ +//> using options -source 3.7 +import language.experimental.captureChecking +import caps.* +class IO +class Ref[X](init: X): + private var _data = init + def get: X = _data + def put(y: X): Unit = _data = y +def runIO(op: IO^ => Unit): Unit = () +def test1(a: IO^, b: IO^, c: IO^): Unit = + val r: Ref[IO^] = Ref(a) + r.put(b) // ok + def outer(x: IO^): Unit = + r.put(x) // error + r.put(c) // ok + runIO: (innerIO: IO^) => + r.put(innerIO) // error + runIO: innerIO => + r.put(innerIO) // should be error, but ok // unsound diff --git a/tests/pos-custom-args/captures/cc-def-fresh.scala b/tests/pos-custom-args/captures/cc-def-fresh.scala new file mode 100644 index 000000000000..4e426326f434 --- /dev/null +++ b/tests/pos-custom-args/captures/cc-def-fresh.scala @@ -0,0 +1,10 @@ +import language.experimental.captureChecking +trait Collection[T] +trait IO +def empty[T]: Collection[T]^ = ??? +def emptyAlt[T](): Collection[T]^ = ??? +def newIO: IO^ = ??? +def test1(): Unit = + val t1: Collection[Int]^ = empty[Int] // ok + val t2: IO^ = newIO // ok + val t3: Collection[Int]^ = emptyAlt[Int]() // ok diff --git a/tests/pos-custom-args/captures/i23421.scala b/tests/pos-custom-args/captures/i23421.scala new file mode 100644 index 000000000000..ef5e7564073e --- /dev/null +++ b/tests/pos-custom-args/captures/i23421.scala @@ -0,0 +1,16 @@ +import language.experimental.captureChecking +import caps.* + +trait Collection[T] extends Mutable: + update def add(elem: T): Unit + update def remove(elem: T): Unit + def get(index: Int): Option[T] + +object Collection: + def empty[T]: Collection[T] = ??? + +trait Foo: + val thunks: Collection[() => Unit] // that's fine + +object FooImpl1 extends Foo: + val thunks: Collection[() => Unit] = Collection.empty // was error, now ok From eaf441ce8d81bcafc110e82697ed3e2d023536e8 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Wed, 25 Jun 2025 23:48:19 +0200 Subject: [PATCH 6/8] Update testcase --- tests/neg-custom-args/captures/i23389.scala | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/neg-custom-args/captures/i23389.scala b/tests/neg-custom-args/captures/i23389.scala index cb62a5e69a2c..3962949e2088 100644 --- a/tests/neg-custom-args/captures/i23389.scala +++ b/tests/neg-custom-args/captures/i23389.scala @@ -15,7 +15,7 @@ package test1: val thunks: Collection[() => Unit] // that's fine object FooImpl1 extends Foo: - val thunks: Collection[() => Unit] = Collection.empty // error + 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 @@ -31,6 +31,6 @@ package test2: val thunks: Collection[() => Unit] // that's fine object FooImpl1 extends Foo: - val thunks: Collection[() => Unit] = Collection.empty // error + 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 \ No newline at end of file + val thunks3: Collection[() => Unit] = Collection.empty[() => Unit] // error From 43b1626b46eb99704166e1f8a45e3218fd4ef6e5 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Fri, 27 Jun 2025 14:54:01 +0200 Subject: [PATCH 7/8] Use `RefinedFunctionOf` instead of `FunctionOrMethod` --- compiler/src/dotty/tools/dotc/cc/Capability.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala index ff01e0ddfc7b..5c1de33aea0e 100644 --- a/compiler/src/dotty/tools/dotc/cc/Capability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala @@ -703,7 +703,7 @@ object Capabilities: this(CapturingType(parent1, ann.tree.toCaptureSet)) else t.derivedAnnotatedType(parent1, ann) - case t @ FunctionOrMethod(_, _) if t.isAliasFun => + case defn.RefinedFunctionOf(_) => t // stop at dependent function types case _ => mapFollowingAliases(t) From 57b09a3418408c42978e5231cdbffa54516bba02 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Fri, 27 Jun 2025 16:28:24 +0200 Subject: [PATCH 8/8] Update cc-fresh-levels.scala It was unsound, but fixed now on main. --- tests/neg-custom-args/captures/cc-fresh-levels.check | 11 +++++++++++ tests/neg-custom-args/captures/cc-fresh-levels.scala | 4 ++-- 2 files changed, 13 insertions(+), 2 deletions(-) diff --git a/tests/neg-custom-args/captures/cc-fresh-levels.check b/tests/neg-custom-args/captures/cc-fresh-levels.check index 09d122f1d8a8..029ee9280993 100644 --- a/tests/neg-custom-args/captures/cc-fresh-levels.check +++ b/tests/neg-custom-args/captures/cc-fresh-levels.check @@ -17,3 +17,14 @@ Flag -source set repeatedly | where: ^ refers to a fresh root capability in the type of value r | | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-fresh-levels.scala:18:9 ------------------------------- +18 | runIO: innerIO => // error + | ^ + |Found: (innerIO: IO^?) ->? Unit + |Required: IO^ => Unit + | + |where: => refers to a fresh root capability created in method test1 when checking argument to parameter op of method runIO + | ^ refers to the universal root capability +19 | r.put(innerIO) + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/cc-fresh-levels.scala b/tests/neg-custom-args/captures/cc-fresh-levels.scala index c8f6e4d9bbac..4cbd079ad627 100644 --- a/tests/neg-custom-args/captures/cc-fresh-levels.scala +++ b/tests/neg-custom-args/captures/cc-fresh-levels.scala @@ -15,5 +15,5 @@ def test1(a: IO^, b: IO^, c: IO^): Unit = r.put(c) // ok runIO: (innerIO: IO^) => r.put(innerIO) // error - runIO: innerIO => - r.put(innerIO) // should be error, but ok // unsound + runIO: innerIO => // error + r.put(innerIO)