It might be useful to quickly give the counter-example to CR in typed calculi with $\beta$ and $\eta$:
$$ t=\lambda x:A.(\lambda y:B.\ y)\ x$$
And we have
$$ t\rightarrow_\beta \lambda x: A.x$$
and
$$ t\rightarrow_\eta \lambda y:B.y$$
It is immediate that if $A\equiv B$, then the two resulting terms are, in fact, $\alpha$ equivalent, but there is no reason for this to be the case, on untyped terms.
On typed terms, it's pretty clear that $A$ has to be equal to $B$ for the resulting term $t$ to be well-typed. The big difficulty that occurs is this:
For dependently typed systems, confluence needs to be proven before type preservation!
This is because you need the property of $\Pi$-injectivity
$$ \Pi x:A.B=_{\beta\eta}\Pi x:A'.B'\ \Leftrightarrow\ A=_{\beta\eta}A'\wedge B=_{\beta\eta} B'$$
in order to prove inversion, which is required to prove preservation/subject reduction.
So you can't even prove that $\beta\eta$-reductions preserve types without confluence, but confluence doesn't even hold on untyped/ill-typed terms!
Breaking out of this vicious circle requires some technical tricks, which are hard to summarize here, but arguably the simplest to understand is to simply stop being interested in $\eta$-reductions, but instead concentrate on $\eta$-expansions: $t\rightarrow_{\eta*}\lambda x:A.t\ x$
Of course, you need to restrict this rule to non-$\lambda$ and non-applied terms to even hope to get termination, but with these restrictions it seems that the reduction behavior is much better behaved, and the meta-theory works out without too many problems. A good reference seems to be Neil Ghani, Eta-Expansions in Dependent Type Theory.
A different, and recently quite popular approach, is described by Abel, Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs.
