Рекурсивно определенные экземпляры и ограничения

Я экспериментировал с векторами и матрицами, размер которых закодирован в их типе, используя новое расширение DataKinds. В основном это выглядит так:

data Nat = Zero | Succ Nat

data Vector :: Nat -> * -> * where
    VNil :: Vector Zero a
    VCons :: a -> Vector n a -> Vector (Succ n) a

Теперь нам нужны типичные экземпляры, такие как Functorи Applicative. Functorпрост:

instance Functor (Vector n) where
    fmap f VNil = VNil
    fmap f (VCons a v) = VCons (f a) (fmap f v)

Но с экземпляром Applicativeвозникает проблема: мы не знаем, какой тип возвращать в чистом виде. Однако мы можем определить экземпляр индуктивно по размеру вектора:

instance Applicative (Vector Zero) where
    pure = const VNil
    VNil <*> VNil = VNil

instance Applicative (Vector n) => Applicative (Vector (Succ n)) where
    pure a = VCons a (pure a)
    VCons f fv <*> VCons a v = VCons (f a) (fv <*> v)

Однако, несмотря на то, что этот экземпляр применим ко всем векторам, средство проверки типов не знает об этом, поэтому мы должны нести Applicative] ограничение каждый раз, когда мы используем экземпляр.

Теперь, если бы это применялось только к экземпляру Applicative, это не было бы проблемой, но оказывается, что трюк с рекурсивными объявлениями экземпляров необходим при программировании с такими типами. Например, если мы определяем матрицу как вектор векторов-строк с помощью библиотеки TypeCompose,

type Matrix nx ny a = (Vector nx :. Vector ny) a

мы должны определить класс типов и добавить объявления рекурсивных экземпляров для реализации как транспонирования, так и умножения матриц. Это приводит к огромному количеству ограничений, которые мы должны использовать каждый раз, когда используем код, даже несмотря на то, что экземпляры фактически применяются ко всем векторам и матрицам (что делает ограничения бесполезными).

Есть ли способ избежать необходимости носить с собой все эти ограничения? Можно ли расширить средство проверки типов, чтобы оно могло обнаруживать такие индуктивные конструкции?