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,
#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]: 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