scala3 icon indicating copy to clipboard operation
scala3 copied to clipboard

Nested dependent matching fails

Open jpablo opened this issue 3 years ago • 0 comments

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.

jpablo avatar Sep 10 '22 19:09 jpablo