Fix error message for leaks

Author: odersky

compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala

@@ -544,15 +544,21 @@ class CheckCaptures extends Recheck, SymTransformer:
         useInfos += ((tree, cs, curEnv))
     end markFree
 
-    /** If capability `c` refers to a parameter that is not @use declared, report an error.
+    /** If capability `c` refers to a parameter that is not implicitly or explicitly
+     *  @use declared, report an error.
      */
     def checkUseDeclared(c: Capability, pos: SrcPos)(using Context): Unit =
       c.paramPathRoot match
         case ref: NamedType if !ref.symbol.isUseParam =>
           val what = if ref.isType then "Capture set parameter" else "Local reach capability"
+          def mitigation =
+            if ccConfig.allowUse
+            then i"\nTo allow this, the ${ref.symbol} should be declared with a @use annotation."
+            else if !ref.isType then i"\nYou could try to abstract the capabilities referred to by $c in a capset variable."
+            else ""
           report.error(
-            em"""$what $c leaks into capture scope of ${ownerStr(ref.symbol.owner)}.
-                |To allow this, the ${ref.symbol} should be declared with a @use annotation""", pos)
+            em"$what $c leaks into capture scope of ${ownerStr(ref.symbol.owner)}.$mitigation",
+            pos)
         case _ =>
 
     /** Include references captured by the called method in the current environment stack */
@@ -1785,7 +1791,7 @@ class CheckCaptures extends Recheck, SymTransformer:
 
         override def checkInheritedTraitParameters: Boolean = false
 
-        /** Check that overrides don't change the @use or @consume status of their parameters */
+        /** Check that overrides don't change the @use, @consume, or @reserve status of their parameters */
         override def additionalChecks(member: Symbol, other: Symbol)(using Context): Unit =
           for
             (params1, params2) <- member.rawParamss.lazyZip(other.rawParamss)

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

