[Haskell-cafe] Pattern match checking for GADTs

[Jon Sterling]

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 <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
> >
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe