Scala 3 match type reduction

Question

Let's say I want to represent a vector using a matched type like this:

type V[I <: Int, N] = I match
  case 2 => (N, N)
  case 3 => (N, N, N)
  case 4 => (N, N, N, N)

so now I can declare my vectors using tuples:

  val v2: V[2, Int] = (2, 2)
  val v3: V[3, Int] = (3, 3, 3)
  val v4: V[4, Int] = (4, 4, 4, 4)

and then I can define a tuple-matrix and a tuple-square-matrix:

type Mx[L <: Int, C <: Int, N] = V[L, V[C, N]]
type Mxq[T <: Int, N] = Mx[T, T, N]
type M3I = Mxq[3, Int]

everything is fine until now:

  //Compiles
  val m3: M3I = (
    (1, 0, 0),
    (0, 1, 0),
    (0, 0, 1)
  )

  //Doesn't compile
  val m3Err: M3I = (
    (1, 0, 0, 1),
    (0, 1, 0),
    (0, 0, 1)
  )

finally I define extension methods to manipulate the matrices

 extension[L <: Int, C <: Int, N] (essa: Mx[L, C, N])

    @implicitNotFound(msg = "Não é possível multiplicar as matrizes pois ${C} != ${LB}")
    def *[LB <: Int, CB <: Int](outra: Mx[LB, CB, N])(using ev: C =:= LB) = ???

but when I try to use it with m1 * m2 (which are both 3x3 matrices) i get this compiler error:

value * is not a member of (TestesKoinos.V[(3 : Int), Int], TestesKoinos.V[(3 : Int), Int], 
  TestesKoinos.V[(3 : Int), Int]
).
An extension method was tried, but could not be fully constructed:

    TestesKoinos.*[L, C, N](m1)[LB, CB]    failed with

        Found:    (TestesKoinos.m1 : (TestesKoinos.V[(3 : Int), Int], 
          TestesKoinos.V[(3 : Int), Int]
        , TestesKoinos.V[(3 : Int), Int]))
        Required: TestesKoinos.Mx[L, C, N]
        
        where:    C is a type variable with constraint <: Int
                  L is a type variable with constraint <: Int
                  N is a type variable
        
        Note: a match type could not be fully reduced:
        
          trying to reduce  TestesKoinos.Mx[L, C, N]
          trying to reduce  TestesKoinos.V[L, TestesKoinos.V[C, N]]
          failed since selector  L
          does not match  case (2 : Int) => (TestesKoinos.V[C, N], TestesKoinos.V[C, N])
          and cannot be shown to be disjoint from it either.
          Therefore, reduction cannot advance to the remaining cases
        
            case (3 : Int) => (TestesKoinos.V[C, N], TestesKoinos.V[C, N], TestesKoinos.V[C, N])
            case (4 : Int) => (TestesKoinos.V[C, N], TestesKoinos.V[C, N], TestesKoinos.V[C, N], 
          TestesKoinos.V[C, N]
        )
  m1 * m2

What is wrong with my code/logic here?

Flier

I do not full understand what happens here, but the problem is more general... Indeed, even if I try to define a method as: def test[I <: Int, C <: Int, N](a : Mx[I, C, Int]) = a and then I call test(m3) the compiler gives the same error as the implicit extension resolution. It seems that it cannot prove that Mx[L, C, N] =:= M3I... Very strange. – Canaletto

Yeah this feels like a bug in the compiler, it seems extension methods and match types don't work well together. – Bridewell

@gianlucaaguzzi In this case it works as long as you explicit the type parameters, like: test[3, 3, Int](m3) – Flier