I recently had an idea to allow one to create types from values. This would have many uses in Haskell; e.g., it would be very nice to have a type of nxn matrices for n that are not necessarily statically determined. (It is easy to create a type of matrices and check that the sizes are compatible at run time; the point is to do more checks at compile time.) Of course, one has to be careful to preserve decidability of type checking. The idea is to provide a function that returns an element of an undetermined (existential) type: class Singleton a b where singletonValue :: b -> a singleton :: forall a . a -> (exists b . (Singleton a b) => b) singleton returns a token of some new type; this token can then be passed around, stored in data structures, etc., to guarantee type consistency. I have no idea what existential types would do to the Haskell type system; is there a way to add them to preserve decidability, etc, etc? They would clearly make some simple program transformations illegal: for the idea to be useful, the type of (a,a) where a = singleton 5 should be of type exists a . (Singleton Int a) => (a, a) while the type of (singleton 5, singleton 5) has to be ((exists a . (Singleton Int a) => a), (exists b . (Singleton Int b) => b)) for decidability. Are there any pointers to previous work I should look at? Thanks, Dylan Thurston