The readability of the arrow seems unimportant, as it's primary use is, from what I can tell, to express a new kind of constraint which can then be produced by inference and used to typecheck a wider gamut of input code with more succinct type annotations. Generally the inference engine assumes all type constructors are matchable - meaning they're both generative and injective (while type families are neither). However, if you want to work with an arbitrary type with unapplied generics, you can't really consider it injective, since you don't know what kind it is, or weather the `f a ~ f b => a ~ b` injective relationship actually holds (it could be a type family for which it wouldn't hold). Generativity, on the other hand, primarily impacts inference and the ability to break a type apart to perform inferences on its parts (where, if assumed for higher kinds, could cause the inference engine to potentially "skip past" the desired inferences, from what I can tell). What the paper seems to be about is that by adding this novel constraint, you can start to work with partially applied types, since you simply need to acknowledge that these two rules need not always hold (when dealing with type constructors), and that so long as the solver is aware of where these rules do not hold, a well-typed and sound program can still be produced.
While _some_ higher-kinded manipulating code needs the explicit ->> syntax to be well-typed, the authors determined that explicitly requiring it (or, likewise, the polymorphic arrow syntax ->^U) would prevent the intent of older code from changing, while the improved inferences allowed just by the new constraint kinds existing allows new flexibility.
Also: I don't think there's anything you could write in the double arrow's place that would be "readable" or "just make sense". I think it's difficult to acquire an innane "sense" for what a higher kinded operation actually _is_. By sticking close to familiar syntax, it should hopefully be easier to grasp as a related concept.
While _some_ higher-kinded manipulating code needs the explicit ->> syntax to be well-typed, the authors determined that explicitly requiring it (or, likewise, the polymorphic arrow syntax ->^U) would prevent the intent of older code from changing, while the improved inferences allowed just by the new constraint kinds existing allows new flexibility.
Also: I don't think there's anything you could write in the double arrow's place that would be "readable" or "just make sense". I think it's difficult to acquire an innane "sense" for what a higher kinded operation actually _is_. By sticking close to familiar syntax, it should hopefully be easier to grasp as a related concept.