Suppressing False Incomplete Pattern Matching Warnings for Polymorphic Pattern Synonyms

[Sylvain Henry]

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 
>> <mailto: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 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 at haskell.org <mailto:ghc-devs at haskell.org>
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20181026/3694cc70/attachment.html>