Fixes to type inference

1. Resolve overloading needs to be done with exploring typerstate
2. Need to handle case where A <: B for type variables in a more symmetric way.

(2) is not yet fully done.

3 files changed, 32 insertions, 11 deletions

diff --git a/src/dotty/tools/dotc/core/TypeComparer.scala b/src/dotty/tools/dotc/core/TypeComparer.scala
index b7027023d..c66e3a111 100644
--- a/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -50,13 +50,13 @@ class TypeComparer(initctx: Context) extends DotClass {
    *  to `constraint`.
    *  @pre `param` is in the constraint's domain
    */
-  def addConstraint(param: PolyParam, bounds: TypeBounds): Boolean =
-    !frozenConstraint && {
+  def addConstraint1(param: PolyParam, bound: Type, fromBelow: Boolean): Boolean = {
       val pt = param.binder
       val pnum = param.paramNum
       val oldEntries = constraint(pt)
       val oldBounds = oldEntries(pnum).asInstanceOf[TypeBounds]
-      val newBounds = oldBounds & bounds
+      val constrBounds = if (fromBelow) TypeBounds.lower(bound) else TypeBounds.upper(bound)
+      val newBounds = oldBounds & constrBounds
       if (oldBounds ne newBounds) {
         val newEntries = oldEntries.clone
         newEntries(pnum) = newBounds
@@ -65,6 +65,20 @@ class TypeComparer(initctx: Context) extends DotClass {
       isSubType(newBounds.lo, newBounds.hi)
     }
 
+  def addConstraint(param: PolyParam, bound: Type, fromBelow: Boolean): Boolean =
+    !frozenConstraint && {
+      bound match {
+        case bound: TypeVar =>
+          if (bound.isInstantiated)
+            addConstraint1(param, bound.instanceOpt, fromBelow)
+          else
+            addConstraint1(param, bound, fromBelow) &&
+            addConstraint1(bound.origin, param, !fromBelow)
+        case _ =>
+          addConstraint1(param, bound, fromBelow)
+      }
+    }
+
   /** Solve constraint for given type parameter `param`.
    *  If `fromBelow` is true the parameter is approximated by its lower bound,
    *  otherwise it is approximated by its upper bound. However, any occurrences
@@ -177,7 +191,7 @@ class TypeComparer(initctx: Context) extends DotClass {
         tp2 == tp1 || {
           //println(constraint.show)
           constraint(tp2) match {
-            case TypeBounds(lo, _) => isSubType(tp1, lo) || addConstraint(tp2, TypeBounds.lower(tp1.widen))
+            case TypeBounds(lo, _) => isSubType(tp1, lo) || addConstraint(tp2, tp1.widen, fromBelow = true)
             case _ => secondTry(tp1, tp2)
           }
         }
@@ -213,7 +227,7 @@ class TypeComparer(initctx: Context) extends DotClass {
     case tp1: PolyParam =>
       (tp1 == tp2) || {
         constraint(tp1) match {
-          case TypeBounds(_, hi) => isSubType(hi, tp2) || addConstraint(tp1, TypeBounds.upper(tp2))
+          case TypeBounds(_, hi) => isSubType(hi, tp2) || addConstraint(tp1, tp2, fromBelow = false)
           case _ => thirdTry(tp1, tp2)
         }
       }
@@ -851,9 +865,9 @@ class ExplainingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
       super.glb(tp1, tp2)
     }
 
-  override  def addConstraint(param: PolyParam, bounds: TypeBounds): Boolean =
-    traceIndented(s"add constraint $param $bounds $frozenConstraint") {
-      super.addConstraint(param, bounds)
+  override  def addConstraint(param: PolyParam, bound: Type, fromBelow: Boolean): Boolean =
+    traceIndented(s"add constraint $param ${if (fromBelow) ">:" else "<:"} $bound $frozenConstraint") {
+      super.addConstraint(param, bound, fromBelow)
     }
 
   override def copyIn(ctx: Context) = new ExplainingTypeComparer(ctx)
diff --git a/src/dotty/tools/dotc/typer/Inferencing.scala b/src/dotty/tools/dotc/typer/Inferencing.scala
index 24fe80c58..8c7285883 100644
--- a/src/dotty/tools/dotc/typer/Inferencing.scala
+++ b/src/dotty/tools/dotc/typer/Inferencing.scala
@@ -212,8 +212,11 @@ object Inferencing {
       if (changed)
         interpolateUndetVars(tp, pos)
       else
-        for (tvar <- ctx.typerState.undetVars if (pos contains tvar.pos) && !(vs contains tvar))
+        for (tvar <- ctx.typerState.undetVars
+             if (pos contains tvar.pos) && !(tvar.pos contains pos) && !(vs contains tvar)) {
+          // println(s"instantiating non-occurring $tvar in $tp")
           tvar.instantiate(fromBelow = true)
+        }
     }
 
     /** Instantiate undetermined type variables to that type `tp` is
diff --git a/src/dotty/tools/dotc/typer/Typer.scala b/src/dotty/tools/dotc/typer/Typer.scala
index 47eee5d4d..244713496 100644
--- a/src/dotty/tools/dotc/typer/Typer.scala
+++ b/src/dotty/tools/dotc/typer/Typer.scala
@@ -981,7 +981,7 @@ class Typer extends Namer with Applications with Implicits {
       val alts = altDenots map (alt =>
         TermRef.withSig(ref.prefix, ref.name, alt.info.signature).withDenot(alt))
       def expectedStr = err.expectedTypeStr(pt)
-      resolveOverloaded(alts, pt) match {
+      resolveOverloaded(alts, pt)(ctx.fresh.withExploreTyperState) match {
         case alt :: Nil =>
           adapt(tree.withType(alt), pt)
         case Nil =>
@@ -1053,7 +1053,11 @@ class Typer extends Namer with Applications with Implicits {
       case _ =>
         if (tree.tpe <:< pt) tree
         else if (ctx.mode is Mode.Pattern) tree // no subtype check for pattern
-        else adaptToSubType(wtp)
+        else {
+          //println(s"adapt to subtype ${tree.tpe} !<:< $pt") // !!!DEBUG
+          //println(TypeComparer.explained(implicit ctx => tree.tpe <:< pt))
+          adaptToSubType(wtp)
+        }
     }
 
     def adaptToSubType(wtp: Type): Tree = {