Recursive match type fails to type check

[mpilquist]

minimized code

scala> type I[A <: Tuple] <: Tuple = A match {
     |   case Unit => Unit
     |   case hd *: tl => hd *: I[tl]
     | }

scala> (1, 2): I[(Int, Int)]
val res4: (Int, Int) = (1,2)

scala> type DU[A <: Tuple] <: Tuple = A match {
     |   case Unit => Unit
     |   case Unit *: tl => DU[tl]
     |   case hd *: tl => hd *: DU[tl]
     | }

scala> (1, 2): DU[(Int, Int)]
1 |(1, 2): DU[(Int, Int)]
  |^^^^^^
  |Found:    (Int, Int)
  |Required: DU[(Int, Int)]

expectation

DU[(Int, Int)] should expand to (Int, Int) but doesn't. Only difference between DU and I (which works), is the Unit *: tl case.

[odersky]

I guess this has to do with overlapping patterns? /cc @OlivierBlanvillain

[mpilquist]

Thanks -- overlapping patterns comment was enough to figure out a workaround:

import scala.compiletime._

object DropUnits {
  type T[A <: Tuple] <: Tuple = A match {
    case hd *: tl => hd match {
      case Unit => T[tl]
      case _ => hd *: T[tl]
    }
    case Unit => Unit
  }

  inline def drop[A <: Tuple](a: A): T[A] = {
    inline erasedValue[A] match {
      case _: (Unit *: tl) => drop[tl](a.asInstanceOf[Unit *: tl].tail)
      case _: (hd *: tl) => a.asInstanceOf[hd *: tl].head *: drop[tl](a.asInstanceOf[hd *: tl].tail)
      case _: Unit => ()
    }
  }.asInstanceOf[T[A]]

  inline def insert[A <: Tuple](t: T[A]): A = {
    inline erasedValue[A] match {
      case _: (Unit *: tl) => (()) *: (insert[tl](t.asInstanceOf[T[tl]]))
      case _: (hd *: tl) =>
        val t2 = t.asInstanceOf[NonEmptyTuple]
        t2.head.asInstanceOf[hd] *: insert[tl](t2.tail.asInstanceOf[T[tl]])
      case _: Unit => ()
    }
  }.asInstanceOf[A]
}

[OlivierBlanvillain]

The issue here is that the compiler is unable to reduce passed case Unit *: tl =>, because it cannot prove that (Int, Int) and Unit *: tl are disjoint. Looking at the definition of *:, the compiler doesn't have enought information to conclude that there are no value of type (Int & Unit) *: Unit.