diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala index 19f2da7bff1c..64ca777f1b76 100644 --- a/compiler/src/dotty/tools/dotc/cc/Capability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala @@ -961,7 +961,6 @@ object Capabilities: case UnapplyInstance(info: MethodType) case LocalInstance(restpe: Type) case NewInstance(tp: Type) - case NewCapability(tp: Type) case LambdaExpected(respt: Type) case LambdaActual(restp: Type) case OverriddenType(member: Symbol) @@ -992,9 +991,6 @@ object Capabilities: i" when instantiating expected result type $restpe of function literal" case NewInstance(tp) => i" when constructing instance $tp" - case NewCapability(tp) => - val kind = if tp.derivesFromMutable then "mutable" else "Capability instance" - i" when constructing $kind $tp" case LambdaExpected(respt) => i" when instantiating expected result type $respt of lambda" case LambdaActual(restp: Type) => diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 87b75cfc9854..3e00907332f2 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -881,16 +881,12 @@ class CheckCaptures extends Recheck, SymTransformer: * annotations avoid problematic intersections of capture sets when those * parameters are selected. * - * Second half: union of initial capture set and all capture sets of arguments - * to tracked parameters. The initial capture set `initCs` is augmented with - * a fresh cap if `core` extends Capability. + * Second half: union of initial capture set, all capture sets of arguments + * to tracked parameters, and the capture set implied by the fields of the class. */ def addParamArgRefinements(core: Type, initCs: CaptureSet): (Type, CaptureSet) = var refined: Type = core - var allCaptures: CaptureSet = - if core.derivesFromCapability - then initCs ++ FreshCap(Origin.NewCapability(core)).singletonCaptureSet - else initCs ++ impliedByFields(core) + var allCaptures: CaptureSet = initCs ++ impliedByFields(core) for (getterName, argType) <- mt.paramNames.lazyZip(argTypes) do val getter = cls.info.member(getterName).suchThat(_.isRefiningParamAccessor).symbol if !getter.is(Private) && getter.hasTrackedParts then @@ -917,7 +913,9 @@ class CheckCaptures extends Recheck, SymTransformer: /** The additional capture set implied by the capture sets of its fields. This * is either empty or, if some fields have a terminal capability in their span * capture sets, it consists of a single fresh cap that subsumes all these terminal - * capabiltities. Class parameters are not counted. + * capabiltities. Class parameters are not counted. If the type is a mutable type, + * we add a fresh cap in any case -- this is because we can currently hide + * mutability in array vals, an example is neg-customargs/captures/matrix.scala. */ def impliedByFields(core: Type): CaptureSet = var infos: List[String] = Nil @@ -925,20 +923,23 @@ class CheckCaptures extends Recheck, SymTransformer: if ctx.settings.YccVerbose.value then infos = msg :: infos /** The classifiers of the fresh caps in the span capture sets of all fields - * in the given class `cls`. + * in the given class `cls`. Mutable types get at least a fresh classified + * as mutable. */ def impliedClassifiers(cls: Symbol): List[ClassSymbol] = cls match case cls: ClassSymbol => - val fieldClassifiers = + val fields = cls.info.decls.toList + var fieldClassifiers = for - sym <- cls.info.decls.toList - if contributesFreshToClass(sym) + sym <- fields if contributesFreshToClass(sym) case fresh: FreshCap <- sym.info.spanCaptureSet.elems .filter(_.isTerminalCapability) .map(_.stripReadOnly) .toList _ = pushInfo(i"Note: ${sym.showLocated} captures a $fresh") yield fresh.hiddenSet.classifier + if cls.typeRef.isMutableType then + fieldClassifiers = defn.Caps_Mutable :: fieldClassifiers val parentClassifiers = cls.parentSyms.map(impliedClassifiers).filter(_.nonEmpty) if fieldClassifiers.isEmpty && parentClassifiers.isEmpty diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala index edb7ea29fc84..fef4adc41b7d 100644 --- a/compiler/src/dotty/tools/dotc/cc/Setup.scala +++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala @@ -332,7 +332,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: if !tptToCheck.isEmpty then report.error(msg, tptToCheck.srcPos) /** If C derives from Capability and we have a C^cs in source, we leave it as is - * instead of expanding it to C^{cap.rd}^cs. We do this by stripping capability-generated + * instead of expanding it to C^{cap}^cs. We do this by stripping capability-generated * universal capture sets from the parent of a CapturingType. */ def stripImpliedCaptureSet(tp: Type): Type = tp match @@ -936,21 +936,24 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: if others.accountsFor(ref) then report.warning(em"redundant capture: $dom already accounts for $ref", pos) - if ref.captureSetOfInfo.elems.isEmpty - && !ref.coreType.derivesFrom(defn.Caps_Capability) - && !ref.coreType.derivesFrom(defn.Caps_CapSet) then - val deepStr = if ref.isReach then " deep" else "" - report.error(em"$ref cannot be tracked since its$deepStr capture set is empty", pos) - check(parent.captureSet, parent) - - val others = - for - j <- 0 until retained.length if j != i - r = retained(j) - if !r.isTerminalCapability - yield r - val remaining = CaptureSet(others*) - check(remaining, remaining) + if !ref.coreType.derivesFrom(defn.Caps_Capability) + // Capability classes don't have their implied capture set yet, so + // they would be seen as pure + && !ref.coreType.derivesFrom(defn.Caps_CapSet) + then + if ref.captureSetOfInfo.elems.isEmpty then + val deepStr = if ref.isReach then " deep" else "" + report.error(em"$ref cannot be tracked since its$deepStr capture set is empty", pos) + check(parent.captureSet, parent) + + val others = + for + j <- 0 until retained.length if j != i + r = retained(j) + if !r.isTerminalCapability + yield r + val remaining = CaptureSet(others*) + check(remaining, remaining) end for catch case ex: IllegalCaptureRef => report.error(em"Illegal capture reference: ${ex.getMessage}", tpt.srcPos) diff --git a/docs/_docs/reference/experimental/capture-checking/basics.md b/docs/_docs/reference/experimental/capture-checking/basics.md index a0f440bbc283..8439810d4528 100644 --- a/docs/_docs/reference/experimental/capture-checking/basics.md +++ b/docs/_docs/reference/experimental/capture-checking/basics.md @@ -219,9 +219,12 @@ This widening is called _avoidance_; it is not specific to capture checking but ## Capability Classes -Classes like `CanThrow` or `FileSystem` have the property that their values are always intended to be capabilities. We can make this intention explicit and save boilerplate by letting these classes extend the `SharedCapability` class defined in object `cap`. +Classes like `CanThrow` or `FileSystem` have the property that their values are always intended to be capabilities. We can make this intention explicit and save boilerplate by letting these classes extend the `SharedCapability` class defined in object `caps`. + +A type extending `SharedCapability` always comes with a capture set. If no capture set is given explicitly, we assume the capture set is `{cap}`. + +This means we could equivalently express the `FileSystem` and `Logger` classes as follows: -The capture set of type extending `SharedCapability` is always `{cap}`. This means we could equivalently express the `FileSystem` and `Logger` classes as follows: ```scala import caps.SharedCapability @@ -234,9 +237,10 @@ def test(using fs: FileSystem) = val l: Logger^{fs} = Logger() ... ``` -In this version, `FileSystem` is a capability class, which means that the `{cap}` capture set is implied on the parameters of `Logger` and `test`. +In this version, `FileSystem` is a capability class, which means that the occurrences of `FileSystem` in the types of the parameters of `Logger` and `test` are implicitly expanded to `FileSystem^`. On the other hand, types like `FileSystem^{f}` or +`FileSystem^{}` are kept as written. -Another, unrelated change in the version of the last example here is that the `FileSystem` capability is now passed as an implicit parameter. It is quite natural to model capabilities with implicit parameters since it greatly reduces the wiring overhead once multiple capabilities are in play. +Another, unrelated change in the last version of the `Logger` example is that the `FileSystem` capability is now passed as an implicit parameter. It is quite natural to model capabilities with implicit parameters since it greatly reduces the wiring overhead once multiple capabilities are in play. ## Escape Checking diff --git a/tests/neg-custom-args/captures/boundary.check b/tests/neg-custom-args/captures/boundary.check index 1d624c9d18bf..b64d1edef8a6 100644 --- a/tests/neg-custom-args/captures/boundary.check +++ b/tests/neg-custom-args/captures/boundary.check @@ -2,14 +2,13 @@ 4 | boundary[AnyRef^]: 5 | l1 ?=> // error // error | ^ - |Found: scala.util.boundary.Label[Object^'s1]^ - |Required: scala.util.boundary.Label[Object^²]^³ + | Found: scala.util.boundary.Label[Object^'s1] + | Required: scala.util.boundary.Label[Object^]^² | - |Note that capability cap cannot be included in outer capture set 's1. + | Note that capability cap cannot be included in outer capture set 's1. | - |where: ^ refers to a fresh root capability classified as Control created in value local when constructing Capability instance scala.util.boundary.Label[Object^'s1] - | ^² and cap refer to the universal root capability - | ^³ refers to a fresh root capability classified as Control in the type of value local + | where: ^ and cap refer to the universal root capability + | ^² refers to a fresh root capability classified as Control in the type of value local 6 | boundary[Unit]: l2 ?=> 7 | boundary.break(l2)(using l1) // error 8 | ??? diff --git a/tests/neg-custom-args/captures/extending-cap-classes.check b/tests/neg-custom-args/captures/extending-cap-classes.check index 44234bf2384c..002c0c62783c 100644 --- a/tests/neg-custom-args/captures/extending-cap-classes.check +++ b/tests/neg-custom-args/captures/extending-cap-classes.check @@ -1,27 +1,5 @@ --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/extending-cap-classes.scala:7:15 ------------------------- -7 | val x2: C1 = new C2 // error - | ^^^^^^ - |Found: C2^ - |Required: C1 - | - |Note that capability cap is not included in capture set {}. - | - |where: ^ and cap refer to a fresh root capability classified as SharedCapability created in value x2 when constructing Capability instance C2 - | - | longer explanation available when compiling with `-explain` --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/extending-cap-classes.scala:8:15 ------------------------- -8 | val x3: C1 = new C3 // error - | ^^^^^^ - |Found: C3^ - |Required: C1 - | - |Note that capability cap is not included in capture set {}. - | - |where: ^ and cap refer to a fresh root capability classified as SharedCapability created in value x3 when constructing Capability instance C3 - | - | longer explanation available when compiling with `-explain` --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/extending-cap-classes.scala:13:15 ------------------------ -13 | val z2: C1 = y2 // error +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/extending-cap-classes.scala:14:15 ------------------------ +14 | val z2: C1 = y2 // error | ^^ | Found: (y2 : C2) | Required: C1 diff --git a/tests/neg-custom-args/captures/extending-cap-classes.scala b/tests/neg-custom-args/captures/extending-cap-classes.scala index 7f38fd0af488..2b8db840ecf8 100644 --- a/tests/neg-custom-args/captures/extending-cap-classes.scala +++ b/tests/neg-custom-args/captures/extending-cap-classes.scala @@ -4,11 +4,13 @@ class C3 extends C2 def test = val x1: C1 = new C1 - val x2: C1 = new C2 // error - val x3: C1 = new C3 // error + val x2: C1 = new C2 // was error, now ok + val x3: C1 = new C3 // was error, now ok val y2: C2 = new C2 val y3: C3 = new C3 + val y2ok: C2^{} = new C2 val z2: C1 = y2 // error + val z2ok: C1 = y2ok diff --git a/tests/neg-custom-args/captures/filevar.check b/tests/neg-custom-args/captures/filevar.check index ebdfdd24d31e..0bfc7f71cd9d 100644 --- a/tests/neg-custom-args/captures/filevar.check +++ b/tests/neg-custom-args/captures/filevar.check @@ -12,7 +12,3 @@ 18 | o.log | | longer explanation available when compiling with `-explain` --- Warning: tests/neg-custom-args/captures/filevar.scala:11:55 --------------------------------------------------------- -11 |def withFile[T](op: (l: caps.Capability) ?-> (f: File^{l}) => T): T = - | ^ - | redundant capture: File already accounts for (l : scala.caps.Capability) diff --git a/tests/neg-custom-args/captures/i15923.check b/tests/neg-custom-args/captures/i15923.check index 3e4a97509237..e018a2ea9f4b 100644 --- a/tests/neg-custom-args/captures/i15923.check +++ b/tests/neg-custom-args/captures/i15923.check @@ -20,11 +20,3 @@ |where: => refers to a fresh root capability created in anonymous function of type (using lcap: scala.caps.Capability): Cap^{lcap} -> Id[Cap] when instantiating expected result type Cap^{lcap} ->{cap²} Id[Cap^'s13]^'s14 of function literal | | longer explanation available when compiling with `-explain` --- Warning: tests/neg-custom-args/captures/i15923.scala:21:56 ---------------------------------------------------------- -21 | def withCap[X](op: (lcap: caps.Capability) ?-> Cap^{lcap} => X): X = { - | ^^^^ - | redundant capture: test2.Cap already accounts for (lcap : scala.caps.Capability) --- Warning: tests/neg-custom-args/captures/i15923.scala:6:54 ----------------------------------------------------------- -6 | def withCap[X](op: (lcap: caps.Capability) ?-> Cap^{lcap} => X): X = { - | ^^^^ - | redundant capture: Cap already accounts for (lcap : scala.caps.Capability) diff --git a/tests/neg-custom-args/captures/i21614.check b/tests/neg-custom-args/captures/i21614.check index fc6f23ec2dc8..399d26c8462d 100644 --- a/tests/neg-custom-args/captures/i21614.check +++ b/tests/neg-custom-args/captures/i21614.check @@ -13,13 +13,12 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:15:12 --------------------------------------- 15 | files.map(new Logger(_)) // error, Q: can we improve the error message? | ^^^^^^^^^^^^^ - |Found: (_$1: File^'s1) ->{C} Logger{val f: File^{_$1}}^{cap, _$1} + |Found: (_$1: File^'s1) ->{C} Logger{val f: File^{_$1}}^{_$1} |Required: File^{C} => Logger{val f: File^'s2}^'s3 | |Note that capability C is not classified as trait SharedCapability, therefore it |cannot be included in capture set 's1 of parameter _$1 of SharedCapability elements. | - |where: => refers to a fresh root capability created in method mkLoggers2 when checking argument to parameter f of method map - | cap is a root capability associated with the result type of (_$1: File^'s1): Logger{val f: File^{_$1}}^{cap, _$1} + |where: => refers to a fresh root capability created in method mkLoggers2 when checking argument to parameter f of method map | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/i23726.check b/tests/neg-custom-args/captures/i23726.check index 1e359316a84a..452de9d23b4f 100644 --- a/tests/neg-custom-args/captures/i23726.check +++ b/tests/neg-custom-args/captures/i23726.check @@ -1,5 +1,5 @@ --- Error: tests/neg-custom-args/captures/i23726.scala:10:5 ------------------------------------------------------------- -10 | f1(a) // error, as expected +-- Error: tests/neg-custom-args/captures/i23726.scala:11:5 ------------------------------------------------------------- +11 | f1(a) // error, as expected | ^ |Separation failure: argument of type (a : Ref^) |to a function of type (x: Ref^) -> List[() ->{a, x} Unit] @@ -15,8 +15,8 @@ | |where: ^ refers to a fresh root capability classified as Mutable in the type of value a | ^² refers to a fresh root capability classified as Mutable created in method test1 when checking argument to parameter x of method apply --- Error: tests/neg-custom-args/captures/i23726.scala:15:5 ------------------------------------------------------------- -15 | f3(b) // error +-- Error: tests/neg-custom-args/captures/i23726.scala:16:5 ------------------------------------------------------------- +16 | f3(b) // error | ^ |Separation failure: argument of type (b : Ref^) |to a function of type (x: Ref^) -> (op: () ->{b} Unit) -> List[() ->{op} Unit] @@ -32,8 +32,8 @@ | |where: ^ refers to a fresh root capability classified as Mutable in the type of value b | ^² refers to a fresh root capability classified as Mutable created in method test1 when checking argument to parameter x of method apply --- Error: tests/neg-custom-args/captures/i23726.scala:23:5 ------------------------------------------------------------- -23 | f7(a) // error +-- Error: tests/neg-custom-args/captures/i23726.scala:24:5 ------------------------------------------------------------- +24 | f7(a) // error | ^ |Separation failure: argument of type (a : Ref^) |to a function of type (x: Ref^) ->{a, b} (y: List[Ref^{a, b}]) ->{a, b} Unit diff --git a/tests/neg-custom-args/captures/i23726.scala b/tests/neg-custom-args/captures/i23726.scala index fc833ef29583..7874a50dddee 100644 --- a/tests/neg-custom-args/captures/i23726.scala +++ b/tests/neg-custom-args/captures/i23726.scala @@ -1,7 +1,8 @@ import language.experimental.captureChecking import language.experimental.separationChecking import caps.* -class Ref extends Mutable +class Ref extends Mutable: + update def set = ??? def swap(a: Ref^, b: Ref^): Unit = () def test1(): Unit = val a = Ref() diff --git a/tests/neg-custom-args/captures/scope-extrude-mut.check b/tests/neg-custom-args/captures/scope-extrude-mut.check index 2e4190168681..5f1671b19a47 100644 --- a/tests/neg-custom-args/captures/scope-extrude-mut.check +++ b/tests/neg-custom-args/captures/scope-extrude-mut.check @@ -1,13 +1,13 @@ --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scope-extrude-mut.scala:9:8 ------------------------------ -9 | a = a1 // error - | ^^ - | Found: (a1 : A^) - | Required: A^² - | - | Note that capability cap is not included in capture set {cap²} - | because cap in method b is not visible from cap² in variable a. - | - | where: ^ and cap refer to a fresh root capability classified as Mutable in the type of value a1 - | ^² and cap² refer to a fresh root capability classified as Mutable in the type of variable a - | - | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scope-extrude-mut.scala:10:8 ----------------------------- +10 | a = a1 // error + | ^^ + | Found: (a1 : A^) + | Required: A^² + | + | Note that capability cap is not included in capture set {cap²} + | because cap in method b is not visible from cap² in variable a. + | + | where: ^ and cap refer to a fresh root capability classified as Mutable in the type of value a1 + | ^² and cap² refer to a fresh root capability classified as Mutable in the type of variable a + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/scope-extrude-mut.scala b/tests/neg-custom-args/captures/scope-extrude-mut.scala index 75ff0e11abcb..a2dfeed491b4 100644 --- a/tests/neg-custom-args/captures/scope-extrude-mut.scala +++ b/tests/neg-custom-args/captures/scope-extrude-mut.scala @@ -1,6 +1,7 @@ import language.experimental.captureChecking -class A extends caps.Mutable +class A extends caps.Mutable: + var x = 0 class B: private var a: A^ = A() diff --git a/tests/neg-custom-args/captures/sep-counter.check b/tests/neg-custom-args/captures/sep-counter.check index 44e4a897a565..2676f3f62362 100644 --- a/tests/neg-custom-args/captures/sep-counter.check +++ b/tests/neg-custom-args/captures/sep-counter.check @@ -9,4 +9,4 @@ |where: ^ refers to a fresh root capability classified as Mutable in the result type of method mkCounter | ^² refers to a fresh root capability classified as Mutable in the result type of method mkCounter | cap is a fresh root capability classified as Mutable in the type of value c - | cap² is a fresh root capability classified as Mutable created in value c when constructing mutable Ref + | cap² is a fresh root capability classified as Mutable created in value c when constructing instance Ref diff --git a/tests/pos-custom-args/captures/no-redundant-capability.scala b/tests/pos-custom-args/captures/no-redundant-capability.scala new file mode 100644 index 000000000000..5a53f20bea60 --- /dev/null +++ b/tests/pos-custom-args/captures/no-redundant-capability.scala @@ -0,0 +1,21 @@ +//> using options -Werror +import caps.* + +trait State[A] extends SharedCapability: + def get: A + def set(a: A): Unit + +def get[A]: State[A] ?-> A = s ?=> s.get +def set[A](a: A): State[A] ?-> Unit = s ?=> s.set(a) + +trait Rand: + def range(min: Int, max: Int): Int + +object Rand: + def fromState: (s: State[Long]) ?-> Rand^{s} = + new Rand: + override def range(min: Int, max: Int): Int = + val seed = get + val (nextSeed, next) = (seed + 1, seed.toInt) // obviously wrong, but not the point... + set(nextSeed) + next diff --git a/tests/pos-custom-args/captures/strip-implied-cs.scala b/tests/pos-custom-args/captures/strip-implied-cs.scala new file mode 100644 index 000000000000..72b257c343c5 --- /dev/null +++ b/tests/pos-custom-args/captures/strip-implied-cs.scala @@ -0,0 +1,21 @@ +//> using options -Werror +import caps.* + +trait State[A] extends SharedCapability: + def get: A + def set(a: A): Unit + +def get[A]: State[A] ?-> A = s ?=> s.get +def set[A](a: A): State[A] ?-> Unit = s ?=> s.set(a) + +trait Rand extends SharedCapability: + def range(min: Int, max: Int): Int + +object Rand: + def fromState: (s: State[Long]) ?-> Rand^{s} = + new Rand: + override def range(min: Int, max: Int): Int = + val seed = get + val (nextSeed, next) = (seed + 1, seed.toInt) // obviously wrong, but not the point... + set(nextSeed) + next