Disallow fresh caps from parameter bounds in results

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

@@ -169,7 +169,7 @@ object Capabilities:
      */
     var skolems: immutable.Map[Symbol, TermRef] = immutable.HashMap.empty
 
-    //assert(rootId != 10, i"fresh $prefix, ${ctx.owner}")
+    //assert(rootId != 4, i"fresh $prefix, $origin, ${ctx.owner}")
 
     /** Is this fresh cap (definitely) classified? If that's the case, the
      *  classifier cannot be changed anymore.

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

@@ -833,6 +833,22 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
             case t =>
               foldOver(c, t)
 
+    /** Check that no fresh caps from the bounds of parameters or abstract types
+     *  are hidden in the result. See issue #24539
+     */
+    def checkNoTParamBounds(refsToCheck: Refs, descr: => String, pos: SrcPos): Unit =
+      for ref <- refsToCheck do
+        ref match
+          case ref: FreshCap =>
+            ref.origin match
+              case Origin.InDecl(sym) if sym.isAbstractOrParamType =>
+                report.error(
+                  em"""Separation failure: $descr $ref, which appears in the bound of $sym.
+                      |This is not allowed. The $sym has to be returned explicitly in the result type.""",
+                  pos)
+              case _ =>
+          case _ =>
+
     /** If `tpe` appears as a (result-) type of a definition, treat its
      *  hidden set minus its explicitly declared footprint as consumed.
      *  If `tpe` appears as an argument to a consume parameter, treat
@@ -847,8 +863,11 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
                                     // "see through them" when we look at hidden sets.
         then
           val refs = tpe.deepCaptureSet.elems
-          val toCheck = refs.transHiddenSet.directFootprint.nonPeaks.deduct(refs.directFootprint.nonPeaks)
-          checkConsumedRefs(toCheck, tpe, role, i"${role.description} $tpe hides", pos)
+          val refsStar = refs.transHiddenSet
+          val toCheck = refsStar.directFootprint.nonPeaks.deduct(refs.directFootprint.nonPeaks)
+          def descr = i"${role.description} $tpe hides"
+          checkConsumedRefs(toCheck, tpe, role, descr, pos)
+          checkNoTParamBounds(refsStar, descr, pos)
       case TypeRole.Argument(arg, _) =>
         if tpe.hasAnnotation(defn.ConsumeAnnot) then
           val capts = spanCaptures(arg).directFootprint.nonPeaks

tests/neg-custom-args/captures/boxed-consume.scala

@@ -0,0 +1,26 @@
+import caps.*
+
+def Test =
+  val c: Object^ = "a"
+  val d: Object^ = "a"
+  val e1, e2: Object^ = "a"
+  val falseDeps: Object^ = "a"
+  def f[T](consume x: T): Unit = ()
+  def g(consume x: Object^): Unit = ()
+  def h(consume x: (Object^, Object^)): Object^ = x._1  // error: local reach leak
+  val cc = (c, c)
+  f(cc)  // no consume, it's boxed
+  f(c)   // no consume, it's boxed
+  println(c)  // ok
+  g(d)   // consume
+  println(d) // error
+  h((e1, e2))  // no consume, still boxed
+  println(e1)  // ok
+
+  class Ref extends Mutable
+  def i[T <: Ref](consume x: Ref): Ref = x
+
+
+
+
+

tests/neg-custom-args/captures/consume-tvar-bound.check

@@ -0,0 +1,30 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/consume-tvar-bound.scala:9:44 ----------------------------
+9 |def hh[T <: Ref^](x: Box[T]): (Ref^, Int) = (x.elem, 1) // error (but msg is strange since it does not highlight the underlying box conflict)
+  |                                            ^^^^^^^^^^^
+  |                                   Found:    (T^'s1, Int)
+  |                                   Required: (Ref^, Int)
+  |
+  |                                   Note that capability cap is not included in capture set {}.
+  |
+  |                                   where:    ^   refers to a fresh root capability in the result type of method hh
+  |                                             cap is a fresh root capability in the type of type T
+  |
+  | longer explanation available when compiling with `-explain`
+-- Error: tests/neg-custom-args/captures/consume-tvar-bound.scala:7:29 -------------------------------------------------
+7 |def h[T <: Ref^](x: Box[T]): Ref^ = x.elem // error
+  |                             ^^^^
+  |                  Separation failure: method h's result type Ref^ hides cap, which appears in the bound of type T.
+  |                  This is not allowed. The type T has to be returned explicitly in the result type.
+  |
+  |                  where:    cap is a fresh root capability in the type of type T
+-- Error: tests/neg-custom-args/captures/consume-tvar-bound.scala:11:37 ------------------------------------------------
+11 |def g[T <: Ref^](consume x: Box[T]): Ref^ = x.elem // error
+   |                                     ^^^^
+   |                Separation failure: method g's result type Ref^ hides cap, which appears in the bound of type T.
+   |                This is not allowed. The type T has to be returned explicitly in the result type.
+   |
+   |                where:    cap is a fresh root capability in the type of type T
+-- Error: tests/neg-custom-args/captures/consume-tvar-bound.scala:20:43 ------------------------------------------------
+20 |  def f[T <: Ref^{rr}](consume x: Box[T]): Ref^ = x.elem // error
+   |                                           ^^^^
+   |                                    Separation failure: method f's result type Ref^ hides non-local parameter rr

tests/neg-custom-args/captures/consume-tvar-bound.scala

@@ -0,0 +1,21 @@
+import scala.language.experimental.captureChecking
+import scala.language.experimental.separationChecking
+
+class Ref
+class Box[T](val elem: T)
+
+def h[T <: Ref^](x: Box[T]): Ref^ = x.elem // error
+
+def hh[T <: Ref^](x: Box[T]): (Ref^, Int) = (x.elem, 1) // error (but msg is strange since it does not highlight the underlying box conflict)
+
+def g[T <: Ref^](consume x: Box[T]): Ref^ = x.elem // error
+
+
+def Test(rr: Ref^) =
+
+  val r: Ref^ = Ref()
+  val r2 = h(Box(r))
+  println(r)
+
+  def f[T <: Ref^{rr}](consume x: Box[T]): Ref^ = x.elem // error
+