Print the terms when there's a type mismatch

[langston-barrett]

Both Elm and GHC compilers print the problematic terms when there is a type mismatch. This will require passing more information to unify, perhaps a new DebugInformation type rather than just an LName.

In the long term, I think Elm's compiler really shines in this sort of thing, and would be great to emulate:

• http://elm-lang.org/blog/compilers-as-assistants
• http://elm-lang.org/blog/compiler-errors-for-humans

[brianhuffman]

We probably won't put much effort into improving error messages for the saw-script type checker, given that we plan to move over to the python interface.

[atomb]

Given @brianhuffman's comment above, I'm going to close this.