Very helpful, thanks! I may come back with more singleton/type families questions :)
On Tue, Mar 26, 2013 at 6:41 PM, Richard Eisenberg <e...@cis.upenn.edu>wrote: > 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