[Haskell-cafe] Wincomplete-uni-patterns and bidirectional patterns

[Tom Smeding]

 > 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