<div dir="ltr">Very helpful, thanks! I may come back with more singleton/type families questions :)</div><div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, Mar 26, 2013 at 6:41 PM, Richard Eisenberg <span dir="ltr"><<a href="mailto:eir@cis.upenn.edu" target="_blank">eir@cis.upenn.edu</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hello Paul,<br>
<br>
> ----- Forwarded message from Paul Brauner <<a href="mailto:polux2001@gmail.com">polux2001@gmail.com</a>> -----<br>
<br>
<snip><br>
<br>
> - is a ~ ('CC ('Left 'CA)) a consequence of the definitions of SCC,<br>
<div class="im">> SLeft, ... (in which case GHC could infer it but for some reason can't)<br>
</div>> - or are these pattern + definitions not sufficient to prove that a<br>
<div class="im">> ~ ('CC ('Left 'CA)) no matter what?<br>
<br>
</div>The first one. GHC can deduce that (a ~ ('CC ('Left b))), for some fresh variable (b :: TA), but it can't yet take the next step and decide that, because TA has only one constructor, b must in fact be 'CA. In type-theory lingo, this deduction is called eta-expansion. There have been on-and-off debates about how best to add this sort of eta-expansion into GHC, but all seem to agree that it's not totally straightforward. For example, see GHC bug #7259. There's a non-negligible chance I will be taking a closer look into this at some point, but not for a few months, so don't hold your breath. I'm not aware of anyone else currently focusing on this problem either, I'm afraid.<br>
<br>
I'm glad you're finding use in the singletons package! Let me know if I can be of further help.<br>
<span class="HOEnZb"><font color="#888888"><br>
Richard</font></span></blockquote></div><br></div>