diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,4 +1,8 @@
-# Revision history for boring
+# Revision history for vec
+
+## 0.1.1.1
+
+- Use `fin-0.1`
 
 ## 0.1.1
 
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright (c) 2017, Oleg Grenrus
+Copyright (c) 2017-2019, Oleg Grenrus
 
 All rights reserved.
 
diff --git a/bench/Bench.hs b/bench/Bench.hs
--- a/bench/Bench.hs
+++ b/bench/Bench.hs
@@ -31,17 +31,17 @@
 
 xsp, ysp :: P.Vec Nat5 Int
 xsp = P.Vec $ \i -> case i of
-    Z               -> 1
-    S Z             -> 2
-    S (S Z)         -> 3
-    S (S (S Z))     -> 4
-    S (S (S (S Z))) -> 5
+    FZ                   -> 1
+    FS FZ                -> 2
+    FS (FS FZ)           -> 3
+    FS (FS (FS FZ))      -> 4
+    FS (FS (FS (FS FZ))) -> 5
 ysp = P.Vec $ \i -> case i of
-    Z               -> 6
-    S Z             -> 7
-    S (S Z)         -> 8
-    S (S (S Z))     -> 9
-    S (S (S (S Z))) -> 0
+    FZ                   -> 6
+    FS FZ                -> 7
+    FS (FS FZ)           -> 8
+    FS (FS (FS FZ))      -> 9
+    FS (FS (FS (FS FZ))) -> 0
 
 main :: IO ()
 main = defaultMain
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
@@ -121,7 +121,7 @@
 import Control.Applicative (Applicative (..), liftA2)
 import Control.DeepSeq     (NFData (..))
 import Data.Distributive   (Distributive (..))
-import Data.Fin            (Fin)
+import Data.Fin            (Fin (..))
 import Data.Functor.Apply  (Apply (..))
 import Data.Functor.Rep    (Representable (..), distributeRep)
 import Data.Hashable       (Hashable (..))
@@ -348,8 +348,8 @@
 
     step :: ToPull m a -> ToPull ('S m) a
     step (ToPull f) = ToPull $ \(x ::: xs) -> P.Vec $ \i -> case i of
-        F.Z    -> x
-        F.S i' -> P.unVec (f xs) i'
+        FZ    -> x
+        FS i' -> P.unVec (f xs) i'
 
 newtype ToPull n a = ToPull { getToPull :: Vec n a -> P.Vec n a }
 
@@ -360,7 +360,7 @@
     start = FromPull $ const VNil
 
     step :: FromPull m a -> FromPull ('S m) a
-    step (FromPull f) = FromPull $ \(P.Vec v) -> v F.Z ::: f (P.Vec (v . F.S))
+    step (FromPull f) = FromPull $ \(P.Vec v) -> v FZ ::: f (P.Vec (v . FS))
 
 newtype FromPull n a = FromPull { getFromPull :: P.Vec n a -> Vec n a }
 
@@ -463,14 +463,14 @@
 
     step :: Index m a-> Index ('N.S m) a
     step (Index go) = Index $ \n (x ::: xs) -> case n of
-        F.Z   -> x
-        F.S m -> go m xs
+        FZ   -> x
+        FS m -> go m xs
 
 newtype Index n a = Index { getIndex :: Fin n -> Vec n a -> a }
 
 -- | Indexing.
 --
--- >>> ('a' ::: 'b' ::: 'c' ::: VNil) ! F.S F.Z
+-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) ! FS FZ
 -- 'b'
 --
 (!) :: N.InlineInduction n => Vec n a -> Fin n -> a
@@ -478,15 +478,15 @@
 
 -- | Index lens.
 --
--- >>> ('a' ::: 'b' ::: 'c' ::: VNil) ^. ix (F.S F.Z)
+-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) ^. ix (FS FZ)
 -- 'b'
 --
--- >>> ('a' ::: 'b' ::: 'c' ::: VNil) & ix (F.S F.Z) .~ 'x'
+-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) & ix (FS FZ) .~ 'x'
 -- 'a' ::: 'x' ::: 'c' ::: VNil
 --
 ix :: Fin n -> I.Lens' (Vec n a) a
