If expressions typed with GADT constraints cause failure with -Ycheck:all
#14776
Comments
Linyxus
added
itype:bug
stat:needs triage
Linyxus
changed the title
-Ycheck:all-Ycheck:all
Kordyjan
added
area:gadt
and removed
stat:needs triage
|
And this could be triggered with the match expression too: trait T1
trait T2 extends T1
trait Expr[T] { val data: T = ??? }
case class Tag2() extends Expr[T2]
def flag: Boolean = ???
def foo[T](e: Expr[T]): T1 = e match {
case Tag2() =>
flag match
case true => new T2 {}
case false => e.data
}Compilation of this snippet fails with |
|
I tried a fix like this. It does fix this issue, but will break a large bunch of tests. |
|
Note to self: why do we even insert a cast to |
|
Because |
|
It turns out that this issue is not necessarily related to GADT casts. The following code reproduces the same problem without direct relationship to the GADT cast. trait Expr[T]
case class IntExpr() extends Expr[Int]
def flag: Boolean = ???
def foo[T](ev: Expr[T]) = ev match
case IntExpr() =>
if flag then
val i: T = 0
i
else
0 |
|
I think that the core of the issue still lies in the fact that we completely ignore the GADT usage when computing the type of the if tree (where we will compute the union of the two branches' types). |
Compiler version
3.1.2-RC2Minimized code
It seems that the cause of the problem is that we did not insert GADT casting properly. The compiler complains that the type of the
ifexpression from the typer (T2) differs from that derived by the checker (T2 | (e.data : T) & T1).The
iftree after the typer looks like:We insert the casting
asInstanceOf[(e.data : T) & T1]because we try to adapte.datato typeT1and find that we used GADT constraints to type this. However, when assigning the type of theifexpression, the type assigner will computelubofT2and(e.data : T) & T1to get the simplified typeT2, which also relies on the GADT constraintT <: T2. Therefore, to assign typeT2to theifexpression, we also have to insert GADT casting somewhere, which is missing for now.Output
Expectation
The code should pass the tree checker.
The text was updated successfully, but these errors were encountered: