scala - Nat的总和的编译时检查？

我试图编写一个类型类SumEq5，以便其HList类型参数的前两个字段加起来等于5:

trait SumEq5[A]
object SumEq5 {
  def apply[L <: HList](implicit ev: SumEq5[L]): SumEq5[L] = ev

  implicit def sumEq5Ev[L <: HList, A <: Nat, B <: Nat](
    implicit hcons: IsHCons.Aux[L, A, B :: HNil],
             ev: Sum.Aux[A, B, _5]
  ): SumEq5[L] = new SumEq5[L] {}
}

但这似乎不起作用:

import shapeless._
import shapeless.nat._
import net.SumEq5

scala> SumEq5[_0 :: _5 :: HNil]
<console>:19: error: could not find implicit value for
    parameter ev: net.SumEq5[shapeless.::[shapeless.nat._0,shapeless.::
       [shapeless.nat._5,shapeless.HNil]]]
       SumEq5[_0 :: _5 :: HNil]

请给我一个提示，为什么_0 :: _5 :: HNil没有证据表明它的两个Nat等于5。

编辑

根据Denis Rosca在shapeless's gitter中的帮助更新了问题。

最佳答案

如果要泛化为任意长度的HList，Dale Wijnand和Marcus Henry都朝着正确的方向发展，但是，如果您确实只想容纳两个元素HList，那么以下是一个相当简单的解决方案，

scala> import shapeless._, nat._, ops.nat._
import shapeless._
import nat._
import ops.nat._

scala> :paste
// Entering paste mode (ctrl-D to finish)

trait SumEq5[A]

object SumEq5 {
  def apply[L <: HList](implicit ev: SumEq5[L]): SumEq5[L] = ev

  implicit def sumEq5AB[A <: Nat, B <: Nat]
    (implicit ev: Sum.Aux[A, B, _5]): SumEq5[A :: B :: HNil] =
      new SumEq5[A :: B :: HNil] {}
}

// Exiting paste mode, now interpreting.

defined trait SumEq5
defined object SumEq5

scala> SumEq5[_0 :: _5 :: HNil]
res0: SumEq5[_0 :: _5 :: HNil]] = SumEq5$$anon$1@658c5e59

此处的主要区别在于，实例是为两个元素列表明确定义的，而不是通常为列表定义的，条件是存在证明该列表恰好具有两个元素的证据。

在Dale更新之后，我们可以将其概括为容纳至少两个(而不是两个)元素的HList，同样无需任何其他见证人，

scala> import shapeless._, nat._, ops.nat._
import shapeless._
import nat._
import ops.nat._

scala> :paste
// Entering paste mode (ctrl-D to finish)

trait SumEq5[A]

object SumEq5 {
  def apply[L <: HList](implicit ev: SumEq5[L]): SumEq5[L] = ev

  implicit def sumEq5AB[A <: Nat, B <: Nat, T <: HList]
    (implicit ev: Sum.Aux[A, B, _5]): SumEq5[A :: B :: T] =
      new SumEq5[A :: B :: T] {}
}

// Exiting paste mode, now interpreting.

defined trait SumEq5
defined object SumEq5

scala> SumEq5[_0 :: _5 :: HNil]
res0: SumEq5[_0 :: _5 :: HNil]] = SumEq5$$anon$1@658c5e59