Suppressing False Incomplete Pattern Matching Warnings for Polymorphic Pattern Synonyms

[Sylvain Henry]

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 
>> <mailto: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 
>>>> <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/20181029/85cecc9b/attachment.html>