diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
index bc4eb92234eb..92cd40a65d5a 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
@@ -46,8 +46,8 @@ object ccConfig:
    */
   def useSealed(using Context) =
     Feature.sourceVersion.stable != SourceVersion.`3.5`
-end ccConfig
 
+end ccConfig
 
 /** Are we at checkCaptures phase? */
 def isCaptureChecking(using Context): Boolean =
@@ -629,6 +629,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..e28aeb8e0313 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
@@ -277,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
@@ -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) =
@@ -363,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) =
@@ -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.dealias eq tp) =>
       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 bbe157d4a29b..bb52d97ac04e 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -2846,6 +2846,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`.
@@ -3477,6 +3480,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/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
new file mode 100644
index 000000000000..7ff185c499a5
--- /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: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: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/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/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
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()