Is it possible to decide $\beta$-equivalence within System F (or another normalizing typed λ-calculus)?
No, it's not possible. Consider the following two inhabitants of the type $(A \to B) \to (A \to B)$. 

$$
\begin{array}{l}
M = \lambda f.\;f \\
N = \lambda f.\;\lambda a.\; f\;a
\end{array}
$$

These are distinct $\beta$-normal forms, but cannot be distinguished by a lambda-term, since $N$ is an $\eta$-expansion of $M$, and $\eta$-expansion preserves observational equivalence in a pure typed lambda calculus. 

Cody asked what happens if we mod out by $\eta$-equivalence, also. The answer is still negative, because of parametricity. Consider the following two terms at the type $(\forall \alpha.\;\alpha \to \alpha) \to (\forall \alpha.\;\alpha \to \alpha)$:

$$
\begin{array}{lcl}
M &amp; = &amp; \lambda f:(\forall \alpha.\;\alpha \to \alpha).\;\Lambda \alpha.\lambda x:\alpha.\;f \;[\forall \alpha.\;\alpha \to \alpha]\;(\Lambda \beta.\lambda y:\beta.\;y)\;[\alpha]\;x\\
N &amp; = &amp; \lambda f:(\forall \alpha.\;\alpha \to \alpha).\;\Lambda \alpha.\lambda x:\alpha.\;f\;[\alpha]\;x
\end{array}
$$

They are distinct $\beta$-normal, $\eta$-long form, but are observationally equivalent. In fact, all functions of this type are equivalent, since $\forall \alpha.\;\alpha \to \alpha$ is the encoding of the unit type, and so all functions of the type $(\forall \alpha.\;\alpha \to \alpha) \to (\forall \alpha.\;\alpha \to \alpha)$ must be extensionally equivalent.