An attempt to use match types for a safe apply in scala 3

sized_list.scala

package sizetypes

import scala.compiletime.ops.int

type LessThan[A <: Int] =
  A match              
    case 0 => Nothing                                                                                          
    case _ =>                                                                   
      int.-[A, 1] | LessThan[int.-[A, 1]]
                                                                                
val two: LessThan[3] = 2

def zeroOrDec[A <: Int](idx: LessThan[int.S[A]]): Either[LessThan[A], 0] =    
  ???
  /*
  How can we implement this method?
  if idx == 0 then Right(0)
  else  
    // we know 0 < idx < S[A], so idx - 1 is 0 <= idx < A == LessThan[A]
    // how can we get scala to see it?
    val prev: LessThan[A] = (idx - 1)                 
    Left(prev)
    */
     
sealed abstract class SList[Z <: Int, +A] {
  def apply(idx: LessThan[Z]): A 
  
  def ::[A1 >: A](item: A1): SList.Cons[Z, A1] =       
    SList.Cons(item, this)
} 

object SList {
  
  sealed abstract class IntEv[A <: Int, B <: Int] {
    def subst[F[_ <: Int]](fa: F[A]): F[B]
  } 
  
  object IntEv {
    implicit def reflIntEv[A <: Int]: IntEv[A, A] =  
      new IntEv[A, A] {
        def subst[F[_ <: Int]](fa: F[A]) = fa
      } 
  } 
  
  case class SNil[Z <: Int](ev: IntEv[Z, 0]) extends SList[Z, Nothing] { 
    def apply(idx: LessThan[Z]): Nothing = {
      val ltz: LessThan[0] = ev.subst[LessThan](idx)       
      // LessThan[0] == Nothing
      ltz
    }                    
  } 
  
  case class Cons[Z <: Int, +A](head: A, tail: SList[Z, A]) extends SList[int.S[Z], A] {
    def apply(idx: LessThan[int.S[Z]]): A =  
      zeroOrDec(idx) match                   
        case Left(lookTail) => tail(lookTail)
        case Right(_) => head
  } 
  
  def empty: SList[0, Nothing] = SNil(IntEv.reflIntEv[0])

  val oneTwoThree = 1 :: 2 :: 3 :: empty

  val one = oneTwoThree(0)
}

I managed to make your encoding (with some changes) to work too:

package original

import scala.annotation.tailrec
import scala.compiletime.ops.int.*
import scala.compiletime.constValue

trait LessThan[Z <: Int] { self =>
  def value: Int
  def pred: LessThan[Z - 1] = new LessThan[Z - 1] {
    override def value: Int = self.value - 1
  }
}

inline implicit def intToLessThanValue[I <: Int & Singleton, Z <: Int](i: I): LessThan[Z] =
  inline if (constValue[I] < constValue[Z]){
    new LessThan[Z] {
      def value: Int = i
    }
  } else {
    scala.compiletime.error("wrong")
  }

implicit def inference[Z <: Int](i: LessThan[S[Z] - 1]): LessThan[Z] =
  new LessThan[Z] {
    override def value: Int = i.value
  }

def zeroOrDec[Z <: Int](idx: LessThan[Z]): Either[LessThan[Z - 1], 0] =
  if idx.value == 0
    then Right(0)
    else
      // without `def inference` it was returning:
      // Found:    (lookTail : original.LessThan[compiletime.ops.int.S[Z] - (1 : Int)])
      // [error]      Required: original.LessThan[Z]
      // We know that: S[Z] - 1 =:= Z but compiler cannot deduce it (I guess in principle it could?)
      // So we manually add inference rule
      val prev: LessThan[Z - 1] = idx.pred
      Left(prev)

sealed abstract class SList[Z <: Int, +A] {
  def apply(idx: LessThan[Z]): A

  def ::[A1 >: A](item: A1): SList.Cons[Z, A1] =
    SList.Cons(item, this)
}

object SList {

  sealed abstract class IntEv[A <: Int, B <: Int] {
    def subst[F[_ <: Int]](fa: F[A]): F[B]
  }

  object IntEv {
    implicit def reflIntEv[A <: Int]: IntEv[A, A] =
      new IntEv[A, A] {
        def subst[F[_ <: Int]](fa: F[A]) = fa
      }
  }

  case class SNil[Z <: Int](ev: IntEv[Z, 0]) extends SList[Z, Nothing] {
    def apply(idx: LessThan[Z]): Nothing = {
      val ltz: LessThan[0] = ev.subst[LessThan](idx)
      // LessThan[0] == Nothing
      ???
    }
  }

  case class Cons[Z <: Int, +A](head: A, tail: SList[Z, A]) extends SList[S[Z], A] {
    def apply(idx: LessThan[S[Z]]): A =
      zeroOrDec(idx) match
        case Left(lookTail) => tail(lookTail)
        case Right(_) => head
  }

}

object OriginalExample:
  @main def main(): Unit =
    def empty: SList[0, Nothing] = SList.SNil(SList.IntEv.reflIntEv[0])
    val oneTwoThree = 1 :: 2 :: 3 :: empty

    val one = oneTwoThree(0)
    val three = oneTwoThree(2)
    // val abc = oneTwoThree(3) // does not compile
    println("one: " + one)
    println("three: " + three)

The crucial change is adding def pred: LessThan[Z - 1] and to do that I had to turn LessThan into trait. Another tricky point was adding inference.

I don't think your original def zeroOrDec[A <: Int](idx: LessThan[int.S[A]]): Either[LessThan[A], 0] is implementable. It's because idx - 1, even if you somehow managed minus working, is of type Int. You can see that in much simpler example:

val two: 0 | 1 | 2 = 2
val a: 0 | 1 | 2 = two - 1 // does not compile as right side is of type Int

You're not able to define any methods on LessThan as long as it's a type and I think defining predecessor method with proper return type is a key in this exercise

Thanks for thinking through this.

I think making something like the original work would be nice, since the LessThan[A] type could be erased to Int.

I added this discussion:
https://contributors.scala-lang.org/t/math-on-union-numeric-union-types/5095/3