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

older
trac ticket about missing in tree...

Ryan Scott

25 Oct 2018 25 Oct '18

2:40 p.m.

You *can* put `LL` into a COMPLETE set, but under the stipulation that you specify which type constructor it's monomorphized to. To quote the wiki page on COMPLETE sets: 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. The type constructor for the whole set of patterns is the type constructor as specified by the user. If the user does not provide a type signature then the definition is rejected as ambiguous. This design is a consequence of the design of the pattern match checker. Complete sets of patterns must be identified relative to a type. This is a sanity check as users would never be able to match on all constructors if the set of patterns is inconsistent in this manner. In other words, this would work provided that you'd be willing to list every single instance of `HasSrcSpan` in its own COMPLETE set. It's tedious, but possible. Ryan S. ----- [1] https://ghc.haskell.org/trac/ghc/wiki/PatternSynonyms/CompleteSigs#Typing

Show replies by date

Shayan Najd

25 Oct 25 Oct

3:59 p.m.

New subject: Suppressing False Incomplete Pattern Matching Warnings for Polymorphic Pattern Synonyms

...

[Ryan Scott:] In other words, this would work provided that you'd be willing to list every single instance of `HasSrcSpan` in its own COMPLETE set. It's tedious, but possible.

Yes, for the cases where `LL` is used monomorphically, we can use the per-instance COMPLETE pragma, but it does not scale to the generic cases where `LL` is used polymorphically. Consider the following where `Exp` and `Pat` are both instances of `HasSrcSpan`: {{{ {-# COMPLETE LL :: Exp #-} {-# COMPLETE LL :: Pat #-} unLocExp :: Exp -> Exp unLocExp (LL _ m) = m unLocPat :: Pat -> Pat unLocPat (LL _ m) = m unLocGen :: HasLoc a => a -> SrcSpanLess a unLocGen (LL _ m) = m }}} In the functions `unLocExp` and `unLocPat`, the related COMPLETE pragmas rightly avoid the false incomplete pattern matching warnings. However, to avoid the false incomplete pattern matching warning in `unLocGen`, either I should add a catch-all case `unLocGen _ = error "Impossible!"` or expose the internal view patterns and hence break the abstraction `unLocGen (decomposeSrcSpan->(_ , m)) = m` We want to avoid both solutions and unfortunately, this problem arises frequently enough. For example, in GHC, there are plenty of such generic cases (e.g., `sL1` or the like in the parser). I believe the source of the issue is what you just mentioned:

...

[Ryan Scott:] Complete sets of patterns must be identified relative to a type.

Technically `HasSrcSpan a0 |- a0` is a type, for a Skolem variable `a0`; I understand if you mean relative to a concrete type, but I don't understand why (I have no experience with GHC's totality checker code). Why can't it be syntactic? We should allow programmers to express things like "when you see `LL` treat the related pattern matching group as total". /Shayan On Thu, Oct 25, 2018 at 4:40 PM Ryan Scott wrote:

...

You *can* put `LL` into a COMPLETE set, but under the stipulation that you specify which type constructor it's monomorphized to. To quote the wiki page on COMPLETE sets:

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. The type constructor for the whole set of patterns is the type constructor as specified by the user. If the user does not provide a type signature then the definition is rejected as ambiguous.

This design is a consequence of the design of the pattern match checker. Complete sets of patterns must be identified relative to a type. This is a sanity check as users would never be able to match on all constructors if the set of patterns is inconsistent in this manner.

In other words, this would work provided that you'd be willing to list every single instance of `HasSrcSpan` in its own COMPLETE set. It's tedious, but possible.

Ryan S. ----- [1] https://ghc.haskell.org/trac/ghc/wiki/PatternSynonyms/CompleteSigs#Typing _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Sylvain Henry

4:24 p.m.

New subject: Suppressing False Incomplete Pattern Matching Warnings for Polymorphic Pattern Synonyms

...

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

Richard Eisenberg

26 Oct 26 Oct

3:59 a.m.

New subject: Suppressing False Incomplete Pattern Matching Warnings for Polymorphic Pattern Synonyms

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 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 https://mail.haskell.org/pipermail/ghc-devs/2018-July/016053.html _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Sylvain Henry

9:20 a.m.

New subject: 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

Richard Eisenberg

5:04 p.m.

New subject: Suppressing False Incomplete Pattern Matching Warnings for Polymorphic Pattern Synonyms

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 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 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 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 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 http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Carter Schonwald

27 Oct 27 Oct

1:43 a.m.

New subject: Suppressing False Incomplete Pattern Matching Warnings for Polymorphic Pattern Synonyms

off hand, once we're in in viewpattern/ pattern synonym land, ORDER of the abstracted constructors matters! consider foo,bar,baz,quux,boom :: Nat -> String plus some pattern synonyms i name "PowerOfTwo", "Even" and "Odd" foo (PowerOfTwo x) = "power of two" foo (Even x) = "even" foo (Odd x) = "odd" bar (Even x) = "even" bar (Odd x) = "odd" baz (PowerOfTwo x) = "power of two" baz (Odd x) = "odd" quux (Even x) = "even" quux (Odd x) = "odd" quux (PowerOfTwo) = "power of two" boom (Even x) = "even" boom (PowerOfTwo x) = "power of two" boom (Odd x) = "odd" foo and bar are both total definitions with unambiguous meanings, even though bar's patterns are a suffix of foos'! baz is partial! both boom and quux have a redudant overlapping case, power of two! so some thoughts 1) order matters! 2) pattern synonyms at type T are part of an infinite lattice, Top element == accept everything, Bottom element = reject everything 3) PowerOfTwo <= Even in the Lattice for Natual, both are "incomparable" with Odd 4) for a simple case on a single value at type T, assume c1 <= c2 , then if c1 x -> ... is before c2 x -> in the cases, then both are useful/computationally meaningful OTHERWISE when its case x :: T of c2 x -> ... c1 x -> ... then the 'c1 x' is redundant this is slightly orthogonal to other facets of this discussion so far, but i realized that Richard's Set of Sets of patterns model misses some useful/ meaningful examples/extra structure from a) the implicit lattice of different patterns possibly being super/subsets (which is still something of an approximation, but with these example I shared above I hope i've sketched out some motivation ) b) we can possibly model HOW ordering of clauses impacts coverage/totality / redundancy of clauses I'm not sure if it'd be pleasant/good from a user experience perspective to have this sort of partial ordering modelling stuff, but certainly seems like it would help distinguish some useful examples where the program meaning / coverage is sensitive to clause ordering i can try to spell this out more if theres interest, but I wanted to share while the iron was hot best! -Carter On Fri, Oct 26, 2018 at 1:05 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 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 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 http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Richard Eisenberg

29 Oct 29 Oct

3:54 a.m.

New subject: Suppressing False Incomplete Pattern Matching Warnings for Polymorphic Pattern Synonyms

...

On Oct 26, 2018, at 9:43 PM, Carter Schonwald wrote:

ORDER of the abstracted constructors matters!

That's a very good point. So we don't have a set of sets -- we have a set of lists (where normal constructors -- which have no overlap -- would appear in the lists in every possible permutation). Again, please don't take my set of lists too seriously from an implementation point of view. We clearly wouldn't implement it this way. But I want to use this abstraction to understand the shape of the problem and what an idealized solution might look like before worrying about implementation and syntax. Richard

Sylvain Henry

1:51 p.m.

New subject: Suppressing False Incomplete Pattern Matching Warnings for Polymorphic Pattern Synonyms

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 mailto:sylvain@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 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

Shayan Najd

10 Nov 10 Nov

1:37 a.m.

New subject: Suppressing False Incomplete Pattern Matching Warnings for Polymorphic Pattern Synonyms

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 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 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 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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

2431

Age (days ago)

2447

Last active (days ago)

List overview

Download

9 comments

5 participants

participants (5)

Carter Schonwald
Richard Eisenberg
Ryan Scott
Shayan Najd
Sylvain Henry