Зависимо типизированная карта — не ошибетесь?

Предположим, я определяю свой собственный тип списка.

data MyVec : Nat -> Type -> Type where
     MyNil : MyVec Z a
     (::)  : a -> MyVec k a -> MyVec (S k) a

И функция myMap, выполняющая роль fmap для MyVec:

myMap : (a -> b) -> MyVec k a -> MyVec k b
myMap f MyNil     = ?rhs_nil
myMap f (x :: xs) = ?rhs_cons

Попытка решить ?rhs_nil дыру в моем сознании:

1. :t ?rhs_nil is MyVec 0 b
2. достаточно справедливо - мне нужен конструктор, который возвращает MyVec, параметризованный b, и мне нужно, чтобы k было 0 (или Z), и я вижу, что MyNil индексируется Z и параметризуется чем угодно, поэтому я могу легко использовать b, поэтому ?rhs_nil = MyNil и он проверяет тип, денди
3. :t ?rhs_cons is MyVec (S k)
4. Мне нужен конструктор, который возвращает MyVec с параметрами b, и мне нужно, чтобы k было (S k)

Я вижу, что конструктор (::) создает список, индексированный (S k), и я пытаюсь его использовать. Первый аргумент должен быть типа b, учитывая, что я создаю MyVec <> b, и единственный способ получить его — применить x к f.

myMap f (x :: xs) = f x :: <>

Теперь я путаюсь. RHS (::) должен быть MyVec k b, почему я не могу просто использовать конструктор MyNil с объединением/заменой k == Z (который MyNil) дает мне, получая:

myMap f (x :: xs) = f x :: MyNil

Я понимаю, что мне нужно рекурсивно и иметь = f x :: myMap f xs, но как компилятор узнает, сколько раз нужно применить конструктор (::)? Как он выводит правильный k для этого случая, не позволяя мне использовать там Z.