<div><span class="gmail_quote">It seems you&#39;ve already figured this out, but here&#39;s a quick counterexample:</span></div>
<div><span class="gmail_quote"></span>&nbsp;</div>
<div><span class="gmail_quote">&gt; {-# LANGUAGE ExistentialQuantification, RankNTypes #-}</span></div>
<div><span class="gmail_quote">&gt; module Box where</span></div>
<div><span class="gmail_quote">&gt; data Box = forall a. B a</span></div>
<div><span class="gmail_quote">&gt;</span></div>
<div><span class="gmail_quote">&gt; --mapBox :: forall a b. (a -&gt; b) -&gt; Box -&gt; Box -- incorrect type</span></div>
<div><span class="gmail_quote">&gt; mapBox f (B x) = B (f x)</span></div>
<div><span class="gmail_quote"></span>&nbsp;</div>
<div><span class="gmail_quote">then:</span></div>
<div><span class="gmail_quote"></span>&nbsp;</div>
<div><span class="gmail_quote">&gt; boxedInt :: Box</span></div>
<div><span class="gmail_quote">&gt; boxedInt = B (1 :: Int)</span></div>
<div><span class="gmail_quote"></span>&nbsp;</div>
<div><span class="gmail_quote">&gt; f :: [Int] -&gt; Int</span></div>
<div><span class="gmail_quote">&gt; f = sum</span></div>
<div><span class="gmail_quote"></span>&nbsp;</div>
<div><span class="gmail_quote">mf :: Box -&gt; Box</span></div>
<div><span class="gmail_quote">mapBox f -- this is well-typed according to the specified type&nbsp;of &quot;mapBox&quot;</span></div>
<div><span class="gmail_quote"></span>&nbsp;</div>
<div><span class="gmail_quote">But,</span></div>
<div><span class="gmail_quote"></span><span class="gmail_quote">mf boxedInt :: Box</span></div>
<div><span class="gmail_quote"></span>&nbsp;</div>
<div><span class="gmail_quote">mf boxedInt</span></div>
<div><span class="gmail_quote">= mapBox f boxedInt</span></div>
<div><span class="gmail_quote">= mapBox sum (B (1 :: Int))</span></div>
<div><span class="gmail_quote">= B (sum (1 :: Int))</span></div>
<div><span class="gmail_quote">which is not well-typed.</span></div>
<div><span class="gmail_quote"></span>&nbsp;</div>
<div><span class="gmail_quote">The&nbsp;least specific type for MapBox is</span></div>
<div><span class="gmail_quote">
<div><span class="gmail_quote"></span>&nbsp;</div>
<div><span class="gmail_quote">&gt; mapBox :: forall&nbsp;b. (forall a. (a -&gt; b)) -&gt; Box -&gt; Box</span></div></span></div>
<div><span class="gmail_quote"></span>&nbsp;</div>
<div><span class="gmail_quote">There are non-bottom functions of this type, for example:</span></div>
<div><span class="gmail_quote">&nbsp;&nbsp; const&nbsp;(1 :: Int)&nbsp;:: forall a. a -&gt; Int</span></div>
<div><span class="gmail_quote"></span>&nbsp;</div>
<div><span class="gmail_quote">With this type,</span></div>
<div><span class="gmail_quote"></span>&nbsp;</div>
<div><span class="gmail_quote">&gt; ok :: Box</span></div>
<div><span class="gmail_quote">&gt; ok =&nbsp;mapBox (const 1) (B &quot;hello&quot;)</span></div>
<div><span class="gmail_quote"></span>&nbsp;</div>
<div><span class="gmail_quote">is well-typed.</span></div>
<div><span class="gmail_quote"></span>&nbsp;</div>
<div><span class="gmail_quote">&nbsp; -- ryan</span></div>
<div><span class="gmail_quote"></span>&nbsp;</div>