证明匹配类型解析为特定的具体类型

我正在尝试创建一个使用匹配类型的特征的实现，其中该匹配类型的右侧是预先已知的。但是，我似乎无法让编译器接受我的“证明”。这对我来说很新，如果这真的很明显，我很抱歉。有人可以帮助我了解我是否/如何能够实现我想要的吗？

这是一些最小的代码（Scastie）来说明我在做什么：

class NumberBox {}

class LongBox {}

trait Boxer[T] {
  def box(): Boxer.Box[T]
}

object Boxer {
  type Box[T] = T match
    case Long => LongBox
    case _ => NumberBox
}

case class Val[T](v: T) extends Boxer[T] {
  def box(): Boxer.Box[T] = v match
    case _: Long => new LongBox()
    case _ => new NumberBox()
}

// here we prove that Boxer.Box[T] is a NumberBox
case class NoLongs[T](v: Boxer[T])(using Boxer.Box[T] =:= NumberBox) extends Boxer[T] {
  override def box(): Boxer.Box[T] = new NumberBox()
}

NoLongs(Val(1))

但这失败了：

Found:    NumberBox
Required: Boxer.Box[T]

Note: a match type could not be fully reduced:

  trying to reduce  Boxer.Box[T]
  failed since selector  T
  does not match  case Long => LongBox
  and cannot be shown to be disjoint from it either.
  Therefore, reduction cannot advance to the remaining case

    case _ => NumberBox
    override def box(): Boxer.Box[T] = new NumberBox()

Scala 不会自动按照您寻找的方式应用证明。但你是对的，你确实有证据。事实上，你的证明构成了一个可调用对象：类型=:=[From, To]定义了一个方法叫做apply:

override def apply(f: From): To

现在，你有一个 type 的值Boxer.Box[T] =:= NumberBox， 意思就是apply会转换一个Boxer.Box[T] to a NumberBox。你想要相反的结果：转换 aNumberBox into a Boxer.Box[T]。所以我们需要flip你的证明然后apply it.

def flip: To =:= From

在您的具体用例中，请考虑

case class NoLongs[T](v: Boxer[T])(using eq: Boxer.Box[T] =:= NumberBox) extends Boxer[T] {
  override def box(): Boxer.Box[T] = eq.flip(new NumberBox())
}

我们给证明论证一个名字，eq，然后我们应用它的对称证明（即NumberBox =:= Boxer.Box[T]）到我们的NumberBox将其转换为所需的类型。

你也可以只证明NumberBox =:= Boxer.Box[T]直接并摆脱flip，如果需要的话。

case class NoLongs[T](v: Boxer[T])(using eq: NumberBox =:= Boxer.Box[T]) extends Boxer[T] {
  override def box(): Boxer.Box[T] = eq(new NumberBox())
}