diff --git a/ranged-list.cabal b/ranged-list.cabal
--- a/ranged-list.cabal
+++ b/ranged-list.cabal
@@ -1,13 +1,13 @@
 cabal-version: 1.12
 
--- This file has been generated from package.yaml by hpack version 0.33.0.
+-- This file has been generated from package.yaml by hpack version 0.34.4.
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 42c7def6fb4ed75b8b978a1de4cdf116653323fb1cee0e251bceaa00ef7be780
+-- hash: 349e85c819f827a30071512b7dc4e2e3b2add699054a5d970f833e60ce71577d
 
 name:           ranged-list
-version:        0.1.0.0
+version:        0.1.0.1
 synopsis:       The list like structure whose length or range of length can be specified
 description:    Please see the README on GitHub at <https://github.com/YoshikuniJujo/ranged-list#readme>
 category:       List
diff --git a/src/Data/List/Length.hs b/src/Data/List/Length.hs
--- a/src/Data/List/Length.hs
+++ b/src/Data/List/Length.hs
@@ -57,6 +57,8 @@
 	LengthR, unfoldl, unfoldlWithBase, unfoldlM, unfoldlMWithBase,
 	ListToLengthR, listToLengthR )
 
+import GHC.TypeNats
+
 ---------------------------------------------------------------------------
 
 -- LENGTH LEFT
@@ -66,7 +68,7 @@
 -- LENGTH LEFT
 ---------------------------------------------------------------------------
 
