Match types fail -Ycheck with GADT constraints
#15743
Comments
Linyxus
added
itype:bug
stat:needs triage
Linyxus
changed the title
-Ycheck with GADT constraints-Ycheck with GADT constraints
This test triggers a bug in the compiler unrelated to path-dependent GADT reasoning. See scala#15743. We should add this test back after fixing this issue.
szymon-rd
added
area:typer
and removed
stat:needs triage
This test triggers a bug in the compiler unrelated to path-dependent GADT reasoning. See scala#15743. We should add this test back after fixing this issue.
|
Minimized and scala-cli-ified: //> using scala "3.2.0-RC3"
//> using option "-Ycheck:typer"
case class Bar[T <: Tuple]()
def bar(e: Any): Int = e match
case _: Bar[t] =>
(??? : Int *: t).head( |
|
Dale's current working hypothesis is that |
|
Note that there are cases where we do have bounds as GADT constraints: enum C[-T]:
case C1() extends C[EmptyTuple]
def foo[A](e: C[A]) = e match {
case C.C1() =>
// GADT constr: A <: EmptyTuple
val i: Int = (??? : Int *: A).head
}
|
|
It makes sense to tackle Linyxus's case first, since it's entirely in GADT-land, and then later consider the original case, which seems to involve crossing in and out of that land. In both cases, the feature intersection involved is bounds and match types: we're using a bounded type as input to a match type. |
|
This is an interesting one. Dale is considering (and experimenting with) a couple possible solution paths. One is to try to solve it by inserting a GADT cast. The other I won't try to summarize but it involves thinking a bit more broadly about how and where GADT constraints are handled during typechecking. |
That's the approach taken in the now-merged PR. |
This test triggers a bug in the compiler unrelated to path-dependent GADT reasoning. See scala#15743. We should add this test back after fixing this issue.
This test triggers a bug in the compiler unrelated to path-dependent GADT reasoning. See scala#15743. We should add this test back after fixing this issue.
Compiler version
3.2.0-RC2(mainbranch)Minimized code
Output
Expectation
This code should pass the tree checker. As seen in the log, the tree checker fails at the expression
xs1.head[(a *: t)], whose expected type isabut the found type isTuple.Head[a *: t]. TheTuple.Headis a match type defined as:The possible cause seems to be: to reduce
Tuple.Head[a *: t]toawe need to show thattis a subtype ofTuple. However, the GADT boundt <: Tupleis not available when we run the checker phase. This is why the expressionxs0.head[(a *: T)]whose type does not need GADT constraints to reduce works butxs1.head[(a *: t)]breaks.The text was updated successfully, but these errors were encountered: