> Property based testing frameworks tend to show you the simplest concrete example of your error. Type checkers tend to show you the most abstract example of your error. Maybe if type checkers started to to incorporate more concrete examples of error, people would generally find them more appealing.

I think this is a really important insight! And in fact, there is some recent research about making type checkers produce counterexamples: http://lambda-the-ultimate.org/node/5355. Ergonomics of type systems is an unfortunately understudied area.