It was a deliberate decision not to present type inference for expressions and definitions. The approach here is to present in as straightforward a way as possible the constraints which the type system imposes, so that when a type error occurs, its source can be understood.
On the other hand, it would be quite possible to build an exposition of type inference on the back of the rules given here.
The presentation here gives the rules in a monomorphic setting first, then generalising them for the polymorphic setting. It would be possible to go straight to the polymorphic version.
I have included the material on restrictions of polymorphism for completeness. It can be omitted without affecting students' ability to program; it simply shows the limits of the possible in this context.