I think the completeness checker works fine in all pattern-synonym-free cases, i.e. when you're using only real constructors.
One can envision a simple recursive divide-and-conquer algorithm, see below.
I don't actually understand why completeness
annotations are needed for pattern synonyms.
I remember reading somewhere, but I can't find it now, that GHC's coverage checker does not look inside pattern synonym definitions at all, and this is by design: namely to ensure abstraction boundaries. Looking inside the definition would mean that type checking behaviour (in a way -- if you count coverage checks as "type checking") of user code is influenced by invisible implementation details of the "constructors" they're using.
Compare that to 'type' versus 'newtype' on the type level: A type is just an alias, a synonym. The type checker has access to all information on the right hand side of the equality. With extensions like TypeSynonymInstances, A type alias is interchangeable with the aliased type. If what you report is true, they should not have called pattern synonyms a "synonym".
My own thoughts on this: if GHC would look inside pattern synonym definitions, then it would be hard to ensure that GHC thinks that certain things are _not_ complete even if technically they are. For example, if you have a data type with, say, 3 constructors, but you hide some of those (don't export them) and use pattern synonyms to make it look like 4 constructors, then you might want GHC's coverage checker to consider that a data type with 4 constructors, not one with 3. COMPLETE pragmas add "positive" information -- "this set is complete, in addition to whatever other complete sets GHC might already know" -- and there is no way to _subtract_ complete sets from GHC's knowledge base.
This is mostly me theorising, but perhaps it helps.
- other Tom
I don't think the number of constructors/patterns is the issue. Likely the problem lies in the fact that while ordinary constructors make up disjoint subsets of the type, with patterns you can define overlapping sets, which makes completeness checks much more complicated. Hence I believe that completeness checks in presence of patterns is equivalent to determine whether a disjunction of logic formulae, which are possibly self-referential, is a tautology. That may well be semi- decidable at best. Olaf