diff --git a/Data/Sized.hs b/Data/Sized.hs
--- a/Data/Sized.hs
+++ b/Data/Sized.hs
@@ -1,14 +1,17 @@
-{-# LANGUAGE ConstraintKinds, DataKinds, DeriveDataTypeable, DeriveFoldable #-}
-{-# LANGUAGE DeriveFunctor, DeriveTraversable, FlexibleContexts             #-}
-{-# LANGUAGE FlexibleInstances, GADTs, GeneralizedNewtypeDeriving           #-}
-{-# LANGUAGE KindSignatures, LambdaCase, LiberalTypeSynonyms                #-}
-{-# LANGUAGE MultiParamTypeClasses, NoMonomorphismRestriction               #-}
-{-# LANGUAGE PatternSynonyms, PolyKinds, ScopedTypeVariables                #-}
-{-# LANGUAGE StandaloneDeriving, TypeFamilies, TypeOperators, ViewPatterns  #-}
+{-# LANGUAGE AllowAmbiguousTypes, ConstraintKinds, DataKinds               #-}
+{-# LANGUAGE DeriveDataTypeable, DeriveFoldable, DeriveFunctor             #-}
+{-# LANGUAGE DeriveTraversable, ExplicitNamespaces, FlexibleContexts       #-}
+{-# LANGUAGE FlexibleInstances, GADTs, GeneralizedNewtypeDeriving          #-}
+{-# LANGUAGE KindSignatures, LambdaCase, LiberalTypeSynonyms               #-}
+{-# LANGUAGE MultiParamTypeClasses, NoMonomorphismRestriction              #-}
+{-# LANGUAGE PatternSynonyms, PolyKinds, ScopedTypeVariables               #-}
+{-# LANGUAGE StandaloneDeriving, TypeApplications, TypeFamilies            #-}
+{-# LANGUAGE TypeInType, TypeOperators, UndecidableInstances, ViewPatterns #-}
 {-# OPTIONS_GHC -fno-warn-type-defaults -fno-warn-orphans #-}
+{-# OPTIONS_GHC -fenable-rewrite-rules #-}
 -- | This module provides the functionality to make length-parametrized types
 --   from existing 'ListLike' and 'Functor' sequential types.
--- 
+--
 --   Most of the complexity of operations for @Sized f n a@ are the same as
 --   original operations for @f@. For example, '!!' is O(1) for
 --   @Sized Vector n a@ but O(i) for @Sized [] n a@.
@@ -17,12 +20,15 @@
 --  inspect the sized sequence. See <#ViewsAndPatterns Views and Patterns> for more detail.
 module Data.Sized
        ( -- * Main Data-types
-         Sized(), ListLikeF, SomeSized(..),
+         Sized(), SomeSized(..),
+         instLL, instFunctor, ListLikeF,
+         withListLikeF, withListLikeF',
          -- * Accessors
          -- ** Length information
          length, sLength, null,
          -- ** Indexing
-         (!!), (%!!), index, sIndex, head, last, uncons, unsnoc,
+         (!!), (%!!), index, sIndex, head, last,
+         uncons, uncons', unsnoc, unsnoc',
          -- ** Slicing
          tail, init, take, takeAtMost, drop, splitAt, splitAtMost,
          -- * Construction
@@ -33,7 +39,7 @@
          -- ** Zips
          zip, zipSame, zipWith, zipWithSame, unzip,
          -- * Transformation
-         map, reverse, intersperse, nub, sort, sortBy, insert, insertBy,
+         map, fmap, reverse, intersperse, nub, sort, sortBy, insert, insertBy,
          -- * Conversion
          -- ** List
          toList, fromList, fromList', unsafeFromList, unsafeFromList',
@@ -47,8 +53,10 @@
          Partitioned(..),
          takeWhile, dropWhile, span, break, partition,
          -- ** Searching
-         elem, notElem, find, findIndex, sFindIndex, findIndices, sFindIndices,
-         elemIndex, sElemIndex, elemIndices, sElemIndices,
+         elem, notElem, find, findF, findIndex, findIndexIF,
+         sFindIndex, sFindIndexIF,
+         findIndices, findIndicesIF, sFindIndices, sFindIndicesIF,
+         elemIndex, sElemIndex, sUnsafeElemIndex, elemIndices, sElemIndices,
          -- * Views and Patterns
          -- $ViewsAndPatterns
 
@@ -66,18 +74,37 @@
 
 import Data.Sized.Internal
 
-import qualified Data.ListLike         as LL
-import           Data.Proxy            (Proxy (..))
-import           Data.Type.Monomorphic
-import           Data.Type.Natural
-import           Data.Type.Ordinal     (Ordinal, ordToInt)
-import           Data.Typeable         (Typeable)
-import           Prelude               (Bool (..), Enum (..), Eq (..),
-                                        Functor (..), Int, Maybe (..), Num (..),
-                                        Ord (..), Ordering, Show (..), flip,
-                                        undefined, ($), (.))
-import qualified Prelude               as P
-import           Unsafe.Coerce         (unsafeCoerce)
+import           Control.Applicative          ((<$>), (<*>))
+import           Control.Lens.Indexed         (FoldableWithIndex (..), ifind)
+import           Data.Foldable                (Foldable)
+import qualified Data.Foldable                as F
+import           Data.Kind                    (Type)
+import qualified Data.List                    as L
+import           Data.ListLike                (ListLike)
+import qualified Data.ListLike                as LL
+import           Data.Monoid                  (Endo (..), First (..))
+import qualified Data.Sequence                as Seq
+import           Data.Singletons.Prelude      (PNum (..), POrd (..), SOrd (..))
+import           Data.Singletons.Prelude      (Sing (..), SingI (..))
+import           Data.Singletons.Prelude      (withSing, withSingI)
+import           Data.Singletons.Prelude.Enum (PEnum (..))
+import           Data.Type.Monomorphic        (Monomorphic (..))
+import           Data.Type.Monomorphic        (Monomorphicable (..))
+import qualified Data.Type.Natural            as Peano
+import           Data.Type.Natural.Class
+import           Data.Type.Ordinal            (HasOrdinal, Ordinal (..))
+import           Data.Type.Ordinal            (ordToInt, unsafeFromInt)
+import           Data.Typeable                (Typeable)
+import qualified Data.Vector                  as V
+import qualified Data.Vector.Storable         as SV
+import qualified Data.Vector.Unboxed          as UV
+import qualified GHC.TypeLits                 as TL
+import           Prelude                      (Bool (..), Enum (..), Eq (..))
+import           Prelude                      (Functor, Int, Maybe (..))
+import           Prelude                      (Num (..), Ord (..), Ordering)
+import           Prelude                      (Show (..), flip, fst, ($), (.))
+import qualified Prelude                      as P
+import           Unsafe.Coerce                (unsafeCoerce)
 
 --------------------------------------------------------------------------------
 -- Main data-types
@@ -91,18 +118,25 @@
 -- @xs@ of element type @a@ and length @sn@.
 --
 -- Since 0.1.0.0
-data SomeSized f a where
-  SomeSized :: (ListLikeF f, SingI n)
-            => SNat n
-            -> Sized f (n :: Nat) a
-            -> SomeSized f a
+data SomeSized f nat a where
+  SomeSized :: (ListLike (f a) a)
+            => Sing n
+            -> Sized f (n :: nat) a
+            -> SomeSized f nat a
 
 deriving instance Typeable SomeSized
 
-deriving instance Show (f a) => Show (SomeSized f a)
-instance Eq (f a) => Eq (SomeSized f a) where
+instance Show (f a) => Show (SomeSized f nat a) where
+  showsPrec d (SomeSized _ s) = P.showParen (d > 9) $
+    P.showString "SomeSized _ " . showsPrec 10 s
+instance Eq (f a) => Eq (SomeSized f nat a) where
   (SomeSized _ (Sized xs)) == (SomeSized _ (Sized ys)) = xs == ys
 
+demote' :: HasOrdinal nat => Sing (n :: nat) -> MonomorphicRep (Sing :: nat -> Type)
+demote' = demote . Monomorphic
+{-# SPECIALISE demote' :: Sing (n :: TL.Nat) -> P.Integer #-}
+{-# SPECIALISE demote' :: Sing (n :: Peano.Nat) -> P.Integer #-}
+
 --------------------------------------------------------------------------------
 -- Accessors
 --------------------------------------------------------------------------------
@@ -114,101 +148,152 @@
 -- | Returns the length of wrapped containers.
 --   If you use @unsafeFromList@ or similar unsafe functions,
 --   this function may return different value from type-parameterized length.
--- 
+--
 -- Since 0.1.0.0
-length :: ListLikeF f => Sized f n a -> Int
-length = givenListLikeF LL.length . runSized
-{-# INLINE length #-}
+length :: ListLike (f a) a => Sized f n a -> Int
+length = LL.length . runSized
+{-# INLINE [1] length #-}
+{-# RULES
+"length/0" [~1] forall (xs :: Sized f 0 a).
+  length xs = 0
+"length/Z" [~1] forall (xs :: Sized f 'Peano.Z a).
+  length xs = 0
+  #-}
 
--- | @SNat@ version of 'length'.
--- 
--- Since 0.1.0.0
-sLength :: SingI n => Sized f n a -> SNat n
-sLength _ = sing
-{-# INLINE sLength #-}
+-- | @Sing@ version of 'length'.
+--
+-- Since 0.2.0.0
+sLength :: forall f (n :: nat) a. (HasOrdinal nat, ListLike (f a) a)
+        => Sized f n a -> Sing n
+sLength (Sized xs) =
+  case promote (P.fromIntegral $ LL.length xs) of
+    Monomorphic (n :: Sing (k :: nat)) -> unsafeCoerce n
+{-# INLINE[2] sLength #-}
+{-# RULES
+"sLength/KnownNat" [~1] forall (xs :: TL.KnownNat n => Sized f n a).
+  sLength xs = sing :: Sing n
+"sLength/SingI" [~2] forall (xs :: SingI n => Sized f n a).
+  sLength xs = sing :: Sing n
+  #-}
 
 -- | Test if the sequence is empty or not.
--- 
+--
 -- Since 0.1.0.0
-null :: ListLikeF f => Sized f n a -> Bool
-null = givenListLikeF' LL.null
-{-# INLINE [2] null #-}
+null :: ListLike (f a) a => Sized f n a -> Bool
+null = LL.null . runSized
+{-# INLINE CONLIKE [1] null #-}
 {-# RULES
-"null/Zero" forall (xs :: Sized f Z a).
+"null/0" [~1] forall (xs :: Sized f 0 a).
   null xs = True
-"null/Succ" forall (xs :: Sized f (S n) a).
-  null xs = False
-  #-}
 
+"null/Z" [~1] forall (xs :: Sized f 'Peano.Z a).
+  null xs = True
+#-}
+
 --------------------------------------------------------------------------------
 --- Indexing
 --------------------------------------------------------------------------------
 
 -- | (Unsafe) indexing with @Int@s.
 --   If you want to check boundary statically, use '%!!' or 'sIndex'.
--- 
+--
 -- Since 0.1.0.0
-(!!) :: (ListLikeF f) => Sized f (S m) a -> Int -> a
-Sized xs !! n = withListLikeF' xs $ LL.index xs n
+(!!) :: (ListLike (f a) a) => Sized f (Succ m) a -> Int -> a
+Sized xs !! n = LL.index xs n
 {-# INLINE (!!) #-}
 
 -- | Safe indexing with 'Ordinal's.
--- 
+--
 -- Since 0.1.0.0
-(%!!) :: ListLikeF f => Sized f n a -> Ordinal n -> a
-Sized xs %!! n = withListLikeF' xs $ LL.index xs (ordToInt n)
+(%!!) :: (HasOrdinal nat, LL.ListLike (f c) c) => Sized f n c -> Ordinal (n :: nat) -> c
+Sized xs %!! n = LL.index xs $ P.fromIntegral $ ordToInt n
 {-# INLINE (%!!) #-}
+{-# SPECIALISE (%!!) :: Sized [] (n :: TL.Nat) a -> Ordinal n -> a #-}
+{-# SPECIALISE (%!!) :: Sized [] (n :: Peano.Nat) a -> Ordinal n -> a #-}
+{-# SPECIALISE (%!!) :: Sized V.Vector (n :: TL.Nat) a -> Ordinal n -> a #-}
+{-# SPECIALISE (%!!) :: Sized V.Vector (n :: Peano.Nat) a -> Ordinal n -> a #-}
+{-# SPECIALISE (%!!) :: UV.Unbox a => Sized UV.Vector (n :: TL.Nat) a -> Ordinal n -> a #-}
+{-# SPECIALISE (%!!) :: UV.Unbox a => Sized UV.Vector (n :: Peano.Nat) a -> Ordinal n -> a #-}
+{-# SPECIALISE (%!!) :: SV.Storable a => Sized SV.Vector (n :: TL.Nat) a -> Ordinal n -> a #-}
+{-# SPECIALISE (%!!) :: SV.Storable a => Sized SV.Vector (n :: Peano.Nat) a -> Ordinal n -> a #-}
+{-# SPECIALISE (%!!) :: Sized Seq.Seq (n :: TL.Nat) a -> Ordinal n -> a #-}
+{-# SPECIALISE (%!!) :: Sized Seq.Seq (n :: Peano.Nat) a -> Ordinal n -> a #-}
 
 -- | Flipped version of '!!'.
--- 
+--
 -- Since 0.1.0.0
-index :: (ListLikeF f) => Int -> Sized f (S m) c -> c
-index = flip (!!)
+index :: (ListLike (f a) a) => Int -> Sized f (Succ m) a -> a
+index n (Sized xs) =  LL.index xs n
 {-# INLINE index #-}
 
 -- | Flipped version of '%!!'.
--- 
+--
 -- Since 0.1.0.0
-sIndex :: ListLikeF f => Ordinal n -> Sized f n c -> c
+sIndex :: (HasOrdinal nat, ListLike (f c) c) => Ordinal (n :: nat) -> Sized f n c -> c
 sIndex = flip (%!!)
 {-# INLINE sIndex #-}
 
 -- | Take the first element of non-empty sequence.
 --   If you want to make case-analysis for general sequence,
 --   see  <#ViewsAndPatterns Views and Patterns> section.
--- 
+--
 -- Since 0.1.0.0
-head :: ListLikeF f => Sized f (S n) a -> a
-head = givenListLikeF LL.head . runSized
+head :: (HasOrdinal nat, ListLike (f a) b, (Zero nat :< n) ~ 'True) => Sized f n a -> b
+head = LL.head . runSized
 {-# INLINE head #-}
 
 -- | Take the last element of non-empty sequence.
 --   If you want to make case-analysis for general sequence,
 --   see  <#ViewsAndPatterns Views and Patterns> section.
--- 
+--
 -- Since 0.1.0.0
-last ::  ListLikeF f => Sized f (S n) a -> a
-last = givenListLikeF LL.last . runSized
+last :: (HasOrdinal nat, (Zero nat :< n) ~ 'True, ListLike (f a) b) => Sized f n a -> b
+last = LL.last . runSized
 {-# INLINE last #-}
 
 -- | Take the 'head' and 'tail' of non-empty sequence.
 --   If you want to make case-analysis for general sequence,
 --   see  <#ViewsAndPatterns Views and Patterns> section.
--- 
+--
 -- Since 0.1.0.0
-uncons :: ListLikeF f => Sized f (S n) a -> (a, Sized f n a)
-uncons = givenListLikeF (\xs -> (LL.head xs, Sized $ LL.tail xs)) . runSized
-{-# INLINE uncons #-}
+uncons :: ListLike (f a) b => Sized f (Succ n) a -> (b, Sized f n a)
+uncons = ((,) <$> LL.head <*> Sized . LL.tail) . runSized
+{-# INLINE [1] uncons #-}
+{-# RULES
+"uncons/[]" [~1] forall (x :: a) (xs:: [a]).
+  uncons (Sized (x : xs)) = (x, Sized xs)
+"uncons/Seq" [~1] forall (xs:: Seq.Seq a).
+  uncons (Sized xs) =
+    case Seq.viewl xs of { (x Seq.:< ys) -> (x, Sized ys)
+                         ; _ -> P.error "Empty seq with non-zero index!"
+                         }
+  #-}
 
+uncons' :: ListLike (f a) b => proxy n -> Sized f (Succ n) a -> (b, Sized f n a)
+uncons' _  = uncons
+{-# INLINE uncons' #-}
+
 -- | Take the 'init' and 'last' of non-empty sequence.
 --   If you want to make case-analysis for general sequence,
 --   see  <#ViewsAndPatterns Views and Patterns> section.
--- 
+--
 -- Since 0.1.0.0
-unsnoc :: ListLikeF f => Sized f (S n) a -> (Sized f n a, a)
-unsnoc = givenListLikeF (\xs -> (Sized $ LL.init xs, LL.last xs)) . runSized
-{-# INLINE unsnoc #-}
+unsnoc :: ListLike (f a) b => Sized f (Succ n) a -> (Sized f n a, b)
+unsnoc = ((,) <$> Sized . LL.init <*> LL.last) . runSized
+{-# NOINLINE [1] unsnoc #-}
+{-# RULES
+"unsnoc/Seq" [~1] forall (xs:: Seq.Seq a).
+  unsnoc (Sized xs) =
+    case Seq.viewr xs of { (ys Seq.:> x) -> (Sized ys, x)
+                         ; _ -> P.error "Empty seq with non-zero index!"
+                         }
+  #-}
 
+unsnoc' :: ListLike (f a) b => proxy n -> Sized f (Succ n) a -> (Sized f n a, b)
+unsnoc' _  = unsnoc
+{-# INLINE unsnoc' #-}
+
+
 --------------------------------------------------------------------------------
 --- Slicing
 --------------------------------------------------------------------------------
@@ -216,63 +301,63 @@
 -- | Take the tail of non-empty sequence.
 --   If you want to make case-analysis for general sequence,
 --   see  <#ViewsAndPatterns Views and Patterns> section.
--- 
+--
 -- Since 0.1.0.0
-tail :: ListLikeF f => Sized f (S n) a -> Sized f n a
-tail = givenListLikeF (Sized . LL.tail) . runSized
+tail :: (HasOrdinal nat, ListLike (f a) a)=> Sized f (Succ n) a -> Sized f (n :: nat) a
+tail = Sized . LL.tail . runSized
 {-# INLINE tail #-}
 
 -- | Take the initial segment of non-empty sequence.
 --   If you want to make case-analysis for general sequence,
 --   see  <#ViewsAndPatterns Views and Patterns> section.
--- 
+--
 -- Since 0.1.0.0
-init :: ListLikeF f => Sized f (S n) a -> Sized f n a
-init = Sized . givenListLikeF LL.init . runSized
+init :: ListLike (f a) a => Sized f (Succ n) a -> Sized f n a
+init = Sized . LL.init . runSized
 {-# INLINE init #-}
 
 -- | @take k xs@ takes first @k@ element of @xs@ where
 -- the length of @xs@ should be larger than @k@.
 -- It is really sad, that this function
 -- takes at least O(k) regardless of base container.
--- 
+--
 -- Since 0.1.0.0
-take :: (ListLikeF f, (n :<<= m) ~ True)
-     => SNat n -> Sized f m a -> Sized f n a
-take sn = Sized . givenListLikeF' (LL.take (sNatToInt sn))
+take :: (ListLike (f a) a, (n :<= m) ~ 'True, HasOrdinal nat)
+     => Sing (n :: nat) -> Sized f m a -> Sized f n a
+take sn = Sized . LL.genericTake (demote' sn) . runSized
 {-# INLINE take #-}
 
 -- | @take k xs@ takes first @k@ element of @xs@ at most.
 -- It is really sad, that this function
 -- takes at least O(k) regardless of base container.
--- 
+--
 -- Since 0.1.0.0
-takeAtMost :: (ListLikeF f)
-           => SNat n -> Sized f m a -> Sized f (Min n m) a
-takeAtMost sn = givenListLikeF' $ Sized . LL.take (sNatToInt sn)
+takeAtMost :: (ListLike (f a) a, HasOrdinal nat)
+           => Sing (n :: nat) -> Sized f m a -> Sized f (Min n m) a
+takeAtMost sn = Sized . LL.genericTake (demote $ Monomorphic sn) . runSized
 {-# INLINE takeAtMost #-}
 
 -- | @drop k xs@ drops first @k@ element of @xs@ and returns
 -- the rest of sequence, where the length of @xs@ should be larger than @k@.
 -- It is really sad, that this function
 -- takes at least O(k) regardless of base container.
--- 
+--
 -- Since 0.1.0.0
-drop :: (ListLikeF f, (n :<<= m) ~ True)
-     => SNat n -> Sized f m a -> Sized f (m :-: n) a
-drop sn = givenListLikeF' $ Sized . LL.drop (sNatToInt sn)
+drop :: (HasOrdinal nat, ListLike (f a) a, (n :<= m) ~ 'True)
+     => Sing (n :: nat) -> Sized f m a -> Sized f (m :- n) a
+drop sn = Sized . LL.genericDrop (demote' sn) . runSized
 {-# INLINE drop #-}
 
 -- | @splitAt k xs@ split @xs@ at @k@, where
 -- the length of @xs@ should be less than or equal to @k@.
 -- It is really sad, that this function
 -- takes at least O(k) regardless of base container.
--- 
+--
 -- Since 0.1.0.0
-splitAt :: (ListLikeF f , (n :<<= m) ~ True)
-        => SNat n -> Sized f m a -> (Sized f n a, Sized f (m :-: n) a)
-splitAt n = givenListLikeF' $ \xs ->
-  let (as, bs) = LL.splitAt (sNatToInt n) xs
+splitAt :: (ListLike (f a) a , (n :<= m) ~ 'True, HasOrdinal nat)
+        => Sing (n :: nat) -> Sized f m a -> (Sized f n a, Sized f (m :-. n) a)
+splitAt n (Sized xs) =
+  let (as, bs) = LL.genericSplitAt (demote' n) xs
   in (Sized as, Sized bs)
 {-# INLINE splitAt #-}
 
@@ -280,12 +365,12 @@
 --   If @k@ exceeds the length of @xs@, then the second result value become empty.
 -- It is really sad, that this function
 -- takes at least O(k) regardless of base container.
--- 
+--
 -- Since 0.1.0.0
-splitAtMost :: ListLikeF f
-            => SNat n -> Sized f m a -> (Sized f (Min n m) a, Sized f (m :-: n) a)
-splitAtMost n = givenListLikeF' $ \xs ->
-  let (as, bs) = LL.splitAt (sNatToInt n) xs
+splitAtMost :: (HasOrdinal nat, ListLike (f a) a)
+            => Sing (n :: nat) -> Sized f m a -> (Sized f (Min n m) a, Sized f (m :-. n) a)
+splitAtMost n (Sized xs) =
+  let (as, bs) = LL.genericSplitAt (demote' n) xs
   in (Sized as, Sized bs)
 {-# INLINE splitAtMost #-}
 
@@ -299,41 +384,42 @@
 --------------------------------------------------------------------------------
 
 -- | Empty sequence.
--- 
+--
 -- Since 0.1.0.0
-empty :: forall f a. ListLikeF f => Sized f Z a
-empty = withListLikeF (Proxy :: Proxy (f a)) $ Sized LL.empty
+empty :: forall f a. (HasOrdinal nat, ListLike (f a) a) => Sized f (Zero nat :: nat) a
+empty = Sized LL.empty
 {-# INLINE empty #-}
 
 -- | Sequence with one element.
--- 
+--
 -- Since 0.1.0.0
-singleton :: forall f a. ListLikeF f => a -> Sized f One a
-singleton = withListLikeF (Proxy :: Proxy (f a)) $ Sized . LL.singleton
+singleton :: forall f a. ListLike (f a) a => a -> Sized f 1 a
+singleton = Sized . LL.singleton
 {-# INLINE singleton #-}
 
 -- | Consruct the 'Sized' sequence from base type, but
 --   the length parameter is dynamically determined and
 --   existentially quantified; see also 'SomeSized'.
--- 
+--
 -- Since 0.1.0.0
-toSomeSized :: forall f a. ListLikeF f => f a -> SomeSized f a
-toSomeSized = givenListLikeF $ \xs ->
-  case promote $ LL.length xs of
+toSomeSized :: forall nat f a. (HasOrdinal nat, ListLike (f a) a)
+            => f a -> SomeSized f nat a
+toSomeSized = \xs ->
+  case promote $ LL.genericLength xs of
     Monomorphic sn -> withSingI sn $ SomeSized sn $ unsafeToSized sn xs
 
 -- | Replicates the same value.
--- 
+--
 -- Since 0.1.0.0
-replicate :: forall f n a. ListLikeF f => SNat n -> a -> Sized f n a
-replicate sn a = withListLikeF (Proxy :: Proxy (f a)) $
-                 Sized $ LL.replicate (sNatToInt sn) a
+replicate :: forall f (n :: nat) a. (HasOrdinal nat, ListLike (f a) a)
+          => Sing n -> a -> Sized f n a
+replicate sn a = Sized $ LL.genericReplicate (demote $ Monomorphic sn) a
 {-# INLINE replicate #-}
 
 -- | 'replicate' with the length inferred.
--- 
+--
 -- Since 0.1.0.0
-replicate' :: (SingI (n :: Nat), ListLikeF f) => a -> Sized f n a
+replicate' :: (HasOrdinal nat, SingI (n :: nat), ListLike (f a) a) => a -> Sized f n a
 replicate' = withSing replicate
 {-# INLINE replicate' #-}
 
@@ -342,115 +428,107 @@
 --------------------------------------------------------------------------------
 
 -- | Append an element to the head of sequence.
--- 
+--
 -- Since 0.1.0.0
-cons :: (ListLikeF f) => a -> Sized f n a -> Sized f (S n) a
-cons a = givenListLikeF' $ Sized . LL.cons a
+cons :: (ListLike (f a) b) => b -> Sized f n a -> Sized f (Succ n) a
+cons a = Sized . LL.cons a . runSized
 {-# INLINE cons #-}
 
 -- | Infix version of 'cons'.
--- 
+--
 -- Since 0.1.0.0
-(<|) :: (ListLikeF f) => a -> Sized f n a -> Sized f (S n) a
+(<|) :: (ListLike (f a) b) => b -> Sized f n a -> Sized f (Succ n) a
 (<|) = cons
 {-# INLINE (<|) #-}
 infixr 5 <|
 
 -- | Append an element to the tail of sequence.
--- 
+--
 -- Since 0.1.0.0
-snoc :: (ListLikeF f) => Sized f n a -> a -> Sized f (S n) a
-snoc (Sized xs) a = withListLikeF' xs $ Sized $ LL.snoc xs a
+snoc :: (ListLike (f a) b) => Sized f n a -> b -> Sized f (Succ n) a
+snoc (Sized xs) a = Sized $ LL.snoc xs a
 {-# INLINE snoc #-}
 
 -- | Infix version of 'snoc'.
--- 
+--
 -- Since 0.1.0.0
-(|>) :: (ListLikeF f) => Sized f n a -> a -> Sized f (S n) a
+(|>) :: (ListLike (f a) b) => Sized f n a -> b -> Sized f (Succ n) a
 (|>) = snoc
 {-# INLINE (|>) #-}
 infixl 5 |>
 
 -- | Append two lists.
--- 
+--
 -- Since 0.1.0.0
-append :: ListLikeF f => Sized f n a -> Sized f m a -> Sized f (n :+ m) a
-append (Sized xs) (Sized ys) = withListLikeF' xs $ Sized $ LL.append xs ys
+append :: ListLike (f a) a => Sized f n a -> Sized f m a -> Sized f (n :+ m) a
+append (Sized xs) (Sized ys) = Sized $ LL.append xs ys
 {-# INLINE append #-}
 
 -- | Infix version of 'append'.
--- 
+--
 -- Since 0.1.0.0
-(++) :: (ListLikeF f) => Sized f n a -> Sized f m a -> Sized f (n :+ m) a
+(++) :: (ListLike (f a) a) => Sized f n a -> Sized f m a -> Sized f (n :+ m) a
 (++) = append
 infixr 5 ++
 
 -- | Concatenates multiple sequences into one.
--- 
+--
 -- Since 0.1.0.0
-concat :: forall f f' m n a. (ListLikeF f, ListLikeF f')
+concat :: forall f f' m n a. (Functor f', Foldable f', ListLike (f a) a)
        => Sized f' m (Sized f n a) -> Sized f (m :* n) a
-concat =
-  givenListLikeF' $ withListLikeF (Proxy :: Proxy (f' (f a))) $
-  withListLikeF (Proxy :: Proxy (f a)) $
-  Sized . LL.concat . fmap runSized
+concat =  Sized . F.foldr LL.append LL.empty . P.fmap runSized
+{-# INLINE [2] concat #-}
 
+{-# RULES
+"concat/list-list" [~1] forall (xss :: [Sized [] n a]).
+  concat (Sized xss) = Sized (L.concatMap runSized xss)
+"concat/list-list" [~2] forall (xss :: (ListLike (f a) a, ListLike (f (Sized f n a)) (Sized f n a))
+                                   => f (Sized f n a)).
+  concat (Sized xss) = Sized (LL.concatMap runSized xss)
+  #-}
+
 --------------------------------------------------------------------------------
 --- Zips
 --------------------------------------------------------------------------------
 
 -- | Zipping two sequences. Length is adjusted to shorter one.
--- 
+--
 -- Since 0.1.0.0
-zip :: forall f a b n m. (ListLikeF f)
+zip :: (ListLike (f a) a, ListLike (f b) b, ListLike (f (a, b)) (a, b))
     => Sized f n a -> Sized f m b -> Sized f (Min n m) (a, b)
-zip (Sized xs) (Sized ys) =
-  withListLikeF' ys $ withListLikeF' xs $
-  withListLikeF (Proxy :: Proxy (f (a,b))) $ Sized $
-  LL.zip xs ys
+zip (Sized xs) (Sized ys) = Sized $ LL.zip xs ys
 {-# INLINE zip #-}
 
 -- | 'zip' for the sequences of the same length.
--- 
+--
 -- Since 0.1.0.0
-zipSame :: forall f n a b. (ListLikeF f)
+zipSame :: (ListLike (f a) a, ListLike (f b) b, ListLike (f (a, b)) (a, b))
         => Sized f n a -> Sized f n b -> Sized f n (a, b)
-zipSame (Sized xs) (Sized ys) =
-  withListLikeF' xs $ withListLikeF' ys $
-  withListLikeF (Proxy :: Proxy (f (a, b))) $
-  Sized $ LL.zip xs ys
+zipSame (Sized xs) (Sized ys) = Sized $ LL.zip xs ys
 {-# INLINE zipSame #-}
 
 -- | Zipping two sequences with funtion. Length is adjusted to shorter one.
--- 
+--
 -- Since 0.1.0.0
-zipWith :: forall f a b c m n. (ListLikeF f)
+zipWith :: (ListLike (f a) a, ListLike (f b) b, ListLike (f c) c)
     => (a -> b -> c) -> Sized f n a -> Sized f m b -> Sized f (Min n m) c
-zipWith f (Sized xs) (Sized ys) =
-  withListLikeF' xs $ withListLikeF' ys $
-  withListLikeF (Proxy :: Proxy (f c)) $
-  Sized $ LL.zipWith f xs ys
+zipWith f (Sized xs) (Sized ys) = Sized $ LL.zipWith f xs ys
 {-# INLINE zipWith #-}
 
 -- | 'zipWith' for the sequences of the same length.
--- 
+--
 -- Since 0.1.0.0
-zipWithSame :: forall f a b c n. ListLikeF f
+zipWithSame :: (ListLike (f a) a, ListLike (f b) b, ListLike (f c) c)
             => (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c
-zipWithSame f (Sized xs) (Sized ys) =
-  withListLikeF' xs $ withListLikeF' ys $
-  withListLikeF (Proxy :: Proxy (f c)) $
-  Sized $ LL.zipWith f xs ys
+zipWithSame f (Sized xs) (Sized ys) = Sized $ LL.zipWith f xs ys
 {-# INLINE zipWithSame #-}
 
 -- | Unzipping the sequence of tuples.
--- 
+--
 -- Since 0.1.0.0
-unzip :: forall f n a b. (ListLikeF f)
+unzip :: (ListLike (f a) a, ListLike (f b) b, ListLike (f (a, b)) (a,b))
       => Sized f n (a, b) -> (Sized f n a, Sized f n b)
-unzip (Sized xys) = withListLikeF' xys $
-  withListLikeF (Proxy :: Proxy (f b)) $
-  withListLikeF (Proxy :: Proxy (f a)) $
+unzip (Sized xys) =
   let (xs, ys) = LL.unzip xys
   in (Sized xs, Sized ys)
 {-# INLINE unzip #-}
@@ -461,56 +539,60 @@
 --------------------------------------------------------------------------------
 
 -- | Map function.
--- 
+--
 -- Since 0.1.0.0
-map :: Functor f => (a -> b) -> Sized f n a -> Sized f n b
-map f = Sized . fmap f . runSized
+map :: (ListLike (f a) a, ListLike (f b) b) => (a -> b) -> Sized f n a -> Sized f n b
+map f = Sized . LL.map f . runSized
 {-# INLINE map #-}
 
+fmap :: forall f n a b. Functor f => (a -> b) -> Sized f n a -> Sized f n b
+fmap f = Sized . P.fmap f . runSized
+{-# INLINE fmap #-}
+
 -- | Reverse function.
--- 
+--
 -- Since 0.1.0.0
-reverse :: ListLikeF f => Sized f n a -> Sized f n a
-reverse = Sized . givenListLikeF LL.reverse . runSized
+reverse :: ListLike (f a) a => Sized f n a -> Sized f n a
+reverse = Sized .  LL.reverse . runSized
 {-# INLINE reverse #-}
 
 -- | Intersperces.
--- 
+--
 -- Since 0.1.0.0
-intersperse :: ListLikeF f => a -> Sized f n a -> Sized f ((Two :* n) :-: One) a
-intersperse a = Sized . givenListLikeF' (LL.intersperse a)
+intersperse :: ListLike (f a) a => a -> Sized f n a -> Sized f ((FromInteger 2 :* n) :-. 1) a
+intersperse a = Sized . LL.intersperse a . runSized
 {-# INLINE intersperse #-}
 
 -- | Remove all duplicates.
--- 
+--
 -- Since 0.1.0.0
-nub :: (ListLikeF f, Eq a) => Sized f n a -> SomeSized f a
-nub = givenListLikeF' $ toSomeSized . LL.nub
+nub :: (HasOrdinal nat, ListLike (f a) a, Eq a) => Sized f n a -> SomeSized f nat a
+nub = toSomeSized . LL.nub . runSized
 
 -- | Sorting sequence by ascending order.
--- 
+--
 -- Since 0.1.0.0
-sort :: (ListLikeF f, Ord a)
+sort :: (ListLike (f a) a, Ord a)
      => Sized f n a -> Sized f n a
-sort = givenListLikeF' $ Sized . LL.sort
+sort = Sized . LL.sort . runSized
 
 -- | Generalized version of 'sort'.
--- 
+--
 -- Since 0.1.0.0
-sortBy :: (ListLikeF  f) => (a -> a -> Ordering) -> Sized f n a -> Sized f n a
-sortBy cmp = givenListLikeF' $ Sized . LL.sortBy cmp
+sortBy :: (ListLike (f a) a) => (a -> a -> Ordering) -> Sized f n a -> Sized f n a
+sortBy cmp = Sized . LL.sortBy cmp . runSized
 
 -- | Insert new element into the presorted sequence.
--- 
+--
 -- Since 0.1.0.0
-insert :: (ListLikeF f, Ord a) => a -> Sized f n a -> Sized f (S n) a
-insert a = givenListLikeF' $ Sized . LL.insert a
+insert :: (ListLike (f a) a, Ord a) => a -> Sized f n a -> Sized f (Succ n) a
+insert a = Sized . LL.insert a . runSized
 
 -- | Generalized version of 'insert'.
--- 
+--
 -- Since 0.1.0.0
-insertBy :: (ListLikeF f) => (a -> a -> Ordering) -> a -> Sized f n a -> Sized f (S n) a
-insertBy cmp a = givenListLikeF' $ Sized . LL.insertBy cmp a
+insertBy :: (ListLike (f a) a) => (a -> a -> Ordering) -> a -> Sized f n a -> Sized f (Succ n) a
+insertBy cmp a = Sized . LL.insertBy cmp a . runSized
 
 
 --------------------------------------------------------------------------------
@@ -522,80 +604,68 @@
 --------------------------------------------------------------------------------
 
 -- | Convert to list.
--- 
+--
 -- Since 0.1.0.0
-toList :: ListLikeF f => Sized f n a -> [a]
-toList = givenListLikeF LL.toList . runSized
+toList :: ListLike (f a) a => Sized f n a -> [a]
+toList = LL.toList . runSized
 {-# INLINE [2] toList #-}
 
 {-# RULES
 "toList/" forall (xs :: Sized [] a n).
-  toList xs = runSized xs
+  Data.Sized.toList xs = runSized xs
   #-}
 
 -- | If the given list is shorter than @n@, then returns @Nothing@
 --   Otherwise returns @Sized f n a@ consisting of initial @n@ element
 --   of given list.
--- 
+--
 -- Since 0.1.0.0
-fromList :: forall f n a. ListLikeF f => SNat n -> [a] -> Maybe (Sized f n a)
-fromList SZ _ = withListLikeF (Proxy :: Proxy (f a)) $
-                Just $ Sized (LL.empty :: f a)
+fromList :: forall f n a. (HasOrdinal nat, ListLike (f a) a)
+         => Sing (n :: nat) -> [a] -> Maybe (Sized f n a)
+fromList Zero _ = Just $ Sized (LL.empty :: f a)
 fromList sn xs =
-  let len = sNatToInt sn
+  let len = P.fromIntegral $ demote $ Monomorphic sn
   in if P.length xs < len
      then Nothing
      else Just $ unsafeFromList sn $ P.take len xs
 {-# INLINABLE [2] fromList #-}
 
-{-# RULES
-"fromList/List" forall sn (xs :: [a]).
-  fromList sn xs = toSized sn xs
-  #-}
-
 -- | 'fromList' with the result length inferred.
--- 
+--
 -- Since 0.1.0.0
-fromList' :: (ListLikeF f, SingI (n :: Nat)) => [a] -> Maybe (Sized f n a)
+fromList' :: (ListLike (f a) a, SingI (n :: TL.Nat)) => [a] -> Maybe (Sized f n a)
 fromList' = withSing fromList
 {-# INLINE fromList' #-}
 
--- | Unsafe version of 'fromList'. If the length of the given list does not 
+-- | Unsafe version of 'fromList'. If the length of the given list does not
 --   equal to @n@, then something unusual happens.
--- 
+--
 -- Since 0.1.0.0
-unsafeFromList :: forall f n a. ListLikeF f => SNat n -> [a] -> Sized f n a
-unsafeFromList _ xs =
-  withListLikeF (Proxy :: Proxy (f a)) $
-  Sized $ LL.fromList xs
+unsafeFromList :: forall f n a. ListLike (f a) a => Sing n -> [a] -> Sized f n a
+unsafeFromList _ xs = Sized $ LL.fromList xs
 {-# INLINE [2] unsafeFromList #-}
 
-{-# RULES
-"unsafeFromList/List" forall sn (xs :: [a]).
-  unsafeFromList sn xs = Sized (P.take (sNatToInt sn) xs)
- #-}
-
 -- | 'unsafeFromList' with the result length inferred.
--- 
+--
 -- Since 0.1.0.0
-unsafeFromList' :: (SingI (n :: Nat), ListLikeF f) => [a] -> Sized f n a
+unsafeFromList' :: (SingI (n :: TL.Nat), ListLike (f a) a) => [a] -> Sized f n a
 unsafeFromList' = withSing unsafeFromList
 {-# INLINE unsafeFromList' #-}
 
 -- | Construct a @Sized f n a@ by padding default value if the given list is short.
--- 
+--
 -- Since 0.1.0.0
-fromListWithDefault :: forall f n a. ListLikeF f => SNat n -> a -> [a] -> Sized f n a
+fromListWithDefault :: forall f (n :: nat) a. (HasOrdinal nat, ListLike (f a) a)
+                    => Sing n -> a -> [a] -> Sized f n a
 fromListWithDefault sn def xs =
-  let len = sNatToInt sn
-  in withListLikeF (Proxy :: Proxy (f a)) $
-     Sized $ LL.fromList (P.take len xs) `LL.append` LL.replicate (len - P.length xs) def
+  let len = demote' sn
+  in Sized $ LL.fromList (L.genericTake len xs) `LL.append` LL.genericReplicate (len - L.genericLength xs) def
 {-# INLINABLE fromListWithDefault #-}
 
 -- | 'fromListWithDefault' with the result length inferred.
--- 
+--
 -- Since 0.1.0.0
-fromListWithDefault' :: (SingI (n :: Nat), ListLikeF f) => a -> [a] -> Sized f n a
+fromListWithDefault' :: (SingI (n :: TL.Nat), ListLike (f a) a) => a -> [a] -> Sized f n a
 fromListWithDefault' = withSing fromListWithDefault
 {-# INLINE fromListWithDefault' #-}
 
@@ -604,7 +674,7 @@
 --------------------------------------------------------------------------------
 
 -- | Forget the length and obtain the wrapped base container.
--- 
+--
 -- Since 0.1.0.0
 unsized :: Sized f n a -> f a
 unsized = runSized
@@ -613,51 +683,53 @@
 -- | If the length of the input is shorter than @n@, then returns @Nothing@.
 --   Otherwise returns @Sized f n a@ consisting of initial @n@ element
 --   of the input.
--- 
+--
 -- Since 0.1.0.0
-toSized :: ListLikeF f => SNat n -> f a -> Maybe (Sized f n a)
-toSized sn = givenListLikeF $ \xs ->
-  let len = sNatToInt sn
-  in if LL.length xs < len
+toSized :: (HasOrdinal nat, ListLike (f a) a)
+        => Sing (n :: nat) -> f a -> Maybe (Sized f n a)
+toSized sn xs =
+  let len = demote' sn
+  in if LL.genericLength xs < len
      then Nothing
-     else Just $ unsafeToSized sn $ LL.take len xs
+     else Just $ unsafeToSized sn $ LL.genericTake len xs
 {-# INLINABLE [2] toSized #-}
 
 -- | 'toSized' with the result length inferred.
--- 
+--
 -- Since 0.1.0.0
-toSized' :: (ListLikeF f, SingI (n :: Nat)) => f a -> Maybe (Sized f n a)
+toSized' :: (ListLike (f a) a, SingI (n :: TL.Nat)) => f a -> Maybe (Sized f n a)
 toSized' = withSing toSized
 {-# INLINE toSized' #-}
 
--- | Unsafe version of 'toSized'. If the length of the given list does not 
+-- | Unsafe version of 'toSized'. If the length of the given list does not
 --   equal to @n@, then something unusual happens.
--- 
+--
 -- Since 0.1.0.0
-unsafeToSized :: SNat n -> f a -> Sized f n a
+unsafeToSized :: Sing n -> f a -> Sized f n a
 unsafeToSized _ = Sized
 {-# INLINE [2] unsafeToSized #-}
 
 -- | 'unsafeToSized' with the result length inferred.
--- 
+--
 -- Since 0.1.0.0
-unsafeToSized' :: (SingI (n :: Nat), ListLikeF f) => f a -> Sized f n a
+unsafeToSized' :: (SingI (n :: TL.Nat), ListLike (f a) a) => f a -> Sized f n a
 unsafeToSized' = withSing unsafeToSized
 {-# INLINE unsafeToSized' #-}
 
 -- | Construct a @Sized f n a@ by padding default value if the given list is short.
--- 
+--
 -- Since 0.1.0.0
-toSizedWithDefault :: ListLikeF f => SNat n -> a -> f a -> Sized f n a
-toSizedWithDefault sn def = givenListLikeF $ \xs ->
-  let len = sNatToInt sn
+toSizedWithDefault :: (HasOrdinal nat, ListLike (f a) a)
+                   => Sing (n :: nat) -> a -> f a -> Sized f n a
+toSizedWithDefault sn def xs =
+  let len = P.fromIntegral $ demote (Monomorphic sn)
   in Sized $ LL.take len xs `LL.append` LL.replicate (len - LL.length xs) def
 {-# INLINABLE toSizedWithDefault #-}
 
 -- | 'toSizedWithDefault' with the result length inferred.
--- 
+--
 -- Since 0.1.0.0
-toSizedWithDefault' :: (SingI (n :: Nat), ListLikeF f) => a -> f a -> Sized f n a
+toSizedWithDefault' :: (SingI (n :: TL.Nat), ListLike (f a) a) => a -> f a -> Sized f n a
 toSizedWithDefault' = withSing toSizedWithDefault
 {-# INLINE toSizedWithDefault' #-}
 
@@ -672,76 +744,76 @@
 
 -- | The type @Partitioned f n a@ represents partitioned sequence of length @n@.
 --   Value @Partitioned lenL ls lenR rs@ stands for:
--- 
+--
 --   * Entire sequence is divided into @ls@ and @rs@, and their length
 --     are @lenL@ and @lenR@ resp.
--- 
+--
 --   * @lenL + lenR = n@
 --
 -- Since 0.1.0.0
 data Partitioned f n a where
-  Partitioned :: (ListLikeF f, SingI n, SingI m)
-              => SNat n
-              -> Sized f (n :: Nat) a
-              -> SNat m
-              -> Sized f (m :: Nat) a
+  Partitioned :: (ListLike (f a) a)
+              => Sing n
+              -> Sized f (n :: TL.Nat) a
+              -> Sing m
+              -> Sized f (m :: TL.Nat) a
               -> Partitioned f (n :+ m) a
 
 -- | Take the initial segment as long as elements satisfys the predicate.
--- 
+--
 -- Since 0.1.0.0
-takeWhile :: ListLikeF f
-          => (a -> Bool) -> Sized f n a -> SomeSized f a
-takeWhile p = givenListLikeF' $ toSomeSized . LL.takeWhile p
+takeWhile :: (HasOrdinal nat, ListLike (f a) a)
+          => (a -> Bool) -> Sized f n a -> SomeSized f nat a
+takeWhile p = toSomeSized . LL.takeWhile p . runSized
 {-# INLINE takeWhile #-}
 
 -- | Drop the initial segment as long as elements satisfys the predicate.
--- 
+--
 -- Since 0.1.0.0
-dropWhile :: ListLikeF f
-          => (a -> Bool) -> Sized f n a -> SomeSized f a
-dropWhile p = givenListLikeF' $ toSomeSized . LL.dropWhile p
+dropWhile :: (HasOrdinal nat, ListLike (f a) a)
+          => (a -> Bool) -> Sized f n a -> SomeSized f nat a
+dropWhile p = toSomeSized . LL.dropWhile p . runSized
 {-# INLINE dropWhile #-}
 
 -- | Invariant: @'ListLike' (f a) a@ instance must be implemented
 -- to satisfy the following property:
 -- @length (fst (span p xs)) + length (snd (span p xs)) == length xs@
 -- Otherwise, this function introduces severe contradiction.
--- 
+--
 -- Since 0.1.0.0
-span :: ListLikeF f
+span :: ListLike (f a) a
      => (a -> Bool) -> Sized f n a -> Partitioned f n a
-span p = givenListLikeF' $ \xs ->
-         let (as, bs) = LL.span p xs
-         in case (toSomeSized as, toSomeSized bs) of
-           (SomeSized lenL ls, SomeSized lenR rs) ->
-             unsafeCoerce $ Partitioned lenL ls lenR rs
+span p xs =
+  let (as, bs) = LL.span p $ runSized xs
+  in case (toSomeSized as, toSomeSized bs) of
+    (SomeSized lenL ls, SomeSized lenR rs) ->
+      unsafeCoerce $ Partitioned lenL ls lenR rs
 {-# INLINE span #-}
 
 -- | Invariant: @'ListLike' (f a) a@ instance must be implemented
 -- to satisfy the following property:
 -- @length (fst (break p xs)) + length (snd (break p xs)) == length xs@
 -- Otherwise, this function introduces severe contradiction.
--- 
+--
 -- Since 0.1.0.0
-break :: ListLikeF f
+break :: ListLike (f a) a
      => (a -> Bool) -> Sized f n a -> Partitioned f n a
-break p = givenListLikeF' $ \xs ->
-         let (as, bs) = LL.break p xs
-         in case (toSomeSized as, toSomeSized bs) of
-           (SomeSized lenL ls, SomeSized lenR rs) ->
-             unsafeCoerce $ Partitioned lenL ls lenR rs
+break p (Sized xs) =
+  let (as, bs) = LL.break p xs
+  in case (toSomeSized as, toSomeSized bs) of
+    (SomeSized lenL ls, SomeSized lenR rs) ->
+      unsafeCoerce $ Partitioned lenL ls lenR rs
 {-# INLINE break #-}
 
 -- | Invariant: @'ListLike' (f a) a@ instance must be implemented
 -- to satisfy the following property:
 -- @length (fst (partition p xs)) + length (snd (partition p xs)) == length xs@
 -- Otherwise, this function introduces severe contradiction.
--- 
+--
 -- Since 0.1.0.0
-partition :: ListLikeF f
+partition :: ListLike (f a) a
      => (a -> Bool) -> Sized f n a -> Partitioned f n a
-partition p = givenListLikeF' $ \xs ->
+partition p (Sized xs) =
          let (as, bs) = LL.partition p xs
          in case (toSomeSized as, toSomeSized bs) of
            (SomeSized lenL ls, SomeSized lenR rs) ->
@@ -752,82 +824,170 @@
 --- Searching
 --------------------------------------------------------------------------------
 -- | Membership test; see also 'notElem'.
--- 
+--
 -- Since 0.1.0.0
-elem :: (ListLikeF f, Eq a) => a -> Sized f n a -> Bool
-elem a = givenListLikeF' $ LL.elem a
+elem :: (ListLike (f a) a, Eq a) => a -> Sized f n a -> Bool
+elem a = LL.elem a . runSized
 {-# INLINE elem #-}
 
 -- | Negation of 'elem'.
--- 
+--
 -- Since 0.1.0.0
-notElem :: (ListLikeF f, Eq a) => a -> Sized f n a -> Bool
-notElem a = givenListLikeF' $ LL.notElem a
+notElem :: (ListLike (f a) a, Eq a) => a -> Sized f n a -> Bool
+notElem a = LL.notElem a . runSized
 {-# INLINE notElem #-}
 
 -- | Find the element satisfying the predicate.
--- 
+--
 -- Since 0.1.0.0
-find :: ListLikeF f => (a -> Bool) -> Sized f n a -> Maybe a
-find p = givenListLikeF' $ LL.find p
-{-# INLINE find #-}
+find :: Foldable f => (a -> Bool) -> Sized f n a -> Maybe a
+find p = F.find p
+{-# INLINE[1] find #-}
+{-# RULES
+"find/List" [~1] forall p (xs :: [a]).
+  find p (Sized xs) = L.find p xs
+"find/Vector" [~1] forall p xs.
+  find p (Sized xs) = V.find p xs
+"find/Storable Vector" [~1] forall p (xs :: SV.Storable a => SV.Vector a).
+  find p (Sized xs) = SV.find p xs
+"find/Unboxed Vector" [~1] forall p (xs :: UV.Unbox a => UV.Vector a).
+  find p (Sized xs) = UV.find p xs
+  #-}
 
+-- | @'Foldable'@ version of @'find'@.
+findF :: (Foldable f) => (a -> Bool) -> Sized f n a -> Maybe a
+findF p = getFirst. F.foldMap (\a -> if p a then First (Just a) else First Nothing) . runSized
+{-# INLINE [1] findF #-}
+{-# SPECIALISE [0] findF :: (a -> Bool) -> Sized Seq.Seq n a -> Maybe a #-}
+{-# RULES
+"findF/list" [~1] forall p.
+  findF p = L.find p
+  #-}
+
 -- | @'findIndex' p xs@ find the element satisfying @p@ and returns its index if exists.
--- 
+--
 -- Since 0.1.0.0
-findIndex :: ListLikeF f => (a -> Bool) -> Sized f n a -> Maybe Int
-findIndex p = givenListLikeF' $ LL.findIndex p
+findIndex :: ListLike (f a) a => (a -> Bool) -> Sized f n a -> Maybe Int
+findIndex p = LL.findIndex p . runSized
 {-# INLINE findIndex #-}
 
 -- | 'Ordinal' version of 'findIndex'.
--- 
+--
 -- Since 0.1.0.0
-sFindIndex :: (SingI n, ListLikeF f) => (a -> Bool) -> Sized f n a -> Maybe (Ordinal n)
-sFindIndex p = fmap toEnum . findIndex p
+sFindIndex :: (SingI (n :: nat), ListLike (f a) a, HasOrdinal nat)
+           => (a -> Bool) -> Sized f n a -> Maybe (Ordinal n)
+sFindIndex p = P.fmap toEnum . findIndex p
 {-# INLINE sFindIndex #-}
 
+-- | @'findIndex'@ implemented in terms of @'FoldableWithIndex'@
+findIndexIF :: (FoldableWithIndex i f) => (a -> Bool) -> Sized f n a -> Maybe i
+findIndexIF p = P.fmap fst . ifind (P.const p) . runSized
+{-# INLINE [1] findIndexIF #-}
+{-# RULES
+"findIndexIF/list" [~1] forall p.
+  findIndexIF p = L.findIndex p . runSized
+"findIndexIF/vector" [~1] forall p.
+  findIndexIF p = V.findIndex p . runSized
+  #-}
+
+-- | @'sFindIndex'@ implemented in terms of @'FoldableWithIndex'@
+sFindIndexIF :: (FoldableWithIndex i f, P.Integral i, HasOrdinal nat, SingI n)
+             => (a -> Bool) -> Sized f (n :: nat) a -> Maybe (Ordinal n)
+sFindIndexIF p = P.fmap fst . ifind (P.const p)
+{-# INLINE [1] sFindIndexIF #-}
+-- {-# RULES
+-- "sFindIndexIF/list" [~1] forall p .
+--   sFindIndexIF p = P.fmap toEnum . L.findIndex p . runSized
+-- "sFindIndexIF/vector" [~1] forall p.
+--   sFindIndexIF p = P.fmap toEnum . V.findIndex p . runSized
+--   #-}
+
 -- | @'findIndices' p xs@ find all elements satisfying @p@ and returns their indices.
--- 
+--
 -- Since 0.1.0.0
-findIndices :: ListLikeF f => (a -> Bool) -> Sized f n a -> [Int]
-findIndices p = givenListLikeF' $ LL.findIndices p
+findIndices :: ListLike (f a) a => (a -> Bool) -> Sized f n a -> [Int]
+findIndices p = LL.findIndices p . runSized
 {-# INLINE findIndices #-}
+{-# SPECIALISE findIndices :: (a -> Bool) -> Sized [] n a -> [Int] #-}
 
+-- | @'findIndices'@ implemented in terms of @'FoldableWithIndex'@
+findIndicesIF :: (FoldableWithIndex i f) => (a -> Bool) -> Sized f n a -> [i]
+findIndicesIF p = flip appEndo [] . ifoldMap (\i x -> if p x then Endo (i:) else Endo P.id) . runSized
+{-# INLINE [1] findIndicesIF #-}
+{-# RULES
+"findIndicesIF/list" [~1] forall p.
+  findIndicesIF p = L.findIndices p . runSized
+"findIndicesIF/vector" [~1] forall p.
+  findIndicesIF p = V.toList . V.findIndices p . runSized
+  #-}
+
+
 -- | 'Ordinal' version of 'findIndices'.
--- 
+--
 -- Since 0.1.0.0
-sFindIndices :: (SingI n, ListLikeF f) => (a -> Bool) -> Sized f n a -> [Ordinal n]
-sFindIndices p = fmap toEnum . findIndices p
+sFindIndices :: (HasOrdinal nat, SingI (n :: nat), ListLike (f a) a)
+             => (a -> Bool) -> Sized f n a -> [Ordinal n]
+sFindIndices p = P.fmap (toEnum . P.fromIntegral) . findIndices p
 {-# INLINE sFindIndices #-}
 
+sFindIndicesIF :: (FoldableWithIndex i f, P.Integral i, HasOrdinal nat, SingI n)
+               => (a -> Bool) -> Sized f (n :: nat) a -> [Ordinal n]
+sFindIndicesIF p = flip appEndo [] .
+                   ifoldMap (\i x -> if p x then Endo (P.toEnum (P.fromIntegral i):) else Endo P.id) .
+                   runSized
+{-# INLINE [1] sFindIndicesIF #-}
+-- {-# RULES
+-- "sFindIndicesIF/list" [~1] forall p.
+--   sFindIndicesIF p = P.map toEnum . L.findIndices p . runSized
+-- "sFindIndicesIF/vector" [~1] forall p.
+--   sFindIndicesIF p = V.toList . V.map toEnum . V.findIndices p . runSized
+--   #-}
+
 -- | Returns the index of the given element in the list, if exists.
--- 
+--
 -- Since 0.1.0.0
-elemIndex :: (Eq a, ListLikeF f) => a -> Sized f n a -> Maybe Int
-elemIndex a = findIndex (== a)
+elemIndex :: (Eq a, ListLike (f a) a) => a -> Sized f n a -> Maybe Int
+elemIndex a (Sized xs) = LL.elemIndex a xs
 {-# INLINE elemIndex #-}
 
 -- | Ordinal version of 'elemIndex'
--- 
--- Since 0.1.0.0
-sElemIndex :: (SingI n, ListLikeF f, Eq a)
+--   It statically checks boundary invariants.
+--   If you don't internal structure on @'Sized'@,
+--   then @'sUnsafeElemIndex'@ is much faster and
+--   also safe for most cases.
+--
+--   Since 0.1.0.0
+sElemIndex :: forall (n :: nat) f a.
+              (SingI n, ListLike (f a) a, Eq a, HasOrdinal nat)
            => a -> Sized f n a -> Maybe (Ordinal n)
-sElemIndex a = sFindIndex (== a)
+sElemIndex a (Sized xs) = do
+  i <- LL.elemIndex a xs
+  case promote (P.fromIntegral i) of
+    Monomorphic sn ->
+      case sn %:< (sing :: Sing n) of
+        STrue  -> Just (OLt sn)
+        SFalse -> Nothing
 {-# INLINE sElemIndex #-}
 
+sUnsafeElemIndex :: forall (n :: nat) f a.
+                    (SingI n, ListLike (f a) a, Eq a, HasOrdinal nat)
+                 => a -> Sized f n a -> Maybe (Ordinal n)
+sUnsafeElemIndex a (Sized xs) =
+  unsafeFromInt . P.fromIntegral <$> LL.elemIndex a xs
 
 -- | Returns all indices of the given element in the list.
--- 
+--
 -- Since 0.1.0.0
-elemIndices :: (ListLikeF f, Eq a) => a -> Sized f n a -> [Int]
-elemIndices a = givenListLikeF' $ LL.elemIndices a
+elemIndices :: (ListLike (f a) a, Eq a) => a -> Sized f n a -> [Int]
+elemIndices a = LL.elemIndices a . runSized
 {-# INLINE elemIndices #-}
 
 -- | Ordinal version of 'elemIndices'
--- 
+--
 -- Since 0.1.0.0
-sElemIndices :: (SingI n, ListLikeF f, Eq a) => a -> Sized f n a -> [Ordinal n]
-sElemIndices p = fmap toEnum . elemIndices p
+sElemIndices :: (HasOrdinal nat, SingI (n :: nat), ListLike (f a) a, Eq a)
+             => a -> Sized f n a -> [Ordinal n]
+sElemIndices p = P.fmap (unsafeFromInt . P.fromIntegral) . elemIndices p
 {-# INLINE sElemIndices #-}
 
 --------------------------------------------------------------------------------
@@ -847,64 +1007,65 @@
 {-$views #views#
 
    With @ViewPatterns@ extension, we can pattern-match on 'Sized' value as follows:
-   
+
 @
-slen :: ('SingI' n, 'ListLikeF' f) => 'Sized' f n a -> 'SNat' n
+slen :: ('SingI' n, 'ListLike (f a) a' f) => 'Sized' f n a -> 'Sing' n
 slen ('viewCons' -> 'NilCV')    = 'SZ'
 slen ('viewCons' -> _ '::-' as) = 'SS' (slen as)
 slen _                          = error "impossible"
 @
-   
-   The constraint @('SingI' n, 'ListLikeF' f)@ is needed for view function.
+
+   The constraint @('SingI' n, 'ListLike (f a) a' f)@ is needed for view function.
    In the above, we have extra wildcard pattern (@_@) at the last.
    Code compiles if we removed it, but current GHC warns for incomplete pattern,
    although we know first two patterns exhausts all the case.
-   
+
    Equivalently, we can use snoc-style pattern-matching:
-   
+
 @
-slen :: ('SingI' n, 'ListLikeF' f) => 'Sized' f n a -> 'SNat' n
+slen :: ('SingI' n, 'ListLike (f a) a' f) => 'Sized' f n a -> 'Sing' n
 slen ('viewSnoc' -> 'NilSV')     = 'SZ'
 slen ('viewSnoc' -> as ':-::' _) = 'SS' (slen as)
 @
 -}
 
 -- | View of the left end of sequence (cons-side).
--- 
+--
 -- Since 0.1.0.0
 data ConsView f n a where
-  NilCV :: ConsView f Z a
-  (::-) :: SingI n => a -> Sized f n a -> ConsView f (S n) a
+  NilCV :: ConsView f (Zero nat) a
+  (::-) :: SingI n => a -> Sized f n a -> ConsView f (Succ n) a
 
 infixr 5 ::-
 
 -- | Case analysis for the cons-side of sequence.
--- 
+--
 -- Since 0.1.0.0
-viewCons :: forall f a n. (SingI n, ListLikeF f)
+viewCons :: forall f a (n :: nat). (HasOrdinal nat, ListLike (f a) a)
          => Sized f n a
          -> ConsView f n a
-viewCons sz = case sing :: SNat n of
-  SZ    -> NilCV
-  SS n' -> withSingI n' $ head sz ::- tail sz
+viewCons sz = case zeroOrSucc (sLength sz) of
+  IsZero   -> NilCV
+  IsSucc n' -> withSingI n' $ P.uncurry (::-) (uncons' n' sz)
 
 -- | View of the left end of sequence (snoc-side).
--- 
+--
 -- Since 0.1.0.0
 data SnocView f n a where
-  NilSV :: SnocView f Z a
-  (:-::) :: SingI n => Sized f n a -> a -> SnocView f (S n) a
+  NilSV :: SnocView f (Zero nat) a
+  (:-::) :: SingI n => Sized f n a -> a -> SnocView f (Succ n) a
 infixl 5 :-::
 
 -- | Case analysis for the snoc-side of sequence.
--- 
+--
 -- Since 0.1.0.0
-viewSnoc :: forall f n a. (SingI n, ListLikeF f)
+viewSnoc :: forall f (n :: nat) a. (HasOrdinal nat, ListLike (f a) a)
          => Sized f n a
          -> SnocView f n a
-viewSnoc sz = case sing :: SNat n of
-  SZ   -> NilSV
-  SS n -> withSingI n $ init sz :-:: last sz
+viewSnoc sz = case zeroOrSucc (sLength sz) of
+  IsZero   -> NilSV
+  IsSucc n' ->
+    withSingI n' $ P.uncurry (:-::) (unsnoc' n' sz)
 
 {-$patterns #patterns#
 
@@ -912,27 +1073,27 @@
    it is rather clumsy to nest it. For example:
 
 @
-nextToHead :: ('ListLikeF' f, 'SingI' n) => 'Sized' f ('S' ('S' n)) a -> a
+nextToHead :: ('ListLike (f a) a' f, 'SingI' n) => 'Sized' f ('S' ('S' n)) a -> a
 nextToHead ('viewCons' -> _ '::-' ('viewCons' -> a '::-' _)) = a
 @
 
    In such a case, with @PatternSynonyms@ extension we can write as follows:
 
 @
-nextToHead :: ('ListLikeF' f, 'SingI' n) => 'Sized' f ('S' ('S' n)) a -> a
+nextToHead :: ('ListLike (f a) a' f, 'SingI' n) => 'Sized' f ('S' ('S' n)) a -> a
 nextToHead (_ ':<' a ':<' _) = a
 @
 
    Of course, we can also rewrite above @slen@ example using @PatternSynonyms@:
 
 @
-slen :: ('SingI' n, 'ListLikeF' f) => 'Sized' f n a -> 'SNat' n
+slen :: ('SingI' n, 'ListLike (f a) a' f) => 'Sized' f n a -> 'Sing' n
 slen 'NilL'      = 'SZ'
 slen (_ ':<' as) = 'SS' (slen as)
 slen _           = error "impossible"
 @
 
-   So, we can use @':<'@ and @'NilL'@ (resp. @':>'@ and @'NilR'@) to 
+   So, we can use @':<'@ and @'NilL'@ (resp. @':>'@ and @'NilR'@) to
    pattern-match directly on cons-side (resp. snoc-side) as we usually do for lists.
    @':<'@, @'NilL'@, @':>'@ and @'NilR'@ are neither functions nor data constructors,
    but pattern synonyms so we cannot use them in expression contexts.
@@ -944,9 +1105,51 @@
 
 infixr 5 :<
 -- | Pattern synonym for cons-side uncons.
-pattern a :< b <- (viewCons -> a ::- b)
-pattern NilL   <- (viewCons -> NilCV)
+pattern (:<) :: forall nat f (n :: nat) a.
+                (ListLike (f a) a, HasOrdinal nat)
+             => forall (n1 :: nat).
+                (n ~ Succ n1, SingI n1)
+             => a -> Sized f n1 a -> Sized f n a
+pattern a :< as <- (viewCons -> a ::- as) where
+   a :< as = a <| as
 
+pattern NilL :: forall nat f (n :: nat) a.
+                (ListLike (f a) a,  HasOrdinal nat)
+             => (n ~ Zero nat) => Sized f n a
+pattern NilL   <- (viewCons -> NilCV) where
+  NilL = empty
+
 infixl 5 :>
-pattern a :> b <- (viewSnoc -> a :-:: b)
-pattern NilR   <- (viewSnoc -> NilSV)
+
+pattern (:>) :: forall nat f (n :: nat) a.
+                (ListLike (f a) a, HasOrdinal nat)
+             => forall (n1 :: nat).
+                (n ~ Succ n1, SingI n1)
+             => Sized f n1 a -> a -> Sized f n a
+pattern a :> b <- (viewSnoc -> a :-:: b) where
+  a :> b = a |> b
+
+pattern NilR :: forall nat f (n :: nat) a.
+                (ListLike (f a) a,  HasOrdinal nat)
+             => n ~ Zero nat => Sized f n a
+pattern NilR   <- (viewSnoc -> NilSV) where
+  NilR = empty
+
+-- | Applicative instance, generalizing @'Data.Monoid.ZipList'@.
+instance (Functor f, HasOrdinal nat, SingI n, ListLikeF f)
+      => P.Applicative (Sized f (n :: nat)) where
+  {-# SPECIALISE instance TL.KnownNat n => P.Applicative (Sized [] (n :: TL.Nat)) #-}
+  {-# SPECIALISE instance TL.KnownNat n => P.Applicative (Sized Seq.Seq (n :: TL.Nat)) #-}
+  {-# SPECIALISE instance TL.KnownNat n => P.Applicative (Sized V.Vector (n :: TL.Nat)) #-}
+
+  pure (x :: a) =
+    withListLikeF (Nothing :: Maybe (f a)) $
+    replicate' x
+  {-# INLINE pure #-}
+
+  Sized (fs :: f (a -> b)) <*> Sized (xs :: f a) =
+    withListLikeF (Nothing :: Maybe (f (a -> b))) $
+    withListLikeF (Nothing :: Maybe (f a)) $
+    withListLikeF (Nothing :: Maybe (f b)) $
+    Sized $ LL.zipWith ($) fs xs
+  {-# INLINE (<*>) #-}
diff --git a/Data/Sized/Builtin.hs b/Data/Sized/Builtin.hs
new file mode 100644
--- /dev/null
+++ b/Data/Sized/Builtin.hs
@@ -0,0 +1,45 @@
+{-# LANGUAGE DataKinds, GADTs, KindSignatures, MultiParamTypeClasses #-}
+{-# LANGUAGE PatternSynonyms, PolyKinds, RankNTypes, TypeInType      #-}
+{-# LANGUAGE ViewPatterns                                            #-}
+-- | This module exports @'S.Sized'@ type specialized to
+--   GHC's built-in type numeral @'TL.Nat'@.
+module Data.Sized.Builtin
+       (Ordinal, Sized, module Data.Sized,
+        pattern (:<), pattern NilL, pattern (:>), pattern NilR) where
+import           Data.Sized hiding ((:<), (:>), NilL, NilR, Sized)
+import qualified Data.Sized as S
+
+import           Data.ListLike                (ListLike)
+import           Data.Singletons.Prelude      (SingI)
+import           Data.Singletons.Prelude.Enum (PEnum (..))
+import qualified Data.Type.Ordinal            as O
+import qualified GHC.TypeLits                 as TL
+
+type Ordinal (n :: TL.Nat) = O.Ordinal n
+type Sized f (n :: TL.Nat) = S.Sized f n
+
+pattern (:<) :: forall f (n :: TL.Nat) a.
+                (ListLike (f a) a)
+             => forall (n1 :: TL.Nat).
+                (n ~ Succ n1, SingI n1)
+             => a -> Sized f n1 a -> Sized f n a
+pattern a :< b = a S.:< b
+infixr 5 :<
+
+pattern NilL :: forall f (n :: TL.Nat) a.
+                (ListLike (f a) a)
+             => n ~ 0 => Sized f n a
+pattern NilL = S.NilL
+
+pattern (:>) :: forall f (n :: TL.Nat) a.
+                (ListLike (f a) a)
+             => forall (n1 :: TL.Nat).
+                (n ~ Succ n1, SingI n1)
+             => Sized f n1 a -> a -> Sized f n a
+pattern a :> b = a S.:> b
+infixl 5 :>
+
+pattern NilR :: forall f (n :: TL.Nat) a.
+                (ListLike (f a) a,  SingI n)
+             => n ~ 0 => Sized f n a
+pattern NilR = S.NilR
diff --git a/Data/Sized/Flipped.hs b/Data/Sized/Flipped.hs
new file mode 100644
--- /dev/null
+++ b/Data/Sized/Flipped.hs
@@ -0,0 +1,93 @@
+{-# LANGUAGE ConstraintKinds, DataKinds, DeriveDataTypeable, DeriveFunctor #-}
+{-# LANGUAGE DeriveTraversable, EmptyDataDecls, ExplicitNamespaces         #-}
+{-# LANGUAGE FlexibleContexts, FlexibleInstances                           #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving, KindSignatures                    #-}
+{-# LANGUAGE LiberalTypeSynonyms, MultiParamTypeClasses, PatternSynonyms   #-}
+{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables                    #-}
+{-# LANGUAGE StandaloneDeriving, TemplateHaskell, TypeFamilies, TypeInType #-}
+{-# LANGUAGE TypeOperators, UndecidableInstances, ViewPatterns             #-}
+module Data.Sized.Flipped (Flipped(..),
+                           pattern (:<), pattern NilL,
+                           pattern (:>), pattern NilR) where
+import qualified Data.Sized          as Orig
+import           Data.Sized.Internal
+
+import           Control.DeepSeq              (NFData(..))
+import           Control.Lens.At              (Index, IxValue, Ixed (..))
+import           Control.Lens.TH              (makeWrapped)
+import           Control.Lens.Wrapped         (_Wrapped)
+import           Data.Hashable                (Hashable (..))
+import           Data.Kind                    (Type)
+import qualified Data.ListLike                as LL
+import           Data.MonoTraversable         (Element, MonoFoldable (..))
+import           Data.MonoTraversable         (MonoFunctor (..))
+import           Data.MonoTraversable         (MonoTraversable (..))
+import qualified Data.Sequence                as Seq
+import           Data.Singletons.Prelude.Enum (PEnum (..))
+import qualified Data.Type.Natural            as PN
+import           Data.Type.Natural.Class      (Zero)
+import           Data.Type.Ordinal            (HasOrdinal, Ordinal (..))
+import           Data.Typeable                (Typeable)
+import qualified Data.Vector                  as V
+import qualified Data.Vector.Storable         as SV
+import qualified Data.Vector.Unboxed          as UV
+import qualified GHC.TypeLits                 as TL
+
+-- | Wrapper for @'Sized'@ which takes length as its last element, instead of the second.
+--
+--   Since 0.2.0.0
+newtype Flipped f a n = Flipped { runFlipped :: Sized f n a }
+                      deriving (Show, Eq, Ord, Typeable, NFData, Hashable)
+
+makeWrapped ''Flipped
+
+type instance Index (Flipped f a n) = Ordinal n
+type instance IxValue (Flipped f a n) = IxValue (f a)
+type instance Element (Flipped f a n) = Element (Sized f n a)
+deriving instance MonoFunctor (f a) => MonoFunctor (Flipped f a n)
+deriving instance MonoFoldable (f a) => MonoFoldable (Flipped f a n)
+instance (MonoTraversable (f a)) => MonoTraversable (Flipped f a n) where
+  otraverse = _Wrapped . otraverse
+  {-# INLINE otraverse #-}
+
+  omapM = _Wrapped . omapM
+  {-# INLINE omapM #-}
+
+instance (Integral (Index (f a)), Ixed (f a), HasOrdinal nat)
+      => Ixed (Flipped f a (n :: nat)) where
+  {-# SPECIALISE instance Ixed (Flipped [] a (n :: TL.Nat)) #-}
+  {-# SPECIALISE instance Ixed (Flipped [] a (n :: PN.Nat)) #-}
+  {-# SPECIALISE instance Ixed (Flipped V.Vector a (n :: TL.Nat)) #-}
+  {-# SPECIALISE instance Ixed (Flipped V.Vector a (n :: PN.Nat)) #-}
+  {-# SPECIALISE instance SV.Storable a => Ixed (Flipped SV.Vector a (n :: TL.Nat)) #-}
+  {-# SPECIALISE instance SV.Storable a => Ixed (Flipped SV.Vector a (n :: PN.Nat)) #-}
+  {-# SPECIALISE instance UV.Unbox a => Ixed (Flipped UV.Vector a (n :: TL.Nat)) #-}
+  {-# SPECIALISE instance UV.Unbox a => Ixed (Flipped UV.Vector a (n :: PN.Nat)) #-}
+  {-# SPECIALISE instance Ixed (Flipped Seq.Seq a (n :: TL.Nat)) #-}
+  {-# SPECIALISE instance Ixed (Flipped Seq.Seq a (n :: PN.Nat)) #-}
+  ix o = _Wrapped . ix o
+  {-# INLINE ix #-}
+
+pattern (:<) :: forall nat (f :: Type -> Type) (n :: nat) a.
+                (LL.ListLike (f a) a, HasOrdinal nat)
+              => forall (n1 :: nat). (n ~ Succ n1, PN.SingI n1)
+              => a -> Flipped f a n1 -> Flipped f a n
+pattern a :< as <- Flipped (a Orig.:< (Flipped -> as)) where
+  a :< Flipped as = Flipped (a Orig.:< as)
+
+pattern NilL :: forall nat (f :: Type -> Type) (n :: nat) a.
+                (LL.ListLike (f a) a, HasOrdinal nat)
+             => n ~ Zero nat => Flipped f a n
+pattern NilL = Flipped Orig.NilL
+
+pattern (:>) :: forall nat (f :: Type -> Type) (n :: nat) a.
+                (LL.ListLike (f a) a, HasOrdinal nat)
+             => forall (n1 :: nat). (n ~ Succ n1, PN.SingI n1)
+             => Flipped f a n1 -> a -> Flipped f a n
+pattern as :> a <- Flipped ((Flipped -> as) Orig.:> a) where
+  Flipped as :> a = Flipped (as Orig.:> a)
+
+pattern NilR :: forall nat (f :: Type -> Type) (n :: nat) a.
+                (LL.ListLike (f a) a, HasOrdinal nat)
+             => n ~ Zero nat => Flipped f a n
+pattern NilR = Flipped Orig.NilR
diff --git a/Data/Sized/Internal.hs b/Data/Sized/Internal.hs
--- a/Data/Sized/Internal.hs
+++ b/Data/Sized/Internal.hs
@@ -1,60 +1,183 @@
 {-# LANGUAGE ConstraintKinds, DataKinds, DeriveDataTypeable, DeriveFunctor #-}
-{-# LANGUAGE DeriveTraversable, EmptyDataDecls, FlexibleContexts           #-}
-{-# LANGUAGE FlexibleInstances, GeneralizedNewtypeDeriving, KindSignatures #-}
+{-# LANGUAGE DeriveTraversable, EmptyDataDecls, ExplicitNamespaces         #-}
+{-# LANGUAGE FlexibleContexts, FlexibleInstances                           #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving, KindSignatures                    #-}
 {-# LANGUAGE LiberalTypeSynonyms, MultiParamTypeClasses, PolyKinds         #-}
-{-# LANGUAGE RankNTypes, ScopedTypeVariables, TypeFamilies, TypeOperators  #-}
+{-# LANGUAGE RankNTypes, ScopedTypeVariables, StandaloneDeriving           #-}
+{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeInType, TypeOperators      #-}
 {-# LANGUAGE UndecidableInstances                                          #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 module Data.Sized.Internal
-       (Sized(..), instLL, instFunctor, ListLikeF,
-        withListLikeF, withListLikeF', givenListLikeF,
-        givenListLikeF') where
-import           Data.Constraint
-import           Data.Constraint.Forall (Forall, inst)
-import           Data.Foldable          (Foldable)
-import           Data.ListLike          (FoldableLL (..), ListLike)
-import qualified Data.ListLike          as LL
-import           Data.Proxy
-import qualified Data.Sequence          as Seq
-import           Data.Traversable       (Traversable)
-import           Data.Type.Natural      (Nat)
-import           Data.Typeable          (Typeable)
-import qualified Data.Vector            as V
+       (Sized(..),instLL, instFunctor, ListLikeF,
+        withListLikeF, withListLikeF'
+       ) where
+import           Control.DeepSeq         (NFData (..))
+import           Control.Lens.At         (Index, IxValue, Ixed (..))
+import           Control.Lens.Indexed    (FoldableWithIndex (..))
+import           Control.Lens.Indexed    (FunctorWithIndex (..))
+import           Control.Lens.Indexed    (TraversableWithIndex (..))
+import           Data.Constraint         ((:-) (..), (:=>) (..), Class (..))
+import           Data.Constraint         (Dict (..), trans, weaken1, weaken2)
+import           Data.Constraint         ((&&&), (\\))
+import           Data.Constraint.Forall  (Forall, inst)
+import           Data.Foldable           (Foldable)
+import           Data.Hashable           (Hashable (..))
+import           Data.Kind               (Type)
+import           Data.ListLike           (ListLike)
+import           Data.MonoTraversable    (Element, MonoFoldable (..))
+import           Data.MonoTraversable    (MonoFunctor (..))
+import           Data.MonoTraversable    (MonoTraversable (..))
+import           Data.Proxy              (Proxy (..))
+import qualified Data.Sequence           as Seq
+import           Data.Singletons.Prelude (SingI)
+import           Data.Traversable        (Traversable)
+import qualified Data.Type.Natural       as PN
+import           Data.Type.Ordinal       (HasOrdinal, Ordinal (..), ordToInt)
+import           Data.Type.Ordinal       (unsafeFromInt)
+import           Data.Typeable           (Typeable)
+import qualified Data.Vector             as V
+import qualified Data.Vector.Storable    as SV
+import qualified Data.Vector.Unboxed     as UV
+import qualified GHC.TypeLits            as TL
 
 -- | @Sized@ wraps a sequential type 'f' and makes length-parametrized version.
---   GHC's type natural is currently poor, so we adopt Peano numeral here.
 --
 -- Here, 'f' must be the instance of 'Functor' and @'ListLike' (f a) a@ for all @a@.
 -- This constraint is expressed by 'ListLikeF'.
 -- Folding and traversing function such as 'all' and 'foldl'' is available
 -- via 'Foldable' or 'Traversable' class, if 'f' is the instance of them.
 --
--- Since 0.1.0.0
-newtype Sized f (n :: Nat) a =
+-- Since 0.2.0.0
+newtype Sized (f :: Type -> Type) (n :: nat) a =
   Sized { runSized :: f a
         } deriving (Eq, Ord, Typeable,
                     Functor, Foldable, Traversable)
 
--- | Since 0.1.0.0
-instance ListLikeF f => FoldableLL (Sized f n a) a where
-  {-# SPECIALISE instance LL.FoldableLL (Sized [] n a) a #-}
-  {-# SPECIALISE instance LL.FoldableLL (Sized V.Vector n a) a #-}
-  {-# SPECIALISE instance LL.FoldableLL (Sized Seq.Seq n a) a #-}
-  foldl  f a = givenListLikeF' $ LL.foldl f a
-  {-# INLINE foldl #-}
-  foldl' f a = givenListLikeF' $ LL.foldl' f a
-  {-# INLINE foldl' #-}
-  foldl1 f   = givenListLikeF' $ LL.foldl1 f
-  {-# INLINE foldl1 #-}
-  foldr  f a = givenListLikeF' $ LL.foldr f a
-  {-# INLINE foldr #-}
-  foldr' f a = givenListLikeF' $ LL.foldr' f a
-  {-# INLINE foldr' #-}
-  foldr1 f   = givenListLikeF' $ LL.foldr1 f
-  {-# INLINE foldr1 #-}
+type instance Element (Sized f n a) = Element (f a)
 
+-- | Since 0.2.0.0
+deriving instance MonoFoldable (f a)
+               => MonoFoldable (Sized f n a)
+
+-- | Since 0.2.0.0
+deriving instance MonoFunctor (f a)
+               => MonoFunctor (Sized f n a)
+
+-- | Since 0.2.0.0
+instance {-# OVERLAPPABLE #-} (MonoTraversable (f a))
+      => MonoTraversable (Sized f n a) where
+  {-# SPECIALISE instance MonoTraversable (Sized [] n a) #-}
+  {-# SPECIALISE instance MonoTraversable (Sized V.Vector n a) #-}
+  {-# SPECIALISE instance MonoTraversable (Sized Seq.Seq n a) #-}
+  {-# SPECIALISE instance UV.Unbox a => MonoTraversable (Sized UV.Vector n a) #-}
+  {-# SPECIALISE instance SV.Storable a => MonoTraversable (Sized SV.Vector n a) #-}
+  otraverse f = fmap Sized . otraverse f . runSized
+  omapM f = fmap Sized . omapM f. runSized
+
+-- | Since 0.2.0.0
+instance {-# OVERLAPS #-} SV.Storable a => MonoTraversable (Sized SV.Vector n a) where
+  otraverse f = fmap Sized . otraverse f . runSized
+  omapM f = fmap Sized . omapM f . runSized
+
+-- | Since 0.2.0.0
+instance {-# OVERLAPS #-} UV.Unbox a => MonoTraversable (Sized UV.Vector n a) where
+  otraverse f = fmap Sized . otraverse f . runSized
+  omapM f = fmap Sized . omapM f . runSized
+
+deriving instance NFData (f a) => NFData (Sized f n a)
+deriving instance Hashable (f a) => Hashable (Sized f n a)
+
 instance Show (f a) => Show (Sized f n a) where
   showsPrec d (Sized x) = showsPrec d x
+
+-- | Since 0.2.0.0
+type instance Index (Sized f n a) = Ordinal n
+
+-- | Since 0.2.0.0
+type instance IxValue (Sized f n a) = IxValue (f a)
+instance (Integral (Index (f a)), Ixed (f a), HasOrdinal nat)
+         => Ixed (Sized f (n :: nat) a) where
+  {-# SPECIALISE instance Ixed (Sized [] (n :: TL.Nat) a) #-}
+  {-# SPECIALISE instance Ixed (Sized [] (n :: PN.Nat) a) #-}
+  {-# SPECIALISE instance Ixed (Sized V.Vector (n :: TL.Nat) a) #-}
+  {-# SPECIALISE instance Ixed (Sized V.Vector (n :: PN.Nat) a) #-}
+  {-# SPECIALISE instance SV.Storable a => Ixed (Sized SV.Vector (n :: TL.Nat) a) #-}
+  {-# SPECIALISE instance SV.Storable a => Ixed (Sized SV.Vector (n :: PN.Nat) a) #-}
+  {-# SPECIALISE instance UV.Unbox a => Ixed (Sized UV.Vector (n :: TL.Nat) a) #-}
+  {-# SPECIALISE instance UV.Unbox a => Ixed (Sized UV.Vector (n :: PN.Nat) a) #-}
+  {-# SPECIALISE instance Ixed (Sized Seq.Seq (n :: TL.Nat) a) #-}
+  {-# SPECIALISE instance Ixed (Sized Seq.Seq (n :: PN.Nat) a) #-}
+  {-# INLINE ix #-}
+  ix n f = fmap Sized . ix (fromIntegral $ ordToInt n) f . runSized
+
+-- | Since 0.2.0.0
+instance (Integral i, FunctorWithIndex i f, HasOrdinal nat, SingI n)
+      => FunctorWithIndex (Ordinal (n :: nat)) (Sized f n) where
+  imap f = Sized . imap (f . unsafeFromInt . fromIntegral) . runSized
+  {-# INLINE imap #-}
+  {-# SPECIALISE instance TL.KnownNat n
+                       => FunctorWithIndex (Ordinal n) (Sized [] (n :: TL.Nat)) #-}
+  {-# SPECIALISE instance SingI n
+                       => FunctorWithIndex (Ordinal n) (Sized [] (n :: PN.Nat)) #-}
+  {-# SPECIALISE instance TL.KnownNat n
+                       => FunctorWithIndex (Ordinal n) (Sized V.Vector (n :: TL.Nat)) #-}
+  {-# SPECIALISE instance SingI n
+                       => FunctorWithIndex (Ordinal n) (Sized V.Vector (n :: PN.Nat)) #-}
+  {-# SPECIALISE instance TL.KnownNat n
+                       => FunctorWithIndex (Ordinal n) (Sized Seq.Seq (n :: TL.Nat)) #-}
+  {-# SPECIALISE instance SingI n
+                       => FunctorWithIndex (Ordinal n) (Sized Seq.Seq (n :: PN.Nat)) #-}
+
+-- | Since 0.2.0.0
+instance (Integral i, FoldableWithIndex i f, HasOrdinal nat, SingI n)
+      => FoldableWithIndex (Ordinal (n :: nat)) (Sized f n) where
+  ifoldMap f = ifoldMap (f . unsafeFromInt . fromIntegral) . runSized
+  {-# INLINE ifoldMap #-}
+
+  ifoldr f e = ifoldr (f . unsafeFromInt . fromIntegral) e . runSized
+  {-# INLINE ifoldr #-}
+
+  ifoldl f e = ifoldl (f . unsafeFromInt . fromIntegral) e . runSized
+  {-# INLINE ifoldl #-}
+
+  ifoldr' f e = ifoldr' (f . unsafeFromInt . fromIntegral) e . runSized
+  {-# INLINE ifoldr' #-}
+
+  ifoldl' f e = ifoldl' (f . unsafeFromInt . fromIntegral) e . runSized
+  {-# INLINE ifoldl' #-}
+
+  {-# SPECIALISE instance TL.KnownNat n
+                       => FoldableWithIndex (Ordinal n) (Sized [] (n :: TL.Nat)) #-}
+  {-# SPECIALISE instance SingI n
+                       => FoldableWithIndex (Ordinal n) (Sized [] (n :: PN.Nat)) #-}
+  {-# SPECIALISE instance TL.KnownNat n
+                       => FoldableWithIndex (Ordinal n) (Sized V.Vector (n :: TL.Nat)) #-}
+  {-# SPECIALISE instance SingI n
+                       => FoldableWithIndex (Ordinal n) (Sized V.Vector (n :: PN.Nat)) #-}
+  {-# SPECIALISE instance TL.KnownNat n
+                       => FoldableWithIndex (Ordinal n) (Sized Seq.Seq (n :: TL.Nat)) #-}
+  {-# SPECIALISE instance SingI n
+                       => FoldableWithIndex (Ordinal n) (Sized Seq.Seq (n :: PN.Nat)) #-}
+
+-- | Since 0.2.0.0
+instance (Integral i, TraversableWithIndex i f, HasOrdinal nat, SingI n)
+      => TraversableWithIndex (Ordinal (n :: nat)) (Sized f n) where
+  itraverse f = fmap Sized . itraverse (f . unsafeFromInt . fromIntegral) . runSized
+  {-# INLINE itraverse #-}
+
+  {-# SPECIALISE instance TL.KnownNat n
+                       => TraversableWithIndex (Ordinal n) (Sized [] (n :: TL.Nat)) #-}
+  {-# SPECIALISE instance SingI n
+                       => TraversableWithIndex (Ordinal n) (Sized [] (n :: PN.Nat)) #-}
+  {-# SPECIALISE instance TL.KnownNat n
+                       => TraversableWithIndex (Ordinal n) (Sized V.Vector (n :: TL.Nat)) #-}
+  {-# SPECIALISE instance SingI n
+                       => TraversableWithIndex (Ordinal n) (Sized V.Vector (n :: PN.Nat)) #-}
+  {-# SPECIALISE instance TL.KnownNat n
+                       => TraversableWithIndex (Ordinal n) (Sized Seq.Seq (n :: TL.Nat)) #-}
+  {-# SPECIALISE instance SingI n
+                       => TraversableWithIndex (Ordinal n) (Sized Seq.Seq (n :: PN.Nat))  #-}
+
 class (ListLike (f a) a) => LLF f a
 instance (ListLike (f a) a) => LLF f a
 
@@ -80,14 +203,6 @@
 instFunctor = weaken1
 {-# INLINE instFunctor #-}
 
-givenListLikeF :: ListLikeF f => ((Functor f, ListLike (f a) a) => f a ->  b) -> f a -> b
-givenListLikeF = withListLikeF Proxy
-{-# INLINE givenListLikeF #-}
-
-givenListLikeF' :: ListLikeF f => ((Functor f, ListLike (f a) a) => f a ->  b) -> Sized f n a -> b
-givenListLikeF' f = givenListLikeF f . runSized
-{-# INLINE givenListLikeF' #-}
-
 withListLikeF :: forall pxy f a b. ListLikeF f
               => pxy (f a) -> ((Functor f, ListLike (f a) a) => b) -> b
 withListLikeF _ b = b \\ llDic &&& instFunctor
@@ -100,12 +215,4 @@
 {-# INLINE withListLikeF' #-}
 
 toProxy :: a -> Proxy a
-toProxy = const Proxy
-{-# INLINE toProxy #-}
-
-instance Class (FoldableLL f a) (ListLike f a) where
-  cls = Sub Dict
-
-instance ListLike f a :=> FoldableLL f a where
-  ins = Sub Dict
-
+toProxy _ = Proxy
diff --git a/Data/Sized/Peano.hs b/Data/Sized/Peano.hs
new file mode 100644
--- /dev/null
+++ b/Data/Sized/Peano.hs
@@ -0,0 +1,45 @@
+{-# LANGUAGE DataKinds, GADTs, KindSignatures, MultiParamTypeClasses #-}
+{-# LANGUAGE PatternSynonyms, PolyKinds, RankNTypes, TypeInType      #-}
+{-# LANGUAGE ViewPatterns                                            #-}
+-- | This module exports @'S.Sized'@ type specialized to
+--   type-level Peano numeral @'PN.Nat'@.
+module Data.Sized.Peano
+       (Ordinal, Sized, module Data.Sized,
+        pattern (:<), pattern NilL, pattern (:>), pattern NilR) where
+import           Data.Sized hiding ((:<), (:>), NilL, NilR, Sized)
+import qualified Data.Sized as S
+
+import           Data.ListLike                (ListLike)
+import           Data.Singletons.Prelude      (SingI)
+import           Data.Singletons.Prelude.Enum (PEnum (..))
+import qualified Data.Type.Ordinal            as O
+import qualified Data.Type.Natural            as PN
+
+type Ordinal (n :: PN.Nat) = O.Ordinal n
+type Sized f (n :: PN.Nat) = S.Sized f n
+
+pattern (:<) :: forall f (n :: PN.Nat) a.
+                (ListLike (f a) a)
+             => forall (n1 :: PN.Nat).
+                (n ~ Succ n1, SingI n1)
+             => a -> Sized f n1 a -> Sized f n a
+pattern a :< b = a S.:< b
+infixr 5 :<
+
+pattern NilL :: forall f (n :: PN.Nat) a.
+                (ListLike (f a) a)
+             => n ~ 'PN.Z => Sized f n a
+pattern NilL = S.NilL
+
+pattern (:>) :: forall f (n :: PN.Nat) a.
+                (ListLike (f a) a)
+             => forall (n1 :: PN.Nat).
+                (n ~ Succ n1, SingI n1)
+             => Sized f n1 a -> a -> Sized f n a
+pattern a :> b = a S.:> b
+infixl 5 :>
+
+pattern NilR :: forall f (n :: PN.Nat) a.
+                (ListLike (f a) a)
+             => n ~ 'PN.Z => Sized f n a
+pattern NilR = S.NilR
diff --git a/sized.cabal b/sized.cabal
--- a/sized.cabal
+++ b/sized.cabal
@@ -2,7 +2,7 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                sized
-version:             0.1.0.0
+version:             0.2.0.0
 synopsis:            Sized sequence data-types
 description:         A wrapper to make length-parametrized data-type from ListLike data-types.
 license:             BSD3
@@ -20,14 +20,24 @@
 
 library
   exposed-modules:     Data.Sized
+                     , Data.Sized.Builtin
+                     , Data.Sized.Peano
+                     , Data.Sized.Flipped
   other-modules:       Data.Sized.Internal
   -- other-extensions:    
-  build-depends:       base >=4.7 && <4.8
-               ,       type-natural
-               ,       ListLike
-               ,       vector
-               ,       containers
-               ,       constraints
-               ,       monomorphic
+  build-depends:       base             >= 4.7 && <5
+                     , type-natural     >= 0.4.1.1
+                     , mono-traversable >= 0.10 && < 1.1
+                     , ListLike
+                     , singletons       >= 2.0
+                     , deepseq
+                     , hashable
+                     , vector
+                     , containers
+                     , constraints
+                     , equational-reasoning == 0.*
+                     , monomorphic
+                     , lens >= 0.14
   -- hs-source-dirs:      
   default-language:    Haskell2010
+  ghc-options:         -Wall -Wno-redundant-constraints