#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:21 dfeuer]:
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.
Ah, no, I think we mean the same thing. Maybe my wording was not clear. :-) For example, for `Fin`, we need to unfold the `x` to `FZ` and `FS y` to check whether the match is exhaustive or not. {{{#!hs data Fin n where FZ :: Fin (Succ n) FS :: Fin n -> Fin (Succ n) f :: Fin Zero -> a f x = case x of {} }}} For what is worth, I have a small patch that does exactly this, expanding patterns of type `T tys` (only type constructor applications) to all possible patterns (one layer unfolding only) and behaves as expected for `Void`, `Fin` and other GADTs I have tried it on. I'll put it on Phab later today :-) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10746#comment:22> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler