Prune constraints that could turn into cycles

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

@@ -15,11 +15,12 @@ object Config {
    */
   final val checkConstraintsNonCyclic = false
 
-  /** Like `checkConstraintsNonCyclic`, but all constrained parameters
-   *  are tested for direct or indirect dependencies, each time a
-   *  constraint is added in TypeComparer.
+  /** Make sure none of the bounds in an OrderingConstraint contains
+   *  another constrained parameter at its toplevel (i.e. as an operand
+   *  of a combination of &'s and |'s.). The check is performed each time
+   *  a new bound is added to the constraint.
    */
-  final val checkConstraintsNonCyclicTrans = false
+  final val checkConstraintsSeparated = false
 
   /** Check that each constraint resulting from a subtype test
    *  is satisfiable.

src/dotty/tools/dotc/core/ConstraintHandling.scala

@@ -6,6 +6,7 @@ import Types._, Contexts._, Symbols._
 import Decorators._
 import config.Config
 import config.Printers._
+import collection.mutable
 
 /** Methods for adding constraints and solving them.
  *
@@ -35,6 +36,18 @@ trait ConstraintHandling {
 
   private def addOneBound(param: PolyParam, bound: Type, isUpper: Boolean): Boolean =
     !constraint.contains(param) || {
+      def occursIn(bound: Type): Boolean = {
+        val b = bound.dealias
+        (b eq param) || {
+          b match {
+            case b: AndOrType => occursIn(b.tp1) || occursIn(b.tp2)
+            case b: TypeVar => occursIn(b.origin)
+            case _ => false
+          }
+        }
+      }
+      if (Config.checkConstraintsSeparated)
+        assert(!occursIn(bound), s"$param occurs in $bound")
       val c1 = constraint.narrowBound(param, bound, isUpper)
       (c1 eq constraint) || {
         constraint = c1
@@ -222,11 +235,67 @@ trait ConstraintHandling {
     //checkPropagated(s"adding $description")(true) // DEBUG in case following fails
     checkPropagated(s"added $description") {
       addConstraintInvocations += 1
+
+      def addParamBound(bound: PolyParam) =
+        if (fromBelow) addLess(bound, param) else addLess(param, bound)
+
+      /** Drop all constrained parameters that occur at the toplevel in `bound` and
+       *  handle them by `addLess` calls.
+       *  The preconditions make sure that such parameters occur only
+       *  in one of two ways:
+       *
+       *  1.
+       *
+       *    P <: Ts1 | ... | Tsm   (m > 0)
+       *    Tsi = T1 & ... Tn      (n >= 0)
+       *    Some of the Ti are constrained parameters
+       *
+       *  2.
+       *
+       *    Ts1 & ... & Tsm <: P   (m > 0)
+       *    Tsi = T1 | ... | Tn    (n >= 0)
+       *    Some of the Ti are constrained parameters
+       *
+       *  In each case we cannot leave the parameter in place,
+       *  because that would risk making a parameter later a subtype or supertype
+       *  of a bound where the parameter occurs again at toplevel, which leads to cycles
+       *  in the subtyping test. So we intentionally narrow the constraint by
+       *  recording an isLess relationship instead (even though this is not implied
+       *  by the bound).
+       *
+       *  Narrowing a constraint is better than widening it, because narrowing leads
+       *  to incompleteness (which we face anyway, see for instance eitherIsSubType)
+       *  but widening leads to unsoundness.
+       *
+       *  A test case that demonstrates the problem is i864.scala.
+       *  Turn Config.checkConstraintsSeparated on to get an accurate diagnostic
+       *  of the cycle when it is created.
+       *
+       *  @return The pruned type if all `addLess` calls succeed, `NoType` otherwise.
+       */
+      def prune(bound: Type): Type = bound match {
+        case bound: AndOrType =>
+          val p1 = prune(bound.tp1)
+          val p2 = prune(bound.tp2)
+          if (p1.exists && p2.exists) bound.derivedAndOrType(p1, p2)
+          else NoType
+        case bound: TypeVar if constraint contains bound.origin =>
+          prune(bound.underlying)
+        case bound: PolyParam if constraint contains bound =>
+          if (!addParamBound(bound)) NoType
+          else if (fromBelow) defn.NothingType
+          else defn.AnyType
+        case _ =>
+          bound
+      }
+
       try bound match {
         case bound: PolyParam if constraint contains bound =>
-          if (fromBelow) addLess(bound, param) else addLess(param, bound)
+          addParamBound(bound)
         case _ =>
-          if (fromBelow) addLowerBound(param, bound) else addUpperBound(param, bound)
+          val pbound = prune(bound)
+          pbound.exists && (
+            if (fromBelow) addLowerBound(param, pbound) else addUpperBound(param, pbound))
       }
       finally addConstraintInvocations -= 1
     }

src/dotty/tools/dotc/core/TypeComparer.scala

@@ -124,7 +124,10 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
       pendingSubTypes = new mutable.HashSet[(Type, Type)]
       ctx.log(s"!!! deep subtype recursion involving ${tp1.show} <:< ${tp2.show}, constraint = ${state.constraint.show}")
       ctx.log(s"!!! constraint = ${constraint.show}")
-      assert(!ctx.settings.YnoDeepSubtypes.value) //throw new Error("deep subtype")
+      //if (ctx.settings.YnoDeepSubtypes.value) {
+      //  new Error("deep subtype").printStackTrace()
+      //}
+      assert(!ctx.settings.YnoDeepSubtypes.value)
       if (Config.traceDeepSubTypeRecursions && !this.isInstanceOf[ExplainingTypeComparer])
         ctx.log(TypeComparer.explained(implicit ctx => ctx.typeComparer.isSubType(tp1, tp2)))
     }
@@ -1047,7 +1050,9 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
     else hkCombine(tp1, tp2, tparams1, tparams2, op)
   }
 
-  /** Try to distribute `&` inside type, detect and handle conflicts */
+  /** Try to distribute `&` inside type, detect and handle conflicts
+   *  @pre !(tp1 <: tp2) && !(tp2 <:< tp1) -- these cases were handled before
+   */
   private def distributeAnd(tp1: Type, tp2: Type): Type = tp1 match {
     // opportunistically merge same-named refinements
     // this does not change anything semantically (i.e. merging or not merging

tests/pos/i864.scala

@@ -0,0 +1,10 @@
+object C {
+  val a: Int = 1
+  val b: Int = 2
+  val c: Int = 2
+
+  trait X[T]
+  implicit def u[A, B]: X[A | B] = new X[A | B] {}
+  def y[T](implicit x: X[T]): T = ???
+  val x: a.type & b.type | b.type & c.type = y
+}