[Haskell-cafe] Pattern match checking for GADTs

[Aaron Levin]

Same with Oliver (can't see email and would like to contribute).
On Thu, Feb 19, 2015 at 12:51 PM Oliver Charles <ollie at ocharles.org.uk>
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 <simonpj at microsoft.com
> > 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 at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>>
>>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20150219/f72980bd/attachment.html>