I wrote the description in the paper, so you’ve already read my best efforts to explain this, but I’ll have another go.
In Haskell, if you have a type Foo Int you know that there is no type Bar Int that will be equal to it. The newtypes/datatypes Foo and Bar are fresh types that do not overlap.
You could create a type alias type Baz x = Foo x but since that alias can never have its definition hidden we can just always expand them away and never consider them as candidates for higher-kinded polymorphism.
This freshness restriction means that if you need to unify Foo Int with m Int you can always just say that Foo = m without any loss of generality.
In OCaml, if you see int foo and int bar they may well be equal, even though foo and bar themselves might not be. For example,
type 'a foo = 'a * int
type 'a bar = int * 'a
In this case, if you need to unify int foo with int 'm (assuming we had higher-kinded variables) you can not just make 'm = foo because 'm = bar would also be a valid solution and neither one is more general than the other – there is no “best” answer and making an arbitrary choice will mean that your type inference’s success is dependent on arbitrary implementation details of your inference algorithm.
So without the freshness restriction of Haskell you cannot have simple higher-kinded polymorphism. However, there are costs to the restriction as well. Support for modular abstraction (i.e. functors in OCaml) requires the ability to have multiple names for the same thing – the parameter of a functor will be equal to the functor’s arguments – and this does not play nicely with these kinds of freshness restrictions.