MatchType does not reduce for GADT aliases

[odersky]

  type T[X] = X match {
    case String => Int
    case Int => String
  }

  class Box[X](x: X)

  def f[X <: String | Int](x: X): T[X] = Box(x) match {
    case x: Box[Int] => ""        // <-- error
    case x: Box[String] => 1
  }

This gives:

10 |    case x: Box[Int] => ""
   |                        ^^
   |              Found:    String("")
   |              Required: Test.T[X]
   |              
   |              where:    X is a type in method f which is an alias of Int

If I swap the two cases in the match type the error is on the next line. This seems to indicate that the problem is in the no-overlap checks for match types. Maybe it needs to be strengthened for GADT aliases.

Generally:

• it would be good to play with more cases like this one
• it would be good to invest effort in better diagnostics when no-overlap check fails.

[odersky]

Assigning to @OlivierBlanvillain and @AleksanderBG since it touches both match types and GADTs.

[VledicFranco]

I am trying to write a safe printf using the new shiny dependent tools on dotty, and I was redirected here after posting on gitter, I hope it is a helpful example:

  enum Format {
    case FInt[T <: Format](t: T)
    case FString[T <: Format](t: T)
    case FOther[T <: Format](other: Char, t: T)
    case FEnd()
  }

  type InterpretFormat[F <: Format] =
    F match {
      case Format.FInt[t] => Int => InterpretFormat[t]
      case Format.FString[t] => String => InterpretFormat[t]
      case Format.FOther[t] => InterpretFormat[t]
      case Format.FEnd => String
    }

  def toFunction[F <: Format](format: F, acc: String): InterpretFormat[F] = 
    format match {
      case Format.FInt(t) => (i: Int) => toFunction(t, acc + i.toString)
      case Format.FString(t) => (s: String) => toFunction(t, acc + s)
      case Format.FOther(other, t) => toFunction(t, acc + other.toString)
      case Format.FEnd() => acc
    }

This gives a compilation error like this one for each line on the pattern matching of the toFunction function:

[error] -- [E007] Type Mismatch Error: D:\Repositories\scala3ex\src\main\scala\Main.scala:49:30  
[error] 49 |      case Format.FInt(t) => (i: Int) => toFunction(t, acc + i.toString)
[error]    |                              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[error]    |Found:    Int => Main.InterpretFormat[Tail$1] 
[error]    |Required: Main.InterpretFormat[F]
[error]    |
[error]    |where:    F      is a type in method toFunction with bounds >: Main.Format.FInt[Tail$1](?1) and <: Main.Format
[error]    |          Tail$1 is a type in method toFunction with bounds <: Main.Format

[VledicFranco]

BTW I am planning a presentation around this... with all kindness may I ask, what is the plan with this limitation?

[OlivierBlanvillain]

@FrancoAra We still haven't decided on a plan, which means it won't be for the near future.

[VledicFranco]

Thank you for your response @OlivierBlanvillain :) it is a shame to hear that though