Merge pull request #1873 from paulp/pr/variance-bonanza

a painstaking examination of Variance

37 files changed, 1249 insertions, 479 deletions

diff --git a/src/compiler/scala/tools/nsc/package.scala b/src/compiler/scala/tools/nsc/package.scala
index 00a9f3b39c..940df1bd1a 100644
--- a/src/compiler/scala/tools/nsc/package.scala
+++ b/src/compiler/scala/tools/nsc/package.scala
@@ -9,6 +9,9 @@ package object nsc {
   type Phase = scala.reflect.internal.Phase
   val NoPhase = scala.reflect.internal.NoPhase
 
+  type Variance = scala.reflect.internal.Variance
+  val Variance = scala.reflect.internal.Variance
+
   type FatalError = scala.reflect.internal.FatalError
   val FatalError = scala.reflect.internal.FatalError
 
diff --git a/src/compiler/scala/tools/nsc/typechecker/Analyzer.scala b/src/compiler/scala/tools/nsc/typechecker/Analyzer.scala
index 5e8bb3e424..d4d6def3cb 100644
--- a/src/compiler/scala/tools/nsc/typechecker/Analyzer.scala
+++ b/src/compiler/scala/tools/nsc/typechecker/Analyzer.scala
@@ -16,7 +16,6 @@ trait Analyzer extends AnyRef
             with Typers
             with Infer
             with Implicits
-            with Variances
             with EtaExpansion
             with SyntheticMethods
             with Unapplies
diff --git a/src/compiler/scala/tools/nsc/typechecker/Checkable.scala b/src/compiler/scala/tools/nsc/typechecker/Checkable.scala
index 9efa3f36b0..fb3909746f 100644
--- a/src/compiler/scala/tools/nsc/typechecker/Checkable.scala
+++ b/src/compiler/scala/tools/nsc/typechecker/Checkable.scala
@@ -200,11 +200,12 @@ trait Checkable {
     def isNeverSubClass(sym1: Symbol, sym2: Symbol) = areIrreconcilableAsParents(sym1, sym2)
 
     private def isNeverSubArgs(tps1: List[Type], tps2: List[Type], tparams: List[Symbol]): Boolean = /*logResult(s"isNeverSubArgs($tps1, $tps2, $tparams)")*/ {
-      def isNeverSubArg(t1: Type, t2: Type, variance: Int) = {
-        if (variance > 0) isNeverSubType(t2, t1)
-        else if (variance < 0) isNeverSubType(t1, t2)
-        else isNeverSameType(t1, t2)
-      }
+      def isNeverSubArg(t1: Type, t2: Type, variance: Variance) = (
+        if (variance.isInvariant) isNeverSameType(t1, t2)
+        else if (variance.isCovariant) isNeverSubType(t2, t1)
+        else if (variance.isContravariant) isNeverSubType(t1, t2)
+        else false
+      )
       exists3(tps1, tps2, tparams map (_.variance))(isNeverSubArg)
     }
     private def isNeverSameType(tp1: Type, tp2: Type): Boolean = (tp1, tp2) match {
diff --git a/src/compiler/scala/tools/nsc/typechecker/Contexts.scala b/src/compiler/scala/tools/nsc/typechecker/Contexts.scala
index e24f0bca1d..274a567075 100644
--- a/src/compiler/scala/tools/nsc/typechecker/Contexts.scala
+++ b/src/compiler/scala/tools/nsc/typechecker/Contexts.scala
@@ -138,7 +138,7 @@ trait Contexts { self: Analyzer =>
     }
 
     var enclMethod: Context = _             // The next outer context whose tree is a method
-    var variance: Int = _                   // Variance relative to enclosing class
+    var variance: Variance = Variance.Invariant     // Variance relative to enclosing class
     private var _undetparams: List[Symbol] = List() // Undetermined type parameters,
                                                     // not inherited to child contexts
     var depth: Int = 0
diff --git a/src/compiler/scala/tools/nsc/typechecker/Infer.scala b/src/compiler/scala/tools/nsc/typechecker/Infer.scala
index 7188290688..88f0ccca98 100644
--- a/src/compiler/scala/tools/nsc/typechecker/Infer.scala
+++ b/src/compiler/scala/tools/nsc/typechecker/Infer.scala
@@ -198,7 +198,7 @@ trait Infer extends Checkable {
    *  @throws NoInstance
    */
   def solvedTypes(tvars: List[TypeVar], tparams: List[Symbol],
-                  variances: List[Int], upper: Boolean, depth: Int): List[Type] = {
+                  variances: List[Variance], upper: Boolean, depth: Int): List[Type] = {
 
     if (tvars.nonEmpty)
       printInference("[solve types] solving for " + tparams.map(_.name).mkString(", ") + " in " + tvars.mkString(", "))
@@ -488,7 +488,7 @@ trait Infer extends Checkable {
                       pt: Type): List[Type] = {
       /** Map type variable to its instance, or, if `variance` is covariant/contravariant,
        *  to its upper/lower bound */
-      def instantiateToBound(tvar: TypeVar, variance: Int): Type = try {
+      def instantiateToBound(tvar: TypeVar, variance: Variance): Type = {
         lazy val hiBounds = tvar.constr.hiBounds
         lazy val loBounds = tvar.constr.loBounds
         lazy val upper = glb(hiBounds)
@@ -501,23 +501,21 @@ trait Infer extends Checkable {
         //Console.println("instantiate "+tvar+tvar.constr+" variance = "+variance);//DEBUG
         if (tvar.constr.inst != NoType)
           instantiate(tvar.constr.inst)
-        else if ((variance & COVARIANT) != 0 && hiBounds.nonEmpty)
-          setInst(upper)
-        else if ((variance & CONTRAVARIANT) != 0 && loBounds.nonEmpty)
+        else if (loBounds.nonEmpty && variance.isContravariant)
           setInst(lower)
-        else if (hiBounds.nonEmpty && loBounds.nonEmpty && upper <:< lower)
+        else if (hiBounds.nonEmpty && (variance.isPositive || loBounds.nonEmpty && upper <:< lower))
           setInst(upper)
         else
           WildcardType
-      } catch {
-        case ex: NoInstance => WildcardType
       }
       val tvars = tparams map freshVar
       if (isConservativelyCompatible(restpe.instantiateTypeParams(tparams, tvars), pt))
         map2(tparams, tvars)((tparam, tvar) =>
-          instantiateToBound(tvar, varianceInTypes(formals)(tparam)))
+          try instantiateToBound(tvar, varianceInTypes(formals)(tparam))
+          catch { case ex: NoInstance => WildcardType }
+        )
       else
-        tvars map (tvar => WildcardType)
+        tvars map (_ => WildcardType)
     }
 
     /** [Martin] Can someone comment this please? I have no idea what it's for
@@ -571,8 +569,8 @@ trait Infer extends Checkable {
 
       foreach3(tparams, tvars, targs) { (tparam, tvar, targ) =>
         val retract = (
-              targ.typeSymbol == NothingClass                                         // only retract Nothings
-          && (restpe.isWildcard || (varianceInType(restpe)(tparam) & COVARIANT) == 0) // don't retract covariant occurrences
+              targ.typeSymbol == NothingClass                                   // only retract Nothings
+          && (restpe.isWildcard || !varianceInType(restpe)(tparam).isPositive)  // don't retract covariant occurrences
         )
 
         buf += ((tparam,
@@ -1316,7 +1314,7 @@ trait Infer extends Checkable {
       val tvars1 = tvars map (_.cloneInternal)
       // Note: right now it's not clear that solving is complete, or how it can be made complete!
       // So we should come back to this and investigate.
-      solve(tvars1, tvars1 map (_.origin.typeSymbol), tvars1 map (x => COVARIANT), false)
+      solve(tvars1, tvars1 map (_.origin.typeSymbol), tvars1 map (_ => Variance.Covariant), false)
     }
 
     // this is quite nasty: it destructively changes the info of the syms of e.g., method type params (see #3692, where the type param T's bounds were set to >: T <: T, so that parts looped)
diff --git a/src/compiler/scala/tools/nsc/typechecker/RefChecks.scala b/src/compiler/scala/tools/nsc/typechecker/RefChecks.scala
index 12562fecf8..8a34d58e6e 100644
--- a/src/compiler/scala/tools/nsc/typechecker/RefChecks.scala
+++ b/src/compiler/scala/tools/nsc/typechecker/RefChecks.scala
@@ -844,159 +844,14 @@ abstract class RefChecks extends InfoTransform with scala.reflect.internal.trans
 
   // Variance Checking --------------------------------------------------------
 
-    private val NoVariance = 0
-    private val CoVariance = 1
-    private val AnyVariance = 2
-
-    private val escapedPrivateLocals = new mutable.HashSet[Symbol]
-
-    val varianceValidator = new Traverser {
-
-      /** Validate variance of info of symbol `base` */
-      private def validateVariance(base: Symbol) {
-        // A flag for when we're in a refinement, meaning method parameter types
-        // need to be checked.
-        var inRefinement = false
-
-        def varianceString(variance: Int): String =
-          if (variance == 1) "covariant"
-          else if (variance == -1) "contravariant"
-          else "invariant";
-
-        /** The variance of a symbol occurrence of `tvar`
-         *  seen at the level of the definition of `base`.
-         *  The search proceeds from `base` to the owner of `tvar`.
-         *  Initially the state is covariant, but it might change along the search.
-         */
-        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
-            // Flip occurrences of type parameters and parameters, unless
-            //  - it's a constructor, or case class factory or extractor
-            //  - it's a type parameter of tvar's owner.
-            if (sym.isParameter && !sym.owner.isConstructor && !sym.owner.isCaseApplyOrUnapply &&
-                !(tvar.isTypeParameterOrSkolem && sym.isTypeParameterOrSkolem &&
-                  tvar.owner == sym.owner)) state = -state;
-            else if (!sym.owner.isClass ||
-                     sym.isTerm && ((sym.isPrivateLocal || sym.isProtectedLocal || sym.isSuperAccessor /* super accessors are implicitly local #4345*/) && !(escapedPrivateLocals contains sym))) {
-              // return AnyVariance if `sym` is local to a term
-              // or is private[this] or protected[this]
-              state = AnyVariance
-            } else if (sym.isAliasType) {
-              // return AnyVariance if `sym` is an alias type
-              // that does not override anything. This is OK, because we always
-              // expand aliases for variance checking.
-              // However, if `sym` does override a type in a base class
-              // we have to assume NoVariance, as there might then be
-              // references to the type parameter that are not variance checked.
-              state = if (sym.isOverridingSymbol) NoVariance else AnyVariance
-            }
-            sym = sym.owner
-          }
-          state
-        }
-
-        /** Validate that the type `tp` is variance-correct, assuming
-         *  the type occurs itself at variance position given by `variance`
-         */
-        def validateVariance(tp: Type, variance: Int): Unit = tp match {
-          case ErrorType =>
-          case WildcardType =>
-          case BoundedWildcardType(bounds) =>
-            validateVariance(bounds, variance)
-          case NoType =>
-          case NoPrefix =>
-          case ThisType(_) =>
-          case ConstantType(_) =>
-          case SingleType(pre, sym) =>
-            validateVariance(pre, variance)
-          case TypeRef(pre, sym, args) =>
-//            println("validate "+sym+" at "+relativeVariance(sym))
-            if (sym.isAliasType/* && relativeVariance(sym) == AnyVariance*/)
-              validateVariance(tp.normalize, variance)
-            else if (sym.variance != NoVariance) {
-              val v = relativeVariance(sym)
-              if (v != AnyVariance && sym.variance != v * variance) {
-                //Console.println("relativeVariance(" + base + "," + sym + ") = " + v);//DEBUG
-                def tpString(tp: Type) = tp match {
-                  case ClassInfoType(parents, _, clazz) => "supertype "+intersectionType(parents, clazz.owner)
-                  case _ => "type "+tp
-                }
-                unit.error(base.pos,
-                           varianceString(sym.variance) + " " + sym +
-                           " occurs in " + varianceString(v * variance) +
-                           " position in " + tpString(base.info) + " of " + base);
-              }
-            }
-            validateVariance(pre, variance)
-            // @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
-            if (args.nonEmpty)
-              validateVarianceArgs(args, variance, sym.typeParams)
-          case ClassInfoType(parents, decls, symbol) =>
-            validateVariances(parents, variance)
-          case RefinedType(parents, decls) =>
-            validateVariances(parents, variance)
-            val saved = inRefinement
-            inRefinement = true
-            for (sym <- decls)
-              validateVariance(sym.info, if (sym.isAliasType) NoVariance else variance)
-            inRefinement = saved
-          case TypeBounds(lo, hi) =>
-            validateVariance(lo, -variance)
-            validateVariance(hi, variance)
-          case mt @ MethodType(formals, result) =>
-            if (inRefinement)
-              validateVariances(mt.paramTypes, -variance)
-            validateVariance(result, variance)
-          case NullaryMethodType(result) =>
-            validateVariance(result, variance)
-          case PolyType(tparams, result) =>
-            // type parameters will be validated separately, because they are defined explicitly.
-            validateVariance(result, variance)
-          case ExistentialType(tparams, result) =>
-            validateVariances(tparams map (_.info), variance)
-            validateVariance(result, variance)
-          case AnnotatedType(annots, tp, selfsym) =>
-            if (!annots.exists(_ matches uncheckedVarianceClass))
-              validateVariance(tp, variance)
-        }
-
-        def validateVariances(tps: List[Type], variance: Int) {
-          tps foreach (tp => validateVariance(tp, variance))
-        }
-
-        def validateVarianceArgs(tps: List[Type], variance: Int, tparams: List[Symbol]) {
-          foreach2(tps, tparams)((tp, tparam) => validateVariance(tp, variance * tparam.variance))
-        }
-
-        validateVariance(base.info, CoVariance)
+    object varianceValidator extends VarianceValidator {
+      private def tpString(tp: Type) = tp match {
+        case ClassInfoType(parents, _, clazz) => "supertype "+intersectionType(parents, clazz.owner)
+        case _                                => "type "+tp
       }
-
-      override def traverse(tree: Tree) {
-        tree match {
-          case ClassDef(_, _, _, _) | TypeDef(_, _, _, _) =>
-            validateVariance(tree.symbol)
-            super.traverse(tree)
-          // ModuleDefs need not be considered because they have been eliminated already
-          case ValDef(_, _, _, _) =>
-            if (!tree.symbol.hasLocalFlag)
-              validateVariance(tree.symbol)
-          case DefDef(_, _, tparams, vparamss, _, _) =>
-            // No variance check for object-private/protected methods/values.
-            if (!tree.symbol.hasLocalFlag) {
-              validateVariance(tree.symbol)
-              traverseTrees(tparams)
-              traverseTreess(vparamss)
-            }
-          case Template(_, _, _) =>
-            super.traverse(tree)
-          case _ =>
-        }
+      override def issueVarianceError(base: Symbol, sym: Symbol, required: Variance) {
+        currentRun.currentUnit.error(base.pos,
+          s"${sym.variance} $sym occurs in $required position in ${tpString(base.info)} of $base")
       }
     }
 
@@ -1594,18 +1449,10 @@ abstract class RefChecks extends InfoTransform with scala.reflect.internal.trans
         checkMigration(sym, tree.pos)
       checkCompileTimeOnly(sym, tree.pos)
 
-      if (sym eq NoSymbol) {
-        unit.warning(tree.pos, "Select node has NoSymbol! " + tree + " / " + tree.tpe)
-      }
-      else if (currentClass != sym.owner && sym.hasLocalFlag) {
-        var o = currentClass
-        var hidden = false
-        while (!hidden && o != sym.owner && o != sym.owner.moduleClass && !o.isPackage) {
-          hidden = o.isTerm || o.isPrivateLocal
-          o = o.owner
-        }
-        if (!hidden) escapedPrivateLocals += sym
-      }
+      if (sym eq NoSymbol)
+        devWarning("Select node has NoSymbol! " + tree + " / " + tree.tpe)
+      else if (sym.hasLocalFlag)
+        varianceValidator.checkForEscape(sym, currentClass)
 
       def checkSuper(mix: Name) =
         // term should have been eliminated by super accessors
diff --git a/src/compiler/scala/tools/nsc/typechecker/TypeDiagnostics.scala b/src/compiler/scala/tools/nsc/typechecker/TypeDiagnostics.scala
index 3bb6ae53dc..56b43eaa41 100644
--- a/src/compiler/scala/tools/nsc/typechecker/TypeDiagnostics.scala
+++ b/src/compiler/scala/tools/nsc/typechecker/TypeDiagnostics.scala
@@ -169,11 +169,6 @@ trait TypeDiagnostics {
     case xs   => " where " + (disambiguate(xs map (_.existentialToString)) mkString ", ")
   }
 
-  def varianceWord(sym: Symbol): String =
-    if (sym.variance == 1) "covariant"
-    else if (sym.variance == -1) "contravariant"
-    else "invariant"
-
   def explainAlias(tp: Type) = {
     // Don't automatically normalize standard aliases; they still will be
     // expanded if necessary to disambiguate simple identifiers.
@@ -223,7 +218,7 @@ trait TypeDiagnostics {
                 )
                 val explainDef = {
                   val prepend = if (isJava) "Java-defined " else ""
-                  "%s%s is %s in %s.".format(prepend, reqsym, varianceWord(param), param)
+                  "%s%s is %s in %s.".format(prepend, reqsym, param.variance, param)
                 }
                 // Don't suggest they change the class declaration if it's somewhere
                 // under scala.* or defined in a java class, because attempting either
@@ -243,7 +238,7 @@ trait TypeDiagnostics {
                 || ((arg <:< reqArg) && param.isCovariant)
                 || ((reqArg <:< arg) && param.isContravariant)
               )
-              val invariant = param.variance == 0
+              val invariant = param.variance.isInvariant
 
               if (conforms)                             Some("")
               else if ((arg <:< reqArg) && invariant)   mkMsg(true)   // covariant relationship
diff --git a/src/compiler/scala/tools/nsc/typechecker/Typers.scala b/src/compiler/scala/tools/nsc/typechecker/Typers.scala
index b853f687a7..acbd71bc31 100644
--- a/src/compiler/scala/tools/nsc/typechecker/Typers.scala
+++ b/src/compiler/scala/tools/nsc/typechecker/Typers.scala
@@ -938,17 +938,18 @@ trait Typers extends Modes with Adaptations with Tags {
           val unapply = unapplyMember(extractor.tpe)
           val clazz = unapplyParameterType(unapply)
 
-          if (unapply.isCase && clazz.isCase && !(clazz.ancestors exists (_.isCase))) {
+          if (unapply.isCase && clazz.isCase) {
             // convert synthetic unapply of case class to case class constructor
             val prefix = tree.tpe.prefix
             val tree1 = TypeTree(clazz.primaryConstructor.tpe.asSeenFrom(prefix, clazz.owner))
               .setOriginal(tree)
 
             val skolems = new mutable.ListBuffer[TypeSymbol]
-            object variantToSkolem extends VariantTypeMap {
+            object variantToSkolem extends TypeMap(trackVariance = true) {
               def apply(tp: Type) = mapOver(tp) match {
-                case TypeRef(NoPrefix, tpSym, Nil) if variance != 0 && tpSym.isTypeParameterOrSkolem && tpSym.owner.isTerm =>
-                  val bounds = if (variance == 1) TypeBounds.upper(tpSym.tpe) else TypeBounds.lower(tpSym.tpe)
+                // !!! FIXME - skipping this when variance.isInvariant allows unsoundness, see SI-5189
+                case TypeRef(NoPrefix, tpSym, Nil) if !variance.isInvariant && tpSym.isTypeParameterOrSkolem && tpSym.owner.isTerm =>
+                  val bounds = if (variance.isPositive) TypeBounds.upper(tpSym.tpe) else TypeBounds.lower(tpSym.tpe)
                   // origin must be the type param so we can deskolemize
                   val skolem = context.owner.newGADTSkolem(unit.freshTypeName("?"+tpSym.name), tpSym, bounds)
                   // println("mapping "+ tpSym +" to "+ skolem + " : "+ bounds +" -- pt= "+ pt +" in "+ context.owner +" at "+ context.tree )
@@ -2076,37 +2077,58 @@ trait Typers extends Modes with Adaptations with Tags {
      */
     def checkMethodStructuralCompatible(ddef: DefDef): Unit = {
       val meth = ddef.symbol
-      def fail(pos: Position, msg: String) = unit.error(pos, msg)
-      val tp: Type = meth.tpe match {
-        case mt @ MethodType(_, _)     => mt
-        case NullaryMethodType(restpe) => restpe  // TODO_NMT: drop NullaryMethodType from resultType?
-        case PolyType(_, restpe)       => restpe
-        case _                         => NoType
-      }
-      def nthParamPos(n: Int) = ddef.vparamss match {
-        case xs :: _ if xs.length > n => xs(n).pos
-        case _                        => meth.pos
-      }
-      def failStruct(pos: Position, what: String, where: String = "Parameter") =
-        fail(pos, s"$where type in structural refinement may not refer to $what")
-
-      foreachWithIndex(tp.paramTypes) { (paramType, idx) =>
-        val sym = paramType.typeSymbol
-        def paramPos = nthParamPos(idx)
-
-        if (sym.isAbstractType) {
-          if (!sym.hasTransOwner(meth.owner))
-            failStruct(paramPos, "an abstract type defined outside that refinement")
-          else if (!sym.hasTransOwner(meth))
-            failStruct(paramPos, "a type member of that refinement")
+      def parentString = meth.owner.parentSymbols filterNot (_ == ObjectClass) match {
+        case Nil => ""
+        case xs  => xs.map(_.nameString).mkString(" (of ", " with ", ")")
+      }
+      def fail(pos: Position, msg: String): Boolean = {
+        unit.error(pos, msg)
+        false
+      }
+      /** Have to examine all parameters in all lists.
+       */
+      def paramssTypes(tp: Type): List[List[Type]] = tp match {
+        case mt @ MethodType(_, restpe) => mt.paramTypes :: paramssTypes(restpe)
+        case PolyType(_, restpe)        => paramssTypes(restpe)
+        case _                          => Nil
+      }
+      def resultType = meth.tpe.finalResultType
+      def nthParamPos(n1: Int, n2: Int) =
+        try ddef.vparamss(n1)(n2).pos catch { case _: IndexOutOfBoundsException => meth.pos }
+
+      def failStruct(pos: Position, what: String, where: String = "Parameter type") =
+        fail(pos, s"$where in structural refinement may not refer to $what")
+
+      foreachWithIndex(paramssTypes(meth.tpe)) { (paramList, listIdx) =>
+        foreachWithIndex(paramList) { (paramType, paramIdx) =>
+          val sym = paramType.typeSymbol
+          def paramPos = nthParamPos(listIdx, paramIdx)
+
+          /** Not enough to look for abstract types; have to recursively check the bounds
+           *  of each abstract type for more abstract types. Almost certainly there are other
+           *  exploitable type soundness bugs which can be seen by bounding a type parameter
+           *  by an abstract type which itself is bounded by an abstract type.
+           */
+          def checkAbstract(tp0: Type, what: String): Boolean = {
+            def check(sym: Symbol): Boolean = !sym.isAbstractType || {
+              log(s"""checking $tp0 in refinement$parentString at ${meth.owner.owner.fullLocationString}""")
+              (    (!sym.hasTransOwner(meth.owner) && failStruct(paramPos, "an abstract type defined outside that refinement", what))
+                || (!sym.hasTransOwner(meth) && failStruct(paramPos, "a type member of that refinement", what))
+                || checkAbstract(sym.info.bounds.hi, "Type bound")
+              )
+            }
+            tp0.dealiasWidenChain forall (t => check(t.typeSymbol))
+          }
+          checkAbstract(paramType, "Parameter type")
+
+          if (sym.isDerivedValueClass)
+            failStruct(paramPos, "a user-defined value class")
+          if (paramType.isInstanceOf[ThisType] && sym == meth.owner)
+            failStruct(paramPos, "the type of that refinement (self type)")
         }
-        if (sym.isDerivedValueClass)
-          failStruct(paramPos, "a user-defined value class")
-        if (paramType.isInstanceOf[ThisType] && sym == meth.owner)
-          failStruct(paramPos, "the type of that refinement (self type)")
       }
-      if (tp.resultType.typeSymbol.isDerivedValueClass)
-        failStruct(ddef.tpt.pos, "a user-defined value class", where = "Result")
+      if (resultType.typeSymbol.isDerivedValueClass)
+        failStruct(ddef.tpt.pos, "a user-defined value class", where = "Result type")
     }
 
     def typedUseCase(useCase: UseCase) {
diff --git a/src/compiler/scala/tools/nsc/typechecker/Variances.scala b/src/compiler/scala/tools/nsc/typechecker/Variances.scala
deleted file mode 100644
index aa66a8d00a..0000000000
--- a/src/compiler/scala/tools/nsc/typechecker/Variances.scala
+++ /dev/null
@@ -1,94 +0,0 @@
-/* NSC -- new scala compiler
- * Copyright 2005-2013 LAMP/EPFL
- * @author  Martin Odersky
- */
-
-package scala.tools.nsc
-package typechecker
-
-import symtab.Flags.{ VarianceFlags => VARIANCES, _ }
-
-/** Variances form a lattice, 0 <= COVARIANT <= Variances, 0 <= CONTRAVARIANT <= VARIANCES
- */
-trait Variances {
-
-  val global: Global
-  import global._
-
-  /** Flip between covariant and contravariant */
-  private def flip(v: Int): Int = {
-    if (v == COVARIANT) CONTRAVARIANT
-    else if (v == CONTRAVARIANT) COVARIANT
-    else v
-  }
-
-  /** Map everything below VARIANCES to 0 */
-  private def cut(v: Int): Int =
-    if (v == VARIANCES) v else 0
-
-  /** Compute variance of type parameter `tparam` in types of all symbols `sym`. */
-  def varianceInSyms(syms: List[Symbol])(tparam: Symbol): Int =
-    (VARIANCES /: syms) ((v, sym) => v & varianceInSym(sym)(tparam))
-
-  /** Compute variance of type parameter `tparam` in type of symbol `sym`. */
-  def varianceInSym(sym: Symbol)(tparam: Symbol): Int =
-    if (sym.isAliasType) cut(varianceInType(sym.info)(tparam))
-    else varianceInType(sym.info)(tparam)
-
-  /** Compute variance of type parameter `tparam` in all types `tps`. */
-  def varianceInTypes(tps: List[Type])(tparam: Symbol): Int =
-    (VARIANCES /: tps) ((v, tp) => v & varianceInType(tp)(tparam))
-
-  /** Compute variance of type parameter `tparam` in all type arguments
-   *  `tps` which correspond to formal type parameters `tparams1`.
-   */
-  def varianceInArgs(tps: List[Type], tparams1: List[Symbol])(tparam: Symbol): Int = {
-    var v: Int = VARIANCES;
-    for ((tp, tparam1) <- tps zip tparams1) {
-      val v1 = varianceInType(tp)(tparam)
-      v = v & (if (tparam1.isCovariant) v1
-	       else if (tparam1.isContravariant) flip(v1)
-	       else cut(v1))
-    }
-    v
-  }
-
-  /** Compute variance of type parameter `tparam` in all type annotations `annots`. */
-  def varianceInAttribs(annots: List[AnnotationInfo])(tparam: Symbol): Int = {
-    (VARIANCES /: annots) ((v, annot) => v & varianceInAttrib(annot)(tparam))
-  }
-
-  /** Compute variance of type parameter `tparam` in type annotation `annot`. */
-  def varianceInAttrib(annot: AnnotationInfo)(tparam: Symbol): Int = {
-    varianceInType(annot.atp)(tparam)
-  }
-
-  /** Compute variance of type parameter `tparam` in type `tp`. */
-  def varianceInType(tp: Type)(tparam: Symbol): Int = tp match {
-    case ErrorType | WildcardType | NoType | NoPrefix | ThisType(_) | ConstantType(_) =>
-      VARIANCES
-    case BoundedWildcardType(bounds) =>
-      varianceInType(bounds)(tparam)
-    case SingleType(pre, sym) =>
-      varianceInType(pre)(tparam)
-    case TypeRef(pre, sym, args) =>
-      if (sym == tparam) COVARIANT
-      // tparam cannot occur in tp's args if tp is a type constructor (those don't have args)
-      else if (tp.isHigherKinded) varianceInType(pre)(tparam)
-      else varianceInType(pre)(tparam) & varianceInArgs(args, sym.typeParams)(tparam)
-    case TypeBounds(lo, hi) =>
-      flip(varianceInType(lo)(tparam)) & varianceInType(hi)(tparam)
-    case RefinedType(parents, defs) =>
-      varianceInTypes(parents)(tparam) & varianceInSyms(defs.toList)(tparam)
-    case MethodType(params, restpe) =>
-      flip(varianceInSyms(params)(tparam)) & varianceInType(restpe)(tparam)
-    case NullaryMethodType(restpe) =>
-      varianceInType(restpe)(tparam)
-    case PolyType(tparams, restpe) =>
-      flip(varianceInSyms(tparams)(tparam)) & varianceInType(restpe)(tparam)
-    case ExistentialType(tparams, restpe) =>
-      varianceInSyms(tparams)(tparam) & varianceInType(restpe)(tparam)
-    case AnnotatedType(annots, tp, _) =>
-      varianceInAttribs(annots)(tparam) & varianceInType(tp)(tparam)
-  }
-}
diff --git a/src/library/scala/collection/TraversableLike.scala b/src/library/scala/collection/TraversableLike.scala
index a55257d128..fdbc5e9857 100644
--- a/src/library/scala/collection/TraversableLike.scala
+++ b/src/library/scala/collection/TraversableLike.scala
@@ -77,7 +77,7 @@ trait TraversableLike[+A, +Repr] extends Any
   import Traversable.breaks._
 
   /** The type implementing this traversable */
-  protected type Self = Repr
+  protected[this] type Self = Repr
 
   /** The collection of type $coll underlying this `TraversableLike` object.
    *  By default this is implemented as the `TraversableLike` object itself,
diff --git a/src/library/scala/collection/generic/GenericClassTagCompanion.scala b/src/library/scala/collection/generic/GenericClassTagCompanion.scala
index a587bbf544..76c12d118e 100644
--- a/src/library/scala/collection/generic/GenericClassTagCompanion.scala
+++ b/src/library/scala/collection/generic/GenericClassTagCompanion.scala
@@ -19,7 +19,7 @@ import scala.reflect.ClassTag
  *  @author Aleksandar Prokopec
  */
 abstract class GenericClassTagCompanion[+CC[X] <: Traversable[X]] {
-  type Coll = CC[_]
+  protected[this] type Coll = CC[_]
 
   def newBuilder[A](implicit ord: ClassTag[A]): Builder[A, CC[A]]
 
diff --git a/src/library/scala/collection/generic/GenericCompanion.scala b/src/library/scala/collection/generic/GenericCompanion.scala
index 5b03f8e5c6..b966ce51db 100644
--- a/src/library/scala/collection/generic/GenericCompanion.scala
+++ b/src/library/scala/collection/generic/GenericCompanion.scala
@@ -24,7 +24,7 @@ import scala.language.higherKinds
  */
 abstract class GenericCompanion[+CC[X] <: GenTraversable[X]] {
   /** The underlying collection type with unknown element type */
-  type Coll = CC[_]
+  protected[this] type Coll = CC[_]
 
   /** The default builder for `$Coll` objects.
    *  @tparam A      the type of the ${coll}'s elements
diff --git a/src/library/scala/collection/generic/GenericOrderedCompanion.scala b/src/library/scala/collection/generic/GenericOrderedCompanion.scala
index a9a50a1c35..094912c75a 100644
--- a/src/library/scala/collection/generic/GenericOrderedCompanion.scala
+++ b/src/library/scala/collection/generic/GenericOrderedCompanion.scala
@@ -19,7 +19,7 @@ import scala.language.higherKinds
  *  @since 2.8
  */
 abstract class GenericOrderedCompanion[+CC[X] <: Traversable[X]] {
-  type Coll = CC[_]
+  protected[this] type Coll = CC[_]
 
   def newBuilder[A](implicit ord: Ordering[A]): Builder[A, CC[A]]
 
diff --git a/src/library/scala/collection/immutable/TrieIterator.scala b/src/library/scala/collection/immutable/TrieIterator.scala
index f117bddb8c..550f4cd7e0 100644
--- a/src/library/scala/collection/immutable/TrieIterator.scala
+++ b/src/library/scala/collection/immutable/TrieIterator.scala
@@ -46,7 +46,7 @@ private[collection] abstract class TrieIterator[+T](elems: Array[Iterable[T]]) e
     case x: HashSetCollision1[_]    => x.ks.map(x => HashSet(x)).toArray
   }).asInstanceOf[Array[Iterable[T]]]
 
-  private type SplitIterators = ((Iterator[T], Int), Iterator[T])
+  private[this] type SplitIterators = ((Iterator[T], Int), Iterator[T])
 
   private def isTrie(x: AnyRef) = x match {
     case _: HashTrieMap[_,_] | _: HashTrieSet[_] => true
diff --git a/src/library/scala/collection/parallel/ParSeqLike.scala b/src/library/scala/collection/parallel/ParSeqLike.scala
index 201b624c72..874cf6fee9 100644
--- a/src/library/scala/collection/parallel/ParSeqLike.scala
+++ b/src/library/scala/collection/parallel/ParSeqLike.scala
@@ -44,8 +44,8 @@ trait ParSeqLike[+T, +Repr <: ParSeq[T], +Sequential <: Seq[T] with SeqLike[T, S
 extends scala.collection.GenSeqLike[T, Repr]
    with ParIterableLike[T, Repr, Sequential] {
 self =>
-  
-  type SuperParIterator = IterableSplitter[T]
+
+  protected[this] type SuperParIterator = IterableSplitter[T]
 
   /** A more refined version of the iterator found in the `ParallelIterable` trait,
    *  this iterator can be split into arbitrary subsets of iterators.
diff --git a/src/reflect/scala/reflect/internal/BaseTypeSeqs.scala b/src/reflect/scala/reflect/internal/BaseTypeSeqs.scala
index 18a4a36840..9daf9504f1 100644
--- a/src/reflect/scala/reflect/internal/BaseTypeSeqs.scala
+++ b/src/reflect/scala/reflect/internal/BaseTypeSeqs.scala
@@ -64,7 +64,7 @@ trait BaseTypeSeqs {
             //Console.println("compute closure of "+this+" => glb("+variants+")")
             pending += i
             try {
-              mergePrefixAndArgs(variants, -1, lubDepth(variants)) match {
+              mergePrefixAndArgs(variants, Variance.Contravariant, lubDepth(variants)) match {
                 case Some(tp0) =>
                   pending(i) = false
                   elems(i) = tp0
diff --git a/src/reflect/scala/reflect/internal/Flags.scala b/src/reflect/scala/reflect/internal/Flags.scala
index 654dbd76e7..6aa7eab689 100644
--- a/src/reflect/scala/reflect/internal/Flags.scala
+++ b/src/reflect/scala/reflect/internal/Flags.scala
@@ -508,4 +508,4 @@ class Flags extends ModifierFlags {
   final val rawFlagPickledOrder: Array[Long] = pickledListOrder.toArray
 }
 
-object Flags extends Flags { }
+object Flags extends Flags
diff --git a/src/reflect/scala/reflect/internal/Kinds.scala b/src/reflect/scala/reflect/internal/Kinds.scala
index 08686832ef..5fecc06128 100644
--- a/src/reflect/scala/reflect/internal/Kinds.scala
+++ b/src/reflect/scala/reflect/internal/Kinds.scala
@@ -93,8 +93,8 @@ trait Kinds {
    *  If `sym2` is invariant, `sym1`'s variance is irrelevant. Otherwise they must be equal.
    */
   private def variancesMatch(sym1: Symbol, sym2: Symbol) = (
-       sym2.variance==0
-    || sym1.variance==sym2.variance
+       sym2.variance.isInvariant
+    || sym1.variance == sym2.variance
   )
 
   /** Check well-kindedness of type application (assumes arities are already checked) -- @M
@@ -229,4 +229,4 @@ trait Kinds {
       }
     }
   }
-}
\ No newline at end of file
+}
diff --git a/src/reflect/scala/reflect/internal/SymbolTable.scala b/src/reflect/scala/reflect/internal/SymbolTable.scala
index 540338dca7..e9ab7fa45d 100644
--- a/src/reflect/scala/reflect/internal/SymbolTable.scala
+++ b/src/reflect/scala/reflect/internal/SymbolTable.scala
@@ -15,6 +15,7 @@ abstract class SymbolTable extends macros.Universe
                               with Names
                               with Symbols
                               with Types
+                              with Variances
                               with Kinds
                               with ExistentialsAndSkolems
                               with FlagSets
diff --git a/src/reflect/scala/reflect/internal/Symbols.scala b/src/reflect/scala/reflect/internal/Symbols.scala
index ae68c1bcfd..0127bd988b 100644
--- a/src/reflect/scala/reflect/internal/Symbols.scala
+++ b/src/reflect/scala/reflect/internal/Symbols.scala
@@ -12,6 +12,7 @@ import util.{ Statistics, shortClassOfInstance }
 import Flags._
 import scala.annotation.tailrec
 import scala.reflect.io.{ AbstractFile, NoAbstractFile }
+import Variance._
 
 trait Symbols extends api.Symbols { self: SymbolTable =>
   import definitions._
@@ -165,10 +166,7 @@ trait Symbols extends api.Symbols { self: SymbolTable =>
     def debugFlagString: String           = flagString(AllFlags)
 
     /** String representation of symbol's variance */
-    def varianceString: String =
-      if (variance == 1) "+"
-      else if (variance == -1) "-"
-      else ""
+    def varianceString: String = variance.symbolicString
 
     override def flagMask =
       if (settings.debug.value && !isAbstractType) AllFlags
@@ -576,6 +574,17 @@ trait Symbols extends api.Symbols { self: SymbolTable =>
      */
     def isEffectiveRoot = false
 
+    /** Can this symbol only be subclassed by bottom classes? This is assessed
+     *  to be the case if it is final, and any type parameters are invariant.
+     */
+    def hasOnlyBottomSubclasses = {
+      def loop(tparams: List[Symbol]): Boolean = tparams match {
+        case Nil     => true
+        case x :: xs => x.variance.isInvariant && loop(xs)
+      }
+      isClass && isFinal && loop(typeParams)
+    }
+
     final def isLazyAccessor       = isLazy && lazyAccessor != NoSymbol
     final def isOverridableMember  = !(isClass || isEffectivelyFinal) && (this ne NoSymbol) && owner.isClass
 
@@ -890,11 +899,11 @@ trait Symbols extends api.Symbols { self: SymbolTable =>
       return true
     }
 
-    /** The variance of this symbol as an integer */
-    final def variance: Int =
-      if (isCovariant) 1
-      else if (isContravariant) -1
-      else 0
+    /** The variance of this symbol. */
+    def variance: Variance =
+      if (isCovariant) Covariant
+      else if (isContravariant) Contravariant
+      else Invariant
 
     /** The sequence number of this parameter symbol among all type
      *  and value parameters of symbol's owner. -1 if symbol does not
@@ -2626,6 +2635,9 @@ trait Symbols extends api.Symbols { self: SymbolTable =>
   class AliasTypeSymbol protected[Symbols] (initOwner: Symbol, initPos: Position, initName: TypeName)
   extends TypeSymbol(initOwner, initPos, initName) {
     type TypeOfClonedSymbol = TypeSymbol
+    override def variance = if (hasLocalFlag) Bivariant else info.typeSymbol.variance
+    override def isContravariant = variance.isContravariant
+    override def isCovariant     = variance.isCovariant
     final override def isAliasType = true
     override def cloneSymbolImpl(owner: Symbol, newFlags: Long): TypeSymbol =
       owner.newNonClassSymbol(name, pos, newFlags)
@@ -3288,7 +3300,6 @@ trait Symbols extends api.Symbols { self: SymbolTable =>
 // ----- Hoisted closures and convenience methods, for compile time reductions -------
 
   private[scala] final val symbolIsPossibleInRefinement = (sym: Symbol) => sym.isPossibleInRefinement
-  private[scala] final val symbolIsNonVariant = (sym: Symbol) => sym.variance == 0
 
   @tailrec private[scala] final
   def allSymbolsHaveOwner(syms: List[Symbol], owner: Symbol): Boolean = syms match {
diff --git a/src/reflect/scala/reflect/internal/Types.scala b/src/reflect/scala/reflect/internal/Types.scala
index 68f51e97bd..9d0d38913c 100644
--- a/src/reflect/scala/reflect/internal/Types.scala
+++ b/src/reflect/scala/reflect/internal/Types.scala
@@ -16,6 +16,7 @@ import scala.annotation.tailrec
 import util.Statistics
 import scala.runtime.ObjectRef
 import util.ThreeValues._
+import Variance._
 
 /* A standard type pattern match:
   case ErrorType =>
@@ -364,8 +365,7 @@ trait Types extends api.Types { self: SymbolTable =>
      *  This is assessed to be the case if the class is final,
      *  and all type parameters (if any) are invariant.
      */
-    def isFinalType =
-      typeSymbol.isFinal && (typeSymbol.typeParams forall symbolIsNonVariant)
+    def isFinalType = typeSymbol.hasOnlyBottomSubclasses
 
     /** Is this type completed (i.e. not a lazy type)? */
     def isComplete: Boolean = true
@@ -2807,7 +2807,7 @@ trait Types extends api.Types { self: SymbolTable =>
       val tvars = quantifiedFresh map (tparam => TypeVar(tparam))
       val underlying1 = underlying.instantiateTypeParams(quantified, tvars) // fuse subst quantified -> quantifiedFresh -> tvars
       op(underlying1) && {
-        solve(tvars, quantifiedFresh, quantifiedFresh map (x => 0), false, depth) &&
+        solve(tvars, quantifiedFresh, quantifiedFresh map (_ => Invariant), false, depth) &&
         isWithinBounds(NoPrefix, NoSymbol, quantifiedFresh, tvars map (_.constr.inst))
       }
     }
@@ -3927,93 +3927,29 @@ trait Types extends api.Types { self: SymbolTable =>
     def keepAnnotation(annot: AnnotationInfo) = annot matches TypeConstraintClass
   }
 
-  trait VariantTypeMap extends TypeMap {
-    private[this] var _variance = 1
-
-    override def variance = _variance
-    def variance_=(x: Int) = _variance = x
-
-    override protected def noChangeToSymbols(origSyms: List[Symbol]) =
-      //OPT inline from forall to save on #closures
-      origSyms match {
-        case sym :: rest =>
-          val v = variance
-          if (sym.isAliasType) variance = 0
-          val result = this(sym.info)
-          variance = v
-          (result eq sym.info) && noChangeToSymbols(rest)
-        case _ =>
-          true
-      }
-
-    override protected def mapOverArgs(args: List[Type], tparams: List[Symbol]): List[Type] =
-      map2Conserve(args, tparams) { (arg, tparam) =>
-        val v = variance
-        if (tparam.isContravariant) variance = -variance
-        else if (!tparam.isCovariant) variance = 0
-        val arg1 = this(arg)
-        variance = v
-        arg1
-      }
-
-    /** Map this function over given type */
-    override def mapOver(tp: Type): Type = tp match {
-      case MethodType(params, result) =>
-        variance = -variance
-        val params1 = mapOver(params)
-        variance = -variance
-        val result1 = this(result)
-        if ((params1 eq params) && (result1 eq result)) tp
-        else copyMethodType(tp, params1, result1.substSym(params, params1))
-      case PolyType(tparams, result) =>
-        variance = -variance
-        val tparams1 = mapOver(tparams)
-        variance = -variance
-        val result1 = this(result)
-        if ((tparams1 eq tparams) && (result1 eq result)) tp
-        else PolyType(tparams1, result1.substSym(tparams, tparams1))
-      case TypeBounds(lo, hi) =>
-        variance = -variance
-        val lo1 = this(lo)
-        variance = -variance
-        val hi1 = this(hi)
-        if ((lo1 eq lo) && (hi1 eq hi)) tp
-        else TypeBounds(lo1, hi1)
-      case tr @ TypeRef(pre, sym, args) =>
-        val pre1 = this(pre)
-        val args1 =
-          if (args.isEmpty)
-            args
-          else if (variance == 0) // fast & safe path: don't need to look at typeparams
-            args mapConserve this
-          else {
-            val tparams = sym.typeParams
-            if (tparams.isEmpty) args
-            else mapOverArgs(args, tparams)
-          }
-        if ((pre1 eq pre) && (args1 eq args)) tp
-        else copyTypeRef(tp, pre1, tr.coevolveSym(pre1), args1)
-      case _ =>
-        super.mapOver(tp)
-    }
-  }
-
   // todo. move these into scala.reflect.api
 
   /** A prototype for mapping a function over all possible types
    */
-  abstract class TypeMap extends (Type => Type) {
+  abstract class TypeMap(trackVariance: Boolean) extends (Type => Type) {
+    def this() = this(trackVariance = false)
     def apply(tp: Type): Type
 
-    /** Mix in VariantTypeMap if you want variances to be significant.
-     */
-    def variance = 0
+    private[this] var _variance: Variance = if (trackVariance) Covariant else Invariant
+
+    def variance_=(x: Variance) = { assert(trackVariance, this) ; _variance = x }
+    def variance = _variance
 
     /** Map this function over given type */
     def mapOver(tp: Type): Type = tp match {
       case tr @ TypeRef(pre, sym, args) =>
         val pre1 = this(pre)
-        val args1 = args mapConserve this
+        val args1 = (
+          if (trackVariance && args.nonEmpty && !variance.isInvariant && sym.typeParams.nonEmpty)
+            mapOverArgs(args, sym.typeParams)
+          else
+            args mapConserve this
+        )
         if ((pre1 eq pre) && (args1 eq args)) tp
         else copyTypeRef(tp, pre1, tr.coevolveSym(pre1), args1)
       case ThisType(_) => tp
@@ -4025,12 +3961,12 @@ trait Types extends api.Types { self: SymbolTable =>
           else singleType(pre1, sym)
         }
       case MethodType(params, result) =>
-        val params1 = mapOver(params)
+        val params1 = flipped(mapOver(params))
         val result1 = this(result)
         if ((params1 eq params) && (result1 eq result)) tp
         else copyMethodType(tp, params1, result1.substSym(params, params1))
       case PolyType(tparams, result) =>
-        val tparams1 = mapOver(tparams)
+        val tparams1 = flipped(mapOver(tparams))
         val result1 = this(result)
         if ((tparams1 eq tparams) && (result1 eq result)) tp
         else PolyType(tparams1, result1.substSym(tparams, tparams1))
@@ -4045,7 +3981,7 @@ trait Types extends api.Types { self: SymbolTable =>
         if ((thistp1 eq thistp) && (supertp1 eq supertp)) tp
         else SuperType(thistp1, supertp1)
       case TypeBounds(lo, hi) =>
-        val lo1 = this(lo)
+        val lo1 = flipped(this(lo))
         val hi1 = this(hi)
         if ((lo1 eq lo) && (hi1 eq hi)) tp
         else TypeBounds(lo1, hi1)
@@ -4068,7 +4004,7 @@ trait Types extends api.Types { self: SymbolTable =>
         else OverloadedType(pre1, alts)
       case AntiPolyType(pre, args) =>
         val pre1 = this(pre)
-        val args1 = args mapConserve (this)
+        val args1 = args mapConserve this
         if ((pre1 eq pre) && (args1 eq args)) tp
         else AntiPolyType(pre1, args1)
       case tv@TypeVar(_, constr) =>
@@ -4096,16 +4032,39 @@ trait Types extends api.Types { self: SymbolTable =>
         // throw new Error("mapOver inapplicable for " + tp);
     }
 
-    protected def mapOverArgs(args: List[Type], tparams: List[Symbol]): List[Type] =
-      args mapConserve this
+    def withVariance[T](v: Variance)(body: => T): T = {
+      val saved = variance
+      variance = v
+      try body finally variance = saved
+    }
+    @inline final def flipped[T](body: => T): T = {
+      if (trackVariance) variance = variance.flip
+      try body
+      finally if (trackVariance) variance = variance.flip
+    }
+    protected def mapOverArgs(args: List[Type], tparams: List[Symbol]): List[Type] = (
+      if (trackVariance)
+        map2Conserve(args, tparams)((arg, tparam) => withVariance(variance * tparam.variance)(this(arg)))
+      else
+        args mapConserve this
+    )
+    /** Applies this map to the symbol's info, setting variance = Invariant
+     *  if necessary when the symbol is an alias.
+     */
+    private def applyToSymbolInfo(sym: Symbol): Type = {
+      if (trackVariance && !variance.isInvariant && sym.isAliasType)
+        withVariance(Invariant)(this(sym.info))
+      else
+        this(sym.info)
+    }
 
     /** Called by mapOver to determine whether the original symbols can
-     *  be returned, or whether they must be cloned.  Overridden in VariantTypeMap.
+     *  be returned, or whether they must be cloned.
      */
     protected def noChangeToSymbols(origSyms: List[Symbol]): Boolean = {
       @tailrec def loop(syms: List[Symbol]): Boolean = syms match {
         case Nil     => true
-        case x :: xs => (x.info eq this(x.info)) && loop(xs)
+        case x :: xs => (x.info eq applyToSymbolInfo(x)) && loop(xs)
       }
       loop(origSyms)
     }
@@ -4259,7 +4218,7 @@ trait Types extends api.Types { self: SymbolTable =>
 
   /** Used by existentialAbstraction.
    */
-  class ExistentialExtrapolation(tparams: List[Symbol]) extends VariantTypeMap {
+  class ExistentialExtrapolation(tparams: List[Symbol]) extends TypeMap(trackVariance = true) {
     private val occurCount = mutable.HashMap[Symbol, Int]()
     private def countOccs(tp: Type) = {
       tp foreach {
@@ -4278,16 +4237,29 @@ trait Types extends api.Types { self: SymbolTable =>
       apply(tpe)
     }
 
+    /** If these conditions all hold:
+     *   1) we are in covariant (or contravariant) position
+     *   2) this type occurs exactly once in the existential scope
+     *   3) the widened upper (or lower) bound of this type contains no references to tparams
+     *  Then we replace this lone occurrence of the type with the widened upper (or lower) bound.
+     *  All other types pass through unchanged.
+     */
     def apply(tp: Type): Type = {
       val tp1 = mapOver(tp)
-      if (variance == 0) tp1
+      if (variance.isInvariant) tp1
       else tp1 match {
         case TypeRef(pre, sym, args) if tparams contains sym =>
-          val repl = if (variance == 1) dropSingletonType(tp1.bounds.hi) else tp1.bounds.lo
-          //println("eliminate "+sym+"/"+repl+"/"+occurCount(sym)+"/"+(tparams exists (repl.contains)))//DEBUG
-          if (!repl.typeSymbol.isBottomClass && occurCount(sym) == 1 && !(tparams exists (repl.contains)))
-            repl
-          else tp1
+          val repl = if (variance.isPositive) dropSingletonType(tp1.bounds.hi) else tp1.bounds.lo
+          val count = occurCount(sym)
+          val containsTypeParam = tparams exists (repl contains _)
+          def msg = {
+            val word = if (variance.isPositive) "upper" else "lower"
+            s"Widened lone occurrence of $tp1 inside existential to $word bound"
+          }
+          if (!repl.typeSymbol.isBottomClass && count == 1 && !containsTypeParam)
+            logResult(msg)(repl)
+          else
+            tp1
         case _ =>
           tp1
       }
@@ -5059,17 +5031,19 @@ trait Types extends api.Types { self: SymbolTable =>
     def isConsistent(tp1: Type, tp2: Type): Boolean = (tp1, tp2) match {
       case (TypeRef(pre1, sym1, args1), TypeRef(pre2, sym2, args2)) =>
         assert(sym1 == sym2, (sym1, sym2))
-        pre1 =:= pre2 &&
-        forall3(args1, args2, sym1.typeParams)((arg1, arg2, tparam) =>
-          if (tparam.variance == 0) arg1 =:= arg2
-          // if left-hand argument is a typevar, make it compatible with variance
-          // this is for more precise pattern matching
-          // todo: work this in the spec of this method
-          // also: think what happens if there are embedded typevars?
-          else arg1 match {
-            case _: TypeVar => if (tparam.variance < 0) arg1 <:< arg2 else arg2 <:< arg1
-            case _          => true
-          }
+        (    pre1 =:= pre2
+          && forall3(args1, args2, sym1.typeParams) { (arg1, arg2, tparam) =>
+               // if left-hand argument is a typevar, make it compatible with variance
+               // this is for more precise pattern matching
+               // todo: work this in the spec of this method
+               // also: think what happens if there are embedded typevars?
+               if (tparam.variance.isInvariant)
+                 arg1 =:= arg2
+               else !arg1.isInstanceOf[TypeVar] || {
+                 if (tparam.variance.isContravariant) arg1 <:< arg2
+                 else arg2 <:< arg1
+               }
+             }
         )
       case (et: ExistentialType, _) =>
         et.withTypeVars(isConsistent(_, tp2))
@@ -5639,9 +5613,11 @@ trait Types extends api.Types { self: SymbolTable =>
     }))
 
   def isSubArgs(tps1: List[Type], tps2: List[Type], tparams: List[Symbol], depth: Int): Boolean = {
-    def isSubArg(t1: Type, t2: Type, variance: Int) =
-      (variance > 0 || isSubType(t2, t1, depth)) &&
-      (variance < 0 || isSubType(t1, t2, depth))
+    def isSubArg(t1: Type, t2: Type, variance: Variance) = (
+         (variance.isContravariant || isSubType(t1, t2, depth))
+      && (variance.isCovariant || isSubType(t2, t1, depth))
+    )
+
     corresponds3(tps1, tps2, tparams map (_.variance))(isSubArg)
   }
 
@@ -6020,7 +5996,7 @@ trait Types extends api.Types { self: SymbolTable =>
    *  `f` maps all elements to themselves.
    */
   def map2Conserve[A <: AnyRef, B](xs: List[A], ys: List[B])(f: (A, B) => A): List[A] =
-    if (xs.isEmpty) xs
+    if (xs.isEmpty || ys.isEmpty) xs
     else {
       val x1 = f(xs.head, ys.head)
       val xs1 = map2Conserve(xs.tail, ys.tail)(f)
@@ -6037,15 +6013,15 @@ trait Types extends api.Types { self: SymbolTable =>
    *  @param upper      When `true` search for max solution else min.
    */
   def solve(tvars: List[TypeVar], tparams: List[Symbol],
-            variances: List[Int], upper: Boolean): Boolean =
+            variances: List[Variance], upper: Boolean): Boolean =
      solve(tvars, tparams, variances, upper, AnyDepth)
 
   def solve(tvars: List[TypeVar], tparams: List[Symbol],
-            variances: List[Int], upper: Boolean, depth: Int): Boolean = {
+            variances: List[Variance], upper: Boolean, depth: Int): Boolean = {
 
-    def solveOne(tvar: TypeVar, tparam: Symbol, variance: Int) {
+    def solveOne(tvar: TypeVar, tparam: Symbol, variance: Variance) {
       if (tvar.constr.inst == NoType) {
-        val up = if (variance != CONTRAVARIANT) upper else !upper
+        val up = if (variance.isContravariant) !upper else upper
         tvar.constr.inst = null
         val bound: Type = if (up) tparam.info.bounds.hi else tparam.info.bounds.lo
         //Console.println("solveOne0(tv, tp, v, b)="+(tvar, tparam, variance, bound))
@@ -6228,7 +6204,7 @@ trait Types extends api.Types { self: SymbolTable =>
             else t
           }
           val tails = tsBts map (_.tail)
-          mergePrefixAndArgs(elimSub(ts1, depth) map elimHigherOrderTypeParam, 1, depth) match {
+          mergePrefixAndArgs(elimSub(ts1, depth) map elimHigherOrderTypeParam, Covariant, depth) match {
             case Some(tp) => loop(tp :: pretypes, tails)
             case _        => loop(pretypes, tails)
           }
@@ -6711,18 +6687,18 @@ trait Types extends api.Types { self: SymbolTable =>
     finally foreach2(tvs, saved)(_.suspended = _)
   }
 
-  /** Compute lub (if `variance == 1`) or glb (if `variance == -1`) of given list
+  /** Compute lub (if `variance == Covariant`) or glb (if `variance == Contravariant`) of given list
    *  of types `tps`. All types in `tps` are typerefs or singletypes
    *  with the same symbol.
    *  Return `Some(x)` if the computation succeeds with result `x`.
    *  Return `None` if the computation fails.
    */
-  def mergePrefixAndArgs(tps: List[Type], variance: Int, depth: Int): Option[Type] = tps match {
+  def mergePrefixAndArgs(tps: List[Type], variance: Variance, depth: Int): Option[Type] = tps match {
     case List(tp) =>
       Some(tp)
     case TypeRef(_, sym, _) :: rest =>
       val pres = tps map (_.prefix) // prefix normalizes automatically
-      val pre = if (variance == 1) lub(pres, depth) else glb(pres, depth)
+      val pre = if (variance.isPositive) lub(pres, depth) else glb(pres, depth)
       val argss = tps map (_.normalize.typeArgs) // symbol equality (of the tp in tps) was checked using typeSymbol, which normalizes, so should normalize before retrieving arguments
       val capturedParams = new ListBuffer[Symbol]
       try {
@@ -6760,7 +6736,7 @@ trait Types extends api.Types { self: SymbolTable =>
               }
               else {
                 if (tparam.variance == variance) lub(as, decr(depth))
-                else if (tparam.variance == -variance) glb(as, decr(depth))
+                else if (tparam.variance == variance.flip) glb(as, decr(depth))
                 else {
                   val l = lub(as, decr(depth))
                   val g = glb(as, decr(depth))
@@ -6784,7 +6760,7 @@ trait Types extends api.Types { self: SymbolTable =>
       }
     case SingleType(_, sym) :: rest =>
       val pres = tps map (_.prefix)
-      val pre = if (variance == 1) lub(pres, depth) else glb(pres, depth)
+      val pre = if (variance.isPositive) lub(pres, depth) else glb(pres, depth)
       try {
         Some(singleType(pre, sym))
       } catch {
@@ -7015,6 +6991,10 @@ trait Types extends api.Types { self: SymbolTable =>
     case _ =>
       1
   }
+
+  def withUncheckedVariance(tp: Type): Type =
+    tp withAnnotation (AnnotationInfo marker uncheckedVarianceClass.tpe)
+
   //OPT replaced with tailrecursive function to save on #closures
   // was:
   //    var d = 0
diff --git a/src/reflect/scala/reflect/internal/Variance.scala b/src/reflect/scala/reflect/internal/Variance.scala
new file mode 100644
index 0000000000..007d56eb35
--- /dev/null
+++ b/src/reflect/scala/reflect/internal/Variance.scala
@@ -0,0 +1,90 @@
+/* NSC -- new Scala compiler
+ * Copyright 2005-2013 LAMP/EPFL
+ * @author  Paul Phillips
+ */
+
+package scala.reflect
+package internal
+
+import Variance._
+
+/** Variances form a lattice:
+ *
+ *            - Covariant -
+ *           /             \
+ *  Invariant               Bivariant
+ *           \             /
+ *            Contravariant
+ *
+ *  The variance of a symbol within a type is calculated based on variance
+ *  annotations, e.g. +A or -A, and the positions of the types in which the
+ *  symbol appears. The actual mechanics are beyond the scope of this
+ *  comment, but the essential operations on a Variance are:
+ *
+ *  '&'  - like bitwise AND. Unless all inputs have compatible variance,
+ *  folding them across & will be invariant.
+ *  '*'  - like multiplication across { -1, 0, 1 } with contravariance as -1.
+ *  flip - if contravariant or covariant, flip to the other; otherwise leave unchanged.
+ *  cut  - if bivariant, remain bivariant; otherwise become invariant.
+ *
+ *  There is an important distinction between "isPositive" and "isCovariant".
+ *  The former is true for both Covariant and Bivariant, but the latter is true
+ *  only for Covariant.
+ */
+final class Variance private (val flags: Int) extends AnyVal {
+  def isBivariant     = flags == 2
+  def isCovariant     = flags == 1    // excludes bivariant
+  def isInvariant     = flags == 0
+  def isContravariant = flags == -1   // excludes bivariant
+  def isPositive      = flags > 0     // covariant or bivariant
+
+  def &(other: Variance): Variance = (
+    if (this == other) this
+    else if (this.isBivariant) other
+    else if (other.isBivariant) this
+    else Invariant
+  )
+
+  def *(other: Variance): Variance = (
+    if (other.isPositive) this
+    else if (other.isContravariant) this.flip
+    else this.cut
+  )
+
+  /** Flip between covariant and contravariant. I chose not to use unary_- because it doesn't stand out enough. */
+  def flip = if (isCovariant) Contravariant else if (isContravariant) Covariant else this
+
+  /** Map everything below bivariant to invariant. */
+  def cut  = if (isBivariant) this else Invariant
+
+  /** The symbolic annotation used to indicate the given kind of variance. */
+  def symbolicString = (
+    if (isBivariant) "+/-"
+    else if (isCovariant) "+"
+    else if (isContravariant) "-"
+    else ""
+  )
+
+  override def toString = (
+    if (isContravariant) "contravariant"
+    else if (isCovariant) "covariant"
+    else if (isInvariant) "invariant"
+    else "" // noisy to print bivariant on everything without type parameters
+  )
+}
+
+object Variance {
+  implicit class SbtCompat(val v: Variance) {
+    def < (other: Int) = v.flags < other
+    def > (other: Int) = v.flags > other
+  }
+
+  def fold(variances: List[Variance]): Variance = (
+    if (variances.isEmpty) Bivariant
+    else variances reduceLeft (_ & _)
+  )
+  val Bivariant     = new Variance(2)
+  val Covariant     = new Variance(1)
+  val Contravariant = new Variance(-1)
+  val Invariant     = new Variance(0)
+}
diff --git a/src/reflect/scala/reflect/internal/Variances.scala b/src/reflect/scala/reflect/internal/Variances.scala
new file mode 100644
index 0000000000..716e49b303
--- /dev/null
+++ b/src/reflect/scala/reflect/internal/Variances.scala
@@ -0,0 +1,196 @@
+/* NSC -- new scala compiler
+ * Copyright 2005-2013 LAMP/EPFL
+ * @author  Martin Odersky
+ */
+
+package scala.reflect
+package internal
+
+import Variance._
+import scala.collection.{ mutable, immutable }
+import scala.annotation.tailrec
+
+/** See comments at scala.reflect.internal.Variance.
+ */
+trait Variances {
+  self: SymbolTable =>
+
+  /** Used in Refchecks.
+   *  TODO - eliminate duplication with varianceInType
+   */
+  class VarianceValidator extends Traverser {
+    private val escapedLocals = mutable.HashSet[Symbol]()
+    // A flag for when we're in a refinement, meaning method parameter types
+    // need to be checked.
+    private var inRefinement = false
+    @inline private def withinRefinement(body: => Type): Type = {
+      val saved = inRefinement
+      inRefinement = true
+      try body finally inRefinement = saved
+    }
+
+    /** Is every symbol in the owner chain between `site` and the owner of `sym`
+     *  either a term symbol or private[this]? If not, add `sym` to the set of
+     *  esacped locals.
+     *  @pre  sym.hasLocalFlag
+     */
+    @tailrec final def checkForEscape(sym: Symbol, site: Symbol) {
+      if (site == sym.owner || site == sym.owner.moduleClass || site.isPackage) () // done
+      else if (site.isTerm || site.isPrivateLocal) checkForEscape(sym, site.owner) // ok - recurse to owner
+      else escapedLocals += sym
+    }
+
+    protected def issueVarianceError(base: Symbol, sym: Symbol, required: Variance): Unit = ()
+
+    // Flip occurrences of type parameters and parameters, unless
+    //  - it's a constructor, or case class factory or extractor
+    //  - it's a type parameter of tvar's owner.
+    def shouldFlip(sym: Symbol, tvar: Symbol) = (
+         sym.isParameter
+      && !(tvar.isTypeParameterOrSkolem && sym.isTypeParameterOrSkolem && tvar.owner == sym.owner)
+    )
+    // return Bivariant if `sym` is local to a term
+    // or is private[this] or protected[this]
+    def isLocalOnly(sym: Symbol) = !sym.owner.isClass || (
+         sym.isTerm
+      && (sym.hasLocalFlag || sym.isSuperAccessor) // super accessors are implicitly local #4345
+      && !escapedLocals(sym)
+    )
+
+    private object ValidateVarianceMap extends TypeMap(trackVariance = true) {
+      private var base: Symbol = _
+
+      /** The variance of a symbol occurrence of `tvar` seen at the level of the definition of `base`.
+       *  The search proceeds from `base` to the owner of `tvar`.
+       *  Initially the state is covariant, but it might change along the search.
+       *
+       *  An alias which does not override anything is treated as Bivariant;
+       *  this is OK because we always expand aliases for variance checking.
+       *  However if it does override a type in a base class, we must assume Invariant
+       *  because there may be references to the type parameter that are not checked.
+       */
+      def relativeVariance(tvar: Symbol): Variance = {
+        def nextVariance(sym: Symbol, v: Variance): Variance = (
+          if (shouldFlip(sym, tvar)) v.flip
+          else if (isLocalOnly(sym)) Bivariant
+          else if (sym.isAliasType) Invariant
+          else v
+        )
+        def loop(sym: Symbol, v: Variance): Variance = (
+          if (sym == tvar.owner || v.isBivariant) v
+          else loop(sym.owner, nextVariance(sym, v))
+        )
+        loop(base, Covariant)
+      }
+      def isUncheckedVariance(tp: Type) = tp match {
+        case AnnotatedType(annots, _, _) => annots exists (_ matches definitions.uncheckedVarianceClass)
+        case _                           => false
+      }
+
+      private def checkVarianceOfSymbol(sym: Symbol) {
+        val relative = relativeVariance(sym)
+        val required = relative * variance
+        if (!relative.isBivariant) {
+          log(s"verifying $sym (${sym.variance}${sym.locationString}) is $required at $base in ${base.owner}")
+          if (sym.variance != required)
+            issueVarianceError(base, sym, required)
+        }
+      }
+      override def mapOver(decls: Scope): Scope = {
+        decls foreach (sym => withVariance(if (sym.isAliasType) Invariant else variance)(this(sym.info)))
+        decls
+      }
+      private def resultTypeOnly(tp: Type) = tp match {
+        case mt: MethodType => !inRefinement
+        case pt: PolyType   => true
+        case _              => false
+      }
+
+      /** For PolyTypes, type parameters are skipped because they are defined
+       *  explicitly (their TypeDefs will be passed here.) For MethodTypes, the
+       *  same is true of the parameters (ValDefs) unless we are inside a
+       *  refinement, in which case they are checked from here.
+       */
+      def apply(tp: Type): Type = tp match {
+        case _ if isUncheckedVariance(tp)                    => tp
+        case _ if resultTypeOnly(tp)                         => this(tp.resultType)
+        case TypeRef(_, sym, _) if sym.isAliasType           => this(tp.normalize)
+        case TypeRef(_, sym, _) if !sym.variance.isInvariant => checkVarianceOfSymbol(sym) ; mapOver(tp)
+        case RefinedType(_, _)                               => withinRefinement(mapOver(tp))
+        case ClassInfoType(parents, _, _)                    => parents foreach this ; tp
+        case mt @ MethodType(_, result)                      => flipped(mt.paramTypes foreach this) ; this(result)
+        case _                                               => mapOver(tp)
+      }
+      def validateDefinition(base: Symbol) {
+        val saved = this.base
+        this.base = base
+        try apply(base.info)
+        finally this.base = saved
+      }
+    }
+
+    /** Validate variance of info of symbol `base` */
+    private def validateVariance(base: Symbol) {
+      ValidateVarianceMap validateDefinition base
+    }
+
+    override def traverse(tree: Tree) {
+      def sym = tree.symbol
+      // No variance check for object-private/protected methods/values.
+      // Or constructors, or case class factory or extractor.
+      def skip = (
+           sym.hasLocalFlag
+        || sym.owner.isConstructor
+        || sym.owner.isCaseApplyOrUnapply
+      )
+      tree match {
+        case defn: MemberDef if skip =>
+          log(s"Skipping variance check of ${sym.defString}")
+        case ClassDef(_, _, _, _) | TypeDef(_, _, _, _) =>
+          validateVariance(sym)
+          super.traverse(tree)
+        // ModuleDefs need not be considered because they have been eliminated already
+        case ValDef(_, _, _, _) =>
+          validateVariance(sym)
+        case DefDef(_, _, tparams, vparamss, _, _) =>
+          validateVariance(sym)
+          traverseTrees(tparams)
+          traverseTreess(vparamss)
+        case Template(_, _, _) =>
+          super.traverse(tree)
+        case _ =>
+      }
+    }
+  }
+
+  /** Compute variance of type parameter `tparam` in all types `tps`. */
+  def varianceInTypes(tps: List[Type])(tparam: Symbol): Variance =
+    fold(tps map (tp => varianceInType(tp)(tparam)))
+
+  /** Compute variance of type parameter `tparam` in type `tp`. */
+  def varianceInType(tp: Type)(tparam: Symbol): Variance = {
+    def inArgs(sym: Symbol, args: List[Type]): Variance = fold(map2(args, sym.typeParams)((a, p) => inType(a) * p.variance))
+    def inSyms(syms: List[Symbol]): Variance            = fold(syms map inSym)
+    def inTypes(tps: List[Type]): Variance              = fold(tps map inType)
+
+    def inSym(sym: Symbol): Variance = if (sym.isAliasType) inType(sym.info).cut else inType(sym.info)
+    def inType(tp: Type): Variance   = tp match {
+      case ErrorType | WildcardType | NoType | NoPrefix => Bivariant
+      case ThisType(_) | ConstantType(_)                => Bivariant
+      case TypeRef(_, `tparam`, _)                      => Covariant
+      case BoundedWildcardType(bounds)                  => inType(bounds)
+      case NullaryMethodType(restpe)                    => inType(restpe)
+      case SingleType(pre, sym)                         => inType(pre)
+      case TypeRef(pre, _, _) if tp.isHigherKinded      => inType(pre)                 // a type constructor cannot occur in tp's args
+      case TypeRef(pre, sym, args)                      => inType(pre)                 & inArgs(sym, args)
+      case TypeBounds(lo, hi)                           => inType(lo).flip             & inType(hi)
+      case RefinedType(parents, defs)                   => inTypes(parents)            & inSyms(defs.toList)
+      case MethodType(params, restpe)                   => inSyms(params).flip         & inType(restpe)
+      case PolyType(tparams, restpe)                    => inSyms(tparams).flip        & inType(restpe)
+      case ExistentialType(tparams, restpe)             => inSyms(tparams)             & inType(restpe)
+      case AnnotatedType(annots, tp, _)                 => inTypes(annots map (_.atp)) & inType(tp)
+    }
+
+    inType(tp)
+  }
+}
diff --git a/test/files/neg/t5378.check b/test/files/neg/t5378.check
new file mode 100644
index 0000000000..c1460083f6
--- /dev/null
+++ b/test/files/neg/t5378.check
@@ -0,0 +1,31 @@
+t5378.scala:7: error: Type bound in structural refinement may not refer to an abstract type defined outside that refinement
+  def contains = new { def apply[T1 <: T](value: T1) = ??? }
+                                          ^
+t5378.scala:8: error: Type bound in structural refinement may not refer to an abstract type defined outside that refinement
+  def contains1 = new { def apply[T1 <: A1](value: T1) = ??? }
+                                            ^
+t5378.scala:9: error: Type bound in structural refinement may not refer to an abstract type defined outside that refinement
+  def contains2 = new { def apply[T1 <: A2](value: T1) = ??? }
+                                            ^
+t5378.scala:15: error: Type bound in structural refinement may not refer to an abstract type defined outside that refinement
+    new Bippy { def apply[T1 <: T](value: T1) = ??? }
+                                   ^
+t5378.scala:16: error: Type bound in structural refinement may not refer to an abstract type defined outside that refinement
+    new Bippy { def apply[T1 <: B1](value: T1) = ??? }
+                                    ^
+t5378.scala:17: error: Type bound in structural refinement may not refer to an abstract type defined outside that refinement
+    new Bippy { def apply[T1 <: B2](value: T1) = ??? }
+                                    ^
+t5378.scala:21: error: Type bound in structural refinement may not refer to an abstract type defined outside that refinement
+      def apply1[T1 <: B3](value: T1) = ???
+                           ^
+t5378.scala:23: error: Parameter type in structural refinement may not refer to an abstract type defined outside that refinement
+      def apply3(value: B3) = ???
+                 ^
+t5378.scala:28: error: Parameter type in structural refinement may not refer to an abstract type defined outside that refinement
+    def apply1(s: String)(x: Int)(value: T) = ???
+                                  ^
+t5378.scala:29: error: Type bound in structural refinement may not refer to an abstract type defined outside that refinement
+    def apply2[T1 <: T](s: String)(x: Int)(value: T1) = ???
+                                           ^
+10 errors found
diff --git a/test/files/neg/t5378.scala b/test/files/neg/t5378.scala
new file mode 100644
index 0000000000..fa6afa02be
--- /dev/null
+++ b/test/files/neg/t5378.scala
@@ -0,0 +1,54 @@
+import scala.language.reflectiveCalls
+
+class Coll[+T] {
+  type A1 <: T
+  type A2 <: A1
+
+  def contains = new { def apply[T1 <: T](value: T1) = ??? }
+  def contains1 = new { def apply[T1 <: A1](value: T1) = ??? }
+  def contains2 = new { def apply[T1 <: A2](value: T1) = ??? }
+  def contains3 = {
+    trait Bippy {
+      type B1 <: T
+      type B2 <: B1
+    }
+    new Bippy { def apply[T1 <: T](value: T1) = ??? }
+    new Bippy { def apply[T1 <: B1](value: T1) = ??? }
+    new Bippy { def apply[T1 <: B2](value: T1) = ??? }
+    new Bippy {
+      type B3 = B2
+      type B4 = List[B2]
+      def apply1[T1 <: B3](value: T1) = ???
+      def apply2[T1 <: B4](value: T1) = ???
+      def apply3(value: B3) = ???
+      def apply4(value: B4) = value.head
+    }
+  }
+  def contains4 = new {
+    def apply1(s: String)(x: Int)(value: T) = ???
+    def apply2[T1 <: T](s: String)(x: Int)(value: T1) = ???
+  }
+  def containsOk = {
+    trait Bippy {
+      type B1 <: AnyRef
+      type B2 <: B1
+    }
+    new Bippy { def apply[T1 <: AnyRef](value: T1) = ??? }
+    new Bippy { type B1 = String ; def apply[T1 <: B1](value: T1) = ??? }
+    new Bippy { type B2 = String ; def apply[T1 <: B2](value: T1) = ??? }
+  }
+}
+
+object Test {
+  def main(args: Array[String]): Unit = {
+    val xs = new Coll[List[String]]
+    val ys: Coll[Traversable[String]] = xs
+
+    println(ys contains Nil)
+    // java.lang.NoSuchMethodException: Coll$$anon$1.apply(scala.collection.Traversable)
+    //  at java.lang.Class.getMethod(Class.java:1605)
+    //  at Test$.reflMethod$Method1(a.scala:14)
+    //  at Test$.main(a.scala:14)
+    //  at Test.main(a.scala)
+  }
+}
diff --git a/test/files/neg/t6566a.check b/test/files/neg/t6566a.check
new file mode 100644
index 0000000000..7668f9d2fb
--- /dev/null
+++ b/test/files/neg/t6566a.check
@@ -0,0 +1,4 @@
+t6566a.scala:2: error: covariant type T occurs in invariant position in type T of type MyType
+  class TypeCheat[+T] { type MyType = T }
+                             ^
+one error found
diff --git a/test/files/neg/t6566a.scala b/test/files/neg/t6566a.scala
new file mode 100644
index 0000000000..74a0b38e56
--- /dev/null
+++ b/test/files/neg/t6566a.scala
@@ -0,0 +1,17 @@
+object WhatsYourTypeIsMyType {
+  class TypeCheat[+T] { type MyType = T }
+
+  class Foo {
+    val tc = new TypeCheat[Foo]
+    var x: tc.MyType = _
+    def setX() = x = new Foo
+  }
+  class Bar extends Foo {
+    override val tc = new TypeCheat[Bar]
+    def unsound = this
+
+    setX()
+    println(x.unsound)
+  }
+  def main(args: Array[String]): Unit = new Bar
+}
diff --git a/test/files/neg/t6566b.check b/test/files/neg/t6566b.check
new file mode 100644
index 0000000000..fb3fe81fca
--- /dev/null
+++ b/test/files/neg/t6566b.check
@@ -0,0 +1,4 @@
+t6566b.scala:3: error: covariant type T occurs in invariant position in type T of type MyType
+    type MyType = T
+         ^
+one error found
diff --git a/test/files/neg/t6566b.scala b/test/files/neg/t6566b.scala
new file mode 100644
index 0000000000..18ddebf88b
--- /dev/null
+++ b/test/files/neg/t6566b.scala
@@ -0,0 +1,19 @@
+object WhatsYourTypeIsMyType {
+  trait WithMyType[+T] {
+    type MyType = T
+  }
+
+  class Foo extends WithMyType[Foo] {
+    var x: MyType = _
+    def setX() = x = new Foo
+  }
+
+  class Bar extends Foo with WithMyType[Bar] {
+    def unsound { println("iAmABar") }
+
+    setX()
+    println(x.unsound)
+  }
+
+  def main(args: Array[String]): Unit = new Bar
+}
diff --git a/test/files/neg/variances-refinement.check b/test/files/neg/variances-refinement.check
new file mode 100644
index 0000000000..2bed3ffa6b
--- /dev/null
+++ b/test/files/neg/variances-refinement.check
@@ -0,0 +1,22 @@
+variances-refinement.scala:17: error: contravariant type A occurs in covariant position in type ()AnyRef{def f0(x: A): A} of method fail1
+  def fail1() = { object O { def f0(x: A): A = ??? } ; O } // fail
+      ^
+variances-refinement.scala:18: error: covariant type B occurs in contravariant position in type ()AnyRef{def f0(x: B): A} of method fail2
+  def fail2() = { object O { def f0(x: B): A = ??? } ; O } // fail
+      ^
+variances-refinement.scala:19: error: covariant type B occurs in contravariant position in type ()AnyRef{def f0(x: B): B} of method fail3
+  def fail3() = { object O { def f0(x: B): B = ??? } ; O } // fail
+      ^
+variances-refinement.scala:20: error: covariant type B occurs in contravariant position in type ()AnyRef{def f0(x: B): C} of method fail4
+  def fail4() = { object O { def f0(x: B): C = ??? } ; O } // fail
+      ^
+variances-refinement.scala:21: error: contravariant type A occurs in covariant position in type ()AnyRef{def f0(x: C): A} of method fail5
+  def fail5() = { object O { def f0(x: C): A = ??? } ; O } // fail
+      ^
+variances-refinement.scala:23: error: contravariant type A occurs in covariant position in type ()O1.type forSome { val O1: AnyRef with O0; type O0 <: AnyRef{def f0(x: A): A; def f1(x: A): B; def f2(x: A): C} } of method fail6
+  def fail6() = { // fail
+      ^
+variances-refinement.scala:32: error: contravariant type A occurs in covariant position in type ()AnyRef{def f0(x: A): A; def f1(x: A): B; def f2(x: A): C} of method fail7
+  def fail7() = { // fail
+      ^
+7 errors found
diff --git a/test/files/neg/variances-refinement.scala b/test/files/neg/variances-refinement.scala
new file mode 100644
index 0000000000..6bfd336ce0
--- /dev/null
+++ b/test/files/neg/variances-refinement.scala
@@ -0,0 +1,40 @@
+trait Trait[-A, +B, C] {
+  def ok() = { // ok
+    object O {
+      private def f0(x: A): A = ???
+      def f1(x: A): B = ???
+      def f2(x: A): C = ???
+      private def f3(x: B): A = ???
+      private def f4(x: B): B = ???
+      private def f5(x: B): C = ???
+      private def f6(x: C): A = ???
+      def f7(x: C): B = ???
+      def f8(x: C): C = ???
+    }
+    O
+  }
+
+  def fail1() = { object O { def f0(x: A): A = ??? } ; O } // fail
+  def fail2() = { object O { def f0(x: B): A = ??? } ; O } // fail
+  def fail3() = { object O { def f0(x: B): B = ??? } ; O } // fail
+  def fail4() = { object O { def f0(x: B): C = ??? } ; O } // fail
+  def fail5() = { object O { def f0(x: C): A = ??? } ; O } // fail
+
+  def fail6() = { // fail
+    trait O0 {
+      def f0(x: A): A = ???
+      def f1(x: A): B = ???
+      def f2(x: A): C = ???
+    }
+    object O1 extends O0
+    O1
+  }
+  def fail7() = { // fail
+    trait O0 {
+      def f0(x: A): A = ???
+      def f1(x: A): B = ???
+      def f2(x: A): C = ???
+    }
+    new O0 { }
+  }
+}
diff --git a/test/files/neg/variances.check b/test/files/neg/variances.check
index 0643e533b7..7d965e94dc 100644
--- a/test/files/neg/variances.check
+++ b/test/files/neg/variances.check
@@ -13,7 +13,10 @@ variances.scala:21: error: covariant type A occurs in invariant position in supe
 variances.scala:74: error: covariant type A occurs in contravariant position in type => test.Covariant.T[A]{val m: A => A} of value x
     val x: T[A] {
         ^
+variances.scala:89: error: covariant type T occurs in invariant position in type T of type A
+    type A = T
+         ^
 variances.scala:90: error: covariant type T occurs in contravariant position in type => test.TestAlias.B[C.this.A] of method foo
     def foo: B[A]
         ^
-6 errors found
+7 errors found
diff --git a/test/files/neg/variances2.check b/test/files/neg/variances2.check
new file mode 100644
index 0000000000..433cc125ad
--- /dev/null
+++ b/test/files/neg/variances2.check
@@ -0,0 +1,229 @@
+variances2.scala:9: error: covariant type B occurs in contravariant position in type B of value x
+    def f1(x: B): Unit = ()
+           ^
+variances2.scala:12: error: covariant type E occurs in contravariant position in type E of value x
+    def f4(x: E): Unit = ()
+           ^
+variances2.scala:15: error: contravariant type A occurs in covariant position in type ()A of method f6
+    def f6(): A = ???
+        ^
+variances2.scala:18: error: contravariant type D occurs in covariant position in type ()D of method f9
+    def f9(): D = ???
+        ^
+variances2.scala:22: error: contravariant type A occurs in covariant position in type A => A of value f
+    def f12(f: A => A): Unit = ()
+            ^
+variances2.scala:23: error: contravariant type A occurs in covariant position in type A => B of value f
+    def f13(f: A => B): Unit = ()
+            ^
+variances2.scala:24: error: contravariant type A occurs in covariant position in type A => C of value f
+    def f14(f: A => C): Unit = ()
+            ^
+variances2.scala:25: error: contravariant type A occurs in covariant position in type A => D of value f
+    def f15(f: A => D): Unit = ()
+            ^
+variances2.scala:26: error: contravariant type A occurs in covariant position in type A => E of value f
+    def f16(f: A => E): Unit = ()
+            ^
+variances2.scala:27: error: contravariant type A occurs in covariant position in type A => F of value f
+    def f17(f: A => F): Unit = ()
+            ^
+variances2.scala:29: error: covariant type B occurs in contravariant position in type B => B of value f
+    def f19(f: B => B): Unit = ()
+            ^
+variances2.scala:32: error: covariant type E occurs in contravariant position in type B => E of value f
+    def f22(f: B => E): Unit = ()
+            ^
+variances2.scala:35: error: covariant type B occurs in contravariant position in type C => B of value f
+    def f25(f: C => B): Unit = ()
+            ^
+variances2.scala:38: error: covariant type E occurs in contravariant position in type C => E of value f
+    def f28(f: C => E): Unit = ()
+            ^
+variances2.scala:40: error: contravariant type D occurs in covariant position in type D => A of value f
+    def f30(f: D => A): Unit = ()
+            ^
+variances2.scala:41: error: contravariant type D occurs in covariant position in type D => B of value f
+    def f31(f: D => B): Unit = ()
+            ^
+variances2.scala:42: error: contravariant type D occurs in covariant position in type D => C of value f
+    def f32(f: D => C): Unit = ()
+            ^
+variances2.scala:43: error: contravariant type D occurs in covariant position in type D => D of value f
+    def f33(f: D => D): Unit = ()
+            ^
+variances2.scala:44: error: contravariant type D occurs in covariant position in type D => E of value f
+    def f34(f: D => E): Unit = ()
+            ^
+variances2.scala:45: error: contravariant type D occurs in covariant position in type D => F of value f
+    def f35(f: D => F): Unit = ()
+            ^
+variances2.scala:47: error: covariant type B occurs in contravariant position in type E => B of value f
+    def f37(f: E => B): Unit = ()
+            ^
+variances2.scala:50: error: covariant type E occurs in contravariant position in type E => E of value f
+    def f40(f: E => E): Unit = ()
+            ^
+variances2.scala:53: error: covariant type B occurs in contravariant position in type F => B of value f
+    def f43(f: F => B): Unit = ()
+            ^
+variances2.scala:56: error: covariant type E occurs in contravariant position in type F => E of value f
+    def f46(f: F => E): Unit = ()
+            ^
+variances2.scala:59: error: contravariant type A occurs in covariant position in type ()A => A of method f48
+    def f48(): A => A = null
+        ^
+variances2.scala:62: error: contravariant type D occurs in covariant position in type ()A => D of method f51
+    def f51(): A => D = null
+        ^
+variances2.scala:65: error: covariant type B occurs in contravariant position in type ()B => A of method f54
+    def f54(): B => A = null
+        ^
+variances2.scala:66: error: covariant type B occurs in contravariant position in type ()B => B of method f55
+    def f55(): B => B = null
+        ^
+variances2.scala:67: error: covariant type B occurs in contravariant position in type ()B => C of method f56
+    def f56(): B => C = null
+        ^
+variances2.scala:68: error: covariant type B occurs in contravariant position in type ()B => D of method f57
+    def f57(): B => D = null
+        ^
+variances2.scala:69: error: covariant type B occurs in contravariant position in type ()B => E of method f58
+    def f58(): B => E = null
+        ^
+variances2.scala:70: error: covariant type B occurs in contravariant position in type ()B => F of method f59
+    def f59(): B => F = null
+        ^
+variances2.scala:71: error: contravariant type A occurs in covariant position in type ()C => A of method f60
+    def f60(): C => A = null
+        ^
+variances2.scala:74: error: contravariant type D occurs in covariant position in type ()C => D of method f63
+    def f63(): C => D = null
+        ^
+variances2.scala:77: error: contravariant type A occurs in covariant position in type ()D => A of method f66
+    def f66(): D => A = null
+        ^
+variances2.scala:80: error: contravariant type D occurs in covariant position in type ()D => D of method f69
+    def f69(): D => D = null
+        ^
+variances2.scala:83: error: covariant type E occurs in contravariant position in type ()E => A of method f72
+    def f72(): E => A = null
+        ^
+variances2.scala:84: error: covariant type E occurs in contravariant position in type ()E => B of method f73
+    def f73(): E => B = null
+        ^
+variances2.scala:85: error: covariant type E occurs in contravariant position in type ()E => C of method f74
+    def f74(): E => C = null
+        ^
+variances2.scala:86: error: covariant type E occurs in contravariant position in type ()E => D of method f75
+    def f75(): E => D = null
+        ^
+variances2.scala:87: error: covariant type E occurs in contravariant position in type ()E => E of method f76
+    def f76(): E => E = null
+        ^
+variances2.scala:88: error: covariant type E occurs in contravariant position in type ()E => F of method f77
+    def f77(): E => F = null
+        ^
+variances2.scala:89: error: contravariant type A occurs in covariant position in type ()F => A of method f78
+    def f78(): F => A = null
+        ^
+variances2.scala:92: error: contravariant type D occurs in covariant position in type ()F => D of method f81
+    def f81(): F => D = null
+        ^
+variances2.scala:96: error: contravariant type A occurs in covariant position in type (x: A)A of method f84
+    def f84(x: A): A = ???
+        ^
+variances2.scala:99: error: contravariant type D occurs in covariant position in type (x: A)D of method f87
+    def f87(x: A): D = ???
+        ^
+variances2.scala:102: error: contravariant type A occurs in covariant position in type (x: B)A of method f90
+    def f90(x: B): A = ???
+        ^
+variances2.scala:102: error: covariant type B occurs in contravariant position in type B of value x
+    def f90(x: B): A = ???
+            ^
+variances2.scala:103: error: covariant type B occurs in contravariant position in type B of value x
+    def f91(x: B): B = ???
+            ^
+variances2.scala:104: error: covariant type B occurs in contravariant position in type B of value x
+    def f92(x: B): C = ???
+            ^
+variances2.scala:105: error: contravariant type D occurs in covariant position in type (x: B)D of method f93
+    def f93(x: B): D = ???
+        ^
+variances2.scala:105: error: covariant type B occurs in contravariant position in type B of value x
+    def f93(x: B): D = ???
+            ^
+variances2.scala:106: error: covariant type B occurs in contravariant position in type B of value x
+    def f94(x: B): E = ???
+            ^
+variances2.scala:107: error: covariant type B occurs in contravariant position in type B of value x
+    def f95(x: B): F = ???
+            ^
+variances2.scala:108: error: contravariant type A occurs in covariant position in type (x: C)A of method f96
+    def f96(x: C): A = ???
+        ^
+variances2.scala:111: error: contravariant type D occurs in covariant position in type (x: C)D of method f99
+    def f99(x: C): D = ???
+        ^
+variances2.scala:114: error: contravariant type A occurs in covariant position in type (x: D)A of method f102
+    def f102(x: D): A = ???
+        ^
+variances2.scala:117: error: contravariant type D occurs in covariant position in type (x: D)D of method f105
+    def f105(x: D): D = ???
+        ^
+variances2.scala:120: error: contravariant type A occurs in covariant position in type (x: E)A of method f108
+    def f108(x: E): A = ???
+        ^
+variances2.scala:120: error: covariant type E occurs in contravariant position in type E of value x
+    def f108(x: E): A = ???
+             ^
+variances2.scala:121: error: covariant type E occurs in contravariant position in type E of value x
+    def f109(x: E): B = ???
+             ^
+variances2.scala:122: error: covariant type E occurs in contravariant position in type E of value x
+    def f110(x: E): C = ???
+             ^
+variances2.scala:123: error: contravariant type D occurs in covariant position in type (x: E)D of method f111
+    def f111(x: E): D = ???
+        ^
+variances2.scala:123: error: covariant type E occurs in contravariant position in type E of value x
+    def f111(x: E): D = ???
+             ^
+variances2.scala:124: error: covariant type E occurs in contravariant position in type E of value x
+    def f112(x: E): E = ???
+             ^
+variances2.scala:125: error: covariant type E occurs in contravariant position in type E of value x
+    def f113(x: E): F = ???
+             ^
+variances2.scala:126: error: contravariant type A occurs in covariant position in type (x: F)A of method f114
+    def f114(x: F): A = ???
+        ^
+variances2.scala:129: error: contravariant type D occurs in covariant position in type (x: F)D of method f117
+    def f117(x: F): D = ???
+        ^
+variances2.scala:133: error: contravariant type A occurs in covariant position in supertype Cov[A] of object O1
+    object O1 extends Cov[A]
+           ^
+variances2.scala:136: error: contravariant type D occurs in covariant position in supertype Cov[D] of object O4
+    object O4 extends Cov[D]
+           ^
+variances2.scala:140: error: covariant type B occurs in contravariant position in supertype Con[B] of object O8
+    object O8 extends Con[B]
+           ^
+variances2.scala:143: error: covariant type E occurs in contravariant position in supertype Con[E] of object O11
+    object O11 extends Con[E]
+           ^
+variances2.scala:145: error: contravariant type A occurs in invariant position in supertype Inv[A] of object O13
+    object O13 extends Inv[A]
+           ^
+variances2.scala:146: error: covariant type B occurs in invariant position in supertype Inv[B] of object O14
+    object O14 extends Inv[B]
+           ^
+variances2.scala:148: error: contravariant type D occurs in invariant position in supertype Inv[D] of object O16
+    object O16 extends Inv[D]
+           ^
+variances2.scala:149: error: covariant type E occurs in invariant position in supertype Inv[E] of object O17
+    object O17 extends Inv[E]
+           ^
+76 errors found
diff --git a/test/files/neg/variances2.scala b/test/files/neg/variances2.scala
new file mode 100644
index 0000000000..d30345dd83
--- /dev/null
+++ b/test/files/neg/variances2.scala
@@ -0,0 +1,303 @@
+trait Cov[+A]
+trait Con[-A]
+trait Inv[A]
+
+trait Trait[-A, +B, C] {
+  // trait Inner[-D <: C, +E >: C, F] {
+  trait Inner[-D <: C, +E >: C, F] {
+    def f0(x: A): Unit = ()
+    def f1(x: B): Unit = ()
+    def f2(x: C): Unit = ()
+    def f3(x: D): Unit = ()
+    def f4(x: E): Unit = ()
+    def f5(x: F): Unit = ()
+
+    def f6(): A = ???
+    def f7(): B = ???
+    def f8(): C = ???
+    def f9(): D = ???
+    def f10(): E = ???
+    def f11(): F = ???
+
+    def f12(f: A => A): Unit = ()
+    def f13(f: A => B): Unit = ()
+    def f14(f: A => C): Unit = ()
+    def f15(f: A => D): Unit = ()
+    def f16(f: A => E): Unit = ()
+    def f17(f: A => F): Unit = ()
+    def f18(f: B => A): Unit = ()
+    def f19(f: B => B): Unit = ()
+    def f20(f: B => C): Unit = ()
+    def f21(f: B => D): Unit = ()
+    def f22(f: B => E): Unit = ()
+    def f23(f: B => F): Unit = ()
+    def f24(f: C => A): Unit = ()
+    def f25(f: C => B): Unit = ()
+    def f26(f: C => C): Unit = ()
+    def f27(f: C => D): Unit = ()
+    def f28(f: C => E): Unit = ()
+    def f29(f: C => F): Unit = ()
+    def f30(f: D => A): Unit = ()
+    def f31(f: D => B): Unit = ()
+    def f32(f: D => C): Unit = ()
+    def f33(f: D => D): Unit = ()
+    def f34(f: D => E): Unit = ()
+    def f35(f: D => F): Unit = ()
+    def f36(f: E => A): Unit = ()
+    def f37(f: E => B): Unit = ()
+    def f38(f: E => C): Unit = ()
+    def f39(f: E => D): Unit = ()
+    def f40(f: E => E): Unit = ()
+    def f41(f: E => F): Unit = ()
+    def f42(f: F => A): Unit = ()
+    def f43(f: F => B): Unit = ()
+    def f44(f: F => C): Unit = ()
+    def f45(f: F => D): Unit = ()
+    def f46(f: F => E): Unit = ()
+    def f47(f: F => F): Unit = ()
+
+    def f48(): A => A = null
+    def f49(): A => B = null
+    def f50(): A => C = null
+    def f51(): A => D = null
+    def f52(): A => E = null
+    def f53(): A => F = null
+    def f54(): B => A = null
+    def f55(): B => B = null
+    def f56(): B => C = null
+    def f57(): B => D = null
+    def f58(): B => E = null
+    def f59(): B => F = null
+    def f60(): C => A = null
+    def f61(): C => B = null
+    def f62(): C => C = null
+    def f63(): C => D = null
+    def f64(): C => E = null
+    def f65(): C => F = null
+    def f66(): D => A = null
+    def f67(): D => B = null
+    def f68(): D => C = null
+    def f69(): D => D = null
+    def f70(): D => E = null
+    def f71(): D => F = null
+    def f72(): E => A = null
+    def f73(): E => B = null
+    def f74(): E => C = null
+    def f75(): E => D = null
+    def f76(): E => E = null
+    def f77(): E => F = null
+    def f78(): F => A = null
+    def f79(): F => B = null
+    def f80(): F => C = null
+    def f81(): F => D = null
+    def f82(): F => E = null
+    def f83(): F => F = null
+
+    def f84(x: A): A = ???
+    def f85(x: A): B = ???
+    def f86(x: A): C = ???
+    def f87(x: A): D = ???
+    def f88(x: A): E = ???
+    def f89(x: A): F = ???
+    def f90(x: B): A = ???
+    def f91(x: B): B = ???
+    def f92(x: B): C = ???
+    def f93(x: B): D = ???
+    def f94(x: B): E = ???
+    def f95(x: B): F = ???
+    def f96(x: C): A = ???
+    def f97(x: C): B = ???
+    def f98(x: C): C = ???
+    def f99(x: C): D = ???
+    def f100(x: C): E = ???
+    def f101(x: C): F = ???
+    def f102(x: D): A = ???
+    def f103(x: D): B = ???
+    def f104(x: D): C = ???
+    def f105(x: D): D = ???
+    def f106(x: D): E = ???
+    def f107(x: D): F = ???
+    def f108(x: E): A = ???
+    def f109(x: E): B = ???
+    def f110(x: E): C = ???
+    def f111(x: E): D = ???
+    def f112(x: E): E = ???
+    def f113(x: E): F = ???
+    def f114(x: F): A = ???
+    def f115(x: F): B = ???
+    def f116(x: F): C = ???
+    def f117(x: F): D = ???
+    def f118(x: F): E = ???
+    def f119(x: F): F = ???
+
+    object O1 extends Cov[A]
+    object O2 extends Cov[B]
+    object O3 extends Cov[C]
+    object O4 extends Cov[D]
+    object O5 extends Cov[E]
+    object O6 extends Cov[F]
+    object O7 extends Con[A]
+    object O8 extends Con[B]
+    object O9 extends Con[C]
+    object O10 extends Con[D]
+    object O11 extends Con[E]
+    object O12 extends Con[F]
+    object O13 extends Inv[A]
+    object O14 extends Inv[B]
+    object O15 extends Inv[C]
+    object O16 extends Inv[D]
+    object O17 extends Inv[E]
+    object O18 extends Inv[F]
+  }
+}
+
+trait Trait2[-A, +B, C] {
+  // trait Inner[-D <: C, +E >: C, F] {
+  def method[D <: A, E >: B, F]() {
+    def f0(x: A): Unit = ()
+    def f1(x: B): Unit = ()
+    def f2(x: C): Unit = ()
+    def f3(x: D): Unit = ()
+    def f4(x: E): Unit = ()
+    def f5(x: F): Unit = ()
+
+    def f6(): A = ???
+    def f7(): B = ???
+    def f8(): C = ???
+    def f9(): D = ???
+    def f10(): E = ???
+    def f11(): F = ???
+
+    def f12(f: A => A): Unit = ()
+    def f13(f: A => B): Unit = ()
+    def f14(f: A => C): Unit = ()
+    def f15(f: A => D): Unit = ()
+    def f16(f: A => E): Unit = ()
+    def f17(f: A => F): Unit = ()
+    def f18(f: B => A): Unit = ()
+    def f19(f: B => B): Unit = ()
+    def f20(f: B => C): Unit = ()
+    def f21(f: B => D): Unit = ()
+    def f22(f: B => E): Unit = ()
+    def f23(f: B => F): Unit = ()
+    def f24(f: C => A): Unit = ()
+    def f25(f: C => B): Unit = ()
+    def f26(f: C => C): Unit = ()
+    def f27(f: C => D): Unit = ()
+    def f28(f: C => E): Unit = ()
+    def f29(f: C => F): Unit = ()
+    def f30(f: D => A): Unit = ()
+    def f31(f: D => B): Unit = ()
+    def f32(f: D => C): Unit = ()
+    def f33(f: D => D): Unit = ()
+    def f34(f: D => E): Unit = ()
+    def f35(f: D => F): Unit = ()
+    def f36(f: E => A): Unit = ()
+    def f37(f: E => B): Unit = ()
+    def f38(f: E => C): Unit = ()
+    def f39(f: E => D): Unit = ()
+    def f40(f: E => E): Unit = ()
+    def f41(f: E => F): Unit = ()
+    def f42(f: F => A): Unit = ()
+    def f43(f: F => B): Unit = ()
+    def f44(f: F => C): Unit = ()
+    def f45(f: F => D): Unit = ()
+    def f46(f: F => E): Unit = ()
+    def f47(f: F => F): Unit = ()
+
+    def f48(): A => A = null
+    def f49(): A => B = null
+    def f50(): A => C = null
+    def f51(): A => D = null
+    def f52(): A => E = null
+    def f53(): A => F = null
+    def f54(): B => A = null
+    def f55(): B => B = null
+    def f56(): B => C = null
+    def f57(): B => D = null
+    def f58(): B => E = null
+    def f59(): B => F = null
+    def f60(): C => A = null
+    def f61(): C => B = null
+    def f62(): C => C = null
+    def f63(): C => D = null
+    def f64(): C => E = null
+    def f65(): C => F = null
+    def f66(): D => A = null
+    def f67(): D => B = null
+    def f68(): D => C = null
+    def f69(): D => D = null
+    def f70(): D => E = null
+    def f71(): D => F = null
+    def f72(): E => A = null
+    def f73(): E => B = null
+    def f74(): E => C = null
+    def f75(): E => D = null
+    def f76(): E => E = null
+    def f77(): E => F = null
+    def f78(): F => A = null
+    def f79(): F => B = null
+    def f80(): F => C = null
+    def f81(): F => D = null
+    def f82(): F => E = null
+    def f83(): F => F = null
+
+    def f84(x: A): A = ???
+    def f85(x: A): B = ???
+    def f86(x: A): C = ???
+    def f87(x: A): D = ???
+    def f88(x: A): E = ???
+    def f89(x: A): F = ???
+    def f90(x: B): A = ???
+    def f91(x: B): B = ???
+    def f92(x: B): C = ???
+    def f93(x: B): D = ???
+    def f94(x: B): E = ???
+    def f95(x: B): F = ???
+    def f96(x: C): A = ???
+    def f97(x: C): B = ???
+    def f98(x: C): C = ???
+    def f99(x: C): D = ???
+    def f100(x: C): E = ???
+    def f101(x: C): F = ???
+    def f102(x: D): A = ???
+    def f103(x: D): B = ???
+    def f104(x: D): C = ???
+    def f105(x: D): D = ???
+    def f106(x: D): E = ???
+    def f107(x: D): F = ???
+    def f108(x: E): A = ???
+    def f109(x: E): B = ???
+    def f110(x: E): C = ???
+    def f111(x: E): D = ???
+    def f112(x: E): E = ???
+    def f113(x: E): F = ???
+    def f114(x: F): A = ???
+    def f115(x: F): B = ???
+    def f116(x: F): C = ???
+    def f117(x: F): D = ???
+    def f118(x: F): E = ???
+    def f119(x: F): F = ???
+
+    object O1 extends Cov[A]
+    object O2 extends Cov[B]
+    object O3 extends Cov[C]
+    object O4 extends Cov[D]
+    object O5 extends Cov[E]
+    object O6 extends Cov[F]
+    object O7 extends Con[A]
+    object O8 extends Con[B]
+    object O9 extends Con[C]
+    object O10 extends Con[D]
+    object O11 extends Con[E]
+    object O12 extends Con[F]
+    object O13 extends Inv[A]
+    object O14 extends Inv[B]
+    object O15 extends Inv[C]
+    object O16 extends Inv[D]
+    object O17 extends Inv[E]
+    object O18 extends Inv[F]
+
+    ()
+  }
+}
diff --git a/test/files/pos/variances-flip.scala b/test/files/pos/variances-flip.scala
new file mode 100644
index 0000000000..c3ea7b571d
--- /dev/null
+++ b/test/files/pos/variances-flip.scala
@@ -0,0 +1,7 @@
+trait Foo[-A, +B, -C, +D] {
+  private[this] def b: B = ???
+  private[this] def d: D = ???
+
+  def f(p1: B => A, p2: D => C) = g(p1(b), p2(d))
+  def g(x: A, y: C) = ((b, d))
+}
diff --git a/test/files/pos/variances-local.scala b/test/files/pos/variances-local.scala
new file mode 100644
index 0000000000..35e395095c
--- /dev/null
+++ b/test/files/pos/variances-local.scala
@@ -0,0 +1,7 @@
+class Foo1[+T] {
+  private[this] type MyType = T
+}
+
+class Foo2[+T] {
+  protected[this] type MyType = T
+}
diff --git a/test/pending/neg/t5378.scala b/test/pending/neg/t5378.scala
deleted file mode 100644
index cada29b0a0..0000000000
--- a/test/pending/neg/t5378.scala
+++ /dev/null
@@ -1,19 +0,0 @@
-import language.reflectiveCalls
-
-class Coll[+T] {
-  def contains = new { def apply[T1 <: T](value: T1) = ??? }
-}
-
-object Test {
-  def main(args: Array[String]): Unit = {
-    val xs = new Coll[List[String]]
-    val ys: Coll[Traversable[String]] = xs
-    
-    println(ys contains Nil)
-    // java.lang.NoSuchMethodException: Coll$$anon$1.apply(scala.collection.Traversable)
-    //  at java.lang.Class.getMethod(Class.java:1605)
-    //  at Test$.reflMethod$Method1(a.scala:14)
-    //  at Test$.main(a.scala:14)
-    //  at Test.main(a.scala)
-  }
-}