Reverting the idea that RefinedThis types take levels.

In the end, this did not buy us anything. What matters is that

 - we can reliably identify RefinedThis types pointing to a given
   refinement type. Making sure that the `binder` field of q RefinedThis
   type in a refinedInfo is always the containing refined type is good
   enough for that.

 - we take care to rebind RefinedThis types in isSubType. This was leaky before,
   is handled now better in the new isSubType.

So, in the end, adding a level was a needless complication. Also, as a next step
we should be able to identify skolem types and RefinedThis types.

8 files changed, 48 insertions, 163 deletions

diff --git a/src/dotty/tools/dotc/core/Substituters.scala b/src/dotty/tools/dotc/core/Substituters.scala
index 9fd01ab56..76264519f 100644
--- a/src/dotty/tools/dotc/core/Substituters.scala
+++ b/src/dotty/tools/dotc/core/Substituters.scala
@@ -183,13 +183,8 @@ trait Substituters { this: Context =>
   // the target type from RefinedThis.
   final def substThis0(tp: Type, from: RefinedType, to: Type, theMap: SubstRefinedThisMap0): Type =
     tp match {
-      case tp @ RefinedThis(rt, level) =>
-        if (rt eq from) 
-          to match { // !!! TODO drop
-            case RefinedThis(rt1, -1) => RefinedThis(rt1, level)
-            case _ => to
-          }
-        else tp
+      case tp @ RefinedThis(rt) =>
+        if (rt eq from) to else tp
       case tp: NamedType =>
         if (tp.currentSymbol.isStatic) tp
         else tp.derivedSelect(substThis0(tp.prefix, from, to, theMap))
@@ -202,29 +197,6 @@ trait Substituters { this: Context =>
       case _ =>
         (if (theMap != null) theMap else new SubstRefinedThisMap0(from, to))
           .mapOver(tp)
-    }      
-      
-    final def substRefinedThis(tp: Type, level: Int, to: Type, theMap: SubstRefinedThisMap): Type =
-    tp match {
-      case tp @ RefinedThis(rt, l) if l == level =>
-        to
-      case tp: NamedType =>
-        if (tp.currentSymbol.isStatic) tp
-        else tp.derivedSelect(substRefinedThis(tp.prefix, level, to, theMap))
-      case _: ThisType | _: BoundType | NoPrefix =>
-        tp
-      case tp: RefinedType =>
-        tp.derivedRefinedType(
-            substRefinedThis(tp.parent, level, to, theMap), tp.refinedName, 
-            substRefinedThis(tp.refinedInfo, level + 1, to, theMap))
-      case tp: TypeAlias =>
-        tp.derivedTypeAlias(substRefinedThis(tp.alias, level, to, theMap))
-      case _ =>
-        val m = if (theMap != null) theMap else new SubstRefinedThisMap(to)
-        val saved = m.level
-        m.level = level
-        try m.mapOver(tp)
-        finally m.level = saved
     }
 
   final def substParam(tp: Type, from: ParamType, to: Type, theMap: SubstParamMap): Type =
@@ -300,11 +272,6 @@ trait Substituters { this: Context =>
     def apply(tp: Type): Type = substThis0(tp, from, to, this)
   }
 
-  final class SubstRefinedThisMap(to: Type) extends DeepTypeMap {
-    var level: Int = 0
-    def apply(tp: Type): Type = substRefinedThis(tp, level, to, this)
-  }
-
   final class SubstParamMap(from: ParamType, to: Type) extends DeepTypeMap {
     def apply(tp: Type) = substParam(tp, from, to, this)
   }
@@ -312,38 +279,4 @@ trait Substituters { this: Context =>
   final class SubstParamsMap(from: BindingType, to: List[Type]) extends DeepTypeMap {
     def apply(tp: Type) = substParams(tp, from, to, this)
   }
-
-  /** Substitute every occurrence of symbol `from_i` with `RefinedThis(leve).select(to_i)`
-   *  where level represents the nesting level of the occurrence (i.e. number
-   *  of refinedInfos between substituted type and the occurrence.
-   *  TODO: Drop `rt` once it is dropped from RefinedThis
-   *  TODO: Apply to enclosing refined type instead of refined info. That way we
-   *        can optimize for types not containing any RefinedThis
-   */
-  final class SubstWithRefinedSelectMap(rt: RefinedType, from: List[Symbol], to: List[TypeName]) extends DeepTypeMap {
-    private var level = 0
-    def apply(tp: Type): Type = tp match {
-      case tp: NamedType =>
-        val sym = tp.symbol
-        var fs = from
-        var ts = to
-        while (fs.nonEmpty) {
-          if (fs.head eq sym) 
-            return RefinedThis(rt, level).select(ts.head)
-          fs = fs.tail
-          ts = ts.tail
-        }
-        if (sym.isStatic && !existsStatic(from)) tp
-        else tp.derivedSelect(apply(tp.prefix))
-      case tp: RefinedType =>
-        val parent1 = apply(tp.parent)
-        level += 1
-        try tp.derivedRefinedType(parent1, tp.refinedName, apply(tp.refinedInfo))
-        finally level -= 1
-      case tp: TypeAlias =>
-        tp.derivedTypeAlias(apply(tp.alias))
-      case _ =>
-        mapOver(tp)
-    }
-  }
 }
\ No newline at end of file
diff --git a/src/dotty/tools/dotc/core/TypeApplications.scala b/src/dotty/tools/dotc/core/TypeApplications.scala
index e71226b68..b29022281 100644
--- a/src/dotty/tools/dotc/core/TypeApplications.scala
+++ b/src/dotty/tools/dotc/core/TypeApplications.scala
@@ -373,29 +373,27 @@ class TypeApplications(val self: Type) extends AnyVal {
     case _ => firstBaseArgInfo(defn.SeqClass)
   }
   
-  def containsRefinedThis(level: Int)(implicit ctx: Context): Boolean = {
-    def recur(tp: Type, level: Int): Boolean = tp.stripTypeVar match {
-      case RefinedThis(rt, `level`) =>
-        true
+  def containsRefinedThis(target: Type)(implicit ctx: Context): Boolean = {
+    def recur(tp: Type): Boolean = tp.stripTypeVar match {
+      case RefinedThis(tp) =>
+        tp eq target
       case tp: NamedType =>
         tp.info match {
-          case TypeAlias(alias) => recur(alias, level)
-          case _ => !tp.symbol.isStatic && recur(tp.prefix, level)
+          case TypeAlias(alias) => recur(alias)
+          case _ => !tp.symbol.isStatic && recur(tp.prefix)
         }
       case tp: RefinedType =>
-        recur(tp.refinedInfo, level + 1) ||
-          recur(tp.parent, level)
+        recur(tp.refinedInfo) || recur(tp.parent)
       case tp: TypeBounds =>
-        recur(tp.lo, level) ||
-          recur(tp.hi, level)
+        recur(tp.lo) || recur(tp.hi)
       case tp: AnnotatedType =>
-        recur(tp.underlying, level)
+        recur(tp.underlying)
       case tp: AndOrType =>
-        recur(tp.tp1, level) || recur(tp.tp2, level)
+        recur(tp.tp1) || recur(tp.tp2)
       case _ =>
         false
     }
-    recur(self, level) 
+    recur(self) 
   }
 
   /** Given a type alias
@@ -432,14 +430,16 @@ class TypeApplications(val self: Type) extends AnyVal {
       if (bsyms.isEmpty) {
         val correspondingNames = correspondingParamName.values.toSet
 
+       def replacements(rt: RefinedType): List[Type] =
+          for (sym <- boundSyms)
+            yield TypeRef(RefinedThis(rt), correspondingParamName(sym))
+
         def rewrite(tp: Type): Type = tp match {
           case tp @ RefinedType(parent, name: TypeName) =>
             if (correspondingNames contains name) rewrite(parent)
             else RefinedType(
-              rewrite(parent),
-              name,
-              new ctx.SubstWithRefinedSelectMap(
-                _, boundSyms, boundSyms map correspondingParamName)(tp.refinedInfo))
+              rewrite(parent), name,
+              rt => tp.refinedInfo.subst(boundSyms, replacements(rt)))
           case tp =>
             tp
         }
@@ -474,8 +474,9 @@ class TypeApplications(val self: Type) extends AnyVal {
     def expand(tp: Type) = {
       val lambda = defn.lambdaTrait(boundSyms.map(_.variance))
       val substitutedRHS = (rt: RefinedType) => {
-        val argNames = boundSyms.indices.toList.map(tpnme.lambdaArgName)
-        new ctx.SubstWithRefinedSelectMap(rt, boundSyms, argNames)(tp).bounds.withVariance(1)
+        val argRefs = boundSyms.indices.toList.map(i =>
+          RefinedThis(rt).select(tpnme.lambdaArgName(i)))
+        tp.subst(boundSyms, argRefs).bounds.withVariance(1)
       }
       val res = RefinedType(lambda.typeRef, tpnme.Apply, substitutedRHS)
       //println(i"lambda abstract $self wrt $boundSyms%, % --> $res")
diff --git a/src/dotty/tools/dotc/core/TypeComparer.scala b/src/dotty/tools/dotc/core/TypeComparer.scala
index 8717a45df..8a810741a 100644
--- a/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -258,9 +258,9 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling wi
             }
         }
       comparePolyParam
-    case tp1: RefinedThis =>
+    case RefinedThis(rt1) =>
       tp2 match {
-        case tp2: RefinedThis if tp1.level == tp2.level => true
+        case RefinedThis(rt2) if rt1 == rt2 => true
         case _ => thirdTry(tp1, tp2)
       }
     case tp1: BoundType =>
@@ -525,7 +525,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling wi
     try {
       def rebindNeeded = tp2.refinementRefersToThis
       val base = if (rebindNeeded) ensureSingleton(tp1) else tp1
-      val rinfo2 = if (rebindNeeded) tp2.refinedInfo.substRefinedThis(0, base) else tp2.refinedInfo
+      val rinfo2 = if (rebindNeeded) tp2.refinedInfo.substThis0(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)
diff --git a/src/dotty/tools/dotc/core/TypeOps.scala b/src/dotty/tools/dotc/core/TypeOps.scala
index 6fc7314c2..3e04eb037 100644
--- a/src/dotty/tools/dotc/core/TypeOps.scala
+++ b/src/dotty/tools/dotc/core/TypeOps.scala
@@ -331,21 +331,6 @@ trait TypeOps { this: Context =>
     parentRefs
   }
   
-  /** Map `C.this` types where `C` is `refineCls` to RefinedThis types with given level.
-   *  The level gets adjusted for nested refined types.
-   */
-  def thisToRefinedThis(rt: RefinedType, refineCls: Symbol, level: Int): TypeMap = new TypeMap {
-    def apply(tp: Type): Type = tp match {
-      case tp: ThisType if tp.cls eq refineCls => RefinedThis(rt, level)
-      case tp: RefinedType =>
-        tp.derivedRefinedType(
-          this(tp.parent), tp.refinedName,
-          thisToRefinedThis(rt, refineCls, level + 1)(tp.refinedInfo))
-      case _ =>
-        mapOver(tp)
-    }
-  }
-  
   /** An argument bounds violation is a triple consisting of
    *   - the argument tree
    *   - a string "upper" or "lower" indicating which bound is violated
diff --git a/src/dotty/tools/dotc/core/Types.scala b/src/dotty/tools/dotc/core/Types.scala
index d64e7340e..933f56cb4 100644
--- a/src/dotty/tools/dotc/core/Types.scala
+++ b/src/dotty/tools/dotc/core/Types.scala
@@ -436,12 +436,9 @@ object Types {
       }
       def goRefined(tp: RefinedType) = {
         val pdenot = go(tp.parent)
-        val rinfo = pre match {
-          case pre: RefinedType => tp.refinedInfo.substThis0(tp, RefinedThis(pre, -1))
-          case _ => 
-            if (tp.refinementRefersToThis) tp.refinedInfo.substRefinedThis(0, pre)
-            else tp.refinedInfo
-        }
+        val rinfo =
+          if (tp.refinementRefersToThis) tp.refinedInfo.substThis0(tp, pre)
+          else tp.refinedInfo
         if (name.isTypeName) { // simplified case that runs more efficiently
           val jointInfo = if (rinfo.isAlias) rinfo else pdenot.info & rinfo
           pdenot.asSingleDenotation.derivedSingleDenotation(pdenot.symbol, jointInfo)
@@ -777,12 +774,12 @@ object Types {
             case TypeAlias(tp) => 
               if (!pre.refinementRefersToThis) tp
               else tp match {
-                case TypeRef(RefinedThis(_, 0), alias) => lookupRefined(alias)
+                case TypeRef(RefinedThis(`pre`), alias) => lookupRefined(alias)
                 case _ => NoType
               }
             case _ => loop(pre.parent)
           }
-        case RefinedThis(rt, _) =>
+        case RefinedThis(rt) =>
           rt.lookupRefined(name)
         case pre: WildcardType =>
           WildcardType
@@ -947,10 +944,6 @@ object Types {
     final def substThis0(rt: RefinedType, tp: Type)(implicit ctx: Context): Type =
       ctx.substThis0(this, rt, tp, null)
 
-    /** Substitute all occurrences of `RefinedThis(level)` by `tp` */
-    final def substRefinedThis(level: Int, to: Type)(implicit ctx: Context): Type =
-      ctx.substRefinedThis(this, level, to, null)
-
     /** Substitute a bound type by some other type */
     final def substParam(from: ParamType, to: Type)(implicit ctx: Context): Type =
       ctx.substParam(this, from, to, null)
@@ -1750,49 +1743,15 @@ object Types {
     
     def refinementRefersToThis(implicit ctx: Context): Boolean = {
       if (!refinementRefersToThisKnown) {
-        refinementRefersToThisCache = refinedInfo.containsRefinedThis(0)
+        refinementRefersToThisCache = refinedInfo.containsRefinedThis(this)
         refinementRefersToThisKnown = true
       }
       refinementRefersToThisCache
     }
-    
-    def checkLevel(implicit ctx: Context): Unit = {
-      val checkAccu = new TypeAccumulator[Unit] {
-        var level = 0
-        def apply(x: Unit, tp: Type) = tp.stripTypeVar match {
-          case RefinedThis(rt, l) => 
-            def dominates(tp: Type, rt: RefinedType): Boolean = 
-              (tp eq rt) || {
-                tp match {
-                  case RefinedType(parent, _) => dominates(parent, rt)
-                  case _ => false
-                }
-              }
-            if (rt eq RefinedType.this) assert(l == level, RefinedType.this)
-          case tp: RefinedType => 
-            level += 1
-            apply(x, tp.refinedInfo)
-            level -= 1
-            apply(x, tp.parent)
-          case tp: TypeBounds => 
-            apply(x, tp.lo)
-            apply(x, tp.hi)
-          case tp: AnnotatedType => 
-            apply(x, tp.underlying)
-          case tp: AndOrType => 
-            apply(x, tp.tp1)
-            apply(x, tp.tp2)
-          case _ => 
-            foldOver(x, tp)
-        }
-      }
-      checkAccu((), refinedInfo)
-    }
 
     override def underlying(implicit ctx: Context) = parent
 
     private def checkInst(implicit ctx: Context): this.type = {
-      checkLevel
       if (Config.checkLambdaVariance)
         refinedInfo match {
           case refinedInfo: TypeBounds if refinedInfo.variance != 0 && refinedName.isLambdaArgName =>
@@ -1820,7 +1779,7 @@ object Types {
         derivedRefinedType(parent.EtaExpand, refinedName, refinedInfo)
       else
         if (false) RefinedType(parent, refinedName, refinedInfo) 
-        else RefinedType(parent, refinedName, rt => refinedInfo.substThis0(this, RefinedThis(rt, -1))) // !!! TODO: replace with simply `refinedInfo`
+        else RefinedType(parent, refinedName, rt => refinedInfo.substThis0(this, RefinedThis(rt)))
     }
 
     override def equals(that: Any) = that match {
@@ -2222,11 +2181,11 @@ object Types {
    *  @param level  The number of enclosing refined types between
    *                the `this` reference and its target.
    */
-  case class RefinedThis(binder: RefinedType, level: Int) extends BoundType with SingletonType {
+  case class RefinedThis(binder: RefinedType) extends BoundType with SingletonType {
     type BT = RefinedType
     override def underlying(implicit ctx: Context) = binder
-    def copyBoundType(bt: BT) = RefinedThis(bt, level)
-
+    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)
@@ -2234,7 +2193,7 @@ object Types {
       case that: RefinedThis => this.binder eq that.binder
       case _ => false
     }
-    override def toString = s"RefinedThis($level, ${binder.hashCode})"
+    override def toString = s"RefinedThis(${binder.hashCode})"
   }
 
   // ------------ Type variables ----------------------------------------
diff --git a/src/dotty/tools/dotc/core/pickling/UnPickler.scala b/src/dotty/tools/dotc/core/pickling/UnPickler.scala
index 2bea977f7..62ad39c07 100644
--- a/src/dotty/tools/dotc/core/pickling/UnPickler.scala
+++ b/src/dotty/tools/dotc/core/pickling/UnPickler.scala
@@ -660,8 +660,12 @@ class UnPickler(bytes: Array[Byte], classRoot: ClassDenotation, moduleClassRoot:
         val parent = parents.reduceLeft(AndType(_, _))
         if (decls.isEmpty) parent
         else {
-          def addRefinement(tp: Type, sym: Symbol) =
-            RefinedType(tp, sym.name, ctx.thisToRefinedThis(_, clazz, 0)(sym.info))
+          def addRefinement(tp: Type, sym: Symbol) = {
+            def subst(info: Type, rt: RefinedType) = 
+              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, _))
+          }
           (parent /: decls.toList)(addRefinement).asInstanceOf[RefinedType]
         }
       case CLASSINFOtpe =>
diff --git a/src/dotty/tools/dotc/printing/PlainPrinter.scala b/src/dotty/tools/dotc/printing/PlainPrinter.scala
index fd6ba44a7..77a308bba 100644
--- a/src/dotty/tools/dotc/printing/PlainPrinter.scala
+++ b/src/dotty/tools/dotc/printing/PlainPrinter.scala
@@ -207,8 +207,11 @@ class PlainPrinter(_ctx: Context) extends Printer {
         toText(value)
       case MethodParam(mt, idx) =>
         nameString(mt.paramNames(idx))
-      case RefinedThis(_, level) =>
-        s"this<$level>"
+      case sk: RefinedThis =>
+        sk.binder match {
+          case rt: RefinedType => s"${nameString(rt.typeSymbol)}{...}.this"
+          case _ => "<skolem>"
+        }
     }
   }
 
diff --git a/src/dotty/tools/dotc/typer/Typer.scala b/src/dotty/tools/dotc/typer/Typer.scala
index dd05fea3f..0ff47b36d 100644
--- a/src/dotty/tools/dotc/typer/Typer.scala
+++ b/src/dotty/tools/dotc/typer/Typer.scala
@@ -791,7 +791,7 @@ class Typer extends Namer with TypeAssigner with Applications with Implicits wit
       checkRefinementNonCyclic(refinement, refineCls, seen)
       val rsym = refinement.symbol
       val rinfo = if (rsym is Accessor) rsym.info.resultType else rsym.info
-      RefinedType(parent, rsym.name, ctx.thisToRefinedThis(_, refineCls, 0)(rinfo))
+      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