Many modern programming languages are statically typed. Every piece of data is classified by its type, and at compile time, programs are checked for consistent usage through a process known as typechecking (TC). Like most complicated systems, good software engineering practices (e.g. separation of concerns via phase separation, computational abstraction through monads and applicatives, etc.) can help language implementors write maintainable TC code. Designing sound and decidable type systems is hard. Therefore, researchers formally study type systems and TC algorithms and strive to mechanize them in proof assistants. Unfortunately, mechanized implementations usually do not follow the same software engineering principles. Exceptions to that rule exist, e.g. Silva et al. [11] implement monadic TC in Coq, but we are unaware of any mechanization that combines a monadic implementation with phase separation. Moreover, practical concerns like elaboration or type reconstruction are usually not covered. Our goal is to develop a general approach to mechanizing TC, that uses abstraction via monads, employs phase separation and can also produce multiple outputs, e.g. for type reconstruction