special case 0 and S[n] in provably disjoint #14572
Description
It would be useful if 0 and S[n] could be treated as provably disjoint - currently you need to make a Nat enum to get sensible behaviour from match types, however Nat is inefficient to materialise
Originally posted by @bishabosha in #14549 (comment):
I think really the issue is that 0 and S[n] are not treated like independent class types, for example, if we substitute Int for some Nat enum then the example works unchanged:
enum Nat { case Zero case Succ[N <: Nat](pred: N) } object Nat { type FromInt[I <: Int] <: Nat = I match { case 0 => Nat.Zero.type case compiletime.ops.int.S[n] => Nat.Succ[FromInt[n]] } } /// begin of example import scala.compiletime.ops.int.* type Fill[N <: Nat, A] <: Tuple = N match { case Nat.Zero.type => EmptyTuple case Nat.Succ[n] => A *: Fill[n, A] } sealed trait SeqToTuple[N <: Nat] { def apply[A](s: Seq[A]): Fill[N, A] } implicit val emptyToZero: SeqToTuple[Nat.Zero.type] = new SeqToTuple[Nat.Zero.type] { override def apply[A](s: Seq[A]): EmptyTuple = EmptyTuple } implicit def successorToSuccessor[N <: Nat](implicit pred: SeqToTuple[N]): SeqToTuple[Nat.Succ[N]] = new SeqToTuple[Nat.Succ[N]] { override def apply[A](s: Seq[A]): Fill[Nat.Succ[N], A] = s.head *: pred(s.tail) // Scala doesn't know that `A *: Fill[N, A]` = `Fill[S[N], A]` for some reason } // scala> summon[SeqToTuple[Nat.FromInt[3]]](List(1,2,3,4,5)) // val res1: Int *: Int *: Int *: EmptyTuple = (1,2,3)