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

[Olaf Klinke]

>  > 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