#10746: No non-exhaustive pattern match warning given for empty case analysis -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: duplicate | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: #7669 | Differential Revisions: -------------------------------------+------------------------------------- Changes (by thomie): * status: new => closed * resolution: => duplicate * related: => #7669 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10746#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10746: No non-exhaustive pattern match warning given for empty case analysis -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: duplicate | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: #7669 | Differential Revisions: -------------------------------------+------------------------------------- Changes (by bgamari): * status: new => closed * resolution: => duplicate Comment: Ahh, in the interest of aiding the bug sweep (see ticket:7669#comment:8) I'll leave this as a duplicate. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10746#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: #7669 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by rwbarton): * status: closed => new * resolution: duplicate => Comment: This was closed through a chain of duplicates leading to #595, but the new pattern exhaustiveness checker in 8.0 still exhibits the issue described in this ticket. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10746#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | -------------------------------------+------------------------------------- Changes (by dfeuer): * related: #7669 => #7669, #11806 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10746#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 dfeuer): I don't actually understand most of this code, but it *looks* like the problem is probably in the `checkMatches'` function in `compiler/deSugar/Check.hs`. Specifically, there's a guard {{{#!hs | null matches = return ([], [], []) }}} that looks fishy. I don't have things set up properly to build GHC at the moment, but my guess is that simply removing this clause and going straight to the `otherwise` will fix the bug. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10746#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 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: _ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10746#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 simonpj): The discussion in #11806 is worth reading -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10746#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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

#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 dfeuer): To summarize, empty case is desugared specially. It therefore needs a special case for coverage checking, but ''not'' the trivial one we currently have. I suspect the right thing is probably to avoid including `_|_` in `mkInitialUncovered` when checking an empty `case`, whatever that involves. You may need to do something else if you want to catch an overlapping trivial pattern in since cases, but even if you miss that it's no big deal. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10746#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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): Replying to [comment:16 dfeuer]:

{{{#!hs Prelude> :set -XEmptyCase -XEmptyDataDecls Prelude> data Void Prelude> let absurd :: Void -> a; absurd x = case x of Prelude> absurd (error "Really?") *** Exception: Really? }}}

Wow! I was indeed not familiar with this unintuitive design choice, you are right. Replying to [comment:17 dfeuer]:

To summarize, empty case is desugared specially. It therefore needs a special case for coverage checking, but ''not'' the trivial one we currently have. I suspect the right thing is probably to avoid including `_|_` in `mkInitialUncovered` when checking an empty `case`, whatever that involves. You may need to do something else if you want to catch an overlapping trivial pattern in since cases, but even if you miss that it's no big deal.

Overlap checking is not affected by this I think. Since this eager evaluation happens only in the `EmptyCase` case, there are no patterns to be considered redundant. Nevertheless, the case needs special treatment. The best fix I can think about this is a function {{{#!hs areInhabited :: [Id] -> TcM [ValVec] }}} which unfolds everything to WHNF if possible (recursively, I guess, if there are strict fields) and checks for satisfiability (approximately, of course, since this may not terminate). Then, `checkMatches'` could be adjusted: {{{#!hs checkMatches' :: [Id] -> [LMatch Id (LHsExpr Id)] -> DsM PmResult checkMatches' vars matches | null matches = areInhabited vars >>= \us -> return ([],us,[]) | otherwise = ... }}} Does this sound reasonable? I'd like to think this through first, but I could write such a fix. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10746#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 dfeuer): Oh, I see what you mean about recursively checking strict fields to some limit. That would be very nice, yes, but it's not urgent because there's a good way to work around it: {{{#!hs data SId a = SId !a --With recursive checking foo :: SId Void -> a foo bad = case bad of --Without recursive checking foo (SId bad) = absurd bad }}} What I don't understand is what you mean about unfolding something to WHNF. If the goal is to try to determine the actual WHNF of the scrutinee, that sounds like overkill to me, unless you're doing that in other cases already. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10746#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 dfeuer): Excellent! I think one layer only is probably a good goal for right this minute. More extensive checking would likely involve more research and design decisions. Thanks a lot for working on this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10746#comment:23 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10746: No non-exhaustive pattern match warning given for empty case analysis -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: patch 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): Phab:D2105 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): This all seems a bit more complicated than it need be. My guiding light is that it should all be very similar to `case x of { C y -> blah }`. For this we enumerate all the data constructors other than `C y` as non- matching (modulo inaccessible GADT constructors). We can do the same here. The only real difference is that we don't have a data constructor `C` to start from. Instead we start from the type of `x :: tyx`. So it looks simple: * Normalise `x`'s type, to get it to the form `T ty1 .. tyn`. (I don't understand the "bounded" bit.) For this, we must reduce type families, but NOT newtypes. For pattern matching purposes, newtypes behave just like data types. So use `FamInstEnv.normaliseType`. * If `T` has no data constructors, we are done. For example, empty data types, which don't produce an error message here. * If none of `T`'s data constructors are GADTs, then just produce an error of form {{{ Blah.hs:4:1: warning: [-Wincomplete-patterns] Pattern match(es) are non-exhaustive In a case alternative: Patterns not matched: _ :: Bool }}} Here I've added the "`:: Bool`" part so the reader understands the type of the pattern. No need to enumerate `True` and `False`. * If some of `T`'s data constructor are GADTs, then enumerate them all and recurse. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10746#comment:25 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10746: No non-exhaustive pattern match warning given for empty case analysis -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: patch 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): Phab:D2105 Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): I don't know about the other stuff, but I think I disagree on the bounded bit. In that situation, I would expect the compiler to go into an infinite loop (unless it has pity on us in that particular case and happens to detect the loop, which is not the pattern checker's problem in any case). If I tell the type checker to go into an infinite loop and heat up my computer, it's really okay if it does that. Again, I can always write {{{#!hs foo :: F Int -> a foo !_ = error "Unreachable, but that's not provable within Haskell." }}} if I want to impose an ad hoc postulate about program behavior. Empty case is for what GHC *can* prove. The case of terminally stuck closed type families (ones that no additional information could possibly reduce) is a bit weird; I think for now at least you should probably treat them the same as stuck open type families and assume them inhabited. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10746#comment:27 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10746: No non-exhaustive pattern match warning given for empty case analysis -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: closed Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 7.10.2 Resolution: fixed | 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): Phab:D2105 Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: patch => closed * resolution: => fixed * milestone: => 8.2.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10746#comment:29 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler