diff --git a/compiler/src/dotty/tools/dotc/ast/DesugarEnums.scala b/compiler/src/dotty/tools/dotc/ast/DesugarEnums.scala
index 112baf56c4c4..61164c4e6aee 100644
--- a/compiler/src/dotty/tools/dotc/ast/DesugarEnums.scala
+++ b/compiler/src/dotty/tools/dotc/ast/DesugarEnums.scala
@@ -49,13 +49,13 @@ object DesugarEnums {
     val tparams = enumClass.typeParams
     def isGround(tp: Type) = tp.subst(tparams, tparams.map(_ => NoType)) eq tp
     val targs = tparams map { tparam =>
-      if (tparam.variance > 0 && isGround(tparam.info.bounds.lo))
+      if (tparam.is(Covariant) && isGround(tparam.info.bounds.lo))
         tparam.info.bounds.lo
-      else if (tparam.variance < 0 && isGround(tparam.info.bounds.hi))
+      else if (tparam.is(Contravariant) && isGround(tparam.info.bounds.hi))
         tparam.info.bounds.hi
       else {
         def problem =
-          if (tparam.variance == 0) "is non variant"
+          if (!tparam.isOneOf(VarianceFlags)) "is non variant"
           else "has bounds that depend on a type parameter in the same parameter list"
         errorType(i"""cannot determine type argument for enum parent $enumClass,
                      |type parameter $tparam $problem""", ctx.source.atSpan(span))
diff --git a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
index e4d85074dc65..7af9f8b9c555 100644
--- a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
+++ b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
@@ -379,8 +379,9 @@ trait ConstraintHandling[AbstractContext] {
           case bounds: TypeBounds =>
             val lower = constraint.lower(param)
             val upper = constraint.upper(param)
-            if (lower.nonEmpty && !bounds.lo.isRef(defn.NothingClass) ||
-              upper.nonEmpty && !bounds.hi.isRef(defn.AnyClass)) constr_println(i"INIT*** $tl")
+            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))
           case _ =>
diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala
index 04c1ba81b08e..66ee24fc3898 100644
--- a/compiler/src/dotty/tools/dotc/core/Definitions.scala
+++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala
@@ -535,7 +535,7 @@ class Definitions {
   @tu lazy val StringModule: Symbol = StringClass.linkedClass
     @tu lazy val String_+ : TermSymbol = enterMethod(StringClass, nme.raw.PLUS, methOfAny(StringType), Final)
     @tu lazy val String_valueOf_Object: Symbol = StringModule.info.member(nme.valueOf).suchThat(_.info.firstParamTypes match {
-      case List(pt) => pt.isRef(AnyClass) || pt.isRef(ObjectClass)
+      case List(pt) => pt.isAny || pt.isAnyRef
       case _ => false
     }).symbol
 
diff --git a/compiler/src/dotty/tools/dotc/core/Denotations.scala b/compiler/src/dotty/tools/dotc/core/Denotations.scala
index 0301a8b9336f..48af80adc3c6 100644
--- a/compiler/src/dotty/tools/dotc/core/Denotations.scala
+++ b/compiler/src/dotty/tools/dotc/core/Denotations.scala
@@ -775,7 +775,7 @@ object Denotations {
 
     def matchesImportBound(bound: Type)(implicit ctx: Context): Boolean =
       if bound.isRef(defn.NothingClass) then false
-      else if bound.isRef(defn.AnyClass) then true
+      else if bound.isAny then true
       else NoViewsAllowed.normalizedCompatible(info, bound, keepConstraint = false)
 
     // ------ Transformations -----------------------------------------
diff --git a/compiler/src/dotty/tools/dotc/core/GadtConstraint.scala b/compiler/src/dotty/tools/dotc/core/GadtConstraint.scala
index 4ed3b42a5ba3..ef97028efd75 100644
--- a/compiler/src/dotty/tools/dotc/core/GadtConstraint.scala
+++ b/compiler/src/dotty/tools/dotc/core/GadtConstraint.scala
@@ -155,26 +155,8 @@ final class ProperGadtConstraint private(
           else if (isUpper) addLess(symTvar.origin, boundTvar.origin)
           else addLess(boundTvar.origin, symTvar.origin)
         case bound =>
-          val oldUpperBound = bounds(symTvar.origin)
-          // If we have bounds:
-          //     F >: [t] => List[t] <: [t] => Any
-          // and we want to record that:
-          //     F <: [+A] => List[A]
-          // we need to adapt the variance and instead record that:
-          //     F <: [A] => List[A]
-          // We cannot record the original bound, since it is false that:
-          //     [t] => List[t]  <:  [+A] => List[A]
-          //
-          // Note that the following code is accepted:
-          //     class Foo[F[t] >: List[t]]
-          //     type T = Foo[List]
-          // precisely because Foo[List] is desugared to Foo[[A] => List[A]].
-          //
-          // Ideally we'd adapt the bound in ConstraintHandling#addOneBound,
-          // but doing it there actually interferes with type inference.
-          val bound1 = bound.adaptHkVariances(oldUpperBound)
-          if (isUpper) addUpperBound(symTvar.origin, bound1)
-          else addLowerBound(symTvar.origin, bound1)
+          if (isUpper) addUpperBound(symTvar.origin, bound)
+          else addLowerBound(symTvar.origin, bound)
       }
     ).reporting({
       val descr = if (isUpper) "upper" else "lower"
diff --git a/compiler/src/dotty/tools/dotc/core/Hashable.scala b/compiler/src/dotty/tools/dotc/core/Hashable.scala
index d554aaecbb58..7a419efa1a9a 100644
--- a/compiler/src/dotty/tools/dotc/core/Hashable.scala
+++ b/compiler/src/dotty/tools/dotc/core/Hashable.scala
@@ -6,7 +6,7 @@ import scala.util.hashing.{ MurmurHash3 => hashing }
 import annotation.tailrec
 
 object Hashable {
- 
+
   /** A null terminated list of BindingTypes. We use `null` here for efficiency */
   class Binders(val tp: BindingType, val next: Binders)
 
@@ -44,7 +44,7 @@ trait Hashable {
     avoidSpecialHashes(hashing.finalizeHash(hashCode, arity))
 
   final def typeHash(bs: Binders, tp: Type): Int =
-    if (bs == null || tp.stableHash) tp.hash else tp.computeHash(bs)
+    if (bs == null || tp.hashIsStable) tp.hash else tp.computeHash(bs)
 
   def identityHash(bs: Binders): Int = avoidSpecialHashes(System.identityHashCode(this))
 
@@ -80,7 +80,7 @@ trait Hashable {
     finishHash(bs, hashing.mix(seed, elemHash), arity + 1, tps)
   }
 
-  
+
   protected final def doHash(x: Any): Int =
     finishHash(hashing.mix(hashSeed, x.hashCode), 1)
 
diff --git a/compiler/src/dotty/tools/dotc/core/NameKinds.scala b/compiler/src/dotty/tools/dotc/core/NameKinds.scala
index d5de95813a6c..bfe4467e8dd5 100644
--- a/compiler/src/dotty/tools/dotc/core/NameKinds.scala
+++ b/compiler/src/dotty/tools/dotc/core/NameKinds.scala
@@ -338,11 +338,6 @@ object NameKinds {
     }
   }
 
-  /** The kind of names that also encode a variance: 0 for contravariance, 1 for covariance. */
-  val VariantName: NumberedNameKind = new NumberedNameKind(VARIANT, "Variant") {
-    def mkString(underlying: TermName, info: ThisInfo) = "-+"(info.num).toString + underlying
-  }
-
   /** Names of the form N_<outer>. Emitted by inliner, replaced by outer path
    *  in ExplicitOuter.
    */
diff --git a/compiler/src/dotty/tools/dotc/core/NameOps.scala b/compiler/src/dotty/tools/dotc/core/NameOps.scala
index 7594b3a749dc..d13edc3e6cac 100644
--- a/compiler/src/dotty/tools/dotc/core/NameOps.scala
+++ b/compiler/src/dotty/tools/dotc/core/NameOps.scala
@@ -139,32 +139,8 @@ object NameOps {
       name.replace { case ExpandedName(_, unexp) => unexp }
     }
 
-    /** Remove the variance from the name. */
-    def invariantName: N = likeSpacedN {
-      name.replace { case VariantName(invariant, _) => invariant }
-    }
-
     def errorName: N = likeSpacedN(name ++ nme.ERROR)
 
-    /** Map variance value -1, +1 to 0, 1 */
-    private def varianceToNat(v: Int) = (v + 1) / 2
-
-    /** Map 0, 1 to variance value -1, +1 */
-    private def natToVariance(n: Int) = n * 2 - 1
-
-    /** Name with variance prefix: `+` for covariant, `-` for contravariant */
-    def withVariance(v: Int): N = {
-      val underlying = name.exclude(VariantName)
-      likeSpacedN(
-          if (v == 0) underlying
-          else VariantName(underlying.toTermName, varianceToNat(v)))
-    }
-
-    /** The variance as implied by the variance prefix, or 0 if there is
-     *  no variance prefix.
-     */
-    def variance: Int = name.collect { case VariantName(_, n) => natToVariance(n) }.getOrElse(0)
-
     def freshened(implicit ctx: Context): N = likeSpacedN {
       name.toTermName match {
         case ModuleClassName(original) => ModuleClassName(original.freshened)
diff --git a/compiler/src/dotty/tools/dotc/core/NameTags.scala b/compiler/src/dotty/tools/dotc/core/NameTags.scala
index df4989dafac9..8b7a581104a9 100644
--- a/compiler/src/dotty/tools/dotc/core/NameTags.scala
+++ b/compiler/src/dotty/tools/dotc/core/NameTags.scala
@@ -45,7 +45,6 @@ object NameTags extends TastyFormat.NameTags {
     case TRAITSETTER => "TRAITSETTER"
     case UNIQUE => "UNIQUE"
     case DEFAULTGETTER => "DEFAULTGETTER"
-    case VARIANT => "VARIANT"
     case OUTERSELECT => "OUTERSELECT"
 
     case SUPERACCESSOR => "SUPERACCESSOR"
diff --git a/compiler/src/dotty/tools/dotc/core/ParamInfo.scala b/compiler/src/dotty/tools/dotc/core/ParamInfo.scala
index ba28e3bc2efc..ed235a2866aa 100644
--- a/compiler/src/dotty/tools/dotc/core/ParamInfo.scala
+++ b/compiler/src/dotty/tools/dotc/core/ParamInfo.scala
@@ -3,6 +3,7 @@ package dotty.tools.dotc.core
 import Names.Name
 import Contexts.Context
 import Types.Type
+import Variances.{Variance, varianceToInt}
 
 /** A common super trait of Symbol and LambdaParam.
  *  Used to capture the attributes of type parameters which can be implemented as either.
@@ -35,7 +36,13 @@ trait ParamInfo {
   def paramInfoOrCompleter(implicit ctx: Context): Type
 
   /** The variance of the type parameter */
-  def paramVariance(implicit ctx: Context): Int
+  def paramVariance(implicit ctx: Context): Variance
+
+  /** The variance of the type parameter, as a number -1, 0, +1.
+   *  Bivariant is mapped to 1, i.e. it is treated like Covariant.
+   */
+  final def paramVarianceSign(implicit ctx: Context): Int =
+    varianceToInt(paramVariance)
 
   /** A type that refers to the parameter */
   def paramRef(implicit ctx: Context): Type
diff --git a/compiler/src/dotty/tools/dotc/core/PatternTypeConstrainer.scala b/compiler/src/dotty/tools/dotc/core/PatternTypeConstrainer.scala
index b6f9284d6269..cbc2f937acbc 100644
--- a/compiler/src/dotty/tools/dotc/core/PatternTypeConstrainer.scala
+++ b/compiler/src/dotty/tools/dotc/core/PatternTypeConstrainer.scala
@@ -191,7 +191,7 @@ trait PatternTypeConstrainer { self: TypeComparer =>
       def apply(tp: Type) = mapOver(tp) match {
         case tp @ AppliedType(tycon, args) =>
           val args1 = args.zipWithConserve(tycon.typeParams)((arg, tparam) =>
-            if (tparam.paramVariance != 0) TypeBounds.empty else arg
+            if (tparam.paramVarianceSign != 0) TypeBounds.empty else arg
           )
           tp.derivedAppliedType(tycon, args1)
         case tp =>
diff --git a/compiler/src/dotty/tools/dotc/core/SymDenotations.scala b/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
index 73380bd7bbfd..0e4e7d4d52e2 100644
--- a/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
+++ b/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
@@ -12,6 +12,7 @@ import dotty.tools.io.AbstractFile
 import Decorators.SymbolIteratorDecorator
 import ast._
 import Trees.Literal
+import Variances.Variance
 import annotation.tailrec
 import util.SimpleIdentityMap
 import util.Stats
@@ -1374,13 +1375,13 @@ object SymDenotations {
     def namedType(implicit ctx: Context): NamedType =
       if (isType) typeRef else termRef
 
-    /** The variance of this type parameter or type member as an Int, with
-     *  +1 = Covariant, -1 = Contravariant, 0 = Nonvariant, or not a type parameter
+    /** The variance of this type parameter or type member as a subset of
+     *  {Covariant, Contravariant}
      */
-    final def variance(implicit ctx: Context): Int =
-      if (this.is(Covariant)) 1
-      else if (this.is(Contravariant)) -1
-      else 0
+    final def variance(implicit ctx: Context): Variance =
+      if is(Covariant) then Covariant
+      else if is(Contravariant) then Contravariant
+      else EmptyFlags
 
     /** The flags to be used for a type parameter owned by this symbol.
      *  Overridden by ClassDenotation.
diff --git a/compiler/src/dotty/tools/dotc/core/Symbols.scala b/compiler/src/dotty/tools/dotc/core/Symbols.scala
index 0fe9076eab8c..4ee962aaa915 100644
--- a/compiler/src/dotty/tools/dotc/core/Symbols.scala
+++ b/compiler/src/dotty/tools/dotc/core/Symbols.scala
@@ -22,6 +22,7 @@ import ast.tpd
 import tpd.{Tree, TreeProvider, TreeOps}
 import ast.TreeTypeMap
 import Constants.Constant
+import Variances.{Variance, varianceFromInt}
 import reporting.diagnostic.Message
 import collection.mutable
 import io.AbstractFile
@@ -699,7 +700,7 @@ object Symbols {
     def paramInfo(implicit ctx: Context): Type = denot.info
     def paramInfoAsSeenFrom(pre: Type)(implicit ctx: Context): Type = pre.memberInfo(this)
     def paramInfoOrCompleter(implicit ctx: Context): Type = denot.infoOrCompleter
-    def paramVariance(implicit ctx: Context): Int = denot.variance
+    def paramVariance(implicit ctx: Context): Variance = denot.variance
     def paramRef(implicit ctx: Context): TypeRef = denot.typeRef
 
 // -------- Printing --------------------------------------------------------
diff --git a/compiler/src/dotty/tools/dotc/core/TypeApplications.scala b/compiler/src/dotty/tools/dotc/core/TypeApplications.scala
index ce386e17ec68..569e7dfaa8bd 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeApplications.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeApplications.scala
@@ -10,6 +10,7 @@ import Decorators._
 import util.Stats._
 import Names._
 import NameOps._
+import Variances.variancesConform
 import dotty.tools.dotc.config.Config
 
 object TypeApplications {
@@ -22,24 +23,6 @@ object TypeApplications {
     case _ => tp
   }
 
-  /** Does variance `v1` conform to variance `v2`?
-   *  This is the case if the variances are the same or `sym` is nonvariant.
-   */
-  def varianceConforms(v1: Int, v2: Int): Boolean =
-    v1 == v2 || v2 == 0
-
-  /** Does the variance of type parameter `tparam1` conform to the variance of type parameter `tparam2`?
-   */
-  def varianceConforms(tparam1: TypeParamInfo, tparam2: TypeParamInfo)(implicit ctx: Context): Boolean =
-    varianceConforms(tparam1.paramVariance, tparam2.paramVariance)
-
-  /** Do the variances of type parameters `tparams1` conform to the variances
-   *  of corresponding type parameters `tparams2`?
-   *  This is only the case of `tparams1` and `tparams2` have the same length.
-   */
-  def variancesConform(tparams1: List[TypeParamInfo], tparams2: List[TypeParamInfo])(implicit ctx: Context): Boolean =
-    tparams1.corresponds(tparams2)(varianceConforms)
-
   /** Extractor for
    *
    *    [v1 X1: B1, ..., vn Xn: Bn] -> C[X1, ..., Xn]
@@ -156,8 +139,6 @@ class TypeApplications(val self: Type) extends AnyVal {
   /** The type parameters of this type are:
    *  For a ClassInfo type, the type parameters of its class.
    *  For a typeref referring to a class, the type parameters of the class.
-   *  For a typeref referring to a Lambda class, the type parameters of
-   *    its right hand side or upper bound.
    *  For a refinement type, the type parameters of its parent, dropping
    *  any type parameter that is-rebound by the refinement.
    */
@@ -269,11 +250,9 @@ class TypeApplications(val self: Type) extends AnyVal {
   /** Convert a type constructor `TC` which has type parameters `X1, ..., Xn`
    *  to `[X1, ..., Xn] -> TC[X1, ..., Xn]`.
    */
-  def EtaExpand(tparams: List[TypeSymbol])(implicit ctx: Context): Type = {
-    val tparamsToUse = if (variancesConform(typeParams, tparams)) tparams else typeParamSymbols
-    HKTypeLambda.fromParams(tparamsToUse, self.appliedTo(tparams.map(_.typeRef)))
+  def EtaExpand(tparams: List[TypeSymbol])(implicit ctx: Context): Type =
+    HKTypeLambda.fromParams(tparams, self.appliedTo(tparams.map(_.typeRef)))
       //.ensuring(res => res.EtaReduce =:= self, s"res = $res, core = ${res.EtaReduce}, self = $self, hc = ${res.hashCode}")
-  }
 
   /** If self is not lambda-bound, eta expand it. */
   def ensureLambdaSub(implicit ctx: Context): Type =
@@ -290,62 +269,6 @@ class TypeApplications(val self: Type) extends AnyVal {
     }
   }
 
-  /** If argument A and type parameter P are higher-kinded, adapt the variances
-   *  of A to those of P, ensuring that the variances of the type lambda A
-   *  agree with the variances of corresponding higher-kinded type parameters of P. Example:
-   *
-   *     class GenericCompanion[+CC[X]]
-   *     GenericCompanion[List]
-   *
-   *  with adaptHkVariances, the argument `List` will expand to
-   *
-   *     [X] => List[X]
-   *
-   *  instead of
-   *
-   *     [+X] => List[X]
-   *
-   *  even though `List` is covariant. This adaptation is necessary to ignore conflicting
-   *  variances in overriding members that have types of hk-type parameters such as
-   *  `GenericCompanion[GenTraversable]` or `GenericCompanion[ListBuffer]`.
-   *  When checking overriding, we need to validate the subtype relationship
-   *
-   *      GenericCompanion[[X] -> ListBuffer[X]] <: GenericCompanion[[+X] -> GenTraversable[X]]
-   *
-   *   Without adaptation, this would be false, and hence an overriding error would
-   *   result. But with adaptation, the rhs argument will be adapted to
-   *
-   *     [X] -> GenTraversable[X]
-   *
-   *   which makes the subtype test succeed. The crucial point here is that, since
-   *   GenericCompanion only expects a non-variant CC, the fact that GenTraversable
-   *   is covariant is irrelevant, so can be ignored.
-   */
-  def adaptHkVariances(bound: Type)(implicit ctx: Context): Type = {
-    val hkParams = bound.hkTypeParams
-    if (hkParams.isEmpty) self
-    else {
-      def adaptArg(arg: Type): Type = arg match {
-        case arg @ HKTypeLambda(tparams, body) if
-             !tparams.corresponds(hkParams)(_.paramVariance == _.paramVariance) &&
-             tparams.corresponds(hkParams)(varianceConforms) =>
-          HKTypeLambda(
-            tparams.lazyZip(hkParams).map((tparam, hkparam) =>
-              tparam.paramName.withVariance(hkparam.paramVariance)))(
-            tl => arg.paramInfos.map(_.subst(arg, tl).bounds),
-            tl => arg.resultType.subst(arg, tl)
-          )
-        case arg: AliasingBounds =>
-          arg.derivedAlias(adaptArg(arg.alias))
-        case arg @ TypeBounds(lo, hi) =>
-          arg.derivedTypeBounds(adaptArg(lo), adaptArg(hi))
-        case _ =>
-          arg
-      }
-      adaptArg(self)
-    }
-  }
-
   /** The type representing
    *
    *     T[U1, ..., Un]
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 0f0b7267fff3..c56823057d4e 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -11,6 +11,7 @@ import config.Config
 import config.Printers.{constr, subtyping, gadts, noPrinter}
 import TypeErasure.{erasedLub, erasedGlb}
 import TypeApplications._
+import Variances.{Variance, variancesConform}
 import Constants.Constant
 import transform.TypeUtils._
 import transform.SymUtils._
@@ -500,7 +501,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
             val base = nonExprBaseType(tp1, cls2)
             if (base.typeSymbol == cls2) return true
           }
-          else if (tp1.isLambdaSub && !tp1.isRef(AnyKindClass))
+          else if tp1.isLambdaSub && !tp1.isAnyKind then
             return recur(tp1, EtaExpansion(cls2.typeRef))
         fourthTry
     }
@@ -595,14 +596,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
             val saved = comparedTypeLambdas
             comparedTypeLambdas += tp1
             comparedTypeLambdas += tp2
-            val variancesOK =
-              variancesConform(tp1.typeParams, tp2.typeParams)
-              || { // if tp1 is of the form [X] =>> C[X] where `C` is co- or contra-variant
-                   // assume the variance of `C` for `tp1` instead. Fixes #7648.
-                tp1 match
-                  case EtaExpansion(tycon1) => variancesConform(tycon1.typeParams, tp2.typeParams)
-                  case _ => false
-              }
+            val variancesOK = variancesConform(tp1.typeParams, tp2.typeParams)
             try variancesOK && boundsOK && isSubType(tp1.resType, tp2.resType.subst(tp2, tp1))
             finally comparedTypeLambdas = saved
           case _ =>
@@ -740,7 +734,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
               (gbounds1 != null) &&
                 (isSubTypeWhenFrozen(gbounds1.hi, tp2) ||
                 narrowGADTBounds(tp1, tp2, approx, isUpper = true)) &&
-                { tp2.isRef(AnyClass) || GADTusage(tp1.symbol) }
+                { tp2.isAny || GADTusage(tp1.symbol) }
             }
             isSubType(hi1, tp2, approx.addLow) || compareGADT || tryLiftedToThis1
           case _ =>
@@ -822,7 +816,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
       case JavaArrayType(elem1) =>
         def compareJavaArray = tp2 match {
           case JavaArrayType(elem2) => isSubType(elem1, elem2)
-          case _ => tp2 isRef ObjectClass
+          case _ => tp2.isAnyRef
         }
         compareJavaArray
       case tp1: ExprType if ctx.phase.id > ctx.gettersPhase.id =>
@@ -1213,7 +1207,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
       if (args1.isEmpty) args2.isEmpty
       else args2.nonEmpty && {
         val tparam = tparams2.head
-        val v = tparam.paramVariance
+        val v = tparam.paramVarianceSign
 
         /** Try a capture conversion:
          *  If the original left-hand type `leftRoot` is a path `p.type`,
@@ -1278,14 +1272,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
             }
         }
 
-        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)
-        }
+        isSubArg(args1.head, args2.head)
       } && recurArgs(args1.tail, args2.tail, tparams2.tail)
 
     recurArgs(args1, args2, tparams2)
@@ -1552,19 +1539,12 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
    *       Further, no refinement refers back to the refined type via a refined this.
    *  The precondition is established by `skipMatching`.
    */
-  private def isSubRefinements(tp1: RefinedType, tp2: RefinedType, limit: Type): Boolean = {
-    def hasSubRefinement(tp1: RefinedType, refine2: Type): Boolean =
-      isSubType(tp1.refinedInfo, refine2) || {
-        // last effort: try to adapt variances of higher-kinded types if this is sound.
-        // TODO: Move this to eta-expansion?
-        val adapted2 = refine2.adaptHkVariances(tp1.parent.member(tp1.refinedName).symbol.info)
-        adapted2.ne(refine2) && hasSubRefinement(tp1, adapted2)
-      }
-    hasSubRefinement(tp1, tp2.refinedInfo) && (
-      (tp2.parent eq limit) ||
-      isSubRefinements(
-        tp1.parent.asInstanceOf[RefinedType], tp2.parent.asInstanceOf[RefinedType], limit))
-  }
+  private def isSubRefinements(tp1: RefinedType, tp2: RefinedType, limit: Type): Boolean =
+    isSubType(tp1.refinedInfo, tp2.refinedInfo)
+    && ((tp2.parent eq limit)
+       || isSubRefinements(
+            tp1.parent.asInstanceOf[RefinedType],
+            tp2.parent.asInstanceOf[RefinedType], limit))
 
   /** A type has been covered previously in subtype checking if it
    *  is some combination of TypeRefs that point to classes, where the
@@ -1649,20 +1629,21 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
             // 'Object|Null', depending on whether explicit nulls are enabled.
             def formal1IsObject =
               if (ctx.explicitNulls) formal1 match {
-                case OrNull(formal1b) => formal1b.isRef(ObjectClass)
+                case OrNull(formal1b) => formal1b.isAnyRef
                 case _ => false
               }
-              else formal1.isRef(ObjectClass)
+              else formal1.isAnyRef
             def formal2IsObject =
               if (ctx.explicitNulls) formal2 match {
-                case OrNull(formal2b) => formal2b.isRef(ObjectClass)
+                case OrNull(formal2b) => formal2b.isAnyRef
                 case _ => false
               }
-              else formal2.isRef(ObjectClass)
+              else formal2.isAnyRef
             (isSameTypeWhenFrozen(formal1, formal2a)
-            || tp1.isJavaMethod && formal2IsObject && (formal1 isRef AnyClass)
-            || tp2.isJavaMethod && formal1IsObject && (formal2 isRef AnyClass)) &&
-            loop(rest1, rest2)
+             || tp1.isJavaMethod && formal2IsObject && formal1.isAny
+             || tp2.isJavaMethod && formal1IsObject && formal2.isAny
+            )
+            && loop(rest1, rest2)
           case nil =>
             false
         }
@@ -1743,8 +1724,8 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
     if (tp1 eq tp2) tp1
     else if (!tp1.exists) tp2
     else if (!tp2.exists) tp1
-    else if ((tp1 isRef AnyClass) && !tp2.isLambdaSub || (tp1 isRef AnyKindClass) || (tp2 isRef NothingClass)) tp2
-    else if ((tp2 isRef AnyClass) && !tp1.isLambdaSub || (tp2 isRef AnyKindClass) || (tp1 isRef NothingClass)) tp1
+    else if tp1.isAny && !tp2.isLambdaSub || tp1.isAnyKind || tp2.isRef(NothingClass) then tp2
+    else if tp2.isAny && !tp1.isLambdaSub || tp2.isAnyKind || tp1.isRef(NothingClass) then tp1
     else tp2 match {  // normalize to disjunctive normal form if possible.
       case OrType(tp21, tp22) =>
         tp1 & tp21 | tp1 & tp22
@@ -1790,11 +1771,12 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
    *  @note  We do not admit singleton types in or-types as lubs.
    */
   def lub(tp1: Type, tp2: Type, canConstrain: Boolean = false): Type = /*>|>*/ trace(s"lub(${tp1.show}, ${tp2.show}, canConstrain=$canConstrain)", subtyping, show = true) /*<|<*/ {
+
     if (tp1 eq tp2) tp1
     else if (!tp1.exists) tp1
     else if (!tp2.exists) tp2
-    else if ((tp1 isRef AnyClass) || (tp1 isRef AnyKindClass) || (tp2 isRef NothingClass)) tp1
-    else if ((tp2 isRef AnyClass) || (tp2 isRef AnyKindClass) || (tp1 isRef NothingClass)) tp2
+    else if tp1.isAny && !tp2.isLambdaSub || tp1.isAnyKind || tp2.isRef(NothingClass) then tp1
+    else if tp2.isAny && !tp1.isLambdaSub || tp2.isAnyKind || tp1.isRef(NothingClass) then tp2
     else {
       def mergedLub: Type = {
         val atoms1 = tp1.atoms
@@ -1839,7 +1821,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
         val arg1 :: args1Rest = args1
         val arg2 :: args2Rest = args2
         val common = singletonInterval(arg1, arg2)
-        val v = tparam.paramVariance
+        val v = tparam.paramVarianceSign
         val lubArg =
           if (common.exists) common
           else if (v > 0) lub(arg1.hiBound, arg2.hiBound, canConstrain)
@@ -1871,7 +1853,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
         val arg1 :: args1Rest = args1
         val arg2 :: args2Rest = args2
         val common = singletonInterval(arg1, arg2)
-        val v = tparam.paramVariance
+        val v = tparam.paramVarianceSign
         val glbArg =
           if (common.exists) common
           else if (v > 0) glb(arg1.hiBound, arg2.hiBound)
@@ -1951,7 +1933,16 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
       val t2 = distributeAnd(tp2, tp1)
       if (t2.exists) t2
       else if (isErased) erasedGlb(tp1, tp2, isJava = false)
-      else liftIfHK(tp1, tp2, op, original)
+      else liftIfHK(tp1, tp2, op, original, _ | _)
+        // The ` | ` on variances is needed since variances are associated with bounds
+        // not lambdas. Example:
+        //
+        //    trait A { def F[-X] }
+        //    trait B { def F[+X] }
+        //    object O extends A, B { ... }
+        //
+        // Here, `F` is treated as bivariant in `O`. That is, only bivariant implementation
+        // of `F` are allowed. See neg/hk-variance2s.scala test.
     }
   }
 
@@ -1999,7 +1990,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
       val t2 = distributeOr(tp2, tp1)
       if (t2.exists) t2
       else if (isErased) erasedLub(tp1, tp2)
-      else liftIfHK(tp1, tp2, OrType(_, _), _ | _)
+      else liftIfHK(tp1, tp2, OrType(_, _), _ | _, _ & _)
     }
   }
 
@@ -2008,7 +1999,8 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
    *
    *    [X1, ..., Xn] -> op(tp1[X1, ..., Xn], tp2[X1, ..., Xn])
    */
-  private def liftIfHK(tp1: Type, tp2: Type, op: (Type, Type) => Type, original: (Type, Type) => Type) = {
+  private def liftIfHK(tp1: Type, tp2: Type,
+      op: (Type, Type) => Type, original: (Type, Type) => Type, combineVariance: (Variance, Variance) => Variance) = {
     val tparams1 = tp1.typeParams
     val tparams2 = tp2.typeParams
     def applied(tp: Type) = tp.appliedTo(tp.typeParams.map(_.paramInfoAsSeenFrom(tp)))
@@ -2019,9 +2011,12 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
       original(applied(tp1), tp2)
     else if (tparams1.hasSameLengthAs(tparams2))
       HKTypeLambda(
-        paramNames = HKTypeLambda.syntheticParamNames(tparams1.length).lazyZip(tparams1).lazyZip(tparams2)
-          .map((pname, tparam1, tparam2) =>
-            pname.withVariance((tparam1.paramVariance + tparam2.paramVariance) / 2)))(
+        paramNames = HKTypeLambda.syntheticParamNames(tparams1.length),
+        variances =
+          if tp1.isDeclaredVarianceLambda && tp2.isDeclaredVarianceLambda then
+            tparams1.lazyZip(tparams2).map((p1, p2) => combineVariance(p1.paramVariance, p2.paramVariance))
+          else Nil
+      )(
         paramInfosExp = tl => tparams1.lazyZip(tparams2).map((tparam1, tparam2) =>
           tl.integrate(tparams1, tparam1.paramInfoAsSeenFrom(tp1)).bounds &
           tl.integrate(tparams2, tparam2.paramInfoAsSeenFrom(tp2)).bounds),
@@ -2210,7 +2205,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
       case OrType(tp1, tp2) => provablyEmpty(tp1) && provablyEmpty(tp2)
       case at @ AppliedType(tycon, args) =>
         args.lazyZip(tycon.typeParams).exists { (arg, tparam) =>
-          tparam.paramVariance >= 0
+          tparam.paramVarianceSign >= 0
           && provablyEmpty(arg)
           && typeparamCorrespondsToField(tycon, tparam)
         }
@@ -2285,7 +2280,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
 
         args1.lazyZip(args2).lazyZip(tycon1.typeParams).exists {
           (arg1, arg2, tparam) =>
-            val v = tparam.paramVariance
+            val v = tparam.paramVarianceSign
             if (v > 0)
               covariantDisjoint(arg1, arg2, tparam)
             else if (v < 0)
diff --git a/compiler/src/dotty/tools/dotc/core/TypeErasure.scala b/compiler/src/dotty/tools/dotc/core/TypeErasure.scala
index ff5671246529..c367a538f7aa 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeErasure.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeErasure.scala
@@ -493,7 +493,7 @@ class TypeErasure(isJava: Boolean, semiEraseVCs: Boolean, isConstructor: Boolean
             case tr :: trs1 =>
               assert(!tr.classSymbol.is(Trait), i"$cls has bad parents $parents%, %")
               val tr1 = if (cls.is(Trait)) defn.ObjectType else tr
-              tr1 :: trs1.filterNot(_ isRef defn.ObjectClass)
+              tr1 :: trs1.filterNot(_.isAnyRef)
             case nil => nil
           }
         val erasedDecls = decls.filteredScope(sym => !sym.isType || sym.isClass)
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index 1722d6ea29b2..1feef89d27c0 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -18,6 +18,7 @@ import Decorators._
 import Denotations._
 import Periods._
 import CheckRealizable._
+import Variances.{Variance, varianceFromInt, varianceToInt, setStructuralVariances, Invariant}
 import util.Stats._
 import util.SimpleIdentitySet
 import reporting.diagnostic.Message
@@ -29,7 +30,7 @@ import Hashable._
 import Uniques._
 import collection.mutable
 import config.Config
-import annotation.tailrec
+import annotation.{tailrec, constructorOnly}
 import language.implicitConversions
 import scala.util.hashing.{ MurmurHash3 => hashing }
 import config.Printers.{core, typr}
@@ -176,18 +177,18 @@ object Types {
      *        It makes no sense for it to be an alias type because isRef would always
      *        return false in that case.
      */
-    def isRef(sym: Symbol)(implicit ctx: Context): Boolean = stripAnnots.stripTypeVar match {
+    def isRef(sym: Symbol, skipRefined: Boolean = true)(implicit ctx: Context): Boolean = stripAnnots.stripTypeVar match {
       case this1: TypeRef =>
         this1.info match { // see comment in Namer#typeDefSig
-          case TypeAlias(tp) => tp.isRef(sym)
+          case TypeAlias(tp) => tp.isRef(sym, skipRefined)
           case _ => this1.symbol eq sym
         }
-      case this1: RefinedOrRecType =>
-        this1.parent.isRef(sym)
+      case this1: RefinedOrRecType if skipRefined =>
+        this1.parent.isRef(sym, skipRefined)
       case this1: AppliedType =>
         val this2 = this1.dealias
-        if (this2 ne this1) this2.isRef(sym)
-        else this1.underlying.isRef(sym)
+        if (this2 ne this1) this2.isRef(sym, skipRefined)
+        else this1.underlying.isRef(sym, skipRefined)
       case _ => false
     }
 
@@ -200,6 +201,10 @@ object Types {
         false
     }
 
+    def isAny(given Context): Boolean     = isRef(defn.AnyClass, skipRefined = false)
+    def isAnyRef(given Context): Boolean  = isRef(defn.ObjectClass, skipRefined = false)
+    def isAnyKind(given Context): Boolean = isRef(defn.AnyKindClass, skipRefined = false)
+
     /** Does this type refer exactly to class symbol `sym`, instead of to a subclass of `sym`?
      *  Implemented like `isRef`, but follows more types: all type proxies as well as and- and or-types
      */
@@ -362,6 +367,9 @@ object Types {
       case _ => false
     }
 
+    /** Is this a higher-kinded type lambda with given parameter variances? */
+    def isDeclaredVarianceLambda: Boolean = false
+
 // ----- Higher-order combinators -----------------------------------
 
     /** Returns true if there is a part of this type that satisfies predicate `p`.
@@ -1670,7 +1678,7 @@ object Types {
     def computeHash(bs: Binders): Int
 
     /** Is the `hash` of this type the same for all possible sequences of enclosing binders? */
-    def stableHash: Boolean = true
+    def hashIsStable: Boolean = true
   }
 
   // end Type
@@ -2035,7 +2043,7 @@ object Types {
       if (0 <= idx && idx < args.length) {
         val argInfo = args(idx) match {
           case arg: TypeBounds =>
-            val v = param.paramVariance
+            val v = param.paramVarianceSign
             val pbounds = param.paramInfo
             if (v > 0 && pbounds.loBound.dealiasKeepAnnots.isBottomType) TypeAlias(arg.hiBound & rebase(pbounds.hiBound))
             else if (v < 0 && pbounds.hiBound.dealiasKeepAnnots.isTopType) TypeAlias(arg.loBound | rebase(pbounds.loBound))
@@ -2191,7 +2199,7 @@ object Types {
         case base: AndOrType =>
           var tp1 = argForParam(base.tp1)
           var tp2 = argForParam(base.tp2)
-          val variance = tparam.paramVariance
+          val variance = tparam.paramVarianceSign
           if (isBounds(tp1) || isBounds(tp2) || variance == 0) {
             // compute argument as a type bounds instead of a point type
             tp1 = tp1.bounds
@@ -2331,8 +2339,8 @@ object Types {
 
     override def computeHash(bs: Binders): Int = doHash(bs, designator, prefix)
 
-    override def stableHash: Boolean = {
-      if (myStableHash == 0) myStableHash = if (prefix.stableHash) 1 else -1
+    override def hashIsStable: Boolean = {
+      if (myStableHash == 0) myStableHash = if (prefix.hashIsStable) 1 else -1
       myStableHash > 0
     }
 
@@ -2616,7 +2624,7 @@ object Types {
       else parent
 
     override def computeHash(bs: Binders): Int = doHash(bs, refinedName, refinedInfo, parent)
-    override def stableHash: Boolean = refinedInfo.stableHash && parent.stableHash
+    override def hashIsStable: Boolean = refinedInfo.hashIsStable && parent.hashIsStable
 
     override def eql(that: Type): Boolean = that match {
       case that: RefinedType =>
@@ -2717,7 +2725,7 @@ object Types {
 
     override def computeHash(bs: Binders): Int = doHash(new Binders(this, bs), parent)
 
-    override def stableHash: Boolean = false
+    override def hashIsStable: Boolean = false
       // this is a conservative observation. By construction RecTypes contain at least
       // one RecThis occurrence. Since `stableHash` does not keep track of enclosing
       // bound types, it will return "unstable" for this occurrence and this would propagate.
@@ -3025,7 +3033,7 @@ object Types {
       if (resType eq this.resType) this else ExprType(resType)
 
     override def computeHash(bs: Binders): Int = doHash(bs, resType)
-    override def stableHash: Boolean = resType.stableHash
+    override def hashIsStable: Boolean = resType.hashIsStable
 
     override def eql(that: Type): Boolean = that match {
       case that: ExprType => resType.eq(that.resType)
@@ -3110,38 +3118,19 @@ object Types {
       if ((paramNames eq this.paramNames) && (paramInfos eq this.paramInfos) && (resType eq this.resType)) this
       else newLikeThis(paramNames, paramInfos, resType)
 
-    final def newLikeThis(paramNames: List[ThisName], paramInfos: List[PInfo], resType: Type)(implicit ctx: Context): This =
+    def newLikeThis(paramNames: List[ThisName], paramInfos: List[PInfo], resType: Type)(implicit ctx: Context): This =
       companion(paramNames)(
           x => paramInfos.mapConserve(_.subst(this, x).asInstanceOf[PInfo]),
           x => resType.subst(this, x))
 
     protected def prefixString: String
-    final override def toString: String = s"$prefixString($paramNames, $paramInfos, $resType)"
+    override def toString: String = s"$prefixString($paramNames, $paramInfos, $resType)"
   }
 
   abstract class HKLambda extends CachedProxyType with LambdaType {
     final override def underlying(implicit ctx: Context): Type = resType
-
-    override def computeHash(bs: Binders): Int =
-      doHash(new Binders(this, bs), paramNames, resType, paramInfos)
-
-    override def stableHash: Boolean = resType.stableHash && paramInfos.stableHash
-
+    final override def hashIsStable: Boolean = resType.hashIsStable && paramInfos.hashIsStable
     final override def equals(that: Any): Boolean = equals(that, null)
-
-    // No definition of `eql` --> fall back on equals, which calls iso
-
-    final override def iso(that: Any, bs: BinderPairs): Boolean = that match {
-      case that: HKLambda =>
-        paramNames.eqElements(that.paramNames) &&
-        companion.eq(that.companion) && {
-          val bs1 = new BinderPairs(this, that, bs)
-          paramInfos.equalElements(that.paramInfos, bs1) &&
-          resType.equals(that.resType, bs1)
-        }
-      case _ =>
-        false
-    }
   }
 
   abstract class MethodOrPoly extends UncachedGroundType with LambdaType with MethodicType {
@@ -3328,14 +3317,11 @@ object Types {
     def apply(paramInfos: List[PInfo], resultType: Type)(implicit ctx: Context): LT =
       apply(syntheticParamNames(paramInfos.length), paramInfos, resultType)
 
-    protected def paramName(param: ParamInfo.Of[N])(implicit ctx: Context): N =
-      param.paramName
-
     protected def toPInfo(tp: Type)(implicit ctx: Context): PInfo
 
     def fromParams[PI <: ParamInfo.Of[N]](params: List[PI], resultType: Type)(implicit ctx: Context): Type =
       if (params.isEmpty) resultType
-      else apply(params.map(paramName))(
+      else apply(params.map(_.paramName))(
         tl => params.map(param => toPInfo(tl.integrate(params, param.paramInfo))),
         tl => tl.integrate(params, resultType))
   }
@@ -3447,17 +3433,20 @@ object Types {
   }
 
   /** A type lambda of the form `[X_0 B_0, ..., X_n B_n] => T`
-   *  Variances are encoded in parameter names. A name starting with `+`
-   *  designates a covariant parameter, a name starting with `-` designates
-   *  a contravariant parameter, and every other name designates a non-variant parameter.
    *
    *  @param  paramNames      The names `X_0`, ..., `X_n`
    *  @param  paramInfosExp  A function that, given the polytype itself, returns the
    *                          parameter bounds `B_1`, ..., `B_n`
    *  @param  resultTypeExp   A function that, given the polytype itself, returns the
    *                          result type `T`.
+   *  @param  variances       The variances of the type parameters, if the type lambda
+   *                          carries variances, i.e. it is a bound of an abstract type
+   *                          or the rhs of a match alias or opaque alias. The parameter
+   *                          is Nil for all other lambdas.
+   *
+   *  Variances are stored in the `typeParams` list of the lambda.
    */
-  class HKTypeLambda(val paramNames: List[TypeName])(
+  class HKTypeLambda(val paramNames: List[TypeName], @constructorOnly variances: List[Variance])(
       paramInfosExp: HKTypeLambda => List[TypeBounds], resultTypeExp: HKTypeLambda => Type)
   extends HKLambda with TypeLambda {
     type This = HKTypeLambda
@@ -3469,7 +3458,55 @@ object Types {
     assert(resType.isInstanceOf[TermType], this)
     assert(paramNames.nonEmpty)
 
+    private def setVariances(tparams: List[LambdaParam], vs: List[Variance]): Unit =
+      if tparams.nonEmpty then
+        tparams.head.declaredVariance = vs.head
+        setVariances(tparams.tail, vs.tail)
+
+    override val isDeclaredVarianceLambda = variances.nonEmpty
+    if isDeclaredVarianceLambda then setVariances(typeParams, variances)
+
+    def declaredVariances =
+      if isDeclaredVarianceLambda then typeParams.map(_.declaredVariance)
+      else Nil
+
+    override def computeHash(bs: Binders): Int =
+      doHash(new Binders(this, bs), declaredVariances ::: paramNames, resType, paramInfos)
+
+    // No definition of `eql` --> fall back on equals, which calls iso
+
+    final override def iso(that: Any, bs: BinderPairs): Boolean = that match {
+      case that: HKTypeLambda =>
+        paramNames.eqElements(that.paramNames)
+        && isDeclaredVarianceLambda == that.isDeclaredVarianceLambda
+        && (!isDeclaredVarianceLambda
+            || typeParams.corresponds(that.typeParams)((x, y) =>
+                  x.declaredVariance == y.declaredVariance))
+        && {
+          val bs1 = new BinderPairs(this, that, bs)
+          paramInfos.equalElements(that.paramInfos, bs1) &&
+          resType.equals(that.resType, bs1)
+        }
+      case _ =>
+        false
+    }
+
+    override def newLikeThis(paramNames: List[ThisName], paramInfos: List[PInfo], resType: Type)(implicit ctx: Context): This =
+      newLikeThis(paramNames, declaredVariances, paramInfos, resType)
+
+    def newLikeThis(paramNames: List[ThisName], variances: List[Variance], paramInfos: List[PInfo], resType: Type)(implicit ctx: Context): This =
+      HKTypeLambda(paramNames, variances)(
+          x => paramInfos.mapConserve(_.subst(this, x).asInstanceOf[PInfo]),
+          x => resType.subst(this, x))
+
+    def withVariances(variances: List[Variance])(implicit ctx: Context): This =
+      newLikeThis(paramNames, variances, paramInfos, resType)
+
     protected def prefixString: String = "HKTypeLambda"
+    final override def toString: String =
+      if isDeclaredVarianceLambda then
+        s"HKTypeLambda($paramNames, $paramInfos, $resType, ${declaredVariances.map(_.flagsString)})"
+      else super.toString
   }
 
   /** The type of a polymorphic method. It has the same form as HKTypeLambda,
@@ -3519,7 +3556,12 @@ object Types {
     def apply(paramNames: List[TypeName])(
         paramInfosExp: HKTypeLambda => List[TypeBounds],
         resultTypeExp: HKTypeLambda => Type)(implicit ctx: Context): HKTypeLambda =
-      unique(new HKTypeLambda(paramNames)(paramInfosExp, resultTypeExp))
+      apply(paramNames, Nil)(paramInfosExp, resultTypeExp)
+
+    def apply(paramNames: List[TypeName], variances: List[Variance])(
+        paramInfosExp: HKTypeLambda => List[TypeBounds],
+        resultTypeExp: HKTypeLambda => Type)(implicit ctx: Context): HKTypeLambda =
+      unique(new HKTypeLambda(paramNames, variances)(paramInfosExp, resultTypeExp))
 
     def unapply(tl: HKTypeLambda): Some[(List[LambdaParam], Type)] =
       Some((tl.typeParams, tl.resType))
@@ -3528,25 +3570,56 @@ object Types {
       apply(syntheticParamNames(n))(
         pt => List.fill(n)(TypeBounds.empty), pt => defn.AnyType)
 
-    override def paramName(param: ParamInfo.Of[TypeName])(implicit ctx: Context): TypeName =
-      param.paramName.withVariance(param.paramVariance)
+    override def fromParams[PI <: ParamInfo.Of[TypeName]](params: List[PI], resultType: Type)(implicit ctx: Context): Type =
+      resultType match
+        case bounds: TypeBounds => boundsFromParams(params, bounds)
+        case _ => super.fromParams(params, resultType)
 
     /** Distributes Lambda inside type bounds. Examples:
      *
      *      type T[X] = U        becomes    type T = [X] -> U
      *      type T[X] <: U       becomes    type T >: Nothing <: ([X] -> U)
      *      type T[X] >: L <: U  becomes    type T >: ([X] -> L) <: ([X] -> U)
+     *
+     *  The variances of regular TypeBounds types, as well as of match aliases
+     *  and of opaque aliases are always determined from the given parameters
+     *  `params`. The variances of other type aliases are determined from
+     *  the given parameters only if one of these parameters carries a `+`
+     *  or `-` variance annotation. Type aliases without variance annotation
+     *  are treated structurally. That is, their parameter variances are
+     *  determined by how the parameter(s) appear in the result type.
+     *
+     *  Examples:
+     *
+     *    type T[X] >: A              // X is invariant
+     *    type T[X] <: List[X]        // X is invariant
+     *    type T[X] = List[X]         // X is covariant (determined structurally)
+     *    opaque type T[X] = List[X]  // X is invariant
+     *    opaque type T[+X] = List[X] // X is covariant
+     *    type T[A, B] = A => B       // A is contravariant, B is covariant (determined structurally)
+     *    type T[A, +B] = A => B      // A is invariant, B is covariant
      */
-    override def fromParams[PI <: ParamInfo.Of[TypeName]](params: List[PI], resultType: Type)(implicit ctx: Context): Type = {
-      def expand(tp: Type) = super.fromParams(params, tp)
-      resultType match {
-        case rt: AliasingBounds =>
-          rt.derivedAlias(expand(rt.alias))
-        case rt @ TypeBounds(lo, hi) =>
-          rt.derivedTypeBounds(
-            if (lo.isRef(defn.NothingClass)) lo else expand(lo), expand(hi))
-        case rt =>
-          expand(rt)
+    def boundsFromParams[PI <: ParamInfo.Of[TypeName]](params: List[PI], bounds: TypeBounds)(implicit ctx: Context): TypeBounds = {
+      def expand(tp: Type, useVariances: Boolean) =
+        if params.nonEmpty && useVariances then
+          apply(params.map(_.paramName), params.map(_.paramVariance))(
+            tl => params.map(param => toPInfo(tl.integrate(params, param.paramInfo))),
+            tl => tl.integrate(params, tp))
+        else
+          super.fromParams(params, tp)
+      def isOpaqueAlias = params match
+        case (param: Symbol) :: _ => param.owner.is(Opaque)
+        case _ => false
+      bounds match {
+        case bounds: MatchAlias =>
+          bounds.derivedAlias(expand(bounds.alias, true))
+        case bounds: TypeAlias =>
+          bounds.derivedAlias(expand(bounds.alias,
+            isOpaqueAlias || params.exists(!_.paramVariance.isEmpty)))
+        case TypeBounds(lo, hi) =>
+          bounds.derivedTypeBounds(
+            if lo.isRef(defn.NothingClass) then lo else expand(lo, true),
+            expand(hi, true))
       }
     }
   }
@@ -3580,13 +3653,49 @@ object Types {
   /** The parameter of a type lambda */
   case class LambdaParam(tl: TypeLambda, n: Int) extends ParamInfo {
     type ThisName = TypeName
+
     def isTypeParam(implicit ctx: Context): Boolean = tl.paramNames.head.isTypeName
     def paramName(implicit ctx: Context): tl.ThisName = tl.paramNames(n)
     def paramInfo(implicit ctx: Context): tl.PInfo = tl.paramInfos(n)
     def paramInfoAsSeenFrom(pre: Type)(implicit ctx: Context): tl.PInfo = paramInfo
     def paramInfoOrCompleter(implicit ctx: Context): Type = paramInfo
-    def paramVariance(implicit ctx: Context): Int = tl.paramNames(n).variance
     def paramRef(implicit ctx: Context): Type = tl.paramRefs(n)
+
+    private var myVariance: FlagSet = UndefinedFlags
+
+    /** Low level setter, only called from Variances.setStructuralVariances */
+    def storedVariance_= (v: Variance): Unit =
+      myVariance = v
+
+    /** Low level getter, only called from Variances.setStructuralVariances */
+    def storedVariance: Variance =
+      myVariance
+
+    /** Set the declared variance of this parameter.
+     *  @pre the containing lambda is a isDeclaredVarianceLambda
+     */
+    def declaredVariance_=(v: Variance): Unit =
+      assert(tl.isDeclaredVarianceLambda)
+      assert(myVariance == UndefinedFlags)
+      myVariance = v
+
+    /** The declared variance of this parameter.
+     *  @pre the containing lambda is a isDeclaredVarianceLambda
+     */
+    def declaredVariance: Variance =
+      assert(tl.isDeclaredVarianceLambda)
+      assert(myVariance != UndefinedFlags)
+      myVariance
+
+    /** The declared or structural variance of this parameter. */
+    def paramVariance(implicit ctx: Context): Variance =
+      if myVariance == UndefinedFlags then
+        tl match
+          case tl: HKTypeLambda =>
+            setStructuralVariances(tl)
+          case _ =>
+            myVariance = Invariant
+      myVariance
   }
 
   /** A type application `C[T_1, ..., T_n]` */
@@ -3758,8 +3867,8 @@ object Types {
 
     override def computeHash(bs: Binders): Int = doHash(bs, tycon, args)
 
-    override def stableHash: Boolean = {
-      if (myStableHash == 0) myStableHash = if (tycon.stableHash && args.stableHash) 1 else -1
+    override def hashIsStable: Boolean = {
+      if (myStableHash == 0) myStableHash = if (tycon.hashIsStable && args.hashIsStable) 1 else -1
       myStableHash > 0
     }
 
@@ -3790,7 +3899,7 @@ object Types {
     type BT <: Type
     val binder: BT
     def copyBoundType(bt: BT): Type
-    override def stableHash: Boolean = false
+    override def hashIsStable: Boolean = false
   }
 
   abstract class ParamRef extends BoundType {
@@ -4193,7 +4302,7 @@ object Types {
       else ClassInfo(prefix, cls, classParents, decls, selfInfo)
 
     override def computeHash(bs: Binders): Int = doHash(bs, cls, prefix)
-    override def stableHash: Boolean = prefix.stableHash && classParents.stableHash
+    override def hashIsStable: Boolean = prefix.hashIsStable && classParents.hashIsStable
 
     override def eql(that: Type): Boolean = that match {
       case that: ClassInfo =>
@@ -4290,7 +4399,7 @@ object Types {
     }
 
     override def computeHash(bs: Binders): Int = doHash(bs, lo, hi)
-    override def stableHash: Boolean = lo.stableHash && hi.stableHash
+    override def hashIsStable: Boolean = lo.hashIsStable && hi.hashIsStable
 
     override def equals(that: Any): Boolean = equals(that, null)
 
@@ -4315,7 +4424,7 @@ object Types {
     def derivedAlias(alias: Type)(implicit ctx: Context): AliasingBounds
 
     override def computeHash(bs: Binders): Int = doHash(bs, alias)
-    override def stableHash: Boolean = alias.stableHash
+    override def hashIsStable: Boolean = alias.hashIsStable
 
     override def iso(that: Any, bs: BinderPairs): Boolean = that match {
       case that: AliasingBounds => this.isTypeAlias == that.isTypeAlias && alias.equals(that.alias, bs)
@@ -4416,7 +4525,7 @@ object Types {
       if (elemtp eq this.elemType) this else JavaArrayType(elemtp)
 
     override def computeHash(bs: Binders): Int = doHash(bs, elemType)
-    override def stableHash: Boolean = elemType.stableHash
+    override def hashIsStable: Boolean = elemType.hashIsStable
 
     override def eql(that: Type): Boolean = that match {
       case that: JavaArrayType => elemType.eq(that.elemType)
@@ -4479,7 +4588,7 @@ object Types {
       else WildcardType(optBounds.asInstanceOf[TypeBounds])
 
     override def computeHash(bs: Binders): Int = doHash(bs, optBounds)
-    override def stableHash: Boolean = optBounds.stableHash
+    override def hashIsStable: Boolean = optBounds.hashIsStable
 
     override def eql(that: Type): Boolean = that match {
       case that: WildcardType => optBounds.eq(that.optBounds)
@@ -4685,7 +4794,7 @@ object Types {
             case arg :: otherArgs if tparams.nonEmpty =>
               val arg1 = arg match {
                 case arg: TypeBounds => this(arg)
-                case arg => atVariance(variance * tparams.head.paramVariance)(this(arg))
+                case arg => atVariance(variance * tparams.head.paramVarianceSign)(this(arg))
               }
               val otherArgs1 = mapArgs(otherArgs, tparams.tail)
               if ((arg1 eq arg) && (otherArgs1 eq otherArgs)) args
@@ -4987,7 +5096,7 @@ object Types {
               // @return  operation succeeded for all arguments.
               def distributeArgs(args: List[Type], tparams: List[ParamInfo]): Boolean = args match {
                 case Range(lo, hi) :: args1 =>
-                  val v = tparams.head.paramVariance
+                  val v = tparams.head.paramVarianceSign
                   if (v == 0) false
                   else {
                     if (v > 0) { loBuf += lo; hiBuf += hi }
@@ -5105,7 +5214,7 @@ object Types {
             val tparam = tparams.head
             val acc = args.head match {
               case arg: TypeBounds => this(x, arg)
-              case arg => atVariance(variance * tparam.paramVariance)(this(x, arg))
+              case arg => atVariance(variance * tparam.paramVarianceSign)(this(x, arg))
             }
             foldArgs(acc, tparams.tail, args.tail)
           }
@@ -5386,8 +5495,8 @@ object Types {
   implicit def decorateTypeApplications(tpe: Type): TypeApplications = new TypeApplications(tpe)
 
   implicit class typeListDeco(val tps1: List[Type]) extends AnyVal {
-    @tailrec def stableHash: Boolean =
-      tps1.isEmpty || tps1.head.stableHash && tps1.tail.stableHash
+    @tailrec def hashIsStable: Boolean =
+      tps1.isEmpty || tps1.head.hashIsStable && tps1.tail.hashIsStable
     @tailrec def equalElements(tps2: List[Type], bs: BinderPairs): Boolean =
       (tps1 `eq` tps2) || {
         if (tps1.isEmpty) tps2.isEmpty
diff --git a/compiler/src/dotty/tools/dotc/typer/Variances.scala b/compiler/src/dotty/tools/dotc/core/Variances.scala
similarity index 63%
rename from compiler/src/dotty/tools/dotc/typer/Variances.scala
rename to compiler/src/dotty/tools/dotc/core/Variances.scala
index 98fdef09a9a4..127c4e6e9a8a 100644
--- a/compiler/src/dotty/tools/dotc/typer/Variances.scala
+++ b/compiler/src/dotty/tools/dotc/core/Variances.scala
@@ -1,8 +1,9 @@
 package dotty.tools.dotc
-package typer
+package core
 
-import core._
 import Types._, Contexts._, Flags._, Symbols._, Annotations._
+import TypeApplications.TypeParamInfo
+import Decorators._
 
 object Variances {
 
@@ -10,6 +11,16 @@ object Variances {
   val Bivariant: Variance = VarianceFlags
   val Invariant: Variance = EmptyFlags
 
+  def varianceFromInt(v: Int): Variance =
+    if v < 0 then Contravariant
+    else if v > 0 then Covariant
+    else Invariant
+
+  def varianceToInt(v: Variance): Int =
+    if v.is(Covariant) then 1
+    else if v.is(Contravariant) then -1
+    else 0
+
   /** Flip between covariant and contravariant */
   def flip(v: Variance): Variance =
     if (v == Covariant) Contravariant
@@ -82,7 +93,7 @@ object Variances {
         args match {
           case arg :: args1 =>
             varianceInArgs(
-              v & compose(varianceInType(arg)(tparam), tparams.head.paramVariance),
+              v & compose(varianceInType(arg)(tparam), tparams.head.paramVarianceSign),
               args1, tparams.tail)
           case nil =>
             v
@@ -98,12 +109,50 @@ object Variances {
       Bivariant
   }
 
-  def varianceString(v: Variance): String =
-    if (v is Covariant) "covariant"
-    else if (v is Contravariant) "contravariant"
-    else "invariant"
+  def setStructuralVariances(lam: HKTypeLambda)(implicit ctx: Context): Unit =
+    assert(!lam.isDeclaredVarianceLambda)
+    for param <- lam.typeParams do param.storedVariance = Bivariant
+    object narrowVariances extends TypeTraverser {
+      def traverse(t: Type): Unit = t match
+        case t: TypeParamRef if t.binder eq lam =>
+          lam.typeParams(t.paramNum).storedVariance &= varianceFromInt(variance)
+        case _ =>
+          traverseChildren(t)
+    }
+    // Note: Normally, we'd need to repeat `traverse` until a fixpoint is reached.
+    // But since recursive lambdas can only appear in bounds, and bounds never have
+    // structural variances, a single traversal is enough.
+    narrowVariances.traverse(lam.resType)
+
+  /** Does variance `v1` conform to variance `v2`?
+   *  This is the case if the variances are the same or `sym` is nonvariant.
+   */
+   def varianceConforms(v1: Int, v2: Int): Boolean =
+    v1 == v2 || v2 == 0
+
+  /** Does the variance of type parameter `tparam1` conform to the variance of type parameter `tparam2`?
+   */
+   def varianceConforms(tparam1: TypeParamInfo, tparam2: TypeParamInfo)(implicit ctx: Context): Boolean =
+    tparam1.paramVariance.isAllOf(tparam2.paramVariance)
+
+  /** Do the variances of type parameters `tparams1` conform to the variances
+   *  of corresponding type parameters `tparams2`?
+   *  This is only the case if `tparams1` and `tparams2` have the same length.
+   */
+  def variancesConform(tparams1: List[TypeParamInfo], tparams2: List[TypeParamInfo])(implicit ctx: Context): Boolean =
+    val needsDetailedCheck = tparams2 match
+      case (_: Symbol) :: _ => true
+      case LambdaParam(tl: HKTypeLambda, _) :: _ => tl.isDeclaredVarianceLambda
+      case _ => false
+    if needsDetailedCheck then tparams1.corresponds(tparams2)(varianceConforms)
+    else tparams1.hasSameLengthAs(tparams2)
+
+  def varianceSign(sym: Symbol)(implicit ctx: Context): String =
+    varianceSign(sym.variance)
+
+  def varianceSign(v: Variance): String = varianceSign(varianceToInt(v))
 
-  def varianceString(v: Int): String =
+  def varianceSign(v: Int): String =
     if (v > 0) "+"
     else if (v < 0) "-"
     else ""
diff --git a/compiler/src/dotty/tools/dotc/core/tasty/TastyUnpickler.scala b/compiler/src/dotty/tools/dotc/core/tasty/TastyUnpickler.scala
index bc40900b2fbb..fa00db183e0b 100644
--- a/compiler/src/dotty/tools/dotc/core/tasty/TastyUnpickler.scala
+++ b/compiler/src/dotty/tools/dotc/core/tasty/TastyUnpickler.scala
@@ -62,7 +62,7 @@ class TastyUnpickler(reader: TastyReader) {
         val originals = until(end)(readName())
         val original = if (originals.isEmpty) EmptyTermName else originals.head
         uniqueNameKindOfSeparator(separator)(original, num)
-      case DEFAULTGETTER | VARIANT =>
+      case DEFAULTGETTER =>
         numberedNameKindOfTag(tag)(readName(), readNat())
       case SIGNED =>
         val original = readName()
diff --git a/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala b/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala
index f4edb6c0057b..dde4c177b8a4 100644
--- a/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala
+++ b/compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala
@@ -134,6 +134,15 @@ class TreePickler(pickler: TastyPickler) {
       pickleType(c.symbolValue.termRef)
   }
 
+  def pickleVariances(tp: Type)(given Context): Unit = tp match
+    case tp: HKTypeLambda if tp.isDeclaredVarianceLambda =>
+      for v <- tp.declaredVariances do
+        writeByte(
+          if v.is(Covariant) then COVARIANT
+          else if v.is(Contravariant) then CONTRAVARIANT
+          else STABLE)
+    case _ =>
+
   def pickleType(tpe0: Type, richTypes: Boolean = false)(implicit ctx: Context): Unit = {
     val tpe = tpe0.stripTypeVar
     try {
@@ -229,12 +238,14 @@ class TreePickler(pickler: TastyPickler) {
     case tpe: RecType =>
       writeByte(RECtype)
       pickleType(tpe.parent)
-    case tpe: TypeAlias =>
-      writeByte(TYPEALIAS)
-      pickleType(tpe.alias, richTypes)
     case tpe: TypeBounds =>
       writeByte(TYPEBOUNDS)
-      withLength { pickleType(tpe.lo, richTypes); pickleType(tpe.hi, richTypes) }
+      withLength {
+        pickleType(tpe.lo, richTypes)
+        if !tpe.isInstanceOf[AliasingBounds] then
+          pickleType(tpe.hi, richTypes)
+        pickleVariances(tpe.hi)
+      }
     case tpe: AnnotatedType =>
       writeByte(ANNOTATEDtype)
       withLength { pickleType(tpe.parent, richTypes); pickleTree(tpe.annot.tree) }
diff --git a/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala b/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala
index 40447a4bbc81..cf4826ba2877 100644
--- a/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala
+++ b/compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala
@@ -16,6 +16,7 @@ import Flags._
 import Constants._
 import Annotations._
 import NameKinds._
+import Variances.Invariant
 import typer.ConstFold
 import typer.Checking.checkNonCyclic
 import util.Spans._
@@ -303,6 +304,17 @@ class TreeUnpickler(reader: TastyReader,
           result.asInstanceOf[LT]
         }
 
+        def readVariances(tp: Type): Type = tp match
+          case tp: HKTypeLambda if currentAddr != end =>
+            val vs = until(end) {
+              readByte() match
+                case STABLE => Invariant
+                case COVARIANT => Covariant
+                case CONTRAVARIANT => Contravariant
+            }
+            tp.withVariances(vs)
+          case _ => tp
+
         val result =
           (tag: @switch) match {
             case TERMREFin =>
@@ -326,8 +338,7 @@ class TreeUnpickler(reader: TastyReader,
             case REFINEDtype =>
               var name: Name = readName()
               val parent = readType()
-              val ttag = nextUnsharedTag
-              if (ttag == TYPEBOUNDS || ttag == TYPEALIAS) name = name.toTypeName
+              if nextUnsharedTag == TYPEBOUNDS then name = name.toTypeName
               RefinedType(parent, name, readType())
                 // Note that the lambda "rt => ..." is not equivalent to a wildcard closure!
                 // Eta expansion of the latter puts readType() out of the expression.
@@ -335,9 +346,10 @@ class TreeUnpickler(reader: TastyReader,
               readType().appliedTo(until(end)(readType()))
             case TYPEBOUNDS =>
               val lo = readType()
-              val hi = readType()
-              if (lo.isMatch && (lo `eq` hi)) MatchAlias(lo)
-              else TypeBounds(lo, hi)
+              if nothingButMods(end) then
+                if lo.isMatch then MatchAlias(readVariances(lo))
+                else TypeAlias(readVariances(lo))
+              else TypeBounds(lo, readVariances(readType()))
             case ANNOTATEDtype =>
               AnnotatedType(readType(), Annotation(readTerm()))
             case ANDtype =>
@@ -404,8 +416,6 @@ class TreeUnpickler(reader: TastyReader,
           }
         case RECthis =>
           readTypeRef().asInstanceOf[RecType].recThis
-        case TYPEALIAS =>
-          TypeAlias(readType())
         case SHAREDtype =>
           val ref = readAddr()
           typeAtAddr.getOrElseUpdate(ref, forkAt(ref).readType())
@@ -506,10 +516,7 @@ class TreeUnpickler(reader: TastyReader,
       val tag = readByte()
       val end = readEnd()
       var name: Name = readName()
-      nextUnsharedTag match {
-        case TYPEBOUNDS | TYPEALIAS => name = name.toTypeName
-        case _ =>
-      }
+      if nextUnsharedTag == TYPEBOUNDS then name = name.toTypeName
       val typeReader = fork
       val completer = new LazyType {
         def complete(denot: SymDenotation)(implicit ctx: Context) =
diff --git a/compiler/src/dotty/tools/dotc/core/unpickleScala2/Scala2Unpickler.scala b/compiler/src/dotty/tools/dotc/core/unpickleScala2/Scala2Unpickler.scala
index 4bfcd1b5236d..a2dd991c50b6 100644
--- a/compiler/src/dotty/tools/dotc/core/unpickleScala2/Scala2Unpickler.scala
+++ b/compiler/src/dotty/tools/dotc/core/unpickleScala2/Scala2Unpickler.scala
@@ -69,8 +69,8 @@ object Scala2Unpickler {
       assert(lastArg isRef defn.ArrayClass)
       val elemtp0 :: Nil = lastArg.baseType(defn.ArrayClass).argInfos
       val elemtp = elemtp0 match {
-        case AndType(t1, t2) => // drop intersection with Object for abstract types an parameters in varargs. Erasure can handle them.
-          if (t2.isRef(defn.ObjectClass))
+        case AndType(t1, t2) => // drop intersection with Object for abstract types and parameters in varargs. Erasure can handle them.
+          if t2.isAnyRef then
             t1 match {
               case t1: TypeParamRef => t1
               case t1: TypeRef if t1.symbol.isAbstractOrParamType => t1
diff --git a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
index 0e984154c0cb..70186f9a6efe 100644
--- a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
+++ b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala
@@ -2845,19 +2845,25 @@ object Parsers {
      *  HkTypeParam       ::=  {Annotation} [‘+’ | ‘-’] (id [HkTypePamClause] | ‘_’) TypeBounds
      */
     def typeParamClause(ownerKind: ParamOwner.Value): List[TypeDef] = inBrackets {
+
+      def variance(vflag: FlagSet): FlagSet =
+        if ownerKind == ParamOwner.Def || ownerKind == ParamOwner.TypeParam then
+          syntaxError(i"no `+/-` variance annotation allowed here")
+          in.nextToken()
+          EmptyFlags
+        else
+          in.nextToken()
+          vflag
+
       def typeParam(): TypeDef = {
         val isAbstractOwner = ownerKind == ParamOwner.Type || ownerKind == ParamOwner.TypeParam
         val start = in.offset
         val mods =
-          annotsAsMods() | {
-            if (ownerKind == ParamOwner.Class) Param | PrivateLocal
-            else Param
-          } | {
-            if (ownerKind == ParamOwner.Def) EmptyFlags
-            else if (isIdent(nme.raw.PLUS)) { in.nextToken(); Covariant }
-            else if (isIdent(nme.raw.MINUS)) { in.nextToken(); Contravariant }
-            else EmptyFlags
-          }
+          annotsAsMods()
+          | (if (ownerKind == ParamOwner.Class) Param | PrivateLocal else Param)
+          | (if isIdent(nme.raw.PLUS) then variance(Covariant)
+             else if isIdent(nme.raw.MINUS) then variance(Contravariant)
+             else EmptyFlags)
         atSpan(start, nameStart) {
           val name =
             if (isAbstractOwner && in.token == USCORE) {
@@ -2865,7 +2871,7 @@ object Parsers {
               WildcardParamName.fresh().toTypeName
             }
             else ident().toTypeName
-          val hkparams = typeParamClauseOpt(ParamOwner.TypeParam)
+          val hkparams = typeParamClauseOpt(ParamOwner.Type)
           val bounds = if (isAbstractOwner) typeBounds() else typeParamBounds(name)
           TypeDef(name, lambdaAbstract(hkparams, bounds)).withMods(mods)
         }
diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
index 0f5ba5d027d6..98d9358f8953 100644
--- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
@@ -8,6 +8,7 @@ import StdNames.nme
 import ast.Trees._
 import typer.Implicits._
 import typer.ImportInfo
+import Variances.varianceSign
 import util.SourcePosition
 import java.lang.Integer.toOctalString
 import config.Config.summarizeDepth
@@ -174,7 +175,7 @@ class PlainPrinter(_ctx: Context) extends Printer {
           def casesText = Text(cases.map(caseText), "\n")
             atPrec(InfixPrec) { toText(scrutinee) } ~
             keywordStr(" match ") ~ "{" ~ casesText ~ "}" ~
-            (" <: " ~ toText(bound) provided !bound.isRef(defn.AnyClass))
+            (" <: " ~ toText(bound) provided !bound.isAny)
         }.close
       case tp: ErrorType =>
         s"<error ${tp.msg.msg}>"
@@ -326,14 +327,39 @@ class PlainPrinter(_ctx: Context) extends Printer {
     case None => "?"
   }
 
+  protected def decomposeLambdas(bounds: TypeBounds): (String, TypeBounds) =
+    def decompose(tp: Type) = tp.stripTypeVar match
+      case lam: HKTypeLambda =>
+        val names =
+          if lam.isDeclaredVarianceLambda then
+            lam.paramNames.lazyZip(lam.declaredVariances).map((name, v) =>
+              varianceSign(v) + name)
+          else lam.paramNames
+        (names.mkString("[", ", ", "]"), lam.resType)
+      case _ =>
+        ("", tp)
+    bounds match
+      case bounds: AliasingBounds =>
+        val (tparamStr, aliasRhs) = decompose(bounds.alias)
+        (tparamStr, bounds.derivedAlias(aliasRhs))
+      case TypeBounds(lo, hi) =>
+        val (_, loRhs) = decompose(lo)
+        val (tparamStr, hiRhs) = decompose(hi)
+        (tparamStr, bounds.derivedTypeBounds(loRhs, hiRhs))
+  end decomposeLambdas
+
   /** String representation of a definition's type following its name */
   protected def toTextRHS(tp: Type): Text = controlled {
     homogenize(tp) match {
-      case tp: AliasingBounds =>
-        " = " ~ toText(tp.alias)
-      case tp @ TypeBounds(lo, hi) =>
-        (if (lo isRef defn.NothingClass) Text() else " >: " ~ toText(lo)) ~
-          (if (hi isRef defn.AnyClass) Text() else " <: " ~ toText(hi))
+      case tp: TypeBounds =>
+        val (tparamStr, rhs) = decomposeLambdas(tp)
+        val binder = rhs match
+          case tp: AliasingBounds =>
+            " = " ~ toText(tp.alias)
+          case TypeBounds(lo, hi) =>
+            (if (lo isRef defn.NothingClass) Text() else " >: " ~ toText(lo))
+            ~ (if hi.isAny then Text() else " <: " ~ toText(hi))
+        tparamStr ~ binder
       case tp @ ClassInfo(pre, cls, cparents, decls, selfInfo) =>
         val preText = toTextLocal(pre)
         val (tparams, otherDecls) = decls.toList partition treatAsTypeParam
@@ -415,15 +441,6 @@ class PlainPrinter(_ctx: Context) extends Printer {
   protected def toTextFlags(sym: Symbol, flags: FlagSet): Text =
     Text(flags.flagStrings(privateWithinString(sym)).map(flag => stringToText(keywordStr(flag))), " ")
 
-  /** String representation of symbol's variance or "" if not applicable */
-  protected def varianceString(sym: Symbol): String = varianceString(sym.variance)
-
-  protected def varianceString(v: Int): String = v match {
-    case -1 => "-"
-    case 1 => "+"
-    case _ => ""
-  }
-
   def annotsText(sym: Symbol): Text = Text(sym.annotations.map(toText))
 
   def dclText(sym: Symbol): Text = dclTextWithInfo(sym, sym.unforcedInfo)
@@ -432,7 +449,7 @@ class PlainPrinter(_ctx: Context) extends Printer {
 
   private def dclTextWithInfo(sym: Symbol, info: Option[Type]): Text =
     (toTextFlags(sym) ~~ keyString(sym) ~~
-      (varianceString(sym) ~ nameString(sym)) ~ toTextRHS(info)).close
+      (varianceSign(sym.variance) ~ nameString(sym)) ~ toTextRHS(info)).close
 
   def toText(sym: Symbol): Text =
     (kindString(sym) ~~ {
diff --git a/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala b/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala
index 512d870005d4..1f4a2dbc9be3 100644
--- a/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala
@@ -882,7 +882,7 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
     if (tree.exists(!_.isEmpty)) encl(blockText(tree)) else ""
 
   override protected def ParamRefNameString(name: Name): String =
-    name.invariantName.toString
+    name.toString
 
   override protected def treatAsTypeParam(sym: Symbol): Boolean = sym.is(TypeParam)
 
diff --git a/compiler/src/dotty/tools/dotc/sbt/ExtractAPI.scala b/compiler/src/dotty/tools/dotc/sbt/ExtractAPI.scala
index e17acc7ccc73..0af442b2c089 100644
--- a/compiler/src/dotty/tools/dotc/sbt/ExtractAPI.scala
+++ b/compiler/src/dotty/tools/dotc/sbt/ExtractAPI.scala
@@ -545,7 +545,7 @@ private class ExtractAPICollector(implicit val ctx: Context) extends ThunkHolder
   }
 
   def apiTypeParameter(tparam: ParamInfo): api.TypeParameter =
-    apiTypeParameter(tparam.paramName.toString, tparam.paramVariance,
+    apiTypeParameter(tparam.paramName.toString, tparam.paramVarianceSign,
       tparam.paramInfo.bounds.lo, tparam.paramInfo.bounds.hi)
 
   def apiTypeParameter(name: String, variance: Int, lo: Type, hi: Type): api.TypeParameter =
diff --git a/compiler/src/dotty/tools/dotc/transform/Erasure.scala b/compiler/src/dotty/tools/dotc/transform/Erasure.scala
index 545d3b86784e..7c882040cdd7 100644
--- a/compiler/src/dotty/tools/dotc/transform/Erasure.scala
+++ b/compiler/src/dotty/tools/dotc/transform/Erasure.scala
@@ -460,9 +460,9 @@ object Erasure {
         untpd.cpy.Select(tree)(qual, sym.name).withType(NamedType(qual.tpe, sym))
 
       def selectArrayMember(qual: Tree, erasedPre: Type): Tree =
-        if (erasedPre isRef defn.ObjectClass)
+        if erasedPre.isAnyRef then
           runtimeCallWithProtoArgs(tree.name.genericArrayOp, pt, qual)
-        else if (!(qual.tpe <:< erasedPre))
+        else if !(qual.tpe <:< erasedPre) then
           selectArrayMember(cast(qual, erasedPre), erasedPre)
         else
           assignType(untpd.cpy.Select(tree)(qual, tree.name.primitiveArrayOp), qual)
diff --git a/compiler/src/dotty/tools/dotc/transform/FullParameterization.scala b/compiler/src/dotty/tools/dotc/transform/FullParameterization.scala
index 7a5ca8a5ee5f..be4bb6d0b346 100644
--- a/compiler/src/dotty/tools/dotc/transform/FullParameterization.scala
+++ b/compiler/src/dotty/tools/dotc/transform/FullParameterization.scala
@@ -98,7 +98,6 @@ trait FullParameterization {
     }
     val ctparams = if (abstractOverClass) clazz.typeParams else Nil
     val ctnames = ctparams.map(_.name)
-    val ctvariances = ctparams.map(_.variance)
 
     /** The method result type */
     def resultType(mapClassParams: Type => Type) = {
diff --git a/compiler/src/dotty/tools/dotc/transform/PostTyper.scala b/compiler/src/dotty/tools/dotc/transform/PostTyper.scala
index 52975976f2fe..70095a2812d5 100644
--- a/compiler/src/dotty/tools/dotc/transform/PostTyper.scala
+++ b/compiler/src/dotty/tools/dotc/transform/PostTyper.scala
@@ -250,6 +250,10 @@ class PostTyper extends MacroTransform with IdentityDenotTransformer { thisPhase
                && sym != defn.SourceFileAnnot
             then
               sym.addAnnotation(Annotation.makeSourceFile(ctx.compilationUnit.source.file.path))
+          else (tree.rhs, sym.info) match
+            case (rhs: LambdaTypeTree, bounds: TypeBounds) =>
+              VarianceChecker.checkLambda(rhs, bounds)
+            case _ =>
           processMemberDef(super.transform(tree))
         case tree: New if isCheckable(tree) =>
           Checking.checkInstantiable(tree.tpe, tree.posd)
@@ -279,9 +283,6 @@ class PostTyper extends MacroTransform with IdentityDenotTransformer { thisPhase
               case tpe => tpe
             }
           )
-        case tree: LambdaTypeTree =>
-          VarianceChecker.checkLambda(tree)
-          super.transform(tree)
         case Import(expr, selectors) =>
           val exprTpe = expr.tpe
           val seen = mutable.Set.empty[Name]
diff --git a/compiler/src/dotty/tools/dotc/typer/Applications.scala b/compiler/src/dotty/tools/dotc/typer/Applications.scala
index 50a39174de0b..703c0831fcd6 100644
--- a/compiler/src/dotty/tools/dotc/typer/Applications.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Applications.scala
@@ -1394,7 +1394,7 @@ trait Applications extends Compatibility {
           def apply(t: Type) = t match {
             case t @ AppliedType(tycon, args) =>
               def mapArg(arg: Type, tparam: TypeParamInfo) =
-                if (variance > 0 && tparam.paramVariance < 0) defn.FunctionOf(arg :: Nil, defn.UnitType)
+                if (variance > 0 && tparam.paramVarianceSign < 0) defn.FunctionOf(arg :: Nil, defn.UnitType)
                 else arg
               mapOver(t.derivedAppliedType(tycon, args.zipWithConserve(tycon.typeParams)(mapArg)))
             case _ => mapOver(t)
diff --git a/compiler/src/dotty/tools/dotc/typer/ErrorReporting.scala b/compiler/src/dotty/tools/dotc/typer/ErrorReporting.scala
index 8ff7e0c26697..f4a58ec542ac 100644
--- a/compiler/src/dotty/tools/dotc/typer/ErrorReporting.scala
+++ b/compiler/src/dotty/tools/dotc/typer/ErrorReporting.scala
@@ -152,9 +152,9 @@ object ErrorReporting {
         if (found1 frozen_<:< expected1) (found, expected) else (found1, expected1)
       val postScript1 =
         if !postScript.isEmpty
-           || expected.isRef(defn.AnyClass)
+           || expected.isAny
+           || expected.isAnyRef
            || expected.isRef(defn.AnyValClass)
-           || expected.isRef(defn.ObjectClass)
            || defn.isBottomType(found)
         then postScript
         else ctx.typer.importSuggestionAddendum(ViewProto(found.widen, expected))
diff --git a/compiler/src/dotty/tools/dotc/typer/Implicits.scala b/compiler/src/dotty/tools/dotc/typer/Implicits.scala
index 538c3fe6d699..f30c3872cd8e 100644
--- a/compiler/src/dotty/tools/dotc/typer/Implicits.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Implicits.scala
@@ -662,14 +662,15 @@ trait Implicits { self: Typer =>
    */
   def inferView(from: Tree, to: Type)(implicit ctx: Context): SearchResult = {
     record("inferView")
-    if    ((to isRef defn.AnyClass)
-        || (to isRef defn.ObjectClass)
-        || (to isRef defn.UnitClass)
-        || (from.tpe isRef defn.NothingClass)
-        || (from.tpe isRef defn.NullClass)
-        || !(ctx.mode is Mode.ImplicitsEnabled)
-        || from.isInstanceOf[Super]
-        || (from.tpe eq NoPrefix)) NoMatchingImplicitsFailure
+    if    to.isAny
+       || to.isAnyRef
+       || to.isRef(defn.UnitClass)
+       || from.tpe.isRef(defn.NothingClass)
+       || from.tpe.isRef(defn.NullClass)
+       || !ctx.mode.is(Mode.ImplicitsEnabled)
+       || from.isInstanceOf[Super]
+       || (from.tpe eq NoPrefix)
+    then NoMatchingImplicitsFailure
     else {
       def adjust(to: Type) = to.stripTypeVar.widenExpr match {
         case SelectionProto(name, memberProto, compat, true) =>
@@ -1032,7 +1033,7 @@ trait Implicits { self: Typer =>
                           }
                           resType <:< target
                           val tparams = poly.paramRefs
-                          val variances = caseClass.typeParams.map(_.paramVariance)
+                          val variances = caseClass.typeParams.map(_.paramVarianceSign)
                           val instanceTypes = tparams.lazyZip(variances).map((tparam, variance) =>
                             ctx.typeComparer.instanceType(tparam, fromBelow = variance < 0))
                           resType.substParams(poly, instanceTypes)
diff --git a/compiler/src/dotty/tools/dotc/typer/Namer.scala b/compiler/src/dotty/tools/dotc/typer/Namer.scala
index fbc65fa6871c..a57c5b39a244 100644
--- a/compiler/src/dotty/tools/dotc/typer/Namer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Namer.scala
@@ -1505,7 +1505,7 @@ class Namer { typer: Typer =>
   }
 
   def typeDefSig(tdef: TypeDef, sym: Symbol, tparamSyms: List[TypeSymbol])(implicit ctx: Context): Type = {
-    def abstracted(tp: Type): Type = HKTypeLambda.fromParams(tparamSyms, tp)
+    def abstracted(tp: TypeBounds): TypeBounds = HKTypeLambda.boundsFromParams(tparamSyms, tp)
     val dummyInfo1 = abstracted(TypeBounds.empty)
     sym.info = dummyInfo1
     sym.setFlag(Provisional)
@@ -1535,9 +1535,8 @@ class Namer { typer: Typer =>
     }
     sym.info = dummyInfo2
 
-    val rhsBodyType = typedAheadType(rhs).tpe
-    val rhsType = if (isDerived) rhsBodyType else abstracted(rhsBodyType)
-    val unsafeInfo = rhsType.toBounds
+    val rhsBodyType: TypeBounds = typedAheadType(rhs).tpe.toBounds
+    val unsafeInfo = if (isDerived) rhsBodyType else abstracted(rhsBodyType)
     if (isDerived) sym.info = unsafeInfo
     else {
       sym.info = NoCompleter
diff --git a/compiler/src/dotty/tools/dotc/typer/QuotesAndSplices.scala b/compiler/src/dotty/tools/dotc/typer/QuotesAndSplices.scala
index 73803a46d9f1..37532d2a9c22 100644
--- a/compiler/src/dotty/tools/dotc/typer/QuotesAndSplices.scala
+++ b/compiler/src/dotty/tools/dotc/typer/QuotesAndSplices.scala
@@ -218,7 +218,7 @@ trait QuotesAndSplices {
         case tdef: TypeDef if tdef.symbol.hasAnnotation(defn.InternalQuoted_patternBindHoleAnnot) =>
           transformTypeBindingTypeDef(tdef, typePatBuf)
         case tree @ AppliedTypeTree(tpt, args) =>
-            val args1: List[Tree] = args.zipWithConserve(tpt.tpe.typeParams.map(_.paramVariance)) { (arg, v) =>
+            val args1: List[Tree] = args.zipWithConserve(tpt.tpe.typeParams.map(_.paramVarianceSign)) { (arg, v) =>
               arg.tpe match {
                 case _: TypeBounds => transform(arg)
                 case _ => atVariance(variance * v)(transform(arg))
diff --git a/compiler/src/dotty/tools/dotc/typer/RefChecks.scala b/compiler/src/dotty/tools/dotc/typer/RefChecks.scala
index b65942013cb3..a5315400efb1 100644
--- a/compiler/src/dotty/tools/dotc/typer/RefChecks.scala
+++ b/compiler/src/dotty/tools/dotc/typer/RefChecks.scala
@@ -667,7 +667,7 @@ object RefChecks {
       def checkCaseClassInheritanceInvariant() =
         for (caseCls <- clazz.info.baseClasses.tail.find(_.is(Case)))
           for (baseCls <- caseCls.info.baseClasses.tail)
-            if (baseCls.typeParams.exists(_.paramVariance != 0))
+            if (baseCls.typeParams.exists(_.paramVarianceSign != 0))
               for (problem <- variantInheritanceProblems(baseCls, caseCls, "non-variant", "case "))
                 ctx.errorOrMigrationWarning(problem(), clazz.sourcePos)
       checkNoAbstractMembers()
diff --git a/compiler/src/dotty/tools/dotc/typer/VarianceChecker.scala b/compiler/src/dotty/tools/dotc/typer/VarianceChecker.scala
index 9258db7839b3..7f2e59b93e6d 100644
--- a/compiler/src/dotty/tools/dotc/typer/VarianceChecker.scala
+++ b/compiler/src/dotty/tools/dotc/typer/VarianceChecker.scala
@@ -7,7 +7,6 @@ import Types._, Contexts._, Flags._, Symbols._, Trees._
 import Decorators._
 import Variances._
 import NameKinds._
-import TypeApplications.varianceConforms
 import util.Spans._
 import util.SourcePosition
 import config.Printers.variances
@@ -26,54 +25,51 @@ object VarianceChecker {
    *  Note: this is achieved by a mechanism separate from checking class type parameters.
    *  Question: Can the two mechanisms be combined in one?
    */
-  def checkLambda(tree: tpd.LambdaTypeTree)(implicit ctx: Context): Unit = {
-    def checkType(tl: HKTypeLambda): Unit = {
-      val checkOK = new TypeAccumulator[Boolean] {
-        def error(tref: TypeParamRef) = {
-          val VariantName(paramName, v) = tl.paramNames(tref.paramNum).toTermName
-          val paramVarianceStr = if (v == 0) "contra" else "co"
-          val occursStr = variance match {
-            case -1 => "contra"
-            case 0 => "in"
-            case 1 => "co"
+  def checkLambda(tree: tpd.LambdaTypeTree, bounds: TypeBounds)(implicit ctx: Context): Unit =
+    def checkType(tpe: Type): Unit = tpe match
+      case tl: HKTypeLambda if tl.isDeclaredVarianceLambda =>
+        val checkOK = new TypeAccumulator[Boolean] {
+          def paramVarianceSign(tref: TypeParamRef) =
+            tl.typeParams(tref.paramNum).paramVarianceSign
+          def error(tref: TypeParamRef) = {
+            val paramName = tl.paramNames(tref.paramNum).toTermName
+            val v = paramVarianceSign(tref)
+            val paramVarianceStr = if (v < 0) "contra" else "co"
+            val occursStr = variance match {
+              case -1 => "contra"
+              case 0 => "in"
+              case 1 => "co"
+            }
+            val pos = tree.tparams
+              .find(_.name.toTermName == paramName)
+              .map(_.sourcePos)
+              .getOrElse(tree.sourcePos)
+            ctx.error(em"${paramVarianceStr}variant type parameter $paramName occurs in ${occursStr}variant position in ${tl.resType}", pos)
           }
-          val pos = tree.tparams
-            .find(_.name.toTermName == paramName)
-            .map(_.sourcePos)
-            .getOrElse(tree.sourcePos)
-          ctx.error(em"${paramVarianceStr}variant type parameter $paramName occurs in ${occursStr}variant position in ${tl.resType}", pos)
-        }
-        def apply(x: Boolean, t: Type) = x && {
-          t match {
-            case tref: TypeParamRef if tref.binder `eq` tl =>
-              val v = tl.typeParams(tref.paramNum).paramVariance
-              varianceConforms(variance, v) || { error(tref); false }
-            case AnnotatedType(_, annot) if annot.symbol == defn.UncheckedVarianceAnnot =>
-              x
-            case _ =>
-              foldOver(x, t)
+          def apply(x: Boolean, t: Type) = x && {
+            t match {
+              case tref: TypeParamRef if tref.binder `eq` tl =>
+                varianceConforms(variance, paramVarianceSign(tref))
+                || { error(tref); false }
+              case AnnotatedType(_, annot) if annot.symbol == defn.UncheckedVarianceAnnot =>
+                x
+              case _ =>
+                foldOver(x, t)
+            }
           }
         }
-      }
-      checkOK.apply(true, tl.resType)
-    }
+        checkOK(true, tl.resType)
+      case _ =>
+    end checkType
 
-    (tree.tpe: @unchecked) match {
-      case tl: HKTypeLambda =>
-        checkType(tl)
-      // The type of a LambdaTypeTree can be a TypeBounds, see the documentation
-      // of `LambdaTypeTree`.
-      case TypeBounds(lo, hi: HKTypeLambda) =>
-        // Can't assume that the lower bound is a type lambda, it could also be
-        // a reference to `Nothing`.
-        lo match {
-          case lo: HKTypeLambda =>
-            checkType(lo)
-          case _ =>
-        }
-        checkType(hi)
-    }
-  }
+    checkType(bounds.lo)
+    checkType(bounds.hi)
+  end checkLambda
+
+  private def varianceLabel(v: Variance): String =
+    if (v is Covariant) "covariant"
+    else if (v is Contravariant) "contravariant"
+    else "invariant"
 }
 
 class VarianceChecker()(implicit ctx: Context) {
@@ -117,10 +113,10 @@ class VarianceChecker()(implicit ctx: Context) {
       if (relative == Bivariant) None
       else {
         val required = compose(relative, this.variance)
-        def tvar_s = s"$tvar (${varianceString(tvar.flags)} ${tvar.showLocated})"
+        def tvar_s = s"$tvar (${varianceLabel(tvar.flags)} ${tvar.showLocated})"
         def base_s = s"$base in ${base.owner}" + (if (base.owner.isClass) "" else " in " + base.owner.enclosingClass)
-        ctx.log(s"verifying $tvar_s is ${varianceString(required)} at $base_s")
-        ctx.log(s"relative variance: ${varianceString(relative)}")
+        ctx.log(s"verifying $tvar_s is ${varianceLabel(required)} at $base_s")
+        ctx.log(s"relative variance: ${varianceLabel(relative)}")
         ctx.log(s"current variance: ${this.variance}")
         ctx.log(s"owner chain: ${base.ownersIterator.toList}")
         if (tvar.isOneOf(required)) None
@@ -138,7 +134,7 @@ class VarianceChecker()(implicit ctx: Context) {
         else tp.normalized match {
           case tp: TypeRef =>
             val sym = tp.symbol
-            if (sym.variance != 0 && base.isContainedIn(sym.owner)) checkVarianceOfSymbol(sym)
+            if (sym.isOneOf(VarianceFlags) && base.isContainedIn(sym.owner)) checkVarianceOfSymbol(sym)
             else sym.info match {
               case MatchAlias(_) => foldOver(status, tp)
               case TypeAlias(alias) => this(status, alias)
@@ -169,7 +165,7 @@ class VarianceChecker()(implicit ctx: Context) {
   private object Traverser extends TreeTraverser {
     def checkVariance(sym: Symbol, pos: SourcePosition) = Validator.validateDefinition(sym) match {
       case Some(VarianceError(tvar, required)) =>
-        def msg = i"${varianceString(tvar.flags)} $tvar occurs in ${varianceString(required)} position in type ${sym.info} of $sym"
+        def msg = i"${varianceLabel(tvar.flags)} $tvar occurs in ${varianceLabel(required)} position in type ${sym.info} of $sym"
         if (ctx.scala2CompatMode &&
             (sym.owner.isConstructor || sym.ownersIterator.exists(_.isAllOf(ProtectedLocal))))
           ctx.migrationWarning(
diff --git a/compiler/test-resources/repl/i6474 b/compiler/test-resources/repl/i6474
index da2763c07502..8b11b42859cf 100644
--- a/compiler/test-resources/repl/i6474
+++ b/compiler/test-resources/repl/i6474
@@ -1,8 +1,8 @@
 scala> object Foo1 { type T[+A] = (A, Int) }
 // defined object Foo1
-scala> object Foo2 { type T[+A] = [+B] =>> (A, B) }
+scala> object Foo2 { type T[+A] = [B] =>> (A, B) }
 // defined object Foo2
-scala> object Foo3 { type T[+A] = [+B] =>> [C] =>> (A, B) }
+scala> object Foo3 { type T[+A] = [B] =>> [C] =>> (A, B) }
 // defined object Foo3
 scala> ((1, 2): Foo1.T[Int]): Foo1.T[Any]
 val res0: (Any, Int) = (1,2)
diff --git a/compiler/test-resources/type-printer/hkAlias b/compiler/test-resources/type-printer/hkAlias
index 14ee45b5a695..04e9a6c77d44 100644
--- a/compiler/test-resources/type-printer/hkAlias
+++ b/compiler/test-resources/type-printer/hkAlias
@@ -1,5 +1,5 @@
 scala> type Identity[T] = T
-// defined alias type Identity = [T] => T
+// defined alias type Identity[T] = T
 scala> def foo[T](x: T): Identity[T] = x
 def foo[T](x: T): Identity[T]
 scala> foo(1)
diff --git a/docs/docs/internals/syntax.md b/docs/docs/internals/syntax.md
index d0e5d9a313cc..9a026cb34d05 100644
--- a/docs/docs/internals/syntax.md
+++ b/docs/docs/internals/syntax.md
@@ -295,7 +295,7 @@ TypTypeParamClause::=  ‘[’ TypTypeParam {‘,’ TypTypeParam} ‘]’
 TypTypeParam      ::=  {Annotation} id [HkTypeParamClause] SubtypeBounds
 
 HkTypeParamClause ::=  ‘[’ HkTypeParam {‘,’ HkTypeParam} ‘]’
-HkTypeParam       ::=  {Annotation} [‘+’ | ‘-’] (Id[HkTypeParamClause] | ‘_’)
+HkTypeParam       ::=  {Annotation} [‘+’ | ‘-’] (id [HkTypeParamClause] | ‘_’)
                        SubtypeBounds
 
 ClsParamClauses   ::=  {ClsParamClause} [[nl] ‘(’ [‘implicit’] ClsParams ‘)’]
diff --git a/docs/docs/reference/new-types/type-lambdas-spec.md b/docs/docs/reference/new-types/type-lambdas-spec.md
index 905d0a75a622..78ce94ee6356 100644
--- a/docs/docs/reference/new-types/type-lambdas-spec.md
+++ b/docs/docs/reference/new-types/type-lambdas-spec.md
@@ -6,9 +6,9 @@ title: "Type Lambdas - More Details"
 ## Syntax
 
 ```
-Type              ::=  ... |  HkTypeParamClause ‘=>>’ Type
-HkTypeParamClause ::=  ‘[’ HkTypeParam {‘,’ HkTypeParam} ‘]’
-HkTypeParam       ::=  {Annotation} [‘+’ | ‘-’] (Id[HkTypeParamClause] | ‘_’) TypeBounds
+Type            ::=  ... |  TypeParamClause ‘=>>’ Type
+TypeParamClause ::=  ‘[’ TypeParam {‘,’ TypeParam} ‘]’
+TypeParam       ::=  {Annotation} (id [HkTypeParamClause] | ‘_’) TypeBounds
 TypeBounds        ::=  [‘>:’ Type] [‘<:’ Type]
 ```
 
@@ -18,41 +18,23 @@ A type lambda such as `[X] =>> F[X]` defines a function from types to types. The
 If a parameter is bounded, as in `[X >: L <: H] =>> F[X]` it is checked that arguments to the parameters conform to the bounds `L` and `H`.
 Only the upper bound `H` can be F-bounded, i.e. `X` can appear in it.
 
-A variance annotation on a parameter indicates a subtyping relationship on type instances. For instance, given
-```scala
-type TL1 = [+A] =>> F[A]
-type TL2 = [-A] =>> F[A]
-```
-and two types `S <: T`, we have
-```scala
-TL1[S] <: TL1[T]
-TL2[T] <: TL2[S]
-```
-It is checked that variance annotations on parameters of type lambdas are respected by the parameter occurrences on the type lambda's body.
-
-**Note** No requirements hold for the variances of occurrences of type variables in their bounds. It is an open question whether we need to impose additional requirements here
-(`scalac` doesn't check variances in bounds either).
-
 ## Subtyping Rules
 
 Assume two type lambdas
 ```scala
-type TL1  =  [v1 X >: L1 <: U1] =>> R1
-type TL2  =  [v2 X >: L2 <: U2] =>> R2
+type TL1  =  [X >: L1 <: U1] =>> R1
+type TL2  =  [X >: L2 <: U2] =>> R2
 ```
-where `v1` and `v2` are optional variance annotations: `+`, `-`, or absent.
 Then `TL1 <: TL2`, if
 
  - the type interval `L2..U2` is contained in the type interval `L1..U1` (i.e.
 `L1 <: L2` and `U2 <: U1`),
- - either `v2` is absent or `v1 = v2`
  - `R1 <: R2`
 
 Here we have relied on alpha renaming to bring match the two bound types `X`.
 
 A partially applied type constructor such as `List` is assumed to be equivalent to
-its eta expansion. I.e, `List = [+X] =>> List[X]`. This allows type constructors
-to be compared with type lambdas.
+its eta expansion. I.e, `List = [X] =>> List[X]`. This allows type constructors to be compared with type lambdas.
 
 ## Relationship with Parameterized Type Definitions
 
@@ -64,6 +46,17 @@ is regarded as a shorthand for an unparameterized definition with a type lambda
 ```scala
 type T = [X] =>> R
 ```
+If the a type definition carries `+` or `-` variance annotations,
+it is checked that the variance annotations are satisfied by the type lambda.
+For instance,
+```scala
+type F2[A, +B] = A => B
+```
+expands to
+```scala
+type F2 = [A, B] =>> A => B
+```
+and at the same time it is checked that the parameter `B` appears covariantly in `A => B`.
 
 A parameterized abstract type
 ```scala
@@ -75,15 +68,15 @@ type T >: ([X] =>> L) <: ([X] =>> U)
 ```
 However, if `L` is `Nothing` it is not parameterized, since `Nothing` is treated as a bottom type for all kinds. For instance,
 ```scala
-type T[-X] <: X => ()
+type T[X] <: X => X
 ```
 is expanded to
 ```scala
-type T >: Nothing <: ([-X] =>> X => ())
+type T >: Nothing <: ([X] =>> X => X)
 ```
 instead of
 ```scala
-type T >: ([X] =>> Nothing) <: ([-X] =>> X => ())
+type T >: ([X] =>> Nothing) <: ([X] =>> X => X)
 ```
 
 The same expansions apply to type parameters. E.g.
@@ -94,6 +87,20 @@ is treated as a shorthand for
 ```scala
 [F >: Nothing <: [X] =>> Coll[X]]
 ```
+Abstract types and opaque type aliases remember the variances they were created with. So the type
+```scala
+def F2[-A, +B]
+```
+is known to be contravariant in `A` and covariant in `B` and can be instantiated only
+with types that satisfy these constraints. Likewise
+```scala
+opaque type O[X] = List[X]
+```
+`O` is known to be invariant (and not covariant, as its right hand side would suggest). On the other hand, a transparent alias
+```scala
+type O2[X] = List[X]
+```
+would be treated as covariant, `X` is used covariantly on its right-hand side.
 
 **Note**: The decision to treat `Nothing` as universal bottom type is provisional, and might be changed afer further discussion.
 
diff --git a/docs/docs/reference/new-types/type-lambdas.md b/docs/docs/reference/new-types/type-lambdas.md
index e2451693cb74..9881f4c71e80 100644
--- a/docs/docs/reference/new-types/type-lambdas.md
+++ b/docs/docs/reference/new-types/type-lambdas.md
@@ -7,24 +7,12 @@ A _type lambda_ lets one express a higher-kinded type directly, without
 a type definition.
 
 ```scala
-[+X, Y] =>> Map[Y, X]
+[X, Y] =>> Map[Y, X]
 ```
 
-For instance, the type above defines a binary type constructor, with a
-covariant parameter `X` and a non-variant parameter `Y`. The
+For instance, the type above defines a binary type constructor, which
 constructor maps arguments `X` and `Y` to `Map[Y, X]`. Type parameters
-of type lambdas can have variances and bounds. A parameterized type
-definition or declaration such as
-
-```scala
-type T[X] = (X, X)
-```
-
-is a shorthand for a plain type definition with a type-lambda as its
-right-hand side:
-
-```scala
-type T = [X] =>> (X, X)
-```
+of type lambdas can have bounds but they cannot carry `+` or `-` variance
+annotations.
 
 [More details](./type-lambdas-spec.md)
diff --git a/language-server/test/dotty/tools/languageserver/SignatureHelpTest.scala b/language-server/test/dotty/tools/languageserver/SignatureHelpTest.scala
index 22393a576fc4..85dc484c95f4 100644
--- a/language-server/test/dotty/tools/languageserver/SignatureHelpTest.scala
+++ b/language-server/test/dotty/tools/languageserver/SignatureHelpTest.scala
@@ -210,7 +210,7 @@ class SignatureHelpTest {
   @Test def typeParameters: Unit = {
     val signature =
       S("foo",
-        List("M <: [X] => Any", "T <: [Z] => M[Z]", "U >: T"),
+        List("M[X]", "T[Z] <: M[Z]", "U >: T"),
         List(
           List(P("p0", "M[Int]"), P("p1", "T[Int]"), P("p2", "U"))
         ),
@@ -315,7 +315,7 @@ class SignatureHelpTest {
   @Test def classTypeParameters: Unit = {
     val signature =
       S("Foo",
-        List("M <: [X] => Any", "T <: [Z] => M[Z]", "U"),
+        List("M[X]", "T[Z] <: M[Z]", "U"),
         List(
           List(P("p0", "M[Int]"), P("p1", "T[Int]"), P("p2", "U")),
           List(P("p3", "Int"))
diff --git a/tasty/src/dotty/tools/tasty/TastyFormat.scala b/tasty/src/dotty/tools/tasty/TastyFormat.scala
index 1a534cd9d547..96d5184c7c04 100644
--- a/tasty/src/dotty/tools/tasty/TastyFormat.scala
+++ b/tasty/src/dotty/tools/tasty/TastyFormat.scala
@@ -34,7 +34,6 @@ Macro-format:
 
                   UNIQUE            Length separator_NameRef uniqid_Nat underlying_NameRef? -- Unique name A<separator><number>
                   DEFAULTGETTER     Length underlying_NameRef index_Nat                     -- DefaultGetter$<number>
-                  VARIANT           Length underlying_NameRef variance_Nat                  -- variance 0: +A, variance = 1: -A
 
                   SUPERACCESSOR     Length underlying_NameRef                               -- super$A
                   INLINEACCESSOR    Length underlying_NameRef                               -- inline$A
@@ -153,8 +152,7 @@ Standard-Section: "ASTs" TopLevelStat*
                   SUPERtype      Length this_Type underlying_Type                  -- A super type reference to `underlying`
                   REFINEDtype    Length underlying_Type refinement_NameRef info_Type -- underlying { refinement_name : info }
                   APPLIEDtype    Length tycon_Type arg_Type*                       -- tycon[args]
-                  TYPEALIAS             alias_Type                                 -- = alias
-                  TYPEBOUNDS     Length low_Type high_Type                         -- >: low <: high
+                  TYPEBOUNDS     Length lowOrAlias_Type high_Type? Variance*       -- = alias or >: low <: high, possibly with variances of lambda parameters
                   ANNOTATEDtype  Length underlying_Type annotation_Term            -- underlying @ annotation
                   ANDtype        Length left_Type right_Type                       -- left & right
                   ORtype         Length left_Type right_Type                       -- lefgt | right
@@ -169,7 +167,7 @@ Standard-Section: "ASTs" TopLevelStat*
                   ERASEDGIVENMETHODtype Length result_Type NamesTypes              -- A method type `given(erased NamesTypes)result`, needed for refinements
                   IMPLICITMETHODtype    Length result_Type NamesTypes              -- A method type `(implicit NamesTypes)result`, needed for refinements
   // TODO: remove ERASEDIMPLICITMETHODtype
-                  TYPELAMBDAtype Length result_Type NamesTypes                     -- A type lambda `[NamesTypes] => result`, variance encoded using VARIANT names
+                  TYPELAMBDAtype Length result_Type NamesTypes                     -- A type lambda `[NamesTypes] => result`
                   SHAREDtype            type_ASTRef                                -- link to previously serialized type
   NamesTypes    = NameType*
   NameType      = paramName_NameRef typeOrBounds_ASTRef                            -- `termName : type`  or  `typeName bounds`
@@ -213,6 +211,10 @@ Standard-Section: "ASTs" TopLevelStat*
                   OPEN                                                             -- an open class
                   Annotation
 
+  Variance      = STABLE                                                           -- invariant
+                | COVARIANT
+                | CONTRAVARIANT
+
   Annotation    = ANNOTATION     Length tycon_Type fullAnnotation_Term             -- An annotation, given (class) type of constructor, and full application tree
 
 Note: Tree tags are grouped into 5 categories that determine what follows, and thus allow to compute the size of the tagged tree in a generic way.
@@ -251,7 +253,7 @@ Standard Section: "Comments" Comment*
 object TastyFormat {
 
   final val header: Array[Int] = Array(0x5C, 0xA1, 0xAB, 0x1F)
-  val MajorVersion: Int = 18
+  val MajorVersion: Int = 19
   val MinorVersion: Int = 0
 
   /** Tags used to serialize names, should update [[nameTagToString]] if a new constant is added */
@@ -272,9 +274,6 @@ object TastyFormat {
     final val DEFAULTGETTER = 11     // The name `<meth-name>$default$<param-num>`
                                      // of a default getter that returns a default argument.
 
-    final val VARIANT = 12           // A name `+<name>` or `-<name>` indicating
-                                     // a co- or contra-variant parameter of a type lambda.
-
     final val SUPERACCESSOR = 20     // The name of a super accessor `super$name` created by SuperAccesors.
 
     final val INLINEACCESSOR = 21    // The name of an inline accessor `inline$name`
@@ -300,7 +299,6 @@ object TastyFormat {
       case EXPANDPREFIX => "EXPANDPREFIX"
       case UNIQUE => "UNIQUE"
       case DEFAULTGETTER => "DEFAULTGETTER"
-      case VARIANT => "VARIANT"
       case SUPERACCESSOR => "SUPERACCESSOR"
       case INLINEACCESSOR => "INLINEACCESSOR"
       case OBJECTCLASS => "OBJECTCLASS"
@@ -392,9 +390,8 @@ object TastyFormat {
   final val PRIVATEqualified = 89
   final val PROTECTEDqualified = 90
   final val RECtype = 91
-  final val TYPEALIAS = 92
-  final val SINGLETONtpt = 93
-  final val BOUNDED = 94
+  final val SINGLETONtpt = 92
+  final val BOUNDED = 93
 
   // Cat. 4:    tag Nat AST
 
@@ -670,7 +667,6 @@ object TastyFormat {
     case APPLIEDtpt => "APPLIEDtpt"
     case TYPEBOUNDS => "TYPEBOUNDS"
     case TYPEBOUNDStpt => "TYPEBOUNDStpt"
-    case TYPEALIAS => "TYPEALIAS"
     case ANDtype => "ANDtype"
     case ORtype => "ORtype"
     case BYNAMEtype => "BYNAMEtype"
diff --git a/tests/neg-custom-args/kind-projector.check b/tests/neg-custom-args/kind-projector.check
index e0b42e4d2aa4..9bda8f03c6ba 100644
--- a/tests/neg-custom-args/kind-projector.check
+++ b/tests/neg-custom-args/kind-projector.check
@@ -5,8 +5,8 @@
 -- Error: tests/neg-custom-args/kind-projector.scala:5:23 --------------------------------------------------------------
 5 |class Bar1 extends Foo[Either[*, *]] // error
   |                       ^^^^^^^^^^^^
-  |                       Type argument Either has not the same kind as its bound  <: [_$1] => Any
+  |                       Type argument Either has not the same kind as its bound [_$1]
 -- Error: tests/neg-custom-args/kind-projector.scala:6:22 --------------------------------------------------------------
 6 |class Bar2 extends Foo[*] // error
   |                      ^
-  |                      Type argument _$4 has not the same kind as its bound  <: [_$1] => Any
+  |                      Type argument _$4 has not the same kind as its bound [_$1]
diff --git a/tests/neg/hk-variance2.scala b/tests/neg/hk-variance2.scala
new file mode 100644
index 000000000000..7eb7511b3d09
--- /dev/null
+++ b/tests/neg/hk-variance2.scala
@@ -0,0 +1,29 @@
+
+trait S {
+  type F[+X]
+}
+trait T {
+  type F[-X]
+}
+object Test2 {
+  object O extends S, T {
+    type F[X] = Int  // OK
+  }
+  object O2 extends S, T {
+    type F[X] = X  // error
+  }
+  object O3 extends S, T {
+    type F[X] = X => X // error
+  }
+}
+object Test3 {
+  object O extends S, T {
+    type F = [X] =>> Int  // OK
+  }
+  object O2 extends S, T {
+    type F = [X] =>> X  // error
+  }
+  object O3 extends S, T {
+    type F = [X] =>> X => X // error
+  }
+}
diff --git a/tests/neg/hk-variance3.scala b/tests/neg/hk-variance3.scala
new file mode 100644
index 000000000000..f26635486670
--- /dev/null
+++ b/tests/neg/hk-variance3.scala
@@ -0,0 +1,8 @@
+object Test4 {
+  def x: Any { type F[+X] } = ???
+  def y: Any { type F[X]} = ???
+  val z = if ??? then x else y
+  val z2 = if ??? then y else x
+  val zc: Any { type F[+X] } = z // error
+  val z2c: Any { type F[+X] } = z2  // error
+}
\ No newline at end of file
diff --git a/tests/neg/i6475.scala b/tests/neg/i6475.scala
new file mode 100644
index 000000000000..61f019840421
--- /dev/null
+++ b/tests/neg/i6475.scala
@@ -0,0 +1,4 @@
+object Foo1 { type T[+A] = (A, Int) }
+object Foo2 { type T[+A] = [+B] =>> (A, B) }   // error no `+/-` variance annotation allowed here
+object Foo3 { type T[+A] = [+B] =>> [C] =>> (A, B) }  // error
+object Foo4 { type T = [+A] =>> [+B] =>> [C] =>> (A, B) } // error // error
diff --git a/tests/neg/type-lambdas-posttyper.scala b/tests/neg/type-lambdas-posttyper.scala
index 5eed086ad632..a94bb9b4a01b 100644
--- a/tests/neg/type-lambdas-posttyper.scala
+++ b/tests/neg/type-lambdas-posttyper.scala
@@ -13,10 +13,10 @@ object Test extends App {
     var x: X = init
   }
 
-  type TL3 = [+X] =>> Ref[X] // error: covariant type parameter X occurs in nonvariant position in Test.Ref[X]
+  type TL3[+X] = Ref[X] // error: covariant type parameter X occurs in nonvariant position in Test.Ref[X]
   type TL4[-X] = X => X // error: contravariant type parameter X occurs in covariant position in X => X
 
-  def f[F <: [+X] =>> Any](x: F[String]): F[Any] = x
+  def f[F[+X]](x: F[String]): F[Any] = x
 
   val sref = new Ref[String]("abc")
   val aref: Ref[Any] = f[TL3](sref)
@@ -27,15 +27,15 @@ object Test extends App {
   type Neg2[-X] >: X // error
   type Neg3[-X] <: X // error
 
-  type Neg4 = [-X] =>> X // error
-  type Neg5 >: [-X] =>> X <: [-X] =>> Any // error
-  type Neg6 <: [-X] =>> X // error
+  type Neg4[-X] = X // error
+  type Neg5[-X] >: X <: Any // error
+  type Neg6[-X] <: X // error
 
   type Pos1[+X] = Ref[X] // error
   type Pos2[+X] >: Ref[X] // error
   type Pos3[+X] <: Ref[X] // error
 
-  type Pos4 = [+X] =>> Ref[X] // error
-  type Pos5 >: [+X] =>> Ref[X] <: [+X] =>> Any // error
-  type Pos6 <: [+X] =>> Ref[X] // error
+  type Pos4[+X] = Ref[X] // error
+  type Pos5[+X] >: Ref[X] <: Any // error
+  type Pos6[+X] <: Ref[X] // error
 }
diff --git a/tests/pos-custom-args/erased/i7868.scala b/tests/pos-custom-args/erased/i7868.scala
index 19ff8376fc3a..6072dc5592e4 100644
--- a/tests/pos-custom-args/erased/i7868.scala
+++ b/tests/pos-custom-args/erased/i7868.scala
@@ -25,7 +25,7 @@ object Coproduct {
   def upCast[A, B](a: A) with (erased evidence: (A <:< B) ): B = a.asInstanceOf[B]
 
   def from[Set, Value, Index <: Int](value: Value) with (erased at: At[Set, Value, Index]) : ValueOf[Index] ?=> Coproduct[Set, Value, Index] = {
-    Coproduct[Set, Value, Index](upCast(value: Value).with(at.cast.liftCo[[+X] =>> Value & X]), valueOf[Index])
+    Coproduct[Set, Value, Index](upCast(value: Value).with(at.cast.liftCo[[X] =>> Value & X]), valueOf[Index])
   }
 
 }
diff --git a/tests/pos/hk-variance.scala b/tests/pos/hk-variance.scala
new file mode 100644
index 000000000000..f070b3cea4da
--- /dev/null
+++ b/tests/pos/hk-variance.scala
@@ -0,0 +1,20 @@
+class C[F[X]]
+class D[F[+X]]
+
+type Id[X] = X
+
+def test =
+  val x = C[Id]()
+  val y = D[Id]()
+
+object Test2 {
+  trait S {
+    type F[+X]
+  }
+  trait T {
+    type F[-X]
+  }
+  object O extends S, T {
+    type F[X] = Int
+  }
+}
diff --git a/tests/neg/i2232.scala b/tests/pos/i2232.scala
similarity index 100%
rename from tests/neg/i2232.scala
rename to tests/pos/i2232.scala
diff --git a/tests/pos/i6475.scala b/tests/pos/i6475.scala
deleted file mode 100644
index f0ebdf5de493..000000000000
--- a/tests/pos/i6475.scala
+++ /dev/null
@@ -1,4 +0,0 @@
-object Foo1 { type T[+A] = (A, Int) }
-object Foo2 { type T[+A] = [+B] =>> (A, B) }
-object Foo3 { type T[+A] = [+B] =>> [C] =>> (A, B) }
-object Foo4 { type T = [+A] =>> [+B] =>> [C] =>> (A, B) }
diff --git a/tests/pos/i7993.scala b/tests/pos/i7993.scala
new file mode 100644
index 000000000000..f214440e924c
--- /dev/null
+++ b/tests/pos/i7993.scala
@@ -0,0 +1,21 @@
+trait TC[F[_]]
+
+object TC {
+  def check[F[_], A](x: F[A])(implicit F: TC[F]): Unit = ()
+}
+
+case class Foo[+E, +A](value: A)
+
+object Foo {
+  type WithList[+E, +A] = Foo[List[E], A]
+
+  implicit def instance[E]: TC[[x] =>> Foo[E, x]] =
+    new TC[[x] =>> Foo[E, x]] {}
+}
+
+val x1: Foo[List[String], Int] = Foo(1)
+val x2: Foo.WithList[String, Int] = Foo(1)
+
+def test =
+  TC.check(x1)
+  TC.check(x2)
\ No newline at end of file
diff --git a/tests/pos/i8049.scala b/tests/pos/i8049.scala
new file mode 100644
index 000000000000..a29fb9badd31
--- /dev/null
+++ b/tests/pos/i8049.scala
@@ -0,0 +1,23 @@
+import scala.language.implicitConversions
+
+class Ops[A](a: A) {
+  def bar: Unit = ()
+}
+
+implicit def toOps[A](a: A): Ops[A] = new Ops[A](a)
+
+type Id[A] = A
+
+class Foo[A](val value: Id[A]) {
+  def same: Foo[A] = new Foo[A](value)
+  def map[B](f: A => B): Foo[B] = new Foo[B](f(value))
+}
+
+val x: Int = 1
+val foo: Foo[Int] = new Foo(1)
+
+val res1 = x.bar
+val res2 = foo.value.bar
+val res3 = foo.same.value.bar
+val res4 = foo.map[Int](_ + 1).value.bar
+val res5 = foo.map(_ + 1).value.bar
\ No newline at end of file
diff --git a/tests/pos/reference/type-lambdas.scala b/tests/pos/reference/type-lambdas.scala
index a6fdcc42460d..3db8fab7b35f 100644
--- a/tests/pos/reference/type-lambdas.scala
+++ b/tests/pos/reference/type-lambdas.scala
@@ -2,7 +2,7 @@ package typeLambdas
 
 object Test {
 
-  type T =  [+X, Y] =>> Map[Y, X]
+  type T[+X, Y] = Map[Y, X]
 
   type CTL = [X] =>> [Y] =>> (X, Y)
   type T3 = CTL[Int][String]
diff --git a/tests/run-macros/tasty-simplified.check b/tests/run-macros/tasty-simplified.check
index d1a9d7904ec2..ae73a625ac58 100644
--- a/tests/run-macros/tasty-simplified.check
+++ b/tests/run-macros/tasty-simplified.check
@@ -1,4 +1,4 @@
-Functor[[+A >: scala.Nothing <: scala.Any] => scala.collection.immutable.List[+A]]
+Functor[[A >: scala.Nothing <: scala.Any] => scala.collection.immutable.List[A]]
 Functor[Const[scala.Int]]
 Functor[Id]
-Functor[[+A >: scala.Nothing <: scala.Any] => scala.Option[+A]]
+Functor[[A >: scala.Nothing <: scala.Any] => scala.Option[A]]
diff --git a/tests/run-staging/i5965.check b/tests/run-staging/i5965.check
index 0f1c479d2902..166c6cdff5c1 100644
--- a/tests/run-staging/i5965.check
+++ b/tests/run-staging/i5965.check
@@ -1,11 +1,11 @@
 {
-  val y: [+A >: scala.Nothing <: scala.Any] => scala.collection.immutable.List[+A][scala.Int] = scala.List.apply[scala.Int](1, 2, 3)
+  val y: [A >: scala.Nothing <: scala.Any] => scala.collection.immutable.List[A][scala.Int] = scala.List.apply[scala.Int](1, 2, 3)
 
   (y: scala.collection.immutable.List[scala.Int])
 }
 List(1, 2, 3)
 {
-  val y: [+A >: scala.Nothing <: scala.Any] => scala.Option[+A][scala.Int] = scala.Option.apply[scala.Int](4)
+  val y: [A >: scala.Nothing <: scala.Any] => scala.Option[A][scala.Int] = scala.Option.apply[scala.Int](4)
 
   (y: scala.Option[scala.Int])
 }