[Haskell-cafe] Pattern match checking for GADTs

[Andres Loeh]

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