Tighten comparison of skolem types

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

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

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 {

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
     }
 
@@ -1038,8 +1040,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)

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)

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 }
     }