title: How does instantiation of higher-rank types and subsumption interact during unification?
body: <p>A function type is higher-rank if a quantifier appears in contravariant position: <code>f :: (forall a. [a] -&gt; b) -&gt; Bool</code></p>
  <p>Regarding the unification of such a type the type variable <code>a</code> is more rigid than <code>b</code>, because the following instantiation rules apply:</p>
  <ul>
  <li><code>a</code> can be instantiated with a flexible type variable, provided this doesn't allow <code>a</code> to escape its scope</li>
  <li>or with another rigid type variable</li>
  <li>but not with a non-abstract type, because not the caller of <code>foo</code> but <code>foo</code> itself decides what <code>a</code> is, while <code>b</code> is already determined by the caller</li>
  </ul>
  <p>However, things get more complicated as soon as subsumption comes into play:</p>
  <pre><code>{-# LANGUAGE RankNTypes #-}
  
  f :: (forall a. [a] -&gt; [a]) -&gt; Int -- rank-2
  f _ = undefined
  
  arg1a :: a -&gt; a
  arg1a x = x
  
  arg1b :: [Int] -&gt; [Int]
  arg1b x = x
  
  f arg1a -- type checks
  f arg1b -- rejected
  
  g :: ((forall a. [a] -&gt; [a]) -&gt; Int) -&gt; Int -- rank-3
  g _ = undefined
  
  arg2a :: (a -&gt; a) -&gt; Int
  arg2a _ = 1
  
  arg2b :: (forall a. a -&gt; a) -&gt; Int
  arg2b _ = 1
  
  arg2c :: ([Int] -&gt; [Int]) -&gt; Int
  arg2c _ = 1
  
  g arg2a -- type checks
  g arg2b -- rejected
  g arg2c -- type checks
  
  h :: (((forall a. [a] -&gt; [a]) -&gt; Int) -&gt; Int) -&gt; Int -- rank-4
  h _ = undefined
  
  arg3a :: ((a -&gt; a) -&gt; Int) -&gt; Int
  arg3a _ = 1
  
  arg3b :: ((forall a. a -&gt; a) -&gt; Int) -&gt; Int
  arg3b _ = 1
  
  arg3c :: (([Int] -&gt; [Int]) -&gt; Int) -&gt; Int
  arg3c _ = 1
  
  h arg3a -- rejected
  h arg3b -- type checks
  h arg3c -- rejected
  </code></pre>
  <p>What immediately catches the eye is the subtype relation, which gets flipped for each additional contravariant position. The application <code>g arg2b</code> is rejected, because <code>(forall a. a -&gt; a)</code> is more polymorphic than <code>(forall a. [a] -&gt; [a])</code> and thus <code>(forall a. a -&gt; a) -&gt; Int</code> is less polymorphic than <code>(forall a. [a] -&gt; [a]) -&gt; Int</code>.</p>
  <p>The first thing I don't understand is why <code>g arg2a</code> is accepted. Does subsumption only kick in if both terms are higher-rank?</p>
  <p>However, the fact that <code>g arg2c</code> type checks puzzles me even more. Doesn't this clearly violate the rule that the rigid type variable <code>a</code> must not be instantiated with a monotype like <code>Int</code>?</p>
  <p>Maybe someone can lay out the unification process for both applications..</p>