Suppressing False Incomplete Pattern Matching Warnings for Polymorphic Pattern Synonyms

[Shayan Najd]

I also realised the COMPLETE pragmas are even less helpful (at least
for my case mentioned above) as they cannot be used when orphaned.
For example, I tried to follow the partial solution of introducing
multiple COMPLETE pragmas, one per a concrete instance of
`HasSrcSpan`. I defined the pattern synonym `LL` in
`basicTypes/SrcLoc.hs` and wanted to naturally define a COMPLETE
pragma for when `LL` is used for `Pat` in `hsSyn/HsPat.hs`. I got an
error complaining about orphaned COMPLETE pragmas. The only
unacceptable way (that I can see) that makes it work is to have a
module defining `LL`, importing all the instances of `HasSrcSpan`, and
all the COMPLETE pragmas (one per instance).

I have made a ticket about the original concern here:
  https://ghc.haskell.org/trac/ghc/ticket/15885

Until we come up with a good and general solution to this ticket, do
you know of a hack to suppress the false incomplete pattern matching
warnings in GHC? Should we add clauses like `foo _ = panic
"Impossible! How did you manage to bypass a complete matching?"`?

/Shayan

On Mon, 29 Oct 2018 at 14:52, Sylvain Henry <sylvain at haskus.fr> wrote:
>
> I've just found this related ticket: https://ghc.haskell.org/trac/ghc/ticket/14422
>
>
> On 10/26/18 7:04 PM, Richard Eisenberg wrote:
>
> Aha. So you're viewing complete sets as a type-directed property, where we can take a type and look up what complete sets of patterns of that type might be.
>
> Then, when checking a pattern-match for completeness, we use the inferred type of the pattern, access its complete sets, and if these match up. (Perhaps an implementation may optimize this process.)
>
> What I like about this approach is that it works well with GADTs, where, e.g., VNil is a complete set for type Vec a Zero but not for Vec a n.
>
> I take back my claim of "No types!" then, as this does sound like it has the right properties.
>
> For now, I don't want to get bogged down by syntax -- let's figure out how the idea should work first, and then we can worry about syntax.
>
> Here's a stab at a formalization of this idea, written in metatheory, not Haskell:
>
> Let C : Type -> Set of set of patterns. C will be the lookup function for complete sets. Suppose we have a pattern match, at type tau, matching against patterns Ps. Let S = C(tau). S is then a set of sets of patterns. The question is this: Is there a set s in S such that Ps is a superset of s? If yes, then the match is complete.
>
> What do we think of this design? Of course, the challenge is in building C, but we'll tackle that next.
>
> Richard
>
> On Oct 26, 2018, at 5:20 AM, Sylvain Henry <sylvain at haskus.fr> wrote:
>
> Sorry I wasn't clear. I'm not an expert on the topic but it seems to me that there are two orthogonal concerns:
>
> 1) How does the checker retrieve COMPLETE sets.
>
> Currently it seems to "attach" them to data type constructors (e.g. Maybe). If instead it retrieved them by matching types (e.g. "Maybe a", "a") we could write:
>
> {-# COMPLETE LL #-}
>
> From an implementation point of view, it seems to me that finding complete sets would become similar to finding (flexible, overlapping) class instances. Pseudo-code:
>
> class Complete a where
>   conlikes :: [ConLike]
> instance Complete (Maybe a) where
>   conlikes = [Nothing @a, Just @a]
> instance Complete (Maybe a) where
>   conlikes = [N @a, J @a]
> instance Complete a where
>   conlikes = [LL @a]
> ...
>
>
> 2) COMPLETE set depending on the matched type.
>
> It is a thread hijack from me but while we are thinking about refactoring COMPLETE pragmas to support polymorphism, maybe we could support this too. The idea is to build a different set of conlikes depending on the matched type. Pseudo-code:
>
> instance Complete (Variant cs) where
>   conlikes = [V @c | c <- cs] -- cs is a type list
>
> (I don't really care about the pragma syntax)
>
> Sorry for the thread hijack!
> Regards,
> Sylvain
>
>
> On 10/26/18 5:59 AM, Richard Eisenberg wrote:
>
> I'm afraid I don't understand what your new syntax means. And, while I know it doesn't work today, what's wrong (in theory) with
>
> {-# COMPLETE LL #-}
>
> No types! (That's a rare thing for me to extol...)
>
> I feel I must be missing something here.
>
> Thanks,
> Richard
>
> On Oct 25, 2018, at 12:24 PM, Sylvain Henry <sylvain at haskus.fr> wrote:
>
> > In the case where all the patterns are polymorphic, a user must
> > provide a type signature but we accept the definition regardless of
> > the type signature they provide.
>
> Currently we can specify the type *constructor* in a COMPLETE pragma:
>
> pattern J :: a -> Maybe a
> pattern J a = Just a
>
> pattern N :: Maybe a
> pattern N = Nothing
>
> {-# COMPLETE N, J :: Maybe #-}
>
>
> Instead if we could specify the type with its free vars, we could refer to them in conlike signatures:
>
> {-# COMPLETE N, [ J :: a -> Maybe a ] :: Maybe a #-}
>
> The COMPLETE pragma for LL could be:
>
> {-# COMPLETE [ LL :: HasSrcSpan a => SrcSpan -> SrcSpanLess a -> a ] :: a #-}
>
>
> I'm borrowing the list comprehension syntax on purpose because it would allow to define a set of conlikes from a type-list (see my request [1]):
>
> {-# COMPLETE [ V :: (c :< cs) => c -> Variant cs
>              | c <- cs
>              ] :: Variant cs
>   #-}
>
> >    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.
>
> Could we use a mechanism similar to instance resolution (with FlexibleInstances) for the checker to return matching COMPLETE sets instead?
>
> --Sylvain
>
>
> [1] https://mail.haskell.org/pipermail/ghc-devs/2018-July/016053.html
>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
>
>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs