Ah... now I understand your concern; I should have written<br>something like: <br><br>where K  +_t  K&#39;  denotes the set of constraints from K plus <br>those from K&#39; that have type variables reachable from t.<br><br>
instead of: <br><br>where K  +_t  K&#39;  denotes the constraint-set obtained by adding from K&#39;<br>only constraints with type variables reachable from t.<br><br>Cheers,<br><br>Carlos<br><br><div class="gmail_quote">On Thu, Sep 16, 2010 at 6:56 PM, Luke Palmer <span dir="ltr">&lt;<a href="mailto:lrpalmer@gmail.com">lrpalmer@gmail.com</a>&gt;</span> wrote:<br>
<blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">I am not totally sure if I understand your proposal correctly, but if<br>
I do, then it has a flaw.  Consider:<br>
<br>
    class Boolable a where<br>
        boolify :: a -&gt; Bool<br>
<div class="im"><br>
    class O a where<br>
        o :: a<br>
<br>
</div>    main = print $ boolify o<br>
<br>
It seems like under your proposal this should not be a type error.<br>
But if that is so, then what is its output?<br>
<br>
Luke<br>
<div><div></div><div class="h5"><br>
On Thu, Sep 16, 2010 at 7:31 AM, Carlos Camarao<br>
&lt;<a href="mailto:carlos.camarao@gmail.com">carlos.camarao@gmail.com</a>&gt; wrote:<br>
&gt; Hi. Consider for example an expression e0 like:<br>
&gt;<br>
&gt;   fst (True,e)<br>
&gt;<br>
&gt; where e is any expression.<br>
&gt;<br>
&gt; e0 should have type Bool IMHO irrespectively of the type of e. In Haskell<br>
&gt; this is the case if e&#39;s type is monomorphic, or polymorphic, or<br>
&gt; constrained and there is a default in the current module that removes<br>
&gt; the constraints. However, e0 is not type-correct if e has a<br>
&gt; constrained type and the constraints are not subject to<br>
&gt; defaulting. For example:<br>
&gt;<br>
&gt;   class O a where o::a<br>
&gt;   main = print $ fst(True,o)<br>
&gt;<br>
&gt; generates a type error; in GHC:<br>
&gt;<br>
&gt;   Ambiguous type variable `a&#39; in the constraint:<br>
&gt;      `O a&#39; arising from a use of `o&#39; at ...<br>
&gt;     Probable fix: add a type signature that fixes these type variable(s)<br>
&gt;<br>
&gt; A solution (that avoids type signatures) can be given as follows.<br>
&gt;<br>
&gt; The type of f e, for f of type, say, K=&gt;t&#39;-&gt;t and e of type K&#39;=&gt; t&#39;<br>
&gt; should be:<br>
&gt;<br>
&gt;       K  +_t   K&#39; =&gt; t      (not K U K&#39; =&gt; t)<br>
&gt;<br>
&gt; where K  +_t  K&#39;  denotes the constraint-set obtained by adding from K&#39;<br>
&gt; only constraints with type variables reachable from t.<br>
&gt;<br>
&gt; (A type variable is reachable if it appears in the same constraint as<br>
&gt; either a type variable free in the type, or another reachable type<br>
&gt; variable.)<br>
&gt;<br>
&gt; Comments? Does that need and deserve a proposal?<br>
&gt;<br>
&gt; Cheers,<br>
&gt;<br>
&gt; Carlos<br>
&gt;<br>
</div></div>&gt; _______________________________________________<br>
&gt; Haskell-Cafe mailing list<br>
&gt; <a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
&gt; <a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
&gt;<br>
&gt;<br>
</blockquote></div><br>