[piinbinary]

I wrote a bit about how to inter types here: http://jeremymikkola.com/posts/2018_03_25_understanding_algo...

Two things I see missing from your code: A current substitution and a unification function.

This paper might also be helpful to read: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.65....

[AnaniasAnanas]

Why does everyone assume that the OP tries to implement type inference? System F and HM are incompatible with each other.