add implicit take/drop

src/Data/Vec.hs

@@ -280,18 +280,26 @@ product ∷ Num a ⇒ Vec a n → a
 product = foldr (T.*) 0
 
 
--- | 'take' @n@ applied to a 'Vec', returns the first @n@ element
--- of the vector
-take ∷ Sℕ n → Vec a m → Vec a n
-take SZ      _        = Nil
-take (SS n) (x :- xs) = x :- take n xs
+-- | 'take' returns the first @n@ element of the vector
+take ∷ ∀ a n m. SingI n ⇒ Vec a m → Vec a n
+take = take' (sing ∷ Sℕ n)
 
 
--- | 'drop' @n@ applied to a 'Vec', returns every element of
--- the vector but the first @n@
-drop ∷ Sℕ n → Vec a m → Vec a (m :- n)
-drop SZ     x         = x
-drop (SS n) (x :- xs) = drop n xs
+-- | Variant of 'take' with an explicit argument.
+take' ∷ Sℕ n → Vec a m → Vec a n
+take' SZ      _        = Nil
+take' (SS n) (x :- xs) = x :- take' n xs
+
+
+-- | 'drop' returns every element of the vector but the first @n@
+drop ∷ ∀ a n m. SingI n ⇒ Vec a m → Vec a (m :- n)
+drop = drop' (sing ∷ Sℕ n)
+
+
+-- | Variant of 'drop' with an explicit argument.
+drop' ∷ Sℕ n → Vec a m → Vec a (m :- n)
+drop' SZ     x         = x
+drop' (SS n) (x :- xs) = drop' n xs