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)
}

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