Failed to reduce match type in Scala

132 views Asked by At

I'm hacking match types in Scala 3, and would like to define such match type that any Either[A, B] would be reassociated to be right-side recursive, i.e.:

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

I've assembled the following piece of code (also 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]
​

I'm curious why it works via RebalanceProxy & RebalancePair match, and yet fails with visibly the same match type Rebalance? The reason I'd like to achieve it directly via Rebalance is that it would be quite simple to define a dependently typed function for Rebalance, but not for a RebalancePair.

0

There are 0 answers