#13717: Pattern synonym exhaustiveness checks don't play well with EmptyCase -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler | Version: 8.2.1-rc1 Keywords: | Operating System: Unknown/Multiple PatternSynonyms, | PatternMatchWarnings | Architecture: | Type of failure: Incorrect Unknown/Multiple | error/warning at compile-time Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- In #8779, mpickering added a `COMPLETE` pragma to allow exhaustiveness checking for matches involving pattern synonyms. Unfortunately, there is still one piece missing: the interaction with `EmptyCase`. Suppose I write {{{#!hs newtype Fin (n :: Nat) = Fin Natural -- constructor not exported pattern FZ :: () => forall m. n ~ 'S m => Fin n pattern FS :: () => n ~ 'S m => Fin m -> Fin n {-# COMPLETE FZ, FS #-} }}} I would very much like to be able to write {{{#!hs finZAbsurd :: Fin 'Z -> Void finZAbsurd x = case x of }}} but this gives me a pattern coverage warning! That's certainly not what we want. I believe what we actually want is this: When checking empty case, check that ''at least one'' complete pattern set is impossible. In this case, it would see two complete pattern sets: the built-in `{Fin}` and the user-decreed `{FZ, FS}`. Since neither `FZ` nor `FS` have matching types, we should conclude that the empty case is fine. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13717 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler