Is there a way to prove that the second snippet below inserts an invisible declaration `struct S;` just before the function declaration?

Question

The code below compiles (demo), which proves that the function declaration void f(struct S&);inserts an invisible declaration (struct S;) in global scope, just before the function declaration, otherwise the second declaration (extern S s;) would fail to compile.

void f(struct S&);
extern S s;

I'm pretty sure the second code below also includes an invisible declaration (struct S;) just before the function declaration, but I can't find a way to prove this. Any suggestion?

struct S{};  
void f(struct S&);

The invisible declarations referred to above are mentioned in the Note in [basic.scope.declarative]/4

Answer 1

I'm pretty sure the second code below also includes an invisible declaration (struct S;) just before the function declaration, but I can't find a way to prove this. Any suggestion?

struct S{};  
void f(struct S&);

It does not. [basic.lookup.elab] describes how we determine if an elaborated-type-specifier declares a new type or refers to an existing one:

If the elaborated-type-specifier is introduced by the class-key and this lookup does not find a previously declared type-name, or if the elaborated-type-specifier appears in a declaration with the form: class-key attribute-specifier-seq_opt identifier ; the elaborated-type-specifier is a declaration that introduces the class-name as described in [basic.scope.pdecl].

In this case, lookup does find a previously declared type-name S (that is, ::S), so there is no declaration.

Regardless though, whether or not it behaves as if it re-declares S isn't observable:

struct S { }; // #1
struct S;     // #2

There's no difference in the behavior of this program if #2 doesn't exist (outside of like... __LINE__, but in this case the declaration would be compiler-generated and so wouldn't affect that anyway).