$\lambda x. \lambda x.x$ vs $\lambda y. \lambda x.x$
You have basically discovered the Barendregt convention.

Yes, it's silly to write terms such as $\lambda x. \lambda x. x$ when $\lambda y. \lambda x. x$ is $\alpha$-equivalent and clearer.

We could forbid the former form the syntax of the lambda calculus. This however would force us to check $x$ does not occur bound in $M$ every time we craft (introduce) the term $\lambda x. M$.

The Barandregt convention goes further. It stipulates that, when building (introducing) a term $\lambda x. M$ we are always allowed to do that. However, when destructuring (eliminating) a term $\lambda x. M$ we can assume that $x$ was $\alpha$-converted so no to cope with other bound names in $M$, nor with other names that we could have around elsewhere at the moment: e.g., if we are writing a proof involving terms $N$ and $O$, the convention stipulates that $x$ does not occur in $N,O$ as well.

The convention is just a convenient shortcut, made for lazy humans which do not want to spend their time and energy to fix trivialities. Basically, we pretend that $\lambda x.\lambda x. M$ is allowed when it's convenient to do so (introduction), yet we pretend that the same is no longer allowed when convenient to do so (elimination).  It feels a bit like cheating, but one could (in theory) always fix the proof to be perfectly sound.