From ecf3428926d039b314dea548d68e91a7a74eb26a Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Fri, 10 Jan 2025 17:25:42 +0100
Subject: [PATCH 1/2] Fix various issues with maximal capabilities

The subsumes check mistakenly allowed any capability to subsume `cap`, since `cap` is expanded
as `caps.cap`, and by the path subcapturing rule `caps.cap <: caps`, where the capture set of
`caps` is empty. This allowed quite a few hidden errors to go through. This commit fixes the
subcapturing issue and all downstream issues caused by that fix.

In particular:

 - Don't use path comparison for `x subsumes caps.cap`

 - Don't allow an opened existential on the left of a comparison to leak into a capture set on
   the right. This would give a "leak" error later in healCaptures.

 - Print pre-cc annotated capturing types with @retains annotations with `^`. The annotation is
   already rendered as a set in this case, but the `^` was missing.

 - Don't recheck `_` right hand sides of uninitialized variables. These were handled in ways
   that broke freshness checking. The new `uninitialied` scheme does not have this problem.
---
 .../src/dotty/tools/dotc/cc/CaptureOps.scala  | 14 +++++++
 .../src/dotty/tools/dotc/cc/CaptureRef.scala  |  4 +-
 .../src/dotty/tools/dotc/cc/CaptureSet.scala  | 14 ++++---
 compiler/src/dotty/tools/dotc/cc/Setup.scala  | 14 ++++---
 .../dotty/tools/dotc/core/TypeComparer.scala  |  6 +++
 .../tools/dotc/printing/PlainPrinter.scala    |  7 +++-
 .../dotty/tools/dotc/transform/Recheck.scala  |  5 ++-
 .../captures/box-adapt-cases.check            | 14 +++++++
 .../captures/boxmap-paper.scala               | 14 ++++++-
 tests/pos-custom-args/captures/cc-cast.scala  | 12 ++++++
 .../captures/ex-fun-aliases.scala.disabled}   |  4 ++
 .../captures/i20237-explicit.scala            | 15 ++++++++
 .../captures}/i20237.scala                    |  0
 .../captures/open-existential.scala           | 15 ++++++++
 tests/pos/boxmap-paper.scala                  | 38 -------------------
 15 files changed, 120 insertions(+), 56 deletions(-)
 create mode 100644 tests/neg-custom-args/captures/box-adapt-cases.check
 create mode 100644 tests/pos-custom-args/captures/cc-cast.scala
 rename tests/{pos/cc-ex-unpack.scala => pos-custom-args/captures/ex-fun-aliases.scala.disabled} (79%)
 create mode 100644 tests/pos-custom-args/captures/i20237-explicit.scala
 rename tests/{pos => pos-custom-args/captures}/i20237.scala (100%)
 create mode 100644 tests/pos-custom-args/captures/open-existential.scala
 delete mode 100644 tests/pos/boxmap-paper.scala

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
index bc4eb92234eb..62a9fe33fc5c 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
@@ -46,6 +46,7 @@ object ccConfig:
    */
   def useSealed(using Context) =
     Feature.sourceVersion.stable != SourceVersion.`3.5`
+
 end ccConfig
 
 
@@ -629,6 +630,19 @@ class CleanupRetains(using Context) extends TypeMap:
         RetainingType(tp, Nil, byName = annot.symbol == defn.RetainsByNameAnnot)
       case _ => mapOver(tp)
 
+/** A typemap that follows aliases and keeps their transformed results if
+ *  there is a change.
+ */
+trait FollowAliasesMap(using Context) extends TypeMap:
+  var follow = true    // Used for debugging so that we can compare results with and w/o following.
+  def mapFollowingAliases(t: Type): Type =
+    val t1 = t.dealiasKeepAnnots
+    if follow && (t1 ne t) then
+      val t2 = apply(t1)
+      if t2 ne t1 then t2
+      else t
+    else mapOver(t)
+
 /** An extractor for `caps.reachCapability(ref)`, which is used to express a reach
  *  capability as a tree in a @retains annotation.
  */
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
index 9bda9102cbb8..e5beb56c6c56 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
@@ -83,7 +83,7 @@ trait CaptureRef extends TypeProxy, ValueType:
     else
       myCaptureSet = CaptureSet.Pending
       val computed = CaptureSet.ofInfo(this)
-      if !isCaptureChecking || underlying.isProvisional then
+      if !isCaptureChecking || ctx.mode.is(Mode.IgnoreCaptures) || underlying.isProvisional then
         myCaptureSet = null
       else
         myCaptureSet = computed
@@ -124,7 +124,7 @@ trait CaptureRef extends TypeProxy, ValueType:
     (this eq y)
     || this.isRootCapability
     || y.match
-        case y: TermRef =>
+        case y: TermRef if !y.isRootCapability =>
             y.prefix.match
               case ypre: CaptureRef =>
                 this.subsumes(ypre)
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index 1750e98f708a..7f4a34bab1f9 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -508,8 +508,13 @@ object CaptureSet:
           res.addToTrace(this)
 
     private def levelOK(elem: CaptureRef)(using Context): Boolean =
-      if elem.isRootCapability || Existential.isExistentialVar(elem) then
+      if elem.isRootCapability then
         !noUniversal
+      else if Existential.isExistentialVar(elem) then
+        !noUniversal
+        && !TypeComparer.isOpenedExistential(elem)
+          // Opened existentials on the left cannot be added to nested capture sets on the right
+          // of a comparison. Test case is open-existential.scala.
       else elem match
         case elem: TermRef if level.isDefined =>
           elem.prefix match
@@ -1065,13 +1070,12 @@ object CaptureSet:
 
   /** The capture set of the type underlying CaptureRef */
   def ofInfo(ref: CaptureRef)(using Context): CaptureSet = ref match
-    case ref: (TermRef | TermParamRef) if ref.isMaxCapability =>
-      if ref.isTrackableRef then ref.singletonCaptureSet
-      else CaptureSet.universal
     case ReachCapability(ref1) =>
       ref1.widen.deepCaptureSet(includeTypevars = true)
         .showing(i"Deep capture set of $ref: ${ref1.widen} = ${result}", capt)
-    case _ => ofType(ref.underlying, followResult = true)
+    case _ =>
+      if ref.isMaxCapability then ref.singletonCaptureSet
+      else ofType(ref.underlying, followResult = true)
 
   /** Capture set of a type */
   def ofType(tp: Type, followResult: Boolean)(using Context): CaptureSet =
diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala
index ebe128d7776c..7cc7e0514599 100644
--- a/compiler/src/dotty/tools/dotc/cc/Setup.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -13,7 +13,7 @@ import ast.tpd, tpd.*
 import transform.{PreRecheck, Recheck}, Recheck.*
 import CaptureSet.{IdentityCaptRefMap, IdempotentCaptRefMap}
 import Synthetics.isExcluded
-import util.{Property, SimpleIdentitySet}
+import util.SimpleIdentitySet
 import reporting.Message
 import printing.{Printer, Texts}, Texts.{Text, Str}
 import collection.mutable
@@ -40,7 +40,7 @@ trait SetupAPI:
 
 object Setup:
 
-  val name: String = "ccSetup"
+  val name: String = "setupCC"
   val description: String = "prepare compilation unit for capture checking"
 
   /** Recognizer for `res $throws exc`, returning `(res, exc)` in case of success */
@@ -192,11 +192,12 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
     *  3. Refine other class types C by adding capture set variables to their parameter getters
     *     (see addCaptureRefinements), provided `refine` is true.
     *  4. Add capture set variables to all types that can be tracked
+    *  5. Perform normalizeCaptures
     *
     *  Polytype bounds are only cleaned using step 1, but not otherwise transformed.
     */
   private def transformInferredType(tp: Type)(using Context): Type =
-    def mapInferred(refine: Boolean): TypeMap = new TypeMap:
+    def mapInferred(refine: Boolean): TypeMap = new TypeMap with FollowAliasesMap:
       override def toString = "map inferred"
 
       /** Refine a possibly applied class type C where the class has tracked parameters
@@ -299,9 +300,10 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
    *   3. Add universal capture sets to types deriving from Capability
    *   4. Map `cap` in function result types to existentially bound variables.
    *   5. Schedule deferred well-formed tests for types with retains annotations.
+   *  6. Perform normalizeCaptures
    */
   private def transformExplicitType(tp: Type, tptToCheck: Tree = EmptyTree)(using Context): Type =
