Weak head normal form and order of evaluation

I've read lots on weak head normal form and seq. But I'm still have trouble imagining the logic behind Haskell's order of evaluation

A common example demonstrating when and how to use but I still don't understand how the common example

foldl (+) 0 [1..5000000]

can result in a stack overflow. While another fold definition using seq doesn't

foldl' _ a [] = a
foldl' f a (x:xs) = let a' = f a x in a' `seq` foldl' f a' xs
foldl' (+) 0 [0..5000000]

From explanations of seq that I've read, authors are very careful to make the following clear:

The first argument of seq is not guaranteed to be evaluated before the second argument
The first argument of seq will only be evaluated to weak head normal form
The evaluation of the first argument of seq will only happen when the second is evaluated to WHNF

So, if the above is correct (is it?) then why does foldl' not overflow like foldl?

When we reduce one step, shouldn't it looks like this, right?

foldl' (+) 0 (1:xs) = let a' = (+) 0 1 in a' `seq` foldl' (+) a' xs

In the above, the second argument of seq is not in WHNF since there is a function application which needs to be done. Are we guaranteed to evaluate the first argument of seq here before we reach the WHNF of the second argument?

The first argument of seq is not guaranteed to be evaluated before the second argument
Not guaranteed, but the compiler will try and usually do it if it prevents thunk buildup. The scenario where this doesn't work so well is parallelism, hence the need for pseq – but for foldl' that's not relevant.
The first argument of seq will only be evaluated to weak head normal form
Yeah, but for built-in number types WHNF = NF.
The evaluation of the first argument of seq will only happen when the second is evaluated to WHNF
Indeed, and that often causes confusion. But in a' `seq` foldl' f a' xs means, if you request any result at all it'll trigger the seq.
When we reduce one step, shouldn't it looks like this, right? ... the second argument of seq is not in WHNF
Precisely that's what forces the seq, because to evaluate the result of foldl' (+) 0 (1:xs) you need foldl' (+) a' xs to be WHNF, and seq ensures this won't happen before a' is WHNF.