Agda stdlib Vec fromList of list with arbitrary length

Question

I'm trying to use Data.Vec fromList on a Data.List of arbitrary length:

natListToVec : {n : ℕ} → List ℕ → Vec ℕ n
natListToVec nats = v.fromList nats

but get the error:

l.foldr (λ _ → suc) 0 nats != n of type ℕ
when checking that the expression fromList nats has type Vec ℕ n

When I try with a List that has a known length I don't get any issue:

ListWith2ToVec : v.fromList (2 l.∷ l.[]) ≡ 2 v.∷ v.[]
ListWith2ToVec = refl

I'm guessing the problem is that with this type signature:

{n : ℕ} → List ℕ → Vec ℕ n

I don't specify that n must be the length of the List ℕ.

How would I do this?

Thanks!

Answer 1

You can simply use the length function in the type signature. You also have to name the argument of type list to refer to it, like so:

natListToVec : (xs : List ℕ) → Vec ℕ (length xs)
[...]