Closed Linyxus closed 3 years ago
~@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.~
@Kordyjan are you sure? The only example with // error
involves GADT constraints.
@smarter: Now I see I misunderstood the sample. It indeed seems to be a problem with GADTs constraints.
@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.
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.
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.
Compiler version
3.0.0-M4-bin-SNAPSHOT
,3.0.0-RC1
Minimized code
Output
Expectation
It should infer the constraint
T = X = Y = Z = Int
.@abgruszecki