Can this code be tweaked so that it compiles?
In it, I first define type-level natural numbers:
sealed trait NatT
case class Zero() extends NatT
case class Succ[N<: NatT](n: N) extends NatT
Then, I define a comparison predicate:
trait IsLessThan[M <: NatT, N <: NatT]
object IsLessThan:
given base[M <: NatT]: IsLessThan[M, Succ[M]]()
given weakening[N <: NatT, M <: NatT] (using IsLessThan[N, M]): IsLessThan[N, Succ[M]]()
given reduction[N <: NatT, M <: NatT] (using IsLessThan[Succ[N], Succ[M]]): IsLessThan[N, M]()
Finaly, I define UniformTuple. I want it to have a method to get the ith element of the tuple, and I want the method to be fully type-safe (no possible runtime exceptions due to out-of-bound indices), so the method demands a proof that the index is within bounds:
sealed trait UniformTuple[Length <: NatT, T]:
def apply[M <: NatT](m: M)(using IsLessThan[M, Length]): T
case class Empty[T: Fractional]() extends UniformTuple[Zero, T]:
def apply[M <: NatT](m: M)(using IsLessThan[M, Zero]): T = throw new AssertionError("Uncallable")
case class Cons[N <: NatT, T: Fractional](head: T, tail: UniformTuple[N, T]) extends UniformTuple[Succ[N], T]:
def apply[M <: NatT](m: M)(using proof: IsLessThan[M, Succ[N]]): T = m match
case Zero() => head
case Succ(predM): Succ[predM] => tail(predM)(using IsLessThan.reduction(using proof))
However, I cannot get the recursion to go through, as the compiler apparently doesn’t know that Succ[predM] is the same as M…