I have come to realize that irrefutable pattern matching of existentials may indeed be problematic. Let us consider the following existential data type
data FE = forall a. Typeable a => Foo a | forall a. Typeable a => Bar a
The following tests type and run (the latter raising the expected exception).
test1 = case (Foo ()) of Foo x -> show $ typeOf x test2 = case (Bar True) of Foo x -> show $ typeOf x
Let us suppose that irrefutable pattern matching of existentials is allowed. What would be the value of the expression case (Bar True) of ~(Foo x) -> show $ typeOf x then? Hopefully not "Bool". One might say that the expression ought to bottom out. However, what reason one may give for that outcome? The only binding in the above expression is of 'x', whose value is never demanded. Indeed, "show $ typeOf (undefined :: ())" yields the non-bottom value "()". One may claim that the existential pattern match also binds an implicit dictionary argument, which is demanded above. That explanation is quite unsatisfactory, because it breaks the abstraction of type classes. The dictionary passing is merely an _implementation technique_ for type classes. Furthermore, it is not the only implementation technique: JHC and Chameleon, for example, use intensional type analysis to implement typeclasses. On a different note, Conor McBride wrote:
It isn't necessary to perform constructor discrimination when it's statically known that exactly one constructor is possible, so those patterns can always be made irrefutable, with matching replaced by projection.
that is, in essence, the idea behind `Tagless Staged Interpreters for Typed Languages' Pasalic, Taha, Sheard: ICFP02 It is well-written paper, with an excellent introduction and motivation. Incidentally, one can write their tagless staged interpreter in Haskell as it is. No dependent types are necessary.