diff --git a/compiler/src/dotty/tools/dotc/ast/tpd.scala b/compiler/src/dotty/tools/dotc/ast/tpd.scala
index 77e655bbe098..7abb8536e0ca 100644
--- a/compiler/src/dotty/tools/dotc/ast/tpd.scala
+++ b/compiler/src/dotty/tools/dotc/ast/tpd.scala
@@ -885,13 +885,20 @@ object tpd extends Trees.Instance[Type] with TypedTreeInfo {
       tree.select(defn.Any_asInstanceOf).appliedToType(tp)
     }
 
-    /** `tree.asInstanceOf[tp]` (or its box/unbox/cast equivalent when after
+    /** cast tree to `tp`, assuming no exception is raised, i.e the operation is pure */
+    def cast(tp: Type)(implicit ctx: Context): Tree = {
+      assert(tp.isValueType, i"bad cast: $tree.asInstanceOf[$tp]")
+      tree.select(if (ctx.erasedTypes) defn.Any_asInstanceOf else defn.Any_typeCast)
+        .appliedToType(tp)
+    }
+
+    /** cast `tree` to `tp` (or its box/unbox/cast equivalent when after
      *  erasure and value and non-value types are mixed),
      *  unless tree's type already conforms to `tp`.
      */
     def ensureConforms(tp: Type)(implicit ctx: Context): Tree =
       if (tree.tpe <:< tp) tree
-      else if (!ctx.erasedTypes) asInstance(tp)
+      else if (!ctx.erasedTypes) cast(tp)
       else Erasure.Boxing.adaptToType(tree, tp)
 
     /** `tree ne null` (might need a cast to be type correct) */
diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala
index 1bc6fcdb737b..6fdb1665b563 100644
--- a/compiler/src/dotty/tools/dotc/core/Definitions.scala
+++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala
@@ -277,7 +277,7 @@ class Definitions {
     lazy val Any_isInstanceOf: TermSymbol = enterT1ParameterlessMethod(AnyClass, nme.isInstanceOf_, _ => BooleanType, Final)
     lazy val Any_asInstanceOf: TermSymbol = enterT1ParameterlessMethod(AnyClass, nme.asInstanceOf_, _.paramRefs(0), Final)
     lazy val Any_typeTest: TermSymbol = enterT1ParameterlessMethod(AnyClass, nme.isInstanceOfPM, _ => BooleanType, Final | Synthetic | Artifact)
-    lazy val Any_typeCast: TermSymbol = enterT1ParameterlessMethod(AnyClass, nme.asInstanceOfPM, _.paramRefs(0), Final | Synthetic | Artifact | Erased)
+    lazy val Any_typeCast: TermSymbol = enterT1ParameterlessMethod(AnyClass, nme.asInstanceOfPM, _.paramRefs(0), Final | Synthetic | Artifact | StableRealizable)
       // generated by pattern matcher, eliminated by erasure
 
     def AnyMethods: List[TermSymbol] = List(Any_==, Any_!=, Any_equals, Any_hashCode,
@@ -680,7 +680,7 @@ class Definitions {
   lazy val ModuleSerializationProxyType: TypeRef  = ctx.requiredClassRef("scala.runtime.ModuleSerializationProxy")
   def ModuleSerializationProxyClass(implicit ctx: Context): ClassSymbol = ModuleSerializationProxyType.symbol.asClass
     lazy val ModuleSerializationProxyConstructor: TermSymbol =
-      ModuleSerializationProxyClass.requiredMethod(nme.CONSTRUCTOR, List(ClassType(WildcardType)))
+      ModuleSerializationProxyClass.requiredMethod(nme.CONSTRUCTOR, List(ClassType(TypeBounds.empty)))
 
   lazy val GenericType: TypeRef                = ctx.requiredClassRef("scala.reflect.Generic")
   def GenericClass(implicit ctx: Context): ClassSymbol    = GenericType.symbol.asClass
@@ -755,6 +755,10 @@ class Definitions {
 
     def Eql_eqlAny(implicit ctx: Context): TermSymbol = EqlModule.requiredMethod(nme.eqlAny)
 
+  lazy val TypeBoxType: TypeRef = ctx.requiredClassRef("scala.internal.TypeBox")
+
+    lazy val TypeBox_CAP: TypeSymbol = TypeBoxType.symbol.requiredType(tpnme.CAP)
+
   lazy val NotType: TypeRef = ctx.requiredClassRef("scala.implicits.Not")
   def NotClass(implicit ctx: Context): ClassSymbol = NotType.symbol.asClass
   def NotModule(implicit ctx: Context): Symbol = NotClass.companionModule
diff --git a/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala b/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala
index 90dd999e25eb..d5219751e04a 100644
--- a/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala
+++ b/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala
@@ -166,8 +166,6 @@ class OrderingConstraint(private val boundsMap: ParamBounds,
     entries != null && isBounds(entries(pnum)) && (typeVar(entries, pnum) eq tvar)
   }
 
-  private def isBounds(tp: Type) = tp.isInstanceOf[TypeBounds]
-
 // ---------- Dependency handling ----------------------------------------------
 
   def lower(param: TypeParamRef): List[TypeParamRef] = lowerLens(this, param.binder, param.paramNum)
diff --git a/compiler/src/dotty/tools/dotc/core/StdNames.scala b/compiler/src/dotty/tools/dotc/core/StdNames.scala
index f07cb119246c..c76ed0603cd2 100644
--- a/compiler/src/dotty/tools/dotc/core/StdNames.scala
+++ b/compiler/src/dotty/tools/dotc/core/StdNames.scala
@@ -326,6 +326,7 @@ object StdNames {
     val AnnotatedType: N        = "AnnotatedType"
     val AppliedTypeTree: N      = "AppliedTypeTree"
     val ArrayAnnotArg: N        = "ArrayAnnotArg"
+    val CAP: N                  = "CAP"
     val Constant: N             = "Constant"
     val ConstantType: N         = "ConstantType"
     val doubleHash: N           = "doubleHash"
diff --git a/compiler/src/dotty/tools/dotc/core/SymDenotations.scala b/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
index 93b04c5bda3e..ab0e9b3ed9d4 100644
--- a/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
+++ b/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
@@ -1790,7 +1790,7 @@ object SymDenotations {
                   case LambdaParam(_, _) :: _ =>
                     recur(tp.superType)
                   case tparams: List[Symbol @unchecked] =>
-                    new ctx.SubstApproxMap(tparams, args).apply(recur(tycon))
+                    recur(tycon).substApprox(tparams, args)
                 }
               record(tp, baseTp)
               baseTp
diff --git a/compiler/src/dotty/tools/dotc/core/TypeApplications.scala b/compiler/src/dotty/tools/dotc/core/TypeApplications.scala
index c38b777a3b20..bc0cf76094ac 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeApplications.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeApplications.scala
@@ -106,7 +106,7 @@ object TypeApplications {
     private[this] var available = (0 until args.length).toSet
     var allReplaced: Boolean = true
     def hasWildcardArg(p: TypeParamRef): Boolean =
-      p.binder == tycon && args(p.paramNum).isInstanceOf[TypeBounds]
+      p.binder == tycon && isBounds(args(p.paramNum))
     def canReduceWildcard(p: TypeParamRef): Boolean =
       !ctx.mode.is(Mode.AllowLambdaWildcardApply) || available.contains(p.paramNum)
     def atNestedLevel(op: => Type): Type = {
@@ -356,7 +356,7 @@ class TypeApplications(val self: Type) extends AnyVal {
     else dealiased match {
       case dealiased: HKTypeLambda =>
         def tryReduce =
-          if (!args.exists(_.isInstanceOf[TypeBounds])) {
+          if (!args.exists(isBounds)) {
             val followAlias = Config.simplifyApplications && {
               dealiased.resType match {
                 case AppliedType(tyconBody, dealiasedArgs) =>
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index c7918426d54c..71e032ffb7eb 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -130,21 +130,51 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
     }
   }
 
-  private[this] var approx: ApproxState = NoApprox
+  /** The current approximation state. See `ApproxState`. */
+  private[this] var approx: ApproxState = FreshApprox
   protected def approxState: ApproxState = approx
 
+  /** The original left-hand type of the comparison. Gets reset
+   *  everytime we compare components of the previous pair of types.
+   *  This type is used for capture conversion in `isSubArgs`.
+   */
+  private [this] var leftRoot: Type = _
+
   protected def isSubType(tp1: Type, tp2: Type, a: ApproxState): Boolean = {
-    val saved = approx
-    this.approx = a
+    val savedApprox = approx
+    val savedLeftRoot = leftRoot
+    if (a == FreshApprox) {
+      this.approx = NoApprox
+      this.leftRoot = tp1
+    }
+    else this.approx = a
     try recur(tp1, tp2)
     catch {
       case ex: Throwable => handleRecursive("subtype", i"$tp1 <:< $tp2", ex, weight = 2)
     }
-    finally this.approx = saved
+    finally {
+      this.approx = savedApprox
+      this.leftRoot = savedLeftRoot
+    }
   }
 
-  def isSubType(tp1: Type, tp2: Type)(implicit nc: AbsentContext): Boolean = isSubType(tp1, tp2, NoApprox)
-
+  def isSubType(tp1: Type, tp2: Type)(implicit nc: AbsentContext): Boolean = isSubType(tp1, tp2, FreshApprox)
+
+  /** The inner loop of the isSubType comparison.
+   *  Recursive calls from recur should go to recur directly if the two types
+   *  compared in the callee are essentially the same as the types compared in the
+   *  caller. "The same" means: represent essentially the same sets of values.
+   * `recur` should not be used to compare components of types. In this case
+   *  one should use `isSubType(_, _)`.
+   *  `recur` should also not be used to compare approximated versions of the original
+   *  types (as when we go from an abstract type to one of its bounds). In that case
+   *  one should use `isSubType(_, _, a)` where `a` defines the kind of approximation.
+   *
+   *  Note: Logicaly, `recur` could be nested in `isSubType`, which would avoid
+   *  the instance state consisting `approx` and `leftRoot`. But then the implemented
+   *  code would have two extra parameters for each of the many calls that go from
+   *  one sub-part of isSubType to another.
+   */
   protected def recur(tp1: Type, tp2: Type): Boolean = trace(s"isSubType ${traceInfo(tp1, tp2)} $approx", subtyping) {
 
     def monitoredIsSubType = {
@@ -277,7 +307,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
       case tp2: SuperType =>
         def compareSuper = tp1 match {
           case tp1: SuperType =>
-            isSubType(tp1.thistpe, tp2.thistpe) &&
+            recur(tp1.thistpe, tp2.thistpe) &&
             isSameType(tp1.supertpe, tp2.supertpe)
           case _ =>
             secondTry
@@ -355,7 +385,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
         }
       case tp1: SkolemType =>
         tp2 match {
-          case tp2: SkolemType if !ctx.phase.isTyper && isSubType(tp1.info, tp2.info) => true
+          case tp2: SkolemType if !ctx.phase.isTyper && recur(tp1.info, tp2.info) => true
           case _ => thirdTry
         }
       case tp1: TypeVar =>
@@ -449,7 +479,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
             // So if the constraint is not yet frozen, we do the same comparison again
             // with a frozen constraint, which means that we get a chance to do the
             // widening in `fourthTry` before adding to the constraint.
-            if (frozenConstraint) isSubType(tp1, bounds(tp2).lo)
+            if (frozenConstraint) recur(tp1, bounds(tp2).lo)
             else isSubTypeWhenFrozen(tp1, tp2)
           alwaysTrue || {
             if (canConstrain(tp2) && !approx.low)
@@ -879,7 +909,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
                 compareLower(info2, tyconIsTypeRef = true)
               case info2: ClassInfo =>
                 tycon2.name.toString.startsWith("Tuple") &&
-                  defn.isTupleType(tp2) && isSubType(tp1, tp2.toNestedPairs) ||
+                  defn.isTupleType(tp2) && recur(tp1, tp2.toNestedPairs) ||
                 tryBaseType(info2.cls)
               case _ =>
                 fourthTry
@@ -1001,44 +1031,93 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
   }
 
   /** Subtype test for corresponding arguments in `args1`, `args2` according to
-  *  variances in type parameters `tparams`.
+  *   variances in type parameters `tparams2`.
+  *   @param  tp1       The applied type containing `args1`
+  *   @param  tparams2  The type parameters of the type constructor applied to `args2`
   */
-  def isSubArgs(args1: List[Type], args2: List[Type], tp1: Type, tparams: List[ParamInfo]): Boolean =
-    if (args1.isEmpty) args2.isEmpty
-    else args2.nonEmpty && {
-      val tparam = tparams.head
-      val v = tparam.paramVariance
-
-      def compareCaptured(arg1: Type, arg2: Type): Boolean = arg1 match {
-        case arg1: TypeBounds =>
-          val captured = TypeRef(tp1, tparam.asInstanceOf[TypeSymbol])
-          isSubArg(captured, arg2)
-        case _ =>
-          false
-      }
+  def isSubArgs(args1: List[Type], args2: List[Type], tp1: Type, tparams2: List[ParamInfo]): Boolean = {
 
-      def isSubArg(arg1: Type, arg2: Type): Boolean = arg2 match {
-        case arg2: TypeBounds =>
-          arg2.contains(arg1) || compareCaptured(arg1, arg2)
-        case _ =>
-          arg1 match {
-            case arg1: TypeBounds =>
-              compareCaptured(arg1, arg2)
-            case _ =>
-              (v > 0 || isSubType(arg2, arg1)) &&
-              (v < 0 || isSubType(arg1, arg2))
-          }
-      }
+    /** The bounds of parameter `tparam`, where all references to type paramneters
+     *  are replaced by corresponding arguments (or their approximations in the case of
+     *  wildcard arguments).
+     */
+    def paramBounds(tparam: Symbol): TypeBounds =
+      tparam.info.substApprox(tparams2.asInstanceOf[List[Symbol]], args2).bounds
 
-      val arg1 = args1.head
-      val arg2 = args2.head
-      isSubArg(arg1, arg2) || {
-        // last effort: try to adapt variances of higher-kinded types if this is sound.
-        // TODO: Move this to eta-expansion?
-        val adapted2 = arg2.adaptHkVariances(tparam.paramInfo)
-        adapted2.ne(arg2) && isSubArg(arg1, adapted2)
-      }
-    } && isSubArgs(args1.tail, args2.tail, tp1, tparams.tail)
+    def recurArgs(args1: List[Type], args2: List[Type], tparams2: List[ParamInfo]): Boolean =
+      if (args1.isEmpty) args2.isEmpty
+      else args2.nonEmpty && {
+        val tparam = tparams2.head
+        val v = tparam.paramVariance
+
+        /** Try a capture conversion:
+         *  If the original left-hand type `leftRoot` is a path `p.type`,
+         *  and the current widened left type is an application with wildcard arguments
+         *  such as `C[_]`, where `X` is `C`'s type parameter corresponding to the `_` argument,
+         *  compare with `C[p.X]` instead. Otherwise return `false`.
+         *  Also do a capture conversion in either of the following cases:
+         *
+         *   - If we are after typer. We generally relax soundness requirements then.
+         *     We need the relaxed condition to correctly compute overriding relationships.
+         *     Missing this case led to AbstractMethod errors in the bootstrap.
+         *
+         *   - If we are in mode TypevarsMissContext, which means we test implicits
+         *     for eligibility. In this case, we can be more permissive, since it's
+         *     just a pre-check. This relaxation is needed since the full
+         *     implicit typing might perform an adaptation that skolemizes the
+         *     type of a synthesized tree before comparing it with an expected type.
+         *     But no such adaptation is applied for implicit eligibility
+         *     testing, so we have to compensate.
+         *
+         *  Note: Doing the capture conversion on path types is actually not necessary
+         *  since we can already deal with the situation through skolemization in Typer#captureWildcards.
+         *  But performance tests indicate that it's better to do it, since we avoid
+         *  skolemizations, which are more expensive . And, besides, capture conversion on
+         *  paths is less intrusive than skolemization.
+         */
+        def compareCaptured(arg1: TypeBounds, arg2: Type) = tparam match {
+          case tparam: Symbol
+          if leftRoot.isStable || ctx.isAfterTyper || ctx.mode.is(Mode.TypevarsMissContext) =>
+            val captured = TypeRef(leftRoot, tparam)
+            assert(captured.exists, i"$leftRoot has no member $tparam in isSubArgs($args1, $args2, $tp1, $tparams2)")
+            isSubArg(captured, arg2)
+          case _ =>
+            false
+        }
+
+        def isSubArg(arg1: Type, arg2: Type): Boolean = arg2 match {
+          case arg2: TypeBounds =>
+            val arg1norm = arg1 match {
+              case arg1: TypeBounds =>
+                tparam match {
+                  case tparam: Symbol => arg1 & paramBounds(tparam)
+                  case _ => arg1 // This case can only arise when a hk-type is illegally instantiated with a wildcard
+                }
+              case _ => arg1
+            }
+            arg2.contains(arg1norm)
+          case _ =>
+            arg1 match {
+              case arg1: TypeBounds =>
+                compareCaptured(arg1, arg2)
+              case _ =>
+                (v > 0 || isSubType(arg2, arg1)) &&
+                (v < 0 || isSubType(arg1, arg2))
+            }
+        }
+
+        val arg1 = args1.head
+        val arg2 = args2.head
+        isSubArg(arg1, arg2) || {
+          // last effort: try to adapt variances of higher-kinded types if this is sound.
+          // TODO: Move this to eta-expansion?
+          val adapted2 = arg2.adaptHkVariances(tparam.paramInfo)
+          adapted2.ne(arg2) && isSubArg(arg1, adapted2)
+        }
+      } && recurArgs(args1.tail, args2.tail, tparams2.tail)
+
+    recurArgs(args1, args2, tparams2)
+  }
 
   /** Test whether `tp1` has a base type of the form `B[T1, ..., Tn]` where
    *   - `B` derives from one of the class symbols of `tp2`,
@@ -1493,7 +1572,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
           if (common.exists) common
           else if (v > 0) glb(arg1.hiBound, arg2.hiBound)
           else if (v < 0) lub(arg1.loBound, arg2.loBound)
-          else if (arg1.isInstanceOf[TypeBounds] || arg2.isInstanceOf[TypeBounds])
+          else if (isBounds(arg1) || isBounds(arg2))
             TypeBounds(lub(arg1.loBound, arg2.loBound),
                        glb(arg1.hiBound, arg2.hiBound))
           else if (homogenizeArgs && !frozenConstraint && isSameType(arg1, arg2)) arg1
@@ -1813,6 +1892,12 @@ object TypeComparer {
   private val LoApprox = 1
   private val HiApprox = 2
 
+  /** The approximation state indicates how the pair of types currently compared
+   *  relates to the types compared originally.
+   *   - `NoApprox`: They are still the same types
+   *   - `LoApprox`: The left type is approximated (i.e widened)"
+   *   - `HiApprox`: The right type is approximated (i.e narrowed)"
+   */
   class ApproxState(private val bits: Int) extends AnyVal {
     override def toString: String = {
       val lo = if ((bits & LoApprox) != 0) "LoApprox" else ""
@@ -1827,6 +1912,12 @@ object TypeComparer {
 
   val NoApprox: ApproxState = new ApproxState(0)
 
+  /** A special approximation state to indicate that this is the first time we
+   *  compare (approximations of) this pair of types. It's converted to `NoApprox`
+   *  in `isSubType`, but also leads to `leftRoot` being set there.
+   */
+  val FreshApprox: ApproxState = new ApproxState(4)
+
   /** Show trace of comparison operations when performing `op` as result string */
   def explaining[T](say: String => Unit)(op: Context => T)(implicit ctx: Context): T = {
     val nestedCtx = ctx.fresh.setTypeComparerFn(new ExplainingTypeComparer(_))
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index 39a503cecee3..b32e29bdc9e5 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -1443,6 +1443,13 @@ object Types {
     final def substSym(from: List[Symbol], to: List[Symbol])(implicit ctx: Context): Type =
       ctx.substSym(this, from, to, null)
 
+    /** Substitute all occurrences of symbols in `from` by corresponding types in `to`.
+     *  Unlike for `subst`, the `to` types can be type bounds. A TypeBounds target
+     *  will be replaced by range that gets absorbed in an approximating type map.
+     */
+    final def substApprox(from: List[Symbol], to: List[Type])(implicit ctx: Context): Type =
+      new ctx.SubstApproxMap(from, to).apply(this)
+
 // ----- misc -----------------------------------------------------------
 
     /** Turn type into a function type.
@@ -2060,7 +2067,7 @@ object Types {
           var tp1 = argForParam(base.tp1)
           var tp2 = argForParam(base.tp2)
           val variance = tparam.paramVariance
-          if (tp1.isInstanceOf[TypeBounds] || tp2.isInstanceOf[TypeBounds] || variance == 0) {
+          if (isBounds(tp1) || isBounds(tp2) || variance == 0) {
             // compute argument as a type bounds instead of a point type
             tp1 = tp1.bounds
             tp2 = tp2.bounds
@@ -3472,6 +3479,8 @@ object Types {
       if (tparams.isEmpty) HKTypeLambda.any(args.length).typeParams else tparams
     }
 
+    def hasWildcardArg(implicit ctx: Context): Boolean = args.exists(isBounds)
+
     def derivedAppliedType(tycon: Type, args: List[Type])(implicit ctx: Context): Type =
       if ((tycon eq this.tycon) && (args eq this.args)) this
       else tycon.appliedTo(args)
@@ -3609,7 +3618,7 @@ object Types {
 
   // ----- Skolem types -----------------------------------------------
 
-  /** A skolem type reference with underlying type `binder`. */
+  /** A skolem type reference with underlying type `info` */
   case class SkolemType(info: Type) extends UncachedProxyType with ValueType with SingletonType {
     override def underlying(implicit ctx: Context): Type = info
     def derivedSkolemType(info: Type)(implicit ctx: Context): SkolemType =
@@ -4365,6 +4374,8 @@ object Types {
       tp.derivedAnnotatedType(underlying, annot)
     protected def derivedWildcardType(tp: WildcardType, bounds: Type): Type =
       tp.derivedWildcardType(bounds)
+    protected def derivedSkolemType(tp: SkolemType, info: Type): Type =
+      tp.derivedSkolemType(info)
     protected def derivedClassInfo(tp: ClassInfo, pre: Type): Type =
       tp.derivedClassInfo(pre)
     protected def derivedJavaArrayType(tp: JavaArrayType, elemtp: Type): Type =
@@ -4462,7 +4473,7 @@ object Types {
           derivedMatchType(tp, this(tp.bound), this(tp.scrutinee), tp.cases.mapConserve(this))
 
         case tp: SkolemType =>
-          tp
+          derivedSkolemType(tp, this(tp.info))
 
         case tp @ AnnotatedType(underlying, annot) =>
           val underlying1 = this(underlying)
@@ -4743,6 +4754,13 @@ object Types {
       tp.derivedWildcardType(rangeToBounds(bounds))
     }
 
+    override protected def derivedSkolemType(tp: SkolemType, info: Type): Type = info match {
+      case Range(lo, hi) =>
+        range(tp.derivedSkolemType(lo), tp.derivedSkolemType(hi))
+      case _ =>
+        tp.derivedSkolemType(info)
+    }
+
     override protected def derivedClassInfo(tp: ClassInfo, pre: Type): Type = {
       assert(!isRange(pre))
         // we don't know what to do here; this case has to be handled in subclasses
@@ -5080,4 +5098,6 @@ object Types {
   private val keepAlways: AnnotatedType => Context => Boolean = _ => _ => true
   private val keepNever: AnnotatedType => Context => Boolean = _ => _ => false
   private val keepIfRefining: AnnotatedType => Context => Boolean = tp => ctx => tp.isRefining(ctx)
+
+  val isBounds: Type => Boolean = _.isInstanceOf[TypeBounds]
 }
diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
index 909bf7a81a71..a30ddea7af1c 100644
--- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
@@ -290,7 +290,9 @@ class PlainPrinter(_ctx: Context) extends Printer {
         if (idx >= 0) selfRecName(idx + 1)
         else "{...}.this" // TODO move underlying type to an addendum, e.g. ... z3 ... where z3: ...
       case tp: SkolemType =>
-        if (homogenizedView) toText(tp.info) else toText(tp.repr)
+        if (homogenizedView) toText(tp.info)
+        else if (ctx.settings.XprintTypes.value) "<" ~ toText(tp.repr) ~ ":" ~ toText(tp.info) ~ ">"
+        else toText(tp.repr)
     }
   }
 
diff --git a/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala b/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala
index 082b737c8d81..c3b96ee9adf9 100644
--- a/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala
@@ -476,7 +476,7 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
             typeDefText(tparamsTxt, toText(rhs))
           case LambdaTypeTree(tparams, body) =>
             recur(body, tparamsText(tparams))
-          case rhs: TypeTree if rhs.typeOpt.isInstanceOf[TypeBounds] =>
+          case rhs: TypeTree if isBounds(rhs.typeOpt) =>
             typeDefText(tparamsTxt, toText(rhs))
           case rhs =>
             typeDefText(tparamsTxt, optText(rhs)(" = " ~ _))
diff --git a/compiler/src/dotty/tools/dotc/transform/CrossCastAnd.scala b/compiler/src/dotty/tools/dotc/transform/CrossCastAnd.scala
index 6b07073a886e..f23bb3d60b3c 100644
--- a/compiler/src/dotty/tools/dotc/transform/CrossCastAnd.scala
+++ b/compiler/src/dotty/tools/dotc/transform/CrossCastAnd.scala
@@ -23,7 +23,7 @@ class CrossCastAnd extends MiniPhase {
     lazy val qtype = tree.qualifier.tpe.widen
     val sym = tree.symbol
     if (sym.is(Flags.Private) && qtype.typeSymbol != sym.owner)
-      cpy.Select(tree)(tree.qualifier.asInstance(AndType(qtype.baseType(sym.owner), tree.qualifier.tpe)), tree.name)
+      cpy.Select(tree)(tree.qualifier.cast(AndType(qtype.baseType(sym.owner), tree.qualifier.tpe)), tree.name)
     else tree
   }
 }
diff --git a/compiler/src/dotty/tools/dotc/transform/Erasure.scala b/compiler/src/dotty/tools/dotc/transform/Erasure.scala
index 67aff2bd40e6..2fd68a391c43 100644
--- a/compiler/src/dotty/tools/dotc/transform/Erasure.scala
+++ b/compiler/src/dotty/tools/dotc/transform/Erasure.scala
@@ -319,8 +319,14 @@ object Erasure {
   class Typer(erasurePhase: DenotTransformer) extends typer.ReTyper with NoChecking {
     import Boxing._
 
+    def isErased(tree: Tree)(implicit ctx: Context): Boolean = tree match {
+      case TypeApply(Select(qual, _), _) if tree.symbol == defn.Any_typeCast =>
+        isErased(qual)
+      case _ => tree.symbol.isEffectivelyErased
+    }
+
     private def checkNotErased(tree: Tree)(implicit ctx: Context): tree.type = {
-      if (tree.symbol.isEffectivelyErased && !ctx.mode.is(Mode.Type))
+      if (isErased(tree) && !ctx.mode.is(Mode.Type))
         ctx.error(em"${tree.symbol} is declared as erased, but is in fact used", tree.sourcePos)
       tree
     }
diff --git a/compiler/src/dotty/tools/dotc/transform/ExplicitSelf.scala b/compiler/src/dotty/tools/dotc/transform/ExplicitSelf.scala
index 0eeac5d97aff..aec65969d706 100644
--- a/compiler/src/dotty/tools/dotc/transform/ExplicitSelf.scala
+++ b/compiler/src/dotty/tools/dotc/transform/ExplicitSelf.scala
@@ -37,7 +37,7 @@ class ExplicitSelf extends MiniPhase {
     case Select(thiz: This, name) if name.isTermName =>
       val cls = thiz.symbol.asClass
       if (cls.givenSelfType.exists && !cls.derivesFrom(tree.symbol.owner))
-        cpy.Select(tree)(thiz.asInstance(AndType(cls.classInfo.selfType, thiz.tpe)), name)
+        cpy.Select(tree)(thiz.cast(AndType(cls.classInfo.selfType, thiz.tpe)), name)
       else tree
     case _ => tree
   }
diff --git a/compiler/src/dotty/tools/dotc/transform/FunctionXXLForwarders.scala b/compiler/src/dotty/tools/dotc/transform/FunctionXXLForwarders.scala
index feacc647f917..993d12a0f974 100644
--- a/compiler/src/dotty/tools/dotc/transform/FunctionXXLForwarders.scala
+++ b/compiler/src/dotty/tools/dotc/transform/FunctionXXLForwarders.scala
@@ -34,9 +34,9 @@ class FunctionXXLForwarders extends MiniPhase with IdentityDenotTransformer {
       var idx = -1
       val argss = receiver.tpe.widenDealias.paramInfoss.map(_.map { param =>
         idx += 1
-        argsApply.appliedToArgs(List(Literal(Constant(idx)))).asInstance(param)
+        argsApply.appliedToArgs(List(Literal(Constant(idx)))).cast(param)
       })
-      ref(receiver.symbol).appliedToArgss(argss).asInstance(defn.ObjectType)
+      ref(receiver.symbol).appliedToArgss(argss).cast(defn.ObjectType)
     }
 
     val forwarders =
diff --git a/compiler/src/dotty/tools/dotc/transform/PatternMatcher.scala b/compiler/src/dotty/tools/dotc/transform/PatternMatcher.scala
index 00ebc03cff46..bbe45fa9638a 100644
--- a/compiler/src/dotty/tools/dotc/transform/PatternMatcher.scala
+++ b/compiler/src/dotty/tools/dotc/transform/PatternMatcher.scala
@@ -330,7 +330,7 @@ object PatternMatcher {
       swapBind(tree) match {
         case Typed(pat, tpt) =>
           TestPlan(TypeTest(tpt), scrutinee, tree.span,
-            letAbstract(ref(scrutinee).asInstance(tpt.tpe)) { casted =>
+            letAbstract(ref(scrutinee).cast(tpt.tpe)) { casted =>
               nonNull += casted
               patternPlan(casted, pat, onSuccess)
             })
diff --git a/compiler/src/dotty/tools/dotc/transform/ReifyQuotes.scala b/compiler/src/dotty/tools/dotc/transform/ReifyQuotes.scala
index 931450af868d..ce2c0a496cdd 100644
--- a/compiler/src/dotty/tools/dotc/transform/ReifyQuotes.scala
+++ b/compiler/src/dotty/tools/dotc/transform/ReifyQuotes.scala
@@ -282,7 +282,7 @@ class ReifyQuotes extends MacroTransform {
                 val argTpe =
                   if (tree.isType) defn.QuotedTypeType.appliedTo(tpw)
                   else defn.QuotedExprType.appliedTo(tpw)
-                val selectArg = arg.select(nme.apply).appliedTo(Literal(Constant(i))).asInstance(argTpe)
+                val selectArg = arg.select(nme.apply).appliedTo(Literal(Constant(i))).cast(argTpe)
                 val capturedArg = SyntheticValDef(UniqueName.fresh(tree.symbol.name.toTermName).toTermName, selectArg)
                 i += 1
                 embedded.addTree(tree, capturedArg.symbol)
diff --git a/compiler/src/dotty/tools/dotc/transform/Staging.scala b/compiler/src/dotty/tools/dotc/transform/Staging.scala
index 103c9ad72fe8..51d4e316d41f 100644
--- a/compiler/src/dotty/tools/dotc/transform/Staging.scala
+++ b/compiler/src/dotty/tools/dotc/transform/Staging.scala
@@ -169,7 +169,7 @@ class Staging extends MacroTransform {
      */
     protected def addSpliceCast(tree: Tree)(implicit ctx: Context): Tree = {
       val tp = checkType(tree.sourcePos).apply(tree.tpe.widenTermRefExpr)
-      tree.asInstance(tp).withSpan(tree.span)
+      tree.cast(tp).withSpan(tree.span)
     }
 
     /** If `tree` refers to a locally defined symbol (either directly, or in a pickled type),
diff --git a/compiler/src/dotty/tools/dotc/transform/SyntheticMethods.scala b/compiler/src/dotty/tools/dotc/transform/SyntheticMethods.scala
index 937ce128e2e1..7aba76cdfd80 100644
--- a/compiler/src/dotty/tools/dotc/transform/SyntheticMethods.scala
+++ b/compiler/src/dotty/tools/dotc/transform/SyntheticMethods.scala
@@ -173,7 +173,7 @@ class SyntheticMethods(thisPhase: DenotTransformer) {
       val matchExpr = Match(that, List(matchingCase, defaultCase))
       if (isDerivedValueClass(clazz)) matchExpr
       else {
-        val eqCompare = This(clazz).select(defn.Object_eq).appliedTo(that.asInstance(defn.ObjectType))
+        val eqCompare = This(clazz).select(defn.Object_eq).appliedTo(that.cast(defn.ObjectType))
         eqCompare or matchExpr
       }
     }
diff --git a/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala b/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala
index e1304633884b..dbd781357c23 100644
--- a/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala
+++ b/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala
@@ -81,7 +81,7 @@ object TypeTestsCasts {
     /** Approximate type parameters depending on variance */
     def stripTypeParam(tp: Type)(implicit ctx: Context) = new ApproximatingTypeMap {
       def apply(tp: Type): Type = tp match {
-        case tp: TypeRef if tp.underlying.isInstanceOf[TypeBounds] =>
+        case tp: TypeRef if isBounds(tp.underlying) =>
           val lo = apply(tp.info.loBound)
           val hi = apply(tp.info.hiBound)
           range(lo, hi)
diff --git a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
index 57ab59897e73..3b184b6bb9fd 100644
--- a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
+++ b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
@@ -624,7 +624,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
         if (maximize) lo else hi
 
     def apply(tp: Type): Type = tp match {
-      case tp: TypeRef if tp.underlying.isInstanceOf[TypeBounds] =>
+      case tp: TypeRef if isBounds(tp.underlying) =>
         val lo = this(tp.info.loBound)
         val hi = this(tp.info.hiBound)
         // See tests/patmat/gadt.scala  tests/patmat/exhausting.scala  tests/patmat/t9657.scala
@@ -632,7 +632,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
         debug.println(s"$tp exposed to =====> $exposed")
         exposed
 
-      case AppliedType(tycon: TypeRef, args) if tycon.underlying.isInstanceOf[TypeBounds] =>
+      case AppliedType(tycon: TypeRef, args) if isBounds(tycon.underlying) =>
         val args2 = args.map(this)
         val lo = this(tycon.info.loBound).applyIfParameterized(args2)
         val hi = this(tycon.info.hiBound).applyIfParameterized(args2)
diff --git a/compiler/src/dotty/tools/dotc/typer/Applications.scala b/compiler/src/dotty/tools/dotc/typer/Applications.scala
index b8053dff8395..d6fa2af91a19 100644
--- a/compiler/src/dotty/tools/dotc/typer/Applications.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Applications.scala
@@ -1075,7 +1075,7 @@ trait Applications extends Compatibility { self: Typer with Dynamic =>
         }
 
         var argTypes = unapplyArgs(unapplyApp.tpe, unapplyFn, args, tree.sourcePos)
-        for (argType <- argTypes) assert(!argType.isInstanceOf[TypeBounds], unapplyApp.tpe.show)
+        for (argType <- argTypes) assert(!isBounds(argType), unapplyApp.tpe.show)
         val bunchedArgs =
           if (argTypes.nonEmpty && argTypes.last.isRepeatedParam)
             args.lastOption match {
diff --git a/compiler/src/dotty/tools/dotc/typer/Checking.scala b/compiler/src/dotty/tools/dotc/typer/Checking.scala
index 904c2fe4190f..667aba1a21d2 100644
--- a/compiler/src/dotty/tools/dotc/typer/Checking.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Checking.scala
@@ -80,8 +80,8 @@ object Checking {
     if (boundsCheck) checkBounds(orderedArgs, bounds, instantiate)
 
     def checkWildcardApply(tp: Type): Unit = tp match {
-      case tp @ AppliedType(tycon, args) =>
-        if (tycon.isLambdaSub && args.exists(_.isInstanceOf[TypeBounds]))
+      case tp @ AppliedType(tycon, _) =>
+        if (tycon.isLambdaSub && tp.hasWildcardArg)
           ctx.errorOrMigrationWarning(
             ex"unreducible application of higher-kinded type $tycon to wildcard arguments",
             tree.sourcePos)
diff --git a/compiler/src/dotty/tools/dotc/typer/Deriving.scala b/compiler/src/dotty/tools/dotc/typer/Deriving.scala
index e618d8de9704..24f20cc8c5df 100644
--- a/compiler/src/dotty/tools/dotc/typer/Deriving.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Deriving.scala
@@ -409,7 +409,7 @@ trait Deriving { this: Typer =>
                 case caseType =>
                   val args =
                     for ((elemTp, idx) <- elems.zipWithIndex)
-                    yield paramRef.select(nme.apply).appliedTo(Literal(Constant(idx))).asInstance(elemTp)
+                    yield paramRef.select(nme.apply).appliedTo(Literal(Constant(idx))).cast(elemTp)
                   New(caseType, args)
               }
               shape match {
diff --git a/compiler/src/dotty/tools/dotc/typer/Dynamic.scala b/compiler/src/dotty/tools/dotc/typer/Dynamic.scala
index 75ba92e4e032..7dbaee2058fb 100644
--- a/compiler/src/dotty/tools/dotc/typer/Dynamic.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Dynamic.scala
@@ -159,7 +159,7 @@ trait Dynamic { self: Typer with Applications =>
 
     fun.tpe.widen match {
       case tpe: ValueType =>
-        structuralCall(nme.selectDynamic, Nil).asInstance(tpe)
+        structuralCall(nme.selectDynamic, Nil).cast(tpe)
 
       case tpe: MethodType =>
         def isDependentMethod(tpe: Type): Boolean = tpe match {
@@ -176,7 +176,7 @@ trait Dynamic { self: Typer with Applications =>
         else {
           val ctags = tpe.paramInfoss.flatten.map(pt =>
             implicitArgTree(defn.ClassTagType.appliedTo(pt.widenDealias :: Nil), fun.span.endPos))
-          structuralCall(nme.applyDynamic, ctags).asInstance(tpe.finalResultType)
+          structuralCall(nme.applyDynamic, ctags).cast(tpe.finalResultType)
         }
 
       // (@allanrenucci) I think everything below is dead code
diff --git a/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala b/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala
index 56923eb93cb9..560cb400eb1c 100644
--- a/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala
+++ b/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala
@@ -605,7 +605,8 @@ object ProtoTypes {
     case tp @ AppliedType(tycon, args) =>
       wildApprox(tycon, theMap, seen) match {
         case _: WildcardType => WildcardType // this ensures we get a * type
-        case tycon1 => tp.derivedAppliedType(tycon1, args.mapConserve(wildApprox(_, theMap, seen)))
+        case tycon1 => tp.derivedAppliedType(tycon1,
+          args.mapConserve(arg => wildApprox(arg, theMap, seen)))
       }
     case tp: RefinedType => // default case, inlined for speed
       tp.derivedRefinedType(
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index 79a3fe4b4040..9582fb6ce7ef 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -79,6 +79,7 @@ object Typer {
    *  search was tried on a tree. This will in some cases be reported in error messages
    */
   private[typer] val HiddenSearchFailure = new Property.Key[SearchFailure]
+
 }
 
 class Typer extends Namer
@@ -1917,7 +1918,7 @@ class Typer extends Namer
           val elemTpes = (elems, pts).zipped.map((elem, pt) =>
             ctx.typeComparer.widenInferred(elem.tpe, pt))
           val resTpe = (elemTpes :\ (defn.UnitType: Type))(defn.PairType.appliedTo(_, _))
-          app1.asInstance(resTpe)
+          app1.cast(resTpe)
         }
       }
     }
@@ -2611,7 +2612,7 @@ class Typer extends Namer
           // I suspect, but am not 100% sure that this might affect inferred types,
           // if the expected type is a supertype of the GADT bound. It would be good to come
           // up with a test case for this.
-          tree.select(defn.Any_typeCast).appliedToType(pt)
+          tree.cast(pt)
         else
           tree
       }
@@ -2697,10 +2698,47 @@ class Typer extends Namer
       case tree: Closure => cpy.Closure(tree)(tpt = TypeTree(pt)).withType(pt)
     }
 
+    /** Replace every top-level occurrence of a wildcard type argument by
+     *  a fresh skolem type. The skolem types are of the form $i.CAP, where
+     *  $i is a skolem of type `scala.internal.TypeBox`, and `CAP` is its
+     *  type member. See the documentation of `TypeBox` for a rationale why we do this.
+     */
+    def captureWildcards(tp: Type)(implicit ctx: Context): Type = tp match {
+      case tp: AndOrType => tp.derivedAndOrType(captureWildcards(tp.tp1), captureWildcards(tp.tp2))
+      case tp: RefinedType => tp.derivedRefinedType(captureWildcards(tp.parent), tp.refinedName, tp.refinedInfo)
+      case tp: RecType => tp.derivedRecType(captureWildcards(tp.parent))
+      case tp: LazyRef => captureWildcards(tp.ref)
+      case tp: AnnotatedType => tp.derivedAnnotatedType(captureWildcards(tp.parent), tp.annot)
+      case tp @ AppliedType(tycon, args) if tp.hasWildcardArg =>
+        tycon.typeParams match {
+          case tparams @ ((_: Symbol) :: _) =>
+            val boundss = tparams.map(_.paramInfo.substApprox(tparams.asInstanceOf[List[TypeSymbol]], args))
+            val args1 = args.zipWithConserve(boundss) { (arg, bounds) =>
+              arg match {
+                case TypeBounds(lo, hi) =>
+                  val skolem = SkolemType(defn.TypeBoxType.appliedTo(lo | bounds.loBound, hi & bounds.hiBound))
+                  TypeRef(skolem, defn.TypeBox_CAP)
+                case arg => arg
+              }
+            }
+            tp.derivedAppliedType(tycon, args1)
+          case _ =>
+            tp
+        }
+      case _ => tp
+    }
+
     def adaptToSubType(wtp: Type): Tree = {
       // try converting a constant to the target type
       val folded = ConstFold(tree, pt)
-      if (folded ne tree) return adaptConstant(folded, folded.tpe.asInstanceOf[ConstantType])
+      if (folded ne tree)
+        return adaptConstant(folded, folded.tpe.asInstanceOf[ConstantType])
+
+      // Try to capture wildcards in type
+      val captured = captureWildcards(wtp)
+      if (captured `ne` wtp)
+        return readapt(tree.cast(captured))
+
       // drop type if prototype is Unit
       if (pt isRef defn.UnitClass) {
         // local adaptation makes sure every adapted tree conforms to its pt
@@ -2709,6 +2747,7 @@ class Typer extends Namer
         checkStatementPurity(tree1)(tree, ctx.owner)
         return tpd.Block(tree1 :: Nil, Literal(Constant(())))
       }
+
       // convert function literal to SAM closure
       tree match {
         case closure(Nil, id @ Ident(nme.ANON_FUN), _)
@@ -2725,6 +2764,7 @@ class Typer extends Namer
           }
         case _ =>
       }
+
       // try an extension method in scope
       pt match {
         case SelectionProto(name, mbrType, _, _) =>
@@ -2749,6 +2789,7 @@ class Typer extends Namer
           }
         case _ =>
       }
+
       // try an implicit conversion
       val prevConstraint = ctx.typerState.constraint
       def recover(failure: SearchFailureType) =
diff --git a/compiler/test/dotty/tools/backend/jvm/DottyBytecodeTests.scala b/compiler/test/dotty/tools/backend/jvm/DottyBytecodeTests.scala
index ecb876bfae2a..66cecaeb3685 100644
--- a/compiler/test/dotty/tools/backend/jvm/DottyBytecodeTests.scala
+++ b/compiler/test/dotty/tools/backend/jvm/DottyBytecodeTests.scala
@@ -418,35 +418,11 @@ class TestBCode extends DottyBytecodeTest {
       val method = getMethod(moduleNode, "test")
 
       val instructions = instructionsFromMethod(method)
-      val expected = List(
-        VarOp(Opcodes.ALOAD, 1),
-        VarOp(Opcodes.ASTORE, 2),
-        VarOp(Opcodes.ALOAD, 2),
-        TypeOp(Opcodes.INSTANCEOF, "Test"),
-        Jump(Opcodes.IFEQ, Label(11)),
-        VarOp(Opcodes.ALOAD, 2),
-        TypeOp(Opcodes.CHECKCAST, "Test"),
-        VarOp(Opcodes.ASTORE, 3),
-        Field(Opcodes.GETSTATIC, "scala/Predef$", "MODULE$", "Lscala/Predef$;"),
-        Invoke(Opcodes.INVOKEVIRTUAL, "scala/Predef$", "$qmark$qmark$qmark", "()Lscala/runtime/Nothing$;", false),
-        Op(Opcodes.ATHROW),
-        Label(11),
-        FrameEntry(1, List("java/lang/Object"), List()),
-        TypeOp(Opcodes.NEW, "scala/MatchError"),
-        Op(Opcodes.DUP),
-        VarOp(Opcodes.ALOAD, 2),
-        Invoke(Opcodes.INVOKESPECIAL, "scala/MatchError", "<init>", "(Ljava/lang/Object;)V", false),
-        Op(Opcodes.ATHROW),
-        Label(18),
-        FrameEntry(0, List(), List("java/lang/Throwable")),
-        Op(Opcodes.ATHROW),
-        Label(21),
-        FrameEntry(4, List(), List("java/lang/Throwable")),
-        Op(Opcodes.ATHROW)
-      )
-      assert(instructions == expected,
-        "`test` was not properly generated\n" + diffInstructions(instructions, expected))
-
+      val hasReturn = instructions.exists {
+        case Op(Opcodes.RETURN) => true
+        case _ => false
+      }
+      assertFalse(hasReturn)
     }
   }
 
diff --git a/library/src/scala/internal/TypeBox.scala b/library/src/scala/internal/TypeBox.scala
new file mode 100644
index 000000000000..1accb4da4c22
--- /dev/null
+++ b/library/src/scala/internal/TypeBox.scala
@@ -0,0 +1,11 @@
+package scala.internal
+
+/** A type for skolems that are generated during capture conversion. Capture conversion
+ *  narrows the type of a tree whose type has wildcard arguments. A typical situation
+ *  is a tree `t` of type `C[_ >: L <: U]` and an expected type `C[X]` where `X` is an
+ *  instantiatable type variable. To be able to instantiate `X`, we cast the tree to type
+ *  `X[$n.CAP]` where `$n` is a fresh skolem type with underlying type `TypeBox[L, U]`.
+ */
+final abstract class TypeBox[-L <: U, +U] {
+  type CAP >: L <: U
+}
diff --git a/tests/neg/capture1.scala b/tests/neg/capture1.scala
new file mode 100644
index 000000000000..67ae41d5aea4
--- /dev/null
+++ b/tests/neg/capture1.scala
@@ -0,0 +1,17 @@
+// Test shows that Java soundness hole does not apply in Dotty
+import collection.mutable
+object Test extends App {
+
+  val l: mutable.Seq[String] = mutable.ArrayBuffer()
+
+  def (xs: List[T]) emap[T, U] (f: T => U): List[U] = xs.map(f)
+
+  def (xs: List[T]) ereduce[T] (f: (T, T) => T): T = xs.reduceLeft(f)
+
+  def (xs: mutable.Seq[T]) append[T] (ys: mutable.Seq[T]): mutable.Seq[T] = xs ++ ys
+
+  List(l, mutable.ArrayBuffer(1))
+    .emap(list => list)
+    .ereduce((xs, ys) => xs `append` ys) // error
+
+}
\ No newline at end of file
diff --git a/tests/neg/i4376.scala b/tests/neg/i4376.scala
new file mode 100644
index 000000000000..69daceafdbc3
--- /dev/null
+++ b/tests/neg/i4376.scala
@@ -0,0 +1,6 @@
+object App {
+  type Id[A] >: A <: A
+
+  val a: Array[_ >: Id[_ <: Int]] =
+    (Array.ofDim[String](1) : Array[_ >: Id[Nothing]]) // error
+}
\ No newline at end of file
diff --git a/tests/neg/i5948b.scala b/tests/neg/i5948b.scala
new file mode 100644
index 000000000000..0961fc8f2f0c
--- /dev/null
+++ b/tests/neg/i5948b.scala
@@ -0,0 +1,32 @@
+class Foo[T](var elem: T) { type TT = T }
+
+object Test {
+  def setFirstInPair[T](pair: (Foo[T], Foo[T])) = {
+    pair._1.elem = pair._2.elem
+  }
+
+  def setFirstInList[T](list: List[Foo[T]]) = {
+    list(0).elem = list(1).elem
+  }
+
+  def test1(): Unit = {
+    val fooInt = new Foo(1)
+    val fooString = new Foo("")
+    val pair: (Foo[_], Foo[_]) = (fooInt, fooString)
+    setFirstInPair(pair) // error
+    println(fooInt.elem + 1)
+  }
+
+  def test2(): Unit = {
+    val fooInt = new Foo(1)
+    val fooString = new Foo("")
+    val list: List[Foo[_]] = List(fooInt, fooString)
+    setFirstInList(list) // error
+    println(fooInt.elem + 1)
+  }
+
+  def main(args: Array[String]): Unit = {
+    test1()
+    test2()
+  }
+}
\ No newline at end of file
diff --git a/tests/neg/t5729.scala b/tests/neg/t5729.scala
deleted file mode 100644
index 69df11fcbbe0..000000000000
--- a/tests/neg/t5729.scala
+++ /dev/null
@@ -1,21 +0,0 @@
-trait T[X]
-object Test {
-  def join(in: Seq[T[_]]): Int = ???
-  def join[S](in: Seq[T[S]]): String = ???
-  join(null: Seq[T[_]]) // error: ambiguous
-}
-
-object C {
-  def join(in: Seq[List[_]]): Int = sys.error("TODO")
-  def join[S](in: Seq[List[S]]): String = sys.error("TODO")
-
-  join(Seq[List[Int]]()) // error: ambiguous
-  //
-  // ./a.scala:13: error: ambiguous reference to overloaded definition,
-  // both method join in object C of type [S](in: Seq[List[S]])String
-  // and  method join in object C of type (in: Seq[List[_]])Int
-  // match argument types (Seq[List[Int]])
-  //   join(Seq[List[Int]]())
-  //   ^
-  // one error found
-}
diff --git a/tests/pos/capture.scala b/tests/pos/capture.scala
new file mode 100644
index 000000000000..76a47bf497b2
--- /dev/null
+++ b/tests/pos/capture.scala
@@ -0,0 +1,37 @@
+// A condensation of shonan-hmm/Lifters.scala that shows why the approach
+// of just skolemizing a tree as a hole to prepare it for capture conversion
+// does not work.
+// I tried two different stratgegies to adapt a tree whose widened type has wildcard
+// arguments. Say the tree is `t` and the widened type is `C[_]`.
+//
+// skolemization-as-a-whole:
+//
+//    Convert `t` to  `t.cast[$i]` where `$i` is a skolem of type C[_]
+//    This then relies on capture conversion for singleton types to do the rest.
+//
+// skolemization-of-each-param:
+//
+//    Convert `t` to `t.cast[C[$j.CAP]]` where `$j` is a skolem of type `TypeBox[Nothing, Any`]
+//    (or more generally, `TypeBox[L, U]`) wgere `L` and `U` are the bounds of the wildcard).
+//
+// skolemization-of-each-param is more robust since it is stable under widening.
+// By contrast, skolemization-as-a-whole risks losing capturing ability if the skolem
+// type is widened in some context. This leads to the difference in behavior shown below.
+class Test {
+
+  abstract class Liftable[T]
+
+  implicit def ClassIsLiftable[T]: Liftable[Class[T]] = new Liftable[Class[T]] {}
+
+  class Expr[+T]
+
+  implicit class LiftExprOps[T](val x: T) {
+    def toExpr(implicit ev: Liftable[T]): Expr[T] = ???
+  }
+
+  def runtimeClass: Class[_] = ???
+
+  runtimeClass.toExpr(ClassIsLiftable) // OK for skolemization-as-a-whole and skolemization-of-each-param
+
+  runtimeClass.toExpr // only works with skolemization-of-each-param, also works in scalac.
+}
\ No newline at end of file
diff --git a/tests/pos/i2104b.decompiled b/tests/pos/i2104b.decompiled
index 74e8214b0f52..2e052fbf1e90 100644
--- a/tests/pos/i2104b.decompiled
+++ b/tests/pos/i2104b.decompiled
@@ -10,7 +10,7 @@ case class Pair[A, B](_1: A, _2: B) {
     acc = scala.runtime.Statics.mix(acc, scala.runtime.Statics.anyHash(Pair.this._2))
     scala.runtime.Statics.finalizeHash(acc, 2)
   }
-  override def equals(x$0: scala.Any): scala.Boolean = Pair.this.eq(x$0.asInstanceOf[java.lang.Object]).||(x$0 match {
+  override def equals(x$0: scala.Any): scala.Boolean = Pair.this.eq(x$0.$asInstanceOf$[java.lang.Object]).||(x$0 match {
     case x$0: Pair[A, B] @scala.unchecked =>
       Pair.this._1.==(x$0._1).&&(Pair.this._2.==(x$0._2))
     case _ =>
diff --git a/tests/pos/i3598.scala b/tests/pos/i3598.scala
index 9e5c8c32e954..99a641e3ad76 100644
--- a/tests/pos/i3598.scala
+++ b/tests/pos/i3598.scala
@@ -1,4 +1,5 @@
 class Foo[A] {
   def baz(foo: Foo[_]): Unit = bar(foo)
+  def bam(foo: => Foo[_]) = bar(foo)
   def bar[A](foo: Foo[A]): A = ???
 }
diff --git a/tests/pos/pos_valueclasses/t7818.scala b/tests/pos/pos_valueclasses/t7818.scala
index 31f542366024..8f01ff15056b 100644
--- a/tests/pos/pos_valueclasses/t7818.scala
+++ b/tests/pos/pos_valueclasses/t7818.scala
@@ -7,6 +7,11 @@ class Observable1[+T](val asJava: JObservable[_ <: T]) extends AnyVal {
   // to the typer parameter of the extension method into which the RHS is
   // transplanted.
   def synchronize: Observable1[T] = new Observable1(foo(asJava))
+
+  // Was generating a Ycheck error after ExtensionMethods.
+  // Fixed by having TypeMap go over info of SkolemTypes
+  private[this] def id(x: JObservable[_ <: T]) = x
+  def synchronize2: Observable1[T] = new Observable1(foo(id(asJava)))
 }
 
 class JObservable[T]
diff --git a/tests/pos/simpleCaseClass-1.decompiled b/tests/pos/simpleCaseClass-1.decompiled
index 02af82592f03..115d3d35d3ec 100644
--- a/tests/pos/simpleCaseClass-1.decompiled
+++ b/tests/pos/simpleCaseClass-1.decompiled
@@ -1,6 +1,6 @@
 case class A() {
   override def hashCode(): scala.Int = 1914112431
-  override def equals(x$0: scala.Any): scala.Boolean = A.this.eq(x$0.asInstanceOf[java.lang.Object]).||(x$0 match {
+  override def equals(x$0: scala.Any): scala.Boolean = A.this.eq(x$0.$asInstanceOf$[java.lang.Object]).||(x$0 match {
     case x$0: A @scala.unchecked =>
       true
     case _ =>
diff --git a/tests/pos/simpleCaseClass-2.decompiled b/tests/pos/simpleCaseClass-2.decompiled
index 08b83cb95297..cfbe7fbcc6b9 100644
--- a/tests/pos/simpleCaseClass-2.decompiled
+++ b/tests/pos/simpleCaseClass-2.decompiled
@@ -4,7 +4,7 @@ case class A(x: scala.Int) {
     acc = scala.runtime.Statics.mix(acc, A.this.x)
     scala.runtime.Statics.finalizeHash(acc, 1)
   }
-  override def equals(x$0: scala.Any): scala.Boolean = A.this.eq(x$0.asInstanceOf[java.lang.Object]).||(x$0 match {
+  override def equals(x$0: scala.Any): scala.Boolean = A.this.eq(x$0.$asInstanceOf$[java.lang.Object]).||(x$0 match {
     case x$0: A @scala.unchecked =>
       A.this.x.==(x$0.x)
     case _ =>
diff --git a/tests/pos/simpleCaseClass-3.decompiled b/tests/pos/simpleCaseClass-3.decompiled
index a1745d0b9f84..43171c07de47 100644
--- a/tests/pos/simpleCaseClass-3.decompiled
+++ b/tests/pos/simpleCaseClass-3.decompiled
@@ -4,7 +4,7 @@ case class A[T](x: T) {
     acc = scala.runtime.Statics.mix(acc, scala.runtime.Statics.anyHash(A.this.x))
     scala.runtime.Statics.finalizeHash(acc, 1)
   }
-  override def equals(x$0: scala.Any): scala.Boolean = A.this.eq(x$0.asInstanceOf[java.lang.Object]).||(x$0 match {
+  override def equals(x$0: scala.Any): scala.Boolean = A.this.eq(x$0.$asInstanceOf$[java.lang.Object]).||(x$0 match {
     case x$0: A[T] @scala.unchecked =>
       A.this.x.==(x$0.x)
     case _ =>
diff --git a/tests/run/literals.decompiled b/tests/run/literals.decompiled
index 6cacc583dddb..9a2ce3f78b4b 100644
--- a/tests/run/literals.decompiled
+++ b/tests/run/literals.decompiled
@@ -6,7 +6,7 @@ object Test {
       acc = scala.runtime.Statics.mix(acc, GGG.this.i)
       scala.runtime.Statics.finalizeHash(acc, 1)
     }
-    override def equals(x$0: scala.Any): scala.Boolean = GGG.this.eq(x$0.asInstanceOf[java.lang.Object]).||(x$0 match {
+    override def equals(x$0: scala.Any): scala.Boolean = GGG.this.eq(x$0.$asInstanceOf$[java.lang.Object]).||(x$0 match {
       case x$0: Test.GGG @scala.unchecked =>
         GGG.this.i.==(x$0.i)
       case _ =>
diff --git a/tests/run/t5729.scala b/tests/run/t5729.scala
new file mode 100644
index 000000000000..3fe3a1dc7f8b
--- /dev/null
+++ b/tests/run/t5729.scala
@@ -0,0 +1,16 @@
+trait T[X]
+object Test extends App {
+  def join(in: Seq[T[_]]): Int = 1
+  def join[S](in: Seq[T[S]]): String = "x"
+  val x = join(null: Seq[T[_]])
+  assert(x == 1)  // first alt chosen, since second requires a capture conversion in adapt
+  C
+}
+
+object C {
+  def join(in: Seq[List[_]]): Int = 1
+  def join[S](in: Seq[List[S]]): String = "x"
+
+  val x= join(Seq[List[Int]]()) // second alt chosen, since it is more specific
+  assert(x == "x")
+}
diff --git a/tests/run/tasty-extractors-2.check b/tests/run/tasty-extractors-2.check
index 2f98f387de8a..d6b33232dacf 100644
--- a/tests/run/tasty-extractors-2.check
+++ b/tests/run/tasty-extractors-2.check
@@ -49,7 +49,7 @@ Type.SymRef(IsClassSymbol(<scala.Unit>), Type.ThisType(Type.SymRef(IsPackageSymb
 Term.Inlined(None, Nil, Term.Block(List(ClassDef("Foo", DefDef("<init>", Nil, List(Nil), TypeTree.Inferred(), None), List(Term.Apply(Term.Select(Term.New(TypeTree.Inferred()), "<init>"), Nil)), Nil, None, List(DefDef("a", Nil, Nil, TypeTree.Inferred(), Some(Term.Literal(Constant.Int(0))))))), Term.Literal(Constant.Unit())))
 Type.SymRef(IsClassSymbol(<scala.Unit>), Type.ThisType(Type.SymRef(IsPackageSymbol(<scala>), NoPrefix())))
 
-Term.Inlined(None, Nil, Term.Block(List(ClassDef("Foo", DefDef("<init>", Nil, List(Nil), TypeTree.Inferred(), None), List(Term.Apply(Term.Select(Term.New(TypeTree.Inferred()), "<init>"), Nil), TypeTree.Select(Term.Select(Term.Ident("_root_"), "scala"), "Product"), TypeTree.Select(Term.Select(Term.Ident("_root_"), "scala"), "Serializable")), Nil, None, List(DefDef("hashCode", Nil, List(Nil), TypeTree.Inferred(), Some(Term.Literal(Constant.Int(394005536)))), DefDef("equals", Nil, List(List(ValDef("x$0", TypeTree.Inferred(), None))), TypeTree.Inferred(), Some(Term.Apply(Term.Select(Term.Apply(Term.Select(Term.This(Some(Id("Foo"))), "eq"), List(Term.TypeApply(Term.Select(Term.Ident("x$0"), "asInstanceOf"), List(TypeTree.Inferred())))), "||"), List(Term.Match(Term.Ident("x$0"), List(CaseDef(Pattern.Bind("x$0", Pattern.TypeTest(TypeTree.Inferred())), None, Term.Literal(Constant.Boolean(true))), CaseDef(Pattern.Value(Term.Ident("_")), None, Term.Literal(Constant.Boolean(false))))))))), DefDef("toString", Nil, List(Nil), TypeTree.Inferred(), Some(Term.Apply(Term.Ident("_toString"), List(Term.This(Some(Id("Foo"))))))), DefDef("canEqual", Nil, List(List(ValDef("that", TypeTree.Inferred(), None))), TypeTree.Inferred(), Some(Term.TypeApply(Term.Select(Term.Ident("that"), "isInstanceOf"), List(TypeTree.Inferred())))), DefDef("productArity", Nil, Nil, TypeTree.Inferred(), Some(Term.Literal(Constant.Int(0)))), DefDef("productPrefix", Nil, Nil, TypeTree.Inferred(), Some(Term.Literal(Constant.String("Foo")))), DefDef("productElement", Nil, List(List(ValDef("n", TypeTree.Inferred(), None))), TypeTree.Inferred(), Some(Term.Match(Term.Ident("n"), List(CaseDef(Pattern.Value(Term.Ident("_")), None, Term.Apply(Term.Ident("throw"), List(Term.Apply(Term.Select(Term.New(TypeTree.Inferred()), "<init>"), List(Term.Apply(Term.Select(Term.Ident("n"), "toString"), Nil)))))))))), DefDef("productElementName", Nil, List(List(ValDef("x$1", TypeTree.Select(Term.Select(Term.Ident("_root_"), "scala"), "Int"), None))), TypeTree.Select(Term.Select(Term.Ident("java"), "lang"), "String"), Some(Term.Match(Term.Ident("x$1"), List(CaseDef(Pattern.Value(Term.Ident("_")), None, Term.Apply(Term.Ident("throw"), List(Term.Apply(Term.Select(Term.New(TypeTree.Select(Term.Select(Term.Ident("java"), "lang"), "IndexOutOfBoundsException")), "<init>"), List(Term.Apply(Term.Select(Term.Select(Term.Select(Term.Ident("java"), "lang"), "String"), "valueOf"), List(Term.Ident("x$1")))))))))))), DefDef("copy", Nil, List(Nil), TypeTree.Inferred(), Some(Term.Apply(Term.Select(Term.New(TypeTree.Inferred()), "<init>"), Nil))))), ValDef("Foo", TypeTree.Ident("Foo$"), Some(Term.Apply(Term.Select(Term.New(TypeTree.Ident("Foo$")), "<init>"), Nil))), ClassDef("Foo$", DefDef("<init>", Nil, List(Nil), TypeTree.Inferred(), None), List(Term.Apply(Term.Select(Term.New(TypeTree.Inferred()), "<init>"), Nil), TypeTree.Applied(TypeTree.Inferred(), List(TypeTree.Inferred())), TypeTree.Select(Term.Select(Term.Ident("_root_"), "scala"), "Serializable")), Nil, Some(ValDef("_", TypeTree.Singleton(Term.Ident("Foo")), None)), List(DefDef("apply", Nil, List(Nil), TypeTree.Inferred(), Some(Term.Apply(Term.Select(Term.New(TypeTree.Inferred()), "<init>"), Nil))), DefDef("unapply", Nil, List(List(ValDef("x$1", TypeTree.Inferred(), None))), TypeTree.Inferred(), Some(Term.Literal(Constant.Boolean(true))))))), Term.Literal(Constant.Unit())))
+Term.Inlined(None, Nil, Term.Block(List(ClassDef("Foo", DefDef("<init>", Nil, List(Nil), TypeTree.Inferred(), None), List(Term.Apply(Term.Select(Term.New(TypeTree.Inferred()), "<init>"), Nil), TypeTree.Select(Term.Select(Term.Ident("_root_"), "scala"), "Product"), TypeTree.Select(Term.Select(Term.Ident("_root_"), "scala"), "Serializable")), Nil, None, List(DefDef("hashCode", Nil, List(Nil), TypeTree.Inferred(), Some(Term.Literal(Constant.Int(394005536)))), DefDef("equals", Nil, List(List(ValDef("x$0", TypeTree.Inferred(), None))), TypeTree.Inferred(), Some(Term.Apply(Term.Select(Term.Apply(Term.Select(Term.This(Some(Id("Foo"))), "eq"), List(Term.TypeApply(Term.Select(Term.Ident("x$0"), "$asInstanceOf$"), List(TypeTree.Inferred())))), "||"), List(Term.Match(Term.Ident("x$0"), List(CaseDef(Pattern.Bind("x$0", Pattern.TypeTest(TypeTree.Inferred())), None, Term.Literal(Constant.Boolean(true))), CaseDef(Pattern.Value(Term.Ident("_")), None, Term.Literal(Constant.Boolean(false))))))))), DefDef("toString", Nil, List(Nil), TypeTree.Inferred(), Some(Term.Apply(Term.Ident("_toString"), List(Term.This(Some(Id("Foo"))))))), DefDef("canEqual", Nil, List(List(ValDef("that", TypeTree.Inferred(), None))), TypeTree.Inferred(), Some(Term.TypeApply(Term.Select(Term.Ident("that"), "isInstanceOf"), List(TypeTree.Inferred())))), DefDef("productArity", Nil, Nil, TypeTree.Inferred(), Some(Term.Literal(Constant.Int(0)))), DefDef("productPrefix", Nil, Nil, TypeTree.Inferred(), Some(Term.Literal(Constant.String("Foo")))), DefDef("productElement", Nil, List(List(ValDef("n", TypeTree.Inferred(), None))), TypeTree.Inferred(), Some(Term.Match(Term.Ident("n"), List(CaseDef(Pattern.Value(Term.Ident("_")), None, Term.Apply(Term.Ident("throw"), List(Term.Apply(Term.Select(Term.New(TypeTree.Inferred()), "<init>"), List(Term.Apply(Term.Select(Term.Ident("n"), "toString"), Nil)))))))))), DefDef("productElementName", Nil, List(List(ValDef("x$1", TypeTree.Select(Term.Select(Term.Ident("_root_"), "scala"), "Int"), None))), TypeTree.Select(Term.Select(Term.Ident("java"), "lang"), "String"), Some(Term.Match(Term.Ident("x$1"), List(CaseDef(Pattern.Value(Term.Ident("_")), None, Term.Apply(Term.Ident("throw"), List(Term.Apply(Term.Select(Term.New(TypeTree.Select(Term.Select(Term.Ident("java"), "lang"), "IndexOutOfBoundsException")), "<init>"), List(Term.Apply(Term.Select(Term.Select(Term.Select(Term.Ident("java"), "lang"), "String"), "valueOf"), List(Term.Ident("x$1")))))))))))), DefDef("copy", Nil, List(Nil), TypeTree.Inferred(), Some(Term.Apply(Term.Select(Term.New(TypeTree.Inferred()), "<init>"), Nil))))), ValDef("Foo", TypeTree.Ident("Foo$"), Some(Term.Apply(Term.Select(Term.New(TypeTree.Ident("Foo$")), "<init>"), Nil))), ClassDef("Foo$", DefDef("<init>", Nil, List(Nil), TypeTree.Inferred(), None), List(Term.Apply(Term.Select(Term.New(TypeTree.Inferred()), "<init>"), Nil), TypeTree.Applied(TypeTree.Inferred(), List(TypeTree.Inferred())), TypeTree.Select(Term.Select(Term.Ident("_root_"), "scala"), "Serializable")), Nil, Some(ValDef("_", TypeTree.Singleton(Term.Ident("Foo")), None)), List(DefDef("apply", Nil, List(Nil), TypeTree.Inferred(), Some(Term.Apply(Term.Select(Term.New(TypeTree.Inferred()), "<init>"), Nil))), DefDef("unapply", Nil, List(List(ValDef("x$1", TypeTree.Inferred(), None))), TypeTree.Inferred(), Some(Term.Literal(Constant.Boolean(true))))))), Term.Literal(Constant.Unit())))
 Type.SymRef(IsClassSymbol(<scala.Unit>), Type.ThisType(Type.SymRef(IsPackageSymbol(<scala>), NoPrefix())))
 
 Term.Inlined(None, Nil, Term.Block(List(ClassDef("Foo1", DefDef("<init>", Nil, List(List(ValDef("a", TypeTree.Ident("Int"), None))), TypeTree.Inferred(), None), List(Term.Apply(Term.Select(Term.New(TypeTree.Inferred()), "<init>"), Nil)), Nil, None, List(ValDef("a", TypeTree.Inferred(), None)))), Term.Literal(Constant.Unit())))