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.commailto: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

I just want to thank you folks for doing this. David On Thu, Feb 19, 2015 at 12: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