How to fix incomplete pattern matching in agda

Question

Here's the code from a custom agda library. In the following code, 𝕍 stands for vector and ℕ for Natural numbers. The take𝕍 type is similar to that of Haskell. Example: "take 3 [1,2,3,4,5,6,7,8]" results in [1,2,3].

take𝕍 : ∀{A : Set}{n : ℕ} → (m : ℕ) → 𝕍 A n → 𝕍 A m
take𝕍 0 xs = []
take𝕍 (suc m) (x :: xs) = x :: take𝕍 m xs

I keep getting the error:

Incomplete pattern matching for take𝕍. Missing cases:
take𝕍 (suc m) [] when checking the definition of take𝕍

I dont understand, what possible proof I might be missing out.

Answer 1

The type signature of take𝕍 says that for any completely unconstrained m you can return a Vec of length m having a Vec of length n. This is not true of course as m must be less or equal to n, because you want to return a prefix of a Vec. And since a number of elements to take and the length of a Vec are unrelated to each other, Agda gives you that error about incomplete pattern matching.

In Agda standard library the restriction that m is less or equal to the length of an input Vec is expressed as follows:

take : ∀ {a} {A : Set a} m {n} → Vec A (m + n) → Vec A m

You can also define something like

take : ∀ {a} {A : Set a} {m n} → m ≤ n → Vec A n → Vec A m

Or even

take : ∀ {a} {A : Set a} m {n} → Vec A n → Vec A (m ⊔ n)

to model the behavior of Data.List.take (where _⊔_ means min in Agda stdlib).

Answer 2

You are pattern-matching on m and a vector xs of type 𝕍 A n. There is no guarantee that, because m is suc-headed that xs is non-empty. As the error suggests, you need to also consider the case where m is a suc and xs is empty.

Alternatively, you can write a function with a more precise type guaranteeing the fact that xs is at least as long as m. This is what is used in the standard library:

take : ∀ {A : Set} m {n} → Vec A (m + n) → Vec A m