diff --git a/compiler/src/dotty/tools/dotc/Run.scala b/compiler/src/dotty/tools/dotc/Run.scala
index 022ffbed5408..f7a08d1640ee 100644
--- a/compiler/src/dotty/tools/dotc/Run.scala
+++ b/compiler/src/dotty/tools/dotc/Run.scala
@@ -164,10 +164,15 @@ class Run(comp: Compiler, ictx: Context) extends ImplicitRunInfo with Constraint
   private var finalizeActions = mutable.ListBuffer[() => Unit]()
 
   /** Will be set to true if any of the compiled compilation units contains
-   *  a pureFunctions or captureChecking language import.
+   *  a pureFunctions language import.
    */
   var pureFunsImportEncountered = false
 
+  /** Will be set to true if any of the compiled compilation units contains
+   *  a captureChecking language import.
+   */
+  var ccImportEncountered = false
+
   def compile(files: List[AbstractFile]): Unit =
     try
       val sources = files.map(runContext.getSource(_))
@@ -229,6 +234,7 @@ class Run(comp: Compiler, ictx: Context) extends ImplicitRunInfo with Constraint
     def runPhases(using Context) = {
       var lastPrintedTree: PrintedTree = NoPrintedTree
       val profiler = ctx.profiler
+      var phasesWereAdjusted = false
 
       for (phase <- ctx.base.allPhases)
         if (phase.isRunnable)
@@ -247,6 +253,11 @@ class Run(comp: Compiler, ictx: Context) extends ImplicitRunInfo with Constraint
               Stats.record(s"retained typed trees at end of $phase", unit.tpdTree.treeSize)
             ctx.typerState.gc()
           }
+          if !phasesWereAdjusted then
+            phasesWereAdjusted = true
+            if !Feature.ccEnabledSomewhere then
+              ctx.base.unlinkPhaseAsDenotTransformer(Phases.checkCapturesPhase.prev)
+              ctx.base.unlinkPhaseAsDenotTransformer(Phases.checkCapturesPhase)
 
       profiler.finished()
     }
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
index 3261cb1d90f8..0ede1825e611 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
@@ -166,8 +166,49 @@ extension (tp: Type)
       case CapturingType(_, _) => true
       case _ => false
 
+  /** Is type known to be always pure by its class structure,
+   *  so that adding a capture set to it would not make sense?
+   */
+  def isAlwaysPure(using Context): Boolean = tp.dealias match
+    case tp: (TypeRef | AppliedType) =>
+      val sym = tp.typeSymbol
+      if sym.isClass then sym.isPureClass
+      else tp.superType.isAlwaysPure
+    case CapturingType(parent, refs) =>
+      parent.isAlwaysPure || refs.isAlwaysEmpty
+    case tp: TypeProxy =>
+      tp.superType.isAlwaysPure
+    case tp: AndType =>
+      tp.tp1.isAlwaysPure || tp.tp2.isAlwaysPure
+    case tp: OrType =>
+      tp.tp1.isAlwaysPure && tp.tp2.isAlwaysPure
+    case _ =>
+      false
+
+extension (cls: ClassSymbol)
+
+  def pureBaseClass(using Context): Option[Symbol] =
+    cls.baseClasses.find(bc =>
+      defn.pureBaseClasses.contains(bc)
+      || {
+        val selfType = bc.givenSelfType
+        selfType.exists && selfType.captureSet.isAlwaysEmpty
+      })
+
 extension (sym: Symbol)
 
+  /** A class is pure if:
+   *   - one its base types has an explicitly declared self type with an empty capture set
+   *   - or it is a value class
+   *   - or it is an exception
+   *   - or it is one of Nothing, Null, or String
+   */
+  def isPureClass(using Context): Boolean = sym match
+    case cls: ClassSymbol =>
+      cls.pureBaseClass.isDefined || defn.pureSimpleClasses.contains(cls)
+    case _ =>
+      false
+
   /** Does this symbol allow results carrying the universal capability?
    *  Currently this is true only for function type applies (since their
    *  results are unboxed) and `erasedValue` since this function is magic in
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
index d3e32ac538a4..6bf6d7770d8b 100644
--- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -271,7 +271,7 @@ sealed abstract class CaptureSet extends Showable:
     map(Substituters.SubstParamsMap(tl, to))
 
   /** Invoke handler if this set has (or later aquires) the root capability `*` */
-  def disallowRootCapability(handler: () => Unit)(using Context): this.type =
+  def disallowRootCapability(handler: () => Context ?=> Unit)(using Context): this.type =
     if isUniversal then handler()
     this
 
@@ -373,7 +373,7 @@ object CaptureSet:
     def isAlwaysEmpty = false
 
     /** A handler to be invoked if the root reference `*` is added to this set */
-    var addRootHandler: () => Unit = () => ()
+    var rootAddedHandler: () => Context ?=> Unit = () => ()
 
     var description: String = ""
 
@@ -404,7 +404,7 @@ object CaptureSet:
     def addNewElems(newElems: Refs, origin: CaptureSet)(using Context, VarState): CompareResult =
       if !isConst && recordElemsState() then
         elems ++= newElems
-        if isUniversal then addRootHandler()
+        if isUniversal then rootAddedHandler()
         // assert(id != 2 || elems.size != 2, this)
         (CompareResult.OK /: deps) { (r, dep) =>
           r.andAlso(dep.tryInclude(newElems, this))
@@ -421,8 +421,8 @@ object CaptureSet:
       else
         CompareResult.fail(this)
 
-    override def disallowRootCapability(handler: () => Unit)(using Context): this.type =
-      addRootHandler = handler
+    override def disallowRootCapability(handler: () => Context ?=> Unit)(using Context): this.type =
+      rootAddedHandler = handler
       super.disallowRootCapability(handler)
 
     private var computingApprox = false
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index cf1d4266e89b..899914e872c8 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -10,7 +10,8 @@ import config.Printers.{capt, recheckr}
 import config.{Config, Feature}
 import ast.{tpd, untpd, Trees}
 import Trees.*
-import typer.RefChecks.{checkAllOverrides, checkParents}
+import typer.RefChecks.{checkAllOverrides, checkSelfAgainstParents}
+import typer.Checking.{checkBounds, checkAppliedTypesIn}
 import util.{SimpleIdentitySet, EqHashMap, SrcPos}
 import transform.SymUtils.*
 import transform.{Recheck, PreRecheck}
@@ -18,6 +19,7 @@ import Recheck.*
 import scala.collection.mutable
 import CaptureSet.{withCaptureSetsExplained, IdempotentCaptRefMap}
 import StdNames.nme
+import NameKinds.DefaultGetterName
 import reporting.trace
 
 /** The capture checker */
@@ -335,12 +337,21 @@ class CheckCaptures extends Recheck, SymTransformer:
     override def recheckApply(tree: Apply, pt: Type)(using Context): Type =
       val meth = tree.fun.symbol
       includeCallCaptures(meth, tree.srcPos)
-      if meth == defn.Caps_unsafeBox || meth == defn.Caps_unsafeUnbox then
+      def mapArgUsing(f: Type => Type) =
         val arg :: Nil = tree.args: @unchecked
-        val argType0 = recheckStart(arg, pt)
-          .forceBoxStatus(boxed = meth == defn.Caps_unsafeBox)
+        val argType0 = f(recheckStart(arg, pt))
         val argType = super.recheckFinish(argType0, arg, pt)
         super.recheckFinish(argType, tree, pt)
+
+      if meth == defn.Caps_unsafeBox then
+        mapArgUsing(_.forceBoxStatus(true))
+      else if meth == defn.Caps_unsafeUnbox then
+        mapArgUsing(_.forceBoxStatus(false))
+      else if meth == defn.Caps_unsafeBoxFunArg then
+        mapArgUsing {
+          case defn.FunctionOf(paramtpe :: Nil, restpe, isContectual, isErased) =>
+            defn.FunctionOf(paramtpe.forceBoxStatus(true) :: Nil, restpe, isContectual, isErased)
+        }
       else
         super.recheckApply(tree, pt) match
           case appType @ CapturingType(appType1, refs) =>
@@ -432,7 +443,8 @@ class CheckCaptures extends Recheck, SymTransformer:
       block match
         case closureDef(mdef) =>
           pt.dealias match
-            case defn.FunctionOf(ptformals, _, _, _) if ptformals.forall(_.captureSet.isAlwaysEmpty) =>
+            case defn.FunctionOf(ptformals, _, _, _)
+            if ptformals.nonEmpty && ptformals.forall(_.captureSet.isAlwaysEmpty) =>
               // Redo setup of the anonymous function so that formal parameters don't
               // get capture sets. This is important to avoid false widenings to `*`
               // when taking the base type of the actual closures's dependent function
@@ -442,9 +454,10 @@ class CheckCaptures extends Recheck, SymTransformer:
               // First, undo the previous setup which installed a completer for `meth`.
               atPhase(preRecheckPhase.prev)(meth.denot.copySymDenotation())
                 .installAfter(preRecheckPhase)
+
               // Next, update all parameter symbols to match expected formals
               meth.paramSymss.head.lazyZip(ptformals).foreach { (psym, pformal) =>
-                psym.copySymDenotation(info = pformal).installAfter(preRecheckPhase)
+                psym.updateInfoBetween(preRecheckPhase, thisPhase, pformal.mapExprType)
               }
               // Next, update types of parameter ValDefs
               mdef.paramss.head.lazyZip(ptformals).foreach { (param, pformal) =>
@@ -452,36 +465,21 @@ class CheckCaptures extends Recheck, SymTransformer:
                 tpt.rememberTypeAlways(pformal)
               }
               // Next, install a new completer reflecting the new parameters for the anonymous method
+              val mt = meth.info.asInstanceOf[MethodType]
               val completer = new LazyType:
                 def complete(denot: SymDenotation)(using Context) =
-                  denot.info = MethodType(ptformals, mdef.tpt.knownType)
+                  denot.info = mt.companion(ptformals, mdef.tpt.knownType)
                     .showing(i"simplify info of $meth to $result", capt)
                   recheckDef(mdef, meth)
-              meth.copySymDenotation(info = completer, initFlags = meth.flags &~ Touched)
-                .installAfter(preRecheckPhase)
+              meth.updateInfoBetween(preRecheckPhase, thisPhase, completer)
             case _ =>
         case _ =>
       super.recheckBlock(block, pt)
 
-    /** If `rhsProto` has `*` as its capture set, wrap `rhs` in a `unsafeBox`.
-     *  Used to infer `unsafeBox` for expressions that get assigned to variables
-     *  that have universal capture set.
-     */
-    def maybeBox(rhs: Tree, rhsProto: Type)(using Context): Tree =
-      if rhsProto.captureSet.isUniversal then
-        ref(defn.Caps_unsafeBox).appliedToType(rhsProto).appliedTo(rhs)
-      else rhs
-
-    override def recheckAssign(tree: Assign)(using Context): Type =
-      val rhsProto = recheck(tree.lhs).widen
-      recheck(maybeBox(tree.rhs, rhsProto), rhsProto)
-      defn.UnitType
-
     override def recheckValDef(tree: ValDef, sym: Symbol)(using Context): Unit =
       try
         if !sym.is(Module) then // Modules are checked by checking the module class
-          if sym.is(Mutable) then recheck(maybeBox(tree.rhs, sym.info), sym.info)
-          else super.recheckValDef(tree, sym)
+          super.recheckValDef(tree, sym)
       finally
         if !sym.is(Param) then
           // Parameters with inferred types belong to anonymous methods. We need to wait
@@ -503,7 +501,8 @@ class CheckCaptures extends Recheck, SymTransformer:
     /** Class-specific capture set relations:
      *   1. The capture set of a class includes the capture sets of its parents.
      *   2. The capture set of the self type of a class includes the capture set of the class.
-     *   3. The capture set of the self type of a class includes the capture set of every class parameter.
+     *   3. The capture set of the self type of a class includes the capture set of every class parameter,
+     *      unless the parameter is marked @constructorOnly.
      */
     override def recheckClassDef(tree: TypeDef, impl: Template, cls: ClassSymbol)(using Context): Type =
       val saved = curEnv
@@ -515,7 +514,12 @@ class CheckCaptures extends Recheck, SymTransformer:
         val thisSet = cls.classInfo.selfType.captureSet.withDescription(i"of the self type of $cls")
         checkSubset(localSet, thisSet, tree.srcPos) // (2)
         for param <- cls.paramGetters do
-          checkSubset(param.termRef.captureSet, thisSet, param.srcPos) // (3)
+          if !param.hasAnnotation(defn.ConstructorOnlyAnnot) then
+            checkSubset(param.termRef.captureSet, thisSet, param.srcPos) // (3)
+        for pureBase <- cls.pureBaseClass do
+          checkSubset(thisSet,
+            CaptureSet.empty.withDescription(i"of pure base class $pureBase"),
+            tree.srcPos)
         super.recheckClassDef(tree, impl, cls)
       finally
         curEnv = saved
@@ -772,7 +776,8 @@ class CheckCaptures extends Recheck, SymTransformer:
               // We can't box/unbox the universal capability. Leave `actual` as it is
               // so we get an error in checkConforms. This tends to give better error
               // messages than disallowing the root capability in `criticalSet`.
-              capt.println(i"cannot box/unbox $actual vs $expected")
+              if ctx.settings.YccDebug.value then
+                println(i"cannot box/unbox $actual vs $expected")
               actual
             else
               // Disallow future addition of `*` to `criticalSet`.
@@ -845,13 +850,21 @@ class CheckCaptures extends Recheck, SymTransformer:
           cls => !parentTrees(cls).exists(ptree => parentTrees.contains(ptree.tpe.classSymbol))
         }
         assert(roots.nonEmpty)
