| In the same paper is the case-eta-expansion, but I don't understand | the correctness of this transformation: | | case e of {p1 -> e1,...,pn -> en} | ===> \y -> case e of {p1 -> e1 y, ..., pn -> en y} | | The rhs is a WHNF, but the lhs isn't, so the rule | can't be correct in general. For example, assume that e is bot.

Right. It's only done if 'e' is cheap (a variable, or something like that).

Actually, looking at the code, we also do it if 'e' is known to be bottom: CoreUtils.exprIsCheap returns True for known-divergent expressions. Which seems wrong for eta expansion, no? It's probably the case that if we have 'case _|_ of ...' then the simplifier will already have turned it into _|_, so it won't crop up. But it still looks wrong, unless I'm missing something? Cheers, Simon