If a lambda is declared inside a default argument, is it different for each call site?

#include <iostream>

int foo(int x = [](){ static int x = 0; return ++x; }()) {
    return x;
};

int main() {
    std::cout << foo() << foo(); // prints "12", not "11"
}

I know that default arguments are evaluated each time a function is called. Does that mean that the lambda type is different on each call? Please point to the standard quotes explaining the behaviour here.

This all comes down to the interpretation of [expr.prim.lambda.closure]/1:

The type of a lambda-expression (which is also the type of the closure object) is a unique, unnamed non-union class type, called the closure type, whose properties are described below.

What does "unique" mean?

"The type of a lambda-expression... is... unique..."

The first word is "the". The type. Implying that a lambda-expression has one type. But since it's "unique", that means that any two lambda-expressions have different types.

The word "lambda-expression" is italicized, denoting a grammar term. A lambda appearing lexically once, but evaluated more than once, is the same lambda-expression on each evaluation. So it has the same type in each evaluation.

The fact that a default argument is evaluated every time a function is called does not mean that the program behaves as if the default argument were repeated verbatim at each call site. A default argument is a piece of code that runs whenever it's used, just like a function body.

Note, however, that instantiating a template does stamp out a copy of each grammar production that occurs in the template definition (though, for name lookup purposes, it's not the same as "replaying the tokens" at the instantiation point). In other words, if you have a lambda-expression inside a template and you instantiate that template, the resulting specialization has its own lambda-expression that is the result of instantiating the one from the template. Thus, each specialization gets a distinct type for the lambda, even though those lambdas were all defined by the same original piece of source code.

There are also cases where two lambdas appearing in different translation units actually have the same type. This occurs because there is a rule that can force multiple identical pieces of source code from different translation units to behave as if only one copy in the program. [basic.def.odr]/17