You are right about C#: The type of `x => x + 1` can't be said to be anything other than "inferred". I stand corrected. But I disagree with the rest of your po

You are right about C#: The type of `x => x + 1` can't be said to be anything other than "inferred". I stand corrected. But I disagree with the rest of your post. From the point of view of type inference, what matters is the nature of the type constraints that the type checking algorithm generates: (0) Traditional type checking: All type constraints are of the form “T1 = T2”, where both “T1” and “T2” are closed type expressions. There is nothing to infer. (1) Type propagation: All type constraints are of the form “X = T”, where “X” is a type variable and “T” is a closed type expression. Again, there is nothing to infer, but we might need to propagate “T” between places. Say, from the RHS to the LHS of a variable initialization. (2) Type inference: Type constraints are arbitrary type expressions, which must be solved using a unification algorithm. As for why type propagation doesn't count as type inference: http://lambda-the-ultimate.org/node/4771#comment-75771 http://lambda-the-ultimate.org/node/4771#comment-75771