From c24ece505e53570566b499b817342a4dfa4087ff Mon Sep 17 00:00:00 2001 From: Martin Odersky Date: Fri, 5 Feb 2016 11:03:12 +0100 Subject: [PATCH 1/6] Prune constraints that could turn into cycles Fixes #864. Review by @smarter. --- .../tools/dotc/core/ConstraintHandling.scala | 49 ++++++++++++++++++- src/dotty/tools/dotc/core/TypeComparer.scala | 9 +++- tests/pos/i864.scala | 10 ++++ 3 files changed, 65 insertions(+), 3 deletions(-) create mode 100644 tests/pos/i864.scala diff --git a/src/dotty/tools/dotc/core/ConstraintHandling.scala b/src/dotty/tools/dotc/core/ConstraintHandling.scala index ff7afe99aeff..07e048ab380b 100644 --- a/src/dotty/tools/dotc/core/ConstraintHandling.scala +++ b/src/dotty/tools/dotc/core/ConstraintHandling.scala @@ -35,6 +35,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.checkConstraintsNonCyclicTrans) + assert(!occursIn(bound), s"$param occurs in $bound") val c1 = constraint.narrowBound(param, bound, isUpper) (c1 eq constraint) || { constraint = c1 @@ -222,11 +234,46 @@ trait ConstraintHandling { //checkPropagated(s"adding $description")(true) // DEBUG in case following fails checkPropagated(s"added $description") { addConstraintInvocations += 1 + + /** Drop all constrained parameters that occur at the toplevel in bound. + * 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 record the relationship as an isLess, because + * of he outer |/&. But we should not leave it in the constraint either + * because that would risk making a parameter 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 loosen the constraint in order + * to keep it safe. A test case that demonstrates the problem is i864.scala. + */ + def prune(bound: Type): Type = bound match { + case bound: AndOrType => + bound.derivedAndOrType(prune(bound.tp1), prune(bound.tp2)) + case bound: TypeVar if constraint contains bound.origin => + prune(bound.underlying) + case bound: PolyParam if constraint contains bound => + 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) case _ => - if (fromBelow) addLowerBound(param, bound) else addUpperBound(param, bound) + val pbound = prune(bound) + if (fromBelow) addLowerBound(param, pbound) else addUpperBound(param, pbound) } finally addConstraintInvocations -= 1 } diff --git a/src/dotty/tools/dotc/core/TypeComparer.scala b/src/dotty/tools/dotc/core/TypeComparer.scala index f468a573f7ca..eeac56519647 100644 --- a/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/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 diff --git a/tests/pos/i864.scala b/tests/pos/i864.scala new file mode 100644 index 000000000000..8d2b859998e9 --- /dev/null +++ b/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 +} From 55832b8020a498d9cd49e2de4f8a8a3ba696814c Mon Sep 17 00:00:00 2001 From: Martin Odersky Date: Fri, 5 Feb 2016 11:19:39 +0100 Subject: [PATCH 2/6] Fix docs and naming --- src/dotty/tools/dotc/config/Config.scala | 9 +++++---- src/dotty/tools/dotc/core/ConstraintHandling.scala | 6 ++++-- 2 files changed, 9 insertions(+), 6 deletions(-) diff --git a/src/dotty/tools/dotc/config/Config.scala b/src/dotty/tools/dotc/config/Config.scala index 212defbbf003..461a15ac83e2 100644 --- a/src/dotty/tools/dotc/config/Config.scala +++ b/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. diff --git a/src/dotty/tools/dotc/core/ConstraintHandling.scala b/src/dotty/tools/dotc/core/ConstraintHandling.scala index 07e048ab380b..d25de9742707 100644 --- a/src/dotty/tools/dotc/core/ConstraintHandling.scala +++ b/src/dotty/tools/dotc/core/ConstraintHandling.scala @@ -45,7 +45,7 @@ trait ConstraintHandling { } } } - if (Config.checkConstraintsNonCyclicTrans) + if (Config.checkConstraintsSeparated) assert(!occursIn(bound), s"$param occurs in $bound") val c1 = constraint.narrowBound(param, bound, isUpper) (c1 eq constraint) || { @@ -252,11 +252,13 @@ trait ConstraintHandling { * Some of the Ti are constrained parameters * * In each case we cannot record the relationship as an isLess, because - * of he outer |/&. But we should not leave it in the constraint either + * of the outer |/&. But we should not leave it in the constraint either * because that would risk making a parameter 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 loosen the constraint in order * to keep it safe. 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. */ def prune(bound: Type): Type = bound match { case bound: AndOrType => From f20b11ae7935664b88d0b1c81782e042356fc11b Mon Sep 17 00:00:00 2001 From: Martin Odersky Date: Fri, 5 Feb 2016 12:05:43 +0100 Subject: [PATCH 3/6] Narrow problematic constraint instead of widening it. --- .../tools/dotc/core/ConstraintHandling.scala | 30 ++++++++++++++----- 1 file changed, 22 insertions(+), 8 deletions(-) diff --git a/src/dotty/tools/dotc/core/ConstraintHandling.scala b/src/dotty/tools/dotc/core/ConstraintHandling.scala index d25de9742707..36b93e1236b7 100644 --- a/src/dotty/tools/dotc/core/ConstraintHandling.scala +++ b/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. * @@ -234,8 +235,11 @@ trait ConstraintHandling { //checkPropagated(s"adding $description")(true) // DEBUG in case following fails checkPropagated(s"added $description") { addConstraintInvocations += 1 + val related = new mutable.ListBuffer[PolyParam]() - /** Drop all constrained parameters that occur at the toplevel in bound. + /** Drop all constrained parameters that occur at the toplevel in bound + * and add them to `related`, which means they will be handled by + * `addLess` calls. * The preconditions make sure that such parameters occur only * in one of two ways: * @@ -251,12 +255,18 @@ trait ConstraintHandling { * Tsi = T1 | ... | Tn (n >= 0) * Some of the Ti are constrained parameters * - * In each case we cannot record the relationship as an isLess, because - * of the outer |/&. But we should not leave it in the constraint either - * because that would risk making a parameter 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 loosen the constraint in order - * to keep it safe. A test case that demonstrates the problem is i864.scala. + * 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. */ @@ -266,15 +276,19 @@ trait ConstraintHandling { case bound: TypeVar if constraint contains bound.origin => prune(bound.underlying) case bound: PolyParam if constraint contains bound => + related += bound if (fromBelow) defn.NothingType else defn.AnyType case _ => bound } + def addParamBound(bound: PolyParam) = + if (fromBelow) addLess(bound, param) else addLess(param, bound) try bound match { case bound: PolyParam if constraint contains bound => - if (fromBelow) addLess(bound, param) else addLess(param, bound) + addParamBound(bound) case _ => val pbound = prune(bound) + related.foreach(addParamBound) if (fromBelow) addLowerBound(param, pbound) else addUpperBound(param, pbound) } finally addConstraintInvocations -= 1 From 8358e979d328fcf430d6f895c39b3a3aae6e722e Mon Sep 17 00:00:00 2001 From: Martin Odersky Date: Fri, 5 Feb 2016 13:14:24 +0100 Subject: [PATCH 4/6] Avoid `related` buffer in `addConstraint`. --- .../tools/dotc/core/ConstraintHandling.scala | 28 +++++++++++-------- 1 file changed, 17 insertions(+), 11 deletions(-) diff --git a/src/dotty/tools/dotc/core/ConstraintHandling.scala b/src/dotty/tools/dotc/core/ConstraintHandling.scala index 36b93e1236b7..2435fd9dc235 100644 --- a/src/dotty/tools/dotc/core/ConstraintHandling.scala +++ b/src/dotty/tools/dotc/core/ConstraintHandling.scala @@ -235,11 +235,12 @@ trait ConstraintHandling { //checkPropagated(s"adding $description")(true) // DEBUG in case following fails checkPropagated(s"added $description") { addConstraintInvocations += 1 - val related = new mutable.ListBuffer[PolyParam]() - /** Drop all constrained parameters that occur at the toplevel in bound - * and add them to `related`, which means they will be handled by - * `addLess` calls. + 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: * @@ -269,27 +270,32 @@ trait ConstraintHandling { * 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 => - bound.derivedAndOrType(prune(bound.tp1), prune(bound.tp2)) + 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 => - related += bound - if (fromBelow) defn.NothingType else defn.AnyType + if (!addParamBound(bound)) NoType + else if (fromBelow) defn.NothingType + else defn.AnyType case _ => bound } - def addParamBound(bound: PolyParam) = - if (fromBelow) addLess(bound, param) else addLess(param, bound) + try bound match { case bound: PolyParam if constraint contains bound => addParamBound(bound) case _ => val pbound = prune(bound) - related.foreach(addParamBound) - if (fromBelow) addLowerBound(param, pbound) else addUpperBound(param, pbound) + pbound.exists && ( + if (fromBelow) addLowerBound(param, pbound) else addUpperBound(param, pbound)) } finally addConstraintInvocations -= 1 } From 73e13e8e16eaef531aafb1ff1666047b9f2f41a4 Mon Sep 17 00:00:00 2001 From: Guillaume Martres Date: Mon, 8 Feb 2016 20:32:08 +0100 Subject: [PATCH 5/6] Fix documentation of Config.checkConstraintsSeparated --- src/dotty/tools/dotc/config/Config.scala | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/dotty/tools/dotc/config/Config.scala b/src/dotty/tools/dotc/config/Config.scala index 461a15ac83e2..3cc3091b5a17 100644 --- a/src/dotty/tools/dotc/config/Config.scala +++ b/src/dotty/tools/dotc/config/Config.scala @@ -15,10 +15,10 @@ object Config { */ final val checkConstraintsNonCyclic = false - /** 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. + /** Make sure none of the bounds of a parameter in an OrderingConstraint + * contains this 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 checkConstraintsSeparated = false From 7d3f6d02141bb362c4c1e383cb21a476383b5c60 Mon Sep 17 00:00:00 2001 From: Guillaume Martres Date: Mon, 8 Feb 2016 20:37:48 +0100 Subject: [PATCH 6/6] Fix documentation of ConstraintHandling#addConstraint --- src/dotty/tools/dotc/core/ConstraintHandling.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/dotty/tools/dotc/core/ConstraintHandling.scala b/src/dotty/tools/dotc/core/ConstraintHandling.scala index 2435fd9dc235..f8eae186a8c4 100644 --- a/src/dotty/tools/dotc/core/ConstraintHandling.scala +++ b/src/dotty/tools/dotc/core/ConstraintHandling.scala @@ -223,7 +223,7 @@ trait ConstraintHandling { final def canConstrain(param: PolyParam): Boolean = !frozenConstraint && (constraint contains param) - /** Add constraint `param <: bond` if `fromBelow` is true, `param >: bound` otherwise. + /** Add constraint `param <: bound` if `fromBelow` is false, `param >: bound` otherwise. * `bound` is assumed to be in normalized form, as specified in `firstTry` and * `secondTry` of `TypeComparer`. In particular, it should not be an alias type, * lazy ref, typevar, wildcard type, error type. In addition, upper bounds may