diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala index b451242d410d..439da067d253 100644 --- a/compiler/src/dotty/tools/dotc/cc/Capability.scala +++ b/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. diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala index 7442b44cf07f..326ab611ff82 100644 --- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala +++ b/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 diff --git a/tests/neg-custom-args/captures/boxed-consume.scala b/tests/neg-custom-args/captures/boxed-consume.scala new file mode 100644 index 000000000000..856aea2d4d0b --- /dev/null +++ b/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 + + + + + diff --git a/tests/neg-custom-args/captures/consume-tvar-bound.check b/tests/neg-custom-args/captures/consume-tvar-bound.check new file mode 100644 index 000000000000..4adfbf54f8f9 --- /dev/null +++ b/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 diff --git a/tests/neg-custom-args/captures/consume-tvar-bound.scala b/tests/neg-custom-args/captures/consume-tvar-bound.scala new file mode 100644 index 000000000000..06f4a259c1bb --- /dev/null +++ b/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 +