If you are interested, I wrote a thesis in 2007 on "object-oriented pattern matching" available at EPFL which "formalizes" pattern matching in Scala. It did not get into path-dependent types and does not have mechanized proofs, but has a discussion of optimizing translation to lower level code, exhaustiveness checks and user definable patterns (extractors). Like the author of the article, I found Maranget's matrix representation a great basis. This is because algebraic data types come in the form of "sum of products" (or enums with records) and once you have tested one level you want to expand the components of the tuple pattern (columns) and you deal with multiple cases (rows).

I won't claim my thesis is the most readable. I think I would do the presentation very differently today, but going back one's theis topic seems to be one of these impossible things in life if you don't work in academia.