Suppressing False Incomplete Pattern Matching Warnings for Polymorphic Pattern Synonyms

[Matthew Pickering]

I think that `LL` is precisely intended for abstraction. If this
`COMPLETE` pragma were possible to implement then a user shouldn't
know the difference between the old and new representations.

The reason that `COMPLETE` pragmas are designed like this is that it's
how the pattern match checker is defined. The collection of patterns
used for the checking are queried by the type of the patterns so it
made sense to associate
each `COMPLETE` set with a specific type.
On Thu, Oct 25, 2018 at 2:31 PM Ryan Scott <ryan.gl.scott at gmail.com> wrote:
>
> The fact that `LL` can't be used in a COMPLETE pragma is a consequence
> of its current design. Per the users' guide [1]:
>
>     To make things more formal, when the pattern-match checker
> requests a set of constructors for some data type constructor T, the
> checker returns:
>
>     * The original set of data constructors for T
>     * Any COMPLETE sets of type T
>
> Note the use of the phrase *type constructor*. The return type of all
> constructor-like things in a COMPLETE set must all be headed by the
> same type constructor T. Since `LL`'s return type is simply a type
> variable `a`, this simply doesn't work with the design of COMPLETE
> sets.
>
> But to be perfectly honest, I feel that trying to put `LL` into a
> COMPLETE set is like putting a square peg into a round hole. The
> original motivation for COMPLETE sets, as given in this wiki page [2],
> is to support using pattern synonyms in an abstract matter—that is, to
> ensure that users who match on pattern synonyms don't have any
> internal implementation details of those pattern synonyms leak into
> error messages. This is well and good for many use cases, but there
> are also many use cases where we don't *care* about abstraction.
> Sometimes, we simply define a pattern synonym to be a convenient
> shorthand for a complicated pattern to facilitate code reuse, and
> nothing more.
>
> `LL` is a perfect example of this, in my opinion. `LL` is simply a
> thin wrapper around the use of `decomposeSrcSpan` as a view pattern.
> Trying to put `LL` into a COMPLETE set is silly since our intention
> isn't to hide the implementation details of decomposing a `SrcSpan`,
> but rather to avoid the need to copy-paste `(decomposeSrcSpan -> (m ,
> s))` in a bazillion patterns. Correspondingly, any use of `LL` ought
> to be treated as if the `(decomposeSrcSpan -> (m , s))` pattern were
> inlined—and from the pattern-match coverage checker's point of view,
> that *is* exhaustive!
>
> What's the moral of the story here? To me, this is a sign that the
> design space of pattern synonym coverage checking isn't rich enough.
> In addition to the existing {-# COMPLETE #-} machinery that we have
> today, I think we need to have a separate pragma for pattern synonyms
> that are intended to be transparent, non-abstract wrappers around
> patterns ({-# TRANSPARENT #-}, perhaps).
>
> Ryan S.
> -----
> [1] https://downloads.haskell.org/~ghc/8.6.1/docs/html/users_guide/glasgow_exts.html#complete-pragma
> [2] https://ghc.haskell.org/trac/ghc/wiki/PatternSynonyms/CompleteSigs
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs