<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>
<div><span class="gmail_quote">On 11/30/07, <b class="gmail_sendername">Pablo Nogueira</b> &lt;<a href="mailto:pirelo@googlemail.com">pirelo@googlemail.com</a>&gt; wrote:</span></div>
<blockquote class="gmail_quote" style="PADDING-LEFT: 1ex; MARGIN: 0px 0px 0px 0.8ex; BORDER-LEFT: #ccc 1px solid">A question about existential quantification:<br><br>Given the existential type:<br><br>data Box = forall a. B a
<br><br>in other words:<br><br>-- data Box = B (exists a.a)<br>-- B :: (exists a.a) -&gt; Box<br><br>I cannot type-check the function:<br><br>mapBox :: forall a b. (a -&gt; b) -&gt; Box -&gt; Box<br>--&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:: forall a b. (a -&gt; b) -&gt; (exists 
a.a) -&gt; (exists a.a)<br>mapBox f (B x) = B (f x)<br><br>Nor can I type check:<br><br>mapBox :: forall a. (a -&gt; a) -&gt; Box -&gt; Box<br>--&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:: forall a. (a -&gt; a) -&gt; (exists a.a) -&gt; (exists a.a)<br>
mapBox f (B x) = B (f x)<br><br>The compiler tells me that in both functions, when it encounters the<br>expression |B (f x)|, it cannot unify the&nbsp;&nbsp;universally quantified |a|<br>(which generates a rigid type var) with the existentially quatified
<br>|a| (which generates a different rigid type var) -- or so I interpret<br>the error message.<br><br>However, at first sight |f| is polymorphic so it could be applied to<br>any value, included the value hidden in&nbsp;&nbsp;|Box|.
<br><br>Of course, this works:<br><br>mapBox :: (forall a b. a -&gt; b) -&gt; Box -&gt; Box<br>mapBox f (B x) = B (f x)<br><br>Because it&#39;s a tautology: given a proof of a -&gt; b for any a or b I can<br>prove Box -&gt; Box. However the only value of type forall a b. a -&gt; b is
<br>bottom.<br><br>This also type-checks:<br><br>mapBox :: (forall a. a -&gt; a) -&gt; Box -&gt; Box<br>mapBox f (B x) = B (f x)<br><br>When trying to give an explanation about why one works and the other<br>doesn&#39;t, I see that, logically, we have:
<br><br>forall a. P(a) =&gt; Q&nbsp;&nbsp;implies (forall a. P(a)) =&gt; Q&nbsp;&nbsp; when a does not<br>occur in Q.<br><br>The proof in our scenario is trivial:<br><br>p :: (forall a. (a -&gt; a) -&gt; (Box -&gt; Box)) -&gt; (forall a. a -&gt; a) -&gt; Box -&gt; Box
<br>p mapBox f b = mapBox f b<br><br>However, the converse is not true.<br><br>Yet, could somebody tell me the logical reason for the type-checking<br>error? In other words, how does the unification failure translate<br>logically. Should the first mapBox actually type-check?
<br><br>Isn&#39;t the code for&nbsp;&nbsp;mapBox :: forall a. (a -&gt; a) -&gt; Box -&gt; Box<br>encoding the proof:<br><br>Assume forall a. a -&gt; a<br>Assume exists a.a<br>unpack the existential, x :: a = T for some T<br>apply f to x, we get (f x) :: a
<br>pack into existential,&nbsp;&nbsp; B (f x) :: exists a.a<br>Discharge first assumption<br>Discharge second assumption<br><br>The error must be in step 3. Sorry if this is obvious, it&#39;s not to me right now.<br>_______________________________________________
<br>Haskell-Cafe mailing list<br><a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br><a href="http://www.haskell.org/mailman/listinfo/haskell-cafe">http://www.haskell.org/mailman/listinfo/haskell-cafe
</a><br></blockquote><br>