-    val toCapturing = new DeepTypeMap:
+    val toCapturing = new DeepTypeMap with FollowAliasesMap:
       override def toString = "expand aliases"
 
       /** Expand $throws aliases. This is hard-coded here since $throws aliases in stdlib
@@ -337,7 +339,6 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
         case tp @ CapturingType(parent, refs)
         if (refs eq defn.universalCSImpliedByCapability) && !tp.isBoxedCapturing =>
           parent
-        case tp @ CapturingType(parent, refs) => tp
         case _ => tp
 
       def apply(t: Type) =
@@ -819,7 +820,8 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
       CapturingType(OrType(parent1, tp2, tp.isSoft), refs1, tp1.isBoxed)
     case tp @ OrType(tp1, tp2 @ CapturingType(parent2, refs2)) =>
       CapturingType(OrType(tp1, parent2, tp.isSoft), refs2, tp2.isBoxed)
-    case tp @ AppliedType(tycon, args) if !defn.isFunctionClass(tp.dealias.typeSymbol) =>
+    case tp @ AppliedType(tycon, args)
+    if !defn.isFunctionClass(tp.dealias.typeSymbol) =>
       tp.derivedAppliedType(tycon, args.mapConserve(box))
     case tp: RealTypeBounds =>
       tp.derivedTypeBounds(tp.lo, box(tp.hi))
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 8414c3795f49..e9143ae88741 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -2845,6 +2845,9 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
         false
     Existential.isExistentialVar(tp1) && canInstantiateWith(assocExistentials)
 
+  def isOpenedExistential(ref: CaptureRef)(using Context): Boolean =
+    openedExistentials.contains(ref)
+
   /** bi-map taking existentials to the left of a comparison to matching
    *  existentials on the right. This is not a bijection. However
    *  we have `forwards(backwards(bv)) == bv` for an existentially bound `bv`.
@@ -3476,6 +3479,9 @@ object TypeComparer {
 
   def subsumesExistentially(tp1: TermParamRef, tp2: CaptureRef)(using Context) =
     comparing(_.subsumesExistentially(tp1, tp2))
+
+  def isOpenedExistential(ref: CaptureRef)(using Context) =
+    comparing(_.isOpenedExistential(ref))
 }
 
 object MatchReducer:
diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
index cac82eb0c4bd..e90aeb217362 100644
--- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
@@ -15,7 +15,7 @@ import util.SourcePosition
 import scala.util.control.NonFatal
 import scala.annotation.switch
 import config.{Config, Feature}
-import cc.{CapturingType, RetainingType, CaptureSet, ReachCapability, MaybeCapability, isBoxed, retainedElems, isRetainsLike}
+import cc.*
 
 class PlainPrinter(_ctx: Context) extends Printer {
 
@@ -297,7 +297,10 @@ class PlainPrinter(_ctx: Context) extends Printer {
         else if (annot.symbol == defn.IntoAnnot || annot.symbol == defn.IntoParamAnnot)
             && !printDebug
         then atPrec(GlobalPrec)( Str("into ") ~ toText(tpe) )
-        else toTextLocal(tpe) ~ " " ~ toText(annot)
+        else if annot.isInstanceOf[CaptureAnnotation] then
+          toTextLocal(tpe) ~ "^" ~ toText(annot)
+        else
+          toTextLocal(tpe) ~ " " ~ toText(annot)
       case FlexibleType(_, tpe) =>
         "(" ~ toText(tpe) ~ ")?"
       case tp: TypeVar =>
diff --git a/compiler/src/dotty/tools/dotc/transform/Recheck.scala b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
index 172ae337d6e6..8936c460de81 100644
--- a/compiler/src/dotty/tools/dotc/transform/Recheck.scala
+++ b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
@@ -255,7 +255,10 @@ abstract class Recheck extends Phase, SymTransformer:
 
     def recheckValDef(tree: ValDef, sym: Symbol)(using Context): Type =
       val resType = recheck(tree.tpt)
-      if tree.rhs.isEmpty then resType
+      def isUninitWildcard = tree.rhs match
+        case Ident(nme.WILDCARD) => tree.symbol.is(Mutable)
+        case _ => false
+      if tree.rhs.isEmpty || isUninitWildcard then resType
       else recheck(tree.rhs, resType)
 
     def recheckDefDef(tree: DefDef, sym: Symbol)(using Context): Type =
diff --git a/tests/neg-custom-args/captures/box-adapt-cases.check b/tests/neg-custom-args/captures/box-adapt-cases.check
new file mode 100644
index 000000000000..8dc088c6f713
--- /dev/null
+++ b/tests/neg-custom-args/captures/box-adapt-cases.check
@@ -0,0 +1,14 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/box-adapt-cases.scala:14:4 -------------------------------
+14 |  x(cap => cap.use())  // error
+   |    ^^^^^^^^^^^^^^^^
+   |    Found:    (cap: box Cap^?) ->{io} Int
+   |    Required: (cap: box Cap^{io}) -> Int
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/box-adapt-cases.scala:28:4 -------------------------------
+28 |  x(cap => cap.use())  // error
+   |    ^^^^^^^^^^^^^^^^
+   |    Found:    (cap: box Cap^?) ->{io, fs} Int
+   |    Required: (cap: box Cap^{io, fs}) ->{io} Int
+   |
+   | longer explanation available when compiling with `-explain`
diff --git a/tests/pos-custom-args/captures/boxmap-paper.scala b/tests/pos-custom-args/captures/boxmap-paper.scala
index 9d5bb49af25d..20282d5813f9 100644
--- a/tests/pos-custom-args/captures/boxmap-paper.scala
+++ b/tests/pos-custom-args/captures/boxmap-paper.scala
@@ -1,7 +1,13 @@
 
-type Cell[+T] = [K] -> (T => K) -> K
+type Cell_orig[+T] = [K] -> (T => K) -> K
 
-def cell[T](x: T): Cell[T] =
+def cell_orig[T](x: T): Cell_orig[T] =
+  [K] => (k: T => K) => k(x)
+
+class Cell[+T](val value: [K] -> (T => K) -> K):
+  def apply[K]: (T => K) -> K = value[K]
+
+def cell[T](x: T): Cell[T] = Cell:
   [K] => (k: T => K) => k(x)
 
 def get[T](c: Cell[T]): T = c[T](identity)
@@ -22,6 +28,10 @@ def test(io: IO^) =
 
   val loggedOne: () ->{io} Int = () => { io.print("1"); 1 }
 
+  // We have a leakage of io because type arguments to alias type `Cell` are not boxed.
+  val c_orig: Cell[() ->{io} Int]^{io}
+      = cell[() ->{io} Int](loggedOne)
+
   val c: Cell[() ->{io} Int]
       = cell[() ->{io} Int](loggedOne)
 
diff --git a/tests/pos-custom-args/captures/cc-cast.scala b/tests/pos-custom-args/captures/cc-cast.scala
new file mode 100644
index 000000000000..cfd96d63bee7
--- /dev/null
+++ b/tests/pos-custom-args/captures/cc-cast.scala
@@ -0,0 +1,12 @@
+import annotation.unchecked.uncheckedCaptures
+import compiletime.uninitialized
+
+def foo(x: Int => Int) = ()
+
+
+object Test:
+  def test(x: Object) =
+    foo(x.asInstanceOf[Int => Int])
+
+  @uncheckedCaptures var x1: Object^ = uninitialized
+  @uncheckedCaptures var x2: Object^ = _
diff --git a/tests/pos/cc-ex-unpack.scala b/tests/pos-custom-args/captures/ex-fun-aliases.scala.disabled
similarity index 79%
rename from tests/pos/cc-ex-unpack.scala
rename to tests/pos-custom-args/captures/ex-fun-aliases.scala.disabled
index ae9b4ea5d805..ff86927b874c 100644
--- a/tests/pos/cc-ex-unpack.scala
+++ b/tests/pos-custom-args/captures/ex-fun-aliases.scala.disabled
@@ -11,8 +11,12 @@ type EX3 = () -> (c: Exists) -> () -> C^{c}
 
 type EX4 = () -> () -> (c: Exists) -> C^{c}
 
+type FUN1 = (c: C^) ->  (C^{c}, C^{c})
+
 def Test =
   def f =
     val ex1: EX1 = ???
     val c1 = ex1
+    val fun1: FUN1 = c => (c, c)
+    val fun2 = fun1
     c1
diff --git a/tests/pos-custom-args/captures/i20237-explicit.scala b/tests/pos-custom-args/captures/i20237-explicit.scala
new file mode 100644
index 000000000000..0999d4acd50e
--- /dev/null
+++ b/tests/pos-custom-args/captures/i20237-explicit.scala
@@ -0,0 +1,15 @@
+import language.experimental.captureChecking
+
+class Cap extends caps.Capability:
+  def use[T](body: Cap => T) = body(this)
+
+class Box[T](body: Cap => T):
+  def open(cap: Cap) = cap.use(body)
+
+object Box:
+  def make[T](body: Cap => T)(cap: Cap): Box[T]^{body} = Box(x => body(x))
+
+def main =
+  val givenCap: Cap = new Cap
+  val xx: Cap => Int = y => 1
+  val box = Box.make[Int](xx)(givenCap).open
\ No newline at end of file
diff --git a/tests/pos/i20237.scala b/tests/pos-custom-args/captures/i20237.scala
similarity index 100%
rename from tests/pos/i20237.scala
rename to tests/pos-custom-args/captures/i20237.scala
diff --git a/tests/pos-custom-args/captures/open-existential.scala b/tests/pos-custom-args/captures/open-existential.scala
new file mode 100644
index 000000000000..8b43f27a051c
--- /dev/null
+++ b/tests/pos-custom-args/captures/open-existential.scala
@@ -0,0 +1,15 @@
+trait Async extends caps.Capability
+
+class Future[+T](x: () => T)(using val a: Async)
+
+class Collector[T](val futs: Seq[Future[T]^]):
+  def add(fut: Future[T]^{futs*}) = ???
+
+def main() =
+  given async: Async = ???
+  val futs = (1 to 20).map(x => Future(() => x))
+  val col = Collector(futs)
+  val col1: Collector[Int] { val futs: Seq[Future[Int]^{async}] }
+    = Collector(futs)
+
+
diff --git a/tests/pos/boxmap-paper.scala b/tests/pos/boxmap-paper.scala
deleted file mode 100644
index aa983114ed8a..000000000000
--- a/tests/pos/boxmap-paper.scala
+++ /dev/null
@@ -1,38 +0,0 @@
-import language.experimental.captureChecking
-
-type Cell[+T] = [K] -> (T => K) -> K
-
-def cell[T](x: T): Cell[T] =
-  [K] => (k: T => K) => k(x)
-
-def get[T](c: Cell[T]): T = c[T](identity)
-
-def map[A, B](c: Cell[A])(f: A => B): Cell[B]
-  = c[Cell[B]]((x: A) => cell(f(x)))
-
-def pureMap[A, B](c: Cell[A])(f: A -> B): Cell[B]
-  = c[Cell[B]]((x: A) => cell(f(x)))
-
-def lazyMap[A, B](c: Cell[A])(f: A => B): () ->{f} Cell[B]
-  = () => c[Cell[B]]((x: A) => cell(f(x)))
-
-trait IO:
-  def print(s: String): Unit
-
-def test(io: IO^) =
-
-  val loggedOne: () ->{io} Int = () => { io.print("1"); 1 }
-
-  val c: Cell[() ->{io} Int]
-      = cell[() ->{io} Int](loggedOne)
-
-  val g = (f: () ->{io} Int) =>
-    val x = f(); io.print(" + ")
-    val y = f(); io.print(s" = ${x + y}")
-
-  val r = lazyMap[() ->{io} Int, Unit](c)(f => g(f))
-  val r2 = lazyMap[() ->{io} Int, Unit](c)(g)
-  val r3 = lazyMap(c)(g)
-  val _ = r()
-  val _ = r2()
-  val _ = r3()

From ec86d5e74dead0891c2ce92897a5b31b4e65749b Mon Sep 17 00:00:00 2001
From: odersky <odersky@gmail.com>
Date: Fri, 10 Jan 2025 18:09:17 +0100
Subject: [PATCH 2/2] Expand aliases when mapping explicit types in Setup

This is necessary because the compiler is free in previous phases to dealias or not.
Therefore, capture checking should not depend on aliasing. The main difference is that
now arguments to type aliases are not necessarily boxed. They are boxed only if they need
boxing in the dealiased type.
---
 .../src/dotty/tools/dotc/cc/CaptureOps.scala  |  1 -
 compiler/src/dotty/tools/dotc/cc/Setup.scala  |  6 ++---
 .../captures/boundschecks2.scala              |  2 +-
 .../captures/boundschecks3.check              |  4 ++++
 .../captures/boundschecks3.scala              | 13 ++++++++++
 .../captures/box-adapt-cases.check            | 20 ++++++++--------
 .../captures/box-adapt-cases.scala            | 16 ++++++-------
 .../captures/box-adapt-cov.scala              | 10 ++++----
 .../captures/box-adapt-depfun.scala           | 12 +++++-----
 .../captures/box-adapt-typefun.scala          |  8 +++----
 tests/neg-custom-args/captures/capt1.check    | 12 +++++-----
 .../captures/cc-ex-conformance.scala          |  2 +-
 .../captures/existential-mapping.check        | 24 +++++++++----------
 tests/neg-custom-args/captures/i15922.scala   |  4 ++--
 tests/neg-custom-args/captures/i16725.scala   |  8 +++----
 tests/neg-custom-args/captures/i19330.check   |  5 ++++
 tests/neg-custom-args/captures/i21401.check   |  8 +++----
 .../neg-custom-args/captures/outer-var.check  | 10 ++++----
 tests/neg-custom-args/captures/try.check      |  4 ++--
 tests/neg-custom-args/captures/vars.check     |  6 ++---
 .../captures/i15749a.scala                    | 10 ++++----
 21 files changed, 102 insertions(+), 83 deletions(-)
 create mode 100644 tests/neg-custom-args/captures/boundschecks3.check
 create mode 100644 tests/neg-custom-args/captures/boundschecks3.scala
 create mode 100644 tests/neg-custom-args/captures/i19330.check
 rename tests/{neg-custom-args => pos-custom-args}/captures/i15749a.scala (51%)

diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
index 62a9fe33fc5c..92cd40a65d5a 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
@@ -49,7 +49,6 @@ object ccConfig:
 
 end ccConfig
 
-
 /** Are we at checkCaptures phase? */
 def isCaptureChecking(using Context): Boolean =
   ctx.phaseId == Phases.checkCapturesPhase.id
diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala
index 7cc7e0514599..e28aeb8e0313 100644
--- a/compiler/src/dotty/tools/dotc/cc/Setup.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -278,7 +278,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
               paramInfos = tp.paramInfos.mapConserve(_.dropAllRetains.bounds),
               resType = this(tp.resType))
           case _ =>
-            mapOver(tp)
+            mapFollowingAliases(tp)
         addVar(addCaptureRefinements(normalizeCaptures(tp1)), ctx.owner)
       end apply
     end mapInferred
@@ -364,7 +364,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
             // Map references to capability classes C to C^
             if t.derivesFromCapability && !t.isSingleton && t.typeSymbol != defn.Caps_Exists
             then CapturingType(t, defn.universalCSImpliedByCapability, boxed = false)
-            else normalizeCaptures(mapOver(t))
+            else normalizeCaptures(mapFollowingAliases(t))
     end toCapturing
 
     def fail(msg: Message) =
@@ -821,7 +821,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
     case tp @ OrType(tp1, tp2 @ CapturingType(parent2, refs2)) =>
       CapturingType(OrType(tp1, parent2, tp.isSoft), refs2, tp2.isBoxed)
     case tp @ AppliedType(tycon, args)
-    if !defn.isFunctionClass(tp.dealias.typeSymbol) =>
+    if !defn.isFunctionClass(tp.dealias.typeSymbol) && (tp.dealias eq tp) =>
       tp.derivedAppliedType(tycon, args.mapConserve(box))
     case tp: RealTypeBounds =>
       tp.derivedTypeBounds(tp.lo, box(tp.hi))
diff --git a/tests/neg-custom-args/captures/boundschecks2.scala b/tests/neg-custom-args/captures/boundschecks2.scala
index 923758d722f9..99366a8e7aff 100644
--- a/tests/neg-custom-args/captures/boundschecks2.scala
+++ b/tests/neg-custom-args/captures/boundschecks2.scala
@@ -8,6 +8,6 @@ object test {
 
   val foo: C[Tree^] = ??? // error
   type T = C[Tree^] // error
-  val bar: T -> T = ???
+  //val bar: T -> T = ???  // --> boundschecks3.scala for what happens if we uncomment
   val baz: C[Tree^] -> Unit = ??? // error
 }
