
On Fri, Jul 21, 2023 at 10:17:33PM +0200, Andreas Källberg wrote:
I think unreachable would be instead of “overlapping”, rather than instead of “redundant”, since those refer to different things. Redundant patterns are when the constructor is already known, while overlapping is when the case unreachable.
It is a bit more general than "constructor known", since GHC is also able to rule out reachability even when the constructor is not fully known: λ> f x = case (x, x) of { (True, True) -> 0; (False, False) -> 1; (_, _) -> 2 } <interactive>:5:64: warning: [GHC-53633] [-Woverlapping-patterns] Pattern match is redundant In a case alternative: (_, _) -> ... Whatever `x` is, the first two patterns are sufficient, though it could be either. Regardless of how it is that the compiler figures out that no value of the scrutinee can reach a pattern, once that is known, the pattern is unreachable, and so redundant in context. That context is the "shape" of the scrutinee plus any earlier patterns. The fact that static knowledge of the scrutinee is also taken into account can make the error message slightly surprising if one is just focusing on the list of patterns. But 'redundant' is still morally true. -- Viktor.