Because lambdas syntactically do not allow annotations, type checkers have to infer parameter and return types for them, but that doesn't mean they "can't be type-checked". For example, given this program:

def f(lst: list[int]):
    reveal_type(list(map(lambda x: str(reveal_type(x)), lst)))

Pyright reveals int for the inner call and list[str] for the outer call, correctly.

However, in a lambda that is not passed as an argument or in a more complicated situation, type checkers may not be able to infer a type.

I don't think it makes sense to change the spec here; this seems more of a topic to discuss in user-facing documentation.

Building on what Jelle said, static typing does work with lambdas, and all lambdas are type checked. As with some other expression forms, there are cases where a type checker doesn't have sufficient information to infer types, so it will fall back on Any (or Unknown) to fill in the missing type information. Lambdas are not unique here.

For example, this program type checks with no errors (using default settings in pyright) thanks to gradual typing.

def x1(a, b): return a + b
x2 = lambda a, b: a + b
x3 = []

reveal_type(x1) # (a: Unknown, b: Unknown) -> Unknown
reveal_type(x2) # (a: Unknown, b: Unknown) -> Unknown
reveal_type(x3) # list[Unknown]

If you want to catch more potential errors statically, you can supply additional type information. In the case of a def statement, this can be done by adding explicit parameter type annotations. For a lambda, an empty list, and various other expressions whose types cannot be inferred without additional context, an explicit type declaration for the target variable can be added.

def x1(a: int, b: int) -> int: return a + b
x2: Callable[[int, int], int] = lambda a, b: a + b
x3: list[int] = []

reveal_type(x1) # (a: int, b: int) -> int
reveal_type(x2) # (a: int, b: int) -> int
reveal_type(x3) # list[int]

The typing spec doesn't dictate type inference behaviors for type checkers, but most type checkers support some form of bidirectional type inference to handle situations like this.

I agree this would make a good addition to the user-facing documentation. The Type System Guides would be a good place for this. Documentation contributions are always welcome!

However, in a lambda that is not passed as an argument or in a more complicated situation, type checkers may not be able to infer a type.

I don't think it makes sense to change the spec here; this seems more of a topic to discuss in user-facing documentation.

Yes, that is what I was suggesting - to explain it better and the suggestion made here:

agree this would make a good addition to the user-facing documentation. The Type System Guides would be a good place for this.

is a good one. It's examples like this that trip people up:

f1 = lambda a, b: a * b

f1([1, 2], [3, 4])

Unfortunately, a static type checker won't flag the call to f1 as incorrect, and I think this is where some of the confusion lies in that the lambda funcs are callables that by default have untyped arguments and untyped results, and for this kind of case, I'm not sure what you'd have to do to get the types right so that the * operator works when you expect it to, e.g., f1([1,2], 3) is valid, as is f1(3,4) and f1(3, [1,2]).

The recommendation that I give to people is if you want type checking in the lambda function, then you either need to convert it to a regular python function with typed arguments and return types, or declare it as a Callable as suggested above.