diff --git a/tests/neg-custom-args/captures/boundschecks3.check b/tests/neg-custom-args/captures/boundschecks3.check
new file mode 100644
index 000000000000..36e1336e8f05
--- /dev/null
+++ b/tests/neg-custom-args/captures/boundschecks3.check
@@ -0,0 +1,4 @@
+-- Error: tests/neg-custom-args/captures/boundschecks3.scala:11:13 -----------------------------------------------------
+11 |  val bar: T -> T = ??? // error, since `T` is expanded here. But the msg is not very good.
+   |           ^^^^^^
+   |           test.C[box test.Tree^] captures the root capability `cap` in invariant position
diff --git a/tests/neg-custom-args/captures/boundschecks3.scala b/tests/neg-custom-args/captures/boundschecks3.scala
new file mode 100644
index 000000000000..f5e9652c0913
--- /dev/null
+++ b/tests/neg-custom-args/captures/boundschecks3.scala
@@ -0,0 +1,13 @@
+object test {
+
+  class Tree
+
+  def f[X <: Tree](x: X): Unit = ()
+
+  class C[X <: Tree](x: X)
+
+  val foo: C[Tree^] = ??? // hidden error
+  type T = C[Tree^] // hidden error
+  val bar: T -> T = ??? // error, since `T` is expanded here. But the msg is not very good.
+  val baz: C[Tree^] -> Unit = ??? // hidden error
+}
diff --git a/tests/neg-custom-args/captures/box-adapt-cases.check b/tests/neg-custom-args/captures/box-adapt-cases.check
index 8dc088c6f713..7ff185c499a5 100644
--- a/tests/neg-custom-args/captures/box-adapt-cases.check
+++ b/tests/neg-custom-args/captures/box-adapt-cases.check
@@ -1,14 +1,14 @@
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/box-adapt-cases.scala:14:4 -------------------------------
-14 |  x(cap => cap.use())  // error
-   |    ^^^^^^^^^^^^^^^^
-   |    Found:    (cap: box Cap^?) ->{io} Int
-   |    Required: (cap: box Cap^{io}) -> Int
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/box-adapt-cases.scala:14:10 ------------------------------
+14 |  x.value(cap => cap.use())  // error
+   |          ^^^^^^^^^^^^^^^^
+   |          Found:    (cap: box Cap^?) ->{io} Int
+   |          Required: (cap: box Cap^{io}) -> Int
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/box-adapt-cases.scala:28:4 -------------------------------
-28 |  x(cap => cap.use())  // error
-   |    ^^^^^^^^^^^^^^^^
-   |    Found:    (cap: box Cap^?) ->{io, fs} Int
-   |    Required: (cap: box Cap^{io, fs}) ->{io} Int
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/box-adapt-cases.scala:28:10 ------------------------------
+28 |  x.value(cap => cap.use())  // error
+   |          ^^^^^^^^^^^^^^^^
+   |          Found:    (cap: box Cap^?) ->{io, fs} Int
+   |          Required: (cap: box Cap^{io, fs}) ->{io} Int
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/box-adapt-cases.scala b/tests/neg-custom-args/captures/box-adapt-cases.scala
index d9ec0f80a548..8f7d7a0a6667 100644
--- a/tests/neg-custom-args/captures/box-adapt-cases.scala
+++ b/tests/neg-custom-args/captures/box-adapt-cases.scala
@@ -1,29 +1,29 @@
 trait Cap { def use(): Int }
 
 def test1(): Unit = {
-  type Id[X] = [T] -> (op: X => T) -> T
+  class Id[X](val value: [T] -> (op: X => T) -> T)
 
   val x: Id[Cap^] = ???
-  x(cap => cap.use())
+  x.value(cap => cap.use())
 }
 
 def test2(io: Cap^): Unit = {
-  type Id[X] = [T] -> (op: X -> T) -> T
+  class Id[X](val value: [T] -> (op: X -> T) -> T)
 
   val x: Id[Cap^{io}] = ???
-  x(cap => cap.use())  // error
+  x.value(cap => cap.use())  // error
 }
 
 def test3(io: Cap^): Unit = {
-  type Id[X] = [T] -> (op: X ->{io} T) -> T
+  class Id[X](val value: [T] -> (op: X ->{io} T) -> T)
 
   val x: Id[Cap^{io}] = ???
-  x(cap => cap.use())  // ok
+  x.value(cap => cap.use())  // ok
 }
 
 def test4(io: Cap^, fs: Cap^): Unit = {
-  type Id[X] = [T] -> (op: X ->{io} T) -> T
+  class Id[X](val value: [T] -> (op: X ->{io} T) -> T)
 
   val x: Id[Cap^{io, fs}] = ???
-  x(cap => cap.use())  // error
+  x.value(cap => cap.use())  // error
 }
diff --git a/tests/neg-custom-args/captures/box-adapt-cov.scala b/tests/neg-custom-args/captures/box-adapt-cov.scala
index 2c1f15a5c77f..e1e6dd4cec1a 100644
--- a/tests/neg-custom-args/captures/box-adapt-cov.scala
+++ b/tests/neg-custom-args/captures/box-adapt-cov.scala
@@ -1,14 +1,14 @@
 trait Cap
 
 def test1(io: Cap^) = {
-  type Op[X] = [T] -> Unit -> X
+  class Op[+X](val value: [T] -> Unit -> X)
   val f: Op[Cap^{io}] = ???
-  val x: [T] -> Unit -> Cap^{io} = f  // error
+  val x: [T] -> Unit -> Cap^{io} = f.value  // error
 }
 
 def test2(io: Cap^) = {
-  type Op[X] = [T] -> Unit -> X^{io}
+  class Op[+X](val value: [T] -> Unit -> X^{io})
   val f: Op[Cap^{io}] = ???
-  val x: Unit -> Cap^{io} = f[Unit]  // error
-  val x1: Unit ->{io} Cap^{io} = f[Unit]  // ok
+  val x: Unit -> Cap^{io} = f.value[Unit]  // error
+  val x1: Unit ->{io} Cap^{io} = f.value[Unit]  // ok
 }
