x `seq` x === x and so x = x `seq` x === x = x but, in general, x = x `seq` foo =/= x = foo consider x = x `seq` ((1:) x) x = x `seq` ((1:) (x `seq` ((1:) x))) x = x `seq` ((1:) (x `seq` ((1:) (x `seq` ((1:) x))))) .. ignoring evaluation order, partially unrolling/substituting x also unrolls/substitutes applications of seq (in proper call-by-need, we couldn't even do the substitution until after the evaluation, so we'd never get this far). no part of the right-hand side is defined unless x is - that is what seq is about, isn't it? i do like the argument about different fixpoints - does that correspond to inductive vs coinductive definitions which are so often mixed in haskell? when working with cyclic structures, we often are quite happy without a base case. so instead of the inductive f 0 = True f n = f (n-1) -- provided that (f (n-1)) is defined, (f n) is defined we have things like nats = 1:map (+1) nats -- nats is partially defined if we just assume that nats is partially defined and it is nice to have both available, if not all that well separated. whether we're talking co-recursion or recursion seems to depend entirely on whether the recursive references are in a non-strict or strict context (so that the definitions are productive or not). so it seems to me that adding seq to a (co-)recursion is precisely about resolving this ambiguity and forcing induction nats = (1:) $! map (+1) nats -- nats is defined if we can prove that nats is defined, which we can't anymore and saying that we can get back to co-induction by eliding the seq may be correct, but irrelevant. and the same reasoning ought to apply to strict fields in data constructors. sorry for waving about precisely defined terms in such a naive manner. i hope it helps, and isn't too far of the mark!-) claus