#15450: Inconsistency w.r.t. coverage checking warnings for EmptyCase under unsatisfiable constraints -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: #12957 | Differential Rev(s): Phab:D5017 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): (Commenting here because my reflections concern the specification, not the coding.) The patch says {{{ We decide to better than this. When beginning coverage checking, we first check if the constraints in scope are unsatisfiable, and if so, we start afresh with an empty set of constraints. This way, we'll get the warnings we expect. }}} That seems quite odd behaviour! The door closes gradually, but when it becomes shut we slam it open again?? What about simpler cases {{{ data T a where T1 :: T Int T2 :: T a f :: T Bool -> Int f T1 = ....(case x of { True -> False })... f T2 = ... }}} The entire RHS of the first equation is unreachable. Should we not just stop reporting errors from that branch altogether? If the door wasn't shut (say we had learned something about `x`, but nothing contradictory) then the inner case might be fine. The more we learn about `x` the fewer alternatives we may need in that inner case. When the door shuts altogether we need no branches in the inner case, so perhaps reporting a redundant match is correct. Or perhaps we just want to shut up once we find a contradiction, and let the user fix that first. But discarding all the constraints seems ... unexpected. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15450#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

(Commenting here because my reflections concern the specification, not

#15450: Inconsistency w.r.t. coverage checking warnings for EmptyCase under unsatisfiable constraints -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: #12957 | Differential Rev(s): Phab:D5017 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: mpickering (added) Comment: Replying to [comment:2 simonpj]: the coding.)

The patch says {{{ We decide to better than this. When beginning coverage checking, we

first

check if the constraints in scope are unsatisfiable, and if so, we start afresh with an empty set of constraints. This way, we'll get the warnings we expect. }}} That seems quite odd behaviour! The door closes gradually, but when it becomes shut we slam it open again??

Another thing. I see in `Note [Checking EmptyCase Expressions]` (in `Check.hs`) this: {{{ Empty case expressions are strict on the scrutinee. That is, `case x of {}` will force argument `x`. Hence, `checkMatches` is not sufficient for checking empty cases, because it assumes that the match is not strict (which is

This is all explained in the commentary in https://phabricator.haskell.org/D3064 (which I've attempted to turn into Note form in this patch). Also cc'ing mpickering, who established this convention. Replying to [comment:3 simonpj]: true

for all other cases, apart from EmptyCase). This gave rise to #10746. }}} I had no idea! The [http://downloads.haskell.org/~ghc/master/users- guide/glasgow_exts.html#empty-case-alternatives user manual entry] says nothing about this non-uniform behaviour of empty case expressions.

What actually stops us from treating an empty case as an ordinary case expression with no alternatives? Anything else seems.. unexpected.

I'm not sure I understand this question. Did you read #10746? That seems to lay out pretty clearly why `EmptyCase` needs to be treated specially (because it's strict, unlike other `case` expressions).

The explanation in the user manual is cryptic (see the text about `absurd`. And it relates directly to this ticket, because it has `True ~ False` in scope, which is a contradiction. So maybe fixing comment:2 would mean we could treat case expressions uniformly, which would mean we could delete code?

Maybe. But I have no interest in doing this here. I only opened this ticket because the lack of sharing between code paths in `checkEmptyCase` and `checkSingle` made it difficult to implement #15305, so I did the exact minimum amount of work to fix the discrepancy. Anything more than this deserves to be in a separate feature request, in my opinion. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15450#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15450: Inconsistency w.r.t. coverage checking warnings for EmptyCase under unsatisfiable constraints -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: #12957 | Differential Rev(s): Phab:D5017 Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Be careful. You're conflating two separate issues: 1. Should we emit coverage warnings in unreachable alternatives? 2. Should `EmptyCase`'s code path (`checkEmptyCase'`) behave differently than other `case` expressions' code path (`checkMatches'`)? I don't feel strongly about (1), and I think we could just as well answer that question with "yes" or "no". Matthew, can you comment here? You're the one who introduced this convention. The answer to (2) is an emphatic "yes". If you try to delete `checkEmptyCase'`, then //all// `EmptyCase` expressions will be reported as non-exhaustive (this isn't just speculation on my part; I actually tried this). And this is not surprising. Regular `case` expressions are lazy, whereas `EmptyCase` expressions are strict. Hypothetically speaking, if `EmptyCase` were lazy, then in the following code: {{{#!hs data Void absurd :: Void -> a absurd x = case x of {} main :: IO () main = putStrLn (absurd undefined) }}} `main` would produce a non-exhaustive pattern-match error at runtime instead of an `undefined` exception! This alone shows that `EmptyCase` needs some degree of special-casing. While an interesting discussion, (2) doesn't pertain much to this ticket, so I'd encourage you not to bog down the discussion with mention of it. (Feel free to open a separate ticket if it's bothering you that much.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15450#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15450: Inconsistency w.r.t. coverage checking warnings for EmptyCase under unsatisfiable constraints -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: fixed | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: #12957 | Differential Rev(s): Phab:D5017 Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: patch => closed * resolution: => fixed Comment: Merged to `ghc-8.6` with ebd773a09be134157880eaa1099f4b5d30a67aac. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15450#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler