[Haskell-cafe] Pattern matching with singletons

[Paul Brauner]

Very helpful, thanks! I may come back with more singleton/type families
questions :)


On Tue, Mar 26, 2013 at 6:41 PM, Richard Eisenberg <eir at cis.upenn.edu>wrote:

> Hello Paul,
>
> > ----- Forwarded message from Paul Brauner <polux2001 at 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20130327/4907fbe7/attachment.htm>