Связывание имени в подписи типа с использованием DataKind

Итак, я наконец нашел задачу, в которой я мог бы использовать новое расширение DataKinds(используя 7.4.1). Вот Vec, который я использую:

data Nat = Z | S Nat deriving (Eq, Show)

data Vec :: Nat -> * -> * where
    Nil :: Vec Z a
    Cons :: a -> Vec n a -> Vec (S n) a

Теперь для удобства я хотел реализовать fromList. В принципе, нет проблем с простой рекурсией/складкой, но я не могу понять, как придать ей правильный тип. Для справки, это версия Agda:

fromList : ∀ {a} {A : Set a} → (xs : List A) → Vec A (List.length xs)

Мой подход на Haskell с использованием синтаксиса, который я видел здесь:

fromList :: (ls :: [a]) -> Vec (length ls) a
fromList [] = Nil 
fromList (x:xs) = Cons x (fromList xs)

Это дает мне ошибку разбора на входе 'a'. Является ли синтаксис, который я нашел, правильным, или они изменили его? Я также добавил еще несколько расширений, которые находятся в коде по ссылке, что тоже не помогло (в настоящее время у меня есть GADT, DataKinds, KindSignatures, TypeOperators, TypeFamilies, UndecidableInstances).

Другое мое подозрение заключалось в том, что я просто не могу связать полиморфные типы, но мой тест на это:

bla :: (n :: Nat) -> a -> Vec (S n) a
bla = undefined

также не прошел с Несоответствие типа Ожидаемый тип 'ArgKind', но 'n' имеет вид «Нат»(не знаю, что это значит).

Может ли кто-нибудь помочь мне с рабочей версией fromList, а также прояснить другие вопросы? К сожалению, DataKindsеще не очень хорошо задокументирован и, похоже, предполагает, что все, кто его использует, обладают глубокими знаниями в области теории типов.