I know I do not need these constraints, it was just the simplest way I found to explain the problem.<br><br>I have fought about that: I was not expecting F d c ~&nbsp; F a (c,a) not mean that F d ~F a /\ c ~(c,a), I thought the whole family was &quot;parameterized&quot;.<br>
If I encoded the family<br><br>type family F a x :: *<br><br>F d c ~&nbsp; F a (c,a) would be semantically different, meaning that this &quot;decomposition rule&quot; does not apply?<br><br>Thanks,<br>hugo<br><br><br><br><div class="gmail_quote">
<br></div><br>