Is it possible to decide $\beta$-equivalence within System F (or another normalizing typed λ-calculus)? I know that's impossible to decide $\beta$-equivalence for untyped lambda calculus. Quoting Barendregt, H. P. The Lambda Calculus: Its Syntax and Semantics. North Holland, Amsterdam (1984).:


  If A and B are disjoint, nonempty sets of lambda terms which are closed under equality, then A and B are recursively inseparable. It follows that if A is a nontrivial set of lambda terms closed under equality, then A is not recursive. So, we cannot decide the problem "M=x?" for any particular M. Also, it follows that Lambda has no recursive models.


If we have a normalizing system, such as System F, then we can decide $\beta$-equivalence "from outside" by reducing the two given terms and comparing if their normal forms are the same or not. However, can we do it "from inside"? Is there a System-F combinator $E$ such that for two combinators $M$ and $N$ we have $E M N = \mbox{true}$ if $M$ and $N$ have the same normal form, and $E M N = \mbox{false}$ otherwise? Or can this be done at least for some $M$s? To construct a combinator $E_M$ such that $E_M N$ is true iff $N\equiv_\beta M$? If not, why?
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.