diff --git a/Data/Vector/Sized.hs b/Data/Vector/Sized.hs
--- a/Data/Vector/Sized.hs
+++ b/Data/Vector/Sized.hs
@@ -165,21 +165,23 @@
 
 -- | 'reverse' @xs@ returns the elements of xs in reverse order. @xs@ must be finite.
 reverse :: forall a n. Vector a n -> Vector a n
-reverse xs0 = case plusZR (sLength xs0) of Refl -> go Nil xs0
+reverse xs0 = coerce (plusZR (sLength xs0)) $ go Nil xs0
   where
     go :: Vector a m -> Vector a k -> Vector a (k :+ m)
     go acc Nil = acc
-    go acc (x :- xs) = case plusSR (sLength xs) (sLength acc) of Refl -> go (x:- acc) xs
+    go acc (x :- xs) = coerce (symmetry $ plusSR (sLength xs) (sLength acc)) $ go (x:- acc) xs
          
 -- | The 'intersperse' function takes an element and a vector and
 -- \`intersperses\' that element between the elements of the vector.
 intersperse :: a -> Vector a n -> Vector a ((Two :* n) :- One)
 intersperse _ Nil = Nil
-intersperse a (x :- xs) = case plusSR (sLength xs) (sLength xs) of Refl -> x :- prependToAll a xs
+intersperse a (x :- xs) =
+  coerce (plusSR (sLength xs) (sLength xs)) $ x :- prependToAll a xs
 
 prependToAll :: a -> Vector a n -> Vector a (Two :* n)
 prependToAll _ Nil = Nil
-prependToAll a (x :- xs) = case plusSR (sLength xs) (sLength xs) of Refl -> x :- a :- prependToAll a xs
+prependToAll a (x :- xs) =
+  x :- (coerce (plusSR (sLength xs) (sLength xs)) $ a :- prependToAll a xs)
 
 -- | The 'transpose' function transposes the rows and columns of its argument.
 transpose :: SingRep n => Vector (Vector a n) m -> Vector (Vector a m) n
@@ -230,8 +232,7 @@
 concat (xs :- xss) =
   let n = sLength xs
       n0 = sLength xss
-  in case plusCommutative (n0 %* n) n of
-       Refl -> xs `append` concat xss
+  in coerce (symmetry $ plusCommutative (n0 %* n) n) $ xs `append` concat xss
 
 and, or :: Vector Bool m -> Bool
 -- | 'and' returns the conjunction of a Boolean vector.
diff --git a/bench/coercion.hs b/bench/coercion.hs
new file mode 100644
--- /dev/null
+++ b/bench/coercion.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE QuasiQuotes #-}
+module Main where
+import           Control.DeepSeq
+import           Control.Parallel.Strategies
+import           Criterion
+import           Data.Type.Natural
+import qualified Data.Vector.Sized           as V
+import           Progression.Main
+import           System.Environment
+
+main :: IO ()
+main = do
+  name : rest <- getArgs
+  v10 <- return $!! ((V.replicate [snat|10|] ()) `using` rdeepseq)
+  v100 <- return $!! ((V.replicate [snat|100|] ()) `using` rdeepseq)
+  v200 <- return $!! ((V.replicate [snat|200|] ()) `using` rdeepseq)
+  withArgs (("-n"++name) : rest) $
+    defaultMain $
+    bgroup "bench" [ bgroup "reverse"
+                     [ bench "10" $ nf V.reverse v10
+                     , bench "100" $ nf V.reverse v100
+                     , bench "1000" $ nf V.reverse v200
+                     ]
+                   , bgroup "intersperse"
+                     [ bench "10" $ nf (V.intersperse ()) v10
+                     , bench "100" $ nf (V.intersperse ()) v100
+                     , bench "200" $ nf (V.intersperse ()) v200
+                     ]
+                   ]
diff --git a/sized-vector.cabal b/sized-vector.cabal
--- a/sized-vector.cabal
+++ b/sized-vector.cabal
@@ -2,7 +2,7 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                sized-vector
-version:             1.2.0.0
+version:             1.3.0.0
 synopsis:            Size-parameterized vector types and functions.
 description:         Size-parameterized vector types and functions using a data-type promotion.
 homepage:            https://github.com/konn/sized-vector
@@ -21,10 +21,24 @@
 
 library
   exposed-modules:     Data.Vector.Sized
-  build-depends:       base                     >= 2.0 && < 5
+  build-depends:       base                     >= 2.0          && < 5
                ,       singletons               == 0.8.*
-               ,       type-natural             >= 0.0.4.0
+               ,       type-natural             == 0.1.*
+               ,       constraints
                ,       monomorphic              == 0.0.*
-               ,       equational-reasoning     == 0.0.*
+               ,       equational-reasoning     >= 0.0.3        && < 0.1
                ,       hashable                 == 1.1.*
                ,       deepseq                  == 1.3.*
+
+Benchmark coercion-bench
+  type:                 exitcode-stdio-1.0
+  main-is:              coercion.hs
+  hs-source-dirs:       bench
+  ghc-options:          -O2 -threaded -fcontext-stack=500
+  build-depends:        criterion
+               ,        progression
+               ,        sized-vector
+               ,        base
+               ,        type-natural
+               ,        parallel
+               ,        deepseq