Fix ordering propagation during parameter unification in constraint solver

[Linyxus]

Before this PR, parameter orderings will not be properly propagated when unifying type parameters.

The following example illustrate this problem.

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
}

GADT logic in the compiler will unify T1 to T2 when we match Expr[T2] against Lit[T1]. During the process, the ordering X <:< T2 (derived from X <:< T1 and T1 <:< T2) will not be propagated. The resulting constraint will be in an inconsistent state where part of the orderings are not propagated. This problem will make isLess(X, T2) return false (since the ordering X <:< T2 is not propagated), thus preventing the above code example from compiling.

This PR fixes the problem by calling OrderingConstraint.addLess when unifying type parameters to propagate the orderings, and tweaking the logic of OrderingConstraint.order to properly consider the parameter unification case.

[dwijnand]

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.

[Linyxus]

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.

[anatoliykmetyuk]

@Linyxus @abgruszecki What's the status of this PR? Is it blocked on something or is it ready for review?

[abgruszecki]

@anatoliykmetyuk it's mostly blocked by my poor memory.