diff --git a/compiler/src/dotty/tools/dotc/core/CheckRealizable.scala b/compiler/src/dotty/tools/dotc/core/CheckRealizable.scala
index 774cc233bff8..9089254ae9ad 100644
--- a/compiler/src/dotty/tools/dotc/core/CheckRealizable.scala
+++ b/compiler/src/dotty/tools/dotc/core/CheckRealizable.scala
@@ -10,7 +10,7 @@ import collection.mutable
 /** Realizability status */
 object CheckRealizable {
 
-  abstract class Realizability(val msg: String) {
+  sealed abstract class Realizability(val msg: String) {
     def andAlso(other: => Realizability): Realizability =
       if (this == Realizable) other else this
     def mapError(f: Realizability => Realizability): Realizability =
@@ -70,16 +70,20 @@ class CheckRealizable(implicit ctx: Context) {
   def realizability(tp: Type): Realizability = tp.dealias match {
     case tp: TermRef =>
       val sym = tp.symbol
-      if (sym.is(Stable)) realizability(tp.prefix)
-      else {
-        val r =
-          if (!sym.isStable) NotStable
-          else if (!isLateInitialized(sym)) realizability(tp.prefix)
-          else if (!sym.isEffectivelyFinal) new NotFinal(sym)
-          else realizability(tp.info).mapError(r => new ProblemInUnderlying(tp.info, r))
-        if (r == Realizable) sym.setFlag(Stable)
-        r
-      }
+      val r =
+        if (sym.is(Stable)) realizability(tp.prefix)
+        else {
+          val r =
+            if (!sym.isStable) NotStable
+            else if (!isLateInitialized(sym)) Realizable
+            else if (!sym.isEffectivelyFinal) new NotFinal(sym)
+            else realizability(tp.info).mapError(r => new ProblemInUnderlying(tp.info, r))
+          r andAlso {
+            sym.setFlag(Stable)
+            realizability(tp.prefix)
+          }
+        }
+      if (r == Realizable || tp.info.isStableRealizable) Realizable else r
     case _: SingletonType | NoPrefix =>
       Realizable
     case tp =>
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 60ad1963ee29..c24ecdfaa667 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -319,7 +319,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling {
         thirdTry
       case tp1: TypeParamRef =>
         def flagNothingBound = {
-          if (!frozenConstraint && tp2.isRef(defn.NothingClass) && state.isGlobalCommittable) {
+          if (!frozenConstraint && tp2.isRef(NothingClass) && state.isGlobalCommittable) {
             def msg = s"!!! instantiated to Nothing: $tp1, constraint = ${constraint.show}"
             if (Config.failOnInstantiationToNothing) assert(false, msg)
             else ctx.log(msg)
@@ -404,8 +404,9 @@ class TypeComparer(initctx: Context) extends ConstraintHandling {
         if (cls2.isClass) {
           if (cls2.typeParams.isEmpty) {
             if (cls2 eq AnyKindClass) return true
-            if (tp1.isRef(defn.NothingClass)) return true
+            if (tp1.isRef(NothingClass)) return true
             if (tp1.isLambdaSub) return false
+            if (cls2 eq AnyClass) return true
               // Note: We would like to replace this by `if (tp1.hasHigherKind)`
               // but right now we cannot since some parts of the standard library rely on the
               // idiom that e.g. `List <: Any`. We have to bootstrap without scalac first.
@@ -417,7 +418,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling {
             val base = tp1.baseType(cls2)
             if (base.typeSymbol == cls2) return true
           }
-          else if (tp1.isLambdaSub && !tp1.isRef(defn.AnyKindClass))
+          else if (tp1.isLambdaSub && !tp1.isRef(AnyKindClass))
             return recur(tp1, EtaExpansion(cls2.typeRef))
         }
         fourthTry
@@ -1382,7 +1383,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling {
                       // at run time. It would not work to replace that with `Nothing`.
                       // However, maybe we can still apply the replacement to
                       // types which are not explicitly written.
-                      defn.NothingType
+                      NothingType
                     case _ => andType(tp1, tp2)
                   }
                 case _ => andType(tp1, tp2)
@@ -1393,8 +1394,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling {
   }
 
   /** The greatest lower bound of a list types */
-  final def glb(tps: List[Type]): Type =
-    ((defn.AnyType: Type) /: tps)(glb)
+  final def glb(tps: List[Type]): Type = ((AnyType: Type) /: tps)(glb)
 
   /** The least upper bound of two types
    *  @param canConstrain  If true, new constraints might be added to simplify the lub.
@@ -1424,7 +1424,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling {
 
   /** The least upper bound of a list of types */
   final def lub(tps: List[Type]): Type =
-    ((defn.NothingType: Type) /: tps)(lub(_,_, canConstrain = false))
+    ((NothingType: Type) /: tps)(lub(_,_, canConstrain = false))
 
   /** Try to produce joint arguments for a lub `A[T_1, ..., T_n] | A[T_1', ..., T_n']` using
    *  the following strategies:
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index 576e69e790cc..7de8e12cd9ad 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -18,6 +18,7 @@ import Denotations._
 import Periods._
 import util.Stats._
 import util.SimpleIdentitySet
+import CheckRealizable._
 import reporting.diagnostic.Message
 import ast.tpd._
 import ast.TreeTypeMap
@@ -157,6 +158,12 @@ object Types {
       case _ => false
     }
 
+    /** Does this type denote a realizable stable reference? Much more expensive to check
+     *  than isStable, that's why some of the checks are done later in PostTyper.
+     */
+    final def isStableRealizable(implicit ctx: Context): Boolean =
+      isStable && realizability(this) == Realizable
+
     /** Is this type a (possibly refined or applied or aliased) type reference
      *  to the given type symbol?
      *  @sym  The symbol to compare to. It must be a class symbol or abstract type.
@@ -4506,6 +4513,8 @@ object Types {
       else if (lo `eq` hi) lo
       else Range(lower(lo), upper(hi))
 
+    protected def emptyRange: Type = range(defn.NothingType, defn.AnyType)
+
     protected def isRange(tp: Type): Boolean = tp.isInstanceOf[Range]
 
     protected def lower(tp: Type): Type = tp match {
@@ -4630,7 +4639,7 @@ object Types {
       else tp.derivedTypeBounds(lo, hi)
 
     override protected def derivedSuperType(tp: SuperType, thistp: Type, supertp: Type): Type =
-      if (isRange(thistp) || isRange(supertp)) range(defn.NothingType, defn.AnyType)
+      if (isRange(thistp) || isRange(supertp)) emptyRange
       else tp.derivedSuperType(thistp, supertp)
 
     override protected def derivedAppliedType(tp: AppliedType, tycon: Type, args: List[Type]): Type =
diff --git a/compiler/src/dotty/tools/dotc/typer/Applications.scala b/compiler/src/dotty/tools/dotc/typer/Applications.scala
index eea06175ecb0..693cb8a95274 100644
--- a/compiler/src/dotty/tools/dotc/typer/Applications.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Applications.scala
@@ -478,8 +478,9 @@ trait Applications extends Compatibility { self: Typer with Dynamic =>
             addArg(typedArg(arg, formal), formal)
             if (methodType.isParamDependent && typeOfArg(arg).exists)
               // `typeOfArg(arg)` could be missing because the evaluation of `arg` produced type errors
-              safeSubstParam(_, methodType.paramRefs(n), typeOfArg(arg))
-            else identity
+              safeSubstParam(_, methodType.paramRefs(n), typeOfArg(arg), initVariance = -1)
+            else
+              identity
           }
 
           def missingArg(n: Int): Unit = {
diff --git a/compiler/src/dotty/tools/dotc/typer/RefChecks.scala b/compiler/src/dotty/tools/dotc/typer/RefChecks.scala
index e36a6817fb91..1d84c3478d33 100644
--- a/compiler/src/dotty/tools/dotc/typer/RefChecks.scala
+++ b/compiler/src/dotty/tools/dotc/typer/RefChecks.scala
@@ -979,7 +979,7 @@ class RefChecks extends MiniPhase { thisPhase =>
     checkAllOverrides(cls)
     tree
   } catch {
-    case ex: MergeError =>
+    case ex: TypeError =>
       ctx.error(ex.getMessage, tree.pos)
       tree
   }
diff --git a/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala b/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala
index 4ca25185d907..38b348227edc 100644
--- a/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala
+++ b/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala
@@ -13,6 +13,7 @@ import NameOps._
 import collection.mutable
 import reporting.diagnostic.messages._
 import Checking.checkNoPrivateLeaks
+import CheckRealizable._
 
 trait TypeAssigner {
   import tpd._
@@ -105,7 +106,7 @@ trait TypeAssigner {
             case info: ClassInfo =>
               range(defn.NothingType, apply(classBound(info)))
             case _ =>
-              range(defn.NothingType, defn.AnyType) // should happen only in error cases
+              emptyRange // should happen only in error cases
           }
         case tp: ThisType if toAvoid(tp.cls) =>
           range(defn.NothingType, apply(classBound(tp.cls.classInfo)))
@@ -340,13 +341,31 @@ trait TypeAssigner {
     }
   }
 
-  /** Substitute argument type `argType` for parameter `pref` in type `tp`,
-   *  skolemizing the argument type if it is not stable and `pref` occurs in `tp`.
+  /** Substitute argument type `argType` for parameter `pref` in type `tp`, but
+   *  take special measures if the argument is not realizable:
+   *  1. If the widened argument type is known to have good bounds,
+   *     substitute the skolemized argument type.
+   *  2. If the widened argument type is not known to have good bounds, eliminate all references
+   *     to the parameter in `tp`.
+   *  (2) is necessary since even with a skolemized type we might break subtyping if
+   *  bounds are bad. This could lead to errors not being detected. A test case is the second
+   *  failure in neg/i4031.scala
    */
-  def safeSubstParam(tp: Type, pref: ParamRef, argType: Type)(implicit ctx: Context): Type = {
+  def safeSubstParam(tp: Type, pref: ParamRef, argType: Type, initVariance: Int = 1)(implicit ctx: Context): Type = {
     val tp1 = tp.substParam(pref, argType)
-    if ((tp1 eq tp) || argType.isStable) tp1
-    else tp.substParam(pref, SkolemType(argType.widen))
+    if ((tp1 eq tp) || argType.isStableRealizable) tp1
+    else {
+      val widenedArgType = argType.widen
+      if (realizability(widenedArgType) == Realizable)
+        tp.substParam(pref, SkolemType(widenedArgType))
+      else {
+        val avoidParam = new ApproximatingTypeMap {
+          variance = initVariance
+          def apply(t: Type) = if (t `eq` pref) emptyRange else mapOver(t)
+        }
+        avoidParam(tp)
+      }
+    }
   }
 
   /** Substitute types of all arguments `args` for corresponding `params` in `tp`.
diff --git a/tests/neg/i4031-anysel.scala b/tests/neg/i4031-anysel.scala
new file mode 100644
index 000000000000..c97209733375
--- /dev/null
+++ b/tests/neg/i4031-anysel.scala
@@ -0,0 +1,3 @@
+object Test {
+  val v: Any = 1: Any#L // error
+}
diff --git a/tests/neg/i4031-posttyper.scala b/tests/neg/i4031-posttyper.scala
new file mode 100644
index 000000000000..b877867267da
--- /dev/null
+++ b/tests/neg/i4031-posttyper.scala
@@ -0,0 +1,7 @@
+object App {
+  trait A { type L >: Any}
+  def upcast(a: A, x: Any): a.L = x
+  lazy val p: A { type L <: Nothing } = p
+  val q = new A { type L = Any }
+  def coerce2(x: Any): Int = upcast(p, x): p.L // error: not a legal path
+}
diff --git a/tests/neg/i4031.scala b/tests/neg/i4031.scala
new file mode 100644
index 000000000000..eb553c117dbe
--- /dev/null
+++ b/tests/neg/i4031.scala
@@ -0,0 +1,17 @@
+object App {
+  trait A { type L >: Any}
+  def upcast(a: A, x: Any): a.L = x
+  lazy val p: A { type L <: Nothing } = p
+  val q = new A { type L = Any }
+  def coerce(x: Any): Int = upcast(p, x)  // error: not a legal path
+
+  def compare(x: A, y: x.L) = assert(x == y)
+  def compare2(x: A)(y: x.type) = assert(x == y)
+
+
+  def main(args: Array[String]): Unit = {
+    println(coerce("Uh oh!"))
+    compare(p, p) // error: not a legal path
+    compare2(p)(p) // error: not a legal path
+  }
+}
diff --git a/tests/neg/i50-volatile.scala b/tests/neg/i50-volatile.scala
index fcfc9592b9a6..c62513d90949 100644
--- a/tests/neg/i50-volatile.scala
+++ b/tests/neg/i50-volatile.scala
@@ -10,16 +10,23 @@ class Test {
   }
   lazy val o: A & B = ???
 
-  class Client extends o.Inner                          // old-error // old-error
+  class Client extends o.Inner                          // error // old-error
 
-  def xToString(x: o.X): String = x                     // old-error
+  def xToString(x: o.X): String = x                     // error
 
   def intToString(i: Int): String = xToString(i)
 }
-object Test2 {
 
-  import Test.o._                                       // error
+object Test2 {
+  trait A {
+    type X = String
+  }
+  trait B {
+    type X = Int
+  }
+  lazy val o: A & B = ???
 
-  def xToString(x: X): String = x
+  def xToString(x: o.X): String = x       // error
 
+  def intToString(i: Int): String = xToString(i)
 }
diff --git a/tests/neg/i5521.scala b/tests/neg/i5521.scala
new file mode 100644
index 000000000000..9edb43605036
--- /dev/null
+++ b/tests/neg/i5521.scala
@@ -0,0 +1,12 @@
+class Hello {
+  class Foo {
+    class Bar
+    final lazy val s: Bar = ???
+  }
+
+  lazy val foo: Foo = ???
+
+  val x: foo.s.type = ???   // error: `foo` must be final since it's a lazy val
+  val x2: foo.s.type = ???  // error: `foo` must be final since it's a lazy val
+}
+
diff --git a/tests/neg/realizability.scala b/tests/neg/realizability.scala
new file mode 100644
index 000000000000..1730873e7692
--- /dev/null
+++ b/tests/neg/realizability.scala
@@ -0,0 +1,22 @@
+class C { type T }
+
+class Test {
+
+  type D <: C
+
+  lazy val a: C = ???
+  final lazy val b: C = ???
+  val c: D = ???
+  final lazy val d: D = ???
+
+  val x1: a.T = ???  // error: not a legal path, since a is lazy & non-final
+  val x2: b.T = ???  // OK, b is lazy but concrete
+  val x3: c.T = ???  // OK, c is abstract but strict
+  val x4: d.T = ???  // error: not a legal path since d is abstract and lazy
+
+  val y1: Singleton = a
+  val y2: Singleton = a
+  val y3: Singleton = a
+  val y4: Singleton = a
+
+}
diff --git a/tests/pos-deep-subtype/i4036.scala b/tests/pos-deep-subtype/i4036.scala
new file mode 100644
index 000000000000..df06ad9b3b3c
--- /dev/null
+++ b/tests/pos-deep-subtype/i4036.scala
@@ -0,0 +1,64 @@
+trait A { def x: this.type = this; type T }
+trait B { def y: this.type = this; def x: y.type = y; type T }
+object A {
+  val v = new A { type T = Int }
+  v: v.
+    x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
+    x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
+    x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
+    x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
+    x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
+    x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
+    x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
+    x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
+    x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
+    x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
+    x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
+    x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
+    x.type
+
+  1: v.
+    x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
+    x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
+    x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
+    x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
+    x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
+    x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
+    x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
+    x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
+    x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
+    x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
+    x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
+    x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
+    x.T
+
+  val u = new B { type T = Int }
+  u: u.
+    x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
+    x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
+    x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
+    x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
+    x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
+    x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
+    x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
+    x.type
+
+  val z = new B { type T = this.type }
+  z: z.T#
+    T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#
+    T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#
+    T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#
+    T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#
+    T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#
+    T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#
+    T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#
+    T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#
+    T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#
+    T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#
+    T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#
+    T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#
+    T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#
+    T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#
+    T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#
+    T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#T
+}
diff --git a/tests/pos/i4031.scala b/tests/pos/i4031.scala
new file mode 100644
index 000000000000..faf8f9d7f256
--- /dev/null
+++ b/tests/pos/i4031.scala
@@ -0,0 +1,8 @@
+object App {
+  trait A { type L >: Any}
+  def upcast(a: A, x: Any): a.L = x
+  lazy val p: A { type L <: Nothing } = p
+  val q = new A { type L = Any }
+  def coerce1(x: Any): Any = upcast(q, x)  // ok
+  def coerce3(x: Any): Any = upcast(p, x)  // ok, since dependent result type is not needed
+}