#15450 closed bug (fixed)

Inconsistency w.r.t. coverage checking warnings for EmptyCase under unsatisfiable constraints

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler Version: 8.4.3
Keywords: PatternMatchWarnings Cc: mpickering
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Poor/confusing error message Test Case:
Blocked By: Blocking:
Related Tickets: #12957 Differential Rev(s): Phab:D5017
Wiki Page:

Description

Consider the following code:

{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE GADTs #-}
{-# OPTIONS_GHC -Wincomplete-patterns #-}
module Bug where

f :: (Int ~ Bool) => Bool -> a
f x = case x of {}

g :: (Int ~ Bool) => Bool -> a
g x = case x of True -> undefined
$ /opt/ghc/8.4.3/bin/ghci Bug.hs
GHCi, version 8.4.3: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:10:7: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In a case alternative: Patterns not matched: False
   |
10 | g x = case x of True -> undefined
   |       ^^^^^^^^^^^^^^^^^^^^^^^^^^^

Observe that we get a non-exhaustivity warning for the case expression in g (thanks to commit adb565aa74582969bbcc3b411d6d518b1c76c3cf), but not for the one in f. The difference is that f uses EmptyCase, whereas g does not, and the codepath for EmptyCase is unfortunately incongruous with the codepath for other coverage checking.

I know how to fix this. Patch incoming.

Change History (8)

comment:1 Changed 14 months ago by RyanGlScott

Differential Rev(s): Phab:D5017
Status: newpatch

comment:2 Changed 14 months ago 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.

comment:3 Changed 14 months ago by simonpj

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 true
for all other cases, apart from EmptyCase). This gave rise to #10746.

I had no idea! The 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.

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?

comment:4 in reply to:  3 Changed 14 months ago by RyanGlScott

Cc: mpickering added

Replying to 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??

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 simonpj:

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 true
for all other cases, apart from EmptyCase). This gave rise to #10746.

I had no idea! The 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.

comment:5 Changed 14 months ago by simonpj

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).

Thank you for turning it into a Note.

Yes, I am questioning the principle. It seems bizarrely discontinuous to fling the door wide open when (but only when) it completely closes. Indeed I see that on Phab:D3064 George did suggest "The patch as is just drops information, we can instead issue no warnings if we are already in a dead-code branch."

Do you agree that if we did this, we could simply delete checkEmptyCase entirely, rendering the current patch moot?

Last edited 14 months ago by simonpj (previous) (diff)

comment:6 Changed 14 months ago 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:

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.)

comment:7 Changed 14 months ago by Ben Gamari <ben@…>

In 7f3cb50d/ghc:

Fix #15450 by refactoring checkEmptyCase'

`checkEmptyCase'` (the code path for coverage-checking
`EmptyCase` expressions) had a fair bit of code duplication from the
code path for coverage-checking non-`EmptyCase` expressions, and to
make things worse, it behaved subtly different in some respects (for
instance, emitting different warnings under unsatisfiable
constraints, as shown in #15450). This patch attempts to clean up
both this discrepancy and the code duplication by doing the
following:

* Factor out a `pmInitialTmTyCs` function, which returns the initial
  set of term and type constraints to use when beginning coverage
  checking. If either set of constraints is unsatisfiable, we use an
  empty set in its place so that we can continue to emit as many
  warnings as possible. (The code path for non-`EmptyCase`
  expressions was doing this already, but not the code path for
  `EmptyCase` expressions, which is the root cause of #15450.)

  Along the way, I added a `Note` to explain why we do this.
* Factor out a `pmIsSatisfiable` constraint which checks if a set of
  term and type constraints are satisfiable. This does not change any
  existing behavior; this is just for the sake of deduplicating code.

Test Plan: make test TEST=T15450

Reviewers: simonpj, bgamari

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #15450

Differential Revision: https://phabricator.haskell.org/D5017

comment:8 Changed 14 months ago by bgamari

Resolution: fixed
Status: patchclosed
Note: See TracTickets for help on using tickets.