diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,17 @@
 # Revision history for vec
 
+## 0.4
+
+- Support `fin-0.2`
+- Add `indexed-traversable` instances
+- Explicitly mark all modules as Safe or Trustworthy.
+- Add `Eq1`, `Ord1` and `Show1` instances
+- Add `init`, `last` and `toNonEmpty`
+
+## 0.3.0.1
+
+- Fix `product`
+
 ## 0.3
 
 - Split `lens` utilities into [`vec-lens`](https://hackage.haskell.org/package/vec-lens) package.
diff --git a/bench/DotProduct.hs b/bench/DotProduct.hs
--- a/bench/DotProduct.hs
+++ b/bench/DotProduct.hs
@@ -25,5 +25,5 @@
 pullDotProduct' :: N.SNatI n => P.Vec n Int -> P.Vec n Int -> Int
 pullDotProduct' xs ys = P.sum (P.zipWith (*) xs ys)
 
-inlineDotProduct :: N.InlineInduction n => L.Vec n Int -> L.Vec n Int -> Int
+inlineDotProduct :: N.SNatI n => L.Vec n Int -> L.Vec n Int -> Int
 inlineDotProduct xs ys = I.sum (I.zipWith (*) xs ys)
diff --git a/src/Control/Lens/Yocto.hs b/src/Control/Lens/Yocto.hs
--- a/src/Control/Lens/Yocto.hs
+++ b/src/Control/Lens/Yocto.hs
@@ -1,5 +1,6 @@
-{-# LANGUAGE CPP        #-}
-{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE CPP         #-}
+{-# LANGUAGE RankNTypes  #-}
+{-# LANGUAGE Trustworthy #-}
 -- | A small module defining the least you need to support
 -- van-Laarhoven lenses without depending on @lens@ or @microlens@ or ...
 --
@@ -43,7 +44,7 @@
 #endif
 
 #if MIN_VERSION_base(4,11,0)
-import Data.Functor        ((<&>))
+import Data.Functor ((<&>))
 #endif
 
 -------------------------------------------------------------------------------
diff --git a/src/Data/Vec/DataFamily/SpineStrict.hs b/src/Data/Vec/DataFamily/SpineStrict.hs
--- a/src/Data/Vec/DataFamily/SpineStrict.hs
+++ b/src/Data/Vec/DataFamily/SpineStrict.hs
@@ -1,8 +1,10 @@
 {-# LANGUAGE CPP                   #-}
 {-# LANGUAGE DataKinds             #-}
 {-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE InstanceSigs          #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE Safe                  #-}
 {-# LANGUAGE ScopedTypeVariables   #-}
 {-# LANGUAGE TypeFamilies          #-}
 {-# LANGUAGE UndecidableInstances  #-}
@@ -61,6 +63,7 @@
     toPull,
     fromPull,
     toList,
+    toNonEmpty,
     fromList,
     fromListPrefix,
     reifyList,
@@ -70,7 +73,9 @@
     cons,
     snoc,
     head,
+    last,
     tail,
+    init,
     -- * Reverse
     reverse,
     -- * Concatenation and splitting
@@ -114,13 +119,14 @@
     ) where
 
 import Prelude
-       (Bool (..), Eq (..), Functor (..), Int, Maybe (..), Monad (..),
-       Num (..), Ord (..), Ordering (EQ), Show (..), ShowS, const, flip, id,
-       seq, showParen, showString, uncurry, ($), (&&), (.))
+       (Bool (..), Eq (..), Functor (..), Int, Maybe (..), Monad (..), Num (..),
+       Ord (..), Ordering (EQ), Show (..), ShowS, const, flip, id, seq,
+       showParen, showString, uncurry, ($), (&&), (.))
 
 import Control.Applicative (Applicative (..), liftA2, (<$>))
 import Control.DeepSeq     (NFData (..))
 import Data.Fin            (Fin (..))
+import Data.List.NonEmpty  (NonEmpty (..))
 import Data.Hashable       (Hashable (..))
 import Data.Monoid         (Monoid (..))
 import Data.Nat            (Nat (..))
@@ -131,6 +137,12 @@
 import qualified Data.Traversable as I (Traversable (..))
 import qualified Test.QuickCheck  as QC
 
+import qualified Data.Foldable.WithIndex    as WI (FoldableWithIndex (..))
+import qualified Data.Functor.WithIndex     as WI (FunctorWithIndex (..))
+import qualified Data.Traversable.WithIndex as WI (TraversableWithIndex (..))
+
+import Data.Functor.Classes (Eq1 (..), Ord1 (..), Show1 (..))
+
 #ifdef MIN_VERSION_adjunctions
 import qualified Data.Functor.Rep as I (Representable (..))
 #endif
@@ -155,7 +167,11 @@
 -- $setup
 -- >>> :set -XScopedTypeVariables -XDataKinds
 -- >>> import Data.Proxy (Proxy (..))
--- >>> import Prelude (Char, not, uncurry, error)
+-- >>> import Control.Applicative ((<$>))
+-- >>> import Prelude (Char, not, uncurry, error, Eq (..), Ord (..), Bool (..), Maybe (..), ($), id, (.), Int)
+-- >>> import qualified Data.Type.Nat as N
+-- >>> import Data.Fin (Fin (..))
+-- >>> import Data.Nat (Nat (..))
 
 -------------------------------------------------------------------------------
 -- Type
@@ -176,34 +192,34 @@
 --
 -- >>> 'a' ::: 'b' ::: VNil == 'a' ::: 'c' ::: VNil
 -- False
-instance (Eq a, N.InlineInduction n) => Eq (Vec n a) where
-    (==) = getEqual (N.inlineInduction1 start step) where
-        start :: Equal 'Z a
+instance (Eq a, N.SNatI n) => Eq (Vec n a) where
+    (==) = getEqual (N.induction start step) where
+        start :: Equal a a 'Z
         start = Equal $ \_ _ -> True
 
-        step :: Equal m a -> Equal ('S m) a
+        step :: Equal a a m -> Equal a a ('S m)
         step (Equal go) = Equal $ \(x ::: xs) (y ::: ys) ->
             x == y && go xs ys
 
-newtype Equal n a = Equal { getEqual :: Vec n a -> Vec n a -> Bool }
+newtype Equal a b n = Equal { getEqual :: Vec n a -> Vec n b -> Bool }
 
 -- |
 --
 -- >>> compare ('a' ::: 'b' ::: VNil) ('a' ::: 'c' ::: VNil)
 -- LT
-instance (Ord a, N.InlineInduction n) => Ord (Vec n a) where
-    compare = getCompare (N.inlineInduction1 start step) where
-        start :: Compare 'Z a
+instance (Ord a, N.SNatI n) => Ord (Vec n a) where
+    compare = getCompare (N.induction start step) where
+        start :: Compare a a 'Z
         start = Compare $ \_ _ -> EQ
 
-        step :: Compare m a -> Compare ('S m) a
+        step :: Compare a a m -> Compare a a ('S m)
         step (Compare go) = Compare $ \(x ::: xs) (y ::: ys) ->
             compare x y <> go xs ys
 
-newtype Compare n a = Compare { getCompare :: Vec n a -> Vec n a -> Ordering }
+newtype Compare a b n = Compare { getCompare :: Vec n a -> Vec n b -> Ordering }
 
-instance (Show a, N.InlineInduction n) => Show (Vec n a) where
-    showsPrec = getShowsPrec (N.inlineInduction1 start step) where
+instance (Show a, N.SNatI n) => Show (Vec n a) where
+    showsPrec = getShowsPrec (N.induction1 start step) where
         start :: ShowsPrec 'Z a
         start = ShowsPrec $ \_ _ -> showString "VNil"
 
@@ -215,10 +231,10 @@
 
 newtype ShowsPrec n a = ShowsPrec { getShowsPrec :: Int -> Vec n a -> ShowS }
 
-instance N.InlineInduction n => Functor (Vec n) where
+instance N.SNatI n => Functor (Vec n) where
     fmap = map
 
-instance N.InlineInduction n => I.Foldable (Vec n) where
+instance N.SNatI n => I.Foldable (Vec n) where
     foldMap = foldMap
 
     foldr  = foldr
@@ -232,34 +248,46 @@
 #endif
 
 #ifdef MIN_VERSION_semigroupoids
-instance (N.InlineInduction m, n ~ 'S m) => I.Foldable1 (Vec n) where
+instance (N.SNatI m, n ~ 'S m) => I.Foldable1 (Vec n) where
     foldMap1 = foldMap1
 
-instance (N.InlineInduction m, n ~ 'S m) => I.Traversable1 (Vec n) where
+instance (N.SNatI m, n ~ 'S m) => I.Traversable1 (Vec n) where
     traverse1 = traverse1
 #endif
 
-instance N.InlineInduction n => I.Traversable (Vec n) where
+instance N.SNatI n => I.Traversable (Vec n) where
     traverse = traverse
 
+-- | @since 0.4
+instance N.SNatI n => WI.FunctorWithIndex (Fin n) (Vec n) where
+    imap = imap
 
-instance (NFData a, N.InlineInduction n) => NFData (Vec n a) where
-    rnf = getRnf (N.inlineInduction1 z s) where
+-- | @since 0.4
+instance N.SNatI n => WI.FoldableWithIndex (Fin n) (Vec n) where
+    ifoldMap = ifoldMap
+    ifoldr   = ifoldr
+
+-- | @since 0.4
+instance N.SNatI n => WI.TraversableWithIndex (Fin n) (Vec n) where
+    itraverse = itraverse
+
+instance (NFData a, N.SNatI n) => NFData (Vec n a) where
+    rnf = getRnf (N.induction1 z s) where
         z           = Rnf $ \VNil -> ()
         s (Rnf rec) = Rnf $ \(x ::: xs) -> rnf x `seq` rec xs
 
 newtype Rnf n a = Rnf { getRnf :: Vec n a -> () }
 
-instance (Hashable a, N.InlineInduction n) => Hashable (Vec n a) where
-    hashWithSalt = getHashWithSalt (N.inlineInduction1 z s) where
+instance (Hashable a, N.SNatI n) => Hashable (Vec n a) where
+    hashWithSalt = getHashWithSalt (N.induction1 z s) where
         z = HashWithSalt $ \salt VNil -> salt `hashWithSalt` (0 :: Int)
         s (HashWithSalt rec) = HashWithSalt $ \salt (x ::: xs) -> rec (salt
             `hashWithSalt` x) xs
 
 newtype HashWithSalt n a = HashWithSalt { getHashWithSalt :: Int -> Vec n a -> Int }
 
-instance N.InlineInduction n => Applicative (Vec n) where
-    pure x = N.inlineInduction1 VNil (x :::)
+instance N.SNatI n => Applicative (Vec n) where
+    pure x = N.induction1 VNil (x :::)
     (<*>)  = zipWith ($)
     _ *> x = x
     x <* _ = x
@@ -267,43 +295,110 @@
     liftA2 = zipWith
 #endif
 
-instance N.InlineInduction n => Monad (Vec n) where
+instance N.SNatI n => Monad (Vec n) where
     return = pure
     (>>=)  = bind
     _ >> x = x
 
 #ifdef MIN_VERSION_distributive
-instance N.InlineInduction n => Distributive (Vec n) where
+instance N.SNatI n => Distributive (Vec n) where
     distribute f = tabulate (\k -> fmap (! k) f)
 
 #ifdef MIN_VERSION_adjunctions
-instance N.InlineInduction n => I.Representable (Vec n) where
+instance N.SNatI n => I.Representable (Vec n) where
     type Rep (Vec n) = Fin n
     tabulate = tabulate
     index    = (!)
 #endif
 #endif
 
-instance (Semigroup a, N.InlineInduction n) => Semigroup (Vec n a) where
+instance (Semigroup a, N.SNatI n) => Semigroup (Vec n a) where
     (<>) = zipWith (<>)
 
-instance (Monoid a, N.InlineInduction n) => Monoid (Vec n a) where
+instance (Monoid a, N.SNatI n) => Monoid (Vec n a) where
     mempty = pure mempty
     mappend = zipWith mappend
 
 #ifdef MIN_VERSION_semigroupoids
-instance N.InlineInduction n => Apply (Vec n) where
+instance N.SNatI n => Apply (Vec n) where
     (<.>) = zipWith ($)
     _ .> x = x
     x <. _ = x
     liftF2 = zipWith
 
-instance N.InlineInduction n => I.Bind (Vec n) where
+instance N.SNatI n => I.Bind (Vec n) where
     (>>-) = bind
     join  = join
 #endif
 
 -------------------------------------------------------------------------------
+-- Data.Functor.Classes
+-------------------------------------------------------------------------------
+
+#ifndef MIN_VERSION_transformers_compat
+#define MIN_VERSION_transformers_compat(x,y,z) 0
+#endif
+
+
+#if MIN_VERSION_base(4,9,0)
+#define LIFTED_FUNCTOR_CLASSES 1
+#else
+#if MIN_VERSION_transformers(0,5,0)
+#define LIFTED_FUNCTOR_CLASSES 1
+#else
+#if MIN_VERSION_transformers_compat(0,5,0) && !MIN_VERSION_transformers(0,4,0)
+#define LIFTED_FUNCTOR_CLASSES 1
+#endif
+#endif
+#endif
+
+#if LIFTED_FUNCTOR_CLASSES
+
+-- | @since 0.4
+instance N.SNatI n => Eq1 (Vec n) where
+    liftEq :: forall a b. (a -> b -> Bool) -> Vec n a -> Vec n b -> Bool
+    liftEq eq = getEqual (N.induction start step) where
+        start :: Equal a b 'Z
+        start = Equal $ \_ _ -> True
+
+        step :: Equal a b m -> Equal a b ('S m)
+        step (Equal go) = Equal $ \(x ::: xs) (y ::: ys) ->
+            eq x y && go xs ys
+
+-- | @since 0.4
+instance N.SNatI n => Ord1 (Vec n) where
+    liftCompare :: forall a b. (a -> b -> Ordering) -> Vec n a -> Vec n b -> Ordering
+    liftCompare cmp = getCompare (N.induction start step) where
+        start :: Compare a b 'Z
+        start = Compare $ \_ _ -> EQ
+
+        step :: Compare a b m -> Compare a b ('S m)
+        step (Compare go) = Compare $ \(x ::: xs) (y ::: ys) ->
+            cmp x y <> go xs ys
+
+-- | @since 0.4
+instance N.SNatI n => Show1 (Vec n) where
+    liftShowsPrec :: forall a. (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Vec n a -> ShowS
+    liftShowsPrec sp _ = getShowsPrec (N.induction1 start step) where
+        start :: ShowsPrec 'Z a
+        start = ShowsPrec $ \_ _ -> showString "VNil"
+
+        step :: ShowsPrec m a -> ShowsPrec ('S m) a
+        step (ShowsPrec go) = ShowsPrec $ \d (x ::: xs) -> showParen (d > 5)
+            $ sp 6 x
+            . showString " ::: "
+            . go 5 xs
+#else
+-- | @since 0.4
+instance N.SNatI n => Eq1 (Vec n) where eq1 = (==)
+
+-- | @since 0.4
+instance N.SNatI n => Ord1 (Vec n) where compare1 = compare
+
+-- | @since 0.4
+instance N.SNatI n => Show1 (Vec n) where showsPrec1 = showsPrec
+#endif
+-------------------------------------------------------------------------------
 -- Construction
 -------------------------------------------------------------------------------
 
@@ -324,8 +419,8 @@
 -------------------------------------------------------------------------------
 
 -- | Convert to pull 'P.Vec'.
-toPull :: forall n a. N.InlineInduction n => Vec n a -> P.Vec n a
-toPull = getToPull (N.inlineInduction1 start step) where
+toPull :: forall n a. N.SNatI n => Vec n a -> P.Vec n a
+toPull = getToPull (N.induction1 start step) where
     start :: ToPull 'Z a
     start = ToPull $ \_ -> P.Vec F.absurd
 
@@ -337,8 +432,8 @@
 newtype ToPull n a = ToPull { getToPull :: Vec n a -> P.Vec n a }
 
 -- | Convert from pull 'P.Vec'.
-fromPull :: forall n a. N.InlineInduction n => P.Vec n a -> Vec n a
-fromPull = getFromPull (N.inlineInduction1 start step) where
+fromPull :: forall n a. N.SNatI n => P.Vec n a -> Vec n a
+fromPull = getFromPull (N.induction1 start step) where
     start :: FromPull 'Z a
     start = FromPull $ const VNil
 
@@ -351,8 +446,8 @@
 --
 -- >>> toList $ 'f' ::: 'o' ::: 'o' ::: VNil
 -- "foo"
-toList :: forall n a. N.InlineInduction n => Vec n a -> [a]
-toList = getToList (N.inlineInduction1 start step) where
+toList :: forall n a. N.SNatI n => Vec n a -> [a]
+toList = getToList (N.induction1 start step) where
     start :: ToList 'Z a
     start = ToList (const [])
 
@@ -361,6 +456,15 @@
 
 newtype ToList n a = ToList { getToList :: Vec n a -> [a] }
 
+-- |
+--
+-- >>> toNonEmpty $ 1 ::: 2 ::: 3 ::: VNil
+-- 1 :| [2,3]
+--
+-- @since 0.4
+toNonEmpty :: forall n a. N.SNatI n => Vec ('S n) a -> NonEmpty a
+toNonEmpty (x ::: xs) = x :| toList xs
+
 -- | Convert list @[a]@ to @'Vec' n a@.
 -- Returns 'Nothing' if lengths don't match exactly.
 --
@@ -373,8 +477,8 @@
 -- >>> fromList "xy" :: Maybe (Vec N.Nat3 Char)
 -- Nothing
 --
-fromList :: N.InlineInduction n => [a] -> Maybe (Vec n a)
-fromList = getFromList (N.inlineInduction1 start step) where
+fromList :: N.SNatI n => [a] -> Maybe (Vec n a)
+fromList = getFromList (N.induction1 start step) where
     start :: FromList 'Z a
     start = FromList $ \xs -> case xs of
         []      -> Just VNil
@@ -399,8 +503,8 @@
 -- >>> fromListPrefix "xy" :: Maybe (Vec N.Nat3 Char)
 -- Nothing
 --
-fromListPrefix :: N.InlineInduction n => [a] -> Maybe (Vec n a)
-fromListPrefix = getFromList (N.inlineInduction1 start step) where
+fromListPrefix :: N.SNatI n => [a] -> Maybe (Vec n a)
+fromListPrefix = getFromList (N.induction1 start step) where
     start :: FromList 'Z a
     start = FromList $ \_ -> Just VNil -- different than in fromList case
 
@@ -413,7 +517,7 @@
 --
 -- >>> reifyList "foo" length
 -- 3
-reifyList :: [a] -> (forall n. N.InlineInduction n => Vec n a -> r) -> r
+reifyList :: [a] -> (forall n. N.SNatI n => Vec n a -> r) -> r
 reifyList []       f = f VNil
 reifyList (x : xs) f = reifyList xs $ \xs' -> f (x ::: xs')
 
@@ -421,8 +525,8 @@
 -- Indexing
 -------------------------------------------------------------------------------
 
-flipIndex :: N.InlineInduction n => Fin n -> Vec n a -> a
-flipIndex = getIndex (N.inlineInduction1 start step) where
+flipIndex :: N.SNatI n => Fin n -> Vec n a -> a
+flipIndex = getIndex (N.induction1 start step) where
     start :: Index 'Z a
     start = Index F.absurd
 
@@ -438,14 +542,14 @@
 -- >>> ('a' ::: 'b' ::: 'c' ::: VNil) ! FS FZ
 -- 'b'
 --
-(!) :: N.InlineInduction n => Vec n a -> Fin n -> a
+(!) :: N.SNatI n => Vec n a -> Fin n -> a
 (!) = flip flipIndex
 
 -- | Tabulating, inverse of '!'.
 --
 -- >>> tabulate id :: Vec N.Nat3 (Fin N.Nat3)
 -- 0 ::: 1 ::: 2 ::: VNil
-tabulate :: N.InlineInduction n => (Fin n -> a) -> Vec n a
+tabulate :: N.SNatI n => (Fin n -> a) -> Vec n a
 tabulate = fromPull . P.tabulate
 
 -- | Cons an element in front of a 'Vec'.
@@ -453,8 +557,8 @@
 cons = (:::)
 
 -- | Add a single element at the end of a 'Vec'.
-snoc :: forall n a. N.InlineInduction n => Vec n a -> a -> Vec ('S n) a
-snoc xs x = getSnoc (N.inlineInduction1 start step) xs where
+snoc :: forall n a. N.SNatI n => Vec n a -> a -> Vec ('S n) a
+snoc xs x = getSnoc (N.induction1 start step) xs where
     start :: Snoc 'Z a
     start = Snoc $ \ys -> x ::: ys
 
@@ -471,6 +575,33 @@
 tail :: Vec ('S n) a -> Vec n a
 tail (_ ::: xs) = xs
 
+-- | The last element of a 'Vec'.
+--
+-- @since 0.4
+last :: forall n a. N.SNatI n => Vec ('S n) a -> a
+last xs = getLast (N.induction1 start step) xs where
+    start :: Last 'Z a
+    start = Last $ \(x:::VNil) -> x
+    
+    step :: Last m a -> Last ('S m) a
+    step (Last rec) = Last $ \(_ ::: ys) -> rec ys
+    
+
+newtype Last n a = Last { getLast :: Vec ('S n) a -> a }
+
+-- | The elements before the 'last' of a 'Vec'.
+--
+-- @since 0.4
+init :: forall n a. N.SNatI n => Vec ('S n) a -> Vec n a
+init xs = getInit (N.induction1 start step) xs where
+    start :: Init 'Z a
+    start = Init (const VNil)
+    
+    step :: Init m a -> Init ('S m) a
+    step (Init rec) = Init $ \(y ::: ys) -> y ::: rec ys
+
+newtype Init n a = Init { getInit :: Vec ('S n) a -> Vec n a}
+
 -------------------------------------------------------------------------------
 -- Reverse
 -------------------------------------------------------------------------------
@@ -482,12 +613,12 @@
 --
 -- @since 0.2.1
 --
-reverse :: forall n a. N.InlineInduction n => Vec n a -> Vec n a
-reverse = getReverse (N.inlineInduction1 start step) where
+reverse :: forall n a. N.SNatI n => Vec n a -> Vec n a
+reverse = getReverse (N.induction1 start step) where
     start :: Reverse 'Z a
     start = Reverse $ \_ -> VNil
 
-    step :: N.InlineInduction m => Reverse m a -> Reverse ('S m) a
+    step :: N.SNatI m => Reverse m a -> Reverse ('S m) a
     step (Reverse rec) = Reverse $ \(x ::: xs) -> snoc (rec xs) x
 
 newtype Reverse n a = Reverse { getReverse :: Vec n a -> Vec n a }
@@ -503,8 +634,8 @@
 -- >>> ('a' ::: 'b' ::: VNil) ++ ('c' ::: 'd' ::: VNil)
 -- 'a' ::: 'b' ::: 'c' ::: 'd' ::: VNil
 --
-(++) :: forall n m a. N.InlineInduction n => Vec n a -> Vec m a -> Vec (N.Plus n m) a
-as ++ ys = getAppend (N.inlineInduction1 start step) as where
+(++) :: forall n m a. N.SNatI n => Vec n a -> Vec m a -> Vec (N.Plus n m) a
+as ++ ys = getAppend (N.induction1 start step) as where
     start :: Append m 'Z a
     start = Append $ \_ -> ys
 
@@ -521,8 +652,8 @@
 -- >>> uncurry (++) (split ('a' ::: 'b' ::: 'c' ::: VNil) :: (Vec N.Nat1 Char, Vec N.Nat2 Char))
 -- 'a' ::: 'b' ::: 'c' ::: VNil
 --
-split :: N.InlineInduction n => Vec (N.Plus n m) a -> (Vec n a, Vec m a)
-split = appSplit (N.inlineInduction1 start step) where
+split :: N.SNatI n => Vec (N.Plus n m) a -> (Vec n a, Vec m a)
+split = appSplit (N.induction1 start step) where
     start :: Split m 'Z a
     start = Split $ \xs -> (VNil, xs)
 
@@ -537,8 +668,8 @@
 -- >>> concatMap (\x -> x ::: x ::: VNil) ('a' ::: 'b' ::: VNil)
 -- 'a' ::: 'a' ::: 'b' ::: 'b' ::: VNil
 --
-concatMap :: forall a b n m. (N.InlineInduction m, N.InlineInduction n) => (a -> Vec m b) -> Vec n a -> Vec (N.Mult n m) b
-concatMap f = getConcatMap $ N.inlineInduction1 start step where
+concatMap :: forall a b n m. (N.SNatI m, N.SNatI n) => (a -> Vec m b) -> Vec n a -> Vec (N.Mult n m) b
+concatMap f = getConcatMap $ N.induction1 start step where
     start :: ConcatMap m a 'Z b
     start = ConcatMap $ \_ -> VNil
 
@@ -548,7 +679,7 @@
 newtype ConcatMap m a n b = ConcatMap { getConcatMap :: Vec n a -> Vec (N.Mult n m) b }
 
 -- | @'concatMap' 'id'@
-concat :: (N.InlineInduction m, N.InlineInduction n) => Vec n (Vec m a) -> Vec (N.Mult n m) a
+concat :: (N.SNatI m, N.SNatI n) => Vec n (Vec m a) -> Vec (N.Mult n m) a
 concat = concatMap id
 
 -- | Inverse of 'concat'.
@@ -560,12 +691,12 @@
 -- >>> concat . idVec . chunks <$> fromListPrefix [1..]
 -- Just (1 ::: 2 ::: 3 ::: 4 ::: 5 ::: 6 ::: VNil)
 --
-chunks :: (N.InlineInduction n, N.InlineInduction m) => Vec (N.Mult n m) a -> Vec n (Vec m a)
+chunks :: (N.SNatI n, N.SNatI m) => Vec (N.Mult n m) a -> Vec n (Vec m a)
 chunks = getChunks $ N.induction1 start step where
     start :: Chunks m 'Z a
     start = Chunks $ \_ -> VNil
 
-    step :: forall m n a. N.InlineInduction m => Chunks m n a -> Chunks m ('S n) a
+    step :: forall m n a. N.SNatI m => Chunks m n a -> Chunks m ('S n) a
     step (Chunks go) = Chunks $ \xs ->
         let (ys, zs) = split xs :: (Vec m a, Vec (N.Mult n m) a)
         in ys ::: go zs
@@ -579,8 +710,8 @@
 -- | >>> map not $ True ::: False ::: VNil
 -- False ::: True ::: VNil
 --
-map :: forall a b n. N.InlineInduction n => (a -> b) -> Vec n a -> Vec n b
-map f = getMap $ N.inlineInduction1 start step where
+map :: forall a b n. N.SNatI n => (a -> b) -> Vec n a -> Vec n b
+map f = getMap $ N.induction1 start step where
     start :: Map a 'Z b
     start = Map $ \_ -> VNil
 
@@ -592,8 +723,8 @@
 -- | >>> imap (,) $ 'a' ::: 'b' ::: 'c' ::: VNil
 -- (0,'a') ::: (1,'b') ::: (2,'c') ::: VNil
 --
-imap :: N.InlineInduction n => (Fin n -> a -> b) -> Vec n a -> Vec n b
-imap = getIMap $ N.inlineInduction1 start step where
+imap :: N.SNatI n => (Fin n -> a -> b) -> Vec n a -> Vec n b
+imap = getIMap $ N.induction1 start step where
     start :: IMap a 'Z b
     start = IMap $ \_ _ -> VNil
 
@@ -603,8 +734,8 @@
 newtype IMap a n b = IMap { getIMap :: (Fin n -> a -> b) -> Vec n a -> Vec n b }
 
 -- | Apply an action to every element of a 'Vec', yielding a 'Vec' of results.
-traverse :: forall n f a b. (Applicative f, N.InlineInduction n) => (a -> f b) -> Vec n a -> f (Vec n b)
-traverse f =  getTraverse $ N.inlineInduction1 start step where
+traverse :: forall n f a b. (Applicative f, N.SNatI n) => (a -> f b) -> Vec n a -> f (Vec n b)
+traverse f =  getTraverse $ N.induction1 start step where
     start :: Traverse f a 'Z b
     start = Traverse $ \_ -> pure VNil
 
@@ -616,8 +747,8 @@
 
 #ifdef MIN_VERSION_semigroupoids
 -- | Apply an action to non-empty 'Vec', yielding a 'Vec' of results.
-traverse1 :: forall n f a b. (Apply f, N.InlineInduction n) => (a -> f b) -> Vec ('S n) a -> f (Vec ('S n) b)
-traverse1 f = getTraverse1 $ N.inlineInduction1 start step where
+traverse1 :: forall n f a b. (Apply f, N.SNatI n) => (a -> f b) -> Vec ('S n) a -> f (Vec ('S n) b)
+traverse1 f = getTraverse1 $ N.induction1 start step where
     start :: Traverse1 f a 'Z b
     start = Traverse1 $ \(x ::: _) -> (::: VNil) <$> f x
 
@@ -628,8 +759,8 @@
 #endif
 
 -- | Apply an action to every element of a 'Vec' and its index, yielding a 'Vec' of results.
-itraverse :: forall n f a b. (Applicative f, N.InlineInduction n) => (Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
-itraverse = getITraverse $ N.inlineInduction1 start step where
+itraverse :: forall n f a b. (Applicative f, N.SNatI n) => (Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
+itraverse = getITraverse $ N.induction1 start step where
     start :: ITraverse f a 'Z b
     start = ITraverse $ \_ _ -> pure VNil
 
@@ -640,8 +771,8 @@
 newtype ITraverse f a n b = ITraverse { getITraverse :: (Fin n -> a -> f b) -> Vec n a -> f (Vec n b) }
 
 -- | Apply an action to every element of a 'Vec' and its index, ignoring the results.
-itraverse_ :: forall n f a b. (Applicative f, N.InlineInduction n) => (Fin n -> a -> f b) -> Vec n a -> f ()
-itraverse_ = getITraverse_ $ N.inlineInduction1 start step where
+itraverse_ :: forall n f a b. (Applicative f, N.SNatI n) => (Fin n -> a -> f b) -> Vec n a -> f ()
+itraverse_ = getITraverse_ $ N.induction1 start step where
     start :: ITraverse_ f a 'Z b
     start = ITraverse_ $ \_ _ -> pure ()
 
@@ -655,15 +786,15 @@
 -------------------------------------------------------------------------------
 
 -- | See 'I.Foldable'.
-foldMap :: (Monoid m, N.InlineInduction n) => (a -> m) -> Vec n a -> m
-foldMap f = getFold $ N.inlineInduction1 (Fold (const mempty)) $ \(Fold go) ->
+foldMap :: (Monoid m, N.SNatI n) => (a -> m) -> Vec n a -> m
+foldMap f = getFold $ N.induction1 (Fold (const mempty)) $ \(Fold go) ->
     Fold $ \(x ::: xs) -> f x `mappend` go xs
 
 newtype Fold  a n b = Fold  { getFold  :: Vec n a -> b }
 
 -- | See 'I.Foldable1'.
-foldMap1 :: forall s a n. (Semigroup s, N.InlineInduction n) => (a -> s) -> Vec ('S n) a -> s
-foldMap1 f = getFold1 $ N.inlineInduction1 start step where
+foldMap1 :: forall s a n. (Semigroup s, N.SNatI n) => (a -> s) -> Vec ('S n) a -> s
+foldMap1 f = getFold1 $ N.induction1 start step where
     start :: Fold1 a 'Z s
     start = Fold1 $ \(x ::: _) -> f x
 
@@ -673,8 +804,8 @@
 newtype Fold1 a n b = Fold1 { getFold1 :: Vec ('S n) a -> b }
 
 -- | See 'I.FoldableWithIndex'.
-ifoldMap :: forall a n m. (Monoid m, N.InlineInduction n) => (Fin n -> a -> m) -> Vec n a -> m
-ifoldMap = getIFoldMap $ N.inlineInduction1 start step where
+ifoldMap :: forall a n m. (Monoid m, N.SNatI n) => (Fin n -> a -> m) -> Vec n a -> m
+ifoldMap = getIFoldMap $ N.induction1 start step where
     start :: IFoldMap a 'Z m
     start = IFoldMap $ \_ _ -> mempty
 
@@ -684,8 +815,8 @@
 newtype IFoldMap a n m = IFoldMap { getIFoldMap :: (Fin n -> a -> m) -> Vec n a -> m }
 
 -- | There is no type-class for this :(
-ifoldMap1 :: forall a n s. (Semigroup s, N.InlineInduction n) => (Fin ('S n) -> a -> s) -> Vec ('S n) a -> s
-ifoldMap1 = getIFoldMap1 $ N.inlineInduction1 start step where
+ifoldMap1 :: forall a n s. (Semigroup s, N.SNatI n) => (Fin ('S n) -> a -> s) -> Vec ('S n) a -> s
+ifoldMap1 = getIFoldMap1 $ N.induction1 start step where
     start :: IFoldMap1 a 'Z s
     start = IFoldMap1 $ \f (x ::: _) -> f FZ x
 
@@ -695,8 +826,8 @@
 newtype IFoldMap1 a n m = IFoldMap1 { getIFoldMap1 :: (Fin ('S n) -> a -> m) -> Vec ('S n) a -> m }
 
 -- | Right fold.
-foldr :: forall a b n. N.InlineInduction n => (a -> b -> b) -> b -> Vec n a -> b
-foldr f z = getFold $ N.inlineInduction1 start step where
+foldr :: forall a b n. N.SNatI n => (a -> b -> b) -> b -> Vec n a -> b
+foldr f z = getFold $ N.induction1 start step where
     start :: Fold a 'Z b
     start = Fold $ \_ -> z
 
@@ -704,8 +835,8 @@
     step (Fold go) = Fold $ \(x ::: xs) -> f x (go xs)
 
 -- | Right fold with an index.
-ifoldr :: forall a b n. N.InlineInduction n => (Fin n -> a -> b -> b) -> b -> Vec n a -> b
-ifoldr = getIFoldr $ N.inlineInduction1 start step where
+ifoldr :: forall a b n. N.SNatI n => (Fin n -> a -> b -> b) -> b -> Vec n a -> b
+ifoldr = getIFoldr $ N.induction1 start step where
     start :: IFoldr a 'Z b
     start = IFoldr $ \_ z _ -> z
 
@@ -715,10 +846,10 @@
 newtype IFoldr a n b = IFoldr { getIFoldr :: (Fin n -> a -> b -> b) -> b -> Vec n a -> b }
 
 -- | Yield the length of a 'Vec'. /O(n)/
-length :: forall n a. N.InlineInduction n => Vec n a -> Int
+length :: forall n a. N.SNatI n => Vec n a -> Int
 length _ = getLength l where
     l :: Length n
-    l = N.inlineInduction (Length 0) $ \(Length n) -> Length (1 + n)
+    l = N.induction (Length 0) $ \(Length n) -> Length (1 + n)
 
 newtype Length (n :: Nat) = Length { getLength :: Int }
 
@@ -733,8 +864,8 @@
 -------------------------------------------------------------------------------
 
 -- | Non-strict 'sum'.
-sum :: (Num a, N.InlineInduction n) => Vec n a -> a
-sum = getFold $ N.inlineInduction1 start step where
+sum :: (Num a, N.SNatI n) => Vec n a -> a
+sum = getFold $ N.induction1 start step where
     start :: Num a => Fold a 'Z a
     start = Fold $ \_ -> 0
 
@@ -742,13 +873,13 @@
     step (Fold f) = Fold $ \(x ::: xs) -> x + f xs
 
 -- | Non-strict 'product'.
-product :: (Num a, N.InlineInduction n) => Vec n a -> a
-product = getFold $ N.inlineInduction1 start step where
+product :: (Num a, N.SNatI n) => Vec n a -> a
+product = getFold $ N.induction1 start step where
     start :: Num a => Fold a 'Z a
-    start = Fold $ \_ -> 0
+    start = Fold $ \_ -> 1
 
     step :: Num a => Fold a m a -> Fold a ('S m) a
-    step (Fold f) = Fold $ \(x ::: xs) -> x + f xs
+    step (Fold f) = Fold $ \(x ::: xs) -> x * f xs
 
 
 -------------------------------------------------------------------------------
@@ -756,8 +887,8 @@
 -------------------------------------------------------------------------------
 
 -- | Zip two 'Vec's with a function.
-zipWith :: forall a b c n. N.InlineInduction n => (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
-zipWith f = getZipWith $ N.inlineInduction start step where
+zipWith :: forall a b c n. N.SNatI n => (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
+zipWith f = getZipWith $ N.induction start step where
     start :: ZipWith a b c 'Z
     start = ZipWith $ \_ _ -> VNil
 
@@ -767,8 +898,8 @@
 newtype ZipWith a b c n = ZipWith { getZipWith :: Vec n a -> Vec n b -> Vec n c }
 
 -- | Zip two 'Vec's. with a function that also takes the elements' indices.
-izipWith :: N.InlineInduction n => (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
-izipWith = getIZipWith $ N.inlineInduction start step where
+izipWith :: N.SNatI n => (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
+izipWith = getIZipWith $ N.induction start step where
     start :: IZipWith a b c 'Z
     start = IZipWith $ \_ _ _ -> VNil
 
@@ -783,16 +914,16 @@
 -- 'x' ::: 'x' ::: 'x' ::: VNil
 --
 -- @since 0.2.1
-repeat :: N.InlineInduction n => x -> Vec n x
-repeat x = N.inlineInduction1 VNil (x :::)
+repeat :: N.SNatI n => x -> Vec n x
+repeat x = N.induction1 VNil (x :::)
 
 -------------------------------------------------------------------------------
 -- Monadic
 -------------------------------------------------------------------------------
 
 -- | Monadic bind.
-bind :: N.InlineInduction n => Vec n a -> (a -> Vec n b) -> Vec n b
-bind = getBind $ N.inlineInduction1 start step where
+bind :: N.SNatI n => Vec n a -> (a -> Vec n b) -> Vec n b
+bind = getBind $ N.induction1 start step where
     start :: Bind a 'Z b
     start = Bind $ \_ _ -> VNil
 
@@ -805,12 +936,12 @@
 --
 -- >>> join $ ('a' ::: 'b' ::: VNil) ::: ('c' ::: 'd' ::: VNil) ::: VNil
 -- 'a' ::: 'd' ::: VNil
-join :: N.InlineInduction n => Vec n (Vec n a) -> Vec n a
-join = getJoin $ N.inlineInduction1 start step where
+join :: N.SNatI n => Vec n (Vec n a) -> Vec n a
+join = getJoin $ N.induction1 start step where
     start :: Join 'Z a
     start = Join $ \_ -> VNil
 
-    step :: N.InlineInduction m => Join m a -> Join ('S m) a
+    step :: N.SNatI m => Join m a -> Join ('S m) a
     step (Join go) = Join $ \(x ::: xs) -> head x ::: go (map tail xs)
 
 newtype Join n a = Join { getJoin :: Vec n (Vec n a) -> Vec n a }
@@ -823,12 +954,12 @@
 --
 -- >>> universe :: Vec N.Nat3 (Fin N.Nat3)
 -- 0 ::: 1 ::: 2 ::: VNil
-universe :: N.InlineInduction n => Vec n (Fin n)
-universe = getUniverse (N.inlineInduction first step) where
+universe :: N.SNatI n => Vec n (Fin n)
+universe = getUniverse (N.induction first step) where
     first :: Universe 'Z
     first = Universe VNil
 
-    step :: N.InlineInduction m => Universe m -> Universe ('S m)
+    step :: N.SNatI m => Universe m -> Universe ('S m)
     step (Universe go) = Universe (FZ ::: map FS go)
 
 newtype Universe n = Universe { getUniverse :: Vec n (Fin n) }
@@ -858,8 +989,8 @@
 -- >>> head $ setHead 'x' $ ensureSpine v
 -- 'x'
 --
-ensureSpine :: N.InlineInduction n => Vec n a -> Vec n a
-ensureSpine = getEnsureSpine (N.inlineInduction1 first step) where
+ensureSpine :: N.SNatI n => Vec n a -> Vec n a
+ensureSpine = getEnsureSpine (N.induction1 first step) where
     first :: EnsureSpine 'Z a
     first = EnsureSpine $ \_ -> VNil
 
diff --git a/src/Data/Vec/DataFamily/SpineStrict/Pigeonhole.hs b/src/Data/Vec/DataFamily/SpineStrict/Pigeonhole.hs
--- a/src/Data/Vec/DataFamily/SpineStrict/Pigeonhole.hs
+++ b/src/Data/Vec/DataFamily/SpineStrict/Pigeonhole.hs
@@ -6,6 +6,7 @@
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE Safe                  #-}
 {-# LANGUAGE ScopedTypeVariables   #-}
 {-# LANGUAGE TypeFamilies          #-}
 {-# LANGUAGE TypeOperators         #-}
@@ -36,9 +37,9 @@
 import Data.Nat                        (Nat (..))
 import Data.Proxy                      (Proxy (..))
 import Data.Vec.DataFamily.SpineStrict (Vec (..), tabulate)
-import GHC.Generics                    ((:*:) (..), M1 (..), Par1 (..), U1 (..))
+import GHC.Generics                    (M1 (..), Par1 (..), U1 (..), (:*:) (..))
 
-import qualified Control.Lens.Yocto              as Lens
+import qualified Control.Lens.Yocto              as YLens
 import qualified Data.Fin                        as F
 import qualified Data.Fin.Enum                   as F
 import qualified Data.Type.Nat                   as N
@@ -53,9 +54,14 @@
 -- >>> :set -XDeriveGeneric
 -- >>> import Control.Applicative (Const (..))
 -- >>> import Data.Char (toUpper)
+-- >>> import Data.Functor.Identity (Identity (..))
 -- >>> import Data.Void (absurd)
 -- >>> import GHC.Generics (Generic, Generic1)
 -- >>> import Prelude (Int, Show, Char, Integer)
+-- >>> import Data.Proxy (Proxy (..))
+-- >>> import qualified Control.Lens as Lens
+-- >>> import Data.Fin (Fin (..))
+-- >>> import Data.Vec.DataFamily.SpineStrict (Vec (..))
 
 -------------------------------------------------------------------------------
 -- Class
@@ -92,10 +98,13 @@
 instance Pigeonhole Identity
 --
 -- | @'Proxy' x@ ~ @x ^ 0@
-instance Pigeonhole Proxy
+instance Pigeonhole Proxy where
+    type PigeonholeSize Proxy = 'Z
+    from _ = VNil
+    to _   = Proxy
 
 -- | @'Product' f g x@ ~ @x ^ (size f + size g)@
-instance (Pigeonhole f, Pigeonhole g, N.InlineInduction (PigeonholeSize f)) => Pigeonhole (Product f g) where
+instance (Pigeonhole f, Pigeonhole g, N.SNatI (PigeonholeSize f)) => Pigeonhole (Product f g) where
     type PigeonholeSize (Product f g) = N.Plus (PigeonholeSize f) (PigeonholeSize g)
 
     to = f . V.split where f (a, b) = Pair (to a) (to b)
@@ -118,7 +127,7 @@
 --
 gindex
     :: ( G.Generic i, F.GFrom i, G.Generic1 f, GFrom f
-       , F.GEnumSize i ~ GPigeonholeSize f, N.InlineInduction (GPigeonholeSize f)
+       , F.GEnumSize i ~ GPigeonholeSize f, N.SNatI (GPigeonholeSize f)
        )
      => f a -> i -> a
 gindex fa i = gfrom fa V.! F.gfrom i
@@ -136,7 +145,7 @@
 --
 gtabulate
     :: ( G.Generic i, F.GTo i, G.Generic1 f, GTo f
-       , F.GEnumSize i ~ GPigeonholeSize f, N.InlineInduction (GPigeonholeSize f)
+       , F.GEnumSize i ~ GPigeonholeSize f, N.SNatI (GPigeonholeSize f)
        )
      => (i -> a) -> f a
 gtabulate idx = gto $ tabulate (idx . F.gto)
@@ -150,7 +159,7 @@
 -- Identity 'X'
 --
 gix :: ( G.Generic i, F.GFrom i, G.Generic1 t, GTo t, GFrom t
-       , F.GEnumSize i ~ GPigeonholeSize t, N.InlineInduction (GPigeonholeSize t)
+       , F.GEnumSize i ~ GPigeonholeSize t, N.SNatI (GPigeonholeSize t)
        , Functor f
        )
     => i -> (a -> f a) -> t a -> f (t a)
@@ -162,14 +171,8 @@
 
 -- | Index lens.
 --
--- >>> Lens.view (ix (FS FZ)) ('a' ::: 'b' ::: 'c' ::: VNil)
--- 'b'
---
--- >>> Lens.set (ix (FS FZ)) 'x' ('a' ::: 'b' ::: 'c' ::: VNil)
--- 'a' ::: 'x' ::: 'c' ::: VNil
---
-ix :: forall n f a. (N.InlineInduction n, Functor f) => Fin n -> Lens.LensLike' f (Vec n a) a
-ix = getIxLens $ N.inlineInduction1 start step where
+ix :: forall n f a. (N.SNatI n, Functor f) => Fin n -> YLens.LensLike' f (Vec n a) a
+ix = getIxLens $ N.induction1 start step where
     start :: IxLens f 'Z a
     start = IxLens F.absurd
 
@@ -178,14 +181,14 @@
         FZ   -> _head
         FS j -> _tail . l j
 
-newtype IxLens f n a = IxLens { getIxLens :: Fin n -> Lens.LensLike' f (Vec n a) a }
+newtype IxLens f n a = IxLens { getIxLens :: Fin n -> YLens.LensLike' f (Vec n a) a }
 
-_head :: Lens.Lens' (Vec ('S n) a) a
+_head :: YLens.Lens' (Vec ('S n) a) a
 _head f (x ::: xs) = (::: xs) <$> f x
 {-# INLINE _head #-}
 
 -- | Head lens. /Note:/ @lens@ 'Lens._head' is a 'Lens.Traversal''.
-_tail :: Lens.Lens' (Vec ('S n) a) (Vec n a)
+_tail :: YLens.Lens' (Vec ('S n) a) (Vec n a)
 _tail f (x ::: xs) = (x :::) <$> f xs
 {-# INLINE _tail #-}
 
@@ -198,7 +201,7 @@
 -- __Don't use__, rather use @DeriveTraversable@
 gtraverse
     :: ( G.Generic1 t, GFrom t, GTo t
-       , N.InlineInduction (GPigeonholeSize t)
+       , N.SNatI (GPigeonholeSize t)
        , Applicative f
        )
     => (a -> f b) -> t a -> f (t b)
@@ -216,7 +219,7 @@
 gitraverse
     :: ( G.Generic i, F.GTo i
        , G.Generic1 t, GFrom t, GTo t
-       , F.GEnumSize i ~ GPigeonholeSize t, N.InlineInduction (GPigeonholeSize t)
+       , F.GEnumSize i ~ GPigeonholeSize t, N.SNatI (GPigeonholeSize t)
        , Applicative f
        )
     => (i -> a -> f b) -> t a -> f (t b)
diff --git a/src/Data/Vec/Lazy.hs b/src/Data/Vec/Lazy.hs
--- a/src/Data/Vec/Lazy.hs
+++ b/src/Data/Vec/Lazy.hs
@@ -7,6 +7,7 @@
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE GADTs                  #-}
 {-# LANGUAGE RankNTypes             #-}
+{-# LANGUAGE Safe                   #-}
 {-# LANGUAGE ScopedTypeVariables    #-}
 {-# LANGUAGE StandaloneDeriving     #-}
 {-# LANGUAGE TypeFamilies           #-}
@@ -22,6 +23,7 @@
     toPull,
     fromPull,
     toList,
+    toNonEmpty,
     fromList,
     fromListPrefix,
     reifyList,
@@ -31,7 +33,9 @@
     cons,
     snoc,
     head,
+    last,
     tail,
+    init,
     -- * Reverse
     reverse,
     -- * Concatenation and splitting
@@ -40,6 +44,9 @@
     concatMap,
     concat,
     chunks,
+    -- * Take and drop
+    take,
+    drop,
     -- * Folds
     foldMap,
     foldMap1,
@@ -76,14 +83,15 @@
     )  where
 
 import Prelude
-       (Bool (..), Eq (..), Functor (..), Int, Maybe (..), Monad (..),
-       Num (..), Ord (..), Show (..), id, seq, uncurry, showParen, showString, ($), (.))
+       (Bool (..), Eq (..), Functor (..), Int, Maybe (..), Monad (..), Num (..),
+       Ord (..), Show (..), id, seq, showParen, showString, uncurry, ($), (.), (&&), Ordering (..))
 
 import Control.Applicative (Applicative (..), (<$>))
 import Control.DeepSeq     (NFData (..))
 import Control.Lens.Yocto  ((<&>))
 import Data.Fin            (Fin (..))
 import Data.Hashable       (Hashable (..))
+import Data.List.NonEmpty  (NonEmpty (..))
 import Data.Monoid         (Monoid (..))
 import Data.Nat            (Nat (..))
 import Data.Semigroup      (Semigroup (..))
@@ -94,6 +102,12 @@
 import qualified Data.Traversable as I (Traversable (..))
 import qualified Test.QuickCheck  as QC
 
+import qualified Data.Foldable.WithIndex    as WI (FoldableWithIndex (..))
+import qualified Data.Functor.WithIndex     as WI (FunctorWithIndex (..))
+import qualified Data.Traversable.WithIndex as WI (TraversableWithIndex (..))
+
+import Data.Functor.Classes (Eq1 (..), Ord1 (..), Show1 (..))
+
 #ifdef MIN_VERSION_adjunctions
 import qualified Data.Functor.Rep as I (Representable (..))
 #endif
@@ -115,10 +129,16 @@
 import qualified Data.Type.Nat as N
 import qualified Data.Vec.Pull as P
 
+import qualified Data.Type.Nat.LE          as LE.ZS
+import qualified Data.Type.Nat.LE.ReflStep as LE.RS
+
+
 -- $setup
 -- >>> :set -XScopedTypeVariables
 -- >>> import Data.Proxy (Proxy (..))
--- >>> import Prelude (Char, not, uncurry)
+-- >>> import Prelude (Char, not, uncurry, Bool (..), Maybe (..), ($), (<$>), id, (.), Int)
+-- >>> import qualified Data.Type.Nat as N
+-- >>> import Data.Fin (Fin (..))
 
 -------------------------------------------------------------------------------
 -- Type
@@ -165,6 +185,19 @@
 instance I.Traversable (Vec n) where
     traverse = traverse
 
+-- | @since 0.4
+instance WI.FunctorWithIndex (Fin n) (Vec n) where
+    imap = imap
+
+-- | @since 0.4
+instance WI.FoldableWithIndex (Fin n) (Vec n) where
+    ifoldMap = ifoldMap
+    ifoldr   = ifoldr
+
+-- | @since 0.4
+instance WI.TraversableWithIndex (Fin n) (Vec n) where
+    itraverse = itraverse
+
 #ifdef MIN_VERSION_semigroupoids
 instance n ~ 'S m => I.Foldable1 (Vec n) where
     foldMap1 = foldMap1
@@ -229,6 +262,55 @@
 #endif
 
 -------------------------------------------------------------------------------
+-- Data.Functor.Classes
+-------------------------------------------------------------------------------
+
+#ifndef MIN_VERSION_transformers_compat
+#define MIN_VERSION_transformers_compat(x,y,z) 0
+#endif
+
+#if MIN_VERSION_base(4,9,0)
+#define LIFTED_FUNCTOR_CLASSES 1
+#else
+#if MIN_VERSION_transformers(0,5,0)
+#define LIFTED_FUNCTOR_CLASSES 1
+#else
+#if MIN_VERSION_transformers_compat(0,5,0) && !MIN_VERSION_transformers(0,4,0)
+#define LIFTED_FUNCTOR_CLASSES 1
+#endif
+#endif
+#endif
+
+#if LIFTED_FUNCTOR_CLASSES
+-- | @since 0.4
+instance Eq1 (Vec n) where
+    liftEq _eq VNil       VNil       = True
+    liftEq  eq (x ::: xs) (y ::: ys) = eq x y && liftEq eq xs ys
+
+-- | @since 0.4
+instance Ord1 (Vec n) where
+    liftCompare _cmp VNil       VNil       = EQ
+    liftCompare  cmp (x ::: xs) (y ::: ys) = cmp x y <> liftCompare cmp xs ys
+
+-- | @since 0.4
+instance Show1 (Vec n) where
+    liftShowsPrec _  _  _ VNil       = showString "VNil"
+    liftShowsPrec sp sl d (x ::: xs) = showParen (d > 5)
+        $ sp 6 x
+        . showString " ::: "
+        . liftShowsPrec sp sl 5 xs
+#else
+-- | @since 0.4
+instance Eq1 (Vec n) where eq1 = (==)
+
+-- | @since 0.4
+instance Ord1 (Vec n) where compare1 = compare
+
+-- | @since 0.4
+instance Show1 (Vec n) where showsPrec1 = showsPrec
+#endif
+
+-------------------------------------------------------------------------------
 -- Construction
 -------------------------------------------------------------------------------
 
@@ -244,7 +326,7 @@
 singleton :: a -> Vec ('S 'Z) a
 singleton x = x ::: VNil
 
--- | /O(n)/. Recover 'N.InlineInduction' (and 'N.SNatI') dictionary from a 'Vec' value.
+-- | /O(n)/. Recover 'N.SNatI' (and 'N.SNatI') dictionary from a 'Vec' value.
 --
 -- Example: 'N.reflect' is constrained with @'N.SNatI' n@, but if we have a
 -- @'Vec' n a@, we can recover that dictionary:
@@ -252,11 +334,11 @@
 -- >>> let f :: forall n a. Vec n a -> N.Nat; f v = withDict v (N.reflect (Proxy :: Proxy n)) in f (True ::: VNil)
 -- 1
 --
--- /Note:/ using 'N.InlineInduction' will be suboptimal, as if GHC has no
+-- /Note:/ using 'N.SNatI' will be suboptimal, as if GHC has no
 -- opportunity to optimise the code, the recusion won't be unfold.
 -- How bad such code will perform? I don't know, we'll need benchmarks.
 --
-withDict :: Vec n a -> (N.InlineInduction n => r) -> r
+withDict :: Vec n a -> (N.SNatI n => r) -> r
 withDict VNil       r = r
 withDict (_ ::: xs) r = withDict xs r
 
@@ -285,6 +367,15 @@
 toList VNil       = []
 toList (x ::: xs) = x : toList xs
 
+-- |  
+--
+-- >>> toNonEmpty $ 1 ::: 2 ::: 3 ::: VNil
+-- 1 :| [2,3]
+--
+-- @since 0.4
+toNonEmpty :: Vec ('S n) a -> NonEmpty a
+toNonEmpty (x ::: xs) = x :| toList xs
+
 -- | Convert list @[a]@ to @'Vec' n a@.
 -- Returns 'Nothing' if lengths don't match exactly.
 --
@@ -337,7 +428,7 @@
 --
 -- >>> reifyList "foo" length
 -- 3
-reifyList :: [a] -> (forall n. N.InlineInduction n => Vec n a -> r) -> r
+reifyList :: [a] -> (forall n. N.SNatI n => Vec n a -> r) -> r
 reifyList []       f = f VNil
 reifyList (x : xs) f = reifyList xs $ \xs' -> f (x ::: xs')
 
@@ -378,10 +469,24 @@
 head :: Vec ('S n) a -> a
 head (x ::: _) = x
 
+-- | The last element of a 'Vec'.
+--
+-- @since 0.4
+last :: Vec ('S n) a -> a
+last (x ::: VNil) = x
+last (_ ::: xs@(_ ::: _)) = last xs
+
 -- | The elements after the 'head' of a 'Vec'.
 tail :: Vec ('S n) a -> Vec n a
 tail (_ ::: xs) = xs
 
+-- | The elements before the 'last' of a 'Vec'.
+--
+-- @since 0.4
+init :: Vec ('S n) a -> Vec n a
+init (_ ::: VNil) = VNil
+init (x ::: xs@(_ ::: _)) = x ::: init xs
+
 -------------------------------------------------------------------------------
 -- Reverse
 -------------------------------------------------------------------------------
@@ -466,6 +571,34 @@
 newtype Chunks  m n a = Chunks  { getChunks  :: Vec (N.Mult n m) a -> Vec n (Vec m a) }
 
 -------------------------------------------------------------------------------
+-- take and drop
+-------------------------------------------------------------------------------
+
+-- |
+--
+-- >>> let xs = 'a' ::: 'b' ::: 'c' ::: 'd' ::: 'e' ::: VNil
+-- >>> take xs :: Vec N.Nat3 Char
+-- 'a' ::: 'b' ::: 'c' ::: VNil
+--
+take :: forall n m a. (LE.ZS.LE n m) => Vec m a -> Vec n a
+take = go LE.ZS.leProof where
+    go :: LE.ZS.LEProof n' m' -> Vec m' a -> Vec n' a
+    go LE.ZS.LEZero _              = VNil
+    go (LE.ZS.LESucc p) (x ::: xs) = x ::: go p xs
+
+-- |
+--
+-- >>> let xs = 'a' ::: 'b' ::: 'c' ::: 'd' ::: 'e' ::: VNil
+-- >>> drop xs :: Vec N.Nat3 Char
+-- 'c' ::: 'd' ::: 'e' ::: VNil
+--
+drop :: forall n m a. (LE.ZS.LE n m, N.SNatI m) => Vec m a -> Vec n a
+drop = go (LE.RS.fromZeroSucc LE.ZS.leProof) where
+    go :: LE.RS.LEProof n' m' -> Vec m' a -> Vec n' a
+    go LE.RS.LERefl xs             = xs
+    go (LE.RS.LEStep p) (_ ::: xs) = go p xs
+
+-------------------------------------------------------------------------------
 -- Mapping
 -------------------------------------------------------------------------------
 
@@ -576,7 +709,7 @@
 -- | Non-strict 'product'.
 product :: Num a => Vec n a -> a
 product VNil       = 1
-product (x ::: xs) = x * sum xs
+product (x ::: xs) = x * product xs
 
 -------------------------------------------------------------------------------
 -- Zipping
@@ -663,8 +796,8 @@
 -- there's no strict need for it.
 --
 class VecEach s t a b | s -> a, t -> b, s b -> t, t a -> s where
-    mapWithVec :: (forall n. N.InlineInduction n => Vec n a -> Vec n b) -> s -> t
-    traverseWithVec :: Applicative f => (forall n. N.InlineInduction n => Vec n a -> f (Vec n b)) -> s -> f t
+    mapWithVec :: (forall n. N.SNatI n => Vec n a -> Vec n b) -> s -> t
+    traverseWithVec :: Applicative f => (forall n. N.SNatI n => Vec n a -> f (Vec n b)) -> s -> f t
 
 instance (a ~ a', b ~ b') => VecEach (a, a') (b, b') a b where
     mapWithVec f ~(x, y) = case f (x ::: y ::: VNil) of
diff --git a/src/Data/Vec/Lazy/Inline.hs b/src/Data/Vec/Lazy/Inline.hs
--- a/src/Data/Vec/Lazy/Inline.hs
+++ b/src/Data/Vec/Lazy/Inline.hs
@@ -4,10 +4,11 @@
 {-# LANGUAGE GADTs                 #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE Safe                  #-}
 {-# LANGUAGE ScopedTypeVariables   #-}
 {-# LANGUAGE TypeFamilies          #-}
 {-# LANGUAGE UndecidableInstances  #-}
--- | A variant of "Data.Vec.Lazy" with functions written using 'N.InlineInduction'.
+-- | A variant of "Data.Vec.Lazy" with functions written using 'N.SNatI'.
 -- The hypothesis is that these (goursive) functions could be fully unrolled,
 -- if the 'Vec' size @n@ is known at compile time.
 --
@@ -22,6 +23,7 @@
     toPull,
     fromPull,
     toList,
+    toNonEmpty,
     fromList,
     fromListPrefix,
     reifyList,
@@ -31,7 +33,9 @@
     cons,
     snoc,
     head,
+    last,
     tail,
+    init,
     -- * Concatenation and splitting
     (++),
     split,
@@ -78,6 +82,7 @@
 
 import Control.Applicative (Applicative (pure, (*>)), liftA2, (<$>))
 import Data.Fin            (Fin (..))
+import Data.List.NonEmpty  (NonEmpty (..))
 import Data.Monoid         (Monoid (..))
 import Data.Nat            (Nat (..))
 import Data.Semigroup      (Semigroup (..))
@@ -88,7 +93,7 @@
 --- Instances
 
 #ifdef MIN_VERSION_semigroupoids
-import Data.Functor.Apply  (Apply, liftF2)
+import Data.Functor.Apply (Apply, liftF2)
 #endif
 
 -- vec siblings
@@ -99,15 +104,17 @@
 -- $setup
 -- >>> :set -XScopedTypeVariables
 -- >>> import Data.Proxy (Proxy (..))
--- >>> import Prelude (Char, not, uncurry, Bool (..))
+-- >>> import Prelude (Char, not, uncurry, Bool (..), Maybe (..), ($), (<$>), id, (.), Int)
+-- >>> import qualified Data.Type.Nat as N
+-- >>> import Data.Fin (Fin (..))
 
 -------------------------------------------------------------------------------
 -- Conversions
 -------------------------------------------------------------------------------
 
 -- | Convert to pull 'P.Vec'.
-toPull :: forall n a. N.InlineInduction n => Vec n a -> P.Vec n a
-toPull = getToPull (N.inlineInduction1 start step) where
+toPull :: forall n a. N.SNatI n => Vec n a -> P.Vec n a
+toPull = getToPull (N.induction1 start step) where
     start :: ToPull 'Z a
     start = ToPull $ \_ -> P.Vec F.absurd
 
@@ -119,8 +126,8 @@
 newtype ToPull n a = ToPull { getToPull :: Vec n a -> P.Vec n a }
 
 -- | Convert from pull 'P.Vec'.
-fromPull :: forall n a. N.InlineInduction n => P.Vec n a -> Vec n a
-fromPull = getFromPull (N.inlineInduction1 start step) where
+fromPull :: forall n a. N.SNatI n => P.Vec n a -> Vec n a
+fromPull = getFromPull (N.induction1 start step) where
     start :: FromPull 'Z a
     start = FromPull $ const VNil
 
@@ -133,8 +140,8 @@
 --
 -- >>> toList $ 'f' ::: 'o' ::: 'o' ::: VNil
 -- "foo"
-toList :: forall n a. N.InlineInduction n => Vec n a -> [a]
-toList = getToList (N.inlineInduction1 start step) where
+toList :: forall n a. N.SNatI n => Vec n a -> [a]
+toList = getToList (N.induction1 start step) where
     start :: ToList 'Z a
     start = ToList (const [])
 
@@ -143,6 +150,15 @@
 
 newtype ToList n a = ToList { getToList :: Vec n a -> [a] }
 
+-- |
+--
+-- >>> toNonEmpty $ 1 ::: 2 ::: 3 ::: VNil
+-- 1 :| [2,3]
+--
+-- @since 0.4
+toNonEmpty :: forall n a. N.SNatI n => Vec ('S n) a -> NonEmpty a
+toNonEmpty (x ::: xs) = x :| toList xs
+
 -- | Convert list @[a]@ to @'Vec' n a@.
 -- Returns 'Nothing' if lengths don't match exactly.
 --
@@ -155,8 +171,8 @@
 -- >>> fromList "xy" :: Maybe (Vec N.Nat3 Char)
 -- Nothing
 --
-fromList :: N.InlineInduction n => [a] -> Maybe (Vec n a)
-fromList = getFromList (N.inlineInduction1 start step) where
+fromList :: N.SNatI n => [a] -> Maybe (Vec n a)
+fromList = getFromList (N.induction1 start step) where
     start :: FromList 'Z a
     start = FromList $ \xs -> case xs of
         []      -> Just VNil
@@ -181,8 +197,8 @@
 -- >>> fromListPrefix "xy" :: Maybe (Vec N.Nat3 Char)
 -- Nothing
 --
-fromListPrefix :: N.InlineInduction n => [a] -> Maybe (Vec n a)
-fromListPrefix = getFromList (N.inlineInduction1 start step) where
+fromListPrefix :: N.SNatI n => [a] -> Maybe (Vec n a)
+fromListPrefix = getFromList (N.induction1 start step) where
     start :: FromList 'Z a
     start = FromList $ \_ -> Just VNil -- different than in fromList case
 
@@ -195,8 +211,8 @@
 -- Indexing
 -------------------------------------------------------------------------------
 
-flipIndex :: N.InlineInduction n => Fin n -> Vec n a -> a
-flipIndex = getIndex (N.inlineInduction1 start step) where
+flipIndex :: N.SNatI n => Fin n -> Vec n a -> a
+flipIndex = getIndex (N.induction1 start step) where
     start :: Index 'Z a
     start = Index F.absurd
 
@@ -212,7 +228,7 @@
 -- >>> ('a' ::: 'b' ::: 'c' ::: VNil) ! FS FZ
 -- 'b'
 --
-(!) :: N.InlineInduction n => Vec n a -> Fin n -> a
+(!) :: N.SNatI n => Vec n a -> Fin n -> a
 (!) = flip flipIndex
 
 -- | Tabulating, inverse of '!'.
@@ -220,15 +236,15 @@
 -- >>> tabulate id :: Vec N.Nat3 (Fin N.Nat3)
 -- 0 ::: 1 ::: 2 ::: VNil
 --
-tabulate :: N.InlineInduction n => (Fin n -> a) -> Vec n a
+tabulate :: N.SNatI n => (Fin n -> a) -> Vec n a
 tabulate = fromPull . P.tabulate
 
 -- | Add a single element at the end of a 'Vec'.
 --
 -- @since 0.2.1
 --
-snoc :: forall n a. N.InlineInduction n => Vec n a -> a -> Vec ('S n) a
-snoc xs x = getSnoc (N.inlineInduction1 start step) xs where
+snoc :: forall n a. N.SNatI n => Vec n a -> a -> Vec ('S n) a
+snoc xs x = getSnoc (N.induction1 start step) xs where
     start :: Snoc 'Z a
     start = Snoc $ \ys -> x ::: ys
 
@@ -237,6 +253,33 @@
 
 newtype Snoc n a = Snoc { getSnoc :: Vec n a -> Vec ('S n) a }
 
+-- | The last element of a 'Vec'.
+--
+-- @since 0.4
+last :: forall n a. N.SNatI n => Vec ('S n) a -> a
+last xs = getLast (N.induction1 start step) xs where
+    start :: Last 'Z a
+    start = Last $ \(x:::VNil) -> x
+    
+    step :: Last m a -> Last ('S m) a
+    step (Last rec) = Last $ \(_ ::: ys) -> rec ys
+    
+
+newtype Last n a = Last { getLast :: Vec ('S n) a -> a }
+
+-- | The elements before the 'last' of a 'Vec'.
+--
+-- @since 0.4
+init :: forall n a. N.SNatI n => Vec ('S n) a -> Vec n a
+init xs = getInit (N.induction1 start step) xs where
+    start :: Init 'Z a
+    start = Init (const VNil)
+    
+    step :: Init m a -> Init ('S m) a
+    step (Init rec) = Init $ \(y ::: ys) -> y ::: rec ys
+
+newtype Init n a = Init { getInit :: Vec ('S n) a -> Vec n a}
+
 -------------------------------------------------------------------------------
 -- Reverse
 -------------------------------------------------------------------------------
@@ -248,12 +291,12 @@
 --
 -- @since 0.2.1
 --
-reverse :: forall n a. N.InlineInduction n => Vec n a -> Vec n a
-reverse = getReverse (N.inlineInduction1 start step) where
+reverse :: forall n a. N.SNatI n => Vec n a -> Vec n a
+reverse = getReverse (N.induction1 start step) where
     start :: Reverse 'Z a
     start = Reverse $ \_ -> VNil
 
-    step :: N.InlineInduction m => Reverse m a -> Reverse ('S m) a
+    step :: N.SNatI m => Reverse m a -> Reverse ('S m) a
     step (Reverse rec) = Reverse $ \(x ::: xs) -> snoc (rec xs) x
 
 newtype Reverse n a = Reverse { getReverse :: Vec n a -> Vec n a }
@@ -269,8 +312,8 @@
 -- >>> ('a' ::: 'b' ::: VNil) ++ ('c' ::: 'd' ::: VNil)
 -- 'a' ::: 'b' ::: 'c' ::: 'd' ::: VNil
 --
-(++) :: forall n m a. N.InlineInduction n => Vec n a -> Vec m a -> Vec (N.Plus n m) a
-as ++ ys = getAppend (N.inlineInduction1 start step) as where
+(++) :: forall n m a. N.SNatI n => Vec n a -> Vec m a -> Vec (N.Plus n m) a
+as ++ ys = getAppend (N.induction1 start step) as where
     start :: Append m 'Z a
     start = Append $ \_ -> ys
 
@@ -287,8 +330,8 @@
 -- >>> uncurry (++) (split ('a' ::: 'b' ::: 'c' ::: VNil) :: (Vec N.Nat1 Char, Vec N.Nat2 Char))
 -- 'a' ::: 'b' ::: 'c' ::: VNil
 --
-split :: N.InlineInduction n => Vec (N.Plus n m) a -> (Vec n a, Vec m a)
-split = appSplit (N.inlineInduction1 start step) where
+split :: N.SNatI n => Vec (N.Plus n m) a -> (Vec n a, Vec m a)
+split = appSplit (N.induction1 start step) where
     start :: Split m 'Z a
     start = Split $ \xs -> (VNil, xs)
 
@@ -302,8 +345,8 @@
 -- >>> concatMap (\x -> x ::: x ::: VNil) ('a' ::: 'b' ::: VNil)
 -- 'a' ::: 'a' ::: 'b' ::: 'b' ::: VNil
 --
-concatMap :: forall a b n m. (N.InlineInduction m, N.InlineInduction n) => (a -> Vec m b) -> Vec n a -> Vec (N.Mult n m) b
-concatMap f = getConcatMap $ N.inlineInduction1 start step where
+concatMap :: forall a b n m. (N.SNatI m, N.SNatI n) => (a -> Vec m b) -> Vec n a -> Vec (N.Mult n m) b
+concatMap f = getConcatMap $ N.induction1 start step where
     start :: ConcatMap m a 'Z b
     start = ConcatMap $ \_ -> VNil
 
@@ -313,7 +356,7 @@
 newtype ConcatMap m a n b = ConcatMap { getConcatMap :: Vec n a -> Vec (N.Mult n m) b }
 
 -- | @'concatMap' 'id'@
-concat :: (N.InlineInduction m, N.InlineInduction n) => Vec n (Vec m a) -> Vec (N.Mult n m) a
+concat :: (N.SNatI m, N.SNatI n) => Vec n (Vec m a) -> Vec (N.Mult n m) a
 concat = concatMap id
 
 -- | Inverse of 'concat'.
@@ -325,12 +368,12 @@
 -- >>> concat . idVec . chunks <$> fromListPrefix [1..]
 -- Just (1 ::: 2 ::: 3 ::: 4 ::: 5 ::: 6 ::: VNil)
 --
-chunks :: (N.InlineInduction n, N.InlineInduction m) => Vec (N.Mult n m) a -> Vec n (Vec m a)
+chunks :: (N.SNatI n, N.SNatI m) => Vec (N.Mult n m) a -> Vec n (Vec m a)
 chunks = getChunks $ N.induction1 start step where
     start :: Chunks m 'Z a
     start = Chunks $ \_ -> VNil
 
-    step :: forall m n a. N.InlineInduction m => Chunks m n a -> Chunks m ('S n) a
+    step :: forall m n a. N.SNatI m => Chunks m n a -> Chunks m ('S n) a
     step (Chunks go) = Chunks $ \xs ->
         let (ys, zs) = split xs :: (Vec m a, Vec (N.Mult n m) a)
         in ys ::: go zs
@@ -344,8 +387,8 @@
 -- | >>> map not $ True ::: False ::: VNil
 -- False ::: True ::: VNil
 --
-map :: forall a b n. N.InlineInduction n => (a -> b) -> Vec n a -> Vec n b
-map f = getMap $ N.inlineInduction1 start step where
+map :: forall a b n. N.SNatI n => (a -> b) -> Vec n a -> Vec n b
+map f = getMap $ N.induction1 start step where
     start :: Map a 'Z b
     start = Map $ \_ -> VNil
 
@@ -357,8 +400,8 @@
 -- | >>> imap (,) $ 'a' ::: 'b' ::: 'c' ::: VNil
 -- (0,'a') ::: (1,'b') ::: (2,'c') ::: VNil
 --
-imap :: N.InlineInduction n => (Fin n -> a -> b) -> Vec n a -> Vec n b
-imap = getIMap $ N.inlineInduction1 start step where
+imap :: N.SNatI n => (Fin n -> a -> b) -> Vec n a -> Vec n b
+imap = getIMap $ N.induction1 start step where
     start :: IMap a 'Z b
     start = IMap $ \_ _ -> VNil
 
@@ -368,8 +411,8 @@
 newtype IMap a n b = IMap { getIMap :: (Fin n -> a -> b) -> Vec n a -> Vec n b }
 
 -- | Apply an action to every element of a 'Vec', yielding a 'Vec' of results.
-traverse :: forall n f a b. (Applicative f, N.InlineInduction n) => (a -> f b) -> Vec n a -> f (Vec n b)
-traverse f =  getTraverse $ N.inlineInduction1 start step where
+traverse :: forall n f a b. (Applicative f, N.SNatI n) => (a -> f b) -> Vec n a -> f (Vec n b)
+traverse f =  getTraverse $ N.induction1 start step where
     start :: Traverse f a 'Z b
     start = Traverse $ \_ -> pure VNil
 
@@ -380,8 +423,8 @@
 
 #ifdef MIN_VERSION_semigroupoids
 -- | Apply an action to non-empty 'Vec', yielding a 'Vec' of results.
-traverse1 :: forall n f a b. (Apply f, N.InlineInduction n) => (a -> f b) -> Vec ('S n) a -> f (Vec ('S n) b)
-traverse1 f = getTraverse1 $ N.inlineInduction1 start step where
+traverse1 :: forall n f a b. (Apply f, N.SNatI n) => (a -> f b) -> Vec ('S n) a -> f (Vec ('S n) b)
+traverse1 f = getTraverse1 $ N.induction1 start step where
     start :: Traverse1 f a 'Z b
     start = Traverse1 $ \(x ::: _) -> (::: VNil) <$> f x
 
@@ -392,8 +435,8 @@
 #endif
 
 -- | Apply an action to every element of a 'Vec' and its index, yielding a 'Vec' of results.
-itraverse :: forall n f a b. (Applicative f, N.InlineInduction n) => (Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
-itraverse = getITraverse $ N.inlineInduction1 start step where
+itraverse :: forall n f a b. (Applicative f, N.SNatI n) => (Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
+itraverse = getITraverse $ N.induction1 start step where
     start :: ITraverse f a 'Z b
     start = ITraverse $ \_ _ -> pure VNil
 
@@ -403,8 +446,8 @@
 newtype ITraverse f a n b = ITraverse { getITraverse :: (Fin n -> a -> f b) -> Vec n a -> f (Vec n b) }
 
 -- | Apply an action to every element of a 'Vec' and its index, ignoring the results.
-itraverse_ :: forall n f a b. (Applicative f, N.InlineInduction n) => (Fin n -> a -> f b) -> Vec n a -> f ()
-itraverse_ = getITraverse_ $ N.inlineInduction1 start step where
+itraverse_ :: forall n f a b. (Applicative f, N.SNatI n) => (Fin n -> a -> f b) -> Vec n a -> f ()
+itraverse_ = getITraverse_ $ N.induction1 start step where
     start :: ITraverse_ f a 'Z b
     start = ITraverse_ $ \_ _ -> pure ()
 
@@ -418,15 +461,15 @@
 -------------------------------------------------------------------------------
 
 -- | See 'I.Foldable'.
-foldMap :: (Monoid m, N.InlineInduction n) => (a -> m) -> Vec n a -> m
-foldMap f = getFold $ N.inlineInduction1 (Fold (const mempty)) $ \(Fold go) ->
+foldMap :: (Monoid m, N.SNatI n) => (a -> m) -> Vec n a -> m
+foldMap f = getFold $ N.induction1 (Fold (const mempty)) $ \(Fold go) ->
     Fold $ \(x ::: xs) -> f x `mappend` go xs
 
 newtype Fold  a n b = Fold  { getFold  :: Vec n a -> b }
 
 -- | See 'I.Foldable1'.
-foldMap1 :: forall s a n. (Semigroup s, N.InlineInduction n) => (a -> s) -> Vec ('S n) a -> s
-foldMap1 f = getFold1 $ N.inlineInduction1 start step where
+foldMap1 :: forall s a n. (Semigroup s, N.SNatI n) => (a -> s) -> Vec ('S n) a -> s
+foldMap1 f = getFold1 $ N.induction1 start step where
     start :: Fold1 a 'Z s
     start = Fold1 $ \(x ::: _) -> f x
 
@@ -436,8 +479,8 @@
 newtype Fold1 a n b = Fold1 { getFold1 :: Vec ('S n) a -> b }
 
 -- | See 'I.FoldableWithIndex'.
-ifoldMap :: forall a n m. (Monoid m, N.InlineInduction n) => (Fin n -> a -> m) -> Vec n a -> m
-ifoldMap = getIFoldMap $ N.inlineInduction1 start step where
+ifoldMap :: forall a n m. (Monoid m, N.SNatI n) => (Fin n -> a -> m) -> Vec n a -> m
+ifoldMap = getIFoldMap $ N.induction1 start step where
     start :: IFoldMap a 'Z m
     start = IFoldMap $ \_ _ -> mempty
 
@@ -447,8 +490,8 @@
 newtype IFoldMap a n m = IFoldMap { getIFoldMap :: (Fin n -> a -> m) -> Vec n a -> m }
 
 -- | There is no type-class for this :(
-ifoldMap1 :: forall a n s. (Semigroup s, N.InlineInduction n) => (Fin ('S n) -> a -> s) -> Vec ('S n) a -> s
-ifoldMap1 = getIFoldMap1 $ N.inlineInduction1 start step where
+ifoldMap1 :: forall a n s. (Semigroup s, N.SNatI n) => (Fin ('S n) -> a -> s) -> Vec ('S n) a -> s
+ifoldMap1 = getIFoldMap1 $ N.induction1 start step where
     start :: IFoldMap1 a 'Z s
     start = IFoldMap1 $ \f (x ::: _) -> f FZ x
 
@@ -458,8 +501,8 @@
 newtype IFoldMap1 a n m = IFoldMap1 { getIFoldMap1 :: (Fin ('S n) -> a -> m) -> Vec ('S n) a -> m }
 
 -- | Right fold.
-foldr :: forall a b n. N.InlineInduction n => (a -> b -> b) -> b -> Vec n a -> b
-foldr f z = getFold $ N.inlineInduction1 start step where
+foldr :: forall a b n. N.SNatI n => (a -> b -> b) -> b -> Vec n a -> b
+foldr f z = getFold $ N.induction1 start step where
     start :: Fold a 'Z b
     start = Fold $ \_ -> z
 
@@ -467,8 +510,8 @@
     step (Fold go) = Fold $ \(x ::: xs) -> f x (go xs)
 
 -- | Right fold with an index.
-ifoldr :: forall a b n. N.InlineInduction n => (Fin n -> a -> b -> b) -> b -> Vec n a -> b
-ifoldr = getIFoldr $ N.inlineInduction1 start step where
+ifoldr :: forall a b n. N.SNatI n => (Fin n -> a -> b -> b) -> b -> Vec n a -> b
+ifoldr = getIFoldr $ N.induction1 start step where
     start :: IFoldr a 'Z b
     start = IFoldr $ \_ z _ -> z
 
@@ -478,10 +521,10 @@
 newtype IFoldr a n b = IFoldr { getIFoldr :: (Fin n -> a -> b -> b) -> b -> Vec n a -> b }
 
 -- | Yield the length of a 'Vec'. /O(n)/
-length :: forall n a. N.InlineInduction n => Vec n a -> Int
+length :: forall n a. N.SNatI n => Vec n a -> Int
 length _ = getLength l where
     l :: Length n
-    l = N.inlineInduction (Length 0) $ \(Length n) -> Length (1 + n)
+    l = N.induction (Length 0) $ \(Length n) -> Length (1 + n)
 
 newtype Length (n :: Nat) = Length { getLength :: Int }
 
@@ -490,8 +533,8 @@
 -------------------------------------------------------------------------------
 
 -- | Non-strict 'sum'.
-sum :: (Num a, N.InlineInduction n) => Vec n a -> a
-sum = getFold $ N.inlineInduction1 start step where
+sum :: (Num a, N.SNatI n) => Vec n a -> a
+sum = getFold $ N.induction1 start step where
     start :: Num a => Fold a 'Z a
     start = Fold $ \_ -> 0
 
@@ -499,21 +542,21 @@
     step (Fold f) = Fold $ \(x ::: xs) -> x + f xs
 
 -- | Non-strict 'product'.
-product :: (Num a, N.InlineInduction n) => Vec n a -> a
-product = getFold $ N.inlineInduction1 start step where
+product :: (Num a, N.SNatI n) => Vec n a -> a
+product = getFold $ N.induction1 start step where
     start :: Num a => Fold a 'Z a
-    start = Fold $ \_ -> 0
+    start = Fold $ \_ -> 1
 
     step :: Num a => Fold a m a -> Fold a ('S m) a
-    step (Fold f) = Fold $ \(x ::: xs) -> x + f xs
+    step (Fold f) = Fold $ \(x ::: xs) -> x * f xs
 
 -------------------------------------------------------------------------------
 -- Zipping
 -------------------------------------------------------------------------------
 
 -- | Zip two 'Vec's with a function.
-zipWith :: forall a b c n. N.InlineInduction n => (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
-zipWith f = getZipWith $ N.inlineInduction start step where
+zipWith :: forall a b c n. N.SNatI n => (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
+zipWith f = getZipWith $ N.induction start step where
     start :: ZipWith a b c 'Z
     start = ZipWith $ \_ _ -> VNil
 
@@ -523,8 +566,8 @@
 newtype ZipWith a b c n = ZipWith { getZipWith :: Vec n a -> Vec n b -> Vec n c }
 
 -- | Zip two 'Vec's. with a function that also takes the elements' indices.
-izipWith :: N.InlineInduction n => (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
-izipWith = getIZipWith $ N.inlineInduction start step where
+izipWith :: N.SNatI n => (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
+izipWith = getIZipWith $ N.induction start step where
     start :: IZipWith a b c 'Z
     start = IZipWith $ \_ _ _ -> VNil
 
@@ -539,16 +582,16 @@
 -- 'x' ::: 'x' ::: 'x' ::: VNil
 --
 -- @since 0.2.1
-repeat :: N.InlineInduction n => x -> Vec n x
-repeat x = N.inlineInduction1 VNil (x :::)
+repeat :: N.SNatI n => x -> Vec n x
+repeat x = N.induction1 VNil (x :::)
 
 -------------------------------------------------------------------------------
 -- Monadic
 -------------------------------------------------------------------------------
 
 -- | Monadic bind.
-bind :: N.InlineInduction n => Vec n a -> (a -> Vec n b) -> Vec n b
-bind = getBind $ N.inlineInduction1 start step where
+bind :: N.SNatI n => Vec n a -> (a -> Vec n b) -> Vec n b
+bind = getBind $ N.induction1 start step where
     start :: Bind a 'Z b
     start = Bind $ \_ _ -> VNil
 
@@ -561,12 +604,12 @@
 --
 -- >>> join $ ('a' ::: 'b' ::: VNil) ::: ('c' ::: 'd' ::: VNil) ::: VNil
 -- 'a' ::: 'd' ::: VNil
-join :: N.InlineInduction n => Vec n (Vec n a) -> Vec n a
-join = getJoin $ N.inlineInduction1 start step where
+join :: N.SNatI n => Vec n (Vec n a) -> Vec n a
+join = getJoin $ N.induction1 start step where
     start :: Join 'Z a
     start = Join $ \_ -> VNil
 
-    step :: N.InlineInduction m => Join m a -> Join ('S m) a
+    step :: N.SNatI m => Join m a -> Join ('S m) a
     step (Join go) = Join $ \(x ::: xs) -> head x ::: go (map tail xs)
 
 newtype Join n a = Join { getJoin :: Vec n (Vec n a) -> Vec n a }
@@ -579,12 +622,12 @@
 --
 -- >>> universe :: Vec N.Nat3 (Fin N.Nat3)
 -- 0 ::: 1 ::: 2 ::: VNil
-universe :: N.InlineInduction n => Vec n (Fin n)
-universe = getUniverse (N.inlineInduction first step) where
+universe :: N.SNatI n => Vec n (Fin n)
+universe = getUniverse (N.induction first step) where
     first :: Universe 'Z
     first = Universe VNil
 
-    step :: N.InlineInduction m => Universe m -> Universe ('S m)
+    step :: N.SNatI m => Universe m -> Universe ('S m)
     step (Universe go) = Universe (FZ ::: map FS go)
 
 newtype Universe n = Universe { getUniverse :: Vec n (Fin n) }
diff --git a/src/Data/Vec/Pull.hs b/src/Data/Vec/Pull.hs
--- a/src/Data/Vec/Pull.hs
+++ b/src/Data/Vec/Pull.hs
@@ -4,6 +4,7 @@
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PolyKinds             #-}
 {-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE Safe                  #-}
 {-# LANGUAGE ScopedTypeVariables   #-}
 {-# LANGUAGE TypeFamilies          #-}
 {-# LANGUAGE UndecidableInstances  #-}
@@ -19,6 +20,7 @@
     singleton,
     -- * Conversions
     toList,
+    toNonEmpty,
     fromList,
     fromListPrefix,
     reifyList,
@@ -28,7 +30,9 @@
     cons,
     snoc,
     head,
+    last,
     tail,
+    init,
     -- * Reverse
     reverse,
     -- * Folds
@@ -59,8 +63,8 @@
     ) where
 
 import Prelude
-       (Bool (..), Eq (..), Functor (..), Int, Maybe (..), Monad (..),
-       Num (..), all, const, id, ($), (.))
+       (Bool (..), Eq (..), Functor (..), Int, Maybe (..), Monad (..), Num (..),
+       all, const, id, maxBound, maybe, ($), (.))
 
 import Control.Applicative (Applicative (..), (<$>))
 import Data.Fin            (Fin (..))
@@ -74,12 +78,15 @@
 --- Instances
 import qualified Data.Foldable as I (Foldable (..))
 
+import qualified Data.Foldable.WithIndex as WI (FoldableWithIndex (..))
+import qualified Data.Functor.WithIndex  as WI (FunctorWithIndex (..))
+
 #ifdef MIN_VERSION_adjunctions
 import qualified Data.Functor.Rep as I (Representable (..))
 #endif
 
 #ifdef MIN_VERSION_distributive
-import Data.Distributive   (Distributive (..))
+import Data.Distributive (Distributive (..))
 #endif
 
 #ifdef MIN_VERSION_semigroupoids
@@ -96,8 +103,10 @@
 -- $setup
 -- >>> :set -XScopedTypeVariables
 -- >>> import Data.Proxy (Proxy (..))
--- >>> import Prelude (Char, Bool (..), not)
+-- >>> import Prelude (Char, Bool (..), not, Maybe (..), (<$>), ($))
 -- >>> import qualified Data.Vec.Lazy as L
+-- >>> import qualified Data.Type.Nat as N
+-- >>> import Data.Fin (Fin (..))
 
 -------------------------------------------------------------------------------
 -- Type
@@ -119,6 +128,15 @@
 instance N.SNatI n => I.Foldable (Vec n) where
     foldMap = foldMap
 
+-- | @since 0.4
+instance WI.FunctorWithIndex (Fin n) (Vec n) where
+    imap = imap
+
+-- | @since 0.4
+instance N.SNatI n => WI.FoldableWithIndex (Fin n) (Vec n) where
+    ifoldMap = ifoldMap
+    ifoldr   = ifoldr
+
 #ifdef MIN_VERSION_semigroupoids
 instance (N.SNatI m, n ~ 'S m)  => I.Foldable1 (Vec n) where
     foldMap1 = foldMap1
@@ -193,6 +211,10 @@
 toList :: N.SNatI n => Vec n a -> [a]
 toList v = unVec v <$> F.universe
 
+-- | Convert 'Vec' to NonEmpty.
+toNonEmpty :: N.SNatI n => Vec ('S n) a -> NonEmpty a
+toNonEmpty v = head v :| toList (tail v)
+
 -- | Convert list @[a]@ to @'Vec' n a@.
 -- Returns 'Nothing' if lengths don't match exactly.
 --
@@ -245,7 +267,7 @@
 --
 -- >>> reifyList "foo" length
 -- 3
-reifyList :: [a] -> (forall n. N.InlineInduction n => Vec n a -> r) -> r
+reifyList :: [a] -> (forall n. N.SNatI n => Vec n a -> r) -> r
 reifyList []       f = f empty
 reifyList (x : xs) f = reifyList xs $ \xs' -> f (cons x xs')
 
@@ -270,19 +292,25 @@
 -- | Add a single element at the end of a 'Vec'.
 --
 -- @since 0.2.1
-snoc :: forall a n. N.InlineInduction n => Vec n a -> a -> Vec ('S n) a
-snoc (Vec xs) x = Vec $ \i -> case F.isMax i of
-    Nothing -> x
-    Just i' -> xs i'
+snoc :: forall a n. N.SNatI n => Vec n a -> a -> Vec ('S n) a
+snoc (Vec xs) x = Vec $ \i -> maybe x xs (F.isMax i)
 
 -- | The first element of a 'Vec'.
 head :: Vec ('S n) a -> a
 head (Vec v) = v FZ
 
+-- | The last element of a 'Vec'.
+last :: forall n a. N.SNatI n => Vec ('S n) a -> a
+last (Vec v) = v maxBound 
+
 -- | The elements after the 'head' of a 'Vec'.
 tail :: Vec ('S n) a -> Vec n a
 tail (Vec v) = Vec (v . FS)
 
+-- | The elements before the 'last' of a 'Vec'.
+init :: forall n a. N.SNatI n => Vec ('S n) a -> Vec n a
+init (Vec v) = Vec (v . F.weakenLeft1)
+
 -------------------------------------------------------------------------------
 -- Reverse
 -------------------------------------------------------------------------------
@@ -291,7 +319,7 @@
 --
 -- @since 0.2.1
 --
-reverse :: forall n a. N.InlineInduction n => Vec n a -> Vec n a
+reverse :: forall n a. N.SNatI n => Vec n a -> Vec n a
 reverse (Vec v) = Vec (v . F.mirror)
 
 -------------------------------------------------------------------------------
diff --git a/test/Inspection.hs b/test/Inspection.hs
--- a/test/Inspection.hs
+++ b/test/Inspection.hs
@@ -6,6 +6,7 @@
 import Prelude hiding (zipWith)
 
 import Data.Fin        (Fin (..))
+import Data.List.NonEmpty (NonEmpty (..))
 import Data.Vec.Lazy   (Vec (..))
 import Test.Inspection
 
@@ -119,3 +120,51 @@
 
 inspect $ 'lhsReverse  === 'rhsReverse
 inspect $ 'lhsReverse' =/= 'rhsReverse
+
+-------------------------------------------------------------------------------
+-- last
+-------------------------------------------------------------------------------
+
+lhsLast :: Char
+lhsLast = I.last $ 'a' ::: 'b' ::: 'c' ::: VNil
+
+lhsLast' :: Char
+lhsLast' = L.last $ 'a' ::: 'b' ::: 'c' :::VNil
+
+rhsLast :: Char 
+rhsLast = 'c'
+
+inspect $ 'lhsLast === 'rhsLast
+inspect $ 'lhsLast' =/= 'rhsLast
+
+-------------------------------------------------------------------------------
+-- init
+-------------------------------------------------------------------------------
+
+lhsInit :: Vec N.Nat2 Char
+lhsInit = I.init $ 'a' ::: 'b' ::: 'c' ::: VNil
+
+lhsInit' :: Vec N.Nat2 Char
+lhsInit' = L.init $ 'a' ::: 'b' ::: 'c' ::: VNil
+
+rhsInit :: Vec N.Nat2 Char
+rhsInit = 'a' ::: 'b' ::: VNil
+
+inspect $ 'lhsInit  === 'rhsInit
+inspect $ 'lhsInit' =/= 'rhsInit
+
+-------------------------------------------------------------------------------
+-- toNonEmpty
+-------------------------------------------------------------------------------
+
+lhsToNonEmpty :: NonEmpty Char
+lhsToNonEmpty = I.toNonEmpty $ 'a' ::: 'b' ::: 'c' ::: VNil
+
+lhsToNonEmpty' :: NonEmpty Char
+lhsToNonEmpty' = L.toNonEmpty $ 'a' ::: 'b' ::: 'c' ::: VNil
+
+rhsToNonEmpty :: NonEmpty Char
+rhsToNonEmpty = 'a' :| ['b', 'c']
+
+inspect $ 'lhsToNonEmpty  === 'rhsToNonEmpty
+inspect $ 'lhsToNonEmpty' =/= 'rhsToNonEmpty
diff --git a/test/Inspection/DataFamily/SpineStrict/Pigeonhole.hs b/test/Inspection/DataFamily/SpineStrict/Pigeonhole.hs
--- a/test/Inspection/DataFamily/SpineStrict/Pigeonhole.hs
+++ b/test/Inspection/DataFamily/SpineStrict/Pigeonhole.hs
@@ -9,7 +9,7 @@
 {-# OPTIONS_GHC -dsuppress-type-signatures #-}
 -- {-# OPTIONS_GHC -dsuppress-uniques #-}
 -- This makes gix tests pass, default is 60
-{-# OPTIONS_GHC -funfolding-use-threshold=200 #-}
+{-# OPTIONS_GHC -funfolding-use-threshold=240 #-}
 module Inspection.DataFamily.SpineStrict.Pigeonhole where
 
 import Data.Functor.Compat                        ((<&>))
diff --git a/vec.cabal b/vec.cabal
--- a/vec.cabal
+++ b/vec.cabal
@@ -1,6 +1,6 @@
 cabal-version:      2.2
 name:               vec
-version:            0.3
+version:            0.4
 synopsis:           Vec: length-indexed (sized) list
 category:           Data, Dependent Types
 description:
@@ -66,7 +66,7 @@
 license-file:       LICENSE
 author:             Oleg Grenrus <oleg.grenrus@iki.fi>
 maintainer:         Oleg.Grenrus <oleg.grenrus@iki.fi>
-copyright:          (c) 2017-2019 Oleg Grenrus
+copyright:          (c) 2017-2021 Oleg Grenrus
 build-type:         Simple
 extra-source-files: ChangeLog.md
 tested-with:
@@ -76,7 +76,9 @@
    || ==8.2.2
    || ==8.4.4
    || ==8.6.5
-   || ==8.8.1
+   || ==8.8.4
+   || ==8.10.4
+   || ==9.0.1
 
 source-repository head
   type:     git
@@ -103,9 +105,9 @@
   default:     True
 
 library
-  default-language: Haskell2010
-  ghc-options:      -Wall -fprint-explicit-kinds
-  hs-source-dirs:   src
+  default-language:         Haskell2010
+  ghc-options:              -Wall -fprint-explicit-kinds
+  hs-source-dirs:           src
   exposed-modules:
     Data.Vec.DataFamily.SpineStrict
     Data.Vec.DataFamily.SpineStrict.Pigeonhole
@@ -119,23 +121,27 @@
 
   -- GHC boot libs
   build-depends:
-    , base          >=4.7     && <4.14
+    , base          >=4.7     && <4.16
     , deepseq       >=1.3.0.1 && <1.5
     , transformers  >=0.3.0.0 && <0.6
 
   if !impl(ghc >=8.0)
     build-depends: semigroups >=0.18.4 && <0.20
 
-  if !impl(ghc >=7.10)
+  -- Ensure Data.Functor.Classes is always available
+  if impl(ghc >= 7.10)
+    build-depends: transformers >= 0.4.2.0
+  else
     build-depends: transformers-compat ^>=0.6.5
 
   -- siblings
-  build-depends:    fin ^>=0.1.1
+  build-depends:            fin ^>=0.2
 
   -- other dependencies
   build-depends:
-    , hashable    >=1.2.7.0 && <1.4
-    , QuickCheck  ^>=2.13.2
+    , hashable             >=1.2.7.0 && <1.4
+    , indexed-traversable  ^>=0.1.1
+    , QuickCheck           ^>=2.14.2
 
   if flag(distributive)
     build-depends: distributive >=0.5.3 && <0.7
@@ -144,13 +150,21 @@
       build-depends: adjunctions ^>=4.4
 
   if flag(semigroupoids)
-    build-depends: semigroupoids >=5.2.2 && <5.4
+    build-depends: semigroupoids >=5.3.5 && <5.4
 
   other-extensions:
     CPP
     FlexibleContexts
     GADTs
     TypeOperators
+
+  if impl(ghc >=9.0)
+    -- these flags may abort compilation with GHC-8.10
+    -- https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3295
+    ghc-options: -Winferred-safe-imports -Wmissing-safe-haskell-mode
+
+  x-docspec-extra-packages: void
+  x-docspec-extra-packages: lens
 
 test-suite inspection
   type:             exitcode-stdio-1.0