You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
There are three kinds of unreachable cases:
1. the cases that are provably disjoint from the scrutinee type
2. the cases that are not subtypes of the scrutinee type
3. the cases that are covered by a previous cases, aka an overlap
The first one should be (I didn't review or stress test it) handled when
type-checking the pattern.
The third one is the safest, in terms of not emitting false positives to
the user, because it's within the conservative approximation of the
scrutinee space and the previous cases spaces.
The second one is where it gets tricky, because we don't know they're
part of the scrutinee type but we also don't know they're _not_ part of
the scrutinee type. Erasure is the simplest example: if the scrutinee
type is `type ThisTree <: Tree` then if you write cases for subtypes of
Tree that aren't subtypes of ThisTree, then they're not subtypes nor are
they provably disjoint from the scrutinee type.
Martin mentioned that it's been tried a few times to restrict patterns
to subtypes, but that it's been found too restrictive and provably
disjoint is the right choice for type errors.
So the logic that I recently reimplemented was to only emit reachability
warnings after a reachable a case was found, therefore avoiding to emit
any warnings in the ThisTree case, emitting for all the overlap
unreachable cases.
The problem was that accidentally introduced a dependency on the
ordering of the cases, where unreachable initial cases aren't warned but
reordered they would. So I hold onto those references and unbuffer as
soon as we find a provably reachable case (covered != Empty) or a
provably unreachable case (prev != Empty).
Also, I've had separate conversations with Seth and Lukas about whether
match analysis should just widen those non-class types, but it's also
plausible that a user has created a whole type hierarchy with type
members and would prefer for it to not discard it all by widening to
class/object types, but instead reason within the bounds of the given
scrutinee type.
0 commit comments