And a snag popped up in thesis stuff.
Turns out showing decidability of typing (specifically showing completeness of the algorithm) is not quite as trivial as I thought. Grr.