diff --git a/src/dotty/tools/dotc/core/SymDenotations.scala b/src/dotty/tools/dotc/core/SymDenotations.scala
index 9801cb629dc7..592a4ff45f6f 100644
--- a/src/dotty/tools/dotc/core/SymDenotations.scala
+++ b/src/dotty/tools/dotc/core/SymDenotations.scala
@@ -432,7 +432,7 @@ object SymDenotations {
     final def isSetter(implicit ctx: Context) =
       (this is Accessor) &&
       originalName.isSetterName &&
-      info.firstParamTypes.nonEmpty // to avoid being fooled by   var x_= : Unit = ...
+      (!isCompleted || info.firstParamTypes.nonEmpty) // to avoid being fooled by   var x_= : Unit = ...
 
     /** is this the constructor of a class? */
     final def isClassConstructor = name == nme.CONSTRUCTOR
diff --git a/src/dotty/tools/dotc/core/TypeApplications.scala b/src/dotty/tools/dotc/core/TypeApplications.scala
index 3beb680d9c92..d00b018c85d1 100644
--- a/src/dotty/tools/dotc/core/TypeApplications.scala
+++ b/src/dotty/tools/dotc/core/TypeApplications.scala
@@ -293,8 +293,9 @@ class TypeApplications(val self: Type) extends AnyVal {
   /** If this is an encoding of a (partially) applied type, return its arguments,
    *  otherwise return Nil.
    *  Existential types in arguments are returned as TypeBounds instances.
+   *  @param interpolate   See argInfo
    */
-  final def argInfos(implicit ctx: Context): List[Type] = {
+  final def argInfos(interpolate: Boolean)(implicit ctx: Context): List[Type] = {
     var tparams: List[TypeSymbol] = null
     def recur(tp: Type, refineCount: Int): mutable.ListBuffer[Type] = tp.stripTypeVar match {
       case tp @ RefinedType(tycon, name) =>
@@ -304,7 +305,7 @@ class TypeApplications(val self: Type) extends AnyVal {
           if (tparams == null) tparams = tycon.typeParams
           if (buf.size < tparams.length) {
             val tparam = tparams(buf.size)
-            if (name == tparam.name) buf += tp.refinedInfo.argInfo(tparam)
+            if (name == tparam.name) buf += tp.refinedInfo.argInfo(tparam, interpolate)
             else null
           } else null
         }
@@ -316,6 +317,8 @@ class TypeApplications(val self: Type) extends AnyVal {
     if (buf == null) Nil else buf.toList
   }
 
+  final def argInfos(implicit ctx: Context): List[Type] = argInfos(interpolate = true)
+
   /** Argument types where existential types in arguments are disallowed */
   def argTypes(implicit ctx: Context) = argInfos mapConserve noBounds
 
@@ -338,16 +341,27 @@ class TypeApplications(val self: Type) extends AnyVal {
 
   /** If this is the image of a type argument to type parameter `tparam`,
    *  recover the type argument, otherwise NoType.
+   *  @param interpolate   If true, replace type bounds as arguments corresponding to
+   *                       variant type parameters by their dominating element. I.e. an argument
+   *
+   *                           T <: U
+   *
+   *                       for a covariant type-parameter becomes U, and an argument
+   *
+   *                           T >: L
+   *
+   *                       for a contravariant type-parameter becomes L.
    */
-  final def argInfo(tparam: Symbol)(implicit ctx: Context): Type = self match {
+  final def argInfo(tparam: Symbol, interpolate: Boolean = true)(implicit ctx: Context): Type = self match {
     case TypeBounds(lo, hi) =>
       if (lo eq hi) hi
-      else {
+      else if (interpolate) {
         val v = tparam.variance
         if (v > 0 && (lo isRef defn.NothingClass)) hi
         else if (v < 0 && (hi isRef defn.AnyClass)) lo
-        else self // it's wildcard type; return its bounds
+        else self
       }
+      else self
     case _ =>
       NoType
   }
diff --git a/src/dotty/tools/dotc/core/TypeComparer.scala b/src/dotty/tools/dotc/core/TypeComparer.scala
index 52abc99a3bfc..2140f9bfe3a7 100644
--- a/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -307,6 +307,11 @@ class TypeComparer(initctx: Context) extends DotClass {
     }
   }
 
+  private def narrowRefined(tp: Type): Type = tp match {
+    case tp: RefinedType => RefinedThis(tp)
+    case _ => tp
+  }
+
   /** If the prefix of a named type is `this` (i.e. an instance of type
    *  `ThisType` or `RefinedThis`), and there is a refinement type R that
    *  "refines" (transitively contains as its parent) a class reference
@@ -650,52 +655,54 @@ class TypeComparer(initctx: Context) extends DotClass {
       }
       compareNamed
     case tp2 @ RefinedType(parent2, name2) =>
+        def qualifies(m: SingleDenotation) = isSubType(m.info, tp2.refinedInfo)
+        def memberMatches(mbr: Denotation): Boolean = mbr match { // inlined hasAltWith for performance
+          case mbr: SingleDenotation => qualifies(mbr)
+          case _ => mbr hasAltWith qualifies
+        }
+      def compareRefinedSlow: Boolean = {
+        def hasMatchingMember(name: Name): Boolean = /*>|>*/ ctx.traceIndented(s"hasMatchingMember($name) ${tp1.member(name).info.show}", subtyping) /*<|<*/ {
+          val tp1r = rebaseQual(tp1, name)
+          (memberMatches(narrowRefined(tp1r) member name)
+            ||
+            { // special case for situations like:
+              //    foo <: C { type T = foo.T }
+              tp2.refinedInfo match {
+                case TypeBounds(lo, hi) if lo eq hi =>
+                  !ctx.phase.erasedTypes && (tp1r select name) =:= lo
+                case _ => false
+              }
+            })
+        }
+        val matchesParent = {
+          val saved = pendingRefinedBases
+          try {
+            addPendingName(name2, tp2, tp2)
+            isSubType(tp1, parent2)
+          } finally pendingRefinedBases = saved
+        }
+        (matchesParent && (
+          name2 == nme.WILDCARD
+          || hasMatchingMember(name2)
+          || fourthTry(tp1, tp2))
+          || needsEtaLift(tp1, tp2) && tp1.testLifted(tp2.typeParams, isSubType(_, tp2)))
+      }
       def compareRefined: Boolean = tp1.widen match {
         case tp1 @ RefinedType(parent1, name1) if name1 == name2 && name1.isTypeName =>
-          // optimized case; all info on tp1.name1 is in refinement tp1.refinedInfo.
-          isSubType(normalizedInfo(tp1), tp2.refinedInfo) && {
-            val saved = pendingRefinedBases
-            try {
-              addPendingName(name1, tp1, tp2)
-              isSubType(parent1, parent2)
-            }
-            finally pendingRefinedBases = saved
+          normalizedInfo(tp1) match {
+            case bounds1 @ TypeBounds(lo1, hi1) if lo1 eq hi1 =>
+              isSubType(bounds1, tp2.refinedInfo) && {
+                val saved = pendingRefinedBases
+                try {
+                  addPendingName(name1, tp1, tp2)
+                  isSubType(parent1, parent2)
+                } finally pendingRefinedBases = saved
+              }
+            case _ =>
+              compareRefinedSlow
           }
         case _ =>
-          def qualifies(m: SingleDenotation) = isSubType(m.info, tp2.refinedInfo)
-          def memberMatches(mbr: Denotation): Boolean = mbr match { // inlined hasAltWith for performance
-            case mbr: SingleDenotation => qualifies(mbr)
-            case _ => mbr hasAltWith qualifies
-          }
-          def hasMatchingMember(name: Name): Boolean = /*>|>*/ ctx.traceIndented(s"hasMatchingMember($name) ${tp1.member(name).info.show}", subtyping) /*<|<*/ {
-            val tp1r = rebaseQual(tp1, name)
-            (  memberMatches(tp1r member name)
-            ||
-               { // special case for situations like:
-                 //    foo <: C { type T = foo.T }
-                 tp2.refinedInfo match {
-                   case TypeBounds(lo, hi) if lo eq hi =>
-                     !ctx.phase.erasedTypes && (tp1r select name) =:= lo
-                   case _ => false
-                 }
-               }
-            )
-          }
-          val matchesParent = {
-            val saved = pendingRefinedBases
-            try {
-              addPendingName(name2, tp2, tp2)
-              isSubType(tp1, parent2)
-            }
-            finally pendingRefinedBases = saved
-          }
-          (  matchesParent && (
-                name2 == nme.WILDCARD
-             || hasMatchingMember(name2)
-             || fourthTry(tp1, tp2)
-             )
-          || needsEtaLift(tp1, tp2) && tp1.testLifted(tp2.typeParams, isSubType(_, tp2))
-          )
+          compareRefinedSlow
       }
       compareRefined
     case OrType(tp21, tp22) =>
diff --git a/src/dotty/tools/dotc/core/TypeOps.scala b/src/dotty/tools/dotc/core/TypeOps.scala
index 7a853ae12c95..7b76feb4d186 100644
--- a/src/dotty/tools/dotc/core/TypeOps.scala
+++ b/src/dotty/tools/dotc/core/TypeOps.scala
@@ -7,12 +7,14 @@ import config.Printers._
 import Decorators._
 import StdNames._
 import util.SimpleMap
+import collection.mutable
+import ast.tpd._
 
 trait TypeOps { this: Context =>
 
   final def asSeenFrom(tp: Type, pre: Type, cls: Symbol, theMap: AsSeenFromMap): Type = {
 
-    def toPrefix(pre: Type, cls: Symbol, thiscls: ClassSymbol): Type = /*>|>*/ ctx.debugTraceIndented(s"toPrefix($pre, $cls, $thiscls)") /*<|<*/ {
+    def toPrefix(pre: Type, cls: Symbol, thiscls: ClassSymbol): Type = /*>|>*/ ctx.conditionalTraceIndented(TypeOps.track, s"toPrefix($pre, $cls, $thiscls)") /*<|<*/ {
       if ((pre eq NoType) || (pre eq NoPrefix) || (cls is PackageClass))
         tp
       else if (thiscls.derivesFrom(cls) && pre.baseTypeRef(thiscls).exists)
@@ -24,7 +26,7 @@ trait TypeOps { this: Context =>
         toPrefix(pre.baseTypeRef(cls).normalizedPrefix, cls.owner, thiscls)
     }
 
-    /*>|>*/ ctx.conditionalTraceIndented(TypeOps.track , s"asSeen ${tp.show} from (${pre.show}, ${cls.show})", show = true) /*<|<*/ { // !!! DEBUG
+    /*>|>*/ ctx.conditionalTraceIndented(TypeOps.track, s"asSeen ${tp.show} from (${pre.show}, ${cls.show})", show = true) /*<|<*/ { // !!! DEBUG
       tp match {
         case tp: NamedType =>
           val sym = tp.symbol
@@ -56,7 +58,13 @@ trait TypeOps { this: Context =>
   final def simplify(tp: Type, theMap: SimplifyMap): Type = tp match {
     case tp: NamedType =>
       if (tp.symbol.isStatic) tp
-      else tp.derivedSelect(simplify(tp.prefix, theMap))
+      else tp.derivedSelect(simplify(tp.prefix, theMap)) match {
+        case tp1: NamedType if tp1.denotationIsCurrent =>
+          val tp2 = tp1.reduceProjection
+          //if (tp2 ne tp1) println(i"simplified $tp1 -> $tp2")
+          tp2
+        case tp1 => tp1
+      }
     case tp: PolyParam =>
       typerState.constraint.typeVarOfParam(tp) orElse tp
     case  _: ThisType | _: BoundType | NoPrefix =>
@@ -301,6 +309,40 @@ trait TypeOps { this: Context =>
     parentRefs
   }
 
+  /** An argument bounds violation is a triple consisting of
+   *   - the argument tree
+   *   - a string "upper" or "lower" indicating which bound is violated
+   *   - the violated bound
+   */
+  type BoundsViolation = (Tree, String, Type)
+
+  /** The list of violations where arguments are not within bounds.
+   *  @param  args          The arguments
+   *  @param  boundss       The list of type bounds
+   *  @param  instantiate   A function that maps a bound type and the list of argument types to a resulting type.
+   *                        Needed to handle bounds that refer to other bounds.
+   */
+  def boundsViolations(args: List[Tree], boundss: List[TypeBounds], instantiate: (Type, List[Type]) => Type)(implicit ctx: Context): List[BoundsViolation] = {
+    val argTypes = args.tpes
+    val violations = new mutable.ListBuffer[BoundsViolation]
+    for ((arg, bounds) <- args zip boundss) {
+      def checkOverlapsBounds(lo: Type, hi: Type): Unit = {
+        //println(i"instantiating ${bounds.hi} with $argTypes")
+        //println(i" = ${instantiate(bounds.hi, argTypes)}")
+        val hiBound = instantiate(bounds.hi, argTypes.mapConserve(_.bounds.hi))
+          // Note that argTypes can contain a TypeBounds type for arguments that are
+          // not fully determined. In that case we need to check against the hi bound of the argument.
+        if (!(lo <:< hiBound)) violations += ((arg, "upper", hiBound))
+        if (!(bounds.lo <:< hi)) violations += ((arg, "lower", bounds.lo))
+      }
+      arg.tpe match {
+        case TypeBounds(lo, hi) => checkOverlapsBounds(lo, hi)
+        case tp => checkOverlapsBounds(tp, tp)
+      }
+    }
+    violations.toList
+  }
+
   /** Is `feature` enabled in class `owner`?
    *  This is the case if one of the following two alternatives holds:
    *
diff --git a/src/dotty/tools/dotc/core/Types.scala b/src/dotty/tools/dotc/core/Types.scala
index 2997e9e779a6..feee05d868e6 100644
--- a/src/dotty/tools/dotc/core/Types.scala
+++ b/src/dotty/tools/dotc/core/Types.scala
@@ -104,9 +104,10 @@ object Types {
      */
     def isRef(sym: Symbol)(implicit ctx: Context): Boolean = stripTypeVar match {
       case this1: TypeRef =>
-        val thissym = this1.symbol
-        if (thissym.isAliasType) this1.info.bounds.hi.isRef(sym)
-        else thissym eq sym
+        this1.info match { // see comment in Namers/typeDefSig
+          case TypeBounds(lo, hi) if lo eq hi => hi.isRef(sym)
+          case _ =>  this1.symbol eq sym
+        }
       case this1: RefinedType =>
         // make sure all refinements are type arguments
         this1.parent.isRef(sym) && this.argInfos.nonEmpty
@@ -719,10 +720,13 @@ object Types {
       case _ => Nil
     }
 
-    /** A prefix-less termRef to a new skolem symbol that has the given type as info */
-    def narrow(implicit ctx: Context): TermRef = TermRef(NoPrefix, ctx.newSkolem(this))
+    /** A prefix-less refined this or a termRef to a new skolem symbol
+     *  that has the given type as info
+     */
+    def narrow(implicit ctx: Context): TermRef =
+      TermRef(NoPrefix, ctx.newSkolem(this))
 
- // ----- Normalizing typerefs over refined types ----------------------------
+    // ----- Normalizing typerefs over refined types ----------------------------
 
     /** If this is a refinement type that has a refinement for `name` (which might be followed
      *  by other refinements), and the refined info is a type alias, return the alias,
@@ -733,58 +737,58 @@ object Types {
      *  to just U. Does not perform the reduction if the resulting type would contain
      *  a reference to the "this" of the current refined type.
      */
-    def lookupRefined(name: Name)(implicit ctx: Context): Type = stripTypeVar match {
-      case pre: RefinedType =>
-        def dependsOnThis(tp: Type): Boolean = tp match {
-          case tp @ TypeRef(RefinedThis(rt), _) if rt refines pre =>
-            tp.info match {
-              case TypeBounds(lo, hi) if lo eq hi => dependsOnThis(hi)
-              case _ => true
-            }
-          case RefinedThis(rt) =>
-            rt refines pre
-          case _ => false
-        }
-        if (pre.refinedName ne name)
-          pre.parent.lookupRefined(name)
-        else pre.refinedInfo match {
-          case TypeBounds(lo, hi) if lo eq hi =>
-            if (hi.existsPart(dependsOnThis)) NoType else hi
-          case _ => NoType
-        }
-      case RefinedThis(rt) =>
-        rt.lookupRefined(name)
-      case pre: WildcardType =>
-        WildcardType
-      case _ =>
-        NoType
+    def lookupRefined(name: Name)(implicit ctx: Context): Type = {
+
+      def dependsOnRefinedThis(tp: Type): Boolean = tp.stripTypeVar match {
+        case tp @ TypeRef(RefinedThis(rt), _) if rt refines this =>
+          tp.info match {
+            case TypeBounds(lo, hi) if lo eq hi => dependsOnRefinedThis(hi)
+            case _ => true
+          }
+        case RefinedThis(rt) => rt refines this
+        case tp: NamedType =>
+          !tp.symbol.isStatic && dependsOnRefinedThis(tp.prefix)
+        case tp: RefinedType => dependsOnRefinedThis(tp.refinedInfo) || dependsOnRefinedThis(tp.parent)
+        case tp: TypeBounds => dependsOnRefinedThis(tp.lo) || dependsOnRefinedThis(tp.hi)
+        case tp: AnnotatedType => dependsOnRefinedThis(tp.underlying)
+        case tp: AndOrType => dependsOnRefinedThis(tp.tp1) || dependsOnRefinedThis(tp.tp2)
+        case _ => false
+      }
+
+      def loop(pre: Type): Type = pre.stripTypeVar match {
+        case pre: RefinedType =>
+          if (pre.refinedName ne name) loop(pre.parent)
+          else this.member(name).info match {
+            case TypeBounds(lo, hi) if (lo eq hi) && !dependsOnRefinedThis(hi) => hi
+            case _ => NoType
+          }
+        case RefinedThis(rt) =>
+          rt.lookupRefined(name)
+        case pre: WildcardType =>
+          WildcardType
+        case _ =>
+          NoType
+      }
+
+      loop(this)
     }
 
     /** The type <this . name> , reduced if possible */
     def select(name: Name)(implicit ctx: Context): Type = name match {
-      case name: TermName =>
-        TermRef.all(this, name)
-      case name: TypeName =>
-        val res = lookupRefined(name)
-        if (res.exists) res else TypeRef(this, name)
+      case name: TermName => TermRef.all(this, name)
+      case name: TypeName => TypeRef(this, name).reduceProjection
     }
 
     /** The type <this . name> , reduced if possible, with given denotation if unreduced */
     def select(name: Name, denot: Denotation)(implicit ctx: Context): Type = name match {
-      case name: TermName =>
-        TermRef(this, name, denot)
-      case name: TypeName =>
-        val res = lookupRefined(name)
-        if (res.exists) res else TypeRef(this, name, denot)
+      case name: TermName => TermRef(this, name, denot)
+      case name: TypeName => TypeRef(this, name, denot).reduceProjection
     }
 
     /** The type <this . name> with given symbol, reduced if possible */
     def select(sym: Symbol)(implicit ctx: Context): Type =
       if (sym.isTerm) TermRef(this, sym.asTerm)
-      else {
-        val res = lookupRefined(sym.name)
-        if (res.exists) res else TypeRef(this, sym.asType)
-      }
+      else TypeRef(this, sym.asType).reduceProjection
 
 // ----- Access to parts --------------------------------------------
 
@@ -1309,6 +1313,18 @@ object Types {
       if (name.isInheritedName) prefix.nonPrivateMember(name.revertInherited)
       else prefix.member(name)
 
+    /** (1) Reduce a type-ref `W # X` or `W { ... } # U`, where `W` is a wildcard type
+     *  to an (unbounded) wildcard type.
+     *
+     *  (2) Reduce a type-ref `T { X = U; ... } # X`  to   `U`
+     *  provided `U` does not refer with a RefinedThis to the
+     *  refinement type `T { X = U; ... }`
+     */
+    def reduceProjection(implicit ctx: Context): Type = {
+      val reduced = prefix.lookupRefined(name)
+      if (reduced.exists) reduced else this
+    }
+
     def symbol(implicit ctx: Context): Symbol = {
       val now = ctx.period
       if (checkedPeriod == now ||
@@ -2130,7 +2146,7 @@ object Types {
 
   case class RefinedThis(binder: RefinedType) extends BoundType with SingletonType {
     type BT = RefinedType
-    override def underlying(implicit ctx: Context) = binder.parent
+    override def underlying(implicit ctx: Context) = binder
     def copyBoundType(bt: BT) = RefinedThis(bt)
 
     // need to customize hashCode and equals to prevent infinite recursion for
diff --git a/src/dotty/tools/dotc/printing/PlainPrinter.scala b/src/dotty/tools/dotc/printing/PlainPrinter.scala
index 809f29924088..e58775b65821 100644
--- a/src/dotty/tools/dotc/printing/PlainPrinter.scala
+++ b/src/dotty/tools/dotc/printing/PlainPrinter.scala
@@ -144,9 +144,13 @@ class PlainPrinter(_ctx: Context) extends Printer {
       case tp: TypeVar =>
         if (tp.isInstantiated)
           toTextLocal(tp.instanceOpt) ~ "'" // debug for now, so that we can see where the TypeVars are.
-        else
-          "(" ~ toText(tp.origin) ~ "?" ~
-          toText(ctx.typerState.constraint.bounds(tp.origin)) ~ ")"
+        else {
+          val bounds = ctx.typerState.constraint.at(tp.origin) match {
+            case bounds: TypeBounds => bounds
+            case _ => TypeBounds.empty
+          }
+          "(" ~ toText(tp.origin) ~ "?" ~ toText(bounds) ~ ")"
+        }
       case _ =>
         tp.fallbackToText(this)
     }
diff --git a/src/dotty/tools/dotc/printing/RefinedPrinter.scala b/src/dotty/tools/dotc/printing/RefinedPrinter.scala
index 12ac03bd0068..a5f1c07fdd33 100644
--- a/src/dotty/tools/dotc/printing/RefinedPrinter.scala
+++ b/src/dotty/tools/dotc/printing/RefinedPrinter.scala
@@ -97,7 +97,7 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
       }
     tp match {
       case tp: RefinedType =>
-        val args = tp.argInfos
+        val args = tp.argInfos(interpolate = false)
         if (args.nonEmpty) {
           val tycon = tp.unrefine
           val cls = tycon.typeSymbol
diff --git a/src/dotty/tools/dotc/transform/FirstTransform.scala b/src/dotty/tools/dotc/transform/FirstTransform.scala
index 29cef09fe97c..42ace148a55e 100644
--- a/src/dotty/tools/dotc/transform/FirstTransform.scala
+++ b/src/dotty/tools/dotc/transform/FirstTransform.scala
@@ -139,8 +139,9 @@ class FirstTransform extends MiniPhaseTransform with IdentityDenotTransformer wi
     case tree: NamedArg => transform(tree.arg)
     case AppliedTypeTree(tycon, args) =>
       val tparams = tycon.tpe.typeSymbol.typeParams
-      Checking.checkBounds(
-        args, tparams.map(_.info.bounds), (tp, argTypes) => tp.substDealias(tparams, argTypes))
+      val bounds = tparams.map(tparam =>
+        tparam.info.asSeenFrom(tycon.tpe.normalizedPrefix, tparam.owner.owner).bounds)
+      Checking.checkBounds(args, bounds, _.substDealias(tparams, _))
       normalizeType(tree)
     case tree =>
       normalizeType(tree)
diff --git a/src/dotty/tools/dotc/typer/Applications.scala b/src/dotty/tools/dotc/typer/Applications.scala
index 9b2e64f356f0..ba770cf2c173 100644
--- a/src/dotty/tools/dotc/typer/Applications.scala
+++ b/src/dotty/tools/dotc/typer/Applications.scala
@@ -593,7 +593,7 @@ trait Applications extends Compatibility { self: Typer =>
           else tree
         if (typedArgs.length <= pt.paramBounds.length)
           typedArgs = typedArgs.zipWithConserve(pt.paramBounds)(adaptTypeArg)
-        checkBounds(typedArgs, pt, tree.pos)
+        checkBounds(typedArgs, pt)
       case _ =>
     }
     assignType(cpy.TypeApply(tree)(typedFn, typedArgs), typedFn, typedArgs)
diff --git a/src/dotty/tools/dotc/typer/Checking.scala b/src/dotty/tools/dotc/typer/Checking.scala
index 982b97f7e243..17cba13737a2 100644
--- a/src/dotty/tools/dotc/typer/Checking.scala
+++ b/src/dotty/tools/dotc/typer/Checking.scala
@@ -33,27 +33,11 @@ object Checking {
   /** A general checkBounds method that can be used for TypeApply nodes as
    *  well as for AppliedTypeTree nodes.
    */
-  def checkBounds(args: List[tpd.Tree], bounds: List[TypeBounds], instantiate: (Type, List[Type]) => Type)(implicit ctx: Context) = {
-    val argTypes = args.tpes
-    for ((arg, bounds) <- args zip bounds) {
-      def notConforms(which: String, bound: Type) = {
-        ctx.error(
+  def checkBounds(args: List[tpd.Tree], boundss: List[TypeBounds], instantiate: (Type, List[Type]) => Type)(implicit ctx: Context) =
+    for ((arg, which, bound) <- ctx.boundsViolations(args, boundss, instantiate))
+      ctx.error(
           d"Type argument ${arg.tpe} does not conform to $which bound $bound ${err.whyNoMatchStr(arg.tpe, bound)}",
           arg.pos)
-      }
-      def checkOverlapsBounds(lo: Type, hi: Type): Unit = {
-        //println(i"instantiating ${bounds.hi} with $argTypes")
-        //println(i" = ${instantiate(bounds.hi, argTypes)}")
-        val hiBound = instantiate(bounds.hi, argTypes)
-        if (!(lo <:< hiBound)) notConforms("upper", hiBound)
-        if (!(bounds.lo <:< hi)) notConforms("lower", bounds.lo)
-      }
-      arg.tpe match {
-        case TypeBounds(lo, hi) => checkOverlapsBounds(lo, hi)
-        case tp => checkOverlapsBounds(tp, tp)
-      }
-    }
-  }
 
   /** A type map which checks that the only cycles in a type are F-bounds
    *  and that protects all F-bounded references by LazyRefs.
@@ -168,6 +152,58 @@ object Checking {
         else info
     }
   }
+
+  /** Check that refinement satisfies the following two conditions
+   *  1. No part of it refers to a symbol that's defined in the same refinement
+   *     at a textually later point.
+   *  2. All references to the refinement itself via `this` are followed by
+   *     selections.
+   *  Note: It's not yet clear what exactly we want to allow and what we want to rule out.
+   *  This depends also on firming up the DOT calculus. For the moment we only issue
+   *  deprecated warnings, not errors.
+   */
+  def checkRefinementNonCyclic(refinement: Tree, refineCls: ClassSymbol)(implicit ctx: Context): Unit = {
+    def flag(what: String, tree: Tree) =
+      ctx.deprecationWarning(i"$what reference in refinement is deprecated", tree.pos)
+    def forwardRef(tree: Tree) = flag("forward", tree)
+    def selfRef(tree: Tree) = flag("self", tree)
+    val checkTree = new TreeAccumulator[Unit] {
+      private var seen = Set[Symbol]()
+      def checkRef(tree: Tree, sym: Symbol) =
+        if (sym.maybeOwner == refineCls && !seen(sym)) forwardRef(tree)
+      def apply(x: Unit, tree: Tree) = tree match {
+        case tree: MemberDef =>
+          foldOver(x, tree)
+          seen += tree.symbol
+        case tree @ Select(This(_), _) =>
+          checkRef(tree, tree.symbol)
+        case tree: RefTree =>
+          checkRef(tree, tree.symbol)
+          foldOver(x, tree)
+        case tree: This =>
+          selfRef(tree)
+        case tree: TypeTree =>
+          val checkType = new TypeAccumulator[Unit] {
+            def apply(x: Unit, tp: Type): Unit = tp match {
+              case tp: NamedType =>
+                checkRef(tree, tp.symbol)
+                tp.prefix match {
+                  case pre: ThisType =>
+                  case pre => foldOver(x, pre)
+                }
+              case tp: ThisType if tp.cls == refineCls =>
+                selfRef(tree)
+              case _ =>
+                foldOver(x, tp)
+            }
+          }
+          checkType((), tree.tpe)
+        case _ =>
+          foldOver(x, tree)
+      }
+    }
+    checkTree((), refinement)
+  }
 }
 
 trait Checking {
@@ -192,10 +228,9 @@ trait Checking {
   /** Check that type arguments `args` conform to corresponding bounds in `poly`
    *  Note: This does not check the bounds of AppliedTypeTrees. These
    *  are handled by method checkBounds in FirstTransform
-   *  TODO: remove pos parameter
    */
-  def checkBounds(args: List[tpd.Tree], poly: PolyType, pos: Position)(implicit ctx: Context): Unit =    Checking.checkBounds(
-      args, poly.paramBounds, (tp, argTypes) => tp.substParams(poly, argTypes))
+  def checkBounds(args: List[tpd.Tree], poly: PolyType)(implicit ctx: Context): Unit =
+    Checking.checkBounds(args, poly.paramBounds, _.substParams(poly, _))
 
   /** Check that type `tp` is stable. */
   def checkStable(tp: Type, pos: Position)(implicit ctx: Context): Unit =
@@ -292,7 +327,7 @@ trait NoChecking extends Checking {
   import tpd._
   override def checkNonCyclic(sym: Symbol, info: TypeBounds, reportErrors: Boolean)(implicit ctx: Context): Type = info
   override def checkValue(tree: Tree, proto: Type)(implicit ctx: Context): tree.type = tree
-  override def checkBounds(args: List[tpd.Tree], poly: PolyType, pos: Position)(implicit ctx: Context): Unit = ()
+  override def checkBounds(args: List[tpd.Tree], poly: PolyType)(implicit ctx: Context): Unit = ()
   override def checkStable(tp: Type, pos: Position)(implicit ctx: Context): Unit = ()
   override def checkLegalPrefix(tp: Type, selector: Name, pos: Position)(implicit ctx: Context): Unit = ()
   override def checkClassTypeWithStablePrefix(tp: Type, pos: Position, traitReq: Boolean)(implicit ctx: Context): Type = tp
diff --git a/src/dotty/tools/dotc/typer/Namer.scala b/src/dotty/tools/dotc/typer/Namer.scala
index bc64e10fc78b..86376356c742 100644
--- a/src/dotty/tools/dotc/typer/Namer.scala
+++ b/src/dotty/tools/dotc/typer/Namer.scala
@@ -673,7 +673,17 @@ class Namer { typer: Typer =>
 
   def typeDefSig(tdef: TypeDef, sym: Symbol)(implicit ctx: Context): Type = {
     completeParams(tdef.tparams)
-    sym.info = TypeBounds.empty // avoid cyclic reference errors for F-bounds
+    sym.info = TypeBounds.empty
+      // Temporarily set info of defined type T to ` >: Nothing <: Any.
+      // This is done to avoid cyclic reference errors for F-bounds.
+      // This is subtle: `sym` has now an empty TypeBounds, but is not automatically
+      // made an abstract type. If it had been made an abstract type, it would count as an
+      // abstract type of its enclosing class, which might make that class an invalid
+      // prefix. I verified this would lead to an error when compiling io.ClassPath.
+      // A distilled version is in pos/prefix.scala.
+      //
+      // The scheme critically relies on an implementation detail of isRef, which
+      // inspects a TypeRef's info, instead of simply dealiasing alias types.
     val tparamSyms = tdef.tparams map symbolOfTree
     val isDerived = tdef.rhs.isInstanceOf[untpd.DerivedTypeTree]
     val toParameterize = tparamSyms.nonEmpty && !isDerived
diff --git a/src/dotty/tools/dotc/typer/Typer.scala b/src/dotty/tools/dotc/typer/Typer.scala
index 4bb6e172b065..9ef73f0b6d62 100644
--- a/src/dotty/tools/dotc/typer/Typer.scala
+++ b/src/dotty/tools/dotc/typer/Typer.scala
@@ -20,6 +20,7 @@ import NameOps._
 import Flags._
 import Decorators._
 import ErrorReporting._
+import Checking._
 import EtaExpansion.etaExpand
 import dotty.tools.dotc.transform.Erasure.Boxing
 import util.Positions._
@@ -761,14 +762,7 @@ class Typer extends Namer with TypeAssigner with Applications with Implicits wit
     assert(tree.refinements.length == refinements1.length, s"${tree.refinements} != $refinements1")
     def addRefinement(parent: Type, refinement: Tree): Type = {
       typr.println(s"adding refinement $refinement")
-      def checkRef(tree: Tree, sym: Symbol) =
-        if (sym.maybeOwner == refineCls && tree.pos.start <= sym.pos.end)
-          ctx.error("illegal forward reference in refinement", tree.pos)
-      refinement foreachSubTree {
-        case tree: RefTree => checkRef(tree, tree.symbol)
-        case tree: TypeTree => checkRef(tree, tree.tpe.typeSymbol)
-        case _ =>
-      }
+      checkRefinementNonCyclic(refinement, refineCls)
       val rsym = refinement.symbol
       val rinfo = if (rsym is Accessor) rsym.info.resultType else rsym.info
       RefinedType(parent, rsym.name, rt => rinfo.substThis(refineCls, RefinedThis(rt)))
diff --git a/test/dotc/tests.scala b/test/dotc/tests.scala
index f4aa074de095..1c437e833018 100644
--- a/test/dotc/tests.scala
+++ b/test/dotc/tests.scala
@@ -68,7 +68,7 @@ class tests extends CompilerTest {
   @Test def neg_typedapply() = compileFile(negDir, "typedapply", xerrors = 4)
   @Test def neg_typedidents() = compileFile(negDir, "typedIdents", xerrors = 2)
   @Test def neg_assignments() = compileFile(negDir, "assignments", xerrors = 3)
-  @Test def neg_typers() = compileFile(negDir, "typers", xerrors = 13)
+  @Test def neg_typers() = compileFile(negDir, "typers", xerrors = 12)
   @Test def neg_privates() = compileFile(negDir, "privates", xerrors = 2)
   @Test def neg_rootImports = compileFile(negDir, "rootImplicits", xerrors = 2)
   @Test def neg_templateParents() = compileFile(negDir, "templateParents", xerrors = 3)
@@ -95,9 +95,7 @@ class tests extends CompilerTest {
   @Test def neg_tailcall = compileFile(negDir, "tailcall/tailrec", xerrors = 7)
   @Test def neg_tailcall2 = compileFile(negDir, "tailcall/tailrec-2", xerrors = 2)
   @Test def neg_tailcall3 = compileFile(negDir, "tailcall/tailrec-3", xerrors = 2)
-  @Test def neg_t1048 = compileFile(negDir, "t1048", xerrors = 1)
   @Test def nef_t1279a = compileFile(negDir, "t1279a", xerrors = 1)
-  @Test def neg_t1843 = compileFile(negDir, "t1843", xerrors = 1)
   @Test def neg_t1843_variances = compileFile(negDir, "t1843-variances", xerrors = 1)
   @Test def neg_t2660_ambi = compileFile(negDir, "t2660", xerrors = 2)
   @Test def neg_t2994 = compileFile(negDir, "t2994", xerrors = 2)
@@ -106,14 +104,15 @@ class tests extends CompilerTest {
   @Test def neg_badAuxConstr = compileFile(negDir, "badAuxConstr", xerrors = 2)
   @Test def neg_typetest = compileFile(negDir, "typetest", xerrors = 1)
   @Test def neg_t1569_failedAvoid = compileFile(negDir, "t1569-failedAvoid", xerrors = 1)
-  @Test def neg_cycles = compileFile(negDir, "cycles", xerrors = 6)
+  @Test def neg_cycles = compileFile(negDir, "cycles", xerrors = 8)
+  @Test def neg_boundspropagation = compileFile(negDir, "boundspropagation", xerrors = 4)
 
   @Test def dotc = compileDir(dotcDir + "tools/dotc", twice)(allowDeepSubtypes)
   @Test def dotc_ast = compileDir(dotcDir + "tools/dotc/ast", twice)
   @Test def dotc_config = compileDir(dotcDir + "tools/dotc/config", twice)
   @Test def dotc_core = compileDir(dotcDir + "tools/dotc/core", twice)(allowDeepSubtypes)
   @Test def dotc_core_pickling = compileDir(dotcDir + "tools/dotc/core/pickling", twice)(allowDeepSubtypes)
-  // @Test def dotc_transform = compileDir(dotcDir + "tools/dotc/transform", twice)
+  // @Test def dotc_transform = compileDir(dotcDir + "tools/dotc/transform", twice)(allowDeepSubtypes)
   // @odersky causes race error in ResolveSuper
 
   @Test def dotc_parsing = compileDir(dotcDir + "tools/dotc/parsing", twice)
diff --git a/tests/neg/boundspropagation.scala b/tests/neg/boundspropagation.scala
index 560d5416c17b..42cf67dba385 100644
--- a/tests/neg/boundspropagation.scala
+++ b/tests/neg/boundspropagation.scala
@@ -24,3 +24,21 @@ object test3 {
     case y: Tree[_] => y
   }
 }
+
+// Example contributed by Jason. I believe this should not typecheck,
+// even though scalac does typecheck it.
+object test4 {
+  class Base {
+    type N
+
+    class Tree[-S, -T >: Option[S]]
+
+    def g(x: Any): Tree[_, _ <: Option[N]] = x match {
+      case y: Tree[_, _] => y
+    }
+  }
+}
+
+class Test5 {
+"": ({ type U = this.type })#U
+}
diff --git a/tests/neg/cycles.scala b/tests/neg/cycles.scala
index dbcbe1efbdb6..0dd24c309ebc 100644
--- a/tests/neg/cycles.scala
+++ b/tests/neg/cycles.scala
@@ -27,3 +27,16 @@ class E {
   }
   val x: F#T = ???
 }
+
+class T1 {
+  type X = (U, U) // cycle
+  type U = X & Int
+}
+class T2 {
+  type X = (U, U) // cycle
+  type U = X | Int
+}
+object T12 {
+  ??? : (T1 {})#U
+  ??? : (T2 {})#U
+}
diff --git a/tests/neg/t1048.scala b/tests/neg/t1048.scala
deleted file mode 100644
index 4b8e78b4cd85..000000000000
--- a/tests/neg/t1048.scala
+++ /dev/null
@@ -1,21 +0,0 @@
-trait T[U] {
-  def x: T[_ <: U]
-}
-
-object T {
-  def unapply[U](t: T[U]): Option[T[_ <: U]] = Some(t.x)
-}
-
-object Test {
-  def f[W](t: T[W]) = t match {
-    case T(T(_)) => ()
-// Gives:
-// t1048.scala:11: error: There is no best instantiation of pattern type T[Any']
-// that makes it a subtype of selector type T[_ <: W].
-// Non-variant type variable U cannot be uniquely instantiated.
-//     case T(T(_)) => ()
-//             ^
-// one error found
-  }
-}
-
diff --git a/tests/neg/typers.scala b/tests/neg/typers.scala
index 2f1cf40c4500..226fd2310408 100644
--- a/tests/neg/typers.scala
+++ b/tests/neg/typers.scala
@@ -62,6 +62,6 @@ object typers {
   }
 
   class Refinements {
-    val y: C { val x: T; type T }  // error: illegal forward reference in refinement
+    val y: C { val x: T; type T }  // deprecated warning: illegal forward reference in refinement
   }
 }
diff --git a/tests/disabled/t1048.scala b/tests/pending/pos/t1048.scala
similarity index 100%
rename from tests/disabled/t1048.scala
rename to tests/pending/pos/t1048.scala
diff --git a/tests/neg/t1843.scala b/tests/pending/pos/t1843.scala
similarity index 99%
rename from tests/neg/t1843.scala
rename to tests/pending/pos/t1843.scala
index 8504bf342cef..871b21346cc2 100644
--- a/tests/neg/t1843.scala
+++ b/tests/pending/pos/t1843.scala
@@ -3,7 +3,6 @@
 * ... Or Will It?
 *
 */
-
 object Crash {
   trait UpdateType[A]
   case class StateUpdate[A](updateType : UpdateType[A], value : A)
diff --git a/tests/pos/boundspropagation.scala b/tests/pos/boundspropagation.scala
new file mode 100644
index 000000000000..c2396c2c6ca3
--- /dev/null
+++ b/tests/pos/boundspropagation.scala
@@ -0,0 +1,26 @@
+// test contributed by @retronym
+object test1 {
+  class Base {
+    type N
+
+    class Tree[-T >: N]
+
+    def f(x: Any): Tree[N] = x match {
+      case y: Tree[_] => y
+    }
+  }
+  class Derived extends Base {
+    def g(x: Any): Tree[N] = x match {
+      case y: Tree[_] => y // now succeeds in dotc
+    }
+  }
+}
+object test2 {
+  class Tree[S, T <: S]
+
+  class Base {
+    def g(x: Any): Tree[_, _ <: Int] = x match {
+      case y: Tree[Int @unchecked, _] => y
+    }
+  }
+}
diff --git a/tests/pos/prefix.scala b/tests/pos/prefix.scala
new file mode 100644
index 000000000000..e18eaa50f6b1
--- /dev/null
+++ b/tests/pos/prefix.scala
@@ -0,0 +1,5 @@
+
+abstract class ClassPath {
+  type AnyClassRep = ClassPath#ClassRep
+  type ClassRep
+}
diff --git a/tests/pos/printbounds.scala b/tests/pos/printbounds.scala
new file mode 100644
index 000000000000..7499b85037b0
--- /dev/null
+++ b/tests/pos/printbounds.scala
@@ -0,0 +1,11 @@
+class Tree[-T >: Number]
+
+
+class Test {
+
+  val x: Tree[_] = ???
+
+  val y = x // With -Xprint:front this should print  val x: Tree[_] = x
+            // used to print Tree[Nothing], which is confusing.
+
+}
diff --git a/tests/pos/wildcardBoundInference.scala b/tests/pos/wildcardBoundInference.scala
new file mode 100644
index 000000000000..65553ed93619
--- /dev/null
+++ b/tests/pos/wildcardBoundInference.scala
@@ -0,0 +1,69 @@
+// Tests translated from scalac SI-6189 by @retronym
+
+/*
+public class Exist<T extends String> {
+  // java helpfully re-interprets Exist<?> as Exist<? extends String>
+  public Exist<?> foo() { throw new RuntimeException(); }
+}
+*/
+class Exist[T <: String] {
+  def foo: Exist[_] = null
+}
+
+/*
+public class ExistF<T extends ExistF<T>> {
+  // java helpfully re-interprets ExistF<?> as ExistF<?0 extends ExistF<?0>>
+  public ExistF<?> foo() { throw new RuntimeException(); }
+}
+*/
+
+class ExistF[T <: ExistF[T]] {
+  def foo: ExistF[_] = null
+}
+
+/*
+public class ExistIndir<T extends String, U extends T> {
+  // java helpfully re-interprets ExistIndir<?> as ExistIndir<? extends String>
+  public ExistIndir<?, ?> foo() { throw new RuntimeException(); }
+}
+*/
+
+class ExistIndir[T <: String, U <: T] {
+  def foo: ExistIndir[_, _] = null
+}
+
+class Test {
+  class MyExist extends ExistF[MyExist]
+  // SI-8197, SI-6169: java infers the bounds of existentials, so we have to as well now that SI-1786 is fixed...
+  def stringy: Exist[_ <: String] = (new Exist[String]).foo
+  // def fbounded: (ExistF[t] forSome {type t <: ExistF[t] }) = (new MyExist).foo
+  def indir: ExistIndir[_ <: String, _ <: String] = (new ExistIndir[String, String]).foo
+}
+
+
+/*
+public abstract class OP<T> { }
+public interface Skin<C extends Skinnable> { }
+public interface Skinnable {
+  OP<Skin<?>> skinProperty();
+}
+*/
+class OP[T]
+trait Skin[C <: Skinnable]
+trait Skinnable {
+  def skinProperty: OP[Skin[_]]
+}
+object ObjectProperty {
+  implicit def jfxObjectProperty2sfx[T](p: OP[T]): ObjectProperty[T] = new ObjectProperty[T](p)
+}
+
+class ObjectProperty[T](val delegate: OP[T])
+
+trait TestWildcardBoundInference {
+  def delegate: Skinnable
+  def skin: ObjectProperty[Skin[_ /* inferred: <: Skinnable */]] = ObjectProperty.jfxObjectProperty2sfx(delegate.skinProperty)
+  skin: ObjectProperty[Skin[_  <: Skinnable]]
+
+  def skinCheckInference = delegate.skinProperty
+  skinCheckInference: ObjectProperty[Skin[_  <: Skinnable]]
+}