#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 mpickering): Replying to [comment:44 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.
I agree with this.
- 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
Yes. 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. There are two problems with this I think. 1. If we allow `COMPLETE` pragmas in modules other than the definition module then we would have to include the RHS of a pattern synonym in the interface file. 2. In most instances, the checker will fail and produce a warning, and then what? The warning wouldn't be actionable in some way without another syntactic clue to tell the compiler to *really* trust us. It seems like a lot of effort.
- 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?
With my latest changes, all else being equal we choose the error from the builtin set rather than any user specified set so the warnings will remain the same.
b. How can I have GHC notice that `f3` is a complete match? Saying
`{-# COMPLETE PInt #-}` would seem disastrous.
The correct thing to specify would be `{-# COMPLETE GBool, PInt #-}` and in that case, my implementation does not warn about `f3`.
- 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,
This is a fair point. It would seem that the `A,B` pragma is redundant because `A` is a subset of `A, B` but it is possible for overlapping pragmas to make sense. For example, we could have two pattern synonyms for `Just`, `PJ1`, `PJ2` and then specify `{-# COMPLETE Nothing, PJ1 #-}` and `{-# COMPLETE Nothing, PJ2 #-}`. polymorphic patterns, and possibly even higher-rank patterns.
It means that we look at the result type of each conlike and then verify that the type constructor for each type is the same. In the case of a set containing polymorphic patterns, at least one pattern in the set must have a definite type or you must specify a type signature to fix the type for the whole set.
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:46 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler