Types from values using existential types?

[Dylan Thurston]

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