I think the completeness checker works fine in all pattern-synonym-free cases, i.e. when you're using only real constructors.  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. 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