Added another example from stackoverflow.

Also reduced the error output on type mismatch.
The example was originally for coq, I translated it to itt.