>I don't understand. You're saying that there is a mismatch between what the programmer knows and what the compiler can deduce? That you know, from the state the program must be in, that the map has to contain the value associated with the given key? I can't think of an example were that would be the case off the top of my head.

Maybe you just put it there or it wasn't Maybe when you checked it?