#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 Resolution: | Keywords: | PatternSynonyms, | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by dfeuer: @@ -8,1 +8,1 @@ - pattern FZ :: () => forall m. n ~ 'S m => Fin n + pattern FZ :: () => n ~ 'S m => Fin n New description: 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 :: () => 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#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler