This isn't about the state monad, it's about seq. "But now seq must distinguish ⊥ from λx → ⊥, so they cannot be equal. But they are eta-equivalent. We have lost eta equality!" - once you lose eta equality you lose everything. A whole raft of monads become impossible, not just state.<p>Equivalence in Haskell is defined only up to ⊥; to work in Haskell we rely on the "Fast and Loose Reasoning is Morally Correct" result that <i>if</i> two expressions are equivalent-up-to-⊥. and both non-⊥ then they are equivalent.<p>(Or, y'know, work in Idris with --total and avoid this problem entirely).