PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
dan.doel at gmail.com
Thu Sep 20 01:24:52 CEST 2012
On Sun, Sep 16, 2012 at 11:49 AM, Simon Peyton-Jones
<simonpj at 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.
More information about the Glasgow-haskell-users