Is shadowing of the type variable allowed in System F second order abstraction?

I'm reading Type Theory and Formal Proof by Nederpelt and Geuvers. Chapter 3 is about $\lambda 2$ and $\Pi$-Types (aka System F, I think?) and the derivation rule for 2nd order abstraction seems to forbid "shadowing" of the type variable; i.e. in context $\Gamma \equiv \alpha : $ it is not possible to derive a term of type $\Pi \alpha : . \alpha \rightarrow \alpha$. This is because the premise of $abst_2$ in Figure 3.1 page 76 has context $\Gamma, \alpha : $ and definition 3.4.4 of $\lambda 2$ context at page 75 explicitly says that $\Gamma, \alpha : \equiv \alpha : , \alpha : $ wouldn't be a valid context. First obvious question is: did I understand correctly? If yes, then the second question is why? Even in C++ I can do it...
struct alpha {};

template
alpha id(alpha x) { return x; }

Edit

I just realised that someone who doesn't have the book might struggle to follow my question. So here's more context. The derivation rule for 2nd order abstraction says:

$$
\frac
{\Gamma, \alpha : * \vdash M : \sigma}
{\Gamma \vdash \lambda \alpha : . M : \Pi \alpha : . \sigma};
$$

a valid $\lambda 2$ context is also recursively defined as:

• the empty context $\emptyset$ with an empty domain, i.e. $\texttt{dom}(\emptyset)=()$;

• if $\Gamma$ is a valid context, and $\alpha$ is a type variable (i.e $\alpha \in \mathbb{V}$) such that $\alpha \notin \texttt{dom($\Gamma$)}$, then $\Gamma, \alpha : $ is a valid context with $\texttt{dom}(\Gamma, \alpha : ) = (\texttt{dom}(\Gamma), \alpha)$;

• if $\Gamma$ is a valid context, $\rho$ is a type (i.e. $\rho \in \mathbb{T}$) such that $\alpha \in \texttt{dom}(\Gamma)$ for all free type variables $\alpha$ occurring in $\rho$, and if $x \notin \texttt{dom}(\Gamma)$, then $\Gamma, x: \rho$ is a valid context with $\texttt{dom}(\Gamma, x: \rho) = (\texttt{dom}(\Gamma), x)$.

So if my goal is to derive some $M : \Pi \alpha : . \sigma$ and my current context is $\Gamma \equiv \alpha : $ then the premise of the 2nd order

Just because two variables have the same name doesn't mean they're the same variable. Shadowing happens when two variables have the same name in overlapping contexts. It's potentially confusing so we try to avoid that. Fortunately, given a term with shadowing, we can always construct an alpha-equivalent term that has no shadowing. Except when studying variable binding itself, we only ever study terms up to alpha equivalence.

Clearly $\Pi \alpha : \ast. \alpha \rightarrow \alpha =_\alpha \Pi \beta : \ast. \beta \rightarrow \beta $ so I can change my problem to search for an alpha-equivalent term and now I can do it, but this feels like a hack.

It's not a hack, it's the normal thing to do. Systematically renaming variables (i.e. performing an alpha conversion) so that no shadowing occurs is called the (weak) Barendregt convention. In fact, the true Barendregt convention (from Barendregt's treatise on the lambda calculus) is a bit stronger: in a given term, you never use the same name for two different variables (even with non-overlapping contexts such as $(\lambda x. x)(\lambda x. x)$, which does not obey the strong Barendregt convention).

See also Free variables as defined in TAPL seems wrong and Substitution lemma for types.

StackExchange Computer Science Q#159688, answer score: 3