Eta expansion in the pattern lambda calculus Klop, van Oostrom, and de Vrijer have a paper on the lambda calculus with patterns.

http://www.sciencedirect.com/science/article/pii/S0304397508000571

In some sense, a pattern is a tree of variables -- though I am just thinking of it as a nested tuple of variables, for example, ((x,y),z),(t,s)).

In the paper they showed that if the patterns are linear, in the sense that no variable in a pattern is repeated, then the rule

(\p . m) n = m [n/p]


where p is a variable pattern and n is a tuple of terms with the exact same shape as p, is confluent.

I am curious if there are similar developments in the literature for the lambda calculus with patterns and the additional eta rule (expansion, reduction, or just equality).

In particular, by eta, I mean 

m = \lambda p . m p


More directly, I am curious what properties such a lambda calculus would have.  For example, is it confluent?

It forces the classifying category to be closed because it forces the property that

m p = n p implies m = n 


By using the \xi-rule in between.  But perhaps something could go wrong?
This is not a complete answer; it is a comment that got too large.

If you extend typed lambda calculus with products with projective eliminators (ie, product eliminators fst(e) and snd(e)), there are no basically issues whatsoever. The reason it took so long to figure out is because it turns out to be more natural to do eta expansions rather than eta reductions.  See Barry Jay's The Virtues of Eta Expansion.

If you want products to have a pattern-style eliminator 

let (a,b) = e in t 


Then matters are more complex. The primary difficulty with pattern matching are the commuting conversions. That is, these calculi have the equation 

C[let (a,b) = e in t] === let (a,b) = e in C[t]


and figuring out (a)  which context C[-] to use and (b) how to orient this equation gets tricky. IMO, the state of the art for rewriting-style approaches are Sam Lindley's  Extensional Rewriting with Sums and Gabriel Scherer's Deciding Equivalence with Sums and the Empty Type, both of which consider the typed lambda calculus with both products and sums.