Charge deep capture set for arguments to @consume parameters

scala · Feb 7, 2025 · c658e3c · c658e3c
1 parent 465c657
commit c658e3c
Show file tree

Hide file tree

Showing 3 changed files with 20 additions and 5 deletions.
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -698,8 +698,8 @@ class CheckCaptures extends Recheck, SymTransformer:
       val freshenedFormal = Fresh.fromCap(formal)
       val argType = recheck(arg, freshenedFormal)
         .showing(i"recheck arg $arg vs $freshenedFormal", capt)
-      if formal.hasAnnotation(defn.UseAnnot) then
-        // The @use annotation is added to `formal` by `prepareFunction`
+      if formal.hasAnnotation(defn.UseAnnot) || formal.hasAnnotation(defn.ConsumeAnnot) then
+        // The @use and/or @consume annotation is added to `formal` by `prepareFunction`
         capt.println(i"charging deep capture set of $arg: ${argType} = ${argType.deepCaptureSet}")
         markFree(argType.deepCaptureSet, arg)
       if formal.containsCap then

diff --git a/tests/neg-custom-args/captures/unsound-reach-6.check b/tests/neg-custom-args/captures/unsound-reach-6.check
@@ -6,7 +6,22 @@
 -- Error: tests/neg-custom-args/captures/unsound-reach-6.scala:11:14 ---------------------------------------------------
 11 |    val z = f(ys)   // error @consume failure
    |              ^^
-   |Separation failure: argument to @consume parameter with type (ys : List[box () ->{io} Unit]) refers to non-local parameter ys
+   |              Local reach capability ys* leaks into capture scope of method test.
+   |              To allow this, the parameter ys should be declared with a @use annotation
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/unsound-reach-6.scala:13:22 ------------------------------
+13 |  val _: () -> Unit = x // error
+   |                      ^
+   |                      Found:    (x : () ->{ys*} Unit)
+   |                      Required: () -> Unit
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/unsound-reach-6.scala:21:22 ------------------------------
+21 |  val _: () -> Unit = x // error
+   |                      ^
+   |                      Found:    (x : () ->{io} Unit)
+   |                      Required: () -> Unit
+   |
+   | longer explanation available when compiling with `-explain`
 -- Error: tests/neg-custom-args/captures/unsound-reach-6.scala:19:14 ---------------------------------------------------
 19 |    val z = f(ys)  // error @consume failure
    |              ^^

diff --git a/tests/neg-custom-args/captures/unsound-reach-6.scala b/tests/neg-custom-args/captures/unsound-reach-6.scala
@@ -10,15 +10,15 @@ def test(io: IO^)(ys: List[() ->{io} Unit]) =
   val x = () =>
     val z = f(ys)   // error @consume failure
     z()
-  val _: () -> Unit = x // !!! ys* gets lost
+  val _: () -> Unit = x // error
   ()
 
 def test(io: IO^) =
   def ys: List[() ->{io} Unit] = ???
   val x = () =>
     val z = f(ys)  // error @consume failure
     z()
-  val _: () -> Unit = x // !!! io gets lost
+  val _: () -> Unit = x // error
   ()