[GHC] #10746: No non-exhaustive pattern match warning given for empty case analysis

[GHC]

#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.pdf,
 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