Skip to content

Prune constraints that could turn into cycles #1058

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 6 commits into from
Feb 8, 2016
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 5 additions & 4 deletions src/dotty/tools/dotc/config/Config.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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 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 checkConstraintsNonCyclicTrans = false
final val checkConstraintsSeparated = false

/** Check that each constraint resulting from a subtype test
* is satisfiable.
Expand Down
75 changes: 72 additions & 3 deletions src/dotty/tools/dotc/core/ConstraintHandling.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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.
*
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -210,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
Expand All @@ -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
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What about narrowing a bit less by using something like prune(constraint.nonParamBounds(bound).lo) instead of defn.NothingType?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That would not add anything. By recording the isLess we get the bounds anyway.

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
}
Expand Down
9 changes: 7 additions & 2 deletions src/dotty/tools/dotc/core/TypeComparer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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)))
}
Expand Down Expand Up @@ -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
Expand Down
10 changes: 10 additions & 0 deletions tests/pos/i864.scala
Original file line number Diff line number Diff line change
@@ -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
}