Sorry, I meant<br><br>type FList a x = Either One (a,x)<br>type instance F [a] = FList a<br><br><div class="gmail_quote">On Thu, Mar 27, 2008 at 4:45 PM, Hugo Pacheco <<a href="mailto:hpacheco@gmail.com">hpacheco@gmail.com</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;"><br><div class="gmail_quote"><div class="Ih2E3d"><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<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></blockquote></div><div>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 more of the parameters? If so, this could be checked...<br>
<br>hugo<br></div></div><br>
</blockquote></div><br>