Typing dependent pattern matching
In general matching with dependent types can be quite subtle! You'll note that in the Coq documentation that the extended pattern-matching syntax is

match t as x in T1 return T2 with
    | C1 a1 ... an
    ...


In particular, ommiting any of the as, in or return clauses can prevent type inference of the statement.

Intuitively, if the type of (say) constructor $C_1$ is
$$ \Pi(x_1:A_1)\ldots(x_k:A_k).I\ \vec{p}$$
and the type of the matched term $t$ is
$$ I\ \vec{v}$$
then you get the constraint
$$ \vec{p}[\vec{a}/\vec{x}]\simeq \vec{v}$$
which may lead to an undecidable problem, as explained in Goguen et al.

Then all you need is for each right hand side to correspond to the appropriate instance of the return type. This return type may depend on $t$, so the return clause specifies the pattern of the return type as a function of $x$ (which represents $t$ through the as clause).

More formally, each $e_i$ must have type:

$$ T_2[C_i\ \vec{a}/x]$$

and the type of the whole match expression is
$$ T_2[t/x]$$

More details can be found here.