diff --git a/ranged-list.cabal b/ranged-list.cabal
--- a/ranged-list.cabal
+++ b/ranged-list.cabal
@@ -1,13 +1,11 @@
 cabal-version: 1.12
 
--- This file has been generated from package.yaml by hpack version 0.34.4.
+-- This file has been generated from package.yaml by hpack version 0.35.0.
 --
 -- see: https://github.com/sol/hpack
---
--- hash: a22ce50d50583c3a0ac25b09f771d7f4456aa22f8154625866fdb128f05eb4b9
 
 name:           ranged-list
-version:        0.1.2.0
+version:        0.1.2.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
@@ -52,7 +50,7 @@
       src
   build-depends:
       base >=4.7 && <5
-    , typecheck-plugin-nat-simple
+    , typecheck-plugin-nat-simple >=0.1.0.9
   default-language: Haskell2010
 
 test-suite ranged-list-doctest
@@ -67,7 +65,7 @@
       base >=4.7 && <5
     , doctest
     , ranged-list
-    , typecheck-plugin-nat-simple
+    , typecheck-plugin-nat-simple >=0.1.0.9
   default-language: Haskell2010
 
 test-suite ranged-list-test
@@ -81,5 +79,5 @@
   build-depends:
       base >=4.7 && <5
     , ranged-list
-    , typecheck-plugin-nat-simple
+    , typecheck-plugin-nat-simple >=0.1.0.9
   default-language: Haskell2010
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
@@ -59,7 +59,7 @@
 
 -- MIN
 
-repeatLMin :: (LoosenLMax n n m, Unfoldr 0 n n) => a -> RangeL n m a
+repeatLMin :: (0 <= n, LoosenLMax n n m, Unfoldr 0 n n) => a -> RangeL n m a
 repeatLMin = unfoldrMin \x -> (x, x)
 
 {-^
@@ -73,7 +73,7 @@
 -}
 
 unfoldrMin ::
-	(LoosenLMax n n m, Unfoldr 0 n n) => (s -> (a, s)) -> s -> RangeL n m a
+	(0 <= n, LoosenLMax n n m, Unfoldr 0 n n) => (s -> (a, s)) -> s -> RangeL n m a
 unfoldrMin f = loosenLMax . unfoldr f
 
 {-^
@@ -88,7 +88,7 @@
 -}
 
 unfoldrMMin ::
