That’s kinda what brought unification to my attention. For my own education I’m writing a compiler for a simple ML-style language. Enjoying Pierce’s Types and Programming Languages meanwhile.