Merge pull request #599 from dotty-staging/add/existential-skolemization

Tighten comparison of skolem types

23 files changed, 364 insertions, 242 deletions

diff --git a/src/dotty/tools/dotc/config/Config.scala b/src/dotty/tools/dotc/config/Config.scala
index 27d5effa5..782a2f2d3 100644
--- a/src/dotty/tools/dotc/config/Config.scala
+++ b/src/dotty/tools/dotc/config/Config.scala
@@ -32,6 +32,11 @@ object Config {
    */
   final val checkConstraintsPropagated = false
 
+  /** Check that no type appearing as the info of a SymDenotation contains
+   *  skolem types.
+   */
+  final val checkNoSkolemsInInfo = false
+
   /** Type comparer will fail with an assert if the upper bound
    *  of a constrained parameter becomes Nothing. This should be turned
    *  on only for specific debugging as normally instantiation to Nothing
diff --git a/src/dotty/tools/dotc/core/Phases.scala b/src/dotty/tools/dotc/core/Phases.scala
index 0ec3320bb..b086308a2 100644
--- a/src/dotty/tools/dotc/core/Phases.scala
+++ b/src/dotty/tools/dotc/core/Phases.scala
@@ -285,6 +285,9 @@ object Phases {
      */
     def relaxedTyping: Boolean = false
 
+    /** Overridden by FrontEnd */
+    def isTyper = false
+
     def exists: Boolean = true
 
     private var myPeriod: Period = Periods.InvalidPeriod
diff --git a/src/dotty/tools/dotc/core/Skolemization.scala b/src/dotty/tools/dotc/core/Skolemization.scala
deleted file mode 100644
index fb47cb62a..000000000
--- a/src/dotty/tools/dotc/core/Skolemization.scala
+++ /dev/null
@@ -1,126 +0,0 @@
-package dotty.tools.dotc
-package core
-
-import Symbols._, Types._, Contexts._
-import collection.mutable
-
-/** Methods to add and remove skolemtypes.
- *
- *  Skolem types are generated when comparing refinements.
- *  A skolem type is simply a fresh singleton type that has a given type
- *  as underlying type.
- *  Two skolem types are equal if they refer to the same underlying type.
- *  To avoid unsoundness, skolem types have to be kept strictly local to the
- *  comparison, they are not allowed to escape the lifetime of a comparison
- *  by surviving in a context or in GADT bounds.
- */
-trait Skolemization {
-
-  implicit val ctx: Context
-
-  protected var skolemsOutstanding = false
-
-  def ensureStableSingleton(tp: Type): SingletonType = tp.stripTypeVar match {
-    case tp: SingletonType if tp.isStable =>
-      tp
-    case tp: ValueType =>
-      skolemsOutstanding = true
-      SkolemType(tp)
-    case tp: TypeProxy =>
-      ensureStableSingleton(tp.underlying)
-  }
-
-  /** Approximate a type `tp` with a type that does not contain skolem types.
-   *  @param  toSuper   if true, return the smallest supertype of `tp` with this property
-   *                    else return the largest subtype.
-   */
-  final def deSkolemize(tp: Type, toSuper: Boolean): Type =
-    if (skolemsOutstanding) deSkolemize(tp, if (toSuper) 1 else -1, Set())
-    else tp
-
-  private def deSkolemize(tp: Type, variance: Int, seen: Set[SkolemType]): Type =
-    ctx.traceIndented(s"deskolemize $tp, variance = $variance, seen = $seen  =  ") {
-    def approx(lo: Type = defn.NothingType, hi: Type = defn.AnyType, newSeen: Set[SkolemType] = seen) =
-      if (variance == 0) NoType
-      else deSkolemize(if (variance < 0) lo else hi, variance, newSeen)
-    tp match {
-      case tp: SkolemType =>
-        if (seen contains tp) NoType
-        else approx(hi = tp.binder, newSeen = seen + tp)
-      case tp: NamedType =>
-        val sym = tp.symbol
-        if (sym.isStatic) tp
-        else {
-          val pre1 = deSkolemize(tp.prefix, variance, seen)
-          if (pre1.exists && !pre1.isRef(defn.NothingClass)) tp.derivedSelect(pre1)
-          else {
-            ctx.log(s"deskolem: $tp: ${tp.info}")
-            tp.info match {
-              case TypeBounds(lo, hi) => approx(lo, hi)
-              case info => approx(defn.NothingType, info)
-            }
-          }
-        }
-      case _: ThisType | _: BoundType | _: SuperType | NoType | NoPrefix =>
-        tp
-      case tp: RefinedType =>
-        val parent1 = deSkolemize(tp.parent, variance, seen)
-        if (parent1.exists) {
-          val refinedInfo1 = deSkolemize(tp.refinedInfo, variance, seen)
-          if (refinedInfo1.exists)
-            tp.derivedRefinedType(parent1, tp.refinedName, refinedInfo1)
-          else
-            approx(hi = parent1)
-        }
-        else approx()
-      case tp: TypeAlias =>
-        val alias1 = deSkolemize(tp.alias, variance * tp.variance, seen)
-        if (alias1.exists) tp.derivedTypeAlias(alias1)
-        else approx(hi = TypeBounds.empty)
-      case tp: TypeBounds =>
-        val lo1 = deSkolemize(tp.lo, -variance, seen)
-        val hi1 = deSkolemize(tp.hi, variance, seen)
-        if (lo1.exists && hi1.exists) tp.derivedTypeBounds(lo1, hi1)
-        else approx(hi =
-          if (lo1.exists) TypeBounds.lower(lo1)
-          else if (hi1.exists) TypeBounds.upper(hi1)
-          else TypeBounds.empty)
-      case tp: ClassInfo =>
-        val pre1 = deSkolemize(tp.prefix, variance, seen)
-        if (pre1.exists) tp.derivedClassInfo(pre1)
-        else NoType
-      case tp: AndOrType =>
-        val tp1d = deSkolemize(tp.tp1, variance, seen)
-        val tp2d = deSkolemize(tp.tp2, variance, seen)
-        if (tp1d.exists && tp2d.exists)
-          tp.derivedAndOrType(tp1d, tp2d)
-        else if (tp.isAnd)
-          approx(hi = tp1d & tp2d)  // if one of tp1d, tp2d exists, it is the result of tp1d & tp2d
-        else
-          approx(lo = tp1d & tp2d)
-      case tp: WildcardType =>
-        val bounds1 = deSkolemize(tp.optBounds, variance, seen)
-        if (bounds1.exists) tp.derivedWildcardType(bounds1)
-        else WildcardType
-      case _ =>
-        if (tp.isInstanceOf[MethodicType]) assert(variance != 0, tp)
-        deSkolemizeMap.mapOver(tp, variance, seen)
-    }
-  }
-
-  object deSkolemizeMap extends TypeMap {
-    private var seen: Set[SkolemType] = _
-    def apply(tp: Type) = deSkolemize(tp, variance, seen)
-    def mapOver(tp: Type, variance: Int, seen: Set[SkolemType]) = {
-      val savedVariance = this.variance
-      val savedSeen = this.seen
-      this.variance = variance
-      this.seen = seen
-      try super.mapOver(tp)
-      finally {
-        this.variance = savedVariance
-        this.seen = savedSeen
-      }
-    }
-  }
-}
diff --git a/src/dotty/tools/dotc/core/Substituters.scala b/src/dotty/tools/dotc/core/Substituters.scala
index 77ecf7fba..e4bbf2305 100644
--- a/src/dotty/tools/dotc/core/Substituters.scala
+++ b/src/dotty/tools/dotc/core/Substituters.scala
@@ -179,21 +179,21 @@ trait Substituters { this: Context =>
           .mapOver(tp)
     }
 
-  final def substSkolem(tp: Type, from: Type, to: Type, theMap: SubstSkolemMap): Type =
+  final def substRefinedThis(tp: Type, from: Type, to: Type, theMap: SubstRefinedThisMap): Type =
     tp match {
-      case tp @ SkolemType(binder) =>
+      case tp @ RefinedThis(binder) =>
         if (binder eq from) to else tp
       case tp: NamedType =>
         if (tp.currentSymbol.isStatic) tp
-        else tp.derivedSelect(substSkolem(tp.prefix, from, to, theMap))
+        else tp.derivedSelect(substRefinedThis(tp.prefix, from, to, theMap))
       case _: ThisType | _: BoundType | NoPrefix =>
         tp
       case tp: RefinedType =>
-        tp.derivedRefinedType(substSkolem(tp.parent, from, to, theMap), tp.refinedName, substSkolem(tp.refinedInfo, from, to, theMap))
+        tp.derivedRefinedType(substRefinedThis(tp.parent, from, to, theMap), tp.refinedName, substRefinedThis(tp.refinedInfo, from, to, theMap))
       case tp: TypeAlias =>
-        tp.derivedTypeAlias(substSkolem(tp.alias, from, to, theMap))
+        tp.derivedTypeAlias(substRefinedThis(tp.alias, from, to, theMap))
       case _ =>
-        (if (theMap != null) theMap else new SubstSkolemMap(from, to))
+        (if (theMap != null) theMap else new SubstRefinedThisMap(from, to))
           .mapOver(tp)
     }
 
@@ -222,7 +222,7 @@ trait Substituters { this: Context =>
       case tp: NamedType =>
         if (tp.currentSymbol.isStatic) tp
         else tp.derivedSelect(substParams(tp.prefix, from, to, theMap))
-      case _: ThisType | NoPrefix | _: SkolemType =>
+      case _: ThisType | NoPrefix =>
         tp
       case tp: RefinedType =>
         tp.derivedRefinedType(substParams(tp.parent, from, to, theMap), tp.refinedName, substParams(tp.refinedInfo, from, to, theMap))
@@ -266,8 +266,8 @@ trait Substituters { this: Context =>
     def apply(tp: Type): Type = substThis(tp, from, to, this)
   }
 
-  final class SubstSkolemMap(from: Type, to: Type) extends DeepTypeMap {
-    def apply(tp: Type): Type = substSkolem(tp, from, to, this)
+  final class SubstRefinedThisMap(from: Type, to: Type) extends DeepTypeMap {
+    def apply(tp: Type): Type = substRefinedThis(tp, from, to, this)
   }
 
   final class SubstParamMap(from: ParamType, to: Type) extends DeepTypeMap {
diff --git a/src/dotty/tools/dotc/core/SymDenotations.scala b/src/dotty/tools/dotc/core/SymDenotations.scala
index d2b0d5030..17d80eb03 100644
--- a/src/dotty/tools/dotc/core/SymDenotations.scala
+++ b/src/dotty/tools/dotc/core/SymDenotations.scala
@@ -79,6 +79,7 @@ object SymDenotations {
       super.validFor_=(p)
     }
     */
+    if (Config.checkNoSkolemsInInfo) assertNoSkolems(initInfo)
 
     // ------ Getting and setting fields -----------------------------
 
@@ -168,8 +169,8 @@ object SymDenotations {
     }
 
     protected[dotc] final def info_=(tp: Type) = {
-      /*
-      def illegal: String = s"illegal type for $this: $tp"
+      /* // DEBUG
+       def illegal: String = s"illegal type for $this: $tp"
       if (this is Module) // make sure module invariants that allow moduleClass and sourceModule to work are kept.
         tp match {
           case tp: ClassInfo => assert(tp.selfInfo.isInstanceOf[TermRefBySym], illegal)
@@ -178,6 +179,7 @@ object SymDenotations {
           case _ =>
         }
         */
+      if (Config.checkNoSkolemsInInfo) assertNoSkolems(initInfo)
       myInfo = tp
     }
 
@@ -1049,8 +1051,28 @@ object SymDenotations {
       s"$kindString $name"
     }
 
+    // ----- Sanity checks and debugging */
+
     def debugString = toString + "#" + symbol.id // !!! DEBUG
 
+        def hasSkolems(tp: Type): Boolean = tp match {
+      case tp: SkolemType => true
+      case tp: NamedType => hasSkolems(tp.prefix)
+      case tp: RefinedType => hasSkolems(tp.parent) || hasSkolems(tp.refinedInfo)
+      case tp: PolyType => tp.paramBounds.exists(hasSkolems) || hasSkolems(tp.resType)
+      case tp: MethodType => tp.paramTypes.exists(hasSkolems) || hasSkolems(tp.resType)
+      case tp: ExprType => hasSkolems(tp.resType)
+      case tp: AndOrType => hasSkolems(tp.tp1) || hasSkolems(tp.tp2)
+      case tp: TypeBounds => hasSkolems(tp.lo) || hasSkolems(tp.hi)
+      case tp: AnnotatedType => hasSkolems(tp.tpe)
+      case tp: TypeVar => hasSkolems(tp.inst)
+      case _ => false
+    }
+
+    def assertNoSkolems(tp: Type) =
+      if (!this.isSkolem)
+        assert(!hasSkolems(tp), s"assigning type $tp containing skolems to $this")
+
     // ----- copies and transforms  ----------------------------------------
 
     protected def newLikeThis(s: Symbol, i: Type): SingleDenotation = new UniqueRefDenotation(s, i, validFor)
diff --git a/src/dotty/tools/dotc/core/TypeApplications.scala b/src/dotty/tools/dotc/core/TypeApplications.scala
index 7f3f8a446..f466cee77 100644
--- a/src/dotty/tools/dotc/core/TypeApplications.scala
+++ b/src/dotty/tools/dotc/core/TypeApplications.scala
@@ -387,9 +387,9 @@ class TypeApplications(val self: Type) extends AnyVal {
     case _ => firstBaseArgInfo(defn.SeqClass)
   }
 
-  def containsSkolemType(target: Type)(implicit ctx: Context): Boolean = {
+  def containsRefinedThis(target: Type)(implicit ctx: Context): Boolean = {
     def recur(tp: Type): Boolean = tp.stripTypeVar match {
-      case SkolemType(tp) =>
+      case RefinedThis(tp) =>
         tp eq target
       case tp: NamedType =>
         tp.info match {
@@ -446,7 +446,7 @@ class TypeApplications(val self: Type) extends AnyVal {
 
        def replacements(rt: RefinedType): List[Type] =
           for (sym <- boundSyms)
-            yield TypeRef(SkolemType(rt), correspondingParamName(sym))
+            yield TypeRef(RefinedThis(rt), correspondingParamName(sym))
 
         def rewrite(tp: Type): Type = tp match {
           case tp @ RefinedType(parent, name: TypeName) =>
@@ -489,7 +489,7 @@ class TypeApplications(val self: Type) extends AnyVal {
       val lambda = defn.lambdaTrait(boundSyms.map(_.variance))
       val substitutedRHS = (rt: RefinedType) => {
         val argRefs = boundSyms.indices.toList.map(i =>
-          SkolemType(rt).select(tpnme.lambdaArgName(i)))
+          RefinedThis(rt).select(tpnme.lambdaArgName(i)))
         tp.subst(boundSyms, argRefs).bounds.withVariance(1)
       }
       val res = RefinedType(lambda.typeRef, tpnme.Apply, substitutedRHS)
diff --git a/src/dotty/tools/dotc/core/TypeComparer.scala b/src/dotty/tools/dotc/core/TypeComparer.scala
index 069525db0..ea815f6c0 100644
--- a/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -16,7 +16,7 @@ import scala.util.control.NonFatal
 
 /** Provides methods to compare types.
  */
-class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling with Skolemization {
+class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
   implicit val ctx: Context = initctx
 
   val state = ctx.typerState
@@ -276,7 +276,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling wi
       }
     case tp1: SkolemType =>
       tp2 match {
-        case tp2: SkolemType if tp1 == tp2 => true
+        case tp2: SkolemType if !ctx.phase.isTyper && tp1.info <:< tp2.info => true
         case _ => thirdTry(tp1, tp2)
       }
     case tp1: TypeVar =>
@@ -536,18 +536,16 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling wi
    *  rebase both itself and the member info of `tp` on a freshly created skolem type.
    */
   protected def hasMatchingMember(name: Name, tp1: Type, tp2: RefinedType): Boolean = {
-    val saved = skolemsOutstanding
-    try {
-      val rebindNeeded = tp2.refinementRefersToThis
-      val base = if (rebindNeeded) ensureStableSingleton(tp1) else tp1
-      val rinfo2 = if (rebindNeeded) tp2.refinedInfo.substSkolem(tp2, base) else tp2.refinedInfo
-      def qualifies(m: SingleDenotation) = isSubType(m.info, rinfo2)
-      def memberMatches(mbr: Denotation): Boolean = mbr match { // inlined hasAltWith for performance
-        case mbr: SingleDenotation => qualifies(mbr)
-        case _ => mbr hasAltWith qualifies
-      }
-      /*>|>*/ ctx.traceIndented(i"hasMatchingMember($base . $name :? ${tp2.refinedInfo}) ${base.member(name).info.show} $rinfo2", subtyping) /*<|<*/ {
-        memberMatches(base member name) ||
+    val rebindNeeded = tp2.refinementRefersToThis
+    val base = if (rebindNeeded) ensureStableSingleton(tp1) else tp1
+    val rinfo2 = if (rebindNeeded) tp2.refinedInfo.substRefinedThis(tp2, base) else tp2.refinedInfo
+    def qualifies(m: SingleDenotation) = isSubType(m.info, rinfo2)
+    def memberMatches(mbr: Denotation): Boolean = mbr match { // inlined hasAltWith for performance
+      case mbr: SingleDenotation => qualifies(mbr)
+      case _ => mbr hasAltWith qualifies
+    }
+    /*>|>*/ ctx.traceIndented(i"hasMatchingMember($base . $name :? ${tp2.refinedInfo}) ${base.member(name).info.show} $rinfo2", subtyping) /*<|<*/ {
+      memberMatches(base member name) ||
         tp1.isInstanceOf[SingletonType] &&
         { // special case for situations like:
           //    class C { type T }
@@ -558,9 +556,13 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling wi
             case _ => false
           }
         }
-      }
     }
-    finally skolemsOutstanding = saved
+  }
+
+  final def ensureStableSingleton(tp: Type): SingletonType = tp.stripTypeVar match {
+    case tp: SingletonType if tp.isStable => tp
+    case tp: ValueType => SkolemType(tp)
+    case tp: TypeProxy => ensureStableSingleton(tp.underlying)
   }
 
   /** Skip refinements in `tp2` which match corresponding refinements in `tp1`.
@@ -645,13 +647,12 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling wi
   private def narrowGADTBounds(tr: NamedType, bound: Type, isUpper: Boolean): Boolean =
     ctx.mode.is(Mode.GADTflexible) && {
     val tparam = tr.symbol
-    val bound1 = deSkolemize(bound, toSuper = !isUpper)
-    typr.println(s"narrow gadt bound of $tparam: ${tparam.info} from ${if (isUpper) "above" else "below"} to $bound1 ${bound1.isRef(tparam)}")
-    !bound1.isRef(tparam) && {
+    typr.println(s"narrow gadt bound of $tparam: ${tparam.info} from ${if (isUpper) "above" else "below"} to $bound ${bound.isRef(tparam)}")
+    !bound.isRef(tparam) && {
       val oldBounds = ctx.gadt.bounds(tparam)
       val newBounds =
-        if (isUpper) TypeBounds(oldBounds.lo, oldBounds.hi & bound1)
-        else TypeBounds(oldBounds.lo | bound1, oldBounds.hi)
+        if (isUpper) TypeBounds(oldBounds.lo, oldBounds.hi & bound)
+        else TypeBounds(oldBounds.lo | bound, oldBounds.hi)
       isSubType(newBounds.lo, newBounds.hi) &&
       { ctx.gadt.setBounds(tparam, newBounds); true }
     }
diff --git a/src/dotty/tools/dotc/core/TypeOps.scala b/src/dotty/tools/dotc/core/TypeOps.scala
index acbd5b6f0..2b2ef83a2 100644
--- a/src/dotty/tools/dotc/core/TypeOps.scala
+++ b/src/dotty/tools/dotc/core/TypeOps.scala
@@ -12,16 +12,61 @@ import ast.tpd._
 
 trait TypeOps { this: Context => // TODO: Make standalone object.
 
-  final def asSeenFrom(tp: Type, pre: Type, cls: Symbol, theMap: AsSeenFromMap): Type = {
+  /** 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 it's 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. We must skolemize if an unstable prefix is used in nonvariant or
+   *  contravariant position of the return type of asSeenFrom.
+   *
+   *  In the implementation of asSeenFrom, we first try to run asSeenFrom without
+   *  skolemizing. If that would be incorrect we will be told by the fact that
+   *  `unstable` is set in the passed AsSeenFromMap. In that case we run asSeenFrom
+   *  again with a skolemized prefix.
+   *
+   *  In the interest of speed we want to avoid creating an AsSeenFromMap every time
+   *  asSeenFrom is called. So we do this here only if the prefix is unstable
+   *  (because then we need the map as a container for the unstable field). For
+   *  stable prefixes the map is `null`; it might however be instantiated later
+   *  for more complicated types.
+   */
+  final def asSeenFrom(tp: Type, pre: Type, cls: Symbol): Type = {
+    val m = if (pre.isStable || !ctx.phase.isTyper) null else new AsSeenFromMap(pre, cls)
+    var res = asSeenFrom(tp, pre, cls, m)
+    if (m != null && m.unstable) asSeenFrom(tp, SkolemType(pre), cls) else res
+  }
 
+  /** 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 if (thiscls.derivesFrom(cls) && pre.baseTypeRef(thiscls).exists)
+      else if (thiscls.derivesFrom(cls) && pre.baseTypeRef(thiscls).exists) {
+        if (theMap != null && theMap.currentVariance <= 0 && !pre.isStable)
+          theMap.unstable = true
         pre match {
           case SuperType(thispre, _) => thispre
           case _ => pre
         }
+      }
       else if ((pre.termSymbol is Package) && !(thiscls is Package))
         toPrefix(pre.select(nme.PACKAGE), cls, thiscls)
       else
@@ -33,7 +78,20 @@ trait TypeOps { this: Context => // TODO: Make standalone object.
         case tp: NamedType =>
           val sym = tp.symbol
           if (sym.isStatic) tp
-          else tp.derivedSelect(asSeenFrom(tp.prefix, pre, cls, theMap))
+          else {
+            val prevStable = theMap == null || !theMap.unstable
+            val pre1 = asSeenFrom(tp.prefix, pre, cls, theMap)
+            if (theMap != null && theMap.unstable && prevStable) {
+              pre1.member(tp.name).info match {
+                case TypeAlias(alias) =>
+                  // try to follow aliases of this will avoid skolemization.
+                  theMap.unstable = false
+                  return alias
+                case _ =>
+              }
+            }
+            tp.derivedSelect(pre1)
+          }
         case tp: ThisType =>
           toPrefix(pre, cls, tp.cls)
         case _: BoundType | NoPrefix =>
@@ -43,7 +101,7 @@ trait TypeOps { this: Context => // TODO: Make standalone object.
             asSeenFrom(tp.parent, pre, cls, theMap),
             tp.refinedName,
             asSeenFrom(tp.refinedInfo, pre, cls, theMap))
-        case tp: TypeAlias  =>
+        case tp: TypeAlias if theMap == null => // if theMap exists, need to do the variance calculation
           tp.derivedTypeAlias(asSeenFrom(tp.alias, pre, cls, theMap))
         case _ =>
           (if (theMap != null) theMap else new AsSeenFromMap(pre, cls))
@@ -52,8 +110,114 @@ trait TypeOps { this: Context => // TODO: Make standalone object.
     }
   }
 
+  /** 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
+
+    /** A field which indicates whether an unstable argument in nonvariant
+     *  or contravariant position was encountered.
+     */
+    var unstable = false
+  }
+
+  /** Approximate a type `tp` with a type that does not contain skolem types.
+   */
+  final def deskolemize(tp: Type): Type = deskolemize(tp, 1, Set())
+
+  private def deskolemize(tp: Type, variance: Int, seen: Set[SkolemType]): Type = {
+    def approx(lo: Type = defn.NothingType, hi: Type = defn.AnyType, newSeen: Set[SkolemType] = seen) =
+      if (variance == 0) NoType
+      else deskolemize(if (variance < 0) lo else hi, variance, newSeen)
+    tp match {
+      case tp: SkolemType =>
+        if (seen contains tp) NoType
+        else approx(hi = tp.info, newSeen = seen + tp)
+      case tp: NamedType =>
+        val sym = tp.symbol
+        if (sym.isStatic) tp
+        else {
+          val pre1 = deskolemize(tp.prefix, variance, seen)
+          if (pre1 eq tp.prefix) tp
+          else {
+            val d = tp.prefix.member(tp.name)
+            d.info match {
+              case TypeAlias(alias) => deskolemize(alias, variance, seen)
+              case _ =>
+                if (pre1.exists && !pre1.isRef(defn.NothingClass)) tp.derivedSelect(pre1)
+                else {
+                  ctx.log(s"deskolem: $tp: ${tp.info}")
+                  tp.info match {
+                    case TypeBounds(lo, hi) => approx(lo, hi)
+                    case info => approx(defn.NothingType, info)
+                  }
+                }
+            }
+          }
+        }
+      case _: ThisType | _: BoundType | _: SuperType | NoType | NoPrefix =>
+        tp
+      case tp: RefinedType =>
+        val parent1 = deskolemize(tp.parent, variance, seen)
+        if (parent1.exists) {
+          val refinedInfo1 = deskolemize(tp.refinedInfo, variance, seen)
+          if (refinedInfo1.exists)
+            tp.derivedRefinedType(parent1, tp.refinedName, refinedInfo1)
+          else
+            approx(hi = parent1)
+        }
+        else approx()
+      case tp: TypeAlias =>
+        val alias1 = deskolemize(tp.alias, variance * tp.variance, seen)
+        if (alias1.exists) tp.derivedTypeAlias(alias1)
+        else approx(hi = TypeBounds.empty)
+      case tp: TypeBounds =>
+        val lo1 = deskolemize(tp.lo, -variance, seen)
+        val hi1 = deskolemize(tp.hi, variance, seen)
+        if (lo1.exists && hi1.exists) tp.derivedTypeBounds(lo1, hi1)
+        else approx(hi =
+          if (lo1.exists) TypeBounds.lower(lo1)
+          else if (hi1.exists) TypeBounds.upper(hi1)
+          else TypeBounds.empty)
+      case tp: ClassInfo =>
+        val pre1 = deskolemize(tp.prefix, variance, seen)
+        if (pre1.exists) tp.derivedClassInfo(pre1)
+        else NoType
+      case tp: AndOrType =>
+        val tp1d = deskolemize(tp.tp1, variance, seen)
+        val tp2d = deskolemize(tp.tp2, variance, seen)
+        if (tp1d.exists && tp2d.exists)
+          tp.derivedAndOrType(tp1d, tp2d)
+        else if (tp.isAnd)
+          approx(hi = tp1d & tp2d)  // if one of tp1d, tp2d exists, it is the result of tp1d & tp2d
+        else
+          approx(lo = tp1d & tp2d)
+      case tp: WildcardType =>
+        val bounds1 = deskolemize(tp.optBounds, variance, seen)
+        if (bounds1.exists) tp.derivedWildcardType(bounds1)
+        else WildcardType
+      case _ =>
+        if (tp.isInstanceOf[MethodicType]) assert(variance != 0, tp)
+        deskolemizeMap.mapOver(tp, variance, seen)
+    }
+  }
+
+  object deskolemizeMap extends TypeMap {
+    private var seen: Set[SkolemType] = _
+    def apply(tp: Type) = deskolemize(tp, variance, seen)
+    def mapOver(tp: Type, variance: Int, seen: Set[SkolemType]) = {
+      val savedVariance = this.variance
+      val savedSeen = this.seen
+      this.variance = variance
+      this.seen = seen
+      try super.mapOver(tp)
+      finally {
+        this.variance = savedVariance
+        this.seen = savedSeen
+      }
+    }
   }
 
   /** Implementation of Types#simplified */
diff --git a/src/dotty/tools/dotc/core/Types.scala b/src/dotty/tools/dotc/core/Types.scala
index ae9088f00..ba39e7bef 100644
--- a/src/dotty/tools/dotc/core/Types.scala
+++ b/src/dotty/tools/dotc/core/Types.scala
@@ -48,6 +48,7 @@ object Types {
    *        |              |                +--- SuperType
    *        |              |                +--- ConstantType
    *        |              |                +--- MethodParam
+   *        |              |                +----RefinedThis
    *        |              |                +--- SkolemType
    *        |              +- PolyParam
    *        |              +- RefinedType
@@ -89,9 +90,10 @@ object Types {
     final def isValueType: Boolean = this.isInstanceOf[ValueType]
 
     /** Does this type denote a stable reference (i.e. singleton type)? */
-    final def isStable(implicit ctx: Context): Boolean = this match {
-      case tp: TermRef => tp.termSymbol.isStable
+    final def isStable(implicit ctx: Context): Boolean = stripTypeVar match {
+      case tp: TermRef => tp.termSymbol.isStable && tp.prefix.isStable
       case _: SingletonType => true
+      case tp: RefinedType => tp.parent.isStable
       case NoPrefix => true
       case _ => false
     }
@@ -154,18 +156,6 @@ object Types {
         false
     }
 
-    /** A type T is a legal prefix in a type selection T#A if
-     *  T is stable or T contains no abstract types except possibly A.
-     *  !!! Todo: What about non-final vals that contain abstract types?
-     */
-    final def isLegalPrefixFor(selector: Name)(implicit ctx: Context): Boolean =
-      isStable || {
-        val absTypeNames = memberNames(abstractTypeNameFilter)
-        if (absTypeNames.nonEmpty) typr.println(s"abstract type members of ${this.showWithUnderlying()}: $absTypeNames")
-        absTypeNames.isEmpty ||
-          absTypeNames.head == selector && absTypeNames.tail.isEmpty
-      }
-
     /** Is this type guaranteed not to have `null` as a value?
      *  For the moment this is only true for modules, but it could
      *  be refined later.
@@ -449,7 +439,7 @@ object Types {
       def goRefined(tp: RefinedType) = {
         val pdenot = go(tp.parent)
         val rinfo =
-          if (tp.refinementRefersToThis) tp.refinedInfo.substSkolem(tp, pre)
+          if (tp.refinementRefersToThis) tp.refinedInfo.substRefinedThis(tp, pre)
           else tp.refinedInfo
         if (name.isTypeName) { // simplified case that runs more efficiently
           val jointInfo =
@@ -594,7 +584,7 @@ object Types {
      */
     final def asSeenFrom(pre: Type, cls: Symbol)(implicit ctx: Context): Type = track("asSeenFrom") {
       if (!cls.membersNeedAsSeenFrom(pre)) this
-      else ctx.asSeenFrom(this, pre, cls, null)
+      else ctx.asSeenFrom(this, pre, cls)
     }
 
 // ----- Subtype-related --------------------------------------------
@@ -833,7 +823,7 @@ object Types {
           object instantiate extends TypeMap {
             var isSafe = true
             def apply(tp: Type): Type = tp match {
-              case TypeRef(SkolemType(`pre`), name) if name.isLambdaArgName =>
+              case TypeRef(RefinedThis(`pre`), name) if name.isLambdaArgName =>
                 val TypeAlias(alias) = member(name).info
                 alias
               case tp: TypeVar if !tp.inst.exists =>
@@ -856,13 +846,15 @@ object Types {
               if (pre.refinedName ne name) loop(pre.parent, pre.refinedName :: resolved)
               else if (!pre.refinementRefersToThis) alias
               else alias match {
-                case TypeRef(SkolemType(`pre`), aliasName) => lookupRefined(aliasName) // (1)
+                case TypeRef(RefinedThis(`pre`), aliasName) => lookupRefined(aliasName) // (1)
                 case _ => if (name == tpnme.Apply) betaReduce(alias) else NoType // (2)
               }
             case _ => loop(pre.parent, resolved)
           }
-        case SkolemType(binder) =>
+        case RefinedThis(binder) =>
           binder.lookupRefined(name)
+        case SkolemType(tp) =>
+          tp.lookupRefined(name)
         case pre: WildcardType =>
           WildcardType
         case pre: TypeRef =>
@@ -1035,8 +1027,8 @@ object Types {
       if (cls.isStaticOwner) this else ctx.substThis(this, cls, tp, null)
 
     /** Substitute all occurrences of `SkolemType(binder)` by `tp` */
-    final def substSkolem(binder: Type, tp: Type)(implicit ctx: Context): Type =
-      ctx.substSkolem(this, binder, tp, null)
+    final def substRefinedThis(binder: Type, tp: Type)(implicit ctx: Context): Type =
+      ctx.substRefinedThis(this, binder, tp, null)
 
     /** Substitute a bound type by some other type */
     final def substParam(from: ParamType, to: Type)(implicit ctx: Context): Type =
@@ -1413,7 +1405,7 @@ object Types {
      *  to an (unbounded) wildcard type.
      *
      *  (2) Reduce a type-ref `T { X = U; ... } # X`  to   `U`
-     *  provided `U` does not refer with a SkolemType to the
+     *  provided `U` does not refer with a RefinedThis to the
      *  refinement type `T { X = U; ... }`
      */
     def reduceProjection(implicit ctx: Context): Type = {
@@ -1827,7 +1819,7 @@ object Types {
 
     def refinementRefersToThis(implicit ctx: Context): Boolean = {
       if (!refinementRefersToThisKnown) {
-        refinementRefersToThisCache = refinedInfo.containsSkolemType(this)
+        refinementRefersToThisCache = refinedInfo.containsRefinedThis(this)
         refinementRefersToThisKnown = true
       }
       refinementRefersToThisCache
@@ -1863,7 +1855,7 @@ object Types {
         derivedRefinedType(parent.EtaExpand, refinedName, refinedInfo)
       else
         if (false) RefinedType(parent, refinedName, refinedInfo)
-        else RefinedType(parent, refinedName, rt => refinedInfo.substSkolem(this, SkolemType(rt)))
+        else RefinedType(parent, refinedName, rt => refinedInfo.substRefinedThis(this, RefinedThis(rt)))
     }
 
     /** Add this refinement to `parent`, provided If `refinedName` is a member of `parent`. */
@@ -2019,7 +2011,7 @@ object Types {
     def isJava = false
     def isImplicit = false
 
-    private val resType = resultTypeExp(this)
+    private[core] val resType = resultTypeExp(this)
     assert(resType.exists)
 
     override def resultType(implicit ctx: Context): Type =
@@ -2247,7 +2239,7 @@ object Types {
       }
   }
 
-  // ----- Bound types: MethodParam, PolyParam, SkolemType --------------------------
+  // ----- Bound types: MethodParam, PolyParam, RefinedThis --------------------------
 
   abstract class BoundType extends CachedProxyType with ValueType {
     type BT <: Type
@@ -2320,20 +2312,39 @@ object Types {
     }
   }
 
-  /** A skolem type reference with underlying type `binder`. */
-  case class SkolemType(binder: Type) extends BoundType with SingletonType {
-    type BT = Type
+  /** a this-reference to an enclosing refined type `binder`. */
+  case class RefinedThis(binder: RefinedType) extends BoundType with SingletonType {
+    type BT = RefinedType
     override def underlying(implicit ctx: Context) = binder
-    def copyBoundType(bt: BT) = SkolemType(bt)
+    def copyBoundType(bt: BT) = RefinedThis(bt)
 
     // need to customize hashCode and equals to prevent infinite recursion for
     // refinements that refer to the refinement type via this
     override def computeHash = addDelta(binder.identityHash, 41)
     override def equals(that: Any) = that match {
-      case that: SkolemType => this.binder eq that.binder
+      case that: RefinedThis => this.binder eq that.binder
       case _ => false
     }
-    override def toString = s"SkolemType(${binder.hashCode})"
+    override def toString = s"RefinedThis(${binder.hashCode})"
+  }
+
+  // ----- Skolem types -----------------------------------------------
+
+  /** A skolem type reference with underlying type `binder`. */
+  abstract case class SkolemType(info: Type) extends CachedProxyType with ValueType with SingletonType {
+    override def underlying(implicit ctx: Context) = info
+    def derivedSkolemType(info: Type)(implicit ctx: Context) =
+      if (info eq this.info) this else SkolemType(info)
+    override def computeHash: Int = identityHash
+    override def equals(that: Any) = this eq that.asInstanceOf[AnyRef]
+    override def toString = s"Skolem($info)"
+  }
+
+  final class CachedSkolemType(info: Type) extends SkolemType(info)
+
+  object SkolemType {
+    def apply(info: Type)(implicit ctx: Context) =
+      unique(new CachedSkolemType(info))
   }
 
   // ------------ Type variables ----------------------------------------
@@ -2894,6 +2905,9 @@ object Types {
         case tp: AndOrType =>
           tp.derivedAndOrType(this(tp.tp1), this(tp.tp2))
 
+        case tp: SkolemType =>
+          tp.derivedSkolemType(this(tp.info))
+
         case tp @ AnnotatedType(annot, underlying) =>
           val underlying1 = this(underlying)
           if (underlying1 eq underlying) tp else tp.derivedAnnotatedType(mapOver(annot), underlying1)
@@ -3033,6 +3047,9 @@ object Types {
       case tp: AndOrType =>
         this(this(x, tp.tp1), tp.tp2)
 
+      case tp: SkolemType =>
+        this(x, tp.info)
+
       case AnnotatedType(annot, underlying) =>
         this(applyToAnnot(x, annot), underlying)
 
diff --git a/src/dotty/tools/dotc/core/tasty/TastyFormat.scala b/src/dotty/tools/dotc/core/tasty/TastyFormat.scala
index 106a6510d..1022fc4da 100644
--- a/src/dotty/tools/dotc/core/tasty/TastyFormat.scala
+++ b/src/dotty/tools/dotc/core/tasty/TastyFormat.scala
@@ -103,10 +103,10 @@ Standard-Section: "ASTs" TopLevelStat*
                   TERMREFpkg            fullyQualified_NameRef
                   TERMREF               possiblySigned_NameRef qual_Type
                   THIS                  clsRef_Type
-                  SKOLEMtype            refinedType_ASTRef
+                  REFINEDthis           refinedType_ASTRef
+                  SKOLEMtype            Type_ASTRef
                   SHARED                path_ASTRef
 
-
   Constant      = UNITconst
                   FALSEconst
                   TRUEconst
@@ -262,15 +262,16 @@ object TastyFormat {
   final val TERMREFpkg = 67
   final val TYPEREFpkg = 68
   final val SKOLEMtype = 69
-  final val BYTEconst = 70
-  final val SHORTconst = 71
-  final val CHARconst = 72
-  final val INTconst = 73
-  final val LONGconst = 74
-  final val FLOATconst = 75
-  final val DOUBLEconst = 76
-  final val STRINGconst = 77
-  final val IMPORTED = 78
+  final val REFINEDthis = 70
+  final val BYTEconst = 71
+  final val SHORTconst = 72
+  final val CHARconst = 73
+  final val INTconst = 74
+  final val LONGconst = 75
+  final val FLOATconst = 76
+  final val DOUBLEconst = 77
+  final val STRINGconst = 78
+  final val IMPORTED = 79
 
   final val THIS = 96
   final val CLASSconst = 97
diff --git a/src/dotty/tools/dotc/core/tasty/TreePickler.scala b/src/dotty/tools/dotc/core/tasty/TreePickler.scala
index 365b5d268..cd49f7c5a 100644
--- a/src/dotty/tools/dotc/core/tasty/TreePickler.scala
+++ b/src/dotty/tools/dotc/core/tasty/TreePickler.scala
@@ -198,9 +198,12 @@ class TreePickler(pickler: TastyPickler) {
       case tpe: SuperType =>
         writeByte(SUPERtype)
         withLength { pickleType(tpe.thistpe); pickleType(tpe.supertpe)}
+      case tpe: RefinedThis =>
+        writeByte(REFINEDthis)
+        writeRef(pickledTypes.get(tpe.binder).asInstanceOf[Addr])
       case tpe: SkolemType =>
         writeByte(SKOLEMtype)
-        writeRef(pickledTypes.get(tpe.binder).asInstanceOf[Addr])
+        pickleType(tpe.info)
       case tpe: RefinedType =>
         val args = tpe.argInfos(interpolate = false)
         if (args.isEmpty) {
diff --git a/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala b/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala
index e753bdcab..d4260e679 100644
--- a/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala
+++ b/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala
@@ -254,6 +254,8 @@ class TreeUnpickler(reader: TastyReader, tastyName: TastyName.Table) {
           }
         case THIS =>
           ThisType.raw(readType().asInstanceOf[TypeRef])
+        case REFINEDthis =>
+          RefinedThis(readTypeRef().asInstanceOf[RefinedType])
         case SKOLEMtype =>
           SkolemType(readTypeRef())
         case SHARED =>
diff --git a/src/dotty/tools/dotc/core/unpickleScala2/Scala2Unpickler.scala b/src/dotty/tools/dotc/core/unpickleScala2/Scala2Unpickler.scala
index b4549a8d8..9498cf43c 100644
--- a/src/dotty/tools/dotc/core/unpickleScala2/Scala2Unpickler.scala
+++ b/src/dotty/tools/dotc/core/unpickleScala2/Scala2Unpickler.scala
@@ -689,7 +689,7 @@ class Scala2Unpickler(bytes: Array[Byte], classRoot: ClassDenotation, moduleClas
         else {
           def addRefinement(tp: Type, sym: Symbol) = {
             def subst(info: Type, rt: RefinedType) =
-              if (clazz.isClass) info.substThis(clazz.asClass, SkolemType(rt))
+              if (clazz.isClass) info.substThis(clazz.asClass, RefinedThis(rt))
               else info // turns out some symbols read into `clazz` are not classes, not sure why this is the case.
             RefinedType(tp, sym.name, subst(sym.info, _))
           }
diff --git a/src/dotty/tools/dotc/printing/PlainPrinter.scala b/src/dotty/tools/dotc/printing/PlainPrinter.scala
index 12c94677f..a7b338be8 100644
--- a/src/dotty/tools/dotc/printing/PlainPrinter.scala
+++ b/src/dotty/tools/dotc/printing/PlainPrinter.scala
@@ -223,16 +223,15 @@ class PlainPrinter(_ctx: Context) extends Printer {
       case SuperType(thistpe: SingletonType, _) =>
         toTextRef(thistpe).map(_.replaceAll("""\bthis$""", "super"))
       case SuperType(thistpe, _) =>
-        "Super(" ~ toTextLocal(thistpe) ~ ")"
+        "Super(" ~ toTextGlobal(thistpe) ~ ")"
       case tp @ ConstantType(value) =>
         toText(value)
       case MethodParam(mt, idx) =>
         nameString(mt.paramNames(idx))
-      case sk: SkolemType =>
-        sk.binder match {
-          case rt: RefinedType => s"${nameString(rt.typeSymbol)}{...}.this"
-          case _ => "<skolem>"
-        }
+      case tp: RefinedThis =>
+        s"${nameString(tp.binder.typeSymbol)}{...}.this"
+      case tp: SkolemType =>
+        "<unknown instance of type " ~ toTextGlobal(tp.info) ~ ">"
     }
   }
 
diff --git a/src/dotty/tools/dotc/printing/RefinedPrinter.scala b/src/dotty/tools/dotc/printing/RefinedPrinter.scala
index fa238f32c..cf80969bf 100644
--- a/src/dotty/tools/dotc/printing/RefinedPrinter.scala
+++ b/src/dotty/tools/dotc/printing/RefinedPrinter.scala
@@ -190,7 +190,7 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
         // LambdaI{...}.HK$i
         val simplifyArgs = new TypeMap {
           override def apply(tp: Type) = tp match {
-            case tp @ TypeRef(SkolemType(_), name) if name.isLambdaArgName =>
+            case tp @ TypeRef(RefinedThis(_), name) if name.isLambdaArgName =>
               TypeRef(NoPrefix, tp.symbol.asType)
             case _ =>
               mapOver(tp)
diff --git a/src/dotty/tools/dotc/typer/Checking.scala b/src/dotty/tools/dotc/typer/Checking.scala
index b2d368e8c..3ef6d059a 100644
--- a/src/dotty/tools/dotc/typer/Checking.scala
+++ b/src/dotty/tools/dotc/typer/Checking.scala
@@ -252,12 +252,6 @@ trait Checking {
     if (!tp.isStable && !tp.isErroneous)
       ctx.error(d"$tp is not stable", pos)
 
-  /** Check that type `tp` is a legal prefix for '#'.
-   *  @return The type itself
-   */
-  def checkLegalPrefix(tp: Type, selector: Name, pos: Position)(implicit ctx: Context): Unit =
-    if (!tp.isLegalPrefixFor(selector)) ctx.error(d"$tp is not a valid prefix for '# $selector'", pos)
-
  /**  Check that `tp` is a class type with a stable prefix. Also, if `traitReq` is
    *  true check that `tp` is a trait.
    *  Stability checking is disabled in phases after RefChecks.
@@ -345,7 +339,6 @@ trait NoChecking extends Checking {
   override def checkValue(tree: Tree, proto: Type)(implicit ctx: Context): tree.type = tree
   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
   override def checkImplicitParamsNotSingletons(vparamss: List[List[ValDef]])(implicit ctx: Context): Unit = ()
   override def checkFeasible(tp: Type, pos: Position, where: => String = "")(implicit ctx: Context): Type = tp
diff --git a/src/dotty/tools/dotc/typer/FrontEnd.scala b/src/dotty/tools/dotc/typer/FrontEnd.scala
index 056a57215..3dda108b0 100644
--- a/src/dotty/tools/dotc/typer/FrontEnd.scala
+++ b/src/dotty/tools/dotc/typer/FrontEnd.scala
@@ -13,6 +13,7 @@ import scala.util.control.NonFatal
 class FrontEnd extends Phase {
 
   override def phaseName = "frontend"
+  override def isTyper = true
 
   def monitor(doing: String)(body: => Unit)(implicit ctx: Context) =
     try body
diff --git a/src/dotty/tools/dotc/typer/Namer.scala b/src/dotty/tools/dotc/typer/Namer.scala
index 10667f884..2e76d3171 100644
--- a/src/dotty/tools/dotc/typer/Namer.scala
+++ b/src/dotty/tools/dotc/typer/Namer.scala
@@ -677,7 +677,8 @@ class Namer { typer: Typer =>
       // println(s"final inherited for $sym: ${inherited.toString}") !!!
       // println(s"owner = ${sym.owner}, decls = ${sym.owner.info.decls.show}")
       val rhsCtx = ctx.fresh addMode Mode.InferringReturnType
-      def rhsType = typedAheadExpr(mdef.rhs, rhsProto)(rhsCtx).tpe.widen.approximateUnion
+      def rhsType = ctx.deskolemize(
+        typedAheadExpr(mdef.rhs, rhsProto)(rhsCtx).tpe.widen.approximateUnion)
       def lhsType = fullyDefinedType(rhsType, "right-hand side", mdef.pos)
       if (inherited.exists) inherited
       else {
diff --git a/src/dotty/tools/dotc/typer/Typer.scala b/src/dotty/tools/dotc/typer/Typer.scala
index acf4f3845..5f03d19e7 100644
--- a/src/dotty/tools/dotc/typer/Typer.scala
+++ b/src/dotty/tools/dotc/typer/Typer.scala
@@ -312,13 +312,12 @@ class Typer extends Namer with TypeAssigner with Applications with Implicits wit
     if (ctx.compilationUnit.isJava && tree.name.isTypeName) {
       // SI-3120 Java uses the same syntax, A.B, to express selection from the
       // value A and from the type A. We have to try both.
-      tryEither(tryCtx => asSelect(tryCtx))((_,_) => asJavaSelectFromTypeTree(ctx))
+      tryEither(tryCtx => asSelect(tryCtx))((_, _) => asJavaSelectFromTypeTree(ctx))
     } else asSelect(ctx)
   }
 
   def typedSelectFromTypeTree(tree: untpd.SelectFromTypeTree, pt: Type)(implicit ctx: Context): Tree = track("typedSelectFromTypeTree") {
     val qual1 = typedType(tree.qualifier, selectionProto(tree.name, pt, this))
-    checkLegalPrefix(qual1.tpe, tree.name, qual1.pos)
     assignType(cpy.SelectFromTypeTree(tree)(qual1, tree.name), qual1)
   }
 
@@ -347,8 +346,8 @@ class Typer extends Namer with TypeAssigner with Applications with Implicits wit
         val clsDef = TypeDef(x, templ).withFlags(Final)
         typed(cpy.Block(tree)(clsDef :: Nil, New(Ident(x), Nil)), pt)
       case _ =>
-          val tpt1 = typedType(tree.tpt)
-          checkClassTypeWithStablePrefix(tpt1.tpe, tpt1.pos, traitReq = false)
+        val tpt1 = typedType(tree.tpt)
+        checkClassTypeWithStablePrefix(tpt1.tpe, tpt1.pos, traitReq = false)
         assignType(cpy.New(tree)(tpt1), tpt1)
         // todo in a later phase: checkInstantiatable(cls, tpt1.pos)
     }
@@ -524,7 +523,6 @@ class Typer extends Namer with TypeAssigner with Applications with Implicits wit
        */
       var fnBody = tree.body
 
-
       /** If function is of the form
        *      (x1, ..., xN) => f(x1, ..., XN)
        *  the type of `f`, otherwise NoType. (updates `fnBody` as a side effect).
@@ -814,7 +812,7 @@ class Typer extends Namer with TypeAssigner with Applications with Implicits wit
       if ((rsym.is(Method) || rsym.isType) && rsym.allOverriddenSymbols.isEmpty)
         ctx.error(i"refinement $rsym without matching type in parent $parent", refinement.pos)
       val rinfo = if (rsym is Accessor) rsym.info.resultType else rsym.info
-      RefinedType(parent, rsym.name, rt => rinfo.substThis(refineCls, SkolemType(rt)))
+      RefinedType(parent, rsym.name, rt => rinfo.substThis(refineCls, RefinedThis(rt)))
       // todo later: check that refinement is within bounds
     }
     val res = cpy.RefinedTypeTree(tree)(tpt1, refinements1) withType
diff --git a/test/dotc/tests.scala b/test/dotc/tests.scala
index b017211a9..a7123602b 100644
--- a/test/dotc/tests.scala
+++ b/test/dotc/tests.scala
@@ -104,7 +104,6 @@ class tests extends CompilerTest {
   @Test def neg_companions = compileFile(negDir, "companions", xerrors = 1)
   @Test def neg_over = compileFile(negDir, "over", xerrors = 3)
   @Test def neg_overrides = compileFile(negDir, "overrides", xerrors = 11)
-  @Test def neg_projections = compileFile(negDir, "projections", xerrors = 1)
   @Test def neg_i39 = compileFile(negDir, "i39", xerrors = 2)
   @Test def neg_i50_volatile = compileFile(negDir, "i50-volatile", xerrors = 6)
   @Test def neg_t0273_doubledefs = compileFile(negDir, "t0273", xerrors = 1)
@@ -133,15 +132,14 @@ class tests extends CompilerTest {
   @Test def neg_i0091_infpaths = compileFile(negDir, "i0091-infpaths", xerrors = 3)
   @Test def neg_i0248_inherit_refined = compileFile(negDir, "i0248-inherit-refined", xerrors = 4)
   @Test def neg_i0281 = compileFile(negDir, "i0281-null-primitive-conforms", xerrors = 3)
+  @Test def neg_i583 = compileFile(negDir, "i0583-skolemize", xerrors = 2)
   @Test def neg_moduleSubtyping = compileFile(negDir, "moduleSubtyping", xerrors = 4)
   @Test def neg_escapingRefs = compileFile(negDir, "escapingRefs", xerrors = 2)
   @Test def neg_instantiateAbstract = compileFile(negDir, "instantiateAbstract", xerrors = 8)
   @Test def neg_selfInheritance = compileFile(negDir, "selfInheritance", xerrors = 5)
 
-
   @Test def run_all = runFiles(runDir)
 
-
   @Test def dotty = compileDir(dottyDir, "tools", "-deep" :: allowDeepSubtypes ++ twice) // note the -deep argument
 
 
diff --git a/tests/neg/i0583-skolemize.scala b/tests/neg/i0583-skolemize.scala
new file mode 100644
index 000000000..e0bb99e5d
--- /dev/null
+++ b/tests/neg/i0583-skolemize.scala
@@ -0,0 +1,27 @@
+import scala.collection.mutable.ListBuffer
+
+object Test1 {
+
+  class Box[T](x: T)
+  def box[T](x: T) = new Box[T](x)
+
+  class C[T] { def x: T = ???; def x_=(y: T): Unit = ??? }
+
+  val c: C[Int] = ???
+  val d: C[Float] = ???
+
+  val xs: List[C[_]] = List(c, d)
+
+  xs(0).x = xs(1).x
+
+}
+object Test {
+  def main(args: Array[String]): Unit = {
+    val f: ListBuffer[Int] = ListBuffer(1,2)
+    val g: ListBuffer[Double] = ListBuffer(3.0,4.0)
+    val lb: ListBuffer[ListBuffer[_]] = ListBuffer(f, g)
+    lb(0)(0) = lb(1)(0)
+    val x: Int = f(0)
+  }
+}
+
diff --git a/tests/neg/projections.scala b/tests/neg/projections.scala
deleted file mode 100644
index 5d80e1151..000000000
--- a/tests/neg/projections.scala
+++ /dev/null
@@ -1,7 +0,0 @@
-class projections {
-
-  class Lambda { type Arg; type Apply }
-
-  var x: (Lambda { type Apply = Int }) # Apply = _ // error: illegal prefix
-
-}
diff --git a/tests/pos/i583a.scala b/tests/pos/i583a.scala
new file mode 100644
index 000000000..a97a3998b
--- /dev/null
+++ b/tests/pos/i583a.scala
@@ -0,0 +1,20 @@
+object Test1 {
+
+  class Box[B](x: B)
+
+  class C {
+    type T
+    val box: Box[T] = ???
+    def f(x: T): T = ???
+    def x: T = ???
+  }
+
+  def c: C = new C
+
+  val b = c.box
+
+  val f = c.f _
+
+}
+
+