Yes, GHC will rewrite this to
force x = x
I'm also not sure if we really want "seq" in all of these cases, or if we want stronger guarantees. For example, GHC can (and often will) rewrite
f x y = x `seq` y `seq` x
to
f x y = y `seq` x
This changes the order of evaluation. For pure computations this is semantically sound. However, it can change the space behaviour of the program, which defeats the point of using "seq" in the first place (usually). If forcing "x" to be evaluated before "y" is the goal, then "pseq" must be used. I think it's worthwhile to consider introducing high-level combinators for this use case as well.