On Sun, Sep 16, 2012 at 11:49 AM, Simon Peyton-Jones <simo...@microsoft.com> wrote: > I don't really want to eagerly eta-expand every type variable, because (a) > we'll bloat the constraints and (b) we might get silly error messages. For > (b) consider the insoluble constraint > [W] a~b > where a and b are both skolems of kind '(k1,k2). If we eta-expand both we'll > get two insoluble constraints (Fst a ~ Fst b) and (Snd a ~ Snd b), and we > DEFINITELY don't want to report that as a type error!
I almost forgot to mention this, but... You should perhaps talk to the agda implementors. They've done a lot of work to avoid eta expanding as much as possible, because it was killing performance (but it does also make for some nicer display). So they probably know some tricks. -- Dan _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
