Hi, I've just looked through this discussion, since I'm working on my own library, I wanted to see what people are doing. It's something like this, using the Prepose (Implicit Configurations) paper: data L n = L Int deriving (Show, Eq, Ord) -- singleton domain type S = L Zero class (Bounded a, Ix a) => IxB a instance ReflectNum n => Bounded (L n) where minBound = L 0 maxBound = L $ reflectNum (__ :: n) - 1 mul :: (Num k, IxB a, IxB b, IxB c) => Matrix k a b -> Matrix k b c -> Matrix k a c add :: (Num k, IxB a, IxB b) => Matrix k a b -> Matrix k a b -> Matrix k a b vec :: (Num k, IxB a, IxB b) => Matrix k a b -> Matrix k (a,b) S This way one can form a type "L n" which represents integers between 0 inclusive and n (rather, 'reflectNum (__ :: n)') exclusive, which can serve to index the matrices and vectors... Of course, other index types are allowed, such as "Either a b" - if we want to, say, take the sum of two vector spaces, one indexed by "a" and the other by "b", then the result should be indexed by "Either a b", etc. - we never have to do anything with the type-level numerals other than assert equality, i.e. we don't have to be able to add or multiply them in our type-signatures, since structural operations will suffice. I think having the ability to guarantee through the type system that column and row dimensions are correct is of paramount importance to those who would use a matrix library, but so far in this thread I haven't seen any suggestions which would accomplish that. I'm sorry if I didn't read carefully. Does my approach not work? I haven't filled in the implementation yet, but it type-checks. Frederik