What is the difference between System F and Hindley-Milner type system?
Yes, In Hindley-Milner universal quantifiers are allowed only at the outside of a type (and therefore omitted). For example, in HM you can have the type $\forall \alpha.(\alpha\to\alpha) \to (\alpha\to\alpha)$ usually abbreviated as $(\alpha\to\alpha)\to(\alpha\to\alpha)$, but you cannot have $(\forall \alpha.\alpha\to\alpha) \to (\forall \alpha.\alpha\to\alpha)$. 

A special feature of HM (that does not make sense for system F) is the distinction between let-bindings and beta reducts. In a let-binding the type of the bound variable may be polymorphic in the sense that its free type variables are quantified separately. For example, 

let f = λ x . x in λ x . f f x


can be typed in HM and in system F (by giving f the polymorphic type $\forall \alpha.\alpha\rightarrow\alpha$), but

(λ f . λ x. f f x) (λ x . x)


cannot be typed in HM, only in Sytem F.

The advantage of these restrictions is that type inference for HM
is decidable and rather efficiently so whereas it is undecidable
for F.