Unification and constraint solving is a big reason why. Prolog is definitely the easiest language to write a type checker in because it not only has unification

Unification and constraint solving is a big reason why. Prolog is definitely the easiest language to write a type checker in because it not only has unification built in, it is also excellent at navigating trees like type hierarchies. Something I've personally used it for was navigating the parse tree of some T-SQL I was analyzing (it was 100k+ LoC so manual analysis was out of the question). There is a pretty good C# library for parsing T-SQL, but it is unwieldy to use since it relies on visitors and has tons of different typed nodes with a huge inheritance hierarchy. I ended up exporting this to JSON including type information and initially used jq for analysis. However, even that ended up being hard to manage so I switched to Prolog and it was way easier to write. In terms of this project, I particularly liked that the code was so dense and expressive that I could write the program by first testing things out in the REPL.