-        for root <- roots do
-          checkParents(root, parentTrees(root))
+        for case root: ClassSymbol <- roots do
+          checkSelfAgainstParents(root, root.baseClasses)
           val selfType = root.asClass.classInfo.selfType
           interpolator(startingVariance = -1).traverse(selfType)
           if !root.isEffectivelySealed  then
+            def matchesExplicitRefsInBaseClass(refs: CaptureSet, cls: ClassSymbol): Boolean =
+              cls.baseClasses.tail.exists { psym =>
+                val selfType = psym.asClass.givenSelfType
+                selfType.exists && selfType.captureSet.elems == refs.elems
+              }
             selfType match
-              case CapturingType(_, refs: CaptureSet.Var) if !refs.isUniversal =>
+              case CapturingType(_, refs: CaptureSet.Var)
+              if !refs.isUniversal && !matchesExplicitRefsInBaseClass(refs, root) =>
+                // Forbid inferred self types unless they are already implied by an explicit
+                // self type in a parent.
                 report.error(
                   i"""$root needs an explicitly declared self type since its
                      |inferred self type $selfType
@@ -867,6 +880,7 @@ class CheckCaptures extends Recheck, SymTransformer:
      *   - Check that externally visible `val`s or `def`s have empty capture sets. If not,
      *     suggest an explicit type. This is so that separate compilation (where external
      *     symbols have empty capture sets) gives the same results as joint compilation.
+     *   - Check that arguments of TypeApplys and AppliedTypes conform to their bounds.
      */
     def postCheck(unit: tpd.Tree)(using Context): Unit =
       unit.foreachSubTree {
@@ -885,15 +899,23 @@ class CheckCaptures extends Recheck, SymTransformer:
           val isLocal =
             sym.owner.ownersIterator.exists(_.isTerm)
             || sym.accessBoundary(defn.RootClass).isContainedIn(sym.topLevelClass)
-
-          // The following classes of definitions need explicit capture types ...
-          if !isLocal                            // ... since external capture types are not inferred
-            || sym.owner.is(Trait)               // ... since we do OverridingPairs checking before capture inference
-            || sym.allOverriddenSymbols.nonEmpty // ... since we do override checking before capture inference
-          then
+          def canUseInferred =    // If canUseInferred is false, all capturing types in the type of `sym` need to be given explicitly
+            sym.is(Private)                   // private symbols can always have inferred types
+            || sym.name.is(DefaultGetterName) // default getters are exempted since otherwise it would be
+                                              // too annoying. This is a hole since a defualt getter's result type
+                                              // might leak into a type variable.
+            ||                                // non-local symbols cannot have inferred types since external capture types are not inferred
+              isLocal                         // local symbols still need explicit types if
+              && !sym.owner.is(Trait)         // they are defined in a trait, since we do OverridingPairs checking before capture inference
+          def isNotPureThis(ref: CaptureRef) = ref match {
+            case ref: ThisType => !ref.cls.isPureClass
+            case _ => true
+          }
+          if !canUseInferred then
             val inferred = t.tpt.knownType
             def checkPure(tp: Type) = tp match
-              case CapturingType(_, refs) if !refs.elems.isEmpty =>
+              case CapturingType(_, refs)
+              if !refs.elems.filter(isNotPureThis).isEmpty =>
                 val resultStr = if t.isInstanceOf[DefDef] then " result" else ""
                 report.error(
                   em"""Non-local $sym cannot have an inferred$resultStr type
@@ -902,8 +924,27 @@ class CheckCaptures extends Recheck, SymTransformer:
                       |The type needs to be declared explicitly.""", t.srcPos)
               case _ =>
             inferred.foreachPart(checkPure, StopAt.Static)
+        case t @ TypeApply(fun, args) =>
+          fun.knownType.widen match
+            case tl: PolyType =>
+              val normArgs = args.lazyZip(tl.paramInfos).map { (arg, bounds) =>
+                arg.withType(arg.knownType.forceBoxStatus(
+                  bounds.hi.isBoxedCapturing | bounds.lo.isBoxedCapturing))
+              }
+              checkBounds(normArgs, tl)
+            case _ =>
         case _ =>
       }
-
+      if !ctx.reporter.errorsReported then
+        // We dont report errors here if previous errors were reported, because other
+        // errors often result in bad applied types, but flagging these bad types gives
+        // often worse error messages than the original errors.
+        val checkApplied = new TreeTraverser:
+          def traverse(t: Tree)(using Context) = t match
+            case tree: InferredTypeTree =>
+            case tree: New =>
+            case tree: TypeTree => checkAppliedTypesIn(tree.withKnownType)
+            case _ => traverseChildren(t)
+        checkApplied.traverse(unit)
   end CaptureChecker
 end CheckCaptures
diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala
index 42c80e524a6e..95f2e71437a8 100644
--- a/compiler/src/dotty/tools/dotc/cc/Setup.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala
@@ -98,7 +98,10 @@ extends tpd.TreeTraverser:
     def addCaptureRefinements(tp: Type): Type = tp match
       case _: TypeRef | _: AppliedType if tp.typeParams.isEmpty =>
         tp.typeSymbol match
-          case cls: ClassSymbol if !defn.isFunctionClass(cls) =>
+          case cls: ClassSymbol
+          if !defn.isFunctionClass(cls) && !cls.is(JavaDefined) =>
+            // We assume that Java classes can refer to capturing Scala types only indirectly,
+            // using type parameters. Hence, no need to refine them.
             cls.paramGetters.foldLeft(tp) { (core, getter) =>
               if getter.termRef.isTracked then
                 val getterType = tp.memberInfo(getter).strippedDealias
@@ -117,14 +120,14 @@ extends tpd.TreeTraverser:
         case tp: (TypeRef | AppliedType) =>
           val sym = tp.typeSymbol
           if sym.isClass then
-            tp.typeSymbol == defn.AnyClass
+            sym == defn.AnyClass
               // we assume Any is a shorthand of {*} Any, so if Any is an upper
               // bound, the type is taken to be impure.
           else superTypeIsImpure(tp.superType)
         case tp: (RefinedOrRecType | MatchType) =>
           superTypeIsImpure(tp.underlying)
         case tp: AndType =>
-          superTypeIsImpure(tp.tp1) || canHaveInferredCapture(tp.tp2)
+          superTypeIsImpure(tp.tp1) || needsVariable(tp.tp2)
         case tp: OrType =>
           superTypeIsImpure(tp.tp1) && superTypeIsImpure(tp.tp2)
         case _ =>
@@ -132,23 +135,26 @@ extends tpd.TreeTraverser:
     }.showing(i"super type is impure $tp = $result", capt)
 
     /** Should a capture set variable be added on type `tp`? */
-    def canHaveInferredCapture(tp: Type): Boolean = {
+    def needsVariable(tp: Type): Boolean = {
       tp.typeParams.isEmpty && tp.match
         case tp: (TypeRef | AppliedType) =>
           val tp1 = tp.dealias
-          if tp1 ne tp then canHaveInferredCapture(tp1)
+          if tp1 ne tp then needsVariable(tp1)
           else
             val sym = tp1.typeSymbol
-            if sym.isClass then !sym.isValueClass && sym != defn.AnyClass
+            if sym.isClass then
+              !sym.isPureClass && sym != defn.AnyClass
             else superTypeIsImpure(tp1)
         case tp: (RefinedOrRecType | MatchType) =>
-          canHaveInferredCapture(tp.underlying)
+          needsVariable(tp.underlying)
         case tp: AndType =>
-          canHaveInferredCapture(tp.tp1) && canHaveInferredCapture(tp.tp2)
+          needsVariable(tp.tp1) && needsVariable(tp.tp2)
         case tp: OrType =>
-          canHaveInferredCapture(tp.tp1) || canHaveInferredCapture(tp.tp2)
-        case CapturingType(_, refs) =>
-          refs.isConst && !refs.isUniversal
+          needsVariable(tp.tp1) || needsVariable(tp.tp2)
+        case CapturingType(parent, refs) =>
+          needsVariable(parent)
+          && refs.isConst      // if refs is a variable, no need to add another
+          && !refs.isUniversal // if refs is {*}, an added variable would not change anything
         case _ =>
           false
     }.showing(i"can have inferred capture $tp = $result", capt)
@@ -181,7 +187,7 @@ extends tpd.TreeTraverser:
         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 _ if canHaveInferredCapture(tp) =>
+      case _ if needsVariable(tp) =>
         val cs = tp.dealias match
           case CapturingType(_, refs) => CaptureSet.Var(refs.elems)
           case _ => CaptureSet.Var()
@@ -382,20 +388,18 @@ extends tpd.TreeTraverser:
           return
         tree.tpt match
           case tpt: TypeTree if tree.symbol.allOverriddenSymbols.hasNext =>
+            tree.paramss.foreach(traverse)
             transformTT(tpt, boxed = false, exact = true)
+            traverse(tree.rhs)
             //println(i"TYPE of ${tree.symbol.showLocated} = ${tpt.knownType}")
           case _ =>
-        traverseChildren(tree)
+            traverseChildren(tree)
       case tree @ ValDef(_, tpt: TypeTree, _) =>
-        val isVar = tree.symbol.is(Mutable)
-        val overrides = tree.symbol.allOverriddenSymbols.hasNext
-        //if overrides then println(i"transforming overriding ${tree.symbol}")
-        if isVar || overrides then
-          transformTT(tpt,
-              boxed = isVar,    // types of mutable variables are boxed
-              exact = overrides // types of symbols that override a parent don't get a capture set
-            )
-        traverseChildren(tree)
+        transformTT(tpt,
+          boxed = tree.symbol.is(Mutable),    // types of mutable variables are boxed
+          exact = tree.symbol.allOverriddenSymbols.hasNext // types of symbols that override a parent don't get a capture set
+        )
+        traverse(tree.rhs)
       case tree @ TypeApply(fn, args) =>
         traverse(fn)
         for case arg: TypeTree <- args do
diff --git a/compiler/src/dotty/tools/dotc/cc/Synthetics.scala b/compiler/src/dotty/tools/dotc/cc/Synthetics.scala
index e8f7fd502baa..dacbd27e0f35 100644
--- a/compiler/src/dotty/tools/dotc/cc/Synthetics.scala
+++ b/compiler/src/dotty/tools/dotc/cc/Synthetics.scala
@@ -31,10 +31,12 @@ object Synthetics:
    *  The types of these symbols are transformed in a special way without
    *  looking at the definitions's RHS
    */
-  def needsTransform(sym: SymDenotation)(using Context): Boolean =
-    isSyntheticCopyMethod(sym)
-    || isSyntheticCompanionMethod(sym, nme.apply, nme.unapply)
-    || isSyntheticCopyDefaultGetterMethod(sym)
+  def needsTransform(symd: SymDenotation)(using Context): Boolean =
+    isSyntheticCopyMethod(symd)
+    || isSyntheticCompanionMethod(symd, nme.apply, nme.unapply)
+    || isSyntheticCopyDefaultGetterMethod(symd)
+    || (symd.symbol eq defn.Object_eq)
+    || (symd.symbol eq defn.Object_ne)
 
   /** Method is excluded from regular capture checking.
    *  Excluded are synthetic class members
@@ -141,13 +143,16 @@ object Synthetics:
   /** Drop added capture information from the type of an `unapply` */
   private def dropUnapplyCaptures(info: Type)(using Context): Type = info match
     case info: MethodType =>
-      val CapturingType(oldParamInfo, _) :: Nil = info.paramInfos: @unchecked
-      def oldResult(tp: Type): Type = tp match
-        case tp: MethodOrPoly =>
-          tp.derivedLambdaType(resType = oldResult(tp.resType))
-        case CapturingType(tp, _) =>
-          tp
-      info.derivedLambdaType(paramInfos = oldParamInfo :: Nil, resType = oldResult(info.resType))
+      info.paramInfos match
+        case CapturingType(oldParamInfo, _) :: Nil =>
+          def oldResult(tp: Type): Type = tp match
+            case tp: MethodOrPoly =>
+              tp.derivedLambdaType(resType = oldResult(tp.resType))
+            case CapturingType(tp, _) =>
+              tp
+          info.derivedLambdaType(paramInfos = oldParamInfo :: Nil, resType = oldResult(info.resType))
+        case _ =>
+          info
     case info: PolyType =>
       info.derivedLambdaType(resType = dropUnapplyCaptures(info.resType))
 
@@ -163,7 +168,9 @@ object Synthetics:
       sym.copySymDenotation(info = addUnapplyCaptures(sym.info))
     case nme.apply | nme.copy =>
       sym.copySymDenotation(info = addCaptureDeps(sym.info))
-
+    case n if n == nme.eq || n == nme.ne =>
+      sym.copySymDenotation(info =
+        MethodType(defn.ObjectType.capturing(CaptureSet.universal) :: Nil, defn.BooleanType))
 
   /** If `sym` refers to a synthetic apply, unapply, copy, or copy default getter method
    *  of a case class, transform it back to what it was before the CC phase.
@@ -176,5 +183,7 @@ object Synthetics:
       sym.copySymDenotation(info = dropUnapplyCaptures(sym.info))
     case nme.apply | nme.copy =>
       sym.copySymDenotation(info = dropCaptureDeps(sym.info))
+    case n if n == nme.eq || n == nme.ne =>
+      sym.copySymDenotation(info = defn.methOfAnyRef(defn.BooleanType))
 
 end Synthetics
\ No newline at end of file
diff --git a/compiler/src/dotty/tools/dotc/config/Feature.scala b/compiler/src/dotty/tools/dotc/config/Feature.scala
index d836716c3901..e7117f542384 100644
--- a/compiler/src/dotty/tools/dotc/config/Feature.scala
+++ b/compiler/src/dotty/tools/dotc/config/Feature.scala
@@ -79,19 +79,27 @@ object Feature:
 
   def scala2ExperimentalMacroEnabled(using Context) = enabled(scala2macros)
 
+  /** Is pureFunctions enabled for this compilation unit? */
   def pureFunsEnabled(using Context) =
     enabledBySetting(pureFunctions)
     || ctx.compilationUnit.knowsPureFuns
     || ccEnabled
 
+  /** Is captureChecking enabled for this compilation unit? */
   def ccEnabled(using Context) =
     enabledBySetting(captureChecking)
     || ctx.compilationUnit.needsCaptureChecking
 
+  /** Is pureFunctions enabled for any of the currently compiled compilation units? */
   def pureFunsEnabledSomewhere(using Context) =
     enabledBySetting(pureFunctions)
-    || enabledBySetting(captureChecking)
     || ctx.run != null && ctx.run.nn.pureFunsImportEncountered
+    || ccEnabledSomewhere
+
+  /** Is captureChecking enabled for any of the currently compiled compilation units? */
+  def ccEnabledSomewhere(using Context) =
+    enabledBySetting(captureChecking)
+    || ctx.run != null && ctx.run.nn.ccImportEncountered
 
   def sourceVersionSetting(using Context): SourceVersion =
     SourceVersion.valueOf(ctx.settings.source.value)
@@ -143,6 +151,11 @@ object Feature:
   def isExperimentalEnabled(using Context): Boolean =
     Properties.experimental && !ctx.settings.YnoExperimental.value
 
+  /** Handle language import `import language.<prefix>.<imported>` if it is one
+   *  of the global imports `pureFunctions` or `captureChecking`. In this case
+   *  make the compilation unit's and current run's fields accordingly.
+   *  @return true iff import that was handled
+   */
   def handleGlobalLanguageImport(prefix: TermName, imported: Name)(using Context): Boolean =
     val fullFeatureName = QualifiedName(prefix, imported.asTermName)
     if fullFeatureName == pureFunctions then
@@ -151,7 +164,7 @@ object Feature:
       true
     else if fullFeatureName == captureChecking then
       ctx.compilationUnit.needsCaptureChecking = true
-      if ctx.run != null then ctx.run.nn.pureFunsImportEncountered = true
+      if ctx.run != null then ctx.run.nn.ccImportEncountered = true
       true
     else
       false
diff --git a/compiler/src/dotty/tools/dotc/core/CheckRealizable.scala b/compiler/src/dotty/tools/dotc/core/CheckRealizable.scala
index 4b441d512dec..a61701eee2d7 100644
--- a/compiler/src/dotty/tools/dotc/core/CheckRealizable.scala
+++ b/compiler/src/dotty/tools/dotc/core/CheckRealizable.scala
@@ -149,7 +149,7 @@ class CheckRealizable(using Context) {
    */
   private def boundsRealizability(tp: Type) = {
 
-    val memberProblems = withMode(Mode.CheckBounds) {
+    val memberProblems = withMode(Mode.CheckBoundsOrSelfType) {
       for {
         mbr <- tp.nonClassTypeMembers
         if !(mbr.info.loBound <:< mbr.info.hiBound)
@@ -157,7 +157,7 @@ class CheckRealizable(using Context) {
       yield new HasProblemBounds(mbr.name, mbr.info)
     }
 
-    val refinementProblems = withMode(Mode.CheckBounds) {
+    val refinementProblems = withMode(Mode.CheckBoundsOrSelfType) {
       for {
         name <- refinedNames(tp)
         if (name.isTypeName)
diff --git a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
index 1dfa04822766..a3d8cabba971 100644
--- a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
+++ b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
@@ -58,6 +58,12 @@ trait ConstraintHandling {
    */
   protected var comparedTypeLambdas: Set[TypeLambda] = Set.empty
 
+  /** Used for match type reduction: If false, we don't recognize an abstract type
+   *  to be a subtype type of any of its base classes. This is in place only at the
+   *  toplevel; it is turned on again when we add parts of the scrutinee to the constraint.
+   */
+  protected var canWidenAbstract: Boolean = true
+
   protected var myNecessaryConstraintsOnly = false
   /** When collecting the constraints needed for a particular subtyping
    *  judgment to be true, we sometimes need to approximate the constraint
@@ -839,13 +845,17 @@ trait ConstraintHandling {
     //checkPropagated(s"adding $description")(true) // DEBUG in case following fails
     checkPropagated(s"added $description") {
       addConstraintInvocations += 1
+      val saved = canWidenAbstract
+      canWidenAbstract = true
       try bound match
         case bound: TypeParamRef if constraint contains bound =>
           addParamBound(bound)
         case _ =>
           val pbound = avoidLambdaParams(bound)
           kindCompatible(param, pbound) && addBoundTransitively(param, pbound, !fromBelow)
-      finally addConstraintInvocations -= 1
+      finally
+        canWidenAbstract = saved
+        addConstraintInvocations -= 1
     }
   end addConstraint
 
diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala
index 174244b4a456..3373fee9fce6 100644
--- a/compiler/src/dotty/tools/dotc/core/Definitions.scala
+++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala
@@ -961,9 +961,11 @@ class Definitions {
   def RuntimeTupleFunctionsModule(using Context): Symbol = requiredModule("scala.runtime.TupledFunctions")
 
   @tu lazy val CapsModule: Symbol = requiredModule("scala.caps")
-    @tu lazy val Caps_unsafeBox: Symbol = CapsModule.requiredMethod("unsafeBox")
-    @tu lazy val Caps_unsafeUnbox: Symbol = CapsModule.requiredMethod("unsafeUnbox")
     @tu lazy val captureRoot: TermSymbol = CapsModule.requiredValue("*")
+    @tu lazy val CapsUnsafeModule: Symbol = requiredModule("scala.caps.unsafe")
+    @tu lazy val Caps_unsafeBox: Symbol = CapsUnsafeModule.requiredMethod("unsafeBox")
+    @tu lazy val Caps_unsafeUnbox: Symbol = CapsUnsafeModule.requiredMethod("unsafeUnbox")
+    @tu lazy val Caps_unsafeBoxFunArg: Symbol = CapsUnsafeModule.requiredMethod("unsafeBoxFunArg")
 
   // Annotation base classes
   @tu lazy val AnnotationClass: ClassSymbol = requiredClass("scala.annotation.Annotation")
@@ -1347,6 +1349,15 @@ class Definitions {
 
   @tu lazy val untestableClasses: Set[Symbol] = Set(NothingClass, NullClass, SingletonClass)
 
+  /** Base classes that are assumed to be pure for the purposes of capture checking.
+   *  Every class inheriting from a pure baseclass is pure.
+   */
+  @tu lazy val pureBaseClasses = Set(defn.AnyValClass, defn.ThrowableClass)
+
+  /** Non-inheritable lasses that are assumed to be pure for the purposes of capture checking,
+   */
+  @tu lazy val pureSimpleClasses = Set(StringClass, NothingClass, NullClass)
+
   @tu lazy val AbstractFunctionType: Array[TypeRef] = mkArityArray("scala.runtime.AbstractFunction", MaxImplementedFunctionArity, 0).asInstanceOf[Array[TypeRef]]
   val AbstractFunctionClassPerRun: PerRun[Array[Symbol]] = new PerRun(AbstractFunctionType.map(_.symbol.asClass))
   def AbstractFunctionClass(n: Int)(using Context): Symbol = AbstractFunctionClassPerRun()(using ctx)(n)
diff --git a/compiler/src/dotty/tools/dotc/core/Mode.scala b/compiler/src/dotty/tools/dotc/core/Mode.scala
index 33ac3de70767..40a45b9f4678 100644
--- a/compiler/src/dotty/tools/dotc/core/Mode.scala
+++ b/compiler/src/dotty/tools/dotc/core/Mode.scala
@@ -70,10 +70,14 @@ object Mode {
   /** We are currently unpickling Scala2 info */
   val Scala2Unpickling: Mode = newMode(13, "Scala2Unpickling")
 
-  /** We are currently checking bounds to be non-empty, so we should not
-   *  do any widening when computing members of refined types.
+  /** Signifies one of two possible situations:
+   *   1. We are currently checking bounds to be non-empty, so we should not
+   *      do any widening when computing members of refined types.
+   *   2. We are currently checking self type conformance, so we should not
+   *      ignore capture sets added to otherwise pure classes (only needed
+   *      for capture checking).
    */
-  val CheckBounds: Mode = newMode(14, "CheckBounds")
+  val CheckBoundsOrSelfType: Mode = newMode(14, "CheckBoundsOrSelfType")
 
   /** Use Scala2 scheme for overloading and implicit resolution */
   val OldOverloadingResolution: Mode = newMode(15, "OldOverloadingResolution")
diff --git a/compiler/src/dotty/tools/dotc/core/Phases.scala b/compiler/src/dotty/tools/dotc/core/Phases.scala
index b4a2dcac1b85..205554e418ed 100644
--- a/compiler/src/dotty/tools/dotc/core/Phases.scala
+++ b/compiler/src/dotty/tools/dotc/core/Phases.scala
@@ -197,6 +197,14 @@ object Phases {
       config.println(s"nextDenotTransformerId = ${nextDenotTransformerId.toList}")
     }
 
+    /** Unlink `phase` from Denot transformer chain. This means that
+     *  any denotation transformer defined by the phase will not be executed.
+     */
+    def unlinkPhaseAsDenotTransformer(phase: Phase)(using Context) =
+      for i <- 0 until nextDenotTransformerId.length do
+        if nextDenotTransformerId(i) == phase.id then
+          nextDenotTransformerId(i) = nextDenotTransformerId(phase.id + 1)
+
     private var myParserPhase: Phase = _
     private var myTyperPhase: Phase = _
     private var myPostTyperPhase: Phase = _
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 283a7e3a474e..658bf4122aa4 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -23,7 +23,7 @@ import typer.ProtoTypes.constrained
 import typer.Applications.productSelectorTypes
 import reporting.trace
 import annotation.constructorOnly
-import cc.{CapturingType, derivedCapturingType, CaptureSet, stripCapturing, isBoxedCapturing, boxed, boxedUnlessFun, boxedIfTypeParam}
+import cc.{CapturingType, derivedCapturingType, CaptureSet, stripCapturing, isBoxedCapturing, boxed, boxedUnlessFun, boxedIfTypeParam, isAlwaysPure}
 
 /** Provides methods to compare types.
  */
@@ -60,8 +60,6 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
   /** Indicates whether the subtype check used GADT bounds */
   private var GADTused: Boolean = false
 
-  protected var canWidenAbstract: Boolean = true
-
   private var myInstance: TypeComparer = this
   def currentInstance: TypeComparer = myInstance
 
@@ -522,7 +520,9 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
         res
 
       case CapturingType(parent1, refs1) =>
-        if subCaptures(refs1, tp2.captureSet, frozenConstraint).isOK && sameBoxed(tp1, tp2, refs1)
+        if tp2.isAny then true
+        else if subCaptures(refs1, tp2.captureSet, frozenConstraint).isOK && sameBoxed(tp1, tp2, refs1)
+          || !ctx.mode.is(Mode.CheckBoundsOrSelfType) && tp1.isAlwaysPure
         then recur(parent1, tp2)
         else thirdTry
       case tp1: AnnotatedType if !tp1.isRefining =>
@@ -826,7 +826,11 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
             if refs1.isAlwaysEmpty then recur(tp1, parent2)
             else subCaptures(refs1, refs2, frozenConstraint).isOK
               && sameBoxed(tp1, tp2, refs1)
-              && recur(tp1.widen.stripCapturing, parent2)
+              && (recur(tp1.widen.stripCapturing, parent2)
+                 || tp1.isInstanceOf[SingletonType] && recur(tp1, parent2)
+                    // this alternative is needed in case the right hand side is a
+                    // capturing type that contains the lhs as an alternative of a union type.
+                 )
           catch case ex: AssertionError =>
             println(i"assertion failed while compare captured $tp1 <:< $tp2")
             throw ex
diff --git a/compiler/src/dotty/tools/dotc/core/TypeOps.scala b/compiler/src/dotty/tools/dotc/core/TypeOps.scala
index 3e3490b1f01b..9363b27b4dde 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeOps.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeOps.scala
@@ -186,7 +186,7 @@ object TypeOps:
         if (normed.exists) normed else mapOver
       case tp: MethodicType =>
         // See documentation of `Types#simplified`
-        val addTypeVars = new TypeMap:
+        val addTypeVars = new TypeMap with IdempotentCaptRefMap:
           val constraint = ctx.typerState.constraint
           def apply(t: Type): Type = t match
             case t: TypeParamRef => constraint.typeVarOfParam(t).orElse(t)
@@ -615,7 +615,7 @@ object TypeOps:
       boundss: List[TypeBounds],
       instantiate: (Type, List[Type]) => Type,
       app: Type)(
-      using Context): List[BoundsViolation] = withMode(Mode.CheckBounds) {
+      using Context): List[BoundsViolation] = withMode(Mode.CheckBoundsOrSelfType) {
     val argTypes = args.tpes
 
     /** Replace all wildcards in `tps` with `<app>#<tparam>` where `<tparam>` is the
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index 4bcd6f0d8de7..2c59be445010 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -765,11 +765,11 @@ object Types {
         val rinfo = tp.refinedInfo
         if (name.isTypeName && !pinfo.isInstanceOf[ClassInfo]) { // simplified case that runs more efficiently
           val jointInfo =
-            if rinfo.isInstanceOf[TypeAlias] && !ctx.mode.is(Mode.CheckBounds) then
+            if rinfo.isInstanceOf[TypeAlias] && !ctx.mode.is(Mode.CheckBoundsOrSelfType) then
               // In normal situations, the only way to "improve" on rinfo is to return an empty type bounds
               // So, we do not lose anything essential in "widening" to rinfo.
               // We need to compute the precise info only when checking for empty bounds
-              // which is communicated by the CheckBounds mode.
+              // which is communicated by the CheckBoundsOrSelfType mode.
               rinfo
             else if ctx.base.pendingMemberSearches.contains(name) then
               pinfo safe_& rinfo
@@ -2338,7 +2338,8 @@ object Types {
       lastDenotation match {
         case lastd0: SingleDenotation =>
           val lastd = lastd0.skipRemoved
-          if (lastd.validFor.runId == ctx.runId && (checkedPeriod != Nowhere)) finish(lastd.current)
+          if lastd.validFor.runId == ctx.runId && checkedPeriod != Nowhere then
+            finish(lastd.current)
           else lastd match {
             case lastd: SymDenotation =>
               if (stillValid(lastd) && (checkedPeriod != Nowhere)) finish(lastd.current)
@@ -2443,6 +2444,8 @@ object Types {
     }
 
     private def checkDenot()(using Context) = {}
+      //if name.toString == "getConstructor" then
+      //  println(i"set denot of $this to ${denot.info}, ${denot.getClass}, ${Phases.phaseOf(denot.validFor.lastPhaseId)} at ${ctx.phase}")
 
     private def checkSymAssign(sym: Symbol)(using Context) = {
       def selfTypeOf(sym: Symbol) =
@@ -6032,14 +6035,10 @@ object Types {
   /** A range of possible types between lower bound `lo` and upper bound `hi`.
    *  Only used internally in `ApproximatingTypeMap`.
    */
-  case class Range(lo: Type, hi: Type) extends UncachedGroundType {
+  case class Range(lo: Type, hi: Type) extends UncachedGroundType:
     assert(!lo.isInstanceOf[Range])
     assert(!hi.isInstanceOf[Range])
 
-    override def toText(printer: Printer): Text =
-      lo.toText(printer) ~ ".." ~ hi.toText(printer)
-  }
-
   /** Approximate wildcards by their bounds */
   class AvoidWildcardsMap(using Context) extends ApproximatingTypeMap:
     protected def mapWild(t: WildcardType) =
diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
index 60a5c74eedbc..e0c940fd81aa 100644
--- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
@@ -278,6 +278,8 @@ class PlainPrinter(_ctx: Context) extends Printer {
             case ex: Throwable => Str("...")
           }
         "LazyRef(" ~ refTxt ~ ")"
+      case Range(lo, hi) =>
+        toText(lo) ~ ".." ~ toText(hi)
       case _ =>
         tp.fallbackToText(this)
     }
diff --git a/compiler/src/dotty/tools/dotc/transform/Recheck.scala b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
index 6d783854ae35..0ac9087a08c0 100644
--- a/compiler/src/dotty/tools/dotc/transform/Recheck.scala
+++ b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
@@ -22,6 +22,7 @@ import StdNames.nme
 import reporting.trace
 import annotation.constructorOnly
 import cc.CaptureSet.IdempotentCaptRefMap
+import dotty.tools.dotc.core.Denotations.SingleDenotation
 
 object Recheck:
   import tpd.*
@@ -71,7 +72,7 @@ object Recheck:
       val symd = sym.denot
       symd.validFor.firstPhaseId == phase.id + 1 && (sym.originDenotation ne symd)
 
-  extension (tree: Tree)
+  extension [T <: Tree](tree: T)
 
     /** Remember `tpe` as the type of `tree`, which might be different from the
      *  type stored in the tree itself, unless a type was already remembered for `tree`.
@@ -86,11 +87,27 @@ object Recheck:
       if tpe ne tree.tpe then tree.putAttachment(RecheckedType, tpe)
 
     /** The remembered type of the tree, or if none was installed, the original type */
-    def knownType =
+    def knownType: Type =
       tree.attachmentOrElse(RecheckedType, tree.tpe)
 
     def hasRememberedType: Boolean = tree.hasAttachment(RecheckedType)
 
+    def withKnownType(using Context): T = tree.getAttachment(RecheckedType) match
+      case Some(tpe) => tree.withType(tpe).asInstanceOf[T]
+      case None => tree
+
+  extension (tpe: Type)
+
+    /** Map ExprType => T to () ?=> T (and analogously for pure versions).
+     *  Even though this phase runs after ElimByName, ExprTypes can still occur
+     *  as by-name arguments of applied types. See note in doc comment for
+     *  ElimByName phase. Test case is bynamefun.scala.
+     */
+    def mapExprType(using Context): Type = tpe match
+      case ExprType(rt) => defn.ByNameFunction(rt)
+      case _ => tpe
+
+
 /** A base class that runs a simplified typer pass over an already re-typed program. The pass
  *  does not transform trees but returns instead the re-typed type of each tree as it is
  *  traversed. The Recheck phase must be directly preceded by a phase of type PreRecheck.
@@ -116,7 +133,9 @@ abstract class Recheck extends Phase, SymTransformer:
     else sym
 
   def run(using Context): Unit =
-    newRechecker().checkUnit(ctx.compilationUnit)
+    val rechecker = newRechecker()
+    rechecker.checkUnit(ctx.compilationUnit)
+    rechecker.reset()
 
   def newRechecker()(using Context): Rechecker
 
@@ -136,6 +155,12 @@ abstract class Recheck extends Phase, SymTransformer:
      */
     def keepType(tree: Tree): Boolean = keepAllTypes
 
+    private val prevSelDenots = util.HashMap[NamedType, Denotation]()
+
+    def reset()(using Context): Unit =
+      for (ref, mbr) <- prevSelDenots.iterator do
+        ref.withDenot(mbr)
+
     /** Constant-folded rechecked type `tp` of tree `tree` */
     protected def constFold(tree: Tree, tp: Type)(using Context): Type =
       val tree1 = tree.withType(tp)
@@ -147,18 +172,42 @@ abstract class Recheck extends Phase, SymTransformer:
 
     def recheckSelect(tree: Select, pt: Type)(using Context): Type =
       val Select(qual, name) = tree
-      recheckSelection(tree, recheck(qual, AnySelectionProto).widenIfUnstable, name, pt)
+      val proto =
+        if tree.symbol == defn.Any_asInstanceOf then WildcardType
+        else AnySelectionProto
+      recheckSelection(tree, recheck(qual, proto).widenIfUnstable, name, pt)
+
+    /** When we select the `apply` of a function with type such as `(=> A) => B`,
+     *  we need to convert the parameter type `=> A` to `() ?=> A`. See doc comment
+     *  of `mapExprType`.
+     */
+    def normalizeByName(mbr: SingleDenotation)(using Context): SingleDenotation = mbr.info match
+      case mt: MethodType if mt.paramInfos.exists(_.isInstanceOf[ExprType]) =>
+        mbr.derivedSingleDenotation(mbr.symbol,
+          mt.derivedLambdaType(paramInfos = mt.paramInfos.map(_.mapExprType)))
+      case _ =>
+        mbr
 
     def recheckSelection(tree: Select, qualType: Type, name: Name,
         sharpen: Denotation => Denotation)(using Context): Type =
       if name.is(OuterSelectName) then tree.tpe
       else
         //val pre = ta.maybeSkolemizePrefix(qualType, name)
-        val mbr = sharpen(
+        val mbr = normalizeByName(
+          sharpen(
             qualType.findMember(name, qualType,
               excluded = if tree.symbol.is(Private) then EmptyFlags else Private
-          )).suchThat(tree.symbol == _)
-        constFold(tree, qualType.select(name, mbr))
+          )).suchThat(tree.symbol == _))
+        val newType = tree.tpe match
+          case prevType: NamedType =>
+            val prevDenot = prevType.denot
+            val newType = qualType.select(name, mbr)
+            if (newType eq prevType) && (mbr.info ne prevDenot.info) && !prevSelDenots.contains(prevType) then
+              prevSelDenots(prevType) = prevDenot
+            newType
+          case _ =>
+            qualType.select(name, mbr)
+        constFold(tree, newType)
           //.showing(i"recheck select $qualType . $name : ${mbr.info} = $result")
 
 
@@ -212,7 +261,8 @@ abstract class Recheck extends Phase, SymTransformer:
       mt.instantiate(argTypes)
 
     def recheckApply(tree: Apply, pt: Type)(using Context): Type =
-      recheck(tree.fun).widen match
+      val funtpe = recheck(tree.fun)
+      funtpe.widen match
         case fntpe: MethodType =>
           assert(fntpe.paramInfos.hasSameLengthAs(tree.args))
           val formals =
@@ -220,7 +270,7 @@ abstract class Recheck extends Phase, SymTransformer:
             else fntpe.paramInfos
           def recheckArgs(args: List[Tree], formals: List[Type], prefs: List[ParamRef]): List[Type] = args match
             case arg :: args1 =>
-              val argType = recheck(arg, formals.head)
+              val argType = recheck(arg, formals.head.mapExprType)
               val formals1 =
                 if fntpe.isParamDependent
                 then formals.tail.map(_.substParam(prefs.head, argType))
@@ -232,6 +282,8 @@ abstract class Recheck extends Phase, SymTransformer:
           val argTypes = recheckArgs(tree.args, formals, fntpe.paramRefs)
           constFold(tree, instantiate(fntpe, argTypes, tree.fun.symbol))
             //.showing(i"typed app $tree : $fntpe with ${tree.args}%, % : $argTypes%, % = $result")
+        case tp =>
+          assert(false, i"unexpected type of ${tree.fun}: $funtpe")
 
     def recheckTypeApply(tree: TypeApply, pt: Type)(using Context): Type =
       recheck(tree.fun).widen match
@@ -262,7 +314,7 @@ abstract class Recheck extends Phase, SymTransformer:
       recheckBlock(tree.stats, tree.expr, pt)
 
     def recheckInlined(tree: Inlined, pt: Type)(using Context): Type =
-      recheckBlock(tree.bindings, tree.expansion, pt)
+      recheckBlock(tree.bindings, tree.expansion, pt)(using inlineContext(tree.call))
 
     def recheckIf(tree: If, pt: Type)(using Context): Type =
       recheck(tree.cond, defn.BooleanType)
@@ -297,7 +349,20 @@ abstract class Recheck extends Phase, SymTransformer:
 
       val rawType = recheck(tree.expr)
       val ownType = avoidMap(rawType)
-      checkConforms(ownType, tree.from.symbol.returnProto, tree)
+
+      // The pattern matching translation, which runs before this phase
+      // sometimes instantiates return types with singleton type alternatives
+      // but the returned expression is widened. We compensate by widening the expected
+      // type as well. See also `widenSkolems` in `checkConformsExpr` which fixes
+      // a more general problem. It turns out that pattern matching returns
+      // are not checked by Ycheck, that's why these problems were allowed to slip
+      // through.
+      def widened(tp: Type): Type = tp match
+        case tp: SingletonType => tp.widen
+        case tp: AndOrType => tp.derivedAndOrType(widened(tp.tp1), widened(tp.tp2))
+        case tp @ AnnotatedType(tp1, ann) => tp.derivedAnnotatedType(widened(tp1), ann)
+        case _ => tp
+      checkConforms(ownType, widened(tree.from.symbol.returnProto), tree)
       defn.NothingType
     end recheckReturn
 
@@ -423,6 +488,27 @@ abstract class Recheck extends Phase, SymTransformer:
           throw ex
       }
 
+    /** Typing and previous transforms sometiems leaves skolem types in prefixes of
+     *  NamedTypes in `expected` that do not match the `actual` Type. -Ycheck does
+     *  not complain (need to find out why), but a full recheck does. We compensate
+     *  by de-skolemizing everywhere in `expected` except when variance is negative.
+     *  @return If `tp` contains SkolemTypes in covariant or invariant positions,
+     *          the type where these SkolemTypes are mapped to their underlying type.
+     *          Otherwise, `tp` itself
+     */
+    def widenSkolems(tp: Type)(using Context): Type =
+      object widenSkolems extends TypeMap, IdempotentCaptRefMap:
+        var didWiden: Boolean = false
+        def apply(t: Type): Type = t match
+          case t: SkolemType if variance >= 0 =>
+            didWiden = true
+            apply(t.underlying)
+          case t: LazyRef => t
+          case t @ AnnotatedType(t1, ann) => t.derivedAnnotatedType(apply(t1), ann)
+          case _ => mapOver(t)
+      val tp1 = widenSkolems(tp)
+      if widenSkolems.didWiden then tp1 else tp
+
     /** If true, print info for some successful checkConforms operations (failing ones give
      *  an error message in any case).
      */
@@ -438,11 +524,16 @@ abstract class Recheck extends Phase, SymTransformer:
 
     def checkConformsExpr(actual: Type, expected: Type, tree: Tree)(using Context): Unit =
       //println(i"check conforms $actual <:< $expected")
-      val isCompatible =
+
+      def isCompatible(expected: Type): Boolean =
         actual <:< expected
         || expected.isRepeatedParam
-            && actual <:< expected.translateFromRepeated(toArray = tree.tpe.isRef(defn.ArrayClass))
-      if !isCompatible then
+            && isCompatible(expected.translateFromRepeated(toArray = tree.tpe.isRef(defn.ArrayClass)))
+        || {
+          val widened = widenSkolems(expected)
+          (widened ne expected) && isCompatible(widened)
+        }
+      if !isCompatible(expected) then
         recheckr.println(i"conforms failed for ${tree}: $actual vs $expected")
         err.typeMismatch(tree.withType(actual), expected)
       else if debugSuccesses then
@@ -450,6 +541,7 @@ abstract class Recheck extends Phase, SymTransformer:
           case _: Ident =>
             println(i"SUCCESS $tree:\n${TypeComparer.explained(_.isSubType(actual, expected))}")
           case _ =>
+    end checkConformsExpr
 
     def checkUnit(unit: CompilationUnit)(using Context): Unit =
       recheck(unit.tpdTree)
diff --git a/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala b/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala
index 6ab0e7fc499f..dc8defa90eef 100644
--- a/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala
+++ b/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala
@@ -91,7 +91,7 @@ class TreeChecker extends Phase with SymTransformer {
     if (ctx.phaseId <= erasurePhase.id) {
       val initial = symd.initial
       assert(symd == initial || symd.signature == initial.signature,
-        i"""Signature of ${sym.showLocated} changed at phase ${ctx.phase.prevMega}
+        i"""Signature of ${sym} in ${sym.ownersIterator.toList}%, % changed at phase ${ctx.phase.prevMega}
            |Initial info: ${initial.info}
            |Initial sig : ${initial.signature}
            |Current info: ${symd.info}
diff --git a/compiler/src/dotty/tools/dotc/typer/Checking.scala b/compiler/src/dotty/tools/dotc/typer/Checking.scala
index c53213d7bd37..16499f6c1f3e 100644
--- a/compiler/src/dotty/tools/dotc/typer/Checking.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Checking.scala
@@ -67,11 +67,12 @@ object Checking {
    */
   def checkBounds(args: List[tpd.Tree], boundss: List[TypeBounds],
     instantiate: (Type, List[Type]) => Type, app: Type = NoType, tpt: Tree = EmptyTree)(using Context): Unit =
-    args.lazyZip(boundss).foreach { (arg, bound) =>
-      if !bound.isLambdaSub && !arg.tpe.hasSimpleKind then
-        errorTree(arg,
-          showInferred(MissingTypeParameterInTypeApp(arg.tpe), app, tpt))
-    }
+    if ctx.phase != Phases.checkCapturesPhase then
+      args.lazyZip(boundss).foreach { (arg, bound) =>
+        if !bound.isLambdaSub && !arg.tpe.hasSimpleKind then
+          errorTree(arg,
+            showInferred(MissingTypeParameterInTypeApp(arg.tpe), app, tpt))
+      }
     for (arg, which, bound) <- TypeOps.boundsViolations(args, boundss, instantiate, app) do
       report.error(
         showInferred(DoesNotConformToBound(arg.tpe, which, bound), app, tpt),
diff --git a/compiler/src/dotty/tools/dotc/typer/CrossVersionChecks.scala b/compiler/src/dotty/tools/dotc/typer/CrossVersionChecks.scala
index 044dd7bb8528..00b037a4e259 100644
--- a/compiler/src/dotty/tools/dotc/typer/CrossVersionChecks.scala
+++ b/compiler/src/dotty/tools/dotc/typer/CrossVersionChecks.scala
@@ -117,7 +117,7 @@ class CrossVersionChecks extends MiniPhase:
 
   /** Check that classes extending experimental classes or nested in experimental classes have the @experimental annotation. */
   private def checkExperimentalInheritance(cls: ClassSymbol)(using Context): Unit =
-    if !cls.isAnonymousClass && !cls.hasAnnotation(defn.ExperimentalAnnot) then
+    if !cls.isAnonymousClass && !cls.isInExperimentalScope then
       cls.info.parents.find(_.typeSymbol.isExperimental) match
         case Some(parent) =>
           report.error(em"extension of experimental ${parent.typeSymbol} must have @experimental annotation", cls.srcPos)
diff --git a/compiler/src/dotty/tools/dotc/typer/RefChecks.scala b/compiler/src/dotty/tools/dotc/typer/RefChecks.scala
index 1aa53d866b5e..8afcec4dee63 100644
--- a/compiler/src/dotty/tools/dotc/typer/RefChecks.scala
+++ b/compiler/src/dotty/tools/dotc/typer/RefChecks.scala
@@ -91,24 +91,42 @@ object RefChecks {
       cls.thisType
   }
 
+  /**  - Check that self type of `cls` conforms to self types of all `parents` as seen from
+   *     `cls.thisType`
+   *   - If self type of `cls` is explicit, check that it conforms to the self types
+   *     of all its class symbols.
+   *  @param deep  If true and a self type of a parent is not given explicitly, recurse to
+   *               check against the parents of the parent. This is needed when capture checking,
+   *               since we assume (& check) that the capture set of an inferred self type
+   *               is the intersection of the capture sets of all its parents
+   */
+  def checkSelfAgainstParents(cls: ClassSymbol, parents: List[Symbol])(using Context): Unit =
+    withMode(Mode.CheckBoundsOrSelfType) {
+      val cinfo = cls.classInfo
+
+      def checkSelfConforms(other: ClassSymbol, category: String, relation: String) =
+        val otherSelf = other.declaredSelfTypeAsSeenFrom(cls.thisType)
+        if otherSelf.exists then
+          if !(cinfo.selfType <:< otherSelf) then
+            report.error(DoesNotConformToSelfType(category, cinfo.selfType, cls, otherSelf, relation, other),
+              cls.srcPos)
+
+      for psym <- parents do
+        checkSelfConforms(psym.asClass, "illegal inheritance", "parent")
+      for reqd <- cls.asClass.givenSelfType.classSymbols do
+        if reqd != cls then
+          checkSelfConforms(reqd, "missing requirement", "required")
+    }
+  end checkSelfAgainstParents
+
   /** Check that self type of this class conforms to self types of parents
    *  and required classes. Also check that only `enum` constructs extend
    *  `java.lang.Enum` and no user-written class extends ContextFunctionN.
    */
   def checkParents(cls: Symbol, parentTrees: List[Tree])(using Context): Unit = cls.info match {
     case cinfo: ClassInfo =>
-      def checkSelfConforms(other: ClassSymbol, category: String, relation: String) = {
-        val otherSelf = other.declaredSelfTypeAsSeenFrom(cls.thisType)
-        if otherSelf.exists && !(cinfo.selfType <:< otherSelf) then
-          report.error(DoesNotConformToSelfType(category, cinfo.selfType, cls, otherSelf, relation, other),
-            cls.srcPos)
-      }
       val psyms = cls.asClass.parentSyms
-      for (psym <- psyms)
-        checkSelfConforms(psym.asClass, "illegal inheritance", "parent")
-      for reqd <- cinfo.cls.givenSelfType.classSymbols do
-        if reqd != cls then
-          checkSelfConforms(reqd, "missing requirement", "required")
+      checkSelfAgainstParents(cls.asClass, psyms)
 
       def isClassExtendingJavaEnum =
         !cls.isOneOf(Enum | Trait) && psyms.contains(defn.JavaEnumClass)
@@ -774,17 +792,19 @@ object RefChecks {
 
         // For each member, check that the type of its symbol, as seen from `self`
         // can override the info of this member
-        for (name <- membersToCheck)
-          for (mbrd <- self.member(name).alternatives) {
-            val mbr = mbrd.symbol
-            val mbrType = mbr.info.asSeenFrom(self, mbr.owner)
-            if (!mbrType.overrides(mbrd.info, relaxedCheck = false, matchLoosely = true))
-              report.errorOrMigrationWarning(
-                em"""${mbr.showLocated} is not a legal implementation of `$name` in $clazz
-                    |  its type             $mbrType
-                    |  does not conform to  ${mbrd.info}""",
-                (if (mbr.owner == clazz) mbr else clazz).srcPos, from = `3.0`)
+        withMode(Mode.IgnoreCaptures) {
+          for (name <- membersToCheck)
+            for (mbrd <- self.member(name).alternatives) {
+              val mbr = mbrd.symbol
+              val mbrType = mbr.info.asSeenFrom(self, mbr.owner)
+              if (!mbrType.overrides(mbrd.info, relaxedCheck = false, matchLoosely = true))
+                report.errorOrMigrationWarning(
+                  em"""${mbr.showLocated} is not a legal implementation of `$name` in $clazz
+                      |  its type             $mbrType
+                      |  does not conform to  ${mbrd.info}""",
+                  (if (mbr.owner == clazz) mbr else clazz).srcPos, from = `3.0`)
           }
+        }
       }
 
       /** Check that inheriting a case class does not constitute a variant refinement
diff --git a/compiler/src/dotty/tools/package.scala b/compiler/src/dotty/tools/package.scala
index 57a58151acc7..4ec9ae40c421 100644
--- a/compiler/src/dotty/tools/package.scala
+++ b/compiler/src/dotty/tools/package.scala
@@ -18,7 +18,7 @@ package object tools {
      *  Flow-typing under explicit nulls will automatically insert many necessary
      *  occurrences of uncheckedNN.
      */
-    inline def uncheckedNN: T = x.asInstanceOf[T]
+    transparent inline def uncheckedNN: T = x.asInstanceOf[T]
 
     inline def toOption: Option[T] =
       if x == null then None else Some(x.asInstanceOf[T])
diff --git a/compiler/test/dotc/pos-test-pickling.blacklist b/compiler/test/dotc/pos-test-pickling.blacklist
index a7d8778d4c61..30126f07b49a 100644
--- a/compiler/test/dotc/pos-test-pickling.blacklist
+++ b/compiler/test/dotc/pos-test-pickling.blacklist
@@ -84,7 +84,6 @@ boxmap-paper.scala
 # Function types print differnt after unpickling since test mispredicts Feature.preFundsEnabled
 caps-universal.scala
 
-
 # GADT cast applied to singleton type difference
 i4176-gadt.scala
 
diff --git a/library/src/scala/caps.scala b/library/src/scala/caps.scala
index 21b2f7a4dece..fb1721f98b35 100644
--- a/library/src/scala/caps.scala
+++ b/library/src/scala/caps.scala
@@ -7,12 +7,26 @@ import annotation.experimental
   /** The universal capture reference */
   val `*`: Any = ()
 
-  /** If argument is of type `cs T`, converts to type `box cs T`. This
-   *  avoids the error that would be raised when boxing `*`.
-   */
-  extension [T](x: T) def unsafeBox: T = x
+  object unsafe:
+
+    /** If argument is of type `cs T`, converts to type `box cs T`. This
+     *  avoids the error that would be raised when boxing `*`.
+     */
+    extension [T](x: T) def unsafeBox: T = x
+
+    /** If argument is of type `box cs T`, converts to type `cs T`. This
+     *  avoids the error that would be raised when unboxing `*`.
+     */
+    extension [T](x: T) def unsafeUnbox: T = x
+
+    /** If argument is of type `box cs T`, converts to type `cs T`. This
+     *  avoids the error that would be raised when unboxing `*`.
+     */
+    extension [T, U](f: T => U) def unsafeBoxFunArg: T => U = f
+  end unsafe
 
-  /** If argument is of type `box cs T`, converts to type `cs T`. This
-   *  avoids the error that would be raised when unboxing `*`.
+  /** Mixing in this trait forces a trait or class to be pure, i.e.
+   *  have no capabilities retained in its self type.
    */
-  extension [T](x: T) def unsafeUnbox: T = x
+  trait Pure:
+    this: Pure =>
diff --git a/project/MiMaFilters.scala b/project/MiMaFilters.scala
index 81510d22d2c2..408930bbeee9 100644
--- a/project/MiMaFilters.scala
+++ b/project/MiMaFilters.scala
@@ -19,5 +19,7 @@ object MiMaFilters {
     ProblemFilters.exclude[MissingClassProblem]("scala.runtime.stdLibPatches.language$experimental$pureFunctions$"),
     ProblemFilters.exclude[MissingClassProblem]("scala.runtime.stdLibPatches.language$experimental$captureChecking$"),
     ProblemFilters.exclude[MissingClassProblem]("scala.caps"),
+    ProblemFilters.exclude[MissingClassProblem]("scala.caps$Pure"),
+    ProblemFilters.exclude[MissingClassProblem]("scala.caps$unsafe$"),
   )
 }
diff --git a/tests/neg-custom-args/captures/boundschecks.scala b/tests/neg-custom-args/captures/boundschecks.scala
new file mode 100644
index 000000000000..cf4eab28f19d
--- /dev/null
+++ b/tests/neg-custom-args/captures/boundschecks.scala
@@ -0,0 +1,18 @@
+object test {
+
+  class Tree
+
+  def f[X <: Tree](x: X): Unit = ()
+
+  class C[X <: Tree](x: X)
+
+  def foo(t: {*} Tree) =
+    f(t) // error
+    f[{*} Tree](t) // error
+    f[Tree](t)  // error
+    val c1 = C(t) // error
+    val c2 = C[{*} Tree](t) // error
+    val c3 = C[Tree](t)  // error
+
+    val foo: C[{*} Tree] = ???
+}
diff --git a/tests/neg-custom-args/captures/boundschecks2.scala b/tests/neg-custom-args/captures/boundschecks2.scala
new file mode 100644
index 000000000000..f6927b04931b
--- /dev/null
+++ b/tests/neg-custom-args/captures/boundschecks2.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] = ??? // error
+  type T = C[{*} Tree] // error
+  val bar: T -> T = ???
+  val baz: C[{*} Tree] -> Unit = ??? // error
+}
diff --git a/tests/neg-custom-args/captures/capt-depfun.scala b/tests/neg-custom-args/captures/capt-depfun.scala
index a74764f432c7..c01eed7c4b25 100644
--- a/tests/neg-custom-args/captures/capt-depfun.scala
+++ b/tests/neg-custom-args/captures/capt-depfun.scala
@@ -1,8 +1,9 @@
 import annotation.retains
 class C
 type Cap = C @retains(caps.*)
+class Str
 
 def f(y: Cap, z: Cap) =
   def g(): C @retains(y, z) = ???
-  val ac: ((x: Cap) => String @retains(x) => String @retains(x)) = ???
-  val dc: (({y, z} String) => {y, z} String) = ac(g()) // error
+  val ac: ((x: Cap) => Str @retains(x) => Str @retains(x)) = ???
+  val dc: (({y, z} Str) => {y, z} Str) = ac(g()) // error
diff --git a/tests/neg-custom-args/captures/capt-depfun2.scala b/tests/neg-custom-args/captures/capt-depfun2.scala
index 74b9441593c1..52dd74aabf9f 100644
--- a/tests/neg-custom-args/captures/capt-depfun2.scala
+++ b/tests/neg-custom-args/captures/capt-depfun2.scala
@@ -1,11 +1,12 @@
 import annotation.retains
 class C
 type Cap = C @retains(caps.*)
+class Str
 
 def f(y: Cap, z: Cap) =
   def g(): C @retains(y, z) = ???
-  val ac: ((x: Cap) => Array[String @retains(x)]) = ???
-  val dc = ac(g()) // error: Needs explicit type Array[? >: String <: {y, z} String]
+  val ac: ((x: Cap) => Array[Str @retains(x)]) = ???
+  val dc = ac(g()) // error: Needs explicit type Array[? >: Str <: {y, z} Str]
                    // This is a shortcoming of rechecking since the originally inferred
-                   // type is `Array[String]` and the actual type after rechecking
-                   // cannot be expressed as `Array[C String]` for any capture set C
\ No newline at end of file
+                   // type is `Array[Str]` and the actual type after rechecking
+                   // cannot be expressed as `Array[C Str]` for any capture set C
\ No newline at end of file
diff --git a/tests/neg-custom-args/captures/cc-this.check b/tests/neg-custom-args/captures/cc-this.check
index c492df15078f..0049f42a5db5 100644
--- a/tests/neg-custom-args/captures/cc-this.check
+++ b/tests/neg-custom-args/captures/cc-this.check
@@ -9,10 +9,7 @@
 10 |  class C2(val x: () => Int): // error
    |               ^
    |        reference (C2.this.x : () => Int) is not included in allowed capture set {} of the self type of class C2
--- [E058] Type Mismatch Error: tests/neg-custom-args/captures/cc-this.scala:17:8 ---------------------------------------
+-- Error: tests/neg-custom-args/captures/cc-this.scala:17:8 ------------------------------------------------------------
 17 |  class C4(val f: () => Int) extends C3 // error
-   |        ^
-   |        illegal inheritance: self type {C4.this.f} C4 of class C4 does not conform to self type C3
-   |        of parent class C3
-   |
-   | longer explanation available when compiling with `-explain`
+   |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   |  reference (C4.this.f : () => Int) is not included in allowed capture set {} of pure base class class C3
diff --git a/tests/neg-custom-args/captures/cc-this2.check b/tests/neg-custom-args/captures/cc-this2.check
index d10519636ca8..086524d307a2 100644
--- a/tests/neg-custom-args/captures/cc-this2.check
+++ b/tests/neg-custom-args/captures/cc-this2.check
@@ -1,8 +1,6 @@
 
--- [E058] Type Mismatch Error: tests/neg-custom-args/captures/cc-this2/D_2.scala:2:6 -----------------------------------
+-- Error: tests/neg-custom-args/captures/cc-this2/D_2.scala:2:6 --------------------------------------------------------
 2 |class D extends C: // error
-  |      ^
-  |      illegal inheritance: self type {*} D of class D does not conform to self type C
-  |      of parent class C
-  |
-  | longer explanation available when compiling with `-explain`
+  |^
+  |reference (scala.caps.* : Any) is not included in allowed capture set {} of pure base class class C
+3 |  this: {*} D =>
diff --git a/tests/neg-custom-args/captures/exception-definitions.check b/tests/neg-custom-args/captures/exception-definitions.check
new file mode 100644
index 000000000000..aca5d9217d64
--- /dev/null
+++ b/tests/neg-custom-args/captures/exception-definitions.check
@@ -0,0 +1,17 @@
+-- Error: tests/neg-custom-args/captures/exception-definitions.scala:2:6 -----------------------------------------------
+2 |class Err extends Exception: // error
+  |^
+  |reference (scala.caps.* : Any) is not included in allowed capture set {} of pure base class class Throwable
+3 |  self: {*} Err =>
+-- Error: tests/neg-custom-args/captures/exception-definitions.scala:10:6 ----------------------------------------------
+10 |class Err4(c: {*} Any) extends AnyVal // error
+   |^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   |reference (Err4.this.c : {*} Any) is not included in allowed capture set {} of pure base class class AnyVal
+-- Error: tests/neg-custom-args/captures/exception-definitions.scala:7:12 ----------------------------------------------
+7 |    val x = c  // error
+  |            ^
+  |(c : {*} Any) cannot be referenced here; it is not included in the allowed capture set {} of pure base class class Throwable
+-- Error: tests/neg-custom-args/captures/exception-definitions.scala:8:8 -----------------------------------------------
+8 |  class Err3(c: {*} Any) extends Exception // error
+  |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+  |  reference (Err3.this.c : {*} Any) is not included in allowed capture set {} of pure base class class Throwable
diff --git a/tests/neg-custom-args/captures/exception-definitions.scala b/tests/neg-custom-args/captures/exception-definitions.scala
new file mode 100644
index 000000000000..9f3539b7febf
--- /dev/null
+++ b/tests/neg-custom-args/captures/exception-definitions.scala
@@ -0,0 +1,12 @@
+
+class Err extends Exception: // error
+  self: {*} Err =>
+
+def test(c: {*} Any) =
+  class Err2 extends Exception:
+    val x = c  // error
+  class Err3(c: {*} Any) extends Exception // error
+
+class Err4(c: {*} Any) extends AnyVal // error
+
+
diff --git a/tests/neg-custom-args/captures/i15116.check b/tests/neg-custom-args/captures/i15116.check
index 83c552087646..8b8d2d2e091b 100644
--- a/tests/neg-custom-args/captures/i15116.check
+++ b/tests/neg-custom-args/captures/i15116.check
@@ -9,7 +9,7 @@
 5 |  val x = Foo(m)   // error
   |  ^^^^^^^^^^^^^^
   |  Non-local value x cannot have an inferred type
-  |  {Baz.this} Foo{m: {Baz.this} String}
+  |  {Baz.this} Foo{m: {*} String}
   |  with non-empty capture set {Baz.this}.
   |  The type needs to be declared explicitly.
 -- Error: tests/neg-custom-args/captures/i15116.scala:7:6 --------------------------------------------------------------
@@ -23,6 +23,6 @@
 9 |  val x = Foo(m)   // error
   |  ^^^^^^^^^^^^^^
   |  Non-local value x cannot have an inferred type
-  |  {Baz2.this} Foo{m: {Baz2.this} String}
+  |  {Baz2.this} Foo{m: {*} String}
   |  with non-empty capture set {Baz2.this}.
   |  The type needs to be declared explicitly.
diff --git a/tests/neg-custom-args/captures/lazylist.check b/tests/neg-custom-args/captures/lazylist.check
index e43538ad97f7..1ad705556b88 100644
--- a/tests/neg-custom-args/captures/lazylist.check
+++ b/tests/neg-custom-args/captures/lazylist.check
@@ -5,6 +5,13 @@
    |        method tail of type -> {*} lazylists.LazyList[Nothing] has incompatible type
    |
    | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylist.scala:17:15 -------------------------------------
+17 |  def tail = xs() // error
+   |             ^^^^
+   |             Found:    {LazyCons.this.xs} lazylists.LazyList[T]
+   |             Required: lazylists.LazyList[T]
+   |
+   | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylist.scala:35:29 -------------------------------------
 35 |  val ref1c: LazyList[Int] = ref1 // error
    |                             ^^^^
@@ -33,10 +40,3 @@
    |                                             Required: {cap1, ref3, cap3} lazylists.LazyList[Int]
    |
    | longer explanation available when compiling with `-explain`
--- Error: tests/neg-custom-args/captures/lazylist.scala:17:6 -----------------------------------------------------------
-17 |  def tail = xs() // error: cannot have an inferred type
-   |  ^^^^^^^^^^^^^^^
-   |  Non-local method tail cannot have an inferred result type
-   |  {LazyCons.this.xs} lazylists.LazyList[? T]
-   |  with non-empty capture set {LazyCons.this.xs}.
-   |  The type needs to be declared explicitly.
diff --git a/tests/neg-custom-args/captures/lazylist.scala b/tests/neg-custom-args/captures/lazylist.scala
index 56bfc3ea6da2..2674f15a0ee3 100644
--- a/tests/neg-custom-args/captures/lazylist.scala
+++ b/tests/neg-custom-args/captures/lazylist.scala
@@ -14,7 +14,7 @@ abstract class LazyList[+T]:
 class LazyCons[+T](val x: T, val xs: () => {*} LazyList[T]) extends LazyList[T]:
   def isEmpty = false
   def head = x
-  def tail = xs() // error: cannot have an inferred type
+  def tail = xs() // error
 
 object LazyNil extends LazyList[Nothing]:
   def isEmpty = true
diff --git a/tests/neg-custom-args/captures/selftype.scala b/tests/neg-custom-args/captures/selftype.scala
new file mode 100644
index 000000000000..21148f625a7a
--- /dev/null
+++ b/tests/neg-custom-args/captures/selftype.scala
@@ -0,0 +1,4 @@
+@annotation.experimental class C(x: () => Unit) extends caps.Pure // error
+
+@annotation.experimental class D(@annotation.constructorOnly x: () => Unit) extends caps.Pure // ok
+
diff --git a/tests/neg-custom-args/captures/try.check b/tests/neg-custom-args/captures/try.check
index 13aff2661b85..c9cc7f7c1b56 100644
--- a/tests/neg-custom-args/captures/try.check
+++ b/tests/neg-custom-args/captures/try.check
@@ -1,7 +1,7 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:23:49 ------------------------------------------
 23 |  val a = handle[Exception, CanThrow[Exception]] { // error
    |                                                 ^
-   |                                                 Found:    ? ({*} CT[Exception]) -> CanThrow[? Exception]
+   |                                                 Found:    ? ({*} CT[Exception]) -> CanThrow[Exception]
    |                                                 Required: CanThrow[Exception] => box {*} CT[Exception]
 24 |    (x: CanThrow[Exception]) => x
 25 |  }{
@@ -10,7 +10,7 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:29:43 ------------------------------------------
 29 |  val b = handle[Exception, () -> Nothing] {  // error
    |                                           ^
-   |                                           Found:    ? (x: {*} CT[Exception]) -> {x} () -> ? Nothing
+   |                                           Found:    ? (x: {*} CT[Exception]) -> {x} () -> Nothing
    |                                           Required: CanThrow[Exception] => () -> Nothing
 30 |    (x: CanThrow[Exception]) => () => raise(new Exception)(using x)
 31 |  } {
diff --git a/tests/neg-custom-args/captures/vars.check b/tests/neg-custom-args/captures/vars.check
index e4f28fd45e93..8fe72a76493a 100644
--- a/tests/neg-custom-args/captures/vars.check
+++ b/tests/neg-custom-args/captures/vars.check
@@ -9,7 +9,7 @@
 15 |  val u = a  // error
    |          ^
    |          Found:    (a : box {*} String -> String)
-   |          Required: {*} (x$0: ? String) -> ? String
+   |          Required: {*} (x$0: String) -> String
    |
    | longer explanation available when compiling with `-explain`
 -- Error: tests/neg-custom-args/captures/vars.scala:16:2 ---------------------------------------------------------------
@@ -25,7 +25,7 @@
 -- Error: tests/neg-custom-args/captures/vars.scala:32:8 ---------------------------------------------------------------
 32 |  local { cap3 => // error
    |  ^
-   |  The expression's type box {*} (x$0: ? String) -> ? String is not allowed to capture the root capability `*`.
+   |  The expression's type box {*} (x$0: String) -> String is not allowed to capture the root capability `*`.
    |  This usually means that a capability persists longer than its allowed lifetime.
 33 |    def g(x: String): String = if cap3 == cap3 then "" else "a"
 34 |    g
diff --git a/tests/pending/pos/i16268.scala b/tests/pending/pos/i16268.scala
new file mode 100644
index 000000000000..6b44e71a2247
--- /dev/null
+++ b/tests/pending/pos/i16268.scala
@@ -0,0 +1,25 @@
+import language.experimental.captureChecking
+class Tree
+case class Thicket(trees: List[Tree]) extends Tree
+
+def test1(segments: List[{*} Tree]) =
+  val elems = segments flatMap { (t: {*} Tree) => t match // error
+    case ts: Thicket => ts.trees.tail
+    case t => Nil
+  }
+  elems
+
+def test2(segments: List[{*} Tree]) =
+  val f = (t: {*} Tree) => t match
+    case ts: Thicket => ts.trees.tail
+    case t => Nil
+  val elems = segments.flatMap(f) // error
+  elems
+
+def test3(c: {*} Any)(segments: List[{c} Tree]) =
+  val elems = segments flatMap { (t: {c} Tree) => t match
+    case ts: Thicket => ts.trees.tail
+    case t => Nil
+  }
+  elems
+
diff --git a/tests/pos-custom-args/captures/bynamefun.scala b/tests/pos-custom-args/captures/bynamefun.scala
new file mode 100644
index 000000000000..86bad201ffc3
--- /dev/null
+++ b/tests/pos-custom-args/captures/bynamefun.scala
@@ -0,0 +1,11 @@
+object test:
+  class Plan(elem: Plan)
+  object SomePlan extends Plan(???)
+  def f1(expr: (-> Plan) -> Plan): Plan = expr(SomePlan)
+  f1 { onf => Plan(onf) }
+  def f2(expr: (=> Plan) -> Plan): Plan = ???
+  f2 { onf => Plan(onf) }
+  def f3(expr: (-> Plan) => Plan): Plan = ???
+  f1 { onf => Plan(onf) }
+  def f4(expr: (=> Plan) => Plan): Plan = ???
+  f2 { onf => Plan(onf) }
diff --git a/tests/pos-custom-args/captures/capt-test.scala b/tests/pos-custom-args/captures/capt-test.scala
index 6ee0d2a4d9f4..c61577e96eb1 100644
--- a/tests/pos-custom-args/captures/capt-test.scala
+++ b/tests/pos-custom-args/captures/capt-test.scala
@@ -21,6 +21,9 @@ def map[A, B](f: A => B)(xs: LIST[A]): LIST[B] =
 class C
 type Cap = {*} C
 
+class Foo(x: Cap):
+  this: {x} Foo =>
+
 def test(c: Cap, d: Cap) =
   def f(x: Cap): Unit = if c == x then ()
   def g(x: Cap): Unit = if d == x then ()
diff --git a/tests/pos-custom-args/captures/cmp-singleton-2.scala b/tests/pos-custom-args/captures/cmp-singleton-2.scala
new file mode 100644
index 000000000000..daaa4add3858
--- /dev/null
+++ b/tests/pos-custom-args/captures/cmp-singleton-2.scala
@@ -0,0 +1,11 @@
+class T
+class A extends T
+class B extends T
+
+def test(tp: T) =
+  val mapping: Map[A, String] = ???
+
+  tp match
+    case a: A => mapping(a) match
+      case s: String => B()
+      case null => a
diff --git a/tests/pos-custom-args/captures/cmp-singleton.scala b/tests/pos-custom-args/captures/cmp-singleton.scala
new file mode 100644
index 000000000000..45b4009f5e89
--- /dev/null
+++ b/tests/pos-custom-args/captures/cmp-singleton.scala
@@ -0,0 +1,10 @@
+class Denotation
+abstract class SingleDenotation extends Denotation
+def goRefined: Denotation =
+  val foo: Denotation = ???
+  val joint = foo
+  joint match
+    case joint: SingleDenotation =>
+      joint
+    case _ =>
+      joint
\ No newline at end of file
diff --git a/tests/pos-custom-args/captures/foreach.scala b/tests/pos-custom-args/captures/foreach.scala
new file mode 100644
index 000000000000..b7dfc49272a9
--- /dev/null
+++ b/tests/pos-custom-args/captures/foreach.scala
@@ -0,0 +1,4 @@
+import caps.unsafe.*
+def test =
+  val tasks = new collection.mutable.ArrayBuffer[() => Unit]
+  val _: Unit = tasks.foreach(((task: () => Unit) => task()).unsafeBoxFunArg)
diff --git a/tests/pos-custom-args/captures/gadt-ycheck.scala b/tests/pos-custom-args/captures/gadt-ycheck.scala
new file mode 100644
index 000000000000..946763b53e7e
--- /dev/null
+++ b/tests/pos-custom-args/captures/gadt-ycheck.scala
@@ -0,0 +1,14 @@
+package test
+
+import reflect.ClassTag
+import language.experimental.pureFunctions
+
+object Settings:
+  val OptionTag: ClassTag[Option[?]] = ClassTag(classOf[Option[?]])
+
+  class Setting[T: ClassTag](propertyClass: Option[Class[?]]):
+    def tryToSet() =
+      def update(value: Any): String = ???
+      implicitly[ClassTag[T]] match
+        case OptionTag =>
+          update(Some(propertyClass.get.getConstructor().newInstance()))
diff --git a/tests/pos-custom-args/captures/matchtypes.scala b/tests/pos-custom-args/captures/matchtypes.scala
new file mode 100644
index 000000000000..b2442277f1f7
--- /dev/null
+++ b/tests/pos-custom-args/captures/matchtypes.scala
@@ -0,0 +1,10 @@
+type HEAD[X <: NonEmptyTuple] = X match {
+  case x *: (_ <: NonEmptyTuple) => x
+}
+
+inline def head[A <: NonEmptyTuple](x: A): HEAD[A] = null.asInstanceOf[HEAD[A]]
+
+def show[A, T <: Tuple](x: A *: T) =
+  show1(head(x))
+  show1(x.head)
+def show1[A](x: A): String = ???
\ No newline at end of file
diff --git a/tests/pos-custom-args/captures/overrides.scala b/tests/pos-custom-args/captures/overrides.scala
index 66f19726ffa7..7e70afe7a327 100644
--- a/tests/pos-custom-args/captures/overrides.scala
+++ b/tests/pos-custom-args/captures/overrides.scala
@@ -12,15 +12,3 @@ class Bar extends Foo:
 class Baz extends Bar:
   override def foo = () => println("baz")
   override def bar = "baz"
-  //override def toString = bar
-
-abstract class Message:
-  protected def msg: String
-  override def toString = msg
-
-abstract class SyntaxMsg extends Message
-
-class CyclicInheritance extends SyntaxMsg:
-  def msg = "cyclic"
-
-
diff --git a/tests/pos-custom-args/captures/overrides/A.scala b/tests/pos-custom-args/captures/overrides/A.scala
new file mode 100644
index 000000000000..6a81f8562164
--- /dev/null
+++ b/tests/pos-custom-args/captures/overrides/A.scala
@@ -0,0 +1,4 @@
+abstract class Message:
+  lazy val message: String = ???
+  def rawMessage = message
+
diff --git a/tests/pos-custom-args/captures/overrides/B.scala b/tests/pos-custom-args/captures/overrides/B.scala
new file mode 100644
index 000000000000..ce4a3f20f1d2
--- /dev/null
+++ b/tests/pos-custom-args/captures/overrides/B.scala
@@ -0,0 +1,6 @@
+
+abstract class SyntaxMsg extends Message
+
+class CyclicInheritance extends SyntaxMsg
+
+
diff --git a/tests/pos-custom-args/captures/selftypes.scala b/tests/pos-custom-args/captures/selftypes.scala
new file mode 100644
index 000000000000..c1b8eefce506
--- /dev/null
+++ b/tests/pos-custom-args/captures/selftypes.scala
@@ -0,0 +1,15 @@
+  import annotation.constructorOnly
+  trait A:
+    self: A =>
+    def foo: Int
+
+  abstract class B extends A:
+    def foo: Int
+
+  class C extends B:
+    def foo = 1
+    def derived = this
+
+  class D(@constructorOnly op: Int => Int) extends C:
+    val x = 1//op(1)
+
diff --git a/tests/pos-custom-args/captures/unsafe-unbox.scala b/tests/pos-custom-args/captures/unsafe-unbox.scala
index e846a7db1b69..b228d8c07925 100644
--- a/tests/pos-custom-args/captures/unsafe-unbox.scala
+++ b/tests/pos-custom-args/captures/unsafe-unbox.scala
@@ -1,4 +1,4 @@
-import caps.*
+import caps.unsafe.*
 def test =
   var finalizeActions = collection.mutable.ListBuffer[() => Unit]()
   val action = finalizeActions.remove(0).unsafeUnbox
diff --git a/tests/pos-custom-args/captures/vars1.scala b/tests/pos-custom-args/captures/vars1.scala
index 8c2f2cb8b5d5..c008bac2e72f 100644
--- a/tests/pos-custom-args/captures/vars1.scala
+++ b/tests/pos-custom-args/captures/vars1.scala
@@ -1,4 +1,4 @@
-import caps.*
+import caps.unsafe.*
 
 object Test:
   type ErrorHandler = (Int, String) => Unit
@@ -11,15 +11,11 @@ object Test:
 
   def defaultIncompleteHandler1(): ErrorHandler = ???
   val defaultIncompleteHandler2: ErrorHandler = ???
-  var incompleteHandler1: ErrorHandler = defaultIncompleteHandler1()
-  var incompleteHandler2: ErrorHandler = defaultIncompleteHandler2
-  var incompleteHandler3: ErrorHandler = defaultIncompleteHandler1().unsafeBox
-  var incompleteHandler4: ErrorHandler = defaultIncompleteHandler2.unsafeBox
-  private var incompleteHandler5 = defaultIncompleteHandler1()
-  private var incompleteHandler6 = defaultIncompleteHandler2
+  var incompleteHandler1: ErrorHandler = defaultIncompleteHandler1().unsafeBox
+  var incompleteHandler2: ErrorHandler = defaultIncompleteHandler2.unsafeBox
   private var incompleteHandler7 = defaultIncompleteHandler1().unsafeBox
   private var incompleteHandler8 = defaultIncompleteHandler2.unsafeBox
 
-  incompleteHandler1 = defaultIncompleteHandler2
+  incompleteHandler1 = defaultIncompleteHandler2.unsafeBox
   incompleteHandler1 = defaultIncompleteHandler2.unsafeBox
   val saved = incompleteHandler1.unsafeUnbox
diff --git a/tests/pos-custom-args/no-experimental/dotty-experimental.scala b/tests/pos-custom-args/no-experimental/dotty-experimental.scala
index 74e79c85eaaa..320c68dbea50 100644
--- a/tests/pos-custom-args/no-experimental/dotty-experimental.scala
+++ b/tests/pos-custom-args/no-experimental/dotty-experimental.scala
@@ -1,6 +1,6 @@
 package dotty.tools
 object test {
 
-  val x = caps.unsafeBox
+  val x = caps.unsafe.unsafeBox
 
 }
diff --git a/tests/pos/byname-purefuns-adapt/A_1.scala b/tests/pos/byname-purefuns-adapt/A_1.scala
index c98664a91a71..441dc24a8ef0 100644
--- a/tests/pos/byname-purefuns-adapt/A_1.scala
+++ b/tests/pos/byname-purefuns-adapt/A_1.scala
@@ -1,3 +1,4 @@
+class Ctx
 object A:
   def f(x: => Int) = ()
-
+  def g(op: Ctx ?=> Int) = op(using Ctx())
diff --git a/tests/pos/byname-purefuns-adapt/B_2.scala b/tests/pos/byname-purefuns-adapt/B_2.scala
index 4bcaa2e6c69b..842161c0fcbd 100644
--- a/tests/pos/byname-purefuns-adapt/B_2.scala
+++ b/tests/pos/byname-purefuns-adapt/B_2.scala
@@ -1,5 +1,8 @@
 import language.experimental.captureChecking
 object B:
   def test(x: => Int) = A.f(x)
+  def opp(using Ctx) = 0
+  A.g(opp)
+
 
 
diff --git a/tests/pos/experimental-inheritance.scala b/tests/pos/experimental-inheritance.scala
new file mode 100644
index 000000000000..78681caa3929
--- /dev/null
+++ b/tests/pos/experimental-inheritance.scala
@@ -0,0 +1,4 @@
+import annotation.experimental
+@experimental class A
+@experimental object o:
+  class B extends A
\ No newline at end of file
diff --git a/tests/run-custom-args/captures/colltest5/Test_2.scala b/tests/run-custom-args/captures/colltest5/Test_2.scala
index 934223a9840b..8c070439db80 100644
--- a/tests/run-custom-args/captures/colltest5/Test_2.scala
+++ b/tests/run-custom-args/captures/colltest5/Test_2.scala
@@ -76,7 +76,7 @@ object Test {
     val x4 = xs.head
     val y4: Int = x4
     val x5 = xs.to(List)
-    val y5: {x5} List[Int] = x5
+    val y5: List[Int] = x5
     val (xs6, xs7) = xs.partition(isEven)
     val ys6: {xs6, isEven} View[Int] = xs6
     val ys7: {xs7, isEven} View[Int] = xs7