diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,6 +1,8 @@
 # tensors
 
-[![Hackage](https://img.shields.io/badge/hackage-v0.1.2-orange.svg)](https://hackage.haskell.org/package/tensors)
+[![Hackage](https://img.shields.io/hackage/v/tensors.svg)](https://hackage.haskell.org/package/tensors)
+[![stackage LTS package](http://stackage.org/package/tensors/badge/lts)](http://stackage.org/lts/package/tensors)
+[![stackage Nightly package](http://stackage.org/package/tensors/badge/nightly)](http://stackage.org/nightly/package/tensors)
 [![Build Status](https://travis-ci.org/leptonyu/tensors.svg?branch=master)](https://travis-ci.org/leptonyu/tensors)
 
 
diff --git a/bench/Bench.hs b/bench/Bench.hs
new file mode 100644
--- /dev/null
+++ b/bench/Bench.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE OverloadedLists #-}
+module Main where
+
+import           Criterion.Main
+import           Data.Tensor
+
+base = [1..10000] :: Tensor '[100,100] Int
+b2se = clone base
+b3se = [1..100] :: Tensor '[10,10] Int
+
+main = defaultMain
+  [ bgroup "tensor"
+    [ bench "identity"    $ nf id (identity :: Tensor '[100,100] Int)
+    , bench "clone"       $ nf clone base
+    , bench "dyad"        $ nf id (b3se  `dyad` b3se)
+    , bench "dot"         $ nf id (base  `dot`  base)
+    , bench "dot-2"       $ nf id (b2se  `dot`  b2se)
+    , bench "contraction" $ nf (contraction (i0,i1)) base
+    ]
+  ]
diff --git a/src/Data/Tensor.hs b/src/Data/Tensor.hs
--- a/src/Data/Tensor.hs
+++ b/src/Data/Tensor.hs
@@ -89,7 +89,6 @@
   , Transpose
   , transpose
   , Swapaxes
-  , CheckSwapaxes
   , swapaxes
   -- ** Dyadic Tensor
   , dyad'
@@ -98,16 +97,14 @@
   , DotTensor
   , dot
   -- ** Contraction Tensor
-  , CheckContraction
   , Contraction
-  , TensorDim
+  , Dimension
   , DropIndex
   , contraction
   -- ** Tensor Selection
   , (!)
-  , CheckDim
+  , CheckDimension
   , CheckSelect
-  , Select
   , select
   , CheckSlice
   , Slice
@@ -125,7 +122,6 @@
   , linspace
   , geospace
   , logspace
-  , CheckGrid
   , grid
   , meshgrid2
   , meshgrid3
@@ -161,7 +157,6 @@
   , i9
   ) where
 
-import           Data.Tensor.Index
 import           Data.Tensor.Matrix
 import           Data.Tensor.Space
 import           Data.Tensor.Statistics
diff --git a/src/Data/Tensor/Index.hs b/src/Data/Tensor/Index.hs
deleted file mode 100644
--- a/src/Data/Tensor/Index.hs
+++ /dev/null
@@ -1,48 +0,0 @@
-{-# LANGUAGE UndecidableInstances #-}
-module Data.Tensor.Index where
-
-import           Data.Proxy
-import           Data.Reflection
-import           Data.Singletons
-import qualified Data.Singletons.Prelude.List as N
-import           Data.Tensor.Type
-import           GHC.Exts
-import           GHC.TypeLits
-
--- | Tensor Index, used to locate each point of tensor
-newtype TensorIndex (shape :: [Nat]) = TensorIndex Index deriving (Eq,Show,Ord)
-
-instance forall s. SingI s => Bounded (TensorIndex s) where
-  minBound = toEnum 0
-  maxBound = let s = natsVal (Proxy :: Proxy s) in  toEnum (product s - 1)
-
-instance forall s. SingI s =>  Enum (TensorIndex s) where
-  toEnum i   = let s = natsVal (Proxy :: Proxy s) in TensorIndex $ viToti s i
-  fromEnum (TensorIndex i) = let s = natsVal (Proxy :: Proxy s) in tiTovi s i
-
-instance forall s. SingI s => IsList (TensorIndex s) where
-  type Item (TensorIndex s) = Int
-  fromList v =
-    let s = natsVal (Proxy :: Proxy s)
-    in if length v /= length s then error "length not match"
-        else if or (zipWith (\i n-> i <0 || i >= n) v s) then error "index overflow"
-          else TensorIndex v
-  toList (TensorIndex v) = v
-
-
--- | Tensor rank.
-type TensorRank (s :: [Nat]) = N.Length s
-
--- type TensorRankConstraint s i = N.And '[ (N.>=) i 0, (N.<) i (TensorRank s)]
-data TensorRankIndex (shape :: [Nat]) = forall (i :: Nat). KnownNat i => TensorRankIndex (Proxy i)
-
-instance SingI s => Show (TensorRankIndex s) where
-  show = show . fromEnum
-
-instance forall s. (SingI s, KnownNat (TensorRank s - 1)) => Bounded (TensorRankIndex s) where
-  minBound = TensorRankIndex i0
-  maxBound = TensorRankIndex (Proxy :: Proxy (TensorRank s - 1))
-
-instance forall (s::[Nat]). (SingI s) => Enum (TensorRankIndex s) where
-  toEnum i =  reifyNat (toInteger i) TensorRankIndex
-  fromEnum (TensorRankIndex p) = fromInteger $ natVal p
diff --git a/src/Data/Tensor/Space.hs b/src/Data/Tensor/Space.hs
--- a/src/Data/Tensor/Space.hs
+++ b/src/Data/Tensor/Space.hs
@@ -1,11 +1,9 @@
 module Data.Tensor.Space where
 
 import           Data.Proxy
-import qualified Data.Singletons.Prelude      as N
-import qualified Data.Singletons.Prelude.List as N
 import           Data.Tensor.Tensor
 import           Data.Tensor.Type
-import qualified Data.Vector                  as V
+import qualified Data.Vector        as V
 import           GHC.TypeLits
 
 -- | Return evenly spaced numbers over a specified interval.
@@ -43,8 +41,6 @@
             v  = V.generate (fromInteger count) (g d start . toInteger)
         in Tensor $ \s i -> v V.! tiTovi s i
 
-
-type CheckGrid i a s = N.And '[ (N.>=) i 0, (N.<) i (N.Length s)]
 -- | Grid
 --
 -- > λ> a = [1..2] :: Vector 2 Int
@@ -66,11 +62,11 @@
 -- > [[1,2],
 -- > [1,2]]]
 grid
-  :: (CheckDim i s ~ 'True
+  :: (CheckDimension i s ~ 'True
     , KnownNat i
-    , KnownNat (TensorDim s i))
+    , KnownNat (Dimension s i))
   => Proxy i
-  -> Vector (TensorDim s i) n
+  -> Vector (Dimension s i) n
   -> Tensor s n
 grid p v@(Tensor t) =
   let i = toNat p
diff --git a/src/Data/Tensor/Statistics.hs b/src/Data/Tensor/Statistics.hs
--- a/src/Data/Tensor/Statistics.hs
+++ b/src/Data/Tensor/Statistics.hs
@@ -1,13 +1,13 @@
 module Data.Tensor.Statistics where
 
-import           Data.Singletons
 import           Data.Tensor.Tensor
+import           Data.Tensor.Type
 
 -- | Average of tensor
 --
 -- > λ> average (identity :: Tensor '[3,3] Float)
 -- > 0.33333334
-average :: forall s n. (SingI s, Fractional n) => Tensor s n -> n
+average :: forall s n. (HasShape s, Fractional n) => Tensor s n -> n
 average t =
   let v = sum t
       s = fromInteger $ toInteger $ product $ shape t
@@ -17,7 +17,7 @@
 --
 -- > λ> var ([1,2,3,4] :: Vector 4 Double )
 -- > 1.25
-var :: forall s n. (SingI s, Fractional n) => Tensor s n -> n
+var :: forall s n. (HasShape s, Fractional n) => Tensor s n -> n
 var t =
   let m = average t
       r = fmap (\v -> let x = v - m in x * x) t
@@ -27,5 +27,6 @@
 --
 -- > λ> std ([1,2,3,4] :: Vector 4 Double )
 -- > 1.118033988749895
-std :: forall s n. (SingI s, Floating n) => Tensor s n -> n
+std :: forall s n. (HasShape s, Floating n) => Tensor s n -> n
 std = sqrt . var
+
diff --git a/src/Data/Tensor/Tensor.hs b/src/Data/Tensor/Tensor.hs
--- a/src/Data/Tensor/Tensor.hs
+++ b/src/Data/Tensor/Tensor.hs
@@ -1,17 +1,16 @@
 {-# OPTIONS_GHC -fno-warn-incomplete-uni-patterns #-}
+{-# LANGUAGE BangPatterns         #-}
+{-# LANGUAGE ConstraintKinds      #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 module Data.Tensor.Tensor where
 
-import           Data.List                    (intercalate)
+import           Data.List        (intercalate)
 import           Data.Proxy
-import           Data.Singletons
-import qualified Data.Singletons.Prelude      as N
-import qualified Data.Singletons.Prelude.List as N
-import           Data.Tensor.Index
 import           Data.Tensor.Type
-import qualified Data.Vector                  as V
-import           GHC.Exts                     (IsList (..))
+import           Data.Type.Bool   hiding (If)
+import qualified Data.Vector      as V
+import           GHC.Exts         (IsList (..))
 import           GHC.TypeLits
 
 -----------------------
@@ -37,23 +36,26 @@
 --
 -- > SimpleTensor 2 3 Int == Matrix 3 3 Int == Tensor '[3,3] Int
 -- > SimpleTensor r 0 Int == Scalar Int
-type SimpleTensor (r :: Nat) (dim :: Nat) n = N.If ((N.==) dim 0) (Scalar n) (Tensor (N.Replicate r dim) n)
-
-instance (SingI s, Eq n) => Eq (Tensor s n) where
-  f == g = all (\i -> f ! i == g ! i ) ([minBound..maxBound] :: [TensorIndex s])
+type SimpleTensor (r :: Nat) (dim :: Nat) n = Tensor (Replicate r dim) n
 
-instance SingI s => Functor (Tensor s) where
-  fmap f (Tensor t) = Tensor (\s i -> f (t s i))
+instance Functor (Tensor s) where
+  fmap f t = Tensor $ \s i -> f (getValue t s i)
 
-instance SingI s => Applicative (Tensor s) where
+instance Applicative (Tensor s) where
   pure n = Tensor $ \_ _ -> n
-  Tensor f <*> Tensor t = Tensor $ \s i -> f s i (t s i)
+  f <*> t = Tensor $ \s i -> getValue f s i (getValue t s i)
 
-instance SingI s => Foldable (Tensor s) where
-  foldMap f t = foldMap (f.(t !)) ([minBound..maxBound] :: [TensorIndex s])
+instance (HasShape s, Eq n) => Eq (Tensor s n) where
+  f == t = and $ (==) <$> f <*> t
 
-instance (SingI s, Show n) => Show (Tensor s n) where
-  show (Tensor f) = let s = natsVal (Proxy :: Proxy s) in go 0 [] s (f s)
+instance HasShape s => Foldable (Tensor s) where
+  foldr f b t =
+    let s = shape t
+        r = toSize (Proxy :: Proxy s)
+    in foldr (f . gx t s) b ([0..r-1] :: [Int])
+
+instance (HasShape s, Show n) => Show (Tensor s n) where
+  show (Tensor f) = let s = unShape (toShape :: SShape s) in go 0 [] s (f s)
     where
       {-# INLINE go #-}
       go :: Int -> [Int] -> [Int] -> (Index -> n) -> String
@@ -70,7 +72,7 @@
 -----------------------
 -- Tensor as Num
 -----------------------
-instance (SingI s, Num n) => Num (Tensor s n) where
+instance (HasShape s, Num n) => Num (Tensor s n) where
   (+) = zipWithTensor (+)
   (*) = zipWithTensor (*)
   abs = fmap abs
@@ -78,16 +80,16 @@
   negate = fmap negate
   fromInteger = pure . fromInteger
 
-instance (SingI s, Fractional n) => Fractional (Tensor s n) where
+instance (HasShape s, Fractional n) => Fractional (Tensor s n) where
   fromRational = pure . fromRational
   (/) = zipWithTensor (/)
 
-instance (SingI s, Floating n) => Floating (Tensor s n) where
+instance (HasShape s, Floating n) => Floating (Tensor s n) where
   pi      = pure pi
   exp     = fmap exp
   log     = fmap log
   sqrt    = fmap sqrt
-  logBase = error "undefined"
+  logBase a b = logBase <$> a <*> b
   sin     = fmap sin
   cos     = fmap cos
   tan     = fmap tan
@@ -103,67 +105,79 @@
 
 
 {-# INLINE generateTensor #-}
-generateTensor :: SingI s => (Index -> n) -> Proxy s -> Tensor s n
-generateTensor fn p =
-  let s  = natsVal p
-      ps = product s
-  in if ps == 0 then pure (fn [0]) else Tensor $ const fn
+generateTensor :: forall s n. HasShape s => (Index -> n) -> Tensor s n
+generateTensor fn = case toSize (Proxy :: Proxy s) of
+  0 -> pure (fn [])
+  _ -> Tensor (const fn)
 
 {-# INLINE transformTensor #-}
 transformTensor
-  :: forall s s' n. SingI s
-  => (([Int], [Int]) -> [Int] -> [Int])
+  :: forall s s' n. HasShape s
+  => (Shape -> (Shape, Index) -> Index)
   -> Tensor s  n
   -> Tensor s' n
-transformTensor go (Tensor f) = let s = natsVal (Proxy :: Proxy s) in Tensor $ \s' i' -> f s (go (i',s') s)
+transformTensor go (Tensor fo) =
+  let s = unShape (toShape :: SShape s)
+      {-# INLINE g #-}
+      g = curry $ fo s . go s
+  in Tensor g
 
 -- | Clone tensor to a new `V.Vector` based tensor
-clone :: SingI s => Tensor s n -> Tensor s n
+clone :: HasShape s => Tensor s n -> Tensor s n
 clone t =
   let s = shape t
-      v = V.generate (product s) (\i -> t ! toEnum i)
+      v = V.generate (product s) (gx t s)
   in Tensor $ \_ i -> v V.! tiTovi s i
 
 {-# INLINE zipWithTensor #-}
-zipWithTensor :: SingI s => (n -> n -> n) -> Tensor s n -> Tensor s n -> Tensor s n
-zipWithTensor f t1 t2 = generateTensor (\i -> f (t1 ! TensorIndex i) (t2 ! TensorIndex i)) Proxy
+zipWithTensor :: HasShape s => (n -> n -> n) -> Tensor s n -> Tensor s n -> Tensor s n
+zipWithTensor f t1 t2 =
+  let s1 = shape t1
+      s2 = shape t2
+  in generateTensor (\i -> f (getValue t1 s1 i) (getValue t2 s2 i))
 
-instance SingI s => IsList (Tensor s n) where
+instance HasShape s => IsList (Tensor s n) where
   type Item (Tensor s n) = n
   fromList v =
-    let s = natsVal (Proxy :: Proxy s)
+    let s = unShape (toShape :: SShape s)
         l = product s
     in if l /= length v
       then error "length not match"
       else let vv = V.fromList v in Tensor $ \s' i -> vv V.! tiTovi s' i
-  toList  t = let n = rank t - 1 in fmap (\i -> t ! toEnum i) [0..n]
+  toList  t =
+    let n = rank t - 1
+        s = unShape (toShape :: SShape s)
+    in fmap (gx t s) [0..n]
 
 -----------------------
 -- Tensor Shape
 -----------------------
 -- | Shape of Tensor, is a list of integers, uniquely determine the shape of tensor.
-shape :: forall s n. SingI s => Tensor s n -> [Int]
-shape _ = natsVal (Proxy :: Proxy s)
+shape :: forall s n. HasShape s => Tensor s n -> [Int]
+shape _ = unShape (toShape :: SShape s)
 
 -- | Rank of Tensor
-rank :: SingI s => Tensor s n -> Int
-rank = length . shape
+rank :: forall s n. HasShape s => Tensor s n -> Int
+rank _ = toRank (Proxy :: Proxy s)
 
 -----------------------
 -- Tensor Operation
 -----------------------
 -- | Get value from tensor by index
-(!) :: SingI s => Tensor s n -> TensorIndex s -> n
+(!) :: HasShape s => Tensor s n -> TensorIndex s -> n
 (!) t (TensorIndex i) = getValue t (shape t) i
 
+gx :: HasShape s => Tensor s n -> Shape -> Int -> n
+gx (Tensor t) s i = t s (viToti s i)
+
 -- | Reshape a tensor to another tensor, with total dimensions are equal.
-reshape :: (N.Product s ~ N.Product s', SingI s) => Tensor s n -> Tensor s' n
+reshape :: (TensorSize s ~ TensorSize s', HasShape s) => Tensor s n -> Tensor s' n
 reshape = transformTensor go
   where
     {-# INLINE go #-}
-    go (i',s') s = viToti s $ tiTovi s' i'
+    go s (s',i') = viToti s $ tiTovi s' i'
 
-type Transpose (a :: [Nat]) = N.Reverse a
+type Transpose (a :: [Nat]) = Reverse a '[]
 
 -- | <https://en.wikipedia.org/wiki/Transpose Transpose> tensor completely
 --
@@ -176,14 +190,13 @@
 -- > [[1,4,7],
 -- > [2,5,8],
 -- > [3,6,9]]
-transpose :: SingI a => Tensor a n -> Tensor (Transpose a) n
+transpose :: HasShape a => Tensor a n -> Tensor (Transpose a) n
 transpose  = transformTensor go
   where
     {-# INLINE go #-}
-    go (i',_) _ = reverse i'
+    go _ (_, i') = reverse i'
 
-type CheckSwapaxes i j s = N.And '[ (N.>=) i 0, (N.<) i j, (N.<) j (N.Length s)]
-type Swapaxes i j s = N.Concat '[N.Take i s, '[(N.!!) s j], N.Tail (N.Drop i (N.Take j s)) , '[(N.!!) s i], N.Tail (N.Drop j s)]
+type Swapaxes i j s = Take i s ++ (Dimension s j : (Drop i (Take j s))) ++ (Dimension s j : (Tail (Drop j s)))
 
 -- | Swapaxes any rank
 --
@@ -211,24 +224,23 @@
 --
 -- > transpose == swapaxes i0 i1
 swapaxes
-  :: (Swapaxes i j s ~ s'
-    , CheckSwapaxes i j s ~ 'True
-    , SingI s
+  :: (CheckIndices i j s
+    , HasShape s
     , KnownNat i
     , KnownNat j)
   => Proxy i
   -> Proxy j
   -> Tensor s n
-  -> Tensor s' n
+  -> Tensor (Swapaxes i j s) n
 swapaxes px pj =
   let i = toNat px
       j = toNat pj
-      go (s,_) _ = take i s ++ [s !! j] ++ tail (drop i (take j s)) ++ [s!!i] ++ tail (drop j s)
+      go _ (_,s) = take i s ++ [s !! j] ++ tail (drop i (take j s)) ++ [s!!i] ++ tail (drop j s)
   in transformTensor go
 
 -- | Unit tensor of shape s, if all the indices are equal then return 1, otherwise return 0.
-identity :: forall s n . (SingI s, Num n) => Tensor s n
-identity = generateTensor go Proxy
+identity :: forall s n . (HasShape s, Num n) => Tensor s n
+identity = generateTensor go
   where
     go []  = 0
     go [_] = 1
@@ -237,17 +249,19 @@
       | otherwise = go (b:cs)
 
 dyad'
-  :: ( r ~ (N.++) s t
-     , SingI s
-     , SingI t
-     , SingI r)
+  :: ( r ~ (s ++ t)
+     , HasShape s
+     , HasShape t
+     , HasShape r)
   => (n -> m -> o)
   -> Tensor s n
   -> Tensor t m
   -> Tensor r o
 dyad' f t1 t2 =
   let l = rank t1
-  in generateTensor (\i -> let (ti1,ti2) = splitAt l i in f (t1 ! TensorIndex ti1) (t2 ! TensorIndex ti2)) Proxy
+      s1 = shape t1
+      s2 = shape t2
+  in generateTensor (\i -> let (ti1,ti2) = splitAt l i in f (getValue t1 s1 ti1) (getValue t2 s2 ti2))
 
 -- | <https://en.wikipedia.org/wiki/Dyadics Dyadic Tensor>
 --
@@ -267,17 +281,17 @@
 -- > [[4,8],
 -- > [12,16]]]]
 dyad
-  :: ( r ~ (N.++) s t
-     , SingI s
-     , SingI t
-     , SingI r
+  :: ( r ~ (s ++ t)
+     , HasShape s
+     , HasShape t
+     , HasShape r
      , Num n
      , Eq n)
   => Tensor s n -> Tensor t n -> Tensor r n
 dyad = dyad' mult
 
 
-type DotTensor s1 s2 = (N.++) (N.Init s1) (N.Tail s2)
+type DotTensor s1 s2 = Init s1 ++ Init s2
 
 -- | Tensor Product
 --
@@ -293,28 +307,28 @@
 --
 -- For rank 2 tensor, it is just matrix product.
 dot
-  :: ( N.Last s ~ N.Head s'
-     , SingI (DotTensor s s')
-     , SingI s
-     , SingI s'
+  :: ( Last s ~ Head s'
+     , r ~ DotTensor s s'
+     , HasShape s
+     , HasShape s'
+     , HasShape r
      , Num n
      , Eq n)
   => Tensor s n
   -> Tensor s' n
-  -> Tensor (DotTensor s s') n
+  -> Tensor r n
 dot t1 t2 =
   let s1 = shape t1
+      s2 = shape t2
       n  = last s1
       b  = length s1 - 1
+      f (!x,!y) = (getValue t1 s1 x) `mult` (getValue t2 s2 y)
   in generateTensor (\i ->
         let (ti1,ti2) = splitAt b i
-        in sum $ fmap (\(x,y) -> (t1 ! TensorIndex x) `mult` (t2 ! TensorIndex y)) [(ti1++[x],x:ti2)| x <- [0..n-1]]) Proxy
-
+        in sum $ f <$> [(ti1++[x],x:ti2)| x <- [0..n-1]])
 
-type CheckContraction s x y = N.And '[(N.<) x y, (N.>=) x 0, (N.<) y (TensorRank s)]
 type Contraction s x y = DropIndex (DropIndex s y) x
-type TensorDim s i = (N.!!) s i
-type DropIndex (s :: [Nat]) (i :: Nat) = (N.++) (N.Fst (N.SplitAt i s)) (N.Tail (N.Snd (N.SplitAt i s)))
+type DropIndex s i = Take i s ++ Drop (i+1) s
 
 -- | Contraction Tensor
 --
@@ -330,14 +344,14 @@
 -- In rank 2 tensor, contraction of tensor is just the <https://en.wikipedia.org/wiki/Trace_(linear_algebra) trace>.
 contraction
   :: forall x y s s' n.
-     ( CheckContraction s x y ~ 'True
+     ( CheckIndices x y s
      , s' ~ Contraction s x y
-     , TensorDim s x ~ TensorDim s y
+     , Dimension s x ~ Dimension s y
      , KnownNat x
      , KnownNat y
-     , SingI s
-     , SingI s'
-     , KnownNat  (TensorDim s x)
+     , HasShape s
+     , HasShape s'
+     , KnownNat (Dimension s x)
      , Num n)
   => (Proxy x, Proxy y)
   -> Tensor s  n
@@ -345,9 +359,9 @@
 contraction (px, py) t@(Tensor f) =
   let x  = toNat px
       y  = toNat py
-      n  = toNat (Proxy :: Proxy (TensorDim s x))
+      n  = toNat (Proxy :: Proxy (Dimension s x))
       s  = shape t
-  in generateTensor (go x (y-x-1) n (f s) ) Proxy
+  in generateTensor (go x (y-x-1) n (f s) )
   where
     {-# INLINE go #-}
     go a b n fs i =
@@ -355,9 +369,7 @@
           (r3,r4) = splitAt b rt
       in sum $ fmap fs [r1 ++ (j:r3) ++ (j:r4) | j <- [0..n-1]]
 
-type CheckDim dim s = N.And '[(N.>=) dim 0, (N.<) dim (N.Length s)]
-type CheckSelect dim i s = N.And '[ CheckDim dim s , (N.>=) i 0, (N.<) i ((N.!!) s dim) ]
-type Select i s = (N.++) (N.Take i s) (N.Tail (N.Drop i s))
+type CheckSelect dim i s = (CheckDimension dim s && IsIndex i (Dimension s dim)) ~ 'True
 
 -- | Select `i` indexing of tensor
 --
@@ -367,24 +379,23 @@
 -- > λ> select (i0,i1) a
 -- > [0,1,0,0]
 select
-  :: ( CheckSelect dim i s ~ 'True
-     , s' ~ Select dim s
-     , SingI s
+  :: ( CheckSelect dim i s
+     , HasShape s
      , KnownNat dim
      , KnownNat i)
   => (Proxy dim, Proxy i)
   -> Tensor s n
-  -> Tensor s' n
+  -> Tensor (DropIndex s dim) n
 select (pd, pid) t=
   let dim = toNat pd
       ind = toNat pid
   in transformTensor (go dim ind) t
   where
     {-# INLINE go #-}
-    go d i (i',_) _ = let (a,b) = splitAt d i' in a ++ (i:b)
+    go d i _ (_,i') = let (a,b) = splitAt d i' in a ++ (i:b)
 
-type CheckSlice dim from to s = N.And '[ CheckDim dim s, CheckSelect dim from s, (N.<) from to , (N.<=) to ((N.!!) s dim)]
-type Slice dim from to s = N.Concat '[N.Take dim s, '[to - from] , N.Tail (N.Drop dim s)]
+type CheckSlice dim from to s = (CheckDimension dim s && IsIndices from to (Dimension s dim)) ~ 'True
+type Slice dim from to s = Take dim s ++ ( to - from : Tail (Drop dim s))
 
 -- | Slice tensor
 --
@@ -403,19 +414,19 @@
 -- > [0,1],
 -- > [0,0]]
 slice
-  :: ( CheckSlice dim from to s ~ 'True
+  :: ( CheckSlice dim from to s
      , s' ~ Slice dim from to s
      , KnownNat dim
      , KnownNat from
      , KnownNat (to - from)
-     , SingI s)
+     , HasShape s)
   => (Proxy dim, (Proxy from, Proxy to))
   -> Tensor s n
   -> Tensor s' n
 slice (pd, (pa,_)) t =
   let d = toNat pd
       a = toNat pa
-  in transformTensor (\(i',_) _ -> let (x,y:ys) = splitAt d i' in x ++ (y+a:ys)) t
+  in transformTensor (\_ (_,i') -> let (x,y:ys) = splitAt d i' in x ++ (y+a:ys)) t
 
 -- | Expand tensor
 --
@@ -430,16 +441,16 @@
 -- > [0,1,0,1]]
 expand
   :: (TensorRank s ~ TensorRank s'
-     , SingI s)
+     , HasShape s)
   => Tensor s n
   -> Tensor s' n
 expand = transformTensor go
   where
     {-# INLINE go #-}
-    go (i',_) = zipWith mod i'
+    go s (_, i') = zipWith mod i' s
 
-type CheckConcatenate i a b = N.And '[ (N.==) (N.Length a) (N.Length b), (N.>=) i 0, (N.<) i (N.Length a), (N.==) (Select i a) (Select i b) ]
-type Concatenate i a b = N.Concat '[N.Take i a, '[(N.+) (TensorDim a i) (TensorDim b i)], N.Tail (N.Drop i a)]
+type CheckConcatenate i a b = (IsIndex i (TensorRank a)) ~ 'True
+type Concatenate i a b = Take i a ++ (Dimension a i + Dimension b i : Drop (i+1) a)
 
 -- | Join a sequence of arrays along an existing axis.
 --
@@ -460,10 +471,12 @@
 -- > [[1,2,1,1],
 -- > [3,4,1,1]]
 concatenate
-  :: (CheckConcatenate i a b ~ 'True
+  :: ( TensorRank a ~ TensorRank b
+    , DropIndex a i ~ DropIndex b i
+    , CheckConcatenate i a b
     , Concatenate i a b ~ c
-    , SingI a
-    , SingI b
+    , HasShape a
+    , HasShape b
     , KnownNat i)
   => Proxy i
   -> Tensor a n
@@ -476,8 +489,8 @@
       n  = sa !! i
   in Tensor $ \_ ind -> let (ai,x:bi) = splitAt i ind in if x >= n then b sb (ai ++ (x-n):bi) else a sa ind
 
-type CheckInsert dim i a b = N.And '[ CheckDim dim b, (N.==) a (Select dim b), (N.>=) i 0, (N.<=) i (TensorDim b dim)]
-type Insert dim a b = N.Concat '[N.Take dim b, '[ TensorDim b dim + 1 ], N.Tail (N.Drop dim b)]
+type CheckInsert dim i b = (CheckDimension dim b && IsIndex i (Dimension b dim))  ~ 'True
+type Insert dim b = Take dim b ++ (Dimension b dim + 1 : Drop (dim + 1) b)
 
 -- | Insert tensor to higher level tensor
 --
@@ -506,16 +519,17 @@
 -- > [[1.0,2.0],
 -- > [2.0,4.0]]]
 insert
-  :: (CheckInsert dim i a b ~ 'True
+  :: ( DropIndex b dim ~ a
+    , CheckInsert dim i b
     , KnownNat i
     , KnownNat dim
-    , SingI a
-    , SingI b)
+    , HasShape a
+    , HasShape b)
   => Proxy dim
   -> Proxy i
   -> Tensor a n
   -> Tensor b n
-  -> Tensor (Insert dim a b) n
+  -> Tensor (Insert dim b) n
 insert pd px a@(Tensor ta) b@(Tensor tb) =
   let d = toNat pd
       i = toNat px
@@ -535,17 +549,18 @@
 -- > [1.0,2.0,3.0]
 append
   :: forall dim a b n.
-    (CheckInsert dim (TensorDim b dim) a b ~ 'True
-    , KnownNat (TensorDim b dim)
+    ( DropIndex b dim ~ a
+    , CheckInsert dim (Dimension b dim) b
+    , KnownNat (Dimension b dim)
     , KnownNat dim
-    , SingI a
-    , SingI b)
+    , HasShape a
+    , HasShape b)
   => Proxy dim
   -> Tensor a n
   -> Tensor b n
-  -> Tensor (Insert dim a b) n
-append pd = insert pd (Proxy :: Proxy (TensorDim b dim))
+  -> Tensor (Insert dim b) n
+append pd = insert pd (Proxy :: Proxy (Dimension b dim))
 
 -- | Convert tensor to untyped function, for internal usage.
-runTensor :: SingI s => Tensor s n -> Index -> n
+runTensor :: HasShape s => Tensor s n -> Index -> n
 runTensor t@(Tensor f) = f (shape t)
diff --git a/src/Data/Tensor/Type.hs b/src/Data/Tensor/Type.hs
--- a/src/Data/Tensor/Type.hs
+++ b/src/Data/Tensor/Type.hs
@@ -1,41 +1,122 @@
+{-# LANGUAGE ConstraintKinds      #-}
+{-# LANGUAGE UndecidableInstances #-}
 module Data.Tensor.Type where
 
-import           Data.List                    (foldl')
+import           Data.List      (foldl')
 import           Data.Proxy
-import           Data.Singletons
-import           Data.Singletons.Prelude.List
+import           Data.Type.Bool hiding (If)
+import           GHC.Exts
 import           GHC.TypeLits
+import qualified GHC.TypeLits   as L
 import           Unsafe.Coerce
 
 type Shape = [Int]
 type Index = [Int]
 
-toNat :: KnownNat s => Proxy s -> Int
+newtype SShape (shape :: [Nat]) = SShape { unShape :: Shape } deriving Show
+
+class HasShape s where
+  toShape :: SShape s
+  toRank  :: Proxy s -> Int
+  toRank _ = length $ unShape (toShape :: SShape s)
+  toSize  :: Proxy s -> Int
+  toSize _ = product $ unShape (toShape :: SShape s)
+
+instance HasShape '[] where
+  toShape = SShape []
+
+instance (KnownNat n, HasShape s) => HasShape (n:s) where
+  toShape = SShape $ fromInteger (natVal (Proxy :: Proxy n)) : unShape (toShape :: SShape s)
+
+toNat :: KnownNat n => Proxy n -> Int
 toNat = unsafeCoerce . natVal
 
-natsVal :: forall proxy (s::[Nat]). SingI s => proxy s -> Index
-natsVal _ = case (sing :: Sing s) of
-  SNil         -> []
-  (SCons x xs) -> unsafeCoerce <$> (fromSing x: fromSing xs)
+viToti :: Shape -> Int -> Index
+viToti s i = snd $ foldl' (\(r,xs) si -> let (r',x) = divMod r si in (r', x:xs)) (i,[]) (reverse s)
 
-viToti :: Index -> Int -> Index
-viToti s i = snd $ foldl' go (i,[]) (reverse s)
-  where
-    {-# INLINE go #-}
-    go (i',x) n = let (d,r) = divMod i' n in (d,r:x)
+tiTovi :: Shape -> Index -> Int
+tiTovi s i = foldl' (\b (n,ind) -> b * n + ind) 0 $ zipWith (,) s i
 
-tiTovi :: Index -> Index -> Int
-tiTovi = go 0
-  where
-    {-# INLINE go #-}
-    go i (n:ns) (ind:inds) = go (i * n + ind) ns inds
-    go i _ _               = i
+-- | Tensor Index, used to locate each point of tensor
+newtype TensorIndex (shape :: [Nat]) = TensorIndex Index deriving (Eq,Show,Ord)
 
-mult :: (Eq a, Num a) => a -> a -> a
-mult a b = case a of
-  0 -> 0
-  c -> c * b
+instance HasShape s => IsList (TensorIndex s) where
+  type Item (TensorIndex s) = Int
+  fromList v =
+    let s = unShape (toShape :: SShape s)
+    in if length v /= length s then error "length not match"
+        else if or (zipWith (\i n-> i <0 || i >= n) v s) then error "index overflow"
+          else TensorIndex v
+  toList (TensorIndex v) = v
 
+-- | Tensor rank.
+type family TensorRank (s :: [Nat]) :: Nat where
+  TensorRank '[] = 0
+  TensorRank (_:s) = TensorRank s + 1
+
+-- | Tensor size.
+type family TensorSize (s :: [Nat]) :: Nat where
+  TensorSize '[] = 1
+  TensorSize (n:s) = n L.* (TensorRank s)
+
+type family Reverse (a :: [k]) (b :: [k]) :: [k] where
+  Reverse '[]    b = b
+  Reverse (a:as) b = Reverse as (a:b)
+
+type family If (b :: Bool) c d where
+  If 'True  c d = c
+  If 'False c d = d
+
+type family Replicate (a :: k) (dim :: Nat) :: [k] where
+  Replicate a 0 = '[]
+  Replicate a n = a : Replicate a n
+
+type family Dimension (s :: [Nat]) (i :: Nat) :: Nat where
+  Dimension (s:_) 0 = s
+  Dimension (_:s) n = Dimension s (n-1)
+  Dimension _ _     = TypeError ('Text "Index overflow")
+
+type CheckDimension dim s = IsIndex dim (TensorRank s)
+type CheckIndices i j s = IsIndices i j (TensorRank s) ~ 'True
+
+type IsIndex i n = (0 <=? i) && (i + 1 <=? n)
+type IsIndices i j n = (0 <=? i) && (i + 1 <=? j) && (j + 1 <=? n)
+
+type family Take (n :: Nat) (a :: [k]) :: [k] where
+  Take 0 _ = '[]
+  Take n (x:xs) = x : Take (n-1) xs
+
+type family Drop (n :: Nat) (a :: [k]) :: [k] where
+  Drop 0 xs = xs
+  Drop n (_:xs) = Take (n-1) xs
+
+type family Tail (a :: [k]) :: [k] where
+  Tail '[] = TypeError ('Text "No tail")
+  Tail (_:xs) = xs
+
+type family Init (a :: [k]) :: [k] where
+  Init '[] = TypeError ('Text "No init")
+  Init '[_] = '[]
+  Init (x:xs) = x : Init xs
+
+type family Head (a :: [k]) :: k where
+  Head '[] = TypeError ('Text "No head")
+  Head (x:_) = x
+
+type family Last (a :: [k]) :: k where
+  Last '[] = TypeError ('Text "No last")
+  Last '[x] = x
+  Last (_:xs) = Last xs
+
+type family (a :: [k]) ++ (b :: [k]) :: [k] where
+  '[] ++ b = b
+  (a:as) ++ b = a : (as ++ b)
+
+mult :: (Eq a, Num a) => a -> a -> a
+mult a b
+  | a == 0 = 0
+  | b == 0 = 0
+  | otherwise = a * b
 -----------------------
 -- Tensor Type Index
 -----------------------
diff --git a/tensors.cabal b/tensors.cabal
--- a/tensors.cabal
+++ b/tensors.cabal
@@ -1,6 +1,6 @@
 cabal-version: 1.12
 name: tensors
-version: 0.1.2
+version: 0.1.3
 license: BSD3
 license-file: LICENSE
 copyright: (c) 2018 Daniel YU
@@ -21,7 +21,6 @@
     hs-source-dirs: src
     other-modules:
         Data.Tensor.Type
-        Data.Tensor.Index
         Data.Tensor.Tensor
         Data.Tensor.Matrix
         Data.Tensor.Space
@@ -36,9 +35,7 @@
                  -Wincomplete-uni-patterns -fno-warn-orphans
                  -fno-warn-missing-signatures
     build-depends:
-        base >=4.7 && <5,
-        reflection >=2.1.4 && <2.2,
-        singletons >=2.5.1 && <2.6,
+        base >=4.9 && <5,
         vector >=0.12.0.2 && <0.13
 
 test-suite spec
@@ -47,7 +44,6 @@
     hs-source-dirs: test src
     other-modules:
         Data.Tensor
-        Data.Tensor.Index
         Data.Tensor.Matrix
         Data.Tensor.Space
         Data.Tensor.Statistics
@@ -64,9 +60,34 @@
                  -Wincomplete-uni-patterns -fno-warn-orphans
                  -fno-warn-missing-signatures
     build-depends:
-        QuickCheck >=2.12.6.1 && <2.13,
-        base >=4.7 && <5,
+        QuickCheck >=2.11.1 && <2.14,
+        base >=4.9 && <5,
         hspec ==2.*,
         reflection >=2.1.4 && <2.2,
-        singletons >=2.5.1 && <2.6,
+        vector >=0.12.0.2 && <0.13
+
+benchmark bm
+    type: exitcode-stdio-1.0
+    main-is: Bench.hs
+    hs-source-dirs: bench src
+    other-modules:
+        Data.Tensor
+        Data.Tensor.Matrix
+        Data.Tensor.Space
+        Data.Tensor.Statistics
+        Data.Tensor.Tensor
+        Data.Tensor.Type
+        Paths_tensors
+    default-language: Haskell2010
+    default-extensions: AllowAmbiguousTypes DataKinds
+                        ExistentialQuantification FlexibleContexts FlexibleInstances
+                        FunctionalDependencies KindSignatures MultiParamTypeClasses
+                        PolyKinds RankNTypes ScopedTypeVariables TypeFamilies TypeOperators
+                        TypeSynonymInstances
+    ghc-options: -Wall -Wcompat -Wincomplete-record-updates
+                 -Wincomplete-uni-patterns -fno-warn-orphans
+                 -fno-warn-missing-signatures
+    build-depends:
+        base >=4.9 && <5,
+        criterion >=1.5.4.0 && <1.6,
         vector >=0.12.0.2 && <0.13
diff --git a/test/Spec.hs b/test/Spec.hs
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -10,7 +10,6 @@
 
 import           Data.Proxy
 import           Data.Reflection
-import           Data.Singletons
 import           Data.Tensor
 import           Data.Tensor.Type
 import           GHC.Exts         (fromList)
@@ -25,12 +24,12 @@
 spec = do
   describe "Data.Tensor" specTensor
 
-newtype MagicNats r = MagicNats (forall (n :: [Nat]). SingI n => Proxy n -> r)
-reifyNats :: forall r. [Int] -> (forall (n :: [Nat]). SingI n => Proxy n -> r) -> r
+newtype MagicNats r = MagicNats (forall (n :: [Nat]). HasShape n => Proxy n -> r)
+reifyNats :: forall r. [Int] -> (forall (n :: [Nat]). HasShape n => Proxy n -> r) -> r
 reifyNats n k = unsafeCoerce (MagicNats k :: MagicNats r) n Proxy
 
-instance SingI a => Reifies (a::[Nat]) [Int] where
-  reflect = natsVal
+instance HasShape a => Reifies (a::[Nat]) [Int] where
+  reflect _ = unShape (toShape :: SShape a)
 
 normalize :: [Int] -> [Int]
 normalize = take 5 . fmap (`mod` 10)
@@ -46,8 +45,6 @@
                 go :: forall (s :: Nat). KnownNat s => Int -> Proxy s -> Bool
                 go x _ = trace (identity :: Tensor '[s,s] Int) == x
             in reifyNat (toInteger i') (go i')
-    it "index range" $ do
-      fmap fromEnum ([minBound..maxBound] :: [TensorIndex '[2,2,2,2,2]]) `shouldBe` [0..31]
     it "det" $ property $
       \s0 -> let s = (if null s0 then [1..16] else take 16 $ cycle s0) :: [Int]
                  a = fromList s :: Tensor '[4,4] Int