diff --git a/Data/Vector/Sized.hs b/Data/Vector/Sized.hs
--- a/Data/Vector/Sized.hs
+++ b/Data/Vector/Sized.hs
@@ -42,13 +42,14 @@
 import           Data.Maybe                 (Maybe (..), fromMaybe, listToMaybe)
 import           Data.Singletons            (SingI, SingInstance (..), sing)
 import           Data.Singletons            (singInstance)
+import           Data.Type.Equality         (sym)
 import           Data.Type.Monomorphic      (Monomorphic (..),
                                              Monomorphicable (..))
 import           Data.Type.Natural          ((:*), (:+), (:-), (:-:), (:<<=),
                                              Min)
 import           Data.Type.Natural          (Nat (..), One, SNat, Sing (..),
                                              Two)
-import           Data.Type.Natural          (plusCommutative, plusSR, plusZR)
+import           Data.Type.Natural          (plusComm, plusSuccR, plusZR)
 import           Data.Type.Natural          (sNatToInt, (%:*))
 import           Data.Type.Ordinal          (Ordinal (..), ordToInt)
 import           Language.Haskell.TH
@@ -204,19 +205,19 @@
   where
     go :: Vector a m -> Vector a k -> Vector a (k :+ m)
     go acc Nil = acc
-    go acc (x :- xs) = coerce (symmetry $ plusSR (sLength xs) (sLength acc)) $ go (x:- acc) xs
+    go acc (x :- xs) = coerce (plusSuccR (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) =
-  coerce (plusSR (sLength xs) (sLength xs)) $ x :- prependToAll a xs
+  coerce (sym $ plusSuccR (sLength xs) (sLength xs)) $ x :- prependToAll a xs
 
 prependToAll :: a -> Vector a n -> Vector a (Two :* n)
 prependToAll _ Nil = Nil
 prependToAll a (x :- xs) =
-  x :- (coerce (plusSR (sLength xs) (sLength xs)) $ a :- prependToAll a xs)
+  x :- (coerce (sym $ plusSuccR (sLength xs) (sLength xs)) $ a :- prependToAll a xs)
 
 -- | The 'transpose' function transposes the rows and columns of its argument.
 transpose :: SingI n => Vector (Vector a n) m -> Vector (Vector a m) n
@@ -267,7 +268,7 @@
 concat (xs :- xss) =
   let n = sLength xs
       n0 = sLength xss
-  in coerce (symmetry $ plusCommutative (n0 %:* n) n) $ xs `append` concat xss
+  in coerce (plusComm n (n0 %:* n)) $ xs `append` concat xss
 
 and, or :: Vector Bool m -> Bool
 -- | 'and' returns the conjunction of a Boolean vector.
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.4.3.0
+version:             1.4.3.1
 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
@@ -11,29 +11,29 @@
 extra-source-files:  README.md
 author:              Hiromi ISHII
 maintainer:          konn.jinro_at_gmail.com
-copyright:           (C) Hiromi ISHII 2013
+copyright:           (C) Hiromi ISHII 2013-2016
 category:            Data
 build-type:          Simple
 cabal-version:       >=1.8
-tested-with:   GHC == 7.10.2, GHC == 7.8.3, GHC == 7.8.4
+tested-with:   GHC == 7.10.3, GHC == 8.0.1
 source-repository head
   Type: git
   Location: git://github.com/konn/sized-vector.git
 
 library
   exposed-modules:     Data.Vector.Sized
-  build-depends:       base                     >= 2.0          && < 5
+  build-depends:       base                     >= 4.8          && < 5
                      , constraints
                      , deepseq                  >= 1.3          && < 1.5
-                     , equational-reasoning     >= 0.2          && < 0.3
+                     , equational-reasoning     >= 0.4          && < 0.5
                      , hashable                 >= 1.1          && < 1.3
                      , monomorphic              == 0.0.*
-                     , template-haskell         >= 2.9.0.0      && < 2.11
-                     , type-natural             >= 0.1          && < 0.4
-  if impl(ghc < 7.7)
-    build-depends:     singletons               == 0.8.*
-  if impl(ghc >= 7.7)
-    build-depends:     singletons               >= 1.0          && < 3
+                     , template-haskell         >= 2.9.0.0      && < 2.12
+                     , type-natural             >= 0.4.1        && < 0.5
+  if impl(ghc >= 8.0)
+    build-depends:     singletons               >= 2.2          && < 3
+  else
+    build-depends:     singletons               == 2.1.*
 
 -- Benchmark coercion-bench
 --   buildable:            False