Emulate "static dependent types" in Haskell (if needed, with GHC extensions)

Assume that I have a type class Vec that implements the theory of, say, vector spaces over the rationals.

class Vec a where
    (+)  :: a -> a -> a
    zero :: a
    -- rest omitted

Now given a natural number n, I can easily construct an instance of Vec whose underlying type is the type of lists of rationals and which implements a vector space of dimension n. We take n = 3 in the following:

newtype RatList3 = RatList3 { list3 :: [Rational] }
instance Vec RatList3 where
    v + w = RatList3 (zipWith (Prelude.+) (list3 v) (list3 w))
    zero  = RatList3 (take 3 (repeat 0))
开发者_C百科

For another natural number, for example a calculated one, I can write

f :: Int -> Int
f x = x * x -- some complicated function
n :: Int
n = f 2
newtype RatListN = RatListN { listN :: [Rational] }
instance Vec RatListN where
    v + w = RatListN (zipWith (Prelude.+) (listN v) (listN w))
    zero  = RatListN (take n (repeat 0))

Now I have two types, one for vector spaces of dimension 3 and one for vector spaces of dimension n. However, if I want to put my instance declaration of the form instance Vec RatList? in a module where I don't know which n my main program eventually uses, I have a problem as the type RatList? doesn't know which n it belongs to.

To solve the problem, I tried to do something along the following lines:

class HasDim a where
    dim      :: Int

instance (HasDim a, Fractional a) => Vec [a] where
    v + w = ...
    zero  = take dim (repeat (fromRational 0))

-- in the main module
instance HasDim Rational where
    dim = n -- some integer

This doesn't work, of course, because dim in HasDim is independent of the type variable a and in instance (HasDim a) => Vec [a] it is not clear which type's dim to take. I tried to circumvent the first problem by introducing another type:

newtype Dim a = Dim { idim :: Int }

Then I can write

class HasDim a where
    dim      :: Dim a

However, it is not clear to me how to use this in instance (HasDim a) => Vec [a] where. Also my whole "solution" looks rather cumbersome to me, while the posed problem looks simple. (I think it is easy to code this with C++ templates.)

EDIT

I have excepted ephemient's answer because without the type arithmetic it solved my problem the way I wanted to. Just for information, my final solution is along the following lines:

class Vec a where
    zero :: a
    -- ...

n :: Int
n = 10

newtype RatListN = RatListN [Rational]

instance Vec RatListN where
    zero = RatListN . take n $ repeat 0
    -- ...

---

This seems like a case where type arithmetic would get you some of what you want.

data Zero
data Succ a
type One = Succ Zero
type Two = Succ One
type Three = Succ Two
-- ...

class NumericType a where
    toNum :: (Num b) => a -> b
instance NumericType Zero where
    toNum = const 0
instance (NumericType a) => NumericType (Succ a) where
    toNum (Succ a) = toNum a + 1

data RatList a b = RatList { list :: [b] }
instance (NumericType a, Num b) => Vec (RatList a b) where
    zero = RatList . take (toNum (undefined :: a)) $ repeat 0

Now RatList Two Int and RatList Three Int are different types. On the other hand, this does prevent you from instantiating new dimensionalities at runtime…