Deskolemize types inferred for vals and defs

We want to establish the invariant (optionally checked by assertNoSkolems)
that symbols do not contain skolemized types as their info. This avoids unsoundness situations
where a skolem gets exported as part if the result type of a method, so different instantiations
look like their are the same instance.

Author: odersky

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/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/Types.scala

@@ -2011,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 =

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 {

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