What is the difference between being "short-circuiting" and being "lazy on the its second argument" for a binary function?

In the Examples section of foldr's documentation, I read that

Infinite structures

⚠️ Applying foldr to infinite structures usually doesn't terminate.

It may still terminate under one of the following conditions:

• the folding function is short-circuiting
• the folding function is lazy on its second argument

Short-circuiting

(||) short-circuits on True values, so the following terminates because there is a True value finitely far from the left side:

>>> foldr (||) False (True : repeat False)
True

But the following doesn't terminate:

>>> foldr (||) False (repeat False ++ [True])
* Hangs forever *

Laziness in the second argument

Applying foldr to infinite structures terminates when the operator is lazy in its second argument (the initial accumulator is never used in this case, and so could be left undefined, but [] is more clear):

>>> take 5 $ foldr (\i acc -> i : fmap (+3) acc) [] (repeat 1)
[1,4,7,10,13]

The folding function in the first example is (||), whereas in the second example it is (\i acc -> i : fmap (+3) acc), so the former is supposed to be an example of a short-circuiting function, and the latter of a function lazy on its second argument, however, the source code for (||) and its documentation is below, and it clearly calls (||) lazy in the second argument, not short-circuiting.

-- | Boolean \"or\", lazy in the second argument
(||)                    :: Bool -> Bool -> Bool
True  || _              =  True
False || x              =  x

Incidentally, the documentation seem to be erroneously suggesting using [] instead of undefined as the accumulator for foldr on an infinite list. Isn't that a bad suggestion? Shouldn't we use undefined precisely to blow up in case one mistakely passes a finite list to our function?

I don't know the exact definitions that were intended by whoever wrote the docs, but in my mind "short-circuiting" is just a special case of "lazy on the second argument".

Perhaps some (admittedly hand-wavy) definitions could be made as follows:

A short-circuiting f is such that for at least some value x the result f x y is non-bottom and constant w.r.t. y. I.e., changing the value of y (including bottom) does not affect the result.

A lazy-on-the-second-argument f is such that for at least some value x the result f x y is non-bottom. The result can depend on y, but it has to be non-bottom in any case (including when y is bottom).

Examples:

• if x > 10 then y else [42] is short-circuiting.

• if x > 10 then 3:y else 4:y is lazy on y. (Not short-circuiting, though.)

• if x > 10 then 3:y else undefined can also be regarded as lazy on y.

Many variations on these definitions can be made, especially to account for the exact values of x (all? some? most?) that trigger the laziness.

The exact conditions for the termination of foldr are rather complex, especially when lazy functions are involved. I don't believe there is a simple criterion that fully characterizes termination. Even the docs you quoted say that laziness may lead to termination, but that is not a given.