Start new, direct HK scheme

- Re-introduce newHK option. Label some things that will be
removed with OLD.

18 files changed, 478 insertions, 186 deletions

diff --git a/src/dotty/tools/dotc/config/Config.scala b/src/dotty/tools/dotc/config/Config.scala
index 7dfc09b3f..bf6f8493b 100644
--- a/src/dotty/tools/dotc/config/Config.scala
+++ b/src/dotty/tools/dotc/config/Config.scala
@@ -10,6 +10,8 @@ object Config {
 
   final val checkCacheMembersNamed = false
 
+  final val newHK = false
+
   /** When updating a constraint bound, check that the constrained parameter
    *  does not appear at the top-level of either of its bounds.
    */
diff --git a/src/dotty/tools/dotc/core/ConstraintHandling.scala b/src/dotty/tools/dotc/core/ConstraintHandling.scala
index e7b05af43..00b8a5d25 100644
--- a/src/dotty/tools/dotc/core/ConstraintHandling.scala
+++ b/src/dotty/tools/dotc/core/ConstraintHandling.scala
@@ -287,8 +287,8 @@ trait ConstraintHandling {
           if (!addParamBound(bound)) NoType
           else if (fromBelow) defn.NothingType
           else defn.AnyType
-        case bound: RefinedType =>
-          bound.normalizeHkApply
+        case bound: RefinedType if !Config.newHK =>
+          bound.normalizeHkApplyOLD
         case _ =>
           bound
       }
diff --git a/src/dotty/tools/dotc/core/MemberBinding.scala b/src/dotty/tools/dotc/core/MemberBinding.scala
index 6f081c542..bff8b30a0 100644
--- a/src/dotty/tools/dotc/core/MemberBinding.scala
+++ b/src/dotty/tools/dotc/core/MemberBinding.scala
@@ -7,6 +7,7 @@ import Types.{Type, TypeBounds}
 /** A common super trait of Symbol and Refinement.
  *  Used to capture the attributes of type parameters
  *  which can be implemented as either symbols or refinements.
+ *  TODO: Rename (TypeParamInfo?)
  */
 trait MemberBinding {
 
diff --git a/src/dotty/tools/dotc/core/NameOps.scala b/src/dotty/tools/dotc/core/NameOps.scala
index b5704480a..120540dc7 100644
--- a/src/dotty/tools/dotc/core/NameOps.scala
+++ b/src/dotty/tools/dotc/core/NameOps.scala
@@ -102,19 +102,19 @@ object NameOps {
     }
 
     /** Is this the name of a higher-kinded type parameter of a Lambda? */
-    def isHkArgName =
+    def isHkArgNameOLD =
       name.length > 0 &&
-      name.head == tpnme.hkArgPrefixHead &&
-      name.startsWith(tpnme.hkArgPrefix) && {
-        val digits = name.drop(tpnme.hkArgPrefixLength)
+      name.head == tpnme.hkArgPrefixHeadOLD &&
+      name.startsWith(tpnme.hkArgPrefixOLD) && {
+        val digits = name.drop(tpnme.hkArgPrefixLengthOLD)
         digits.length <= 4 && digits.forall(_.isDigit)
       }
 
     /** The index of the higher-kinded type parameter with this name.
      *  Pre: isLambdaArgName.
      */
-    def hkArgIndex: Int =
-      name.drop(tpnme.hkArgPrefixLength).toString.toInt
+    def hkArgIndexOLD: Int =
+      name.drop(tpnme.hkArgPrefixLengthOLD).toString.toInt
 
     /** If the name ends with $nn where nn are
       * all digits, strip the $ and the digits.
diff --git a/src/dotty/tools/dotc/core/StdNames.scala b/src/dotty/tools/dotc/core/StdNames.scala
index c767f4c29..0adf80d8f 100644
--- a/src/dotty/tools/dotc/core/StdNames.scala
+++ b/src/dotty/tools/dotc/core/StdNames.scala
@@ -529,9 +529,9 @@ object StdNames {
 
     val synthSwitch: N          = "$synthSwitch"
 
-    val hkArgPrefix: N          = "$hk"
-    val hkArgPrefixHead: Char   = hkArgPrefix.head
-    val hkArgPrefixLength: Int  = hkArgPrefix.length
+    val hkArgPrefixOLD: N          = "$hk"
+    val hkArgPrefixHeadOLD: Char   = hkArgPrefixOLD.head
+    val hkArgPrefixLengthOLD: Int  = hkArgPrefixOLD.length
 
     // unencoded operators
     object raw {
@@ -737,12 +737,16 @@ object StdNames {
   class ScalaTypeNames extends ScalaNames[TypeName] {
     protected implicit def fromString(s: String): TypeName = typeName(s)
 
-    @switch def syntheticTypeParamName(i: Int): TypeName = "T" + i
+    def syntheticTypeParamName(i: Int): TypeName = "T" + i
+    def syntheticLambdaParamName(i: Int): TypeName = "X" + i
 
     def syntheticTypeParamNames(num: Int): List[TypeName] =
       (0 until num).map(syntheticTypeParamName)(breakOut)
 
-    def hkArg(n: Int): TypeName = hkArgPrefix ++ n.toString
+    def syntheticLambdaParamNames(num: Int): List[TypeName] =
+      (0 until num).map(syntheticLambdaParamName)(breakOut)
+
+    def hkArgOLD(n: Int): TypeName = hkArgPrefixOLD ++ n.toString
 
     final val Conforms = encode("<:<")
   }
diff --git a/src/dotty/tools/dotc/core/SymDenotations.scala b/src/dotty/tools/dotc/core/SymDenotations.scala
index e8053a740..2692f57a2 100644
--- a/src/dotty/tools/dotc/core/SymDenotations.scala
+++ b/src/dotty/tools/dotc/core/SymDenotations.scala
@@ -1130,6 +1130,7 @@ object SymDenotations {
       case tp: PolyType => tp.paramBounds.exists(hasSkolems) || hasSkolems(tp.resType)
       case tp: MethodType => tp.paramTypes.exists(hasSkolems) || hasSkolems(tp.resType)
       case tp: ExprType => hasSkolems(tp.resType)
+      case tp: HKApply => hasSkolems(tp.tycon) || tp.args.exists(hasSkolems)
       case tp: AndOrType => hasSkolems(tp.tp1) || hasSkolems(tp.tp2)
       case tp: TypeBounds => hasSkolems(tp.lo) || hasSkolems(tp.hi)
       case tp: AnnotatedType => hasSkolems(tp.tpe)
diff --git a/src/dotty/tools/dotc/core/TypeApplications.scala b/src/dotty/tools/dotc/core/TypeApplications.scala
index 33aa060b5..12b42642d 100644
--- a/src/dotty/tools/dotc/core/TypeApplications.scala
+++ b/src/dotty/tools/dotc/core/TypeApplications.scala
@@ -56,13 +56,13 @@ object TypeApplications {
   def variancesConform(tparams1: List[MemberBinding], tparams2: List[MemberBinding])(implicit ctx: Context): Boolean =
     tparams1.corresponds(tparams2)(varianceConforms)
 
-  def fallbackTypeParams(variances: List[Int])(implicit ctx: Context): List[MemberBinding] = {
+  def fallbackTypeParamsOLD(variances: List[Int])(implicit ctx: Context): List[MemberBinding] = {
     def memberBindings(vs: List[Int]): Type = vs match {
       case Nil => NoType
       case v :: vs1 =>
         RefinedType(
             memberBindings(vs1),
-            tpnme.hkArg(vs1.length),
+            tpnme.hkArgOLD(vs1.length),
             TypeBounds.empty.withBindingKind(BindingKind.fromVariance(v)))
     }
     def decompose(t: Type, acc: List[MemberBinding]): List[MemberBinding] = t match {
@@ -78,14 +78,14 @@ object TypeApplications {
    *    ==>
    *    ([X_i := this.$hk_i] T) { type v_i $hk_i: (new)B_i }
    */
-  object TypeLambda {
+  object TypeLambdaOLD {
     def apply(argBindingFns: List[RecType => TypeBounds],
               bodyFn: RecType => Type)(implicit ctx: Context): Type = {
-      val argNames = argBindingFns.indices.toList.map(tpnme.hkArg)
+      val argNames = argBindingFns.indices.toList.map(tpnme.hkArgOLD)
       var idx = 0
       RecType.closeOver(rt =>
         (bodyFn(rt) /: argBindingFns) { (parent, argBindingFn) =>
-          val res = RefinedType(parent, tpnme.hkArg(idx), argBindingFn(rt))
+          val res = RefinedType(parent, tpnme.hkArgOLD(idx), argBindingFn(rt))
           idx += 1
           res
         })
@@ -117,26 +117,33 @@ object TypeApplications {
    *  @param tycon     C
    */
   object EtaExpansion {
-    def apply(tycon: TypeRef)(implicit ctx: Context) = {
-      assert(tycon.isEtaExpandable)
+    def apply(tycon: Type)(implicit ctx: Context) = {
+      if (!Config.newHK) assert(tycon.isEtaExpandableOLD)
       tycon.EtaExpand(tycon.typeParamSymbols)
     }
 
-    def unapply(tp: Type)(implicit ctx: Context): Option[TypeRef] = {
-      def argsAreForwarders(args: List[Type], n: Int): Boolean = args match {
-        case Nil =>
-          n == 0
-        case TypeRef(RecThis(rt), sel) :: args1 if false =>
-          rt.eq(tp) && sel == tpnme.hkArg(n - 1) && argsAreForwarders(args1, n - 1)
-        case _ =>
-          false
-      }
-      tp match {
-        case TypeLambda(argBounds, AppliedType(fn: TypeRef, args))
-        if argsAreForwarders(args, tp.typeParams.length) => Some(fn)
-        case _ => None
+    def unapply(tp: Type)(implicit ctx: Context): Option[TypeRef] =
+      if (Config.newHK)
+        tp match {
+          case tp @ TypeLambda(tparams, AppliedType(fn: TypeRef, args))
+          if (args == tparams.map(_.toArg)) => Some(fn)
+          case _ => None
+        }
+      else {
+        def argsAreForwarders(args: List[Type], n: Int): Boolean = args match {
+          case Nil =>
+            n == 0
+          case TypeRef(RecThis(rt), sel) :: args1 if false =>
+            rt.eq(tp) && sel == tpnme.hkArgOLD(n - 1) && argsAreForwarders(args1, n - 1)
+          case _ =>
+            false
+        }
+        tp match {
+          case TypeLambdaOLD(argBounds, AppliedType(fn: TypeRef, args))
+          if argsAreForwarders(args, tp.typeParams.length) => Some(fn)
+          case _ => None
+        }
       }
-    }
   }
 
   /** Extractor for type application T[U_1, ..., U_n]. This is the refined type
@@ -169,6 +176,8 @@ object TypeApplications {
             None
         }
         collectArgs(tycon.typeParams, refinements, new mutable.ListBuffer[Type])
+      case HKApply(tycon, args) =>
+        Some((tycon, args))
       case _ =>
         None
     }
@@ -187,15 +196,15 @@ object TypeApplications {
     }
 
   /** The references `<rt>.this.$hk0, ..., <rt>.this.$hk<n-1>`. */
-  def argRefs(rt: RecType, n: Int)(implicit ctx: Context) =
-    List.range(0, n).map(i => RecThis(rt).select(tpnme.hkArg(i)))
+  def argRefsOLD(rt: RecType, n: Int)(implicit ctx: Context) =
+    List.range(0, n).map(i => RecThis(rt).select(tpnme.hkArgOLD(i)))
 
-  private class InstMap(fullType: Type)(implicit ctx: Context) extends TypeMap {
+  private class InstMapOLD(fullType: Type)(implicit ctx: Context) extends TypeMap {
     var localRecs: Set[RecType] = Set.empty
     var keptRefs: Set[Name] = Set.empty
     var tyconIsHK: Boolean = true
     def apply(tp: Type): Type = tp match {
-      case tp @ TypeRef(RecThis(rt), sel) if sel.isHkArgName && localRecs.contains(rt) =>
+      case tp @ TypeRef(RecThis(rt), sel) if sel.isHkArgNameOLD && localRecs.contains(rt) =>
         fullType.member(sel).info match {
           case TypeAlias(alias) => apply(alias)
           case _ => keptRefs += sel; tp
@@ -203,7 +212,7 @@ object TypeApplications {
       case tp: TypeVar if !tp.inst.exists =>
         val bounds = tp.instanceOpt.orElse(ctx.typeComparer.bounds(tp.origin))
         bounds.foreachPart {
-          case TypeRef(RecThis(rt), sel) if sel.isHkArgName && localRecs.contains(rt) =>
+          case TypeRef(RecThis(rt), sel) if sel.isHkArgNameOLD && localRecs.contains(rt) =>
             keptRefs += sel
           case _ =>
         }
@@ -329,7 +338,9 @@ class TypeApplications(val self: Type) extends AnyVal {
   /** Is self type higher-kinded (i.e. of kind != "*")? */
   def isHK(implicit ctx: Context): Boolean = self.dealias match {
     case self: TypeRef => self.info.isHK
-    case self: RefinedType => self.isTypeParam
+    case self: RefinedType => !Config.newHK && self.isTypeParam
+    case self: TypeLambda => true
+    case self: HKApply => false
     case self: SingletonType => false
     case self: TypeVar => self.origin.isHK
     case self: WildcardType => self.optBounds.isHK
@@ -354,7 +365,9 @@ class TypeApplications(val self: Type) extends AnyVal {
           else 0
       }
     case self: RefinedType =>
-      if (self.isTypeParam) 1 else -1
+      if (!Config.newHK && self.isTypeParam) 1 else -1
+    case self: TypeLambda => 1
+    case self: HKApply => -1
     case self: SingletonType => -1
     case self: TypeVar => self.origin.knownHK
     case self: WildcardType => self.optBounds.knownHK
@@ -364,15 +377,14 @@ class TypeApplications(val self: Type) extends AnyVal {
     case _ => -1
   }
 
-  /** is receiver of the form T#$Apply? */
-  def isHKApply(implicit ctx: Context): Boolean = self match {
-    case self @ RefinedType(_, name, _) => name.isHkArgName && !self.isTypeParam
+  /** is receiver a higher-kinded application? */
+  def isHKApplyOLD(implicit ctx: Context): Boolean = self match {
+    case self @ RefinedType(_, name, _) => name.isHkArgNameOLD && !self.isTypeParam
     case _ => false
   }
 
   /** True if it can be determined without forcing that the class symbol
-   *  of this application exists and is not a lambda trait.
-   *  Equivalent to
+   *  of this application exists. Equivalent to
    *
    *    self.classSymbol.exists
    *
@@ -402,11 +414,11 @@ class TypeApplications(val self: Type) extends AnyVal {
   /** Replace references to type parameters with references to hk arguments `this.$hk_i`
    * Care is needed not to cause cyclic reference errors, hence `SafeSubstMap`.
    */
-  def recursify[T <: Type](tparams: List[MemberBinding])(implicit ctx: Context): RecType => T =
+  def recursifyOLD[T <: Type](tparams: List[MemberBinding])(implicit ctx: Context): RecType => T =
     tparams match {
       case (_: Symbol) :: _ =>
         (rt: RecType) =>
-          new ctx.SafeSubstMap(tparams.asInstanceOf[List[Symbol]], argRefs(rt, tparams.length))
+          new ctx.SafeSubstMap(tparams.asInstanceOf[List[Symbol]], argRefsOLD(rt, tparams.length))
             .apply(self).asInstanceOf[T]
       case _ =>
         def mapRefs(rt: RecType) = new TypeMap {
@@ -421,23 +433,34 @@ class TypeApplications(val self: Type) extends AnyVal {
   /** Lambda abstract `self` with given type parameters. Examples:
    *
    *      type T[X] = U        becomes    type T = [X] -> U
-   *      type T[X] >: L <: U  becomes    type T >: L <: ([X] -> _ <: U)
+   *      type T[X] >: L <: U  becomes    type T >: L <: ([X] -> U)
+   *
+   *  TODO: Handle parameterized lower bounds
    */
   def LambdaAbstract(tparams: List[Symbol])(implicit ctx: Context): Type = {
     def expand(tp: Type) =
-      TypeLambda(
-        tparams.map(tparam =>
-          tparam.memberBoundsAsSeenFrom(self)
-            .withBindingKind(BindingKind.fromVariance(tparam.variance))
-            .recursify(tparams)),
-        tp.recursify(tparams))
+      if (Config.newHK) TypeLambda.fromSymbols(tparams, tp)
+      else
+        TypeLambdaOLD(
+          tparams.map(tparam =>
+            tparam.memberBoundsAsSeenFrom(self)
+              .withBindingKind(BindingKind.fromVariance(tparam.variance))
+              .recursifyOLD(tparams)),
+          tp.recursifyOLD(tparams))
 
     assert(!isHK, self)
-    self match {
+    if (Config.newHK) self match {
       case self: TypeAlias =>
-        self.derivedTypeAlias(expand(self.alias.normalizeHkApply))
+        self.derivedTypeAlias(expand(self.alias))
       case self @ TypeBounds(lo, hi) =>
-        self.derivedTypeBounds(lo, expand(hi.normalizeHkApply))
+        self.derivedTypeBounds(lo, expand(hi))
+      case _ => expand(self)
+    }
+    else self match {
+      case self: TypeAlias =>
+        self.derivedTypeAlias(expand(self.alias.normalizeHkApplyOLD))
+      case self @ TypeBounds(lo, hi) =>
+        self.derivedTypeBounds(lo, expand(hi.normalizeHkApplyOLD))
       case _ => expand(self)
     }
   }
@@ -470,9 +493,9 @@ class TypeApplications(val self: Type) extends AnyVal {
    *   - dropping refinements and rec-types
    *   - going from a wildcard type to its upper bound
    */
-  def normalizeHkApply(implicit ctx: Context): Type = self.strictDealias match {
-    case self1 @ RefinedType(_, rname, _) if rname.isHkArgName && self1.typeParams.isEmpty =>
-      val inst = new InstMap(self)
+  def normalizeHkApplyOLD(implicit ctx: Context): Type = self.strictDealias match {
+    case self1 @ RefinedType(_, rname, _) if rname.isHkArgNameOLD && self1.typeParams.isEmpty =>
+      val inst = new InstMapOLD(self)
 
       def instTop(tp: Type): Type = tp.strictDealias match {
         case tp: RecType =>
@@ -480,12 +503,12 @@ class TypeApplications(val self: Type) extends AnyVal {
           tp.rebind(instTop(tp.parent))
         case tp @ RefinedType(parent, rname, rinfo) =>
           rinfo match {
-            case TypeAlias(TypeRef(RecThis(rt), sel)) if sel.isHkArgName && inst.localRecs.contains(rt) =>
+            case TypeAlias(TypeRef(RecThis(rt), sel)) if sel.isHkArgNameOLD && inst.localRecs.contains(rt) =>
               val bounds @ TypeBounds(_, _) = self.member(sel).info
               instTop(tp.derivedRefinedType(parent, rname, bounds.withBindingKind(NoBinding)))
             case _ =>
               val parent1 = instTop(parent)
-              if (rname.isHkArgName &&
+              if (rname.isHkArgNameOLD &&
                 !inst.tyconIsHK &&
                 !inst.keptRefs.contains(rname)) parent1
               else tp.derivedRefinedType(parent1, rname, inst(rinfo))
@@ -527,7 +550,7 @@ class TypeApplications(val self: Type) extends AnyVal {
    *  In that case we can look for parameterized base types of the type
    *  to eta expand them.
    */
-  def isEtaExpandable(implicit ctx: Context) = self match {
+  def isEtaExpandableOLD(implicit ctx: Context) = self match {
     case self: TypeRef => self.symbol.isClass
     case _ => false
   }
@@ -603,7 +626,14 @@ class TypeApplications(val self: Type) extends AnyVal {
     if (hkParams.isEmpty) self
     else {
       def adaptArg(arg: Type): Type = arg match {
-        case arg @ TypeLambda(tparamBounds, body) if
+        case arg @ TypeLambda(tparams, body) if
+             !tparams.corresponds(hkParams)(_.memberVariance == _.memberVariance) &&
+             tparams.corresponds(hkParams)(varianceConforms) =>
+          TypeLambda(tparams.map(_.memberName), hkParams.map(_.memberVariance))(
+            tl => arg.paramBounds.map(_.subst(arg, tl).bounds),
+            tl => arg.resultType.subst(arg, tl)
+          )
+        case arg @ TypeLambdaOLD(tparamBounds, body) if
              !arg.typeParams.corresponds(hkParams)(_.memberVariance == _.memberVariance) &&
              arg.typeParams.corresponds(hkParams)(varianceConforms) =>
           def adjustVariance(bounds: TypeBounds, tparam: MemberBinding): TypeBounds =
@@ -613,7 +643,7 @@ class TypeApplications(val self: Type) extends AnyVal {
             case _ => (x => tp)
           }
           val adjusted = (tparamBounds, hkParams).zipped.map(adjustVariance)
-          TypeLambda(adjusted.map(lift), lift(body))
+          TypeLambdaOLD(adjusted.map(lift), lift(body))
         case arg @ TypeAlias(alias) =>
           arg.derivedTypeAlias(adaptArg(alias))
         case arg @ TypeBounds(lo, hi) =>
@@ -641,22 +671,22 @@ class TypeApplications(val self: Type) extends AnyVal {
    *  3. If `T` is a polytype, instantiate it to `U1,...,Un`.
    */
   final def appliedTo(args: List[Type])(implicit ctx: Context): Type = /*>|>*/ track("appliedTo") /*<|<*/ {
-    def substHkArgs = new TypeMap {
-      def apply(tp: Type): Type = tp match {
-        case TypeRef(RecThis(rt), name) if rt.eq(self) && name.isHkArgName =>
-          args(name.hkArgIndex)
-        case _ =>
-          mapOver(tp)
-      }
-    }
     if (args.isEmpty || ctx.erasedTypes) self
-    else self.stripTypeVar match {
+    else self.stripTypeVar match { // TODO investigate why we can't do safeDealias here
+      case self: PolyType if !args.exists(_.isInstanceOf[TypeBounds]) =>
+        self.instantiate(args)
       case EtaExpansion(self1) =>
         self1.appliedTo(args)
-      case TypeLambda(_, body) if !args.exists(_.isInstanceOf[TypeBounds]) =>
+      case TypeLambdaOLD(_, body) if !args.exists(_.isInstanceOf[TypeBounds]) =>
+        def substHkArgs = new TypeMap {
+          def apply(tp: Type): Type = tp match {
+            case TypeRef(RecThis(rt), name) if rt.eq(self) && name.isHkArgNameOLD =>
+              args(name.hkArgIndexOLD)
+            case _ =>
+              mapOver(tp)
+          }
+        }
         substHkArgs(body)
-      case self: PolyType =>
-        self.instantiate(args)
       case self1 =>
         self1.safeDealias.appliedTo(args, typeParams)
     }
@@ -682,9 +712,10 @@ class TypeApplications(val self: Type) extends AnyVal {
       case nil => t
     }
     assert(args.nonEmpty)
-    matchParams(self, typParams, args) match {
-      case refined @ RefinedType(_, pname, _) if pname.isHkArgName =>
-        refined.betaReduce // TODO Move to matchparams
+    if (Config.newHK && self.isHK) AppliedType(self, args)
+    else matchParams(self, typParams, args) match {
+      case refined @ RefinedType(_, pname, _) if !Config.newHK && pname.isHkArgNameOLD =>
+        refined.betaReduceOLD
       case refined =>
         refined
     }
@@ -698,17 +729,25 @@ class TypeApplications(val self: Type) extends AnyVal {
    *  up hk type parameters matching the arguments. This is needed when unpickling
    *  Scala2 files such as `scala.collection.generic.Mapfactory`.
    */
-  final def safeAppliedTo(args: List[Type])(implicit ctx: Context) = {
-    val safeTypeParams = self match {
-      case self: TypeRef if !self.symbol.isClass && self.symbol.isCompleting =>
-        // This happens when unpickling e.g. scala$collection$generic$GenMapFactory$$CC
-        ctx.warning(i"encountered F-bounded higher-kinded type parameters for ${self.symbol}; assuming they are invariant")
-        fallbackTypeParams(args map alwaysZero)
-      case _ =>
-        typeParams
+  final def safeAppliedTo(args: List[Type])(implicit ctx: Context) =
+    if (Config.newHK)
+      self match {
+        case self: TypeRef if !self.symbol.isClass && self.symbol.isCompleting =>
+          AppliedType(self, args)
+        case _ =>
+          appliedTo(args, typeParams)
+      }
+    else {
+      val safeTypeParams = self match {
+        case self: TypeRef if !self.symbol.isClass && self.symbol.isCompleting =>
+          // This happens when unpickling e.g. scala$collection$generic$GenMapFactory$$CC
+          ctx.warning(i"encountered F-bounded higher-kinded type parameters for ${self.symbol}; assuming they are invariant")
+          fallbackTypeParamsOLD(args map alwaysZero)
+        case _ =>
+          typeParams
+      }
+      appliedTo(args, safeTypeParams)
     }
-    appliedTo(args, safeTypeParams)
-  }
 
   /** Turn this type, which is used as an argument for
    *  type parameter `tparam`, into a TypeBounds RHS
@@ -731,7 +770,10 @@ class TypeApplications(val self: Type) extends AnyVal {
    */
   final def baseArgInfos(base: Symbol)(implicit ctx: Context): List[Type] =
     if (self derivesFrom base)
-      base.typeParams map (param => self.member(param.name).info.argInfo)
+      self match {
+        case self: HKApply => self.upperBound.baseArgInfos(base)
+        case _ => base.typeParams.map(param => self.member(param.name).info.argInfo)
+      }
     else
       Nil
 
@@ -756,7 +798,10 @@ class TypeApplications(val self: Type) extends AnyVal {
   /** The first type argument of the base type instance wrt `base` of this type */
   final def firstBaseArgInfo(base: Symbol)(implicit ctx: Context): Type = base.typeParams match {
     case param :: _ if self derivesFrom base =>
-      self.member(param.name).info.argInfo
+      self match {
+        case self: HKApply => self.upperBound.firstBaseArgInfo(base)
+        case _ => self.member(param.name).info.argInfo
+      }
     case _ =>
       NoType
   }
@@ -778,6 +823,8 @@ class TypeApplications(val self: Type) extends AnyVal {
         tp.wrapIfMember(parent.baseTypeWithArgs(base))
       case tp: TermRef =>
         tp.underlying.baseTypeWithArgs(base)
+      case tp: HKApply =>
+        tp.upperBound.baseTypeWithArgs(base)
       case AndType(tp1, tp2) =>
         tp1.baseTypeWithArgs(base) & tp2.baseTypeWithArgs(base)
       case OrType(tp1, tp2) =>
@@ -832,12 +879,16 @@ class TypeApplications(val self: Type) extends AnyVal {
   /** The core type without any type arguments.
    *  @param `typeArgs` must be the type arguments of this type.
    */
-  final def withoutArgs(typeArgs: List[Type]): Type = typeArgs match {
-    case _ :: typeArgs1 =>
-      val RefinedType(tycon, _, _) = self
-      tycon.withoutArgs(typeArgs1)
-    case nil =>
-      self
+  final def withoutArgs(typeArgs: List[Type]): Type = self match {
+    case HKApply(tycon, args) => tycon
+    case _ =>
+      typeArgs match {
+        case _ :: typeArgs1 =>
+          val RefinedType(tycon, _, _) = self
+          tycon.withoutArgs(typeArgs1)
+        case nil =>
+          self
+      }
   }
 
   final def typeConstructor(implicit ctx: Context): Type = self.stripTypeVar match {
diff --git a/src/dotty/tools/dotc/core/TypeComparer.scala b/src/dotty/tools/dotc/core/TypeComparer.scala
index cf3086323..566865eb4 100644
--- a/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -365,11 +365,11 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
               fourthTry(tp1, tp2) || compareRefinedSlow
             case _ =>
               if (tp2.isTypeParam) {
-                compareHkLambda(tp1, tp2) ||
+                compareHkLambdaOLD(tp1, tp2) ||
                 fourthTry(tp1, tp2)
               }
               else {
-                compareHkApply(tp2, tp1, inOrder = false) ||
+                compareHkApplyOLD(tp2, tp1, inOrder = false) ||
                 compareRefinedSlow ||
                 fourthTry(tp1, tp2) ||
                 compareAliasedRefined(tp2, tp1, inOrder = false)
@@ -389,6 +389,53 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
           val tp1stable = ensureStableSingleton(tp1)
           isSubType(fixRecs(tp1stable, tp1stable.widenExpr), tp2.parent.substRecThis(tp2, tp1stable))
        }
+    case tp2 @ HKApply(tycon2, args2) =>
+      def compareHkApply(tycon2: Type): Boolean = tycon2 match {
+        case tycon2: TypeVar => compareHkApply(tycon2.underlying)
+        case param2: PolyParam if canConstrain(param2) =>
+          val tparams2 = tycon2.typeParams
+
+          def tyconOK(tycon1a: Type) =
+            variancesConform(tycon1a.typeParams, tparams2) && {
+              if (ctx.mode.is(Mode.TypevarsMissContext)) isSubType(tp1, tycon1a.appliedTo(args2))
+              else tryInstantiate(param2, tycon1a) && isSubType(tp1, tp2)
+            }
+
+          tp1 match {
+            case tp1 @ HKApply(tycon1, _) =>
+              tyconOK(tycon1) || isSubType(tp1.upperBound, tp2)
+            case _ if tp1.widenDealias.typeSymbol.isClass =>
+              val classBounds = tp2.classSymbols
+              def liftToBase(bcs: List[ClassSymbol]): Boolean = bcs match {
+                case bc :: bcs1 =>
+                  classBounds.exists(bc.derivesFrom) && tyconOK(tp1.baseTypeRef(bc)) ||
+                  liftToBase(bcs1)
+                case _ =>
+                  false
+              }
+              liftToBase(tp1.baseClasses)
+            case tp1: TypeProxy =>
+              isSubType(tp1.underlying, tp2)
+            case _ =>
+              false
+         }
+        case _ =>
+          // TODO handle lower bounds of hk params here
+          false
+        }
+      compareHkApply(tycon2) || fourthTry(tp1, tp2)
+    case tp2 @ TypeLambda(tparams2, body2) =>
+      def compareHkLambda = tp1.stripTypeVar match {
+        case tp1 @ TypeLambda(tparams1, body1) =>
+          val boundsConform =
+            tparams1.corresponds(tparams2)((tparam1, tparam2) =>
+              isSubType(tparam2.memberBounds.subst(tp2, tp1), tparam1.memberBounds))
+          val bodiesConform = isSubType(body1, body2.subst(tp2, tp1))
+          variancesConform(tparams1, tparams2) && boundsConform && bodiesConform
+        case _ =>
+          fourthTry(tp1, tp2)
+      }
+      compareHkLambda
     case OrType(tp21, tp22) =>
       // Rewrite T1 <: (T211 & T212) | T22 to T1 <: (T211 | T22) and T1 <: (T212 | T22)
       // and analogously for T1 <: T21 | (T221 & T222)
@@ -502,11 +549,22 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
       }
       isNewSubType(tp1.underlying.widenExpr, tp2) || comparePaths
     case tp1: RefinedType =>
-      compareHkApply(tp1, tp2, inOrder = true) ||
+      compareHkApplyOLD(tp1, tp2, inOrder = true) ||
       isNewSubType(tp1.parent, tp2) ||
       compareAliasedRefined(tp1, tp2, inOrder = true)
     case tp1: RecType =>
       isNewSubType(tp1.parent, tp2)
+    case HKApply(tycon1, args1) =>
+      tp2 match {
+        case AppliedType(tycon2, args2) =>
+          assert(!tycon2.isHK) // this should have been handled by thirdTry
+          isSubType(tycon1, EtaExpansion(tycon2)) &&
+          isSubArgs(args1, args2, tycon2.typeParams)
+        case _ =>
+          false
+      }
+    case EtaExpansion(tycon1) =>
+      isSubType(tycon1, tp2)
     case AndType(tp11, tp12) =>
       // Rewrite (T111 | T112) & T12 <: T2 to (T111 & T12) <: T2 and (T112 | T12) <: T2
       // and analogously for T11 & (T121 | T122) & T12 <: T2
@@ -537,6 +595,14 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
       false
   }
 
+  def isSubArgs(args1: List[Type], args2: List[Type], tparams: List[MemberBinding]): Boolean =
+    if (args1.isEmpty) args2.isEmpty
+    else args2.nonEmpty && {
+      val v = tparams.head.memberVariance
+      (v > 0 || isSubType(args2.head, args1.head)) &&
+      (v < 0 || isSubType(args1.head, args2.head))
+    }
+
   /** Test whether `tp1` has a base type of the form `B[T1, ..., Tn]` where
    *   - `B` derives from one of the class symbols of `tp2`,
    *   - the type parameters of `B` match one-by-one the variances of `tparams`,
@@ -588,7 +654,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
    *
    *   (4) If `inOrder`, test `app <: other` else test `other <: app`.
    */
-  def compareHkApply(app: RefinedType, other: Type, inOrder: Boolean): Boolean = {
+  def compareHkApplyOLD(app: RefinedType, other: Type, inOrder: Boolean): Boolean = {
     def tryInfer(tp: Type): Boolean = ctx.traceIndented(i"compareHK($app, $other, inOrder = $inOrder, constr = $tp)", subtyping) {
       tp match {
         case tp: TypeVar => tryInfer(tp.underlying)
@@ -597,7 +663,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
           def unifyWith(liftedOther: Type): Boolean = {
             subtyping.println(i"unify with $liftedOther")
             liftedOther.typeConstructor.widen match {
-              case tycon: TypeRef if tycon.isEtaExpandable && tycon.typeParams.nonEmpty =>
+              case tycon: TypeRef if tycon.isEtaExpandableOLD && tycon.typeParams.nonEmpty =>
                 val (ok, app1) =
                   if (ctx.mode.is(Mode.TypevarsMissContext))
                     (true, EtaExpansion(tycon).appliedTo(app.argInfos))
@@ -634,8 +700,8 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
           false
       }
     }
-    app.isHKApply && !other.isHKApply && {
-      val reduced = if (inOrder) app else app.normalizeHkApply
+    app.isHKApplyOLD && !other.isHKApplyOLD && {
+      val reduced = if (inOrder) app else app.normalizeHkApplyOLD
       if (reduced ne app)
         if (inOrder) isSubType(reduced, other) else isSubType(other, reduced)
       else tryInfer(app.typeConstructor.dealias)
@@ -643,11 +709,11 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
   }
 
   /** Compare type lambda with non-lambda type. */
-  def compareHkLambda(tp1: Type, tp2: RefinedType): Boolean = tp1.stripTypeVar match {
-    case TypeLambda(args1, body1) =>
+  def compareHkLambdaOLD(tp1: Type, tp2: RefinedType): Boolean = tp1.stripTypeVar match {
+    case TypeLambdaOLD(args1, body1) =>
       //println(i"comparing $tp1 <:< $tp2")
       tp2 match {
-        case TypeLambda(args2, body2) =>
+        case TypeLambdaOLD(args2, body2) =>
           args1.corresponds(args2)((arg1, arg2) =>
             varianceConforms(BindingKind.toVariance(arg1.bindingKind),
                               BindingKind.toVariance(arg2.bindingKind))) &&
@@ -656,7 +722,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
         case _ => false
       }
     case RefinedType(parent1, _, _) =>
-      compareHkLambda(parent1, tp2)
+      compareHkLambdaOLD(parent1, tp2)
     case _ =>
       false
   }
@@ -1161,22 +1227,36 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
     val tparams2 = tp2.typeParams
     if (tparams1.isEmpty || tparams2.isEmpty) op(tp1, tp2)
     else if (tparams1.length != tparams2.length) mergeConflict(tp1, tp2)
+    else if (Config.newHK) {
+      val numArgs = tparams1.length
+      def argRefs(tl: PolyType) = List.range(0, numArgs).map(PolyParam(tl, _))
+      TypeLambda(
+        paramNames = tpnme.syntheticLambdaParamNames(numArgs),
+        variances = (tparams1, tparams2).zipped.map((tparam1, tparam2) =>
+          (tparam1.memberVariance + tparam2.memberVariance) / 2))(
+        paramBoundsExp = tl => (tparams1, tparams2).zipped.map((tparam1, tparam2) =>
+          tl.lifted(tparams1, tparam1.memberBoundsAsSeenFrom(tp1)).bounds &
+          tl.lifted(tparams2, tparam2.memberBoundsAsSeenFrom(tp2)).bounds),
+        resultTypeExp = tl =>
+          op(tl.lifted(tparams1, tp1).appliedTo(argRefs(tl)),
+             tl.lifted(tparams2, tp2).appliedTo(argRefs(tl))))
+    }
     else {
       val bindings: List[RecType => TypeBounds] =
         (tparams1, tparams2).zipped.map { (tparam1, tparam2) =>
           val b1: RecType => TypeBounds =
-            tparam1.memberBoundsAsSeenFrom(tp1).recursify(tparams1)
+            tparam1.memberBoundsAsSeenFrom(tp1).recursifyOLD(tparams1)
           val b2: RecType => TypeBounds =
-            tparam2.memberBoundsAsSeenFrom(tp2).recursify(tparams2)
+            tparam2.memberBoundsAsSeenFrom(tp2).recursifyOLD(tparams2)
           (rt: RecType) => (b1(rt) & b2(rt))
             .withBindingKind(
               BindingKind.fromVariance(
                 (tparam1.memberVariance + tparam2.memberVariance) / 2))
         }
-      val app1: RecType => Type = rt => tp1.appliedTo(argRefs(rt, tparams1.length))
-      val app2: RecType => Type = rt => tp2.appliedTo(argRefs(rt, tparams2.length))
+      val app1: RecType => Type = rt => tp1.appliedTo(argRefsOLD(rt, tparams1.length))
+      val app2: RecType => Type = rt => tp2.appliedTo(argRefsOLD(rt, tparams2.length))
       val body: RecType => Type = rt => op(app1(rt), app2(rt))
-      TypeLambda(bindings, body)
+      TypeLambdaOLD(bindings, body)
     }
   }
 
@@ -1459,19 +1539,19 @@ class ExplainingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
 
   override def copyIn(ctx: Context) = new ExplainingTypeComparer(ctx)
 
-  override def compareHkApply(app: RefinedType, other: Type, inOrder: Boolean) =
-    if (app.isHKApply)
-      traceIndented(i"compareHkApply $app, $other, $inOrder, ${app.normalizeHkApply}") {
-        super.compareHkApply(app, other, inOrder)
+  override def compareHkApplyOLD(app: RefinedType, other: Type, inOrder: Boolean) =
+    if (app.isHKApplyOLD)
+      traceIndented(i"compareHkApply $app, $other, $inOrder, ${app.normalizeHkApplyOLD}") {
+        super.compareHkApplyOLD(app, other, inOrder)
       }
-    else super.compareHkApply(app, other, inOrder)
+    else super.compareHkApplyOLD(app, other, inOrder)
 
-  override def compareHkLambda(tp1: Type, tp2: RefinedType): Boolean =
+  override def compareHkLambdaOLD(tp1: Type, tp2: RefinedType): Boolean =
     if (tp2.isTypeParam)
       traceIndented(i"compareHkLambda $tp1, $tp2") {
-        super.compareHkLambda(tp1, tp2)
+        super.compareHkLambdaOLD(tp1, tp2)
       }
-    else super.compareHkLambda(tp1, tp2)
+    else super.compareHkLambdaOLD(tp1, tp2)
 
   override def toString = "Subtype trace:" + { try b.toString finally b.clear() }
 }
diff --git a/src/dotty/tools/dotc/core/TypeErasure.scala b/src/dotty/tools/dotc/core/TypeErasure.scala
index a5aabe9c4..c71726a3e 100644
--- a/src/dotty/tools/dotc/core/TypeErasure.scala
+++ b/src/dotty/tools/dotc/core/TypeErasure.scala
@@ -356,6 +356,8 @@ class TypeErasure(isJava: Boolean, semiEraseVCs: Boolean, isConstructor: Boolean
         case rt =>
           tp.derivedMethodType(tp.paramNames, formals, rt)
       }
+    case tp: TypeLambda =>
+      this(tp.resultType)
     case tp: PolyType =>
       this(tp.resultType) match {
         case rt: MethodType => rt
diff --git a/src/dotty/tools/dotc/core/TypeOps.scala b/src/dotty/tools/dotc/core/TypeOps.scala
index 6b75b574e..9019df6b7 100644
--- a/src/dotty/tools/dotc/core/TypeOps.scala
+++ b/src/dotty/tools/dotc/core/TypeOps.scala
@@ -158,7 +158,7 @@ trait TypeOps { this: Context => // TODO: Make standalone object.
       tp
     case tp: RefinedType =>
       tp.derivedRefinedType(simplify(tp.parent, theMap), tp.refinedName, simplify(tp.refinedInfo, theMap))
-        .normalizeHkApply
+        .normalizeHkApplyOLD
     case tp: TypeAlias =>
       tp.derivedTypeAlias(simplify(tp.alias, theMap))
     case AndType(l, r) =>
@@ -384,7 +384,7 @@ trait TypeOps { this: Context => // TODO: Make standalone object.
     var formals: SimpleMap[TypeName, Symbol] = SimpleMap.Empty // A map of all formal parent parameter
 
     // Strip all refinements from parent type, populating `refinements` and `formals` maps.
-    def normalizeToRef(tp: Type): TypeRef = tp.dealias.normalizeHkApply match {
+    def normalizeToRef(tp: Type): TypeRef = tp.dealias.normalizeHkApplyOLD match {
       case tp: TypeRef =>
         tp
       case tp @ RefinedType(tp1, name: TypeName, rinfo) =>
diff --git a/src/dotty/tools/dotc/core/Types.scala b/src/dotty/tools/dotc/core/Types.scala
index cd1b5739d..8d152a616 100644
--- a/src/dotty/tools/dotc/core/Types.scala
+++ b/src/dotty/tools/dotc/core/Types.scala
@@ -56,6 +56,7 @@ object Types {
    *        |              +- PolyParam
    *        |              +- RefinedOrRecType -+-- RefinedType
    *        |              |                   -+-- RecType
+   *        |              +- HKApply
    *        |              +- TypeBounds
    *        |              +- ExprType
    *        |              +- AnnotatedType
@@ -65,8 +66,8 @@ object Types {
    *                       +- OrType
    *                       +- MethodType -----+- ImplicitMethodType
    *                       |                  +- JavaMethodType
-   *                       +- PolyType
    *                       +- ClassInfo
+   *                       +- PolyType --------- TypeLambda
    *                       |
    *                       +- NoType
    *                       +- NoPrefix
@@ -476,7 +477,8 @@ object Types {
           // twice during findMember which risks picking the wrong prefix in the `substRecThis(rt, pre)`
           // call below. To avoid this problem we do a defensive copy of the recursive
           // type first. But if we do this always we risk being inefficient and we run into
-          // stackoverflows when compiling pos/hk.scala. So we only do a copy if the type
+          // stackoverflows when compiling pos/hk.scala under the refinement encoding
+          // of hk-types. So we only do a copy if the type
           // is visited again in a recursive call to `findMember`, as tracked by `tp.opened`.
           // Furthermore, if this happens we mark the original recursive type with `openedTwice`
           // which means that we always defensively copy the type in the future. This second
@@ -893,7 +895,7 @@ object Types {
       case _ => this
     }
 
-    /** If this is a TypeAlias type, its alias otherwise this type itself */
+    /** If this is a TypeAlias type, its alias, otherwise this type itself */
     final def followTypeAlias(implicit ctx: Context): Type = this match {
       case TypeAlias(alias) => alias
       case _ => this
@@ -1326,8 +1328,14 @@ object Types {
   /** A marker trait for types that apply only to type symbols */
   trait TypeType extends Type
 
-  /** A marker trait for types that apply only to term symbols */
-  trait TermType extends Type
+  /** A marker trait for types that apply only to term symbols or that
+   *  represent higher-kinded types.
+   */
+  trait TermOrHkType extends Type
+
+  /** A marker trait for types that apply only to term symbols.
+   */
+  trait TermType extends TermOrHkType
 
   /** A marker trait for types that can be types of values or prototypes of value types */
   trait ValueTypeOrProto extends TermType
@@ -1568,6 +1576,7 @@ object Types {
       // we might now get cycles over members that are in a refinement but that lack
       // a symbol. Without the following precaution i974.scala stackoverflows when compiled
       // with new hk scheme.
+      // TODO: Do we still need the complications here?
       val savedDenot = lastDenotation
       val savedSymbol = lastSymbol
       if (prefix.isInstanceOf[RecThis] && name.isTypeName) {
@@ -1765,7 +1774,7 @@ object Types {
 
     override def underlying(implicit ctx: Context): Type = {
       val res = info
-      assert(res != this, this)
+      assert(res != this, this)  // TODO drop
       res
     }
   }
@@ -2076,8 +2085,8 @@ object Types {
       this
     }
 
-    def betaReduce(implicit ctx: Context): Type = refinedInfo match {
-      case TypeAlias(alias) if refinedName.isHkArgName =>
+    def betaReduceOLD(implicit ctx: Context): Type = refinedInfo match {
+      case TypeAlias(alias) if refinedName.isHkArgNameOLD =>
         def instantiate(rt: RecType) = new TypeMap {
           def apply(t: Type) = t match {
             case TypeRef(RecThis(`rt`), `refinedName`) => alias
@@ -2121,7 +2130,7 @@ object Types {
         // A Y-check error (incompatible types involving hk lambdas) for dotty itself.
         // TODO: investigate and, if possible, drop after revision.
         val normalizedRefinedInfo = refinedInfo.substRecThis(dummyRec, dummyRec)
-        RefinedType(parent, refinedName, normalizedRefinedInfo).betaReduce
+        RefinedType(parent, refinedName, normalizedRefinedInfo).betaReduceOLD
       }
 
     /** Add this refinement to `parent`, provided If `refinedName` is a member of `parent`. */
@@ -2130,6 +2139,7 @@ object Types {
       else parent
 
     // MemberBinding methods
+    // TODO: Needed?
     def isTypeParam(implicit ctx: Context) = refinedInfo match {
       case tp: TypeBounds => tp.isBinding
       case _ => false
@@ -2563,7 +2573,7 @@ object Types {
   }
 
   abstract case class PolyType(paramNames: List[TypeName])(paramBoundsExp: PolyType => List[TypeBounds], resultTypeExp: PolyType => Type)
-    extends CachedGroundType with BindingType with TermType with MethodOrPoly {
+    extends CachedGroundType with BindingType with TermOrHkType with MethodOrPoly {
 
     val paramBounds = paramBoundsExp(this)
     val resType = resultTypeExp(this)
@@ -2572,6 +2582,9 @@ object Types {
 
     override def resultType(implicit ctx: Context) = resType
 
+    /** If this is a type lambda, the variances of its parameters, otherwise Nil.*/
+    def variances: List[Int] = Nil
+
     protected def computeSignature(implicit ctx: Context) = resultSignature
 
     def isPolymorphicMethodType: Boolean = resType match {
@@ -2590,17 +2603,33 @@ object Types {
       else duplicate(paramNames, paramBounds, resType)
 
     def duplicate(paramNames: List[TypeName] = this.paramNames, paramBounds: List[TypeBounds] = this.paramBounds, resType: Type)(implicit ctx: Context) =
-      PolyType(paramNames)(
+      if (this.variances.isEmpty)
+        PolyType(paramNames)(
           x => paramBounds mapConserve (_.subst(this, x).bounds),
           x => resType.subst(this, x))
+      else
+        TypeLambda(paramNames, variances)(
+          x => paramBounds mapConserve (_.subst(this, x).bounds),
+          x => resType.subst(this, x))
+
+    def lifted(tparams: List[MemberBinding], t: Type)(implicit ctx: Context): Type =
+      tparams match {
+        case LambdaParam(poly, _) :: _ =>
+          t.subst(poly, this)
+        case tparams: List[Symbol] =>
+          t.subst(tparams, tparams.indices.toList.map(PolyParam(this, _)))
+      }
 
     override def equals(other: Any) = other match {
       case other: PolyType =>
-        other.paramNames == this.paramNames && other.paramBounds == this.paramBounds && other.resType == this.resType
+        other.paramNames == this.paramNames &&
+        other.paramBounds == this.paramBounds &&
+        other.resType == this.resType &&
+        other.variances == this.variances
       case _ => false
     }
     override def computeHash = {
-      doHash(paramNames, resType, paramBounds)
+      doHash(variances ::: paramNames, resType, paramBounds)
     }
 
     override def toString = s"PolyType($paramNames, $paramBounds, $resType)"
@@ -2616,13 +2645,75 @@ object Types {
 
     def fromSymbols(tparams: List[Symbol], resultType: Type)(implicit ctx: Context) =
       if (tparams.isEmpty) resultType
-      else {
-        def transform(pt: PolyType, tp: Type) =
-          tp.subst(tparams, (0 until tparams.length).toList map (PolyParam(pt, _)))
-        apply(tparams map (_.name.asTypeName))(
-          pt => tparams map (tparam => transform(pt, tparam.info).bounds),
-          pt => transform(pt, resultType))
+      else apply(tparams map (_.name.asTypeName))(
+          pt => tparams.map(tparam => pt.lifted(tparams, tparam.info).bounds),
+          pt => pt.lifted(tparams, resultType))
+  }
+
+  // ----- HK types: TypeLambda, LambdaParam, HKApply ---------------------
+
+  /** A type lambda of the form `[v_0 X_0, ..., v_n X_n] => T` */
+  class TypeLambda(paramNames: List[TypeName], variances: List[Int])(paramBoundsExp: PolyType => List[TypeBounds], resultTypeExp: PolyType => Type)
+  extends PolyType(paramNames)(paramBoundsExp, resultTypeExp) {
+
+    lazy val typeParams: List[LambdaParam] =
+      paramNames.indices.toList.map(new LambdaParam(this, _))
+
+    override def toString = s"TypeLambda($variances, $paramNames, $paramBounds, $resType)"
+
+  }
+
+  /** The parameter of a type lambda */
+  case class LambdaParam(tl: TypeLambda, n: Int) extends MemberBinding {
+    def isTypeParam(implicit ctx: Context) = true
+    def memberName(implicit ctx: Context): TypeName = tl.paramNames(n)
+    def memberBounds(implicit ctx: Context): TypeBounds = tl.paramBounds(n)
+    def memberBoundsAsSeenFrom(pre: Type)(implicit ctx: Context): TypeBounds = memberBounds
+    def memberVariance(implicit ctx: Context): Int = tl.variances(n)
+    def toArg: Type = PolyParam(tl, n)
+  }
+
+  object TypeLambda {
+    def apply(paramNames: List[TypeName], variances: List[Int])(paramBoundsExp: PolyType => List[TypeBounds], resultTypeExp: PolyType => Type)(implicit ctx: Context): PolyType = {
+      unique(new TypeLambda(paramNames, variances)(paramBoundsExp, resultTypeExp))
+    }
+    def fromSymbols(tparams: List[Symbol], resultType: Type)(implicit ctx: Context) =
+      if (tparams.isEmpty) resultType
+      else apply(tparams map (_.name.asTypeName), tparams.map(_.variance))(
+          pt => tparams.map(tparam => pt.lifted(tparams, tparam.info).bounds),
+          pt => pt.lifted(tparams, resultType))
+     def unapply(tl: TypeLambda): Some[(List[LambdaParam], Type)] =
+      Some((tl.typeParams, tl.resType))
+  }
+
+  /** A higher kinded type application `C[T_1, ..., T_n]` */
+  abstract case class HKApply(tycon: Type, args: List[Type])
+  extends CachedProxyType with TermOrHkType {
+    override def underlying(implicit ctx: Context): Type = tycon
+    def derivedAppliedType(tycon: Type, args: List[Type])(implicit ctx: Context): Type =
+      if ((tycon eq this.tycon) && (args eq this.args)) this
+      else tycon.appliedTo(args)
+    override def computeHash = doHash(tycon, args)
+
+    def upperBound(implicit ctx: Context): Type = tycon.stripTypeVar match {
+      case tp: TypeProxy => tp.underlying.appliedTo(args)
+      case _ => tycon
+    }
+
+    protected def checkInst(implicit ctx: Context): this.type = {
+      tycon.stripTypeVar match {
+        case _: TypeRef | _: PolyParam | _: WildcardType | ErrorType =>
+        case _ => assert(false, s"illegal type constructor in $this")
       }
+      this
+    }
+  }
+
+  final class CachedHKApply(tycon: Type, args: List[Type]) extends HKApply(tycon, args)
+
+  object HKApply {
+    def apply(tycon: Type, args: List[Type])(implicit ctx: Context) =
+      unique(new CachedHKApply(tycon, args)).checkInst
   }
 
   // ----- Bound types: MethodParam, PolyParam --------------------------
@@ -3021,8 +3112,8 @@ object Types {
    */
   abstract case class TypeBounds(lo: Type, hi: Type)(val bindingKind: BindingKind) extends CachedProxyType with TypeType {
 
-    assert(lo.isInstanceOf[TermType])
-    assert(hi.isInstanceOf[TermType])
+    assert(lo.isInstanceOf[TermOrHkType])
+    assert(hi.isInstanceOf[TermOrHkType])
 
     def variance: Int = 0
     def isBinding = bindingKind != NoBinding
@@ -3151,6 +3242,7 @@ object Types {
   /** A value class defining the interpretation of a TypeBounds
    *  as either a regular type bounds or a binding (i.e. introduction) of a
    *  higher-kinded type parameter.
+   *  TODO: drop
    */
   class BindingKind(val n: Byte) extends AnyVal {
     def join(that: BindingKind) =
@@ -3225,7 +3317,7 @@ object Types {
   object ErrorType extends ErrorType
 
   /** Wildcard type, possibly with bounds */
-  abstract case class WildcardType(optBounds: Type) extends CachedGroundType with TermType {
+  abstract case class WildcardType(optBounds: Type) extends CachedGroundType with TermOrHkType {
     def derivedWildcardType(optBounds: Type)(implicit ctx: Context) =
       if (optBounds eq this.optBounds) this
       else if (!optBounds.exists) WildcardType
@@ -3323,6 +3415,8 @@ object Types {
       tp.derivedTypeBounds(lo, hi)
     protected def derivedSuperType(tp: SuperType, thistp: Type, supertp: Type): Type =
       tp.derivedSuperType(thistp, supertp)
+    protected def derivedAppliedType(tp: HKApply, tycon: Type, args: List[Type]): Type =
+      tp.derivedAppliedType(tycon, args)
     protected def derivedAndOrType(tp: AndOrType, tp1: Type, tp2: Type): Type =
       tp.derivedAndOrType(tp1, tp2)
     protected def derivedAnnotatedType(tp: AnnotatedType, underlying: Type, annot: Annotation): Type =
@@ -3405,6 +3499,17 @@ object Types {
           val inst = tp.instanceOpt
           if (inst.exists) apply(inst) else tp
 
+        case tp: HKApply =>
+          def mapArg(arg: Type, tparam: MemberBinding): Type = {
+            val saved = variance
+            if (tparam.memberVariance < 0) variance = -variance
+            else if (tparam.memberVariance == 0) variance = 0
+            try this(arg)
+            finally variance = saved
+          }
+          derivedAppliedType(tp, this(tp.tycon),
+              tp.args.zipWithConserve(tp.tycon.typeParams)(mapArg))
+
         case tp: AndOrType =>
           derivedAndOrType(tp, this(tp.tp1), this(tp.tp2))
 
@@ -3508,6 +3613,9 @@ object Types {
     override protected def derivedSuperType(tp: SuperType, thistp: Type, supertp: Type) =
       if (thistp.exists && supertp.exists) tp.derivedSuperType(thistp, supertp)
       else NoType
+    override protected def derivedAppliedType(tp: HKApply, tycon: Type, args: List[Type]): Type =
+      if (tycon.exists && args.forall(_.exists)) tp.derivedAppliedType(tycon, args)
+      else approx() // This is rather coarse, but to do better is a bit complicated
     override protected def derivedAndOrType(tp: AndOrType, tp1: Type, tp2: Type) =
       if (tp1.exists && tp2.exists) tp.derivedAndOrType(tp1, tp2)
       else if (tp.isAnd) approx(hi = tp1 & tp2)  // if one of tp1d, tp2d exists, it is the result of tp1d & tp2d
@@ -3600,6 +3708,9 @@ object Types {
       case tp @ ClassInfo(prefix, _, _, _, _) =>
         this(x, prefix)
 
+      case tp @ HKApply(tycon, args) =>
+        foldOver(this(x, tycon), args)
+
       case tp: AndOrType =>
         this(this(x, tp.tp1), tp.tp2)
 
diff --git a/src/dotty/tools/dotc/core/tasty/TastyFormat.scala b/src/dotty/tools/dotc/core/tasty/TastyFormat.scala
index 38d55e0e8..b23ee5aba 100644
--- a/src/dotty/tools/dotc/core/tasty/TastyFormat.scala
+++ b/src/dotty/tools/dotc/core/tasty/TastyFormat.scala
@@ -138,6 +138,7 @@ Standard-Section: "ASTs" TopLevelStat*
                   BIND           Length boundName_NameRef bounds_Type
                                         // for type-variables defined in a type pattern
                   BYNAMEtype            underlying_Type
+                  LAMBDAtype     Length result_Type NamesTypes      // variance encoded in front of name: +/-/=
                   POLYtype       Length result_Type NamesTypes      // needed for refinements
                   METHODtype     Length result_Type NamesTypes      // needed for refinements
                   PARAMtype      Length binder_ASTref paramNum_Nat  // needed for refinements
@@ -326,7 +327,8 @@ object TastyFormat {
   final val ORtype = 172
   final val METHODtype = 174
   final val POLYtype = 175
-  final val PARAMtype = 176
+  final val LAMBDAtype = 176
+  final val PARAMtype = 177
   final val ANNOTATION = 178
 
   final val firstSimpleTreeTag = UNITconst
@@ -500,4 +502,8 @@ object TastyFormat {
     case TYPEBOUNDS => -2
     case _ => 0
   }
+
+  /** Map between variances and name prefixes */
+  val varianceToPrefix = Map(-1 -> '-', 0 -> '=', 1 -> '+')
+  val prefixToVariance = Map('-' -> -1, '=' -> 0, '+' -> 1)
 }
diff --git a/src/dotty/tools/dotc/core/tasty/TreePickler.scala b/src/dotty/tools/dotc/core/tasty/TreePickler.scala
index d6e6c4d6b..f604bff62 100644
--- a/src/dotty/tools/dotc/core/tasty/TreePickler.scala
+++ b/src/dotty/tools/dotc/core/tasty/TreePickler.scala
@@ -254,6 +254,11 @@ class TreePickler(pickler: TastyPickler) {
     case tpe: ExprType =>
       writeByte(BYNAMEtype)
       pickleType(tpe.underlying)
+    case tpe: TypeLambda =>
+      writeByte(LAMBDAtype)
+      val paramNames = tpe.typeParams.map(tparam =>
+        varianceToPrefix(tparam.memberVariance) +: tparam.memberName)
+      pickleMethodic(tpe.resultType, paramNames, tpe.paramBounds)
     case tpe: MethodType if richTypes =>
       writeByte(METHODtype)
       pickleMethodic(tpe.resultType, tpe.paramNames, tpe.paramTypes)
diff --git a/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala b/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala
index 2d230c630..6f0596ac0 100644
--- a/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala
+++ b/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala
@@ -287,6 +287,15 @@ class TreeUnpickler(reader: TastyReader, tastyName: TastyName.Table) {
               val sym = ctx.newSymbol(ctx.owner, readName().toTypeName, BindDefinedType, readType())
               registerSym(start, sym)
               TypeRef.withFixedSym(NoPrefix, sym.name, sym)
+            case LAMBDAtype =>
+              val (rawNames, paramReader) = readNamesSkipParams[TypeName]
+              val (variances, paramNames) = rawNames
+                .map(name => (prefixToVariance(name.head), name.tail.asTypeName)).unzip
+              val result = TypeLambda(paramNames, variances)(
+                pt => registeringType(pt, paramReader.readParamTypes[TypeBounds](end)),
+                pt => readType())
+              goto(end)
+              result
             case POLYtype =>
               val (names, paramReader) = readNamesSkipParams[TypeName]
               val result = PolyType(names)(
diff --git a/src/dotty/tools/dotc/printing/PlainPrinter.scala b/src/dotty/tools/dotc/printing/PlainPrinter.scala
index a8888fd3c..07819ef77 100644
--- a/src/dotty/tools/dotc/printing/PlainPrinter.scala
+++ b/src/dotty/tools/dotc/printing/PlainPrinter.scala
@@ -6,6 +6,7 @@ import Texts._, Types._, Flags._, Names._, Symbols._, NameOps._, Constants._, De
 import Contexts.Context, Scopes.Scope, Denotations.Denotation, Annotations.Annotation
 import StdNames.{nme, tpnme}
 import ast.Trees._, ast._
+import config.Config
 import java.lang.Integer.toOctalString
 import config.Config.summarizeDepth
 import scala.annotation.switch
@@ -50,8 +51,8 @@ class PlainPrinter(_ctx: Context) extends Printer {
           homogenize(tp1) & homogenize(tp2)
         case OrType(tp1, tp2) =>
           homogenize(tp1) | homogenize(tp2)
-        case tp: RefinedType =>
-          tp.normalizeHkApply
+        case tp: RefinedType if !Config.newHK =>
+          tp.normalizeHkApplyOLD
         case tp: SkolemType =>
           homogenize(tp.info)
         case tp: LazyRef =>
@@ -110,6 +111,30 @@ class PlainPrinter(_ctx: Context) extends Printer {
   protected def toTextRefinement(rt: RefinedType) =
     (refinementNameString(rt) ~ toTextRHS(rt.refinedInfo)).close
 
+  protected def argText(arg: Type): Text = arg match {
+    case arg: TypeBounds => "_" ~ toTextGlobal(arg)
+    case _ => toTextGlobal(arg)
+  }
+
+  /** The text for a TypeLambda
+   *
+   *     [v_1 p_1: B_1, ..., v_n p_n: B_n] -> T
+   *
+   *  where
+   *  @param  paramNames  = p_1, ..., p_n
+   *  @param  variances   = v_1, ..., v_n
+   *  @param  argBoundss  = B_1, ..., B_n
+   *  @param  body        = T
+   */
+  protected def typeLambdaText(paramNames: List[String], variances: List[Int], argBoundss: List[TypeBounds], body: Type): Text = {
+    def lambdaParamText(variance: Int, name: String, bounds: TypeBounds): Text =
+      varianceString(variance) ~ name ~ toText(bounds)
+    changePrec(GlobalPrec) {
+      "[" ~ Text((variances, paramNames, argBoundss).zipped.map(lambdaParamText), ", ") ~
+      "] -> " ~ toTextGlobal(body)
+    }
+  }
+
   /** The longest sequence of refinement types, starting at given type
    *  and following parents.
    */
@@ -174,6 +199,10 @@ class PlainPrinter(_ctx: Context) extends Printer {
         toText(polyParamName(pt.paramNames(n))) ~ polyHash(pt)
       case AnnotatedType(tpe, annot) =>
         toTextLocal(tpe) ~ " " ~ toText(annot)
+      case tp: TypeLambda =>
+        typeLambdaText(tp.paramNames.map(_.toString), tp.variances, tp.paramBounds, tp.resultType)
+      case HKApply(tycon, args) =>
+        toTextLocal(tycon) ~ "[!" ~ Text(args.map(argText), ", ") ~ "]"
       case tp: TypeVar =>
         if (tp.isInstantiated)
           toTextLocal(tp.instanceOpt) ~ "'" // debug for now, so that we can see where the TypeVars are.
@@ -186,7 +215,7 @@ class PlainPrinter(_ctx: Context) extends Printer {
           else toText(tp.origin)
         }
       case tp: LazyRef =>
-        "LazyRef(" ~ toTextGlobal(tp.ref) ~ ")"
+        "LazyRef(" ~ toTextGlobal(tp.ref) ~ ")" // TODO: only print this during debug mode?
       case _ =>
         tp.fallbackToText(this)
     }
diff --git a/src/dotty/tools/dotc/printing/RefinedPrinter.scala b/src/dotty/tools/dotc/printing/RefinedPrinter.scala
index 3da977b31..91f896da2 100644
--- a/src/dotty/tools/dotc/printing/RefinedPrinter.scala
+++ b/src/dotty/tools/dotc/printing/RefinedPrinter.scala
@@ -95,10 +95,6 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
     }
 
   override def toText(tp: Type): Text = controlled {
-    def argText(arg: Type): Text = arg match {
-      case arg: TypeBounds => "_" ~ toTextGlobal(arg)
-      case _ => toTextGlobal(arg)
-    }
     def toTextTuple(args: List[Type]): Text =
       "(" ~ toTextGlobal(args, ", ") ~ ")"
     def toTextFunction(args: List[Type]): Text =
@@ -117,7 +113,7 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
         if (defn.isFunctionClass(cls)) return toTextFunction(args)
         if (defn.isTupleClass(cls)) return toTextTuple(args)
         return (toTextLocal(tycon) ~ "[" ~ Text(args map argText, ", ") ~ "]").close
-      case tp @ TypeLambda(argBoundss, body) =>
+      case tp @ TypeLambdaOLD(argBoundss, body) =>
         val variances = argBoundss.map(b => BindingKind.toVariance(b.bindingKind))
         val prefix = ((('X' - 'A') + lambdaNestingLevel) % 26 + 'A').toChar
         val paramNames = argBoundss.indices.toList.map(prefix.toString + _)
@@ -130,13 +126,13 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
               }
             }
           def apply(t: Type): Type = t match {
-            case TypeRef(RecThis(rt), name) if name.isHkArgName && contains(tp, rt) =>
+            case TypeRef(RecThis(rt), name) if name.isHkArgNameOLD && contains(tp, rt) =>
               // Make up a name that prints as "Xi". Need to be careful we do not
               // accidentally unique-hash to something else. That's why we can't
               // use prefix = NoPrefix or a WithFixedSym instance.
               TypeRef.withSymAndName(
                 defn.EmptyPackageClass.thisType, defn.AnyClass,
-                paramNames(name.hkArgIndex).toTypeName)
+                paramNames(name.hkArgIndexOLD).toTypeName)
             case _ =>
               mapOver(t)
           }
@@ -186,25 +182,6 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
   def blockText[T >: Untyped](trees: List[Tree[T]]): Text =
     "{" ~ toText(trees, "\n") ~ "}"
 
-  /** The text for a TypeLambda
-   *
-   *     [v_1 p_1: B_1, ..., v_n p_n: B_n] -> T
-   *
-   *  where
-   *  @param  paramNames  = p_1, ..., p_n
-   *  @param  variances   = v_1, ..., v_n
-   *  @param  argBoundss  = B_1, ..., B_n
-   *  @param  body        = T
-   */
-  def typeLambdaText(paramNames: List[String], variances: List[Int], argBoundss: List[TypeBounds], body: Type): Text = {
-    def lambdaParamText(variance: Int, name: String, bounds: TypeBounds): Text =
-      varianceString(variance) ~ name ~ toText(bounds)
-    changePrec(GlobalPrec) {
-      "[" ~ Text((variances, paramNames, argBoundss).zipped.map(lambdaParamText), ", ") ~
-      "] -> " ~ toTextGlobal(body)
-    }
-  }
-
   override def toText[T >: Untyped](tree: Tree[T]): Text = controlled {
 
     import untpd.{modsDeco => _, _}
diff --git a/src/dotty/tools/dotc/typer/TypeAssigner.scala b/src/dotty/tools/dotc/typer/TypeAssigner.scala
index 3f3108ac2..27cc0e6f5 100644
--- a/src/dotty/tools/dotc/typer/TypeAssigner.scala
+++ b/src/dotty/tools/dotc/typer/TypeAssigner.scala
@@ -4,9 +4,10 @@ package typer
 
 import core._
 import ast._
+import config.Config.newHK
 import Scopes._, Contexts._, Constants._, Types._, Symbols._, Names._, Flags._, Decorators._
 import ErrorReporting._, Annotations._, Denotations._, SymDenotations._, StdNames._, TypeErasure._
-import TypeApplications.AppliedType
+import TypeApplications.{AppliedType, TypeLambdaOLD}
 import util.Positions._
 import config.Printers._
 import ast.Trees._
@@ -426,14 +427,16 @@ trait TypeAssigner {
     tree.withType(ownType)
   }
 
-  def assignType(tree: untpd.TypeLambdaTree, tparamDefs: List[TypeDef], body: Tree)(implicit ctx: Context) = {
-    val tparams = tparamDefs.map(_.symbol)
-    val argBindingFns = tparams.map(tparam =>
-      tparam.info.bounds
-        .withBindingKind(BindingKind.fromVariance(tparam.variance))
-        .recursify(tparams))
-    val bodyFn = body.tpe.recursify(tparams)
-    tree.withType(TypeApplications.TypeLambda(argBindingFns, bodyFn))
+  def assignType(tree: untpd.TypeLambdaTree, tparamDefs: List[TypeDef], body: Tree)(implicit ctx: Context) =
+    if (newHK) tree.withType(TypeLambda.fromSymbols(tparamDefs.map(_.symbol), body.tpe))
+    else {
+      val tparams = tparamDefs.map(_.symbol)
+      val argBindingFns = tparams.map(tparam =>
+        tparam.info.bounds
+          .withBindingKind(BindingKind.fromVariance(tparam.variance))
+          .recursifyOLD(tparams))
+      val bodyFn = body.tpe.recursifyOLD(tparams)
+      tree.withType(TypeLambdaOLD(argBindingFns, bodyFn))
   }
 
   def assignType(tree: untpd.ByNameTypeTree, result: Tree)(implicit ctx: Context) =
diff --git a/src/dotty/tools/dotc/typer/Variances.scala b/src/dotty/tools/dotc/typer/Variances.scala
index e88423f98..9af11a0f4 100644
--- a/src/dotty/tools/dotc/typer/Variances.scala
+++ b/src/dotty/tools/dotc/typer/Variances.scala
@@ -83,6 +83,17 @@ object Variances {
       flip(varianceInTypes(paramTypes)(tparam)) & varianceInType(tp.resultType)(tparam)
     case ExprType(restpe) =>
       varianceInType(restpe)(tparam)
+    case tp @ HKApply(tycon, args) =>
+      def varianceInArgs(v: Variance, args: List[Type], tparams: List[MemberBinding]): Variance =
+        args match {
+          case arg :: args1 =>
+            varianceInArgs(
+              v & compose(varianceInType(arg)(tparam), tparams.head.memberVariance),
+              args1, tparams.tail)
+          case nil =>
+            v
+        }
+      varianceInArgs(varianceInType(tycon)(tparam), args, tycon.typeParams)
     case tp @ PolyType(_) =>
       flip(varianceInTypes(tp.paramBounds)(tparam)) & varianceInType(tp.resultType)(tparam)
     case AnnotatedType(tp, annot) =>