Yes, but doesn't the confluence problem only occur for type synonyms that ignore one or more of the parameters? If so, this could be checked...<br><br><div class="gmail_quote">On Fri, Mar 28, 2008 at 12:04 AM, Manuel M T Chakravarty <<a href="mailto:chak@cse.unsw.edu.au">chak@cse.unsw.edu.au</a>> wrote:<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">Hugo Pacheco:<br>
<div class="Ih2E3d">> Sorry, I meant<br>
><br>
> type FList a x = Either One (a,x)<br>
> type instance F [a] = FList a<br>
<br>
</div>We should not allow such programs.<br>
<font color="#888888"><br>
Manuel<br>
</font><div><div></div><div class="Wj3C7c"><br>
><br>
><br>
> On Thu, Mar 27, 2008 at 4:45 PM, Hugo Pacheco <<a href="mailto:hpacheco@gmail.com">hpacheco@gmail.com</a>><br>
> wrote:<br>
><br>
><br>
> The current implementation is wrong, as it permits<br>
><br>
> type S a b = a<br>
> type family F a :: * -> *<br>
> type instance F a = S a<br>
><br>
> Why do we need to forbid this type instance? Because it breaks the<br>
> confluence of equality constraint normalisation. Here are two<br>
> diverging normalisations:<br>
><br>
> (1)<br>
><br>
> F Int Bool ~ F Int Char<br>
><br>
> ==> DECOMP<br>
><br>
> F Int ~ F Int, Bool ~ Char<br>
><br>
> ==> FAIL<br>
><br>
><br>
> (2)<br>
><br>
> F Int Bool ~ F Int Char<br>
><br>
> ==> TOP<br>
><br>
> S Int Bool ~ S Int Char<br>
><br>
> ==> (expand type synonym)<br>
><br>
> Int ~ Int<br>
><br>
> ==> TRIVIAL<br>
><br>
> This does mean that a program such as<br>
><br>
> type FList a = Either One ((,) a)<br>
> type instance F [a] = FList a<br>
><br>
> will be disallowed in further versions?<br>
> Doesn't this problem occur only for type synonyms that ignore one or<br>
> more of the parameters? If so, this could be checked...<br>
><br>
> hugo<br>
><br>
><br>
<br>
</div></div></blockquote></div><br>