merged in tcpoly branch (at r10641)

31 files changed, 954 insertions, 537 deletions

diff --git a/src/compiler/scala/tools/nsc/Global.scala b/src/compiler/scala/tools/nsc/Global.scala
index 8743a4d73e..b78bcb9edc 100644
--- a/src/compiler/scala/tools/nsc/Global.scala
+++ b/src/compiler/scala/tools/nsc/Global.scala
@@ -125,7 +125,7 @@ class Global(var settings: Settings, var reporter: Reporter) extends SymbolTable
     informProgress(msg + " in " + (currentTime - start) + "ms")
 
   def log(msg: AnyRef): unit =
-    if (settings.log contains phase.name) inform("[log " + phase + "] " + msg)
+    if (settings.logAll.value || (settings.log contains phase.name)) inform("[log " + phase + "] " + msg)
 
   class ErrorWithPosition(val pos: Int, val error: Throwable) extends Error
 
diff --git a/src/compiler/scala/tools/nsc/Settings.scala b/src/compiler/scala/tools/nsc/Settings.scala
index f3e073ac6f..e1e239b92e 100644
--- a/src/compiler/scala/tools/nsc/Settings.scala
+++ b/src/compiler/scala/tools/nsc/Settings.scala
@@ -114,6 +114,7 @@ class Settings(error: String => unit) {
   val browse        = PhasesSetting ("-browse", "Browse the abstract syntax tree after")
   val stop          = PhasesSetting ("-stop", "Stop after phase")
   val log           = PhasesSetting ("-log", "Log operations in")
+  val logAll        = BooleanSetting("-logall", "Log all operations")   //@M
   val version       = new BooleanSetting("-version", "Print product version and exit") { override def hiddenToIDE = true }
   val help          = new BooleanSetting("-help", "Print a synopsis of standard options") { override def hiddenToIDE = true }
   val nouescape     = new BooleanSetting("-nouescape", "disables handling of \\u unicode escapes")
diff --git a/src/compiler/scala/tools/nsc/ast/TreeBrowsers.scala b/src/compiler/scala/tools/nsc/ast/TreeBrowsers.scala
index 308fefba31..fc5131358e 100644
--- a/src/compiler/scala/tools/nsc/ast/TreeBrowsers.scala
+++ b/src/compiler/scala/tools/nsc/ast/TreeBrowsers.scala
@@ -275,7 +275,7 @@ abstract class TreeBrowsers {
       case DefDef(mods, name, tparams, vparams, tpe, rhs) =>
         ("DefDef", name)
 
-      case AbsTypeDef(mods, name, rhs, lobound) =>
+      case AbsTypeDef(mods, name, tparams, rhs, lobound) =>
         ("AbsTypeDef", name)
 
       case AliasTypeDef(mods, name, tparams, rhs) =>
@@ -417,8 +417,8 @@ abstract class TreeBrowsers {
         tpe :: rhs :: children
       }
 
-      case AbsTypeDef(mods, name, rhs, lobound) =>
-        List(rhs, lobound)
+      case AbsTypeDef(mods, name, tparams, rhs, lobound) =>
+        rhs :: lobound :: tparams // @M: was List(rhs, lobound)
 
       case AliasTypeDef(mods, name, tparams, rhs) => {
         var children: List[Tree] = List()
diff --git a/src/compiler/scala/tools/nsc/ast/TreeGen.scala b/src/compiler/scala/tools/nsc/ast/TreeGen.scala
index 15033d83e8..510e07c0cf 100644
--- a/src/compiler/scala/tools/nsc/ast/TreeGen.scala
+++ b/src/compiler/scala/tools/nsc/ast/TreeGen.scala
@@ -87,6 +87,7 @@ abstract class TreeGen {
   def mkAttributedCast(tree: Tree, pt: Type): Tree = {
     if (settings.debug.value) log("casting " + tree + ":" + tree.tpe + " to " + pt)
     assert(!tree.tpe.isInstanceOf[MethodType], tree)
+    assert(pt eq pt.normalize) //@MAT only called during erasure, which already takes care of that
     typer.typed {
       atPos(tree.pos) {
         Apply(TypeApply(mkAttributedSelect(tree, Object_asInstanceOf), List(TypeTree(pt))), List())
@@ -132,7 +133,7 @@ abstract class TreeGen {
     Apply(
       TypeApply(
         mkAttributedSelect(value, sym),
-        List(TypeTree(tpe))),
+        List(TypeTree(tpe.normalize))),
       List())
   }
 
@@ -149,7 +150,7 @@ abstract class TreeGen {
     Apply(
       TypeApply(
         mkAttributedSelect(value, sym),
-        List(TypeTree(tpe))),
+        List(TypeTree(tpe.normalize))),
       List())
   }
 
diff --git a/src/compiler/scala/tools/nsc/ast/TreeInfo.scala b/src/compiler/scala/tools/nsc/ast/TreeInfo.scala
index 0ce35746ab..89ad2c1ac9 100644
--- a/src/compiler/scala/tools/nsc/ast/TreeInfo.scala
+++ b/src/compiler/scala/tools/nsc/ast/TreeInfo.scala
@@ -36,7 +36,7 @@ abstract class TreeInfo {
   def isDeclaration(tree: Tree): boolean = tree match {
     case DefDef(_, _, _, _, _, EmptyTree)
        | ValDef(_, _, _, EmptyTree)
-       | AbsTypeDef(_, _, _, _)
+       | AbsTypeDef(_, _, _, _, _)
        | AliasTypeDef(_, _, _, _) => true
     case _ => false
   }
@@ -46,7 +46,7 @@ abstract class TreeInfo {
   def isInterfaceMember(tree: Tree): boolean = tree match {
     case EmptyTree                     => true
     case Import(_, _)                  => true
-    case AbsTypeDef(_, _, _, _)        => true
+    case AbsTypeDef(_, _, _, _, _)        => true
     case AliasTypeDef(_, _, _, _)      => true
     case DefDef(mods, _, _, _, _, __)  => mods.hasFlag(DEFERRED)
     case ValDef(mods, _, _, _)         => mods.hasFlag(DEFERRED)
@@ -59,7 +59,7 @@ abstract class TreeInfo {
   def isPureDef(tree: Tree): boolean = tree match {
     case EmptyTree
        | ClassDef(_, _, _, _, _)
-       | AbsTypeDef(_, _, _, _)
+       | AbsTypeDef(_, _, _, _, _)
        | AliasTypeDef(_, _, _, _)
        | Import(_, _)
        | DefDef(_, _, _, _, _, _) =>
diff --git a/src/compiler/scala/tools/nsc/ast/TreePrinters.scala b/src/compiler/scala/tools/nsc/ast/TreePrinters.scala
index 838b70de44..c32728ac81 100644
--- a/src/compiler/scala/tools/nsc/ast/TreePrinters.scala
+++ b/src/compiler/scala/tools/nsc/ast/TreePrinters.scala
@@ -67,9 +67,9 @@ abstract class TreePrinters {
       case ValDef(mods, name, tp, rhs) =>
         printAnnotations(tree)
         print(symName(tree, name)); printOpt(": ", tp)
-      case AbsTypeDef(mods, name, lo, hi) =>
+      case AbsTypeDef(mods, name, tparams, lo, hi) =>
         print(symName(tree, name))
-        printOpt(" >: ", lo); printOpt(" <: ", hi)
+        printTypeParams(tparams); printOpt(" >: ", lo); printOpt(" <: ", hi)
     }
 
     def printBlock(tree: Tree): unit = tree match {
@@ -165,7 +165,7 @@ abstract class TreePrinters {
           printTypeParams(tparams); vparamss foreach printValueParams
           printOpt(": ", tp); printOpt(" = ", rhs)
 
-        case AbsTypeDef(mods, name, lo, hi) =>
+        case AbsTypeDef(mods, name, _, lo, hi) =>
           printModifiers(tree, mods); print("type "); printParam(tree)
 
         case AliasTypeDef(mods, name, tparams, rhs) =>
@@ -346,7 +346,7 @@ abstract class TreePrinters {
             case ModuleDef(_, _, impl)      => ModuleDef(tree.symbol, impl)
 //            case ValDef(_, _, _, rhs)       => ValDef(tree.symbol, rhs)
             case DefDef(_, _, _, vparamss, _, rhs) => DefDef(tree.symbol, vparamss, rhs)
-            case AbsTypeDef(_, _, _, _)     => AbsTypeDef(tree.symbol)
+            case AbsTypeDef(_, _, _, _, _)     => AbsTypeDef(tree.symbol)
             case AliasTypeDef(_, _, _, rhs) => AliasTypeDef(tree.symbol, rhs)
             case _ => tree
           }
diff --git a/src/compiler/scala/tools/nsc/ast/Trees.scala b/src/compiler/scala/tools/nsc/ast/Trees.scala
index e516fa86a3..b49018b377 100644
--- a/src/compiler/scala/tools/nsc/ast/Trees.scala
+++ b/src/compiler/scala/tools/nsc/ast/Trees.scala
@@ -60,6 +60,9 @@ trait Trees requires Global {
 
   val NoMods = Modifiers(0)
 
+  // @M helper method for asserts that check consistency in kinding
+  //def kindingIrrelevant(tp: Type) = (tp eq null) || phase.name == "erasure" || phase.erasedTypes
+
   abstract class Tree {
     {
       import util.Statistics
@@ -71,9 +74,9 @@ trait Trees requires Global {
     def pos = rawpos
 
     var tpe: Type = _
-
+    //var kindStar = false //@M: kindStar implies !tpe.isHigherKinded --> if true, setType does not accept higher-kinded types
     def setPos(pos: PositionType): this.type = { rawpos = pos; this }
-    def setType(tp: Type): this.type = { tpe = tp; this }
+    def setType(tp: Type): this.type = { /*assert(kindingIrrelevant(tp) || !kindStar || !tp.isHigherKinded, ""+tp+" should not be higher-kinded");*/ tpe = tp; this }
 
     def symbol: Symbol = null
     def symbol_=(sym: Symbol): unit =
@@ -281,6 +284,8 @@ trait Trees requires Global {
   case class ValDef(mods: Modifiers, name: Name, tpt: Tree, rhs: Tree)
        extends ValOrDefDef {
     assert(tpt.isType, tpt)
+    //assert(kindingIrrelevant(tpt.tpe) || !tpt.tpe.isHigherKinded, tpt.tpe) //@M a value definition should never be typed with a higher-kinded type (values must be classified by types with kind *)
+    //tpt.kindStar=true //@M turn on consistency checking in Tree
     assert(rhs.isTerm, rhs)
   }
 
@@ -307,6 +312,8 @@ trait Trees requires Global {
                     vparamss: List[List[ValDef]], tpt: Tree, rhs: Tree)
        extends ValOrDefDef {
     assert(tpt.isType)
+    //assert(kindingIrrelevant(tpt.tpe) || !tpt.tpe.isHigherKinded, tpt.tpe) //@M a method definition should never be typed with a higher-kinded type (values must be classified by types with kind *)
+    //tpt.kindStar=true //@M turn on consistency checking in Tree
     assert(rhs.isTerm)
   }
 
@@ -336,17 +343,18 @@ trait Trees requires Global {
    *
    *  @param mods
    *  @param name
+   *  @param tparams
    *  @param lo
    *  @param hi
    */
-  case class AbsTypeDef(mods: Modifiers, name: Name, lo: Tree, hi: Tree)
+  case class AbsTypeDef(mods: Modifiers, name: Name, tparams: List[AbsTypeDef], lo: Tree, hi: Tree)
        extends DefTree {
     def namePos = pos - name.length
   }
 
   def AbsTypeDef(sym: Symbol): AbsTypeDef =
     posAssigner.atPos(sym.pos) {
-      AbsTypeDef(Modifiers(sym.flags), sym.name,
+      AbsTypeDef(Modifiers(sym.flags), sym.name, sym.typeParams map AbsTypeDef,
                  TypeTree(sym.info.bounds.lo), TypeTree(sym.info.bounds.hi))
     }
 
@@ -697,7 +705,7 @@ trait Trees requires Global {
   case ModuleDef(mods, name, impl) =>                         (eliminated by refcheck)
   case ValDef(mods, name, tpt, rhs) =>
   case DefDef(mods, name, tparams, vparamss, tpt, rhs) =>
-  case AbsTypeDef(mods, name, lo, hi) =>                          (eliminated by erasure)
+  case AbsTypeDef(mods, name, tparams, lo, hi) =>                 (eliminated by erasure)
   case AliasTypeDef(mods, name, tparams, rhs) =>                  (eliminated by erasure)
   case LabelDef(name, params, rhs) =>
   case Import(expr, selectors) =>                                 (eliminated by typecheck)
@@ -744,7 +752,7 @@ trait Trees requires Global {
     def ModuleDef(tree: Tree, mods: Modifiers, name: Name, impl: Template): ModuleDef
     def ValDef(tree: Tree, mods: Modifiers, name: Name, tpt: Tree, rhs: Tree): ValDef
     def DefDef(tree: Tree, mods: Modifiers, name: Name, tparams: List[AbsTypeDef], vparamss: List[List[ValDef]], tpt: Tree, rhs: Tree): DefDef
-    def AbsTypeDef(tree: Tree, mods: Modifiers, name: Name, lo: Tree, hi: Tree): AbsTypeDef
+    def AbsTypeDef(tree: Tree, mods: Modifiers, name: Name, tparams: List[AbsTypeDef], lo: Tree, hi: Tree): AbsTypeDef
     def AliasTypeDef(tree: Tree, mods: Modifiers, name: Name, tparams: List[AbsTypeDef], rhs: Tree): AliasTypeDef
     def LabelDef(tree: Tree, name: Name, params: List[Ident], rhs: Tree): LabelDef
     def Import(tree: Tree, expr: Tree, selectors: List[(Name, Name)]): Import
@@ -796,8 +804,8 @@ trait Trees requires Global {
       new ValDef(mods, name, tpt, rhs).copyAttrs(tree)
     def DefDef(tree: Tree, mods: Modifiers, name: Name, tparams: List[AbsTypeDef], vparamss: List[List[ValDef]], tpt: Tree, rhs: Tree) =
       new DefDef(mods, name, tparams, vparamss, tpt, rhs).copyAttrs(tree)
-    def AbsTypeDef(tree: Tree, mods: Modifiers, name: Name, lo: Tree, hi: Tree) =
-      new AbsTypeDef(mods, name, lo, hi).copyAttrs(tree)
+    def AbsTypeDef(tree: Tree, mods: Modifiers, name: Name, tparams: List[AbsTypeDef], lo: Tree, hi: Tree) =
+      new AbsTypeDef(mods, name, tparams, lo, hi).copyAttrs(tree)
     def AliasTypeDef(tree: Tree, mods: Modifiers, name: Name, tparams: List[AbsTypeDef], rhs: Tree) =
       new AliasTypeDef(mods, name, tparams, rhs).copyAttrs(tree)
     def LabelDef(tree: Tree, name: Name, params: List[Ident], rhs: Tree) =
@@ -904,10 +912,10 @@ trait Trees requires Global {
          (vparamss0 == vparamss) && (tpt0 == tpt) && (rhs == rhs0) => t
       case _ => copy.DefDef(tree, mods, name, tparams, vparamss, tpt, rhs)
     }
-    def AbsTypeDef(tree: Tree, mods: Modifiers, name: Name, lo: Tree, hi: Tree) = tree match {
-      case t @ AbsTypeDef(mods0, name0, lo0, hi0)
-      if (mods0 == mods) && (name0 == name) && (lo0 == lo) && (hi0 == hi) => t
-      case _ => copy.AbsTypeDef(tree, mods, name, lo, hi)
+    def AbsTypeDef(tree: Tree, mods: Modifiers, name: Name, tparams: List[AbsTypeDef], lo: Tree, hi: Tree) = tree match {
+      case t @ AbsTypeDef(mods0, name0, tparams0, lo0, hi0)
+      if (mods0 == mods) && (name0 == name) && (tparams0 == tparams) && (lo0 == lo) && (hi0 == hi) => t
+      case _ => copy.AbsTypeDef(tree, mods, name, tparams, lo, hi)
     }
     def AliasTypeDef(tree: Tree, mods: Modifiers, name: Name, tparams: List[AbsTypeDef], rhs: Tree) = tree match {
       case t @ AliasTypeDef(mods0, name0, tparams0, rhs0)
@@ -1133,9 +1141,9 @@ trait Trees requires Global {
           copy.DefDef(
             tree, mods, name, transformAbsTypeDefs(tparams), transformValDefss(vparamss), transform(tpt), transform(rhs))
         }
-      case AbsTypeDef(mods, name, lo, hi) =>
+      case AbsTypeDef(mods, name, tparams, lo, hi) =>
         atOwner(tree.symbol) {
-          copy.AbsTypeDef(tree, mods, name, transform(lo), transform(hi))
+          copy.AbsTypeDef(tree, mods, name, transformAbsTypeDefs(tparams), transform(lo), transform(hi))
         }
       case AliasTypeDef(mods, name, tparams, rhs) =>
         atOwner(tree.symbol) {
@@ -1277,9 +1285,9 @@ trait Trees requires Global {
         atOwner(tree.symbol) {
           traverseTrees(tparams); traverseTreess(vparamss); traverse(tpt); traverse(rhs)
         }
-      case AbsTypeDef(mods, name, lo, hi) =>
+      case AbsTypeDef(mods, name, tparams, lo, hi) =>
         atOwner(tree.symbol) {
-          traverse(lo); traverse(hi)
+          traverseTrees(tparams); traverse(lo); traverse(hi)
         }
       case AliasTypeDef(mods, name, tparams, rhs) =>
         atOwner(tree.symbol) {
diff --git a/src/compiler/scala/tools/nsc/ast/parser/Parsers.scala b/src/compiler/scala/tools/nsc/ast/parser/Parsers.scala
index 863d489667..b38ed20e1d 100644
--- a/src/compiler/scala/tools/nsc/ast/parser/Parsers.scala
+++ b/src/compiler/scala/tools/nsc/ast/parser/Parsers.scala
@@ -1636,7 +1636,7 @@ trait Parsers requires SyntaxAnalyzer {
      *  VariantTypeParam      ::= [`+' | `-'] TypeParam
      *  FunTypeParamClauseOpt ::= [FunTypeParamClause]
      *  FunTypeParamClause    ::= `[' TypeParam {`,' TypeParam} `]']
-     *  TypeParam             ::= Id TypeBounds [<% Type]
+     *  TypeParam             ::= Id TypeParamClauseOpt TypeBounds [<% Type]
      */
     def typeParamClauseOpt(owner: Name, implicitViewBuf: ListBuffer[Tree]): List[AbsTypeDef] = {
       def typeParam(): AbsTypeDef = {
@@ -1651,8 +1651,14 @@ trait Parsers requires SyntaxAnalyzer {
           }
         }
         val pos = in.currentPos
-        val pname = ident()
-        val param = atPos(pos) { typeBounds(mods, pname) }
+        val pname =
+          if (in.token == USCORE) { // @M! also allow underscore
+            in.nextToken()
+            nme.WILDCARD
+          } else ident()
+
+        val tparams = typeParamClauseOpt(pname.toTypeName, null) // @M TODO null --> no higher-order view bounds for now
+        val param = atPos(pos) { typeBounds(mods, pname, tparams) }
         if (in.token == VIEWBOUND && (implicitViewBuf ne null))
           implicitViewBuf += atPos(in.skipToken()) {
             makeFunctionTypeTree(List(Ident(pname.toTypeName)), typ())
@@ -1675,8 +1681,8 @@ trait Parsers requires SyntaxAnalyzer {
 
     /** TypeBounds ::= [`>:' Type] [`<:' Type]
      */
-    def typeBounds(mods: Modifiers, name: Name): AbsTypeDef =
-      AbsTypeDef(mods, name.toTypeName,
+    def typeBounds(mods: Modifiers, name: Name, tparams: List[AbsTypeDef]): AbsTypeDef =
+      AbsTypeDef(mods, name.toTypeName, tparams, // @M: an abstract type may have type parameters
                  bound(SUPERTYPE, nme.Nothing),
                  bound(SUBTYPE, nme.Any))
 
@@ -1930,21 +1936,26 @@ trait Parsers requires SyntaxAnalyzer {
       }
 
     /** TypeDef ::= Id [TypeParamClause] `=' Type
-     *  TypeDcl ::= Id TypeBounds
+     *  TypeDcl ::= Id [TypeParamClause] TypeBounds
      */
     def typeDefOrDcl(mods: Modifiers): Tree =
       atPos(in.currentPos) {
         val name = ident().toTypeName
-        in.token match {
+
+        // @M! a type alias as well as an abstract type may declare type parameters
+        val tparams = in.token match {
           case LBRACKET =>
-            val tparams = typeParamClauseOpt(name, null)
-            accept(EQUALS)
-            AliasTypeDef(mods, name, tparams, typ())
+             typeParamClauseOpt(name, null)
+          case _ =>
+             Nil
+        }
+
+        in.token match {
           case EQUALS =>
             in.nextToken()
-            AliasTypeDef(mods, name, List(), typ())
+            AliasTypeDef(mods, name, tparams, typ())
           case SUPERTYPE | SUBTYPE | SEMI | NEWLINE | NEWLINES | COMMA | RBRACE =>
-            typeBounds(mods | Flags.DEFERRED, name)
+            typeBounds(mods | Flags.DEFERRED, name, tparams) // @M: last arg is new
           case _ =>
             syntaxErrorOrIncomplete("`=', `>:', or `<:' expected", true)
             EmptyTree
diff --git a/src/compiler/scala/tools/nsc/doc/DocGenerator.scala b/src/compiler/scala/tools/nsc/doc/DocGenerator.scala
index 9fc93f2009..ac1f48483b 100644
--- a/src/compiler/scala/tools/nsc/doc/DocGenerator.scala
+++ b/src/compiler/scala/tools/nsc/doc/DocGenerator.scala
@@ -565,7 +565,7 @@ abstract class DocGenerator extends Models {
         val cflags = if (tree.mods.isCovariant) "+"
         else if (tree.mods.isContravariant) "-"
         else ""
-        Text(cflags + tree.symbol.nameString) ++ ifT(tree.hi, Text(" <: "), true) ++ ifT(tree.lo, Text(" >: "), true)
+        Text(cflags + tree.symbol.nameString) ++ surround("[", "]", forTrees(tree.tparams)) ++ ifT(tree.hi, Text(" <: "), true) ++ ifT(tree.lo, Text(" >: "), true)
       case tpt: TypeTree =>
         urlFor(tpt.tpe, contentFrame)
       case id: Ident =>
diff --git a/src/compiler/scala/tools/nsc/matching/ParallelMatching.scala b/src/compiler/scala/tools/nsc/matching/ParallelMatching.scala
index 96d6d02a7b..5c9c66b5b2 100644
--- a/src/compiler/scala/tools/nsc/matching/ParallelMatching.scala
+++ b/src/compiler/scala/tools/nsc/matching/ParallelMatching.scala
@@ -568,7 +568,7 @@ trait ParallelMatching requires (transform.ExplicitOuter with PatternMatchers wi
       gen.mkIsInstanceOf(Ident(scrut), tpe)
   }
 
-  def needsOuterTest(tpe2test:Type, scrutinee:Type) = tpe2test match {
+  def needsOuterTest(tpe2test:Type, scrutinee:Type) = tpe2test.normalize match {
     case TypeRef(prefix,_,_) =>
       prefix.symbol.isTerm &&
     !prefix.symbol.isPackage &&
@@ -579,7 +579,7 @@ trait ParallelMatching requires (transform.ExplicitOuter with PatternMatchers wi
   /** returns a result if both are TypeRefs, returns Some(true) if left and right are statically known to have
    *  the same outer, i.e. if their prefixes are the same
    */
-  def outerAlwaysEqual(left: Type, right: Type): Option[Boolean] = (left,right) match {
+  def outerAlwaysEqual(left: Type, right: Type): Option[Boolean] = (left.normalize,right.normalize) match {
     case (TypeRef(lprefix, _,_), TypeRef(rprefix,_,_)) =>
       if(!(lprefix =:= rprefix)) {
         DEBUG("DEBUG(outerAlwaysEqual) Some(f) for"+(left,right))
diff --git a/src/compiler/scala/tools/nsc/models/Models.scala b/src/compiler/scala/tools/nsc/models/Models.scala
index 1fe18a0ff5..3c0d6ba889 100644
--- a/src/compiler/scala/tools/nsc/models/Models.scala
+++ b/src/compiler/scala/tools/nsc/models/Models.scala
@@ -120,7 +120,8 @@ abstract class Models {
         }
         ret = ret + " : " + textFor(vdef.tpt)
       case atd: AbsTypeDef =>
-        ret = ret + ((if(atd.hi ne null) " <: " + textFor(atd.hi) else "") +
+        ret = ret + "[" + (for (val tparam <- atd.tparams) yield textFor(tparam)) + "]" +
+                     ((if(atd.hi ne null) " <: " + textFor(atd.hi) else "") +
                      (if(atd.lo ne null) " >: " + textFor(atd.lo) else ""));
       case _ =>
         ret = ret + tree.toString()
diff --git a/src/compiler/scala/tools/nsc/models/SemanticTokens.scala b/src/compiler/scala/tools/nsc/models/SemanticTokens.scala
index 0702498396..2584b0286e 100644
--- a/src/compiler/scala/tools/nsc/models/SemanticTokens.scala
+++ b/src/compiler/scala/tools/nsc/models/SemanticTokens.scala
@@ -401,6 +401,7 @@ class SemanticTokens(val compiler: Global) {
         //Console.err.println("ABS: " + tree.symbol + " " + unit.source.dbg(tree.namePos) + " " + unit.source.dbg(tree.pos));
         buildDef(tree.symbol, tree.namePos)
         buildDef(tree.symbol, tree.pos)
+        build(tree.tparams); //@M
         build(tree.lo)
         build(tree.hi)
       case tree: Bind =>
diff --git a/src/compiler/scala/tools/nsc/reporters/ConsoleReporter.scala b/src/compiler/scala/tools/nsc/reporters/ConsoleReporter.scala
index 504b91fee3..38bb1580b1 100644
--- a/src/compiler/scala/tools/nsc/reporters/ConsoleReporter.scala
+++ b/src/compiler/scala/tools/nsc/reporters/ConsoleReporter.scala
@@ -40,23 +40,8 @@ class ConsoleReporter(val settings: Settings, reader: BufferedReader, writer: Pr
    *  @return         ...
    */
   private def getCountString(severity: Severity): String =
-    getCountString0(count(severity), label(severity))
+    countElementsAsString(count(severity), label(severity))
 
-  /** Returns a string meaning "n elements".
-   *
-   *  @param n        ...
-   *  @param elements ...
-   *  @return         ...
-   */
-  private def getCountString0(n: Int, elements: String): String =
-    n match {
-      case 0 => "no "    + elements + "s"
-      case 1 => "one "   + elements
-      case 2 => "two "   + elements + "s"
-      case 3 => "three " + elements + "s"
-      case 4 => "four "  + elements + "s"
-      case _ => "" + n + " " + elements + "s"
-    }
 
   /** Prints the message. */
   def printMessage(msg: String) = writer.println(msg)
diff --git a/src/compiler/scala/tools/nsc/reporters/Reporter.scala b/src/compiler/scala/tools/nsc/reporters/Reporter.scala
index 54690ba03b..4981a7c9fa 100644
--- a/src/compiler/scala/tools/nsc/reporters/Reporter.scala
+++ b/src/compiler/scala/tools/nsc/reporters/Reporter.scala
@@ -64,4 +64,36 @@ abstract class Reporter {
       incompleteInputError = savedHandler
     }
   }
+
+  // @M: moved here from ConsoleReporter and made public -- also useful in e.g. Typers
+  /** Returns a string meaning "n elements".
+   *
+   *  @param n        ...
+   *  @param elements ...
+   *  @return         ...
+   */
+  def countElementsAsString(n: Int, elements: String): String =
+    n match {
+      case 0 => "no "    + elements + "s"
+      case 1 => "one "   + elements
+      case 2 => "two "   + elements + "s"
+      case 3 => "three " + elements + "s"
+      case 4 => "four "  + elements + "s"
+      case _ => "" + n + " " + elements + "s"
+    }
+
+  /** Turns a count into a friendly English description if n<=4.
+   *
+   *  @param n        ...
+   *  @return         ...
+   */
+  def countAsString(n: Int): String =
+    n match {
+      case 0 => "none"
+      case 1 => "one"
+      case 2 => "two"
+      case 3 => "three"
+      case 4 => "four"
+      case _ => "" + n
+    }
 }
diff --git a/src/compiler/scala/tools/nsc/symtab/Definitions.scala b/src/compiler/scala/tools/nsc/symtab/Definitions.scala
index 21515a3d57..a0fffdbbef 100644
--- a/src/compiler/scala/tools/nsc/symtab/Definitions.scala
+++ b/src/compiler/scala/tools/nsc/symtab/Definitions.scala
@@ -111,7 +111,7 @@ trait Definitions requires SymbolTable {
     val MaxTupleArity = 22
     val TupleClass: Array[Symbol] = new Array(MaxTupleArity + 1)
       def tupleField(n: Int, j: Int) = getMember(TupleClass(n), "_" + j)
-      def isTupleType(tp: Type): Boolean = tp match {
+      def isTupleType(tp: Type): Boolean = tp.normalize match {
         case TypeRef(_, sym, elems) =>
           elems.length <= MaxTupleArity && sym == TupleClass(elems.length)
         case _ =>
@@ -129,7 +129,7 @@ trait Definitions requires SymbolTable {
       def productProj(z:Symbol, j: Int): Symbol = getMember(z, nme.Product_(j))
       def productProj(n: Int,   j: Int): Symbol = productProj(ProductClass(n), j)
     /** returns true if this type is exactly ProductN[T1,...,Tn], not some subclass */
-      def isExactProductType(tp: Type): Boolean = tp match {
+      def isExactProductType(tp: Type): Boolean = tp.normalize match {
         case TypeRef(_, sym, elems) =>
           elems.length <= MaxProductArity && sym == ProductClass(elems.length)
         case _ =>
@@ -157,34 +157,34 @@ trait Definitions requires SymbolTable {
     private var NoneClass_ : Symbol = null
     def NoneClass: Symbol = { if(NoneClass_ eq null) SomeClass_ = getModule("scala.None"); NoneClass_ }
 
-    def isOptionType(tp: Type) = tp match {
+    def isOptionType(tp: Type) = tp.normalize match {
       case TypeRef(_, sym, List(_)) if sym == OptionClass => true
       case _ => false
     }
-    def isOptionOrSomeType(tp: Type) = tp match {
+    def isOptionOrSomeType(tp: Type) = tp.normalize match {
       case TypeRef(_, sym, List(_)) => sym == OptionClass || sym == SomeClass
       case _ => false
     }
     def optionType(tp: Type) =
       typeRef(OptionClass.typeConstructor.prefix, OptionClass, List(tp))
 
-    def isSomeType(tp: Type) = tp match {
+    def isSomeType(tp: Type) = tp.normalize match {
       case TypeRef(_, sym, List(_)) if sym == SomeClass => true
       case _ => false
     }
     def someType(tp: Type) =
       typeRef(SomeClass.typeConstructor.prefix, SomeClass, List(tp))
 
-    def isNoneType(tp: Type) = tp match {
+    def isNoneType(tp: Type) = tp.normalize match {
       case TypeRef(_, sym, List(_)) if sym == NoneClass => true
       case _ => false
     }
 
-    def unapplyUnwrap(tpe:Type) = tpe match {
+    def unapplyUnwrap(tpe:Type) = (tpe match {
       case PolyType(_,MethodType(_, res)) => res
       case MethodType(_, res)             => res
       case tpe                            => tpe
-    }
+    }).normalize
 
     /** returns type list for return type of the extraction */
     def unapplyTypeList(ufn: Symbol, ufntpe: Type) = {
@@ -272,7 +272,7 @@ trait Definitions requires SymbolTable {
           val sym = FunctionClass(formals.length)
           typeRef(sym.typeConstructor.prefix, sym, formals ::: List(restpe))
         } else NoType;
-      def isFunctionType(tp: Type): boolean = tp match {
+      def isFunctionType(tp: Type): boolean = tp.normalize match {
         case TypeRef(_, sym, args) =>
           (args.length > 0) && (args.length - 1 <= MaxFunctionArity) &&
           (sym == FunctionClass(args.length - 1))
diff --git a/src/compiler/scala/tools/nsc/symtab/Symbols.scala b/src/compiler/scala/tools/nsc/symtab/Symbols.scala
index 49c52072fd..63c502db84 100644
--- a/src/compiler/scala/tools/nsc/symtab/Symbols.scala
+++ b/src/compiler/scala/tools/nsc/symtab/Symbols.scala
@@ -194,6 +194,7 @@ trait Symbols requires SymbolTable {
     final def isError = hasFlag(IS_ERROR)
     final def isErroneous = isError || isInitialized && tpe.isErroneous
     final def isTrait = isClass & hasFlag(TRAIT)
+    final def isTypeMember = isType && !isClass
     final def isAliasType = isType && !isClass && !hasFlag(DEFERRED)
     final def isAbstractType = isType && !isClass && hasFlag(DEFERRED)
     final def isTypeParameterOrSkolem = isType && hasFlag(PARAM)
@@ -525,6 +526,8 @@ trait Symbols requires SymbolTable {
     def typeConstructor: Type =
       throw new Error("typeConstructor inapplicable for " + this)
 
+    def tpeHK =  if(isType) typeConstructor else tpe // @M! used in memberType
+
     /** The type parameters of this symbol */
     def unsafeTypeParams: List[Symbol] = rawInfo.typeParams
     /*
@@ -1014,7 +1017,7 @@ trait Symbols requires SymbolTable {
     def infosString = infos.toString()
 
     /** String representation of symbol's variance */
-    private def varianceString: String =
+    def varianceString: String =
       if (variance == 1) "+"
       else if (variance == -1) "-"
       else ""
@@ -1117,7 +1120,12 @@ trait Symbols requires SymbolTable {
    *  of this class. Classes are instances of a subclass.
    */
   class TypeSymbol(initOwner: Symbol, initPos: PositionType, initName: Name)
-  extends Symbol(initOwner, initPos, initName) {
+  extends Symbol(initOwner, initPos,
+// @M type params with name "_" implicitly get unique name @M TODO: the name generation is a bit hacky...
+                 if(initName.length==1 && initName(0)=='_') // faster equality test than first converting to string
+                   newTypeName("_$" + (ids+1))
+                 else initName) {
+    override def nameString: String = if(name.startsWith("_$")) "_"+idString else super.nameString // @M: undo underscore-mangling
     override def isType = true
     privateWithin = NoSymbol
     private var tyconCache: Type = null
@@ -1133,7 +1141,9 @@ trait Symbols requires SymbolTable {
           if (isInitialized) tpePeriod = currentPeriod
           tpeCache = NoType
           val targs = if (phase.erasedTypes && this != ArrayClass) List()
-          else unsafeTypeParams map (.tpe)
+          else unsafeTypeParams map (.typeConstructor) //@M! use typeConstructor to generate dummy type arguments,
+          // sym.tpe should not be called on a symbol that's supposed to be a higher-kinded type
+          // memberType should be used instead, that's why it uses tpeHK and not tpe
           tpeCache = typeRef(if (isTypeParameterOrSkolem) NoPrefix else owner.thisType, this, targs)
         }
       }
@@ -1181,6 +1191,7 @@ trait Symbols requires SymbolTable {
                    initName: Name, typeParam: Symbol)
   extends TypeSymbol(initOwner, initPos, initName) {
     override def deSkolemize = typeParam
+    override def typeParams = info.typeParams //@M! (not deSkolemize.typeParams!!), also can't leave superclass definition: use info, not rawInfo
     override def cloneSymbolImpl(owner: Symbol): Symbol = {
       throw new Error("should not clone a type skolem")
     }
diff --git a/src/compiler/scala/tools/nsc/symtab/Types.scala b/src/compiler/scala/tools/nsc/symtab/Types.scala
index 69853c37bc..fcb09f31e9 100644
--- a/src/compiler/scala/tools/nsc/symtab/Types.scala
+++ b/src/compiler/scala/tools/nsc/symtab/Types.scala
@@ -70,7 +70,9 @@ trait Types requires SymbolTable {
      */
     def isTrivial: boolean = false
 
-    /** The symbol associated with the type */
+    /** The symbol associated with the type
+      * Note that the symbol of the normalized type is returned (@see normalize)
+      */
     def symbol: Symbol = NoSymbol
 
     /** The base type underlying a singleton type,
@@ -108,7 +110,7 @@ trait Types requires SymbolTable {
      *  The empty list for all other types */
     def parents: List[Type] = List()
 
-    /** For a typeref or single-type, its prefix. NoType for all other types. */
+    /** For a typeref or single-type, the prefix of the normalized type (@see normalize). NoType for all other types. */
     def prefix: Type = NoType
 
     /** For a typeref, its arguments. The empty list for all other types */
@@ -134,6 +136,18 @@ trait Types requires SymbolTable {
      *  the empty list for all other types */
     def typeParams: List[Symbol] = List()
 
+    /** Replace formal type parameter symbols with actual type arguments.
+     *
+     * Amounts to substitution except for higher-kinded types. (See overridden method in TypeRef) -- @M (contact adriaan.moors at cs.kuleuven.be)
+     */
+    def instantiateTypeParams(formals: List[Symbol], actuals: List[Type]): Type = this.subst(formals, actuals)
+
+    /** Is this type higher-kinded, i.e., is it a type constructor @M */
+    def isHigherKinded: boolean = false
+
+    /** Reduce to beta eta-long normal form. Expands type aliases and converts higher-kinded TypeRef's to PolyTypes. @M */
+    def normalize = this // @MAT
+
     /** Is this type produced as a repair for an error? */
     def isError: boolean = symbol.isError
 
@@ -221,7 +235,8 @@ trait Types requires SymbolTable {
 
     /** The type of `sym', seen as a member of this type. */
     def memberType(sym: Symbol): Type = {
-      sym.tpe match {
+      //@M don't prematurely instantiate higher-kinded types, they will be instantiated by transform, typedTypeApply, etc. when really necessary
+     sym.tpeHK match {
         case ov @ OverloadedType(pre, alts) =>
           OverloadedType(this, alts)
 /*
@@ -237,9 +252,9 @@ trait Types requires SymbolTable {
             ov
           }
 */
-        case _ =>
+        case tp =>
           //Console.println("" + this + ".memberType(" + sym +":" + sym.tpe +")" + sym.ownerChain);//DEBUG
-          sym.tpe.asSeenFrom(this, sym.owner)
+          tp.asSeenFrom(this, sym.owner)
       }
     }
 
@@ -1010,7 +1025,7 @@ trait Types requires SymbolTable {
     assert(value.tpe.symbol != UnitClass)
     override def isTrivial: boolean = true
     override def symbol: Symbol = value.tpe.symbol
-    override def singleDeref: Type = value.tpe
+    override def singleDeref: Type = value.tpe //M@ probably ok since constants don't take type params?
     override def deconst: Type = value.tpe
     override def toString(): String =
       value.tpe.toString() + "(" + value.escapedStringValue + ")"
@@ -1021,8 +1036,9 @@ trait Types requires SymbolTable {
   /** A class for named types of the form
    *  <code>&lt;prefix&gt;.&lt;sym.name&gt;[args]</code>
    *  Cannot be created directly; one should always use <code>typeRef</code>
-   *  for creation.
+   *  for creation. (@M: Otherwise hashing breaks)
    *
+   * @M: Higher-kinded types are represented as TypeRefs with a symbol that has type parameters, but with args==List()
    *  @param pre  ...
    *  @param sym  ...
    *  @param args ...
@@ -1041,10 +1057,18 @@ trait Types requires SymbolTable {
     override val isTrivial: boolean =
       pre.isTrivial && !sym.isTypeParameter && args.forall(.isTrivial)
 
+    // @M: propagate actual type params (args) to `tp', by replacing formal type parameters with actual ones
     def transform(tp: Type): Type =
-      tp.asSeenFrom(pre, sym.owner).subst(sym.typeParams, args)
+      tp.asSeenFrom(pre, sym.owner).instantiateTypeParams(sym.typeParams, argsMaybeDummy)
+      // @M TODO maybe we shouldn't instantiate type params if isHigherKinded -- probably needed for partial type application though
 
-    def thisInfo = if (sym.isAbstractType) transform(sym.info) else sym.info
+    //@M! use appliedType on the polytype that represents the bounds (or if aliastype, the rhs)
+    def transformInfo(tp: Type): Type =
+      appliedType(tp.asSeenFrom(pre, sym.owner), argsMaybeDummy)
+      // TODO: argsMaybeDummy --> ok? or don't instantiate type params if isHigherKinded
+
+    def thisInfo     = if (sym.isTypeMember) transformInfo(sym.info) else sym.info
+    def relativeInfo = if (sym.isTypeMember) transformInfo(pre.memberInfo(sym)) else pre.memberInfo(sym)
 
     def transform(cl: Array[Type]): Array[Type] = {
       val cl1 = new Array[Type](cl.length)
@@ -1056,7 +1080,7 @@ trait Types requires SymbolTable {
       cl1
     }
 
-    override def symbol = sym
+    override def symbol = if(normalize ne this) normalize.symbol else sym
 
     override def bounds: TypeBounds =
       if (sym.isAbstractType) transform(thisInfo.bounds).asInstanceOf[TypeBounds]
@@ -1078,17 +1102,50 @@ trait Types requires SymbolTable {
     override def narrow =
       if (sym.isModuleClass) transform(sym.thisType) else super.narrow
 
-    override def prefix: Type = pre
+    override def prefix: Type = if(normalize ne this) normalize.resultType.prefix else pre
+// @M: .resultType because normalisation may eta-expand to a poly type, we want the resultType's prefix, not the surrounding polytype's
+// @M: should PolyType override prefix to return resultType.prefix?
+
 
     override def typeArgs: List[Type] = args
 
     override def typeParams: List[Symbol] =
-      if (args.isEmpty) symbol.unsafeTypeParams else List()
+      if (args.isEmpty) sym.unsafeTypeParams else List()
+         // @MAT was symbol.unsafeTypeParams, but symbol normalizes now
+
+    override def instantiateTypeParams(formals: List[Symbol], actuals: List[Type]): Type =
+      if(isHigherKinded) {
+        val substTps = formals.intersect(typeParams)
+
+        if(substTps.length == typeParams.length)
+          typeRef(pre, sym, actuals)
+        else // partial application (needed in infer when bunching type arguments from classes and methods together)
+          typeRef(pre, sym, higherKindedArgs).subst(formals, actuals)
+      }
+      else
+        super.instantiateTypeParams(formals, actuals)
+
+    override def isHigherKinded = !typeParams.isEmpty  //@M args.isEmpty is checked in typeParams
+
+    private def higherKindedArgs = typeParams map (.typeConstructor) //@M must be .typeConstructor
+    private def argsMaybeDummy = if(isHigherKinded) higherKindedArgs else args
+
+    override def normalize =
+      if (sym.isAliasType) {
+        if(sym.info.typeParams.length == args.length) // beta-reduce
+          transform(sym.info.resultType).normalize // cycles have been checked in typeRef -- TODO: .resultType necessary?
+        else { // eta-expand
+          assert(isHigherKinded)
+          PolyType(typeParams, transform(sym.info.resultType).normalize)
+        }
+      } else if (isHigherKinded) {
+        PolyType(typeParams, typeRef(pre, sym, higherKindedArgs))
+      } else super.normalize
 
     override def decls: Scope = {
       sym.info match {
         case TypeRef(_, sym1, _) =>
-          assert(sym1 != symbol, this)
+          assert(sym1 != sym, this) // @MAT was != symbol
         case _ =>
       }
       thisInfo.decls
@@ -1097,7 +1154,7 @@ trait Types requires SymbolTable {
     override def baseType(clazz: Symbol): Type =
       if (sym == clazz) this
       else if (sym.isClass) transform(sym.info.baseType(clazz))
-      else pre.memberInfo(sym).baseType(clazz)
+      else relativeInfo.baseType(clazz) // @M! use relativeInfo instead of pre.memberInfo(sym)
 
     override def closure: Array[Type] = {
       val period = closurePeriod
@@ -1180,6 +1237,8 @@ trait Types requires SymbolTable {
 
   /** A class representing a polymorphic type or, if tparams.length == 0,
    *  a parameterless method type.
+   *  (@M: note that polymorphic nullary methods have non-empty tparams, e.g., isInstanceOf or def makeList[T] = new List[T]
+   *       ideally, there would be a NullaryMethodType, so that higher-kinded types could use PolyType instead of TypeRef with empty args)
    */
   case class PolyType(override val typeParams: List[Symbol], override val resultType: Type)
        extends Type {
@@ -1198,8 +1257,14 @@ trait Types requires SymbolTable {
     override def baseType(clazz: Symbol): Type = resultType.baseType(clazz)
     override def narrow: Type = resultType.narrow
 
+    // @M: abstractTypeSig now wraps a TypeBounds in a PolyType to represent a higher-kinded type parameter
+    // wrap lo&hi in polytypes to bind variables
+    override def bounds: TypeBounds = TypeBounds(PolyType(typeParams, resultType.bounds.lo), PolyType(typeParams, resultType.bounds.hi))
+
     // override def isNullable: boolean = resultType.isNullable;
 
+    override def isHigherKinded = !typeParams.isEmpty
+
     override def toString(): String =
       (if (typeParams.isEmpty) "=> "
        else (typeParams map (.defString)).mkString("[", ",", "]")) + resultType
@@ -1444,23 +1509,25 @@ trait Types requires SymbolTable {
    *  with possibility of approximating in case of malformed types */
   def typeRef(pre: Type, sym: Symbol, args: List[Type], variance: int): Type = {
     var sym1 = if (sym.isAbstractType) rebind(pre, sym) else sym
+    def transform(tp: Type): Type =
+      tp.resultType.asSeenFrom(pre, sym1.owner).instantiateTypeParams(sym1.typeParams, args)
+
     if (sym1.isAliasType && sym1.info.typeParams.length == args.length) {
       // note: we require that object is initialized,
       // that's why we use info.typeParams instead of typeParams.
       if (sym1.hasFlag(LOCKED))
         throw new TypeError("illegal cyclic reference involving " + sym1)
       sym1.setFlag(LOCKED)
-      val result = sym1.info.resultType.asSeenFrom(pre, sym1.owner).subst(sym1.typeParams, args)
+      val result = transform(sym1.info)
       sym1.resetFlag(LOCKED)
-      result
+      //result // @M: original version -- this would expand the type alias immediately
+      rawTypeRef(pre, sym1, args) //@MAT -- don't expand type alias, but still check there are no cycles
     } else {
       val pre1 = removeSuper(pre, sym1)
       if (pre1 ne pre) {
         if (sym1.isAbstractType) sym1 = rebind(pre1, sym1)
         typeRef(pre1, sym1, args, variance)
       } else if (checkMalformedSwitch && sym1.isAbstractType && !pre.isStable && !pre.isError) {
-        def transform(tp: Type): Type =
-          tp.asSeenFrom(pre, sym1.owner).subst(sym1.typeParams, args)
         if (healTypes && variance == 1 && !(sym1.info.bounds.hi contains sym1)) transform(sym1.info.bounds.hi)
         //else if (variance == -1 && !(sym1.info.bounds.lo contains sym1)) transform(sym1.info.bounds.lo)
         else throw new MalformedType(pre, sym1.nameString)
@@ -1521,15 +1588,17 @@ trait Types requires SymbolTable {
   }
 
   /** A creator for type applications */
-  def appliedType(tycon: Type, args: List[Type]): Type = tycon match {
-    case TypeRef(pre, sym, _) => typeRef(pre, sym, args)
-    case PolyType(tparams, restpe) => restpe.subst(tparams, args)
-    case ErrorType => tycon
-    case _ =>
-      Console.println(tycon.getClass())
-      Console.println(tycon.$tag())
-      throw new Error()
-  }
+  def appliedType(tycon: Type, args: List[Type]): Type =
+    if(args.isEmpty) tycon //@M! `if(args.isEmpty) tycon' is crucial (otherwise we create new types in phases after typer and then they don't get adapted (??))
+    else tycon match {
+      case TypeRef(pre, sym, _) => typeRef(pre, sym, args)
+      case PolyType(tparams, restpe) => restpe.instantiateTypeParams(tparams, args)
+      case ErrorType => tycon
+      case _ =>
+        Console.println(tycon.getClass())
+        Console.println(tycon.$tag())
+        throw new Error()
+    }
 
 // Hash consing --------------------------------------------------------------
 
@@ -1759,7 +1828,7 @@ trait Types requires SymbolTable {
           }
         case TypeRef(prefix, sym, args) if (sym.isTypeParameter) =>
           def toInstance(pre: Type, clazz: Symbol): Type =
-            if ((pre eq NoType) || (pre eq NoPrefix) || !clazz.isClass) tp
+            if ((pre eq NoType) || (pre eq NoPrefix) || !clazz.isClass) mapOver(tp) //@M! see test pos/tcpoly_return_overriding.scala why mapOver is necessary
             else {
               val symclazz = sym.owner;
               def throwError =
@@ -1767,7 +1836,8 @@ trait Types requires SymbolTable {
                                 " cannot be instantiated from " + pre.widen);
               def instParam(ps: List[Symbol], as: List[Type]): Type =
                 if (ps.isEmpty) throwError
-                else if (sym eq ps.head) as.head
+                else if (sym eq ps.head)  // @M! don't just replace the whole thing, might be followed by type application
+                  appliedType(as.head, List.mapConserve(args)(this)) // @M: was as.head
                 else instParam(ps.tail, as.tail);
               if (symclazz == clazz && (pre.widen.symbol isNonBottomSubClass symclazz))
                 pre.baseType(symclazz) match {
@@ -1802,24 +1872,38 @@ trait Types requires SymbolTable {
     /** Map target to type, can be tuned by subclasses */
     protected def toType(fromtp: Type, t: T): Type
 
-    def apply(tp: Type): Type = {
+    def apply(tp0: Type): Type = if(from.isEmpty) tp0 else {
+      val tp = mapOver(tp0)
+
       def subst(sym: Symbol, from: List[Symbol], to: List[T]): Type =
         if (from.isEmpty) tp
         else if (to.isEmpty && inIDE) throw new TypeError(NoPos, "type parameter list problem");
         else if (matches(from.head, sym)) toType(tp, to.head)
         else subst(sym, from.tail, to.tail)
+
       tp match {
-        case TypeRef(NoPrefix, sym, _) =>
-          val tp1 = subst(sym, from, to)
-          if (tp1 ne tp) tp1
-          else mapOver(tp)
+        // @M
+        // 1) arguments must also be substituted (even when the "head" of the applied type has already been substituted)
+        // example: (subst RBound[RT] from [type RT,type RBound] to [type RT&,type RBound&]) = RBound&[RT&]
+        // 2) avoid loops (which occur because alpha-conversion is not performed properly imo)
+        // e.g. if in class Iterable[a] there is a new Iterable[(a,b)], we must replace the a in Iterable[a] by (a,b)
+        // (must not recurse --> loops)
+        // 3) replacing m by List in m[Int] should yield List[Int], not just List
+        case TypeRef(NoPrefix, sym, args) =>
+          subst(sym, from, to) match {
+            case r @ TypeRef(pre1, sym1, args1) =>
+              if (args.isEmpty) r
+              else rawTypeRef(pre1, sym1, args)
+            case r =>
+              r
+          }
         case SingleType(NoPrefix, sym) =>
           subst(sym, from, to)
         case PolyType(tparams, restp) =>
           assert(!(tparams exists (from contains)))
-          mapOver(tp)
+          tp
         case _ =>
-          mapOver(tp)
+          tp
       }
     }
   }
@@ -1831,14 +1915,14 @@ trait Types requires SymbolTable {
       case TypeRef(pre, _, args) => typeRef(pre, sym, args, variance)
       case SingleType(pre, _) => singleType(pre, sym, variance)
     }
-    override def apply(tp: Type): Type = {
+    override def apply(tp: Type): Type = if(from.isEmpty) tp else {
       def subst(sym: Symbol, from: List[Symbol], to: List[Symbol]): Symbol =
         if (from.isEmpty) sym
         else if (matches(from.head, sym)) to.head
         else subst(sym, from.tail, to.tail)
       tp match {
         case TypeRef(pre, sym, args) if !(pre eq NoPrefix) =>
-          mapOver(typeRef(pre, subst(sym, from, to), args, variance))
+          mapOver(typeRef(pre, subst(sym, from, to), args, variance)) //@M TODO subst args? List.mapConserve(args)(this)
         case SingleType(pre, sym) if !(pre eq NoPrefix) =>
           mapOver(singleType(pre, subst(sym, from, to), variance))
         case _ =>
@@ -1883,7 +1967,7 @@ trait Types requires SymbolTable {
     var result = false
     def traverse(tp: Type): ContainsTraverser = {
       if (!result) {
-        tp match {
+        tp.normalize match {
           case TypeRef(_, sym1, _) if (sym == sym1) => result = true
           case SingleType(_, sym1) if (sym == sym1) => result = true
           case _ => mapOver(tp)
@@ -1925,7 +2009,7 @@ trait Types requires SymbolTable {
     def init = { result = NoSymbol }
     def apply(tp: Type): Type = {
       assert(tp ne null)
-      tp match {
+      tp.normalize match {
         case ThisType(sym) =>
           register(sym)
         case TypeRef(NoPrefix, sym, args) =>
@@ -2088,7 +2172,14 @@ trait Types requires SymbolTable {
    *             equivalent types.
    */
   def isSameType(tp1: Type, tp2: Type): boolean = {
-    (tp1, tp2) match {
+    //@MAT
+    def isSameTypeNormalize(tp1: Type, tp2: Type): boolean = {
+      val tp1n= tp1.normalize
+      val tp2n= tp2.normalize
+      ((tp1n ne tp1) || (tp2n ne tp2)) && isSameType(tp1n, tp2n)
+    }
+
+    val res = (tp1, tp2) match {
       case (ErrorType, _) => true
       case (WildcardType, _) => true
       case (_, ErrorType) => true
@@ -2120,7 +2211,10 @@ trait Types requires SymbolTable {
       case (ConstantType(value1), ConstantType(value2)) =>
         value1 == value2
       case (TypeRef(pre1, sym1, args1), TypeRef(pre2, sym2, args2)) =>
-        sym1 == sym2 && (phase.erasedTypes || pre1 =:= pre2) && isSameTypes(args1, args2)
+        sym1 == sym2 && (phase.erasedTypes || pre1 =:= pre2) &&
+          // @M! normalize reduces higher-kinded case to PolyType's
+        ( (tp1.isHigherKinded && tp2.isHigherKinded && tp1.normalize =:= tp2.normalize)
+         || isSameTypes(args1, args2))
       case (RefinedType(parents1, ref1), RefinedType(parents2, ref2)) =>
         def isSubScope(s1: Scope, s2: Scope): boolean = s2.toList.forall {
           sym2 =>
@@ -2165,6 +2259,8 @@ trait Types requires SymbolTable {
           ((origin1 ne tp1) || (origin2 ne tp2)) && (origin1 =:= origin2)
         } else false
     }
+
+    (res || isSameTypeNormalize(tp1, tp2)) //@MAT
   }
 
   /** Are <code>tps1</code> and <code>tps2</code> lists of pairwise equivalent
@@ -2177,7 +2273,14 @@ trait Types requires SymbolTable {
   var stc: int = 0
   private var pendingSubTypes = new collection.mutable.HashSet[SubTypePair]
 
-  def isSubType(tp1: Type, tp2: Type): boolean =
+  def isSubType(tp1: Type, tp2: Type): boolean = {
+    //@MAT
+    def isSubTypeNormalize(tp1: Type, tp2: Type): boolean = {
+      val tp1n= tp1.normalize
+      val tp2n= tp2.normalize
+      ((tp1n ne tp1) || (tp2n ne tp2)) && isSubType0(tp1n, tp2n)
+    }
+
     try {
       stc = stc + 1
       if (stc >= LogPendingSubTypesThreshold) {
@@ -2187,14 +2290,15 @@ trait Types requires SymbolTable {
         else
           try {
             pendingSubTypes += p
-            isSubType0(tp1, tp2)
+            (isSubType0(tp1, tp2) || isSubTypeNormalize(tp1, tp2))  //@MAT
           } finally {
             pendingSubTypes -= p
           }
-      } else isSubType0(tp1, tp2)
+      } else (isSubType0(tp1, tp2) || isSubTypeNormalize(tp1, tp2))  //@MAT
     } finally {
       stc = stc - 1
     }
+  }
   /** hook for IDE */
   protected def trackTypeIDE(sym : Symbol) : Boolean = true;
 
@@ -2222,8 +2326,7 @@ trait Types requires SymbolTable {
       case (SingleType(_, _), SingleType(_, _)) => tp1 =:= tp2
       case (ConstantType(_), ConstantType(_))   => tp1 =:= tp2
 
-      case (TypeRef(pre1, sym1, args1), TypeRef(pre2, sym2, args2)) =>
-        //Console.println("isSubType " + tp1 + " " + tp2);//DEBUG
+      case (TypeRef(pre1, sym1, args1), TypeRef(pre2, sym2, args2)) if !(tp1.isHigherKinded || tp2.isHigherKinded) =>         //Console.println("isSubType " + tp1 + " " + tp2);//DEBUG
         if (inIDE) { trackTypeIDE(sym1); trackTypeIDE(sym2); }
 
         def isSubArgs(tps1: List[Type], tps2: List[Type],
@@ -2236,22 +2339,22 @@ trait Types requires SymbolTable {
           isSubArgs(tps1.tail, tps2.tail, tparams.tail)
         );
         (sym1 == sym2 &&
-         (phase.erasedTypes || pre1 <:< pre2) &&
-         isSubArgs(args1, args2, sym1.typeParams)
+          (phase.erasedTypes || pre1 <:< pre2) &&
+          (sym2 == AnyClass || isSubArgs(args1, args2, sym1.typeParams)) //@M: Any is kind-polymorphic
          ||
-         sym1.isAbstractType && !(tp1 =:= tp1.bounds.hi) && (tp1.bounds.hi <:< tp2)
+          sym1.isAbstractType && !(tp1 =:= tp1.bounds.hi) && (tp1.bounds.hi <:< tp2)
          ||
-         sym2.isAbstractType && !(tp2 =:= tp2.bounds.lo) && (tp1 <:< tp2.bounds.lo)
+          sym2.isAbstractType && !(tp2 =:= tp2.bounds.lo) && (tp1 <:< tp2.bounds.lo)
          ||
 //         sym2 == NonNullClass && tp1.isNonNull
 //         ||
-         sym2.isClass &&
-           ({ val base = tp1 baseType sym2; !(base eq tp1) && (base <:< tp2) })
+          sym2.isClass &&
+            ({ val base = tp1 baseType sym2; !(base eq tp1) && (base <:< tp2) })
          ||
-         sym1 == AllClass
+          sym1 == AllClass
          ||
          // Console.println("last chance " + sym1 + " " + sym2 + " " + sym2.isClass + " " (sym2 isSubClass ObjectClass))
-         sym1 == AllRefClass && sym2.isClass && sym2 != AllClass && (sym2 isSubClass ObjectClass))
+          sym1 == AllRefClass && sym2.isClass && sym2 != AllClass && (sym2 isSubClass ObjectClass))
       case (MethodType(pts1, res1), MethodType(pts2, res2)) =>
         (pts1.length == pts2.length &&
          matchingParams(pts1, pts2, tp2.isInstanceOf[JavaMethodType]) &&
@@ -2262,6 +2365,12 @@ trait Types requires SymbolTable {
          List.forall2(tparams1, tparams2)
            ((p1, p2) => p2.info.substSym(tparams2, tparams1) <:< p1.info) &&
          res1 <:< res2.substSym(tparams2, tparams1))
+      case (_, _)  if (tp1.isHigherKinded || tp2.isHigherKinded) =>
+          (tp1.symbol == AllClass
+         ||
+          tp2.symbol == AnyClass // @M Any and Nothing are super-type resp. subtype of every well-kinded type
+         || // @M! normalize reduces higher-kinded case to PolyType's
+          (tp1.isHigherKinded && tp2.isHigherKinded) && isSubType0(tp1.normalize, tp2.normalize))
       case (TypeBounds(lo1, hi1), TypeBounds(lo2, hi2)) =>
         lo2 <:< lo1 && hi1 <:< hi2
       case (BoundedWildcardType(bounds), _) =>
@@ -2338,7 +2447,7 @@ trait Types requires SymbolTable {
     //System.out.println("specializes "+tp1+"."+sym1+":"+info1+sym1.locationString+" AND "+tp2+"."+sym2+":"+info2)//DEBUG
     sym2.isTerm && (info1 <:< info2) ||
     sym2.isAbstractType && info2.bounds.containsType(tp1.memberType(sym1)) ||
-    sym2.isAliasType && tp2.memberType(sym2).substThis(tp2.symbol, tp1) =:= tp1.memberType(sym1)
+    sym2.isAliasType && tp2.memberType(sym2).substThis(tp2.symbol, tp1) =:= tp1.memberType(sym1) //@MAT ok
   }
 
   /** A function implementing <code>tp1</code> matches <code>tp2</code> */
diff --git a/src/compiler/scala/tools/nsc/transform/AddInterfaces.scala b/src/compiler/scala/tools/nsc/transform/AddInterfaces.scala
index b1235c9c94..a184a1a0b7 100644
--- a/src/compiler/scala/tools/nsc/transform/AddInterfaces.scala
+++ b/src/compiler/scala/tools/nsc/transform/AddInterfaces.scala
@@ -176,7 +176,7 @@ abstract class AddInterfaces extends InfoTransform {
    */
   private def mixinToImplClass(tp: Type): Type =
     erasure(
-      tp match {
+      tp match { //@MATN: no normalize needed (comes after erasure)
         case TypeRef(pre, sym, args) if (sym.needsImplClass) =>
           typeRef(pre, implClass(sym), args)
         case _ =>
diff --git a/src/compiler/scala/tools/nsc/transform/Erasure.scala b/src/compiler/scala/tools/nsc/transform/Erasure.scala
index 06f667cada..3039b7efef 100644
--- a/src/compiler/scala/tools/nsc/transform/Erasure.scala
+++ b/src/compiler/scala/tools/nsc/transform/Erasure.scala
@@ -58,39 +58,41 @@ abstract class Erasure extends AddInterfaces with typechecker.Analyzer {
    *  </ul>
    */
   val erasure = new TypeMap {
-    def apply(tp: Type): Type = tp match {
-      case ConstantType(_) =>
-        tp
-      case st: SubType =>
-        apply(st.supertype)
-      case TypeRef(pre, sym, args) =>
-        if (sym == ArrayClass)
-          args.head match {
-            case TypeRef(_, tvar, _) if (tvar.isAbstractType) => erasedTypeRef(BoxedArrayClass)
-            case _ => typeRef(apply(pre), sym, args map this)
-          }
-        else if (sym == AnyClass || sym == AnyValClass) erasedTypeRef(ObjectClass)
-        else if (sym == UnitClass) erasedTypeRef(BoxedUnitClass)
-        else if (sym.isClass)
-          typeRef(apply(if (sym.owner.isClass) sym.owner.tpe else pre), sym, List())
-        else apply(sym.info)
-      case PolyType(tparams, restpe) =>
-        apply(restpe)
-      case MethodType(formals, restpe) =>
-        MethodType(
-          formals map apply,
-          if (restpe.symbol == UnitClass) erasedTypeRef(UnitClass) else apply(restpe))
-      case RefinedType(parents, decls) =>
-        if (parents.isEmpty) erasedTypeRef(ObjectClass)
-        else apply(parents.head)
-      case ClassInfoType(parents, decls, clazz) =>
-        ClassInfoType(
-          if ((clazz == ObjectClass) || (isValueType(clazz))) List()
-          else if (clazz == ArrayClass) List(erasedTypeRef(ObjectClass))
-          else removeDoubleObject(parents map this),
-          decls, clazz)
-      case _ =>
-        mapOver(tp)
+    def apply(tp0: Type): Type = { val tp = tp0.normalize
+      tp match {
+        case ConstantType(_) =>
+          tp
+        case st: SubType =>
+          apply(st.supertype)
+        case TypeRef(pre, sym, args) =>
+          if (sym == ArrayClass)
+            args.head match {
+              case TypeRef(_, tvar, _) if (tvar.isAbstractType) => erasedTypeRef(BoxedArrayClass)
+              case _ => typeRef(apply(pre), sym, args map this)
+            }
+          else if (sym == AnyClass || sym == AnyValClass) erasedTypeRef(ObjectClass)
+          else if (sym == UnitClass) erasedTypeRef(BoxedUnitClass)
+          else if (sym.isClass)
+            typeRef(apply(if (sym.owner.isClass) sym.owner.tpe else pre), sym, List())
+          else apply(sym.info)
+        case PolyType(tparams, restpe) =>
+          apply(restpe)
+        case MethodType(formals, restpe) =>
+          MethodType(
+            formals map apply,
+            if (restpe.symbol == UnitClass) erasedTypeRef(UnitClass) else apply(restpe))
+        case RefinedType(parents, decls) =>
+          if (parents.isEmpty) erasedTypeRef(ObjectClass)
+          else apply(parents.head)
+        case ClassInfoType(parents, decls, clazz) =>
+          ClassInfoType(
+            if ((clazz == ObjectClass) || (isValueType(clazz))) List()
+            else if (clazz == ArrayClass) List(erasedTypeRef(ObjectClass))
+            else removeDoubleObject(parents map this),
+            decls, clazz)
+        case _ =>
+          mapOver(tp).normalize
+      }
     }
   }
 
@@ -246,7 +248,9 @@ abstract class Erasure extends AddInterfaces with typechecker.Analyzer {
      *    </tr>
      *  </table>
      */
-    private def cast(tree: Tree, pt: Type): Tree =
+    private def cast(tree: Tree, pt: Type): Tree = {
+      assert(pt eq pt.normalize)
+
       if (tree.tpe.symbol == ObjectClass) {
         if (pt.symbol == ArrayClass)
           typed {
@@ -301,6 +305,7 @@ abstract class Erasure extends AddInterfaces with typechecker.Analyzer {
           }
         else gen.mkAttributedCast(tree, pt)
       } else gen.mkAttributedCast(tree, pt)
+    }
 
     /** Is symbol a member of unboxed arrays (which will be expanded directly
      *  later)?
@@ -728,7 +733,7 @@ abstract class Erasure extends AddInterfaces with typechecker.Analyzer {
             copy.ClassDef(tree, mods, name, List(), emptyValDef, impl)
           case DefDef(mods, name, tparams, vparamss, tpt, rhs) =>
             copy.DefDef(tree, mods, name, List(), vparamss, tpt, rhs)
-          case AbsTypeDef(_, _, _, _) =>
+          case AbsTypeDef(_, _, _, _, _) =>
             EmptyTree
           case AliasTypeDef(_, _, _, _) =>
             EmptyTree
diff --git a/src/compiler/scala/tools/nsc/transform/LiftCode.scala b/src/compiler/scala/tools/nsc/transform/LiftCode.scala
index df301eb159..f8bd3e782a 100644
--- a/src/compiler/scala/tools/nsc/transform/LiftCode.scala
+++ b/src/compiler/scala/tools/nsc/transform/LiftCode.scala
@@ -302,7 +302,7 @@ abstract class LiftCode extends Transform {
 // case ClassDef(mods, name, tparams, self, impl) =>
 // case ValDef(mods, name, tpt, rhs) =>
 // case DefDef(mods, name, tparams, vparamss, tpt, rhs) =>
-// case AbsTypeDef(mods, name, lo, hi) =>
+// case AbsTypeDef(mods, name, tparams, lo, hi) =>
 // case AliasTypeDef(mods, name, tparams, rhs) =>
 // case LabelDef(name, params, rhs) =>
 // case Template(parents, body) =>
diff --git a/src/compiler/scala/tools/nsc/transform/OverridingPairs.scala b/src/compiler/scala/tools/nsc/transform/OverridingPairs.scala
index 6aef9fc691..fcf9da53e0 100644
--- a/src/compiler/scala/tools/nsc/transform/OverridingPairs.scala
+++ b/src/compiler/scala/tools/nsc/transform/OverridingPairs.scala
@@ -103,6 +103,7 @@ abstract class OverridingPairs {
     var overriding: Symbol = _
     var overridden: Symbol = _
 
+    //@M: note that next is called once during object initialisation
     def hasNext: boolean = curEntry ne null
 
     def next: unit =
@@ -131,6 +132,6 @@ abstract class OverridingPairs {
         }
       }
 
-    next
+    next //@M: ATTN! this method gets called during construction!
   }
 }
diff --git a/src/compiler/scala/tools/nsc/transform/TailCalls.scala b/src/compiler/scala/tools/nsc/transform/TailCalls.scala
index 2302a41514..2148790c34 100644
--- a/src/compiler/scala/tools/nsc/transform/TailCalls.scala
+++ b/src/compiler/scala/tools/nsc/transform/TailCalls.scala
@@ -195,7 +195,7 @@ abstract class TailCalls extends Transform
           res
 
         case ValDef(mods, name, tpt, rhs) => tree
-        case AbsTypeDef(mods, name, lo, hi) => tree //  (eliminated by erasure)
+        case AbsTypeDef(mods, name, tparams, lo, hi) => tree //  (eliminated by erasure)
         case AliasTypeDef(mods, name, tparams, rhs) => tree // (eliminated by erasure)
         case LabelDef(name, params, rhs) => super.transform(tree)
 
diff --git a/src/compiler/scala/tools/nsc/transform/UnCurry.scala b/src/compiler/scala/tools/nsc/transform/UnCurry.scala
index d6510e9aec..824e20a56e 100644
--- a/src/compiler/scala/tools/nsc/transform/UnCurry.scala
+++ b/src/compiler/scala/tools/nsc/transform/UnCurry.scala
@@ -81,7 +81,7 @@ abstract class UnCurry extends InfoTransform with TypingTransformers {
    *  - if symbol is a def parameter with transformed type T, return () => T
    */
   def transformInfo(sym: Symbol, tp: Type): Type =
-    if (sym.isType) uncurryType(tp) else uncurry(tp)
+    if (sym.isType) uncurryType(tp.normalize) else uncurry(tp.normalize)
 
   class UnCurryTransformer(unit: CompilationUnit) extends TypingTransformer(unit) {
 
diff --git a/src/compiler/scala/tools/nsc/typechecker/Contexts.scala b/src/compiler/scala/tools/nsc/typechecker/Contexts.scala
index eece1dabd0..156700d590 100644
--- a/src/compiler/scala/tools/nsc/typechecker/Contexts.scala
+++ b/src/compiler/scala/tools/nsc/typechecker/Contexts.scala
@@ -381,7 +381,8 @@ trait Contexts requires Analyzer {
         if (settings.debug.value) log("resetting " + sym + " to " + info);
         sym.info match {
           case TypeBounds(lo, hi) if (hi <:< lo && lo <:< hi) =>
-            current = current.subst(List(sym), List(lo))
+            current = current.instantiateTypeParams(List(sym), List(lo))
+//@M TODO: when higher-kinded types are inferred, probably need a case PolyType(_, TypeBounds(...)) if ... =>
           case _ =>
         }
         sym.setInfo(info)
diff --git a/src/compiler/scala/tools/nsc/typechecker/Infer.scala b/src/compiler/scala/tools/nsc/typechecker/Infer.scala
index 64e49e4b35..18b757d981 100644
--- a/src/compiler/scala/tools/nsc/typechecker/Infer.scala
+++ b/src/compiler/scala/tools/nsc/typechecker/Infer.scala
@@ -64,7 +64,7 @@ trait Infer requires Analyzer {
    *  @return       ...
    */
   def freshVar(tparam: Symbol): TypeVar =
-    new TypeVar(tparam.tpe, new TypeConstraint)
+    new TypeVar(tparam.tpe, new TypeConstraint)  //@M TODO: might be affected by change to tpe in Symbol
 
   //todo: remove comments around following privates; right now they cause an IllegalAccess
   // error when built with scalac
@@ -117,7 +117,7 @@ trait Infer requires Analyzer {
    */
   private def isWithinBounds(pre: Type, owner: Symbol, tparams: List[Symbol], targs: List[Type]): boolean = {
     val bounds = tparams map { tparam =>
-      tparam.info.asSeenFrom(pre, owner).subst(tparams, targs).bounds
+      tparam.info.asSeenFrom(pre, owner).instantiateTypeParams(tparams, targs).bounds
     }
     !(List.map2(bounds, targs)((bound, targ) => bound containsType targ) contains false)
   }
@@ -145,8 +145,8 @@ trait Infer requires Analyzer {
         for (val (tvar2, (tparam2, variance2)) <- config) {
           if (tparam2 != tparam &&
               ((bound contains tparam2) ||
-               up && (tparam2.info.bounds.lo =:= tparam.tpe) ||
-               !up && (tparam2.info.bounds.hi =:= tparam.tpe))) {
+               up && (tparam2.info.bounds.lo =:= tparam.tpe) ||  //@M TODO: might be affected by change to tpe in Symbol
+               !up && (tparam2.info.bounds.hi =:= tparam.tpe))) {  //@M TODO: might be affected by change to tpe in Symbol
             if (tvar2.constr.inst eq null) cyclic = true
             solveOne(tvar2, tparam2, variance2)
           }
@@ -155,21 +155,21 @@ trait Infer requires Analyzer {
           if (up) {
             if (bound.symbol != AnyClass) {
               tvar.constr.hibounds =
-                bound.subst(tparams, tvars) :: tvar.constr.hibounds
+                bound.instantiateTypeParams(tparams, tvars) :: tvar.constr.hibounds
             }
             for (val tparam2 <- tparams)
-              if (tparam2.info.bounds.lo =:= tparam.tpe)
+              if (tparam2.info.bounds.lo =:= tparam.tpe)  //@M TODO: might be affected by change to tpe in Symbol
                 tvar.constr.hibounds =
-                  tparam2.tpe.subst(tparams, tvars) :: tvar.constr.hibounds
+                  tparam2.tpe.instantiateTypeParams(tparams, tvars) :: tvar.constr.hibounds
           } else {
             if (bound.symbol != AllClass && bound.symbol != tparam) {
               tvar.constr.lobounds =
-                bound.subst(tparams, tvars) :: tvar.constr.lobounds
+                bound.instantiateTypeParams(tparams, tvars) :: tvar.constr.lobounds
             }
             for (val tparam2 <- tparams)
-              if (tparam2.info.bounds.hi =:= tparam.tpe)
+              if (tparam2.info.bounds.hi =:= tparam.tpe)  //@M TODO: might be affected by change to tpe in Symbol
                 tvar.constr.lobounds =
-                  tparam2.tpe.subst(tparams, tvars) :: tvar.constr.lobounds
+                  tparam2.tpe.instantiateTypeParams(tparams, tvars) :: tvar.constr.lobounds
           }
         }
         tvar.constr.inst = NoType // necessary because hibounds/lobounds may contain tvar
@@ -203,7 +203,7 @@ trait Infer requires Analyzer {
       normalize(restpe)
     case tp1 =>
       if (util.Statistics.enabled) normO = normO + 1
-      tp1
+      tp1 // @MAT aliases already handled by subtyping
   }
 
   private val stdErrorClass = RootClass.newErrorClass(nme.ERROR.toTypeName)
@@ -395,7 +395,7 @@ trait Infer requires Analyzer {
      */
     private def exprTypeArgs(tparams: List[Symbol], restpe: Type, pt: Type): List[Type] = {
       val tvars = tparams map freshVar
-      if (isCompatible(restpe.subst(tparams, tvars), pt)) {
+      if (isCompatible(restpe.instantiateTypeParams(tparams, tvars), pt)) {
         try {
           solve(tvars, tparams, tparams map varianceInType(restpe), false)
         } catch {
@@ -447,7 +447,7 @@ trait Infer requires Analyzer {
         case ex: NoInstance => WildcardType
       }
       val tvars = tparams map freshVar
-      if (isWeaklyCompatible(restpe.subst(tparams, tvars), pt))
+      if (isWeaklyCompatible(restpe.instantiateTypeParams(tparams, tvars), pt))
         List.map2(tparams, tvars) ((tparam, tvar) =>
           instantiateToBound(tvar, varianceInTypes(formals)(tparam)))
       else
@@ -483,7 +483,7 @@ trait Infer requires Analyzer {
       }
       // check first whether type variables can be fully defined from
       // expected result type.
-      if (!isWeaklyCompatible(restpe.subst(tparams, tvars), pt)) {
+      if (!isWeaklyCompatible(restpe.instantiateTypeParams(tparams, tvars), pt)) {
         throw new DeferredNoInstance(() =>
           "result type " + normalize(restpe) + " is incompatible with expected type " + pt)
       }
@@ -492,13 +492,13 @@ trait Infer requires Analyzer {
 
       // Then define remaining type variables from argument types.
       List.map2(argtpes, formals) {(argtpe, formal) =>
-        if (!isCompatible(argtpe.deconst.subst(tparams, tvars),
-                          formal.subst(tparams, tvars))) {
+        if (!isCompatible(argtpe.deconst.instantiateTypeParams(tparams, tvars),
+                          formal.instantiateTypeParams(tparams, tvars))) {
           if (settings.explaintypes.value)
-            explainTypes(argtpe.deconst.subst(tparams, tvars), formal.subst(tparams, tvars))
+            explainTypes(argtpe.deconst.instantiateTypeParams(tparams, tvars), formal.instantiateTypeParams(tparams, tvars))
           throw new DeferredNoInstance(() =>
             "argument expression's type is not compatible with formal parameter type" +
-            foundReqMsg(argtpe.deconst.subst(tparams, tvars), formal.subst(tparams, tvars)))
+            foundReqMsg(argtpe.deconst.instantiateTypeParams(tparams, tvars), formal.instantiateTypeParams(tparams, tvars)))
         }
         ()
       }
@@ -506,7 +506,7 @@ trait Infer requires Analyzer {
       List.map2(tparams, targs) {(tparam, targ) =>
         if (targ.symbol == AllClass && (varianceInType(restpe)(tparam) & COVARIANT) == 0) {
           uninstantiated += tparam
-          tparam.tpe
+          tparam.tpe  //@M TODO: might be affected by change to tpe in Symbol
         } else targ}
     }
 
@@ -535,7 +535,7 @@ trait Infer requires Analyzer {
             try {
               val uninstantiated = new ListBuffer[Symbol]
               val targs = methTypeArgs(undetparams, formals, restpe, argtpes, pt, uninstantiated)
-              (exprTypeArgs(uninstantiated.toList, restpe.subst(undetparams, targs), pt) ne null) &&
+              (exprTypeArgs(uninstantiated.toList, restpe.instantiateTypeParams(undetparams, targs), pt) ne null) &&
               isWithinBounds(NoPrefix, NoSymbol, undetparams, targs)
             } catch {
               case ex: NoInstance => false
@@ -595,8 +595,18 @@ trait Infer requires Analyzer {
 
     /** error if arguments not within bounds. */
     def checkBounds(pos: PositionType, pre: Type, owner: Symbol,
-                    tparams: List[Symbol], targs: List[Type], prefix: String) {
-      if (!isWithinBounds(pre, owner, tparams, targs)) {
+                    tparams: List[Symbol], targs: List[Type], prefix: String) = {
+      //@M validate variances & bounds of targs wrt variances & bounds of tparams
+      //@M TODO: better place to check this?
+      //@M TODO: errors for getters & setters are reported separately
+      val kindErrors = checkKindBounds(tparams, targs)
+
+      if(!kindErrors.isEmpty)
+        error(pos,
+          prefix + "the kinds of the type arguments " + targs.mkString("(", ",", ")") +
+          " do not conform to the expected kinds of the type parameters "+ tparams.mkString("(", ",", ")") + tparams.head.locationString+ "." +
+          kindErrors.toList.mkString("\n", ", ", ""))
+      else if (!isWithinBounds(pre, owner, tparams, targs)) {
         if (!(targs exists (.isErroneous)) && !(tparams exists (.isErroneous))) {
           error(pos,
                 prefix + "type arguments " + targs.mkString("[", ",", "]") +
@@ -604,7 +614,7 @@ trait Infer requires Analyzer {
                 (tparams map (.defString)).mkString("[", ",", "]"))
         }
         if (settings.explaintypes.value) {
-          val bounds = tparams map (.info.subst(tparams, targs).bounds)
+          val bounds = tparams map (tp => tp.info.instantiateTypeParams(tparams, targs).bounds)
           List.map2(targs, bounds)((targ, bound) => explainTypes(bound.lo, targ))
           List.map2(targs, bounds)((targ, bound) => explainTypes(targ, bound.hi))
           ()
@@ -612,6 +622,87 @@ trait Infer requires Analyzer {
       }
     }
 
+    /** Check whether <arg>sym1</arg>'s variance conforms to <arg>sym2</arg>'s variance
+     *
+     * If <arg>sym2</arg> is invariant, <arg>sym1</arg>'s variance is irrelevant. Otherwise they must be equal.
+     */
+    def variancesMatch(sym1: Symbol, sym2: Symbol): boolean = (sym2.variance==0 || sym1.variance==sym2.variance)
+
+    /** Check well-kindedness of type application (assumes arities are already checked) -- @M
+     *
+     * This check is also performed when abstract type members become concrete (aka a "type alias") -- then tparams.length==1
+     * (checked one type member at a time -- in that case, prefix is the name of the type alias)
+     *
+     * Type application is just like value application: it's "contravariant" in the sense that
+     * the type parameters of the supplied type arguments must conform to the type parameters of
+     * the required type parameters:
+     *   - their bounds must be less strict
+     *   - variances must match (here, variances are absolute, the variance of a type parameter does not influence the variance of its higher-order parameters)
+     *   - @M TODO: are these conditions correct,sufficient&necessary?
+     *
+     *  e.g. class Iterable[t, m[+x <: t]] --> the application Iterable[Int, List] is okay, since
+     *       List's type parameter is also covariant and its bounds are weaker than <: Int
+     */
+    def checkKindBounds(tparams: List[Symbol], targs: List[Type]): List[String] = {
+      // check that the type parameters <arg>hkargs</arg> to a higher-kinded type conform to the expected params <arg>hkparams</arg>
+      def checkKindBoundsHK(hkargs: List[Symbol], hkparams: List[Symbol]): (List[(Symbol, Symbol)], List[(Symbol, Symbol)]) = {
+        val _varianceMismatches = new ListBuffer[(Symbol, Symbol)]
+        val _stricterBounds = new ListBuffer[(Symbol, Symbol)]
+        def varianceMismatch(a: Symbol, p: Symbol): unit = _varianceMismatches += (a, p)
+        def stricterBound(a: Symbol, p: Symbol): unit = _stricterBounds += (a, p)
+        def varianceMismatches(as: Iterable[(Symbol, Symbol)]): unit = _varianceMismatches ++= as
+        def stricterBounds(as: Iterable[(Symbol, Symbol)]): unit = _stricterBounds ++= as
+
+        for(val (hkarg, hkparam) <- hkargs zip hkparams) {
+          if(hkparam.typeParams.isEmpty) { // base-case: kind *
+            if(!variancesMatch(hkarg, hkparam))
+              varianceMismatch(hkarg, hkparam)
+
+            // instantiateTypeParams(tparams, targs) --> higher-order bounds may contain references to type arguments
+            // substSym(hkparams, hkargs) --> these types are going to be compared as types of kind *
+            //    --> their arguments use different symbols, but are conceptually the same
+            //        (could also replace the types by polytypes, but can't just strip the symbols, as ordering is lost then)
+            if(!(hkparam.info.instantiateTypeParams(tparams, targs).bounds.substSym(hkparams, hkargs) <:< hkarg.info.bounds))
+              stricterBound(hkarg, hkparam)
+          } else {
+            val (vm, sb) = checkKindBoundsHK(hkarg.typeParams, hkparam.typeParams)
+            varianceMismatches(vm)
+            stricterBounds(sb)
+          }
+        }
+
+        (_varianceMismatches.toList, _stricterBounds.toList)
+      }
+
+      // @M TODO this method is duplicated all over the place (varianceString)
+      def varStr(s: Symbol): String =
+        if (s.isCovariant) "covariant"
+        else if (s.isContravariant) "contravariant"
+        else "invariant";
+
+      def qualify(a0: Symbol, b0: Symbol): String = if(a0.toString != b0.toString) "" else {
+        assert((a0 ne b0) && (a0.owner ne b0.owner)); var a=a0; var b=b0
+        while(a.owner.name == b.owner.name) {a=a.owner; b=b.owner}
+        if(a.locationString ne "") " (" + a.locationString.trim + ")" else ""
+      }
+
+      val errors = new ListBuffer[String]
+      (tparams zip targs).foreach{ case (tparam, targ) if(targ.isHigherKinded) =>
+        val (varianceMismatches, stricterBounds) = checkKindBoundsHK(targ.typeParams, tparam.typeParams)
+
+        if(!(varianceMismatches.isEmpty && stricterBounds.isEmpty)){
+          errors += (targ+"'s type parameters do not match "+tparam+"'s expected parameters: "+
+            (for(val (a,p) <- varianceMismatches) yield a+qualify(a,p)+ " is "+varStr(a)+", but "+
+              p+qualify(p,a)+" is declared "+varStr(p)).toList.mkString("", ", ", "") +
+            (for(val (a,p) <- stricterBounds) yield a+qualify(a,p)+"'s bounds "+a.info+" are stricter than "+
+              p+qualify(p,a)+"'s declared bounds "+p.info).toList.mkString("", ", ", ""))
+        }
+        case _ =>
+      }
+
+      errors.toList
+    }
+
     /** Substitite free type variables `undetparams' of polymorphic argument
      *  expression `tree', given two prototypes `strictPt', and `lenientPt'.
      *  `strictPt' is the first attempt prototype where type parameters
@@ -717,7 +808,7 @@ trait Infer requires Analyzer {
     }
 
     /** Type with all top-level occurrences of abstract types replaced by their bounds */
-    def widen(tp: Type): Type = tp match {
+    def widen(tp: Type): Type = tp.normalize match {
       case TypeRef(pre, sym, _) if sym.isAbstractType =>
         widen(tp.bounds.hi)
       case rtp @ RefinedType(parents, decls) =>
@@ -752,28 +843,28 @@ trait Infer requires Analyzer {
         }
       def instError = {
         if (settings.debug.value) Console.println("ici " + tree + " " + undetparams + " " + pt)
-        if (settings.explaintypes.value) explainTypes(restpe.subst(undetparams, tvars), pt)
+        if (settings.explaintypes.value) explainTypes(restpe.instantiateTypeParams(undetparams, tvars), pt)
         errorTree(tree, "constructor cannot be instantiated to expected type" +
                   foundReqMsg(restpe, pt))
       }
-      if (restpe.subst(undetparams, tvars) <:< pt) {
+      if (restpe.instantiateTypeParams(undetparams, tvars) <:< pt) {
         computeArgs
       } else if (isFullyDefined(pt)) {
         if (settings.debug.value) log("infer constr " + tree + ":" + restpe + ", pt = " + pt)
         var ptparams = freeTypeParamsOfTerms.collect(pt)
         if (settings.debug.value) log("free type params = " + ptparams)
-        val ptWithWildcards = pt.subst(ptparams, ptparams map (ptparam => WildcardType))
+        val ptWithWildcards = pt.instantiateTypeParams(ptparams, ptparams map (ptparam => WildcardType))
         tvars = undetparams map freshVar
-        if (restpe.subst(undetparams, tvars) <:< ptWithWildcards) {
+        if (restpe.instantiateTypeParams(undetparams, tvars) <:< ptWithWildcards) {
           computeArgs
           restpe = skipImplicit(tree.tpe.resultType)
           if (settings.debug.value) log("new tree = " + tree + ":" + restpe)
           val ptvars = ptparams map freshVar
-          val pt1 = pt.subst(ptparams, ptvars)
+          val pt1 = pt.instantiateTypeParams(ptparams, ptvars)
           if (isPopulated(restpe, pt1)) {
             ptvars foreach instantiateTypeVar
           } else { if (settings.debug.value) Console.println("no instance: "); instError }
-        } else { if (settings.debug.value) Console.println("not a subtype " + restpe.subst(undetparams, tvars) + " of " + ptWithWildcards); instError }
+        } else { if (settings.debug.value) Console.println("not a subtype " + restpe.instantiateTypeParams(undetparams, tvars) + " of " + ptWithWildcards); instError }
       } else { if (settings.debug.value) Console.println("not fuly defined: " + pt); instError }
     }
 
@@ -869,14 +960,14 @@ trait Infer requires Analyzer {
         val tpparams = freeTypeParamsOfTerms.collect(pattp)
         if (settings.debug.value) log("free type params (1) = " + tpparams)
         var tvars = tpparams map freshVar
-        var tp = pattp.subst(tpparams, tvars)
+        var tp = pattp.instantiateTypeParams(tpparams, tvars)
         if (!(tp <:< pt)) {
           tvars = tpparams map freshVar
-          tp = pattp.subst(tpparams, tvars)
+          tp = pattp.instantiateTypeParams(tpparams, tvars)
           val ptparams = freeTypeParamsOfTerms.collect(pt)
           if (settings.debug.value) log("free type params (2) = " + ptparams)
           val ptvars = ptparams map freshVar
-          val pt1 = pt.subst(ptparams, ptvars)
+          val pt1 = pt.instantiateTypeParams(ptparams, ptvars)
           if (!isPopulated(tp, pt1)) {
             error(pos, "pattern type is incompatibe with expected type"+foundReqMsg(pattp, pt))
             return pattp
@@ -893,7 +984,7 @@ trait Infer requires Analyzer {
         val ptparams = freeTypeParamsOfTerms.collect(pt)
         if (settings.debug.value) log("free type params (2) = " + ptparams)
         val ptvars = ptparams map freshVar
-        val pt1 = pt.subst(ptparams, ptvars)
+        val pt1 = pt.instantiateTypeParams(ptparams, ptvars)
         if (pat.tpe <:< pt1)
           ptvars foreach instantiateTypeVar
         else
@@ -912,7 +1003,7 @@ trait Infer requires Analyzer {
       protected def includeCondition(sym: Symbol): boolean
 
       override def traverse(tp: Type): TypeTraverser = {
-        tp match {
+        tp.normalize match {
           case TypeRef(_, sym, _) =>
             if (includeCondition(sym) && !result.contains(sym)) result = sym :: result
           case _ =>
@@ -934,7 +1025,7 @@ trait Infer requires Analyzer {
     }
 
     object approximateAbstracts extends TypeMap {
-      def apply(tp: Type): Type = tp match {
+      def apply(tp: Type): Type = tp.normalize match {
         case TypeRef(pre, sym, _) if sym.isAbstractType => WildcardType
         case _ => mapOver(tp)
       }
@@ -1110,7 +1201,7 @@ trait Infer requires Analyzer {
           if (sym.hasFlag(OVERLOADED)) {
             val tparams = new AsSeenFromMap(pre, sym.alternatives.head.owner).mapOver(
               sym.alternatives.head.typeParams)
-            val bounds = tparams map (.tpe)
+            val bounds = tparams map (.tpe)  //@M TODO: might be affected by change to tpe in Symbol
             val tpe =
               PolyType(tparams,
                        OverloadedType(AntiPolyType(pre, bounds), sym.alternatives))
diff --git a/src/compiler/scala/tools/nsc/typechecker/Namers.scala b/src/compiler/scala/tools/nsc/typechecker/Namers.scala
index c41a30de7e..be5d2600d9 100644
--- a/src/compiler/scala/tools/nsc/typechecker/Namers.scala
+++ b/src/compiler/scala/tools/nsc/typechecker/Namers.scala
@@ -46,6 +46,15 @@ trait Namers requires Analyzer {
   protected final def doEnterValueParams = !inIDE;
   protected def inIDE = false;
 
+  //@M a worklist of AbsTypeDef trees we must process when the next finishWith is called
+  // example: trait FOO3[m[A <: B], B]
+  // if we go depth-first, B will not be in scope yet when we create the context in which A <: B will be typed
+  // instead, an AbsTypeDef registers its type parameters in lateParams, which will be processed when all
+  // type parameters in the enclosing scope have been entered (i.e., when m as well as B have been entered by
+  // the finishWith in the case for ClassDef in enterSym, that finishWith will then handle m's type param, A,
+  // which has been registered in lateParams by the finishWithLate in the case for AbsTypeDef)
+  private val lateParams = new scala.collection.mutable.ListBuffer[(Namer, Symbol, Tree, List[AbsTypeDef])]
+
   class Namer(val context: Context) {
 
     val typer = newTyper(context)
@@ -113,14 +122,14 @@ trait Namers requires Analyzer {
     def enterInScope(sym: Symbol): Symbol = {
       // allow for overloaded methods
       if (!(sym.isSourceMethod && sym.owner.isClass && !sym.owner.isPackageClass)) {
-      	val prev = context.scope.lookupEntry(sym.name);
-      	if ((prev ne null) && prev.owner == context.scope &&
+        val prev = context.scope.lookupEntry(sym.name);
+        if ((prev ne null) && prev.owner == context.scope &&
             (!prev.sym.isSourceMethod ||
              nme.isSetterName(sym.name) ||
              sym.owner.isPackageClass)) {
-     	   doubleDefError(sym.pos, prev.sym)
+           doubleDefError(sym.pos, prev.sym)
            sym setInfo ErrorType
-      	} else context.scope enter sym
+        } else context.scope enter sym
       } else context.scope enter sym
       sym
     }
@@ -152,9 +161,9 @@ trait Namers requires Analyzer {
         c = enterInScope(context.owner.newClass(pos, name)).setFlag(flags | inConstructorFlag)
       }
       if (c.owner.isPackageClass) {
-      	val file = context.unit.source.getFile()
-      	val clazz = c.asInstanceOf[ClassSymbol]
-      	if (settings.debug.value && (clazz.sourceFile ne null) && !clazz.sourceFile.equals(file)) {
+        val file = context.unit.source.getFile()
+        val clazz = c.asInstanceOf[ClassSymbol]
+        if (settings.debug.value && (clazz.sourceFile ne null) && !clazz.sourceFile.equals(file)) {
           Console.err.println("SOURCE MISMATCH: " + clazz.sourceFile + " vs. " + file + " SYM=" + c);
         }
         clazz.sourceFile = file
@@ -211,12 +220,14 @@ trait Namers requires Analyzer {
       val tskolems = tparams map (.newTypeSkolem)
       val ltp = new LazyType {
         override def complete(sym: Symbol): unit =
-          sym setInfo sym.deSkolemize.info.substSym(tparams, tskolems)
+          sym setInfo sym.deSkolemize.info.substSym(tparams, tskolems) //@M the info of a skolem is the skolemized info of the actual type parameter of the skolem
       }
       tskolems foreach (.setInfo(ltp))
       tskolems
     }
 
+    //@M? Replace type parameters with their TypeSkolems, which can later be deskolemized to the original type param
+    // (a skolem is a representation of a bound variable when viewed outside its scope?)
     def skolemize(tparams: List[AbsTypeDef]): unit = {
       val tskolems = newTypeSkolems(tparams map (.symbol))
       for (val (tparam, tskolem) <- tparams zip tskolems) tparam.symbol = tskolem
@@ -228,40 +239,63 @@ trait Namers requires Analyzer {
 
     def deSkolemize: TypeMap = new DeSkolemizeMap(applicableTypeParams(context.owner))
 
-    def enterSym(tree: Tree): Context = {
 
-      def finishWith(tparams: List[AbsTypeDef]): unit = {
-        val sym = tree.symbol
-        if (settings.debug.value) log("entered " + sym + " in " + context.owner + ", scope-id = " + context.scope.hashCode());
-        var ltype: LazyType = namerOf(sym).typeCompleter(tree)
-        if (!tparams.isEmpty) {
-          new Namer(context.makeNewScope(tree, sym)).enterSyms(tparams)
-          ltype = new LazyPolyType(tparams map (.symbol), ltype)
-          if (sym.isTerm) skolemize(tparams)
+    private def doLateParams = if(!lateParams.isEmpty) {
+        val todo = lateParams.toList
+        lateParams.clear
+        for(val rec <- todo) {
+          rec._1.finishWith0(rec._2, rec._3, rec._4)
         }
-        sym.setInfo(ltype)
       }
-      def finish = finishWith(List())
 
+    private def finishWith0(sym: Symbol, tree: Tree, tparams: List[AbsTypeDef]): unit = {
+      if (settings.debug.value) log("entered " + sym + " in " + context.owner + ", scope-id = " + context.scope.hashCode());
+
+      var ltype: LazyType = namerOf(sym).typeCompleter(tree)
+
+      if (!tparams.isEmpty) {
+        new Namer(context.makeNewScope(tree, sym)).enterSyms(tparams)
+
+        ltype = new LazyPolyType(tparams map (.symbol), ltype)
+
+        if (sym.isTerm) // skolemize the type parameters of a method
+         skolemize(tparams)
+      }
+
+      sym.setInfo(ltype)
+
+      doLateParams
+    }
+
+    def enterSym(tree: Tree): Context = {
+      def finishWith(tparams: List[AbsTypeDef]): unit = finishWith0(tree.symbol, tree, tparams)
+      def finish = finishWith(List())
+      def finishWithLate(tparams: List[AbsTypeDef]): unit = {
+        if(tparams.isEmpty) finishWith(tparams)
+        else {
+          lateParams += (this, tree.symbol, tree, tparams) // this and tree.symbol must be remembered too, these will change by the time the worklist is performed (new nested namer, skolemization for tree's symbol)
+        }
+      }
 
       if (tree.symbol == NoSymbol) {
-	val owner = context.owner
-	tree match {
-	  case PackageDef(name, stats) =>
-	    tree.symbol = enterPackageSymbol(tree.pos, name)
-	    val namer = new Namer(
-	      context.make(tree, tree.symbol.moduleClass, tree.symbol.info.decls))
-	    namer.enterSyms(stats)
-	  case ClassDef(mods, name, tparams, _, impl) =>
-	    if ((mods.flags & CASE) != 0) { // enter case factory method.
-	      tree.symbol = enterCaseFactorySymbol(
-        		tree.pos, mods.flags & AccessFlags | METHOD | CASE, name.toTermName)
+        val owner = context.owner
+        tree match {
+          case PackageDef(name, stats) =>
+            tree.symbol = enterPackageSymbol(tree.pos, name)
+            val namer = new Namer(
+                context.make(tree, tree.symbol.moduleClass, tree.symbol.info.decls))
+            namer.enterSyms(stats)
+          case ClassDef(mods, name, tparams, _, impl) =>
+            if ((mods.flags & CASE) != 0) { // enter case factory method.
+              tree.symbol = enterCaseFactorySymbol(
+                  tree.pos, mods.flags & AccessFlags | METHOD | CASE, name.toTermName)
               tree.symbol.setInfo(namerOf(tree.symbol).caseFactoryCompleter(tree))
               setPrivateWithin(tree, tree.symbol, mods)
             }
             tree.symbol = enterClassSymbol(tree.pos, mods.flags, name)
             setPrivateWithin(tree, tree.symbol, mods)
             finishWith(tparams)
+            assert(lateParams.isEmpty)
           case ModuleDef(mods, name, _) =>
             tree.symbol = enterModuleSymbol(tree.pos, mods.flags | MODULE | FINAL, name)
             setPrivateWithin(tree, tree.symbol, mods)
@@ -278,16 +312,16 @@ trait Namers requires Analyzer {
               enterInScope(getter)
               if ((mods.flags & MUTABLE) != 0) {
                 val setter = owner.newMethod(tree.pos, nme.getterToSetter(name))
-        	  .setFlag(accflags & ~STABLE & ~CASEACCESSOR)
+                                .setFlag(accflags & ~STABLE & ~CASEACCESSOR)
                 setter.setInfo(namerOf(setter).setterTypeCompleter(tree))
                 setPrivateWithin(tree, setter, mods)
                 enterInScope(setter)
               }
               tree.symbol =
-        	if ((mods.flags & DEFERRED) == 0) {
+                if ((mods.flags & DEFERRED) == 0) {
                   val value =
-        	    enterInScope(owner.newValue(tree.pos, nme.getterToLocal(name)))
- 	              .setFlag(mods.flags & FieldFlags | PRIVATE | LOCAL)
+                    enterInScope(owner.newValue(tree.pos, nme.getterToLocal(name)))
+                                  .setFlag(mods.flags & FieldFlags | PRIVATE | LOCAL)
                   value.setInfo(namerOf(value).typeCompleter(tree))
                   value
                 } else getter;
@@ -301,16 +335,18 @@ trait Namers requires Analyzer {
               .setFlag(mods.flags | owner.getFlag(ConstrFlags))
             setPrivateWithin(tree, tree.symbol, mods)
             finishWith(tparams)
+            assert(lateParams.isEmpty)
           case DefDef(mods, name, tparams, _, _, _) =>
             tree.symbol = enterInScope(owner.newMethod(tree.pos, name))
               .setFlag(mods.flags)
             setPrivateWithin(tree, tree.symbol, mods)
             finishWith(tparams)
-          case AbsTypeDef(mods, name, _, _) =>
+            assert(lateParams.isEmpty)
+          case AbsTypeDef(mods, name, tparams, _, _) =>
             tree.symbol = enterInScope(owner.newAbstractType(tree.pos, name))
               .setFlag(mods.flags)
             setPrivateWithin(tree, tree.symbol, mods)
-            finish
+            finishWithLate(tparams) // @M! enter this AbsTypeDef's type params in scope after all the siblings of this abstypedef have been entered (e.g., in [A[x <: B], B], A and B are entered first, then x is entered)
           case AliasTypeDef(mods, name, tparams, _) =>
             tree.symbol = enterInScope(owner.newAliasType(tree.pos, name))
               .setFlag(mods.flags)
@@ -331,7 +367,7 @@ trait Namers requires Analyzer {
 // --- Lazy Type Assignment --------------------------------------------------
 
     def typeCompleter(tree: Tree) = new TypeCompleter(tree) {
-      override def complete(sym: Symbol): unit = {
+      override def complete(sym: Symbol): unit = {  //@M? toString (on sym/tree/...? don't know exactly) will force a lazy type and execute this method (quantum debugging!)
         if (settings.debug.value) log("defining " + sym);
         val tp = typeSig(tree)
         sym.setInfo(tp)
@@ -428,7 +464,10 @@ trait Namers requires Analyzer {
       }
       val parents = typer.parentTypes(templ) map checkParent
       val decls = newDecls(templ, clazz)
-      new Namer(context.make(templ, clazz, decls)).enterSyms(templ.body)
+      val namer = new Namer(context.make(templ, clazz, decls))
+      namer.enterSyms(templ.body)
+      namer.doLateParams // @M set info on higher-kinded type members -- @M TODO cleanup & document
+
       ClassInfoType(parents, decls, clazz)
     }
 
@@ -564,8 +603,8 @@ trait Namers requires Analyzer {
         for (val r <- required(tp)) {
           if (!isContainedIn(r, p) || (r =:= p)) {
             context.error(sym.pos, "implicit " + sym + " is not contractive," +
-        		  "\n because the implicit parameter type " + r +
-        		  "\n is not strictly contained in the signature " + p);
+                          "\n because the implicit parameter type " + r +
+                          "\n is not strictly contained in the signature " + p);
             result = ErrorType;
           }
         }
@@ -573,6 +612,19 @@ trait Namers requires Analyzer {
       result
     }
 
+    //@M! an abstract type definition (abstract type member/type parameter) may take type parameters, which are in scope in its bounds
+    private def abstractTypeSig(tree: Tree, tpsym: Symbol, tparams: List[AbsTypeDef], lo: Tree, hi: Tree) = {
+      val tparamSyms = typer.reenterTypeParams(tparams) //@M make tparams available in scope (just for this abstypedef)
+
+      var lt = typer.typedType(lo).tpe
+      if (lt.isError) lt = AllClass.tpe
+
+      var ht = typer.typedType(hi).tpe
+      if (ht.isError) ht = AnyClass.tpe
+
+      makePolyType(tparamSyms,  mkTypeBounds(lt, ht)) //@M
+    }
+
     private def aliasTypeSig(tpsym: Symbol, tparams: List[AbsTypeDef], rhs: Tree): Type =
       makePolyType(typer.reenterTypeParams(tparams), typer.typedType(rhs).tpe);
 
@@ -611,8 +663,8 @@ trait Namers requires Analyzer {
             case vdef @ ValDef(mods, _, tpt, rhs) =>
               if (tpt.isEmpty) {
                 if (rhs.isEmpty) {
-        	  context.error(tpt.pos, "missing parameter type");
-        	  ErrorType
+                  context.error(tpt.pos, "missing parameter type");
+                  ErrorType
                 } else {
         	  tpt.tpe = deconstIfNotFinal(sym,
                     typer.valDefRhsTyper(vdef).computeType(rhs, WildcardType))
@@ -629,12 +681,8 @@ trait Namers requires Analyzer {
             case tree @ AliasTypeDef(_, _, tparams, rhs) =>
               new Namer(makeNewScope(context, tree, sym)).aliasTypeSig(sym, tparams, rhs)
 
-            case AbsTypeDef(_, _, lo, hi) =>
-              var lt = typer.typedType(lo).tpe
-              if (lt.isError) lt = AllClass.tpe
-              var ht = typer.typedType(hi).tpe
-              if (ht.isError) ht = AnyClass.tpe
-              mkTypeBounds(lt, ht)
+            case AbsTypeDef(_, _, tparams, lo, hi) =>
+              new Namer(makeNewScope(context, tree, sym)).abstractTypeSig(tree, sym, tparams, lo, hi) //@M!
 
             case Import(expr, selectors) =>
               val expr1 = typer.typedQualifier(expr)
@@ -661,17 +709,17 @@ trait Namers requires Analyzer {
               }
               def checkSelectors(selectors: List[(Name, Name)]): unit = selectors match {
                 case (from, to) :: rest =>
-        	  if (from != nme.WILDCARD && base != ErrorType) {
-        	    if (base.member(from) == NoSymbol && base.member(from.toTypeName) == NoSymbol)
-        	      context.error(tree.pos, from.decode + " is not a member of " + expr);
+                  if (from != nme.WILDCARD && base != ErrorType) {
+                    if (base.member(from) == NoSymbol && base.member(from.toTypeName) == NoSymbol)
+                      context.error(tree.pos, from.decode + " is not a member of " + expr);
                     if (checkNotRedundant(tree.pos, from, to))
                       checkNotRedundant(tree.pos, from.toTypeName, to.toTypeName)
                   }
-        	  if (from != nme.WILDCARD && (rest.exists (sel => sel._1 == from)))
-        	    context.error(tree.pos, from.decode + " is renamed twice");
-        	  if ((to ne null) && to != nme.WILDCARD && (rest exists (sel => sel._2 == to)))
-        	    context.error(tree.pos, to.decode + " appears twice as a target of a renaming");
-        	  checkSelectors(rest)
+                  if (from != nme.WILDCARD && (rest.exists (sel => sel._1 == from)))
+                    context.error(tree.pos, from.decode + " is renamed twice");
+                  if ((to ne null) && to != nme.WILDCARD && (rest exists (sel => sel._2 == to)))
+                    context.error(tree.pos, to.decode + " appears twice as a target of a renaming");
+                  checkSelectors(rest)
                 case Nil =>
               }
               checkSelectors(selectors)
diff --git a/src/compiler/scala/tools/nsc/typechecker/RefChecks.scala b/src/compiler/scala/tools/nsc/typechecker/RefChecks.scala
index 00e015956c..39ff15d671 100644
--- a/src/compiler/scala/tools/nsc/typechecker/RefChecks.scala
+++ b/src/compiler/scala/tools/nsc/typechecker/RefChecks.scala
@@ -72,11 +72,13 @@ abstract class RefChecks extends InfoTransform {
      *    1.2. O must not be final.
      *    1.3. O is deferred, or M has `override' modifier.
      *    1.4. If O is an immutable value, then so is M.
-     *    1.5. Neither M nor O are a parameterized type alias
+     *     // @M: LIFTED 1.5. Neither M nor O are a parameterized type alias
      *    1.6. If O is a type alias, then M is an alias of O.
      *    1.7. If O is an abstract type then
-     *         either M is an abstract type, and M's bounds are sharper than O's bounds.
-     *         or M is an unparameterized type alias or class which conforms to O's bounds.
+     *       1.7.1 either M is an abstract type, and M's bounds are sharper than O's bounds.
+     *             or M is a type alias or class which conforms to O's bounds.
+     *       1.7.2 higher-order type arguments must respect bounds on higher-order type parameters  -- @M
+     *              (explicit bounds and those implied by variance annotations) -- @see checkKindBounds
      *    1.8. If O and M are values, then
      *    1.8.1  M's type is a subtype of O's type, or
      *    1.8.2  M is of type []S, O is of type ()T and S <: T, or
@@ -100,7 +102,7 @@ abstract class RefChecks extends InfoTransform {
                 else "")))
       }
 
-      def overridesType(tp1: Type, tp2: Type): boolean = (tp1, tp2) match {
+      def overridesType(tp1: Type, tp2: Type): boolean = (tp1.normalize, tp2.normalize) match {
         case (MethodType(List(), rtp1), PolyType(List(), rtp2)) =>
           rtp1 <:< rtp2
         case (PolyType(List(), rtp1), MethodType(List(), rtp2)) =>
@@ -115,52 +117,52 @@ abstract class RefChecks extends InfoTransform {
        *  <code>member</code> are met.
        */
       def checkOverride(clazz: Symbol, member: Symbol, other: Symbol): unit = {
-	val pos = if (member.owner == clazz) member.pos else clazz.pos
+        val pos = if (member.owner == clazz) member.pos else clazz.pos
 
-	def overrideError(msg: String): unit =
-	  if (other.tpe != ErrorType && member.tpe != ErrorType)
-	    unit.error(pos, "error overriding " + infoString(other) +
-		       ";\n " + infoString(member) + " " + msg);
+        def overrideError(msg: String): unit =
+          if (other.tpe != ErrorType && member.tpe != ErrorType)
+            unit.error(pos, "error overriding " + infoString(other) +
+                       ";\n " + infoString(member) + " " + msg);
 
-	def overrideTypeError(): unit = {
-	  if (other.tpe != ErrorType && member.tpe != ErrorType) {
-	    overrideError("has incompatible type "+analyzer.underlying(member).tpe);
-	    explainTypes(member.tpe, other.tpe);
-	  }
-	}
+        def overrideTypeError(): unit = {
+          if (other.tpe != ErrorType && member.tpe != ErrorType) {
+            overrideError("has incompatible type "+analyzer.underlying(member).tpe.normalize);
+            explainTypes(member.tpe, other.tpe);
+          }
+        }
 
         def overrideAccessError(): unit = {
           val pwString = if (other.privateWithin == NoSymbol) ""
                          else other.privateWithin.name.toString
           val otherAccess = flagsToString(other getFlag (PRIVATE | PROTECTED), pwString)
-	  overrideError("has weaker access privileges; it should be "+
+          overrideError("has weaker access privileges; it should be "+
                         (if (otherAccess == "") "public" else "at least "+otherAccess))
         }
 
-	//Console.println(infoString(member) + " overrides " + infoString(other) + " in " + clazz);//DEBUG
-
-	// return if we already checked this combination elsewhere
-	if (member.owner != clazz) {
-	  if ((member.owner isSubClass other.owner) &&
-	      ((member hasFlag DEFERRED) || !(other hasFlag DEFERRED))) {
-		//Console.println(infoString(member) + " shadows1 " + infoString(other) " in " + clazz);//DEBUG
-		return;
-	      }
-	  if (clazz.info.parents exists (parent =>
-	    (parent.symbol isSubClass other.owner) && (parent.symbol isSubClass member.owner) &&
-	    ((member hasFlag DEFERRED) || !(other hasFlag DEFERRED)))) {
-	      //Console.println(infoString(member) + " shadows2 " + infoString(other) + " in " + clazz);//DEBUG
-		return;
-	    }
-	  if (clazz.info.parents forall (parent =>
-	    (parent.symbol isSubClass other.owner) == (parent.symbol isSubClass member.owner))) {
-	      //Console.println(infoString(member) + " shadows " + infoString(other) + " in " + clazz);//DEBUG
-	      return;
-	    }
-	}
-
-	if (member hasFlag PRIVATE) { // (1.1)
-	  overrideError("has weaker access privileges; it should not be private")
+        //Console.println(infoString(member) + " overrides " + infoString(other) + " in " + clazz);//DEBUG
+
+        // return if we already checked this combination elsewhere
+        if (member.owner != clazz) {
+          if ((member.owner isSubClass other.owner) &&
+              ((member hasFlag DEFERRED) || !(other hasFlag DEFERRED))) {
+                //Console.println(infoString(member) + " shadows1 " + infoString(other) " in " + clazz);//DEBUG
+                return;
+              }
+          if (clazz.info.parents exists (parent =>
+            (parent.symbol isSubClass other.owner) && (parent.symbol isSubClass member.owner) &&
+            ((member hasFlag DEFERRED) || !(other hasFlag DEFERRED)))) {
+              //Console.println(infoString(member) + " shadows2 " + infoString(other) + " in " + clazz);//DEBUG
+                return;
+            }
+          if (clazz.info.parents forall (parent =>
+            (parent.symbol isSubClass other.owner) == (parent.symbol isSubClass member.owner))) {
+              //Console.println(infoString(member) + " shadows " + infoString(other) + " in " + clazz);//DEBUG
+              return;
+            }
+        }
+
+        if (member hasFlag PRIVATE) { // (1.1)
+          overrideError("has weaker access privileges; it should not be private")
         }
         val mb = member.accessBoundary(member.owner)
         val ob = other.accessBoundary(member.owner)
@@ -170,81 +172,106 @@ abstract class RefChecks extends InfoTransform {
              (other hasFlag PROTECTED) && !(member hasFlag PROTECTED))) {
           overrideAccessError()
         } else if (other hasFlag FINAL) { // (1.2)
-	  overrideError("cannot override final member");
-	} else if (!(other hasFlag DEFERRED) && !(member hasFlag (OVERRIDE | ABSOVERRIDE))) { // (1.3)
-	  overrideError("needs `override' modifier");
-	} else if ((other hasFlag ABSOVERRIDE) && other.isIncompleteIn(clazz) && !(member hasFlag ABSOVERRIDE)) {
-	  overrideError("needs `abstract override' modifiers")
+          overrideError("cannot override final member");
+        } else if (!(other hasFlag DEFERRED) && !(member hasFlag (OVERRIDE | ABSOVERRIDE))) { // (1.3)
+          overrideError("needs `override' modifier");
+        } else if ((other hasFlag ABSOVERRIDE) && other.isIncompleteIn(clazz) && !(member hasFlag ABSOVERRIDE)) {
+          overrideError("needs `abstract override' modifiers")
         } else if ((member hasFlag (OVERRIDE | ABSOVERRIDE)) &&
                    (other hasFlag ACCESSOR) && other.accessed.isVariable) {
           overrideError("cannot override a mutable variable")
-	} else if (other.isStable && !member.isStable) { // (1.4)
-	  overrideError("needs to be an immutable value")
+        } else if (other.isStable && !member.isStable) { // (1.4)
+          overrideError("needs to be an immutable value")
         } else if (other.isStable && !(other hasFlag DEFERRED) && other.owner.isTrait && (member hasFlag OVERRIDE)) {
           overrideError("cannot override a value or variable definition in a trait " +
                         "\n (this is an implementation restriction)")
-	} else {
-	  if (other.isAliasType) {
-	    if (!member.typeParams.isEmpty) // (1.5)
-	      overrideError("may not be parameterized");
-	    if (!other.typeParams.isEmpty) // (1.5)
-	      overrideError("may not override parameterized type");
-	    if (!(self.memberType(member) =:= self.memberType(other))) // (1.6)
-	      overrideTypeError();
-	  } else if (other.isAbstractType) {
-	    if (!member.typeParams.isEmpty) // (1.7)
-	      overrideError("may not be parameterized");
-	    if (!(self.memberInfo(other).bounds containsType self.memberType(member))) { // (1.7) {
-	      overrideTypeError(); // todo: do an explaintypes with bounds here
+        } else {
+          if (other.isAliasType) {
+            //if (!member.typeParams.isEmpty) // (1.5)  @MAT
+            //  overrideError("may not be parameterized");
+            //if (!other.typeParams.isEmpty) // (1.5)   @MAT
+            //  overrideError("may not override parameterized type");
+            // @M: substSym
+            if (!(self.memberType(member).substSym(member.typeParams, other.typeParams) =:= self.memberType(other))) // (1.6)
+              overrideTypeError();
+          } else if (other.isAbstractType) {
+            //if (!member.typeParams.isEmpty) // (1.7)  @MAT
+            //  overrideError("may not be parameterized");
+            var memberTp = self.memberType(member)
+
+            if (!(self.memberInfo(other).bounds containsType memberTp)) { // (1.7.1) {
+              overrideTypeError(); // todo: do an explaintypes with bounds here
             }
-	  } else if (other.isTerm) {
-	    if (!overridesType(self.memberInfo(member), self.memberInfo(other))) { // 8
-	      overrideTypeError();
+
+            // check overriding (abstract type --> abstract type or abstract type --> concrete type member (a type alias))
+            // making an abstract type member concrete is like passing a type argument
+            val kindErrors = typer.infer.checkKindBounds(List(other), List(memberTp)) // (1.7.2)
+
+            if(!kindErrors.isEmpty)
+              unit.error(member.pos,
+                "The kind of "+member.keyString+" "+member.varianceString + member.nameString+
+                " does not conform to the expected kind of " + other.defString + other.locationString + "." +
+                kindErrors.toList.mkString("\n", ", ", ""))
+
+            // check a type alias's RHS corresponds to its declaration
+            // this overlaps somewhat with validateVariance
+            if(member.isAliasType) {
+              val kindErrors = typer.infer.checkKindBounds(List(member), List(memberTp.normalize))
+
+              if(!kindErrors.isEmpty)
+                unit.error(member.pos,
+                  "The kind of the right-hand side "+memberTp.normalize+" of "+member.keyString+" "+
+                  member.varianceString + member.nameString+ " does not conform to its expected kind."+
+                  kindErrors.toList.mkString("\n", ", ", ""))
+            }
+          } else if (other.isTerm) {
+            if (!overridesType(self.memberInfo(member), self.memberInfo(other))) { // 8
+              overrideTypeError();
             }
-	  }
-	}
+          }
+        }
       }
 
       val opc = new overridingPairs.Cursor(clazz)
       while (opc.hasNext) {
-	//Console.println("overrides " + opc.overriding/* + ":" + opc.overriding.tpe*/ + opc.overriding.locationString + " " + opc.overridden/* + ":" + opc.overridden.tpe*/ + opc.overridden.locationString + opc.overridden.hasFlag(DEFERRED));//DEBUG
-	if (!opc.overridden.isClass) checkOverride(clazz, opc.overriding, opc.overridden);
+        //Console.println("overrides " + opc.overriding/* + ":" + opc.overriding.tpe*/ + opc.overriding.locationString + " " + opc.overridden/* + ":" + opc.overridden.tpe*/ + opc.overridden.locationString + opc.overridden.hasFlag(DEFERRED));//DEBUG
+        if (!opc.overridden.isClass) checkOverride(clazz, opc.overriding, opc.overridden);
 
-	opc.next
+        opc.next
       }
       // 2. Check that only abstract classes have deferred members
       if (clazz.isClass && !clazz.isTrait) {
-	def abstractClassError(mustBeMixin: boolean, msg: String): unit = {
-	  unit.error(clazz.pos,
-	    (if (clazz.isAnonymousClass || clazz.isModuleClass) "object creation impossible"
-	     else if (mustBeMixin) clazz.toString() + " needs to be a mixin"
-	     else clazz.toString() + " needs to be abstract") + ", since " + msg);
-	  clazz.setFlag(ABSTRACT)
-	}
-	for (val member <- clazz.tpe.nonPrivateMembers)
-	  if ((member hasFlag DEFERRED) && !(clazz hasFlag ABSTRACT)) {
-	    abstractClassError(
+        def abstractClassError(mustBeMixin: boolean, msg: String): unit = {
+          unit.error(clazz.pos,
+            (if (clazz.isAnonymousClass || clazz.isModuleClass) "object creation impossible"
+             else if (mustBeMixin) clazz.toString() + " needs to be a mixin"
+             else clazz.toString() + " needs to be abstract") + ", since " + msg);
+          clazz.setFlag(ABSTRACT)
+        }
+        for (val member <- clazz.tpe.nonPrivateMembers)
+          if ((member hasFlag DEFERRED) && !(clazz hasFlag ABSTRACT)) {
+            abstractClassError(
               false, infoString(member) + " is not defined" + analyzer.varNotice(member))
-	  } else if ((member hasFlag ABSOVERRIDE) && member.isIncompleteIn(clazz)) {
-	    val other = member.superSymbol(clazz);
-	    abstractClassError(true,
-	      infoString(member) + " is marked `abstract' and `override'" +
-	      (if (other != NoSymbol)
-		" and overrides incomplete superclass member " + infoString(other)
-	       else ""))
-	  }
+          } else if ((member hasFlag ABSOVERRIDE) && member.isIncompleteIn(clazz)) {
+            val other = member.superSymbol(clazz);
+            abstractClassError(true,
+              infoString(member) + " is marked `abstract' and `override'" +
+              (if (other != NoSymbol)
+                " and overrides incomplete superclass member " + infoString(other)
+               else ""))
+          }
       }
 
       // 3. Check that every defined member with an `override' modifier overrides some other member.
       for (val member <- clazz.info.decls.toList)
-	if ((member hasFlag (OVERRIDE | ABSOVERRIDE)) &&
-	    (clazz.info.baseClasses.tail forall {
+        if ((member hasFlag (OVERRIDE | ABSOVERRIDE)) &&
+            (clazz.info.baseClasses.tail forall {
                bc => member.matchingSymbol(bc, clazz.thisType) == NoSymbol
             })) {
           // for (val bc <- clazz.info.baseClasses.tail) Console.println("" + bc + " has " + bc.info.decl(member.name) + ":" + bc.info.decl(member.name).tpe);//DEBUG
-	  unit.error(member.pos, member.toString() + " overrides nothing");
-	  member resetFlag OVERRIDE
-	}
+          unit.error(member.pos, member.toString() + " overrides nothing");
+          member resetFlag OVERRIDE
+        }
     }
 
   // Basetype Checking --------------------------------------------------------
@@ -270,37 +297,37 @@ abstract class RefChecks extends InfoTransform {
       var seenCaseClass = if (clazz hasFlag CASE) clazz else NoSymbol
 
       def validateTypes(tps: List[Type], includeSuper: boolean): unit = {
-	if (!tps.isEmpty) {
-	  for (val tp <- tps.tail.reverse) validateType(tp, false);
-	  if (includeSuper) validateType(tps.head, true);
-	}
+        if (!tps.isEmpty) {
+          for (val tp <- tps.tail.reverse) validateType(tp, false);
+          if (includeSuper) validateType(tps.head, true);
+        }
       }
 
       def validateType(tp: Type, includeSuper: boolean): unit = {
-	val baseClass = tp.symbol
-	if (baseClass.isClass) {
-	  val index = clazz.info.closurePos(baseClass)
-	  if (index >= 0) {
-	    if ((seenTypes(index) ne null) && !(seenTypes(index) <:< tp))
-	      unit.error(clazz.pos, "illegal inheritance;\n " + clazz +
-			 " inherits different type instances of " + baseClass +
-			 ":\n" + tp + " and " + seenTypes(index));
-	    seenTypes(index) = tp;
-	    // check that case classes do not inherit from case classes
-	    if (baseClass hasFlag CASE) {
-	      if (seenCaseClass != NoSymbol && seenCaseClass != baseClass)
-		unit.error(clazz.pos, "implementation restriction: case " +
-			   seenCaseClass + " and case " + baseClass +
+        val baseClass = tp.symbol
+        if (baseClass.isClass) {
+          val index = clazz.info.closurePos(baseClass)
+          if (index >= 0) {
+            if ((seenTypes(index) ne null) && !(seenTypes(index) <:< tp))
+              unit.error(clazz.pos, "illegal inheritance;\n " + clazz +
+                         " inherits different type instances of " + baseClass +
+                         ":\n" + tp + " and " + seenTypes(index));
+            seenTypes(index) = tp;
+            // check that case classes do not inherit from case classes
+            if (baseClass hasFlag CASE) {
+              if (seenCaseClass != NoSymbol && seenCaseClass != baseClass)
+                unit.error(clazz.pos, "implementation restriction: case " +
+                           seenCaseClass + " and case " + baseClass +
                            " cannot be combined in one object");
-	      seenCaseClass = baseClass
-	    }
-	    // check that inner classes do not inherit from Annotation
+              seenCaseClass = baseClass
+            }
+            // check that inner classes do not inherit from Annotation
             if (baseClass == ClassfileAnnotationClass)
               if (!clazz.owner.isPackageClass)
                 unit.error(clazz.pos, "inner classes cannot be classfile annotations")
-	  }
-	  validateTypes(tp.parents, includeSuper)
-	}
+          }
+          validateTypes(tp.parents, includeSuper)
+        }
       }
 
       validateTypes(clazz.info.parents, true)
@@ -322,68 +349,70 @@ abstract class RefChecks extends InfoTransform {
     private def validateVariance(base: Symbol, all: Type, variance: int): unit = {
 
       def varianceString(variance: int): String =
-	if (variance == 1) "covariant"
-	else if (variance == -1) "contravariant"
-	else "invariant";
+        if (variance == 1) "covariant"
+        else if (variance == -1) "contravariant"
+        else "invariant";
 
       def relativeVariance(tvar: Symbol): int = {
-	val clazz = tvar.owner
-	var sym = base
-	var state = CoVariance
-	while (sym != clazz && state != AnyVariance) {
-	  //Console.println("flip: " + sym + " " + sym.isParameter());//DEBUG
-	  if ((sym hasFlag PARAM) && !sym.owner.isConstructor) state = -state;
-	  else if (!sym.owner.isClass || sym.isPrivateLocal) state = AnyVariance;
-	  else if (sym.isAliasType) state = NoVariance;
-	  sym = sym.owner
-	}
-	state
+        val clazz = tvar.owner
+        var sym = base
+        var state = CoVariance
+        while (sym != clazz && state != AnyVariance) {
+          //Console.println("flip: " + sym + " " + sym.isParameter());//DEBUG
+          if ((sym hasFlag PARAM) && !sym.owner.isConstructor) state = -state;
+          else if (!sym.owner.isClass || sym.isPrivateLocal) state = AnyVariance;
+          else if (sym.isAliasType) state = NoVariance;
+          sym = sym.owner
+        }
+        state
       }
 
       def validateVariance(tp: Type, variance: int): unit = tp match {
-	case ErrorType => ;
-	case WildcardType => ;
-	case NoType => ;
-	case NoPrefix => ;
-	case ThisType(_) => ;
-	case ConstantType(_) => ;
-	case SingleType(pre, sym) =>
-	  validateVariance(pre, variance)
-	case TypeRef(pre, sym, args) =>
-	  if (sym.variance != NoVariance) {
-	    val v = relativeVariance(sym);
-	    if (v != AnyVariance && sym.variance != v * variance) {
-	      //Console.println("relativeVariance(" + base + "," + sym + ") = " + v);//DEBUG
-	      unit.error(base.pos,
-			 varianceString(sym.variance) + " " + sym +
-			 " occurs in " + varianceString(v * variance) +
-			 " position in type " + all + " of " + base);
-	    }
-	  }
-	  validateVariance(pre, variance)
-	  validateVarianceArgs(args, variance, sym.typeParams)
-	case ClassInfoType(parents, decls, symbol) =>
-	  validateVariances(parents, variance)
-	case RefinedType(parents, decls) =>
-	  validateVariances(parents, variance)
-	case TypeBounds(lo, hi) =>
-	  validateVariance(lo, -variance)
-	  validateVariance(hi, variance)
-	case MethodType(formals, result) =>
-	  validateVariance(result, variance)
-	case PolyType(tparams, result) =>
-	  validateVariance(result, variance)
+        case ErrorType => ;
+        case WildcardType => ;
+        case NoType => ;
+        case NoPrefix => ;
+        case ThisType(_) => ;
+        case ConstantType(_) => ;
+        case SingleType(pre, sym) =>
+          validateVariance(pre, variance)
+        case TypeRef(pre, sym, args) =>
+          if (sym.variance != NoVariance) {
+            val v = relativeVariance(sym);
+            if (v != AnyVariance && sym.variance != v * variance) {
+              //Console.println("relativeVariance(" + base + "," + sym + ") = " + v);//DEBUG
+              unit.error(base.pos,
+                         varianceString(sym.variance) + " " + sym +
+                         " occurs in " + varianceString(v * variance) +
+                         " position in type " + all + " of " + base);
+            }
+          }
+          validateVariance(pre, variance)
+          validateVarianceArgs(args, variance, sym.typeParams) //@M for higher-kinded typeref, args.isEmpty
+          // However, these args respect variances by construction anyway
+          // -- the interesting case is in type application, see checkKindBounds in Infer
+        case ClassInfoType(parents, decls, symbol) =>
+          validateVariances(parents, variance)
+        case RefinedType(parents, decls) =>
+          validateVariances(parents, variance)
+        case TypeBounds(lo, hi) =>
+          validateVariance(lo, -variance)
+          validateVariance(hi, variance)
+        case MethodType(formals, result) =>
+          validateVariance(result, variance)
+        case PolyType(tparams, result) =>
+          validateVariance(result, variance)
         case AnnotatedType(attribs, tp) =>
           validateVariance(tp, variance)
       }
 
       def validateVariances(tps: List[Type], variance: int): unit =
-	tps foreach (tp => validateVariance(tp, variance))
+        tps foreach (tp => validateVariance(tp, variance))
 
       def validateVarianceArgs(tps: List[Type], variance: int, tparams: List[Symbol]): unit =
-	(tps zip tparams) foreach {
-	  case (tp, tparam) => validateVariance(tp, variance * tparam.variance)
-	}
+        (tps zip tparams) foreach {
+          case (tp, tparam) => validateVariance(tp, variance * tparam.variance)
+        }
 
       validateVariance(all, variance)
     }
@@ -409,35 +438,38 @@ abstract class RefChecks extends InfoTransform {
     private def enterSyms(stats: List[Tree]): unit = {
       var index = -1
       for (val stat <- stats) {
-	index = index + 1;
-	stat match {
+        index = index + 1;
+        stat match {
           case ClassDef(_, _, _, _, _) | DefDef(_, _, _, _, _, _) | ModuleDef(_, _, _) | ValDef(_, _, _, _) =>
             assert(stat.symbol != NoSymbol, stat);//debug
             if (stat.symbol.isLocal) {
-	      currentLevel.scope.enter(newScopeEntry(stat.symbol, currentLevel.scope));
-	      symIndex(stat.symbol) = index;
+              currentLevel.scope.enter(newScopeEntry(stat.symbol, currentLevel.scope));
+              symIndex(stat.symbol) = index;
             }
           case _ =>
-	}
+        }
       }
     }
 
     private def enterReference(pos: int, sym: Symbol): unit =
       if (sym.isLocal) {
-	val e = currentLevel.scope.lookupEntry(sym.name)
-	if ((e ne null) && sym == e.sym) {
+        val e = currentLevel.scope.lookupEntry(sym.name)
+        if ((e ne null) && sym == e.sym) {
           var l = currentLevel
           while (l.scope != e.owner) l = l.outer;
-	  val symindex = symIndex(sym)
-	  if (l.maxindex < symindex) {
-	    l.refpos = pos
-	    l.refsym = sym
-	    l.maxindex = symindex
-	  }
-	}
+          val symindex = symIndex(sym)
+          if (l.maxindex < symindex) {
+            l.refpos = pos
+            l.refsym = sym
+            l.maxindex = symindex
+          }
+        }
       }
 
 // Comparison checking -------------------------------------------------------
+    object normalizeAll extends TypeMap {
+      def apply(tp: Type) = mapOver(tp).normalize
+    }
 
     def checkSensible(pos: int, fn: Tree, args: List[Tree]) = fn match {
       case Select(qual, name) if (args.length == 1) =>
@@ -461,8 +493,8 @@ abstract class RefChecks extends InfoTransform {
               unit.warning(pos, "comparing "+what+" using `"+name.decode+"' will always yield "+
                            (alwaysEqual == (name == nme.EQ || name == nme.LE || name == nme.GE)))
             def nonSensible(pre: String, alwaysEqual: boolean) =
-              nonSensibleWarning(pre+"values of types "+qual.tpe.widen+" and "+args.head.tpe.widen,
-                                 alwaysEqual)
+              nonSensibleWarning(pre+"values of types "+normalizeAll(qual.tpe.widen)+" and "+normalizeAll(args.head.tpe.widen),
+                                 alwaysEqual) // @MAT normalize for consistency in error message, otherwise part is normalized due to use of `symbol', but the rest isn't
             def hasObjectEquals = receiver.info.member(nme.equals_) == Object_equals
             if (formal == UnitClass && actual == UnitClass)
               nonSensible("", true)
@@ -511,13 +543,13 @@ abstract class RefChecks extends InfoTransform {
 
     def transformStat(tree: Tree, index: int): List[Tree] = tree match {
       case ModuleDef(mods, name, impl) =>
-	val sym = tree.symbol
-	val cdef = ClassDef(mods | MODULE, name, List(), emptyValDef, impl)
-	  .setPos(tree.pos)
+        val sym = tree.symbol
+        val cdef = ClassDef(mods | MODULE, name, List(), emptyValDef, impl)
+          .setPos(tree.pos)
           .setSymbol(sym.moduleClass)
           .setType(NoType);
-	if (sym.isStatic) List(transform(cdef))
-	else {
+        if (sym.isStatic) List(transform(cdef))
+        else {
           val vdef =
             localTyper.typed {
               atPos(tree.pos) {
@@ -526,8 +558,8 @@ abstract class RefChecks extends InfoTransform {
             }
 
           val ddef =
-	    atPhase(phase.next) {
-	      localTyper.typed {
+            atPhase(phase.next) {
+              localTyper.typed {
                 if (sym.owner.isTrait) gen.mkModuleAccessDcl(sym)
                 else gen.mkModuleAccessDef(sym, vdef.symbol)
               }
@@ -535,7 +567,7 @@ abstract class RefChecks extends InfoTransform {
 
           if (sym.owner.isTrait) transformTrees(List(cdef, ddef))
           else transformTrees(List(cdef, vdef, ddef))
-	}
+        }
 
       case ClassDef(_, _, _, _, _) if isConcreteLocalCaseFactory(tree.symbol) =>
         val clazz = tree.symbol
@@ -564,27 +596,27 @@ abstract class RefChecks extends InfoTransform {
         }
 
       case ValDef(_, _, _, _) =>
-	val tree1 = transform(tree); // important to do before forward reference check
-	if (tree.symbol.isLocal && index <= currentLevel.maxindex) {
-	  if (settings.debug.value) Console.println(currentLevel.refsym);
-	  unit.error(currentLevel.refpos, "forward reference extends over definition of " + tree.symbol);
-	}
-	List(tree1)
+        val tree1 = transform(tree); // important to do before forward reference check
+        if (tree.symbol.isLocal && index <= currentLevel.maxindex) {
+          if (settings.debug.value) Console.println(currentLevel.refsym);
+          unit.error(currentLevel.refpos, "forward reference extends over definition of " + tree.symbol);
+        }
+        List(tree1)
 
       case Import(_, _) =>
-	List()
+        List()
 
       case _ =>
-	List(transform(tree))
+        List(transform(tree))
     }
 
     override def transform(tree: Tree): Tree = try {
 
       /* Check whether argument types conform to bounds of type parameters */
       def checkBounds(pre: Type, owner: Symbol, tparams: List[Symbol], argtps: List[Type]): unit = try {
-	typer.infer.checkBounds(tree.pos, pre, owner, tparams, argtps, "");
+        typer.infer.checkBounds(tree.pos, pre, owner, tparams, argtps, "");
       } catch {
-	case ex: TypeError => unit.error(tree.pos, ex.getMessage());
+        case ex: TypeError => unit.error(tree.pos, ex.getMessage());
       }
 
       def isIrrefutable(pat: Tree, seltpe: Type): boolean = {
@@ -631,40 +663,41 @@ abstract class RefChecks extends InfoTransform {
       val sym = tree.symbol
       var result = tree
       tree match {
-	case ClassDef(mods, name, tparams, _, impl) =>
-	  validateVariance(sym, sym.info, CoVariance)
-	  validateVariance(sym, sym.typeOfThis, CoVariance)
+        case ClassDef(mods, name, tparams, _, impl) =>
+          validateVariance(sym, sym.info, CoVariance)
+          validateVariance(sym, sym.typeOfThis, CoVariance)
 
-	case DefDef(_, _, _, _, _, _) =>
-          validateVariance(sym, sym.tpe, CoVariance)
+        case DefDef(_, _, _, _, _, _) =>
+          validateVariance(sym, sym.tpe, CoVariance) //@M TODO: might be affected by change in tpe --> can't use tree.tpe though
           checkDeprecatedOvers()
 
-	case ValDef(_, _, _, _) =>
-          validateVariance(sym, sym.tpe, if (sym.isVariable) NoVariance else CoVariance)
+        case ValDef(_, _, _, _) =>
+          validateVariance(sym, sym.tpe, if (sym.isVariable) NoVariance else CoVariance) //@M TODO: might be affected by change in tpe --> can't use tree.tpe though
           checkDeprecatedOvers()
 
-	case AbsTypeDef(_, _, _, _) =>
-	  validateVariance(sym, sym.info, CoVariance)
+        case AbsTypeDef(_, _, _, _, _) =>
+          validateVariance(sym, sym.info, CoVariance)
 
-	case AliasTypeDef(_, _, _, _) =>
-	  validateVariance(sym, sym.info, CoVariance)
+        case AliasTypeDef(_, _, _, _) =>
+          validateVariance(sym, sym.info, CoVariance)
 
-	case Template(_, _) =>
-	  localTyper = localTyper.atOwner(tree, currentOwner)
-	  validateBaseTypes(currentOwner)
-	  checkAllOverrides(currentOwner)
+        case Template(_, _) =>
+          localTyper = localTyper.atOwner(tree, currentOwner)
+          validateBaseTypes(currentOwner)
+          checkAllOverrides(currentOwner)
 
-	case TypeTree() =>
-	  new TypeTraverser {
-	    def traverse(tp: Type): TypeTraverser = tp match {
-	      case TypeRef(pre, sym, args) => checkBounds(pre, sym.owner, sym.typeParams, args); this
-	      case _ => this
-	    }
-	  } traverse tree.tpe
+        case TypeTree() =>
+          new TypeTraverser {
+            def traverse(tp: Type): TypeTraverser = tp match {
+              case tr@TypeRef(pre, sym, _) if tr.isHigherKinded => this //@M a higher-kinded typeref doesn't have any args to check
+              case TypeRef(pre, sym, args) => checkBounds(pre, sym.owner, sym.typeParams, args); this
+              case _ => this
+            }
+          } traverse tree.tpe
 
-	case TypeApply(fn, args) =>
-	  checkBounds(NoPrefix, NoSymbol, fn.tpe.typeParams, args map (.tpe))
-	  if (sym.isSourceMethod && sym.hasFlag(CASE)) result = toConstructor(tree.pos, tree.tpe)
+        case TypeApply(fn, args) =>
+          checkBounds(NoPrefix, NoSymbol, fn.tpe.typeParams, args map (.tpe))
+          if (sym.isSourceMethod && sym.hasFlag(CASE)) result = toConstructor(tree.pos, tree.tpe)
 
         case Apply(
           Select(qual, nme.filter),
@@ -686,37 +719,37 @@ abstract class RefChecks extends InfoTransform {
             case _ =>
           }
 
-	case New(tpt) =>
-	  enterReference(tree.pos, tpt.tpe.symbol)
-
-	case Ident(name) =>
-	  if (sym.isSourceMethod && sym.hasFlag(CASE))
-	    result = toConstructor(tree.pos, tree.tpe)
-	  else if (name != nme.WILDCARD && name != nme.WILDCARD_STAR.toTypeName) {
-	    assert(sym != NoSymbol, tree)//debug
-	    enterReference(tree.pos, sym)
-	  }
-
-	case Select(qual, name) =>
-	  if (sym.isSourceMethod && sym.hasFlag(CASE))
-	    result = toConstructor(tree.pos, tree.tpe)
-	  else qual match {
-	    case Super(qualifier, mix) =>
+        case New(tpt) =>
+          enterReference(tree.pos, tpt.tpe.symbol)
+
+        case Ident(name) =>
+          if (sym.isSourceMethod && sym.hasFlag(CASE))
+            result = toConstructor(tree.pos, tree.tpe)
+          else if (name != nme.WILDCARD && name != nme.WILDCARD_STAR.toTypeName) {
+            assert(sym != NoSymbol, tree)//debug
+            enterReference(tree.pos, sym)
+          }
+
+        case Select(qual, name) =>
+          if (sym.isSourceMethod && sym.hasFlag(CASE))
+            result = toConstructor(tree.pos, tree.tpe)
+          else qual match {
+            case Super(qualifier, mix) =>
               val base = qual.symbol;
               //Console.println("super: " + tree + " in " + base);//DEBUG
               assert(!(base.isTrait && sym.isTerm && mix == nme.EMPTY.toTypeName)) // term should have been eliminated by super accessors
             case _ =>
           }
-	case _ =>
+        case _ =>
       }
       result = super.transform(result)
       localTyper = savedLocalTyper
       result
     } catch {
       case ex: TypeError =>
-	if (settings.debug.value) ex.printStackTrace();
-	unit.error(tree.pos, ex.getMessage())
-	tree
+        if (settings.debug.value) ex.printStackTrace();
+        unit.error(tree.pos, ex.getMessage())
+        tree
     }
   }
 }
diff --git a/src/compiler/scala/tools/nsc/typechecker/Typers.scala b/src/compiler/scala/tools/nsc/typechecker/Typers.scala
index b54d378eb7..329eb344c6 100644
--- a/src/compiler/scala/tools/nsc/typechecker/Typers.scala
+++ b/src/compiler/scala/tools/nsc/typechecker/Typers.scala
@@ -239,8 +239,9 @@ trait Typers requires Analyzer {
       tp match {
         case TypeRef(pre, sym, args) =>
           (checkNotLocked(sym)) && (
-            !sym.isAliasType && !sym.isAbstractType ||
-            checkNonCyclic(pos, pre.memberInfo(sym).subst(sym.typeParams, args), sym)
+            !sym.isTypeMember ||
+            checkNonCyclic(pos, appliedType(pre.memberInfo(sym), args), sym)   // @M! info for a type ref to a type parameter now returns a polytype
+            // @M was: checkNonCyclic(pos, pre.memberInfo(sym).subst(sym.typeParams, args), sym)
           )
         case SingleType(pre, sym) =>
           checkNotLocked(sym)
@@ -524,7 +525,8 @@ trait Typers requires Analyzer {
      *        unapply or unapplySeq method.
      *
      *  (6) Convert all other types to TypeTree nodes.
-     *  (7) When in TYPEmode nut not FUNmode, check that types are fully parameterized
+     *  (7) When in TYPEmode but not FUNmode, check that types are fully parameterized
+     *      (7.1) @M! when in POLYmode | TAPPmode, check that types have the expected kind
      *  (8) When in both EXPRmode and FUNmode, add apply method calls to values of object type.
      *  (9) If there are undetermined type variables and not POLYmode, infer expression instance
      *  Then, if tree's type is not a subtype of expected type, try the following adaptations:
@@ -584,8 +586,16 @@ trait Typers requires Analyzer {
         if (tree.isType) {
           if ((mode & FUNmode) != 0) {
             tree
-          } else if (tree.hasSymbol && !tree.symbol.typeParams.isEmpty) { // (7)
+          } else if (tree.hasSymbol && !tree.symbol.typeParams.isEmpty && (mode & (POLYmode | TAPPmode)) == 0) { // (7)
+            // @M higher-kinded types are allowed in (POLYmode | TAPPmode) -- see (7.1)
             errorTree(tree, tree.symbol+" takes type parameters")
+            tree setType tree.tpe
+          } else if (tree.hasSymbol && ((mode & (POLYmode | TAPPmode)) == (POLYmode | TAPPmode)) &&             // (7.1) @M: check kind-arity (full checks are done in checkKindBounds in Infer)
+                     tree.symbol.typeParams.length != pt.typeParams.length &&
+                     !(tree.symbol==AnyClass || tree.symbol==AllClass || pt == WildcardType )) { //@M Any and Nothing are kind-polymorphic -- WildcardType is only used when typing type arguments to an overloaded method, before the overload is resolved
+              errorTree(tree, tree.symbol+" takes "+reporter.countElementsAsString(tree.symbol.typeParams.length, "type parameter")+
+                              ", expected: "+reporter.countAsString(pt.typeParams.length))
+              tree setType tree.tpe
           } else tree match { // (6)
             case TypeTree() => tree
             case _ => TypeTree(tree.tpe) setOriginal(tree)
@@ -648,7 +658,7 @@ trait Typers requires Analyzer {
           if (tree1.tpe <:< pt) adapt(tree1, mode, pt)
           else {
             if ((mode & (EXPRmode | FUNmode)) == EXPRmode) {
-              pt match {
+              pt.normalize match {
                 case TypeRef(_, sym, _) =>
                   // note: was if (pt.symbol == UnitClass) but this leads to a potentially
                   // infinite expansion if pt is constant type ()
@@ -824,7 +834,7 @@ trait Typers requires Analyzer {
             else
               psym addChild context.owner
           }
-          if (!(selfType <:< parent.tpe.typeOfThis) && !phase.erasedTypes) {
+          if (!(selfType <:< parent.tpe.typeOfThis) && !phase.erasedTypes) { //@M .typeOfThis seems necessary
             //Console.println(context.owner);//DEBUG
             //Console.println(context.owner.unsafeTypeParams);//DEBUG
             //Console.println(List.fromArray(context.owner.info.closure));//DEBUG
@@ -848,7 +858,7 @@ trait Typers requires Analyzer {
         if (classinfo.expansiveRefs(tparam) contains tparam) {
           error(tparam.pos, "class graph is not finitary because type parameter "+tparam.name+" is expansively recursive")
           val newinfo = ClassInfoType(
-            classinfo.parents map (.subst(List(tparam), List(AnyRefClass.tpe))),
+            classinfo.parents map (.instantiateTypeParams(List(tparam), List(AnyRefClass.tpe))),
             classinfo.decls,
             clazz)
           clazz.setInfo {
@@ -1137,13 +1147,15 @@ trait Typers requires Analyzer {
     }
 
     def typedAbsTypeDef(tdef: AbsTypeDef): AbsTypeDef = {
+      reenterTypeParams(tdef.tparams) // @M!
+      val tparams1 = List.mapConserve(tdef.tparams)(typedAbsTypeDef) // @M!
       val lo1 = checkNoEscaping.privates(tdef.symbol, typedType(tdef.lo))
       val hi1 = checkNoEscaping.privates(tdef.symbol, typedType(tdef.hi))
       checkNonCyclic(tdef.symbol)
       if (!(lo1.tpe <:< hi1.tpe))
         error(tdef.pos,
               "lower bound "+lo1.tpe+" does not conform to upper bound "+hi1.tpe)
-      copy.AbsTypeDef(tdef, tdef.mods, tdef.name, lo1, hi1) setType NoType
+      copy.AbsTypeDef(tdef, tdef.mods, tdef.name, tparams1, lo1, hi1) setType NoType
     }
 
     def typedAliasTypeDef(tdef: AliasTypeDef): AliasTypeDef = {
@@ -1231,7 +1243,7 @@ trait Typers requires Analyzer {
           body1 =
             typed {
               atPos(body1.pos) {
-                TypeApply(Select(body1, Any_asInstanceOf), List(TypeTree(pt)))
+                TypeApply(Select(body1, Any_asInstanceOf), List(TypeTree(pt))) // @M no need for pt.normalize here, is done in erasure
               }
             }
       }
@@ -1503,12 +1515,12 @@ trait Typers requires Analyzer {
               val strictTargs = List.map2(lenientTargs, tparams)((targ, tparam) =>
                 if (targ == WildcardType) tparam.tpe else targ)
               def typedArgToPoly(arg: Tree, formal: Type): Tree = {
-                val lenientPt = formal.subst(tparams, lenientTargs)
+                val lenientPt = formal.instantiateTypeParams(tparams, lenientTargs)
                 val arg1 = typedArg(arg, mode, POLYmode, lenientPt)
                 val argtparams = context.undetparams
                 context.undetparams = List()
                 if (!argtparams.isEmpty) {
-                  val strictPt = formal.subst(tparams, strictTargs)
+                  val strictPt = formal.instantiateTypeParams(tparams, strictTargs)
                   inferArgumentInstance(arg1, argtparams, strictPt, lenientPt)
                 }
                 arg1
@@ -1651,10 +1663,24 @@ trait Typers requires Analyzer {
       //Console.println("typed1("+tree.getClass()+","+Integer.toHexString(mode)+","+pt+")")
       def ptOrLub(tps: List[Type]) = if (isFullyDefined(pt)) pt else lub(tps)
 
+      //@M! get the type of the qualifier in a Select tree, otherwise: NoType
+      def prefixType(fun: Tree): Type = fun match {
+        case Select(qualifier, _) => qualifier.tpe
+//        case Ident(name) => ??
+        case _ => NoType
+      }
+
       def typedTypeApply(fun: Tree, args: List[Tree]): Tree = fun.tpe match {
         case OverloadedType(pre, alts) =>
           inferPolyAlternatives(fun, args map (.tpe))
-          typedTypeApply(fun, args)
+          val tparams = fun.symbol.typeParams
+          assert(args.length == tparams.length)  //@M: in case TypeApply we can't check the kind-arities
+          // of the type arguments as we don't know which alternative to choose... here we do
+          val args1 = map2Conserve(args, tparams) {
+            //@M! the polytype denotes the expected kind
+            (arg, tparam) => typedHigherKindedType(arg, makePolyType(tparam.typeParams, AnyClass.tpe))
+          }
+          typedTypeApply(fun, args1)
         case PolyType(tparams, restpe) if (tparams.length != 0) =>
           if (tparams.length == args.length) {
             val targs = args map (.tpe)
@@ -1663,8 +1689,14 @@ trait Typers requires Analyzer {
               if (!targs.head.symbol.isClass || targs.head.symbol.isRefinementClass)
                 error(args.head.pos, "class type required");
               Literal(Constant(targs.head)) setPos tree.pos setType ClassClass.tpe
-            } else
-              copy.TypeApply(tree, fun, args) setType restpe.subst(tparams, targs)
+            } else {
+              val resultpe0 = restpe.instantiateTypeParams(tparams, targs)
+              //@M TODO -- probably ok
+              //@M example why asSeenFrom is necessary: class Foo[a] { def foo[m[x]]: m[a] } (new Foo[Int]).foo[List] : List[Int]
+              //@M however, asSeenFrom widens a singleton type, thus cannot use it for those types
+              val resultpe = if(resultpe0.isInstanceOf[SingletonType]) resultpe0 else resultpe0.asSeenFrom(prefixType(fun), fun.symbol.owner)
+              copy.TypeApply(tree, fun, args) setType resultpe
+            }
           } else {
             errorTree(tree, "wrong number of type parameters for "+treeSymTypeMsg(fun))
           }
@@ -1867,7 +1899,7 @@ trait Typers requires Analyzer {
         var qual: Tree = EmptyTree       // the qualififier tree if transformed tree is a select
         // if we are in a constructor of a pattern, ignore all methods
         // which are not case factories (note if we don't do that
-        // case x :: xs in class List would return the :: method.
+        // case x :: xs in class List would return the :: method).
         def qualifies(sym: Symbol): boolean =
           sym.exists &&
           ((mode & PATTERNmode | FUNmode) != (PATTERNmode | FUNmode) ||
@@ -1982,6 +2014,9 @@ trait Typers requires Analyzer {
         }
       }
 
+      // @M: copied from Namers
+      def makePolyType(tparams: List[Symbol], tpe: Type) = if (tparams.isEmpty) tpe else PolyType(tparams, tpe)
+
       // begin typed1
       val sym: Symbol = tree.symbol
       if (sym ne null) sym.initialize
@@ -2004,7 +2039,7 @@ trait Typers requires Analyzer {
         case ddef @ DefDef(_, _, _, _, _, _) =>
           newTyper(makeNewScope(context, tree, sym)).typedDefDef(ddef)
 
-        case tdef @ AbsTypeDef(_, _, _, _) =>
+        case tdef @ AbsTypeDef(_, _, _, _, _) =>
           newTyper(makeNewScope(context, tree, sym)).typedAbsTypeDef(tdef)
 
         case tdef @ AliasTypeDef(_, _, _, _) =>
@@ -2263,9 +2298,39 @@ trait Typers requires Analyzer {
           copy.Typed(tree, expr1, tpt1) setType owntype
 
         case TypeApply(fun, args) =>
-          val args1 = List.mapConserve(args)(typedType)
-          // do args first in order to maintain conext.undetparams on the function side.
-          typedTypeApply(typed(fun, funMode(mode) | TAPPmode, WildcardType), args1)
+          // @M: kind-arity checking is done here and in adapt, full kind-checking is in checkKindBounds (in Infer)
+          //@M! we must type fun in order to type the args, as that requires the kinds of fun's type parameters.
+          // However, args should apparently be done first, to save context.undetparams. Unfortunately, the args
+          // *really* have to be typed *after* fun. We escape from this classic Catch-22 by simply saving&restoring undetparams.
+
+          // @M TODO: the compiler still bootstraps&all tests pass when this is commented out..
+          //val undets = context.undetparams
+
+          // @M: fun is typed in TAPPmode because it is being applied to its actual type parameters
+          val fun1 = typed(fun, funMode(mode) | TAPPmode, WildcardType)
+          val tparams = fun1.symbol.typeParams
+
+          //@M TODO: val undets_fun = context.undetparams  ?
+          // "do args first" (by restoring the context.undetparams) in order to maintain context.undetparams on the function side.
+
+          // @M TODO: the compiler still bootstraps when this is commented out.. TODO: run tests
+          //context.undetparams = undets
+
+          // @M maybe the well-kindedness check should be done when checking the type arguments conform to the type parameters' bounds?
+          val args1 = if(args.length == tparams.length) map2Conserve(args, tparams) {
+                        //@M! the polytype denotes the expected kind
+                        (arg, tparam) => typedHigherKindedType(arg, makePolyType(tparam.typeParams, AnyClass.tpe))
+                      } else {
+                        assert(fun1.symbol.info.isInstanceOf[OverloadedType])
+                      // @M this branch is hit for an overloaded polymorphic type.
+                      // Until the right alternative is known, be very liberal,
+                      // typedTypeApply will find the right alternative and then do the same check as
+                      // in the then-branch above. (see pos/tcpoly_overloaded.scala)
+                        List.mapConserve(args)(typedHigherKindedType)
+                      }
+
+          //@M TODO: context.undetparams = undets_fun ?
+          typedTypeApply(fun1, args1)
 
         case Apply(Block(stats, expr), args) =>
           typed1(atPos(tree.pos)(Block(stats, Apply(expr, args))), mode, pt)
@@ -2408,13 +2473,18 @@ trait Typers requires Analyzer {
         case AppliedTypeTree(tpt, args) =>
           val tpt1 = typed1(tpt, mode | FUNmode | TAPPmode, WildcardType)
           val tparams = tpt1.symbol.typeParams
-          val args1 = List.mapConserve(args)(typedType)
+
           if (tpt1.tpe.isError) {
             setError(tree)
-          } else if (tparams.length == args1.length) {
+          } else if (tparams.length == args.length) {
+            // @M: kind-arity checking is done here and in adapt, full kind-checking is in checkKindBounds (in Infer)
+            val args1 = map2Conserve(args, tparams) {
+              (arg, tparam) => typedHigherKindedType(arg, makePolyType(tparam.typeParams, AnyClass.tpe)) //@M! the polytype denotes the expected kind
+            }
             val argtypes = args1 map (.tpe)
-            val owntype = if (tpt1.symbol.isClass) appliedType(tpt1.tpe, argtypes)
-                          else tpt1.tpe.subst(tparams, argtypes)
+            val owntype = if (tpt1.symbol.isClass || tpt1.symbol.isTypeMember) // @M! added the latter condition
+                               appliedType(tpt1.tpe, argtypes)
+                          else tpt1.tpe.instantiateTypeParams(tparams, argtypes)
             List.map2(args, tparams) { (arg, tparam) => arg match {
               // note: can't use args1 in selector, because Bind's got replaced
               case Bind(_, _) =>
@@ -2476,8 +2546,8 @@ trait Typers requires Analyzer {
           reportTypeError(tree.pos, ex)
           setError(tree)
         case ex: Throwable =>
-          if (settings.debug.value)
-            Console.println("exception when typing "+tree+", pt = "+pt)
+//          if (settings.debug.value) // @M causes cyclic reference error
+//            Console.println("exception when typing "+tree+", pt = "+pt)
           if ((context ne null) && (context.unit ne null) &&
               (context.unit.source ne null) && (tree ne null))
             logError("AT: " + context.unit.source.dbg(tree.pos), ex);
@@ -2530,12 +2600,20 @@ trait Typers requires Analyzer {
     def typedType(tree: Tree): Tree =
       withNoGlobalVariance{ typed(tree, TYPEmode, WildcardType) }
 
+    /** Types a higher-kinded type tree -- pt denotes the expected kind*/
+    def typedHigherKindedType(tree: Tree, pt: Type): Tree =
+      if(pt.typeParams.isEmpty) typedType(tree) // kind is known and it's *
+      else withNoGlobalVariance{ typed(tree, POLYmode | TAPPmode, pt) }
+
+    def typedHigherKindedType(tree: Tree): Tree =
+      withNoGlobalVariance{ typed(tree, POLYmode | TAPPmode, WildcardType) }
+
     /** Types a type constructor tree used in a new or supertype */
     def typedTypeConstructor(tree: Tree): Tree = {
       val result = withNoGlobalVariance{ typed(tree, TYPEmode | FUNmode, WildcardType) }
       if (!phase.erasedTypes && result.tpe.isInstanceOf[TypeRef] && !result.tpe.prefix.isStable)
         error(tree.pos, result.tpe.prefix+" is not a legal prefix for a constructor")
-      result
+      result setType(result.tpe.normalize) // @MAT remove aliases when instantiating
     }
 
     def computeType(tree: Tree, pt: Type): Type = {
@@ -2558,7 +2636,7 @@ trait Typers requires Analyzer {
     /* -- Views --------------------------------------------------------------- */
 
     private def tparamsToWildcards(tp: Type, tparams: List[Symbol]) =
-      tp.subst(tparams, tparams map (t => WildcardType))
+      tp.instantiateTypeParams(tparams, tparams map (t => WildcardType))
 
     private def depoly(tp: Type): Type = tp match {
       case PolyType(tparams, restpe) => tparamsToWildcards(restpe, tparams)
diff --git a/src/library/scala/AllRef$.scala b/src/library/scala/AllRef$.scala
index de1fa94bff..dcfd9ad300 100644
--- a/src/library/scala/AllRef$.scala
+++ b/src/library/scala/AllRef$.scala
@@ -6,7 +6,7 @@
 **                          |/                                          **
 \*                                                                      */
 
-// $Id: AllRef$.scala 9262 2006-11-14 17:29:59 +0000 (Tue, 14 Nov 2006) mihaylov $
+// $Id: AllRef$.scala 10086 2007-02-21 19:10:41Z odersky $
 
 
 package scala
diff --git a/src/library/scala/runtime/Nothing$.scala b/src/library/scala/runtime/Nothing$.scala
index d6b9708bc0..0151f95c41 100644
--- a/src/library/scala/runtime/Nothing$.scala
+++ b/src/library/scala/runtime/Nothing$.scala
@@ -6,7 +6,7 @@
 **                          |/                                          **
 \*                                                                      */
 
-// $Id: Nothing$.scala 9261 2006-11-14 17:11:16 +0000 (Tue, 14 Nov 2006) mihaylov $
+// $Id: Nothing$.scala 10086 2007-02-21 19:10:41Z odersky $
 
 
 package scala.runtime
diff --git a/src/library/scala/runtime/Null$.scala b/src/library/scala/runtime/Null$.scala
index 5aa8518b9b..3dd19efeb0 100644
--- a/src/library/scala/runtime/Null$.scala
+++ b/src/library/scala/runtime/Null$.scala
@@ -6,7 +6,7 @@
 **                          |/                                          **
 \*                                                                      */
 
-// $Id: Null$.scala 9261 2006-11-14 17:11:16 +0000 (Tue, 14 Nov 2006) mihaylov $
+// $Id: Null$.scala 10086 2007-02-21 19:10:41Z odersky $
 
 
 package scala.runtime