> (It should also do so using a straightforward explanation, ideally featuring a counterexample or stripped-down unprovable proposition. I don't know any type checker that does this, currently.)

I guess the incomplete-pattern-matching warnings (in eg ghc) come closest. They usually give you an example of an example of a value you haven't matched. But that's a very restricted and simple domain.