<br><div class="gmail_quote"><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>
 &nbsp; type S a b = a<br>
 &nbsp; type family F a :: * -&gt; *<br>
 &nbsp; type instance F a = S a<br>
<br>
Why do we need to forbid this type instance? &nbsp;Because it breaks the<br>
confluence of equality constraint normalisation. &nbsp;Here are two<br>
diverging normalisations:<br>
<br>
 &nbsp; (1)<br>
<br>
 &nbsp; &nbsp; F Int Bool &nbsp;~ &nbsp;F Int Char<br>
<br>
 &nbsp; ==&gt; DECOMP<br>
<br>
 &nbsp; &nbsp; F Int ~ F Int, Bool ~ Char<br>
<br>
 &nbsp; ==&gt; FAIL<br>
<br>
<br>
 &nbsp; (2)<br>
<br>
 &nbsp; &nbsp; F Int Bool &nbsp;~ &nbsp;F Int Char<br>
<br>
 &nbsp; ==&gt; TOP<br>
<br>
 &nbsp; &nbsp; S Int Bool &nbsp;~ &nbsp;S Int Char<br>
<br>
 &nbsp; ==&gt; (expand type synonym)<br>
<br>
 &nbsp; &nbsp; Int &nbsp;~ &nbsp;Int<br>
<br>
 &nbsp; ==&gt; TRIVIAL<br>
<br></blockquote><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&#39;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>