[Haskell-cafe] Documenting the impossible

[Derek Elkins]

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.