diff --git a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
index 15f24a7fe50c..81ee865aa96c 100644
--- a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
+++ b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
@@ -362,13 +362,11 @@ trait ConstraintHandling {
       def pruneLambdaParams(tp: Type) =
         if (comparedTypeLambdas.nonEmpty) {
           val approx = new ApproximatingTypeMap {
+            if (fromBelow) variance = -1
             def apply(t: Type): Type = t match {
               case t @ TypeParamRef(tl: TypeLambda, n) if comparedTypeLambdas contains tl =>
-                val effectiveVariance = if (fromBelow) -variance else variance
                 val bounds = tl.paramInfos(n)
-                if (effectiveVariance > 0) bounds.lo
-                else if (effectiveVariance < 0) bounds.hi
-                else NoType
+                range(bounds.lo, bounds.hi)
               case _ =>
                 mapOver(t)
             }
diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala
index 452dc1a03357..62d8d57f6f47 100644
--- a/compiler/src/dotty/tools/dotc/core/Definitions.scala
+++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala
@@ -657,8 +657,6 @@ class Definitions {
   def UncheckedStableAnnot(implicit ctx: Context) = UncheckedStableAnnotType.symbol.asClass
   lazy val UncheckedVarianceAnnotType = ctx.requiredClassRef("scala.annotation.unchecked.uncheckedVariance")
   def UncheckedVarianceAnnot(implicit ctx: Context) = UncheckedVarianceAnnotType.symbol.asClass
-  lazy val UnsafeNonvariantAnnotType = ctx.requiredClassRef("scala.annotation.internal.UnsafeNonvariant")
-  def UnsafeNonvariantAnnot(implicit ctx: Context) = UnsafeNonvariantAnnotType.symbol.asClass
   lazy val VolatileAnnotType = ctx.requiredClassRef("scala.volatile")
   def VolatileAnnot(implicit ctx: Context) = VolatileAnnotType.symbol.asClass
   lazy val FieldMetaAnnotType = ctx.requiredClassRef("scala.annotation.meta.field")
diff --git a/compiler/src/dotty/tools/dotc/core/Denotations.scala b/compiler/src/dotty/tools/dotc/core/Denotations.scala
index 74a9138ca3b8..75d1261c3d44 100644
--- a/compiler/src/dotty/tools/dotc/core/Denotations.scala
+++ b/compiler/src/dotty/tools/dotc/core/Denotations.scala
@@ -1005,7 +1005,7 @@ object Denotations {
         case _ => if (symbol.exists) symbol.owner else NoSymbol
       }
       if (!owner.membersNeedAsSeenFrom(pre)) this
-      else derivedSingleDenotation(symbol, info.asSeenFrom(pre, owner))
+      else derivedSingleDenotation(symbol, symbol.info.asSeenFrom(pre, owner))
     }
 
     private def overlaps(fs: FlagSet)(implicit ctx: Context): Boolean = this match {
diff --git a/compiler/src/dotty/tools/dotc/core/SymDenotations.scala b/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
index bfaa12729090..1b9d57186468 100644
--- a/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
+++ b/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
@@ -1537,22 +1537,22 @@ object SymDenotations {
      *  have existing symbols.
      *  @param inherited  The method is called on a parent class from computeNPMembersNamed
      */
-    final def nonPrivateMembersNamed(name: Name, inherited: Boolean = false)(implicit ctx: Context): PreDenotation = {
+    final def nonPrivateMembersNamed(name: Name)(implicit ctx: Context): PreDenotation = {
       Stats.record("nonPrivateMembersNamed")
       if (Config.cacheMembersNamed) {
         var denots: PreDenotation = memberCache lookup name
         if (denots == null) {
-          denots = computeNPMembersNamed(name, inherited)
+          denots = computeNPMembersNamed(name)
           memberCache.enter(name, denots)
         } else if (Config.checkCacheMembersNamed) {
-          val denots1 = computeNPMembersNamed(name, inherited)
+          val denots1 = computeNPMembersNamed(name)
           assert(denots.exists == denots1.exists, s"cache inconsistency: cached: $denots, computed $denots1, name = $name, owner = $this")
         }
         denots
-      } else computeNPMembersNamed(name, inherited)
+      } else computeNPMembersNamed(name)
     }
 
-    private[core] def computeNPMembersNamed(name: Name, inherited: Boolean)(implicit ctx: Context): PreDenotation = /*>|>*/ Stats.track("computeNPMembersNamed") /*<|<*/ {
+    private[core] def computeNPMembersNamed(name: Name)(implicit ctx: Context): PreDenotation = /*>|>*/ Stats.track("computeNPMembersNamed") /*<|<*/ {
       Stats.record("computeNPMembersNamed after fingerprint")
       ensureCompleted()
       val ownDenots = info.decls.denotsNamed(name, selectNonPrivate)
@@ -1564,7 +1564,7 @@ object SymDenotations {
           p.symbol.denot match {
             case parentd: ClassDenotation =>
               denots1 union
-                parentd.nonPrivateMembersNamed(name, inherited = true)
+                parentd.nonPrivateMembersNamed(name)
                 .mapInherited(ownDenots, denots1, thisType)
             case _ =>
               denots1
@@ -1768,19 +1768,19 @@ object SymDenotations {
      *  object that hides a class or object in the scala package of the same name, because
      *  the behavior would then be unintuitive for such members.
      */
-    override def computeNPMembersNamed(name: Name, inherited: Boolean)(implicit ctx: Context): PreDenotation =
+    override def computeNPMembersNamed(name: Name)(implicit ctx: Context): PreDenotation =
       packageObj.moduleClass.denot match {
         case pcls: ClassDenotation if !pcls.isCompleting =>
           if (symbol eq defn.ScalaPackageClass) {
-            val denots = super.computeNPMembersNamed(name, inherited)
-            if (denots.exists) denots else pcls.computeNPMembersNamed(name, inherited)
+            val denots = super.computeNPMembersNamed(name)
+            if (denots.exists) denots else pcls.computeNPMembersNamed(name)
           }
           else {
-            val denots = pcls.computeNPMembersNamed(name, inherited)
-            if (denots.exists) denots else super.computeNPMembersNamed(name, inherited)
+            val denots = pcls.computeNPMembersNamed(name)
+            if (denots.exists) denots else super.computeNPMembersNamed(name)
           }
         case _ =>
-          super.computeNPMembersNamed(name, inherited)
+          super.computeNPMembersNamed(name)
       }
 
     /** The union of the member names of the package and the package object */
diff --git a/compiler/src/dotty/tools/dotc/core/TypeOps.scala b/compiler/src/dotty/tools/dotc/core/TypeOps.scala
index 829b5acec00c..6915a0197bab 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeOps.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeOps.scala
@@ -19,131 +19,76 @@ import ast.tpd._
 trait TypeOps { this: Context => // TODO: Make standalone object.
 
   /** The type `tp` as seen from prefix `pre` and owner `cls`. See the spec
-   *  for what this means. Called very often, so the code is optimized heavily.
-   *
-   *  A tricky aspect is what to do with unstable prefixes. E.g. say we have a class
-   *
-   *    class C { type T; def f(x: T): T }
-   *
-   *  and an expression `e` of type `C`. Then computing the type of `e.f` leads
-   *  to the query asSeenFrom(`C`, `(x: T)T`). What should its result be? The
-   *  naive answer `(x: C#T)C#T` is incorrect given that we treat `C#T` as the existential
-   *  `exists(c: C)c.T`. What we need to do instead is to skolemize the existential. So
-   *  the answer would be `(x: c.T)c.T` for some (unknown) value `c` of type `C`.
-   *  `c.T` is expressed in the compiler as a skolem type `Skolem(C)`.
-   *
-   *  Now, skolemization is messy and expensive, so we want to do it only if we absolutely
-   *  must. Also, skolemizing immediately would mean that asSeenFrom was no longer
-   *  idempotent - each call would return a type with a different skolem.
-   *  Instead we produce an annotated type that marks the prefix as unsafe:
-   *
-   *     (x: (C @ UnsafeNonvariant)#T)C#T
-   *
-   *  We also set a global state flag `unsafeNonvariant` to the current run.
-   *  When typing a Select node, typer will check that flag, and if it
-   *  points to the current run will scan the result type of the select for
-   *  @UnsafeNonvariant annotations. If it finds any, it will introduce a skolem
-   *  constant for the prefix and try again.
-   *
-   *  The scheme is efficient in particular because we expect that unsafe situations are rare;
-   *  most compiles would contain none, so no scanning would be necessary.
+   *  for what this means.
    */
   final def asSeenFrom(tp: Type, pre: Type, cls: Symbol): Type =
-    asSeenFrom(tp, pre, cls, null)
+    new AsSeenFromMap(pre, cls).apply(tp)
 
-  /** Helper method, taking a map argument which is instantiated only for more
-   *  complicated cases of asSeenFrom.
-   */
-  private def asSeenFrom(tp: Type, pre: Type, cls: Symbol, theMap: AsSeenFromMap): Type = {
-
-    /** Map a `C.this` type to the right prefix. If the prefix is unstable and
-     *  the `C.this` occurs in nonvariant or contravariant position, mark the map
-     *  to be unstable.
-     */
-    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 pre match {
-        case pre: SuperType => toPrefix(pre.thistpe, cls, thiscls)
-        case _ =>
-          if (thiscls.derivesFrom(cls) && pre.baseTypeRef(thiscls).exists) {
-            if (theMap != null && theMap.currentVariance <= 0 && !isLegalPrefix(pre)) {
-              ctx.base.unsafeNonvariant = ctx.runId
-              pre match {
-                case AnnotatedType(_, ann) if ann.symbol == defn.UnsafeNonvariantAnnot => pre
-                case _ => AnnotatedType(pre, Annotation(defn.UnsafeNonvariantAnnot, Nil))
-              }
-            }
-            else pre
-          }
-          else if ((pre.termSymbol is Package) && !(thiscls is Package))
-            toPrefix(pre.select(nme.PACKAGE), cls, thiscls)
-          else
-            toPrefix(pre.baseTypeRef(cls).normalizedPrefix, cls.owner, thiscls)
+  /** The TypeMap handling the asSeenFrom */
+  class AsSeenFromMap(pre: Type, cls: Symbol) extends ApproximatingTypeMap {
+
+    def apply(tp: Type): Type = {
+
+      /** Map a `C.this` type to the right prefix. If the prefix is unstable and
+      *  the `C.this` occurs in nonvariant or contravariant position, mark the map
+      *  to be unstable.
+      */
+      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 pre match {
+          case pre: SuperType => toPrefix(pre.thistpe, cls, thiscls)
+          case _ =>
+            if (thiscls.derivesFrom(cls) && pre.baseTypeRef(thiscls).exists)
+              if (variance <= 0 && !isLegalPrefix(pre)) range(pre.bottomType, pre)
+              else pre
+            else if ((pre.termSymbol is Package) && !(thiscls is Package))
+              toPrefix(pre.select(nme.PACKAGE), cls, thiscls)
+            else
+              toPrefix(pre.baseTypeRef(cls).normalizedPrefix, cls.owner, thiscls)
+        }
       }
-    }
 
-    /*>|>*/ 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
-          if (sym.isStatic) tp
-          else {
-            val pre1 = asSeenFrom(tp.prefix, pre, cls, theMap)
-            if (pre1.isUnsafeNonvariant) {
-              val safeCtx = ctx.withProperty(TypeOps.findMemberLimit, Some(()))
-              pre1.member(tp.name)(safeCtx).info match {
-                case TypeAlias(alias) =>
-                  // try to follow aliases of this will avoid skolemization.
-                  return alias
-                case _ =>
-              }
+      /*>|>*/ ctx.conditionalTraceIndented(TypeOps.track, s"asSeen ${tp.show} from (${pre.show}, ${cls.show})", show = true) /*<|<*/ { // !!! DEBUG
+        tp match {
+          case tp: NamedType => // inlined for performance; TODO: factor out into inline method
+            if (tp.symbol.isStatic) tp
+            else {
+              val saved = variance
+              variance = variance max 0
+              val prefix1 = this(tp.prefix)
+              variance = saved
+              derivedSelect(tp, prefix1)
             }
-            tp.derivedSelect(pre1)
-          }
-        case tp: ThisType =>
-          toPrefix(pre, cls, tp.cls)
-        case _: BoundType | NoPrefix =>
-          tp
-        case tp: RefinedType =>
-          tp.derivedRefinedType(
-            asSeenFrom(tp.parent, pre, cls, theMap),
-            tp.refinedName,
-            asSeenFrom(tp.refinedInfo, pre, cls, theMap))
-        case tp: TypeAlias if tp.variance == 1 => // if variance != 1, need to do the variance calculation
-          tp.derivedTypeAlias(asSeenFrom(tp.alias, pre, cls, theMap))
-        case _ =>
-          (if (theMap != null) theMap else new AsSeenFromMap(pre, cls))
-            .mapOver(tp)
+          case tp: ThisType =>
+            toPrefix(pre, cls, tp.cls)
+          case _: BoundType | NoPrefix =>
+            tp
+          case tp: RefinedType =>
+            derivedRefinedType(tp, apply(tp.parent), apply(tp.refinedInfo))
+          case tp: TypeAlias if tp.variance == 1 => // if variance != 1, need to do the variance calculation
+            derivedTypeAlias(tp, apply(tp.alias))
+          case _ =>
+            mapOver(tp)
+        }
       }
     }
+
+    override def reapply(tp: Type) =
+      // derives infos have already been subjected to asSeenFrom, hence to need to apply the map again.
+      tp
   }
 
   private def isLegalPrefix(pre: Type)(implicit ctx: Context) =
     pre.isStable || !ctx.phase.isTyper
 
-  /** The TypeMap handling the asSeenFrom in more complicated cases */
-  class AsSeenFromMap(pre: Type, cls: Symbol) extends TypeMap {
-    def apply(tp: Type) = asSeenFrom(tp, pre, cls, this)
-
-    /** A method to export the current variance of the map */
-    def currentVariance = variance
-  }
-
   /** Approximate a type `tp` with a type that does not contain skolem types. */
   object deskolemize extends ApproximatingTypeMap {
-    private var seen: Set[SkolemType] = Set()
-    def apply(tp: Type) = tp match {
-      case tp: SkolemType =>
-        if (seen contains tp) NoType
-        else {
-          val saved = seen
-          seen += tp
-          try approx(hi = tp.info)
-          finally seen = saved
-        }
-      case _ =>
-        mapOver(tp)
+    def apply(tp: Type) = /*ctx.traceIndented(i"deskolemize($tp) at $variance", show = true)*/ {
+      tp match {
+        case tp: SkolemType => range(tp.bottomType, atVariance(1)(apply(tp.info)))
+        case _ => mapOver(tp)
+      }
     }
   }
 
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index 3dd56aa1cebf..721f2358ce79 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -136,6 +136,12 @@ object Types {
       case _ => false
     }
 
+    /** Is this type exactly Nothing (no vars, aliases, refinements etc allowed)? */
+    def isBottomType(implicit ctx: Context): Boolean = this match {
+      case tp: TypeRef => tp.symbol eq defn.NothingClass
+      case _ => false
+    }
+
     /** Is this type a (neither aliased nor applied) reference to class `sym`? */
     def isDirectRef(sym: Symbol)(implicit ctx: Context): Boolean = stripTypeVar match {
       case this1: TypeRef =>
@@ -249,16 +255,6 @@ object Types {
     def isRepeatedParam(implicit ctx: Context): Boolean =
       typeSymbol eq defn.RepeatedParamClass
 
-    /** Does this type carry an UnsafeNonvariant annotation? */
-    final def isUnsafeNonvariant(implicit ctx: Context): Boolean = this match {
-      case AnnotatedType(_, annot) => annot.symbol == defn.UnsafeNonvariantAnnot
-      case _ => false
-    }
-
-    /** Does this type have an UnsafeNonvariant annotation on one of its parts? */
-    final def hasUnsafeNonvariant(implicit ctx: Context): Boolean =
-      new HasUnsafeNonAccumulator().apply(false, this)
-
     /** Is this the type of a method that has a repeated parameter type as
      *  last parameter type?
      */
@@ -275,7 +271,7 @@ object Types {
     }
 
     /** Is this an alias TypeBounds? */
-    def isAlias: Boolean = this.isInstanceOf[TypeAlias]
+    final def isAlias: Boolean = this.isInstanceOf[TypeAlias]
 
 // ----- Higher-order combinators -----------------------------------
 
@@ -1220,6 +1216,18 @@ object Types {
       case _ => TypeAlias(this)
     }
 
+    /** The lower bound of a TypeBounds type, the type itself otherwise */
+    def loBound = this match {
+      case tp: TypeBounds => tp.lo
+      case _ => this
+    }
+
+    /** The upper bound of a TypeBounds type, the type itself otherwise */
+    def hiBound = this match {
+      case tp: TypeBounds => tp.hi
+      case _ => this
+    }
+
     /** The type parameter with given `name`. This tries first `decls`
      *  in order not to provoke a cycle by forcing the info. If that yields
      *  no symbol it tries `member` as an alternative.
@@ -1766,6 +1774,7 @@ object Types {
      */
     def derivedSelect(prefix: Type)(implicit ctx: Context): Type =
       if (prefix eq this.prefix) this
+      else if (prefix.isBottomType) prefix
       else if (isType) {
         val res = prefix.lookupRefined(name)
         if (res.exists) res
@@ -3733,7 +3742,7 @@ object Types {
 
         case tp: TypeAlias =>
           val saved = variance
-          variance = variance * tp.variance
+          variance *= tp.variance
           val alias1 = this(tp.alias)
           variance = saved
           derivedTypeAlias(tp, alias1)
@@ -3851,63 +3860,197 @@ object Types {
     def apply(tp: Type) = tp
   }
 
-  /** A type map that approximates NoTypes by upper or lower known bounds depending on
+  /** A type map that approximates TypeBounds types depending on
    *  variance.
    *
    *  if variance > 0 : approximate by upper bound
    *     variance < 0 : approximate by lower bound
-   *     variance = 0 : propagate NoType to next outer level
+   *     variance = 0 : propagate bounds to next outer level
    */
   abstract class ApproximatingTypeMap(implicit ctx: Context) extends TypeMap { thisMap =>
-    def approx(lo: Type = defn.NothingType, hi: Type = defn.AnyType) =
-      if (variance == 0) NoType
-      else apply(if (variance < 0) lo else hi)
 
+    protected def range(lo: Type, hi: Type) =
+      if (variance > 0) hi
+      else if (variance < 0) lo
+      else Range(lower(lo), upper(hi))
+
+    protected def isRange(tp: Type) = tp.isInstanceOf[Range]
+
+    protected def lower(tp: Type) = tp match {
+      case tp: Range => tp.lo
+      case _ => tp
+    }
+
+    protected def upper(tp: Type) = tp match {
+      case tp: Range => tp.hi
+      case _ => tp
+    }
+
+    protected def rangeToBounds(tp: Type) = tp match {
+      case Range(lo, hi) => TypeBounds(lo, hi)
+      case _ => tp
+    }
+
+    protected def atVariance[T](v: Int)(op: => T): T = {
+      val saved = variance
+      variance = v
+      try op finally variance = saved
+    }
+
+    /** Derived selection.
+     *  @pre   the (upper bound of) prefix `pre` has a member named `tp.name`.
+     */
     override protected def derivedSelect(tp: NamedType, pre: Type) =
       if (pre eq tp.prefix) tp
-      else tp.info match {
-        case TypeAlias(alias) => apply(alias) // try to heal by following aliases
-        case _ =>
-          if (pre.exists && !pre.isRef(defn.NothingClass) && variance > 0) tp.derivedSelect(pre)
-          else tp.info match {
-            case TypeBounds(lo, hi) => approx(lo, hi)
-            case _ => approx()
+      else pre match {
+        case Range(preLo, preHi) =>
+          preHi.member(tp.name).info.widenExpr match {
+            case TypeAlias(alias) =>
+              // if H#T = U, then for any x in L..H, x.T =:= U,
+              // hence we can replace with U under all variances
+              reapply(alias)
+            case TypeBounds(lo, hi) =>
+              // If H#T = _ >: S <: U, then for any x in L..H, S <: x.T <: U,
+              // hence we can replace with S..U under all variances
+              range(atVariance(-variance)(reapply(lo)), reapply(hi))
+            case info: SingletonType =>
+              // if H#x: y.type, then for any x in L..H, x.type =:= y.type,
+              // hence we can replace with y.type under all variances
+              reapply(info)
+            case _ =>
+              range(tp.derivedSelect(preLo), tp.derivedSelect(preHi))
           }
+        case _ => tp.derivedSelect(pre)
       }
+
     override protected def derivedRefinedType(tp: RefinedType, parent: Type, info: Type) =
-      if (parent.exists && info.exists) tp.derivedRefinedType(parent, tp.refinedName, info)
-      else approx(hi = parent)
+      if ((parent eq tp.parent) && (info eq tp.refinedInfo)) tp
+      else parent match {
+        case Range(parentLo, parentHi) =>
+          range(derivedRefinedType(tp, parentLo, info), derivedRefinedType(tp, parentHi, info))
+        case _ =>
+          if (parent.isBottomType) parent
+          else info match {
+            case Range(infoLo, infoHi) =>
+              def propagate(lo: Type, hi: Type) =
+                range(derivedRefinedType(tp, parent, lo), derivedRefinedType(tp, parent, hi))
+              tp.refinedInfo match {
+                case rinfo: TypeBounds =>
+                  val v = if (rinfo.isAlias) rinfo.variance * variance else variance
+                  if (v > 0) tp.derivedRefinedType(parent, tp.refinedName, rangeToBounds(info))
+                  else if (v < 0) propagate(infoHi, infoLo)
+                  else range(tp.bottomType, tp.topType)
+                case _ =>
+                  propagate(infoLo, infoHi)
+              }
+            case _ =>
+              tp.derivedRefinedType(parent, tp.refinedName, info)
+          }
+        }
+
     override protected def derivedRecType(tp: RecType, parent: Type) =
-      if (parent.exists) tp.rebind(parent)
-      else approx()
+      if (parent eq tp.parent) tp
+      else parent match {
+        case Range(lo, hi) => range(tp.rebind(lo), tp.rebind(hi))
+        case _ => tp.rebind(parent)
+      }
+
     override protected def derivedTypeAlias(tp: TypeAlias, alias: Type) =
-      if (alias.exists) tp.derivedTypeAlias(alias)
-      else approx(NoType, TypeBounds.empty)
+      if (alias eq tp.alias) tp
+      else alias match {
+        case Range(lo, hi) =>
+          if (variance > 0) TypeBounds(lo, hi)
+          else range(TypeAlias(lo), TypeAlias(hi))
+        case _ => tp.derivedTypeAlias(alias)
+      }
+
     override protected def derivedTypeBounds(tp: TypeBounds, lo: Type, hi: Type) =
-      if (lo.exists && hi.exists) tp.derivedTypeBounds(lo, hi)
-      else approx(NoType,
-        if (lo.exists) TypeBounds.lower(lo)
-        else if (hi.exists) TypeBounds.upper(hi)
-        else TypeBounds.empty)
+      if ((lo eq tp.lo) && (hi eq tp.hi)) tp
+      else if (isRange(lo) || isRange(hi))
+        if (variance > 0) TypeBounds(lower(lo), upper(hi))
+        else range(TypeBounds(upper(lo), lower(hi)), TypeBounds(lower(lo), upper(hi)))
+      else tp.derivedTypeBounds(lo, hi)
+
     override protected def derivedSuperType(tp: SuperType, thistp: Type, supertp: Type) =
-      if (thistp.exists && supertp.exists) tp.derivedSuperType(thistp, supertp)
-      else NoType
+      if (isRange(thistp) || isRange(supertp)) range(thistp.bottomType, thistp.topType)
+      else tp.derivedSuperType(thistp, supertp)
+
     override protected def derivedAppliedType(tp: HKApply, tycon: Type, args: List[Type]): Type =
-      if (tycon.exists && args.forall(_.exists)) tp.derivedAppliedType(tycon, args)
-      else approx() // This is rather coarse, but to do better is a bit complicated
+      tycon match {
+        case Range(tyconLo, tyconHi) =>
+          range(derivedAppliedType(tp, tyconLo, args), derivedAppliedType(tp, tyconHi, args))
+        case _ =>
+          if (args.exists(isRange)) {
+            if (variance > 0) tp.derivedAppliedType(tycon, args.map(rangeToBounds))
+            else {
+              val loBuf, hiBuf = new mutable.ListBuffer[Type]
+              def distributeArgs(args: List[Type], tparams: List[ParamInfo]): Boolean = args match {
+                case Range(lo, hi) :: args1 =>
+                  val v = tparams.head.paramVariance
+                  if (v == 0) false
+                  else {
+                    if (v > 0) { loBuf += lo; hiBuf += hi }
+                    else { loBuf += hi; hiBuf += lo }
+                    distributeArgs(args1, tparams.tail)
+                  }
+                case arg :: args1 =>
+                  loBuf += arg; hiBuf += arg
+                  distributeArgs(args1, tparams.tail)
+                case nil =>
+                  true
+              }
+              if (distributeArgs(args, tp.typeParams))
+                range(tp.derivedAppliedType(tycon, loBuf.toList),
+                      tp.derivedAppliedType(tycon, hiBuf.toList))
+              else range(tp.bottomType, tp.topType)
+            }
+          }
+          else tp.derivedAppliedType(tycon, args)
+      }
+
     override protected def derivedAndOrType(tp: AndOrType, tp1: Type, tp2: Type) =
-      if (tp1.exists && tp2.exists) tp.derivedAndOrType(tp1, tp2)
-      else if (tp.isAnd) approx(hi = tp1 & tp2)  // if one of tp1d, tp2d exists, it is the result of tp1d & tp2d
-      else approx(lo = tp1 & tp2)
+      if (tp1.isInstanceOf[Range] || tp2.isInstanceOf[Range])
+        if (tp.isAnd) range(lower(tp1) & lower(tp2), upper(tp1) & upper(tp2))
+        else range(lower(tp1) | lower(tp2), upper(tp1) | upper(tp2))
+      else tp.derivedAndOrType(tp1, tp2)
+
     override protected def derivedAnnotatedType(tp: AnnotatedType, underlying: Type, annot: Annotation) =
-      if (underlying.exists) tp.derivedAnnotatedType(underlying, annot)
-      else NoType
-    override protected def derivedWildcardType(tp: WildcardType, bounds: Type) =
-      if (bounds.exists) tp.derivedWildcardType(bounds)
-      else WildcardType
-    override protected def derivedClassInfo(tp: ClassInfo, pre: Type): Type =
-      if (pre.exists) tp.derivedClassInfo(pre)
-      else NoType
+      underlying match {
+        case Range(lo, hi) =>
+          range(tp.derivedAnnotatedType(lo, annot), tp.derivedAnnotatedType(hi, annot))
+        case _ =>
+          if (underlying.isBottomType) underlying
+          else tp.derivedAnnotatedType(underlying, annot)
+      }
+    override protected def derivedWildcardType(tp: WildcardType, bounds: Type) = {
+      tp.derivedWildcardType(rangeToBounds(bounds))
+    }
+
+    override protected def derivedClassInfo(tp: ClassInfo, pre: Type): Type = {
+      assert(!pre.isInstanceOf[Range])
+      tp.derivedClassInfo(pre)
+    }
+
+    override protected def derivedLambdaType(tp: LambdaType)(formals: List[tp.PInfo], restpe: Type): Type =
+      restpe match {
+        case Range(lo, hi) =>
+          range(derivedLambdaType(tp)(formals, lo), derivedLambdaType(tp)(formals, hi))
+        case _ =>
+          tp.derivedLambdaType(tp.paramNames, formals, restpe)
+      }
+
+    protected def reapply(tp: Type): Type = apply(tp)
+  }
+
+  /** A range of possible types between lower bound `lo` and upper bound `hi`.
+   *  Only used internally in `ApproximatingTypeMap`.
+   */
+  private case class Range(lo: Type, hi: Type) extends UncachedGroundType {
+    assert(!lo.isInstanceOf[Range])
+    assert(!hi.isInstanceOf[Range])
+
+    override def toText(printer: Printer): Text =
+      lo.toText(printer) ~ ".." ~ hi.toText(printer)
   }
 
   // ----- TypeAccumulators ----------------------------------------------------
@@ -4047,10 +4190,6 @@ object Types {
     def apply(x: Unit, tp: Type): Unit = foldOver(p(tp), tp)
   }
 
-  class HasUnsafeNonAccumulator(implicit ctx: Context) extends TypeAccumulator[Boolean] {
-    def apply(x: Boolean, tp: Type) = x || tp.isUnsafeNonvariant || foldOver(x, tp)
-  }
-
   class NamedPartsAccumulator(p: NamedType => Boolean, excludeLowerBounds: Boolean = false)
     (implicit ctx: Context) extends TypeAccumulator[mutable.Set[NamedType]] {
     override def stopAtStatic = false
diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
index 8a10ef60ebbe..8fd557981dc7 100644
--- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
@@ -68,6 +68,15 @@ class PlainPrinter(_ctx: Context) extends Printer {
       }
     else tp
 
+  private def sameBound(lo: Type, hi: Type): Boolean =
+    try lo =:= hi
+    catch { case ex: Throwable => false }
+
+  private def homogenizeArg(tp: Type) = tp match {
+    case TypeBounds(lo, hi) if sameBound(lo, hi) => homogenize(hi)
+    case _ => tp
+  }
+
   private def selfRecName(n: Int) = s"z$n"
 
   /** Render elements alternating with `sep` string */
@@ -113,9 +122,9 @@ class PlainPrinter(_ctx: Context) extends Printer {
   protected def toTextRefinement(rt: RefinedType) =
     (refinementNameString(rt) ~ toTextRHS(rt.refinedInfo)).close
 
-  protected def argText(arg: Type): Text = arg match {
+  protected def argText(arg: Type): Text = homogenizeArg(arg) match {
     case arg: TypeBounds => "_" ~ toTextGlobal(arg)
-    case _ => toTextGlobal(arg)
+    case arg => toTextGlobal(arg)
   }
 
   /** The longest sequence of refinement types, starting at given type
diff --git a/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala b/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala
index 42cee77cb899..3641915b53e7 100644
--- a/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala
+++ b/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala
@@ -39,95 +39,90 @@ trait TypeAssigner {
     }
   }
 
+  /** Given a class info, the intersection of its parents, refined by all
+   *  non-private fields, methods, and type members.
+   */
+  def classBound(info: ClassInfo)(implicit ctx: Context): Type = {
+    val parentType = info.parentsWithArgs.reduceLeft(ctx.typeComparer.andType(_, _))
+    def addRefinement(parent: Type, decl: Symbol) = {
+      val inherited =
+        parentType.findMember(decl.name, info.cls.thisType, Private)
+          .suchThat(decl.matches(_))
+      val inheritedInfo = inherited.info
+      if (inheritedInfo.exists && decl.info <:< inheritedInfo && !(inheritedInfo <:< decl.info)) {
+        val r = RefinedType(parent, decl.name, decl.info)
+        typr.println(i"add ref $parent $decl --> " + r)
+        r
+      }
+      else
+        parent
+    }
+    val refinableDecls = info.decls.filter(
+      sym => !(sym.is(TypeParamAccessor | Private) || sym.isConstructor))
+    val raw = (parentType /: refinableDecls)(addRefinement)
+    RecType.closeOver(rt => raw.substThis(info.cls, RecThis(rt)))
+  }
+
   /** An upper approximation of the given type `tp` that does not refer to any symbol in `symsToAvoid`.
-   *  Approximation steps are:
+   *  We need to approximate with ranges:
+   *
+   *    term references to symbols in `symsToAvoid`,
+   *    term references that have a widened type of which some part refers
+   *    to a symbol in `symsToAvoid`,
+   *    type references to symbols in `symsToAvoid`,
+   *    this types of classes in `symsToAvoid`.
    *
-   *   - follow aliases and upper bounds if the original refers to a forbidden symbol
-   *   - widen termrefs that refer to a forbidden symbol
-   *   - replace ClassInfos of forbidden classes by the intersection of their parents, refined by all
-   *     non-private fields, methods, and type members.
-   *   - if the prefix of a class refers to a forbidden symbol, first try to replace the prefix,
-   *     if this is not possible, replace the ClassInfo as above.
-   *   - drop refinements referring to a forbidden symbol.
+   *  Type variables that would be interpolated to a type that
+   *  needs to be widened are replaced by the widened interpolation instance.
    */
   def avoid(tp: Type, symsToAvoid: => List[Symbol])(implicit ctx: Context): Type = {
-    val widenMap = new TypeMap {
+    val widenMap = new ApproximatingTypeMap {
       lazy val forbidden = symsToAvoid.toSet
-      def toAvoid(tp: Type): Boolean =
-        // TODO: measure the cost of using `existsPart`, and if necessary replace it
-        // by a `TypeAccumulator` where we have set `stopAtStatic = true`.
-        tp existsPart {
-          case tp: TermRef => forbidden.contains(tp.symbol) || toAvoid(tp.underlying)
-          case tp: TypeRef => forbidden.contains(tp.symbol)
-          case tp: ThisType => forbidden.contains(tp.cls)
-          case _ => false
-        }
+      def toAvoid(sym: Symbol) = !sym.isStatic && forbidden.contains(sym)
+      def partsToAvoid = new NamedPartsAccumulator(tp => toAvoid(tp.symbol))
       def apply(tp: Type): Type = tp match {
         case tp: TermRef
-        if toAvoid(tp) && (variance > 0 || tp.info.widenExpr <:< tp) =>
-          // Can happen if `x: y.type`, then `x.type =:= y.type`, hence we can widen `x.type`
-          // to y.type in all contexts, not just covariant ones.
-          apply(tp.info.widenExpr)
-        case tp: TypeRef if toAvoid(tp) =>
-          tp.info match {
-            case TypeAlias(ref) =>
-              apply(ref)
-            case info: ClassInfo if variance > 0 =>
-              if (!(forbidden contains tp.symbol)) {
-                val prefix = apply(tp.prefix)
-                val tp1 = tp.derivedSelect(prefix)
-                if (tp1.typeSymbol.exists)
-                  return tp1
-              }
-              val parentType = info.parentsWithArgs.reduceLeft(ctx.typeComparer.andType(_, _))
-              def addRefinement(parent: Type, decl: Symbol) = {
-                val inherited =
-                  parentType.findMember(decl.name, info.cls.thisType, Private)
-                    .suchThat(decl.matches(_))
-                val inheritedInfo = inherited.info
-                if (inheritedInfo.exists && decl.info <:< inheritedInfo && !(inheritedInfo <:< decl.info)) {
-                  val r = RefinedType(parent, decl.name, decl.info)
-                  typr.println(i"add ref $parent $decl --> " + r)
-                  r
-                }
-                else
-                  parent
-              }
-              val refinableDecls = info.decls.filter(
-                sym => !(sym.is(TypeParamAccessor | Private) || sym.isConstructor))
-              val fullType = (parentType /: refinableDecls)(addRefinement)
-              apply(fullType)
-            case TypeBounds(lo, hi) if variance > 0 =>
-              apply(hi)
-            case _ =>
-              mapOver(tp)
+        if toAvoid(tp.symbol) || partsToAvoid(mutable.Set.empty, tp.info).nonEmpty =>
+          tp.info.widenExpr match {
+            case info: SingletonType => apply(info)
+            case info => range(tp.info.bottomType, apply(info))
           }
-        case tp @ HKApply(tycon, args) if toAvoid(tycon) =>
-          apply(tp.superType)
-        case tp @ AppliedType(tycon, args) if toAvoid(tycon) =>
-          val base = apply(tycon)
-          var args = tp.baseArgInfos(base.typeSymbol)
-          if (base.typeParams.length != args.length)
-            args = base.typeParams.map(_.paramInfo)
-          apply(base.appliedTo(args))
-        case tp @ RefinedType(parent, name, rinfo) if variance > 0 =>
-          val parent1 = apply(tp.parent)
-          val refinedInfo1 = apply(rinfo)
-          if (toAvoid(refinedInfo1)) {
-            typr.println(s"dropping refinement from $tp")
-            if (name.isTypeName) tp.derivedRefinedType(parent1, name, TypeBounds.empty)
-            else parent1
-          } else {
-            tp.derivedRefinedType(parent1, name, refinedInfo1)
+        case tp: TypeRef if toAvoid(tp.symbol) =>
+          val avoided = tp.info match {
+            case TypeAlias(alias) =>
+              apply(alias)
+            case TypeBounds(lo, hi) =>
+              range(atVariance(-variance)(apply(lo)), apply(hi))
+            case info: ClassInfo =>
+              range(tp.bottomType, apply(classBound(info)))
+            case _ =>
+              range(tp.bottomType, tp.topType) // should happen only in error cases
           }
+          avoided
+        case tp: ThisType if toAvoid(tp.cls) =>
+          range(tp.bottomType, apply(classBound(tp.cls.classInfo)))
         case tp: TypeVar if ctx.typerState.constraint.contains(tp) =>
-          val lo = ctx.typerState.constraint.fullLowerBound(tp.origin)
-          val lo1 = avoid(lo, symsToAvoid)
+          val lo = ctx.typeComparer.instanceType(tp.origin, fromBelow = variance >= 0)
+          val lo1 = apply(lo)
           if (lo1 ne lo) lo1 else tp
         case _ =>
           mapOver(tp)
       }
+
+      /** Two deviations from standard derivedSelect:
+       *   1. The teh approximation result is a singleton references C#x.type, we
+       *      replace by the widened type, which is usually more natural.
+       *   2. We need to handle the case where the prefix type does not have a member
+       *      named `tp.name` anymmore.
+       */
+      override def derivedSelect(tp: NamedType, pre: Type) =
+        if (pre eq tp.prefix) tp
+        else if (tp.isTerm && variance > 0 && !pre.isInstanceOf[SingletonType])
+          apply(tp.info.widenExpr)
+        else if (upper(pre).member(tp.name).exists) super.derivedSelect(tp, pre)
+        else range(tp.bottomType, tp.topType)
     }
+
     widenMap(tp)
   }
 
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index a389cf77e98c..252e9c438c26 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -386,27 +386,7 @@ class Typer extends Namer with TypeAssigner with Applications with Implicits wit
   }
 
   private def typedSelect(tree: untpd.Select, pt: Type, qual: Tree)(implicit ctx: Context): Select =
-    healNonvariant(
-      checkValue(assignType(cpy.Select(tree)(qual, tree.name), qual), pt),
-      pt)
-
-  /** Let `tree = p.n` where `p: T`. If tree's type is an unsafe instantiation
-   *  (see TypeOps#asSeenFrom for how this can happen), rewrite the prefix `p`
-   *  to `(p: <unknown skolem of type T>)` and try again with the new (stable)
-   *  prefix. If the result has another unsafe instantiation, raise an error.
-   */
-  private def healNonvariant[T <: Tree](tree: T, pt: Type)(implicit ctx: Context): T  =
-    if (ctx.unsafeNonvariant == ctx.runId && tree.tpe.widen.hasUnsafeNonvariant)
-      tree match {
-        case tree @ Select(qual, _) if !qual.tpe.isStable =>
-          val alt = typedSelect(tree, pt, Typed(qual, TypeTree(SkolemType(qual.tpe.widen))))
-          typr.println(i"healed type: ${tree.tpe} --> $alt")
-          alt.asInstanceOf[T]
-        case _ =>
-          ctx.error(ex"unsafe instantiation of type ${tree.tpe}", tree.pos)
-          tree
-      }
-    else tree
+    checkValue(assignType(cpy.Select(tree)(qual, tree.name), qual), pt)
 
   def typedSelect(tree: untpd.Select, pt: Type)(implicit ctx: Context): Tree = track("typedSelect") {
     def typeSelectOnTerm(implicit ctx: Context): Tree = {
@@ -616,8 +596,7 @@ class Typer extends Namer with TypeAssigner with Applications with Implicits wit
                 case lhsCore: RefTree if setter.exists =>
                   val setterTypeRaw = pre.select(setterName, setter)
                   val setterType = ensureAccessible(setterTypeRaw, isSuperSelection(lhsCore), tree.pos)
-                  val lhs2 = healNonvariant(
-                    untpd.rename(lhsCore, setterName).withType(setterType), WildcardType)
+                  val lhs2 = untpd.rename(lhsCore, setterName).withType(setterType)
                   typedUnadapted(untpd.Apply(untpd.TypedSplice(lhs2), tree.rhs :: Nil))
                 case _ =>
                   reassignmentToVal
@@ -1427,7 +1406,7 @@ class Typer extends Namer with TypeAssigner with Applications with Implicits wit
       val impl1 = cpy.Template(impl)(constr1, parents1, self1, body1)
         .withType(dummy.nonMemberTermRef)
       checkVariance(impl1)
-      if (!cls.is(AbstractOrTrait) && !ctx.isAfterTyper) checkRealizableBounds(cls.typeRef, cdef.namePos)
+      if (!cls.is(AbstractOrTrait) && !ctx.isAfterTyper) checkRealizableBounds(cls.thisType, cdef.namePos)
       val cdef1 = assignType(cpy.TypeDef(cdef)(name, impl1), cls)
       if (ctx.phase.isTyper && cdef1.tpe.derivesFrom(defn.DynamicClass) && !ctx.dynamicsEnabled) {
         val isRequired = parents1.exists(_.tpe.isRef(defn.DynamicClass))
diff --git a/library/src/scala/annotation/internal/UnsafeNonvariant.scala b/library/src/scala/annotation/internal/UnsafeNonvariant.scala
deleted file mode 100644
index b33df65d6345..000000000000
--- a/library/src/scala/annotation/internal/UnsafeNonvariant.scala
+++ /dev/null
@@ -1,8 +0,0 @@
-package scala.annotation.internal
-
-import scala.annotation.Annotation
-
-/** This annotation is used as a marker for unsafe
- *  instantiations in asSeenFrom. See TypeOps.asSeenfrom for an explanation.
- */
-class UnsafeNonvariant extends Annotation
diff --git a/tests/neg/i1662.scala b/tests/neg/i1662.scala
index 1f9d02ba660b..722078023513 100644
--- a/tests/neg/i1662.scala
+++ b/tests/neg/i1662.scala
@@ -2,5 +2,5 @@ class Lift {
   def apply(f: F0) // error
   class F0
   object F0 { implicit def f2f0(String): F0 = ??? } // error
-  (new Lift)("")
+  (new Lift)("") // error after switch to approximating asSeenFrom
 }
diff --git a/tests/pos/i2948.scala b/tests/pos/i2948.scala
new file mode 100644
index 000000000000..0dac0f5284be
--- /dev/null
+++ b/tests/pos/i2948.scala
@@ -0,0 +1,5 @@
+import scala.collection.mutable.ListBuffer
+class Foo {
+  val zipped: ListBuffer[(String, Int)] = null
+  val unzipped:  (ListBuffer[String], ListBuffer[Int]) = zipped.unzip
+}
diff --git a/tests/pos/t2435.scala b/tests/pos/t2435.scala
index 697e9e1f2d5e..f913b3bcae21 100644
--- a/tests/pos/t2435.scala
+++ b/tests/pos/t2435.scala
@@ -23,5 +23,6 @@ object Test {
   val a2 = a1.chain("a")
 
   println("\nDoesn't compile:")
-  val a = FNil.chain("a").chain("a").chain("a")
+  val a3 = FNil.chain("a").chain("a").chain("a")
+  val a4: FConstant[_ <: FConstant[_ <: FConstant[FNil.type]]] = a3
 }