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.

5 files changed, 52 insertions, 4 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/SymDenotations.scala b/src/dotty/tools/dotc/core/SymDenotations.scala
index f24c41ee2..8162126a5 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
     }
 
@@ -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)
diff --git a/src/dotty/tools/dotc/core/Types.scala b/src/dotty/tools/dotc/core/Types.scala
index 4e1da7c34..ba39e7bef 100644
--- a/src/dotty/tools/dotc/core/Types.scala
+++ b/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 =
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/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 _
+
+}
+
+