Type equality failure on pattern match with tuple types

[nrinaudo]

Compiler version

3.1.2

Minimized code

enum Format[A]:
  case Str[Next](next: Format[Next]) extends Format[(String, Next)]
  case Num[Next](next: Format[Next]) extends Format[(Int, Next)]
  case Constant[Next](value: String, next: Format[Next]) extends Format[Next]
  case Done extends Format[Unit]

def printf[A](format: Format[A], params: A): Unit = (format, params) match
  case (Format.Done, ()) =>
    ()

  case (Format.Constant(value, next), params) =>
    println(value)
    printf(next, params)

  case (Format.Str(next), (str, rest)) =>
    println(str)
    printf(next, rest)

  case (Format.Num(next), (i, rest)) =>
    println(i)
    printf(next, rest)

Output

Compilation failure, the compiler cannot convince itself that, in the Format.Str branch, for example, A is of type (String, ...) (where ... is the right type to pass to next).

Expectation

This should compile: the compiler already knows the right types. As shown by @smarter , the following code compiles (and runs as expected):

enum Format[A]:
  case Str[Next](next: Format[Next]) extends Format[(String, Next)]
  case Num[Next](next: Format[Next]) extends Format[(Int, Next)]
  case Constant[Next](value: String, next: Format[Next]) extends Format[Next]
  case Done extends Format[Unit]

def printf[A](format: Format[A], params: A): Unit = format match
  case Format.Done =>
    ()

  case Format.Constant(value, next) =>
    print(value)
    printf(next, params)

  case Format.Str(next) =>
    print(params(0))
    printf(next, params(1))

  case Format.Num(next) =>
    print(params(0))
    printf(next, params(1))

Note that the only difference is, instead of pattern matching on the tuple, this code explicitly calls apply on it, which somehow satisfies the compiler that everything is alright.

[dwijnand]

I think I've figured it out. The A gets a symbol, and a type reference to that symbol is in format and params. Then the method as a whole gets a type parameter reference to A added to the GADT constraint, which can be refined in specific cases. But we're not doing anything based on the reference A, we're doing things in terms of references to format and params. So I think the fix to do this is the "Adding support of path-dependent GADT reasoning" PR: https://github.com/lampepfl/dotty/pull/14754. /cc @Linyxus @abgruszecki

[Linyxus]

I tried to compile the code on the #14754 branch but it also fails. After inspecting the GADT traces, I found that the cause of the failure may lie in the upcasting logic of GADT constrainer (here): when upcasting the scrutinee type we do not take existing GADT upper bounds into consideration.

In the minimal example below:

enum Format[A]:
  case Str[Next](next: Format[Next]) extends Format[(String, Next)]

def printf[A](format: Format[A], params: A): Unit = (format, params) match
  case (Format.Str(next), (str, rest)) =>
    val s: String = str  // error

To see why this limitation causes the compilation failure:

1. By constraining the type of the first elements (format and Format.Str(next)), Format[A] >:< Format.Str, we derive that A =:= (String, Next$1), here Next$1 is a type variable we create for the type parameter of the pattern Format.Str.

2. When constraining the second elements params and (str, rest) (A >:< (α, β)), here α and β are the type variables we create for str and rest, ideally we should upcast A to its GADT upper bound (String, Next$1), and constrain (String, Next$1) >:< (α, β) to derive α =:= String. However, in fact we will only upcast the A to its super type (as seen here), which is Any, preventing the desired constraint from being derived.

This is not necessarily related to pattern matching on tuples. We can decompose the tuple pattern matching into two steps, and the issue is still there:

enum Format[A]:
  case Str[Next](next: Format[Next]) extends Format[(String, Next)]

def printf[A](format: Format[A], params: A): Unit = format match
  case Format.Str(next) => params match
    case (str, rest) =>
      val s: String = str

Here is a straightforward fix for this issue: when upcasting the scrutinee type we also try the GADT upper bound. This allows the snippet to compile, and does not break tests on my machine. By principle upcasting the scrutinee will always be safe given that the upper bound is sound, but I am not 100% sure if this will cause soundness problems. Shall we go with this fix?