From 95d23a41ee2a073786cb4e2c677f8d6e7cf43711 Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Fri, 7 Jun 2024 13:27:17 +0200
Subject: [PATCH] Go back to original no cap in box/unbox restrictions

We go back to the original lifetime restriction that box/unbox cannot
apply to universal capture sets, and drop the later restriction that
type variable instantiations may not deeply capture cap.

The original restriction is proven to be sound and is probably expressive
enough when we add reach capabilities.

This required some changes in tests and also in the standard library.

The original restriction is in place for source <= 3.2 and >= 3.5. Source
3.3 and 3.4 use the alternative restriction on type variable instances.

Some neg tests have not been brought forward to 3.4. They are all in
tests/neg-customargs/captures and start with

//> using options -source 3.4

We need to look at these tests one-by-one and analyze whether the new 3.5 behavior
is correct.
---
 .../src/dotty/tools/dotc/cc/CaptureOps.scala  |  4 +-
 .../src/scala/collection/Iterator.scala       |  4 +-
 .../src/scala/collection/SeqView.scala        | 12 +++--
 .../immutable/LazyListIterable.scala          | 53 ++++++++++---------
 .../captures/box-adapt-cases.scala            |  2 +-
 .../neg-custom-args/captures/capt-test.scala  |  4 +-
 tests/neg-custom-args/captures/capt1.check    | 40 +++++++-------
 tests/neg-custom-args/captures/capt1.scala    |  2 +
 .../captures/effect-swaps-explicit.check      | 22 ++++----
 .../captures/effect-swaps-explicit.scala      |  2 +
 tests/neg-custom-args/captures/filevar.scala  |  2 +-
 tests/neg-custom-args/captures/i15749.scala   | 15 ++++++
 tests/neg-custom-args/captures/i15772.check   |  8 +--
 tests/neg-custom-args/captures/i15922.scala   |  2 +
 .../captures/i15923-cases.scala               |  7 +++
 tests/neg-custom-args/captures/i16114.scala   |  2 +
 .../captures/i19330-alt2.scala                |  2 +
 tests/neg-custom-args/captures/i19330.scala   |  2 +
 .../captures/lazylists-exceptions.check       |  5 +-
 tests/neg-custom-args/captures/levels.check   |  8 +--
 tests/neg-custom-args/captures/levels.scala   |  2 +
 .../neg-custom-args/captures/outer-var.check  | 30 ++++++-----
 tests/neg-custom-args/captures/reaches.check  | 28 +++++-----
 tests/neg-custom-args/captures/reaches.scala  |  2 +
 tests/neg-custom-args/captures/real-try.check | 52 +++++++++---------
 tests/neg-custom-args/captures/real-try.scala |  2 +
 tests/neg-custom-args/captures/try.check      | 16 +++---
 tests/neg-custom-args/captures/try.scala      |  4 +-
 .../captures}/unsound-reach-2.scala           |  2 +
 .../captures}/unsound-reach-3.scala           |  2 +
 .../captures}/unsound-reach-4.check           |  4 +-
 .../captures}/unsound-reach-4.scala           |  2 +
 .../captures/unsound-reach.check              | 12 +++++
 .../captures}/unsound-reach.scala             |  2 +-
 .../captures/vars-simple.check                |  9 ++--
 tests/neg-custom-args/captures/vars.check     | 16 +++---
 tests/neg-custom-args/captures/vars.scala     |  2 +
 tests/neg/unsound-reach.check                 |  5 --
 tests/pos-custom-args/captures/casts.scala    |  4 ++
 .../captures/filevar-expanded.scala           |  3 +-
 tests/pos-custom-args/captures/i15749.scala   |  4 +-
 .../captures/i15923-cases.scala               |  4 --
 tests/pos-custom-args/captures/i15925.scala   |  5 +-
 tests/pos-custom-args/captures/levels.scala   | 23 ++++++++
 .../captures/unsafe-captures.scala            |  8 +++
 .../captures/untracked-captures.scala         | 34 ++++++++++++
 .../colltest5/CollectionStrawManCC5_1.scala   |  2 +-
 47 files changed, 310 insertions(+), 167 deletions(-)
 create mode 100644 tests/neg-custom-args/captures/i15749.scala
 create mode 100644 tests/neg-custom-args/captures/i15923-cases.scala
 rename tests/{neg => neg-custom-args/captures}/unsound-reach-2.scala (89%)
 rename tests/{neg => neg-custom-args/captures}/unsound-reach-3.scala (89%)
 rename tests/{neg => neg-custom-args/captures}/unsound-reach-4.check (55%)
 rename tests/{neg => neg-custom-args/captures}/unsound-reach-4.scala (85%)
 create mode 100644 tests/neg-custom-args/captures/unsound-reach.check
 rename tests/{neg => neg-custom-args/captures}/unsound-reach.scala (83%)
 delete mode 100644 tests/neg/unsound-reach.check
 create mode 100644 tests/pos-custom-args/captures/casts.scala
 create mode 100644 tests/pos-custom-args/captures/levels.scala
 create mode 100644 tests/pos-custom-args/captures/unsafe-captures.scala
 create mode 100644 tests/pos-custom-args/captures/untracked-captures.scala

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
index d8c567f145d4..7a8ed7b3651a 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
@@ -32,7 +32,9 @@ object ccConfig:
    *  previous global retriction that `cap` can't be boxed or unboxed.
    */
   def allowUniversalInBoxed(using Context) =
-    Feature.sourceVersion.isAtLeast(SourceVersion.`3.3`)
+    Feature.sourceVersion.stable == SourceVersion.`3.3`
+    || Feature.sourceVersion.stable == SourceVersion.`3.4`
+    //|| Feature.sourceVersion.stable == SourceVersion.`3.5` // drop `//` if you want to test with the sealed type params strategy
 end ccConfig
 
 
diff --git a/scala2-library-cc/src/scala/collection/Iterator.scala b/scala2-library-cc/src/scala/collection/Iterator.scala
index 58ef4beb930d..4d1b0ed4ff95 100644
--- a/scala2-library-cc/src/scala/collection/Iterator.scala
+++ b/scala2-library-cc/src/scala/collection/Iterator.scala
@@ -1008,7 +1008,7 @@ object Iterator extends IterableFactory[Iterator] {
   def newBuilder[A]: Builder[A, Iterator[A]] =
     new ImmutableBuilder[A, Iterator[A]](empty[A]) {
       override def addOne(elem: A): this.type = { elems = elems ++ single(elem); this }
-    }
+    }.asInstanceOf // !!! CC unsafe op
 
   /** Creates iterator that produces the results of some element computation a number of times.
     *
@@ -1160,7 +1160,7 @@ object Iterator extends IterableFactory[Iterator] {
         @tailrec def merge(): Unit =
           if (current.isInstanceOf[ConcatIterator[_]]) {
             val c = current.asInstanceOf[ConcatIterator[A]]
-            current = c.current
+            current = c.current.asInstanceOf // !!! CC unsafe op
             currentHasNextChecked = c.currentHasNextChecked
             if (c.tail != null) {
               if (last == null) last = c.last
diff --git a/scala2-library-cc/src/scala/collection/SeqView.scala b/scala2-library-cc/src/scala/collection/SeqView.scala
index 34405e06eedb..c7af0077ce1a 100644
--- a/scala2-library-cc/src/scala/collection/SeqView.scala
+++ b/scala2-library-cc/src/scala/collection/SeqView.scala
@@ -186,12 +186,14 @@ object SeqView {
   }
 
   @SerialVersionUID(3L)
-  class Sorted[A, B >: A] private (private[this] var underlying: SomeSeqOps[A]^,
+  class Sorted[A, B >: A] private (underlying: SomeSeqOps[A]^,
                                    private[this] val len: Int,
                                    ord: Ordering[B])
     extends SeqView[A] {
     outer: Sorted[A, B]^ =>
 
+    private var myUnderlying: SomeSeqOps[A]^{underlying} = underlying
+
     // force evaluation immediately by calling `length` so infinite collections
     // hang on `sorted`/`sortWith`/`sortBy` rather than on arbitrary method calls
     def this(underlying: SomeSeqOps[A]^, ord: Ordering[B]) = this(underlying, underlying.length, ord)
@@ -221,10 +223,10 @@ object SeqView {
       val res = {
         val len = this.len
         if (len == 0) Nil
-        else if (len == 1) List(underlying.head)
+        else if (len == 1) List(myUnderlying.head)
         else {
           val arr = new Array[Any](len) // Array[Any] =:= Array[AnyRef]
-          underlying.copyToArray(arr)
+          myUnderlying.copyToArray(arr)
           java.util.Arrays.sort(arr.asInstanceOf[Array[AnyRef]], ord.asInstanceOf[Ordering[AnyRef]])
           // casting the Array[AnyRef] to Array[A] and creating an ArraySeq from it
           // is safe because:
@@ -238,12 +240,12 @@ object SeqView {
         }
       }
       evaluated = true
-      underlying = null
+      myUnderlying = null
       res
     }
 
     private[this] def elems: SomeSeqOps[A]^{this} = {
-      val orig = underlying
+      val orig = myUnderlying
       if (evaluated) _sorted else orig
     }
 
diff --git a/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala b/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala
index ac24995e6892..2f7b017a6729 100644
--- a/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala
+++ b/scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala
@@ -24,6 +24,7 @@ import scala.language.implicitConversions
 import scala.runtime.Statics
 import language.experimental.captureChecking
 import annotation.unchecked.uncheckedCaptures
+import caps.untrackedCaptures
 
 /**  This class implements an immutable linked list. We call it "lazy"
   *  because it computes its elements only when they are needed.
@@ -245,7 +246,7 @@ import annotation.unchecked.uncheckedCaptures
   *  @define evaluatesAllElements This method evaluates all elements of the collection.
   */
 @SerialVersionUID(3L)
