deniok

(\x y -> x) undefined таки не является WHNF, в ней происходит вычисление при форсировании seq'ом, то есть она превращается при этом в \y -> undefined. Но никаких других вычислений, кроме связывания x с undefined не выполняется, потому что результат связывания спрятан за барьером лямбда абстракции, а там вычисления не происходят, так как это уже WHNF.

Мне казалось по глупости, что если что-то не находится в WHNF, то всегда можно исхитриться и вклеить в процесс редукции к WHNF расходимость.