#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: mpickering Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2669 Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Somehow I've not looked at this thread, finding this only by a mention of `COMPLETE` elsewhere. (This is my fault -- just explaining my silence on this topic which is in my area of interest.) A few nitpicks about the specification: - The wiki page uses "total" in several places, but I think you mean "covering". I use "total" to refer to functions that are both covering and terminating. - Would the following be acceptable? {{{ data Void data T = T1 Int | T2 Bool | T3 Void {-# COMPLETE T1, T2 #-} }}} It would seem so. I'm happy for this to be accepted; I'm just stress- testing the spec. - The argument for not having the pattern-match checker look through pattern synonyms is reasonable. But is there a way to have GHC do some checking on `COMPLETE` declarations? It would be great -- especially if the `COMPLETE` pragma were in the synonyms' defining module -- to check these declarations. Of course, GHC will issue false negatives (that is, say that a set is not complete when it actually is) but some checking is better than none. - How does this interact with GADTs? For example, load this code into your head: {{{ data G a where GInt :: G Int GBool :: G Bool pattern PInt :: forall a. () => a ~ Int => G a pattern PInt = GInt f1 :: G a -> () f1 GInt = () f2 :: G Int -> () f2 GInt = () f3 :: G Int -> () f3 PInt = () }}} By default, `f1` and `f3` will get incomplete match warnings, and `f2` does not. a. If I say `{-# COMPLETE GInt, GBool #-}`, does this change the default warning behavior? b. How can I have GHC notice that `f3` is a complete match? Saying `{-# COMPLETE PInt #-}` would seem disastrous. - What if multiple conflicting `COMPLETE` pragmas are in scope? For example, I have `{-# COMPLETE A, B #-}` and `{-# COMPLETE A #-}` in scope. Is a match over `A` complete? Is a warning/error issued about the pragmas? - The spec says "We verify that the result types of each constructor in a complete match agrees with each other." What does this sentence mean? Consider the possibility of pattern synonyms that match against functions, polymorphic patterns, and possibly even higher-rank patterns. I've not looked at all at the implementation, wanting to nail down the spec before considering any implementation. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:44 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler