Hello Paul,
> ----- Forwarded message from Paul Brauner <polux2...@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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
