Don't interpolate type variables if doing so would narrow the constraint

Author: odersky

compiler/src/dotty/tools/dotc/config/Config.scala

@@ -22,6 +22,8 @@ object Config {
    */
   inline val checkConstraintsNonCyclic = false
 
+  inline val checkConstraintDeps = false
+
   /** Check that each constraint resulting from a subtype test
    *  is satisfiable. Also check that a type variable instantiation
    *  satisfies its constraints.

compiler/src/dotty/tools/dotc/core/Constraint.scala

@@ -189,7 +189,7 @@ abstract class Constraint extends Showable {
   def dependsOn(tv: TypeVar, except: TypeVars, co: Boolean)(using Context): Boolean
 
   /** Check that no constrained parameter contains itself as a bound */
-  def checkNonCyclic()(using Context): this.type
+  def checkWellFormed()(using Context): this.type
 
   /** Does `param` occur at the toplevel in `tp` ?
    *  Toplevel means: the type itself or a factor in some

compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala

@@ -433,7 +433,7 @@ class OrderingConstraint(private val boundsMap: ParamBounds,
         todos.dropInPlace(1)
       i += 1
     }
-    current.checkNonCyclic()
+    current.checkWellFormed()
   }
 
 // ---------- Updates ------------------------------------------------------------
@@ -572,10 +572,10 @@ class OrderingConstraint(private val boundsMap: ParamBounds,
 
   /** The public version of `updateEntry`. Guarantees that there are no cycles */
   def updateEntry(param: TypeParamRef, tp: Type)(using Context): This =
-    updateEntry(this, param, ensureNonCyclic(param, tp)).checkNonCyclic()
+    updateEntry(this, param, ensureNonCyclic(param, tp)).checkWellFormed()
 
   def addLess(param1: TypeParamRef, param2: TypeParamRef, direction: UnificationDirection)(using Context): This =
-    order(this, param1, param2, direction).checkNonCyclic()
+    order(this, param1, param2, direction).checkWellFormed()
 
 // ---------- Replacements and Removals -------------------------------------
 
@@ -585,7 +585,7 @@ class OrderingConstraint(private val boundsMap: ParamBounds,
    */
   def replace(param: TypeParamRef, tp: Type)(using Context): OrderingConstraint =
     val replacement = tp.dealiasKeepAnnots.stripTypeVar
-    if param == replacement then this.checkNonCyclic()
+    if param == replacement then this.checkWellFormed()
     else
       assert(replacement.isValueTypeOrLambda)
       var current =
@@ -607,7 +607,7 @@ class OrderingConstraint(private val boundsMap: ParamBounds,
         current = upperLens.map(this, current, p, i, removeParam)
       }
       current.dropDeps(typeVarOfParam(param))
-      current.checkNonCyclic()
+      current.checkWellFormed()
   end replace
 
   def remove(pt: TypeLambda)(using Context): This = {
@@ -620,8 +620,8 @@ class OrderingConstraint(private val boundsMap: ParamBounds,
     }
     val hardVars1 = pt.paramRefs.foldLeft(hardVars)((hvs, param) => hvs - typeVarOfParam(param))
     newConstraint(boundsMap.remove(pt), removeFromOrdering(lowerMap), removeFromOrdering(upperMap), hardVars1)
-      .checkNonCyclic()
       .adjustDeps(boundsMap(pt).nn, add = false)
+      .checkWellFormed()
   }
 
   def isRemovable(pt: TypeLambda): Boolean = {
@@ -655,7 +655,7 @@ class OrderingConstraint(private val boundsMap: ParamBounds,
       current = upperLens.map(this, current, p, i, _.map(subst))
     }
     constr.println(i"renamed $this to $current")
-    current.checkNonCyclic()
+    current.checkWellFormed()
 
   def isHard(tv: TypeVar) = hardVars.contains(tv)
 
@@ -739,7 +739,7 @@ class OrderingConstraint(private val boundsMap: ParamBounds,
 
 // ---------- Checking -----------------------------------------------
 
-  def checkNonCyclic()(using Context): this.type =
+  def checkWellFormed()(using Context): this.type =
     if Config.checkConstraintsNonCyclic then
       domainParams.foreach { param =>
         val inst = entry(param)
@@ -748,6 +748,14 @@ class OrderingConstraint(private val boundsMap: ParamBounds,
         assert(!occursAtToplevel(param, inst),
           s"cyclic bound for $param: ${inst.show} in ${this.show}")
       }
+    if Config.checkConstraintDeps then
+      def checkDeps(deps: TypeVarDeps) =
+        deps.foreachBinding { (tv, tvs) =>
+          for tv1 <- tvs do
+            assert(!tv1.instanceOpt.exists, i"$this")
+        }
+      checkDeps(coDeps)
+      checkDeps(contraDeps)
     this
 
   def occursAtToplevel(param: TypeParamRef, inst: Type)(using Context): Boolean =

compiler/src/dotty/tools/dotc/typer/Inferencing.scala

@@ -640,6 +640,31 @@ trait Inferencing { this: Typer =>
                 typr.println(i"no interpolation for nonvariant $tvar in $state")
             )
 
+        def typeVarsIn(xs: collection.Seq[(TypeVar, Int)]): TypeVars =
+          xs.foldLeft(SimpleIdentitySet.empty: TypeVars)((tvs, tvi) => tvs + tvi._1)
+
+        def filterByDeps(tvs0: List[(TypeVar, Int)]): List[(TypeVar, Int)] = {
+          val excluded = typeVarsIn(tvs0)
+          def step(tvs: List[(TypeVar, Int)]): List[(TypeVar, Int)] = tvs match
+            case tvs @ (hd @ (tvar, v)) :: tvs1 =>
+              def aboveOK = !constraint.dependsOn(tvar, excluded, co = true)
+              def belowOK = !constraint.dependsOn(tvar, excluded, co = false)
+              if v == 0 && !aboveOK then
+                step((tvar, 1) :: tvs1)
+              else if v == 0 && !belowOK then
+                step((tvar, -1) :: tvs1)
+              else if v == -1 && !aboveOK || v == 1 && !belowOK then
+                println(i"drop $tvar, $v in $tp, $pt, qualifying = ${qualifying.toList}, tvs0 = ${tvs0.toList}%, %, excluded = ${excluded.toList}, $constraint")
+                step(tvs1)
+              else
+                tvs.derivedCons(hd, step(tvs1))
+            case Nil =>
+              Nil
+          val tvs1 = step(tvs0)
+          if tvs1 eq tvs0 then tvs1 else filterByDeps(tvs1)
+        }//.showing(i"filter $tvs0 in $constraint = $result")
+        end filterByDeps
+
         /** Instantiate all type variables in `buf` in the indicated directions.
          *  If a type variable A is instantiated from below, and there is another
          *  type variable B in `buf` that is known to be smaller than A, wait and
@@ -669,38 +694,45 @@ trait Inferencing { this: Typer =>
          *
          *      V2 := V3, O2 := O3
          */
-        def doInstantiate(buf: InstantiateQueue): Unit =
-          val varsToInstantiate = buf.foldLeft(SimpleIdentitySet.empty: TypeVars) {
-            case (tvs, (tv, _)) => tvs + tv
-          }
-          if buf.nonEmpty then
-            val suspended = new InstantiateQueue
-            while buf.nonEmpty do
-              val first @ (tvar, v) = buf.head
+        def doInstantiate(tvs: List[(TypeVar, Int)]): Unit =
+          def excluded = typeVarsIn(tvs)
+          def tryInstantiate(tvs: List[(TypeVar, Int)]): List[(TypeVar, Int)] = tvs match
+            case (hd @ (tvar, v)) :: tvs1 =>
               val fromBelow =
                 if v == 0 then
-                  val aboveOK = !constraint.dependsOn(tvar, varsToInstantiate, co = true)
-                  val belowOK = !constraint.dependsOn(tvar, varsToInstantiate, co = false)
+                  val aboveOK = true // !constraint.dependsOn(tvar, excluded, co = true, track = true)
+                  val belowOK = true // !constraint.dependsOn(tvar, excluded, co = false, track = true)
+                  assert(aboveOK, i"$tvar, excluded = ${excluded.toList}, $constraint")
+                  assert(belowOK, i"$tvar, excluded = ${excluded.toList}, $constraint")
                   if aboveOK == belowOK then tvar.hasLowerBound
                   else belowOK
                 else
                   v == 1
               typr.println(
-                i"interpolate${if v == 0 then "non-occurring" else ""} $tvar in $state in $tree: $tp, fromBelow = $fromBelow, $constraint")
-              buf.dropInPlace(1)
-              if !tvar.isInstantiated then
-                val suspend = buf.exists{ (following, _) =>
-                  if fromBelow then
-                    constraint.isLess(following.origin, tvar.origin)
-                  else
-                    constraint.isLess(tvar.origin, following.origin)
+                i"interpolate${if v == 0 then " non-occurring" else ""} $tvar in $state in $tree: $tp, fromBelow = $fromBelow, $constraint")
+              if tvar.isInstantiated then
+                tryInstantiate(tvs1)
+              else
+                val suspend = tvs1.exists{ (following, _) =>
+                  if fromBelow
+                  then constraint.isLess(following.origin, tvar.origin)
+                  else constraint.isLess(tvar.origin, following.origin)
                 }
-                if suspend then suspended += first else tvar.instantiate(fromBelow)
-              end if
-            end while
-            doInstantiate(suspended)
+                if suspend then
+                  typr.println(i"suspended: $hd")
+                  hd :: tryInstantiate(tvs1)
+                else
+                  tvar.instantiate(fromBelow)
+                  tryInstantiate(tvs1)
+            case Nil => Nil
+          if tvs.nonEmpty then doInstantiate(tryInstantiate(tvs))
         end doInstantiate
-        doInstantiate(toInstantiate)
+        val toInst = toInstantiate.toList
+        if toInst.nonEmpty then
+          typr.println(i"interpolating $toInst for $tp/$pt in $constraint")
+          val filtered = filterByDeps(toInst)
+          typr.println(i"filtered $filtered")
+          doInstantiate(filtered)
       }
     }
     tree