On Tue, Sep 4, 2012 at 5:14 AM, Andreas Abel
I agree with Timothy. In the Agda code base, we have many occurrences of Timothy's pattern
aux (OneSpecificConstructor args) = ... aux _ = __IMPOSSIBLE__
where __IMPOSSIBLE__ generates code to throw an internal error.
+1 I've run into this situation quite a few times. I'm guessing it's especially irritating to fans of -Wall, in particular coupled with -Werror, the former of which includes exhaustiveness checking for patterns. Even without changing the type system it might still be useful, for example, to prevent such warnings for those cases when the missing patterns can be statically determined never to be used -- e.g. for functions known not to escape the module's scope. (Incidentally, exhaustiveness checking in lambdas doesn't seem to be enabled as of GHC version 7.2.2.)