Implementing decidable type inference

I've wanted to fully implement type synthesis for a good while now and it's about time. This isn't a formal project just a place for me to stash what I have. I started with typed lambda calculus and am expanding from there. I've resolved to not use any annotations and see how far I can get before going back to my homework.