Hello Paul,

> ----- Forwarded message from Paul Brauner <polux2001@gmail.com> -----

<snip>

>   - is a ~ ('CC ('Left 'CA)) a consequence of the definitions of SCC,

>   SLeft, ... (in which case GHC could infer it but for some reason can't)

>   - or are these pattern + definitions not sufficient to prove that a

>   ~ ('CC ('Left 'CA)) no matter what?

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.

I'm glad you're finding use in the singletons package! Let me know if I can be of further help.

Richard