Suppressing False Incomplete Pattern Matching Warnings for Polymorphic Pattern Synonyms

Richard Eisenberg rae at
Fri Oct 26 17:04:45 UTC 2018

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.


> On Oct 26, 2018, at 5:20 AM, Sylvain Henry <sylvain at> 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 <mailto:sylvain at>> 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] <>
>>> _______________________________________________
>>> ghc-devs mailing list
>>> ghc-devs at <mailto:ghc-devs at>
>>> <>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <>

More information about the ghc-devs mailing list