-ix F.Z     f (x ::: xs) = (::: xs) <$> f x
-ix (F.S n) f (x ::: xs) = (x :::)  <$> ix n f xs
+ix FZ     f (x ::: xs) = (::: xs) <$> f x
+ix (FS n) f (x ::: xs) = (x :::)  <$> ix n f xs
 
 -- | Match on non-empty 'Vec'.
 --
@@ -631,7 +631,7 @@
     start = IMap $ \_ _ -> VNil
 
     step :: IMap a m b -> IMap a ('S m) b
-    step (IMap go) = IMap $ \f (x ::: xs) -> f F.Z x ::: go (f . F.S) xs
+    step (IMap go) = IMap $ \f (x ::: xs) -> f FZ x ::: go (f . FS) xs
 
 newtype IMap a n b = IMap { getIMap :: (Fin n -> a -> b) -> Vec n a -> Vec n b }
 
@@ -665,7 +665,7 @@
     start = ITraverse $ \_ _ -> pure VNil
 
     step :: ITraverse f a m b -> ITraverse f a ('S m) b
-    step (ITraverse go) = ITraverse $ \f (x ::: xs) -> liftA2 (:::) (f F.Z x) (go (f . F.S) xs)
+    step (ITraverse go) = ITraverse $ \f (x ::: xs) -> liftA2 (:::) (f FZ x) (go (f . FS) xs)
 {-# INLINE itraverse #-}
 
 newtype ITraverse f a n b = ITraverse { getITraverse :: (Fin n -> a -> f b) -> Vec n a -> f (Vec n b) }
@@ -677,7 +677,7 @@
     start = ITraverse_ $ \_ _ -> pure ()
 
     step :: ITraverse_ f a m b -> ITraverse_ f a ('S m) b
-    step (ITraverse_ go) = ITraverse_ $ \f (x ::: xs) -> f F.Z x *> go (f . F.S) xs
+    step (ITraverse_ go) = ITraverse_ $ \f (x ::: xs) -> f FZ x *> go (f . FS) xs
 
 newtype ITraverse_ f a n b = ITraverse_ { getITraverse_ :: (Fin n -> a -> f b) -> Vec n a -> f () }
 
@@ -710,7 +710,7 @@
     start = IFoldMap $ \_ _ -> mempty
 
     step :: IFoldMap a p m -> IFoldMap a ('S p) m
-    step (IFoldMap go) = IFoldMap $ \f (x ::: xs) -> f F.Z x `mappend` go (f . F.S) xs
+    step (IFoldMap go) = IFoldMap $ \f (x ::: xs) -> f FZ x `mappend` go (f . FS) xs
 
 newtype IFoldMap a n m = IFoldMap { getIFoldMap :: (Fin n -> a -> m) -> Vec n a -> m }
 
@@ -718,10 +718,10 @@
 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
     start :: IFoldMap1 a 'Z s
-    start = IFoldMap1 $ \f (x ::: _) -> f F.Z x
+    start = IFoldMap1 $ \f (x ::: _) -> f FZ x
 
     step :: IFoldMap1 a p s -> IFoldMap1 a ('S p) s
-    step (IFoldMap1 go) = IFoldMap1 $ \f (x ::: xs) -> f F.Z x <> go (f . F.S) xs
+    step (IFoldMap1 go) = IFoldMap1 $ \f (x ::: xs) -> f FZ x <> go (f . FS) xs
 
 newtype IFoldMap1 a n m = IFoldMap1 { getIFoldMap1 :: (Fin ('S n) -> a -> m) -> Vec ('S n) a -> m }
 
@@ -741,7 +741,7 @@
     start = IFoldr $ \_ z _ -> z
 
     step :: IFoldr a m b -> IFoldr a ('S m) b
-    step (IFoldr go) = IFoldr $ \f z (x ::: xs) -> f F.Z x (go (f . F.S) z xs)
+    step (IFoldr go) = IFoldr $ \f z (x ::: xs) -> f FZ x (go (f . FS) z xs)
 
 newtype IFoldr a n b = IFoldr { getIFoldr :: (Fin n -> a -> b -> b) -> b -> Vec n a -> b }
 
@@ -804,7 +804,7 @@
     start = IZipWith $ \_ _ _ -> VNil
 
     step :: IZipWith a b c m -> IZipWith a b c ('S m)
-    step (IZipWith go) = IZipWith $ \f (x ::: xs) (y ::: ys) -> f F.Z x y ::: go (f . F.S) xs ys
+    step (IZipWith go) = IZipWith $ \f (x ::: xs) (y ::: ys) -> f FZ x y ::: go (f . FS) xs ys
 
 newtype IZipWith a b c n = IZipWith { getIZipWith :: (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c }
 
@@ -851,7 +851,7 @@
     first = Universe VNil
 
     step :: N.InlineInduction m => Universe m -> Universe ('S m)
-    step (Universe go) = Universe (F.Z ::: map F.S go)
+    step (Universe go) = Universe (FZ ::: map FS go)
 
 newtype Universe n = Universe { getUniverse :: Vec n (Fin n) }
 
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
@@ -43,6 +43,7 @@
 
 -- $setup
 -- >>> :set -XDeriveGeneric
+-- >>> import Control.Applicative (Const (..))
 -- >>> import Data.Void (absurd)
 -- >>> import GHC.Generics (Generic, Generic1)
 
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
@@ -85,7 +85,7 @@
 import Control.DeepSeq     (NFData (..))
 import Control.Lens        ((<&>))
 import Data.Distributive   (Distributive (..))
-import Data.Fin            (Fin)
+import Data.Fin            (Fin (..))
 import Data.Functor.Apply  (Apply (..))
 import Data.Functor.Rep    (Representable (..), distributeRep)
 import Data.Hashable       (Hashable (..))
@@ -288,14 +288,14 @@
 toPull :: Vec n a -> P.Vec n a
 toPull VNil       = P.Vec F.absurd
 toPull (x ::: xs) = P.Vec $ \n -> case n of
-    F.Z   -> x
-    F.S m -> P.unVec (toPull xs) m
+    FZ   -> x
+    FS m -> P.unVec (toPull xs) m
 
 -- | Convert from pull 'P.Vec'.
 fromPull :: forall n a. N.SNatI n => P.Vec n a -> Vec n a
 fromPull (P.Vec f) = case N.snat :: N.SNat n of
     N.SZ -> VNil
-    N.SS -> f F.Z ::: fromPull (P.Vec (f . F.S))
+    N.SS -> f FZ ::: fromPull (P.Vec (f . FS))
 
 -- | An 'I.Iso' from 'toPull' and 'fromPull'.
 _Pull :: N.SNatI n => I.Iso (Vec n a) (Vec n b) (P.Vec n a) (P.Vec n b)
@@ -385,25 +385,25 @@
 
 -- | Indexing.
 --
--- >>> ('a' ::: 'b' ::: 'c' ::: VNil) ! F.S F.Z
+-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) ! FS FZ
 -- 'b'
 --
 (!) :: Vec n a -> Fin n -> a
-(!) (x ::: _)  F.Z     = x
-(!) (_ ::: xs) (F.S n) = xs ! n
+(!) (x ::: _)  FZ     = x
+(!) (_ ::: xs) (FS n) = xs ! n
 (!) VNil n = case n of {}
 
 -- | Index lens.
 --
--- >>> ('a' ::: 'b' ::: 'c' ::: VNil) ^. ix (F.S F.Z)
+-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) ^. ix (FS FZ)
 -- 'b'
 --
--- >>> ('a' ::: 'b' ::: 'c' ::: VNil) & ix (F.S F.Z) .~ 'x'
+-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) & ix (FS FZ) .~ 'x'
 -- 'a' ::: 'x' ::: 'c' ::: VNil
 --
 ix :: Fin n -> I.Lens' (Vec n a) a
-ix F.Z     f (x ::: xs) = (::: xs) <$> f x
-ix (F.S n) f (x ::: xs) = (x :::)  <$> ix n f xs
+ix FZ     f (x ::: xs) = (::: xs) <$> f x
+ix (FS n) f (x ::: xs) = (x :::)  <$> ix n f xs
 
 -- | Match on non-empty 'Vec'.
 --
@@ -526,7 +526,7 @@
 --
 imap :: (Fin n -> a -> b) -> Vec n a -> Vec n b
 imap _ VNil       = VNil
-imap f (x ::: xs) = f F.Z x ::: imap (f . F.S) xs
+imap f (x ::: xs) = f FZ x ::: imap (f . FS) xs
 
 -- | Apply an action to every element of a 'Vec', yielding a 'Vec' of results.
 traverse :: forall n f a b. Applicative f => (a -> f b) -> Vec n a -> f (Vec n b)
@@ -545,12 +545,12 @@
 -- | Apply an action to every element of a 'Vec' and its index, yielding a 'Vec' of results.
 itraverse :: Applicative f => (Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
 itraverse _ VNil       = pure VNil
-itraverse f (x ::: xs) = (:::) <$> f F.Z x <*> I.itraverse (f . F.S) xs
+itraverse f (x ::: xs) = (:::) <$> f FZ x <*> I.itraverse (f . FS) xs
 
 -- | Apply an action to every element of a 'Vec' and its index, ignoring the results.
 itraverse_ :: Applicative f => (Fin n -> a -> f b) -> Vec n a -> f ()
 itraverse_ _ VNil       = pure ()
-itraverse_ f (x ::: xs) = f F.Z x *> itraverse_ (f . F.S) xs
+itraverse_ f (x ::: xs) = f FZ x *> itraverse_ (f . FS) xs
 
 -------------------------------------------------------------------------------
 -- Folding
@@ -569,12 +569,12 @@
 -- | See 'I.FoldableWithIndex'.
 ifoldMap :: Monoid m => (Fin n -> a -> m) -> Vec n a -> m
 ifoldMap _ VNil       = mempty
-ifoldMap f (x ::: xs) = mappend (f F.Z x) (ifoldMap (f . F.S) xs)
+ifoldMap f (x ::: xs) = mappend (f FZ x) (ifoldMap (f . FS) xs)
 
 -- | There is no type-class for this :(
 ifoldMap1 :: Semigroup s => (Fin ('S n) -> a -> s) -> Vec ('S n) a -> s
-ifoldMap1 f (x ::: VNil)         = f F.Z x
-ifoldMap1 f (x ::: xs@(_ ::: _)) = f F.Z x <> ifoldMap1 (f . F.S) xs
+ifoldMap1 f (x ::: VNil)         = f FZ x
+ifoldMap1 f (x ::: xs@(_ ::: _)) = f FZ x <> ifoldMap1 (f . FS) xs
 
 -- | Right fold.
 foldr :: forall a b n. (a -> b -> b) -> b -> Vec n a -> b
@@ -586,7 +586,7 @@
 -- | Right fold with an index.
 ifoldr :: forall a b n. (Fin n -> a -> b -> b) -> b -> Vec n a -> b
 ifoldr _ z VNil       = z
-ifoldr f z (x ::: xs) = f F.Z x (ifoldr (f . F.S) z xs)
+ifoldr f z (x ::: xs) = f FZ x (ifoldr (f . FS) z xs)
 
 -- | Strict left fold.
 foldl' :: forall a b n. (b -> a -> b) -> b -> Vec n a -> b
@@ -631,7 +631,7 @@
 -- | Zip two 'Vec's. with a function that also takes the elements' indices.
 izipWith :: (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
 izipWith _ VNil       VNil       = VNil
-izipWith f (x ::: xs) (y ::: ys) = f F.Z x y ::: izipWith (f . F.S) xs ys
+izipWith f (x ::: xs) (y ::: ys) = f FZ x y ::: izipWith (f . FS) xs ys
 
 -------------------------------------------------------------------------------
 -- Monadic
@@ -664,7 +664,7 @@
     first = Universe VNil
 
     step :: Universe m -> Universe ('S m)
-    step (Universe go) = Universe (F.Z ::: map F.S go)
+    step (Universe go) = Universe (FZ ::: map FS go)
 
 newtype Universe n = Universe { getUniverse :: Vec n (Fin n) }
 
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
@@ -80,7 +80,7 @@
        id, ($), (.), (<$>))
 
 import Control.Applicative (liftA2)
-import Data.Fin            (Fin)
+import Data.Fin            (Fin (..))
 import Data.Functor.Apply  (Apply, liftF2)
 import Data.Nat
 import Data.Semigroup      (Semigroup (..))
@@ -107,8 +107,8 @@
 
     step :: ToPull m a -> ToPull ('S m) a
     step (ToPull f) = ToPull $ \(x ::: xs) -> P.Vec $ \i -> case i of
-        F.Z    -> x
-        F.S i' -> P.unVec (f xs) i'
+        FZ    -> x
+        FS i' -> P.unVec (f xs) i'
 
 newtype ToPull n a = ToPull { getToPull :: Vec n a -> P.Vec n a }
 
@@ -119,7 +119,7 @@
     start = FromPull $ const VNil
 
     step :: FromPull m a -> FromPull ('S m) a
-    step (FromPull f) = FromPull $ \(P.Vec v) -> v F.Z ::: f (P.Vec (v . F.S))
+    step (FromPull f) = FromPull $ \(P.Vec v) -> v FZ ::: f (P.Vec (v . FS))
 
 newtype FromPull n a = FromPull { getFromPull :: P.Vec n a -> Vec n a }
 
@@ -214,14 +214,14 @@
 
     step :: Index m a-> Index ('N.S m) a
     step (Index go) = Index $ \n (x ::: xs) -> case n of
-        F.Z   -> x
-        F.S m -> go m xs
+        FZ   -> x
+        FS m -> go m xs
 
 newtype Index n a = Index { getIndex :: Fin n -> Vec n a -> a }
 
 -- | Indexing.
 --
--- >>> ('a' ::: 'b' ::: 'c' ::: VNil) ! F.S F.Z
+-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) ! FS FZ
 -- 'b'
 --
 (!) :: N.InlineInduction n => Vec n a -> Fin n -> a
@@ -229,10 +229,10 @@
 
 -- | Index lens.
 --
--- >>> ('a' ::: 'b' ::: 'c' ::: VNil) ^. ix (F.S F.Z)
+-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) ^. ix (FS FZ)
 -- 'b'
 --
--- >>> ('a' ::: 'b' ::: 'c' ::: VNil) & ix (F.S F.Z) .~ 'x'
+-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) & ix (FS FZ) .~ 'x'
 -- 'a' ::: 'x' ::: 'c' ::: VNil
 --
 ix :: N.InlineInduction n => Fin n -> I.Lens' (Vec n a) a
@@ -242,8 +242,8 @@
 
     step :: IxLens m a -> IxLens ('S m) a
     step (IxLens l) = IxLens $ \i -> case i of
-        F.Z   -> _head
-        F.S j -> _tail . l j
+        FZ   -> _head
+        FS j -> _tail . l j
 
 newtype IxLens n a = IxLens { getIxLens :: Fin n -> I.Lens' (Vec n a) a }
 
@@ -352,7 +352,7 @@
     start = IMap $ \_ _ -> VNil
 
     step :: IMap a m b -> IMap a ('S m) b
-    step (IMap go) = IMap $ \f (x ::: xs) -> f F.Z x ::: go (f . F.S) xs
+    step (IMap go) = IMap $ \f (x ::: xs) -> f FZ x ::: go (f . FS) xs
 
 newtype IMap a n b = IMap { getIMap :: (Fin n -> a -> b) -> Vec n a -> Vec n b }
 
@@ -385,7 +385,7 @@
     start = ITraverse $ \_ _ -> pure VNil
 
     step :: ITraverse f a m b -> ITraverse f a ('S m) b
-    step (ITraverse go) = ITraverse $ \f (x ::: xs) -> liftA2 (:::) (f F.Z x) (go (f . F.S) xs)
+    step (ITraverse go) = ITraverse $ \f (x ::: xs) -> liftA2 (:::) (f FZ x) (go (f . FS) xs)
 
 newtype ITraverse f a n b = ITraverse { getITraverse :: (Fin n -> a -> f b) -> Vec n a -> f (Vec n b) }
 
@@ -396,7 +396,7 @@
     start = ITraverse_ $ \_ _ -> pure ()
 
     step :: ITraverse_ f a m b -> ITraverse_ f a ('S m) b
-    step (ITraverse_ go) = ITraverse_ $ \f (x ::: xs) -> f F.Z x *> go (f . F.S) xs
+    step (ITraverse_ go) = ITraverse_ $ \f (x ::: xs) -> f FZ x *> go (f . FS) xs
 
 newtype ITraverse_ f a n b = ITraverse_ { getITraverse_ :: (Fin n -> a -> f b) -> Vec n a -> f () }
 
@@ -429,7 +429,7 @@
     start = IFoldMap $ \_ _ -> mempty
 
     step :: IFoldMap a p m -> IFoldMap a ('S p) m
-    step (IFoldMap go) = IFoldMap $ \f (x ::: xs) -> f F.Z x `mappend` go (f . F.S) xs
+    step (IFoldMap go) = IFoldMap $ \f (x ::: xs) -> f FZ x `mappend` go (f . FS) xs
 
 newtype IFoldMap a n m = IFoldMap { getIFoldMap :: (Fin n -> a -> m) -> Vec n a -> m }
 
@@ -437,10 +437,10 @@
 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
     start :: IFoldMap1 a 'Z s
-    start = IFoldMap1 $ \f (x ::: _) -> f F.Z x
+    start = IFoldMap1 $ \f (x ::: _) -> f FZ x
 
     step :: IFoldMap1 a p s -> IFoldMap1 a ('S p) s
-    step (IFoldMap1 go) = IFoldMap1 $ \f (x ::: xs) -> f F.Z x <> go (f . F.S) xs
+    step (IFoldMap1 go) = IFoldMap1 $ \f (x ::: xs) -> f FZ x <> go (f . FS) xs
 
 newtype IFoldMap1 a n m = IFoldMap1 { getIFoldMap1 :: (Fin ('S n) -> a -> m) -> Vec ('S n) a -> m }
 
@@ -460,7 +460,7 @@
     start = IFoldr $ \_ z _ -> z
 
     step :: IFoldr a m b -> IFoldr a ('S m) b
-    step (IFoldr go) = IFoldr $ \f z (x ::: xs) -> f F.Z x (go (f . F.S) z xs)
+    step (IFoldr go) = IFoldr $ \f z (x ::: xs) -> f FZ x (go (f . FS) z xs)
 
 newtype IFoldr a n b = IFoldr { getIFoldr :: (Fin n -> a -> b -> b) -> b -> Vec n a -> b }
 
@@ -516,7 +516,7 @@
     start = IZipWith $ \_ _ _ -> VNil
 
     step :: IZipWith a b c m -> IZipWith a b c ('S m)
-    step (IZipWith go) = IZipWith $ \f (x ::: xs) (y ::: ys) -> f F.Z x y ::: go (f . F.S) xs ys
+    step (IZipWith go) = IZipWith $ \f (x ::: xs) (y ::: ys) -> f FZ x y ::: go (f . FS) xs ys
 
 newtype IZipWith a b c n = IZipWith { getIZipWith :: (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c }
 
@@ -563,7 +563,7 @@
     first = Universe VNil
 
     step :: N.InlineInduction m => Universe m -> Universe ('S m)
-    step (Universe go) = Universe (F.Z ::: map F.S go)
+    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
@@ -64,7 +64,7 @@
 import Control.Applicative (Applicative (..))
 import Control.Lens        ((<&>))
 import Data.Distributive   (Distributive (..))
-import Data.Fin            (Fin)
+import Data.Fin            (Fin (..))
 import Data.Functor.Apply  (Apply (..))
 import Data.Functor.Rep    (Representable (..))
 import Data.Nat
@@ -236,10 +236,10 @@
 
 -- | Index lens.
 --
--- >>> ('a' L.::: 'b' L.::: 'c' L.::: L.VNil) ^. L._Pull . ix (F.S F.Z)
+-- >>> ('a' L.::: 'b' L.::: 'c' L.::: L.VNil) ^. L._Pull . ix (FS FZ)
 -- 'b'
 --
--- >>> ('a' L.::: 'b' L.::: 'c' L.::: L.VNil) & L._Pull . ix (F.S F.Z) .~ 'x'
+-- >>> ('a' L.::: 'b' L.::: 'c' L.::: L.VNil) & L._Pull . ix (FS FZ) .~ 'x'
 -- 'a' ::: 'x' ::: 'c' ::: VNil
 --
 ix :: Fin n -> I.Lens' (Vec n a) a
@@ -254,7 +254,7 @@
 -- In fact, @'Vec' n a@ cannot have an instance of 'I.Cons' as types don't match.
 --
 _Cons :: I.Iso (Vec ('S n) a) (Vec ('S n) b) (a, Vec n a) (b, Vec n b)
-_Cons = I.iso (\(Vec v) -> (v F.Z, Vec (v . F.S))) (\(x, xs) -> cons x xs)
+_Cons = I.iso (\(Vec v) -> (v FZ, Vec (v . FS))) (\(x, xs) -> cons x xs)
 
 -- | Head lens. /Note:/ @lens@ 'I._head' is a 'I.Traversal''.
 --
@@ -265,28 +265,28 @@
 -- 'x' ::: 'b' ::: 'c' ::: VNil
 --
 _head :: I.Lens' (Vec ('S n) a) a
-_head f (Vec v) = f (v F.Z) <&> \a -> Vec $ \j -> case j of
-    F.Z -> a
+_head f (Vec v) = f (v FZ) <&> \a -> Vec $ \j -> case j of
+    FZ -> a
     _   -> v j
 {-# INLINE head #-}
 
 -- | Head lens. /Note:/ @lens@ 'I._head' is a 'I.Traversal''.
 _tail :: I.Lens' (Vec ('S n) a) (Vec n a)
-_tail f (Vec v) = f (Vec (v . F.S)) <&> \xs -> cons (v F.Z) xs
+_tail f (Vec v) = f (Vec (v . FS)) <&> \xs -> cons (v FZ) xs
 {-# INLINE _tail #-}
 
 cons :: a -> Vec n a -> Vec ('S n) a
 cons x (Vec v) = Vec $ \i -> case i of
-    F.Z   -> x
-    F.S j -> v j
+    FZ   -> x
+    FS j -> v j
 
 -- | The first element of a 'Vec'.
 head :: Vec ('S n) a -> a
-head (Vec v) = v F.Z
+head (Vec v) = v FZ
 
 -- | The elements after the 'head' of a 'Vec'.
 tail :: Vec ('S n) a -> Vec n a
-tail (Vec v) = Vec (v . F.S)
+tail (Vec v) = Vec (v . FS)
 
 -------------------------------------------------------------------------------
 -- Mapping
diff --git a/test/Inspection.hs b/test/Inspection.hs
--- a/test/Inspection.hs
+++ b/test/Inspection.hs
@@ -5,6 +5,7 @@
 
 import Prelude hiding (zipWith)
 
+import Data.Fin        (Fin (..))
 import Data.Vec.Lazy   (Vec (..))
 import Test.Inspection
 
@@ -48,7 +49,7 @@
 lhsIMap' = L.imap (,) $ 'a' ::: 'b' ::: VNil
 
 rhsIMap :: Vec N.Nat2 (F.Fin N.Nat2, Char)
-rhsIMap = (F.Z,'a') ::: (F.S F.Z,'b') ::: VNil
+rhsIMap = (FZ,'a') ::: (FS FZ,'b') ::: VNil
 
 inspect $ 'lhsIMap  === 'rhsIMap
 inspect $ 'lhsIMap' =/= 'rhsIMap
diff --git a/test/Inspection/DataFamily/SpineStrict.hs b/test/Inspection/DataFamily/SpineStrict.hs
--- a/test/Inspection/DataFamily/SpineStrict.hs
+++ b/test/Inspection/DataFamily/SpineStrict.hs
@@ -6,7 +6,8 @@
 
 import Prelude hiding (zipWith)
 
-import Data.Vec.DataFamily.SpineStrict   (Vec (..))
+import Data.Fin                        (Fin (..))
+import Data.Vec.DataFamily.SpineStrict (Vec (..))
 import Test.Inspection
 
 import qualified Data.Fin                        as F
@@ -40,7 +41,7 @@
 lhsIMap = I.imap (,) $ 'a' ::: 'b' ::: VNil
 
 rhsIMap :: Vec N.Nat2 (F.Fin N.Nat2, Char)
-rhsIMap = (F.Z,'a') ::: (F.S F.Z,'b') ::: VNil
+rhsIMap = (FZ,'a') ::: (FS FZ,'b') ::: VNil
 
 inspect $ 'lhsIMap  === 'rhsIMap
 
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
@@ -48,6 +48,7 @@
 rhsIndex (Values _ _ _ x _) Key4 = x
 rhsIndex (Values _ _ _ _ x) Key5 = x
 
+inspect $ hasNoGenerics 'lhsIndex
 inspect $ 'lhsIndex === 'rhsIndex
 
 -------------------------------------------------------------------------------
@@ -60,6 +61,7 @@
 rhsTabulate :: (Key -> a) -> Values a
 rhsTabulate f = Values (f Key1) (f Key2) (f Key3) (f Key4) (f Key5)
 
+inspect $ hasNoGenerics 'lhsTabulate
 inspect $ 'lhsTabulate === 'rhsTabulate
 
 -------------------------------------------------------------------------------
@@ -77,6 +79,7 @@
     <*> f u
     <*> f v
 
+inspect $ hasNoGenerics 'lhsTraverse
 inspect $ 'lhsTraverse === 'rhsTraverse
 
 lhsITraverse :: Applicative f => (Key -> a -> f b) -> Values a -> f (Values b)
@@ -90,4 +93,5 @@
     <*> f Key4 u
     <*> f Key5 v
 
+inspect $ hasNoGenerics 'lhsITraverse
 inspect $ 'lhsITraverse === 'rhsITraverse
diff --git a/vec.cabal b/vec.cabal
--- a/vec.cabal
+++ b/vec.cabal
@@ -1,8 +1,8 @@
 cabal-version:      >=1.10
 name:               vec
-version:            0.1.1
+version:            0.1.1.1
 synopsis:           Vec: length-indexed (sized) list
-category:           Data
+category:           Data, Dependent Types
 description:
   This package provides length-indexed (sized) lists, also known as vectors.
   .
@@ -64,7 +64,7 @@
 license-file:       LICENSE
 author:             Oleg Grenrus <oleg.grenrus@iki.fi>
 maintainer:         Oleg.Grenrus <oleg.grenrus@iki.fi>
-copyright:          (c) 2017 Oleg Grenrus
+copyright:          (c) 2017-2019 Oleg Grenrus
 build-type:         Simple
 extra-source-files: ChangeLog.md
 tested-with:
@@ -91,14 +91,14 @@
     , base-compat    >=0.9.3   && <0.11
     , deepseq        >=1.3.0.2 && <1.5
     , distributive   >=0.5.3   && <0.7
-    , fin            >=0.0.2   && <0.1
-    , hashable       >=1.2.7.0 && <1.3
+    , fin            >=0.1     && <0.2
+    , hashable       >=1.2.7.0 && <1.4
     , lens           >=4.16    && <4.18
     , semigroupoids  >=5.2.2   && <5.4
     , transformers   >=0.3.0.0 && <0.6
 
   if !impl(ghc >=8.0)
-    build-depends: semigroups >=0.18.4 && <0.18.6
+    build-depends: semigroups >=0.18.4 && <0.20
 
   ghc-options:      -Wall -fprint-explicit-kinds
   hs-source-dirs:   src