diff --git a/tests/neg-custom-args/captures/box-adapt-depfun.scala b/tests/neg-custom-args/captures/box-adapt-depfun.scala
index d1c1c73f8207..f673c657f753 100644
--- a/tests/neg-custom-args/captures/box-adapt-depfun.scala
+++ b/tests/neg-custom-args/captures/box-adapt-depfun.scala
@@ -1,23 +1,23 @@
 trait Cap { def use(): Int }
 
 def test1(io: Cap^): Unit = {
-  type Id[X] = [T] -> (op: X ->{io} T) -> T
+  class Id[X](val value: [T] -> (op: X ->{io} T) -> T)
 
   val x: Id[Cap]^{io} = ???
-  x(cap => cap.use())  // ok
+  x.value(cap => cap.use())  // ok
 }
 
 def test2(io: Cap^): Unit = {
-  type Id[X] = [T] -> (op: (x: X) ->{io} T) -> T
+  class Id[X](val value: [T] -> (op: (x: X) ->{io} T) -> T)
 
   val x: Id[Cap^{io}] = ???
-  x(cap => cap.use())
+  x.value(cap => cap.use())
   // should work when the expected type is a dependent function
 }
 
 def test3(io: Cap^): Unit = {
-  type Id[X] = [T] -> (op: (x: X) ->{} T) -> T
+  class Id[X](val value: [T] -> (op: (x: X) ->{} T) -> T)
 
   val x: Id[Cap^{io}] = ???
-  x(cap => cap.use()) // error
+  x.value(cap => cap.use()) // error
 }
diff --git a/tests/neg-custom-args/captures/box-adapt-typefun.scala b/tests/neg-custom-args/captures/box-adapt-typefun.scala
index 175acdda1c8f..76da047f42a9 100644
--- a/tests/neg-custom-args/captures/box-adapt-typefun.scala
+++ b/tests/neg-custom-args/captures/box-adapt-typefun.scala
@@ -1,13 +1,13 @@
 trait Cap { def use(): Int }
 
 def test1(io: Cap^): Unit = {
-  type Op[X] = [T] -> X -> Unit
+  class Op[X](val value: [T] -> X -> Unit)
   val f: [T] -> (Cap^{io}) -> Unit = ???
-  val op: Op[Cap^{io}] = f // error
+  val op: Op[Cap^{io}] = Op(f) // was error, now ok
 }
 
 def test2(io: Cap^): Unit = {
-  type Lazy[X] = [T] -> Unit -> X
+  class Lazy[X](val value: [T] -> Unit -> X)
   val f: Lazy[Cap^{io}] = ???
-  val test: [T] -> Unit -> (Cap^{io}) = f // error
+  val test: [T] -> Unit -> (Cap^{io}) = f.value // error
 }
diff --git a/tests/neg-custom-args/captures/capt1.check b/tests/neg-custom-args/captures/capt1.check
index f63c55ca48c4..acf8faa7a969 100644
--- a/tests/neg-custom-args/captures/capt1.check
+++ b/tests/neg-custom-args/captures/capt1.check
@@ -36,15 +36,15 @@
 -- Error: tests/neg-custom-args/captures/capt1.scala:34:16 -------------------------------------------------------------
 34 |  val z2 = h[() -> Cap](() => x) // error // error
    |             ^^^^^^^^^
-   |             Type variable X of method h cannot be instantiated to () -> box C^ since
-   |             the part box C^ of that type captures the root capability `cap`.
+   |             Type variable X of method h cannot be instantiated to () -> (ex$15: caps.Exists) -> C^{ex$15} since
+   |             the part C^{ex$15} of that type captures the root capability `cap`.
 -- Error: tests/neg-custom-args/captures/capt1.scala:34:30 -------------------------------------------------------------
 34 |  val z2 = h[() -> Cap](() => x) // error // error
    |                              ^
-   |                              reference (x : C^) is not included in the allowed capture set {}
-   |                              of an enclosing function literal with expected type () -> box C^
+   |                     reference (x : C^) is not included in the allowed capture set {}
+   |                     of an enclosing function literal with expected type () -> (ex$15: caps.Exists) -> C^{ex$15}
 -- Error: tests/neg-custom-args/captures/capt1.scala:36:13 -------------------------------------------------------------
 36 |  val z3 = h[(() -> Cap) @retains(x)](() => x)(() => C())  // error
    |             ^^^^^^^^^^^^^^^^^^^^^^^
-   |             Type variable X of method h cannot be instantiated to box () ->{x} Cap since
-   |             the part Cap of that type captures the root capability `cap`.
+   |      Type variable X of method h cannot be instantiated to box () ->{x} (ex$20: caps.Exists) -> C^{ex$20} since
+   |      the part C^{ex$20} of that type captures the root capability `cap`.
diff --git a/tests/neg-custom-args/captures/cc-ex-conformance.scala b/tests/neg-custom-args/captures/cc-ex-conformance.scala
index a953466daa9a..16e13376c5b3 100644
--- a/tests/neg-custom-args/captures/cc-ex-conformance.scala
+++ b/tests/neg-custom-args/captures/cc-ex-conformance.scala
@@ -21,5 +21,5 @@ def Test =
   val ex3: EX3 = ???
   val ex4: EX4 = ???
   val _: EX4 = ex3 // ok
-  val _: EX4 = ex4
+  val _: EX4 = ex4 // error (???) Probably since we also introduce existentials on expansion
   val _: EX3 = ex4 // error
diff --git a/tests/neg-custom-args/captures/existential-mapping.check b/tests/neg-custom-args/captures/existential-mapping.check
index cd71337868e1..30836bc427cf 100644
--- a/tests/neg-custom-args/captures/existential-mapping.check
+++ b/tests/neg-custom-args/captures/existential-mapping.check
@@ -33,56 +33,56 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:21:30 --------------------------
 21 |  val _: A^ -> (x: C^) -> C = x5 // error
    |                              ^^
-   |                              Found:    (x5 : A^ -> (ex$27: caps.Exists) -> Fun[C^{ex$27}])
+   |                              Found:    (x5 : A^ -> (x: C^) -> (ex$27: caps.Exists) -> C^{ex$27})
    |                              Required: A^ -> (x: C^) -> C
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:24:30 --------------------------
 24 |  val _: A^ -> (x: C^) => C = x6 // error
    |                              ^^
-   |                              Found:    (x6 : A^ -> (ex$33: caps.Exists) -> IFun[C^{ex$33}])
-   |                              Required: A^ -> (ex$36: caps.Exists) -> (x: C^) ->{ex$36} C
+   |              Found:    (x6 : A^ -> (ex$36: caps.Exists) -> (x: C^) ->{ex$36} (ex$35: caps.Exists) -> C^{ex$35})
+   |              Required: A^ -> (ex$39: caps.Exists) -> (x: C^) ->{ex$39} C
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:27:25 --------------------------
 27 |  val _:  (x: C^) => C = y1 // error
    |                         ^^
