&gt; Actually, my question is why the different type can&#39;t be unified with the inferred type?<br><br>Because without ScopedTypeVariable, both types got expanded to :<br><br>legSome :: <b>forall nt</b> t s. LegGram nt t s -&gt; nt -&gt; Either String ([t], s)<br>

<br>subsome :: <b>forall nt</b> t s. [RRule nt t s] -&gt;  Either String ([t], s)<br><br>So you see subsome declare new variables, which <b>do not </b>match the <b>rigid </b>ones declared by legSome signature, hence the incompatibility.<br>

<br>
As we said before, you have three ways to work it out:<br>
1) Use scoped type variables with explicit forall nt on legSome and <b>no forall </b>on subsome, so that nt in subsome matches nt declared in legSome.<br>
2) Don&#39;t give a type signature for subsome and let GHC find out which is its correct type.<br>
3) Extract subsome so that it becomes a top-level function with a polymorphic type (Recommended).<br>
<br><br>Now, concerning the error I asked you to deliberately provoke, that&#39;s the quickest way I found to know what is the output of the type inferer, and maybe the only simple one.<br>So this error is:<br>&gt; Couldn&#39;t match expected type `Int&#39;<br>


 &gt;               with actual type `[([Symbols nt t], [s] -&gt; t0)]<br>
 &gt;                                 -&gt; Either [Char] ([t], t0)&#39;<br>
 &gt;   In the expression: subsome :: Int<br>
GHC tells you the type it infers for subsome: [([Symbols nt t], [s] -&gt; t0)] -&gt; Either [Char] ([t], t0)<br>The nt you see is the one from legSome, those messages show scoped variables. (You&#39;d get something like &#39;nt1&#39; or &#39;nt0&#39; if it was another variable, meant to be instanciated to a different type).<br>

This accords with your previous error message, which happens to give you more details about where the rigid type variable nt comes from:<br>&gt;      `nt&#39; is a rigid type variable bound by<br>
&gt;           the type signature for<br>
&gt;             legSome :: LegGram nt t s -&gt; nt -&gt; Either String ([t], s)<br><br>HTH.<br><br><div class="gmail_quote">2012/1/3 Yucheng Zhang <span dir="ltr">&lt;<a href="mailto:yczhang89@gmail.com">yczhang89@gmail.com</a>&gt;</span><br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">On Wed, Jan 4, 2012 at 2:48 AM, Bardur Arantsson &lt;<a href="mailto:spam@scientician.net">spam@scientician.net</a>&gt; wrote:<br>


&gt; &#39;subsome&#39; to a different type than the one you intended -- and indeed one<br>
&gt; which can&#39;t be unified with the inferred type. (Unless you use<br>
&gt; ScopedTypeVariables.)<br>
<br>
</div>Thanks for the reply.<br>
<br>
Actually, my question is why the different type can&#39;t be unified with<br>
the inferred type? Could you point me some related resources?<br>
<div class="HOEnZb"><div class="h5"><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" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</div></div></blockquote></div><br>