...

...

data Any = forall a. Any a

get :: Any -> Maybe Char get (Any (c::Char)) = Just c -- bad get _ = Nothing .. It can also be questioned from a software engineering standpoint. Much of the purpose with existential types is to provide information hiding; that is, the user of an existentially quantified type is not supposed to know its concrete representation. The merits of an information hiding dicipline is probably no news to anybody on this list.

This discussion reminds me of an old paper by MacQueen: David MacQueen. Using dependent types to express modular structure. In Proc. 13th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 277--286, January 1986. He discusses some of the disadvantages of using plain existential quantification for modular programming purposes and proposes an alternative based on dependent sums, represented as pairing the witness type with the expression in which it is used, instead of existentials, where there is no witness for the existentially quantified type. See CiteSeer for some of the follow-on work that references MacQueen's paper: http://citeseer.nj.nec.com/context/32982/0 Some of that work tried to find a balance between having no witness types and carrying witness types around at runtime. In this context, Claudio Russo's work might be of interest, as he proposes to avoid the problems of existentials without going into (value-)dependent types: http://www.dcs.ed.ac.uk/home/cvr/ Claus