Pattern match checking for GADTs

[Simon Peyton Jones]

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 at gmail.com<mailto:george.karachalias at 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 at haskell.org); Haskell Cafe (haskell-cafe at haskell.org)
Cc: George Karachalias; Tom Schrijvers; Dimitrios Vytiniotis (dimitris at 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20150219/4ecb5011/attachment.html>