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 {
    trait Dim { /* ... */ }

    case object One

    type Max[D1, D2] = (D1, D2) match {
      case (One.type, _) => D2
      case (_, One.type) => D1
    }

    case object Two
    val tstA: Max[One.type, Two.type] = Two // ok
    val tstB: Max[Two.type, One.type] = Two // ok

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

Output:

[error] -- [E007] Type Mismatch Error: /home/jan/workspace/s3torch/src/test/scala/Tst.scala:17:32
[error] 17 |      val B: Max[C, One.type] = c // does not compile
[error]    |                                ^
[error]    |             Found:    (c : C)
[error]    |             Required: Tst.Max[C, Tst.One.type]
[error]    |
[error]    |             Note: a match type could not be fully reduced:
[error]    |
[error]    |               trying to reduce  Tst.Max[C, Tst.One.type]
[error]    |               failed since selector (C, Tst.One.type)
[error]    |               does not match  case (Tst.One.type, _) => Tst.One.type
[error]    |               and cannot be shown to be disjoint from it either.
[error]    |               Therefore, reduction cannot advance to the remaining case
[error]    |
[error]    |                 case (_, Tst.One.type) => C
[error]    |----------------------------------------------------------------------------
[error]    | Explanation (enabled by `-explain`)
[error]    |- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
[error]    |
[error]    | Tree:
[error]    |
[error]    | c
[error]    |
[error]    | I tried to show that
[error]    |   (c : C)
[error]    | conforms to
[error]    |   Tst.Max[C, Tst.One.type]
[error]    | but none of the attempts shown below succeeded:
[error]    |
[error]    |   ==> (c : C)  <:  Tst.Max[C, Tst.One.type]
[error]    |     ==> (c : C)  <:  (C, Tst.One.type) match {   case (Tst.One.type, _) => Tst.One.type   case (_, Tst.One.type) => C } <: Tst.One.type | C
[error]    |       ==> C  <:  (C, Tst.One.type) match {   case (Tst.One.type, _) => Tst.One.type   case (_, Tst.One.type) => C } <: Tst.One.type | C
[error]    |         ==> Any  <:  (C, Tst.One.type) match {   case (Tst.One.type, _) => Tst.One.type   case (_, Tst.One.type) => C } <: Tst.One.type | C  = false
[error]    |         ==> Any  <:  (C, Tst.One.type) match {   case (Tst.One.type, _) => Tst.One.type   case (_, Tst.One.type) => C } <: Tst.One.type | C in frozen constraint  = false
[error]    |
[error]    | The tests were made under the empty constraint
[error]     ----------------------------------------------------------------------------

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.

[jypma]

I've minimized the example somewhat more.