Patterns and Existentials

I am reading papers again and this always activates my creative fantasy. I want to explain a small revelation I had just now.

Patterns are the same thing as declaring existential values corresponding to all pattern variables according to their respective types as stated in their respective constructors and asserting that the pattern interpreted as a value is the same as the scrutinee.

The body behind the pattern in turn is similarly evaluated with the existential variables in scope. Of course the existential values are filled in by some oracle which is uninteresting from the typing perspective. A strong corollary of the asserted value identity is that we can also assert that the type of the scrutinee unifies with the type of the pattern-value (in the scope of the existentials, but not outside of it)!

Just as universally quantified values are typed by dependent products (∏-stuff) the existentially quantified values are typed by dependent sums (∑-stuff). Note that the stuff is at stratum 1, e.g. types. This is in contrast to the Haskell data declaration

data Foo = forall a . Foo a

where a is at stratum 1, being an existential type.

Hmm, when thinking this to the end we may either end up at the conventional non-inference for GADTs or something like the generalized existentials as proposed in Chuan-kai Lin's thesis.

I conjecture also that this is the same thing as the post-facto type inference I suggested here.

Now all remains to is to reinterpret function calls as a data type being a tuple with existential values and to apply the above trick.