Match types don't always fully resolve against statically-known types, if the types come from a type parameter.

[jypma]

The example is from a typesafe tensor/matrix library I'm writing, where the matrix sizes and shapes are known at compile time.

Compiler version

3.7.4

Minimized code

object Tst {
  import scala.compiletime.ops.int.*
  import Tuple.*

  trait Dim { /* ... */ }
  abstract class Static[S <: Long](using ValueOf[S]) extends Dim { /* ... */ }
  class Dynamic(_size: Long) extends Dim { /* ... */ }

  type One = Static[1L]

  type Max[D1 <: Dim, D2 <: Dim] <: Dim = (D1, D2) match {
    case (One, _) => D2
    case (_, One) => D1
    case (Static[s1], Static[s2]) => (s1 > s2) match {
      case true => D1
      case false => D2
    }
    case _ => Dynamic
  }

  case object NamedDim extends Dynamic(42)
  val tstA: Max[One, NamedDim.type] = NamedDim // ok
  val tstB: Max[NamedDim.type, One] = NamedDim // ok

  def tryme[C <: Dim, D <: Dim](c: C, d: D) = {
    val A: Max[One, D] = d // ok
    val B: Max[C, One] = c // does not compile
  }
}

Output:

[error] 28 |    val B: Max[C, One] = c // does not compile
[error]    |                         ^
[error]    |            Found:    (c : C)
[error]    |            Required: Tst.Max[C, Tst.One]
[error]    |
[error]    |            where:    C is a type in method tryme with bounds <: Tst.Dim
[error]    |
[error]    |
[error]    |            Note: a match type could not be fully reduced:
[error]    |
[error]    |              trying to reduce  Tst.Max[C, Tst.One]
[error]    |              failed since selector (C, Tst.One)
[error]    |              does not match  case (Tst.One, _) => Tst.One
[error]    |              and cannot be shown to be disjoint from it either.
[error]    |              Therefore, reduction cannot advance to the remaining cases

Expectation

When invoking Max, both matches of (One, _) and (_, One) should resolve to their respective D1 and D2 types. This works fine when matching against real types, but not for the generic method. Curiously, once of the Max branches does resolve.

If the two top case lines for Max are reversed, suddenly the val B will compile and val A won't.