Propagate orderings before unifying type parameters

[Linyxus]

The PR fixes a problem illustrated in the following code sample.

trait Expr[T]
final class Inv[T] extends Expr[T]

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

The code currently fails. The compiler complains that we give a X when we need a T2, and it believes that X >: T2.

We should know that X == T1 == T2 after the pattern matching, but currently the compiler assume that T2 <: X but not X == T2. This is because some part of ordering information does not propagate properly when we unify T1 to T2. In details, when we constrain the pattern match Expr[T2] >:< Inv[T1], we can discover that T1 == T2. To record this piece of information into constraints, we first add the ordering T2 <:< T1. After this, the constraints become:

Orderings: (propagated orderings are also displayed)
  X >: T1, T2 <: T1
  T1 >: T2, X <: X
  T2 <: T1, X

Then, when we add T1 <:< T2, the compiler discover that we already know T2 <:< T1, so it will unify T1 to T2. However, since we do not propagate orderings based on the fact that T1 <:< T2 before the unification, and the compiler does not seem to propoerly handle the ordering information when unifying the two type parameters, the ordering that T2 <:< T1 <:< X will not get propagated. After the unification, the constraints become

Bounds:
  T1 := T2
Orderings:
  X >: T2
  T1 >: X <: T2
  T2 <: X

This is why (??? : X) <:< T2 does not type check. To fix this, we could propagate the bounds with addLess before we unify the two type parameters.

[anatoliykmetyuk]

Hi @Linyxus, thanks for the PR! Since there hasn't been any activity on this PR for a while, we'll close it. If you'd like to resume working on it, feel free to open it or submit a new one. If the issue persists, it would be good to have it reported on the issue tracker.

[Linyxus]

I have opened another PR #13031 on this issue, with further tweaks! :^)