title: What happens to missing type variables in Church-style core?
body: <p>This is a bit esoteric, but maddening. In an answer to <a href="https://stackoverflow.com/questions/7074322/haskell-type-system-nuances">another question</a>, I noted that in this entirely valid program</p>
  
  <pre><code>poo :: String -&gt; a -&gt; a
  poo _ = id
  
  qoo :: (a -&gt; a) -&gt; String
  qoo _ = ""
  
  roo :: String -&gt; String
  roo = qoo . poo
  </code></pre>
  
  <p>the type variable <code>a</code> is neither solved nor generalized in the process of checking <code>roo</code>. I'm wondering what happens in the translation to GHC's core language, a Church-style variant of System F. Let me spell things out longhand, with explicit type lambdas <code>/\</code> and type applications <code>@</code>.</p>
  
  <pre><code>poo :: forall a. [Char] -&gt; a -&gt; a
  poo = /\ a -&gt; \ s x -&gt; id @ a
  
  qoo :: forall a. (a -&gt; a) -&gt; [Char]
  qoo = /\ a -&gt; \ f -&gt; [] @ Char
  
  roo :: [Char] -&gt; [Char]
  roo = (.) @ [Char] @ (? -&gt; ?) @ [Char] (qoo @ ?) (poo @ ?)
  </code></pre>
  
  <p>What on earth goes in the <code>?</code> places? How does <code>roo</code> become a valid core term? Or do we really get a mysterious vacuous quantifier, despite what the type signature says?</p>
  
  <pre><code>roo :: forall a. [Char] -&gt; [Char]
  roo = /\ a -&gt; ...
  </code></pre>
  
  <p>I've just checked that</p>
  
  <pre><code>roo :: forall . String -&gt; String
  roo = qoo . poo
  </code></pre>
  
  <p>goes through ok, which may or may not mean that the thing typechecks with no extra quantification.</p>
  
  <p>What's happening down there?</p>