Better printing of capabilities in error messages

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
 

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):

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")

compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala

@@ -173,10 +173,11 @@ class PlainPrinter(_ctx: Context) extends Printer {
     else if cs == CaptureSet.Fluid then "<fluid>"
     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

docs/_docs/reference/experimental/cc.md

@@ -44,9 +44,11 @@ followed by `^`. We'll see that this turns the parameter into a _capability_ who
 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.
+   |                           ^^^^^^^^^^^^^^^^^^^^^^^^^
+   |  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:
@@ -58,11 +60,11 @@ val xs = usingLogFile { f =>
 and the following unsafe one:
 ```scala
 val xs = usingLogFile { f =>
-  LazyList(1, 2, 3).map { x => f.write(x); x * x }
+  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 of `LazyList` which we will present later in this page).
+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:
@@ -87,12 +89,12 @@ The capture checker extension introduces a new kind of types and it enforces som
 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
+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 most sweeping capability, from which ultimately all others are derived is written `cap`. We call it the _universal capability_.
+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:
@@ -105,8 +107,8 @@ class Logger(fs: FileSystem^):
 def test(fs: FileSystem^) =
   val l: Logger^{fs} = Logger(fs)
   l.log("hello world!")
-  val xs: LazyList[Int]^{l} =
-    LazyList.from(1)
+  val xs: LzyList[Int]^{l} =
+    LzyList.from(1)
       .map { i =>
         l.log(s"computing elem # $i")
         i * i
@@ -118,9 +120,9 @@ and retained as a field in class `Logger`. Hence, the local variable `l` has typ
 `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,
+`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 `LazyList[Int]^{l}`. On the other hand, since `xs` only logs but does
+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`.
 
@@ -138,7 +140,7 @@ This type is a shorthand for `(A -> B)^{c, d}`, i.e. the function type `A -> B`
 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})`.
+`A -> B^{c}` is read as `A -> (B^{c})` and `A -> B^` is read as `A -> (B^{cap})`.
 
 Analogous conventions apply to context function types. `A ?=> B` is an impure context function, with `A ?-> B` as its pure complement.
 
@@ -203,15 +205,15 @@ we have
 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:
+**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^): LazyList[Int] = {
+11 |def test(using fs: FileSystem^): LzyList[Int] = {
    |                                                 ^
-   |                                        Found:    LazyList[Int]^{fs}
-   |                                        Required: LazyList[Int]
+   |                                        Found:    LzyList[Int]^{fs}
+   |                                        Required: LzyList[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.
+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
@@ -361,39 +363,37 @@ This principle plays an important part in making capture checking concise and pr
 
 ## 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.
+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 can now reconstruct how this principle produced the error in the introductory example, where
+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) }
-   |              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-   |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.
+   |                           ^^^^^^^^^^^^^^^^^^^^^^^^^
+   |  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^) -> () ->{f} Unit`.
+   `(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`.
- - 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.
+ - 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
@@ -406,23 +406,8 @@ usingLogFile { f =>
 }
 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.
-```
+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_:
 

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 = {

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`

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`

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`