#10746: No non-exhaustive pattern match warning given for empty case analysis -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: #7669, #11806 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by gkaracha): I guess my wording was not clear in #11806 after all, I will try to elaborate here in more detail. :-) == Current state == Indeed the guard in `checkMatches'` is responsible for the current behaviour on empty case expressions: {{{ | null matches = return ([], [], []) }}} By default, the new checker would issue a non-exhaustive warning for empty cases, which is correct. Yet, there has been a request (#7669) to **not** issue a warning in these cases. Hence, Simon changed this with commit 9162d159a62d19d4b371b7348eb1b524001fddcd. I have added the above guard in the new implementation to keep the same behaviour (even though I strongly disagree with it) and by removing it we get the default behaviour, which #11806 & #10746 request. == Laziness == Replying to [comment:12 dfeuer]:
Replying to [comment:11 erikd]:
Hmm, wit this fix, building base fails due to:
{{{ absurd :: Void -> a absurd a = case a of {} }}}
which triggers:
{{{ libraries/base/Data/Void.hs:66:12: warning: [-Wincomplete-patterns] Pattern match(es) are non-exhaustive In a case alternative: Patterns not matched: _ }}}
Argh! That seems surprising. I'd have expected `mkInitialUncovered` to have produced an empty list there.
This is the right behaviour! The call `(absurd undefined) :: Int` will crash, not because of evaluating `undefined` but because the match is non- exhaustive, try it out and see! About `mkInitialUncovered`, it should **not** produce an empty list: If you check our paper (https://people.cs.kuleuven.be/~george.karachalias/papers/p424-karachalias.pd..., paragraph Initialisation, Section 4.2), you will see that U_0 is not empty, independently of the argument types. Replying to [comment:14 dfeuer]:
If I understand it correctly, empty case *always* forces its scrutinee, and thus should be considered complete if that is guaranteed to diverge. I don't really understand gkaracha's argument to the contrary, but he knows much more about this than I do, so I could be missing some key point.
This is probably the key point that is not clear. The part `case x of` does not force `x`, the patterns that appear after do that. This means that, for example, `case x of { y -> ... }` does not force x. == Type Inhabitation == All the related tickets give me the impression that it is expected for `f` to be non-exhaustive and `g` to be exhaustive, which is not in accordance with Haskell's operational semantics. {{{#!hs f :: Int -> a f x = case x of {} g :: Void -> a g x = case x of {} }}} Unless you force `x` in another way, both `case x of {}` are equally non- exhaustive. In OCaml for example this is different, and this is precisely why the OCaml community identifies the pattern match checking as a type inhabitation problem http://www.math.nagoya-u.ac.jp/~garrigue/papers/gadtspm.pdf, in contrast to what we do. Nevertheless, there are ways in Haskell to force arguments explicitly (e.g. via `seq`) which means that it becomes an inhabitation problem for us as well (like for `g'` below) in some cases. {{{#!hs g' :: Void -> a g' x = x `seq` case x of {} }}} Indeed, this kind of reasoning we lack at the moment. I can imagine that if the strictness analysis phase came before our checking we would be able to use this information and improve our reasoning for cases like `g'`, by checking type inhabitation, where possible. == Conclusion == Personally, I am really happy that the guard from `checkMatches'` is finally removed, and I surely vote for non-exhaustive warnings in empty case expressions, including function `absurd` above which **is** non- exhaustive. I'd be happy to see how we can make `g'` issue no warnings, but this, I think, is a quite different problem. Sorry for the long post, I just hope things are more clear now :-) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10746#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler