Can't write type-safe implementations of Tuple methods

[TomasMikula]

The implementations of Tuple methods delegate to unsafe runtime.Tuples methods and then use a type cast (asInstanceOf).

Tuples bring generic programming to Scala 3 shows how we could safely implement the ++ (concat) method.

However, I'm at a loss to know how to safely implement other methods, such as drop, take, splitAt, to the point that I don't think it's possible (but perhaps just undocumented?).

Below is a failed attempt at implementing the drop method. I would be happy to be shown the correct way, but for now I just think it is not possible.

Compiler version

3.0.0-RC

Minimized example

import compiletime._
import compiletime.ops.int._
import Tuple.Drop

def drop[T <: Tuple, N <: Int](t: T, n: N): Drop[T, N] =
  n match {
    case _ : 0 => t
    case n : S[n1] => t match {
      case _ : EmptyTuple => EmptyTuple
      case (_ *: t1): (_ *: t1) => drop[t1, n1](t1, n-1)
    }
  }

Output

-- [E007] Type Mismatch Error: drop.scala:9:29 ---------------------------------
9 |      case _ : EmptyTuple => EmptyTuple
  |                             ^^^^^^^^^^
  |Found:    EmptyTuple.type
  |Required: T match {
  |  case EmptyTuple => EmptyTuple
  |  case 
  |    [x, xs <: Tuple] =>> 
  |      scala.runtime.MatchCase[x *: xs, LazyRef(scala.Tuple.Drop[xs, n1])]
  |} <: Tuple
  |
  |where:    T  is a type in method drop with bounds >: (?1 : EmptyTuple.type) and <: Tuple
  |          n1 is a type in method drop with bounds <: Int

longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: drop.scala:10:52 --------------------------------
10 |      case (_ *: t1): (_ *: t1) => drop[t1, n1](t1, n-1)
   |                                                    ^^^
   |                Found:    Int
   |                Required: n1
   |
   |                where:    n1 is a type in method drop with bounds <: Int

longer explanation available when compiling with `-explain`
2 errors found

[odersky]

Moving to discussions. It would be good if others could participate.