How to implement HList literal type constraints?

Question

I'm trying to do some calculations on HList types (to enforce a tensor algebra). I'm failing so far, using 2.13.0-M4.

Here is the challenge:

type XInt = Int with Singleton
def mult[N <: XInt, M <: XInt, P <: XInt, T <: HList]
     (a: N :: M :: T, b: M :: P :: T): N :: P :: T= ???
val a = 8.narrow :: 4.narrow :: HNil
val b = 4.narrow :: 5.narrow :: HNil
mult(a, b) // should yield 8 :: 5 :: HNil

Answer 1

Try

def mult[N <: XInt, M <: XInt, P <: XInt, T <: HList](a: N :: M :: T, b: M :: P :: T): N :: P :: T = 
  (a, b) match { case (n :: _ :: t, _ :: p :: _) => n :: p :: t }

or

def mult[N <: XInt, M <: XInt, P <: XInt, T <: HList](a: N :: M :: T, b: M :: P :: T): N :: P :: T = 
  a.head :: b.tail.head :: b.tail.tail

or simply

def mult[N <: XInt, M <: XInt, P <: XInt, T <: HList](a: N :: M :: T, b: M :: P :: T): N :: P :: T = 
  a.head :: b.tail