[Haskell-cafe] Over general types are too easy to make.

[Alvaro Gutierrez]

On Tue, Sep 4, 2012 at 5:14 AM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> 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.)