Is eta-equivalence for functions compatiable with Haskell's seq operation?
First, let us be explicit about how seq distinguishes $\bot$ from $\lambda x . \bot$:

bottom :: a
bottom = bottom

eta :: a -&gt; b
eta x = bottom

-- This terminates
fortytwo = seq eta 42

-- This does not terminate
infinity = seq bottom 42


It is therefore an experimental fact that in Haskell $\bot$ and $\lambda x . \bot$ are operationally distinguishable. It is also a fact, and a quite obvious one, that seq is computable because Haskell computes it. So much about Haskell. You are asking about the very particular phrasing of the Haskell documentation. I read it as saying that seq is supposed to satisfy the two given equations, but those two equations are not sufficient for the definition of seq. Here is why: I can give you two models of (simply typed) $\lambda$-calculus in which seq is computable and satisfies the given equations, but in one of the models $\bot$ and $\lambda x . \bot$ agree, while in the other they do not.

In a simple domain-theoretic model where $\lambda$-expressions are interpreted in the domain of continuous functions $[D \to E]$ we have $\bot = \lambda x . \bot$, obviously. Take effective Scott domains or some such to make everything computable. It is easy to define seq in such a model.

We can also have a model of $\lambda$-calculus in which seq distinguishes $\bot$ and $\lambda x . \bot$, and then of course $\eta$-rule cannot hold. For instance, we can do this by interpreting functions in the domain $[D \to E]_\bot$, i.e., the function space domain with an extra bottom attached. Now $\bot$ is, well, the bottom of $[D \to E]_\bot$, while $\lambda x . \bot$ is the element just above it. They cannot be distinguished by application because they both evaluate to $\bot$, no matter what you apply them to (they are extensionally equal). But we do have seq as a map between domains and it alwyas distinguishes bottom from all other elements.