Dependently typed map - can't get it wrong?

Question

Suppose I define my own list type.

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

And a myMap function serving as fmap for MyVec:

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

Attempting to solve the ?rhs_nil hole in my mind:

1. :t ?rhs_nil is MyVec 0 b
2. fair enough - I need a constructor that returns MyVec parameterized by b and I need k to be 0 (or Z) and I can see that MyNil is indexed by Z and parameterized by whatever, so I can use b easily, therefore ?rhs_nil = MyNil and it typechecks, dandy
3. :t ?rhs_cons is MyVec (S k)
4. I need a constructor that returns MyVec parameterized by b and I need k to be (S k)

I do see that the constructor (::) constructs a list indexed by (S k) and I try to use it. The first argument needs to be of type b considering I am building a MyVec <> b and the only way to get it is to apply x to f.

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

Now I get confused. The RHS of (::) is supposed to be MyVec k b, why can I not simply use the MyNil constructor, with unification / substitution k == Z (that MyNil) gives me, getting:

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

I do understand that I need to recurse and have = f x :: myMap f xs, but how does the compiler know the number of times the (::) constructor needs to be applied? How does it infer the correct k for this case, preventing me from using Z there.

Answer 1

The k is already implied by xs : MyVec k a. So you cannot unify k with Z if xs contains some elements.