Match type does not check bounds

[bishabosha]

Compiler version

Scala 3.1.1-RC1-bin-20211008-0a89c6f-NIGHTLY-git-0a89c6f

Minimized code

type Init[X <: NonEmptyTuple] <: Tuple = X match {
  case _ *: EmptyTuple => EmptyTuple
  case x *: xs => x *: Init[xs] // statically `xs` does not match, in practice it will not fail
}

Output

compiles ok

Expectation

A static failure for the recursive step as xs is not <: NonEmptyTuple, or is all checking left until a concrete type is applied?

[soronpo]

I think it is the required behavior. Type matches check bounds somewhat lazily, when the type is more concrete.
It's equivalent to a method that only can invoke runtime error when it's actually running.

[dwijnand]

Fix

         case m @ MatchTypeTree(bounds, selector, cases) =>
           // Analog to the case above for match types
           def transformIgnoringBoundsCheck(x: CaseDef): CaseDef =
-            withMode(Mode.Pattern)(super.transform(x)).asInstanceOf[CaseDef]
+            val CaseDef(pat, guard, body) = x
+            cpy.CaseDef(tree)(inMode(Mode.Pattern)(transform(pat)), transform(guard), transform(body))
+
           cpy.MatchTypeTree(tree)(
             super.transform(bounds),
             super.transform(selector),

using the example

import scala.NonEmptyTuple

type Init[X <: NonEmptyTuple] <: Tuple = X match
  case EmptyTuple => EmptyTuple
  case x *: xs => x *: Init[xs]

def a: Init[Tuple3[Int, String, Boolean]] = ???

[sjrd]

I think it is the required behavior. Type matches check bounds somewhat lazily, when the type is more concrete. It's equivalent to a method that only can invoke runtime error when it's actually running.

Taking the analogy of term levels, it would not be about run-time errors but about type errors, in the sense that a term t: T is used where U is expected but T </: U. For example

def init(x: ::[Int]): List[Int] = x match
  case _ :: Nil => Nil
  case x :: xs => x :: init(xs) // statically type error because xs: List[Int] </: ::[Int]

So IMO this should be a compile error.

@dwijnand Do you want to pursue your fix as a PR?