Finished getting type soundness refactored

It now fits properly in the REPL top-level.