diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,21 @@
 # Revision history for finitary
 
+## 1.0.0.0 -- 2019-09-17
+
+* Rewritten documentation to be more clear, and state more laws.
+* Added ``nextSkipping`` and ``previousSkipping`` methods to allow 'skipping
+  over' some elements when enumerating in a more efficient manner.
+* Added ``Eq a`` as a constraint for ``Finitary a`` instances (as without it,
+  the laws don't make much sense).
+* Fixed numerous typoes and unclear statements.
+* Stated that ``Finitary`` must be order-preserving relative any instances with
+  ``Ord`` instances; existing instances modified to follow this law.
+* Added more tests.
+* Fixed odd issue with some element cardinalities and lengths for sized
+  ``Vector`` instances.
+* Tightened bounds to be more conservative.
+* Support GHC 8.8.
+
 ## 0.1.0.0 -- 2019-09-10
 
 * First version. Released on an unsuspecting world.
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -107,7 +107,7 @@
 import qualified Data.Vector.Sized as VS
 
 data Foo = Bar | Baz (Word8, Word8) | Quux (VS.Vector 4 Bool)
-  deriving (Generic, Finitary) 
+  deriving (Eq, Generic, Finitary) 
 ```
 
 Furthermore, GHC will even calculate the cardinality for you. To assist in this,
diff --git a/finitary.cabal b/finitary.cabal
--- a/finitary.cabal
+++ b/finitary.cabal
@@ -3,7 +3,7 @@
 -- PVP summary:        +-+------- breaking API changes
 --                     | | +----- non-breaking API additions
 --                     | | | +--- code changes with no API change
-version:               0.1.0.0
+version:               1.0.0.0
 synopsis:              A better, more type-safe Enum.
 description:           Provides a type class witnessing that a type has
                        finitely-many inhabitants, as well as its cardinality.
@@ -19,7 +19,8 @@
 copyright:             (C) Koz Ross 2019
 category:              Data
 build-type:            Simple
-tested-with:           GHC == 8.6.5, 
+tested-with:           GHC == 8.8.1,
+                       GHC == 8.6.5, 
                        GHC == 8.4.4
 extra-source-files:    CHANGELOG.md,
                        README.md,
@@ -32,15 +33,18 @@
 library
   exposed-modules:     Data.Finitary
   other-modules:       Data.Finitary.TH
-  build-depends:       base >= 4.11 && < 4.13,
-                       finite-typelits >= 0.1.4.2 && < 1.0.0.0,
+  build-depends:       base >= 4.11 && < 4.14,
+                       finite-typelits >= 0.1.4.2 && < 0.2.0.0,
                        coercible-utils >= 0.0.0 && < 1.0.0,
-                       ghc-typelits-knownnat >= 0.7 && < 1.0,
-                       ghc-typelits-natnormalise >= 0.7 && < 1.0,
-                       vector-sized >= 1.2.0.1 && < 2.0.0.0,
-                       mtl >= 2.2.2 && < 3.0.0,
-                       template-haskell >= 2.13.0.0 && < 3.0.0.0,
-                       bitvec >= 1.0.0.1 && < 2.0.0.0
+                       ghc-typelits-knownnat >= 0.7 && < 0.8,
+                       ghc-typelits-natnormalise >= 0.7 && < 0.8,
+                       vector-sized >= 1.4.0.0 && < 1.5.0.0,
+                       mtl >= 2.2.2 && < 2.3.0,
+                       template-haskell >= 2.13.0.0 && < 2.16.0.0,
+                       bitvec >= 1.0.0.1 && < 1.2.0.0,
+                       primitive >= 0.6.4.0 && < 0.8.0.0,
+                       vector >= 0.12.0.3 && < 0.13.0.0,
+                       typelits-witnesses >= 0.4.0.0 && < 0.5.0.0
   hs-source-dirs:      src
   default-language:    Haskell2010
 
@@ -48,12 +52,12 @@
   type:                exitcode-stdio-1.0
   main-is:             Main.hs
   hs-source-dirs:      test
-  ghc-options:         -threaded -rtsopts -with-rtsopts=-N
+  ghc-options:         -O2 -threaded -rtsopts -with-rtsopts=-N
   build-depends:       base,
-                       hedgehog >= 1.0 && < 2.0,
+                       hedgehog >= 1.0.1 && < 1.2,
                        finitary,
                        finite-typelits,
                        vector-sized,
-                       monad-loops >= 0.4.3 && < 1.0.0,
+                       monad-loops >= 0.4.3 && < 0.5.0,
                        bitvec
   default-language:    Haskell2010
diff --git a/src/Data/Finitary.hs b/src/Data/Finitary.hs
--- a/src/Data/Finitary.hs
+++ b/src/Data/Finitary.hs
@@ -18,6 +18,7 @@
 {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
 {-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
 
+{-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE ConstrainedClassMethods #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE FlexibleContexts #-}
@@ -62,7 +63,7 @@
 -- > import Data.Word
 -- >
 -- > data Foo = Bar | Baz (Word8, Word8) | Quux Word16
--- >    deriving (Generic, Finitary)
+-- >    deriving (Eq, Generic, Finitary)
 --
 -- This is the easiest method, and also the safest, as GHC will automatically
 -- determine the cardinality of @Foo@, as well as defining law-abiding methods.
@@ -73,8 +74,8 @@
 -- If you want a manually-defined instance, but don't wish to define every
 -- method, only 'fromFinite' and 'toFinite' are needed, along with
 -- 'Cardinality'. 'Cardinality' in particular must be defined with care, as
--- otherwise, you may end up with inconstructable values or values of @Finite
--- (Cardinality YourType)@ that don't correspond to anything.
+-- otherwise, you may end up with inconstructable values or indexes that don't 
+-- correspond to anything.
 --
 -- __By defining everything__
 --
@@ -85,16 +86,9 @@
 Finitary(..)
 ) where
 
+import Numeric.Natural (Natural)
 import Data.Semigroup (Max, Min, Sum, Product, Dual, Last, First, Any, All)
 import Data.Functor.Identity (Identity)
-#if MIN_VERSION_base(4,12,0)
-import Data.Ord (Down)
-#else
-import Data.Ord (Down(..))
-#endif
-import Foreign.Storable (Storable)
-import Data.Maybe (fromJust)
-import Control.Monad.State.Strict (MonadState(..), modify, evalState)
 import Data.Int (Int8, Int16, Int32, Int64)
 import Data.Word (Word8, Word16, Word32, Word64)
 import Data.Proxy (Proxy(..))
@@ -105,17 +99,31 @@
 import Control.Applicative (Alternative(..), Const)
 import Data.Kind (Type)
 import GHC.TypeNats
-import Data.Finite (Finite, separateSum, separateProduct, combineProduct, weakenN, shiftN, strengthenN, finite)
+import Data.Finite (Finite, separateSum, separateProduct, combineProduct, weakenN, shiftN)
+import Data.Ord (Down(..))
+import Control.Monad.Primitive (PrimMonad(..))
+import Control.Monad (forM_)
+import GHC.TypeLits.Compare (isLE)
+import Data.Type.Equality ((:~:)(..))
+import Control.Monad.ST (ST, runST)
+import Foreign.Storable (Storable)
 
 import qualified Data.Bit as B
 import qualified Data.Bit.ThreadSafe as BTS
 import qualified Data.Vector.Sized as VS
+import qualified Data.Vector.Generic as VG
+import qualified Data.Vector.Mutable.Sized as VMS
+import qualified Data.Vector.Generic.Sized as VGS
+import qualified Data.Vector.Generic.Mutable as VGM
+import qualified Data.Vector.Generic.Mutable.Sized as VGMS
 import qualified Data.Vector.Unboxed.Sized as VUS
+import qualified Data.Vector.Unboxed.Mutable.Sized as VUMS
 import qualified Data.Vector.Storable.Sized as VSS
+import qualified Data.Vector.Storable.Mutable.Sized as VSMS
 
 import Data.Finitary.TH
 
--- | Witnesses an isomorphism between @a@ and @(KnownNat n) => Finite n@.
+-- | Witnesses an isomorphism between @a@ and some @(KnownNat n) => Finite n@.
 -- Effectively, a lawful instance of this shows that @a@ has exactly @n@
 -- (non-@_|_@) inhabitants, and that we have a bijection with 'fromFinite' and
 -- 'toFinite' as each \'direction\'.
@@ -133,19 +141,30 @@
 --
 --    * \[\texttt{fromFinite} \circ \texttt{toFinite} = \texttt{toFinite} \circ
 -- \texttt{fromFinite} = \texttt{id}\]
---    * \[\forall x, y :: \texttt{Finite} \; n \; \texttt{fromFinite} \; x = \texttt{fromFinite} \; y
+--    * \[\forall x, y :: \texttt{Finite} \; (\texttt{Cardinality} \; a) \; \texttt{fromFinite} \; x = \texttt{fromFinite} \; y
 -- \rightarrow x = y\]
---    * \[\forall x :: \texttt{Finite} \; n \; \exists y :: a \mid \texttt{fromFinite} \; x
+--    * \[\forall x :: \texttt{Finite} \; (\texttt{Cardinality} \; a) \; \exists y :: a \mid \texttt{fromFinite} \; x
 -- = y\]
 --
--- Additionally, if you define any of the other methods, these laws must hold:
+-- Furthermore, 'fromFinite' should be _order-preserving_. Namely, if @a@ is an
+-- instance of @Ord@, we must have:
 --
---    * \[ a \neq \emptyset \rightarrow \texttt{start} = \texttt{fromFinite} \; 0 \]
---    * \[ a \neq \emptyset \rightarrow \texttt{end} = \texttt{fromFinite} \; (n - 1)) \]
+--    * \[\forall i, j :: \texttt{Finite} \; (\texttt{Cardinality} \; a) \;
+--    \texttt{fromFinite} \; i \leq \texttt{fromFinite} \; j \rightarrow i \leq j \]
+--
+-- Lastly, if you define any of the other methods, these laws must hold:
+--
+--    * \[ a \neq \emptyset \rightarrow \texttt{start} = \texttt{fromFinite} \; \texttt{minBound} \]
+--    * \[ a \neq \emptyset \rightarrow \texttt{end} = \texttt{fromFinite} \; \texttt{maxBound} \]
 --    * \[ \forall x :: a \; \texttt{end} \neq x \rightarrow \texttt{next} \; x =
 -- (\texttt{fromFinite} \circ + 1 \circ \texttt{toFinite}) \; x \]
---    * \[ \forall x :: a \; \texttt{start} \neq x \rightarrow \texttt{prev} \; x =
+--    * \[ \forall i :: \texttt{Finite} \; (\texttt{Cardinality} \; a) \; \texttt{nextSkipping} \; i =
+--    \underbrace{\texttt{next} \circ \ldots \circ \texttt{next}}_{i} \]
+--    * \[ \forall x :: a \; \texttt{start} \neq x \rightarrow \texttt{previous} \; x =
 -- (\texttt{fromFinite} \circ - 1 \circ \texttt{toFinite}) \; x \]
+--    * \[ \forall i :: \texttt{Finite} \; (\texttt{Cardinality} \; a) \;
+--    \texttt{previousSkipping} \; i = \underbrace{\texttt{previous} \circ
+--    \ldots \circ \texttt{previous}}_{i} \] 
 --    * \[ \forall x :: a \; \texttt{enumerateFrom} \; x = \texttt{fromFinite <\$> [toFinite} \; x \texttt{..]} \]
 --    * \[ \forall x, y :: a \; \texttt{enumerateFromThen} \; x y =
 --    \texttt{fromFinite <\$> [toFinite} \; x \texttt{, }\; y \texttt{..]} \]
@@ -153,18 +172,21 @@
 --    \texttt{fromFinite <\$> [toFinite} \; x \texttt{..} \; y \texttt{]} \]
 --    * \[ \forall x, y, z :: a \; \texttt{enumerateFromThenTo} \; x \; y \; z =
 --    \texttt{fromFinite <\$> [toFinite} \; x \texttt{,} \; y \texttt{..} \; z \texttt{]} \] 
---
--- The default definitions follow these laws. Additionally, if you derive via
--- 'Generic', these are also followed for you.
---
--- Lastly, we /strongly/ suggest that @fromFinite@ and @toFinite@ should have
--- time complexity \(\Theta(1)\), or, if that's not possible, \(O(\texttt{n})\), where @n@ is the
--- cardinality of @a@. The latter is in effect for instances generated using
+-- 
+-- Together with the fact that @Finite n@ is well-ordered whenever @KnownNat n@
+-- holds, a law-abiding @Finitary@ instance for a type @a@ defines a constructive
+-- [well-order](https://en.wikipedia.org/wiki/Well-order), witnessed by
+-- 'toFinite' and 'fromFinite', which agrees with the @Ord@ instance for @a@, if
+-- any.
+-- 
+-- We /strongly/ suggest that @fromFinite@ and @toFinite@ should have
+-- time complexity \(\Theta(1)\), or, if that's not possible, \(O(\texttt{Cardinality} \; a)\). 
+-- The latter is the case for instances generated using
 -- @Generics@-based derivation, but not for \'basic\' types; thus, these
 -- functions for your derived types will only be as slow as their \'structure\',
 -- rather than their \'contents\', provided the contents are of these \'basic\'
 -- types. 
-class (KnownNat (Cardinality a)) => Finitary (a :: Type) where
+class (Eq a, KnownNat (Cardinality a)) => Finitary (a :: Type) where
   -- | How many (non-@_|_@) inhabitants @a@ has, as a typelevel natural number. 
   type Cardinality a :: Nat
   type Cardinality a = GCardinality (Rep a)
@@ -186,14 +208,27 @@
   -- or 'empty' if no such index exists.
   previous :: (Alternative f) => a -> f a
   previous = fmap fromFinite . guarded (== maxBound) . dec . toFinite
+  -- | @previousSkipping i x@ \'skips back\' @i@ index values from the index of
+  -- @x@, then gives the inhabitant whose index precedes the result, or 'empty'
+  -- if no such index exists.
+  previousSkipping :: (Alternative f) => Finite (Cardinality a) -> a -> f a
+  previousSkipping i x = fmap fromFinite . guarded (> index) . subtract i $ index
+    where index = toFinite x
   -- | @next x@ gives the inhabitant whose index follows the index of @x@, or
   -- 'empty' if no such index exists.
   next :: (Alternative f) => a -> f a
   next = fmap fromFinite . guarded (== minBound) . inc . toFinite
+  -- | @nextSkipping i x@ \'skips forward\' @i@ index values from the index of
+  -- @x@, then gives the inhabitant whose index follows the result, or 'empty'
+  -- if no such index exists.
+  nextSkipping :: (Alternative f) => Finite (Cardinality a) -> a -> f a
+  nextSkipping i x = fmap fromFinite . guarded (< index) . (+ i) $ index
+    where index = toFinite x
   -- | @enumerateFrom x@ gives a list of inhabitants, starting with @x@,
   -- followed by all other values whose indexes follow @x@, in index order.
   enumerateFrom :: a -> [a]
   enumerateFrom x = fromFinite <$> [toFinite x ..]
+  -- | Like @enumerateFrom@, except in steps of @toFinite y - toFinite x@.
   enumerateFromThen :: a -> a -> [a]
   enumerateFromThen x y = fromFinite <$> [toFinite x, toFinite y ..]
   -- | @enumerateFromTo x y@ gives a list of inhabitants, starting with @x@,
@@ -201,6 +236,7 @@
   -- those of @x@ and @y@. The list is in index order.
   enumerateFromTo :: a -> a -> [a]
   enumerateFromTo x y = fromFinite <$> [toFinite x .. toFinite y]
+  -- | Like @enumerateFromTo@, except in steps of @toFinite y - toFinite x@.
   enumerateFromThenTo :: a -> a -> a -> [a]
   enumerateFromThenTo x y z = fromFinite <$> [toFinite x, toFinite y .. toFinite z]
 
@@ -331,6 +367,8 @@
   next = fmap succ . guarded (/= maxBound)
   {-# INLINE previous #-}
   previous = fmap pred . guarded (/= minBound)
+  {-# INLINE previousSkipping #-}
+  previousSkipping i = fmap toEnum . guarded (>= 0) . subtract (fromIntegral i) . fromEnum
   {-# INLINE enumerateFrom #-}
   enumerateFrom = enumFrom
   {-# INLINE enumerateFromThen #-}
@@ -354,6 +392,8 @@
   next = fmap succ . guarded (/= maxBound)
   {-# INLINE previous #-}
   previous = fmap pred . guarded (/= minBound)
+  {-# INLINE previousSkipping #-}
+  previousSkipping i = fmap fromIntegral . guarded (>= 0) . subtract (fromIntegral i) . fromIntegral @_ @Int
   {-# INLINE enumerateFrom #-}
   enumerateFrom = enumFrom
   {-# INLINE enumerateFromThen #-}
@@ -377,6 +417,8 @@
   next = fmap succ . guarded (/= maxBound)
   {-# INLINE previous #-}
   previous = fmap pred . guarded (/= minBound)
+  {-# INLINE previousSkipping #-}
+  previousSkipping i = fmap fromIntegral . guarded (>= 0) . subtract (fromIntegral i) . fromIntegral @_ @Int
   {-# INLINE enumerateFrom #-}
   enumerateFrom = enumFrom
   {-# INLINE enumerateFromThen #-}
@@ -400,6 +442,8 @@
   next = guarded (== minBound) . inc
   {-# INLINE previous #-}
   previous = guarded (== maxBound) . dec
+  {-# INLINE previousSkipping #-}
+  previousSkipping i = fmap fromIntegral . guarded (>= 0) . subtract (fromIntegral i) . fromIntegral @_ @Integer
   {-# INLINE enumerateFrom #-}
   enumerateFrom = enumFrom
   {-# INLINE enumerateFromThen #-}
@@ -423,6 +467,8 @@
   next = guarded (== minBound) . inc
   {-# INLINE previous #-}
   previous = guarded (== maxBound) . dec
+  {-# INLINE previousSkipping #-}
+  previousSkipping i = fmap fromIntegral . guarded (>= 0) . subtract (fromIntegral i) . fromIntegral @_ @Integer
   {-# INLINE enumerateFrom #-}
   enumerateFrom = enumFrom
   {-# INLINE enumerateFromThen #-}
@@ -567,6 +613,8 @@
   next = guarded (== minBound) . inc
   {-# INLINE previous #-}
   previous = guarded (== maxBound) . dec
+  {-# INLINE previousSkipping #-}
+  previousSkipping i = fmap fromIntegral . guarded (>= 0) . subtract (fromIntegral i) . fromIntegral @_ @Integer
   {-# INLINE enumerateFrom #-}
   enumerateFrom = enumFrom
   {-# INLINE enumerateFromThen #-}
@@ -592,6 +640,8 @@
   next = guarded (== minBound) . inc
   {-# INLINE previous #-}
   previous = guarded (== maxBound) . dec
+  {-# INLINE previousSkipping #-}
+  previousSkipping i = guarded (< i) . subtract i
   {-# INLINE enumerateFrom #-}
   enumerateFrom = enumFrom
   {-# INLINE enumerateFromThen #-}
@@ -622,33 +672,8 @@
 
 instance (Finitary a) => Finitary (Const a b)
 
-#if MIN_VERSION_base(4,12,0)
-instance (Finitary a) => Finitary (Down a)
-#else
-instance (Finitary a) => Finitary (Down a) where
-  type Cardinality (Down a) = Cardinality a
-  {-# INLINE fromFinite #-}
-  fromFinite = Down . fromFinite
-  {-# INLINE toFinite #-}
-  toFinite = toFinite . op Down
-  {-# INLINE start #-}
-  start = Down start
-  {-# INLINE end #-}
-  end = Down end
-  {-# INLINE previous #-}
-  previous = fmap Down . previous . op Down
-  {-# INLINE next #-}
-  next = fmap Down . next . op Down
-  {-# INLINE enumerateFrom #-}
-  enumerateFrom = fmap Down . enumerateFrom . op Down
-  {-# INLINE enumerateFromThen #-}
-  enumerateFromThen (Down x) (Down y) = fmap Down . enumerateFromThen x $ y
-  {-# INLINE enumerateFromTo #-}
-  enumerateFromTo (Down x) (Down y) = fmap Down . enumerateFromTo x $ y
-  {-# INLINE enumerateFromThenTo #-}
-  enumerateFromThenTo (Down x) (Down y) (Down z) = fmap Down . enumerateFromThenTo x y $ z
-#endif
-
+-- | For any @newtype@-esque thing over a type with a @Finitary@ instance, we
+-- can just \'inherit\' the behaviour of @a@.
 instance (Finitary a) => Finitary (Sum a)
 
 instance (Finitary a) => Finitary (Product a)
@@ -665,56 +690,72 @@
 
 instance (Finitary a) => Finitary (Min a)
 
--- | We can treat explicitly-sized @Vector@s as a fixed-length string over a
--- finite alphabet, with the cardinality of the alphabet being the same as the
--- cardinality of @a@. Thus, we can \'number off\' the possible @Vector@s starting
--- with the one where every position is @start :: a@, and finishing with the one
--- where every position is @end :: a@.
-instance (Finitary a, KnownNat n, Cardinality a <= Cardinality a ^ n) => Finitary (VS.Vector n a) where
+-- | Despite the @newtype@-esque nature of @Down@, due to the requirement that
+-- 'fromFinite' is order-preserving, the instance for @Down a@ reverses the
+-- indexing.
+instance (Finitary a) => Finitary (Down a) where
+  type Cardinality (Down a) = Cardinality a
+  {-# INLINE fromFinite #-}
+  fromFinite = Down . fromFinite . opp
+    where opp = fromIntegral @_ @(Finite (Cardinality a)) . (`mod` n) . (* (n - 1)) . (+ 1) . fromIntegral @_ @Natural 
+          n = natVal @(Cardinality a) Proxy
+  {-# INLINE toFinite #-}
+  toFinite = fromIntegral @_ @(Finite (Cardinality a)) . (`mod` n) . (* (n - 1)) . (+ 1) . fromIntegral @_ @Natural . toFinite . op Down
+    where n = natVal @(Cardinality a) Proxy 
+
+-- | A fixed-length vector over a type @a@ with an instance of @Finitary@ can be
+-- thought of as a fixed-length word over an alphabet of size @Cardinality a@.
+-- Since there are only finitely-many of these, we can index them in lex order,
+-- with the ordering determined by the @Finitary a@ instance (thus, the
+-- \'first\' such @Vector@ is the one where each element is @start :: a@, and
+-- the \'last\' is the one where each element is @end :: a@).
+instance (Finitary a, KnownNat n) => Finitary (VS.Vector n a) where
   type Cardinality (VS.Vector n a) = Cardinality a ^ n
   {-# INLINE fromFinite #-}
-  fromFinite = evalState (VS.replicateM (unrank typeSize))
-    where typeSize = finite @(Cardinality (VS.Vector n a)) . fromIntegral . natVal @(Cardinality a) $ Proxy
+  fromFinite i = runST (go i)
+    where go :: Finite (Cardinality (VS.Vector n a)) -> ST s (VS.Vector n a)
+          go ix = do v <- VMS.new
+                     unroll v ix
+                     VS.unsafeFreeze v
   {-# INLINE toFinite #-}
-  toFinite v = evalState go base
-    where go = VS.foldM' (accumStep base) minBound v
-          base = finite @(Cardinality (VS.Vector n a)) . fromIntegral . natVal @(Cardinality a) $ Proxy
+  toFinite = roll
 
-instance (Finitary a, VUS.Unbox a, KnownNat n, Cardinality a <= Cardinality a ^ n) => Finitary (VUS.Vector n a) where
+instance (Finitary a, VUMS.Unbox a, KnownNat n) => Finitary (VUS.Vector n a) where
   type Cardinality (VUS.Vector n a) = Cardinality a ^ n
   {-# INLINE fromFinite #-}
-  fromFinite = evalState (VUS.replicateM (unrank typeSize))
-    where typeSize = finite @(Cardinality (VUS.Vector n a)) . fromIntegral . natVal @(Cardinality a) $ Proxy
+  fromFinite i = runST (go i)
+    where go :: Finite (Cardinality (VUS.Vector n a)) -> ST s (VUS.Vector n a)
+          go ix = do v <- VUMS.new
+                     unroll v ix
+                     VUS.unsafeFreeze v
   {-# INLINE toFinite #-}
-  toFinite v = evalState go base
-    where go = VUS.foldM' (accumStep base) minBound v
-          base = finite @(Cardinality (VUS.Vector n a)) . fromIntegral . natVal @(Cardinality a) $ Proxy
+  toFinite = roll
 
-instance (Finitary a, Storable a, KnownNat n, Cardinality a <= Cardinality a ^ n) => Finitary (VSS.Vector n a) where
+instance (Finitary a, Storable a, KnownNat n) => Finitary (VSS.Vector n a) where
   type Cardinality (VSS.Vector n a) = Cardinality a ^ n
   {-# INLINE fromFinite #-}
-  fromFinite = evalState (VSS.replicateM (unrank typeSize))
-    where typeSize = finite @(Cardinality (VSS.Vector n a)) . fromIntegral . natVal @(Cardinality a) $ Proxy
+  fromFinite i = runST (go i)
+    where go :: Finite (Cardinality (VSS.Vector n a)) -> ST s (VSS.Vector n a)
+          go ix = do v <- VSMS.new
+                     unroll v ix
+                     VSS.unsafeFreeze v
   {-# INLINE toFinite #-}
-  toFinite v = evalState go base
-    where go = VSS.foldM' (accumStep base) minBound v
-          base = finite @(Cardinality (VSS.Vector n a)) . fromIntegral . natVal @(Cardinality a) $ Proxy
+  toFinite = roll
 
 -- Helpers
- 
-{-# INLINE unrank #-}
-unrank :: (MonadState (Finite n) m, Finitary a, KnownNat n, (Cardinality a) <= n) => Finite n -> m a
-unrank typeSize = do remaining <- get
-                     let (d, r) = remaining `divMod` typeSize
-                     put d
-                     return (fromFinite . fromJust . strengthenN $ r)
 
-{-# INLINE accumStep #-}
-accumStep :: (MonadState (Finite n) m, Finitary a, KnownNat n, (Cardinality a) <= n) => Finite n -> Finite n -> a -> m (Finite n)
-accumStep base total e = do let e' = weakenN . toFinite $ e
-                            ex <- get
-                            modify (* base)
-                            return (total + (e' * ex))
+unroll :: forall a m v n . (Finitary a, PrimMonad m, KnownNat n, VGM.MVector v a) => VGMS.MVector v n (PrimState m) a -> Finite (Cardinality a ^ n) -> m ()
+unroll v acc = forM_ @_ @_ @_ @() (isLE (Proxy @1) (Proxy @n)) 
+                               (\Refl -> do let (d, r) = separateProduct @(Cardinality a ^ (n -1)) @(Cardinality a) acc
+                                            let x = fromFinite r
+                                            VGMS.write v 0 x
+                                            unroll (VGMS.tail v) d)
+
+roll :: forall a v n . (Finitary a, VG.Vector v a, KnownNat n) => VGS.Vector v n a -> Finite (Cardinality a ^ n)
+roll v = case isLE (Proxy @1) (Proxy @n) of
+          Nothing -> 0
+          Just Refl -> let (h, t) = (VGS.head v, VGS.tail v) in
+                          combineProduct (roll t, toFinite h) 
 
 {-# INLINE inc #-}
 inc :: (Num a) => a -> a
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -1,3 +1,20 @@
+{-
+ - Copyright (C) 2019  Koz Ross <koz.ross@retro-freedom.nz>
+ -
+ - This program is free software: you can redistribute it and/or modify
+ - it under the terms of the GNU General Public License as published by
+ - the Free Software Foundation, either version 3 of the License, or
+ - (at your option) any later version.
+ -
+ - This program is distributed in the hope that it will be useful,
+ - but WITHOUT ANY WARRANTY; without even the implied warranty of
+ - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ - GNU General Public License for more details.
+ -
+ - You should have received a copy of the GNU General Public License
+ - along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ -}
+
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE TypeInType #-}
@@ -12,6 +29,7 @@
 
 module Main where
 
+import Data.Ord (Down)
 import Data.Maybe (isNothing)
 import Data.Int (Int8, Int16, Int32, Int64)
 import Data.Word (Word8, Word16, Word32, Word64)
@@ -37,16 +55,26 @@
 
 -- A representation of types
 data SomeFinitaryRep where
-  SomeFinitaryRep :: forall (a :: Type) . (Finitary a, Show a, Eq a, Typeable a, 1 <= (Cardinality a)) => Proxy a -> SomeFinitaryRep
+  SomeFinitaryRep :: forall (a :: Type) . (Finitary a, Ord a, Show a, Typeable a, 1 <= (Cardinality a)) => Proxy a -> SomeFinitaryRep
 
 -- A representation of test functions
 data SomeTestFunction where
-  SomeTestFunction :: (forall (a :: Type) . (Finitary a, Show a, Eq a, 1 <= (Cardinality a)) => Proxy a -> Property) -> SomeTestFunction
+  SomeTestFunction :: (forall (a :: Type) . (Finitary a, Ord a, Show a, 1 <= (Cardinality a)) => Proxy a -> Property) -> SomeTestFunction
 
 -- Some weird generic
 data Foo = Bar | Baz (VS.Vector 4 Bool) | Quux Word8
-  deriving (Eq, Show, Typeable, Generic, Finitary)
+  deriving (Eq, Show, Typeable, Generic, Finitary, Ord)
 
+-- Something I will need for further tests
+iterateMN :: forall (m :: Type -> Type) (a :: Type) (b :: Type) . (Eq a, Bounded a, Enum a, Monad m) => a -> (b -> m b) -> b -> m b
+iterateMN i f x = if i == minBound
+                  then f x
+                  else iterateMN (pred i) f x >>= f
+
+-- How much testing do I want to do for random inputs?
+testLimit :: forall (a :: Type) (b :: Type) . (Finitary a, Num b) => b
+testLimit = fromIntegral . (* 2) . min 32767 . natVal $ Proxy @(Cardinality a) 
+
 -- Generators
 choose :: forall (a :: Type) m . (MonadGen m, Finitary a) => m a
 choose = fromFinite <$> chooseFinite
@@ -75,6 +103,7 @@
   SomeFinitaryRep @Int64 Proxy,
   SomeFinitaryRep @Int Proxy,
   SomeFinitaryRep @Word Proxy,
+  SomeFinitaryRep @(Down Int) Proxy,
   SomeFinitaryRep @(Maybe Word8) Proxy,
   SomeFinitaryRep @(Either Word8 Int8) Proxy,
   SomeFinitaryRep @(Word8, Int8) Proxy,
@@ -89,12 +118,16 @@
   where go (SomeFinitaryRep p) = (fromString . show . typeRep $ p, testFunc p)
 
 -- Properties
-isBijection :: forall (a :: Type) . (Finitary a, Show a, Eq a) => Proxy a -> Property
-isBijection _ = withTests testLimit (property $ do x <- forAll $ choose @a
-                                                   x === (fromFinite . toFinite $ x))
-  where testLimit = fromIntegral . (* 2) . min 32767 . natVal @(Cardinality a) $ Proxy
+isBijection :: forall (a :: Type) . (Finitary a, Show a) => Proxy a -> Property
+isBijection _ = withTests (testLimit @a) (property $ do x <- forAll $ choose @a
+                                                        x === (fromFinite . toFinite $ x))
 
-startIsCorrect :: forall (a :: Type) . (Finitary a, Show a, Eq a, 1 <= (Cardinality a)) => Proxy a -> Property
+isOrderPreserving :: forall (a :: Type) . (Finitary a, Ord a) => Proxy a -> Property
+isOrderPreserving _ = withTests (testLimit @a) (property $ do i <- forAll $ chooseFinite @(Cardinality a)
+                                                              j <- forAll $ chooseFinite @(Cardinality a)
+                                                              assert (fromFinite @a i > fromFinite @a j || i <= j)) 
+
+startIsCorrect :: forall (a :: Type) . (Finitary a, Show a, 1 <= (Cardinality a)) => Proxy a -> Property
 startIsCorrect _ = property $ start @a === fromFinite minBound
 
 previousStartNothing :: forall (a :: Type) . (Finitary a, 1 <= (Cardinality a)) => Proxy a -> Property
@@ -103,16 +136,40 @@
 endNextNothing :: forall (a :: Type) . (Finitary a, 1 <= (Cardinality a)) => Proxy a -> Property
 endNextNothing _ = property $ assert (isNothing . next $ end @a)
 
-endIsCorrect :: forall (a :: Type) . (Finitary a, Show a, Eq a, 1 <= (Cardinality a)) => Proxy a -> Property
+endIsCorrect :: forall (a :: Type) . (Finitary a, Show a, 1 <= (Cardinality a)) => Proxy a -> Property
 endIsCorrect _ = property $ end @a === fromFinite maxBound
 
+skipZeroIsPrevious :: forall (a :: Type) . (Finitary a, Show a) => Proxy a -> Property
+skipZeroIsPrevious _ = withTests (testLimit @a) (property $ do x <- forAll $ choose @a
+                                                               previous @a @Maybe x === previousSkipping 0 x)
+
+skipZeroIsNext :: forall (a :: Type) . (Finitary a, Show a) => Proxy a -> Property
+skipZeroIsNext _ = withTests (testLimit @a) (property $ do x <- forAll $ choose @a
+                                                           next @a @Maybe x === nextSkipping 0 x)
+
+skipNPreviousAgrees :: forall (a :: Type) . (Finitary a, Show a) => Proxy a -> Property
+skipNPreviousAgrees _ = withTests (testLimit @a) (property $ do x <- forAll $ choose @a
+                                                                i <- forAll $ choose @(Finite (Cardinality a))
+                                                                iterateMN @Maybe i previous x === previousSkipping i x)
+
+skipNNextAgrees :: forall (a :: Type) . (Finitary a, Show a) => Proxy a -> Property
+skipNNextAgrees _ = withTests (testLimit @a) (property $ do x <- forAll $ choose @a
+                                                            i <- forAll $ choose @(Finite (Cardinality a))
+                                                            iterateMN @Maybe i next x === nextSkipping i x)
+
+-- All the tests I want to use
 allTests :: [(SomeTestFunction, GroupName)]
 allTests = [
   (SomeTestFunction isBijection, "bijectivity"),
+  (SomeTestFunction isOrderPreserving, "order preservation"),
   (SomeTestFunction startIsCorrect, "start"),
   (SomeTestFunction endIsCorrect, "end"),
   (SomeTestFunction previousStartNothing, "previous + start"),
-  (SomeTestFunction endNextNothing, "next + end")
+  (SomeTestFunction endNextNothing, "next + end"),
+  (SomeTestFunction skipZeroIsPrevious, "previousSkipping 0"),
+  (SomeTestFunction skipZeroIsNext, "nextSkipping 0"),
+  (SomeTestFunction skipNPreviousAgrees, "previousSkipping n"),
+  (SomeTestFunction skipNNextAgrees, "nextSkipping n")
   ]
 
 main :: IO Bool