So the error message should talk about "unreachable pattern" instead of "redundant pattern". That would cover all situations and would be less confusing in this special one. Cheers Ben Am 20.07.23 um 06:53 schrieb Viktor Dukhovni:

On Wed, Jul 19, 2023 at 09:24:20PM -0700, Todd Wilson wrote:

...

Can someone please explain this:

ghci> case 1 of 2 -> 3

<interactive>:1:11: warning: [-Woverlapping-patterns] Pattern match is redundant In a case alternative: 2 -> ... *** Exception: <interactive>:1:1-16: Non-exhaustive patterns in case

The non-exhaustive patterns part is obvious, but what is redundant about this match? And how can there be overlapping patterns when there's only one?

The error message changed betweek 8.8 and 8.10:

GHCi, version 8.8.4: https://www.haskell.org/ghc/ :? for help λ> data X = A | B λ> case A of B -> 42

*** Exception: <interactive>:2:1-18: Non-exhaustive patterns in case

vs.

GHCi, version 8.10.5: https://www.haskell.org/ghc/ :? for help λ> data X = A | B λ> case A of B -> 42

<interactive>:2:11: warning: [-Woverlapping-patterns] Pattern match is redundant In a case alternative: B -> ... *** Exception: <interactive>:2:1-17: Non-exhaustive patterns in case

The exception part is the same, and I hope non-controversial, the pattern match is indeed non-exhaustive. What's new is the compile-time warning. It is documented at, e.g.:

https://ghc.gitlab.haskell.org/ghc/doc/users_guide/using-warnings.html#ghc-f...

where it is explained that a pattern is considered "overlapping" when it is unreachable, which is true in this case, though for reasons other than redundancy wrt. a prior pattern. And indeed we see the true issue/criterion is "reachability":

λ> case A of B | GHC.Exts.considerAccessible -> 42

*** Exception: <interactive>:3:1-47: Non-exhaustive patterns in case

The same is of course seen if the warning is disabled:

λ> :set -Wno-overlapping-patterns λ> case A of B -> 42

*** Exception: <interactive>:6:1-17: Non-exhaustive patterns in case

The pattern match is redundant given the specific scrutinee. Perhaps non-reachability in this case could be reported via a different warning, but we have what we have.

-- I would rather have questions that cannot be answered, than answers that cannot be questioned. -- Richard Feynman

λ: data X = A|B λ: let x = A in case x of A -> True; B -> False True λ: case A of A -> True ; B -> False <interactive>:3:23: warning: [-Woverlapping-patterns] Pattern match is redundant In a case alternative: B -> ... True Isn't this violating referential transparency (in a way)? --Todd On Fri, Jul 21, 2023 at 3:15 AM Jeff Clites via Haskell-Cafe < haskell-cafe@haskell.org> wrote:

I think it’s saying it’s redundant because you already known what constructor it is; I’m guessing you’d get the same error from “case A of A -> …”.

Jeff

...

On Jul 21, 2023, at 2:57 AM, Ben Franksen wrote:

So the error message should talk about "unreachable pattern" instead of "redundant pattern". That would cover all situations and would be less confusing in this special one.

Cheers Ben

...

...

On Wed, Jul 19, 2023 at 09:24:20PM -0700, Todd Wilson wrote: Can someone please explain this:

ghci> case 1 of 2 -> 3

<interactive>:1:11: warning: [-Woverlapping-patterns] Pattern match is redundant In a case alternative: 2 -> ... *** Exception: <interactive>:1:1-16: Non-exhaustive patterns in case

The non-exhaustive patterns part is obvious, but what is redundant about this match? And how can there be overlapping patterns when there's only one? The error message changed betweek 8.8 and 8.10: GHCi, version 8.8.4: https://www.haskell.org/ghc/ :? for help λ> data X = A | B λ> case A of B -> 42 *** Exception: <interactive>:2:1-18: Non-exhaustive patterns in case vs. GHCi, version 8.10.5: https://www.haskell.org/ghc/ :? for help λ> data X = A | B λ> case A of B -> 42 <interactive>:2:11: warning: [-Woverlapping-patterns] Pattern match is redundant In a case alternative: B -> ... *** Exception: <interactive>:2:1-17: Non-exhaustive patterns in case The exception part is the same, and I hope non-controversial, the

Am 20.07.23 um 06:53 schrieb Viktor Dukhovni: pattern match is indeed non-exhaustive. What's new is the compile-time warning. It is documented at, e.g.:

https://ghc.gitlab.haskell.org/ghc/doc/users_guide/using-warnings.html#ghc-f...

...

where it is explained that a pattern is considered "overlapping" when it is unreachable, which is true in this case, though for reasons other than redundancy wrt. a prior pattern. And indeed we see the true issue/criterion is "reachability": λ> case A of B | GHC.Exts.considerAccessible -> 42 *** Exception: <interactive>:3:1-47: Non-exhaustive patterns in case The same is of course seen if the warning is disabled: λ> :set -Wno-overlapping-patterns λ> case A of B -> 42 *** Exception: <interactive>:6:1-17: Non-exhaustive patterns in case The pattern match is redundant given the specific scrutinee. Perhaps non-reachability in this case could be reported via a different warning, but we have what we have.

