> (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.
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.