scala - 未能减少 Scala 中的匹配类型

Question

我正在破解 Scala 3 中的匹配类型，并希望定义这样的匹配类型，以便Either[A, B]将任何匹配类型重新关联为右侧递归，即：

Rebalance[(Int Either String) Either (Boolean Either Long)] =:= (Int Either (String Either (Boolean Either Long)))

我已经组装了以下代码（也是scastie）：

type Rebalance[A] = A match {
  case Either[Either[a, b], c] => Rebalance[Either[a, Either[b, c]]]
  case Either[a, Either[b, c]] => Either[a, Rebalance[Either[b, c]]]
  case Either[a, b]            => Either[a, b]
}

type RebalancePair[A, B] = (A, B) match {
  case (Either[a, b], c) => RebalancePair[a, Either[b, c]]
  case (a, Either[b, c]) => Either[a, RebalancePair[b, c]]
  case (a, b) => Either[a, b]
}

type RebalanceProxy[A] = A match {
  case Either[a, b] => RebalancePair[a, b]
}

type Balanced = Int Either (String Either (Boolean Either Long))

summon[RebalanceProxy[(Int Either String) Either (Boolean Either Long)] =:= Balanced] //this works
summon[Rebalance[(Int Either String) Either (Boolean Either Long)] =:= Balanced] //this doesn't

^^^ 

Cannot prove that Playground.Rebalance[Either[Int, Either[String, Either[Boolean, Long]]]] =:= Playground.Balanced.

Note: a match type could not be fully reduced:

  trying to reduce  Playground.Rebalance[Either[Int, Either[String, Either[Boolean, Long]]]]
  failed since selector  Either[Int, Either[String, Either[Boolean, Long]]]
  does not match  case Either[Either[a, b], c] => Playground.Rebalance[Either[a, Either[b, c]]]
  and cannot be shown to be disjoint from it either.
  Therefore, reduction cannot advance to the remaining cases

    case Either[a, Either[b, c]] => Either[a, Playground.Rebalance[Either[b, c]]]
    case Either[a, b] => Either[a, b]
​

我很好奇为什么它可以通过RebalanceProxy&RebalancePair匹配工作，却以明显相同的匹配类型失败Rebalance？我想直接通过它来实现它的原因Rebalance是，为 定义一个依赖类型的函数会非常简单Rebalance，但不是为RebalancePair.

标签： scalascala-3match-types