-- I would rather have questions that cannot be answered, than answers that cannot be questioned. -- Richard Feynman

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

---

Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

On Jul 21, 2023, at 3:20 PM, Jeff Clites via Haskell-Cafe wrote:

Also, one other comment, about Ben Franksen's message:

...

...

So the error message should talk about "unreachable pattern" instead of "redundant pattern".

Ah but the message is actually:

...

Pattern match is redundant

So I think it's trying to say not that the one pattern is redundant, but the whole case expression is redundant. Perhaps it should say something like "unnecessary case expression" instead.

Oh no I take that back, it is talking about a specific pattern:

...

Pattern match is redundant In a case alternative: B -> ...

But I do think a better complaint is that you don't need a case expression there at all, but it seems like that's not actually what it's complaining about. Hmm. Jeff

...

On Jul 21, 2023, at 12:21 PM, Todd Wilson wrote:

λ: data X = A|B λ: let x = A in case x of A -> True; B -> False True λ: case A of A -> True ; B -> False

<interactive>:3:23: warning: [-Woverlapping-patterns] Pattern match is redundant In a case alternative: B -> ... True

Isn't this violating referential transparency (in a way)?

--Todd

On Fri, Jul 21, 2023 at 3:15 AM Jeff Clites via Haskell-Cafe wrote: I think it’s saying it’s redundant because you already known what constructor it is; I’m guessing you’d get the same error from “case A of A -> …”.

Jeff

...

On Jul 21, 2023, at 2:57 AM, Ben Franksen wrote:

So the error message should talk about "unreachable pattern" instead of "redundant pattern". That would cover all situations and would be less confusing in this special one.

Cheers Ben

...

...

On Wed, Jul 19, 2023 at 09:24:20PM -0700, Todd Wilson wrote: Can someone please explain this:

ghci> case 1 of 2 -> 3

<interactive>:1:11: warning: [-Woverlapping-patterns] Pattern match is redundant In a case alternative: 2 -> ... *** Exception: <interactive>:1:1-16: Non-exhaustive patterns in case

The non-exhaustive patterns part is obvious, but what is redundant about this match? And how can there be overlapping patterns when there's only one? The error message changed betweek 8.8 and 8.10: GHCi, version 8.8.4: https://www.haskell.org/ghc/ :? for help λ> data X = A | B λ> case A of B -> 42 *** Exception: <interactive>:2:1-18: Non-exhaustive patterns in case vs. GHCi, version 8.10.5: https://www.haskell.org/ghc/ :? for help λ> data X = A | B λ> case A of B -> 42 <interactive>:2:11: warning: [-Woverlapping-patterns] Pattern match is redundant In a case alternative: B -> ... *** Exception: <interactive>:2:1-17: Non-exhaustive patterns in case The exception part is the same, and I hope non-controversial, the

Am 20.07.23 um 06:53 schrieb Viktor Dukhovni: pattern match is indeed non-exhaustive. What's new is the compile-time warning. It is documented at, e.g.: https://ghc.gitlab.haskell.org/ghc/doc/users_guide/using-warnings.html#ghc-f... where it is explained that a pattern is considered "overlapping" when it is unreachable, which is true in this case, though for reasons other than redundancy wrt. a prior pattern. And indeed we see the true issue/criterion is "reachability": λ> case A of B | GHC.Exts.considerAccessible -> 42 *** Exception: <interactive>:3:1-47: Non-exhaustive patterns in case The same is of course seen if the warning is disabled: λ> :set -Wno-overlapping-patterns λ> case A of B -> 42 *** Exception: <interactive>:6:1-17: Non-exhaustive patterns in case The pattern match is redundant given the specific scrutinee. Perhaps non-reachability in this case could be reported via a different warning, but we have what we have.

-- I would rather have questions that cannot be answered, than answers that cannot be questioned. -- Richard Feynman

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

---

Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

On Fri, Jul 21, 2023 at 5:14 PM Todd Wilson wrote:

On Fri, Jul 21, 2023 at 3:27 PM Jeff Clites via Haskell-Cafe < haskell-cafe@haskell.org> wrote:

...

Oh no I take that back, it is talking about a specific pattern:

...

...

Pattern match is redundant In a case alternative: B -> ...

But I do think a better complaint is that you don't need a case expression there at all, but it seems like that's not actually what it's complaining about. Hmm.

My take-away from all this is that, if a case branch can be determined *statically* (i.e., without applying any evaluation steps) not to match, then it is "redundant." If there are counterexamples to this take-away, though, please let me know!

--Todd

At the risk of descending into bikeshedding, I think "redundant" applies to anything that can be safely removed, and it is widely used in the ghc error messages. Using different words like "unreachable" and "unnecessary" is distracting and doesn't confer any benefit that I can see.

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.