The Hindley-Milner type system plus polymorphic recursion is undecidable or semidecidable?
The answer you gave is right, but I'd like to stress the relationship between the two terms.

A formal language is decidable if and only if there exists an algorithm which correctly accepts or rejects every input in finite time. We also say it's computable.

A formal language is undecidable if and only if it is not decidable.

A formal language is semidecidable if and only if an algorithm exists that recognizing an input that is in the language. In particular, all decidable languages are semidecidable! However the halting problem is an example of a semidecidable language that is also undecidable. The complement of the halting problem is not even semidecidable.

We say type inference is undecidable rather than semidecidable (even though both characterizations are true) because the former is usually more relevant.