Re: Types from values using existential types?

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. ..... Are there any pointers to previous work I should look at?

If type systems for matrices are of interest for you then I think you should check out Barray Jay's work on the language FiSH. Björn Lisper