More evidence needed than necessary for method using Shapeless

Question

I was exploring Shapeless with a few colleagues yesterday, and we decided to write a toy method to add one to the first parameter of a case class, when that parameter is an Int:

def addOneToCaseClass[C, H <: HList, E, T <: HList]
    (c: C)
    (implicit gen: Generic.Aux[C, H],
              h:   IsHCons.Aux[H, E, T],
              ev:  E =:= Int,
              ev2: (Int :: T) =:= H
    ): C = {

  val hList = gen.to(c)

  val elem = hList.head
  val tail = hList.tail

  val newElem = elem + 1

  gen.from(newElem :: tail)
}

It seems to me that the ev2 parameter is redundant - surely it can be inferred that E :: T =:= Int :: T, but the compiler was not able to make that happen.

Is there a particular reason why?

Answer 1

Your intuitions are reasonable, but unfortunately the Scala compiler isn't quite clever enough to derive ev2 from h and ev. The problem is that h only establishes that H decomposes to E :: T, it doesn't establish the converse, namely that E and T combine to equal H.

The tersest formulation of this that I can come up with is similar to your original, but has one less witness,

def addOneToCaseClass[C, R <: HList, T <: HList](c: C)
  (implicit
    gen: Generic.Aux[C, R],
    h: IsHCons.Aux[R, Int, T],
    ev: (Int :: T) =:= R) = {
  val hList = gen.to(c)
  val elem = hList.head
  val tail = hList.tail
  gen.from(elem+1 :: tail)
}

Here we're able to eliminate the proof that E =:= Int by using h to show that R decomposes to Int :: T. However we still need to show that Int :: T is equal to R to move back across gen with the updated elements.