Nested dependent matching fails

[jpablo]

Compiler version

3.2

Minimized code

import compiletime.ops.int._
import compiletime.constValue

type Elem[X <: Tuple, N <: Int] = X match
  case x *: xs =>
    N match
      case 0 => x
      case S[k] => Elem[xs, k]

inline def elem[X <: Tuple, N <: Int](x: X, n: N) : Elem[X, N] = x match
  case (h *: t): (x *: _) =>
    inline n match
      case _: 0    => h
      case _: S[k] => elem(t, constValue[k])

Output

[error] 37 |      case _: 0    => h
[error]    |                      ^
[error]    |               Found:    (h : x)
[error]    |               Required: N match {
[error]    |                 case (0 : Int) => x
[error]    |                 case compiletime.ops.int.S[k] => Elem[_, k]
[error]    |               }
[error]    |
[error]    |               where:    N is a type in method elem with bounds <: Int
[error]    |                         _ is a type in method elem with bounds <: Tuple
[error]    |                         x is a type in method elem with bounds 
[error]    |
[error]    | longer explanation available when compiling with `-explain`
[error] -- [E007] Type Mismatch Error: .../src/main/scala/Part3.scala:38:26 
[error] 38 |      case _: S[k] => elem(t, constValue[k])
[error]    |                      ^^^^^^^^^^^^^^^^^^^^^^
[error]    |              Found:    Elem[_, k]
[error]    |              Required: N match {
[error]    |                case (0 : Int) => x
[error]    |                case compiletime.ops.int.S[k²] => Elem[_, k²]
[error]    |              }
[error]    |
[error]    |              where:    N  is a type in method elem with bounds <: Int
[error]    |                        _  is a type in method elem with bounds <: Tuple
[error]    |                        k  is a type in method elem with bounds <: Int
[error]    |                        k² is a type variable with constraint <: Int
[error]    |                        x  is a type in method elem with bounds 
[error]    |
[error]    |
[error]    |              Note: a match type could not be fully reduced:
[error]    |
[error]    |                trying to reduce  Elem[_, k]
[error]    |                failed since selector  _
[error]    |                does not match  case x *: xs => k match {
[error]    |                case (0 : Int) => x
[error]    |                case compiletime.ops.int.S[k] => Elem[xs, k]
[error]    |              }
[error]    |                and cannot be shown to be disjoint from it either.
[error]    |
[error]    | longer explanation available when compiling with `-explain`

Expectation

The code should compile.

[mbovel]

This compiles in Scala 3.3, but emits the following warning:

Compiling project (Scala 3.3.0, JVM)
[warn] ./sync.scala:11:16
[warn] Type ascriptions after patterns other than:
[warn]   * variable pattern, e.g. `case x: String =>`
[warn]   * number literal pattern, e.g. `case 10.5: Double =>`
[warn] are no longer supported. Remove the type ascription or move it to a separate variable pattern.
[warn]   case (h *: t): (x *: _) =>
[warn]                ^
[warn] ./sync.scala:10:66
[warn] match may not be exhaustive.
[warn] 
[warn] It would fail on pattern case: EmptyTuple
[warn] inline def elem[X <: Tuple, N <: Int](x: X, n: N) : Elem[X, N] = x match
[warn]