[Haskell-cafe] Extensionality principles for kinds?

[Rob]

On 11/08/2014 07:30 PM, Richard Eisenberg wrote:
> The problem is that GHC doesn't do eta expansion for product types. See #7259, which won't be fixed by 7.10, as I would imagine a fair amount of theory needs to be done for this to be valid.
>
> Luckily, you can do eta expansion manually yourself: either by requiring that the caller know the eta-expanded form (1) or by storing that knowledge in a GADT (2):
I was afraid that would be the answer.  Unfortunately, I think I really 
need the non-eta-expanded form, because either of the eta forms you 
suggest break other things.  The problem is that Twice and Dbl occur in 
some definitions that go by polymorphic recursion, an the eta-expanded 
forms don't seem to work.

I'll see if I can get by without this...

Cheers,
   Rob