Scala 3: typed tuple zipping

I'm trying to zip tuples together and use match types to get the exact type of the resulting zip. I have a match type and the function:

  type Z[A <: Tuple, B <: Tuple] <: Tuple = (A, B) match
    case (EmptyTuple, EmptyTuple) => EmptyTuple
    case (a *: as, b *: bs) => (a, b) *: Z[as, bs]

  def z[A <: Tuple, B <: Tuple](a: A, b: B): Z[A, B] = (a, b) match
    case (EmptyTuple, EmptyTuple) => EmptyTuple
    case (ah *: at, bh *: bt) => (ah, bh) *: z(at, bt)

However, both cases in z() result in an error: Found: EmptyTuple.type Required: test.Tuples.Z[A, B] and Found: (Any, Any) *: test.Tuples.Z[Tuple, Tuple] Required: test.Tuples.Z[A, B], respectively. I would have guessed this would be a pretty straightforward application of match types, but clearly I'm wrong. What am I missing here?

I would also like to restrict both the match type and the function z() to tuples that have the same length (like how shapeless' Length could be used in scala 2), but perhaps that is a separate question.

EDIT:

I managed to get the function z() working with explicit casting, but I still think there has to be a way to avoid that:

  def z[A <: Tuple, B <: Tuple, M <: Int](a: A, b: B): Z[A, B] = (a, b) match
    case (ah *: at, bh *: bt) => ((ah, bh) *: z(at, bt)).asInstanceOf[Z[A, B]]
    case (EmptyTuple, EmptyTuple) => EmptyTuple.asInstanceOf[Z[A, B]]

Also, I was able to get the length aspect working for the function z() as well, but I would love to know if a) there is a cleaner/less verbose way to achieve this (perhaps without the need to define L) and b) if there's a way to restrict the type arguments to Z to be tuples of the same length:

  type L[T <: Tuple] <: Int = T match
    case EmptyTuple => 0
    case _ *: t => 1 + L[t]

  type Z[A <: Tuple, B <: Tuple] <: Tuple = (A, B) match
    case (EmptyTuple, EmptyTuple) => EmptyTuple
    case (a *: as, b *: bs) => (a, b) *: Z[as, bs]

  def z[A <: Tuple, B <: Tuple, M <: Int](a: A, b: B)(using L[A] =:= L[B]): Z[A, B] = (a, b) match
    case (ah *: at, bh *: bt) => ((ah, bh) *: z(at, bt)).asInstanceOf[Z[A, B]]
    case (EmptyTuple, EmptyTuple) => EmptyTuple.asInstanceOf[Z[A, B]]

  println(z(1 *: true *: EmptyTuple, "seven" *: 9.8 *: EmptyTuple)) // <-- correctly zips tuples: ((1,seven),(true,9.8))

//    println(z(1 *: EmptyTuple, "seven" *: 9.8 *: EmptyTuple)) // <-- results in compile-time error as desired: "Cannot prove that test.Tuples.L[(Int *: EmptyTuple.type)] =:= test.Tuples.L[(String, Double)]..."

EDIT 2: So actually it turns out that the tuple lengths are already restricted to be equal, as otherwise the match type Z does not resolve, so I guess the question is just how to avoid the casts in z().

Currently match types have many limitations on value level:

This special mode of typing for match expressions is only used when the following conditions are met:

1. The match expression patterns do not have guards
2. The match expression scrutinee's type is a subtype of the match type scrutinee's type
3. The match expression and the match type have the same number of cases
4. The match expression patterns are all Typed Patterns, and these types are =:= to their corresponding type patterns in the match type

Your code

type Z[A <: Tuple, B <: Tuple] <: Tuple = (A, B) match
  case (EmptyTuple, EmptyTuple) => EmptyTuple
  case (a *: as, b *: bs) => (a, b) *: Z[as, bs]

def z[A <: Tuple, B <: Tuple](a: A, b: B): Z[A, B] = (a, b) match
  case (EmptyTuple, EmptyTuple) => EmptyTuple
  case (ah *: at, bh *: bt) => (ah, bh) *: z(at, bt)

breaks condition 4. case (EmptyTuple, EmptyTuple) and case (ah *: at, bh *: bt) are not typed patterns.

It would make sense to try

type Z[A <: Tuple, B <: Tuple] <: Tuple = (A, B) match
  case (EmptyTuple, EmptyTuple) => EmptyTuple
  case (a *: as, b *: bs) => (a, b) *: Z[as, bs]

def z[A <: Tuple, B <: Tuple](a: A, b: B): Z[A, B] = (a, b) match
  case _: (EmptyTuple, EmptyTuple) => EmptyTuple
  case t: (_ *: _, _ *: _) => t match
    case (ah *: at, bh *: bt) => (ah, bh) *: z(at, bt)

but unfortunately this doesn't work because of type erasure

z((1, "a"), (true, 2.0)) // ()

Actually, case _: (EmptyTuple, EmptyTuple) and case t: (_ *: _, _ *: _) are just case _: (_, _) and match everything. And if we swap the cases then z((1, "a"), (true, 2.0)) throws runtime exception (java.lang.IndexOutOfBoundsException: 0).

The following approach with nested match types/pattern matchings seems to work

type Z[A <: Tuple, B <: Tuple] <: Tuple = A match
  case EmptyTuple => Z1[B]
  case a *: as => Z2[a, as, B]

type Z1[B <: Tuple] <: Tuple = B match
  case EmptyTuple => EmptyTuple

type Z2[A, As <: Tuple, B <: Tuple] <: Tuple = B match
  case b *: bs => (A, b) *: Z[As, bs]

def z[A <: Tuple, B <: Tuple](a: A, b: B): Z[A, B] = a match
  case _: EmptyTuple => z1(b)
  case a1: (_ *: _) => a1 match
    case a2 *: as => z2(a2, as, b)

def z1[B <: Tuple](b: B): Z1[B] = b match
  case _: EmptyTuple => EmptyTuple

def z2[A, As <: Tuple, B <: Tuple](a: A, as: As, b: B): Z2[A, As, B] = b match
  case b1: (_ *: _) => b1 match
    case b2 *: bs => (a, b2) *: z(as, bs)

// compiles
summon[Z[(Int, String), (Boolean, Double)] =:= ((Int, Boolean), (String, Double))]

z((1, "a"), (true, 2.0)) // ((1,true),(a,2.0))

//   doesn't compile
// summon[Z[(Int, String, Long), (Boolean, Double)] =:= ((Int, Boolean), (String, Double))]
// z((1, "a", 3L), (true, 2.0))
//   Match type reduction failed since selector EmptyTuple.type
//   matches none of the cases
//     case b *: bs => (Long, b) *: Z[EmptyTuple.type, bs]

//   doesn't compile
// summon[Z[(Int, String), (Boolean, Double, Long)] =:= ((Int, Boolean), (String, Double))]
// z((1, "a"), (true, 2.0, 3L))
//   Match type reduction failed since selector  Long *: EmptyTuple.type
//   matches none of the cases
//     case EmptyTuple => EmptyTuple 

How to get match type to work correctly in Scala 3

Shapeless3 and annotations