Unification

I'm reading a Haskell tutorial:
http://www.cs.cornell.edu/courses/cs3110/2011sp/lectures/lec26-type-inference/type-inference.htm

where is the proof that unification always exists?

>>10
but isnt 'computer aided learning' just turning language reference manuals into interactive fiction games? how could that possibly make learning easier rather than 100x more irritating and difficult?