diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala index 55e7762a9269..41a084a5d87e 100644 --- a/compiler/src/dotty/tools/dotc/cc/Capability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala @@ -703,14 +703,6 @@ object Capabilities: (this eq y) || this.match case x: FreshCap => - def levelOK = - if ccConfig.useFreshLevels && !CCState.collapseFresh then - val yOwner = y.levelOwner - yOwner.isStaticOwner || x.ccOwner.isContainedIn(yOwner) - else y.core match - case ResultCap(_) | _: ParamRef => false - case _ => true - vs.ifNotSeen(this)(x.hiddenSet.elems.exists(_.subsumes(y))) || x.acceptsLevelOf(y) && ( y.tryClassifyAs(x.hiddenSet.classifier) @@ -788,6 +780,9 @@ object Capabilities: case _: Maybe => MaybeCapability(c1) case _ => c1 + def showAsCapability(using Context) = + i"capability ${ctx.printer.toTextCapability(this).show}" + def toText(printer: Printer): Text = printer.toTextCapability(this) end Capability diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index 70274f3fc057..0ababe60e743 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala @@ -20,6 +20,8 @@ import CCState.* import TypeOps.AvoidMap import compiletime.uninitialized import Capabilities.* +import Names.Name +import NameKinds.CapsetName /** A class for capture sets. Capture sets can be constants or variables. * Capture sets support inclusion constraints <:< where <:< is subcapturing. @@ -738,6 +740,17 @@ object CaptureSet: var description: String = "" + private var myRepr: Name | Null = null + + /** A represtentation of this capture set as a unique name. We print + * empty capture set variables in this representation. Bimapped sets have + * the representation of their source set. + */ + def repr(using Context): Name = { + if (myRepr == null) myRepr = CapsetName.fresh() + myRepr.nn + } + /** Check that all maps recorded in skippedMaps map `elem` to itself * or something subsumed by it. */ @@ -1028,6 +1041,7 @@ object CaptureSet: override def isMaybeSet: Boolean = bimap.isInstanceOf[MaybeMap] override def toString = s"BiMapped$id($source, elems = $elems)" override def summarize = bimap.getClass.toString + override def repr(using Context): Name = source.repr end BiMapped /** A variable with elements given at any time as { x <- source.elems | p(x) } */ @@ -1300,24 +1314,23 @@ object CaptureSet: case cs: Var => if !cs.levelOK(elem) then val levelStr = elem match - case ref: TermRef => i", defined in ${ref.symbol.maybeOwner}" - case _ => "" - i"""capability ${elem}$levelStr - |cannot be included in outer capture set $cs""" + case ref: TermRef => i", defined in ${ref.symbol.maybeOwner}\n" + case _ => " " + i"""${elem.showAsCapability}${levelStr}cannot be included in outer capture set $cs""" else if !elem.tryClassifyAs(cs.classifier) then - i"""capability ${elem} is not classified as ${cs.classifier}, therefore it + i"""${elem.showAsCapability} is not classified as ${cs.classifier}, therefore it |cannot be included in capture set $cs of ${cs.classifier.name} elements""" else if cs.isBadRoot(elem) then elem match case elem: FreshCap => - i"""local capability $elem created in ${elem.ccOwner} + i"""local ${elem.showAsCapability} created in ${elem.ccOwner} |cannot be included in outer capture set $cs""" case _ => - i"universal capability $elem cannot be included in capture set $cs" + i"universal ${elem.showAsCapability} cannot be included in capture set $cs" else - i"capability $elem cannot be included in capture set $cs" + i"${elem.showAsCapability} cannot be included in capture set $cs" case _ => - i"capability $elem is not included in capture set $cs$why" + i"${elem.showAsCapability} is not included in capture set $cs$why" override def toText(printer: Printer): Text = inContext(printer.printerContext): diff --git a/compiler/src/dotty/tools/dotc/core/NameKinds.scala b/compiler/src/dotty/tools/dotc/core/NameKinds.scala index ff41eeb81ca0..f41062d908e9 100644 --- a/compiler/src/dotty/tools/dotc/core/NameKinds.scala +++ b/compiler/src/dotty/tools/dotc/core/NameKinds.scala @@ -328,6 +328,7 @@ object NameKinds { val ExceptionBinderName: UniqueNameKind = new UniqueNameKind("ex") val ExistentialBinderName: UniqueNameKind = new UniqueNameKind("ex$") val SkolemName: UniqueNameKind = new UniqueNameKind("?") + val CapsetName: UniqueNameKind = new UniqueNameKind("'s") val SuperArgName: UniqueNameKind = new UniqueNameKind("$superArg$") val DocArtifactName: UniqueNameKind = new UniqueNameKind("$doc") val UniqueInlineName: UniqueNameKind = new UniqueNameKind("$i") diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala index c00c4d04a0ee..cda3e7d4b6f2 100644 --- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala +++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala @@ -173,10 +173,11 @@ class PlainPrinter(_ctx: Context) extends Printer { else if cs == CaptureSet.Fluid then "" else val core: Text = - if !cs.isConst && cs.elems.isEmpty then "?" - else "{" ~ Text(cs.processElems(_.toList.map(toTextCapability)), ", ") ~ "}" + if !cs.isConst && cs.elems.isEmpty then cs.asVar.repr.show + else + Str("'").provided(ccVerbose && !cs.isConst) + ~ "{" ~ Text(cs.processElems(_.toList.map(toTextCapability)), ", ") ~ "}" ~ Str(".reader").provided(ccVerbose && cs.mutability == Mutability.Reader) - ~ Str("?").provided(ccVerbose && !cs.isConst) ~ Str(s"#${cs.asVar.id}").provided(showUniqueIds && !cs.isConst) core ~ cs.optionalInfo @@ -243,8 +244,6 @@ class PlainPrinter(_ctx: Context) extends Printer { selectionString(tp) else toTextPrefixOf(tp) ~ selectionString(tp) - case tp: TermParamRef => - ParamRefNameString(tp) ~ hashStr(tp.binder) ~ ".type" case tp: TypeParamRef => val suffix = if showNestingLevel then diff --git a/docs/_docs/reference/experimental/cc-advanced.md b/docs/_docs/reference/experimental/capture-checking/advanced.md similarity index 96% rename from docs/_docs/reference/experimental/cc-advanced.md rename to docs/_docs/reference/experimental/capture-checking/advanced.md index 52d1956caf49..9c19cefc1f8e 100644 --- a/docs/_docs/reference/experimental/cc-advanced.md +++ b/docs/_docs/reference/experimental/capture-checking/advanced.md @@ -1,7 +1,7 @@ --- layout: doc-page -title: "Capture Checking -- Advanced Use Cases" -nightlyOf: https://docs.scala-lang.org/scala3/reference/experimental/cc-advanced.html +title: "Capability Polymorphism -- Advanced Use Cases" +nightlyOf: https://docs.scala-lang.org/scala3/reference/experimental/capture-checking/advanced.html --- @@ -75,4 +75,4 @@ By leveraging capability polymorphism, capability members, and path-dependent ca * `Label`s store the free capabilities `C` of the `block` passed to `boundary` in their capability member `Fv`. * When suspending on a given label, the suspension handler can capture at most the capabilities that occur freely at the `boundary` that introduced the label. That prevents mentioning nested bound labels. -[Back to Capture Checking](cc.md) \ No newline at end of file +[Back to Capability Polymorphism](polymorphism.md) \ No newline at end of file diff --git a/docs/_docs/reference/experimental/capture-checking/cc.md b/docs/_docs/reference/experimental/capture-checking/cc.md new file mode 100644 index 000000000000..dec31d0c82a4 --- /dev/null +++ b/docs/_docs/reference/experimental/capture-checking/cc.md @@ -0,0 +1,304 @@ +--- +layout: doc-page +title: "Capture Checking" +nightlyOf: https://docs.scala-lang.org/scala3/reference/experimental/capture-checking/cc.html +--- + +Capture checking is a research project that modifies the Scala type system to track references to capabilities in values. + +## Introduction + +Capture checking can be enabled by the language import +```scala +import language.experimental.captureChecking +``` +At present, capture checking is still highly experimental and unstable, and it evolves quickly. +Before trying it out, make sure you have the latest version of Scala. + +The rest of this page explains the basics capture checking. Further topics are described in the following pages: + + - [Capture Checking of Classes](./classes.md) + - [Capability Polymorphism](./polymorphism.md) + - [Scoped Caps](./scoped-caps.md) + - [Capability Classifiers](./classifiers.md) + - [Checked Exceptions](./checked-exceptions.md) + - [Separation Checking](./separation-checking.md) + - [How to Use the Capture Checker](./how-to-use.md) + - [Capture Checking Internals](./internals.md) + + +To get an idea what capture checking can do, let's start with a small example: +```scala +def usingLogFile[T](op: FileOutputStream => T): T = + val logFile = FileOutputStream("log") + val result = op(logFile) + logFile.close() + result +``` +The `usingLogFile` method invokes a given operation with a fresh log file as parameter. Once the operation has ended, the log file is closed and the +operation's result is returned. This is a typical _try-with-resources_ pattern, similar to many other such patterns which are often supported by special language constructs in other languages. + +The problem is that `usingLogFile`'s implementation is not entirely safe. One can +undermine it by passing an operation that performs the logging at some later point +after it has terminated. For instance: +```scala +val later = usingLogFile { file => () => file.write(0) } +later() // crash +``` +When `later` is executed it tries to write to a file that is already closed, which +results in an uncaught `IOException`. + +Capture checking gives us the mechanism to prevent such errors _statically_. To +prevent unsafe usages of `usingLogFile`, we can declare it like this: +```scala +def usingLogFile[T](op: FileOutputStream^ => T): T = + // same body as before +``` +The only thing that's changed is that the `FileOutputStream` parameter of `op` is now +followed by `^`. We'll see that this turns the parameter into a _capability_ whose lifetime is tracked. + +If we now try to define the problematic value `later`, we get a static error: +``` + | val later = usingLogFile { f => () => f.write(0) } + | ^^^^^^^^^^^^^^^^^^^^^^^^^ + | Found: (f: java.io.FileOutputStream^'s1) ->'s2 () ->{f} Unit + | Required: java.io.FileOutputStream^ => () ->'s3 Unit + | + | Note that capability f cannot be included in outer capture set 's3. +``` +In this case, it was easy to see that the `logFile` capability escapes in the closure passed to `usingLogFile`. But capture checking also works for more complex cases. +For instance, capture checking is able to distinguish between the following safe code: +```scala +val xs = usingLogFile { f => + List(1, 2, 3).map { x => f.write(x); x * x } +} +``` +and the following unsafe one: +```scala +val xs = usingLogFile { f => + LzyList(1, 2, 3).map { x => f.write(x); x * x } +} +``` +An error would be issued in the second case, but not the first one (this assumes a capture-aware +formulation `LzyList` of lazily evaluated lists, which we will present later in this page). + +It turns out that capture checking has very broad applications. Besides the various +try-with-resources patterns, it can also be a key part to the solutions of many other long standing problems in programming languages. Among them: + + - How to have a simple and flexible system for checked exceptions. We show later + how capture checking enables a clean and fully safe system for checked exceptions in Scala. + - How to address the problem of effect polymorphism in general. + - How to solve the "what color is your function?" problem of mixing synchronous + and asynchronous computations. + - How to do region-based allocation, safely, + - How to reason about capabilities associated with memory locations. + +The following sections explain in detail how capture checking works in Scala 3. + + +## Capabilities and Capturing Types + +The capture checker extension introduces a new kind of types and it enforces some rules for working with these types. + + +Capture checking is done in terms of _capturing types_ of the form +`T^{c₁, ..., cᵢ}`. Here `T` is a type, and `{c₁, ..., cᵢ}` is a _capture set_ consisting of references to capabilities `c₁, ..., cᵢ`. + +An _object capability_ is syntactically a method- or class-parameter, a local variable, or the `this` of an enclosing class. The type of a capability +must be a capturing type with a non-empty capture set. We also say that +variables that are capabilities are _tracked_. + +In a sense, every +capability gets its authority from some other, more sweeping capability which it captures. The recursion stops with a _universal capability_, written `cap`, from which all other capabilities are ultimately derived. +If `T` is a type, then `T^` is a shorthand for `T^{cap}`, meaning `T` can capture arbitrary capabilities. + +Here is an example: +```scala +class FileSystem + +class Logger(fs: FileSystem^): + def log(s: String): Unit = ... // Write to a log file, using `fs` + +def test(fs: FileSystem^) = + val l: Logger^{fs} = Logger(fs) + l.log("hello world!") + val xs: LzyList[Int]^{l} = + LzyList.from(1) + .map { i => + l.log(s"computing elem # $i") + i * i + } + xs +``` +Here, the `test` method takes a `FileSystem` as a parameter. `fs` is a capability since its type has a non-empty capture set. The capability is passed to the `Logger` constructor +and retained as a field in class `Logger`. Hence, the local variable `l` has type +`Logger^{fs}`: it is a `Logger` which retains the `fs` capability. + +The second variable defined in `test` is `xs`, a lazy list that is obtained from +`LzyList.from(1)` by logging and mapping consecutive numbers. Since the list is lazy, +it needs to retain the reference to the logger `l` for its computations. Hence, the +type of the list is `LzyList[Int]^{l}`. On the other hand, since `xs` only logs but does +not do other file operations, it retains the `fs` capability only indirectly. That's why +`fs` does not show up in the capture set of `xs`. + +Capturing types come with a subtype relation where types with "smaller" capture sets are subtypes of types with larger sets (the _subcapturing_ relation is defined in more detail below). If a type `T` does not have a capture set, it is called _pure_, and is a subtype of +any capturing type that adds a capture set to `T`. + +## Function Types + +The usual function type `A => B` now stands for a function that can capture arbitrary capabilities. We call such functions +_impure_. By contrast, the new single arrow function type `A -> B` stands for a function that cannot capture any capabilities, or otherwise said, is _pure_. +One can add a capture set after the arrow of an otherwise pure function. +For instance, `A ->{c, d} B` would be a function that can capture capabilities `c` and `d`, but no others. +This type is a shorthand for `(A -> B)^{c, d}`, i.e. the function type `A -> B` with possible captures `{c, d}`. + +The impure function type `A => B` is treated as an alias for `A ->{cap} B`. That is, impure functions are functions that can capture anything. + +A capture annotation `^` binds more strongly than a function arrow. So +`A -> B^{c}` is read as `A -> (B^{c})` and `A -> B^` is read as `A -> (B^)`. + +Analogous conventions apply to context function types. `A ?=> B` is an impure context function, with `A ?-> B` as its pure complement. + +**Note 1:** The identifiers `->` and `?->` are now treated as soft keywords when used as infix type operators. They are +still available as regular identifiers for terms. For instance, the mapping syntax `Map("x" -> 1, "y" -> 2)` is still supported since it only applies to terms. + +**Note 2:** The distinctions between pure vs impure function types do not apply to methods. In fact, since methods are not values they never capture anything directly. References to +capabilities in a method are instead counted in the capture set of the enclosing object. + +## By-Name Parameter Types + +A convention analogous to function types also extends to by-name parameters. In +```scala +def f(x: => Int): Int +``` +the actual argument can refer to arbitrary capabilities. So the following would be OK: +```scala +f(if p(y) then throw Ex() else 1) +``` +On the other hand, if `f` was defined like this +```scala +def f(x: -> Int): Int +``` +the actual argument to `f` could not refer to any capabilities, so the call above would be rejected. +One can also allow specific capabilities like this: +```scala +def f(x: ->{c} Int): Int +``` +Here, the actual argument to `f` is allowed to use the `c` capability but no others. + +## Subtyping and Subcapturing + +Capturing influences subtyping. As usual we write `T₁ <: T₂` to express that the type +`T₁` is a subtype of the type `T₂`, or equivalently, that `T₁` conforms to `T₂`. An +analogous _subcapturing_ relation applies to capture sets. If `C₁` and `C₂` are capture sets, we write `C₁ <: C₂` to express that `C₁` _is covered by_ `C₂`, or, swapping the operands, that `C₂` _covers_ `C₁`. + +Subtyping extends as follows to capturing types: + + - Pure types are subtypes of capturing types. That is, `T <: C T`, for any type `T`, capturing set `C`. + - For capturing types, smaller capturing sets produce subtypes: `C₁ T₁ <: C₂ T₂` if + `C₁ <: C₂` and `T₁ <: T₂`. + +A subcapturing relation `C₁ <: C₂` holds if `C₂` _accounts for_ every element `c` in `C₁`. This means one of the following three conditions must be true: + + - `c ∈ C₂`, + - `c` refers to a parameter of some class `Cls` and `C₂` contains `Cls.this`, + - `c`'s type has capturing set `C` and `C₂` accounts for every element of `C` (that is, `C <: C₂`). + + +**Example 1.** Given +```scala +fs: FileSystem^ +ct: CanThrow[Exception]^ +l : Logger^{fs} +``` +we have +``` +{l} <: {fs} <: {cap} +{fs} <: {fs, ct} <: {cap} +{ct} <: {fs, ct} <: {cap} +``` +The set consisting of the root capability `{cap}` covers every other capture set. This is +a consequence of the fact that, ultimately, every capability is created from `cap`. + +**Example 2.** Consider again the FileSystem/Logger example from before. `LzyList[Int]` is a proper subtype of `LzyList[Int]^{l}`. So if the `test` method in that example +was declared with a result type `LzyList[Int]`, we'd get a type error. Here is the error message: +``` +11 |def test(using fs: FileSystem^): LzyList[Int] = { + | ^ + | Found: LzyList[Int]^{fs} + | Required: LzyList[Int] +``` +Why does it say `LzyList[Int]^{fs}` and not `LzyList[Int]^{l}`, which is, after all, the type of the returned value `xs`? The reason is that `l` is a local variable in the body of `test`, so it cannot be referred to in a type outside that body. What happens instead is that the type is _widened_ to the smallest supertype that does not mention `l`. Since `l` has capture set `fs`, we have that `{fs}` covers `{l}`, and `{fs}` is acceptable in a result type of `test`, so `{fs}` is the result of that widening. +This widening is called _avoidance_; it is not specific to capture checking but applies to all variable references in Scala types. + +## 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`. + +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 + +class FileSystem extends SharedCapability + +class Logger(using FileSystem): + def log(s: String): Unit = ??? + +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`. + +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. + +## Escape Checking + +Capabilities follow the usual scoping discipline, which means that capture sets +can contain only capabilities that are visible at the point where the set is defined. + +We now reconstruct how this principle produced the error in the introductory example, where +`usingLogFile` was declared like this: +```scala +def usingLogFile[T](op: FileOutputStream^ => T): T = ... +``` +The error message was: +``` + | val later = usingLogFile { f => () => f.write(0) } + | ^^^^^^^^^^^^^^^^^^^^^^^^^ + | Found: (f: java.io.FileOutputStream^'s1) ->'s2 () ->{f} Unit + | Required: java.io.FileOutputStream^ => () ->'s3 Unit + | + | Note that capability f cannot be included in outer capture set 's3. +``` +This error message was produced by the following logic: + + - The `f` parameter has type `FileOutputStream^`, which makes it a capability. + - Therefore, the type of the expression `() => f.write(0)` is `() ->{f} Unit`. + - This makes the type of the whole closure passed to `usingLogFile` the dependent function type + `(f: FileOutputStream^'s1) ->'s2 () ->{f} Unit`, + for some as yet uncomputed capture sets `'s1` and `'s2`. + - The expected type of the closure is a simple, parametric, impure function type `FileOutputStream^ => T`, + for some instantiation of the type variable `T`. + - Matching with the found type, `T` must have the shape `() ->'s3 Unit`, for + some capture set `'s3` defined at the level of value `later`. + - That capture set cannot include the capability `f` since `f` is locally bound. + This causes the error. + +An analogous restriction applies to the type of a mutable variable. +Another way one could try to undermine capture checking would be to +assign a closure with a local capability to a global variable. Maybe +like this: +```scala +var loophole: () => Unit = () => () +usingLogFile { f => + loophole = () => f.write(0) +} +loophole() +``` +But this will not compile either, since the capture set of the mutable variable `loophole` cannot refer to variable `f`, which is not visible +where `loophole` is defined. + +Looking at object graphs, we observe a monotonicity property: The capture set of an object `x` covers the capture sets of all objects reachable through `x`. This property is reflected in the type system by the following _monotonicity rule_: + + - In a class `C` with a field `f`, the capture set `{this}` covers the capture set `{this.f}` as well as the capture set of any application of `this.f` to pure arguments. diff --git a/docs/_docs/reference/experimental/capture-checking/checked-exceptions.md b/docs/_docs/reference/experimental/capture-checking/checked-exceptions.md new file mode 100644 index 000000000000..2c78ea457a93 --- /dev/null +++ b/docs/_docs/reference/experimental/capture-checking/checked-exceptions.md @@ -0,0 +1,88 @@ +--- +layout: doc-page +title: "Checked Exceptions" +nightlyOf: https://docs.scala-lang.org/scala3/reference/experimental/capture-checking/checked-exceptions.html +--- + +## Introduction + +Scala enables checked exceptions through a language import. Here is an example, +taken from the [safer exceptions page](../canthrow.md), and also described in a +[paper](https://infoscience.epfl.ch/record/290885) presented at the + 2021 Scala Symposium. +```scala +import language.experimental.saferExceptions + +class LimitExceeded extends Exception + +val limit = 10e+10 +def f(x: Double): Double throws LimitExceeded = + if x < limit then x * x else throw LimitExceeded() +``` +The new `throws` clause expands into an implicit parameter that provides +a `CanThrow` capability. Hence, function `f` could equivalently be written +like this: +```scala +def f(x: Double)(using CanThrow[LimitExceeded]): Double = ... +``` +If the implicit parameter is missing, an error is reported. For instance, the function definition +```scala +def g(x: Double): Double = + if x < limit then x * x else throw LimitExceeded() +``` +is rejected with this error message: +``` + | if x < limit then x * x else throw LimitExceeded() + | ^^^^^^^^^^^^^^^^^^^^^ + |The capability to throw exception LimitExceeded is missing. + |The capability can be provided by one of the following: + | - Adding a using clause `(using CanThrow[LimitExceeded])` to the definition of the enclosing method + | - Adding `throws LimitExceeded` clause after the result type of the enclosing method + | - Wrapping this piece of code with a `try` block that catches LimitExceeded +``` +`CanThrow` capabilities are required by `throw` expressions and are created +by `try` expressions. For instance, the expression +```scala +try xs.map(f).sum +catch case ex: LimitExceeded => -1 +``` +would be expanded by the compiler to something like the following: +```scala +try + erased given ctl: CanThrow[LimitExceeded] = compiletime.erasedValue + xs.map(f).sum +catch case ex: LimitExceeded => -1 +``` +(The `ctl` capability is only used for type checking but need not show up in the generated code, so it can be declared as +erased.) + +As with other capability based schemes, one needs to guard against capabilities +that are captured in results. For instance, here is a problematic use case: +```scala +def escaped(xs: Double*): (() => Double) throws LimitExceeded = + try () => xs.map(f).sum + catch case ex: LimitExceeded => () => -1 +val crasher = escaped(1, 2, 10e+11) +crasher() +``` +This code needs to be rejected since otherwise the call to `crasher()` would cause +an unhandled `LimitExceeded` exception to be thrown. + +Under the language import `language.experimental.captureChecking`, the code is indeed rejected + + + +To integrate exception and capture checking, only two changes are needed: + + - `CanThrow` is declared as a class extending `Control`, so all references to `CanThrow` instances are tracked. + - Escape checking is extended to `try` expressions. The result type of a `try` is not allowed to + capture capabilities defined in the body of the `try`. diff --git a/docs/_docs/reference/experimental/capture-checking/classes.md b/docs/_docs/reference/experimental/capture-checking/classes.md new file mode 100644 index 000000000000..9f9269915233 --- /dev/null +++ b/docs/_docs/reference/experimental/capture-checking/classes.md @@ -0,0 +1,233 @@ +--- +layout: doc-page +title: "Capture Checking of Classes" +nightlyOf: https://docs.scala-lang.org/scala3/reference/experimental/capture-checking/classes.html +--- + +## Introduction + +The principles for capture checking closures also apply to classes. For instance, consider: +```scala +class Logger(using fs: FileSystem): + def log(s: String): Unit = ... summon[FileSystem] ... + +def test(xfs: FileSystem): Logger^{xfs} = + Logger(xfs) +``` +Here, class `Logger` retains the capability `fs` as a (private) field. Hence, the result +of `test` is of type `Logger^{xfs}` + +Sometimes, a tracked capability is meant to be used only in the constructor of a class, but +is not intended to be retained as a field. This fact can be communicated to the capture +checker by declaring the parameter as `@constructorOnly`. Example: +```scala +import annotation.constructorOnly + +class NullLogger(using @constructorOnly fs: FileSystem): + ... +def test2(using fs: FileSystem): NullLogger = NullLogger() // OK +``` + +The captured references of a class include _local capabilities_ and _argument capabilities_. Local capabilities are capabilities defined outside the class and referenced from its body. Argument capabilities are passed as parameters to the primary constructor of the class. Local capabilities are inherited: +the local capabilities of a superclass are also local capabilities of its subclasses. Example: + +```scala +class Cap extends caps.SharedCapability + +def test(a: Cap, b: Cap, c: Cap) = + class Super(y: Cap): + def f = a + class Sub(x: Cap) extends Super(x) + def g = b + Sub(c) +``` +Here class `Super` has local capability `a`, which gets inherited by class +`Sub` and is combined with `Sub`'s own local capability `b`. Class `Sub` also has an argument capability corresponding to its parameter `x`. This capability gets instantiated to `c` in the final constructor call `Sub(c)`. Hence, +the capture set of that call is `{a, b, c}`. + +The capture set of the type of `this` of a class is inferred by the capture checker, unless the type is explicitly declared with a self type annotation like this one: +```scala +class C: + self: D^{a, b} => ... +``` +The inference observes the following constraints: + + - The type of `this` of a class `C` includes all captured references of `C`. + - The type of `this` of a class `C` is a subtype of the type of `this` + of each parent class of `C`. + - The type of `this` must observe all constraints where `this` is used. + +For instance, in +```scala +class Cap extends caps.SharedCapability +def test(c: Cap) = + class A: + val x: A = this + def f = println(c) // error +``` +we know that the type of `this` must be pure, since `this` is the right hand side of a `val` with type `A`. However, in the last line we find that the capture set of the class, and with it the capture set of `this`, would include `c`. This leads to a contradiction, and hence to a checking error: +``` + | def f = println(c) // error + | ^ + | reference (c : Cap) is not included in the allowed capture set {} + | of the enclosing class A +``` + +## Capture Tunnelling + +Consider the following simple definition of a `Pair` class: +```scala +class Pair[+A, +B](x: A, y: B): + def fst: A = x + def snd: B = y +``` +What happens if `Pair` is instantiated like this (assuming `ct` and `fs` are two capabilities in scope)? +```scala +def x: Int ->{ct} String +def y: Logger^{fs} +def p = Pair(x, y) +``` +The last line will be typed as follows: +```scala +def p: Pair[Int ->{ct} String, Logger^{fs}] = Pair(x, y) +``` +This might seem surprising. The `Pair(x, y)` value does capture capabilities `ct` and `fs`. Why don't they show up in its type at the outside? + +The answer is capture tunnelling. Once a type variable is instantiated to a capturing type, the +capture is not propagated beyond this point. On the other hand, if the type variable is instantiated +again on access, the capture information "pops out" again. For instance, even though `p` is technically pure because its capture set is empty, writing `p.fst` would record a reference to the captured capability `ct`. So if this access was put in a closure, the capability would again form part of the outer capture set. E.g. +```scala +() => p.fst : () -> Int ->{ct} String +``` +In other words, references to capabilities "tunnel through" in generic instantiations from creation to access; they do not affect the capture set of the enclosing generic data constructor applications. +This principle plays an important part in making capture checking concise and practical. + + +## A Larger Example + +As a larger example, we present an implementation of lazy lists and some use cases. For simplicity, +our lists are lazy only in their tail part. This corresponds to what the Scala-2 type `Stream` did, whereas Scala 3's `LazyList` type computes strictly less since it is also lazy in the first argument. + +Here is the base trait `LzyList` for our version of lazy lists: +```scala +trait LzyList[+A]: + def isEmpty: Boolean + def head: A + def tail: LzyList[A]^{this} +``` +Note that `tail` carries a capture annotation. It says that the tail of a lazy list can +potentially capture the same references as the lazy list as a whole. + +The empty case of a `LzyList` is written as usual: +```scala +object LzyNil extends LzyList[Nothing]: + def isEmpty = true + def head = ??? + def tail = ??? +``` +Here is a formulation of the class for lazy cons nodes: +```scala +import scala.compiletime.uninitialized + +final class LzyCons[+A](hd: A, tl: () => LzyList[A]^) extends LzyList[A]: + private var forced = false + private var cache: LzyList[A]^{this} = uninitialized + private def force = + if !forced then { cache = tl(); forced = true } + cache + + def isEmpty = false + def head = hd + def tail: LzyList[A]^{this} = force +end LzyCons +``` +The `LzyCons` class takes two parameters: A head `hd` and a tail `tl`, which is a function +returning a `LzyList`. Both the function and its result can capture arbitrary capabilities. +The result of applying the function is memoized after the first dereference of `tail` in +the private mutable field `cache`. Note that the typing of the assignment `cache = tl()` relies on the monotonicity rule for `{this}` capture sets. + +Here is an extension method to define an infix cons operator `#:` for lazy lists. It is analogous +to `::` but instead of a strict list it produces a lazy list without evaluating its right operand. +```scala +extension [A](x: A) + def #:(xs1: => LzyList[A]^): LzyList[A]^{xs1} = + LzyCons(x, () => xs1) +``` +Note that `#:` takes an impure call-by-name parameter `xs1` as its right argument. The result +of `#:` is a lazy list that captures that argument. + +As an example usage of `#:`, here is a method `tabulate` that creates a lazy list +of given length with a generator function `gen`. The generator function is allowed +to have side effects. +```scala +def tabulate[A](n: Int)(gen: Int => A): LzyList[A]^{gen} = + def recur(i: Int): LzyList[A]^{gen} = + if i == n then LzyNil + else gen(i) #: recur(i + 1) + recur(0) +``` +Here is a use of `tabulate`: +```scala +class LimitExceeded extends Exception +def squares(n: Int)(using ct: CanThrow[LimitExceeded]) = + tabulate(10): i => + if i > 9 then throw LimitExceeded() + i * i +``` +The inferred result type of `squares` is `LzyList[Int]^{ct}`, i.e it is a lazy list of +`Int`s that can throw the `LimitExceeded` exception when it is elaborated by calling `tail` +one or more times. + +Here are some further extension methods for mapping, filtering, and concatenating lazy lists: +```scala +extension [A](xs: LzyList[A]^) + def map[B](f: A => B): LzyList[B]^{xs, f} = + if xs.isEmpty then LzyNil + else f(xs.head) #: xs.tail.map(f) + + def filter(p: A => Boolean): LzyList[A]^{xs, p} = + if xs.isEmpty then LzyNil + else if p(xs.head) then xs.head #: xs.tail.filter(p) + else xs.tail.filter(p) + + def concat(ys: LzyList[A]^): LzyList[A]^{xs, ys} = + if xs.isEmpty then ys + else xs.head #: xs.tail.concat(ys) + + def drop(n: Int): LzyList[A]^{xs} = + if n == 0 then xs else xs.tail.drop(n - 1) +``` +Their capture annotations are all as one would expect: + + - Mapping a lazy list produces a lazy list that captures the original list as well + as the (possibly impure) mapping function. + - Filtering a lazy list produces a lazy list that captures the original list as well + as the (possibly impure) filtering predicate. + - Concatenating two lazy lists produces a lazy list that captures both arguments. + - Dropping elements from a lazy list gives a safe approximation where the original list is captured in the result. In fact, it's only some suffix of the list that is retained at run time, but our modelling identifies lazy lists and their suffixes, so this additional knowledge would not be useful. + +Of course the function passed to `map` or `filter` could also be pure. After all, `A -> B` is a subtype of `(A -> B)^{cap}` which is the same as `A => B`. In that case, the pure function +argument will _not_ show up in the result type of `map` or `filter`. For instance: +```scala +val xs = squares(10) +val ys: LzyList[Int]^{xs} = xs.map(_ + 1) +``` +The type of the mapped list `ys` has only `xs` in its capture set. The actual function +argument does not show up since it is pure. Likewise, if the lazy list +`xs` was pure, it would not show up in any of the method results. +This demonstrates that capability-based +effect systems with capture checking are naturally _effect polymorphic_. + +This concludes our example. It's worth mentioning that an equivalent program defining and using standard, strict lists would require no capture annotations whatsoever. It would compile exactly as written now in standard Scala 3, yet one gets the capture checking for free. Essentially, `=>` already means "can capture anything" and since in a strict list side effecting operations are not retained in the result, there are no additional captures to record. A strict list could of course capture side-effecting closures in its elements but then tunnelling applies, since +these elements are represented by a type variable. This means we don't need to annotate anything there either. + +Another possibility would be a variant of lazy lists that requires all functions passed to `map`, `filter` and other operations like it to be pure. E.g. `map` on such a list would be defined like this: +```scala +extension [A](xs: LzyList[A]) + def map[B](f: A -> B): LzyList[B] = ... +``` +That variant would not require any capture annotations either. + +To summarize, there are two "sweet spots" of data structure design: strict lists in +side-effecting or resource-aware code and lazy lists in purely functional code. +Both are already correctly capture-typed without requiring any explicit annotations. Capture annotations only come into play where the semantics gets more complicated because we deal with delayed effects such as in impure lazy lists or side-effecting iterators over strict lists. This property is probably one of the greatest plus points of our approach to capture checking compared to previous techniques which tend to be more noisy. diff --git a/docs/_docs/reference/experimental/capture-checking/classifiers.md b/docs/_docs/reference/experimental/capture-checking/classifiers.md new file mode 100644 index 000000000000..5de21e4e469f --- /dev/null +++ b/docs/_docs/reference/experimental/capture-checking/classifiers.md @@ -0,0 +1,109 @@ +--- +layout: doc-page +title: "Capability Classifiers" +nightlyOf: https://docs.scala-lang.org/scala3/reference/experimental/capture-checking/classifiers.html +--- + +## Introduction + +Capabilities are extremely versatile. They can express concepts from many different domains. Exceptions, continuations, I/O, mutation, information flow, security permissions, are just some examples, the list goes on. + +Sometimes it is important to restrict, or: _classify_ what kind of capabilities are expected or returned in a context. For instance, we might want to allow only control capabilities such as `CanThrow`s or boundary `Label`s but no +other capabilities. Or might want to allow mutation, but no other side effects. This is achieved by having a capability class extend a _classifier_. + +For instance, the `scala.caps` package defines a classifier trait called `Control`, +like this: +```scala + trait Control extends SharedCapability, Classifier +``` +The Gears library then defines a capability class `Async` which extends `Control`. + +```scala + trait Async extends Control +``` +Unlike normal inheritance, classifiers also restrict the capture set of a capability. For instance, say we have a function +```scala + def f(using async: Async^) = body +``` +(the `^` is as usual redundant here since `Async` is a capability trait). +Then we have the guarantee that any actual `async` argument can only capture +capabilities that have types extending `Control`. No other capabilities such as mutation or I/O are allowed. + +A class or trait becomes a classifier by extending directly the marker trait +`caps.Classifier`. So with the definitions above, `Control` is a classifier trait, but `Async` is not, since it extends `Classifier` only indirectly, through `Control`. + +Classifiers are unique: a class cannot extend directly or transitively at the same time two unrelated classifier traits. So if a class transitively extends two classifier traits `C1` and `C2` then one of them must be a subtrait of the other. + +### Predefined Classifiers + +The `caps` object defines the `Classifier` trait itself and some traits that extend it: +```scala +trait Classifier + +sealed trait Capability + +trait SharedCapability extends Capability Classifier +trait Control extends SharedCapability, Classifier + +trait ExclusiveCapability extends Capability, Classifier +trait Mutable extends ExclusiveCapability, Classifier +``` +Here is a graph showing the hierarchy of predefined classifier traits: +``` + Capability + / \ + / \ + / \ + / \ + SharedCapability ExclusiveCapability + | | + | | + | | + | | + Control Mutable +``` +At the top of the hierarchy, we distinguish between _shared_ and _exclusive_ capabilities in two classifier traits `SharedCapability` and `ExclusiveCapability`. All capability classes we have seen so far are shared. +`ExclusiveCapability` is a base trait for capabilities that allow only un-aliased access to the data they represent, with the rules governed by [separation checking](separation-checking.md). Separation checking is currently an optional extension of capture checking, enabled by a different language import. Since `Capability` is a sealed trait, all capability classes are either shared or exclusive. + +`Control` capabilities are shared. This means they cannot directly or indirectly capture exclusive capabilities such as capabilities that control access to mutable state. Typical `Control` capabilities are: + + - `Label`s that enable to return from a `boundary`, + - `CanThrow` capabilities that enable throwing exceptions, or + - `Async` capabilities that allow to suspend. + +These are all expressed by having their capability classes extend `Control`. + +### Classifier Restriction + +Consider the following problem: The `Try.apply` method takes in its `body` parameter a computation, and runs it while catching any exceptions or `boundary.break` aborts. The exception or break will be re-issued when calling +the `get` method of a `Try` object. What should a capability-aware signature of `Try` be? + +The body passed to `Try.apply` can have arbitrary effects, so it can retain arbitrary capabilities. Yet the resulting `Try` object will retain only those capabilities of `body` which are classified as `Control`. So the signature of `Try.apply` should look like this: +```scala +object Try: + def apply[T](body: => T): Try[T]^{body.only[Control]} +``` +Note a new form of capability in the result's capture set: `body.only[Control]`. This is called a _restricted capability_. The general form of a restricted capability is +`c.only[A]` where + + - `c` is a regular, unrestricted capability + - `A` is a classifier trait. + + When substituting a capability set for the underlying capability, we drop all capabilities that are known to be unrelated to the classifier. For instance, say we have an actual body `{ expr }` that uses a capture set `{io, async}` where + + - `io` is an `IO` capability, where IO is assumed to extend `SharedCapability` but not `Control`. + - `async` is a `Control` capability. + +Then the result of `Try { expr }` would have type `Try^{async}`. We drop `io` since +`io`'s type is a `Capability` class that does not extend `Control`. + +If `expr` would use an additional capability `proc: () => Unit`, then `proc` would also show up in the result capture set. Since `proc` is fully effect-polymorphic, we can't exclude that it retains `Control` capabilities, so we have to keep it in the restricted capture set. These elements are shown together in the following example: +```scala +class IO extends caps.SharedCapability +class Async extends caps.Control + +def test(io: IO, async: Async, proc: () => Unit) = + val r = Try: + // code accessing `io`, `async`, and `proc` and returning an `Int. + val _: Try[Int]^{async, proc} = r +``` diff --git a/docs/_docs/reference/experimental/capture-checking/how-to-use.md b/docs/_docs/reference/experimental/capture-checking/how-to-use.md new file mode 100644 index 000000000000..d08125dc3fc8 --- /dev/null +++ b/docs/_docs/reference/experimental/capture-checking/how-to-use.md @@ -0,0 +1,19 @@ +--- +layout: doc-page +title: "How to Use the Capture Checker" +nightlyOf: https://docs.scala-lang.org/scala3/reference/experimental/capture-checking/how-to-use.html +--- + +## Enabling Capture Checking + +TODO + +## Compilation Options + +The following options are relevant for capture checking. + + - **-Vprint:cc** Prints the program with capturing types as inferred by capture checking. + - **-Ycc-verbose** Prints capabilities and capturing types in more detail. + - **-Ycc-debug** Gives more detailed, implementation-oriented information about capture checking, as described in the next section. + + The implementation supporting capture checking with these options is currently in branch `cc-experiment` on dotty.epfl.ch. diff --git a/docs/_docs/reference/experimental/capture-checking/internals.md b/docs/_docs/reference/experimental/capture-checking/internals.md new file mode 100644 index 000000000000..6aff9b208fd9 --- /dev/null +++ b/docs/_docs/reference/experimental/capture-checking/internals.md @@ -0,0 +1,84 @@ +--- +layout: doc-page +title: "Capture Checking Internals" +nightlyOf: https://docs.scala-lang.org/scala3/reference/experimental/capture-checking/internals.html +--- + +The capture checker is architected as a propagation constraint solver, which runs as a separate phase after type-checking and some initial transformations. + +Constraint variables stand for unknown capture sets. A constraint variable is introduced + + - for every part of a previously inferred type, + - for the accessed references of every method, class, anonymous function, or by-name argument, + - for the parameters passed in a class constructor call. + +Capture sets in explicitly written types are treated as constants (before capture checking, such sets are simply ignored). + +The capture checker essentially rechecks the program with the usual typing rules. Every time a subtype requirement between capturing types is checked, this translates to a subcapturing test on capture sets. If the two sets are constant, this is simply a yes/no question, where a no will produce an error message. + +If the lower set `C₁` of a comparison `C₁ <: C₂` is a variable, the set `C₂` is recorded +as a _superset_ of `C₁`. If the upper set `C₂` is a variable, the elements of `C₁` are _propagated_ to `C₂`. Propagation of an element `x` to a set `C` means that `x` is included as an element in `C`, and it is also propagated +to all known supersets of `C`. If such a superset is a constant, it is checked that `x` is included in it. If that's not the case, the original comparison `C₁ <: C₂` has no solution and an error is reported. + +The type checker also performs various maps on types, for instance when substituting actual argument types for formal parameter types in dependent functions, or mapping +member types with "as-seen-from" in a selection. Maps keep track of the variance +of positions in a type. The variance is initially covariant, it flips to +contravariant in function parameter positions, and can be either covariant, +contravariant, or nonvariant in type arguments, depending on the variance of +the type parameter. + +When capture checking, the same maps are also performed on capture sets. If a capture set is a constant, its elements (which are capabilities) are mapped as regular types. If the result of such a map is not a capability, the result is approximated according to the variance of the type. A covariant approximation replaces a type by its capture set. +A contravariant approximation replaces it with the empty capture set. A nonvariant +approximation replaces the enclosing capturing type with a range of possible types +that gets propagated and resolved further out. + +When a mapping `m` is performed on a capture set variable `C`, a new variable `Cm` is created that contains the mapped elements and that is linked with `C`. If `C` subsequently acquires further elements through propagation, these are also propagated to `Cm` after being transformed by the `m` mapping. `Cm` also gets the same supersets as `C`, mapped again using `m`. + +One interesting aspect of the capture checker concerns the implementation of capture tunnelling. The [foundational theory](https://infoscience.epfl.ch/record/290885) on which capture checking is based makes tunnelling explicit through so-called _box_ and +_unbox_ operations. Boxing hides a capture set and unboxing recovers it. The capture checker inserts virtual box and unbox operations based on actual and expected types similar to the way the type checker inserts implicit conversions. When capture set variables are first introduced, any capture set in a capturing type that is an instance of a type parameter instance is marked as "boxed". A boxing operation is +inserted if the expected type of an expression is a capturing type with +a boxed capture set variable. The effect of the insertion is that any references +to capabilities in the boxed expression are forgotten, which means that capture +propagation is stopped. Dually, if the actual type of an expression has +a boxed variable as capture set, an unbox operation is inserted, which adds all +elements of the capture set to the environment. + +Boxing and unboxing has no runtime effect, so the insertion of these operations is only simulated; the only visible effect is the retraction and insertion +of variables in the capture sets representing the environment of the currently checked expression. + +The `-Ycc-debug` option provides some insight into the workings of the capture checker. +When it is turned on, boxed sets are marked explicitly and capture set variables are printed with an ID and some information about their provenance. For instance, the string `{f, xs}33M5V` indicates a capture set +variable that is known to hold elements `f` and `xs`. The variable's ID is `33`. The `M` +indicates that the variable was created through a mapping from a variable with ID `5`. The latter is a regular variable, as indicated + by `V`. + +Generally, the string following the capture set consists of alternating numbers and letters where each number gives a variable ID and each letter gives the provenance of the variable. Possible letters are + + - `V` : a regular variable, + - `M` : a variable resulting from a _mapping_ of the variable indicated by the string to the right, + - `B` : similar to `M` but where the mapping is a _bijection_, + - `F` : a variable resulting from _filtering_ the elements of the variable indicated by the string to the right, + - `I` : a variable resulting from an _intersection_ of two capture sets, + - `D` : a variable resulting from the set _difference_ of two capture sets. + - `R` : a regular variable that _refines_ a class parameter, so that the capture + set of a constructor argument is known in the class instance type. + +At the end of a compilation run, `-Ycc-debug` will print all variable dependencies of variables referred to in previous output. Here is an example: +``` +Capture set dependencies: + {}2V :: + {}3V :: + {}4V :: + {f, xs}5V :: {f, xs}31M5V, {f, xs}32M5V + {f, xs}31M5V :: {xs, f} + {f, xs}32M5V :: +``` +This section lists all variables that appeared in previous diagnostics and their dependencies, recursively. For instance, we learn that + + - variables 2, 3, 4 are empty and have no dependencies, + - variable `5` has two dependencies: variables `31` and `32` which both result from mapping variable `5`, + - variable `31` has a constant fixed superset `{xs, f}` + - variable `32` has no dependencies. + + + diff --git a/docs/_docs/reference/experimental/capture-checking/polymorphism.md b/docs/_docs/reference/experimental/capture-checking/polymorphism.md new file mode 100644 index 000000000000..8e168de03f2c --- /dev/null +++ b/docs/_docs/reference/experimental/capture-checking/polymorphism.md @@ -0,0 +1,95 @@ +--- +layout: doc-page +title: "Capability Polymorphism" +nightlyOf: https://docs.scala-lang.org/scala3/reference/experimental/capture-checking/polymorphism.html +--- + +## Introduction + +It is sometimes convenient to write operations that are parameterized with a capture set of capabilities. For instance consider a type of event sources +`Source` on which `Listener`s can be registered. Listeners can hold certain capabilities, which show up as a parameter to `Source`: +```scala +class Source[X^]: + private var listeners: Set[Listener^{X}] = Set.empty + def register(x: Listener^{X}): Unit = + listeners += x + + def allListeners: Set[Listener^{X}] = listeners +``` +The type variable `X^` can be instantiated with a set of capabilities. It can occur in capture sets in its scope. For instance, in the example above +we see a variable `listeners` that has as type a `Set` of `Listeners` capturing `X`. The `register` method takes a listener of this type +and assigns it to the variable. + +Capture-set variables `X^` without user-annotated bounds by default range over the interval `>: {} <: {caps.cap}` which is the universe of capture sets instead of regular types. + +Under the hood, such capture-set variables are represented as regular type variables within the special interval + `>: CapSet <: CapSet^`. +For instance, `Source` from above could be equivalently +defined as follows: +```scala +class Source[X >: CapSet <: CapSet^]: + ... +``` +`CapSet` is a sealed trait in the `caps` object. It cannot be instantiated or inherited, so its only +purpose is to identify type variables which are capture sets. In non-capture-checked +usage contexts, the type system will treat `CapSet^{a}` and `CapSet^{a,b}` as the type `CapSet`, whereas +with capture checking enabled, it will take the annotated capture sets into account, +so that `CapSet^{a}` and `CapSet^{a,b}` are distinct. +This representation based on `CapSet` is subject to change and +its direct use is discouraged. + +Capture-set variables can be inferred like regular type variables. When they should be instantiated +explicitly one supplies a concrete capture set. For instance: +```scala +class Async extends caps.SharedCapability + +def listener(async: Async): Listener^{async} = ??? + +def test1(async1: Async, others: List[Async]) = + val src = Source[{async1, others*}] + ... +``` +Here, `src` is created as a `Source` on which listeners can be registered that refer to the `async` capability or to any of the capabilities in list `others`. So we can continue the example code above as follows: +```scala + src.register(listener(async1)) + others.map(listener).foreach(src.register) + val ls: Set[Listener^{async, others*}] = src.allListeners +``` +A common use-case for explicit capture parameters is describing changes to the captures of mutable fields, such as concatenating +effectful iterators: +```scala +class ConcatIterator[A, C^](var iterators: mutable.List[IterableOnce[A]^{C}]): + def concat(it: IterableOnce[A]^): ConcatIterator[A, {C, it}]^{this, it} = + iterators ++= it // ^ + this // track contents of `it` in the result +``` +In such a scenario, we also should ensure that any pre-existing alias of a `ConcatIterator` object should become +inaccessible after invoking its `concat` method. This is achieved with mutation and separation tracking which are +currently in development. + +## Capability Members + +Just as parametrization by types can be equally expressed with type members, we could +also define the `Source[X^]` class above could using a _capability member_: +```scala +class Source: + type X^ + private var listeners: Set[Listener^{this.X}] = Set.empty + ... // as before +``` +Here, we can refer to capability members using paths in capture sets (such as `{this.X}`). Similarly to type members, +capability members can be upper- and lower-bounded with capture sets: +```scala +trait Thread: + type Cap^ + def run(block: () ->{this.Cap} -> Unit): Unit + +trait GPUThread extends Thread: + type Cap^ >: {cudaMalloc, cudaFree} <: {caps.cap} +``` +Since `caps.cap` is the top element for subcapturing, we could have also left out the +upper bound: `type Cap^ >: {cudaMalloc, cudaFree}`. + +---- + +[More Advanced Use Cases](advanced.md) diff --git a/docs/_docs/reference/experimental/capture-checking/scoped-caps.md b/docs/_docs/reference/experimental/capture-checking/scoped-caps.md new file mode 100644 index 000000000000..455a916e1692 --- /dev/null +++ b/docs/_docs/reference/experimental/capture-checking/scoped-caps.md @@ -0,0 +1,120 @@ +--- +layout: doc-page +title: "Scoped Caps" +nightlyOf: https://docs.scala-lang.org/scala3/reference/experimental/capture-checking/scoped-caps.html +--- + +## Introduction + +When discussing escape checking, we referred to a scoping discipline. That is, capture sets can contain only capabilities that are visible at the point where the set is defined. But that raises the question where a universal capability `cap` is defined? In fact, what is written as the top type `cap` can mean different capabilities, depending on scope. Usually a `cap` refers to a universal capability defined in the scope where the `cap` appears. + +Special rules apply to `cap`s in method and function parameters and results. For example, take this method: + +```scala + def makeLogger(fs: FileSystem^): Logger^ = new Logger(fs) +``` +This creates a `Logger` that captures `fs`. +We could have been more specific in specifying `Logger^{fs}` as the return type of makeLogger, but the current definition is also valid, and might be preferable if we want to hide details what the returned logger captures. If we write it as above then certainly the implied `cap` in the return type of `Logger` should be able subsume the capability `fs`. This means that this `cap` has to be defined in a scope in which +`fs` is visible. + +In logic, the usual way to achieve this scoping is with an existential binder. We can express the type of `makeLogger` like this: +```scala +makeLogger: (fs: ∃cap₁.FileSystem^{cap₁}): ∃cap₂. Logger^{cap₂} +``` +In words: `makeLogger` takes a parameter `fs` of type `Filesystem` capturing _some_ universal capability `cap` and returns a `Logger` capturing some other (possibly different) universal `cap`. + +We can also turn the existential in the function parameter to a universal "forall" +in the function itself. In that alternative notation, the type of makeLogger would read like this: +```scala +makeLogger: ∀cap₁.(fs: FileSystem^{cap₁}): ∃cap₂. Logger^{cap₂} +``` +There's a connection with capture polymorphism here. `cap`s in function parameters behave like additional +capture parameters that can be instantiated at the call site to arbitrary capabilities. + +The conventions for method types carry over to function types. A function type +```scala + (x: T) -> U^ +``` +is interpreted as having an existentially bound `cap` in the result, like this +```scala + (x: T) -> ∃cap.U^{cap} +``` +The same rules hold for the other kinds of function arrows, `=>`, `?->`, and `?=>`. So `cap` can in this case +subsume the function parameter `x` since it is locally bound in the function result. + +However, the expansion of `cap` into an existentially bound variable only applies to functions that use +the dependent function style syntax, with explicitly named parameters. Parametric functions such as +`A => B^` or `(A₍, ..., Aₖ) -> B^` don't bind their result cap in an existential quantifier. +For instance, the function +```scala + (x: A) -> B -> C^ +``` +is interpreted as +```scala + (x: A) -> ∃cap.B -> C^{cap} +``` +In other words, existential quantifiers are only inserted in results of function arrows that follow an explicitly named parameter list. + +To summarize: + + - If a function result type follows a named parameter list and contains covariant occurrences of `cap`, + we replace these occurrences with a fresh existential variable which + is bound by a quantifier scoping over the result type. + - If a function parameter type contains covariant occurrences of `cap`, we replace these occurrences with + a fresh existential variable scoping over the parameter type. + - Occurrences of `cap` elsewhere are not translated. They can be seen as representing an existential in the + scope of the definition in which they appear. + +**Examples:** + + - `A => B` is an alias type that expands to `A ->{cap} B`, therefore + `(x: T) -> A => B` expands to `(x: T) -> ∃cap.(A ->{cap} B)`. + + - `(x: T) -> Iterator[A => B]` expands to `() -> ∃cap.Iterator[A ->{cap} B]` + + +## Reach Capabilities + +Say you have a method `f` that takes an impure function argument which gets stored in a `var`: +```scala +def f(op: A => B) + var x: A ->{op} B = op + ... +``` +This is legal even though `var`s cannot have types with `cap` or existential capabilities. The trick is that the type of the variable `x` +is not `A => B` (this would be rejected), but is the "narrowed" type +`A ->{op} B`. In other words, all capabilities retained by values of `x` +are all also referred to by `op`, which justifies the replacement of `cap` by `op`. + +A more complicated situation is if we want to store successive values +held in a list. Example: +```scala +def f(ops: List[A => B]) + var xs = ops + var x: ??? = xs.head + while xs.nonEmpty do + xs = xs.tail + x = xs.head + ... +``` +Here, `x` cannot be given a type with an `ops` capability. In fact, `ops` is pure, i.e. it's capture set is empty, so it cannot be used as the name of a capability. What we would like to express is that `x` refers to +any operation "reachable" through `ops`. This can be expressed using a +_reach capability_ `ops*`. +```scala +def f(ops: List[A => B]) + var xs = ops + var x: A ->{ops*} B = xs.head + ... +``` +Reach capabilities take the form `x*` where `x` is syntactically a regular capability. If `x: T` then `x*` stands for any capability that appears covariantly in `T` and that is accessed through `x`. The least supertype of this capability is the set of all capabilities appearing covariantly in `T`. diff --git a/docs/_docs/reference/experimental/capture-checking/separation-checking.md b/docs/_docs/reference/experimental/capture-checking/separation-checking.md new file mode 100644 index 000000000000..8b0b2850d611 --- /dev/null +++ b/docs/_docs/reference/experimental/capture-checking/separation-checking.md @@ -0,0 +1,7 @@ +--- +layout: doc-page +title: "Separation Checking" +nightlyOf: https://docs.scala-lang.org/scala3/reference/experimental/capture-checking/separation-checking.html +--- + +## TODO \ No newline at end of file diff --git a/docs/_docs/reference/experimental/cc.md b/docs/_docs/reference/experimental/cc.md deleted file mode 100644 index 04c9d440a427..000000000000 --- a/docs/_docs/reference/experimental/cc.md +++ /dev/null @@ -1,902 +0,0 @@ ---- -layout: doc-page -title: "Capture Checking" -nightlyOf: https://docs.scala-lang.org/scala3/reference/experimental/cc.html ---- - -Capture checking is a research project that modifies the Scala type system to track references to capabilities in values. It can be enabled by the language import -```scala -import language.experimental.captureChecking -``` -At present, capture checking is still highly experimental and unstable, and it evolves quickly. -Before trying it out, make sure you have the latest version of Scala. - -To get an idea what capture checking can do, let's start with a small example: -```scala -def usingLogFile[T](op: FileOutputStream => T): T = - val logFile = FileOutputStream("log") - val result = op(logFile) - logFile.close() - result -``` -The `usingLogFile` method invokes a given operation with a fresh log file as parameter. Once the operation has ended, the log file is closed and the -operation's result is returned. This is a typical _try-with-resources_ pattern, similar to many other such patterns which are often supported by special language constructs in other languages. - -The problem is that `usingLogFile`'s implementation is not entirely safe. One can -undermine it by passing an operation that performs the logging at some later point -after it has terminated. For instance: -```scala -val later = usingLogFile { file => () => file.write(0) } -later() // crash -``` -When `later` is executed it tries to write to a file that is already closed, which -results in an uncaught `IOException`. - -Capture checking gives us the mechanism to prevent such errors _statically_. To -prevent unsafe usages of `usingLogFile`, we can declare it like this: -```scala -def usingLogFile[T](op: FileOutputStream^ => T): T = - // same body as before -``` -The only thing that's changed is that the `FileOutputStream` parameter of `op` is now -followed by `^`. We'll see that this turns the parameter into a _capability_ whose lifetime is tracked. - -If we now try to define the problematic value `later`, we get a static error: -``` - | val later = usingLogFile { f => () => f.write(0) } - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - |The expression's type () => Unit is not allowed to capture the root capability `cap`. - |This usually means that a capability persists longer than its allowed lifetime. -``` -In this case, it was easy to see that the `logFile` capability escapes in the closure passed to `usingLogFile`. But capture checking also works for more complex cases. -For instance, capture checking is able to distinguish between the following safe code: -```scala -val xs = usingLogFile { f => - List(1, 2, 3).map { x => f.write(x); x * x } -} -``` -and the following unsafe one: -```scala -val xs = usingLogFile { f => - LazyList(1, 2, 3).map { x => f.write(x); x * x } -} -``` -An error would be issued in the second case, but not the first one (this assumes a capture-aware -formulation of `LazyList` which we will present later in this page). - -It turns out that capture checking has very broad applications. Besides the various -try-with-resources patterns, it can also be a key part to the solutions of many other long standing problems in programming languages. Among them: - - - How to have a simple and flexible system for checked exceptions. We show later - how capture checking enables a clean and fully safe system for checked exceptions in Scala. - - How to address the problem of effect polymorphism in general. - - How to solve the "what color is your function?" problem of mixing synchronous - and asynchronous computations. - - How to do region-based allocation, safely, - - How to reason about capabilities associated with memory locations. - -The following sections explain in detail how capture checking works in Scala 3. - - -## Overview - -The capture checker extension introduces a new kind of types and it enforces some rules for working with these types. - -## Capabilities and Capturing Types - -Capture checking is done in terms of _capturing types_ of the form -`T^{c₁, ..., cᵢ}`. Here `T` is a type, and `{c₁, ..., cᵢ}` is a _capture set_ consisting of references to capabilities `c₁, ..., cᵢ`. - -A _capability_ is syntactically a method- or class-parameter, a local variable, or the `this` of an enclosing class. The type of a capability -must be a capturing type with a non-empty capture set. We also say that -variables that are capabilities are _tracked_. - -In a sense, every -capability gets its authority from some other, more sweeping capability which it captures. The most sweeping capability, from which ultimately all others are derived is written `cap`. We call it the _universal capability_. -If `T` is a type, then `T^` is a shorthand for `T^{cap}`, meaning `T` can capture arbitrary capabilities. - -Here is an example: -```scala -class FileSystem - -class Logger(fs: FileSystem^): - def log(s: String): Unit = ... // Write to a log file, using `fs` - -def test(fs: FileSystem^) = - val l: Logger^{fs} = Logger(fs) - l.log("hello world!") - val xs: LazyList[Int]^{l} = - LazyList.from(1) - .map { i => - l.log(s"computing elem # $i") - i * i - } - xs -``` -Here, the `test` method takes a `FileSystem` as a parameter. `fs` is a capability since its type has a non-empty capture set. The capability is passed to the `Logger` constructor -and retained as a field in class `Logger`. Hence, the local variable `l` has type -`Logger^{fs}`: it is a `Logger` which retains the `fs` capability. - -The second variable defined in `test` is `xs`, a lazy list that is obtained from -`LazyList.from(1)` by logging and mapping consecutive numbers. Since the list is lazy, -it needs to retain the reference to the logger `l` for its computations. Hence, the -type of the list is `LazyList[Int]^{l}`. On the other hand, since `xs` only logs but does -not do other file operations, it retains the `fs` capability only indirectly. That's why -`fs` does not show up in the capture set of `xs`. - -Capturing types come with a subtype relation where types with "smaller" capture sets are subtypes of types with larger sets (the _subcapturing_ relation is defined in more detail below). If a type `T` does not have a capture set, it is called _pure_, and is a subtype of -any capturing type that adds a capture set to `T`. - -## Function Types - -The usual function type `A => B` now stands for a function that can capture arbitrary capabilities. We call such functions -_impure_. By contrast, the new single arrow function type `A -> B` stands for a function that cannot capture any capabilities, or otherwise said, is _pure_. -One can add a capture set after the arrow of an otherwise pure function. -For instance, `A ->{c, d} B` would be a function that can capture capabilities `c` and `d`, but no others. -This type is a shorthand for `(A -> B)^{c, d}`, i.e. the function type `A -> B` with possible captures `{c, d}`. - -The impure function type `A => B` is treated as an alias for `A ->{cap} B`. That is, impure functions are functions that can capture anything. - -A capture annotation `^` binds more strongly than a function arrow. So -`A -> B^{c}` is read as `A -> (B^{c})`. - -Analogous conventions apply to context function types. `A ?=> B` is an impure context function, with `A ?-> B` as its pure complement. - -**Note 1:** The identifiers `->` and `?->` are now treated as soft keywords when used as infix type operators. They are -still available as regular identifiers for terms. For instance, the mapping syntax `Map("x" -> 1, "y" -> 2)` is still supported since it only applies to terms. - -**Note 2:** The distinctions between pure vs impure function types do not apply to methods. In fact, since methods are not values they never capture anything directly. References to -capabilities in a method are instead counted in the capture set of the enclosing object. - -## By-Name Parameter Types - -A convention analogous to function types also extends to by-name parameters. In -```scala -def f(x: => Int): Int -``` -the actual argument can refer to arbitrary capabilities. So the following would be OK: -```scala -f(if p(y) then throw Ex() else 1) -``` -On the other hand, if `f` was defined like this -```scala -def f(x: -> Int): Int -``` -the actual argument to `f` could not refer to any capabilities, so the call above would be rejected. -One can also allow specific capabilities like this: -```scala -def f(x: ->{c} Int): Int -``` -Here, the actual argument to `f` is allowed to use the `c` capability but no others. - -## Subtyping and Subcapturing - -Capturing influences subtyping. As usual we write `T₁ <: T₂` to express that the type -`T₁` is a subtype of the type `T₂`, or equivalently, that `T₁` conforms to `T₂`. An -analogous _subcapturing_ relation applies to capture sets. If `C₁` and `C₂` are capture sets, we write `C₁ <: C₂` to express that `C₁` _is covered by_ `C₂`, or, swapping the operands, that `C₂` _covers_ `C₁`. - -Subtyping extends as follows to capturing types: - - - Pure types are subtypes of capturing types. That is, `T <: C T`, for any type `T`, capturing set `C`. - - For capturing types, smaller capturing sets produce subtypes: `C₁ T₁ <: C₂ T₂` if - `C₁ <: C₂` and `T₁ <: T₂`. - -A subcapturing relation `C₁ <: C₂` holds if `C₂` _accounts for_ every element `c` in `C₁`. This means one of the following three conditions must be true: - - - `c ∈ C₂`, - - `c` refers to a parameter of some class `Cls` and `C₂` contains `Cls.this`, - - `c`'s type has capturing set `C` and `C₂` accounts for every element of `C` (that is, `C <: C₂`). - - -**Example 1.** Given -```scala -fs: FileSystem^ -ct: CanThrow[Exception]^ -l : Logger^{fs} -``` -we have -``` -{l} <: {fs} <: {cap} -{fs} <: {fs, ct} <: {cap} -{ct} <: {fs, ct} <: {cap} -``` -The set consisting of the root capability `{cap}` covers every other capture set. This is -a consequence of the fact that, ultimately, every capability is created from `cap`. - -**Example 2.** Consider again the FileSystem/Logger example from before. `LazyList[Int]` is a proper subtype of `LazyList[Int]^{l}`. So if the `test` method in that example -was declared with a result type `LazyList[Int]`, we'd get a type error. Here is the error message: -``` -11 |def test(using fs: FileSystem^): LazyList[Int] = { - | ^ - | Found: LazyList[Int]^{fs} - | Required: LazyList[Int] -``` -Why does it say `LazyList[Int]^{fs}` and not `LazyList[Int]^{l}`, which is, after all, the type of the returned value `xs`? The reason is that `l` is a local variable in the body of `test`, so it cannot be referred to in a type outside that body. What happens instead is that the type is _widened_ to the smallest supertype that does not mention `l`. Since `l` has capture set `fs`, we have that `{fs}` covers `{l}`, and `{fs}` is acceptable in a result type of `test`, so `{fs}` is the result of that widening. -This widening is called _avoidance_; it is not specific to capture checking but applies to all variable references in Scala types. - -## 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 `Capability` class defined in object `cap`. - -The capture set of a `Capability` subclass type is always `{cap}`. This means we could equivalently express the `FileSystem` and `Logger` classes as follows: -```scala -import caps.Capability - -class FileSystem extends Capability - -class Logger(using FileSystem): - def log(s: String): Unit = ??? - -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`. Writing the capture set explicitly produces a warning: -```scala -class Logger(using FileSystem^{cap}): - ^^^^^^^^^^^^^^ - redundant capture: FileSystem already accounts for cap -``` -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. - -## Capture Checking of Closures - -If a closure refers to capabilities in its body, it captures these capabilities in its type. For instance, consider: -```scala -def test(fs: FileSystem): String ->{fs} Unit = - (x: String) => Logger(fs).log(x) -``` -Here, the body of `test` is a lambda that refers to the capability `fs`, which means that `fs` is retained in the lambda. -Consequently, the type of the lambda is `String ->{fs} Unit`. - -**Note:** Function values are always written with `=>` (or `?=>` for context functions). There is no syntactic -distinction for pure _vs_ impure function values. The distinction is only made in their types. - -A closure also captures all capabilities that are captured by the functions -it calls. For instance, in -```scala -def test(fs: FileSystem) = - def f() = g() - def g() = (x: String) => Logger(fs).log(x) - f -``` -the result of `test` has type `String ->{fs} Unit` even though function `f` itself does not refer to `fs`. - -## Capture Checking of Classes - -The principles for capture checking closures also apply to classes. For instance, consider: -```scala -class Logger(using fs: FileSystem): - def log(s: String): Unit = ... summon[FileSystem] ... - -def test(xfs: FileSystem): Logger^{xfs} = - Logger(xfs) -``` -Here, class `Logger` retains the capability `fs` as a (private) field. Hence, the result -of `test` is of type `Logger^{xfs}` - -Sometimes, a tracked capability is meant to be used only in the constructor of a class, but -is not intended to be retained as a field. This fact can be communicated to the capture -checker by declaring the parameter as `@constructorOnly`. Example: -```scala -import annotation.constructorOnly - -class NullLogger(using @constructorOnly fs: FileSystem): - ... -def test2(using fs: FileSystem): NullLogger = NullLogger() // OK -``` - -The captured references of a class include _local capabilities_ and _argument capabilities_. Local capabilities are capabilities defined outside the class and referenced from its body. Argument capabilities are passed as parameters to the primary constructor of the class. Local capabilities are inherited: -the local capabilities of a superclass are also local capabilities of its subclasses. Example: - -```scala -class Cap extends caps.Capability - -def test(a: Cap, b: Cap, c: Cap) = - class Super(y: Cap): - def f = a - class Sub(x: Cap) extends Super(x) - def g = b - Sub(c) -``` -Here class `Super` has local capability `a`, which gets inherited by class -`Sub` and is combined with `Sub`'s own local capability `b`. Class `Sub` also has an argument capability corresponding to its parameter `x`. This capability gets instantiated to `c` in the final constructor call `Sub(c)`. Hence, -the capture set of that call is `{a, b, c}`. - -The capture set of the type of `this` of a class is inferred by the capture checker, unless the type is explicitly declared with a self type annotation like this one: -```scala -class C: - self: D^{a, b} => ... -``` -The inference observes the following constraints: - - - The type of `this` of a class `C` includes all captured references of `C`. - - The type of `this` of a class `C` is a subtype of the type of `this` - of each parent class of `C`. - - The type of `this` must observe all constraints where `this` is used. - -For instance, in -```scala -class Cap extends caps.Capability -def test(c: Cap) = - class A: - val x: A = this - def f = println(c) // error -``` -we know that the type of `this` must be pure, since `this` is the right hand side of a `val` with type `A`. However, in the last line we find that the capture set of the class, and with it the capture set of `this`, would include `c`. This leads to a contradiction, and hence to a checking error: -``` -16 | def f = println(c) // error - | ^ - |(c : Cap) cannot be referenced here; it is not included in the allowed capture set {} -``` - -## Capture Tunnelling - -Consider the following simple definition of a `Pair` class: -```scala -class Pair[+A, +B](x: A, y: B): - def fst: A = x - def snd: B = y -``` -What happens if `Pair` is instantiated like this (assuming `ct` and `fs` are two capabilities in scope)? -```scala -def x: Int ->{ct} String -def y: Logger^{fs} -def p = Pair(x, y) -``` -The last line will be typed as follows: -```scala -def p: Pair[Int ->{ct} String, Logger^{fs}] = Pair(x, y) -``` -This might seem surprising. The `Pair(x, y)` value does capture capabilities `ct` and `fs`. Why don't they show up in its type at the outside? - -The answer is capture tunnelling. Once a type variable is instantiated to a capturing type, the -capture is not propagated beyond this point. On the other hand, if the type variable is instantiated -again on access, the capture information "pops out" again. For instance, even though `p` is technically pure because its capture set is empty, writing `p.fst` would record a reference to the captured capability `ct`. So if this access was put in a closure, the capability would again form part of the outer capture set. E.g. -```scala -() => p.fst : () -> Int ->{ct} String -``` -In other words, references to capabilities "tunnel through" in generic instantiations from creation to access; they do not affect the capture set of the enclosing generic data constructor applications. -This principle plays an important part in making capture checking concise and practical. - -## Escape Checking - -Some capture sets are restricted so that -they are not allowed to contain the universal capability. - -Specifically, if a capturing type is an instance of a type variable, that capturing type -is not allowed to carry the universal capability `cap`. There's a connection to tunnelling here. -The capture set of a type has to be present in the environment when a type is instantiated from -a type variable. But `cap` is not itself available as a global entity in the environment. Hence, -an error should result. - -We can now reconstruct how this principle produced the error in the introductory example, where -`usingLogFile` was declared like this: -```scala -def usingLogFile[T](op: FileOutputStream^ => T): T = ... -``` -The error message was: -``` - | val later = usingLogFile { f => () => f.write(0) } - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - |The expression's type () => Unit is not allowed to capture the root capability `cap`. - |This usually means that a capability persists longer than its allowed lifetime. -``` -This error message was produced by the following logic: - - - The `f` parameter has type `FileOutputStream^`, which makes it a capability. - - Therefore, the type of the expression `() => f.write(0)` is `() ->{f} Unit`. - - This makes the type of the whole closure passed to `usingLogFile` the dependent function type - `(f: FileOutputStream^) -> () ->{f} Unit`. - - The expected type of the closure is a simple, parametric, impure function type `FileOutputStream^ => T`, - for some instantiation of the type variable `T`. - - The smallest supertype of the closure's dependent function type that is a parametric function type is - `FileOutputStream^ => () ->{cap} Unit` - - Hence, the type variable `T` is instantiated to `() ->{cap} Unit`, or abbreviated `() => Unit`, - which causes the error. - -An analogous restriction applies to the type of a mutable variable. -Another way one could try to undermine capture checking would be to -assign a closure with a local capability to a global variable. Maybe -like this: -```scala -var loophole: () => Unit = () => () -usingLogFile { f => - loophole = () => f.write(0) -} -loophole() -``` -But this will not compile either, since mutable variables cannot have universal capture sets. - -One also needs to prevent returning or assigning a closure with a local capability in an argument of a parametric type. For instance, here is a -slightly more refined attack: -```scala -class Cell[+A](x: A) -val sneaky = usingLogFile { f => Cell(() => f.write(0)) } -sneaky.x() -``` -At the point where the `Cell` is created, the capture set of the argument is `f`, which -is OK. But at the point of use, it is `cap` (because `f` is no longer in scope), which causes again an error: -``` - | sneaky.x() - | ^^^^^^^^ - |The expression's type () => Unit is not allowed to capture the root capability `cap`. - |This usually means that a capability persists longer than its allowed lifetime. -``` - -Looking at object graphs, we observe a monotonicity property: The capture set of an object `x` covers the capture sets of all objects reachable through `x`. This property is reflected in the type system by the following _monotonicity rule_: - - - In a class `C` with a field `f`, the capture set `{this}` covers the capture set `{this.f}` as well as the capture set of any application of `this.f` to pure arguments. - -## Checked Exceptions - -Scala enables checked exceptions through a language import. Here is an example, -taken from the [safer exceptions page](./canthrow.md), and also described in a -[paper](https://infoscience.epfl.ch/record/290885) presented at the - 2021 Scala Symposium. -```scala -import language.experimental.saferExceptions - -class LimitExceeded extends Exception - -val limit = 10e+10 -def f(x: Double): Double throws LimitExceeded = - if x < limit then x * x else throw LimitExceeded() -``` -The new `throws` clause expands into an implicit parameter that provides -a `CanThrow` capability. Hence, function `f` could equivalently be written -like this: -```scala -def f(x: Double)(using CanThrow[LimitExceeded]): Double = ... -``` -If the implicit parameter is missing, an error is reported. For instance, the function definition -```scala -def g(x: Double): Double = - if x < limit then x * x else throw LimitExceeded() -``` -is rejected with this error message: -``` - | if x < limit then x * x else throw LimitExceeded() - | ^^^^^^^^^^^^^^^^^^^^^ - |The capability to throw exception LimitExceeded is missing. - |The capability can be provided by one of the following: - | - Adding a using clause `(using CanThrow[LimitExceeded])` to the definition of the enclosing method - | - Adding `throws LimitExceeded` clause after the result type of the enclosing method - | - Wrapping this piece of code with a `try` block that catches LimitExceeded -``` -`CanThrow` capabilities are required by `throw` expressions and are created -by `try` expressions. For instance, the expression -```scala -try xs.map(f).sum -catch case ex: LimitExceeded => -1 -``` -would be expanded by the compiler to something like the following: -```scala -try - erased given ctl: CanThrow[LimitExceeded] = compiletime.erasedValue - xs.map(f).sum -catch case ex: LimitExceeded => -1 -``` -(The `ctl` capability is only used for type checking but need not show up in the generated code, so it can be declared as -erased.) - -As with other capability based schemes, one needs to guard against capabilities -that are captured in results. For instance, here is a problematic use case: -```scala -def escaped(xs: Double*): (() => Double) throws LimitExceeded = - try () => xs.map(f).sum - catch case ex: LimitExceeded => () => -1 -val crasher = escaped(1, 2, 10e+11) -crasher() -``` -This code needs to be rejected since otherwise the call to `crasher()` would cause -an unhandled `LimitExceeded` exception to be thrown. - -Under the language import `language.experimental.captureChecking`, the code is indeed rejected -``` -14 | try () => xs.map(f).sum - | ^ - |The expression's type () => Double is not allowed to capture the root capability `cap`. - |This usually means that a capability persists longer than its allowed lifetime. -15 | catch case ex: LimitExceeded => () => -1 -``` -To integrate exception and capture checking, only two changes are needed: - - - `CanThrow` is declared as a class extending `Capability`, so all references to `CanThrow` instances are tracked. - - Escape checking is extended to `try` expressions. The result type of a `try` is not allowed to - capture the universal capability. - -## A Larger Example - -As a larger example, we present an implementation of lazy lists and some use cases. For simplicity, -our lists are lazy only in their tail part. This corresponds to what the Scala-2 type `Stream` did, whereas Scala 3's `LazyList` type computes strictly less since it is also lazy in the first argument. - -Here is the base trait `LzyList` for our version of lazy lists: -```scala -trait LzyList[+A]: - def isEmpty: Boolean - def head: A - def tail: LzyList[A]^{this} -``` -Note that `tail` carries a capture annotation. It says that the tail of a lazy list can -potentially capture the same references as the lazy list as a whole. - -The empty case of a `LzyList` is written as usual: -```scala -object LzyNil extends LzyList[Nothing]: - def isEmpty = true - def head = ??? - def tail = ??? -``` -Here is a formulation of the class for lazy cons nodes: -```scala -import scala.compiletime.uninitialized - -final class LzyCons[+A](hd: A, tl: () => LzyList[A]^) extends LzyList[A]: - private var forced = false - private var cache: LzyList[A]^{this} = uninitialized - private def force = - if !forced then { cache = tl(); forced = true } - cache - - def isEmpty = false - def head = hd - def tail: LzyList[A]^{this} = force -end LzyCons -``` -The `LzyCons` class takes two parameters: A head `hd` and a tail `tl`, which is a function -returning a `LzyList`. Both the function and its result can capture arbitrary capabilities. -The result of applying the function is memoized after the first dereference of `tail` in -the private mutable field `cache`. Note that the typing of the assignment `cache = tl()` relies on the monotonicity rule for `{this}` capture sets. - -Here is an extension method to define an infix cons operator `#:` for lazy lists. It is analogous -to `::` but instead of a strict list it produces a lazy list without evaluating its right operand. -```scala -extension [A](x: A) - def #:(xs1: => LzyList[A]^): LzyList[A]^{xs1} = - LzyCons(x, () => xs1) -``` -Note that `#:` takes an impure call-by-name parameter `xs1` as its right argument. The result -of `#:` is a lazy list that captures that argument. - -As an example usage of `#:`, here is a method `tabulate` that creates a lazy list -of given length with a generator function `gen`. The generator function is allowed -to have side effects. -```scala -def tabulate[A](n: Int)(gen: Int => A) = - def recur(i: Int): LzyList[A]^{gen} = - if i == n then LzyNil - else gen(i) #: recur(i + 1) - recur(0) -``` -Here is a use of `tabulate`: -```scala -class LimitExceeded extends Exception -def squares(n: Int)(using ct: CanThrow[LimitExceeded]) = - tabulate(10): i => - if i > 9 then throw LimitExceeded() - i * i -``` -The inferred result type of `squares` is `LzyList[Int]^{ct}`, i.e it is a lazy list of -`Int`s that can throw the `LimitExceeded` exception when it is elaborated by calling `tail` -one or more times. - -Here are some further extension methods for mapping, filtering, and concatenating lazy lists: -```scala -extension [A](xs: LzyList[A]^) - def map[B](f: A => B): LzyList[B]^{xs, f} = - if xs.isEmpty then LzyNil - else f(xs.head) #: xs.tail.map(f) - - def filter(p: A => Boolean): LzyList[A]^{xs, p} = - if xs.isEmpty then LzyNil - else if p(xs.head) then xs.head #: xs.tail.filter(p) - else xs.tail.filter(p) - - def concat(ys: LzyList[A]^): LzyList[A]^{xs, ys} = - if xs.isEmpty then ys - else xs.head #: xs.tail.concat(ys) - - def drop(n: Int): LzyList[A]^{xs} = - if n == 0 then xs else xs.tail.drop(n - 1) -``` -Their capture annotations are all as one would expect: - - - Mapping a lazy list produces a lazy list that captures the original list as well - as the (possibly impure) mapping function. - - Filtering a lazy list produces a lazy list that captures the original list as well - as the (possibly impure) filtering predicate. - - Concatenating two lazy lists produces a lazy list that captures both arguments. - - Dropping elements from a lazy list gives a safe approximation where the original list is captured in the result. In fact, it's only some suffix of the list that is retained at run time, but our modelling identifies lazy lists and their suffixes, so this additional knowledge would not be useful. - -Of course the function passed to `map` or `filter` could also be pure. After all, `A -> B` is a subtype of `(A -> B)^{cap}` which is the same as `A => B`. In that case, the pure function -argument will _not_ show up in the result type of `map` or `filter`. For instance: -```scala -val xs = squares(10) -val ys: LzyList[Int]^{xs} = xs.map(_ + 1) -``` -The type of the mapped list `ys` has only `xs` in its capture set. The actual function -argument does not show up since it is pure. Likewise, if the lazy list -`xs` was pure, it would not show up in any of the method results. -This demonstrates that capability-based -effect systems with capture checking are naturally _effect polymorphic_. - -This concludes our example. It's worth mentioning that an equivalent program defining and using standard, strict lists would require no capture annotations whatsoever. It would compile exactly as written now in standard Scala 3, yet one gets the capture checking for free. Essentially, `=>` already means "can capture anything" and since in a strict list side effecting operations are not retained in the result, there are no additional captures to record. A strict list could of course capture side-effecting closures in its elements but then tunnelling applies, since -these elements are represented by a type variable. This means we don't need to annotate anything there either. - -Another possibility would be a variant of lazy lists that requires all functions passed to `map`, `filter` and other operations like it to be pure. E.g. `map` on such a list would be defined like this: -```scala -extension [A](xs: LzyList[A]) - def map[B](f: A -> B): LzyList[B] = ... -``` -That variant would not require any capture annotations either. - -To summarize, there are two "sweet spots" of data structure design: strict lists in -side-effecting or resource-aware code and lazy lists in purely functional code. -Both are already correctly capture-typed without requiring any explicit annotations. Capture annotations only come into play where the semantics gets more complicated because we deal with delayed effects such as in impure lazy lists or side-effecting iterators over strict lists. This property is probably one of the greatest plus points of our approach to capture checking compared to previous techniques which tend to be more noisy. - -## Existential Capabilities - -In fact, what is written as the top type `cap` can mean different capabilities, depending on scope. For instance, consider the function type -`() -> Iterator[T]^`. This is taken to mean -```scala - () -> Exists x. Iterator[T]^x -``` -In other words, it means an unknown type bound `x` by an "existential" in the scope of the function result. A `cap` in a function result is therefore different from a `cap` at the top-level or in a function parameter. - -Internally, an existential type is represented as a kind of dependent function type. The type above would be modelled as -```scala - () -> (x: Exists) -> Iterator[T]^x -``` -Here, `Exists` is a sealed trait in the `caps` object that serves to mark -dependent functions as representations of existentials. It should be noted -that this is strictly an internal representation. It is explained here because it can show up in error messages. It is generally not recommended to use this syntax in source code. Instead one should rely on the automatic expansion of `^` and `cap` to existentials, which can be -influenced by introducing the right alias types. The rules for this expansion are as follows: - - - If a function result type contains covariant occurrences of `cap`, - we replace these occurrences with a fresh existential variable which - is bound by a quantifier scoping over the result type. - - We might want to do the same expansion in function arguments, but right now this is not done. - - Occurrences of `cap` elsewhere are not translated. They can be seen as representing an existential at the top-level scope. - -**Examples:** - - - `A => B` is an alias type that expands to `(A -> B)^`, therefore - `() -> A => B` expands to `() -> Exists c. A ->{c} B`. - - - `() -> Iterator[A => B]` expands to `() -> Exists c. Iterator[A ->{c} B]` - - - `A -> B^` expands to `A -> Exists c.B^{c}`. - - - If we define `type Fun[T] = A -> T`, then `() -> Fun[B^]` expands to `() -> Exists c.Fun[B^{c}]`, which dealiases to `() -> Exists c.A -> B^{c}`. This demonstrates how aliases can be used to force existential binders to be in some specific outer scope. - - - If we define - ```scala - type F = A -> Fun[B^] - ``` - then the type alias expands to - ```scala - type F = A -> Exists c.A -> B^{c} - ``` - -**Typing Rules:** - - - When we typecheck the body of a function or method, any covariant occurrences of `cap` in the result type are bound with a fresh existential. - - Conversely, when we typecheck the application of a function or method, - with an existential result type `Exists ex.T`, the result of the application is `T` where every occurrence of the existentially bound - variable `ex` is replaced by `cap`. - -## Reach Capabilities - -Say you have a method `f` that takes an impure function argument which gets stored in a `var`: -```scala -def f(op: A => B) - var x: A ->{op} B = op - ... -``` -This is legal even though `var`s cannot have types with `cap` or existential capabilities. The trick is that the type of the variable `x` -is not `A => B` (this would be rejected), but is the "narrowed" type -`A ->{op} B`. In other words, all capabilities retained by values of `x` -are all also referred to by `op`, which justifies the replacement of `cap` by `op`. - -A more complicated situation is if we want to store successive values -held in a list. Example: -```scala -def f(ops: List[A => B]) - var xs = ops - var x: ??? = xs.head - while xs.nonEmpty do - xs = xs.tail - x = xs.head - ... -``` -Here, `x` cannot be given a type with an `ops` capability. In fact, `ops` is pure, i.e. it's capture set is empty, so it cannot be used as the name of a capability. What we would like to express is that `x` refers to -any operation "reachable" through `ops`. This can be expressed using a -_reach capability_ `ops*`. -```scala -def f(ops: List[A => B]) - var xs = ops - var x: A ->{ops*} B = xs.head - ... -``` -Reach capabilities take the form `x*` where `x` is syntactically a regular capability. If `x: T` then `x*` stands for any capability that appears covariantly in `T` and that is accessed through `x`. The least supertype of this capability is the set of all capabilities appearing covariantly in `T`. - -## Capability Polymorphism - -It is sometimes convenient to write operations that are parameterized with a capture set of capabilities. For instance consider a type of event sources -`Source` on which `Listener`s can be registered. Listeners can hold certain capabilities, which show up as a parameter to `Source`: -```scala -class Source[X^]: - private var listeners: Set[Listener^{X}] = Set.empty - def register(x: Listener^{X}): Unit = - listeners += x - - def allListeners: Set[Listener^{X}] = listeners -``` -The type variable `X^` can be instantiated with a set of capabilities. It can occur in capture sets in its scope. For instance, in the example above -we see a variable `listeners` that has as type a `Set` of `Listeners` capturing `X`. The `register` method takes a listener of this type -and assigns it to the variable. - -Capture-set variables `X^` without user-annotated bounds by default range over the interval `>: {} <: {caps.cap}` which is the universe of capture sets instead of regular types. - -Under the hood, such capture-set variables are represented as regular type variables within the special interval - `>: CapSet <: CapSet^`. -For instance, `Source` from above could be equivalently -defined as follows: -```scala -class Source[X >: CapSet <: CapSet^]: - ... -``` -`CapSet` is a sealed trait in the `caps` object. It cannot be instantiated or inherited, so its only -purpose is to identify type variables which are capture sets. In non-capture-checked -usage contexts, the type system will treat `CapSet^{a}` and `CapSet^{a,b}` as the type `CapSet`, whereas -with capture checking enabled, it will take the annotated capture sets into account, -so that `CapSet^{a}` and `CapSet^{a,b}` are distinct. -This representation based on `CapSet` is subject to change and -its direct use is discouraged. - -Capture-set variables can be inferred like regular type variables. When they should be instantiated -explicitly one supplies a concrete capture set. For instance: -```scala -class Async extends caps.Capability - -def listener(async: Async): Listener^{async} = ??? - -def test1(async1: Async, others: List[Async]) = - val src = Source[{async1, others*}] - ... -``` -Here, `src` is created as a `Source` on which listeners can be registered that refer to the `async` capability or to any of the capabilities in list `others`. So we can continue the example code above as follows: -```scala - src.register(listener(async1)) - others.map(listener).foreach(src.register) - val ls: Set[Listener^{async, others*}] = src.allListeners -``` -A common use-case for explicit capture parameters is describing changes to the captures of mutable fields, such as concatenating -effectful iterators: -```scala -class ConcatIterator[A, C^](var iterators: mutable.List[IterableOnce[A]^{C}]): - def concat(it: IterableOnce[A]^): ConcatIterator[A, {C, it}]^{this, it} = - iterators ++= it // ^ - this // track contents of `it` in the result -``` -In such a scenario, we also should ensure that any pre-existing alias of a `ConcatIterator` object should become -inaccessible after invoking its `concat` method. This is achieved with mutation and separation tracking which are -currently in development. - - -## Capability Members - -Just as parametrization by types can be equally expressed with type members, we could -also define the `Source[X^]` class above could using a _capability member_: -```scala -class Source: - type X^ - private var listeners: Set[Listener^{this.X}] = Set.empty - ... // as before -``` -Here, we can refer to capability members using paths in capture sets (such as `{this.X}`). Similarly to type members, -capability members can be upper- and lower-bounded with capture sets: -```scala -trait Thread: - type Cap^ - def run(block: () ->{this.Cap} -> Unit): Unit - -trait GPUThread extends Thread: - type Cap^ >: {cudaMalloc, cudaFree} <: {caps.cap} -``` -Since `caps.cap` is the top element for subcapturing, we could have also left out the -upper bound: `type Cap^ >: {cudaMalloc, cudaFree}`. - - -[More Advanced Use Cases](cc-advanced.md) - -## Compilation Options - -The following options are relevant for capture checking. - - - **-Vprint:cc** Prints the program with capturing types as inferred by capture checking. - - **-Ycc-debug** Gives more detailed, implementation-oriented information about capture checking, as described in the next section. - - The implementation supporting capture checking with these options is currently in branch `cc-experiment` on dotty.epfl.ch. - -## Capture Checking Internals - -The capture checker is architected as a propagation constraint solver, which runs as a separate phase after type-checking and some initial transformations. - -Constraint variables stand for unknown capture sets. A constraint variable is introduced - - - for every part of a previously inferred type, - - for the accessed references of every method, class, anonymous function, or by-name argument, - - for the parameters passed in a class constructor call. - -Capture sets in explicitly written types are treated as constants (before capture checking, such sets are simply ignored). - -The capture checker essentially rechecks the program with the usual typing rules. Every time a subtype requirement between capturing types is checked, this translates to a subcapturing test on capture sets. If the two sets are constant, this is simply a yes/no question, where a no will produce an error message. - -If the lower set `C₁` of a comparison `C₁ <: C₂` is a variable, the set `C₂` is recorded -as a _superset_ of `C₁`. If the upper set `C₂` is a variable, the elements of `C₁` are _propagated_ to `C₂`. Propagation of an element `x` to a set `C` means that `x` is included as an element in `C`, and it is also propagated -to all known supersets of `C`. If such a superset is a constant, it is checked that `x` is included in it. If that's not the case, the original comparison `C₁ <: C₂` has no solution and an error is reported. - -The type checker also performs various maps on types, for instance when substituting actual argument types for formal parameter types in dependent functions, or mapping -member types with "as-seen-from" in a selection. Maps keep track of the variance -of positions in a type. The variance is initially covariant, it flips to -contravariant in function parameter positions, and can be either covariant, -contravariant, or nonvariant in type arguments, depending on the variance of -the type parameter. - -When capture checking, the same maps are also performed on capture sets. If a capture set is a constant, its elements (which are capabilities) are mapped as regular types. If the result of such a map is not a capability, the result is approximated according to the variance of the type. A covariant approximation replaces a type by its capture set. -A contravariant approximation replaces it with the empty capture set. A nonvariant -approximation replaces the enclosing capturing type with a range of possible types -that gets propagated and resolved further out. - -When a mapping `m` is performed on a capture set variable `C`, a new variable `Cm` is created that contains the mapped elements and that is linked with `C`. If `C` subsequently acquires further elements through propagation, these are also propagated to `Cm` after being transformed by the `m` mapping. `Cm` also gets the same supersets as `C`, mapped again using `m`. - -One interesting aspect of the capture checker concerns the implementation of capture tunnelling. The [foundational theory](https://infoscience.epfl.ch/record/290885) on which capture checking is based makes tunnelling explicit through so-called _box_ and -_unbox_ operations. Boxing hides a capture set and unboxing recovers it. The capture checker inserts virtual box and unbox operations based on actual and expected types similar to the way the type checker inserts implicit conversions. When capture set variables are first introduced, any capture set in a capturing type that is an instance of a type parameter instance is marked as "boxed". A boxing operation is -inserted if the expected type of an expression is a capturing type with -a boxed capture set variable. The effect of the insertion is that any references -to capabilities in the boxed expression are forgotten, which means that capture -propagation is stopped. Dually, if the actual type of an expression has -a boxed variable as capture set, an unbox operation is inserted, which adds all -elements of the capture set to the environment. - -Boxing and unboxing has no runtime effect, so the insertion of these operations is only simulated; the only visible effect is the retraction and insertion -of variables in the capture sets representing the environment of the currently checked expression. - -The `-Ycc-debug` option provides some insight into the workings of the capture checker. -When it is turned on, boxed sets are marked explicitly and capture set variables are printed with an ID and some information about their provenance. For instance, the string `{f, xs}33M5V` indicates a capture set -variable that is known to hold elements `f` and `xs`. The variable's ID is `33`. The `M` -indicates that the variable was created through a mapping from a variable with ID `5`. The latter is a regular variable, as indicated - by `V`. - -Generally, the string following the capture set consists of alternating numbers and letters where each number gives a variable ID and each letter gives the provenance of the variable. Possible letters are - - - `V` : a regular variable, - - `M` : a variable resulting from a _mapping_ of the variable indicated by the string to the right, - - `B` : similar to `M` but where the mapping is a _bijection_, - - `F` : a variable resulting from _filtering_ the elements of the variable indicated by the string to the right, - - `I` : a variable resulting from an _intersection_ of two capture sets, - - `D` : a variable resulting from the set _difference_ of two capture sets. - - `R` : a regular variable that _refines_ a class parameter, so that the capture - set of a constructor argument is known in the class instance type. - -At the end of a compilation run, `-Ycc-debug` will print all variable dependencies of variables referred to in previous output. Here is an example: -``` -Capture set dependencies: - {}2V :: - {}3V :: - {}4V :: - {f, xs}5V :: {f, xs}31M5V, {f, xs}32M5V - {f, xs}31M5V :: {xs, f} - {f, xs}32M5V :: -``` -This section lists all variables that appeared in previous diagnostics and their dependencies, recursively. For instance, we learn that - - - variables 2, 3, 4 are empty and have no dependencies, - - variable `5` has two dependencies: variables `31` and `32` which both result from mapping variable `5`, - - variable `31` has a constant fixed superset `{xs, f}` - - variable `32` has no dependencies. - - - diff --git a/docs/_docs/reference/experimental/overview.md b/docs/_docs/reference/experimental/overview.md index f70cf32b9c24..9242056d8405 100644 --- a/docs/_docs/reference/experimental/overview.md +++ b/docs/_docs/reference/experimental/overview.md @@ -32,4 +32,4 @@ Hence, dependent projects also have to be experimental. Some experimental language features that are still in research and development can be enabled with special compiler options. These include * [`-Yexplicit-nulls`](./explicit-nulls.md). Enable support for tracking null references in the type system. -* [`-Ycc`](./cc.md). Enable support for capture checking. +* [`-Ycc`](./capture-checking/cc.md). Enable support for capture checking. diff --git a/docs/sidebar.yml b/docs/sidebar.yml index 440cfa450849..06e811ca62b8 100644 --- a/docs/sidebar.yml +++ b/docs/sidebar.yml @@ -162,9 +162,19 @@ subsection: - page: reference/experimental/explicit-nulls.md - page: reference/experimental/main-annotation.md - page: reference/experimental/into.md - - page: reference/experimental/cc.md - - page: reference/experimental/cc-advanced.md - hidden: true + - title: Capture Checking + index: reference/experimental/capture-checking/cc.md + subsection: + - page: reference/experimental/capture-checking/classes.md + - page: reference/experimental/capture-checking/polymorphism.md + - page: reference/experimental/capture-checking/advanced.md + hidden: true + - page: reference/experimental/capture-checking/scoped-caps.md + - page: reference/experimental/capture-checking/classifiers.md + - page: reference/experimental/capture-checking/checked-exceptions.md + - page: reference/experimental/capture-checking/separation-checking.md + - page: reference/experimental/capture-checking/how-to-use.md + - page: reference/experimental/capture-checking/internals.md - page: reference/experimental/purefuns.md - page: reference/experimental/tupled-function.md - page: reference/experimental/modularity.md diff --git a/language-server/test/dotty/tools/languageserver/CompletionTest.scala b/language-server/test/dotty/tools/languageserver/CompletionTest.scala index 528aa1055c6f..f796ba0e0646 100644 --- a/language-server/test/dotty/tools/languageserver/CompletionTest.scala +++ b/language-server/test/dotty/tools/languageserver/CompletionTest.scala @@ -27,7 +27,7 @@ class CompletionTest { @Test def completionFromNewScalaPredef: Unit = { code"class Foo { val foo = summ${m1} }" - .completion(("summon", Method, "[T](using x: T): x.type")) + .completion(("summon", Method, "[T](using x: T): (x : T)")) } @Test def completionFromScalaPackage: Unit = { diff --git a/tests/neg-custom-args/captures/box-adapt-cases.check b/tests/neg-custom-args/captures/box-adapt-cases.check index 5cbceb1d6c64..0e403308ec2f 100644 --- a/tests/neg-custom-args/captures/box-adapt-cases.check +++ b/tests/neg-custom-args/captures/box-adapt-cases.check @@ -3,14 +3,14 @@ | ^^^^^^^^^^^^^^^^ | Found: (cap: Cap^{io}) ->{io} Int | Required: Cap^{io} -> Int - | Note that capability (io : Cap^) is not included in capture set {}. + | Note that capability io is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/box-adapt-cases.scala:29:10 ------------------------------ 29 | x.value(cap => cap.use()) // error | ^^^^^^^^^^^^^^^^ - | Found: (cap: Cap^?) ->{io, fs} Int + | Found: (cap: Cap^'s1) ->{io, fs} Int | Required: Cap^{io, fs} ->{io} Int - | Note that capability (fs : Cap^) is not included in capture set {io}. + | Note that capability fs is not included in capture set {io}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/byname.check b/tests/neg-custom-args/captures/byname.check index 152900a5b29a..7fbeb6f2ddbe 100644 --- a/tests/neg-custom-args/captures/byname.check +++ b/tests/neg-custom-args/captures/byname.check @@ -12,22 +12,22 @@ | |where: ?=> refers to a fresh root capability created in method test when checking argument to parameter ff of method h | - |Note that capability (cap1 : Cap) is not included in capture set {cap2}. + |Note that capability cap1 is not included in capture set {cap2}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/byname.scala:19:5 ---------------------------------------- 19 | h(g()) // error | ^^^ - | Found: () ?->{cap2} I^? + | Found: () ?->{cap2} I^'s1 | Required: () ?->{cap1} I - | Note that capability (cap2 : Cap) is not included in capture set {cap1}. + | Note that capability cap2 is not included in capture set {cap1}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/byname.scala:22:5 ---------------------------------------- 22 | h2(() => g())() // error | ^^^^^^^^^ - | Found: () ->{cap2} I^? + | Found: () ->{cap2} I^'s2 | Required: () ->{cap1} I - | Note that capability (cap2 : Cap) is not included in capture set {cap1}. + | Note that capability cap2 is not included in capture set {cap1}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/capt-depfun.check b/tests/neg-custom-args/captures/capt-depfun.check index ee80bb335d61..fe60eea0b886 100644 --- a/tests/neg-custom-args/captures/capt-depfun.check +++ b/tests/neg-custom-args/captures/capt-depfun.check @@ -6,6 +6,6 @@ | | where: => refers to a fresh root capability in the type of value dc | - | Note that capability (y : C^) is not included in capture set {}. + | Note that capability y is not included in capture set {}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/capt1.check b/tests/neg-custom-args/captures/capt1.check index 0cd908d081ee..9d2ae82d814c 100644 --- a/tests/neg-custom-args/captures/capt1.check +++ b/tests/neg-custom-args/captures/capt1.check @@ -3,15 +3,15 @@ | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ | Found: () ->{x} C | Required: () -> C - | Note that capability (x : C^) is not included in capture set {}. + | Note that capability x is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:8:2 ------------------------------------------ 8 | () => if x == null then y else y // error | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - | Found: () ->{x} C^? + | Found: () ->{x} C^'s1 | Required: Matchable - | Note that capability (x : C^) is not included in capture set {}. + | Note that capability x is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:15:2 ----------------------------------------- @@ -19,7 +19,7 @@ | ^ | Found: (y: Int) ->{x} Int | Required: Matchable - | Note that capability (x : C^) is not included in capture set {}. + | Note that capability x is not included in capture set {}. 16 | f | | longer explanation available when compiling with `-explain` @@ -28,7 +28,7 @@ | ^ | Found: A^{x} | Required: A - | Note that capability (x : C^) is not included in capture set {}. + | Note that capability x is not included in capture set {}. 23 | def m() = if x == null then y else y 24 | F(22) | @@ -38,7 +38,7 @@ | ^ | Found: A^{x} | Required: A - | Note that capability (x : C^) is not included in capture set {}. + | Note that capability x is not included in capture set {}. 28 | def m() = if x == null then y else y | | longer explanation available when compiling with `-explain` @@ -52,7 +52,7 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:36:24 ---------------------------------------- 36 | val z2 = h[() -> Cap](() => x) // error // error | ^^^^^^^ - |Found: () ->? C^ + |Found: () ->'s2 C^ |Required: () -> C^² | |where: ^ refers to a root capability associated with the result type of (): C^ @@ -65,7 +65,7 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:37:5 ----------------------------------------- 37 | (() => C()) // error | ^^^^^^^^^ - |Found: () ->? C^ + |Found: () ->'s3 C^ |Required: () -> C^² | |where: ^ refers to a root capability associated with the result type of (): C^ diff --git a/tests/neg-custom-args/captures/cc-glb.check b/tests/neg-custom-args/captures/cc-glb.check index 1d978f834175..eff591ea6ea1 100644 --- a/tests/neg-custom-args/captures/cc-glb.check +++ b/tests/neg-custom-args/captures/cc-glb.check @@ -3,6 +3,6 @@ | ^^ | Found: (x1 : (Foo[T] & Foo[Any])^{io}) | Required: Foo[T] - | Note that capability (io : Cap^) is not included in capture set {}. + | Note that capability io is not included in capture set {}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/cc-poly-2.check b/tests/neg-custom-args/captures/cc-poly-2.check index 0577b4f9d22b..863a3fa98539 100644 --- a/tests/neg-custom-args/captures/cc-poly-2.check +++ b/tests/neg-custom-args/captures/cc-poly-2.check @@ -14,6 +14,6 @@ | ^ | Found: (x : Test.D^{d}) | Required: Test.D^{c1} - | Note that capability (d : Test.D^) is not included in capture set {c1}. + | Note that capability d is not included in capture set {c1}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/cc-this.check b/tests/neg-custom-args/captures/cc-this.check index 85040bbaa0b3..672d8f57d3d2 100644 --- a/tests/neg-custom-args/captures/cc-this.check +++ b/tests/neg-custom-args/captures/cc-this.check @@ -3,7 +3,7 @@ | ^^^^ | Found: (C.this : C^{C.this.x}) | Required: C - | Note that capability (C.this.x : () => Int) is not included in capture set {}. + | Note that capability C.this.x is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/cc-this.scala:12:15 ----------------------------------------------------------- diff --git a/tests/neg-custom-args/captures/cc-this5.check b/tests/neg-custom-args/captures/cc-this5.check index 253ef3985af9..4ff9452a0956 100644 --- a/tests/neg-custom-args/captures/cc-this5.check +++ b/tests/neg-custom-args/captures/cc-this5.check @@ -8,7 +8,7 @@ | ^^^^ | Found: (A.this : A^{c}) | Required: A - | Note that capability (c : Cap) is not included in capture set {}. + | Note that capability c is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E058] Type Mismatch Error: tests/neg-custom-args/captures/cc-this5.scala:7:9 --------------------------------------- diff --git a/tests/neg-custom-args/captures/class-contra.check b/tests/neg-custom-args/captures/class-contra.check index 1c2b7f8e2157..f5ac2ebb219f 100644 --- a/tests/neg-custom-args/captures/class-contra.check +++ b/tests/neg-custom-args/captures/class-contra.check @@ -3,6 +3,6 @@ | ^ | Found: (a : T^{x, y}) | Required: T^{k.f} - | Note that capability (x : C^) is not included in capture set {k.f}. + | Note that capability x is not included in capture set {k.f}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/class-level-attack.check b/tests/neg-custom-args/captures/class-level-attack.check index 9c22c305b1bd..e005dca26b29 100644 --- a/tests/neg-custom-args/captures/class-level-attack.check +++ b/tests/neg-custom-args/captures/class-level-attack.check @@ -13,7 +13,7 @@ | | where: ^ refers to a fresh root capability in the type of value r | - | Note that capability (x : IO^) is not included in capture set {cap} + | Note that capability x is not included in capture set {cap} | because (x : IO^) in method set is not visible from cap in value r. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/contracap.check b/tests/neg-custom-args/captures/contracap.check index 65af3d27cf1d..a18fb11d4883 100644 --- a/tests/neg-custom-args/captures/contracap.check +++ b/tests/neg-custom-args/captures/contracap.check @@ -1,11 +1,11 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/contracap.scala:15:48 ------------------------------------ 15 | val g: (Ref[Int]^{a}, Ref[Int]^{a}) -> Unit = f // error | ^ - | Found: (f : (Ref[Int]^, Ref[Int]^) -> Unit) - | Required: (Ref[Int]^{a}, Ref[Int]^{a}) -> Unit + | Found: (f : (Ref[Int]^, Ref[Int]^) -> Unit) + | Required: (Ref[Int]^{a}, Ref[Int]^{a}) -> Unit | - | where: ^ refers to the universal root capability + | where: ^ refers to the universal root capability | - | Note that capability (a : Ref[Int]^) is not included in capture set {cap}. + | Note that capability a is not included in capture set {cap}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/depfun-reach.check b/tests/neg-custom-args/captures/depfun-reach.check index 446ba4151c9a..310ca9abc2c2 100644 --- a/tests/neg-custom-args/captures/depfun-reach.check +++ b/tests/neg-custom-args/captures/depfun-reach.check @@ -1,7 +1,7 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/depfun-reach.scala:12:27 --------------------------------- 12 | List(() => op.foreach((f,g) => { f(); g() })) // error (???) | ^^^^^^^^^^^^^^^^^^^^ - |Found: (x$1: (() ->? Unit, () ->? Unit)^?) ->? Unit + |Found: (x$1: (() ->'s1 Unit, () ->'s2 Unit)^'s3) ->'s4 Unit |Required: ((() ->{op*} Unit, () ->{op*} Unit)) => Unit | |where: => refers to a fresh root capability created in anonymous function of type (): Unit when checking argument to parameter op of method foreach diff --git a/tests/neg-custom-args/captures/effect-swaps-explicit.check b/tests/neg-custom-args/captures/effect-swaps-explicit.check index 4b38fb01d207..cd2efbc233c6 100644 --- a/tests/neg-custom-args/captures/effect-swaps-explicit.check +++ b/tests/neg-custom-args/captures/effect-swaps-explicit.check @@ -2,9 +2,9 @@ 63 | Result: 64 | Future: // error, type mismatch | ^ - | Found: Result.Ok[Future[T^?]^{fr, contextual$1}] + | Found: Result.Ok[Future[T^'s1]^{fr, contextual$1}] | Required: Result[Future[T], Nothing] - | Note that capability (fr : Future[Result[T, E]]^) is not included in capture set {}. + | Note that capability fr is not included in capture set {}. 65 | fr.await.ok |-------------------------------------------------------------------------------------------------------------------- |Inline stack trace @@ -18,27 +18,26 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps-explicit.scala:69:10 ------------------------ 69 | Future: fut ?=> // error, type mismatch | ^ - |Found: (contextual$9: boundary.Label[Result[Future[T^?]^?, E^?]^?]^?) ?->{fr, async} Future[T^?]^{fr, contextual$9} - |Required: (boundary.Label[Result[Future[T^?]^?, E^?]]^) ?=> Future[T^?]^? + |Found: (contextual$9: boundary.Label[Result[Future[T^'s2]^'s3, E^'s4]^'s5]^'s6) ?->{fr, async} Future[T^'s7]^{fr, contextual$9} + |Required: (boundary.Label[Result[Future[T^'s8]^'s9, E^'s10]]^) ?=> Future[T^'s8]^'s9 | |where: ?=> refers to a fresh root capability created in method fail4 when checking argument to parameter body of method make | ^ refers to the universal root capability | - |Note that capability contextual$9.type - |cannot be included in outer capture set ?. + |Note that capability contextual$9 cannot be included in outer capture set 's9. 70 | fr.await.ok | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps-explicit.scala:73:35 ------------------------ 73 | Result.make[Future[T], E]: lbl ?=> // error: type mismatch | ^ - |Found: (lbl: boundary.Label[Result[Future[T^?]^?, E^?]^?]^?) ?->{fr, async} Future[T^?]^{fr, lbl} + |Found: (lbl: boundary.Label[Result[Future[T^'s11]^'s12, E^'s13]^'s14]^'s15) ?->{fr, async} Future[T^'s16]^{fr, lbl} |Required: (boundary.Label[Result[Future[T], E]]^) ?=> Future[T] | |where: ?=> refers to a fresh root capability created in method fail5 when checking argument to parameter body of method make | ^ refers to the universal root capability | - |Note that capability (fr : Future[Result[T, E]]^) is not included in capture set {}. + |Note that capability fr is not included in capture set {}. 74 | Future: fut ?=> 75 | fr.await.ok | diff --git a/tests/neg-custom-args/captures/effect-swaps.check b/tests/neg-custom-args/captures/effect-swaps.check index 25b3247ea161..b9bcfdfa667d 100644 --- a/tests/neg-custom-args/captures/effect-swaps.check +++ b/tests/neg-custom-args/captures/effect-swaps.check @@ -2,9 +2,9 @@ 63 | Result: 64 | Future: // error, type mismatch | ^ - | Found: Result.Ok[Future[T^?]^{fr, contextual$1}] + | Found: Result.Ok[Future[T^'s1]^{fr, contextual$1}] | Required: Result[Future[T], Nothing] - | Note that capability (fr : Future[Result[T, E]]^) is not included in capture set {}. + | Note that capability fr is not included in capture set {}. 65 | fr.await.ok |-------------------------------------------------------------------------------------------------------------------- |Inline stack trace @@ -18,27 +18,26 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps.scala:69:10 --------------------------------- 69 | Future: fut ?=> // error, type mismatch | ^ - |Found: (contextual$9: boundary.Label[Result[Future[T^?]^?, E^?]^?]^?) ?->{fr, async} Future[T^?]^{fr, contextual$9} - |Required: (boundary.Label[Result[Future[T^?]^?, E^?]]^) ?=> Future[T^?]^? + |Found: (contextual$9: boundary.Label[Result[Future[T^'s2]^'s3, E^'s4]^'s5]^'s6) ?->{fr, async} Future[T^'s7]^{fr, contextual$9} + |Required: (boundary.Label[Result[Future[T^'s8]^'s9, E^'s10]]^) ?=> Future[T^'s8]^'s9 | |where: ?=> refers to a fresh root capability created in method fail4 when checking argument to parameter body of method make | ^ refers to the universal root capability | - |Note that capability contextual$9.type - |cannot be included in outer capture set ?. + |Note that capability contextual$9 cannot be included in outer capture set 's9. 70 | fr.await.ok | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps.scala:73:35 --------------------------------- 73 | Result.make[Future[T], E]: lbl ?=> // error: type mismatch | ^ - |Found: (lbl: boundary.Label[Result[Future[T^?]^?, E^?]^?]^?) ?->{fr, async} Future[T^?]^{fr, lbl} + |Found: (lbl: boundary.Label[Result[Future[T^'s11]^'s12, E^'s13]^'s14]^'s15) ?->{fr, async} Future[T^'s16]^{fr, lbl} |Required: (boundary.Label[Result[Future[T], E]]^) ?=> Future[T] | |where: ?=> refers to a fresh root capability created in method fail5 when checking argument to parameter body of method make | ^ refers to the universal root capability | - |Note that capability (fr : Future[Result[T, E]]^) is not included in capture set {}. + |Note that capability fr is not included in capture set {}. 74 | Future: fut ?=> 75 | fr.await.ok | diff --git a/tests/neg-custom-args/captures/eta.check b/tests/neg-custom-args/captures/eta.check index c0123ec59ae4..bc11637022b0 100644 --- a/tests/neg-custom-args/captures/eta.check +++ b/tests/neg-custom-args/captures/eta.check @@ -3,6 +3,6 @@ | ^ | Found: (g : () -> A) | Required: () -> Proc^{f} - | Note that capability (f : Proc^) is not included in capture set {}. + | Note that capability f is not included in capture set {}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/filevar.check b/tests/neg-custom-args/captures/filevar.check index 84101f64b963..81a41fe3c257 100644 --- a/tests/neg-custom-args/captures/filevar.check +++ b/tests/neg-custom-args/captures/filevar.check @@ -1,13 +1,12 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/filevar.scala:15:12 -------------------------------------- 15 | withFile: f => // error with level checking, was OK under both schemes before | ^ - |Found: (f: File^?) ->? Unit + |Found: (f: File^'s1) ->'s2 Unit |Required: (f: File^{l}) => Unit | |where: => refers to a fresh root capability created in anonymous function of type (using l²: scala.caps.Capability): File^{l²} -> Unit when instantiating expected result type (f: File^{l}) ->{cap} Unit of function literal | - |Note that capability l.type - |cannot be included in outer capture set ? of parameter f. + |Note that capability l cannot be included in outer capture set 's1 of parameter f. 16 | val o = Service() 17 | o.file = f 18 | o.log @@ -16,4 +15,4 @@ -- 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.type + | redundant capture: File already accounts for (l : scala.caps.Capability) diff --git a/tests/neg-custom-args/captures/heal-tparam-cs.check b/tests/neg-custom-args/captures/heal-tparam-cs.check index 8a149664ffe7..2d5ee98059f3 100644 --- a/tests/neg-custom-args/captures/heal-tparam-cs.check +++ b/tests/neg-custom-args/captures/heal-tparam-cs.check @@ -1,14 +1,13 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/heal-tparam-cs.scala:10:23 ------------------------------- 10 | val test1 = localCap { c => // error | ^ - |Found: (c: Capp^?) ->? () ->{c} Unit - |Required: (c: Capp^) => () ->? Unit + |Found: (c: Capp^'s1) ->'s2 () ->{c} Unit + |Required: (c: Capp^) => () ->'s3 Unit | |where: => refers to a fresh root capability created in value test1 when checking argument to parameter op of method localCap | ^ refers to the universal root capability | - |Note that capability c.type - |cannot be included in outer capture set ?. + |Note that capability c cannot be included in outer capture set 's3. 11 | () => { c.use() } 12 | } | @@ -16,13 +15,13 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/heal-tparam-cs.scala:15:13 ------------------------------- 15 | localCap { c => // error | ^ - | Found: (x$0: Capp^?) ->? () ->{x$0} Unit + | Found: (x$0: Capp^'s4) ->'s5 () ->{x$0} Unit | Required: (c: Capp^) -> () => Unit | | where: => refers to a root capability associated with the result type of (c: Capp^): () => Unit | ^ refers to the universal root capability | - | Note that capability x$0.type is not included in capture set {{x$0} Unit>}. + | Note that capability x$0 is not included in capture set {{x$0} Unit>}. 16 | (c1: Capp^) => () => { c1.use() } 17 | } | @@ -30,9 +29,9 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/heal-tparam-cs.scala:25:13 ------------------------------- 25 | localCap { c => // error | ^ - | Found: (x$0: Capp^?) ->? () ->{x$0} Unit + | Found: (x$0: Capp^'s6) ->'s7 () ->{x$0} Unit | Required: (c: Capp^{io}) -> () ->{net} Unit - | Note that capability x$0.type is not included in capture set {net}. + | Note that capability x$0 is not included in capture set {net}. 26 | (c1: Capp^{io}) => () => { c1.use() } 27 | } | @@ -42,7 +41,7 @@ | ^^^^^^^^^^^^^^ | Found: () ->{io} Unit | Required: () -> Unit - | Note that capability (io : Capp^) is not included in capture set {}. + | Note that capability io is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/heal-tparam-cs.scala:44:10 ------------------------------- @@ -50,6 +49,6 @@ | ^^^^^^^^^^^^^^ | Found: () ->{io} Unit | Required: () -> Unit - | Note that capability (io : Capp^) is not included in capture set {}. + | Note that capability io is not included in capture set {}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/i15772.check b/tests/neg-custom-args/captures/i15772.check index 4fbd86815112..d285e2715aa7 100644 --- a/tests/neg-custom-args/captures/i15772.check +++ b/tests/neg-custom-args/captures/i15772.check @@ -37,7 +37,7 @@ | ^ | Found: (x : () ->{filesList, sayHello} Unit) | Required: () -> Unit - | Note that capability (filesList : List[File]^{io}) is not included in capture set {}. + | Note that capability filesList is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/i15772.scala:34:10 ------------------------------------------------------------ diff --git a/tests/neg-custom-args/captures/i15923.check b/tests/neg-custom-args/captures/i15923.check index 70d8acffd227..1adeeb60edb8 100644 --- a/tests/neg-custom-args/captures/i15923.check +++ b/tests/neg-custom-args/captures/i15923.check @@ -1,34 +1,32 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15923.scala:27:23 --------------------------------------- 27 | val leak = withCap(cap => mkId(cap)) // error (was: no error here since type aliases don't box) | ^^^^^^^^^^^^^^^^ - |Found: (cap: test2.Cap^?) ->? [T] => (op: test2.Cap^? ->? T) ->? T - |Required: test2.Cap^{lcap} => [T] => (op²: test2.Cap^? ->? T) ->? T + |Found: (cap: test2.Cap^'s1) ->'s2 [T] => (op: test2.Cap^'s3 ->'s4 T) ->'s5 T + |Required: test2.Cap^{lcap} => [T] => (op²: test2.Cap^'s6 ->'s7 T) ->'s8 T | - |where: => refers to a fresh root capability created in anonymous function of type (using lcap²: scala.caps.Capability): test2.Cap^{lcap²} -> [T] => (op³: test2.Cap^{lcap²} => T) -> T when instantiating expected result type test2.Cap^{lcap} ->{cap²} [T] => (op²: test2.Cap^? ->? T) ->? T of function literal + |where: => refers to a fresh root capability created in anonymous function of type (using lcap²: scala.caps.Capability): test2.Cap^{lcap²} -> [T] => (op³: test2.Cap^{lcap²} => T) -> T when instantiating expected result type test2.Cap^{lcap} ->{cap²} [T] => (op²: test2.Cap^'s6 ->'s7 T) ->'s8 T of function literal | op is a reference to a value parameter | op² is a reference to a value parameter | - |Note that capability lcap.type - |cannot be included in outer capture set ? of parameter cap. + |Note that capability lcap cannot be included in outer capture set 's1 of parameter cap. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15923.scala:12:21 --------------------------------------- 12 | val leak = withCap(cap => mkId(cap)) // error | ^^^^^^^^^^^^^^^^ - |Found: (cap: Cap^?) ->? Id[Cap^?]^? - |Required: Cap^{lcap} => Id[Cap^?]^? + |Found: (cap: Cap^'s9) ->'s10 Id[Cap^'s11]^'s12 + |Required: Cap^{lcap} => Id[Cap^'s13]^'s14 | - |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^?]^? of function literal + |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 | - |Note that capability lcap.type - |cannot be included in outer capture set ? of parameter cap. + |Note that capability lcap cannot be included in outer capture set 's9 of parameter cap. | | 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.type + | 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.type + | redundant capture: Cap already accounts for (lcap : scala.caps.Capability) diff --git a/tests/neg-custom-args/captures/i15923a.check b/tests/neg-custom-args/captures/i15923a.check index 6d2156d89a97..0971b025f653 100644 --- a/tests/neg-custom-args/captures/i15923a.check +++ b/tests/neg-custom-args/captures/i15923a.check @@ -1,14 +1,13 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15923a.scala:7:21 --------------------------------------- 7 | val leak = withCap(lcap => () => mkId(lcap)) // error | ^^^^^^^^^^^^^^^^^^^^^^^^ - |Found: (lcap: Cap^?) ->? () ->? Id[Cap^?]^? - |Required: (lcap: Cap^) => () =>² Id[Cap^?]^? + |Found: (lcap: Cap^'s1) ->'s2 () ->'s3 Id[Cap^'s4]^'s5 + |Required: (lcap: Cap^) => () =>² Id[Cap^'s6]^'s7 | |where: => refers to a fresh root capability created in value leak when checking argument to parameter op of method withCap - | =>² refers to a root capability associated with the result type of (lcap: Cap^): () =>² Id[Cap^?]^? + | =>² refers to a root capability associated with the result type of (lcap: Cap^): () =>² Id[Cap^'s6]^'s7 | ^ refers to the universal root capability | - |Note that capability - |cannot be included in outer capture set ?. + |Note that capability cannot be included in outer capture set 's6. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/i15923b.check b/tests/neg-custom-args/captures/i15923b.check index 80e1b3f8b4ba..cba83424a4ca 100644 --- a/tests/neg-custom-args/captures/i15923b.check +++ b/tests/neg-custom-args/captures/i15923b.check @@ -2,12 +2,11 @@ 8 | val leak = withCap(f) // error | ^ |Found: (x$0: Cap^) -> Id[Cap^{x$0}] - |Required: (lcap: Cap^) => Id[Cap^?]^? + |Required: (lcap: Cap^) => Id[Cap^'s1]^'s2 | |where: => refers to a fresh root capability created in value leak when checking argument to parameter op of method withCap | ^ refers to the universal root capability | - |Note that capability lcap.type - |cannot be included in outer capture set ?. + |Note that capability lcap cannot be included in outer capture set 's1. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/i16226.check b/tests/neg-custom-args/captures/i16226.check index e7acc515af2c..7cd8b91aa076 100644 --- a/tests/neg-custom-args/captures/i16226.check +++ b/tests/neg-custom-args/captures/i16226.check @@ -1,29 +1,36 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i16226.scala:13:4 ---------------------------------------- 13 | (ref1, f1) => map[A, B](ref1, f1) // error | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - |Found: (ref1: LazyRef[A^?]{val elem: () ->? A^?}^?, f1: A^? ->? B^?) ->? LazyRef[B^?]{val elem: () => B^?}^{f1, ref1} + |Found: (ref1: LazyRef[A^'s1]{val elem: () ->'s2 A^'s3}^'s4, f1: A^'s5 ->'s6 B^'s7) ->'s8 + | LazyRef[B^'s9]{val elem: () => B^'s10}^{f1, ref1} |Required: (LazyRef[A]^{io}, A =>² B) =>³ LazyRef[B]^ | - |where: => refers to a root capability associated with the result type of (ref1: LazyRef[A^?]{val elem: () ->? A^?}^?, f1: A^? ->? B^?): LazyRef[B^?]{val elem: () => B^?}^{f1, ref1} + |where: => refers to a root capability associated with the result type of (ref1: LazyRef[A^'s1]{val elem: () ->'s2 A^'s3}^'s4, f1: A^'s5 ->'s6 B^'s7): + | LazyRef[B^'s9]{val elem: () => B^'s10}^{f1, ref1} | =>² refers to the universal root capability | =>³ refers to a fresh root capability in the result type of method mapc | ^ refers to a fresh root capability in the result type of method mapc | - |Note that capability f1.type is not included in capture set {cap} - |because f1.type is not visible from cap in method mapc. + |Note that capability f1 is not included in capture set {cap} + |because (f1 : A^'s5 ->'s6 B^'s7) is not visible from cap in method mapc. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i16226.scala:15:4 ---------------------------------------- 15 | (ref1, f1) => map[A, B](ref1, f1) // error | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - |Found: (ref1: LazyRef[A^?]{val elem: () ->? A^?}^?, f1: A^? ->? B^?) ->? LazyRef[B^?]{val elem: () => B^?}^{f1, ref1} + |Found: (ref1: LazyRef[A^'s11]{val elem: () ->'s12 A^'s13}^'s14, f1: A^'s15 ->'s16 B^'s17) ->'s18 + | LazyRef[B^'s19]{val elem: () => B^'s20}^{f1, ref1} |Required: (ref: LazyRef[A]^{io}, f: A =>² B) =>³ LazyRef[B]^ | - |where: => refers to a root capability associated with the result type of (ref1: LazyRef[A^?]{val elem: () ->? A^?}^?, f1: A^? ->? B^?): LazyRef[B^?]{val elem: () => B^?}^{f1, ref1} + |where: => refers to a root capability associated with the result type of (ref1: LazyRef[A^'s11]{val elem: () ->'s12 A^'s13}^'s14, f1: A^'s15 ->'s16 B^'s17): + | LazyRef[B^'s19]{val elem: () => B^'s20}^{f1, ref1} | =>² refers to the universal root capability | =>³ refers to a fresh root capability in the result type of method mapd | ^ refers to a root capability associated with the result type of (ref: LazyRef[A]^{io}, f: A =>² B): LazyRef[B]^ | - |Note that capability f1.type is not included in capture set {? A^?}^?, f1: A^? ->? B^?): LazyRef[B^?]{val elem: () => B^?}^{f1, ref1}>}. + |Note that capability f1 is not included in capture set {'s12 A^'s13}^'s14, f1: A^'s15 ->'s16 B^'s17): + | LazyRef[B^'s19]{val elem: () => B^'s20}^{f1, ref1} + |>}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/i19330.check b/tests/neg-custom-args/captures/i19330.check index 044ebd553c07..88219f0ffa83 100644 --- a/tests/neg-custom-args/captures/i19330.check +++ b/tests/neg-custom-args/captures/i19330.check @@ -8,7 +8,7 @@ | ^ | Found: () ->{t} Logger^{t*} | Required: x.T - | Note that capability (t : () => Logger^) is not included in capture set {}. + | Note that capability t is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i19330.scala:22:22 --------------------------------------- diff --git a/tests/neg-custom-args/captures/i19470.check b/tests/neg-custom-args/captures/i19470.check index d674e8f1c764..b1279c9f1ef1 100644 --- a/tests/neg-custom-args/captures/i19470.check +++ b/tests/neg-custom-args/captures/i19470.check @@ -2,7 +2,7 @@ 9 | List(foo(f())) // error | ^^^^^^^^ | Found: Inv[IO^{f?}] - | Required: Inv[IO^?]^? - | Note that capability (f : () => IO^) is not included in capture set {f?}. + | Required: Inv[IO^'s1]^'s2 + | Note that capability f is not included in capture set {f?}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/i21313.check b/tests/neg-custom-args/captures/i21313.check index 04c5f452bf54..c1af867788af 100644 --- a/tests/neg-custom-args/captures/i21313.check +++ b/tests/neg-custom-args/captures/i21313.check @@ -10,6 +10,6 @@ | |where: ^ refers to a fresh root capability created in method test when checking argument to parameter src of method await | - |Note that capability (ac1 : Async^) cannot be included in capture set {ac2} of value src2. + |Note that capability ac1 cannot be included in capture set {ac2} of value src2. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/i21347.check b/tests/neg-custom-args/captures/i21347.check index ec0e708e079a..39f97eed7539 100644 --- a/tests/neg-custom-args/captures/i21347.check +++ b/tests/neg-custom-args/captures/i21347.check @@ -3,7 +3,7 @@ | ^^^^^^^^^^^^^^^^^^^^^^ | Found: () ->{f} Unit | Required: () -> Unit - | Note that capability (f : () => Unit) is not included in capture set {}. + | Note that capability f is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/i21347.scala:11:15 ------------------------------------------------------------ diff --git a/tests/neg-custom-args/captures/i21401.check b/tests/neg-custom-args/captures/i21401.check index 52be12983cbb..a8dfba1296c9 100644 --- a/tests/neg-custom-args/captures/i21401.check +++ b/tests/neg-custom-args/captures/i21401.check @@ -15,15 +15,15 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21401.scala:15:23 --------------------------------------- 15 | val a = usingIO[IO^](x => x) // error // error | ^^^^^^ - |Found: (x: IO^?) ->? IO^{x} + |Found: (x: IO^'s1) ->'s2 IO^{x} |Required: IO^ => IO^² | |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 | ^² refers to a fresh root capability created in value a when checking argument to parameter op of method usingIO | - |Note that capability x.type is not included in capture set {cap} - |because x.type is not visible from cap in value a. + |Note that capability x is not included in capture set {cap} + |because (x : IO^'s1) is not visible from cap in value a. | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/i21401.scala:16:66 ------------------------------------------------------------ @@ -50,14 +50,14 @@ -- [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 | ^^^^^^ - | Found: (x: Boxed[IO^]^?) ->? Boxed[IO^²] - | Required: Boxed[IO^] -> Boxed[IO^³] + | Found: (x: Boxed[IO^]^'s3) ->'s4 Boxed[IO^²] + | Required: Boxed[IO^] -> Boxed[IO^³] | - | where: ^ refers to the universal root capability - | ^² refers to a root capability associated with the result type of (x: Boxed[IO^]^?): Boxed[IO^²] - | ^³ refers to a fresh root capability created in value x² + | where: ^ refers to the universal root capability + | ^² refers to a root capability associated with the result type of (x: Boxed[IO^]^'s3): Boxed[IO^²] + | ^³ refers to a fresh root capability created in value x² | - | Note that capability is not included in capture set {cap} - | because is not visible from cap in value x. + | Note that capability is not included in capture set {cap} + | because is not visible from cap in value x. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/i21614.check b/tests/neg-custom-args/captures/i21614.check index 90dee8a8dbe5..dfc4f9ce2e40 100644 --- a/tests/neg-custom-args/captures/i21614.check +++ b/tests/neg-custom-args/captures/i21614.check @@ -12,13 +12,13 @@ -- [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^?) ->{C} Logger{val f: File^{_$1}}^{cap.rd, _$1} - |Required: File^{C} => Logger{val f: File^?}^? + |Found: (_$1: File^'s1) ->{C} Logger{val f: File^{_$1}}^{cap.rd, _$1} + |Required: File^{C} => Logger{val f: File^'s2}^'s3 | |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^?): Logger{val f: File^{_$1}}^{cap.rd, _$1} + | cap is a root capability associated with the result type of (_$1: File^'s1): Logger{val f: File^{_$1}}^{cap.rd, _$1} | |Note that capability C is not classified as trait SharedCapability, therefore it - |cannot be included in capture set ? of parameter _$1 of SharedCapability elements. + |cannot be included in capture set 's1 of parameter _$1 of SharedCapability elements. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/i21620.check b/tests/neg-custom-args/captures/i21620.check index 019ae9623dca..d5c99ede02ec 100644 --- a/tests/neg-custom-args/captures/i21620.check +++ b/tests/neg-custom-args/captures/i21620.check @@ -15,7 +15,7 @@ | ^ | Found: (f : () ->{x} () ->{x} Unit) | Required: () -> () ->{x} Unit - | Note that capability (x : C^) is not included in capture set {}. + | Note that capability x is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21620.scala:20:33 --------------------------------------- @@ -23,6 +23,6 @@ | ^ | Found: (f : () ->{x} () ->{x} Unit) | Required: () -> () ->{x} Unit - | Note that capability (x : C^) is not included in capture set {}. + | Note that capability x is not included in capture set {}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/i21920.check b/tests/neg-custom-args/captures/i21920.check index 2b860553c3af..66994fc36122 100644 --- a/tests/neg-custom-args/captures/i21920.check +++ b/tests/neg-custom-args/captures/i21920.check @@ -1,13 +1,12 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21920.scala:34:35 --------------------------------------- 34 | val cell: Cell[File] = File.open(f => Cell(() => Seq(f))) // error | ^^^^^^^^^^^^^^^^^^^^^^^ - |Found: (f: File^?) ->? Cell[File^?]{val head: () ->? IterableOnce[File^?]^?}^? - |Required: File^ => Cell[File^?]{val head: () ->? IterableOnce[File^?]^?}^? + |Found: (f: File^'s1) ->'s2 Cell[File^'s3]{val head: () ->'s4 IterableOnce[File^'s5]^'s6}^'s7 + |Required: File^ => Cell[File^'s8]{val head: () ->'s9 IterableOnce[File^'s10]^'s11}^'s12 | |where: => refers to a fresh root capability created in value cell when checking argument to parameter f of method open | ^ refers to the universal root capability | - |Note that capability - |cannot be included in outer capture set ?. + |Note that capability cannot be included in outer capture set 's13. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/i23207.check b/tests/neg-custom-args/captures/i23207.check index e66b6fb0e285..cc41779b6b47 100644 --- a/tests/neg-custom-args/captures/i23207.check +++ b/tests/neg-custom-args/captures/i23207.check @@ -3,7 +3,7 @@ | ^^^^^ | Found: (box.x : (b : B^{io})^{b}) | Required: A - | Note that capability (io : AnyRef^) is not included in capture set {}. + | Note that capability io is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i23207.scala:18:13 --------------------------------------- @@ -11,7 +11,7 @@ | ^ | Found: (c : B^{b}) | Required: A - | Note that capability (b : B^{io}) is not included in capture set {}. + | Note that capability b is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i23207.scala:23:2 ---------------------------------------- @@ -19,7 +19,7 @@ | ^ | Found: A^{io} | Required: A - | Note that capability (io : AnyRef^) is not included in capture set {}. + | Note that capability io is not included in capture set {}. 24 | val hide: AnyRef^{io} = io 25 | val b = new B 26 | val c = b.getBox.x diff --git a/tests/neg-custom-args/captures/i23431.check b/tests/neg-custom-args/captures/i23431.check index 9d48a8f4e099..34f8e3beac72 100644 --- a/tests/neg-custom-args/captures/i23431.check +++ b/tests/neg-custom-args/captures/i23431.check @@ -27,7 +27,7 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i23431.scala:12:12 --------------------------------------- 12 | withIO: io3 => // error | ^ - |Found: (io3: IO^?) ->? Unit + |Found: (io3: IO^'s1) ->'s2 Unit |Required: IO^ => Unit | |where: => refers to a fresh root capability created in anonymous function of type (io1: IO^): Unit when checking argument to parameter op of method withIO diff --git a/tests/neg-custom-args/captures/lazylist.check b/tests/neg-custom-args/captures/lazylist.check index 4bf4f1ac94f9..f2fbef088d18 100644 --- a/tests/neg-custom-args/captures/lazylist.check +++ b/tests/neg-custom-args/captures/lazylist.check @@ -1,9 +1,9 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylist.scala:17:15 ------------------------------------- 17 | def tail = xs() // error | ^^^^ - | Found: lazylists.LazyList[T]^{LazyCons.this.xs} - | Required: lazylists.LazyList[T] - | Note that capability (LazyCons.this.xs : () => lazylists.LazyList[T]^) is not included in capture set {}. + | Found: lazylists.LazyList[T]^{LazyCons.this.xs} + | Required: lazylists.LazyList[T] + | Note that capability LazyCons.this.xs is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylist.scala:35:29 ------------------------------------- @@ -11,31 +11,31 @@ | ^^^^ | Found: (ref1 : lazylists.LazyCons[Int]{val xs: () ->{cap1} lazylists.LazyList[Int]^{}}^{cap1}) | Required: lazylists.LazyList[Int] - | Note that capability (cap1 : lazylists.CC^) is not included in capture set {}. + | Note that capability cap1 is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylist.scala:37:36 ------------------------------------- 37 | val ref2c: LazyList[Int]^{ref1} = ref2 // error | ^^^^ - | Found: (ref2 : lazylists.LazyList[Int]^{cap2, ref1}) - | Required: lazylists.LazyList[Int]^{ref1} - | Note that capability (cap2 : lazylists.CC^) is not included in capture set {ref1}. + | Found: (ref2 : lazylists.LazyList[Int]^{cap2, ref1}) + | Required: lazylists.LazyList[Int]^{ref1} + | Note that capability cap2 is not included in capture set {ref1}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylist.scala:39:36 ------------------------------------- 39 | val ref3c: LazyList[Int]^{cap2} = ref3 // error | ^^^^ - |Found: (ref3 : lazylists.LazyList[Int]^{cap2, ref1}) - |Required: lazylists.LazyList[Int]^{cap2} - |Note that capability (ref1 : lazylists.LazyCons[Int]{val xs: () ->{cap1} lazylists.LazyList[Int]^{}}^{cap1}) is not included in capture set {cap2}. + | Found: (ref3 : lazylists.LazyList[Int]^{cap2, ref1}) + | Required: lazylists.LazyList[Int]^{cap2} + | Note that capability ref1 is not included in capture set {cap2}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylist.scala:41:42 ------------------------------------- 41 | val ref4c: LazyList[Int]^{cap1, ref3} = ref4 // error | ^^^^ - | Found: (ref4 : lazylists.LazyList[Int]^{cap3, cap1, cap2}) - | Required: lazylists.LazyList[Int]^{cap1, ref3} - | Note that capability (cap3 : lazylists.CC^) is not included in capture set {cap1, ref3}. + | Found: (ref4 : lazylists.LazyList[Int]^{cap3, cap1, cap2}) + | Required: lazylists.LazyList[Int]^{cap1, ref3} + | Note that capability cap3 is not included in capture set {cap1, ref3}. | | longer explanation available when compiling with `-explain` -- [E164] Declaration Error: tests/neg-custom-args/captures/lazylist.scala:22:6 ---------------------------------------- diff --git a/tests/neg-custom-args/captures/lazylists1.check b/tests/neg-custom-args/captures/lazylists1.check index c14568b9600c..a642351ddea9 100644 --- a/tests/neg-custom-args/captures/lazylists1.check +++ b/tests/neg-custom-args/captures/lazylists1.check @@ -1,8 +1,8 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylists1.scala:25:66 ----------------------------------- 25 | def concat(other: LazyList[A]^{f}): LazyList[A]^{this, f} = ??? : (LazyList[A]^{xs, f}) // error | ^^^^^^^^^^^^^^^^^^^^^^^^^^^ - | Found: LazyList[A]^{xs, f} - | Required: LazyList[A]^{Mapped.this, f} - | Note that capability (xs : LazyList[A]^) is not included in capture set {Mapped.this, f}. + | Found: LazyList[A]^{xs, f} + | Required: LazyList[A]^{Mapped.this, f} + | Note that capability xs is not included in capture set {Mapped.this, f}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/lazylists2.check b/tests/neg-custom-args/captures/lazylists2.check index 1f7fd0e509cb..bd90de396a22 100644 --- a/tests/neg-custom-args/captures/lazylists2.check +++ b/tests/neg-custom-args/captures/lazylists2.check @@ -1,9 +1,9 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylists2.scala:18:4 ------------------------------------ 18 | final class Mapped extends LazyList[B]: // error | ^ - | Found: LazyList[B^?]^{f, xs} + | Found: LazyList[B^'s1]^{f, xs} | Required: LazyList[B]^{f} - | Note that capability (xs : LazyList[A]^) is not included in capture set {f}. + | Note that capability xs is not included in capture set {f}. 19 | this: (Mapped^{xs, f}) => 20 | def isEmpty = false 21 | def head: B = f(xs.head) @@ -14,9 +14,9 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylists2.scala:27:4 ------------------------------------ 27 | final class Mapped extends LazyList[B]: // error | ^ - | Found: LazyList[B^?]^{f, xs} + | Found: LazyList[B^'s2]^{f, xs} | Required: LazyList[B]^{xs} - | Note that capability (f : A => B) is not included in capture set {xs}. + | Note that capability f is not included in capture set {xs}. 28 | this: Mapped^{xs, f} => 29 | def isEmpty = false 30 | def head: B = f(xs.head) @@ -35,9 +35,9 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylists2.scala:45:4 ------------------------------------ 45 | final class Mapped extends LazyList[B]: // error | ^ - | Found: LazyList[B^?]^{f, xs} + | Found: LazyList[B^'s3]^{f, xs} | Required: LazyList[B]^{xs} - | Note that capability (f : A => B) is not included in capture set {xs}. + | Note that capability f is not included in capture set {xs}. 46 | this: (Mapped^{xs, f}) => 47 | def isEmpty = false 48 | def head: B = f(xs.head) diff --git a/tests/neg-custom-args/captures/lazyref.check b/tests/neg-custom-args/captures/lazyref.check index 933b75cabdb8..596e688faf0b 100644 --- a/tests/neg-custom-args/captures/lazyref.check +++ b/tests/neg-custom-args/captures/lazyref.check @@ -3,31 +3,31 @@ | ^^^^ | Found: (ref1 : LazyRef[Int]{val elem: () ->{cap1} Int}^{cap1}) | Required: LazyRef[Int] - | Note that capability (cap1 : CC^) is not included in capture set {}. + | Note that capability cap1 is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazyref.scala:22:35 -------------------------------------- 22 | val ref2c: LazyRef[Int]^{cap2} = ref2 // error | ^^^^ - |Found: LazyRef[Int]{val elem: () ->{ref2*} Int}^{ref2} - |Required: LazyRef[Int]^{cap2} - |Note that capability (ref2 : LazyRef[Int]{val elem: () => Int}^{cap2, ref1}) is not included in capture set {cap2}. + | Found: LazyRef[Int]{val elem: () ->{ref2*} Int}^{ref2} + | Required: LazyRef[Int]^{cap2} + | Note that capability ref2 is not included in capture set {cap2}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazyref.scala:24:35 -------------------------------------- 24 | val ref3c: LazyRef[Int]^{ref1} = ref3 // error | ^^^^ - |Found: LazyRef[Int]{val elem: () ->{ref3*} Int}^{ref3} - |Required: LazyRef[Int]^{ref1} - |Note that capability (ref3 : LazyRef[Int]{val elem: () => Int}^{cap2, ref1}) is not included in capture set {ref1}. + | Found: LazyRef[Int]{val elem: () ->{ref3*} Int}^{ref3} + | Required: LazyRef[Int]^{ref1} + | Note that capability ref3 is not included in capture set {ref1}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazyref.scala:30:35 -------------------------------------- 30 | val ref4c: LazyRef[Int]^{cap1} = ref4 // error | ^^^^ - |Found: LazyRef[Int]{val elem: () ->{ref4*} Int}^{ref4} - |Required: LazyRef[Int]^{cap1} - |Note that capability (ref4 : LazyRef[Int]{val elem: () => Int}^{cap2, ref1}) is not included in capture set {cap1}. + | Found: LazyRef[Int]{val elem: () ->{ref4*} Int}^{ref4} + | Required: LazyRef[Int]^{cap1} + | Note that capability ref4 is not included in capture set {cap1}. | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/lazyref.scala:8:24 ------------------------------------------------------------ diff --git a/tests/neg-custom-args/captures/leak-problem-2.check b/tests/neg-custom-args/captures/leak-problem-2.check index 5af4d1135454..71af3da33844 100644 --- a/tests/neg-custom-args/captures/leak-problem-2.check +++ b/tests/neg-custom-args/captures/leak-problem-2.check @@ -1,8 +1,8 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/leak-problem-2.scala:8:8 --------------------------------- 8 | = race(Seq(src1, src2)) // error | ^^^^^^^^^^^^^^^^^^^^^ - | Found: Source[T^?]^{src1, src2} + | Found: Source[T^'s1]^{src1, src2} | Required: Source[T] - | Note that capability (src1 : Source[T]^) is not included in capture set {}. + | Note that capability src1 is not included in capture set {}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/leaking-iterators.check b/tests/neg-custom-args/captures/leaking-iterators.check index 80461c0496ee..51bef2ed5e0f 100644 --- a/tests/neg-custom-args/captures/leaking-iterators.check +++ b/tests/neg-custom-args/captures/leaking-iterators.check @@ -1,14 +1,13 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/leaking-iterators.scala:56:16 ---------------------------- 56 | usingLogFile: log => // error | ^ - |Found: (log: java.io.FileOutputStream^?) ->? cctest.Iterator[Int]^{log} - |Required: java.io.FileOutputStream^ => cctest.Iterator[Int]^? + |Found: (log: java.io.FileOutputStream^'s1) ->'s2 cctest.Iterator[Int]^{log} + |Required: java.io.FileOutputStream^ => cctest.Iterator[Int]^'s3 | |where: => refers to a fresh root capability created in method test when checking argument to parameter op of method usingLogFile | ^ refers to the universal root capability | - |Note that capability log.type - |cannot be included in outer capture set ?. + |Note that capability log cannot be included in outer capture set 's3. 57 | xs.iterator.map: x => 58 | log.write(x) 59 | x * x diff --git a/tests/neg-custom-args/captures/leaky.check b/tests/neg-custom-args/captures/leaky.check index 57630a636f73..932ab1ebf7af 100644 --- a/tests/neg-custom-args/captures/leaky.check +++ b/tests/neg-custom-args/captures/leaky.check @@ -3,7 +3,7 @@ | ^ | Found: test.runnable.Transform{val fun: Any ->{a} Any}^{a} | Required: test.runnable.Transform - | Note that capability (a : test.runnable.A) is not included in capture set {}. + | Note that capability a is not included in capture set {}. 15 | a.print() 16 | () 17 | Transform(f) @@ -14,7 +14,7 @@ | ^ | Found: test.runnable.Transform{val fun: Any ->{a} Any}^{a} | Required: test.runnable.Transform - | Note that capability (a : test.runnable.A) is not included in capture set {}. + | Note that capability a is not included in capture set {}. 21 | a.print() 22 | () 23 | val x = Transform(f) @@ -26,7 +26,7 @@ | ^ | Found: test.runnable.Transform{val fun: Any ->{a} Any}^{a} | Required: test.runnable.Transform - | Note that capability (a : test.runnable.A) is not included in capture set {}. + | Note that capability a is not included in capture set {}. 28 | a.print() 29 | () 30 | val x = Transform.app(f) diff --git a/tests/neg-custom-args/captures/levels.check b/tests/neg-custom-args/captures/levels.check index 34f339e57869..30bad568e021 100644 --- a/tests/neg-custom-args/captures/levels.check +++ b/tests/neg-custom-args/captures/levels.check @@ -10,6 +10,6 @@ | ^ | Found: (x: String) ->{cap3} String | Required: String -> String - | Note that capability (cap3 : CC^) is not included in capture set {}. + | Note that capability cap3 is not included in capture set {}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/lubs.check b/tests/neg-custom-args/captures/lubs.check index 24f4d2e6546b..b290c442956a 100644 --- a/tests/neg-custom-args/captures/lubs.check +++ b/tests/neg-custom-args/captures/lubs.check @@ -3,7 +3,7 @@ | ^^ | Found: (x1 : D^{d1}) | Required: D - | Note that capability (d1 : D^{c1}) is not included in capture set {}. + | Note that capability d1 is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lubs.scala:18:13 ----------------------------------------- @@ -11,7 +11,7 @@ | ^^ | Found: (x2 : D^{d1}) | Required: D - | Note that capability (d1 : D^{c1}) is not included in capture set {}. + | Note that capability d1 is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lubs.scala:19:13 ----------------------------------------- @@ -19,6 +19,6 @@ | ^^ | Found: (x3 : D^{d1, d2}) | Required: D - | Note that capability (d1 : D^{c1}) is not included in capture set {}. + | Note that capability d1 is not included in capture set {}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/nestedclass.check b/tests/neg-custom-args/captures/nestedclass.check index 5c4125b30535..c50c06d908cd 100644 --- a/tests/neg-custom-args/captures/nestedclass.check +++ b/tests/neg-custom-args/captures/nestedclass.check @@ -3,6 +3,6 @@ | ^^ | Found: (xs : C^{cap1}) | Required: C - | Note that capability (cap1 : CC^) is not included in capture set {}. + | Note that capability cap1 is not included in capture set {}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/reaches.check b/tests/neg-custom-args/captures/reaches.check index d3847b13e870..25574538070a 100644 --- a/tests/neg-custom-args/captures/reaches.check +++ b/tests/neg-custom-args/captures/reaches.check @@ -1,7 +1,7 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:22:13 -------------------------------------- 22 | usingFile: f => // error | ^ - |Found: (f: File^?) ->? Unit + |Found: (f: File^'s1) ->'s2 Unit |Required: File^ => Unit | |where: => refers to a fresh root capability created in method runAll0 when checking argument to parameter f of method usingFile @@ -14,7 +14,7 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:32:13 -------------------------------------- 32 | usingFile: f => // error | ^ - |Found: (f: File^?) ->? Unit + |Found: (f: File^'s3) ->'s4 Unit |Required: File^ => Unit | |where: => refers to a fresh root capability created in method runAll1 when checking argument to parameter f of method usingFile @@ -68,7 +68,7 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:59:27 -------------------------------------- 59 | val id: File^ -> File^ = x => x // error | ^^^^^^ - | Found: (x: File^) ->? File^² + | Found: (x: File^) ->'s5 File^² | Required: File^ -> File^³ | | where: ^ refers to the universal root capability @@ -82,7 +82,7 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:69:38 -------------------------------------- 69 | val leaked = usingFile[File^{id*}]: f => // error | ^ - |Found: (f: File^?) ->? File^{id*} + |Found: (f: File^'s6) ->'s7 File^{id*} |Required: File^ => File^{id*} | |where: => refers to a fresh root capability created in value leaked when checking argument to parameter f of method usingFile @@ -96,8 +96,8 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:87:10 -------------------------------------- 87 | ps.map((x, y) => compose1(x, y)) // error | ^^^^^^^^^^^^^^^^^^^^^^^ - |Found: (x$1: (A^ ->? A^?, A^ ->? A^?)^?) ->? A^? ->? A^? - |Required: ((A ->{ps*} A, A ->{ps*} A)) => A^? ->? A^? + |Found: (x$1: (A^ ->'s8 A^'s9, A^ ->'s10 A^'s11)^'s12) ->'s13 A^'s14 ->'s15 A^'s16 + |Required: ((A ->{ps*} A, A ->{ps*} A)) => A^'s17 ->'s18 A^'s19 | |where: => refers to a fresh root capability created in method mapCompose when checking argument to parameter f of method map | ^ refers to the universal root capability @@ -108,8 +108,8 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:90:10 -------------------------------------- 90 | ps.map((x, y) => compose1(x, y)) // error | ^^^^^^^^^^^^^^^^^^^^^^^ - |Found: (x$1: (A^ ->? A^?, A^ ->? A^?)^?) ->? A^? ->? A^? - |Required: ((A ->{C} A, A ->{C} A)) => A^? ->? A^? + |Found: (x$1: (A^ ->'s20 A^'s21, A^ ->'s22 A^'s23)^'s24) ->'s25 A^'s26 ->'s27 A^'s28 + |Required: ((A ->{C} A, A ->{C} A)) => A^'s29 ->'s30 A^'s31 | |where: => refers to a fresh root capability created in method mapCompose2 when checking argument to parameter f of method map | ^ refers to the universal root capability diff --git a/tests/neg-custom-args/captures/reaches2.check b/tests/neg-custom-args/captures/reaches2.check index e91ea3c3859e..5ab7b14a85c1 100644 --- a/tests/neg-custom-args/captures/reaches2.check +++ b/tests/neg-custom-args/captures/reaches2.check @@ -1,8 +1,8 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches2.scala:10:10 ------------------------------------- 10 | ps.map((x, y) => compose1(x, y)) // error | ^^^^^^^^^^^^^^^^^^^^^^^ - | Found: (x$1: (A^? ->{ps*} A^?, A^? ->{ps*} A^?)^?) ->{ps*} A^? ->{ps*} A^? - | Required: ((A ->{ps*} A, A ->{ps*} A)) -> A^? ->{ps*} A^? + | Found: (x$1: (A^'s1 ->{ps*} A^'s2, A^'s3 ->{ps*} A^'s4)^'s5) ->{ps*} A^'s6 ->{ps*} A^'s7 + | Required: ((A ->{ps*} A, A ->{ps*} A)) -> A^'s6 ->{ps*} A^'s7 | Note that capability ps* is not included in capture set {}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/readOnly.check b/tests/neg-custom-args/captures/readOnly.check index e212cf2f1a6f..31d9940ab87e 100644 --- a/tests/neg-custom-args/captures/readOnly.check +++ b/tests/neg-custom-args/captures/readOnly.check @@ -11,7 +11,7 @@ | ^^^^ | Found: (putA : Int ->{a} Unit) | Required: Int -> Unit - | Note that capability (a : Ref^) is not included in capture set {}. + | Note that capability a is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/readOnly.scala:20:23 ---------------------------------------------------------- diff --git a/tests/neg-custom-args/captures/real-try.check b/tests/neg-custom-args/captures/real-try.check index 9663a134a3a1..bca841e11094 100644 --- a/tests/neg-custom-args/captures/real-try.check +++ b/tests/neg-custom-args/captures/real-try.check @@ -31,7 +31,7 @@ -- Error: tests/neg-custom-args/captures/real-try.scala:26:10 ---------------------------------------------------------- 26 | val y = try // error | ^ - | The result of `try` cannot have type () => Cell[Unit]^? since + | The result of `try` cannot have type () => Cell[Unit]^'s1 since | that type captures the root capability `cap`. | This is often caused by a locally generated exception capability leaking as part of its result. | @@ -43,7 +43,7 @@ -- Error: tests/neg-custom-args/captures/real-try.scala:32:10 ---------------------------------------------------------- 32 | val b = try // error | ^ - | The result of `try` cannot have type Cell[() => Unit]^? since + | The result of `try` cannot have type Cell[() => Unit]^'s2 since | the part () => Unit of that type captures the root capability `cap`. | This is often caused by a locally generated exception capability leaking as part of its result. | diff --git a/tests/neg-custom-args/captures/reference-cc.check b/tests/neg-custom-args/captures/reference-cc.check new file mode 100644 index 000000000000..a76238e5fade --- /dev/null +++ b/tests/neg-custom-args/captures/reference-cc.check @@ -0,0 +1,43 @@ +-- Error: tests/neg-custom-args/captures/reference-cc.scala:42:20 ------------------------------------------------------ +42 | def f = println(c) // error + | ^ + | reference (c : Cap) is not included in the allowed capture set {} + | of the enclosing class A +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reference-cc.scala:44:27 --------------------------------- +44 | val later = usingLogFile { file => () => file.write(0) } // error + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + |Found: (file: java.io.FileOutputStream^'s1) ->'s2 () ->{file} Unit + |Required: java.io.FileOutputStream^ => () ->'s3 Unit + | + |where: => refers to a fresh root capability created in value later when checking argument to parameter op of method usingLogFile + | ^ refers to the universal root capability + | + |Note that capability file cannot be included in outer capture set 's3. + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reference-cc.scala:47:25 --------------------------------- +47 | val xs = usingLogFile: f => // error + | ^ + |Found: (f: java.io.FileOutputStream^'s4) ->'s5 LzyList[Int]^{f} + |Required: java.io.FileOutputStream^ => LzyList[Int]^'s6 + | + |where: => refers to a fresh root capability created in value xs when checking argument to parameter op of method usingLogFile + | ^ refers to the universal root capability + | + |Note that capability f cannot be included in outer capture set 's6. +48 | LzyList(1, 2, 3).map { x => f.write(x); x * x } + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reference-cc.scala:58:8 ---------------------------------- +58 | try () => xs.map(f).sum // error TODO improve error message + | ^^^^^^^^^^^^^^^^^^^ + |Found: () => Double + |Required: () =>² Double + | + |where: => refers to a fresh root capability classified as Control in the type of given instance canThrow$1 + | =>² refers to a fresh root capability created in anonymous function of type (using erased x$1: CanThrow[LimitExceeded]): () => Double when instantiating expected result type () ->{cap} Double of function literal + | + |Note that capability cap is not included in capture set {cap} + |because cap in method try$1 is not visible from cap in enclosing function. + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/reference-cc.scala b/tests/neg-custom-args/captures/reference-cc.scala new file mode 100644 index 000000000000..c94ad207bb04 --- /dev/null +++ b/tests/neg-custom-args/captures/reference-cc.scala @@ -0,0 +1,59 @@ +import language.experimental.captureChecking +import scala.compiletime.uninitialized +import java.io.* +import language.experimental.saferExceptions + + +def usingLogFile[T](op: FileOutputStream^ => T): T = + val logFile = FileOutputStream("log") + val result = op(logFile) + logFile.close() + result + +trait LzyList[+A]: + def isEmpty: Boolean + def head: A + def tail: LzyList[A]^{this} + def map[B](f: A => B): LzyList[B]^{f, this} = ??? +object LzyList: + def apply[A](xs: A*): LzyList[A] = ??? + +object LzyNil extends LzyList[Nothing]: + def isEmpty = true + def head = ??? + def tail = ??? + +final class LzyCons[+A](hd: A, tl: () => LzyList[A]^) extends LzyList[A]: + private var forced = false + private var cache: LzyList[A]^{this} = uninitialized + private def force = + if !forced then { cache = tl(); forced = true } + cache + + def isEmpty = false + def head = hd + def tail: LzyList[A]^{this} = force +end LzyCons + +class Cap extends caps.SharedCapability +def test(c: Cap) = + class A: + val x: A = this + def f = println(c) // error + + val later = usingLogFile { file => () => file.write(0) } // error + later() // crash + + val xs = usingLogFile: f => // error + LzyList(1, 2, 3).map { x => f.write(x); x * x } + +class LimitExceeded extends Exception + +def testException = + val limit = 10e+10 + def f(x: Double): Double throws LimitExceeded = + if x < limit then x * x else throw LimitExceeded() + + def escaped(xs: Double*): (() => Double) throws LimitExceeded = + try () => xs.map(f).sum // error TODO improve error message + catch case ex: LimitExceeded => () => -1 diff --git a/tests/neg-custom-args/captures/ro-mut-conformance.check b/tests/neg-custom-args/captures/ro-mut-conformance.check index 0f6ce6bfcf58..5fe6730551b4 100644 --- a/tests/neg-custom-args/captures/ro-mut-conformance.check +++ b/tests/neg-custom-args/captures/ro-mut-conformance.check @@ -11,6 +11,6 @@ | | where: ^ refers to a fresh root capability classified as Mutable in the type of value t | - | Note that capability (a : Ref) is not included in capture set {}. + | Note that capability a is not included in capture set {}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/scoped-caps.check b/tests/neg-custom-args/captures/scoped-caps.check index 90b957c4cb43..d1559c50f0fc 100644 --- a/tests/neg-custom-args/captures/scoped-caps.check +++ b/tests/neg-custom-args/captures/scoped-caps.check @@ -48,7 +48,7 @@ | ^² refers to a root capability associated with the result type of (x: A^): B^² | ^³ refers to a fresh root capability in the type of value _$5 | - | Note that capability (g : A^ -> B^) is not included in capture set {}. + | Note that capability g is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:16:24 ---------------------------------- @@ -73,7 +73,7 @@ | ^² refers to a root capability associated with the result type of (x: S^): B^² | ^³ refers to a root capability associated with the result type of (x: S^): B^³ | - | Note that capability (h : S -> B^) is not included in capture set {}. + | Note that capability h is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:21:23 ---------------------------------- @@ -86,7 +86,7 @@ | ^² refers to a root capability associated with the result type of (x: S^): S^² | ^³ refers to a root capability associated with the result type of (x: S^): S^³ | - | Note that capability (h2 : S -> S) is not included in capture set {}. + | Note that capability h2 is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:27:19 ---------------------------------- @@ -106,7 +106,7 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:28:19 ---------------------------------- 28 | val _: S -> B^ = x => j(x) // error | ^^^^^^^^^ - | Found: (x: S^) ->? B^² + | Found: (x: S^) ->'s1 B^² | Required: S^ -> B^³ | | where: ^ refers to the universal root capability diff --git a/tests/neg-custom-args/captures/sep-curried.check b/tests/neg-custom-args/captures/sep-curried.check index dd0c4d14efa2..47a3aecd9511 100644 --- a/tests/neg-custom-args/captures/sep-curried.check +++ b/tests/neg-custom-args/captures/sep-curried.check @@ -1,12 +1,12 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/sep-curried.scala:48:43 ---------------------------------- 48 | val f: (y: Ref[Int]^{a}) ->{a} Unit = foo(a) // error | ^^^^^^ - | Found: (y: Ref[Int]^) ->{a} Unit - | Required: (y: Ref[Int]^{a}) ->{a} Unit + | Found: (y: Ref[Int]^) ->{a} Unit + | Required: (y: Ref[Int]^{a}) ->{a} Unit | - | where: ^ refers to the universal root capability + | where: ^ refers to the universal root capability | - | Note that capability (a : Ref[Int]^) is not included in capture set {cap}. + | Note that capability a is not included in capture set {cap}. | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/sep-curried.scala:16:6 -------------------------------------------------------- diff --git a/tests/neg-custom-args/captures/simple-using.check b/tests/neg-custom-args/captures/simple-using.check index 681e83136571..dbe4ee74ff52 100644 --- a/tests/neg-custom-args/captures/simple-using.check +++ b/tests/neg-custom-args/captures/simple-using.check @@ -1,13 +1,12 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/simple-using.scala:8:15 ---------------------------------- 8 | usingLogFile { f => () => f.write(2) } // error | ^^^^^^^^^^^^^^^^^^^^^^^^^ - |Found: (f: java.io.FileOutputStream^?) ->? () ->{f} Unit - |Required: java.io.FileOutputStream^ => () ->? Unit + |Found: (f: java.io.FileOutputStream^'s1) ->'s2 () ->{f} Unit + |Required: java.io.FileOutputStream^ => () ->'s3 Unit | |where: => refers to a fresh root capability created in method test when checking argument to parameter op of method usingLogFile | ^ refers to the universal root capability | - |Note that capability f.type - |cannot be included in outer capture set ?. + |Note that capability f cannot be included in outer capture set 's3. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/try.check b/tests/neg-custom-args/captures/try.check index 1d5434b04010..ea67bcd4b414 100644 --- a/tests/neg-custom-args/captures/try.check +++ b/tests/neg-custom-args/captures/try.check @@ -8,15 +8,15 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:23:49 ------------------------------------------ 23 | val a = handle[Exception, CanThrow[Exception]] { // error // error | ^ - |Found: (x: CT[Exception]^) ->? CT[Exception]^{x} + |Found: (x: CT[Exception]^) ->'s1 CT[Exception]^{x} |Required: CT[Exception]^ => CT[Exception]^² | |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 | ^² refers to a fresh root capability created in value a when checking argument to parameter op of method handle | - |Note that capability x.type is not included in capture set {cap} - |because x.type is not visible from cap in value a. + |Note that capability x is not included in capture set {cap} + |because (x : CT[Exception]^) is not visible from cap in value a. 24 | (x: CanThrow[Exception]) => x 25 | }{ | @@ -24,13 +24,13 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:29:43 ------------------------------------------ 29 | val b = handle[Exception, () -> Nothing] { // error | ^ - |Found: (x: CT[Exception]^) ->? () ->{x} Nothing + |Found: (x: CT[Exception]^) ->'s2 () ->{x} Nothing |Required: CT[Exception]^ => () -> Nothing | |where: => refers to a fresh root capability created in value b when checking argument to parameter op of method handle | ^ refers to the universal root capability | - |Note that capability x.type is not included in capture set {}. + |Note that capability x is not included in capture set {}. 30 | (x: CanThrow[Exception]) => () => raise(new Exception)(using x) 31 | } { | @@ -38,14 +38,13 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:35:18 ------------------------------------------ 35 | val xx = handle { // error | ^ - |Found: (x: CT[Exception]^) ->? () ->{x} Int - |Required: CT[Exception]^ => () ->? Int + |Found: (x: CT[Exception]^) ->'s3 () ->{x} Int + |Required: CT[Exception]^ => () ->'s4 Int | |where: => refers to a fresh root capability created in value xx when checking argument to parameter op of method handle | ^ refers to the universal root capability | - |Note that capability x.type - |cannot be included in outer capture set ?. + |Note that capability x cannot be included in outer capture set 's4. 36 | (x: CanThrow[Exception]) => 37 | () => 38 | raise(new Exception)(using x) @@ -56,14 +55,13 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:47:31 ------------------------------------------ 47 |val global: () -> Int = handle { // error | ^ - |Found: (x: CT[Exception]^) ->? () ->{x} Int - |Required: CT[Exception]^ => () ->? Int + |Found: (x: CT[Exception]^) ->'s5 () ->{x} Int + |Required: CT[Exception]^ => () ->'s6 Int | |where: => refers to a fresh root capability created in value global when checking argument to parameter op of method handle | ^ refers to the universal root capability | - |Note that capability x.type - |cannot be included in outer capture set ?. + |Note that capability x cannot be included in outer capture set 's6. 48 | (x: CanThrow[Exception]) => 49 | () => 50 | raise(new Exception)(using x) diff --git a/tests/neg-custom-args/captures/unsound-reach-4.check b/tests/neg-custom-args/captures/unsound-reach-4.check index be216502f3ad..2baeaa5b9ad6 100644 --- a/tests/neg-custom-args/captures/unsound-reach-4.check +++ b/tests/neg-custom-args/captures/unsound-reach-4.check @@ -8,7 +8,7 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/unsound-reach-4.scala:20:29 ------------------------------ 20 | val backdoor: Foo[File^] = new Bar // error (follow-on, since the parent Foo[File^] of bar is illegal). | ^^^^^^^ - | Found: Bar^? + | Found: Bar^'s1 | Required: Foo[File^] | | where: ^ refers to a fresh root capability in the type of value backdoor diff --git a/tests/neg-custom-args/captures/unsound-reach-6.check b/tests/neg-custom-args/captures/unsound-reach-6.check index 9cbcf4d37145..9a21ef84cb97 100644 --- a/tests/neg-custom-args/captures/unsound-reach-6.check +++ b/tests/neg-custom-args/captures/unsound-reach-6.check @@ -11,7 +11,7 @@ | ^ | Found: (x : () ->{io} Unit) | Required: () -> Unit - | Note that capability (io : IO^) is not included in capture set {}. + | Note that capability io is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/unsound-reach-6.scala:7:13 ---------------------------------------------------- diff --git a/tests/neg-custom-args/captures/unsound-reach.check b/tests/neg-custom-args/captures/unsound-reach.check index b9cb97a9819a..512d1088fa27 100644 --- a/tests/neg-custom-args/captures/unsound-reach.check +++ b/tests/neg-custom-args/captures/unsound-reach.check @@ -15,7 +15,7 @@ -- [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). | ^^^^^^^ - | Found: Bar^? + | Found: Bar^'s1 | Required: Foo[File^] | | where: ^ refers to a fresh root capability in the type of value backdoor diff --git a/tests/neg-custom-args/captures/use-capset.check b/tests/neg-custom-args/captures/use-capset.check index d093a9ceff15..a00d77fc560f 100644 --- a/tests/neg-custom-args/captures/use-capset.check +++ b/tests/neg-custom-args/captures/use-capset.check @@ -3,15 +3,15 @@ | ^ | Found: (h : () ->{io} Unit) | Required: () -> Unit - | Note that capability (io : Object^) is not included in capture set {}. + | Note that capability io is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:13:50 ----------------------------------- 13 | val _: () -> List[Object^{io}] -> Object^{io} = h2 // error, should be ->{io} | ^^ - | Found: (h2 : () ->{} List[Object^{io}]^{} ->{io} Object^{io}) - | Required: () -> List[Object^{io}] -> Object^{io} - | Note that capability (io : Object^) is not included in capture set {}. + | Found: (h2 : () ->{} List[Object^{io}]^{} ->{io} Object^{io}) + | Required: () -> List[Object^{io}] -> Object^{io} + | Note that capability io is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/use-capset.scala:5:49 --------------------------------------------------------- diff --git a/tests/neg-custom-args/captures/uses.check b/tests/neg-custom-args/captures/uses.check index c5044c647ce0..43d0ff8cec6d 100644 --- a/tests/neg-custom-args/captures/uses.check +++ b/tests/neg-custom-args/captures/uses.check @@ -3,7 +3,7 @@ | ^ | Found: (d : D^{x, y}) | Required: D^{y} - | Note that capability (x : C^) is not included in capture set {y}. + | Note that capability x is not included in capture set {y}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/uses.scala:9:13 ------------------------------------------ @@ -11,7 +11,7 @@ | ^ | Found: (d : D^{x, y}) | Required: D - | Note that capability (x : C^) is not included in capture set {}. + | Note that capability x is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/uses.scala:18:34 ----------------------------------------- @@ -19,7 +19,7 @@ | ^ | Found: () ->{x, y} () ->{y} Unit | Required: () ->{x} () ->{y} Unit - | Note that capability (y : C^) is not included in capture set {x}. + | Note that capability y is not included in capture set {x}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/uses.scala:19:28 ----------------------------------------- @@ -27,6 +27,6 @@ | ^ | Found: () ->{x, y} () ->{y} Unit | Required: () -> () -> Unit - | Note that capability (x : C^) is not included in capture set {}. + | Note that capability x is not included in capture set {}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/usingLogFile.check b/tests/neg-custom-args/captures/usingLogFile.check index 3add71106063..e4a8ae2e42f3 100644 --- a/tests/neg-custom-args/captures/usingLogFile.check +++ b/tests/neg-custom-args/captures/usingLogFile.check @@ -1,52 +1,48 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/usingLogFile.scala:22:27 --------------------------------- 22 | val later = usingLogFile { f => () => f.write(0) } // error | ^^^^^^^^^^^^^^^^^^^^^^^^^ - |Found: (f: java.io.FileOutputStream^?) ->? () ->{f} Unit - |Required: java.io.FileOutputStream^ => () ->? Unit + |Found: (f: java.io.FileOutputStream^'s1) ->'s2 () ->{f} Unit + |Required: java.io.FileOutputStream^ => () ->'s3 Unit | |where: => refers to a fresh root capability created in value later when checking argument to parameter op of method usingLogFile | ^ refers to the universal root capability | - |Note that capability f.type - |cannot be included in outer capture set ?. + |Note that capability f cannot be included in outer capture set 's3. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/usingLogFile.scala:27:36 --------------------------------- 27 | private val later2 = usingLogFile { f => Cell(() => f.write(0)) } // error | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - |Found: (f: java.io.FileOutputStream^?) ->? Test2.Cell[() ->{f} Unit]^? - |Required: java.io.FileOutputStream^ => Test2.Cell[() ->? Unit]^? + |Found: (f: java.io.FileOutputStream^'s4) ->'s5 Test2.Cell[() ->{f} Unit]^'s6 + |Required: java.io.FileOutputStream^ => Test2.Cell[() ->'s7 Unit]^'s8 | |where: => refers to a fresh root capability created in value later2 when checking argument to parameter op of method usingLogFile | ^ refers to the universal root capability | - |Note that capability f.type - |cannot be included in outer capture set ?. + |Note that capability f cannot be included in outer capture set 's7. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/usingLogFile.scala:43:33 --------------------------------- 43 | val later = usingFile("out", f => (y: Int) => xs.foreach(x => f.write(x + y))) // error | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - |Found: (f: java.io.OutputStream^?) ->? Int ->{f} Unit - |Required: java.io.OutputStream^ => Int ->? Unit + |Found: (f: java.io.OutputStream^'s9) ->'s10 Int ->{f} Unit + |Required: java.io.OutputStream^ => Int ->'s11 Unit | |where: => refers to a fresh root capability created in value later when checking argument to parameter op of method usingFile | ^ refers to the universal root capability | - |Note that capability f.type - |cannot be included in outer capture set ?. + |Note that capability f cannot be included in outer capture set 's11. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/usingLogFile.scala:52:6 ---------------------------------- 52 | usingLogger(_, l => () => l.log("test"))) // error after checking mapping scheme | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - |Found: (_$1: java.io.OutputStream^?) ->? () ->{_$1} Unit - |Required: java.io.OutputStream^ => () ->? Unit + |Found: (_$1: java.io.OutputStream^'s12) ->'s13 () ->{_$1} Unit + |Required: java.io.OutputStream^ => () ->'s14 Unit | |where: => refers to a fresh root capability created in value later when checking argument to parameter op of method usingFile | ^ refers to the universal root capability | - |Note that capability _$1.type - |cannot be included in outer capture set ?. + |Note that capability _$1 cannot be included in outer capture set 's14. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/vars-simple.check b/tests/neg-custom-args/captures/vars-simple.check index 931fb0c19cca..2fd7ead20da3 100644 --- a/tests/neg-custom-args/captures/vars-simple.check +++ b/tests/neg-custom-args/captures/vars-simple.check @@ -14,7 +14,7 @@ | ^ | Found: (x: String) ->{cap3} String | Required: String ->{cap1, cap2} String - | Note that capability (cap3 : CC^) is not included in capture set {cap1, cap2}. + | Note that capability cap3 is not included in capture set {cap1, cap2}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/vars-simple.scala:17:12 ---------------------------------- @@ -22,6 +22,6 @@ | ^^^^^^^ | Found: List[String ->{cap3} String] | Required: List[String ->{cap1, cap2} String] - | Note that capability (cap3 : CC^) is not included in capture set {cap1, cap2}. + | Note that capability cap3 is not included in capture set {cap1, cap2}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/vars.check b/tests/neg-custom-args/captures/vars.check index 0ce74f481b56..052fd6bec10f 100644 --- a/tests/neg-custom-args/captures/vars.check +++ b/tests/neg-custom-args/captures/vars.check @@ -3,7 +3,7 @@ | ^^^^^^^^^ | Found: (x: String) ->{cap3} String | Required: String ->{cap1} String - | Note that capability (cap3 : CC^), defined in method scope + | Note that capability cap3, defined in method scope | cannot be included in outer capture set {cap1} of variable a. | | longer explanation available when compiling with `-explain` @@ -12,7 +12,7 @@ | ^ | Found: (x: String) ->{cap3} String | Required: String ->{cap1} String - | Note that capability (cap3 : CC^), defined in method scope + | Note that capability cap3, defined in method scope | cannot be included in outer capture set {cap1} of variable a. | | longer explanation available when compiling with `-explain` @@ -21,21 +21,20 @@ | ^^^^^^^ | Found: List[String ->{cap3} String] | Required: List[String ->{cap1, cap2} String] - | Note that capability (cap3 : CC^) is not included in capture set {cap1, cap2}. + | Note that capability cap3 is not included in capture set {cap1, cap2}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/vars.scala:36:8 ------------------------------------------ 36 | local { cap3 => // error | ^ - |Found: (cap3: CC^) ->? String => String + |Found: (cap3: CC^) ->'s1 String => String |Required: CC^ -> String =>² String | |where: => refers to a root capability associated with the result type of (cap3: CC^): String => String | =>² refers to a fresh root capability created in method test of parameter parameter cap3² of method $anonfun | ^ refers to the universal root capability | - |Note that capability String> - |cannot be included in outer capture set {cap}. + |Note that capability String> cannot be included in outer capture set {cap}. 37 | def g(x: String): String = if cap3 == cap3 then "" else "a" 38 | g 39 | } diff --git a/tests/neg-custom-args/captures/widen-reach.check b/tests/neg-custom-args/captures/widen-reach.check index 7e25b96d87b1..e1f76704a3d2 100644 --- a/tests/neg-custom-args/captures/widen-reach.check +++ b/tests/neg-custom-args/captures/widen-reach.check @@ -8,7 +8,7 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/widen-reach.scala:9:24 ----------------------------------- 9 | val foo: IO^ -> IO^ = x => x // error | ^^^^^^ - | Found: (x: IO^) ->? IO^² + | Found: (x: IO^) ->'s1 IO^² | Required: IO^ -> IO^³ | | where: ^ refers to the universal root capability diff --git a/tests/neg/i16842.check b/tests/neg/i16842.check index 936b08f95dbb..9a77e194add0 100644 --- a/tests/neg/i16842.check +++ b/tests/neg/i16842.check @@ -1,4 +1,4 @@ -- Error: tests/neg/i16842.scala:24:7 ---------------------------------------------------------------------------------- 24 | Liter(SemanticArray[SemanticInt.type], x) // error | ^ - | invalid new prefix (dim: Int): SemanticArray[SemanticInt.type] cannot replace ty.type in type ty.T + |invalid new prefix (dim: Int): SemanticArray[SemanticInt.type] cannot replace (ty : SemanticArray[SemanticType]) in type ty.T diff --git a/tests/neg/i18058.check b/tests/neg/i18058.check index f610d9e7abb1..993b7b0362ed 100644 --- a/tests/neg/i18058.check +++ b/tests/neg/i18058.check @@ -1,4 +1,4 @@ -- Error: tests/neg/i18058.scala:4:21 ---------------------------------------------------------------------------------- 4 |type G = (f: ? <: F) => f.A // error | ^ - | invalid new prefix <: F cannot replace f.type in type f.A + | invalid new prefix <: F cannot replace (f : <: F) in type f.A diff --git a/tests/neg/lambda-rename.check b/tests/neg/lambda-rename.check index 39969d4a7cfa..53c43ca8f1b4 100644 --- a/tests/neg/lambda-rename.check +++ b/tests/neg/lambda-rename.check @@ -1,8 +1,8 @@ -- [E007] Type Mismatch Error: tests/neg/lambda-rename.scala:4:33 ------------------------------------------------------ 4 |val a: (x: Int) => Bar[x.type] = ??? : ((x: Int) => Foo[x.type]) // error | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - | Found: (x: Int) => Foo[x.type] - | Required: (x: Int) => Bar[x.type] + | Found: (x: Int) => Foo[(x : Int)] + | Required: (x: Int) => Bar[(x : Int)] | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg/lambda-rename.scala:7:33 ------------------------------------------------------ diff --git a/tests/neg/polymorphic-functions1.check b/tests/neg/polymorphic-functions1.check index f925fe7b0f52..612c1d0688a1 100644 --- a/tests/neg/polymorphic-functions1.check +++ b/tests/neg/polymorphic-functions1.check @@ -1,8 +1,8 @@ -- [E007] Type Mismatch Error: tests/neg/polymorphic-functions1.scala:1:33 --------------------------------------------- 1 |val f: [T] => (x: T) => x.type = [T] => (x: Int) => x // error | ^^^^^^^^^^^^^^^^^^^^ - | Found: [T] => (x: Int) => x.type - | Required: [T] => (x²: T) => x².type + | Found: [T] => (x: Int) => (x : Int) + | Required: [T] => (x²: T) => (x² : T) | | where: x is a reference to a value parameter | x² is a reference to a value parameter diff --git a/tests/pos-custom-args/captures/reference-cc.scala b/tests/pos-custom-args/captures/reference-cc.scala new file mode 100644 index 000000000000..ea0dbf6860aa --- /dev/null +++ b/tests/pos-custom-args/captures/reference-cc.scala @@ -0,0 +1,8 @@ +import language.experimental.captureChecking +import java.io.* + +def usingLogFile[T](op: FileOutputStream^ => T): T = + val logFile = FileOutputStream("log") + val result = op(logFile) + logFile.close() + result \ No newline at end of file