Re: [Haskell-cafe] What's the motivation for η rules?

David, Conor wrote:

But the news is not all bad. It is possible to add some eta-rules without breaking the Geuvers property (for functions it's ok; for pairs and unit it's ok if you make their patterns irrefutable).

Note that, in Haskell, for functions it's only ok if you leave seq and the like out of the equation: otherwise undefined and (\x. undefined x) can be told apart using seq. (That's a minor detail, though.) Cheers, Stefan