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.
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 if two expressions are equivalent-up-to-⊥. and both non-⊥ then they are equivalent.
(Or, y'know, work in Idris with --total and avoid this problem entirely).
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 if two expressions are equivalent-up-to-⊥. and both non-⊥ then they are equivalent.
(Or, y'know, work in Idris with --total and avoid this problem entirely).