On Sat, 2008-06-14 at 19:58 +0100, Andrew Coppin wrote:
I have a small idea. I'm curios if anybody else thinks it's a good idea...
How about a {-# IMPOSSIBLE #-} pragma that documents the fact that a particular point in the program *should* be unreachable?
For example, you look up a key in a Map. You know the key is there, because you just put it there yourself two seconds ago. But, theoretically, lookup returns a Maybe x so - theoretically - it's possible it might return Nothing. No matter what you do, GHC will insert code to check whether we have Just x or Nothing, and in the Nothing case throw an exception.
Obviously there is no way in hell this code path can ever be executed. At least, assuming your code isn't broken... This is where the pragma comes in. The idea is that you write something like
case lookup k m of Just v -> process v Nothing -> {-# IMPOSSIBLE "lookup in step 3" #-}
When compiled without optimisations, the pragma just causes an exception to be thrown, rather like "error" does. When compiled with optimisations, the whole case alternative is removed, and no code is generated for it. (And if the impossible somehow happens... behaviour is undefined.) So you test your program with your code compiled unoptimised, and when you're "sure" the impossible can't happen, you tell the compiler to remove the check for it. (Actually, it would possibly be a good idea to have a switch to turn this on and off seperately if needed...)
Does anybody think this is a useful idea? If so I'll add a feature request ticket to the GHC Trac. But I want to see if folks like the idea first...
I think it's a horrible idea.