Typing dependent pattern matching

I'm curious on how to type a dependent pattern matching in a functional language. What should the rule for typing

match e with
| C_1 a_1_1 a_1_2 ... a_1_n1 -> e_1
| C_2 a_2_1 a_2_2 ... a_2_n1 -> e_2
| ...
| C_m a_m_1 a_m_2 ... a_m_nm -> e_m
end

be, where e is of type T, which has constructors C_i for each i.

I think that to prove that the pattern match has a type T', we need to prove
that each e_i has type T' under specific assumptions, but I can't quite pinpoint those assumption to add into the context.

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.

StackExchange Computer Science Q#51882, answer score: 6