GADT type unification chain length limitation

[Linyxus]

Compiler version

3.0.0-M4-bin-SNAPSHOT, 3.0.0-RC1

Minimized code

object Test {
  trait Tag[T]

  // works: Int = Z = Y = T
  def func1[Z >: Int <: Int, Y >: Z <: Z, T >: Y <: Y]: T = {
    0
  }

  // works: Int = Z = Y = T
  def func2[Z >: Int <: Int, Y >: Z <: Z, T]: Tag[T] => T = {
    case _ : Tag[Y] => 0
  }

  // works: Int = Z = Y = X = T
  def func3[Z >: Int <: Int, Y >: Z <: Z, X >: Y <: Y, T >: X <: X]: T = {
    0
  }

  // expect: Int = Z = Y = X = T
  // actual: can not derive T = Int
  def func4[Z >: Int <: Int, Y >: Z <: Z, X >: Y <: Y, T]: Tag[T] => T = {
    case _ : Tag[X] => 0  // error
  }
}

Output

-- [E007] Type Mismatch Error: foobar/gadt-poly.scala:24:23 --------------------
24 |    case _ : Tag[X] => 0
   |                       ^
   |                       Found:    (0 : Int)
   |                       Required: T
1 error found

Expectation

It should infer the constraint T = X = Y = Z = Int.

@abgruszecki

[Kordyjan]

@Linyxus Your example shows that the problem has a scope broader than just GADTs and is a result of the limitation of the current typechecker.

[smarter]

@Kordyjan are you sure? The only example with // error involves GADT constraints.

[Kordyjan]

@smarter: Now I see I misunderstood the sample. It indeed seems to be a problem with GADTs constraints.

[abgruszecki]

@smarter I guess this issue doesn't remind you of anything similar in type inference? I'd be somewhat surprised if there was anything specific to the GADT logic that would make us handle correctly instantiation chains of length 3, but not of length 4, so my intuition is that there's something in constraint handling to blame. Ofc, it's entirely possible that I'm (still) misusing constraint handling.

[smarter]

No, this doesn't ring a bell, I thought it might be a deep subtype issue but running with -Yno-deep-subtypes does not make a difference.