Non-exhaustive pattern-match warning in code-example from "Dependently Typed Programming with Singletons"

[Edsko de Vries]

Yes, this is a nuisance, esp because ghc can most of the time see perfectly
well that if you *do* write down the "missing" cases that they are
inaccessible. There are a bunch of open tickets about it. I too use
Richard's trick; I tend to use

    foo _ _ = error "inaccessible"

Fixing ghc so that it can always see that clauses are not actually missing
might be difficult; perhaps the solution adopted in Agda would be easier,
where you would write

    foo (SomeConstructor _) (SomeOtherConstructor _) ()

(where SomeConstructor and SomeOtherConstructor are the "missing" cases) to
indicate that "this is inaccessible pattern".

-E


On Mon, May 19, 2014 at 12:45 AM, Richard Eisenberg <eir at cis.upenn.edu>wrote:

> The short answer here (to "Is there a way to avoid the non-exhaustive
> pattern-match warning?") is "no, not in general". See #3927 (
> https://ghc.haskell.org/trac/ghc/ticket/3927).
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140519/3ee409d1/attachment.html>