In case of a C++ auto, type is specified explicitly - it is an RHS type of an assignment. Type is not deduced here, it is symply propagated.
Auto does not add anything new at all on top of the existing type checking: if for a specific LHS type a checker would normalise both left and right hand types and check for assignability, in case of auto it will assume LHS=RHS without checking anything.
Therefore auto is a subset of type propagation, not type inference.
In `7`. It's an `int` literal, so `x` has to be an `int`. C++ won't even do you the favor of accounting for the possibility that `x` might have some other type, say, `double`, to which an `int` can be coerced. As for why you would want C++ to infer a different type, consider `std::size_t n = 0;`.
The point is that this is not a type inference, it is a restricted form of a type propagation (i.e., a subset of the pre-auto C++ type propagation, not an extension of it).
Type of x is a very explicit literal type. Type of y is also fully explitit, it is a 'return type of f()'. Not any different from a type of a sub-expression.
The type of f() is explicitly specified somewhere outside the local context. The type of x is not explicitly specified anywhere. It is inferred from the rhs expression.
The type 'return type of f()' is still a type. It does not matter that it is not normalised, most of the C++ types are used in a non normal form. Type 'struct MyKewlMegaStructure' is not any different and not any more "local".
Ok. Then in 'struct _abc x;' we also have a type inference. And in any sub-expression there is also a "type inference".
Although I think this kind of twisting the common term definitions is totally pointless. "Type inference" got a very well defined meaning, which got nothing to do with any kind of a type propagation - the latter term also existing for a reason, to designate a certain sort of type systems, fundamentally different from the inference-based ones.
Then a lot of what people write on this subject seems to be using incorrect terminology, including tons of stuff issued by computer science departments and wikipedia.
After digging a little deeper into the history of this terminology I have to concede that you and catnaroek are right. There was from the beginning in the 1950s a distinction that I didn't know about. So I was wrong.
Auto does not add anything new at all on top of the existing type checking: if for a specific LHS type a checker would normalise both left and right hand types and check for assignability, in case of auto it will assume LHS=RHS without checking anything.
Therefore auto is a subset of type propagation, not type inference.