-   |                         Found:    (y1 : (x: C^) => (ex$38: caps.Exists) -> C^{ex$38})
+   |                         Found:    (y1 : (x: C^) => (ex$41: caps.Exists) -> C^{ex$41})
    |                         Required: (x: C^) => C
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:30:20 --------------------------
 30 |  val _:  C^ => C = y2 // error
    |                    ^^
-   |                    Found:    (y2 : C^ => (ex$42: caps.Exists) -> C^{ex$42})
+   |                    Found:    (y2 : C^ => (ex$45: caps.Exists) -> C^{ex$45})
    |                    Required: C^ => C
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:33:30 --------------------------
 33 |  val _: A^ => (x: C^) => C = y3 // error
    |                              ^^
-   |              Found:    (y3 : A^ => (ex$47: caps.Exists) -> (x: C^) ->{ex$47} (ex$46: caps.Exists) -> C^{ex$46})
-   |              Required: A^ => (ex$50: caps.Exists) -> (x: C^) ->{ex$50} C
+   |              Found:    (y3 : A^ => (ex$50: caps.Exists) -> (x: C^) ->{ex$50} (ex$49: caps.Exists) -> C^{ex$49})
+   |              Required: A^ => (ex$53: caps.Exists) -> (x: C^) ->{ex$53} C
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:36:25 --------------------------
 36 |  val _: A^ => C^ => C = y4 // error
    |                         ^^
-   |                   Found:    (y4 : A^ => (ex$53: caps.Exists) -> C^ ->{ex$53} (ex$52: caps.Exists) -> C^{ex$52})
-   |                   Required: A^ => (ex$56: caps.Exists) -> C^ ->{ex$56} C
+   |                   Found:    (y4 : A^ => (ex$56: caps.Exists) -> C^ ->{ex$56} (ex$55: caps.Exists) -> C^{ex$55})
+   |                   Required: A^ => (ex$59: caps.Exists) -> C^ ->{ex$59} C
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:39:30 --------------------------
 39 |  val _: A^ => (x: C^) -> C = y5 // error
    |                              ^^
-   |                              Found:    (y5 : A^ => (ex$58: caps.Exists) -> Fun[C^{ex$58}])
+   |                              Found:    (y5 : A^ => (x: C^) -> (ex$61: caps.Exists) -> C^{ex$61})
    |                              Required: A^ => (x: C^) -> C
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:42:30 --------------------------
 42 |  val _: A^ => (x: C^) => C = y6 // error
    |                              ^^
-   |                              Found:    (y6 : A^ => (ex$64: caps.Exists) -> IFun[C^{ex$64}])
-   |                              Required: A^ => (ex$67: caps.Exists) -> (x: C^) ->{ex$67} C
+   |              Found:    (y6 : A^ => (ex$70: caps.Exists) -> (x: C^) ->{ex$70} (ex$69: caps.Exists) -> C^{ex$69})
+   |              Required: A^ => (ex$73: caps.Exists) -> (x: C^) ->{ex$73} C
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/i15922.scala b/tests/neg-custom-args/captures/i15922.scala
index 848a22fe5341..b8bcc346ef81 100644
--- a/tests/neg-custom-args/captures/i15922.scala
+++ b/tests/neg-custom-args/captures/i15922.scala
@@ -1,8 +1,8 @@
 
 
 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)
+class Id[+X](val value: [T] -> (op: X => T) -> T)
+def mkId[X](x: X): Id[X] = Id([T] => (op: X => T) => op(x))
 
 def withCap[X](op: (Cap^) => X): X = {
   val cap: Cap^ = new Cap { def use() = { println("cap is used"); 0 } }
diff --git a/tests/neg-custom-args/captures/i16725.scala b/tests/neg-custom-args/captures/i16725.scala
index 1accf197c626..96cf44e72f3c 100644
--- a/tests/neg-custom-args/captures/i16725.scala
+++ b/tests/neg-custom-args/captures/i16725.scala
@@ -3,12 +3,12 @@ class IO extends caps.Capability:
   def brewCoffee(): Unit = ???
 def usingIO[T](op: IO => T): T = ???
 
-type Wrapper[T] = [R] -> (f: T => R) -> R
-def mk[T](x: T): Wrapper[T] = [R] => f => f(x)
+class Wrapper[T](val value: [R] -> (f: T => R) -> R)
+def mk[T](x: T): Wrapper[T] = Wrapper([R] => f => f(x))
 def useWrappedIO(wrapper: Wrapper[IO]): () -> Unit =
   () =>
-    wrapper: io =>  // error
+    wrapper.value: io =>  // error
       io.brewCoffee()
 def main(): Unit =
-  val escaped = usingIO(io => useWrappedIO(mk(io)))
+  val escaped = usingIO(io => useWrappedIO(mk(io))) // error
   escaped()  // boom
diff --git a/tests/neg-custom-args/captures/i19330.check b/tests/neg-custom-args/captures/i19330.check
new file mode 100644
index 000000000000..a8925b117611
--- /dev/null
+++ b/tests/neg-custom-args/captures/i19330.check
@@ -0,0 +1,5 @@
+-- Error: tests/neg-custom-args/captures/i19330.scala:15:29 ------------------------------------------------------------
+15 |  val leaked = usingLogger[x.T]: l =>  // error
+   |                           ^^^
+   |                           Type variable T of method usingLogger cannot be instantiated to x.T since
+   |                           the part () => Logger^ of that type captures the root capability `cap`.
diff --git a/tests/neg-custom-args/captures/i21401.check b/tests/neg-custom-args/captures/i21401.check
index 679c451949bd..e7483e10bfa6 100644
--- a/tests/neg-custom-args/captures/i21401.check
+++ b/tests/neg-custom-args/captures/i21401.check
@@ -11,8 +11,8 @@
 -- Error: tests/neg-custom-args/captures/i21401.scala:16:66 ------------------------------------------------------------
 16 |  val leaked: [R, X <: Boxed[IO^] -> R] -> (op: X) -> R = usingIO[Res](mkRes) // error
    |                                                                  ^^^
-   |                                           Type variable R of method usingIO cannot be instantiated to Res since
-   |                                           the part box IO^ of that type captures the root capability `cap`.
+   | Type variable R of method usingIO cannot be instantiated to [R, X <: Boxed[box IO^] -> R] => (op: X) -> R since
+   | the part box IO^ of that type captures the root capability `cap`.
 -- Error: tests/neg-custom-args/captures/i21401.scala:17:29 ------------------------------------------------------------
 17 |  val x: Boxed[IO^] = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x) // error // error
    |                             ^^^^^^^^^^
