(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