Type inference plays a key role in the practical implementations of type systems. In the implementations of type inference, such as those in GHC and the OCaml compiler, various implementation techniques are often incorporated. While these implementation techniques can improve algorithmic efficiency and lead to a more uniform handling of multiple type features, they often exist only as folklore within the compiler source code, understandable only to a select group of implementers. Moreover, these techniques are not always reflected in the formal specifications of type inference, compromising the theoretical guarantees established by the formalism. In this talk, we argue that formalization of type inference implementation techniques is crucial in its own right. It exposes folklore to a wider community, and places implementation techniques on a more secured theoretical foundation, uncovering subtle bugs in the implementation.