From a9de45fe2453d774f4a97c59c4de928186c48aee Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Tue, 30 Dec 2025 14:47:36 +0100
Subject: [PATCH] Warn if reach capability in result will cause leakage

An unboxed reach in a result type of a method will in almost all cases lead
to use leakage error in the body of the method (except if the body is pure, and
we widen to the reach without cause). Warn at this point already so that the
leakage error that follows can be better understood.
---
 compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala |  6 +++++-
 tests/neg-custom-args/captures/nicolas2.check        | 11 +++++++++++
 tests/neg-custom-args/captures/nicolas2.scala        | 11 +++++++++++
 tests/pos-custom-args/captures/nicolas1.scala        | 11 +++++++++++
 4 files changed, 38 insertions(+), 1 deletion(-)
 create mode 100644 tests/neg-custom-args/captures/nicolas2.check
 create mode 100644 tests/neg-custom-args/captures/nicolas2.scala
 create mode 100644 tests/pos-custom-args/captures/nicolas1.scala

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 9790f366fb21..6dddd4835830 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -663,6 +663,8 @@ class CheckCaptures extends Recheck, SymTransformer:
           if param.isUseParam then markFree(arg.nuType.deepCaptureSet, errTree)
     end markFreeTypeArgs
 
+// ---- Check for leakages of reach capabilities ------------------------------
+
     /** If capability `c` refers to a parameter that is not implicitly or explicitly
      *  @use declared, report an error.
      */
@@ -695,7 +697,7 @@ class CheckCaptures extends Recheck, SymTransformer:
                     case tp: TermRef =>
                       report.warning(
                         em"""Reach capability $ref in function result refers to ${tp.symbol}.
-                            |To avoid errors of the form "Local reach capability $ref leaks into capture set ..."
+                            |To avoid errors of the form "Local reach capability $ref leaks into capture scope ..."
                             |you should replace the reach capability with a new capset variable in ${tree.symbol}.""",
                         tree.tpt.srcPos)
                     case _ =>
@@ -703,6 +705,8 @@ class CheckCaptures extends Recheck, SymTransformer:
         tpt.nuType.foreachPart(checkType, StopAt.Static)
       case _ =>
 
+// ---- Rechecking operations for different kinds of trees----------------------
+
     /** If `tp` (possibly after widening singletons) is an ExprType
      *  of a parameterless method, map Result instances in it to Fresh instances
      */
diff --git a/tests/neg-custom-args/captures/nicolas2.check b/tests/neg-custom-args/captures/nicolas2.check
new file mode 100644
index 000000000000..1b8d23c24bda
--- /dev/null
+++ b/tests/neg-custom-args/captures/nicolas2.check
@@ -0,0 +1,11 @@
+-- Warning: tests/neg-custom-args/captures/nicolas2.scala:9:53 ---------------------------------------------------------
+9 |def oneOf[A](head: Rand ?=> A, tail: (Rand ?=> A)*): Rand ?->{head, tail*} A =
+  |                                                     ^^^^^^^^^^^^^^^^^^^^^^^
+  |                           Reach capability tail* in function result refers to parameter tail.
+  |                           To avoid errors of the form "Local reach capability tail* leaks into capture scope ..."
+  |                           you should replace the reach capability with a new capset variable in method oneOf.
+-- Error: tests/neg-custom-args/captures/nicolas2.scala:11:5 -----------------------------------------------------------
+11 |  all(nextInt(all.length))  // error
+   |  ^^^^^^^^^^^^^^^^^^^^^^^^
+   |  Local reach capability tail* leaks into capture scope of method oneOf.
+   |  You could try to abstract the capabilities referred to by tail* in a capset variable.
diff --git a/tests/neg-custom-args/captures/nicolas2.scala b/tests/neg-custom-args/captures/nicolas2.scala
new file mode 100644
index 000000000000..409357327813
--- /dev/null
+++ b/tests/neg-custom-args/captures/nicolas2.scala
@@ -0,0 +1,11 @@
+import caps.*
+
+trait Rand extends SharedCapability:
+  def range(min: Int, max: Int): Int
+
+def nextInt(max: Int): Rand ?-> Int =
+  r ?=> r.range(0, max)
+
+def oneOf[A](head: Rand ?=> A, tail: (Rand ?=> A)*): Rand ?->{head, tail*} A =
+  val all: Seq[Rand ?->{head, tail*} A] = head +: tail
+  all(nextInt(all.length))  // error
diff --git a/tests/pos-custom-args/captures/nicolas1.scala b/tests/pos-custom-args/captures/nicolas1.scala
new file mode 100644
index 000000000000..52ff62c9aebb
--- /dev/null
+++ b/tests/pos-custom-args/captures/nicolas1.scala
@@ -0,0 +1,11 @@
+import caps.*
+
+trait Rand extends SharedCapability:
+  def range(min: Int, max: Int): Int
+
+def nextInt(max: Int): Rand ?-> Int =
+  r ?=> r.range(0, max)
+
+def oneOf[A, B^](head: Rand ?=> A, tail: (Rand ?->{B} A)*): Rand ?->{head, B} A =
+  val all: Seq[Rand ?->{head, B} A] = head +: tail // error
+  all(nextInt(all.length))
\ No newline at end of file