title: Why doesn't subtyping via existentials and constraints work?
body: <p>I've been trying to see how Haskell copes with subtyping so I came up with the following snippet:</p>
  
  <pre class="lang-hs prettyprint-override"><code>{-# LANGUAGE RankNTypes #-}
  
  f1 :: () -&gt; Int
  f1 _ = 5
  
  f2 :: () -&gt; (forall a. Integral a =&gt; a)
  f2 = f1
  </code></pre>
  
  <p>The line <code>f2 = f1</code> fails with an unexpected error message:</p>
  
  <pre><code>Couldn't match type ‘a’ with ‘Int’
    ‘a’ is a rigid type variable bound by
      the type signature for:
        f2 :: forall a. Integral a =&gt; () -&gt; a
  </code></pre>
  
  <p>It seems that the existential has been promoted to a universal, which of course is unintended.</p>
  
  <p>My guess is that in implementation terms <code>f2</code> needs to return a value and a corresponding dictionary, while <code>f1</code> simply returns a value of type <code>Int</code>. However, from a logical perspective the contract of <code>f2</code> is "a function from <code>()</code> to some unknown instance of <code>Integral</code>" and <code>f1</code> satisfies it perfectly.</p>
  
  <p>Should GHC do some implicit magic to make it work or am I missing something?</p>