implementing typelevel Nat tracking in scala 3

NatInc.scala

package example    
    
sealed trait Nat     
case object Zero extends Nat    
case class Succ[N <: Nat](n: N) extends Nat       
                
type Inc[N <: Nat] <: Nat =                
  N match {     
    case Zero.type => Succ[Zero.type]    
    case Succ[n] => Succ[Inc[n]]    
  }             
                
object Nat {    
  def inc[N <: Nat](n: N): Inc[N] =
    // it's important to match on the type below, or it won't unify (for some reason)
    n match {    
      case _: Zero.type => Succ(Zero)                                      
      case s: Succ[a] => Succ(inc(s.n))                     
    }                                 
}