diff --git a/compiler/src/dotty/tools/dotc/ast/Desugar.scala b/compiler/src/dotty/tools/dotc/ast/Desugar.scala
index c2517145c935..8d4ff4565134 100644
--- a/compiler/src/dotty/tools/dotc/ast/Desugar.scala
+++ b/compiler/src/dotty/tools/dotc/ast/Desugar.scala
@@ -681,7 +681,12 @@ object desugar {
               if (restrictedAccess) mods.withPrivateWithin(constr1.mods.privateWithin)
               else mods
             }
-            val appParamss =
+            // FIXME: This now infers `List[List[DefTree]]`, the issue
+            // is that `withMods` is defined in `DefTree` so that becomes the
+            // upper bound of the type variable (see logic in `constrainSelectionQualifier`),
+            // but the result type of `withMods` is a type member which is
+            // refined in `ValDef`.
+            val appParamss: List[List[ValDef]] =
               derivedVparamss.nestedZipWithConserve(constrVparamss)((ap, cp) =>
                 ap.withMods(ap.mods | (cp.mods.flags & HasDefault)))
             val app = DefDef(nme.apply, derivedTparams, appParamss, applyResultTpt, widenedCreatorExpr)
diff --git a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
index d0a52808df6a..b3bbd4f7018b 100644
--- a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
+++ b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
@@ -87,9 +87,22 @@ trait ConstraintHandling[AbstractContext] {
 
   protected def addOneBound(param: TypeParamRef, bound: Type, isUpper: Boolean)(using AbstractContext): Boolean =
     if !constraint.contains(param) then true
-    else if !isUpper && param.occursIn(bound)
-      // We don't allow recursive lower bounds when defining a type,
-      // so we shouldn't allow them as constraints either.
+    else if
+      bound.existsPart {
+        case `param` =>
+          // We don't allow recursive lower bounds when defining a type,
+          // so we shouldn't allow them as constraints either.
+          !isUpper
+        case AppliedType(tycon: TypeRef, args) if tycon.info.isInstanceOf[MatchAlias] =>
+          // FIXME: this is incomplete, see tests/pos/type-match-fbounds.scala
+          args.exists {
+            case `param` => true
+            case tp: TypeVar => tp.origin eq param
+            case _ => false
+          }
+        case _ => false
+      }
+    then
       false
     else
       val oldBounds @ TypeBounds(lo, hi) = constraint.nonParamBounds(param)
@@ -432,8 +445,9 @@ trait ConstraintHandling[AbstractContext] {
             if lower.nonEmpty && !bounds.lo.isRef(defn.NothingClass)
                || upper.nonEmpty && !bounds.hi.isAny
             then constr.println(i"INIT*** $tl")
-            lower.forall(addOneBound(_, bounds.hi, isUpper = true)) &&
-              upper.forall(addOneBound(_, bounds.lo, isUpper = false))
+
+               lower.forall(loParam => addOneBound(loParam, bounds.hi, isUpper =  true) && addOneBound(param, constraint.nonParamBounds(loParam).lo, isUpper = false))
+            && upper.forall(upParam => addOneBound(upParam, bounds.lo, isUpper = false) && addOneBound(param, constraint.nonParamBounds(upParam).hi, isUpper =  true))
           case _ =>
             // Happens if param was already solved while processing earlier params of the same TypeLambda.
             // See #4720.
diff --git a/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala b/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala
index 7ebdb04da641..01eda29eefec 100644
--- a/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala
+++ b/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala
@@ -232,7 +232,7 @@ class OrderingConstraint(private val boundsMap: ParamBounds,
    *  @param isUpper   If true, `bound` is an upper bound, else a lower bound.
    */
   private def stripParams(tp: Type, paramBuf: mutable.ListBuffer[TypeParamRef],
-      isUpper: Boolean)(implicit ctx: Context): Type = tp match {
+      isUpper: Boolean)(implicit ctx: Context): Type = tp.stripTypeVar match {
     case param: TypeParamRef if contains(param) =>
       if (!paramBuf.contains(param)) paramBuf += param
       NoType
@@ -310,6 +310,9 @@ class OrderingConstraint(private val boundsMap: ParamBounds,
   private def ensureNonCyclic(param: TypeParamRef, inst: Type)(using Context): Type =
 
     def recur(tp: Type, fromBelow: Boolean): Type = tp match
+      case tp: NamedType =>
+        val underlying1 = recur(tp.underlying, fromBelow)
+        if underlying1 ne tp.underlying then underlying1 else tp
       case tp: AndOrType =>
         val r1 = recur(tp.tp1, fromBelow)
         val r2 = recur(tp.tp2, fromBelow)
@@ -365,7 +368,7 @@ class OrderingConstraint(private val boundsMap: ParamBounds,
    *    Q <: tp  implies  Q <: P      and isUpper = true, or
    *    tp <: Q  implies  P <: Q      and isUpper = false
    */
-  private def dependentParams(tp: Type, isUpper: Boolean): List[TypeParamRef] = tp match
+  private def dependentParams(tp: Type, isUpper: Boolean)(using Context): List[TypeParamRef] = tp.stripTypeVar match
     case param: TypeParamRef if contains(param) =>
       param :: (if (isUpper) upper(param) else lower(param))
     case tp: AndType if isUpper  =>
@@ -479,6 +482,12 @@ class OrderingConstraint(private val boundsMap: ParamBounds,
         case (e1: TypeBounds, _) if e1 contains e2 => e2
         case (_, e2: TypeBounds) if e2 contains e1 => e1
         case (tv1: TypeVar, tv2: TypeVar) if tv1 eq tv2 => e1
+
+        // Should this be based on the merged entries instead of
+        // using this.entry/other.entry ?
+        case (e1: TypeParamRef, e2) if  this.entry(e1).bounds.contains(e2) => e2
+        case (e1, e2: TypeParamRef) if other.entry(e2).bounds.contains(e1) => e1
+
         case _ =>
           if (otherHasErrors)
             e1
@@ -607,6 +616,8 @@ class OrderingConstraint(private val boundsMap: ParamBounds,
   def occursAtToplevel(param: TypeParamRef, inst: Type)(implicit ctx: Context): Boolean =
 
     def occurs(tp: Type)(using Context): Boolean = tp match
+      case tp: NamedType =>
+        occurs(tp.underlying)
       case tp: AndOrType =>
         occurs(tp.tp1) || occurs(tp.tp2)
       case tp: TypeParamRef =>
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 7ae72bf4317f..a689e2353737 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -1983,8 +1983,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
   /** Merge `t1` into `tp2` if t1 is a subtype of some &-summand of tp2.
    */
   private def mergeIfSub(tp1: Type, tp2: Type): Type =
-    if (isSubTypeWhenFrozen(tp1, tp2))
-      if (isSubTypeWhenFrozen(tp2, tp1)) tp2 else tp1 // keep existing type if possible
+    if (isSubTypeWhenFrozen(tp1, tp2)) tp1
     else tp2 match {
       case tp2 @ AndType(tp21, tp22) =>
         val lower1 = mergeIfSub(tp1, tp21)
@@ -2004,8 +2003,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
    *  @param canConstrain  If true, new constraints might be added to make the merge possible.
    */
   private def mergeIfSuper(tp1: Type, tp2: Type, canConstrain: Boolean): Type =
-    if (isSubType(tp2, tp1, whenFrozen = !canConstrain))
-      if (isSubType(tp1, tp2, whenFrozen = !canConstrain)) tp2 else tp1 // keep existing type if possible
+    if (isSubType(tp2, tp1, whenFrozen = !canConstrain)) tp1
     else tp2 match {
       case tp2 @ OrType(tp21, tp22) =>
         val higher1 = mergeIfSuper(tp1, tp21, canConstrain)
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index 8d28aa97a05f..10e23b00ba9e 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -3927,7 +3927,7 @@ object Types {
         NoType
     }
 
-    def tyconTypeParams(implicit ctx: Context): List[ParamInfo] = {
+    def tyconTypeParams(implicit ctx: Context): List[TypeApplications.TypeParamInfo] = {
       val tparams = tycon.typeParams
       if (tparams.isEmpty) HKTypeLambda.any(args.length).typeParams else tparams
     }
diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
index 100891a50df0..b7a3d1f5dcba 100644
--- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
@@ -60,6 +60,10 @@ class PlainPrinter(_ctx: Context) extends Printer {
         case tp @ AppliedType(tycon, args) =>
           if (defn.isCompiletimeAppliedType(tycon.typeSymbol)) tp.tryCompiletimeConstantFold
           else tycon.dealias.appliedTo(args)
+        // Workaround for https://github.com/lampepfl/dotty/issues/8988
+        case tp @ AnnotatedType(underlying @ AnnotatedType(_, annot2), annot1)
+            if (annot1.symbol eq defn.UncheckedVarianceAnnot) && (annot1.symbol eq annot2.symbol) =>
+          homogenize(underlying)
         case _ =>
           tp
       }
diff --git a/compiler/src/dotty/tools/dotc/typer/Inferencing.scala b/compiler/src/dotty/tools/dotc/typer/Inferencing.scala
index c6b241458ee1..dddca0823951 100644
--- a/compiler/src/dotty/tools/dotc/typer/Inferencing.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Inferencing.scala
@@ -381,7 +381,7 @@ object Inferencing {
    *
    *  we want to instantiate U to x.type right away. No need to wait further.
    */
-  private def variances(tp: Type)(using Context): VarianceMap = {
+  def variances(tp: Type)(using Context): VarianceMap = {
     Stats.record("variances")
     val constraint = ctx.typerState.constraint
 
diff --git a/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala b/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala
index eeb65cc5727a..46abe7f12da9 100644
--- a/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala
+++ b/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala
@@ -135,7 +135,12 @@ object ProtoTypes {
      *  or as an upper bound of a prefix or underlying type.
      */
     private def hasUnknownMembers(tp: Type)(using Context): Boolean = tp match {
-      case tp: TypeVar => !tp.isInstantiated
+      case tp: TypeVar =>
+        // FIXME: This used to be `!tp.isInstantiated` but that prevents
+        // extension methods from being selected with the changes in this PR.
+        // This change doesn't break any testcase, can we construct a testcase
+        // where this matters?
+        false
       case tp: WildcardType => true
       case NoType => true
       case tp: TypeRef =>
@@ -152,13 +157,15 @@ object ProtoTypes {
       case _ => false
     }
 
-    override def isMatchedBy(tp1: Type, keepConstraint: Boolean)(using Context): Boolean =
-      name == nme.WILDCARD || hasUnknownMembers(tp1) ||
-      {
-        val mbr = if (privateOK) tp1.member(name) else tp1.nonPrivateMember(name)
+    override def isMatchedBy(tp1: Type, keepConstraint: Boolean)(using Context): Boolean = {
+      if name == nme.WILDCARD || hasUnknownMembers(tp1) then
+        return true
+
+      def go(pre: Type): Boolean = {
+        val mbr = if (privateOK) pre.member(name) else pre.nonPrivateMember(name)
         def qualifies(m: SingleDenotation) =
           memberProto.isRef(defn.UnitClass) ||
-          tp1.isValueType && compat.normalizedCompatible(NamedType(tp1, name, m), memberProto, keepConstraint)
+          pre.isValueType && compat.normalizedCompatible(NamedType(pre, name, m), memberProto, keepConstraint)
             // Note: can't use `m.info` here because if `m` is a method, `m.info`
             //       loses knowledge about `m`'s default arguments.
         mbr match { // hasAltWith inlined for performance
@@ -166,6 +173,14 @@ object ProtoTypes {
           case _ => mbr hasAltWith qualifies
         }
       }
+      tp1.widenDealias.stripTypeVar match {
+        case tp: TypeParamRef =>
+          val bounds = ctx.typeComparer.bounds(tp)
+          go(bounds.hi) || go(bounds.lo)
+        case _ =>
+          go(tp1)
+      }
+    }
 
     def underlying(using Context): Type = WildcardType
 
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index 8ed14c2fd32b..0ca5ae6a7d87 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -516,6 +516,203 @@ class Typer extends Namer
     tree
   }
 
+  /** Try to add constraints to type a selection where the qualifier is a type variable.
+   *
+   *  Currently, this should only happen with lambdas, for example when typechecking:
+   *
+   *    def foo[T <: List[Any]](x: T => T)
+   *    foo(x => x.head: Int)
+   *
+   *  In the past, `typedFunctionValue` would have instantiated the type
+   *  variable corresponding to the type parameter `T` to `List[Any]` before
+   *  typing the lambda, which would then fail because `x.head` has type `Any`.
+   *  But we now leave such type variables uninstantiated, which means we need
+   *  to figure out how to type a selection where the prefix is an
+   *  uninstantiated type variable, and in particular how to propagate
+   *  constraints from typing this selection back to that type variable.
+   *
+   *  @param qual           The type of the qualifier of the selection
+   *  @param name           The name of the member being selected
+   *  @param underlyingVar  The uninstantiated type variable underlying the type of the qualifier
+   *  @param pt             The expected type of the selection
+   */
+  private def constrainSelectionQualifier(
+    qual: Type, name: Name, underlyingVar: TypeVar, pt: Type)(using Context): Boolean = {
+
+    /** Return `tycon[?A, ?B, ...]` where `?A`, `?B`, ... are fresh type variables
+     *  conforming to the corresponding type parameter in `tparams`.
+     */
+    def appliedWithVars(tycon: Type, tparams: List[TypeApplications.TypeParamInfo]): Type = {
+      if (tparams.isEmpty)
+        tycon
+      else {
+        val tl = tycon.EtaExpand(tparams).asInstanceOf[HKTypeLambda]
+        val tvars = constrained(tl, untpd.EmptyTree, alwaysAddTypeVars = true)._2.map(_.tpe)
+        tycon.appliedTo(tvars)
+      }
+    }
+
+    /** Replace all applied types `tycon[T, S, ...]` by `tycon[?A, ?B, ...]`
+     *  where `?A`, `?B`, ... are fresh type variables.
+     */
+    def replaceArgsByVars = new TypeMap {
+      def apply(t: Type): Type = t match {
+        case tp: TypeLambda =>
+          tp
+        case tp @ AppliedType(tycon, args) =>
+          // Note that we don't constrain the fresh type variables
+          // such that the mapped type is a subtype of `tp`, we let
+          // the caller deal with that.
+          appliedWithVars(tycon, tp.tyconTypeParams)
+        case _ =>
+          mapOver(t)
+      }
+    }
+
+    /** Does `@uncheckedVariance` appears somewhere in the type of `d` ? */
+    def hasUncheckedVariance(d: SingleDenotation) = d.info.widen.existsPart {
+      case tp @ AnnotatedType(_, annot) =>
+        annot.symbol eq defn.UncheckedVarianceAnnot
+      case tp =>
+        false
+    }
+
+    /** The members of one of the bound of `underlyingVar` which the selection
+     *  could resolve to.
+     *
+     * @param isUpper  If true, look for candidates in the upper bound,
+     *                 otherwise look in the lower bound.
+     */
+    def candidatesInBound(isUpper: Boolean): List[SingleDenotation] = {
+      val bounds = ctx.typeComparer.bounds(underlyingVar.origin)
+      val bound = if (isUpper) bounds.hi else bounds.lo
+      val d = bound.member(name)
+      d.alternatives
+    }
+
+    /** Try to add additional constraints on `underlyingVar`
+     *  to allow a selection of `candidate` to typecheck.
+     *
+     *  @param  isUpper  Does `candidate` come from the upper bound
+     *                   of the qualifier type?
+     */
+    def constrainTo(candidate: SingleDenotation, isUpper: Boolean): Boolean = {
+      if (hasUncheckedVariance(candidate)) {
+        // If `@uncheckedVariance` appears in the type of the candidate, give up
+        // on delaying instantiation and just instantiate the type variable at
+        // that point. If we don't do that, the type variable might later
+        // be constrained in a way that prevents the selection from typechecking,
+        // because narrowing does not hold with unchecked variance.
+        // See tests/pos/fold-infer-uncheckedVariance.scala for an example
+        // which did not pass `-Ytest-pickler` before.
+        // FIXME: `-Ycheck:all` did not pick up on this issue in
+        // fold-infer-uncheckedVariance.scala because the ReTyper never retypes
+        // selections, I think it's important to get TreeChecker to actually
+        // verify this stuff, especially with everything going on in this PR.
+        underlyingVar.instantiate(fromBelow = !isUpper)
+        return true
+      }
+
+      val owner = candidate.symbol.maybeOwner
+      // TODO: Deal with methods in structural types?
+      if (!owner.exists || !owner.isClass)
+        return false
+
+      if (isUpper) {
+        // The candidate comes from the upper bound of the qualifier.
+        // In that case we replace type arguments in the upper bound
+        // by fresh type variables to make it more flexible.
+        //
+        // For example, we might have `qual: ?T` where `?T <: List[AnyVal]`.
+        // in which case `qual.head` will have type `qual.A` where `A`
+        // is an abstract type >: Nothing <: AnyVal.
+        // Therefore, when typechecking `qual.head: Int`, we get:
+        //
+        //   qual.A <:< Int
+        //   AnyVal <:< Int
+        //         false
+        //
+        // The problem is that subtype checks on `qual.A` do
+        // not allow us to constraint `?T` further.
+        //
+        // To fix this, we need a more precise upper-bound for `?T`:
+        // we can safely rewrite the constraint:
+        //
+        //   ?T <: List[AnyVal]
+        //
+        // as:
+        //
+        //   ?T <: List[?X]
+        //   ?X <: AnyVal
+        //
+        // Now, if we try to typecheck `qual.head: Int`, we get:
+        //
+        //   qual.A <:< Int
+        //       ?X <:< Int
+        //         true, with extra constraint `?X <: Int`
+        //
+        // And at a later point, `?T` will be instantiated to a
+        // subtype of `List[Int]` as expected.
+
+        val base = qual.baseType(owner)
+        // FIXME: this is wasteful: if we have multiple selections with the
+        // same qualifier, we'll create fresh type variables every time.
+        val newUpperBound = replaceArgsByVars(base)
+
+        if newUpperBound ne base then
+          underlyingVar <:< newUpperBound
+      } else {
+        // The candidate comes from the lower bound of the qualifier.
+        // In that case, we need to constrain the upper bound of the
+        // qualifier to be able to typecheck the selection at all,
+        // and like in the isUpper case, we want type variables in
+        // the arguments of that upper bound for flexibility.
+        //
+        // For example, if we have `qual: ?T` where `?T >: Nil`, then
+        // `qual.::` will fail as there is no member named `::`
+        // defined on `Any`, so we need to further constrain the upper
+        // bound. We know that `::` is defined on `List`, so we can add
+        // a constraint:
+        //
+        //   ?T <: List[?X]
+        //   ?X
+        //
+        // (in this example, the fresh type variable `?X` can stay
+        // unconstrained since `Nil <:< List[?X]` is true for all `?X`)
+
+        // FIXME: better handling of overrides: `candidate` might be an
+        // override of some member defined in a parent class, in which
+        // case we're overconstraining the upper bound.
+        val newUpperBound = appliedWithVars(owner.typeRef, owner.typeParams)
+        underlyingVar <:< newUpperBound
+      }
+
+      // FIXME: it would be nice if we could use the expected type
+      // to filter out some candidates, but it's hard to rule out
+      // anything since some implicit conversion might kick in
+      // during adaptation.
+      true
+    }
+
+    /** Try to add additional constraints on `underlyingVar`
+     *  to allow a selection based on the candidates found
+     *  in one of its own bound.
+     *
+     *  @param isUpper  If true, look for candidates in the upper bound,
+     *                  otherwise look in the lower bound.
+     */
+    def constrainInBound(isUpper: Boolean): Boolean = {
+      // FIXME: we just stop after finding a matching candidate, should we
+      // take the union of the constraints they add instead?
+      candidatesInBound(isUpper).exists(constrainTo(_, isUpper))
+    }
+
+    // FIXME: We currently only look at the lower bound if we don't find a
+    // matching member in the upper bound, but that could exclude
+    // the right candidate.
+    constrainInBound(isUpper = true) || constrainInBound(isUpper = false)
+  }
+
   def typedSelect(tree: untpd.Select, pt: Type, qual: Tree)(using Context): Tree = qual match {
     case qual @ IntegratedTypeArgs(app) =>
       pt.revealIgnored match {
@@ -523,6 +720,16 @@ class Typer extends Namer
         case _ => app
       }
     case qual =>
+      qual.tpe.widenDealias.stripTypeVar match {
+        case tp: TypeParamRef =>
+          ctx.typerState.constraint.typeVarOfParam(tp) match {
+            case tvar: TypeVar =>
+              constrainSelectionQualifier(qual.tpe, tree.name, tvar, pt)
+            case _ =>
+          }
+        case _ =>
+      }
+
       val select = assignType(cpy.Select(tree)(qual, tree.name), qual)
       val select1 = toNotNullTermRef(select, pt)
 
@@ -1096,6 +1303,21 @@ class Typer extends Namer
       case _ =>
     }
 
+    // The set of type variables in the prototype which appear only in covariant or
+    // contravariant positions. These should be instantiatable without
+    // preventing the body of the lambda from typechecking (...except in situations
+    // like `def foo[T, U <: T](x: T => U)`, where instantiating `T` to a specific
+    // type might overconstrain `U`).
+    //
+    // This doesn't exclude type variables which appear with a different
+    // variance at a later point in the same method call, or a subsequent chained
+    // call.
+    //
+    // TODO: try to replace this by an empty list and see how that affects
+    // inference and performance (we would end up creating a lot more type
+    // variables in `typedSelect`).
+    lazy val protoVariantVars = variances(pt).toList.filter(_._2 != 0).map(_._1)
+
     val (protoFormals, resultTpt) = decomposeProtoFunction(pt, params.length)
 
     /** The inferred parameter type for a parameter in a lambda that does
@@ -1118,7 +1340,7 @@ class Typer extends Namer
      *  If all attempts fail, issue a "missing parameter type" error.
      */
     def inferredParamType(param: untpd.ValDef, formal: Type): Type =
-      if isFullyDefined(formal, ForceDegree.failBottom) then return formal
+      if isFullyDefined(formal, ForceDegree.none) then return formal
       val target = calleeType.widen match
         case mtpe: MethodType =>
           val pos = paramIndex(param.name)
@@ -1128,9 +1350,17 @@ class Typer extends Namer
           else NoType
         case _ => NoType
       if target.exists then formal <:< target
-      if isFullyDefined(formal, ForceDegree.flipBottom) then formal
+      // if isFullyDefined(formal, ForceDegree.flipBottom) then formal
+      if isFullyDefined(formal, ForceDegree.none) then formal
       else if target.exists && isFullyDefined(target, ForceDegree.flipBottom) then target
-      else errorType(AnonymousFunctionMissingParamType(param, params, tree, formal), param.sourcePos)
+      else if !formal.isInstanceOf[WildcardType] then
+        instantiateSelected(formal, protoVariantVars)
+        // Intentionally leave uninstantiated type variables in the types of parameters,
+        // this works because `typedSelect` special cases the handling of qualifiers
+        // whose type is a type variable.
+        formal
+      else
+        errorType(AnonymousFunctionMissingParamType(param, params, tree, formal), param.sourcePos)
 
     def protoFormal(i: Int): Type =
       if (protoFormals.length == params.length) protoFormals(i)
diff --git a/tests/neg/i4564.scala b/tests/neg/i4564.scala
index 327baf0d35d8..cbe57b1ad03f 100644
--- a/tests/neg/i4564.scala
+++ b/tests/neg/i4564.scala
@@ -42,5 +42,4 @@ class BaseCNSP[T] {
 }
 
 object ClashNoSigPoly extends BaseCNSP[Int]
-// TODO: improve error message
-case class ClashNoSigPoly private(x: Int)  // error: found: ClashNoSigPoly required: Nothing
\ No newline at end of file
+case class ClashNoSigPoly private(x: Int)
diff --git a/tests/pos/i5735.scala b/tests/neg/i5735.scala
similarity index 90%
rename from tests/pos/i5735.scala
rename to tests/neg/i5735.scala
index c03b2e3dfecf..db8df8722f22 100644
--- a/tests/pos/i5735.scala
+++ b/tests/neg/i5735.scala
@@ -8,5 +8,5 @@ object Test {
   class Foo[T] { def apply[Y >: T <: Nested[T, Tuple2, Unit]](t: T): T = t }
   def foo[T] = new Foo[T]
 
-  foo.apply((21, ()))
+  foo.apply((21, ())) // error
 }
diff --git a/tests/neg/type-match-fbounds.scala b/tests/neg/type-match-fbounds.scala
new file mode 100644
index 000000000000..48cdcaf3c17b
--- /dev/null
+++ b/tests/neg/type-match-fbounds.scala
@@ -0,0 +1,28 @@
+class A {
+  type Foo[T] = T match {
+    case Int => String
+    case T => T
+  }
+
+  // FIXME: These cases are not disallowed currently and cause
+  // infinite loops
+  /*
+  def a1[T <: (T match {
+    case Int => String
+    case T => T
+  })]: T = ???
+  a1
+
+  def a2[T, U >: T <: (T match {
+    case Int => String
+    case T => T
+  })]: T = ???
+  a2
+
+  def a3[T <: Foo[T]]: T = ???
+  a3
+  */
+
+  def a4[T, U >: T <: Foo[T]]: T = ???
+  a4 // error
+}
diff --git a/tests/pos/dependent-typevar.scala b/tests/pos/dependent-typevar.scala
new file mode 100644
index 000000000000..860a36265f81
--- /dev/null
+++ b/tests/pos/dependent-typevar.scala
@@ -0,0 +1,8 @@
+class Foo[A] {
+  // Previously, we did not record the constraint ordering `A <: B` here
+  def bar[B >: A <: String]: String = ""
+}
+object Test {
+  // ... which prevented the following from typechecking.
+  val ret = (new Foo).bar
+}
diff --git a/tests/pos/fold-infer-2.scala b/tests/pos/fold-infer-2.scala
new file mode 100644
index 000000000000..d8b0fb60fa11
--- /dev/null
+++ b/tests/pos/fold-infer-2.scala
@@ -0,0 +1,32 @@
+class Foo[A, B <: A] {
+  def get: A = ???
+  def hi: Foo[A, B] = this
+}
+class A {
+  def foo[T <: Foo[_, _]]: T = ???
+  foo.get // OK
+
+  def list[T <: List[_]]: T = ???
+  list.head: Int
+  list.::(1)
+
+  def foldLeft1[B <: List[_]](op: (B, Int) => B): B = ???
+  val l = foldLeft1((acc, i) => acc.::(i))
+
+  def foldLeft2[B >: Nil.type](op: (B, Int) => B): B = ???
+
+  val l2 = foldLeft2((acc, i) => acc.::(i))
+
+  extension fooOps on (x: List[Int]) {
+    def hi: Int = 0
+  }
+
+  def foo1[B >: Foo[Int, Int]](op: B => B) = ???
+  foo1(b => b.hi)
+
+  def foo2[B >: List[Int]](op: B => Int) = ???
+  foo2(b => b.hi)
+
+  def foo3(xs: Seq[Option[List[Int]]]) =
+    xs.map(_.getOrElse(Nil)).reduceLeft(_ ++ _)
+}
diff --git a/tests/pos/fold-infer-uncheckedVariance.scala b/tests/pos/fold-infer-uncheckedVariance.scala
new file mode 100644
index 000000000000..de57da3d68ac
--- /dev/null
+++ b/tests/pos/fold-infer-uncheckedVariance.scala
@@ -0,0 +1,19 @@
+import scala.annotation.unchecked.uncheckedVariance
+
+class Bar
+
+class Foo[-T >: Null] {
+  def tpe: T @uncheckedVariance = ???
+}
+
+object Test {
+  def foo(xs: List[Int], x: Foo[Bar]): Unit = {
+    val r = xs.foldLeft(x) { (acc, x) =>
+      // B >: Foo[Bar] <: Foo[T]
+      // T >: Null <: Bar
+      val m = acc.tpe
+      acc
+    }
+    val s: Foo[Bar] = r
+  }
+}
diff --git a/tests/pos/fold-infer.scala b/tests/pos/fold-infer.scala
new file mode 100644
index 000000000000..e22732aa9172
--- /dev/null
+++ b/tests/pos/fold-infer.scala
@@ -0,0 +1,29 @@
+object Test {
+  val li = List(1, 2, 3).foldLeft(Nil)((acc, x) => x :: acc)
+  val cli: List[Int] = li
+
+  val li2 = List(1, 2, 3).foldLeft(Nil)((acc, x) => acc)
+  val cli2: List[Int] = li2
+
+  val ld = List(1, 2, 3).foldLeft(Nil)((acc, x) => x.toDouble :: acc)
+  val cld: List[Double] = ld
+
+  val si = Seq(1, 2, 3).foldLeft(Set())((acc, x) => acc + x)
+  val csi: Set[Int] = si
+
+  val si2 = Seq(1, 2, 3).foldLeft(Set())((acc, x) => acc ++ Set(x))
+  val csi2: Set[Int] = si2
+
+  val ssi = Seq(1, 2, 3).foldLeft(Set())((acc, x) => acc + Set(x))
+  val cssi: Set[Set[Int]] = ssi
+}
+
+object NotWorking {
+  /*
+  val ld2 = List(1, 2, 3).foldLeft(Nil)((acc, x) => {
+    val y = x.toDouble :: acc
+    y // error: found: List[Double], required: List[Nothing]
+  })
+  val cld2: List[Double] = ld2
+  */
+}
diff --git a/tests/pos/merge-constraint.scala b/tests/pos/merge-constraint.scala
new file mode 100644
index 000000000000..7434be81e53f
--- /dev/null
+++ b/tests/pos/merge-constraint.scala
@@ -0,0 +1,11 @@
+class Hi
+class Lo extends Hi
+
+object Test {
+  def foo[T, U <: T](t: T, f: T => U): U = ???
+
+  def test(hi: Hi, lo: Lo): Unit = {
+    val ret = foo(hi, x => lo) // This used to infer U := Hi
+    val y: Lo = ret
+  }
+}