-repeatL :: Unfoldr 0 n n => a -> LengthL n a
+repeatL :: (0 <= n, Unfoldr 0 n n) => a -> LengthL n a
 repeatL = fillL NilL
 
 {-^
@@ -128,7 +130,7 @@
 -- LENGTH RIGHT
 ---------------------------------------------------------------------------
 
-repeatR :: Unfoldl 0 n n => a -> LengthR n a
+repeatR :: (0 <= n, Unfoldl 0 n n) => a -> LengthR n a
 repeatR = (`fillR` NilR)
 
 {-^
diff --git a/src/Data/List/Length/LengthL.hs b/src/Data/List/Length/LengthL.hs
--- a/src/Data/List/Length/LengthL.hs
+++ b/src/Data/List/Length/LengthL.hs
@@ -27,7 +27,7 @@
 -- UNFOLDR
 ---------------------------------------------------------------------------
 
-unfoldr :: Unfoldr 0 n n => (s -> (a, s)) -> s -> LengthL n a
+unfoldr :: (0 <= n, Unfoldr 0 n n) => (s -> (a, s)) -> s -> LengthL n a
 unfoldr = unfoldrWithBase NilL
 
 {-^
@@ -56,7 +56,7 @@
 
 -}
 
-unfoldrM :: (Monad m, Unfoldr 0 n n) => m a -> m (LengthL n a)
+unfoldrM :: (Monad m, 0 <= n, Unfoldr 0 n n) => m a -> m (LengthL n a)
 unfoldrM = unfoldrMWithBase NilL
 
 {-^
@@ -114,7 +114,7 @@
 	splitL = \case [] -> Left NilL; x : xs -> Right (x :. NilL, xs)
 
 instance {-# OVERLAPPABLE #-}
-	(1 <= n, 1 <= (n - 1), ListToLengthL (n - 1)) => ListToLengthL n where
+	(1 <= n, 1 <= (n - 1), 0 <= (n - 1), ListToLengthL (n - 1)) => ListToLengthL n where
 	splitL = \case
 		[] -> Left NilL
 		x : xs -> (x :..) +++ ((x :.) `first`) $ splitL xs
diff --git a/src/Data/List/Length/LengthR.hs b/src/Data/List/Length/LengthR.hs
--- a/src/Data/List/Length/LengthR.hs
+++ b/src/Data/List/Length/LengthR.hs
@@ -39,7 +39,7 @@
 -- UNFOLDL
 ---------------------------------------------------------------------------
 
-unfoldl :: Unfoldl 0 n n => (s -> (s, a)) -> s -> LengthR n a
+unfoldl :: (0 <= n, Unfoldl 0 n n) => (s -> (s, a)) -> s -> LengthR n a
 unfoldl f s = unfoldlWithBase f s NilR
 
 {-^
@@ -68,7 +68,7 @@
 
 -}
 
-unfoldlM :: (Monad m, Unfoldl 0 n n) => m a -> m (LengthR n a)
+unfoldlM :: (Monad m, 0 <= n, Unfoldl 0 n n) => m a -> m (LengthR n a)
 unfoldlM = (`unfoldlMWithBase` NilR)
 
 {-^
@@ -125,7 +125,7 @@
 	listToLengthR = \case [] -> Left NilR; x : xs -> Right (NilR :+ x, xs)
 
 instance {-# OVERLAPPABLE #-}
-	(1 <= n, 1 <= (n - 1), ListToLengthR (n - 1)) => ListToLengthR n where
+	(1 <= n, 1 <= (n - 1), 0 <= (n - 1), ListToLengthR (n - 1)) => ListToLengthR n where
 	listToLengthR = \case
 		[] -> Left NilR
 		x : xs -> (:++ x) +++ ((:+ x) `first`) $ listToLengthR xs
diff --git a/src/Data/List/Range.hs b/src/Data/List/Range.hs
--- a/src/Data/List/Range.hs
+++ b/src/Data/List/Range.hs
@@ -279,7 +279,7 @@
 instance LeftToRight n m 0 0 where n ++.+ _ = n
 
 instance {-# OVERLAPPABLE #-} (
-	PushR (n - 1) (m - 1), LoosenRMax n m (m + w),
+	1 <= n, PushR (n - 1) (m - 1), LoosenRMax n m (m + w),
 	LeftToRight n (m + 1) 0 (w - 1) ) => LeftToRight n m 0 w where
 	(++.+) n = \case NilL -> loosenRMax n; x :.. v -> n .:++ x ++.+ v
 
@@ -339,7 +339,7 @@
 instance RightToLeft 0 0 v w where _ ++.. v = v
 
 instance {-# OVERLAPPABLE #-} (
-	PushL (v - 1) (w - 1), LoosenLMax v w (m + w),
+	1 <= v, PushL (v - 1) (w - 1), LoosenLMax v w (m + w),
 	RightToLeft 0 (m - 1) v (w + 1) ) => RightToLeft 0 m v w where
 	(++..) = \case NilR -> loosenLMax; n :++ x -> (n ++..) . (x .:..)
 
diff --git a/src/Data/List/Range/Nat.hs b/src/Data/List/Range/Nat.hs
--- a/src/Data/List/Range/Nat.hs
+++ b/src/Data/List/Range/Nat.hs
@@ -3,6 +3,8 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
 
+{-# LANGUAGE GADTs #-}
+
 module Data.List.Range.Nat (
 	-- * RangedNatL
 	RangedNatL, natL, toIntL, fromIntL, splitAtL,
@@ -16,6 +18,8 @@
 	RangeL, Unfoldr, unfoldrRangeMaybe, ZipL, zipWithL,
 	RangeR, Unfoldl, unfoldlRangeMaybe, ZipR, zipWithR )
 
+import GHC.TypeNats
+
 ---------------------------------------------------------------------------
 
 -- * RANGED NAT LEFT
@@ -27,7 +31,7 @@
 
 type RangedNatL n m = RangeL n m ()
 
-natL :: Unfoldr 0 n n => RangedNatL n n
+natL :: (0 <= n, Unfoldr 0 n n) => RangedNatL n n
 natL = repeatL ()
 
 {-^
@@ -92,7 +96,7 @@
 
 type RangedNatR n m = RangeR n m ()
 
-natR :: Unfoldl 0 n n => RangedNatR n n
+natR :: (0 <= n, Unfoldl 0 n n) => RangedNatR n n
 natR = repeatR ()
 
 {-^
diff --git a/src/Data/List/Range/RangeL.hs b/src/Data/List/Range/RangeL.hs
--- a/src/Data/List/Range/RangeL.hs
+++ b/src/Data/List/Range/RangeL.hs
@@ -276,7 +276,7 @@
 	loosenLMin (x :. xs) = x :.. loosenLMin xs
 	
 instance {-# OVERLAPPABLE #-}
-	(1 <= n, LoosenLMin (n - 1) (m - 1) (v - 1)) => LoosenLMin n m v where
+	(1 <= n, 1 <= v, LoosenLMin (n - 1) (m - 1) (v - 1)) => LoosenLMin n m v where
 	loosenLMin (x :. xs) = x :. loosenLMin xs
 
 -- LOOSEN LEFT MAX
@@ -302,11 +302,11 @@
 instance LoosenLMax 0 0 w where loosenLMax NilL = NilL
 
 instance {-# OVERLAPPABLE #-}
-	LoosenLMax 0 (m - 1) (w - 1) => LoosenLMax 0 m w where
+	(1 <= w, LoosenLMax 0 (m - 1) (w - 1)) => LoosenLMax 0 m w where
 	loosenLMax = \case NilL -> NilL; (x :.. xs) -> x :.. loosenLMax xs
 
 instance {-# OVERLAPPABLE #-}
-	(1 <= n, LoosenLMax (n - 1) (m - 1) (w - 1)) => LoosenLMax n m w where
+	(1 <= n, 1 <= w, LoosenLMax (n - 1) (m - 1) (w - 1)) => LoosenLMax n m w where
 	loosenLMax (x :. xs) = x :. loosenLMax xs
 
 ---------------------------------------------------------------------------
@@ -362,7 +362,7 @@
 	unfoldrMRangeWithBase NilL _ _ = pure NilL
 	unfoldrMRangeMaybeWithBase NilL p _ = bool (Just NilL) Nothing <$> p
 
-instance {-# OVERLAPPABLE #-} Unfoldr 0 0 (w - 1) => Unfoldr 0 0 w where
+instance {-# OVERLAPPABLE #-} (1 <= w, Unfoldr 0 0 (w - 1)) => Unfoldr 0 0 w where
 	unfoldrMRangeWithBase NilL p f =
 		(p >>=) . bool (pure NilL) $ f >>= \x ->
 			(x :..) <$> unfoldrMRangeWithBase NilL p f
@@ -376,7 +376,7 @@
 		((x :..) <$>) <$> unfoldrMRangeMaybeWithBase xs p f
 
 instance {-# OVERLAPPABLE #-}
-	Unfoldr 0 (v - 1) (w - 1) => Unfoldr 0 v w where
+	(1 <= v, 1 <= w, Unfoldr 0 (v - 1) (w - 1)) => Unfoldr 0 v w where
 	unfoldrMRangeWithBase NilL p f =
 		f >>= \x -> (x :.) <$> unfoldrMRangeWithBase NilL p f
 	unfoldrMRangeWithBase (x :.. xs) p f =
@@ -389,7 +389,7 @@
 		((x :.) <$>) <$> unfoldrMRangeMaybeWithBase xs p f
 
 instance {-# OVERLAPPABLE #-}
-	(1 <= n, Unfoldr (n - 1) (v - 1) (w - 1)) => Unfoldr n v w where
+	(1 <= n, 1 <= v, Unfoldr (n - 1) (v - 1) (w - 1)) => Unfoldr n v w where
 	unfoldrMRangeWithBase (x :. xs) p f =
 		(x :.) <$> unfoldrMRangeWithBase xs p f
 
@@ -588,7 +588,7 @@
 instance ZipL 0 0 v w where zipWithML _ NilL = pure . (NilL ,)
 
 instance {-# OVERLAPPABLE #-} (
-	1 <= v, LoosenLMin v w (v - m), LoosenLMax (v - m) (w - 1) w,
+	1 <= v, m <= v, LoosenLMin v w (v - m), LoosenLMax (v - m) (w - 1) w,
 	ZipL 0 (m - 1) (v - 1) (w - 1) ) => ZipL 0 m v w where
 	zipWithML _ NilL ys = pure (NilL, loosenLMin ys)
 	zipWithML (%) (x :.. xs) (y :. ys) =
diff --git a/src/Data/List/Range/RangeR.hs b/src/Data/List/Range/RangeR.hs
--- a/src/Data/List/Range/RangeR.hs
+++ b/src/Data/List/Range/RangeR.hs
@@ -267,7 +267,7 @@
 	loosenRMin (xs :+ x) = loosenRMin xs :++ x
 
 instance {-# OVERLAPPABLE #-}
-	(1 <= n, LoosenRMin (n - 1) (m - 1) (v - 1)) => LoosenRMin n m v where
+	(1 <= n, 1 <= v, LoosenRMin (n - 1) (m - 1) (v - 1)) => LoosenRMin n m v where
 	loosenRMin (xs :+ x) = loosenRMin xs :+ x
 
 -- LOOSEN RIGHT MAX
@@ -293,11 +293,11 @@
 instance LoosenRMax 0 0 m where loosenRMax NilR = NilR
 
 instance {-# OVERLAPPABLE #-}
-	LoosenRMax 0 (m - 1) (w - 1) => LoosenRMax 0 m w where
+	(1 <= w, LoosenRMax 0 (m - 1) (w - 1)) => LoosenRMax 0 m w where
 	loosenRMax = \case NilR -> NilR; xs :++ x -> loosenRMax xs :++ x
 
 instance {-# OVERLAPPABLE #-}
-	(1 <= n, LoosenRMax (n - 1) (m - 1) (w - 1)) => LoosenRMax n m w where
+	(1 <= n, 1 <= w, LoosenRMax (n - 1) (m - 1) (w - 1)) => LoosenRMax n m w where
 	loosenRMax (xs :+ x) = loosenRMax xs :+ x
 
 ---------------------------------------------------------------------------
@@ -354,7 +354,7 @@
 	unfoldlMRangeWithBase _ _ NilR = pure NilR
 	unfoldlMRangeMaybeWithBase p _ NilR = bool (Just NilR) Nothing <$> p
 
-instance {-# OVERLAPPABLE #-} Unfoldl 0 0 (w - 1) => Unfoldl 0 0 w where
+instance {-# OVERLAPPABLE #-} (1 <= w, Unfoldl 0 0 (w - 1)) => Unfoldl 0 0 w where
 	unfoldlMRangeWithBase p f = \case
 		NilR -> (p >>=) . bool (pure NilR) $ f >>= \x ->
 			(:++ x) <$> unfoldlMRangeWithBase p f NilR
@@ -365,7 +365,7 @@
 			((:++ x) <$>) <$> unfoldlMRangeMaybeWithBase p f NilR
 		xs :++ x -> ((:++ x) <$>) <$> unfoldlMRangeMaybeWithBase p f xs
 
-instance {-# OVERLAPPABLE #-} Unfoldl 0 (v - 1) (w - 1) => Unfoldl 0 v w where
+instance {-# OVERLAPPABLE #-} (1 <= v, 1 <= w, Unfoldl 0 (v - 1) (w - 1)) => Unfoldl 0 v w where
 	unfoldlMRangeWithBase p f = \case
 		NilR -> f >>= \x -> (:+ x) <$> unfoldlMRangeWithBase p f NilR
 		xs :++ x -> (:+ x) <$> unfoldlMRangeWithBase p f xs
@@ -376,7 +376,7 @@
 		xs :++ x -> ((:+ x) <$>) <$> unfoldlMRangeMaybeWithBase p f xs
 
 instance {-# OVERLAPPABLE #-}
-	(1 <= n, Unfoldl (n - 1) (v - 1) (w - 1)) => Unfoldl n v w where
+	(1 <= n, 1 <= v, Unfoldl (n - 1) (v - 1) (w - 1)) => Unfoldl n v w where
 	unfoldlMRangeWithBase p f (xs :+ x) =
 		(:+ x) <$> unfoldlMRangeWithBase p f xs
 
@@ -572,7 +572,7 @@
 instance ZipR n m 0 0 where zipWithMR _ xs NilR = pure (xs, NilR)
 
 instance {-# OVERLAPPABLE #-} (
-	1 <= n, LoosenRMin n m (n - w), LoosenRMax (n - w) (m - 1) m,
+	1 <= n, 1 <= m, w <= n, LoosenRMin n m (n - w), LoosenRMax (n - w) (m - 1) m,
 	ZipR (n - 1) (m - 1) 0 (w - 1) ) => ZipR n m 0 w where
 	zipWithMR _ xs NilR = pure (loosenRMin xs, NilR)
 	zipWithMR (%) (xs :+ x) (ys :++ y) =