-	(Monad m, LoosenLMax n n w, Unfoldr 0 n n) => m a -> m (RangeL n w a)
+	(0 <= n, Monad m, LoosenLMax n n w, Unfoldr 0 n n) => m a -> m (RangeL n w a)
 unfoldrMMin f = loosenLMax <$> unfoldrM f
 
 {-^
@@ -106,7 +106,7 @@
 
 -- MAX
 
-repeatLMax :: (LoosenLMin m m n, Unfoldr 0 m m) => a -> RangeL n m a
+repeatLMax :: (0 <= m, LoosenLMin m m n, Unfoldr 0 m m) => a -> RangeL n m a
 repeatLMax = unfoldrMax \x -> (x, x)
 
 {-^
@@ -120,7 +120,7 @@
 -}
 
 unfoldrMax ::
-	(LoosenLMin m m n, Unfoldr 0 m m) => (s -> (a, s)) -> s -> RangeL n m a
+	(0 <= m, LoosenLMin m m n, Unfoldr 0 m m) => (s -> (a, s)) -> s -> RangeL n m a
 unfoldrMax f = loosenLMin . unfoldr f
 
 {-^
@@ -135,7 +135,7 @@
 -}
 
 unfoldrMMax ::
-	(Monad m, LoosenLMin w w n, Unfoldr 0 w w) => m a -> m (RangeL n w a)
+	(0 <= w, Monad m, LoosenLMin w w n, Unfoldr 0 w w) => m a -> m (RangeL n w a)
 unfoldrMMax f = loosenLMin <$> unfoldrM f
 
 {-^
@@ -157,7 +157,7 @@
 
 -- MIN
 
-repeatRMin :: (LoosenRMax n n m, Unfoldl 0 n n) => a -> RangeR n m a
+repeatRMin :: (0 <= n, LoosenRMax n n m, Unfoldl 0 n n) => a -> RangeR n m a
 repeatRMin = unfoldlMin \x -> (x, x)
 
 {-^
@@ -171,7 +171,7 @@
 -}
 
 unfoldlMin ::
-	(LoosenRMax n n m, Unfoldl 0 n n) => (s -> (s, a)) -> s -> RangeR n m a
+	(0 <= n, LoosenRMax n n m, Unfoldl 0 n n) => (s -> (s, a)) -> s -> RangeR n m a
 unfoldlMin f = loosenRMax . unfoldl f
 
 {-^
@@ -186,7 +186,7 @@
 -}
 
 unfoldlMMin ::
-	(Monad m, LoosenRMax n n w, Unfoldl 0 n n) => m a -> m (RangeR n w a)
+	(0 <= n, Monad m, LoosenRMax n n w, Unfoldl 0 n n) => m a -> m (RangeR n w a)
 unfoldlMMin f = loosenRMax <$> unfoldlM f
 
 {-^
@@ -204,7 +204,7 @@
 
 -- MAX
 
-repeatRMax :: (LoosenRMin m m n, Unfoldl 0 m m) => a -> RangeR n m a
+repeatRMax :: (0 <= m, LoosenRMin m m n, Unfoldl 0 m m) => a -> RangeR n m a
 repeatRMax = unfoldlMax \x -> (x, x)
 
 {-^
@@ -218,7 +218,7 @@
 -}
 
 unfoldlMax ::
-	(LoosenRMin m m n, Unfoldl 0 m m) => (s -> (s, a)) -> s -> RangeR n m a
+	(0 <= m, LoosenRMin m m n, Unfoldl 0 m m) => (s -> (s, a)) -> s -> RangeR n m a
 unfoldlMax f = loosenRMin . unfoldl f
 
 {-^
@@ -233,7 +233,7 @@
 -}
 
 unfoldlMMax ::
-	(Monad m, LoosenRMin w w n, Unfoldl 0 w w) => m a -> m (RangeR n w a)
+	(0 <= w, Monad m, LoosenRMin w w n, Unfoldl 0 w w) => m a -> m (RangeR n w a)
 unfoldlMMax f = loosenRMin <$> unfoldlM f
 
 {-^
@@ -279,12 +279,14 @@
 instance LeftToRight n m 0 0 where n ++.+ _ = n
 
 instance {-# OVERLAPPABLE #-} (
-	1 <= n, PushR (n - 1) (m - 1), LoosenRMax n m (m + w),
+	1 <= n, 1 <= m + 1, PushR (n - 1) m, 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
+	(++.+) :: forall a . RangeR n m a -> RangeL 0 w a -> RangeR n (m + w) a
+	(++.+) n = \case NilL -> loosenRMax n; x :.. v -> (n .:++ x :: RangeR n (m + 1) a) ++.+ v
 
-instance {-# OVERLAPPABLE #-}
-	(1 <= v, LeftToRight (n + 1) (m + 1) (v - 1) (w - 1)) =>
+instance {-# OVERLAPPABLE #-} (
+	1 <= n + 1, 1 <= m + 1, 1 <= v,
+	LeftToRight (n + 1) (m + 1) (v - 1) (w - 1)) =>
 	LeftToRight n m v w where
 	(++.+) :: forall a .
 		RangeR n m a -> RangeL v w a -> RangeR (n + v) (m + w) a
@@ -339,12 +341,15 @@
 instance RightToLeft 0 0 v w where _ ++.. v = v
 
 instance {-# OVERLAPPABLE #-} (
-	1 <= v, PushL (v - 1) (w - 1), LoosenLMax v w (m + w),
+	1 <= v, 1 <= w + 1, PushL (v - 1) w, 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 .:..)
+	(++..) :: forall a . RangeR 0 m a -> RangeL v w a -> RangeL v (m + w) a
+	NilR ++.. l = loosenLMax l
+	(n :++ x) ++.. l = n ++.. (x .:.. l :: RangeL v (w + 1) a)
 
 instance {-# OVERLAPPABLE #-} (
-	1 <= n, RightToLeft (n - 1) (m - 1) (v + 1) (w + 1) ) =>
+	1 <= n, 1 <= v + 1, 1 <= w + 1,
+	RightToLeft (n - 1) (m - 1) (v + 1) (w + 1) ) =>
 	RightToLeft n m v w where
 	(++..) :: forall a .
 		RangeR n m a -> RangeL v w a -> RangeL (n + v) (m + w) a
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
@@ -58,7 +58,7 @@
 
 -}
 
-fromIntL :: Unfoldr 0 n m => Int -> Maybe (RangedNatL n m)
+fromIntL :: (0 <= m, Unfoldr 0 n m) => Int -> Maybe (RangedNatL n m)
 fromIntL = unfoldrRangeMaybe \s -> bool Nothing (Just ((), s - 1)) (s > 0)
 
 {-^
@@ -123,7 +123,7 @@
 
 -}
 
-fromIntR :: Unfoldl 0 n m => Int -> Maybe (RangedNatR n m)
+fromIntR :: (0 <= m, Unfoldl 0 n m) => Int -> Maybe (RangedNatR n m)
 fromIntR = unfoldlRangeMaybe \s -> bool Nothing (Just (s - 1, ())) (s > 0)
 
 {-^
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
@@ -152,30 +152,39 @@
 
 instance Applicative (LengthL 0) where pure _ = NilL; _ <*> _ = NilL
 
-instance {-# OVERLAPPABLE #-} (Functor (RangeL 0 m), Applicative (RangeL 0 (m - 1)), Unfoldr 0 0 m) => Applicative (RangeL 0 m) where
+instance {-# OVERLAPPABLE #-} (
+	0 <= m,
+	Functor (RangeL 0 m), Applicative (RangeL 0 (m - 1)), Unfoldr 0 0 m) =>
+	Applicative (RangeL 0 m) where
 	pure = unfoldrRange (const True) (\x -> (x, x))
 	NilL <*> _ = NilL
 	_ <*> NilL = NilL
 	f :.. fs <*> x :.. xs = f x :.. (fs <*> xs)
 
-instance {-# OVERLAPPABLE #-} (1 <= n, Functor (RangeL n m), Applicative (RangeL (n - 1) (m - 1)), Unfoldr 0 n m) => Applicative (RangeL n m) where
+instance {-# OVERLAPPABLE #-} (
+	1 <= n, 0 <= m,
+	Functor (RangeL n m), Applicative (RangeL (n - 1) (m - 1)),
+	Unfoldr 0 n m) =>
+	Applicative (RangeL n m) where
 	pure = unfoldrRange (const True) (\x -> (x, x))
 	f :. fs <*> x :. xs = f x :. (fs <*> xs)
 
 instance Applicative (LengthL 0) => Monad (LengthL 0) where
 	NilL >>= _ = NilL
 
-instance {-# OVERLAPPABLE #-} (1 <= n, Applicative (LengthL n), Monad (LengthL (n - 1))) => Monad (LengthL n) where
+instance {-# OVERLAPPABLE #-} (
+	1 <= n, Applicative (LengthL n), Monad (LengthL (n - 1)) ) =>
+	Monad (LengthL n) where
 	x :. xs >>= f = y :. (xs >>= \z -> case f z of _ :. zs -> zs)
 		where y :. _ = f x
 
 -- INSTANCE ISSTRING
 
-instance Unfoldr 0 n m => IsString (RangeL n m Char) where
+instance (0 <= m, Unfoldr 0 n m) => IsString (RangeL n m Char) where
 	fromString s = fromMaybe (error $ "The string " ++ show s ++ " is not within range.")
 		$ unfoldrRangeMaybe (\case "" -> Nothing; c : cs -> Just (c, cs)) s
 
-instance (Foldable (RangeL n m), Unfoldr 0 n m) => IsList (RangeL n m a) where
+instance (0 <= m, Foldable (RangeL n m), Unfoldr 0 n m) => IsList (RangeL n m a) where
 	type Item (RangeL n m a) = a
 	fromList lst = fromMaybe (error $ "The list is not within range.")
 		$ unfoldrRangeMaybe (\case [] -> Nothing; x : xs -> Just (x, xs)) lst
@@ -188,7 +197,7 @@
 infixr 5 .:..
 
 class PushL n m where
-	(.:..) :: a -> RangeL n m a -> RangeL n (m + 1) a
+	(.:..) :: a -> RangeL n (m - 1) a -> RangeL n m a
 
 	{-^
 
@@ -203,10 +212,9 @@
 
 	-}
 
-instance PushL 0 m where
-	(.:..) x = \case NilL -> x :.. NilL; xs@(_ :.. _) -> x :.. xs
+instance 1 <= m => PushL 0 m where (.:..) = (:..)
 
-instance {-# OVERLAPPABLE #-} (1 <= n, PushL (n - 1) (m - 1)) => PushL n m where
+instance {-# OVERLAPPABLE #-} (1 <= n, 1 <= m, PushL (n - 1) (m - 1)) => PushL n m where
 	x .:.. y :. ys = x :. (y .:.. ys)
 
 ---------------------------------------------------------------------------
@@ -236,14 +244,15 @@
 instance AddL 0 0 v w where NilL ++. ys = ys
 
 instance {-# OVERLAPPABLE #-}
-	(PushL v (m + w - 1), AddL 0 (m - 1) v w, LoosenLMax v w (m + w)) =>
+	(PushL v (m + w), AddL 0 (m - 1) v w, LoosenLMax v w (m + w)) =>
 	AddL 0 m v w where
 	(++.) :: forall a .  RangeL 0 m a -> RangeL v w a -> RangeL v (m + w) a
 	NilL ++. ys = loosenLMax ys
 	x :.. xs ++. ys = x .:.. (xs ++. ys :: RangeL v (m + w - 1) a)
 
 instance {-# OVERLAPPABLE #-}
-	(1 <= n, AddL (n - 1) (m - 1) v w) => AddL n m v w where
+	(1 <= n, 1 <= n + v, 1 <= m + w, AddL (n - 1) (m - 1) v w) =>
+	AddL n m v w where
 	x :. xs ++. ys = x :. (xs ++. ys)
 
 ---------------------------------------------------------------------------
@@ -317,10 +326,10 @@
 
 	-}
 
-instance LoosenLMax 0 0 w where loosenLMax NilL = NilL
+instance 0 <= w => LoosenLMax 0 0 w where loosenLMax NilL = NilL
 
 instance {-# OVERLAPPABLE #-}
-	(1 <= w, LoosenLMax 0 (m - 1) (w - 1)) => LoosenLMax 0 m w where
+	(0 <= w, 1 <= w, LoosenLMax 0 (m - 1) (w - 1)) => LoosenLMax 0 m w where
 	loosenLMax = \case NilL -> NilL; (x :.. xs) -> x :.. loosenLMax xs
 
 instance {-# OVERLAPPABLE #-}
@@ -380,7 +389,8 @@
 	unfoldrMRangeWithBase NilL _ _ = pure NilL
 	unfoldrMRangeMaybeWithBase NilL p _ = bool (Just NilL) Nothing <$> p
 
-instance {-# OVERLAPPABLE #-} (1 <= w, Unfoldr 0 0 (w - 1)) => Unfoldr 0 0 w where
+instance {-# OVERLAPPABLE #-} (0 <= w - 1, 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
@@ -394,7 +404,7 @@
 		((x :..) <$>) <$> unfoldrMRangeMaybeWithBase xs p f
 
 instance {-# OVERLAPPABLE #-}
-	(1 <= v, 1 <= w, Unfoldr 0 (v - 1) (w - 1)) => Unfoldr 0 v w where
+	(1 <= v, 0 <= w - 1, 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 =
@@ -416,7 +426,7 @@
 
 -- UNFOLDR RANGE
 
-unfoldrRange :: Unfoldr 0 v w =>
+unfoldrRange :: (0 <= w, Unfoldr 0 v w) =>
 	(s -> Bool) -> (s -> (a, s)) -> s -> RangeL v w a
 unfoldrRange = unfoldrRangeWithBase NilL
 
@@ -473,7 +483,7 @@
 
 -}
 
-unfoldrMRange :: (Unfoldr 0 v w, Monad m) => m Bool -> m a -> m (RangeL v w a)
+unfoldrMRange :: (0 <= w, Unfoldr 0 v w, Monad m) => m Bool -> m a -> m (RangeL v w a)
 unfoldrMRange = unfoldrMRangeWithBase NilL
 
 {-^
@@ -491,7 +501,7 @@
 
 -- UNFOLDR RANGE MAYBE
 
-unfoldrRangeMaybe :: Unfoldr 0 v w =>
+unfoldrRangeMaybe :: (0 <= w, Unfoldr 0 v w) =>
 	(s -> Maybe (a, s)) -> s -> Maybe (RangeL v w a)
 unfoldrRangeMaybe = unfoldrRangeMaybeWithBase NilL
 
@@ -541,7 +551,7 @@
 unfoldrRangeMaybeWithBaseGen xs p f =
 	runStateL $ unfoldrMRangeMaybeWithBase xs (StateL p) (StateL f)
 
-unfoldrMRangeMaybe :: (Unfoldr 0 v w, Monad m) =>
+unfoldrMRangeMaybe :: (0 <= w, Unfoldr 0 v w, Monad m) =>
 	m Bool -> m a -> m (Maybe (RangeL v w a))
 unfoldrMRangeMaybe = unfoldrMRangeMaybeWithBase NilL
 
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
@@ -139,17 +139,17 @@
 
 instance Applicative (RangeR 0 0) where pure _ = NilR; _ <*> _ = NilR
 
-instance {-# OVERLAPPABLE #-} (1 <= n, Functor (RangeR n n), Applicative (RangeR (n - 1) (n - 1)), Unfoldl 0 n n) => Applicative (RangeR n n) where
+instance {-# OVERLAPPABLE #-} (0 <= n, 1 <= n, Functor (RangeR n n), Applicative (RangeR (n - 1) (n - 1)), Unfoldl 0 n n) => Applicative (RangeR n n) where
 	pure = unfoldlRange (const True) (\x -> (x, x))
 	fs :+ f <*> xs :+ x = (fs <*> xs) :+ f x
 
-instance {-# OVERLAPPABLE #-} (Functor (RangeR 0 m), Applicative (RangeR 0 (m - 1)), Unfoldl 0 0 m) => Applicative (RangeR 0 m) where
+instance {-# OVERLAPPABLE #-} (0 <= m, Functor (RangeR 0 m), Applicative (RangeR 0 (m - 1)), Unfoldl 0 0 m) => Applicative (RangeR 0 m) where
 	pure = unfoldlRange (const True) (\x -> (x, x))
 	NilR <*> _ = NilR
 	_ <*> NilR = NilR
 	fs :++ f <*> xs :++ x = (fs <*> xs) :++ f x
 
-instance {-# OVERLAPPABLE #-} (1 <= n, Functor (RangeR n m), Applicative (RangeR (n - 1) (m - 1)), Unfoldl 0 n m) => Applicative (RangeR n m) where
+instance {-# OVERLAPPABLE #-} (0 <= m, 1 <= n, Functor (RangeR n m), Applicative (RangeR (n - 1) (m - 1)), Unfoldl 0 n m) => Applicative (RangeR n m) where
 	pure = unfoldlRange (const True) (\x -> (x, x))
 	fs :+ f <*> xs :+ x = (fs <*> xs) :+ f x
 
@@ -162,11 +162,11 @@
 
 -- INSTANCE ISSTRING
 
-instance Unfoldl 0 n m => IsString (RangeR n m Char) where
+instance (0 <= m, Unfoldl 0 n m) => IsString (RangeR n m Char) where
 	fromString s = fromMaybe (error $ "The string " ++ show s ++ " is not within range.")
 		. unfoldlRangeMaybe (\case "" -> Nothing; c : cs -> Just (cs, c)) $ reverse s
 
-instance (Foldable (RangeR n m), Unfoldl 0 n m) => IsList (RangeR n m a) where
+instance (0 <= m, Foldable (RangeR n m), Unfoldl 0 n m) => IsList (RangeR n m a) where
 	type Item (RangeR n m a) = a
 	fromList lst = fromMaybe (error $ "The list is not within range.")
 		. unfoldlRangeMaybe (\case [] -> Nothing; x : xs -> Just (xs, x)) $ reverse lst
@@ -179,7 +179,7 @@
 infixl 5 .:++
 
 class PushR n m where
-	(.:++) :: RangeR n m a -> a -> RangeR n (m + 1) a
+	(.:++) :: RangeR n (m - 1) a -> a -> RangeR n m a
 
 	{-^
 
@@ -194,10 +194,10 @@
 
 	-}
 
-instance PushR 0 m where
+instance 1 <= m => PushR 0 m where
 	(.:++) = \case NilR -> (NilR :++); xs@(_ :++ _) -> (xs :++)
 
-instance {-# OVERLAPPABLE #-} (1 <= n, PushR (n - 1) (m - 1)) => PushR n m where
+instance {-# OVERLAPPABLE #-} (1 <= m, 1 <= n, PushR (n - 1) (m - 1)) => PushR n m where
 	xs :+ x .:++ y = (xs .:++ x) :+ y
 
 ---------------------------------------------------------------------------
@@ -226,15 +226,16 @@
 instance AddR n m 0 0 where xs +++ NilR = xs
 
 instance {-# OVERLAPPABLE #-}
-	(PushR n (m + w - 1), AddR n m 0 (w - 1), LoosenRMax n m (m + w)) =>
+	(1 <= n, PushR n (m + w), AddR n m 0 (w - 1), LoosenRMax n m (m + w)) =>
 	AddR n m 0 w where
 	(+++) :: forall a . RangeR n m a -> RangeR 0 w a -> RangeR n (m + w) a
 	(+++) xs = \case
 		NilR -> loosenRMax xs
 		ys :++ y -> (xs +++ ys :: RangeR n (m + w - 1) a) .:++ y
 
-instance {-# OVERLAPPABLE #-}
-	(1 <= v, AddR n m (v - 1) (w - 1)) => AddR n m v w where
+instance {-# OVERLAPPABLE #-} (
+	1 <= v, 1 <= n + v, 1 <= m + w, AddR n m (v - 1) (w - 1) ) =>
+	AddR n m v w where
 	xs +++ ys :+ y = (xs +++ ys) :+ y
 
 ---------------------------------------------------------------------------
@@ -308,10 +309,10 @@
 
 	-}
 
-instance LoosenRMax 0 0 m where loosenRMax NilR = NilR
+instance 0 <= m => LoosenRMax 0 0 m where loosenRMax NilR = NilR
 
 instance {-# OVERLAPPABLE #-}
-	(1 <= w, LoosenRMax 0 (m - 1) (w - 1)) => LoosenRMax 0 m w where
+	(0 <= w, 1 <= w, LoosenRMax 0 (m - 1) (w - 1)) => LoosenRMax 0 m w where
 	loosenRMax = \case NilR -> NilR; xs :++ x -> loosenRMax xs :++ x
 
 instance {-# OVERLAPPABLE #-}
@@ -372,7 +373,7 @@
 	unfoldlMRangeWithBase _ _ NilR = pure NilR
 	unfoldlMRangeMaybeWithBase p _ NilR = bool (Just NilR) Nothing <$> p
 
-instance {-# OVERLAPPABLE #-} (1 <= w, Unfoldl 0 0 (w - 1)) => Unfoldl 0 0 w where
+instance {-# OVERLAPPABLE #-} (0 <= w - 1, 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
@@ -383,7 +384,7 @@
 			((:++ x) <$>) <$> unfoldlMRangeMaybeWithBase p f NilR
 		xs :++ x -> ((:++ x) <$>) <$> unfoldlMRangeMaybeWithBase p f xs
 
-instance {-# OVERLAPPABLE #-} (1 <= v, 1 <= w, Unfoldl 0 (v - 1) (w - 1)) => Unfoldl 0 v w where
+instance {-# OVERLAPPABLE #-} (1 <= v, 0 <= w - 1, 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
@@ -403,7 +404,7 @@
 
 -- UNFOLDL RANGE
 
-unfoldlRange :: Unfoldl 0 v w =>
+unfoldlRange :: (0 <= w, Unfoldl 0 v w) =>
 	(s -> Bool) -> (s -> (s, a)) -> s -> RangeR v w a
 unfoldlRange p f s = unfoldlRangeWithBase p f s NilR
 
@@ -461,7 +462,7 @@
 
 -}
 
-unfoldlMRange :: (Unfoldl 0 v w, Monad m) => m Bool -> m a -> m (RangeR v w a)
+unfoldlMRange :: (0 <= w, Unfoldl 0 v w, Monad m) => m Bool -> m a -> m (RangeR v w a)
 unfoldlMRange p f = unfoldlMRangeWithBase p f NilR
 
 {-^
@@ -480,7 +481,7 @@
 -- UNFOLDL RANGE MAYBE
 
 unfoldlRangeMaybe ::
-	Unfoldl 0 v w => (s -> Maybe (s, a)) -> s -> Maybe (RangeR v w a)
+	(0 <= w, Unfoldl 0 v w) => (s -> Maybe (s, a)) -> s -> Maybe (RangeR v w a)
 unfoldlRangeMaybe f s = unfoldlRangeMaybeWithBase f s NilR
 
 {-^
@@ -530,7 +531,7 @@
 unfoldlRangeMaybeWithBaseGen p f =
 	runStateR . unfoldlMRangeMaybeWithBase (StateR p) (StateR f)
 
-unfoldlMRangeMaybe :: (Unfoldl 0 v w, Monad m) =>
+unfoldlMRangeMaybe :: (0 <= w, Unfoldl 0 v w, Monad m) =>
 	m Bool -> m a -> m (Maybe (RangeR v w a))
 unfoldlMRangeMaybe p f = unfoldlMRangeMaybeWithBase p f NilR