Why do we need a separate notation for П-types?
I think we just need to get some things straight here:

In the expression $\lambda a : \mathsf{type} . \lambda x : a . x$ the variable $a$ is bound (by the outer $\lambda$). The expressions $\lambda a : \mathsf{type} . \lambda x : a . x$ and $\lambda b : \mathsf{type} . \lambda x : b . x$ are $\alpha$-equal.
The expression $\lambda a : \mathsf{type} . \lambda x : a . x$ is the identity function, it is not the &quot;signature of the identity function&quot;.
If by &quot;signature of the identity function&quot; you mean to say &quot;the type of the identity function&quot;, then it would be something like $\Pi_{a : \mathsf{type}} . (a \to a)$, or if you want only product types, then it is $\Pi_{a : \mathsf{type}} \Pi_{x : a} a$.

Is there still a question?
Maybe this will help:

the type of the identity function $\lambda x : a . x$ is $a \to a$
the type of the identity function $\lambda y : b . y$ is $b \to b$
the functions $\lambda x : a . x$ and $\lambda y : b . y$ are different
the types $a \to a$ and $b \to b$ are different
the type of the polymorphic identity function $\lambda c : \mathsf{type} . \lambda z : c . z$ is $\Pi_{c : \mathsf{type}} . c \to c$.
the functions $\lambda a : \mathsf{type} . \lambda x : a . x$ and $\lambda c : \mathsf{type} . \lambda z : c . z$ are $\alpha$-equal
the types $\Pi_{a : \mathsf{type}} . a \to a$ and $\Pi_{c : \mathsf{type}} . c \to c$ are $\alpha$-equal.

Supplemental: After talking to Alex Simpson over a cup of tea, there is one more thing I can say. We don't need separate $\lambda$ and $\Pi$ constructors, as they both have precisely the same syntactic shape (take two arguments, bind one variable). In fact, if my memory serves me right, Automath used the same notation for $\lambda$-abstractions and $\Pi$-types. But the point is that we want to use two different constructors because they denote different concepts.