The Coq mailing list

[Andrew Cave <acave1 AT cs.mcgill.ca>]

On Tue, Aug 28, 2012 at 10:18 AM, Ryan Wisnesky 
<ryan AT cs.harvard.edu>
 wrote:
> In the simply typed case, one might like eta-conversion for functions, 
> products, and sums - three conversions in total.  In Coq 8.4, it looks like 
> we now have eta for functions, and you're working on eta for products, so 
> I'm wondering about the third conversion, eta for sums - is that possible 
> or even sensible?

There's two papers I know of on this topic:

Altenkirch et al. Normalization by evaluation for typed lambda
calculus with coproducts. LICS 2001.

Balat, Di Cosmo, and Fiore. Extensional normalisation and
type-directed partial evaluation for typed lambda calculus with sums.
POPL 2004.

So it's possible, but it strikes me as quite complex to implement.