GADT parameter ordering is not recorded during registration

[Linyxus]

If we have a function def[A <: B]foo(...) = ..., the ordering A <: B are not properly recorded if B has been instantiated. Instead, A <: B will be recorded as a /non-param bound/ of A.

Compiler version

The main branch

Minimized code

enum Tag[A]:
  case Data[A]() extends Tag[A]

def foo0[A](e: Tag[A]) = e.match {
  case _: Tag.Data[a] =>

    def bar[C >: Int <: a]() =
      val t1: a = 0  // fails
}

def foo1[A, C >: Int <: A]() =
  val t1: A = 0  // works

Output

-- [E007] Type Mismatch Error: issues/gadt-inst-dep.scala:8:18 -------------------------------------------------------------------------------------------------------------------------------------------
8 |      val t1: a = 0  // fails
  |                  ^
  |                  Found:    (0 : Int)
  |                  Required: a
  |
  |                  where:    a is a type in method foo0 which is an alias of A
  |
  | longer explanation available when compiling with `-explain`

Expectation

The code should compile without error.

In foo0 and foo1 we introduce the type parameter C with bounds >: Int <: a (or A). In foo1 the ordering between C and A is properly handled (so the bound >: Int gets propagated to A), but it is not the case in foo0. The main difference between foo0 and foo1 is that a in foo0 has been instantiated.

The reason why the ordering is not recorded in foo0 is that when processing the newly-defined type parameter C, the OrderingConstraint class will check whether a is a constrained parameter by calling constraint.contains(a). However, since the a has been instantiated and the related type lambda gets removed in the constraint, constraint.contains(a) returns false. So OrderingConstraint will keep a in the non-param bounds of C, without recording the orderings.

This is an issue discovered while developing #14754. #14754 already contains a fix for this issue that tries to check whether a has been instantiated and strips the type variable to its instance if possible. See this commit.