At PivotCloud, we have some internal code that would benefit from this being fixed; it's internal for aesthetic reasons, rather than IP, so we would be happy to share it with anyone who is trying to work on this problem. Kind regards, Jon On Thu, Feb 19, 2015, at 10:17 AM, Aaron Levin wrote:

Same with Oliver (can't see email and would like to contribute). On Thu, Feb 19, 2015 at 12:51 PM Oliver Charles wrote:

...

I have some code that I could provide, but I don't seem to see George's email address in the CC (only Tom's). Perhaps GMail ate it for some reason - but either way, I don't know where to send my code :)

-- Ollie

On Thu, Feb 19, 2015 at 5:37 PM, Simon Peyton Jones

...

wrote:

...

Friends

George Karachalas, Tom Schrijvers, Dimitrios Vytiniotis, and I are working on finally cracking the problem of accurately reporting pattern-match overlap and redundancy warnings, in the presence of GADTs. You know the problem; consider

vzip :: Vect n a -> Vect n b -> Vect n (a,b)

vzip VN VN = VN

vzip (VC x xs) (VC y ys) = VC (x,y) (vzip xs ys)

data Vect :: Nat -> * -> * where

VN :: Vect Zero a

VC :: a -> Vect n a -> Vect (Succ n) a

Are there any missing equations in vzip? No! But GHC complains anyway. We have lots of Trac tickets about this; e.g. https://ghc.haskell.org/trac/ghc/ticket/3927.

We now have a draft paper (wait a week) and a prototype implementation, that fixes the problem. But we need your help. We’d like to try our prototype on real code, not just toy examples.

*So, could you send George a pointer to any packages you have, or know of, that*

· *use GADTS (or other fancy type features) and *

· *would benefit from accurate pattern-match overlap/redundancy warnings?*

Specifically:

· Where you have had to add a catch-all

f _ _ = error “impossible”

to silence GHC from saying “missing patterns”

· Or where you have added {-# OPTIONS_GHC –fno-warn-missing-patterns #-} to silence the warnings.

· Or something else like that.

George’s email is in cc.

Time is short – the ICFP deadline is on 27 Feb. So sooner is better than later for us. But later is better than never.

Thank you!

Simon

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

Hi Simon and George. All of generics-sop, basic-sop, pretty-sop, lens-sop, json-sop (all on Hackage) have instances of such pattern matches. You can grep for 'error "inaccessible"' to find the places in question. Cheers, Andres On Thu, Feb 19, 2015 at 7:21 PM, Simon Peyton Jones wrote:

I have some code that I could provide, but I don't seem to see George's email address in the CC (only Tom's). Perhaps GMail ate it for some reason - but either way, I don't know where to send my code :)

Second attempt, to try to include George’s email. If it’s not in cc, it is: george.karachalias@gmail.com

Strange. My “sent items” folder definitely shows him in cc.

Sorry for the spam.

Simon

From: Simon Peyton Jones Sent: 19 February 2015 17:38 To: Haskell Libraries (libraries@haskell.org); Haskell Cafe (haskell-cafe@haskell.org) Cc: George Karachalias; Tom Schrijvers; Dimitrios Vytiniotis (dimitris@microsoft.com); Simon Peyton-Jones Subject: Pattern match checking for GADTs

Friends

George Karachalas, Tom Schrijvers, Dimitrios Vytiniotis, and I are working on finally cracking the problem of accurately reporting pattern-match overlap and redundancy warnings, in the presence of GADTs. You know the problem; consider

vzip :: Vect n a -> Vect n b -> Vect n (a,b)

vzip VN VN = VN

vzip (VC x xs) (VC y ys) = VC (x,y) (vzip xs ys)

data Vect :: Nat -> * -> * where

VN :: Vect Zero a

VC :: a -> Vect n a -> Vect (Succ n) a

Are there any missing equations in vzip? No! But GHC complains anyway. We have lots of Trac tickets about this; e.g. https://ghc.haskell.org/trac/ghc/ticket/3927.

We now have a draft paper (wait a week) and a prototype implementation, that fixes the problem. But we need your help. We’d like to try our prototype on real code, not just toy examples.

So, could you send George a pointer to any packages you have, or know of, that

· use GADTS (or other fancy type features) and

· would benefit from accurate pattern-match overlap/redundancy warnings?

Specifically:

· Where you have had to add a catch-all

f _ _ = error “impossible”

to silence GHC from saying “missing patterns”

· Or where you have added {-# OPTIONS_GHC –fno-warn-missing-patterns #-} to silence the warnings.

· Or something else like that.

George’s email is in cc.

Time is short – the ICFP deadline is on 27 Feb. So sooner is better than later for us. But later is better than never.

Thank you!

Simon

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe