Inference is a little more involved once you add lambda abstraction and function application.
Recommended:
Christoph Hegemann: type inference from scratch: https://www.youtube.com/watch?v=ytPAlhnAKro
Their grammar's a bit off, since they have:
<bool> ::= T | F | IsZero <num>
<num> ::= O
<arith> ::= Succ <num> | Pred <num>
That doesn't affect the actual implementation, since (as they say right after) "For simplicity, we merge all them together in a single Term."
Another educational (but more sophisticated) evaluator / typechecker in Haskell is described in "Stitch: The Sound Type-Indexed Type Checker" https://cs.brynmawr.edu/~rae/papers/2018/stitch/stitch.pdf
Isn’t this a reskin of Stephen Diehl’s earlier set of blog posts? Or is this a common PL example? http://dev.stephendiehl.com/fun/004_type_systems.html
This basically summarized the first half of the programming languages course I took. Nicely done
If you are interested in the subject, The Implementation of Functional Programming Languages by Simon Peyton Jones is actually freely available on his Microsoft Research page : https://www.microsoft.com/en-us/research/publication/the-imp...
The book is really great. It starts with a very interesting explanation of lambda calculus and how high-level functional programming language can be tied to it. Chapters 8 and 9 were written by Peter Hancock and cover step by step how to write a polymorphic type-checker (the examples are in Miranda but it's not far from Haskell).
For a 1987 book, it all aged very well.