@@ -21,8 +21,8 @@
 -- Error: tests/neg-custom-args/captures/i21401.scala:17:52 ------------------------------------------------------------
 17 |  val x: Boxed[IO^] = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x) // error // error
    |                                         ^^^^^^^^^^^^^^^^^^^^^^^^
-   |Type variable X of value leaked cannot be instantiated to Boxed[box IO^] -> (ex$18: caps.Exists) -> Boxed[box IO^{ex$18}] since
-   |the part box IO^{ex$18} of that type captures the root capability `cap`.
+   |Type variable X of value leaked cannot be instantiated to Boxed[box IO^] -> (ex$20: caps.Exists) -> Boxed[box IO^{ex$20}] since
+   |the part box IO^{ex$20} of that type captures the root capability `cap`.
 -- Error: tests/neg-custom-args/captures/i21401.scala:18:21 ------------------------------------------------------------
 18 |  val y: IO^{x*} = x.unbox // error
    |                   ^^^^^^^
diff --git a/tests/neg-custom-args/captures/outer-var.check b/tests/neg-custom-args/captures/outer-var.check
index 72af842728a1..b24579b7a69f 100644
--- a/tests/neg-custom-args/captures/outer-var.check
+++ b/tests/neg-custom-args/captures/outer-var.check
@@ -1,7 +1,7 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/outer-var.scala:11:8 -------------------------------------
 11 |    x = q           // error
    |        ^
-   |        Found:    (q : Proc)
+   |        Found:    (q : () => Unit)
    |        Required: () ->{p, q²} Unit
    |
    |        where:    q  is a parameter in method inner
@@ -11,14 +11,14 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/outer-var.scala:12:9 -------------------------------------
 12 |    x = (q: Proc)   // error
    |         ^^^^^^^
-   |         Found:    Proc
+   |         Found:    () => Unit
    |         Required: () ->{p, q} Unit
    |
    | 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
+   |         Found:    () => Unit
    |         Required: () ->{p} Unit
    |
    |         Note that the universal capability `cap`
@@ -28,10 +28,10 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/outer-var.scala:14:8 -------------------------------------
 14 |    y = q           // error, was OK under unsealed
    |        ^
-   |        Found:    (q : Proc)
+   |        Found:    (q : () => Unit)
    |        Required: () ->{p} Unit
    |
-   |        Note that reference (q : Proc), defined in method inner
+   |        Note that reference (q : () => Unit), defined in method inner
    |        cannot be included in outer capture set {p} of variable y
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/try.check b/tests/neg-custom-args/captures/try.check
index 72604451472c..23c1b056c659 100644
--- a/tests/neg-custom-args/captures/try.check
+++ b/tests/neg-custom-args/captures/try.check
@@ -6,8 +6,8 @@
 -- Error: tests/neg-custom-args/captures/try.scala:30:65 ---------------------------------------------------------------
 30 |    (x: CanThrow[Exception]) => () => raise(new Exception)(using x) // error
    |                                                                 ^
-   |                               reference (x : CanThrow[Exception]) is not included in the allowed capture set {}
-   |                               of an enclosing function literal with expected type () ->? Nothing
+   |                                    reference (x : CT[Exception]^) is not included in the allowed capture set {}
+   |                                    of an enclosing function literal with expected type () ->? Nothing
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:52:2 -------------------------------------------
 47 |val global: () -> Int = handle {
 48 |  (x: CanThrow[Exception]) =>
diff --git a/tests/neg-custom-args/captures/vars.check b/tests/neg-custom-args/captures/vars.check
index e4b1e71a2000..db5c8083e3b7 100644
--- a/tests/neg-custom-args/captures/vars.check
+++ b/tests/neg-custom-args/captures/vars.check
@@ -1,9 +1,9 @@
 -- 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
+   |             reference (cap3 : CC^) is not included in the allowed capture set {cap1} of variable a
    |
-   |             Note that reference (cap3 : Cap), defined in method scope
+   |             Note that reference (cap3 : CC^), 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:25:8 ------------------------------------------
 25 |    a = g      // error
@@ -11,7 +11,7 @@
    |        Found:    (x: String) ->{cap3} String
    |        Required: (x$0: String) ->{cap1} String
    |
-   |        Note that reference (cap3 : Cap), defined in method scope
+   |        Note that reference (cap3 : CC^), defined in method scope
    |        cannot be included in outer capture set {cap1} of variable a
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/i15749a.scala b/tests/pos-custom-args/captures/i15749a.scala
similarity index 51%
rename from tests/neg-custom-args/captures/i15749a.scala
rename to tests/pos-custom-args/captures/i15749a.scala
index d3c1fce13322..184f980d6d70 100644
--- a/tests/neg-custom-args/captures/i15749a.scala
+++ b/tests/pos-custom-args/captures/i15749a.scala
@@ -6,19 +6,17 @@ object u extends Unit
 
 type Top = Any^
 
-type Wrapper[+T] = [X] -> (op: T ->{cap} X) -> X
+class Wrapper[+T](val value: [X] -> (op: T ->{cap} X) -> X)
 
 def test =
 
-  def wrapper[T](x: T): Wrapper[T] =
+  def wrapper[T](x: T): Wrapper[T] = Wrapper:
     [X] => (op: T ->{cap} X) => op(x)
 
   def strictMap[A <: Top,  B <: Top](mx: Wrapper[A])(f: A ->{cap} B): Wrapper[B] =
-    mx((x: A) => wrapper(f(x)))
+    mx.value((x: A) => wrapper(f(x)))
 
   def force[A](thunk: Unit ->{cap} A): A = thunk(u)
 
   def forceWrapper[A](@use mx: Wrapper[Unit ->{cap} A]): Wrapper[A] =
-    // Γ ⊢ mx: Wrapper[□ {cap} Unit => A]
-    // `force` should be typed as ∀(□ {cap} Unit -> A) A, but it can not
-    strictMap[Unit ->{mx*} A, A](mx)(t => force[A](t)) // error // should work
+    strictMap[Unit ->{mx*} A, A](mx)(t => force[A](t)) // was error when Wrapper was an alias type