@@ -379,7 +379,8 @@ class PlainPrinter(_ctx: Context) extends Printer {
     finally elideCapabilityCaps = saved
 
   /** Print the annotation that are meant to be on the parameter symbol but was moved
-   * to parameter types. Examples are `@use` and `@consume`. */
+   * to parameter types. Examples are `@use` and `@consume`.
+   */
   protected def specialAnnotText(sym: ClassSymbol, tp: Type): Text =
     Str(s"@${sym.name} ").provided(tp.hasAnnotation(sym))
 

tests/neg-custom-args/captures/delayedRunops.check

@@ -20,7 +20,7 @@
 22 |      runOps(ops1)  // error
    |      ^^^^^^
    |      Local reach capability ops* leaks into capture scope of method delayedRunOps2.
-   |      To allow this, the parameter ops should be declared with a @use annotation
+   |      You could try to abstract the capabilities referred to by ops* in a capset variable.
 -- Error: tests/neg-custom-args/captures/delayedRunops.scala:21:16 -----------------------------------------------------
 21 |      val ops1: List[() => Unit] = ops // error
    |                ^^^^^^^^^^^^^^^^

tests/neg-custom-args/captures/i21347.check

@@ -9,5 +9,5 @@
 11 |  ops.foreach: op => // error
    |               ^
    |               Local reach capability ops* leaks into capture scope of method runOpsAlt.
-   |               To allow this, the parameter ops should be declared with a @use annotation
+   |               You could try to abstract the capabilities referred to by ops* in a capset variable.
 12 |    op()

tests/neg-custom-args/captures/i21442.check

@@ -2,12 +2,12 @@
 10 |  val io = x.unbox // error: local reach capability {x*} leaks
    |           ^^^^^^^
    |           Local reach capability x.unbox* leaks into capture scope of method foo.
-   |           To allow this, the parameter x should be declared with a @use annotation
+   |           You could try to abstract the capabilities referred to by x.unbox* in a capset variable.
 -- Error: tests/neg-custom-args/captures/i21442.scala:18:14 ------------------------------------------------------------
 18 |  val io = x1.unbox // error
    |           ^^^^^^^^
    |           Local reach capability x* leaks into capture scope of method bar.
-   |           To allow this, the parameter x should be declared with a @use annotation
+   |           You could try to abstract the capabilities referred to by x* in a capset variable.
 -- Error: tests/neg-custom-args/captures/i21442.scala:17:10 ------------------------------------------------------------
 17 |  val x1: Boxed[IO^] = x // error
    |          ^^^^^^^^^^

tests/neg-custom-args/captures/i23303.check

@@ -1,10 +1,10 @@
 -- Error: tests/neg-custom-args/captures/i23303.scala:6:36 -------------------------------------------------------------
 6 |    def execute: Unit = ops.foreach(f => f()) // error
   |                                    ^^^^^^^^
-  |                                 Local reach capability Runner.this.ops* leaks into capture scope of class Runner.
-  |                                 To allow this, the value ops should be declared with a @use annotation
+  |                  Local reach capability Runner.this.ops* leaks into capture scope of class Runner.
+  |                  You could try to abstract the capabilities referred to by Runner.this.ops* in a capset variable.
 -- Error: tests/neg-custom-args/captures/i23303.scala:9:22 -------------------------------------------------------------
 9 |    () => ops.foreach(f => f()) // error
   |                      ^^^^^^^^
   |                      Local reach capability ops* leaks into capture scope of method Runner2.
-  |                      To allow this, the parameter ops should be declared with a @use annotation
+  |                      You could try to abstract the capabilities referred to by ops* in a capset variable.

tests/neg-custom-args/captures/localReaches.check

@@ -2,12 +2,12 @@
 24 |  var x: () ->{xs*} Unit = ys.head // error
    |                           ^^^^^^^
    |                           Local reach capability ops* leaks into capture scope of method localReach3.
-   |                           To allow this, the parameter ops should be declared with a @use annotation
+   |                           You could try to abstract the capabilities referred to by ops* in a capset variable.
 -- Error: tests/neg-custom-args/captures/localReaches.scala:27:11 ------------------------------------------------------
 27 |    x = ys.head  // error
    |        ^^^^^^^
    |        Local reach capability ops* leaks into capture scope of method localReach3.
-   |        To allow this, the parameter ops should be declared with a @use annotation
+   |        You could try to abstract the capabilities referred to by ops* in a capset variable.
 -- Error: tests/neg-custom-args/captures/localReaches.scala:14:10 ------------------------------------------------------
 14 |  val xs: List[() => Unit] = op :: Nil // error
    |          ^^^^^^^^^^^^^^^^

tests/neg-custom-args/captures/reaches.check

@@ -114,4 +114,4 @@
 39 |    val next: () => Unit = cur.head   // error
    |                           ^^^^^^^^
    |                           Local reach capability xs* leaks into capture scope of method runAll2.
-   |                           To allow this, the parameter xs should be declared with a @use annotation
+   |                           You could try to abstract the capabilities referred to by xs* in a capset variable.

tests/neg-custom-args/captures/unsound-reach-6.check

@@ -16,12 +16,12 @@
 7 |  println(xs.head) // error
   |          ^^^^^^^
   |          Local reach capability xs* leaks into capture scope of method f.
-  |          To allow this, the parameter xs should be declared with a @use annotation
+  |          You could try to abstract the capabilities referred to by xs* in a capset variable.
 -- Error: tests/neg-custom-args/captures/unsound-reach-6.scala:11:14 ---------------------------------------------------
 11 |    val z = f(ys)   // error @consume failure
    |              ^^
    |              Local reach capability ys* leaks into capture scope of method test.
-   |              To allow this, the parameter ys should be declared with a @use annotation
+   |              You could try to abstract the capabilities referred to by ys* in a capset variable.
 -- Error: tests/neg-custom-args/captures/unsound-reach-6.scala:19:14 ---------------------------------------------------
 19 |    val z = f(ys)  // error @consume failure
    |              ^^

tests/neg-custom-args/captures/use-capset.check

@@ -16,4 +16,3 @@
 5 |private def g[C^] = (xs: List[Object^{C}]) => xs.head // error TODO: allow this
   |                                              ^^^^^^^
   |                                              Capture set parameter C leaks into capture scope of method g.
-  |                                              To allow this, the type C should be declared with a @use annotation