Define auxiliary unifying type checker

[jonsterling]

In order to unleash #118, it will be necessary to have a (non-core/untrusted) version of the typechecker that runs in the Contextual monad and invokes the unifier at key points. It's a shame to have two typecheckers, but I don't know how to avoid it; I think it's simple enough that we can maintain both of them.