I feel like the hardest part of implementing a type system is unification. A lot of the literature assumes that you know how to introduce and solve unification variables correctly and efficiently, but it's pretty challenging to author and maintain that sort of code
Conversation
If you stick to Hindley-Milner unification is very simple. But once you include higher-ranked types you have to keep track of the type variable scoping which is trickier. And then if you also want some subtyping between the foralls...difficult.
2
6
Glad I can refer to the elaboration-zoo for this stuff now 😳