[Haskell-cafe] Documenting the impossible

[Andrew Coppin]

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 was thinking the message in the pragma would be what gets displayed 
on screen, along with some auto-generated location info. Just a module 
name and line number ought to be sufficient...)