Higher-ranked polymorphism without explicit application or subtyping?
The Dunfield &amp; Krishnaswami paper's introduction refers to Practical type inference for arbitrary-rank types


  As can be seen, it scales well to advanced type systems; moreover,
  it is easy to implement, and yields relatively high-quality error messages
  (Peyton Jones et al. 2007)


In System F-ish approach there is also a "subtyping" relation. See section 3.3 Subsumption. 



I'd also emphasize that Haskell doesn't have impredicative types (or inference for them). See: https://mail.haskell.org/pipermail/ghc-devs/2016-September/012940.html for pointers.


  
  You can write a polytype in a visible type argument; eg.  f @(forall a. a->a)
  You can write a polytype as an argument of a type in a signature  e.g.  f :: [forall a. a->a] -> Int
  
  And that’s all.  A unification variable STILL CANNOT be unified with a polytype.  The only way you can call a polymorphic function at a polytype is to use Visible Type Application.
  
  
  In short, if you call a function at a polytype, you must use VTA.  Simple, easy, predictable; and doubtless annoying.  But possible.


I.e. id id will always be elaborated as

forall a. id @(a -&gt; a) (id @a)


not

id @(forall a. a -&gt; a) id


Yet, you can write the latter explictly, if you enable ImpredicativeTypes.