special case 0 and S[n] in provably disjoint

[bishabosha]

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 https://github.com/lampepfl/dotty/issues/14549#issuecomment-1050881334:

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)

[bishabosha]

is this possible?

[sjrd]

Doesn't 0 match S[-1]?

[bishabosha]

Doesn't 0 match S[-1]?

type Foo[I <: Int] <: Int = I match { case compiletime.ops.int.S[n] => n }

scala> val m: Foo[1] = 0
val m: 0 = 0

scala> val m: Foo[0] = -1
-- [E007] Type Mismatch Error: -------------------------------------------------
1 |val m: Foo[0] = -1
  |                ^^
  |                Found:    (-1 : Int)
  |                Required: Foo[(0 : Int)]
  |
  |                Note: a match type could not be fully reduced:
  |
  |                  trying to reduce  Foo[(0 : Int)]
  |                  failed since selector  (0 : Int)
  |                  does not match  case compiletime.ops.int.S[n] => n
  |                  and cannot be shown to be disjoint from it either.

scala> val m: Foo[-1] = -2
-- [E007] Type Mismatch Error: -------------------------------------------------
1 |val m: Foo[-1] = -2
  |                 ^^
  |                 Found:    (-2 : Int)
  |                 Required: Foo[(-1 : Int)]
  |
  |                 Note: a match type could not be fully reduced:
  |
  |                   trying to reduce  Foo[(-1 : Int)]
  |                   failed since selector  (-1 : Int)
  |                   does not match  case compiletime.ops.int.S[n] => n
  |                   and cannot be shown to be disjoint from it either.

[dwijnand]

Glancing, it looks like this is already special-cased in TypeComparer: https://github.com/lampepfl/dotty/blob/482c67e894805c83e256c22f2106929b28366e77/compiler/src/dotty/tools/dotc/core/TypeComparer.scala#L1261

Personally I would rather not continue to special-case here and there, but rather implement a general way to declare sealed types. But then I would say that...

[sjrd]

If this is still desired, it should be brought up in SIP-56 Proper Specification for Match Types. After, it will be too late.

[bishabosha]

@sjrd given that S is getting a special case in the logic of match types, then it wouldn't be too far of a stretch to add it to disjointness maybe?