-
Notifications
You must be signed in to change notification settings - Fork 1.1k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Combine cases of Tuple.Zip
disjoint from (h1 *: t1, h2 *: t2)
#21287
Conversation
Well actually it looks like the doc was just incorrect: scala3/library/src/scala/Tuple.scala Lines 177 to 186 in 7a0230d
-- [E007] Type Mismatch Error: tests/playground/example.scala:10:59 ------------
10 | val z: Tuple.Zip[Int *: Int *: Tuple, String *: Tuple] = (1, "a") *: (??? : Tuple)
| ^^^^^^^^^^^^^^^
|Found: (Int, String) *: Tuple
|Required: (Int, String) *: Tuple.Zip[Int *: Tuple, Tuple]
|
|Note: a match type could not be fully reduced:
|
| trying to reduce Tuple.Zip[Int *: Tuple, Tuple]
| failed since selector (Int *: Tuple, Tuple)
| does not match case (h1 *: t1, h2 *: t2) => (h1, h2) *: Tuple.Zip[t1, t2]
| and cannot be shown to be disjoint from it either.
| Therefore, reduction cannot advance to the remaining cases
|
| case (EmptyTuple, _) => EmptyTuple
| case Any => Tuple even though the doc would suggest the match type reduces to |
Tuple.Zip
unreachable match type caseTuple.Zip
disjoint from (h1 *: t1, h2 *: t2)
47a3cbf
to
f8e584d
Compare
f8e584d
to
85420c3
Compare
If we reach the second case of `Zip[T1 <: Tuple, T2 <: Tuple]`, then we know `(T1, T2)` is disjoint from `(NonEmptyTuple, NonEmptyTuple)`, from which we can conclude at least one of the two is an `EmptyTuple`. Addressing scala#19175
85420c3
to
995d63b
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Do we have enough tests of the various ways Zip
can reduce? In particular if there's (S <: Tuple) / EmptyTuple
or EmptyTuple / (S <: Tuple)
at the end of the chain?
I've added a test will all possible combinations I could think of. |
If we reach the second case of
Zip[T1 <: Tuple, T2 <: Tuple]
, then we know(T1, T2)
is disjoint from(NonEmptyTuple, NonEmptyTuple)
, from which we can conclude at least one of the two is anEmptyTuple
.Addressing #19175