sameLength(3)

gistfile1.scala

object Test extends App {
  sealed trait Nat
  case class Zero private (dummy: Zero) extends Nat
  case class Succ[T <: Nat] private (dummy: Succ[T]) extends Nat

  sealed abstract class Vec[L <: Nat, +T]
  case object VNil extends Vec[Zero, Nothing]
  case class VCons[L <: Nat, +T](head: T, tail: Vec[L, T]) extends Vec[Succ[L], T]
  
  def fromList[T, R](l: List[T])(k: (Vec[A, T] forSome {type A <: Nat}) => R): R = {
    if (l.isEmpty) {
      k(VNil)
    } else {
      fromList(l.tail)(v => k(VCons(l.head, v)))
    }
  }

  def eqType[A <: Nat, B <: Nat](a: Vec[A, _])(b: Vec[B, _])(implicit ev: A =:= B) = {}

  def sameLength[L1 <: Nat, L2 <: Nat, T1, T2](
    v1: Vec[L1, T1],
    v2: Vec[L2, T2]
  ): Option[(Vec[L1, T1], Vec[L1, T2])] = {
    def rec[L1 <: Nat, L2 <: Nat, T1, T2](
      v1: Vec[L1, T1],
      v2: Vec[L2, T2]
    ): Boolean = {
      (v1, v2) match {
        case (VNil, VNil) => true
        case (VCons(h1, t1), VCons(h2, t2)) => rec(t1, t2)
        case _ => false
      }
    }
    if (rec(v1, v2)) Some((v1, v2.asInstanceOf[Vec[L1, T2]]))
    else None
  }

  def test = {
    fromList(List(1, 2, 3)){ v1 =>
      fromList(List(10, 20, 30)){ v2 =>
        fromList(List(100, 200, 300)){ v3 =>
        sameLength(v1, v2) match {
          case Some((v1, v2)) =>
            //eqType(v2)(v3) //compile error
            sameLength(v1, v3) match {
              case Some((v1, v3)) => eqType(v2)(v3)
            }
          }
        }
      }
    }
  }

  test
}