Swapping the first two values of a case class, when their type is the same

shapeless.scala

  // Given a case class where the first two elements have the same type, swap those values:
  def swap[T, U <: HList, H1, H2, T1 <: HList, T2 <: HList](v: T)(
    implicit // proofs:

      // Case class T can be represented by U
      // (U is an output, must be used as an output before using it as an input in the proofs below)
      gen: Generic.Aux[T, U],

      // U is composed of H1 :: T1
      isc1: IsHCons.Aux[U, H1, T1],

      // T1 is composed of H2 :: T2
      isc2: IsHCons.Aux[T1, H2, T2],

      // The HList H2 :: H1 :: T2 can be represented by U (that is, the HList repr of the original case class T)
      // Note, you don't need both H1 and H2, they are the same (so don't need ev), but I've left it in to show the breakdown of the U HList
      ev: (H2 :: H1 :: T2) =:= U

    ): T = {

    val u = gen.to(v)

    val h1 = u.head
    val t1 = u.tail
    val h2 = t1.head
    val t2 = t1.tail

    gen.from(h2 :: h1 :: t2)
  }