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
.