Re: Suppressing False Incomplete Pattern Matching Warnings for Polymorphic Pattern Synonyms

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 mailto:sylvain@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 apattern J a = Just apattern N :: Maybe apattern 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@haskell.org mailto:ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs