diff --git a/compiler/src/dotty/tools/dotc/transform/PostTyper.scala b/compiler/src/dotty/tools/dotc/transform/PostTyper.scala
index 5cd8795b4d04..b57410c25f25 100644
--- a/compiler/src/dotty/tools/dotc/transform/PostTyper.scala
+++ b/compiler/src/dotty/tools/dotc/transform/PostTyper.scala
@@ -4,7 +4,7 @@ package transform
 import dotty.tools.dotc.ast.{Trees, tpd, untpd}
 import scala.collection.mutable
 import core._
-import typer.Checking
+import typer.{Checking, VarianceChecker}
 import Types._, Contexts._, Names._, Flags._, DenotTransformers._, Phases._
 import SymDenotations._, StdNames._, Annotations._, Trees._, Scopes._
 import Decorators._
@@ -296,6 +296,9 @@ class PostTyper extends MacroTransform with IdentityDenotTransformer { thisPhase
           // when trying to typecheck self types which are intersections.
           Checking.checkNonCyclicInherited(tree.tpe, tree.left.tpe :: tree.right.tpe :: Nil, EmptyScope, tree.pos)
           super.transform(tree)
+        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/VarianceChecker.scala b/compiler/src/dotty/tools/dotc/typer/VarianceChecker.scala
index 871b77809f23..fe59723ed3c0 100644
--- a/compiler/src/dotty/tools/dotc/typer/VarianceChecker.scala
+++ b/compiler/src/dotty/tools/dotc/typer/VarianceChecker.scala
@@ -7,6 +7,7 @@ import Types._, Contexts._, Flags._, Symbols._, Trees._
 import Decorators._
 import Variances._
 import NameKinds._
+import TypeApplications.varianceConforms
 import util.Positions._
 import config.Printers.variances
 import reporting.trace
@@ -19,6 +20,41 @@ object VarianceChecker {
   case class VarianceError(tvar: Symbol, required: Variance)
   def check(tree: tpd.Tree)(implicit ctx: Context): Unit =
     new VarianceChecker()(ctx).Traverser.traverse(tree)
+
+  /** Check that variances of type lambda correspond to their occurrences in its body.
+   *  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 = tree.tpe match {
+    case tl: HKTypeLambda =>
+      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 => "non"
+            case 1 => "co"
+          }
+          val pos = tree.tparams
+            .find(_.name.toTermName == paramName)
+            .map(_.pos)
+            .getOrElse(tree.pos)
+          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 _ =>
+              foldOver(x, t)
+          }
+        }
+      }
+      checkOK.apply(true, tl.resType)
+    case _ =>
+  }
 }
 
 class VarianceChecker()(implicit ctx: Context) {
diff --git a/docs/docs/reference/type-lambdas-spec.md b/docs/docs/reference/type-lambdas-spec.md
new file mode 100644
index 000000000000..c4580b6a635e
--- /dev/null
+++ b/docs/docs/reference/type-lambdas-spec.md
@@ -0,0 +1,111 @@
+---
+layout: doc-page
+title: "Type Lambdas - More Details"
+---
+
+## Syntax
+
+```
+Type              ::=  ... |  HkTypeParamClause ‘=>’ Type
+HkTypeParamClause ::=  ‘[’ HkTypeParam {‘,’ HkTypeParam} ‘]’
+HkTypeParam       ::=  {Annotation} [‘+’ | ‘-’] (Id[HkTypeParamClause] | ‘_’) TypeBounds
+TypeBounds        ::=  [‘>:’ Type] [‘<:’ Type]
+```
+
+### Type Checking
+
+A type lambda such `[X] => F[X]` defines a function from types to types. The parameter(s) may carry bounds and variance annotations.
+If a parameter is 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
+```
+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.
+
+## Relationship with Parameterized Type Definitions
+
+A parameterized type definition
+```scala
+type T[X] = R
+```
+is regarded as a shorthand for an unparameterized definition with a type lambda as right-hand side:
+```scala
+type T = [X] => R
+```
+
+A parameterized abstract type
+```scala
+type T[X] >: L <: U
+```
+is regarded as shorthand for an unparameterized abstract type with type lambdas as bounds.
+```scala
+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 => ()
+```
+is expanded to
+```scala
+type T >: Nothing <: ([-X] => X => ())
+```
+instead of
+```scala
+type T >: ([X] => Nothing) <: ([-X] => X => ())
+```
+
+The same expansions apply to type parameters. E.g.
+```scala
+[F[X] <: Coll[X]]
+```
+is treated as a shorthand for
+```scala
+[F >: Nothing <: [X] => Coll[X]]
+```
+
+**Note**: The decision to treat `Nothing` as universal bottom type is provisional, and might be changed afer further discussion.
+
+**Note**: Scala 2 and 3 differ in that Scala 2 also treats `Any` as universal top-type. This is not done in Scala 3. See also the discussion on [kind polymorphism](./kind-polymorphism.html)
+
+## Curried Type Parameters
+
+The body of a type lambda can again be a type lambda. Example:
+```scala
+type TL = [X] => [Y] => (X, Y)
+```
+Currently, no special provision is made to infer type arguments to such curried type lambdas. This is left for future work.
+
+
+
diff --git a/docs/docs/reference/type-lambdas.md b/docs/docs/reference/type-lambdas.md
index 748033840aa2..9a382987dafe 100644
--- a/docs/docs/reference/type-lambdas.md
+++ b/docs/docs/reference/type-lambdas.md
@@ -20,3 +20,5 @@ is a shorthand for a plain type definition with a type-lambda as its
 right-hand side:
 
     type T = [X] => (X, X)
+
+[More details](./type-lambdas-spec.html)
\ No newline at end of file
diff --git a/tests/neg/type-lambdas-posttyper.scala b/tests/neg/type-lambdas-posttyper.scala
new file mode 100644
index 000000000000..d6ed328d883d
--- /dev/null
+++ b/tests/neg/type-lambdas-posttyper.scala
@@ -0,0 +1,26 @@
+object Test extends App {
+
+  trait Ord[X]
+
+  type TL1 = [X <: Ord[X]] => (X, X)
+
+  class C extends Ord[C]
+
+  type T1 = TL1[Int] // error: Type argument Int does not conform to upper bound Test.Ord[LazyRef(Int)
+  type T2 = TL1[C]   // OK
+
+  class Ref[X](init: X) {
+    var x: X = init
+  }
+
+  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
+
+  val sref = new Ref[String]("abc")
+  val aref: Ref[Any] = f[TL3](sref)
+  aref.x = 1
+  val s: String = sref.x
+
+}
diff --git a/tests/neg/type-lambdas.scala b/tests/neg/type-lambdas.scala
new file mode 100644
index 000000000000..6c048c40f7a6
--- /dev/null
+++ b/tests/neg/type-lambdas.scala
@@ -0,0 +1,8 @@
+object Test extends App {
+
+  trait Ord[X]
+
+  type TL1 = [X <: Ord[X]] => (X, X) // OK
+  type TL2 = [X >: Ord[X]] => (X, X) // error: illegal cyclic reference: lower bound Test.Ord[X] of type X refers back to the type itself
+
+}
diff --git a/tests/pos/polytypes.scala b/tests/pos/polytypes.scala
index ec6c89d10c45..e0e2224b8496 100644
--- a/tests/pos/polytypes.scala
+++ b/tests/pos/polytypes.scala
@@ -1,6 +1,6 @@
 object Test {
 
-  type T = [+X] => (List[X] => List[X])
+  type T = [X] => (List[X] => List[X])
 
   def reverse[X](xs: List[X]): List[X] = ???
 
diff --git a/tests/pos/reference/type-lambdas.scala b/tests/pos/reference/type-lambdas.scala
index af5f84709f95..7456456dc113 100644
--- a/tests/pos/reference/type-lambdas.scala
+++ b/tests/pos/reference/type-lambdas.scala
@@ -4,4 +4,8 @@ object Test {
 
   type T =  [+X, Y] => Map[Y, X]
 
+  type CTL = [X] => [Y] => (X, Y)
+  type T3 = CTL[Int][String]
+
+  type T2[+X <: X => X] = Any  // OK - variance is not checked in param bounds
 }
diff --git a/tests/pos/seqtype-cycle/Test2.scala b/tests/pos/seqtype-cycle/Test2.scala
index a9e1fc7ee214..cd52cb26864e 100644
--- a/tests/pos/seqtype-cycle/Test2.scala
+++ b/tests/pos/seqtype-cycle/Test2.scala
@@ -3,6 +3,6 @@ package object scala {
   type Throwable = java.lang.Throwable
   type IndexOutOfBoundsException = java.lang.IndexOutOfBoundsException
 
-  type Seq[+A] = scala.collection.Seq[A]
+  type Seq[A] = scala.collection.Seq[A]
   val Seq = scala.collection.Seq
 }