-final class LazyListIterable[+A] private(private[this] var lazyState: () => LazyListIterable.State[A]^)
+final class LazyListIterable[+A] private(@untrackedCaptures lazyState: () => LazyListIterable.State[A]^)
   extends AbstractIterable[A]
     with Iterable[A]
     with IterableOps[A, LazyListIterable, LazyListIterable[A]]
@@ -253,6 +254,8 @@ final class LazyListIterable[+A] private(private[this] var lazyState: () => Lazy
     with Serializable {
   import LazyListIterable._
 
+  private var myLazyState = lazyState
+
   @volatile private[this] var stateEvaluated: Boolean = false
   @inline private def stateDefined: Boolean = stateEvaluated
   private[this] var midEvaluation = false
@@ -264,11 +267,11 @@ final class LazyListIterable[+A] private(private[this] var lazyState: () => Lazy
       throw new RuntimeException("self-referential LazyListIterable or a derivation thereof has no more elements")
     }
     midEvaluation = true
-    val res = try lazyState() finally midEvaluation = false
+    val res = try myLazyState() finally midEvaluation = false
     // if we set it to `true` before evaluating, we may infinite loop
     // if something expects `state` to already be evaluated
     stateEvaluated = true
-    lazyState = null // allow GC
+    myLazyState = null // allow GC
     res
   }
 
@@ -755,7 +758,7 @@ final class LazyListIterable[+A] private(private[this] var lazyState: () => Lazy
     * The iterator returned by this method mostly preserves laziness;
     * a single element ahead of the iterator is evaluated.
     */
-  override def grouped(size: Int): Iterator[LazyListIterable[A]] = {
+  override def grouped(size: Int): Iterator[LazyListIterable[A]]^{this} = {
     require(size > 0, "size must be positive, but was " + size)
     slidingImpl(size = size, step = size)
   }
@@ -765,12 +768,12 @@ final class LazyListIterable[+A] private(private[this] var lazyState: () => Lazy
     * The iterator returned by this method mostly preserves laziness;
     * `size - step max 1` elements ahead of the iterator are evaluated.
     */
-  override def sliding(size: Int, step: Int): Iterator[LazyListIterable[A]] = {
+  override def sliding(size: Int, step: Int): Iterator[LazyListIterable[A]]^{this} = {
     require(size > 0 && step > 0, s"size=$size and step=$step, but both must be positive")
     slidingImpl(size = size, step = step)
   }
 
-  @inline private def slidingImpl(size: Int, step: Int): Iterator[LazyListIterable[A]] =
+  @inline private def slidingImpl(size: Int, step: Int): Iterator[LazyListIterable[A]]^{this} =
     if (knownIsEmpty) Iterator.empty
     else new SlidingIterator[A](this, size = size, step = step)
 
@@ -996,7 +999,7 @@ object LazyListIterable extends IterableFactory[LazyListIterable] {
 
   private def filterImpl[A](ll: LazyListIterable[A]^, p: A => Boolean, isFlipped: Boolean): LazyListIterable[A]^{ll, p} = {
     // DO NOT REFERENCE `ll` ANYWHERE ELSE, OR IT WILL LEAK THE HEAD
-    var restRef: LazyListIterable[A]^{ll*} = ll  // restRef is captured by closure arg to newLL, so A is not recognized as parametric
+    var restRef: LazyListIterable[A]^{ll} = ll  // restRef is captured by closure arg to newLL, so A is not recognized as parametric
     newLL {
       var elem: A = null.asInstanceOf[A]
       var found   = false
@@ -1013,7 +1016,7 @@ object LazyListIterable extends IterableFactory[LazyListIterable] {
 
   private def collectImpl[A, B](ll: LazyListIterable[A]^, pf: PartialFunction[A, B]^): LazyListIterable[B]^{ll, pf} = {
     // DO NOT REFERENCE `ll` ANYWHERE ELSE, OR IT WILL LEAK THE HEAD
-    var restRef: LazyListIterable[A]^{ll*} = ll  // restRef is captured by closure arg to newLL, so A is not recognized as parametric
+    var restRef: LazyListIterable[A]^{ll} = ll  // restRef is captured by closure arg to newLL, so A is not recognized as parametric
     newLL {
       val marker = Statics.pfMarker
       val toMarker = anyToMarker.asInstanceOf[A => B] // safe because Function1 is erased
@@ -1032,7 +1035,7 @@ object LazyListIterable extends IterableFactory[LazyListIterable] {
 
   private def flatMapImpl[A, B](ll: LazyListIterable[A]^, f: A => IterableOnce[B]^): LazyListIterable[B]^{ll, f} = {
     // DO NOT REFERENCE `ll` ANYWHERE ELSE, OR IT WILL LEAK THE HEAD
-    var restRef: LazyListIterable[A]^{ll*} = ll  // restRef is captured by closure arg to newLL, so A is not recognized as parametric
+    var restRef: LazyListIterable[A]^{ll} = ll  // restRef is captured by closure arg to newLL, so A is not recognized as parametric
     newLL {
       var it: Iterator[B]^{ll, f} = null
       var itHasNext       = false
@@ -1056,7 +1059,7 @@ object LazyListIterable extends IterableFactory[LazyListIterable] {
 
   private def dropImpl[A](ll: LazyListIterable[A]^, n: Int): LazyListIterable[A]^{ll} = {
     // DO NOT REFERENCE `ll` ANYWHERE ELSE, OR IT WILL LEAK THE HEAD
-    var restRef: LazyListIterable[A]^{ll*} = ll    // restRef is captured by closure arg to newLL, so A is not recognized as parametric
+    var restRef: LazyListIterable[A]^{ll} = ll    // restRef is captured by closure arg to newLL, so A is not recognized as parametric
     var iRef    = n                      // val iRef    = new IntRef(n)
     newLL {
       var rest = restRef                 // var rest = restRef.elem
@@ -1073,7 +1076,7 @@ object LazyListIterable extends IterableFactory[LazyListIterable] {
 
   private def dropWhileImpl[A](ll: LazyListIterable[A]^, p: A => Boolean): LazyListIterable[A]^{ll, p} = {
     // DO NOT REFERENCE `ll` ANYWHERE ELSE, OR IT WILL LEAK THE HEAD
-    var restRef: LazyListIterable[A]^{ll*} = ll  // restRef is captured by closure arg to newLL, so A is not recognized as parametric
+    var restRef: LazyListIterable[A]^{ll} = ll  // restRef is captured by closure arg to newLL, so A is not recognized as parametric
     newLL {
       var rest = restRef                        // var rest = restRef.elem
       while (!rest.isEmpty && p(rest.head)) {
@@ -1086,8 +1089,8 @@ object LazyListIterable extends IterableFactory[LazyListIterable] {
 
   private def takeRightImpl[A](ll: LazyListIterable[A]^, n: Int): LazyListIterable[A]^{ll} = {
     // DO NOT REFERENCE `ll` ANYWHERE ELSE, OR IT WILL LEAK THE HEAD
-    var restRef: LazyListIterable[A]^{ll*} = ll  // restRef is captured by closure arg to newLL, so A is not recognized as parametric
-    var scoutRef: LazyListIterable[A]^{ll*} = ll  // same situation
+    var restRef: LazyListIterable[A]^{ll} = ll  // restRef is captured by closure arg to newLL, so A is not recognized as parametric
+    var scoutRef: LazyListIterable[A]^{ll} = ll  // same situation
     var remainingRef = n                          // val remainingRef = new IntRef(n)
     newLL {
       var scout     = scoutRef                    // var scout     = scoutRef.elem
@@ -1236,33 +1239,35 @@ object LazyListIterable extends IterableFactory[LazyListIterable] {
     */
   def newBuilder[A]: Builder[A, LazyListIterable[A]] = new LazyBuilder[A]
 
-  private class LazyIterator[+A](private[this] var lazyList: LazyListIterable[A]^) extends AbstractIterator[A] {
-    override def hasNext: Boolean = !lazyList.isEmpty
+  private class LazyIterator[+A](lazyList: LazyListIterable[A]^) extends AbstractIterator[A] {
+    private var myLazyList = lazyList
+    override def hasNext: Boolean = !myLazyList.isEmpty
 
     override def next(): A =
-      if (lazyList.isEmpty) Iterator.empty.next()
+      if (myLazyList.isEmpty) Iterator.empty.next()
       else {
-        val res = lazyList.head
-        lazyList = lazyList.tail
+        val res = myLazyList.head
+        myLazyList = myLazyList.tail
         res
       }
   }
 
-  private class SlidingIterator[A](private[this] var lazyList: LazyListIterable[A]^, size: Int, step: Int)
+  private class SlidingIterator[A](lazyList: LazyListIterable[A]^, size: Int, step: Int)
     extends AbstractIterator[LazyListIterable[A]] {
+    private var myLazyList = lazyList
     private val minLen = size - step max 0
     private var first = true
 
     def hasNext: Boolean =
-      if (first) !lazyList.isEmpty
-      else lazyList.lengthGt(minLen)
+      if (first) !myLazyList.isEmpty
+      else myLazyList.lengthGt(minLen)
 
     def next(): LazyListIterable[A] = {
       if (!hasNext) Iterator.empty.next()
       else {
         first = false
-        val list = lazyList
-        lazyList = list.drop(step)
+        val list = myLazyList
+        myLazyList = list.drop(step)
         list.take(size)
       }
     }
@@ -1281,7 +1286,7 @@ object LazyListIterable extends IterableFactory[LazyListIterable] {
     import LazyBuilder._
 
     private[this] var next: DeferredState[A] = _
-    private[this] var list: LazyListIterable[A] = _
+    @uncheckedCaptures private[this] var list: LazyListIterable[A]^ = _
 
     clear()
 
diff --git a/tests/neg-custom-args/captures/box-adapt-cases.scala b/tests/neg-custom-args/captures/box-adapt-cases.scala
index 3dac26a98318..681d699842ed 100644
--- a/tests/neg-custom-args/captures/box-adapt-cases.scala
+++ b/tests/neg-custom-args/captures/box-adapt-cases.scala
@@ -4,7 +4,7 @@ def test1(): Unit = {
   type Id[X] = [T] -> (op: X => T) -> T
 
   val x: Id[Cap^] = ???
-  x(cap => cap.use())  // was error, now OK
+  x(cap => cap.use())  // error, OK under sealed
 }
 
 def test2(io: Cap^): Unit = {
diff --git a/tests/neg-custom-args/captures/capt-test.scala b/tests/neg-custom-args/captures/capt-test.scala
index 80ee1aba84e1..b202a14d0940 100644
--- a/tests/neg-custom-args/captures/capt-test.scala
+++ b/tests/neg-custom-args/captures/capt-test.scala
@@ -20,8 +20,8 @@ def handle[E <: Exception,  R <: Top](op: (CT[E] @retains(caps.cap)) => R)(handl
   catch case ex: E => handler(ex)
 
 def test: Unit =
-  val b = handle[Exception, () => Nothing] { // error
+  val b = handle[Exception, () => Nothing] {
     (x: CanThrow[Exception]) => () => raise(new Exception)(using x)
-  } {
+  } { // error
     (ex: Exception) => ???
   }
diff --git a/tests/neg-custom-args/captures/capt1.check b/tests/neg-custom-args/captures/capt1.check
index 0e99d1876d3c..3d0ed538b2e5 100644
--- a/tests/neg-custom-args/captures/capt1.check
+++ b/tests/neg-custom-args/captures/capt1.check
@@ -1,52 +1,52 @@
--- Error: tests/neg-custom-args/captures/capt1.scala:4:11 --------------------------------------------------------------
-4 |  () => if x == null then y else y  // error
+-- Error: tests/neg-custom-args/captures/capt1.scala:6:11 --------------------------------------------------------------
+6 |  () => if x == null then y else y  // error
   |           ^
   |           (x : C^) cannot be referenced here; it is not included in the allowed capture set {}
   |           of an enclosing function literal with expected type () -> C
--- Error: tests/neg-custom-args/captures/capt1.scala:7:11 --------------------------------------------------------------
-7 |  () => if x == null then y else y  // error
+-- Error: tests/neg-custom-args/captures/capt1.scala:9:11 --------------------------------------------------------------
+9 |  () => if x == null then y else y  // error
   |           ^
   |           (x : C^) cannot be referenced here; it is not included in the allowed capture set {}
   |           of an enclosing function literal with expected type Matchable
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:14:2 -----------------------------------------
-14 |  def f(y: Int) = if x == null then y else y  // error
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:16:2 -----------------------------------------
+16 |  def f(y: Int) = if x == null then y else y  // error
    |  ^
    |  Found:    (y: Int) ->{x} Int
    |  Required: Matchable
-15 |  f
+17 |  f
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:21:2 -----------------------------------------
-21 |  class F(y: Int) extends A:   // error
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:23:2 -----------------------------------------
+23 |  class F(y: Int) extends A:   // error
    |  ^
    |  Found:    A^{x}
    |  Required: A
-22 |    def m() = if x == null then y else y
-23 |  F(22)
+24 |    def m() = if x == null then y else y
+25 |  F(22)
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:26:2 -----------------------------------------
-26 |  new A: // error
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:28:2 -----------------------------------------
+28 |  new A: // error
    |  ^
    |  Found:    A^{x}
    |  Required: A
-27 |    def m() = if x == null then y else y
+29 |    def m() = if x == null then y else y
    |
    | longer explanation available when compiling with `-explain`
--- Error: tests/neg-custom-args/captures/capt1.scala:32:12 -------------------------------------------------------------
-32 |  val z2 = h[() -> Cap](() => x) // error // error
+-- Error: tests/neg-custom-args/captures/capt1.scala:34:12 -------------------------------------------------------------
+34 |  val z2 = h[() -> Cap](() => x) // error // error
    |           ^^^^^^^^^^^^
    |           Sealed type variable X cannot be instantiated to () -> box C^ since
    |           the part box C^ of that type captures the root capability `cap`.
    |           This is often caused by a local capability in an argument of method h
    |           leaking as part of its result.
--- Error: tests/neg-custom-args/captures/capt1.scala:32:30 -------------------------------------------------------------
-32 |  val z2 = h[() -> Cap](() => x) // error // error
+-- Error: tests/neg-custom-args/captures/capt1.scala:34:30 -------------------------------------------------------------
+34 |  val z2 = h[() -> Cap](() => x) // error // error
    |                              ^
    |                            (x : C^) cannot be referenced here; it is not included in the allowed capture set {}
    |                            of an enclosing function literal with expected type () -> box C^
--- Error: tests/neg-custom-args/captures/capt1.scala:34:12 -------------------------------------------------------------
-34 |  val z3 = h[(() -> Cap) @retains(x)](() => x)(() => C())  // error
+-- Error: tests/neg-custom-args/captures/capt1.scala:36:12 -------------------------------------------------------------
+36 |  val z3 = h[(() -> Cap) @retains(x)](() => x)(() => C())  // error
    |           ^^^^^^^^^^^^^^^^^^^^^^^^^^
    |           Sealed type variable X cannot be instantiated to box () ->{x} Cap since
    |           the part Cap of that type captures the root capability `cap`.
diff --git a/tests/neg-custom-args/captures/capt1.scala b/tests/neg-custom-args/captures/capt1.scala
index 48c4d889bf8d..cad0bad4ba56 100644
--- a/tests/neg-custom-args/captures/capt1.scala
+++ b/tests/neg-custom-args/captures/capt1.scala
@@ -1,3 +1,5 @@
+//> using options -source 3.4
+// (to make sure we use the sealed policy)
 import annotation.retains
 class C
 def f(x: C @retains(caps.cap), y: C): () -> C =
diff --git a/tests/neg-custom-args/captures/effect-swaps-explicit.check b/tests/neg-custom-args/captures/effect-swaps-explicit.check
index 8c4d1f315fd8..47559ab97568 100644
--- a/tests/neg-custom-args/captures/effect-swaps-explicit.check
+++ b/tests/neg-custom-args/captures/effect-swaps-explicit.check
@@ -1,29 +1,29 @@
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps-explicit.scala:62:8 -------------------------
-61 |      Result:
-62 |        Future: // error, type mismatch
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps-explicit.scala:64:8 -------------------------
+63 |      Result:
+64 |        Future: // error, type mismatch
    |      ^
    |      Found:    Result.Ok[box Future[box T^?]^{fr, contextual$1}]
    |      Required: Result[Future[T], Nothing]
-63 |          fr.await.ok
+65 |          fr.await.ok
    |--------------------------------------------------------------------------------------------------------------------
    |Inline stack trace
    |- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
-   |This location contains code that was inlined from effect-swaps-explicit.scala:39
-39 |    boundary(Ok(body))
+   |This location contains code that was inlined from effect-swaps-explicit.scala:41
+41 |    boundary(Ok(body))
    |             ^^^^^^^^
     --------------------------------------------------------------------------------------------------------------------
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps-explicit.scala:72:10 ------------------------
-72 |          Future: fut ?=> // error: type mismatch
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps-explicit.scala:74:10 ------------------------
+74 |          Future: fut ?=> // error: type mismatch
    |          ^
    |          Found:    Future[box T^?]^{fr, lbl}
    |          Required: Future[box T^?]^?
-73 |            fr.await.ok
+75 |            fr.await.ok
    |
    | longer explanation available when compiling with `-explain`
--- Error: tests/neg-custom-args/captures/effect-swaps-explicit.scala:66:15 ---------------------------------------------
-66 |        Result.make: //lbl ?=> // error, escaping label from Result
+-- Error: tests/neg-custom-args/captures/effect-swaps-explicit.scala:68:15 ---------------------------------------------
+68 |        Result.make: //lbl ?=> // error, escaping label from Result
    |        ^^^^^^^^^^^
    |local reference contextual$9 from (using contextual$9: boundary.Label[Result[box Future[box T^?]^{fr, contextual$9}, box E^?]]^):
    |  box Future[box T^?]^{fr, contextual$9} leaks into outer capture set of type parameter T of method make in object Result
diff --git a/tests/neg-custom-args/captures/effect-swaps-explicit.scala b/tests/neg-custom-args/captures/effect-swaps-explicit.scala
index 052beaab01b2..7474e1711b34 100644
--- a/tests/neg-custom-args/captures/effect-swaps-explicit.scala
+++ b/tests/neg-custom-args/captures/effect-swaps-explicit.scala
@@ -1,3 +1,5 @@
+//> using options -source 3.4
+// (to make sure we use the sealed policy)
 object boundary:
 
   final class Label[-T] // extends caps.Capability
diff --git a/tests/neg-custom-args/captures/filevar.scala b/tests/neg-custom-args/captures/filevar.scala
index 0d9cbed164e3..2859f4c5e826 100644
--- a/tests/neg-custom-args/captures/filevar.scala
+++ b/tests/neg-custom-args/captures/filevar.scala
@@ -6,7 +6,7 @@ class File:
 
 class Service:
   var file: File^ = uninitialized  // error
-  def log = file.write("log")
+  def log = file.write("log") // error, was OK under sealed
 
 def withFile[T](op: (l: caps.Capability) ?-> (f: File^{l}) => T): T =
   op(using caps.cap)(new File)
diff --git a/tests/neg-custom-args/captures/i15749.scala b/tests/neg-custom-args/captures/i15749.scala
new file mode 100644
index 000000000000..c5b59042085a
--- /dev/null
+++ b/tests/neg-custom-args/captures/i15749.scala
@@ -0,0 +1,15 @@
+class Unit
+object unit extends Unit
+
+type Top = Any^
+
+type LazyVal[T] = Unit => T
+
+class Foo[T](val x: T)
+
+// Foo[□ Unit => T]
+type BoxedLazyVal[T] = Foo[LazyVal[T]]
+
+def force[A](v: BoxedLazyVal[A]): A =
+  // Γ ⊢ v.x : □ {cap} Unit -> A
+  v.x(unit)  // error: (unbox v.x)(unit), was ok under the sealed policy
\ No newline at end of file
diff --git a/tests/neg-custom-args/captures/i15772.check b/tests/neg-custom-args/captures/i15772.check
index 0f8f0bf6eac5..58582423b101 100644
--- a/tests/neg-custom-args/captures/i15772.check
+++ b/tests/neg-custom-args/captures/i15772.check
@@ -25,11 +25,11 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15772.scala:33:34 ---------------------------------------
 33 |  val boxed2 : Observe[C]^ = box2(c) // error
    |                                  ^
-   |                                  Found:    box C^
-   |                                  Required: box C{val arg: C^?}^?
+   |                                  Found:    C^
+   |                                  Required: box C{val arg: C^?}^
    |
-   |                                  Note that the universal capability `cap`
-   |                                  cannot be included in capture set ?
+   |                                  Note that C^ cannot be box-converted to box C{val arg: C^?}^
+   |                                  since at least one of their capture sets contains the root capability `cap`
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15772.scala:44:2 ----------------------------------------
diff --git a/tests/neg-custom-args/captures/i15922.scala b/tests/neg-custom-args/captures/i15922.scala
index 974870cd769c..89bf91493fcd 100644
--- a/tests/neg-custom-args/captures/i15922.scala
+++ b/tests/neg-custom-args/captures/i15922.scala
@@ -1,3 +1,5 @@
+//> using options -source 3.4
+// (to force sealed encapsulation checking)
 trait Cap { def use(): Int }
 type Id[X] = [T] -> (op: X => T) -> T
 def mkId[X](x: X): Id[X] = [T] => (op: X => T) => op(x)
diff --git a/tests/neg-custom-args/captures/i15923-cases.scala b/tests/neg-custom-args/captures/i15923-cases.scala
new file mode 100644
index 000000000000..83cfa554e8b9
--- /dev/null
+++ b/tests/neg-custom-args/captures/i15923-cases.scala
@@ -0,0 +1,7 @@
+trait Cap { def use(): Int }
+type Id[X] = [T] -> (op: X => T) -> T
+def mkId[X](x: X): Id[X] = [T] => (op: X => T) => op(x)
+
+def foo(x: Id[Cap^]) = {
+  x(_.use())  // error, was OK under sealed policy
+}
diff --git a/tests/neg-custom-args/captures/i16114.scala b/tests/neg-custom-args/captures/i16114.scala
index d363bb665dc3..ec04fe9c9827 100644
--- a/tests/neg-custom-args/captures/i16114.scala
+++ b/tests/neg-custom-args/captures/i16114.scala
@@ -1,3 +1,5 @@
+//> using options -source 3.4
+// (to make sure we use the sealed policy)
 trait Cap { def use(): Int; def close(): Unit }
 def mkCap(): Cap^ = ???
 
diff --git a/tests/neg-custom-args/captures/i19330-alt2.scala b/tests/neg-custom-args/captures/i19330-alt2.scala
index b49dce4b71ef..86634b45dbe3 100644
--- a/tests/neg-custom-args/captures/i19330-alt2.scala
+++ b/tests/neg-custom-args/captures/i19330-alt2.scala
@@ -1,3 +1,5 @@
+//> using options -source 3.4
+// (to make sure we use the sealed policy)
 import language.experimental.captureChecking
 
 trait Logger
diff --git a/tests/neg-custom-args/captures/i19330.scala b/tests/neg-custom-args/captures/i19330.scala
index 8acb0dd8f66b..5fbdc00db311 100644
--- a/tests/neg-custom-args/captures/i19330.scala
+++ b/tests/neg-custom-args/captures/i19330.scala
@@ -1,3 +1,5 @@
+//> using options -source 3.4
+// (to force sealed encapsulation checking)
 import language.experimental.captureChecking
 
 trait Logger
diff --git a/tests/neg-custom-args/captures/lazylists-exceptions.check b/tests/neg-custom-args/captures/lazylists-exceptions.check
index 3095c1f2f4f9..4a8738118609 100644
--- a/tests/neg-custom-args/captures/lazylists-exceptions.check
+++ b/tests/neg-custom-args/captures/lazylists-exceptions.check
@@ -1,9 +1,8 @@
 -- Error: tests/neg-custom-args/captures/lazylists-exceptions.scala:36:2 -----------------------------------------------
 36 |  try // error
    |  ^
-   |  result of `try` cannot have type LazyList[Int]^ since
-   |  that type captures the root capability `cap`.
-   |  This is often caused by a locally generated exception capability leaking as part of its result.
+   |  The expression's type LazyList[Int]^ is not allowed to capture the root capability `cap`.
+   |  This usually means that a capability persists longer than its allowed lifetime.
 37 |    tabulate(10) { i =>
 38 |      if i > 9 then throw Ex1()
 39 |      i * i
diff --git a/tests/neg-custom-args/captures/levels.check b/tests/neg-custom-args/captures/levels.check
index 479a231a0404..2dae3ec3bbc6 100644
--- a/tests/neg-custom-args/captures/levels.check
+++ b/tests/neg-custom-args/captures/levels.check
@@ -1,12 +1,12 @@
--- Error: tests/neg-custom-args/captures/levels.scala:17:13 ------------------------------------------------------------
-17 |  val _ = Ref[String => String]((x: String) => x) // error
+-- Error: tests/neg-custom-args/captures/levels.scala:19:13 ------------------------------------------------------------
+19 |  val _ = Ref[String => String]((x: String) => x) // error
    |          ^^^^^^^^^^^^^^^^^^^^^
    |          Sealed type variable T cannot be instantiated to box String => String since
    |          that type captures the root capability `cap`.
    |          This is often caused by a local capability in an argument of constructor Ref
    |          leaking as part of its result.
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/levels.scala:22:11 ---------------------------------------
-22 |    r.setV(g) // error
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/levels.scala:24:11 ---------------------------------------
+24 |    r.setV(g) // error
    |           ^
    |           Found:    box (x: String) ->{cap3} String
    |           Required: box (x$0: String) ->? String
diff --git a/tests/neg-custom-args/captures/levels.scala b/tests/neg-custom-args/captures/levels.scala
index b28e87f03ef7..4709fd80d9b8 100644
--- a/tests/neg-custom-args/captures/levels.scala
+++ b/tests/neg-custom-args/captures/levels.scala
@@ -1,3 +1,5 @@
+//> using options -source 3.4
+// (to make sure we use the sealed policy)
 class CC
 
 def test1(cap1: CC^) =
diff --git a/tests/neg-custom-args/captures/outer-var.check b/tests/neg-custom-args/captures/outer-var.check
index d57d615cda64..ee32c3ce03f2 100644
--- a/tests/neg-custom-args/captures/outer-var.check
+++ b/tests/neg-custom-args/captures/outer-var.check
@@ -1,8 +1,8 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/outer-var.scala:11:8 -------------------------------------
 11 |    x = q           // error
    |        ^
-   |        Found:    (q : Proc)
-   |        Required: () ->{p, q²} Unit
+   |        Found:    box () ->{q} Unit
+   |        Required: box () ->{p, q²} Unit
    |
    |        where:    q  is a parameter in method inner
    |                  q² is a parameter in method test
@@ -12,14 +12,17 @@
 12 |    x = (q: Proc)   // error
    |         ^^^^^^^
    |         Found:    Proc
-   |         Required: () ->{p, q} Unit
+   |         Required: box () ->{p, q} Unit
+   |
+   |         Note that () => Unit cannot be box-converted to box () ->{p, q} Unit
+   |         since at least one of their capture sets contains the root capability `cap`
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/outer-var.scala:13:9 -------------------------------------
 13 |    y = (q: Proc)   // error
    |         ^^^^^^^
    |         Found:    Proc
-   |         Required: () ->{p} Unit
+   |         Required: box () ->{p} Unit
    |
    |         Note that the universal capability `cap`
    |         cannot be included in capture set {p} of variable y
@@ -28,17 +31,20 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/outer-var.scala:14:8 -------------------------------------
 14 |    y = q           // error
    |        ^
-   |        Found:    (q : Proc)
-   |        Required: () ->{p} Unit
+   |        Found:    box () ->{q} Unit
+   |        Required: box () ->{p} Unit
    |
    |        Note that reference (q : Proc), defined in method inner
    |        cannot be included in outer capture set {p} of variable y
    |
    | longer explanation available when compiling with `-explain`
--- Error: tests/neg-custom-args/captures/outer-var.scala:16:53 ---------------------------------------------------------
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/outer-var.scala:16:65 ------------------------------------
 16 |  var finalizeActions = collection.mutable.ListBuffer[() => Unit]() // error
-   |                        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-   |                        Sealed type variable A cannot be instantiated to box () => Unit since
-   |                        that type captures the root capability `cap`.
-   |                        This is often caused by a local capability in an argument of method apply
-   |                        leaking as part of its result.
+   |                        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   |                        Found:    scala.collection.mutable.ListBuffer[box () => Unit]
+   |                        Required: box scala.collection.mutable.ListBuffer[box () ->? Unit]^?
+   |
+   |                        Note that the universal capability `cap`
+   |                        cannot be included in capture set ? of variable finalizeActions
+   |
+   | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/reaches.check b/tests/neg-custom-args/captures/reaches.check
index 45c1776d8c43..f20dbdf311ad 100644
--- a/tests/neg-custom-args/captures/reaches.check
+++ b/tests/neg-custom-args/captures/reaches.check
@@ -1,12 +1,12 @@
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:21:11 --------------------------------------
-21 |    cur = (() => f.write()) :: Nil // error since {f*} !<: {xs*}
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:23:11 --------------------------------------
+23 |    cur = (() => f.write()) :: Nil // error since {f*} !<: {xs*}
    |           ^^^^^^^^^^^^^^^^^^^^^^^
    |           Found:    List[box () ->{f} Unit]
    |           Required: List[box () ->{xs*} Unit]
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:32:7 ---------------------------------------
-32 |      (() => f.write()) :: Nil // error since {f*} !<: {xs*}
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:34:7 ---------------------------------------
+34 |      (() => f.write()) :: Nil // error since {f*} !<: {xs*}
    |       ^^^^^^^^^^^^^^^^^^^^^^^
    |       Found:    List[box () ->{f} Unit]
    |       Required: box List[box () ->{xs*} Unit]^?
@@ -15,34 +15,34 @@
    |       cannot be included in outer capture set {xs*} of value cur
    |
    | longer explanation available when compiling with `-explain`
--- Error: tests/neg-custom-args/captures/reaches.scala:35:6 ------------------------------------------------------------
-35 |  var cur: List[Proc] = xs // error: Illegal type for var
+-- Error: tests/neg-custom-args/captures/reaches.scala:37:6 ------------------------------------------------------------
+37 |  var cur: List[Proc] = xs // error: Illegal type for var
    |      ^
    |      Mutable variable cur cannot have type List[box () => Unit] since
    |      the part box () => Unit of that type captures the root capability `cap`.
--- Error: tests/neg-custom-args/captures/reaches.scala:42:15 -----------------------------------------------------------
-42 |  val cur = Ref[List[Proc]](xs) // error: illegal type for type argument to Ref
+-- Error: tests/neg-custom-args/captures/reaches.scala:44:15 -----------------------------------------------------------
+44 |  val cur = Ref[List[Proc]](xs) // error: illegal type for type argument to Ref
    |            ^^^^^^^^^^^^^^^
    |            Sealed type variable T cannot be instantiated to List[box () => Unit] since
    |            the part box () => Unit of that type captures the root capability `cap`.
    |            This is often caused by a local capability in an argument of constructor Ref
    |            leaking as part of its result.
--- Error: tests/neg-custom-args/captures/reaches.scala:52:31 -----------------------------------------------------------
-52 |  val id: Id[Proc, Proc] = new Id[Proc, () -> Unit] // error
+-- Error: tests/neg-custom-args/captures/reaches.scala:54:31 -----------------------------------------------------------
+54 |  val id: Id[Proc, Proc] = new Id[Proc, () -> Unit] // error
    |                               ^^^^^^^^^^^^^^^^^^^^
    |                               Sealed type variable A cannot be instantiated to box () => Unit since
    |                               that type captures the root capability `cap`.
    |                               This is often caused by a local capability in an argument of constructor Id
    |                               leaking as part of its result.
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:61:27 --------------------------------------
-61 |    val f1: File^{id*} = id(f) // error, since now id(f): File^
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:63:27 --------------------------------------
+63 |    val f1: File^{id*} = id(f) // error, since now id(f): File^
    |                         ^^^^^
    |                         Found:    File^{id, f}
    |                         Required: File^{id*}
    |
    | longer explanation available when compiling with `-explain`
--- Error: tests/neg-custom-args/captures/reaches.scala:78:5 ------------------------------------------------------------
-78 |  ps.map((x, y) => compose1(x, y)) // error: cannot mix cap and * (should work now)
+-- Error: tests/neg-custom-args/captures/reaches.scala:80:5 ------------------------------------------------------------
+80 |  ps.map((x, y) => compose1(x, y)) // error: cannot mix cap and * (should work now)
    |  ^^^^^^
    |  Reach capability cap and universal capability cap cannot both
    |  appear in the type [B](f: ((box A ->{ps*} A, box A ->{ps*} A)) => B): List[B] of this expression
diff --git a/tests/neg-custom-args/captures/reaches.scala b/tests/neg-custom-args/captures/reaches.scala
index 6a5ffd51c2c6..eadb76c69e5b 100644
--- a/tests/neg-custom-args/captures/reaches.scala
+++ b/tests/neg-custom-args/captures/reaches.scala
@@ -1,3 +1,5 @@
+//> using options -source 3.4
+// (to make sure we use the sealed policy)
 class File:
   def write(): Unit = ???
 
diff --git a/tests/neg-custom-args/captures/real-try.check b/tests/neg-custom-args/captures/real-try.check
index 50dcc16f5f54..7f8ab50bc222 100644
--- a/tests/neg-custom-args/captures/real-try.check
+++ b/tests/neg-custom-args/captures/real-try.check
@@ -1,46 +1,46 @@
--- [E190] Potential Issue Warning: tests/neg-custom-args/captures/real-try.scala:36:4 ----------------------------------
-36 |  b.x
+-- [E190] Potential Issue Warning: tests/neg-custom-args/captures/real-try.scala:38:4 ----------------------------------
+38 |  b.x
    |  ^^^
    |  Discarded non-Unit value of type () -> Unit. You may want to use `()`.
    |
    | longer explanation available when compiling with `-explain`
--- Error: tests/neg-custom-args/captures/real-try.scala:12:2 -----------------------------------------------------------
-12 |  try  // error
+-- Error: tests/neg-custom-args/captures/real-try.scala:14:2 -----------------------------------------------------------
+14 |  try  // error
    |  ^
    |  result of `try` cannot have type () => Unit since
    |  that type captures the root capability `cap`.
    |  This is often caused by a locally generated exception capability leaking as part of its result.
-13 |    () => foo(1)
-14 |  catch
-15 |    case _: Ex1 => ???
-16 |    case _: Ex2 => ???
--- Error: tests/neg-custom-args/captures/real-try.scala:18:10 ----------------------------------------------------------
-18 |  val x = try // error
+15 |    () => foo(1)
+16 |  catch
+17 |    case _: Ex1 => ???
+18 |    case _: Ex2 => ???
+-- Error: tests/neg-custom-args/captures/real-try.scala:20:10 ----------------------------------------------------------
+20 |  val x = try // error
    |          ^
    |          result of `try` cannot have type () => Unit since
    |          that type captures the root capability `cap`.
    |          This is often caused by a locally generated exception capability leaking as part of its result.
-19 |    () => foo(1)
-20 |  catch
-21 |    case _: Ex1 => ???
-22 |    case _: Ex2 => ???
--- Error: tests/neg-custom-args/captures/real-try.scala:24:10 ----------------------------------------------------------
-24 |  val y = try  // error
+21 |    () => foo(1)
+22 |  catch
+23 |    case _: Ex1 => ???
+24 |    case _: Ex2 => ???
+-- Error: tests/neg-custom-args/captures/real-try.scala:26:10 ----------------------------------------------------------
+26 |  val y = try  // error
    |          ^
    |          result of `try` cannot have type () => Cell[Unit]^? since
    |          that type captures the root capability `cap`.
    |          This is often caused by a locally generated exception capability leaking as part of its result.
-25 |    () => Cell(foo(1))
-26 |  catch
-27 |    case _: Ex1 => ???
-28 |    case _: Ex2 => ???
--- Error: tests/neg-custom-args/captures/real-try.scala:30:10 ----------------------------------------------------------
-30 |  val b = try // error
+27 |    () => Cell(foo(1))
+28 |  catch
+29 |    case _: Ex1 => ???
+30 |    case _: Ex2 => ???
+-- Error: tests/neg-custom-args/captures/real-try.scala:32:10 ----------------------------------------------------------
+32 |  val b = try // error
    |          ^
    |          result of `try` cannot have type Cell[box () => Unit]^? since
    |          the part box () => Unit of that type captures the root capability `cap`.
    |          This is often caused by a locally generated exception capability leaking as part of its result.
-31 |    Cell(() => foo(1))
-32 |  catch
-33 |    case _: Ex1 => ???
-34 |    case _: Ex2 => ???
+33 |    Cell(() => foo(1))
+34 |  catch
+35 |    case _: Ex1 => ???
+36 |    case _: Ex2 => ???
diff --git a/tests/neg-custom-args/captures/real-try.scala b/tests/neg-custom-args/captures/real-try.scala
index 23961e884ea3..51f1a0fdea5a 100644
--- a/tests/neg-custom-args/captures/real-try.scala
+++ b/tests/neg-custom-args/captures/real-try.scala
@@ -1,3 +1,5 @@
+//> using options -source 3.4
+// (to make sure we use the sealed policy)
 import language.experimental.saferExceptions
 
 class Ex1 extends Exception("Ex1")
diff --git a/tests/neg-custom-args/captures/try.check b/tests/neg-custom-args/captures/try.check
index 3b96927de738..77a5fc06e05a 100644
--- a/tests/neg-custom-args/captures/try.check
+++ b/tests/neg-custom-args/captures/try.check
@@ -1,10 +1,12 @@
--- Error: tests/neg-custom-args/captures/try.scala:23:16 ---------------------------------------------------------------
-23 |  val a = handle[Exception, CanThrow[Exception]] {  // error
-   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-   |          Sealed type variable R cannot be instantiated to box CT[Exception]^ since
-   |          that type captures the root capability `cap`.
-   |          This is often caused by a local capability in an argument of method handle
-   |          leaking as part of its result.
+-- Error: tests/neg-custom-args/captures/try.scala:25:3 ----------------------------------------------------------------
+23 |  val a = handle[Exception, CanThrow[Exception]] {
+24 |    (x: CanThrow[Exception]) => x
+25 |  }{  // error (but could be better)
+   |          ^
+   |          The expression's type box CT[Exception]^ is not allowed to capture the root capability `cap`.
+   |          This usually means that a capability persists longer than its allowed lifetime.
+26 |    (ex: Exception) => ???
+27 |  }
 -- Error: tests/neg-custom-args/captures/try.scala:30:65 ---------------------------------------------------------------
 30 |    (x: CanThrow[Exception]) => () => raise(new Exception)(using x) // error
    |                                                                 ^
diff --git a/tests/neg-custom-args/captures/try.scala b/tests/neg-custom-args/captures/try.scala
index 3d25dff4cd2c..45a1b346a512 100644
--- a/tests/neg-custom-args/captures/try.scala
+++ b/tests/neg-custom-args/captures/try.scala
@@ -20,9 +20,9 @@ def handle[E <: Exception,  R <: Top](op: CT[E]^ => R)(handler: E => R): R =
   catch case ex: E => handler(ex)
 
 def test =
-  val a = handle[Exception, CanThrow[Exception]] {  // error
+  val a = handle[Exception, CanThrow[Exception]] {
     (x: CanThrow[Exception]) => x
-  }{
+  }{  // error (but could be better)
     (ex: Exception) => ???
   }
 
diff --git a/tests/neg/unsound-reach-2.scala b/tests/neg-custom-args/captures/unsound-reach-2.scala
similarity index 89%
rename from tests/neg/unsound-reach-2.scala
rename to tests/neg-custom-args/captures/unsound-reach-2.scala
index 083cec6ee5b2..384af31ee1fc 100644
--- a/tests/neg/unsound-reach-2.scala
+++ b/tests/neg-custom-args/captures/unsound-reach-2.scala
@@ -1,3 +1,5 @@
+//> using options -source 3.4
+// (to make sure we use the sealed policy)
 import language.experimental.captureChecking
 trait Consumer[-T]:
   def apply(x: T): Unit
diff --git a/tests/neg/unsound-reach-3.scala b/tests/neg-custom-args/captures/unsound-reach-3.scala
similarity index 89%
rename from tests/neg/unsound-reach-3.scala
rename to tests/neg-custom-args/captures/unsound-reach-3.scala
index 71c27fe5007d..985beb7ae55d 100644
--- a/tests/neg/unsound-reach-3.scala
+++ b/tests/neg-custom-args/captures/unsound-reach-3.scala
@@ -1,3 +1,5 @@
+//> using options -source 3.4
+// (to make sure we use the sealed policy)
 import language.experimental.captureChecking
 trait File:
   def close(): Unit
diff --git a/tests/neg/unsound-reach-4.check b/tests/neg-custom-args/captures/unsound-reach-4.check
similarity index 55%
rename from tests/neg/unsound-reach-4.check
rename to tests/neg-custom-args/captures/unsound-reach-4.check
index 47256baf408a..9abf86c772d5 100644
--- a/tests/neg/unsound-reach-4.check
+++ b/tests/neg-custom-args/captures/unsound-reach-4.check
@@ -1,5 +1,5 @@
--- Error: tests/neg/unsound-reach-4.scala:20:19 ------------------------------------------------------------------------
-20 |    escaped = boom.use(f)  // error
+-- Error: tests/neg-custom-args/captures/unsound-reach-4.scala:22:19 ---------------------------------------------------
+22 |    escaped = boom.use(f)  // error
    |              ^^^^^^^^
    |              Reach capability backdoor* and universal capability cap cannot both
    |              appear in the type (x: F): box File^{backdoor*} of this expression
diff --git a/tests/neg/unsound-reach-4.scala b/tests/neg-custom-args/captures/unsound-reach-4.scala
similarity index 85%
rename from tests/neg/unsound-reach-4.scala
rename to tests/neg-custom-args/captures/unsound-reach-4.scala
index fa395fa117ca..14050b4afff2 100644
--- a/tests/neg/unsound-reach-4.scala
+++ b/tests/neg-custom-args/captures/unsound-reach-4.scala
@@ -1,3 +1,5 @@
+//> using options -source 3.4
+// (to make sure we use the sealed policy)
 import language.experimental.captureChecking
 trait File:
   def close(): Unit
diff --git a/tests/neg-custom-args/captures/unsound-reach.check b/tests/neg-custom-args/captures/unsound-reach.check
new file mode 100644
index 000000000000..22b00b74deb1
--- /dev/null
+++ b/tests/neg-custom-args/captures/unsound-reach.check
@@ -0,0 +1,12 @@
+-- Error: tests/neg-custom-args/captures/unsound-reach.scala:18:13 -----------------------------------------------------
+18 |        boom.use(f): (f1: File^{backdoor*}) => // error
+   |        ^^^^^^^^
+   |        Reach capability backdoor* and universal capability cap cannot both
+   |        appear in the type (x: File^)(op: box File^{backdoor*} => Unit): Unit of this expression
+-- [E164] Declaration Error: tests/neg-custom-args/captures/unsound-reach.scala:10:8 -----------------------------------
+10 |    def use(x: File^)(op: File^ => Unit): Unit = op(x) // error, was OK using sealed checking
+   |        ^
+   |        error overriding method use in trait Foo of type (x: File^)(op: box File^ => Unit): Unit;
+   |          method use of type (x: File^)(op: File^ => Unit): Unit has incompatible type
+   |
+   | longer explanation available when compiling with `-explain`
diff --git a/tests/neg/unsound-reach.scala b/tests/neg-custom-args/captures/unsound-reach.scala
similarity index 83%
rename from tests/neg/unsound-reach.scala
rename to tests/neg-custom-args/captures/unsound-reach.scala
index 48a74f86d311..c3c31a7f32ff 100644
--- a/tests/neg/unsound-reach.scala
+++ b/tests/neg-custom-args/captures/unsound-reach.scala
@@ -7,7 +7,7 @@ def withFile[R](path: String)(op: File^ => R): R = ???
 trait Foo[+X]:
     def use(x: File^)(op: X => Unit): Unit
 class Bar extends Foo[File^]:
-    def use(x: File^)(op: File^ => Unit): Unit = op(x)
+    def use(x: File^)(op: File^ => Unit): Unit = op(x) // error, was OK using sealed checking
 
 def bad(): Unit =
     val backdoor: Foo[File^] = new Bar
diff --git a/tests/neg-custom-args/captures/vars-simple.check b/tests/neg-custom-args/captures/vars-simple.check
index 2bc014e9a4e7..2ef301b6ec1f 100644
--- a/tests/neg-custom-args/captures/vars-simple.check
+++ b/tests/neg-custom-args/captures/vars-simple.check
@@ -2,14 +2,17 @@
 15 |    a = (g: String => String)      // error
    |         ^^^^^^^^^^^^^^^^^^^
    |         Found:    String => String
-   |         Required: String ->{cap1, cap2} String
+   |         Required: box String ->{cap1, cap2} String
+   |
+   |         Note that String => String cannot be box-converted to box String ->{cap1, cap2} String
+   |         since at least one of their capture sets contains the root capability `cap`
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/vars-simple.scala:16:8 -----------------------------------
 16 |    a = g  // error
    |        ^
-   |        Found:    (x: String) ->{cap3} String
-   |        Required: (x: String) ->{cap1, cap2} String
+   |        Found:    box (x: String) ->{cap3} String
+   |        Required: box (x: String) ->{cap1, cap2} String
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/vars-simple.scala:17:12 ----------------------------------
diff --git a/tests/neg-custom-args/captures/vars.check b/tests/neg-custom-args/captures/vars.check
index e2d817f2d8bd..e4b1e71a2000 100644
--- a/tests/neg-custom-args/captures/vars.check
+++ b/tests/neg-custom-args/captures/vars.check
@@ -1,12 +1,12 @@
--- Error: tests/neg-custom-args/captures/vars.scala:22:14 --------------------------------------------------------------
-22 |    a = x => g(x)      // error
+-- Error: tests/neg-custom-args/captures/vars.scala:24:14 --------------------------------------------------------------
+24 |    a = x => g(x)      // error
    |             ^^^^
    |             reference (cap3 : Cap) is not included in the allowed capture set {cap1} of variable a
    |
    |             Note that reference (cap3 : Cap), defined in method scope
    |             cannot be included in outer capture set {cap1} of variable a
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/vars.scala:23:8 ------------------------------------------
-23 |    a = g      // error
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/vars.scala:25:8 ------------------------------------------
+25 |    a = g      // error
    |        ^
    |        Found:    (x: String) ->{cap3} String
    |        Required: (x$0: String) ->{cap1} String
@@ -15,14 +15,14 @@
    |        cannot be included in outer capture set {cap1} of variable a
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/vars.scala:25:12 -----------------------------------------
-25 |    b = List(g) // error
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/vars.scala:27:12 -----------------------------------------
+27 |    b = List(g) // error
    |        ^^^^^^^
    |        Found:    List[box (x$0: String) ->{cap3} String]
    |        Required: List[box String ->{cap1, cap2} String]
    |
    | longer explanation available when compiling with `-explain`
--- Error: tests/neg-custom-args/captures/vars.scala:34:2 ---------------------------------------------------------------
-34 |  local { cap3 => // error
+-- Error: tests/neg-custom-args/captures/vars.scala:36:2 ---------------------------------------------------------------
+36 |  local { cap3 => // error
    |  ^^^^^
    |  local reference cap3 leaks into outer capture set of type parameter T of method local
diff --git a/tests/neg-custom-args/captures/vars.scala b/tests/neg-custom-args/captures/vars.scala
index ab5a2f43acc7..5eb1e3fedda9 100644
--- a/tests/neg-custom-args/captures/vars.scala
+++ b/tests/neg-custom-args/captures/vars.scala
@@ -1,3 +1,5 @@
+//> using options -source 3.4
+// (to make sure we use the sealed policy)
 class CC
 type Cap = CC^
 
diff --git a/tests/neg/unsound-reach.check b/tests/neg/unsound-reach.check
deleted file mode 100644
index 8cabbe1571a0..000000000000
--- a/tests/neg/unsound-reach.check
+++ /dev/null
@@ -1,5 +0,0 @@
--- Error: tests/neg/unsound-reach.scala:18:13 --------------------------------------------------------------------------
-18 |        boom.use(f): (f1: File^{backdoor*}) => // error
-   |        ^^^^^^^^
-   |        Reach capability backdoor* and universal capability cap cannot both
-   |        appear in the type (x: File^)(op: box File^{backdoor*} => Unit): Unit of this expression
diff --git a/tests/pos-custom-args/captures/casts.scala b/tests/pos-custom-args/captures/casts.scala
new file mode 100644
index 000000000000..572b58d008f6
--- /dev/null
+++ b/tests/pos-custom-args/captures/casts.scala
@@ -0,0 +1,4 @@
+import language.experimental.captureChecking
+def Test =
+  val x: Any = ???
+  val y = x.asInstanceOf[Int => Int]
diff --git a/tests/pos-custom-args/captures/filevar-expanded.scala b/tests/pos-custom-args/captures/filevar-expanded.scala
index 13051994f346..a883471e8d2e 100644
--- a/tests/pos-custom-args/captures/filevar-expanded.scala
+++ b/tests/pos-custom-args/captures/filevar-expanded.scala
@@ -32,5 +32,6 @@ object test2:
   def test(io3: IO^) =
     withFile(io3): f =>
       val o = Service(io3)
-      o.file = f
+      o.file = f  // this is a bit dubious. It's legal since we treat class refinements
+                  // as capture set variables that can be made to include refs coming from outside.
       o.log
diff --git a/tests/pos-custom-args/captures/i15749.scala b/tests/pos-custom-args/captures/i15749.scala
index 0a552ae1a3c5..58274c7cc817 100644
--- a/tests/pos-custom-args/captures/i15749.scala
+++ b/tests/pos-custom-args/captures/i15749.scala
@@ -1,3 +1,5 @@
+//> using options -source 3.4
+// (to make sure we use the sealed policy)
 class Unit
 object unit extends Unit
 
@@ -12,4 +14,4 @@ type BoxedLazyVal[T] = Foo[LazyVal[T]]
 
 def force[A](v: BoxedLazyVal[A]): A =
   // Γ ⊢ v.x : □ {cap} Unit -> A
-  v.x(unit)  // was error: (unbox v.x)(unit), where (unbox v.x) should be untypable, now ok
\ No newline at end of file
+  v.x(unit)  // should be error: (unbox v.x)(unit), where (unbox v.x) should be untypable, now ok
\ No newline at end of file
diff --git a/tests/pos-custom-args/captures/i15923-cases.scala b/tests/pos-custom-args/captures/i15923-cases.scala
index 7c5635f7b3dd..4b5a36f208ec 100644
--- a/tests/pos-custom-args/captures/i15923-cases.scala
+++ b/tests/pos-custom-args/captures/i15923-cases.scala
@@ -2,10 +2,6 @@ trait Cap { def use(): Int }
 type Id[X] = [T] -> (op: X => T) -> T
 def mkId[X](x: X): Id[X] = [T] => (op: X => T) => op(x)
 
-def foo(x: Id[Cap^]) = {
-  x(_.use())  // was error, now OK
-}
-
 def bar(io: Cap^, x: Id[Cap^{io}]) = {
   x(_.use())
 }
diff --git a/tests/pos-custom-args/captures/i15925.scala b/tests/pos-custom-args/captures/i15925.scala
index 63b6962ff9f8..1c448c7377c2 100644
--- a/tests/pos-custom-args/captures/i15925.scala
+++ b/tests/pos-custom-args/captures/i15925.scala
@@ -1,4 +1,5 @@
 import language.experimental.captureChecking
+import annotation.unchecked.uncheckedCaptures
 
 class Unit
 object u extends Unit
@@ -6,8 +7,8 @@ object u extends Unit
 type Foo[X] = [T] -> (op: X => T) -> T
 type Lazy[X] = Unit => X
 
-def force[X](fx: Foo[Lazy[X]]): X =
+def force[X](fx: Foo[Lazy[X] @uncheckedCaptures]): X =
   fx[X](f => f(u))
 
-def force2[X](fx: Foo[Unit => X]): X =
+def force2[X](fx: Foo[(Unit => X) @uncheckedCaptures]): X =
   fx[X](f => f(u))
diff --git a/tests/pos-custom-args/captures/levels.scala b/tests/pos-custom-args/captures/levels.scala
new file mode 100644
index 000000000000..cabd537442a5
--- /dev/null
+++ b/tests/pos-custom-args/captures/levels.scala
@@ -0,0 +1,23 @@
+class CC
+
+def test1(cap1: CC^) =
+
+  class Ref[T](init: T):
+    private var v: T = init
+    def setV(x: T): Unit = v = x
+    def getV: T = v
+
+def test2(cap1: CC^) =
+
+  class Ref[T](init: T):
+    private var v: T = init
+    def setV(x: T): Unit = v = x
+    def getV: T = v
+
+  val _ = Ref[String => String]((x: String) => x) // ok
+  val r = Ref((x: String) => x)
+
+  def scope(cap3: CC^) =
+    def g(x: String): String = if cap3 == cap3 then "" else "a"
+    r.setV(g) // error
+  ()
diff --git a/tests/pos-custom-args/captures/unsafe-captures.scala b/tests/pos-custom-args/captures/unsafe-captures.scala
new file mode 100644
index 000000000000..5e0144331344
--- /dev/null
+++ b/tests/pos-custom-args/captures/unsafe-captures.scala
@@ -0,0 +1,8 @@
+import annotation.unchecked.uncheckedCaptures
+class LL[+A] private (private var lazyState: (() => LL.State[A]^) @uncheckedCaptures):
+  private val res = lazyState() // without unchecked captures we get a van't unbox cap error
+
+
+object LL:
+
+  private trait State[+A]
diff --git a/tests/pos-custom-args/captures/untracked-captures.scala b/tests/pos-custom-args/captures/untracked-captures.scala
new file mode 100644
index 000000000000..7a090a5dd24f
--- /dev/null
+++ b/tests/pos-custom-args/captures/untracked-captures.scala
@@ -0,0 +1,34 @@
+import caps.untrackedCaptures
+class LL[+A] private (@untrackedCaptures lazyState: () => LL.State[A]^):
+  private val res = lazyState()
+
+
+object LL:
+
+  private trait State[+A]
+  private object State:
+    object Empty extends State[Nothing]
+
+  private def newLL[A](state: () => State[A]^): LL[A]^{state} = ???
+
+  private def sCons[A](hd: A, tl: LL[A]^): State[A]^{tl} = ???
+
+  def filterImpl[A](ll: LL[A]^, p: A => Boolean): LL[A]^{ll, p} =
+      // DO NOT REFERENCE `ll` ANYWHERE ELSE, OR IT WILL LEAK THE HEAD
+      var restRef: LL[A]^{ll} = ll  // restRef is captured by closure arg to newLL, so A is not recognized as parametric
+
+      val cl = () =>
+        var elem: A = null.asInstanceOf[A]
+        var found   = false
+        var rest    = restRef  // Without untracked captures a type ascription would be needed here
+                               // because the compiler tries to keep track of lazyState in refinements
+                               // of LL and gets confused (c.f Setup.addCaptureRefinements)
+
+        while !found do
+          found   = p(elem)
+          rest    = rest
+          restRef = rest
+        val res = if found then sCons(elem, filterImpl(rest, p)) else State.Empty
+        ??? : State[A]^{ll, p}
+      val nll = newLL(cl)
+      nll
diff --git a/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala b/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala
index 20a6a33d3e02..5443758afa72 100644
--- a/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala
+++ b/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala
@@ -552,7 +552,7 @@ object CollectionStrawMan5 {
     }
 
     def flatMap[B](f: A => IterableOnce[B]^): Iterator[B]^{this, f} = new Iterator[B] {
-      private var myCurrent: Iterator[B]^{this} = Iterator.empty
+      private var myCurrent: Iterator[B]^{this, f} = Iterator.empty
       private def current = {
         while (!myCurrent.hasNext && self.hasNext)
           myCurrent = f(self.next()).iterator