Skip to content

Fix ordering propagation during parameter unification in constraint solver #13031

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.

Sign up for GitHub

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 3 commits into from
Oct 4, 2021
Merged

Fix ordering propagation during parameter unification in constraint solver #13031

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
bb9ba6b
Propagate bounds when unifying type parameters
Linyxus Jul 8, 2021
4fde618
Refactor special handling for unification in `order`
Linyxus Jul 8, 2021
d1fca8a
Add pos test
Linyxus Jul 8, 2021
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
1 change: 1 addition & 0 deletions compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -197,6 +197,7 @@ trait ConstraintHandling {
private def unify(p1: TypeParamRef, p2: TypeParamRef)(using Context): Boolean = {
constr.println(s"unifying $p1 $p2")
assert(constraint.isLess(p1, p2))
constraint = constraint.addLess(p2, p1)
val down = constraint.exclusiveLower(p2, p1)
val up = constraint.exclusiveUpper(p1, p2)
constraint = constraint.unify(p1, p2)
Expand Down
23 changes: 21 additions & 2 deletions compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -353,8 +353,27 @@ class OrderingConstraint(private val boundsMap: ParamBounds,
else {
assert(contains(param1), i"$param1")
assert(contains(param2), i"$param2")
val newUpper = param2 :: exclusiveUpper(param2, param1)
val newLower = param1 :: exclusiveLower(param1, param2)
// Is `order` called during parameter unification?
val unifying = isLess(param2, param1)
val newUpper = {
val up = exclusiveUpper(param2, param1)
if unifying then
// Since param2 <:< param1 already holds now, filter out param1 to avoid adding
// duplicated orderings.
param2 :: up.filterNot(_ eq param1)
else
param2 :: up
}
val newLower = {
val lower = exclusiveLower(param1, param2)
if unifying then
// Do not add bounds for param1 since it will be unified to param2 soon.
// And, similarly filter out param2 from lowerly-ordered parameters
// to avoid duplicated orderings.
Copy link
Member

Choose a reason for hiding this comment

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

Are these changes correctness fixes or are they providing some other value (e.g. debug clarity or performance)? On the face of it "avoid duplicated orderings" and "will be unified to param2 soon" sounds like the kind of optional things that doesn't impact the end result - but I'm wondering if that's right or not.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Sorry for the late reply!

The special handling here actually avoid two different types of redundancy.

The first redundancy is that you may have duplicated entries in lowerMap and upperMap (which store the ordering between parameters) of OrderingConstraint. For example, you may get A <: B, B stored in the constriant.

This type of redundancy, actually, looks harmless. Actually, since the lowerMap and upperMap are all lists but not set, such situation will happen whenever some ordering is propagated along multiple different paths (and irrelated to the code change proposed by the PR). This will not bring erroneous behaviors of the compiler.

The second redundacy is that the constraint may end up storing B <: A even if B is unified to A. For example, we may have the constraint state as following.

Bounds:
  B  := A
Ordering:
  B  <: A

Such redundancy will break a patmat test. I could not figure out the exact reason, but preventing the redundancy ordering can solve the problem.

I am not sure if the broken patmat test is an expected behavior, since having the ordering B <: A while also having B unified to A will leave the constraints in a weird state. Anyway, I think I should refine the comments to clarify the issues here.

lower.filterNot(_ eq param2)
else
param1 :: lower
}
val current1 = newLower.foldLeft(current)(upperLens.map(this, _, _, newUpper ::: _))
val current2 = newUpper.foldLeft(current1)(lowerLens.map(this, _, _, newLower ::: _))
current2
Expand Down
6 changes: 6 additions & 0 deletions tests/pos/gadt-param-unification.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
trait Expr[T]
final class Lit[T] extends Expr[T]

def foo[X, T1 >: X, T2](m: Expr[T2]): T2 = m match {
case _: Lit[T1] => ??? : X
}