Dependently Typed Vector in Scala

Vec.scala

package dependent

import scala.language.implicitConversions

import shapeless._, shapeless.nat._

object Vector {
  trait Vec[+A, N <: Nat]

  case object Nil extends Vec[Nothing, _0]

  case class Cons[+A, N <: Nat](h: A, t: Vec[A, N]) extends Vec[A, Succ[N]]

  implicit def narrow[A, N <: Nat](v: Vec[A, Succ[N]]): Cons[A, N] = v match {
    case vc @ Cons(_, _) => vc
  }

  trait SNat[A, N <: Nat] {
    def apply(a: A): Vec[A, N]
  }

  implicit def zNat[A] = new SNat[A, _0] {
    def apply(a: A) = Nil
  }

  implicit def sNat[A, N <: Nat](implicit nat: SNat[A, N]) =
    new SNat[A, Succ[N]] {
      def apply(a: A) = Cons(a, rep[A, N](a))
    }

  def rep[A, N <: Nat](a: A)
    (implicit snat: SNat[A, N]): Vec[A, N] = snat(a)

  trait Plus[A, XS, YS] {
    type MN <: Nat
    type Out = Vec[A, MN]
    def apply(xs: XS, ys: YS): Out
  }

  implicit def zPlus[A, N <: Nat] =
    new Plus[A, Vec[A, _0], Vec[A, N]] {
      type MN = N
      def apply(xs: Vec[A, _0], ys: Vec[A, N]): Out = ys
    }

  implicit def sPlus[A, M <: Nat, N <: Nat]
    (implicit tail: Plus[A, Vec[A, M], Vec[A, N]]) =
    new Plus[A, Vec[A, Succ[M]], Vec[A, N]] {
      type MN = Succ[tail.MN]
      def apply(xs: Vec[A, Succ[M]], ys: Vec[A, N]): Out =
        Cons(xs.h, app(xs.t, ys))
    }

  def app[A, N <: Nat, M <: Nat](xs: Vec[A, N], ys: Vec[A, M])
    (implicit plus: Plus[A, Vec[A, N], Vec[A, M]]): plus.Out =
    plus(xs, ys)
}