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.

[abgruszecki]

Ok, I took a look and it indeed seems like the problem is in ConstraintHandling. The traces are here: https://gist.github.com/abgruszecki/b6cc78b3f38aeec04f9d8d7160a6ee3b

It seems that for the case that works, when we initially add the constraints, we have:

added to constraint: [[Z(param)1 >: Int <: Int, Y(param)1 >: Z(param)1 <: Z(param)1, T(param)2] => Any] type Z, type Y, type T
Constraint(
 uninstantiated variables: Z(param)1, T(param)2
 constrained types: [Z(param)1 >: Int <: Int, Y(param)1 >: Z(param)1 <: Z(param)1, T(param)2] => Any
 bounds: 
     Z(param)1 >: Int <: Int
     Y(param)1 := Int
     T(param)2
 ordering: 
     Y(param)1 <: Z(param)1
)
type Z:  >: Int <: Int
type Y:  >: Int <: Z
type T: 

And for the case that doesn't work, we have:

added to constraint: [[Z(param)1 >: Int <: Int, Y(param)1 >: Z(param)1 <: Z(param)1, X(param)1 >: Y(param)1 <: Y(param)1, 
  T(param)2
] => Any] type Z, type Y, type X, type T
Constraint(
 uninstantiated variables: Z(param)1, X(param)1, T(param)2
 constrained types: 
  [Z(param)1 >: Int <: Int, Y(param)1 >: Z(param)1 <: Z(param)1, X(param)1 >: Y(param)1 <: Y(param)1, 
    T(param)2
  ] => Any
 bounds: 
     Z(param)1 >: Int <: Int
     Y(param)1 := Int
     X(param)1 <: AnyKind
     T(param)2
 ordering: 
     Y(param)1 <: X(param)1, Z(param)1
)
type Z:  >: Int <: Int
type Y:  >: Int <: Z
type X:  <: AnyKind
type T: 

Note that X is only <: AnyKind, where it probably should be X := Int. That seems to be the source of the problem.