diff --git a/sized.cabal b/sized.cabal
--- a/sized.cabal
+++ b/sized.cabal
@@ -1,12 +1,12 @@
 cabal-version: >=2.0
 name:          sized
-version:       0.9.0.0
+version:       1.0.0.0
 license:       BSD3
 license-file:  LICENSE
 maintainer:    konn.jinro_at_gmail.com
 author:        Hiromi ISHII
 tested-with:
-    ghc ==8.6.5, ghc ==8.8.3, ghc ==8.10.1
+    ghc ==8.6.5, ghc ==8.8.4, ghc ==8.10.3
 
 synopsis:      Sized sequence data-types
 description:
@@ -23,7 +23,6 @@
     exposed-modules:
         Data.Sized
         Data.Sized.Builtin
-        Data.Sized.Peano
         Data.Sized.Flipped
 
     hs-source-dirs:   src
@@ -35,11 +34,9 @@
         constraints,
         these,
         type-natural >=0.8.1.0,
-        ghc-typelits-presburger >=0.2.0.0,
+        ghc-typelits-presburger >=0.4,
         ghc-typelits-knownnat,
-        singletons-presburger,
         mono-traversable >=0.10,
-        singletons >=2.0,
         subcategories,
         deepseq >=1.4,
         hashable >=1.2,
@@ -61,9 +58,9 @@
         hspec -any,
         inspection-testing ^>=0.4,
         mono-traversable -any,
-        singletons -any,
         sized -any,
         template-haskell -any,
+        type-natural,
         th-lift -any,
         subcategories -any,
         vector -any
diff --git a/src/Data/Sized.hs b/src/Data/Sized.hs
--- a/src/Data/Sized.hs
+++ b/src/Data/Sized.hs
@@ -1,1415 +1,1831 @@
-{-# LANGUAGE AllowAmbiguousTypes, CPP, ConstraintKinds, DataKinds          #-}
-{-# LANGUAGE DeriveDataTypeable, DeriveFoldable, DeriveFunctor             #-}
-{-# LANGUAGE DeriveTraversable, DerivingStrategies, ExplicitNamespaces     #-}
-{-# LANGUAGE FlexibleContexts, FlexibleInstances, GADTs                    #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving, InstanceSigs, KindSignatures      #-}
-{-# LANGUAGE LambdaCase, LiberalTypeSynonyms, MultiParamTypeClasses        #-}
-{-# LANGUAGE NoMonomorphismRestriction, NoStarIsType, PatternSynonyms      #-}
-{-# LANGUAGE PolyKinds, QuantifiedConstraints, RankNTypes                  #-}
-{-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, TypeApplications     #-}
-{-# LANGUAGE TypeFamilies, TypeInType, TypeOperators, UndecidableInstances #-}
-{-# LANGUAGE UndecidableSuperClasses, 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 'CFreeMonoid' 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@.
---
---  This module also provides powerful view types and pattern synonyms to
---  inspect the sized sequence. See <#ViewsAndPatterns Views and Patterns> for more detail.
-module Data.Sized
-  ( -- * Main Data-types
-    Sized(), SomeSized'(..),
-    DomC(),
-    -- * Accessors
-    -- ** Length information
-    length, sLength, null,
-    -- ** Indexing
-    (!!), (%!!), index, sIndex, head, last,
-    uncons, uncons', Uncons(..),
-    unsnoc, unsnoc', Unsnoc(..),
-    -- ** Slicing
-    tail, init, take, takeAtMost, drop, splitAt, splitAtMost,
-    -- * Construction
-    -- ** Initialisation
-    empty, singleton, toSomeSized, replicate, replicate', generate, generate',
-    -- ** Concatenation
-    cons, (<|), snoc, (|>), append, (++), concat,
-    -- ** Zips
-    zip, zipSame, zipWith, zipWithSame, unzip, unzipWith,
-    -- * Transformation
-    map, reverse, intersperse, nub, sort, sortBy, insert, insertBy,
-    -- * Conversion
-    -- ** List
-    toList, fromList, fromList', unsafeFromList, unsafeFromList',
-    fromListWithDefault, fromListWithDefault',
-    -- ** Base container
-    unsized,
-    toSized, toSized', unsafeToSized, unsafeToSized',
-    toSizedWithDefault, toSizedWithDefault',
-    -- * Querying
-    -- ** Partitioning
-    Partitioned(..),
-    takeWhile, dropWhile, span, break, partition,
-    -- ** Searching
-    elem, notElem, find, findIndex, sFindIndex,
-    findIndices, sFindIndices,
-    elemIndex, sElemIndex, sUnsafeElemIndex, elemIndices, sElemIndices,
-    -- * Views and Patterns
-    -- $ViewsAndPatterns
-
-    -- ** Views
-    -- $views
-
-    -- ** Patterns
-    -- $patterns
-
-    -- ** Definitions
-    viewCons, ConsView (..), viewSnoc, SnocView(..),
-
-    pattern Nil, pattern (:<), pattern (:>),
-  ) where
-
-import Data.Sized.Internal
-
-import           Control.Applicative          (ZipList (..), (<*>))
-import           Control.Subcategory          (CApplicative (..),
-                                               CFoldable (..), CFreeMonoid (..),
-                                               CFunctor (..), CPointed (..),
-                                               CRepeat (..), CSemialign (..),
-                                               CTraversable (..), CUnzip (..),
-                                               CZip (..), Constrained (Dom),
-                                               cfromList, ctoList)
-import           Data.Coerce                  (coerce)
-import           Data.Constraint              (Dict (..), withDict)
-import qualified Data.Foldable                as F
-import           Data.Kind                    (Type)
-import qualified Data.List                    as L
-import           Data.Maybe                   (fromJust)
-import           Data.Monoid                  (Monoid (..), (<>))
-import qualified Data.Sequence                as Seq
-import           Data.Singletons.Prelude      (SingI (..), SomeSing (..),
-                                               withSing, withSingI)
-import           Data.Singletons.Prelude.Bool (Sing)
-import           Data.Singletons.Prelude.Enum (PEnum (..), sPred, sSucc)
-import           Data.These                   (These (..))
-import           Data.Type.Equality           (gcastWith, (:~:) (..))
-import qualified Data.Type.Natural            as Peano
-import           Data.Type.Natural.Class      (IsPeano (..), One, PNum (..),
-                                               POrd (..), PeanoOrder (..), S,
-                                               SNum (..), Zero, ZeroOrSucc (..),
-                                               pattern Zero, sOne, sZero,
-                                               type (-.))
-import           Data.Type.Ordinal            (HasOrdinal, Ordinal (..),
-                                               ordToNatural)
-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 (..),
-                                               Functor, Int, Maybe (..),
-                                               Num (..), Ord (..), Ordering,
-                                               Show (..), const, flip, fmap,
-                                               fromIntegral, uncurry, ($), (.))
-import qualified Prelude                      as P
-import           Proof.Propositional          (IsTrue (..), withWitness)
-import           Unsafe.Coerce                (unsafeCoerce)
-
---------------------------------------------------------------------------------
--- Main data-types
---------------------------------------------------------------------------------
-
--- | 'Sized' vector with the length is existentially quantified.
---   This type is used mostly when the return type's length cannot
---   be statically determined beforehand.
---
--- @SomeSized' sn xs :: SomeSized' f a@ stands for the 'Sized' sequence
--- @xs@ of element type @a@ and length @sn@.
---
--- Since 0.7.0.0
-data SomeSized' f nat a where
-  SomeSized' :: Sing n
-            -> Sized f (n :: nat) a
-            -> SomeSized' f nat a
-
-deriving instance Typeable SomeSized'
-
-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
-
---------------------------------------------------------------------------------
--- Accessors
---------------------------------------------------------------------------------
-
---------------------------------------------------------------------------------
---- Length infromation
---------------------------------------------------------------------------------
-
--- | 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.8.0.0 (type changed)
-length
-  :: forall nat f (n :: nat) a.
-    (IsPeano nat, Dom f a, SingI n)
-  => Sized f n a -> Int
-length = const $ fromIntegral $ toNatural $ sing @n
-{-# INLINE CONLIKE [1] length #-}
-
-lengthTLZero :: Sized f 0 a -> Int
-lengthTLZero = P.const 0
-{-# INLINE lengthTLZero #-}
-
-lengthPeanoZero :: Sized f 'Peano.Z a -> Int
-lengthPeanoZero = P.const 0
-{-# INLINE lengthPeanoZero #-}
-
-{-# RULES
-"length/0" [~1] length = lengthTLZero
-"length/Z" [~1] length = lengthPeanoZero
-  #-}
-
--- | @Sing@ version of 'length'.
---
--- Since 0.8.0.0 (type changed)
-sLength :: forall nat f (n :: nat) a.
-            (HasOrdinal nat, Dom f a, SingI n)
-        => Sized f n a -> Sing n
-sLength _ = sing @n
-{-# INLINE[2] sLength #-}
-
--- | Test if the sequence is empty or not.
---
--- Since 0.7.0.0
-null
-  :: forall nat f (n :: nat) a. (CFoldable f, Dom f a)
-  => Sized f n a -> Bool
-null = coerce $ cnull @f @a
-{-# INLINE CONLIKE [2] null #-}
-
-nullTL0 :: Sized f 0 a -> Bool
-nullTL0 = P.const True
-{-# INLINE nullTL0 #-}
-
-nullPeano0 :: Sized f 'Peano.Z a -> Bool
-nullPeano0 = P.const True
-{-# INLINE nullPeano0 #-}
-
-nullPeanoSucc :: Sized f (S n) a -> Bool
-nullPeanoSucc = P.const False
-{-# INLINE nullPeanoSucc #-}
-
-nullTLSucc :: Sized f (n + 1) a -> Bool
-nullTLSucc = P.const False
-{-# INLINE nullTLSucc #-}
-
-{-# RULES
-"null/0"  [~2] null = nullTL0
-"null/0"  [~2] null = nullTLSucc
-"null/0"  [~1] forall (vec :: 1 TL.<= n => Sized f n a).
-  null vec = False
-"null/Z"  [~2] null = nullPeano0
-"null/Sn" [~2] null = nullPeanoSucc
- #-}
-
---------------------------------------------------------------------------------
---- Indexing
---------------------------------------------------------------------------------
-
--- | (Unsafe) indexing with @Int@s.
---   If you want to check boundary statically, use '%!!' or 'sIndex'.
---
--- Since 0.7.0.0
-(!!)
-  :: forall nat f (m :: nat) a. (CFoldable f, Dom f a, (One nat <= m) ~ 'True)
-  => Sized f m a -> Int -> a
-(!!) = coerce $ cindex @f @a
-{-# INLINE (!!) #-}
-
--- | Safe indexing with 'Ordinal's.
---
--- Since 0.7.0.0
-(%!!)
-  :: forall nat f (n :: nat) c.
-    (HasOrdinal nat, CFoldable f, Dom f c)
-  => Sized f n c -> Ordinal n -> c
-(%!!) = coerce $ (. (P.fromIntegral . ordToNatural)) . cindex @f @c
-{-# 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.7.0.0
-index
-  :: forall nat f (m :: nat) a.
-      (CFoldable f, Dom f a, (One nat <= m) ~ 'True)
-  => Int -> Sized f m a -> a
-index =  flip (!!)
-{-# INLINE index #-}
-
--- | Flipped version of '%!!'.
---
--- Since 0.7.0.0
-sIndex
-  :: forall nat f (n :: nat) c. (HasOrdinal nat, CFoldable f, Dom f c)
-  => Ordinal n -> Sized f n c -> c
-sIndex = flip $ (%!!) @nat @f @n @c
-{-# 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.7.0.0
-head
-  :: forall nat f (n :: nat) a.
-      (HasOrdinal nat, CFoldable f, Dom f a, (Zero nat < n) ~ 'True)
-  => Sized f n a -> a
-head = coerce $ chead @f @a
-{-# 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.7.0.0
-last :: forall nat f (n :: nat) a.
-  (HasOrdinal nat, (Zero nat < n) ~ 'True, CFoldable f, Dom f a)
-  => Sized f n a -> a
-last = coerce $ clast @f @a
-{-# 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.7.0.0
-uncons :: forall nat f (n :: nat) a.
-  (PeanoOrder nat, SingI n, CFreeMonoid f, Dom f a, (Zero nat < n) ~ 'True)
-  => Sized f n a -> Uncons f n a
-uncons =
-  withSingI
-    (sPred $ sing @n)
-  $ gcastWith
-      (succAndPlusOneL $ sPred $ sing @n)
-  $ gcastWith
-      (lneqRightPredSucc sZero (sing @n) Witness
-      )
-  $ uncurry (Uncons @nat @f @(Pred n) @a) . coerce (fromJust . cuncons @f @a)
-
--- | 'uncons' with explicit specified length @n@
---
---   Since 0.7.0.0
-uncons'
-  :: forall nat f (n :: nat) a proxy.
-    (HasOrdinal nat, SingI n, CFreeMonoid f, Dom f a)
-  => proxy n -> Sized f (Succ n) a -> Uncons f (Succ n) a
-uncons' _  = withSingI (sSucc $ sing @n)
-  $ withWitness (lneqZero $ sing @n) uncons
-{-# INLINE uncons' #-}
-
-data Uncons f (n :: nat) a where
-  Uncons :: forall nat f (n :: nat) a. SingI n
-    => a -> Sized f n a -> Uncons f (One nat + n) a
-
--- | 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.7.0.0
-unsnoc
-  :: forall nat f (n :: nat) a.
-    (HasOrdinal nat, SingI n, CFreeMonoid f, Dom f a, (Zero nat < n) ~ 'True)
-  => Sized f n a -> Unsnoc f n a
-unsnoc = withSingI
-    (sPred $ sing @n)
-  $ gcastWith
-      (lneqRightPredSucc sZero (sing @n) Witness
-      )
-  $ uncurry (Unsnoc @nat @f @(Pred n)) . coerce (fromJust . cunsnoc @f @a)
-{-# NOINLINE [1] unsnoc #-}
-
-data Unsnoc f n a where
-  Unsnoc :: forall nat f n a. Sized f (n :: nat) a -> a -> Unsnoc f (Succ n) a
-
--- | 'unsnoc'' with explicit specified length @n@
---
---   Since 0.7.0.0
-unsnoc'
-  :: forall nat f (n :: nat) a proxy.
-    (HasOrdinal nat, SingI n, CFreeMonoid f, Dom f a)
-  => proxy n -> Sized f (Succ n) a -> Unsnoc f (Succ n) a
-unsnoc' _  =
-  withSingI (sSucc $ sing @n)
-  $ withWitness (lneqZero $ sing @n) unsnoc
-{-# INLINE unsnoc' #-}
-
-
---------------------------------------------------------------------------------
---- Slicing
---------------------------------------------------------------------------------
-
--- | 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.7.0.0
-tail
-  :: forall nat f (n :: nat) a. (HasOrdinal nat, CFreeMonoid f, Dom f a)
-  => Sized f (One nat + n) a -> Sized f n a
-tail = coerce $ ctail @f @a
-{-# 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.7.0.0
-init
-  :: forall nat f (n :: nat) a. (HasOrdinal nat, CFreeMonoid f, Dom f a)
-  => Sized f (n + One nat) a -> Sized f n a
-init = coerce $ cinit @f @a
-{-# INLINE init #-}
-
--- | @take k xs@ takes first @k@ element of @xs@ where
--- the length of @xs@ should be larger than @k@.
---
--- Since 0.7.0.0
-take
-  :: forall nat (n :: nat) f (m :: nat) a.
-    (CFreeMonoid f, Dom f a, (n <= m) ~ 'True, HasOrdinal nat)
-  => Sing n -> Sized f m a -> Sized f n a
-take = coerce $ ctake @f @a . P.fromIntegral . toNatural @nat @n
-{-# INLINE take #-}
-
--- | @'takeAtMost' k xs@ takes first at most @k@ elements of @xs@.
---
--- Since 0.7.0.0
-takeAtMost
-  :: forall nat (n :: nat) f m a.
-      (CFreeMonoid f, Dom f a, HasOrdinal nat)
-  => Sing n -> Sized f m a -> Sized f (Min n m) a
-takeAtMost = coerce $ ctake @f @a . P.fromIntegral . toNatural @nat @n
-{-# 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@.
---
--- Since 0.7.0.0
-drop
-  :: forall nat (n :: nat) f (m :: nat) a.
-    (HasOrdinal nat, CFreeMonoid f, Dom f a, (n <= m) ~ 'True)
-  => Sing n -> Sized f m a -> Sized f (m - n) a
-drop = coerce $ cdrop @f @a . P.fromIntegral . toNatural @nat @n
-{-# INLINE drop #-}
-
--- | @splitAt k xs@ split @xs@ at @k@, where
--- the length of @xs@ should be less than or equal to @k@.
---
--- Since 0.7.0.0
-splitAt
-  :: forall nat (n :: nat) f m a.
-      (CFreeMonoid f, Dom f a , (n <= m) ~ 'True, HasOrdinal nat)
-  => Sing n -> Sized f m a -> (Sized f n a, Sized f (m -. n) a)
-splitAt =
-  coerce $ csplitAt @f @a . P.fromIntegral . toNatural @nat @n
-{-# INLINE splitAt #-}
-
--- | @splitAtMost k xs@ split @xs@ at @k@.
---   If @k@ exceeds the length of @xs@, then the second result value become empty.
---
--- Since 0.7.0.0
-splitAtMost
-  :: forall nat (n :: nat) f (m :: nat) a.
-      (HasOrdinal nat, CFreeMonoid f, Dom f a)
-  => Sing n -> Sized f m a -> (Sized f (Min n m) a, Sized f (m -. n) a)
-splitAtMost =
-  coerce $ csplitAt @f @a . P.fromIntegral . toNatural @nat @n
-{-# INLINE splitAtMost #-}
-
-
---------------------------------------------------------------------------------
--- Construction
---------------------------------------------------------------------------------
-
---------------------------------------------------------------------------------
---- Initialisation
---------------------------------------------------------------------------------
-
--- | Empty sequence.
---
--- Since 0.7.0.0 (type changed)
-empty
-  :: forall nat f a. (Monoid (f a), HasOrdinal nat, Dom f a)
-  => Sized f (Zero nat) a
-empty = coerce $ mempty @(f a)
-{-# INLINE empty #-}
-
--- | Sequence with one element.
---
--- Since 0.7.0.0
-singleton :: forall nat f a. (CPointed f, Dom f a) => a -> Sized f (One nat) a
-singleton = coerce $ cpure @f @a
-{-# INLINE singleton #-}
-
--- | Consruct the 'Sized' sequence from base type, but
---   the length parameter is dynamically determined and
---   existentially quantified; see also 'SomeSized''.
---
--- Since 0.7.0.0
-toSomeSized
-  :: forall nat f a. (HasOrdinal nat, Dom f a, CFoldable f)
-  => f a -> SomeSized' f nat a
-toSomeSized = \xs ->
-  case fromNatural $ P.fromIntegral $ clength xs of
-    SomeSing sn -> withSingI sn $ SomeSized' sn $ unsafeToSized sn xs
-
--- | Replicates the same value.
---
--- Since 0.7.0.0
-replicate :: forall nat f (n :: nat) a. (HasOrdinal nat, CFreeMonoid f, Dom f a)
-          => Sing n -> a -> Sized f n a
-replicate = coerce $ creplicate @f @a . P.fromIntegral . toNatural @nat @n
-{-# INLINE replicate #-}
-
--- | 'replicate' with the length inferred.
---
--- Since 0.7.0.0
-replicate'
-  :: forall nat f (n :: nat) a.
-    (HasOrdinal nat, SingI (n :: nat), CFreeMonoid f, Dom f a)
-  => a -> Sized f n a
-replicate' = withSing replicate
-{-# INLINE replicate' #-}
-
--- | Construct a sequence of the given length by applying the function to each index.
---
--- Since 0.7.0.0
-generate
-  :: forall (nat :: Type) f (n :: nat) (a :: Type).
-      (CFreeMonoid f, Dom f a, HasOrdinal nat)
-  => Sing n -> (Ordinal n -> a) -> Sized f n a
-generate = coerce $ \sn -> withSingI sn $
-  cgenerate @f @a (P.fromIntegral $ toNatural @nat @n sn)
-    . (. toEnum @(Ordinal n))
-{-# INLINE [1] generate #-}
-
--- | 'generate' with length inferred.
---
---   Since 0.8.0.0
-generate'
-  :: forall (nat :: Type) f (n :: nat) (a :: Type).
-      (SingI n, CFreeMonoid f, Dom f a, HasOrdinal nat)
-  => (Ordinal n -> a) -> Sized f n a
-generate' = generate sing
-{-# INLINE [1] generate' #-}
-
-genVector :: forall nat (n :: nat) a.
-            (HasOrdinal nat)
-          => Sing n -> (Ordinal n -> a) -> Sized V.Vector n a
-genVector n f = withSingI n $ Sized $ V.generate (P.fromIntegral $ toNatural n) (f . toEnum)
-{-# INLINE genVector #-}
-
-genSVector :: forall nat (n :: nat) a.
-             (HasOrdinal nat, SV.Storable a)
-           => Sing n -> (Ordinal n -> a) -> Sized SV.Vector n a
-genSVector n f = withSingI n $ Sized $ SV.generate (P.fromIntegral $ toNatural n) (f . toEnum)
-{-# INLINE genSVector #-}
-
-genSeq :: forall nat (n :: nat) a.
-          (HasOrdinal nat)
-       => Sing n -> (Ordinal n -> a) -> Sized Seq.Seq n a
-genSeq n f = withSingI n $ Sized $ Seq.fromFunction (P.fromIntegral $ toNatural n)  (f . toEnum)
-{-# INLINE genSeq #-}
-
-{-# RULES
-"generate/Vector"  [~1] generate = genVector
-"generate/SVector" [~1] forall (n :: HasOrdinal nat => Sing (n :: nat))
-                       (f :: SV.Storable a => Ordinal n -> a).
-  generate n f = genSVector n f
-"generate/UVector" [~1] forall (n :: HasOrdinal nat => Sing (n :: nat))
-                       (f :: UV.Unbox a => Ordinal n -> a).
-  generate n f = withSingI n $ Sized (UV.generate (P.fromIntegral $ toNatural n) (f . toEnum))
-"generate/Seq" [~1] generate = genSeq
- #-}
-
---------------------------------------------------------------------------------
---- Concatenation
---------------------------------------------------------------------------------
-
--- | Append an element to the head of sequence.
---
--- Since 0.8.0.0
-cons
-  :: forall nat f (n :: nat) a.
-    (CFreeMonoid f, Dom f a)
-  => a -> Sized f n a -> Sized f (One nat + n) a
-cons = coerce $ ccons @f @a
-{-# INLINE cons #-}
-
--- | Infix version of 'cons'.
---
--- Since 0.8.0.0
-(<|)
-  :: forall nat f (n :: nat) a. (CFreeMonoid f, Dom f a)
-  => a -> Sized f n a -> Sized f (One nat + n) a
-(<|) = cons
-{-# INLINE (<|) #-}
-infixr 5 <|
-
--- | Append an element to the tail of sequence.
---
--- Since 0.7.0.0
-snoc
-  :: forall nat f (n :: nat) a.
-      (CFreeMonoid f, Dom f a)
-  => Sized f n a -> a -> Sized f (n + One nat) a
-snoc (Sized xs) a = Sized $ csnoc xs a
-{-# INLINE snoc #-}
-
--- | Infix version of 'snoc'.
---
--- Since 0.7.0.0
-(|>) :: forall nat f (n :: nat) a.
-  (CFreeMonoid f, Dom f a) => Sized f n a -> a -> Sized f (n + One nat) a
-(|>) = snoc
-{-# INLINE (|>) #-}
-infixl 5 |>
-
--- | Append two lists.
---
--- Since 0.7.0.0
-append
-  :: forall nat f (n :: nat) (m :: nat) a.
-    (CFreeMonoid f, Dom f a)
-  => Sized f n a -> Sized f m a -> Sized f (n + m) a
-append = coerce $ mappend @(f a)
-{-# INLINE append #-}
-
--- | Infix version of 'append'.
---
--- Since 0.7.0.0
-(++)
-  :: forall nat f (n :: nat) (m :: nat) a.
-    (CFreeMonoid f, Dom f a)
-  => Sized f n a -> Sized f m a -> Sized f (n + m) a
-(++) = append
-infixr 5 ++
-
--- | Concatenates multiple sequences into one.
---
--- Since 0.7.0.0
-concat :: forall nat f' (m :: nat) f (n :: nat) a.
-  (CFreeMonoid f, CFunctor f', CFoldable f', Dom f a, Dom f' (f a),
-    Dom f' (Sized f n a)
-  )
-  => Sized f' m (Sized f n a) -> Sized f (m * n) a
-concat = coerce $ cfoldMap @f' @(Sized f n a) runSized
-{-# INLINE [2] concat #-}
-
---------------------------------------------------------------------------------
---- Zips
---------------------------------------------------------------------------------
-
--- | Zipping two sequences. Length is adjusted to shorter one.
---
--- Since 0.7.0.0
-zip
-  :: forall nat f (n :: nat) a (m :: nat) b.
-    (Dom f a, CZip f, Dom f b, Dom f (a, b))
-  => Sized f n a -> Sized f m b -> Sized f (Min n m) (a, b)
-zip = coerce $ czip @f @a @b
-
--- | 'zip' for the sequences of the same length.
---
--- Since 0.7.0.0
-zipSame
-  :: forall nat f (n :: nat) a b.
-      (Dom f a, CZip f, Dom f b, Dom f (a, b))
-  => Sized f n a -> Sized f n b -> Sized f n (a, b)
-zipSame = coerce $ czip @f @a @b
-{-# INLINE [1] zipSame #-}
-
--- | Zipping two sequences with funtion. Length is adjusted to shorter one.
---
--- Since 0.7.0.0
-zipWith
-  :: forall nat f (n :: nat) a (m :: nat) b c.
-    (Dom f a, CZip f, Dom f b, CFreeMonoid f, Dom f c)
-  => (a -> b -> c)
-  -> Sized f n a
-  -> Sized f m b
-  -> Sized f (Min n m) c
-zipWith = coerce $ czipWith @f @a @b @c
-{-# INLINE [1] zipWith #-}
-
--- | 'zipWith' for the sequences of the same length.
---
--- Since 0.7.0.0
-zipWithSame
-  :: forall nat f (n :: nat) a b c.
-      (Dom f a, CZip f, Dom f b, CFreeMonoid f, Dom f c)
-  => (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c
-zipWithSame = coerce $ czipWith @f @a @b @c
-{-# INLINE [1] zipWithSame #-}
-
--- | Unzipping the sequence of tuples.
---
--- Since 0.7.0.0
-unzip
-  :: forall nat f (n :: nat) a b.
-      (CUnzip f, Dom f a, Dom f b, Dom f (a, b))
-  => Sized f n (a, b) -> (Sized f n a, Sized f n b)
-unzip = coerce $ cunzip @f @a @b
-{-# INLINE unzip #-}
-
--- | Unzipping the sequence of tuples.
---
--- Since 0.7.0.0
-unzipWith
-  :: forall nat f (n :: nat) a b c.
-      (CUnzip f, Dom f a, Dom f b, Dom f c)
-  => (a -> (b, c))
-  -> Sized f n a -> (Sized f n b, Sized f n c)
-unzipWith = coerce $ cunzipWith @f @a @b @c
-{-# INLINE unzipWith #-}
-
---------------------------------------------------------------------------------
--- Transformation
---------------------------------------------------------------------------------
-
--- | Map function.
---
--- Since 0.7.0.0
-map
-  :: forall nat f (n :: nat) a b.
-    (CFreeMonoid f, Dom f a, Dom f b)
-  => (a -> b) -> Sized f n a -> Sized f n b
-map f = Sized . cmap f . runSized
-{-# INLINE map #-}
-
--- | Reverse function.
---
--- Since 0.7.0.0
-reverse
-  :: forall nat f (n :: nat) a.
-    (Dom f a, CFreeMonoid f)
-  => Sized f n a -> Sized f n a
-reverse = coerce $ creverse @f @a
-{-# INLINE reverse #-}
-
--- | Intersperces.
---
--- Since 0.7.0.0
-intersperse
-  :: forall nat f (n :: nat) a.
-    (CFreeMonoid f, Dom f a)
-  => a -> Sized f n a -> Sized f ((FromInteger 2 * n) -. One nat) a
-intersperse = coerce $ cintersperse @f @a
-{-# INLINE intersperse #-}
-
--- | Remove all duplicates.
---
--- Since 0.7.0.0
-nub
-  :: forall nat f (n :: nat) a.
-      (HasOrdinal nat, Dom f a, Eq a, CFreeMonoid f)
-  => Sized f n a -> SomeSized' f nat a
-nub = toSomeSized . coerce (cnub @f @a)
-
--- | Sorting sequence by ascending order.
---
--- Since 0.7.0.0
-sort :: forall nat f (n :: nat) a.
-    (CFreeMonoid f, Dom f a, Ord a)
-  => Sized f n a -> Sized f n a
-sort = coerce $ csort @f @a
-
--- | Generalized version of 'sort'.
---
--- Since 0.7.0.0
-sortBy
-  :: forall nat f (n :: nat) a. (CFreeMonoid f, Dom f a)
-  => (a -> a -> Ordering) -> Sized f n a -> Sized f n a
-sortBy = coerce $ csortBy @f @a
-
--- | Insert new element into the presorted sequence.
---
--- Since 0.7.0.0
-insert
-  :: forall nat f (n :: nat) a.
-    (CFreeMonoid f, Dom f a, Ord a)
-  => a -> Sized f n a -> Sized f (Succ n) a
-insert = coerce $ cinsert @f @a
-
--- | Generalized version of 'insert'.
---
--- Since 0.7.0.0
-insertBy
-  :: forall nat f (n :: nat) a.
-    (CFreeMonoid f, Dom f a)
-  => (a -> a -> Ordering) -> a -> Sized f n a -> Sized f (Succ n) a
-insertBy = coerce $ cinsertBy @f @a
-
---------------------------------------------------------------------------------
--- Conversion
---------------------------------------------------------------------------------
-
---------------------------------------------------------------------------------
---- List
---------------------------------------------------------------------------------
-
--- | Convert to list.
---
--- Since 0.7.0.0
-toList
-  :: forall nat f (n :: nat) a.
-    (CFoldable f, Dom f a)
-  => Sized f n a -> [a]
-toList = coerce $ ctoList @f @a
-{-# INLINE [2] toList #-}
-
-{-# RULES
-"toList/List"
-  Data.Sized.toList = runSized
-  #-}
-
--- | 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.7.0.0 (type changed)
-fromList
-  :: forall nat f (n :: nat) a.
-      (HasOrdinal nat, CFreeMonoid f, Dom f a)
-  => Sing n -> [a] -> Maybe (Sized f n a)
-fromList Zero _ = Just $ Sized (mempty :: f a)
-fromList sn xs =
-  let len = P.fromIntegral $ toNatural sn
-  in if P.length xs < len
-     then Nothing
-     else Just $ Sized $ ctake len $ cfromList xs
-{-# INLINABLE [2] fromList #-}
-
--- | 'fromList' with the result length inferred.
---
--- Since 0.7.0.0
-fromList'
-  :: forall nat f (n :: nat) a.
-    (PeanoOrder nat, Dom f a, CFreeMonoid f, SingI n)
-  => [a] -> Maybe (Sized f n a)
-fromList' = withSing fromList
-{-# INLINE fromList' #-}
-
--- | Unsafe version of 'fromList'. If the length of the given list does not
---   equal to @n@, then something unusual happens.
---
--- Since 0.7.0.0
-unsafeFromList
-  :: forall (nat :: Type) f (n :: nat) a.
-    (CFreeMonoid f, Dom f a)
-  => Sing n -> [a] -> Sized f n a
-unsafeFromList = const $ coerce $ cfromList  @f @a
-{-# INLINE [1] unsafeFromList #-}
-
--- | 'unsafeFromList' with the result length inferred.
---
--- Since 0.7.0.0
-unsafeFromList'
-  :: forall nat f (n :: nat) a.
-      (SingI n, CFreeMonoid f, Dom f a)
-  => [a] -> Sized f n a
-unsafeFromList' = withSing unsafeFromList
-{-# INLINE [1] unsafeFromList' #-}
-{-# RULES
-"unsafeFromList'/List" [~1]
-  unsafeFromList' = Sized
-"unsafeFromList'/Vector" [~1]
-  unsafeFromList' = Sized . V.fromList
-"unsafeFromList'/Seq" [~1]
-  unsafeFromList' = Sized . Seq.fromList
-"unsafeFromList'/SVector" [~1] forall (xs :: SV.Storable a => [a]).
-  unsafeFromList'  xs = Sized (SV.fromList xs)
-"unsafeFromList'/UVector" [~1] forall (xs :: UV.Unbox a => [a]).
-  unsafeFromList'  xs = Sized (UV.fromList xs)
-  #-}
-
--- | Construct a @Sized f n a@ by padding default value if the given list is short.
---
---   Since 0.5.0.0 (type changed)
-fromListWithDefault
-  :: forall nat f (n :: nat) a.
-      (HasOrdinal nat, Dom f a, CFreeMonoid f)
-  => Sing n -> a -> [a] -> Sized f n a
-fromListWithDefault sn def xs =
-  let len = P.fromIntegral $ toNatural sn
-  in Sized $ cfromList (ctake len xs) <>
-        creplicate (len - clength xs) def
-{-# INLINABLE fromListWithDefault #-}
-
--- | 'fromListWithDefault' with the result length inferred.
---
--- Since 0.7.0.0
-fromListWithDefault'
-  :: forall nat f (n :: nat) a. (PeanoOrder nat, SingI n, CFreeMonoid f, Dom f a)
-  => a -> [a] -> Sized f n a
-fromListWithDefault' = withSing fromListWithDefault
-{-# INLINE fromListWithDefault' #-}
-
---------------------------------------------------------------------------------
---- Base containes
---------------------------------------------------------------------------------
-
--- | Forget the length and obtain the wrapped base container.
---
--- Since 0.7.0.0
-unsized :: forall nat f (n :: nat) a. Sized f n a -> f a
-unsized = runSized
-{-# INLINE unsized #-}
-
--- | 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.7.0.0
-toSized
-  :: forall nat f (n :: nat) a.
-      (HasOrdinal nat, CFreeMonoid f, Dom f a)
-  => Sing (n :: nat) -> f a -> Maybe (Sized f n a)
-toSized sn xs =
-  let len = P.fromIntegral $ toNatural sn
-  in if clength xs < len
-     then Nothing
-     else Just $ unsafeToSized sn $ ctake len xs
-{-# INLINABLE [2] toSized #-}
-
--- | 'toSized' with the result length inferred.
---
--- Since 0.7.0.0
-toSized'
-  :: forall nat f (n :: nat) a.
-    (PeanoOrder nat, Dom f a, CFreeMonoid f, SingI n)
-  => 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
---   equal to @n@, then something unusual happens.
---
--- Since 0.7.0.0
-unsafeToSized :: forall nat f (n :: nat) a. Sing n -> f a -> Sized f n a
-unsafeToSized _ = Sized
-{-# INLINE [2] unsafeToSized #-}
-
--- | 'unsafeToSized' with the result length inferred.
---
--- Since 0.7.0.0
-unsafeToSized'
-  :: forall nat f (n :: nat) a.
-    (SingI n, Dom f 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.7.0.0
-toSizedWithDefault
-  :: forall nat f (n :: nat) a.
-    (HasOrdinal nat, CFreeMonoid f, Dom f a)
-  => Sing (n :: nat) -> a -> f a -> Sized f n a
-toSizedWithDefault sn def xs =
-  let len = P.fromIntegral $ toNatural sn
-  in Sized $ ctake len xs <> creplicate (len - clength xs) def
-{-# INLINABLE toSizedWithDefault #-}
-
--- | 'toSizedWithDefault' with the result length inferred.
---
--- Since 0.7.0.0
-toSizedWithDefault'
-  :: forall nat f (n :: nat) a.
-      (PeanoOrder nat, SingI n, CFreeMonoid f, Dom f a)
-  => a -> f a -> Sized f n a
-toSizedWithDefault' = withSing toSizedWithDefault
-{-# INLINE toSizedWithDefault' #-}
-
-
---------------------------------------------------------------------------------
--- Querying
---------------------------------------------------------------------------------
-
---------------------------------------------------------------------------------
---- Partitioning
---------------------------------------------------------------------------------
-
--- | 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.7.0.0
-data Partitioned f n a where
-  Partitioned :: (Dom f a)
-              => Sing n
-              -> Sized f n a
-              -> Sing m
-              -> Sized f m a
-              -> Partitioned f (n + m) a
-
--- | Take the initial segment as long as elements satisfys the predicate.
---
--- Since 0.7.0.0
-takeWhile
-  :: forall nat f (n :: nat) a.
-    (HasOrdinal nat, Dom f a, CFreeMonoid f)
-  => (a -> Bool) -> Sized f n a -> SomeSized' f nat a
-takeWhile = (toSomeSized .) . coerce (ctakeWhile @f @a)
-{-# INLINE takeWhile #-}
-
--- | Drop the initial segment as long as elements satisfys the predicate.
---
--- Since 0.7.0.0
-dropWhile
-  :: forall nat f (n :: nat) a.
-      (HasOrdinal nat, CFreeMonoid f, Dom f a)
-  => (a -> Bool) -> Sized f n a -> SomeSized' f nat a
-dropWhile = (toSomeSized .) . coerce (cdropWhile @f @a)
-{-# INLINE dropWhile #-}
-
--- | Split the sequence into the longest prefix
---   of elements that satisfy the predicate
---   and the rest.
---
--- Since 0.7.0.0
-span
-  :: forall nat f (n :: nat) a.
-      (HasOrdinal nat, CFreeMonoid f, Dom f a)
-  => (a -> Bool) -> Sized f n a -> Partitioned f n a
-span = (unsafePartitioned @nat @n .) . coerce (cspan @f @a)
-{-# INLINE span #-}
-
--- | Split the sequence into the longest prefix
---   of elements that do not satisfy the
---   predicate and the rest.
---
--- Since 0.7.0.0
-break
-  :: forall nat f (n :: nat) a.
-      (HasOrdinal nat, CFreeMonoid f, Dom f a)
-  => (a -> Bool) -> Sized f n a -> Partitioned f n a
-break = (unsafePartitioned @nat @n .) . coerce (cbreak @f @a)
-{-# INLINE break #-}
-
--- | Split the sequence in two parts, the first one containing those elements that satisfy the predicate and the second one those that don't.
---
--- Since 0.7.0.0
-partition
-  :: forall nat f (n :: nat) a.
-      (HasOrdinal nat, CFreeMonoid f, Dom f a)
-  => (a -> Bool) -> Sized f n a -> Partitioned f n a
-partition = (unsafePartitioned @nat @n .) . coerce (cpartition @f @a)
-{-# INLINE partition #-}
-
-unsafePartitioned
-  :: forall nat (n :: nat) f a.
-    (HasOrdinal nat, CFreeMonoid f, Dom f a)
-  => (f a, f a) -> Partitioned f n a
-unsafePartitioned (l, r) =
-  case (toSomeSized @nat l, toSomeSized @nat r) of
-    ( SomeSized' (lenL :: Sing nl) ls,
-      SomeSized' (lenR :: Sing nr) rs
-      ) ->
-        gcastWith
-        (unsafeCoerce $ Refl @()
-          :: n :~: nl + nr
-        )
-        $ Partitioned lenL ls lenR rs
-
---------------------------------------------------------------------------------
---- Searching
---------------------------------------------------------------------------------
--- | Membership test; see also 'notElem'.
---
--- Since 0.7.0.0
-elem
-  :: forall nat f (n :: nat) a.
-    (CFoldable f, Dom f a, Eq a)
-  => a -> Sized f n a -> Bool
-elem = coerce $ celem @f @a
-{-# INLINE elem #-}
-
--- | Negation of 'elem'.
---
--- Since 0.7.0.0
-notElem
-  :: forall nat f (n :: nat) a.
-    (CFoldable f, Dom f a, Eq a)
-  => a -> Sized f n a -> Bool
-notElem = coerce $ cnotElem @f @a
-{-# INLINE notElem #-}
-
--- | Find the element satisfying the predicate.
---
--- Since 0.7.0.0
-find
-  :: forall nat f (n :: nat) a.
-      (CFoldable f, Dom f a)
-  => (a -> Bool) -> Sized f n a -> Maybe a
-find = coerce $ cfind @f @a
-{-# INLINE[1] find #-}
-{-# RULES
-"find/List" [~1] forall p.
-  find p = L.find @[] p . runSized
-"find/Vector" [~1] forall p.
-  find p = V.find p . runSized
-"find/Storable Vector" [~1] forall (p :: SV.Storable a => a -> Bool).
-  find p = SV.find p . runSized
-"find/Unboxed Vector" [~1] forall (p :: UV.Unbox a => a -> Bool).
-  find p = UV.find p . runSized
-  #-}
-
--- | @'findIndex' p xs@ find the element satisfying @p@ and returns its index if exists.
---
--- Since 0.7.0.0
-findIndex
-  :: forall nat f (n :: nat) a .
-    (CFoldable f, Dom f a)
-  => (a -> Bool) -> Sized f n a -> Maybe Int
-findIndex = coerce $ cfindIndex @f @a
-{-# INLINE findIndex #-}
-
--- | 'Ordinal' version of 'findIndex'.
---
--- Since 0.7.0.0
-sFindIndex
-  :: forall nat f (n :: nat) a .
-    (SingI (n :: nat), CFoldable f, Dom f a, HasOrdinal nat)
-  => (a -> Bool) -> Sized f n a -> Maybe (Ordinal n)
-sFindIndex = (fmap toEnum .) . coerce (cfindIndex @f @a)
-{-# INLINE sFindIndex #-}
-
--- | @'findIndices' p xs@ find all elements satisfying @p@ and returns their indices.
---
--- Since 0.7.0.0
-findIndices
-  :: forall nat f (n :: nat) a .
-    (CFoldable f, Dom f a) => (a -> Bool) -> Sized f n a -> [Int]
-findIndices = coerce $ cfindIndices @f @a
-{-# INLINE findIndices #-}
-{-# SPECIALISE findIndices :: (a -> Bool) -> Sized [] n a -> [Int] #-}
-
--- | 'Ordinal' version of 'findIndices'.
---
--- Since 0.7.0.0
-sFindIndices
-  :: forall nat f (n :: nat) a .
-    (HasOrdinal nat, CFoldable f, Dom f a, SingI (n :: nat))
-  => (a -> Bool) -> Sized f n a -> [Ordinal n]
-sFindIndices p = P.fmap (toEnum . P.fromIntegral) . findIndices p
-{-# INLINE sFindIndices #-}
-
-
-{-# RULES
-"Foldable.sum/Vector"
-  F.sum = V.sum . runSized
-  #-}
-
--- | Returns the index of the given element in the list, if exists.
---
--- Since 0.7.0.0
-elemIndex :: forall nat f (n :: nat) a .
-  (CFoldable f, Eq a, Dom f a) => a -> Sized f n a -> Maybe Int
-elemIndex = coerce $ celemIndex @f @a
-{-# INLINE elemIndex #-}
-
--- | Ordinal version of 'elemIndex'.
---   Since 0.7.0.0, we no longer do boundary check inside the definition.
---
---   Since 0.7.0.0
-sElemIndex, sUnsafeElemIndex :: forall nat f (n :: nat) a.
-              (SingI n, CFoldable f, Dom f a, Eq a, HasOrdinal nat)
-           => a -> Sized f n a -> Maybe (Ordinal n)
-sElemIndex = (fmap toEnum .) . coerce (celemIndex @f @a)
-{-# INLINE sElemIndex #-}
-
--- | Since 0.5.0.0 (type changed)
-sUnsafeElemIndex = sElemIndex
-{-# DEPRECATED sUnsafeElemIndex "No difference with sElemIndex; use sElemIndex instead." #-}
-
--- | Returns all indices of the given element in the list.
---
--- Since 0.7.0.0
-elemIndices
-  :: forall nat f (n :: nat) a .
-    (CFoldable f, Dom f a, Eq a) => a -> Sized f n a -> [Int]
-elemIndices = coerce $ celemIndices @f @a
-{-# INLINE elemIndices #-}
-
--- | Ordinal version of 'elemIndices'
---
--- Since 0.7.0.0
-sElemIndices
-  :: forall nat f (n :: nat) a .
-    (CFoldable f, HasOrdinal nat, SingI (n :: nat), Dom f a, Eq a)
-  => a -> Sized f n a -> [Ordinal n]
-sElemIndices = (fmap toEnum .) . elemIndices
-{-# INLINE sElemIndices #-}
-
---------------------------------------------------------------------------------
--- Views and Patterns
---------------------------------------------------------------------------------
-
-{-$ViewsAndPatterns #ViewsAndPatterns#
-
-   With GHC's @ViewPatterns@ and @PatternSynonym@ extensions,
-   we can pattern-match on arbitrary @Sized f n a@ if @f@ is list-like functor.
-   Curretnly, there are two direction view and patterns: Cons and Snoc.
-   Assuming underlying sequence type @f@ has O(1) implementation for 'cnull', 'chead'
-   (resp. 'clast') and 'ctail' (resp. 'cinit'), We can view and pattern-match on
-   cons (resp. snoc) of @Sized f n a@ in O(1).
--}
-
-{-$views #views#
-
-   With @ViewPatterns@ extension, we can pattern-match on 'Sized' value as follows:
-
-@
-slen :: ('SingI' n, 'Dom f 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, 'Dom f 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, 'Dom f 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.7.0.0
-data ConsView f n a where
-  NilCV :: ConsView f (Zero nat) a
-  (:-)
-    :: (SingI n, SingI (One nat + n))
-    => a -> Sized f n a -> ConsView f (One nat + n) a
-
-infixr 5 :-
-
--- | Case analysis for the cons-side of sequence.
---
--- Since 0.5.0.0 (type changed)
-viewCons :: forall nat f (n :: nat) a .
-  (HasOrdinal nat, SingI n, CFreeMonoid f,Dom f a)
-  => Sized f n a
-  -> ConsView f n a
-viewCons sz = case zeroOrSucc $ sing @n of
-  IsZero -> NilCV
-  IsSucc n' ->
-    withSingI n'
-    $ withSingI (sOne %+ n')
-    $ case uncons' n' sz of
-        Uncons a xs -> a :- xs
-
--- | View of the left end of sequence (snoc-side).
---
--- Since 0.7.0.0
-data SnocView f n a where
-  NilSV :: SnocView f (Zero nat) a
-  (:-::) :: SingI (n :: nat) => Sized f n a -> a -> SnocView f (n + One nat) a
-infixl 5 :-::
-
--- | Case analysis for the snoc-side of sequence.
---
--- Since 0.5.0.0 (type changed)
-viewSnoc :: forall nat f (n :: nat) a.
-    (HasOrdinal nat, SingI n, CFreeMonoid f, Dom f a)
-         => Sized f n a
-         -> SnocView f n a
-viewSnoc sz = case zeroOrSucc (sing @n) of
-  IsZero   -> NilSV
-  IsSucc (n' :: Sing n') ->
-    withSingI n' $
-    gcastWith (succAndPlusOneR n') $
-    case unsnoc' n' sz of
-      Unsnoc (xs :: Sized f m a) a ->
-        gcastWith
-          (unsafeCoerce (Refl @()) :: n' :~: m)
-        $ xs :-:: a
-
-{-$patterns #patterns#
-
-   So we can pattern match on both end of sequence via views, but
-   it is rather clumsy to nest it. For example:
-
-@
-nextToHead :: ('Dom f 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 :: ('Dom f 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, 'Dom f a' f) => 'Sized' f n a -> 'Sing' n
-slen 'Nil'      = 'SZ'
-slen (_ ':<' as) = 'SS' (slen as)
-@
-
-   So, we can use @':<'@ and @'Nil'@ (resp. @':>'@ and @'Nil'@) to
-   pattern-match directly on cons-side (resp. snoc-side) as we usually do for lists.
-   @'Nil'@, @':<'@, and @':>'@ are neither functions nor data constructors,
-   but pattern synonyms so we cannot use them in expression contexts.
-   For more detail on pattern synonyms, see
-   <http://www.haskell.org/ghc/docs/latest/html/users_guide/syntax-extns.html#pattern-synonyms GHC Users Guide>
-   and
-   <https://ghc.haskell.org/trac/ghc/wiki/PatternSynonyms HaskellWiki>.
--}
-
-infixr 5 :<
--- | Pattern synonym for cons-side uncons.
-pattern (:<)
-  :: forall nat (f :: Type -> Type) a (n :: nat).
-      (Dom f a, PeanoOrder nat, SingI n, CFreeMonoid f)
-  => forall (n1 :: nat). (n ~ (One nat + n1), SingI n1)
-  => a -> Sized f n1 a -> Sized f n a
-pattern a :< as <- (viewCons -> a :- as) where
-   a :< as = a <| as
-
-chkNil
-  :: forall nat f (n :: nat) a.
-      (IsPeano nat, SingI n)
-  => Sized f n a -> ZeroOrSucc n
-chkNil = const $ zeroOrSucc $ sing @n
-
--- | Pattern synonym for a nil sequence.
-pattern Nil :: forall nat f (n :: nat) a.
-                (SingI n, CFreeMonoid f, Dom f a,  HasOrdinal nat)
-            => (n ~ Zero nat) => Sized f n a
-pattern Nil <- (chkNil -> IsZero) where
-  Nil = empty
-
-infixl 5 :>
-
--- | Pattern synonym for snoc-side unsnoc.
-pattern (:>)
-  :: forall nat (f :: Type -> Type) a (n :: nat).
-      (Dom f a, PeanoOrder nat, SingI n, CFreeMonoid f)
-  => forall (n1 :: nat). (n ~ (n1 + One nat), SingI n1)
-  => Sized f n1 a -> a -> Sized f n a
-pattern a :> b <- (viewSnoc -> a :-:: b) where
-  a :> b = a |> b
-
-{-# COMPLETE (:<), Nil #-}
-{-# COMPLETE (:>), Nil #-}
-
-class Dom f a => DomC f a
-instance Dom f a => DomC f a
-
--- | Applicative instance, generalizing @'Data.Monoid.ZipList'@.
-instance
-  ( Functor f, CFreeMonoid f, CZip f,
-    HasOrdinal nat, SingI n, forall a. DomC f a)
-      => 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) = withDict (Dict @(DomC f a))
-    $ replicate' x
-  {-# INLINE pure #-}
-
-  (fs :: Sized f n (a -> b)) <*> (xs :: Sized f n a) =
-    withDict (Dict @(DomC f b))
-    $ withDict (Dict @(DomC f a))
-    $ withDict (Dict @(DomC f (a -> b)))
-    $ zipWithSame ($) fs xs
-  {-# INLINE [1] (<*>) #-}
-{-# RULES
-"<*>/List" [~1] forall fs xs.
-  Sized fs <*> Sized xs = Sized (getZipList (ZipList fs <*> ZipList xs))
-"<*>/Seq" [~1] forall fs xs.
-  Sized fs <*> Sized xs = Sized (Seq.zipWith ($) fs xs)
-"<*>/Vector" [~1] forall fs xs.
-  Sized fs <*> Sized xs = Sized (V.zipWith ($) fs xs)
- #-}
-
-instance (CFreeMonoid f, PeanoOrder nat, SingI (n :: nat))
-      => CPointed (Sized f n) where
-  cpure = replicate'
-
-instance (CFreeMonoid f, CZip f)
-      => CApplicative (Sized f n) where
-  pair = zipSame
-  (<.>) = zipWithSame ($)
-  (<.) = P.const
-  (.>) = P.flip P.const
-
--- | __N.B.__ Since @calign@ is just zipping for fixed @n@,
---   we require more strong 'CZip' constraint here.
-instance (CZip f, CFreeMonoid f) => CSemialign (Sized f n) where
-  calignWith = coerce (\f -> czipWith @f @a @b @c ((f .) . These))
-    :: forall a b c.
-        (Dom f a, Dom f b, Dom f c)
-    => (These a b -> c) -> Sized f n a -> Sized f n b -> Sized f n c
-  {-# INLINE [1] calignWith #-}
-  calign = coerce $ czipWith @f @a @b These
-    :: forall a b.
-      (Dom f a, Dom f b, Dom f (These a b))
-    => Sized f n a -> Sized f n b -> Sized f n (These a b)
-  {-# INLINE [1] calign #-}
-
-instance (CZip f, CFreeMonoid f) => CZip (Sized f n) where
-  czipWith = coerce $ czipWith @f @a @b @c
-    :: forall a b c.
-        (Dom f a, Dom f b, Dom f c)
-    => (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c
-  {-# INLINE [1] czipWith #-}
-  czip = coerce $ czip @f @a @b
-    :: forall a b.
-      (Dom f a, Dom f b, Dom f (a, b))
-    => Sized f n a -> Sized f n b -> Sized f n (a, b)
-  {-# INLINE [1] czip #-}
-
-instance
-  (PeanoOrder nat, SingI (n :: nat), CZip f, CFreeMonoid f)
-  => CRepeat (Sized f n) where
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE LiberalTypeSynonyms #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE NoStarIsType #-}
+{-# OPTIONS_GHC -fenable-rewrite-rules #-}
+{-# OPTIONS_GHC -fno-warn-type-defaults -fno-warn-orphans #-}
+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-}
+
+{- | This module provides the functionality to make length-parametrized types
+   from existing 'CFreeMonoid' 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@.
+
+  This module also provides powerful view types and pattern synonyms to
+  inspect the sized sequence. See <#ViewsAndPatterns Views and Patterns> for more detail.
+-}
+module Data.Sized
+  ( -- * Main Data-types
+    Sized (),
+    SomeSized (..),
+    DomC (),
+
+    -- * Accessors
+
+    -- ** Length information
+    length,
+    sLength,
+    null,
+
+    -- ** Indexing
+    (!!),
+    (%!!),
+    index,
+    sIndex,
+    head,
+    last,
+    uncons,
+    uncons',
+    Uncons (..),
+    unsnoc,
+    unsnoc',
+    Unsnoc (..),
+
+    -- ** Slicing
+    tail,
+    init,
+    take,
+    takeAtMost,
+    drop,
+    splitAt,
+    splitAtMost,
+
+    -- * Construction
+
+    -- ** Initialisation
+    empty,
+    singleton,
+    toSomeSized,
+    replicate,
+    replicate',
+    generate,
+    generate',
+
+    -- ** Concatenation
+    cons,
+    (<|),
+    snoc,
+    (|>),
+    append,
+    (++),
+    concat,
+
+    -- ** Zips
+    zip,
+    zipSame,
+    zipWith,
+    zipWithSame,
+    unzip,
+    unzipWith,
+
+    -- * Transformation
+    map,
+    reverse,
+    intersperse,
+    nub,
+    sort,
+    sortBy,
+    insert,
+    insertBy,
+
+    -- * Conversion
+
+    -- ** List
+    toList,
+    fromList,
+    fromList',
+    unsafeFromList,
+    unsafeFromList',
+    fromListWithDefault,
+    fromListWithDefault',
+
+    -- ** Base container
+    unsized,
+    toSized,
+    toSized',
+    unsafeToSized,
+    unsafeToSized',
+    toSizedWithDefault,
+    toSizedWithDefault',
+
+    -- * Querying
+
+    -- ** Partitioning
+    Partitioned (..),
+    takeWhile,
+    dropWhile,
+    span,
+    break,
+    partition,
+
+    -- ** Searching
+    elem,
+    notElem,
+    find,
+    findIndex,
+    sFindIndex,
+    findIndices,
+    sFindIndices,
+    elemIndex,
+    sElemIndex,
+    sUnsafeElemIndex,
+    elemIndices,
+    sElemIndices,
+
+    -- * Views and Patterns
+    -- $ViewsAndPatterns
+
+    -- ** Views
+    -- $views
+
+    -- ** Patterns
+    -- $patterns
+
+    -- ** Definitions
+    viewCons,
+    ConsView (..),
+    viewSnoc,
+    SnocView (..),
+    pattern Nil,
+    pattern (:<),
+    pattern (:>),
+  )
+where
+
+import Control.Applicative (ZipList (..), (<*>))
+import Control.Subcategory
+  ( CApplicative (..),
+    CFoldable (..),
+    CFreeMonoid (..),
+    CFunctor (..),
+    CPointed (..),
+    CRepeat (..),
+    CSemialign (..),
+    CTraversable (..),
+    CUnzip (..),
+    CZip (..),
+    Constrained (Dom),
+    cfromList,
+    ctoList,
+  )
+import Data.Coerce (coerce)
+import Data.Constraint (Dict (..), withDict)
+import qualified Data.Foldable as F
+import Data.Kind (Type)
+import qualified Data.List as L
+import Data.Maybe (fromJust)
+import Data.Monoid (Monoid (..), (<>))
+import qualified Data.Sequence as Seq
+import Data.Sized.Internal
+import Data.These (These (..))
+import Data.Type.Equality (gcastWith, (:~:) (..))
+import Data.Type.Natural
+import Data.Type.Ordinal (Ordinal (..), ordToNatural)
+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 Unsafe.Coerce (unsafeCoerce)
+import Prelude
+  ( Bool (..),
+    Enum (..),
+    Eq (..),
+    Functor,
+    Int,
+    Maybe (..),
+    Num (..),
+    Ord (..),
+    Ordering,
+    Show (..),
+    const,
+    flip,
+    fmap,
+    fromIntegral,
+    uncurry,
+    ($),
+    (.),
+  )
+import qualified Prelude as P
+
+--------------------------------------------------------------------------------
+-- Main data-types
+--------------------------------------------------------------------------------
+
+{- | 'Sized' vector with the length is existentially quantified.
+   This type is used mostly when the return type's length cannot
+   be statically determined beforehand.
+
+ @SomeSized sn xs :: SomeSized f a@ stands for the 'Sized' sequence
+ @xs@ of element type @a@ and length @sn@.
+
+ Since 0.7.0.0
+-}
+data SomeSized f a where
+  SomeSized ::
+    SNat n ->
+    Sized f n a ->
+    SomeSized f a
+
+deriving instance Typeable SomeSized
+
+instance Show (f a) => Show (SomeSized f a) where
+  showsPrec d (SomeSized _ s) =
+    P.showParen (d > 9) $
+      P.showString "SomeSized _ " . showsPrec 10 s
+
+instance Eq (f a) => Eq (SomeSized f a) where
+  (SomeSized _ (Sized xs)) == (SomeSized _ (Sized ys)) = xs == ys
+
+--------------------------------------------------------------------------------
+-- Accessors
+--------------------------------------------------------------------------------
+
+--------------------------------------------------------------------------------
+--- Length infromation
+--------------------------------------------------------------------------------
+
+{- | 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.8.0.0 (type changed)
+-}
+length ::
+  forall f (n :: Nat) a.
+  (Dom f a, KnownNat n) =>
+  Sized f n a ->
+  Int
+length = const $ fromIntegral $ toNatural $ sNat @n
+{-# INLINE CONLIKE [1] length #-}
+
+lengthTLZero :: Sized f 0 a -> Int
+lengthTLZero = P.const 0
+{-# INLINE lengthTLZero #-}
+
+{-# RULES
+"length/0" [~1] length = lengthTLZero
+  #-}
+
+{- | @SNat@ version of 'length'.
+
+ Since 0.8.0.0 (type changed)
+-}
+sLength ::
+  forall f (n :: Nat) a.
+  (Dom f a, KnownNat n) =>
+  Sized f n a ->
+  SNat n
+sLength _ = sNat @n
+{-# INLINE [2] sLength #-}
+
+{- | Test if the sequence is empty or not.
+
+ Since 0.7.0.0
+-}
+null ::
+  forall f (n :: Nat) a.
+  (CFoldable f, Dom f a) =>
+  Sized f n a ->
+  Bool
+null = coerce $ cnull @f @a
+{-# INLINE CONLIKE [2] null #-}
+
+nullTL0 :: Sized f 0 a -> Bool
+nullTL0 = P.const True
+{-# INLINE nullTL0 #-}
+
+nullPeanoSucc :: Sized f (S n) a -> Bool
+nullPeanoSucc = P.const False
+{-# INLINE nullPeanoSucc #-}
+
+nullTLSucc :: Sized f (n + 1) a -> Bool
+nullTLSucc = P.const False
+{-# INLINE nullTLSucc #-}
+
+{-# RULES
+"null/0" [~2] null = nullTL0
+"null/0" [~2] null = nullTLSucc
+"null/0" [~1] forall (vec :: 1 <= n => Sized f n a).
+  null vec =
+    False
+"null/Sn" [~2] null = nullPeanoSucc
+  #-}
+
+--------------------------------------------------------------------------------
+--- Indexing
+--------------------------------------------------------------------------------
+
+{- | (Unsafe) indexing with @Int@s.
+   If you want to check boundary statically, use '%!!' or 'sIndex'.
+
+ Since 0.7.0.0
+-}
+(!!) ::
+  forall f (m :: Nat) a.
+  (CFoldable f, Dom f a, (1 <= m)) =>
+  Sized f m a ->
+  Int ->
+  a
+(!!) = coerce $ cindex @f @a
+{-# INLINE (!!) #-}
+
+{- | Safe indexing with 'Ordinal's.
+
+ Since 0.7.0.0
+-}
+(%!!) ::
+  forall f (n :: Nat) c.
+  (CFoldable f, Dom f c) =>
+  Sized f n c ->
+  Ordinal n ->
+  c
+(%!!) = coerce $ (. (P.fromIntegral . ordToNatural)) . cindex @f @c
+{-# INLINE (%!!) #-}
+{-# SPECIALIZE (%!!) :: Sized [] (n :: Nat) a -> Ordinal n -> a #-}
+{-# SPECIALIZE (%!!) :: Sized V.Vector (n :: Nat) a -> Ordinal n -> a #-}
+{-# SPECIALIZE (%!!) :: UV.Unbox a => Sized UV.Vector (n :: Nat) a -> Ordinal n -> a #-}
+{-# SPECIALIZE (%!!) :: SV.Storable a => Sized SV.Vector (n :: Nat) a -> Ordinal n -> a #-}
+{-# SPECIALIZE (%!!) :: Sized Seq.Seq (n :: Nat) a -> Ordinal n -> a #-}
+
+{- | Flipped version of '!!'.
+
+ Since 0.7.0.0
+-}
+index ::
+  forall f (m :: Nat) a.
+  (CFoldable f, Dom f a, (1 <= m)) =>
+  Int ->
+  Sized f m a ->
+  a
+index = flip (!!)
+{-# INLINE index #-}
+
+{- | Flipped version of '%!!'.
+
+ Since 0.7.0.0
+-}
+sIndex ::
+  forall f (n :: Nat) c.
+  (CFoldable f, Dom f c) =>
+  Ordinal n ->
+  Sized f n c ->
+  c
+sIndex = flip $ (%!!) @f @n @c
+{-# 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.7.0.0
+-}
+head ::
+  forall f (n :: Nat) a.
+  (CFoldable f, Dom f a, (0 < n)) =>
+  Sized f n a ->
+  a
+head = coerce $ chead @f @a
+{-# 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.7.0.0
+-}
+last ::
+  forall f (n :: Nat) a.
+  ((0 < n), CFoldable f, Dom f a) =>
+  Sized f n a ->
+  a
+last = coerce $ clast @f @a
+{-# 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.7.0.0
+-}
+uncons ::
+  forall f (n :: Nat) a.
+  (KnownNat n, CFreeMonoid f, Dom f a, (1 <= n)) =>
+  Sized f n a ->
+  Uncons f n a
+uncons =
+  withKnownNat
+    (sPred $ sNat @n)
+    $ uncurry (Uncons @f @(Pred n) @a) . coerce (fromJust . cuncons @f @a)
+
+{- | 'uncons' with explicit specified length @n@
+
+   Since 0.7.0.0
+-}
+uncons' ::
+  forall f (n :: Nat) a proxy.
+  (KnownNat n, CFreeMonoid f, Dom f a) =>
+  proxy n ->
+  Sized f (Succ n) a ->
+  Uncons f (Succ n) a
+uncons' _ =
+  withKnownNat (sSucc $ sNat @n) uncons
+{-# INLINE uncons' #-}
+
+data Uncons f (n :: Nat) a where
+  Uncons ::
+    forall f (n :: Nat) a.
+    KnownNat n =>
+    a ->
+    Sized f n a ->
+    Uncons f (1 + n) a
+
+{- | 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.7.0.0
+-}
+unsnoc ::
+  forall f (n :: Nat) a.
+  (KnownNat n, CFreeMonoid f, Dom f a, (0 < n)) =>
+  Sized f n a ->
+  Unsnoc f n a
+unsnoc =
+  withKnownNat
+    (sPred $ sNat @n)
+    $ uncurry (Unsnoc @f @(Pred n)) . coerce (fromJust . cunsnoc @f @a)
+{-# NOINLINE [1] unsnoc #-}
+
+data Unsnoc f n a where
+  Unsnoc :: forall f n a. Sized f (n :: Nat) a -> a -> Unsnoc f (Succ n) a
+
+{- | 'unsnoc'' with explicit specified length @n@
+
+   Since 0.7.0.0
+-}
+unsnoc' ::
+  forall f (n :: Nat) a proxy.
+  (KnownNat n, CFreeMonoid f, Dom f a) =>
+  proxy n ->
+  Sized f (Succ n) a ->
+  Unsnoc f (Succ n) a
+unsnoc' _ =
+  withKnownNat (sSucc $ sNat @n) unsnoc
+{-# INLINE unsnoc' #-}
+
+--------------------------------------------------------------------------------
+--- Slicing
+--------------------------------------------------------------------------------
+
+{- | 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.7.0.0
+-}
+tail ::
+  forall f (n :: Nat) a.
+  (CFreeMonoid f, Dom f a) =>
+  Sized f (1 + n) a ->
+  Sized f n a
+tail = coerce $ ctail @f @a
+{-# 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.7.0.0
+-}
+init ::
+  forall f (n :: Nat) a.
+  (CFreeMonoid f, Dom f a) =>
+  Sized f (n + 1) a ->
+  Sized f n a
+init = coerce $ cinit @f @a
+{-# INLINE init #-}
+
+{- | @take k xs@ takes first @k@ element of @xs@ where
+ the length of @xs@ should be larger than @k@.
+
+ Since 0.7.0.0
+-}
+take ::
+  forall (n :: Nat) f (m :: Nat) a.
+  (CFreeMonoid f, Dom f a, (n <= m)) =>
+  SNat n ->
+  Sized f m a ->
+  Sized f n a
+take = coerce $ ctake @f @a . P.fromIntegral . toNatural @n
+{-# INLINE take #-}
+
+{- | @'takeAtMost' k xs@ takes first at most @k@ elements of @xs@.
+
+ Since 0.7.0.0
+-}
+takeAtMost ::
+  forall (n :: Nat) f m a.
+  (CFreeMonoid f, Dom f a) =>
+  SNat n ->
+  Sized f m a ->
+  Sized f (Min n m) a
+takeAtMost = coerce $ ctake @f @a . P.fromIntegral . toNatural @n
+{-# 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@.
+
+ Since 0.7.0.0
+-}
+drop ::
+  forall (n :: Nat) f (m :: Nat) a.
+  (CFreeMonoid f, Dom f a, (n <= m)) =>
+  SNat n ->
+  Sized f m a ->
+  Sized f (m - n) a
+drop = coerce $ cdrop @f @a . P.fromIntegral . toNatural @n
+{-# INLINE drop #-}
+
+{- | @splitAt k xs@ split @xs@ at @k@, where
+ the length of @xs@ should be less than or equal to @k@.
+
+ Since 0.7.0.0
+-}
+splitAt ::
+  forall (n :: Nat) f m a.
+  (CFreeMonoid f, Dom f a, (n <= m)) =>
+  SNat n ->
+  Sized f m a ->
+  (Sized f n a, Sized f (m -. n) a)
+splitAt =
+  coerce $ csplitAt @f @a . P.fromIntegral . toNatural @n
+{-# INLINE splitAt #-}
+
+{- | @splitAtMost k xs@ split @xs@ at @k@.
+   If @k@ exceeds the length of @xs@, then the second result value become empty.
+
+ Since 0.7.0.0
+-}
+splitAtMost ::
+  forall (n :: Nat) f (m :: Nat) a.
+  (CFreeMonoid f, Dom f a) =>
+  SNat n ->
+  Sized f m a ->
+  (Sized f (Min n m) a, Sized f (m -. n) a)
+splitAtMost =
+  coerce $ csplitAt @f @a . P.fromIntegral . toNatural @n
+{-# INLINE splitAtMost #-}
+
+--------------------------------------------------------------------------------
+-- Construction
+--------------------------------------------------------------------------------
+
+--------------------------------------------------------------------------------
+--- Initialisation
+--------------------------------------------------------------------------------
+
+{- | Empty sequence.
+
+ Since 0.7.0.0 (type changed)
+-}
+empty ::
+  forall f a.
+  (Monoid (f a), Dom f a) =>
+  Sized f (0) a
+empty = coerce $ mempty @(f a)
+{-# INLINE empty #-}
+
+{- | Sequence with one element.
+
+ Since 0.7.0.0
+-}
+singleton :: forall f a. (CPointed f, Dom f a) => a -> Sized f (1) a
+singleton = coerce $ cpure @f @a
+{-# INLINE singleton #-}
+
+{- | Consruct the 'Sized' sequence from base type, but
+   the length parameter is dynamically determined and
+   existentially quantified; see also 'SomeSized'.
+
+ Since 0.7.0.0
+-}
+toSomeSized ::
+  forall f a.
+  (Dom f a, CFoldable f) =>
+  f a ->
+  SomeSized f a
+{-# INLINE toSomeSized #-}
+toSomeSized = \xs ->
+  case toSomeSNat $ P.fromIntegral $ clength xs of
+    SomeSNat sn -> withKnownNat sn $ SomeSized sn $ unsafeToSized sn xs
+
+{- | Replicates the same value.
+
+ Since 0.7.0.0
+-}
+replicate ::
+  forall f (n :: Nat) a.
+  (CFreeMonoid f, Dom f a) =>
+  SNat n ->
+  a ->
+  Sized f n a
+replicate = coerce $ creplicate @f @a . P.fromIntegral . toNatural @n
+{-# INLINE replicate #-}
+
+{- | 'replicate' with the length inferred.
+
+ Since 0.7.0.0
+-}
+replicate' ::
+  forall f (n :: Nat) a.
+  (KnownNat (n :: Nat), CFreeMonoid f, Dom f a) =>
+  a ->
+  Sized f n a
+replicate' = replicate (sNat @n)
+{-# INLINE replicate' #-}
+
+{- | Construct a sequence of the given length by applying the function to each index.
+
+ Since 0.7.0.0
+-}
+generate ::
+  forall f (n :: Nat) (a :: Type).
+  (CFreeMonoid f, Dom f a) =>
+  SNat n ->
+  (Ordinal n -> a) ->
+  Sized f n a
+generate = coerce $ \sn ->
+  withKnownNat sn $
+    cgenerate @f @a (P.fromIntegral $ toNatural @n sn)
+      . (. toEnum @(Ordinal n))
+{-# INLINE [1] generate #-}
+
+{- | 'generate' with length inferred.
+
+   Since 0.8.0.0
+-}
+generate' ::
+  forall f (n :: Nat) (a :: Type).
+  (KnownNat n, CFreeMonoid f, Dom f a) =>
+  (Ordinal n -> a) ->
+  Sized f n a
+generate' = generate sNat
+{-# INLINE [1] generate' #-}
+
+genVector ::
+  forall (n :: Nat) a.
+  SNat n ->
+  (Ordinal n -> a) ->
+  Sized V.Vector n a
+genVector n f = withKnownNat n $ Sized $ V.generate (P.fromIntegral $ toNatural n) (f . toEnum)
+{-# INLINE genVector #-}
+
+genSVector ::
+  forall (n :: Nat) a.
+  (SV.Storable a) =>
+  SNat n ->
+  (Ordinal n -> a) ->
+  Sized SV.Vector n a
+genSVector n f = withKnownNat n $ Sized $ SV.generate (P.fromIntegral $ toNatural n) (f . toEnum)
+{-# INLINE genSVector #-}
+
+genSeq ::
+  forall (n :: Nat) a.
+  SNat n ->
+  (Ordinal n -> a) ->
+  Sized Seq.Seq n a
+genSeq n f = withKnownNat n $ Sized $ Seq.fromFunction (P.fromIntegral $ toNatural n) (f . toEnum)
+{-# INLINE genSeq #-}
+
+{-# RULES
+"generate/Vector" [~1] generate = genVector
+"generate/SVector" [~1] forall
+  (n :: SNat (n :: Nat))
+  (f :: SV.Storable a => Ordinal n -> a).
+  generate n f =
+    genSVector n f
+"generate/UVector" [~1] forall
+  (n :: SNat (n :: Nat))
+  (f :: UV.Unbox a => Ordinal n -> a).
+  generate n f =
+    withKnownNat n $ Sized (UV.generate (P.fromIntegral $ toNatural n) (f . toEnum))
+"generate/Seq" [~1] generate = genSeq
+  #-}
+
+--------------------------------------------------------------------------------
+--- Concatenation
+--------------------------------------------------------------------------------
+
+{- | Append an element to the head of sequence.
+
+ Since 0.8.0.0
+-}
+cons ::
+  forall f (n :: Nat) a.
+  (CFreeMonoid f, Dom f a) =>
+  a ->
+  Sized f n a ->
+  Sized f (1 + n) a
+cons = coerce $ ccons @f @a
+{-# INLINE cons #-}
+
+{- | Infix version of 'cons'.
+
+ Since 0.8.0.0
+-}
+(<|) ::
+  forall f (n :: Nat) a.
+  (CFreeMonoid f, Dom f a) =>
+  a ->
+  Sized f n a ->
+  Sized f (1 + n) a
+(<|) = cons
+{-# INLINE (<|) #-}
+
+infixr 5 <|
+
+{- | Append an element to the tail of sequence.
+
+ Since 0.7.0.0
+-}
+snoc ::
+  forall f (n :: Nat) a.
+  (CFreeMonoid f, Dom f a) =>
+  Sized f n a ->
+  a ->
+  Sized f (n + 1) a
+snoc (Sized xs) a = Sized $ csnoc xs a
+{-# INLINE snoc #-}
+
+{- | Infix version of 'snoc'.
+
+ Since 0.7.0.0
+-}
+(|>) ::
+  forall f (n :: Nat) a.
+  (CFreeMonoid f, Dom f a) =>
+  Sized f n a ->
+  a ->
+  Sized f (n + 1) a
+(|>) = snoc
+{-# INLINE (|>) #-}
+
+infixl 5 |>
+
+{- | Append two lists.
+
+ Since 0.7.0.0
+-}
+append ::
+  forall f (n :: Nat) (m :: Nat) a.
+  (CFreeMonoid f, Dom f a) =>
+  Sized f n a ->
+  Sized f m a ->
+  Sized f (n + m) a
+append = coerce $ mappend @(f a)
+{-# INLINE append #-}
+
+{- | Infix version of 'append'.
+
+ Since 0.7.0.0
+-}
+(++) ::
+  forall f (n :: Nat) (m :: Nat) a.
+  (CFreeMonoid f, Dom f a) =>
+  Sized f n a ->
+  Sized f m a ->
+  Sized f (n + m) a
+(++) = append
+
+infixr 5 ++
+
+{- | Concatenates multiple sequences into one.
+
+ Since 0.7.0.0
+-}
+concat ::
+  forall f' (m :: Nat) f (n :: Nat) a.
+  ( CFreeMonoid f
+  , CFunctor f'
+  , CFoldable f'
+  , Dom f a
+  , Dom f' (f a)
+  , Dom f' (Sized f n a)
+  ) =>
+  Sized f' m (Sized f n a) ->
+  Sized f (m * n) a
+concat = coerce $ cfoldMap @f' @(Sized f n a) runSized
+{-# INLINE [2] concat #-}
+
+--------------------------------------------------------------------------------
+--- Zips
+--------------------------------------------------------------------------------
+
+{- | Zipping two sequences. Length is adjusted to shorter one.
+
+ Since 0.7.0.0
+-}
+zip ::
+  forall f (n :: Nat) a (m :: Nat) b.
+  (Dom f a, CZip f, Dom f b, Dom f (a, b)) =>
+  Sized f n a ->
+  Sized f m b ->
+  Sized f (Min n m) (a, b)
+zip = coerce $ czip @f @a @b
+
+{- | 'zip' for the sequences of the same length.
+
+ Since 0.7.0.0
+-}
+zipSame ::
+  forall f (n :: Nat) a b.
+  (Dom f a, CZip f, Dom f b, Dom f (a, b)) =>
+  Sized f n a ->
+  Sized f n b ->
+  Sized f n (a, b)
+zipSame = coerce $ czip @f @a @b
+{-# INLINE [1] zipSame #-}
+
+{- | Zipping two sequences with funtion. Length is adjusted to shorter one.
+
+ Since 0.7.0.0
+-}
+zipWith ::
+  forall f (n :: Nat) a (m :: Nat) b c.
+  (Dom f a, CZip f, Dom f b, CFreeMonoid f, Dom f c) =>
+  (a -> b -> c) ->
+  Sized f n a ->
+  Sized f m b ->
+  Sized f (Min n m) c
+zipWith = coerce $ czipWith @f @a @b @c
+{-# INLINE [1] zipWith #-}
+
+{- | 'zipWith' for the sequences of the same length.
+
+ Since 0.7.0.0
+-}
+zipWithSame ::
+  forall f (n :: Nat) a b c.
+  (Dom f a, CZip f, Dom f b, CFreeMonoid f, Dom f c) =>
+  (a -> b -> c) ->
+  Sized f n a ->
+  Sized f n b ->
+  Sized f n c
+zipWithSame = coerce $ czipWith @f @a @b @c
+{-# INLINE [1] zipWithSame #-}
+
+{- | Unzipping the sequence of tuples.
+
+ Since 0.7.0.0
+-}
+unzip ::
+  forall f (n :: Nat) a b.
+  (CUnzip f, Dom f a, Dom f b, Dom f (a, b)) =>
+  Sized f n (a, b) ->
+  (Sized f n a, Sized f n b)
+unzip = coerce $ cunzip @f @a @b
+{-# INLINE unzip #-}
+
+{- | Unzipping the sequence of tuples.
+
+ Since 0.7.0.0
+-}
+unzipWith ::
+  forall f (n :: Nat) a b c.
+  (CUnzip f, Dom f a, Dom f b, Dom f c) =>
+  (a -> (b, c)) ->
+  Sized f n a ->
+  (Sized f n b, Sized f n c)
+unzipWith = coerce $ cunzipWith @f @a @b @c
+{-# INLINE unzipWith #-}
+
+--------------------------------------------------------------------------------
+-- Transformation
+--------------------------------------------------------------------------------
+
+{- | Map function.
+
+ Since 0.7.0.0
+-}
+map ::
+  forall f (n :: Nat) a b.
+  (CFreeMonoid f, Dom f a, Dom f b) =>
+  (a -> b) ->
+  Sized f n a ->
+  Sized f n b
+map f = Sized . cmap f . runSized
+{-# INLINE map #-}
+
+{- | Reverse function.
+
+ Since 0.7.0.0
+-}
+reverse ::
+  forall f (n :: Nat) a.
+  (Dom f a, CFreeMonoid f) =>
+  Sized f n a ->
+  Sized f n a
+reverse = coerce $ creverse @f @a
+{-# INLINE reverse #-}
+
+{- | Intersperces.
+
+ Since 0.7.0.0
+-}
+intersperse ::
+  forall f (n :: Nat) a.
+  (CFreeMonoid f, Dom f a) =>
+  a ->
+  Sized f n a ->
+  Sized f ((2 * n) -. 1) a
+intersperse = coerce $ cintersperse @f @a
+{-# INLINE intersperse #-}
+
+{- | Remove all duplicates.
+
+ Since 0.7.0.0
+-}
+nub ::
+  forall f (n :: Nat) a.
+  (Dom f a, Eq a, CFreeMonoid f) =>
+  Sized f n a ->
+  SomeSized f a
+nub = toSomeSized . coerce (cnub @f @a)
+
+{- | Sorting sequence by ascending order.
+
+ Since 0.7.0.0
+-}
+sort ::
+  forall f (n :: Nat) a.
+  (CFreeMonoid f, Dom f a, Ord a) =>
+  Sized f n a ->
+  Sized f n a
+sort = coerce $ csort @f @a
+
+{- | Generalized version of 'sort'.
+
+ Since 0.7.0.0
+-}
+sortBy ::
+  forall f (n :: Nat) a.
+  (CFreeMonoid f, Dom f a) =>
+  (a -> a -> Ordering) ->
+  Sized f n a ->
+  Sized f n a
+sortBy = coerce $ csortBy @f @a
+
+{- | Insert new element into the presorted sequence.
+
+ Since 0.7.0.0
+-}
+insert ::
+  forall f (n :: Nat) a.
+  (CFreeMonoid f, Dom f a, Ord a) =>
+  a ->
+  Sized f n a ->
+  Sized f (Succ n) a
+insert = coerce $ cinsert @f @a
+
+{- | Generalized version of 'insert'.
+
+ Since 0.7.0.0
+-}
+insertBy ::
+  forall f (n :: Nat) a.
+  (CFreeMonoid f, Dom f a) =>
+  (a -> a -> Ordering) ->
+  a ->
+  Sized f n a ->
+  Sized f (Succ n) a
+insertBy = coerce $ cinsertBy @f @a
+
+--------------------------------------------------------------------------------
+-- Conversion
+--------------------------------------------------------------------------------
+
+--------------------------------------------------------------------------------
+--- List
+--------------------------------------------------------------------------------
+
+{- | Convert to list.
+
+ Since 0.7.0.0
+-}
+toList ::
+  forall f (n :: Nat) a.
+  (CFoldable f, Dom f a) =>
+  Sized f n a ->
+  [a]
+toList = coerce $ ctoList @f @a
+{-# INLINE [2] toList #-}
+
+{-# RULES
+"toList/List"
+  Data.Sized.toList =
+    runSized
+  #-}
+
+{- | 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.7.0.0 (type changed)
+-}
+fromList ::
+  forall f (n :: Nat) a.
+  (CFreeMonoid f, Dom f a) =>
+  SNat n ->
+  [a] ->
+  Maybe (Sized f n a)
+fromList Zero _ = Just $ Sized (mempty :: f a)
+fromList sn xs =
+  let len = P.fromIntegral $ toNatural sn
+   in if P.length xs < len
+        then Nothing
+        else Just $ Sized $ ctake len $ cfromList xs
+{-# INLINEABLE [2] fromList #-}
+
+{- | 'fromList' with the result length inferred.
+
+ Since 0.7.0.0
+-}
+fromList' ::
+  forall f (n :: Nat) a.
+  (Dom f a, CFreeMonoid f, KnownNat n) =>
+  [a] ->
+  Maybe (Sized f n a)
+fromList' = fromList sNat
+{-# INLINE fromList' #-}
+
+{- | Unsafe version of 'fromList'. If the length of the given list does not
+   equal to @n@, then something unusual happens.
+
+ Since 0.7.0.0
+-}
+unsafeFromList ::
+  forall f (n :: Nat) a.
+  (CFreeMonoid f, Dom f a) =>
+  SNat n ->
+  [a] ->
+  Sized f n a
+unsafeFromList = const $ coerce $ cfromList @f @a
+{-# INLINE [1] unsafeFromList #-}
+
+{- | 'unsafeFromList' with the result length inferred.
+
+ Since 0.7.0.0
+-}
+unsafeFromList' ::
+  forall f (n :: Nat) a.
+  (KnownNat n, CFreeMonoid f, Dom f a) =>
+  [a] ->
+  Sized f n a
+unsafeFromList' = unsafeFromList sNat
+{-# INLINE [1] unsafeFromList' #-}
+
+{-# RULES
+"unsafeFromList'/List" [~1]
+  unsafeFromList' =
+    Sized
+"unsafeFromList'/Vector" [~1]
+  unsafeFromList' =
+    Sized . V.fromList
+"unsafeFromList'/Seq" [~1]
+  unsafeFromList' =
+    Sized . Seq.fromList
+"unsafeFromList'/SVector" [~1] forall (xs :: SV.Storable a => [a]).
+  unsafeFromList' xs =
+    Sized (SV.fromList xs)
+"unsafeFromList'/UVector" [~1] forall (xs :: UV.Unbox a => [a]).
+  unsafeFromList' xs =
+    Sized (UV.fromList xs)
+  #-}
+
+{- | Construct a @Sized f n a@ by padding default value if the given list is short.
+
+   Since 0.5.0.0 (type changed)
+-}
+fromListWithDefault ::
+  forall f (n :: Nat) a.
+  (Dom f a, CFreeMonoid f) =>
+  SNat n ->
+  a ->
+  [a] ->
+  Sized f n a
+fromListWithDefault sn def xs =
+  let len = P.fromIntegral $ toNatural sn
+   in Sized $
+        cfromList (ctake len xs)
+          <> creplicate (len - clength xs) def
+{-# INLINEABLE fromListWithDefault #-}
+
+{- | 'fromListWithDefault' with the result length inferred.
+
+ Since 0.7.0.0
+-}
+fromListWithDefault' ::
+  forall f (n :: Nat) a.
+  (KnownNat n, CFreeMonoid f, Dom f a) =>
+  a ->
+  [a] ->
+  Sized f n a
+fromListWithDefault' = fromListWithDefault sNat
+{-# INLINE fromListWithDefault' #-}
+
+--------------------------------------------------------------------------------
+--- Base containes
+--------------------------------------------------------------------------------
+
+{- | Forget the length and obtain the wrapped base container.
+
+ Since 0.7.0.0
+-}
+unsized :: forall f (n :: Nat) a. Sized f n a -> f a
+unsized = runSized
+{-# INLINE unsized #-}
+
+{- | 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.7.0.0
+-}
+toSized ::
+  forall f (n :: Nat) a.
+  (CFreeMonoid f, Dom f a) =>
+  SNat (n :: Nat) ->
+  f a ->
+  Maybe (Sized f n a)
+toSized sn xs =
+  let len = P.fromIntegral $ toNatural sn
+   in if clength xs < len
+        then Nothing
+        else Just $ unsafeToSized sn $ ctake len xs
+{-# INLINEABLE [2] toSized #-}
+
+{- | 'toSized' with the result length inferred.
+
+ Since 0.7.0.0
+-}
+toSized' ::
+  forall f (n :: Nat) a.
+  (Dom f a, CFreeMonoid f, KnownNat n) =>
+  f a ->
+  Maybe (Sized f n a)
+toSized' = toSized sNat
+{-# INLINE toSized' #-}
+
+{- | Unsafe version of 'toSized'. If the length of the given list does not
+   equal to @n@, then something unusual happens.
+
+ Since 0.7.0.0
+-}
+unsafeToSized :: forall f (n :: Nat) a. SNat n -> f a -> Sized f n a
+unsafeToSized _ = Sized
+{-# INLINE [2] unsafeToSized #-}
+
+{- | 'unsafeToSized' with the result length inferred.
+
+ Since 0.7.0.0
+-}
+unsafeToSized' ::
+  forall f (n :: Nat) a.
+  (KnownNat n, Dom f a) =>
+  f a ->
+  Sized f n a
+unsafeToSized' = unsafeToSized sNat
+{-# INLINE unsafeToSized' #-}
+
+{- | Construct a @Sized f n a@ by padding default value if the given list is short.
+
+ Since 0.7.0.0
+-}
+toSizedWithDefault ::
+  forall f (n :: Nat) a.
+  (CFreeMonoid f, Dom f a) =>
+  SNat (n :: Nat) ->
+  a ->
+  f a ->
+  Sized f n a
+toSizedWithDefault sn def xs =
+  let len = P.fromIntegral $ toNatural sn
+   in Sized $ ctake len xs <> creplicate (len - clength xs) def
+{-# INLINEABLE toSizedWithDefault #-}
+
+{- | 'toSizedWithDefault' with the result length inferred.
+
+ Since 0.7.0.0
+-}
+toSizedWithDefault' ::
+  forall f (n :: Nat) a.
+  (KnownNat n, CFreeMonoid f, Dom f a) =>
+  a ->
+  f a ->
+  Sized f n a
+toSizedWithDefault' = toSizedWithDefault sNat
+{-# INLINE toSizedWithDefault' #-}
+
+--------------------------------------------------------------------------------
+-- Querying
+--------------------------------------------------------------------------------
+
+--------------------------------------------------------------------------------
+--- Partitioning
+--------------------------------------------------------------------------------
+
+{- | 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.7.0.0
+-}
+data Partitioned f n a where
+  Partitioned ::
+    (Dom f a) =>
+    SNat n ->
+    Sized f n a ->
+    SNat m ->
+    Sized f m a ->
+    Partitioned f (n + m) a
+
+{- | Take the initial segment as long as elements satisfys the predicate.
+
+ Since 0.7.0.0
+-}
+takeWhile ::
+  forall f (n :: Nat) a.
+  (Dom f a, CFreeMonoid f) =>
+  (a -> Bool) ->
+  Sized f n a ->
+  SomeSized f a
+takeWhile = (toSomeSized .) . coerce (ctakeWhile @f @a)
+{-# INLINE takeWhile #-}
+
+{- | Drop the initial segment as long as elements satisfys the predicate.
+
+ Since 0.7.0.0
+-}
+dropWhile ::
+  forall f (n :: Nat) a.
+  (CFreeMonoid f, Dom f a) =>
+  (a -> Bool) ->
+  Sized f n a ->
+  SomeSized f a
+dropWhile = (toSomeSized .) . coerce (cdropWhile @f @a)
+{-# INLINE dropWhile #-}
+
+{- | Split the sequence into the longest prefix
+   of elements that satisfy the predicate
+   and the rest.
+
+ Since 0.7.0.0
+-}
+span ::
+  forall f (n :: Nat) a.
+  (CFreeMonoid f, Dom f a) =>
+  (a -> Bool) ->
+  Sized f n a ->
+  Partitioned f n a
+span = (unsafePartitioned @n .) . coerce (cspan @f @a)
+{-# INLINE span #-}
+
+{- | Split the sequence into the longest prefix
+   of elements that do not satisfy the
+   predicate and the rest.
+
+ Since 0.7.0.0
+-}
+break ::
+  forall f (n :: Nat) a.
+  (CFreeMonoid f, Dom f a) =>
+  (a -> Bool) ->
+  Sized f n a ->
+  Partitioned f n a
+break = (unsafePartitioned @n .) . coerce (cbreak @f @a)
+{-# INLINE break #-}
+
+{- | Split the sequence in two parts, the first one containing those elements that satisfy the predicate and the second one those that don't.
+
+ Since 0.7.0.0
+-}
+partition ::
+  forall f (n :: Nat) a.
+  (CFreeMonoid f, Dom f a) =>
+  (a -> Bool) ->
+  Sized f n a ->
+  Partitioned f n a
+partition = (unsafePartitioned @n .) . coerce (cpartition @f @a)
+{-# INLINE partition #-}
+
+unsafePartitioned ::
+  forall (n :: Nat) f a.
+  (CFreeMonoid f, Dom f a) =>
+  (f a, f a) ->
+  Partitioned f n a
+unsafePartitioned (l, r) =
+  case (toSomeSized l, toSomeSized r) of
+    ( SomeSized (lenL :: SNat nl) ls
+      , SomeSized (lenR :: SNat nr) rs
+      ) ->
+        gcastWith
+          ( unsafeCoerce $ Refl @() ::
+              n :~: nl + nr
+          )
+          $ Partitioned lenL ls lenR rs
+
+--------------------------------------------------------------------------------
+--- Searching
+--------------------------------------------------------------------------------
+
+{- | Membership test; see also 'notElem'.
+
+ Since 0.7.0.0
+-}
+elem ::
+  forall f (n :: Nat) a.
+  (CFoldable f, Dom f a, Eq a) =>
+  a ->
+  Sized f n a ->
+  Bool
+elem = coerce $ celem @f @a
+{-# INLINE elem #-}
+
+{- | Negation of 'elem'.
+
+ Since 0.7.0.0
+-}
+notElem ::
+  forall f (n :: Nat) a.
+  (CFoldable f, Dom f a, Eq a) =>
+  a ->
+  Sized f n a ->
+  Bool
+notElem = coerce $ cnotElem @f @a
+{-# INLINE notElem #-}
+
+{- | Find the element satisfying the predicate.
+
+ Since 0.7.0.0
+-}
+find ::
+  forall f (n :: Nat) a.
+  (CFoldable f, Dom f a) =>
+  (a -> Bool) ->
+  Sized f n a ->
+  Maybe a
+find = coerce $ cfind @f @a
+{-# INLINE [1] find #-}
+
+{-# RULES
+"find/List" [~1] forall p.
+  find p =
+    L.find @[] p . runSized
+"find/Vector" [~1] forall p.
+  find p =
+    V.find p . runSized
+"find/Storable Vector" [~1] forall (p :: SV.Storable a => a -> Bool).
+  find p =
+    SV.find p . runSized
+"find/Unboxed Vector" [~1] forall (p :: UV.Unbox a => a -> Bool).
+  find p =
+    UV.find p . runSized
+  #-}
+
+{- | @'findIndex' p xs@ find the element satisfying @p@ and returns its index if exists.
+
+ Since 0.7.0.0
+-}
+findIndex ::
+  forall f (n :: Nat) a.
+  (CFoldable f, Dom f a) =>
+  (a -> Bool) ->
+  Sized f n a ->
+  Maybe Int
+findIndex = coerce $ cfindIndex @f @a
+{-# INLINE findIndex #-}
+
+{- | 'Ordinal' version of 'findIndex'.
+
+ Since 0.7.0.0
+-}
+sFindIndex ::
+  forall f (n :: Nat) a.
+  (KnownNat (n :: Nat), CFoldable f, Dom f a) =>
+  (a -> Bool) ->
+  Sized f n a ->
+  Maybe (Ordinal n)
+sFindIndex = (fmap toEnum .) . coerce (cfindIndex @f @a)
+{-# INLINE sFindIndex #-}
+
+{- | @'findIndices' p xs@ find all elements satisfying @p@ and returns their indices.
+
+ Since 0.7.0.0
+-}
+findIndices ::
+  forall f (n :: Nat) a.
+  (CFoldable f, Dom f a) =>
+  (a -> Bool) ->
+  Sized f n a ->
+  [Int]
+findIndices = coerce $ cfindIndices @f @a
+{-# INLINE findIndices #-}
+{-# SPECIALIZE findIndices :: (a -> Bool) -> Sized [] n a -> [Int] #-}
+
+{- | 'Ordinal' version of 'findIndices'.
+
+ Since 0.7.0.0
+-}
+sFindIndices ::
+  forall f (n :: Nat) a.
+  (CFoldable f, Dom f a, KnownNat (n :: Nat)) =>
+  (a -> Bool) ->
+  Sized f n a ->
+  [Ordinal n]
+sFindIndices p = P.fmap (toEnum . P.fromIntegral) . findIndices p
+{-# INLINE sFindIndices #-}
+
+{-# RULES
+"Foldable.sum/Vector"
+  F.sum =
+    V.sum . runSized
+  #-}
+
+{- | Returns the index of the given element in the list, if exists.
+
+ Since 0.7.0.0
+-}
+elemIndex ::
+  forall f (n :: Nat) a.
+  (CFoldable f, Eq a, Dom f a) =>
+  a ->
+  Sized f n a ->
+  Maybe Int
+elemIndex = coerce $ celemIndex @f @a
+{-# INLINE elemIndex #-}
+
+{- | Ordinal version of 'elemIndex'.
+   Since 0.7.0.0, we no longer do boundary check inside the definition.
+
+   Since 0.7.0.0
+-}
+sElemIndex
+  , sUnsafeElemIndex ::
+    forall f (n :: Nat) a.
+    (KnownNat n, CFoldable f, Dom f a, Eq a) =>
+    a ->
+    Sized f n a ->
+    Maybe (Ordinal n)
+sElemIndex = (fmap toEnum .) . coerce (celemIndex @f @a)
+{-# INLINE sElemIndex #-}
+
+-- | Since 0.5.0.0 (type changed)
+sUnsafeElemIndex = sElemIndex
+{-# DEPRECATED sUnsafeElemIndex "No difference with sElemIndex; use sElemIndex instead." #-}
+
+{- | Returns all indices of the given element in the list.
+
+ Since 0.7.0.0
+-}
+elemIndices ::
+  forall f (n :: Nat) a.
+  (CFoldable f, Dom f a, Eq a) =>
+  a ->
+  Sized f n a ->
+  [Int]
+elemIndices = coerce $ celemIndices @f @a
+{-# INLINE elemIndices #-}
+
+{- | Ordinal version of 'elemIndices'
+
+ Since 0.7.0.0
+-}
+sElemIndices ::
+  forall f (n :: Nat) a.
+  (CFoldable f, KnownNat (n :: Nat), Dom f a, Eq a) =>
+  a ->
+  Sized f n a ->
+  [Ordinal n]
+sElemIndices = (fmap toEnum .) . elemIndices
+{-# INLINE sElemIndices #-}
+
+--------------------------------------------------------------------------------
+-- Views and Patterns
+--------------------------------------------------------------------------------
+
+{- $ViewsAndPatterns #ViewsAndPatterns#
+
+   With GHC's @ViewPatterns@ and @PatternSynonym@ extensions,
+   we can pattern-match on arbitrary @Sized f n a@ if @f@ is list-like functor.
+   Curretnly, there are two direction view and patterns: Cons and Snoc.
+   Assuming underlying sequence type @f@ has O(1) implementation for 'cnull', 'chead'
+   (resp. 'clast') and 'ctail' (resp. 'cinit'), We can view and pattern-match on
+   cons (resp. snoc) of @Sized f n a@ in O(1).
+-}
+
+{- $views #views#
+
+   With @ViewPatterns@ extension, we can pattern-match on 'Sized' value as follows:
+
+@
+slen :: ('KnownNat' n, 'Dom f a' f) => 'Sized' f n a -> 'SNat' n
+slen ('viewCons' -> 'NilCV')    = 'SZ'
+slen ('viewCons' -> _ ':-' as) = 'SS' (slen as)
+slen _                          = error "impossible"
+@
+
+   The constraint @('KnownNat' n, 'Dom f 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 :: ('KnownNat' n, 'Dom f a' f) => 'Sized' f n a -> 'SNat' n
+slen ('viewSnoc' -> 'NilSV')     = 'SZ'
+slen ('viewSnoc' -> as '-::' _) = 'SS' (slen as)
+@
+-}
+
+{- | View of the left end of sequence (cons-side).
+
+ Since 0.7.0.0
+-}
+data ConsView f n a where
+  NilCV :: ConsView f (0) a
+  (:-) ::
+    (KnownNat n, KnownNat (1 + n)) =>
+    a ->
+    Sized f n a ->
+    ConsView f (1 + n) a
+
+infixr 5 :-
+
+{- | Case analysis for the cons-side of sequence.
+
+ Since 0.5.0.0 (type changed)
+-}
+viewCons ::
+  forall f (n :: Nat) a.
+  (KnownNat n, CFreeMonoid f, Dom f a) =>
+  Sized f n a ->
+  ConsView f n a
+viewCons sz = case zeroOrSucc $ sNat @n of
+  IsZero -> NilCV
+  IsSucc n' ->
+    withKnownNat n' $
+      withKnownNat (sOne %+ n') $
+        case uncons' n' sz of
+          Uncons a xs -> a :- xs
+
+{- | View of the left end of sequence (snoc-side).
+
+ Since 0.7.0.0
+-}
+data SnocView f n a where
+  NilSV :: SnocView f (0) a
+  (:-::) :: KnownNat (n :: Nat) => Sized f n a -> a -> SnocView f (n + 1) a
+
+infixl 5 :-::
+
+{- | Case analysis for the snoc-side of sequence.
+
+ Since 0.5.0.0 (type changed)
+-}
+viewSnoc ::
+  forall f (n :: Nat) a.
+  (KnownNat n, CFreeMonoid f, Dom f a) =>
+  Sized f n a ->
+  SnocView f n a
+viewSnoc sz = case zeroOrSucc (sNat @n) of
+  IsZero -> NilSV
+  IsSucc (n' :: SNat n') ->
+    withKnownNat n' $
+      case unsnoc' n' sz of
+        Unsnoc (xs :: Sized f m a) a ->
+          gcastWith
+            (unsafeCoerce (Refl @()) :: n' :~: m)
+            $ xs :-:: a
+
+{- $patterns #patterns#
+
+   So we can pattern match on both end of sequence via views, but
+   it is rather clumsy to nest it. For example:
+
+@
+nextToHead :: ('Dom f a' f, 'KnownNat' 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 :: ('Dom f a' f, 'KnownNat' n) => 'Sized' f ('S' ('S' n)) a -> a
+nextToHead (_ ':<' a ':<' _) = a
+@
+
+   Of course, we can also rewrite above @slen@ example usNat @PatternSynonyms@:
+
+@
+slen :: ('KnownNat' n, 'Dom f a' f) => 'Sized' f n a -> 'SNat' n
+slen 'Nil'      = 'SZ'
+slen (_ ':<' as) = 'SS' (slen as)
+@
+
+   So, we can use @':<'@ and @'Nil'@ (resp. @':>'@ and @'Nil'@) to
+   pattern-match directly on cons-side (resp. snoc-side) as we usually do for lists.
+   @'Nil'@, @':<'@, and @':>'@ are neither functions nor data constructors,
+   but pattern synonyms so we cannot use them in expression contexts.
+   For more detail on pattern synonyms, see
+   <http://www.haskell.org/ghc/docs/latest/html/users_guide/syntax-extns.html#pattern-synonyms GHC Users Guide>
+   and
+   <https://ghc.haskell.org/trac/ghc/wiki/PatternSynonyms HaskellWiki>.
+-}
+
+infixr 5 :<
+
+-- | Pattern synonym for cons-side uncons.
+pattern (:<) ::
+  forall (f :: Type -> Type) a (n :: Nat).
+  (Dom f a, KnownNat n, CFreeMonoid f) =>
+  forall (n1 :: Nat).
+  (n ~ (1 + n1), KnownNat n1) =>
+  a ->
+  Sized f n1 a ->
+  Sized f n a
+pattern a :< as <-
+  (viewCons -> a :- as)
+  where
+    a :< as = a <| as
+
+chkNil ::
+  forall f (n :: Nat) a.
+  (KnownNat n) =>
+  Sized f n a ->
+  ZeroOrSucc n
+chkNil = const $ zeroOrSucc $ sNat @n
+
+-- | Pattern synonym for a nil sequence.
+pattern Nil ::
+  forall f (n :: Nat) a.
+  (KnownNat n, CFreeMonoid f, Dom f a) =>
+  (n ~ 0) =>
+  Sized f n a
+pattern Nil <-
+  (chkNil -> IsZero)
+  where
+    Nil = empty
+
+infixl 5 :>
+
+-- | Pattern synonym for snoc-side unsnoc.
+pattern (:>) ::
+  forall (f :: Type -> Type) a (n :: Nat).
+  (Dom f a, KnownNat n, CFreeMonoid f) =>
+  forall (n1 :: Nat).
+  (n ~ (n1 + 1), KnownNat n1) =>
+  Sized f n1 a ->
+  a ->
+  Sized f n a
+pattern a :> b <-
+  (viewSnoc -> a :-:: b)
+  where
+    a :> b = a |> b
+
+{-# COMPLETE (:<), Nil #-}
+
+{-# COMPLETE (:>), Nil #-}
+
+class Dom f a => DomC f a
+
+instance Dom f a => DomC f a
+
+-- | Applicative instance, generalizing @'Data.Monoid.ZipList'@.
+instance
+  ( Functor f
+  , CFreeMonoid f
+  , CZip f
+  , KnownNat n
+  , forall a. DomC f a
+  ) =>
+  P.Applicative (Sized f (n :: Nat))
+  where
+  {-# SPECIALIZE instance KnownNat n => P.Applicative (Sized [] (n :: Nat)) #-}
+  {-# SPECIALIZE instance KnownNat n => P.Applicative (Sized Seq.Seq (n :: Nat)) #-}
+  {-# SPECIALIZE instance KnownNat n => P.Applicative (Sized V.Vector (n :: Nat)) #-}
+
+  pure (x :: a) =
+    withDict (Dict @(DomC f a)) $
+      replicate' x
+  {-# INLINE pure #-}
+
+  (fs :: Sized f n (a -> b)) <*> (xs :: Sized f n a) =
+    withDict (Dict @(DomC f b)) $
+      withDict (Dict @(DomC f a)) $
+        withDict (Dict @(DomC f (a -> b))) $
+          zipWithSame ($) fs xs
+  {-# INLINE [1] (<*>) #-}
+
+{-# RULES
+"<*>/List" [~1] forall fs xs.
+  Sized fs <*> Sized xs =
+    Sized (getZipList (ZipList fs <*> ZipList xs))
+"<*>/Seq" [~1] forall fs xs.
+  Sized fs <*> Sized xs =
+    Sized (Seq.zipWith ($) fs xs)
+"<*>/Vector" [~1] forall fs xs.
+  Sized fs <*> Sized xs =
+    Sized (V.zipWith ($) fs xs)
+  #-}
+
+instance
+  (CFreeMonoid f, KnownNat (n :: Nat)) =>
+  CPointed (Sized f n)
+  where
+  cpure = replicate'
+
+instance
+  (CFreeMonoid f, CZip f) =>
+  CApplicative (Sized f n)
+  where
+  pair = zipSame
+  (<.>) = zipWithSame ($)
+  (<.) = P.const
+  (.>) = P.flip P.const
+
+{- | __N.B.__ Since @calign@ is just zipping for fixed @n@,
+   we require more strong 'CZip' constraint here.
+-}
+instance (CZip f, CFreeMonoid f) => CSemialign (Sized f n) where
+  calignWith =
+    coerce (\f -> czipWith @f @a @b @c ((f .) . These)) ::
+      forall a b c.
+      (Dom f a, Dom f b, Dom f c) =>
+      (These a b -> c) ->
+      Sized f n a ->
+      Sized f n b ->
+      Sized f n c
+  {-# INLINE [1] calignWith #-}
+  calign =
+    coerce $ czipWith @f @a @b These ::
+      forall a b.
+      (Dom f a, Dom f b, Dom f (These a b)) =>
+      Sized f n a ->
+      Sized f n b ->
+      Sized f n (These a b)
+  {-# INLINE [1] calign #-}
+
+instance (CZip f, CFreeMonoid f) => CZip (Sized f n) where
+  czipWith =
+    coerce $ czipWith @f @a @b @c ::
+      forall a b c.
+      (Dom f a, Dom f b, Dom f c) =>
+      (a -> b -> c) ->
+      Sized f n a ->
+      Sized f n b ->
+      Sized f n c
+  {-# INLINE [1] czipWith #-}
+  czip =
+    coerce $ czip @f @a @b ::
+      forall a b.
+      (Dom f a, Dom f b, Dom f (a, b)) =>
+      Sized f n a ->
+      Sized f n b ->
+      Sized f n (a, b)
+  {-# INLINE [1] czip #-}
+
+instance
+  (KnownNat (n :: Nat), CZip f, CFreeMonoid f) =>
+  CRepeat (Sized f n)
+  where
   crepeat = replicate'
   {-# INLINE [1] crepeat #-}
 
diff --git a/src/Data/Sized/Builtin.hs b/src/Data/Sized/Builtin.hs
--- a/src/Data/Sized/Builtin.hs
+++ b/src/Data/Sized/Builtin.hs
@@ -1,1005 +1,4 @@
-{-# LANGUAGE CPP, ConstraintKinds, DataKinds, FlexibleContexts             #-}
-{-# LANGUAGE FlexibleInstances, GADTs, KindSignatures                      #-}
-{-# LANGUAGE MultiParamTypeClasses, NoImplicitPrelude                      #-}
-{-# LANGUAGE NoMonomorphismRestriction, NoStarIsType, PatternSynonyms      #-}
-{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables, TypeApplications  #-}
-{-# LANGUAGE TypeInType, TypeOperators, UndecidableInstances, ViewPatterns #-}
-{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
-{-# OPTIONS_GHC -fplugin Data.Singletons.TypeNats.Presburger #-}
--- | This module exports provides the functionality to make length-parametrized types
---   from existing 'CFreeMonoid' sequential types,
---   parametrised with GHC's built in 'Nat' kind.
---
---   Most of the complexity of operations on @'Sized' f n a@ are the same as
---   original operations on @f@. For example, '!!' is O(1) for
---   @Sized Vector n a@ but O(i) for @Sized [] n a@.
---
---  This module also provides powerful view types and pattern synonyms to
---  inspect the sized sequence. See <#ViewsAndPatterns Views and Patterns> for more detail.
-module Data.Sized.Builtin
-  ( -- * Main Data-types
-    Sized(), SomeSized, pattern SomeSized, Ordinal,
-    DomC(),
-    -- * Accessors
-    -- ** Length information
-    length, sLength, null,
-    -- ** Indexing
-    (!!), (%!!), index, sIndex, head, last,
-    uncons, uncons', Uncons, pattern Uncons,
-    unsnoc, unsnoc', Unsnoc, pattern Unsnoc,
-    -- ** Slicing
-    tail, init, take, takeAtMost, drop, splitAt, splitAtMost,
-    -- * Construction
-    -- ** Initialisation
-    empty, singleton, toSomeSized, replicate, replicate', generate, generate',
-    -- ** Concatenation
-    cons, (<|), snoc, (|>), append, (++), concat,
-    -- ** Zips
-    zip, zipSame, zipWith, zipWithSame, unzip, unzipWith,
-    -- * Transformation
-    map, reverse, intersperse, nub, sort, sortBy, insert, insertBy,
-    -- * Conversion
-    -- ** List
-    toList, fromList, fromList', unsafeFromList, unsafeFromList',
-    fromListWithDefault, fromListWithDefault',
-    -- ** Base container
-    unsized,
-    toSized, toSized', unsafeToSized, unsafeToSized',
-    toSizedWithDefault, toSizedWithDefault',
-    -- * Querying
-    -- ** Partitioning
-    Partitioned(), pattern Partitioned,
-    takeWhile, dropWhile, span, break, partition,
-    -- ** Searching
-    elem, notElem, find, findIndex, sFindIndex,
-    findIndices, sFindIndices,
-    elemIndex, sElemIndex, sUnsafeElemIndex, elemIndices, sElemIndices,
-    -- * Views and Patterns
-    -- $ViewsAndPatterns
-
-    -- ** Views
-    -- $views
-
-    -- ** Patterns
-    -- $patterns
-
-    -- ** Definitions
-    viewCons, ConsView,
-    pattern (:-), pattern NilCV,
-    viewSnoc, SnocView,
-    pattern (:-::), pattern NilSV,
-
-    pattern Nil, pattern (:<), pattern (:>),
-  ) where
-import           Data.Sized (DomC)
-import qualified Data.Sized as S
-
-import           Control.Subcategory
-import           Data.Coerce                  (coerce)
-import           Data.Kind                    (Type)
-import           Data.Maybe                   (fromJust)
-import           Data.Singletons.Prelude      (SNum ((%+)), SingI (sing))
-import           Data.Singletons.Prelude.Enum (PEnum (..))
-import           Data.Singletons.TypeLits     (SNat, withKnownNat)
-import qualified Data.Sized.Internal          as Internal
-import           Data.Type.Natural            (IsPeano (toNatural, zeroOrSucc),
-                                               Min, PeanoOrder (plusMonotoneR))
-import           Data.Type.Natural.Class      (ZeroOrSucc (IsSucc, IsZero),
-                                               type (-.))
-import qualified Data.Type.Ordinal            as O
-import           GHC.TypeNats                 (KnownNat, Nat, type (*),
-                                               type (+), type (-), type (<=))
-import           Prelude                      (Bool (..), Eq, Int, Maybe,
-                                               Monoid, Ord, Ordering, const,
-                                               uncurry, ($), (.))
-import qualified Prelude                      as P
-import           Proof.Propositional          (IsTrue (Witness), withWitness)
-
-type Ordinal = (O.Ordinal :: Nat -> Type)
-type a < b = a + 1 <= b
-
--- | @Sized@ wraps a sequential type 'f' and makes length-parametrized version.
---
--- Here, 'f' must satisfy @'CFreeMonoid' f@ and @Dom f a@.
---
--- Since 0.2.0.0
-type Sized = (Internal.Sized :: (Type -> Type) -> Nat -> Type -> Type)
-
--- | 'Sized' sequence with the length is existentially quantified.
---   This type is used mostly when the return type's length cannot
---   be statically determined beforehand.
---
--- @SomeSized' sn xs :: SomeSized' f a@ stands for the 'Sized' sequence
--- @xs@ of element type @a@ and length @sn@.
---
--- Since 0.7.0.0
-type SomeSized f a = S.SomeSized' f Nat a
-
-pattern SomeSized
-  :: forall (f :: Type -> Type) a. ()
-  => forall (n :: Nat). SNat n
-  -> Sized f n a -> SomeSized f a
-{-# COMPLETE SomeSized #-}
-pattern SomeSized n s = S.SomeSized'  n s
-
--- | 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.8.0.0 (type changed)
-{-# INLINE length #-}
-length :: (Dom f a, KnownNat n) => Sized f n a -> Int
-length = S.length @Nat
-
--- | @Sing@ version of 'length'.
---
--- Since 0.8.0.0 (type changed)
-sLength :: (Dom f a, KnownNat n) => Sized f n a -> SNat n
-{-# INLINE sLength #-}
-sLength = S.sLength @Nat
-
--- | Test if the sequence is empty or not.
---
--- Since 0.7.0.0
-null :: (Dom f a, CFoldable f) => Sized f n a -> Bool
-{-# INLINE null #-}
-null = S.null @Nat
-
---------------------------------------------------------------------------------
---- Indexing
---------------------------------------------------------------------------------
-
--- | (Unsafe) indexing with @Int@s.
---   If you want to check boundary statically, use '%!!' or 'sIndex'.
---
--- Since 0.7.0.0
-(!!) :: forall f m a. (Dom f a, CFoldable f, (1 <= m)) => Sized f m a -> Int -> a
-{-# INLINE (!!) #-}
-(!!) = coerce $ cindex @f @a
-
--- | Safe indexing with 'Ordinal's.
---
--- Since 0.7.0.0
-(%!!) :: (Dom f c, CFoldable f) => Sized f n c -> Ordinal n -> c
-{-# INLINE (%!!) #-}
-(%!!) = (S.%!!) @Nat
-
--- | Flipped version of '!!'.
---
--- Since 0.7.0.0
-index
-  :: (Dom f a, CFoldable f, (1 <= m))
-  => Int -> Sized f m a -> a
-{-# INLINE index #-}
-index = P.flip (!!)
-
--- | Flipped version of '%!!'.
---
--- Since 0.7.0.0
-sIndex :: (Dom f c, CFoldable f) => Ordinal n -> Sized f n c -> c
-{-# INLINE sIndex #-}
-sIndex = S.sIndex @Nat
-
--- | 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.7.0.0
-head :: forall f n a. (Dom f a, CFoldable f, (1 <= n)) => Sized f n a -> a
-{-# INLINE head #-}
-head = coerce $ chead @f @a
-
--- | 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.7.0.0
-last :: forall f n a. (Dom f a, CFoldable f, (0 < n)) => Sized f n a -> a
-{-# INLINE last #-}
-last = coerce $ clast @f @a
-
--- | 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.7.0.0
-uncons
-  :: forall f n a.
-    (Dom f a, KnownNat n, CFreeMonoid f, (0 < n))
-  => Sized f n a -> Uncons f n a
-{-# INLINE uncons #-}
-uncons =
-  uncurry (Uncons @f @(Pred n) @a) . coerce (fromJust . cuncons @f @a)
-
--- | 'uncons' with explicit specified length @n@
---
---   Since 0.7.0.0
-uncons'
-  :: (Dom f a, KnownNat n, CFreeMonoid f, (0 < n))
-  => Sized f n a
-  -> Uncons f n a
-{-# INLINE uncons' #-}
-uncons' = 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.7.0.0
-unsnoc
-  :: (Dom f a, KnownNat n, CFreeMonoid f, (0 < n))
-  => Sized f n a -> Unsnoc f n a
-{-# INLINE unsnoc #-}
-unsnoc = P.undefined
-
--- | 'unsnoc'' with explicit specified length @n@
---
---   Since 0.7.0.0
-unsnoc' :: (Dom f a, KnownNat n, CFreeMonoid f) => proxy n -> Sized f (n + 1) a -> Unsnoc f (n + 1) a
-{-# INLINE unsnoc' #-}
-unsnoc' = S.unsnoc' @Nat
-
-data Uncons f n a where
-  Uncons :: forall f n a. KnownNat n
-    => a -> Sized f n a -> Uncons f (1 + n) a
-
-
-type Unsnoc f (n :: Nat) a = S.Unsnoc f n a
-
-pattern Unsnoc
-  :: forall (f :: Type -> Type) (n :: Nat) a. ()
-  => forall (n1 :: Nat). (n ~ Succ n1)
-  => Sized f n1 a -> a -> Unsnoc f n a
-pattern Unsnoc xs x = S.Unsnoc xs x
-
--- | 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.7.0.0
-tail :: (Dom f a, CFreeMonoid f) => Sized f (1 + n) a -> Sized f n a
-{-# INLINE tail #-}
-tail = S.tail @Nat
-
--- | 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.7.0.0
-init :: (Dom f a, CFreeMonoid f) => Sized f (n + 1) a -> Sized f n a
-{-# INLINE init #-}
-init = S.init @Nat
-
--- | @take k xs@ takes first @k@ element of @xs@ where
--- the length of @xs@ should be larger than @k@.
---
--- Since 0.7.0.0
-take
-  :: forall n f m a. (Dom f a, CFreeMonoid f, (n <= m))
-  => SNat n -> Sized f m a -> Sized f n a
-{-# INLINE take #-}
-take = coerce $ ctake @f @a . P.fromIntegral . toNatural @Nat @n
-
--- | @'takeAtMost' k xs@ takes first at most @k@ elements of @xs@.
---
--- Since 0.7.0.0
-takeAtMost
-  :: (Dom f a, CFreeMonoid f)
-  => SNat n -> Sized f m a -> Sized f (Min n m) a
-{-# INLINE takeAtMost #-}
-takeAtMost = S.takeAtMost @Nat
-
--- | @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@.
---
--- Since 0.7.0.0
-drop
-  :: forall n f m a. (Dom f a, CFreeMonoid f, (n <= m))
-  => SNat n -> Sized f m a -> Sized f (m - n) a
-{-# INLINE drop #-}
-drop = coerce $ cdrop @f @a . P.fromIntegral . toNatural @Nat @n
-
--- | @splitAt k xs@ split @xs@ at @k@, where
--- the length of @xs@ should be less than or equal to @k@.
---
--- Since 0.7.0.0
-splitAt
-  :: forall n f m a. (Dom f a, CFreeMonoid f, (n <= m))
-  => SNat n -> Sized f m a -> (Sized f n a, Sized f (m - n) a)
-{-# INLINE splitAt #-}
-splitAt = coerce $ csplitAt @f @a . P.fromIntegral . toNatural @Nat
-
--- | @splitAtMost k xs@ split @xs@ at @k@.
---   If @k@ exceeds the length of @xs@, then the second result value become empty.
---
--- Since 0.7.0.0
-splitAtMost
-  :: (Dom f a, CFreeMonoid f)
-  => SNat n -> Sized f m a
-  -> (Sized f (Min n m) a, Sized f (m -. n) a)
-{-# INLINE splitAtMost #-}
-splitAtMost = S.splitAtMost @Nat
-
---------------------------------------------------------------------------------
--- Construction
---------------------------------------------------------------------------------
-
---------------------------------------------------------------------------------
---- Initialisation
---------------------------------------------------------------------------------
-
--- | Empty sequence.
---
--- Since 0.7.0.0 (type changed)
-empty :: (Dom f a, Monoid (f a)) => Sized f 0 a
-{-# INLINE empty #-}
-empty = S.empty @Nat
-
--- | Sequence with one element.
---
--- Since 0.7.0.0
-singleton :: (Dom f a, CFreeMonoid f) => a -> Sized f 1 a
-{-# INLINE singleton #-}
-singleton = S.singleton @Nat
-
-
--- | Consruct the 'Sized' sequence from base type, but
---   the length parameter is dynamically determined and
---   existentially quantified; see also 'SomeSized''.
---
--- Since 0.7.0.0
-toSomeSized :: (Dom f a, CFoldable f) => f a -> SomeSized f a
-{-# INLINE toSomeSized #-}
-toSomeSized = S.toSomeSized @Nat
-
--- | Replicates the same value.
---
--- Since 0.7.0.0
-replicate :: (Dom f a, CFreeMonoid f) => SNat n -> a -> Sized f n a
-{-# INLINE replicate #-}
-replicate = S.replicate @Nat
-
--- | 'replicate' with the length inferred.
---
--- Since 0.7.0.0
-replicate' :: (Dom f a, KnownNat n, CFreeMonoid f) => a -> Sized f n a
-{-# INLINE replicate' #-}
-replicate' = S.replicate' @Nat
-
--- | Construct a sequence of the given length by applying the function to each index.
---
--- Since 0.7.0.0
-generate :: (Dom f a, CFreeMonoid f) => SNat n -> (Ordinal n -> a) -> Sized f n a
-{-# INLINE generate #-}
-generate = S.generate @Nat
-
--- | 'generate' with length inferred.
---
---   Since 0.8.0.0
-generate'
-  :: forall f n a. (KnownNat n, Dom f a, CFreeMonoid f) => (Ordinal n -> a) -> Sized f n a
-{-# INLINE generate' #-}
-generate' = S.generate' @Nat
-
---------------------------------------------------------------------------------
---- Concatenation
---------------------------------------------------------------------------------
-
--- | Append an element to the head of sequence.
---
--- Since 0.7.0.0
-cons :: (Dom f a, CFreeMonoid f) => a -> Sized f n a -> Sized f (1 + n) a
-{-# INLINE cons #-}
-cons = S.cons @Nat
-
--- | Append an element to the tail of sequence.
---
--- Since 0.7.0.0
-snoc :: (Dom f a, CFreeMonoid f) => Sized f n a -> a -> Sized f (n + 1) a
-{-# INLINE snoc #-}
-snoc = S.snoc @Nat
-
--- | Infix version of 'snoc'.
---
--- Since 0.7.0.0
-(<|) :: (Dom f a, CFreeMonoid f) => a -> Sized f n a -> Sized f (1 + n) a
-{-# INLINE (<|) #-}
-(<|) = (S.<|) @Nat
-
--- | Append an element to the tail of sequence.
---
--- Since 0.7.0.0
-(|>) :: (Dom f a, CFreeMonoid f) => Sized f n a -> a -> Sized f (n + 1) a
-{-# INLINE (|>) #-}
-(|>) = (S.|>) @Nat
-
--- | Infix version of 'append'.
---
--- Since 0.7.0.0
-(++) :: (Dom f a, CFreeMonoid f) => Sized f n a -> Sized f m a -> Sized f (n + m) a
-{-# INLINE (++) #-}
-(++) = (S.++) @Nat
-
--- | Append two lists.
---
--- Since 0.7.0.0
-append :: (Dom f a, CFreeMonoid f) => Sized f n a -> Sized f m a -> Sized f (n + m) a
-{-# INLINE append #-}
-append = S.append @Nat
-
--- | Concatenates multiple sequences into one.
---
--- Since 0.7.0.0
-concat
-  :: (Dom f a, Dom f' (f a), Dom f' (Sized f n a),
-      CFreeMonoid f, CFunctor f', CFoldable f'
-    ) => Sized f' m (Sized f n a) -> Sized f (m * n) a
-{-# INLINE concat #-}
-concat = S.concat @Nat
-
-
---------------------------------------------------------------------------------
---- Zips
---------------------------------------------------------------------------------
-
--- | Zipping two sequences. Length is adjusted to shorter one.
---
--- Since 0.7.0.0
-zip :: (Dom f a, Dom f b, Dom f (a, b), CZip f)
-  => Sized f n a -> Sized f m b -> Sized f (Min n m) (a, b)
-{-# INLINE zip #-}
-zip = S.zip @Nat
-
--- | 'zip' for the sequences of the same length.
---
--- Since 0.7.0.0
-zipSame :: (Dom f a, Dom f b, Dom f (a, b), CZip f)
-  => Sized f n a -> Sized f n b -> Sized f n (a, b)
-{-# INLINE zipSame #-}
-zipSame = S.zipSame @Nat
-
--- | Zipping two sequences with funtion. Length is adjusted to shorter one.
---
--- Since 0.7.0.0
-zipWith :: (Dom f a, Dom f b, Dom f c, CZip f, CFreeMonoid f)
-  => (a -> b -> c) -> Sized f n a -> Sized f m b -> Sized f (Min n m) c
-{-# INLINE zipWith #-}
-zipWith = S.zipWith @Nat
-
--- | 'zipWith' for the sequences of the same length.
---
--- Since 0.7.0.0
-zipWithSame
-  :: (Dom f a, Dom f b, Dom f c, CZip f, CFreeMonoid f)
-  => (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c
-{-# INLINE zipWithSame #-}
-zipWithSame = S.zipWithSame @Nat
-
--- | Unzipping the sequence of tuples.
---
--- Since 0.7.0.0
-unzip
-  :: (Dom f a, Dom f b, Dom f (a, b), CUnzip f)
-  => Sized f n (a, b) -> (Sized f n a, Sized f n b)
-{-# INLINE unzip #-}
-unzip = S.unzip @Nat
-
--- | Unzipping the sequence of tuples.
---
--- Since 0.7.0.0
-unzipWith
-  :: (Dom f a, Dom f b, Dom f c, CUnzip f)
-  => (a -> (b, c)) -> Sized f n a -> (Sized f n b, Sized f n c)
-{-# INLINE unzipWith #-}
-unzipWith = S.unzipWith @Nat
-
---------------------------------------------------------------------------------
--- Transformation
---------------------------------------------------------------------------------
-
--- | Map function.
---
--- Since 0.7.0.0
-map
-  :: (Dom f a, Dom f b, CFreeMonoid f)
-  => (a -> b) -> Sized f n a -> Sized f n b
-{-# INLINE map #-}
-map = S.map @Nat
-
--- | Reverse function.
---
--- Since 0.7.0.0
-reverse :: (Dom f a, CFreeMonoid f) => Sized f n a -> Sized f n a
-{-# INLINE reverse #-}
-reverse = S.reverse @Nat
-
--- | Intersperces.
---
--- Since 0.7.0.0
-intersperse
-  :: (Dom f a, CFreeMonoid f)
-  => a -> Sized f n a -> Sized f ((2 * n) -. 1) a
-{-# INLINE intersperse #-}
-intersperse = S.intersperse @Nat
-
--- | Remove all duplicates.
---
--- Since 0.7.0.0
-nub :: (Dom f a, Eq a, CFreeMonoid f) => Sized f n a -> SomeSized f a
-{-# INLINE nub #-}
-nub = S.nub @Nat
-
--- | Sorting sequence by ascending order.
---
--- Since 0.7.0.0
-sort :: (Dom f a, CFreeMonoid f, Ord a) => Sized f n a -> Sized f n a
-{-# INLINE sort #-}
-sort = S.sort @Nat
-
--- | Generalized version of 'sort'.
---
--- Since 0.7.0.0
-sortBy
-  :: (Dom f a, CFreeMonoid f)
-  => (a -> a -> Ordering)
-  -> Sized f n a -> Sized f n a
-{-# INLINE sortBy #-}
-sortBy = S.sortBy @Nat
-
--- | Insert new element into the presorted sequence.
---
--- Since 0.7.0.0
-insert
-  :: (Dom f a, CFreeMonoid f, Ord a)
-  => a -> Sized f n a -> Sized f (n + 1) a
-{-# INLINE insert #-}
-insert = S.insert @Nat
-
--- | Generalized version of 'insert'.
---
--- Since 0.7.0.0
-{-# INLINE insertBy #-}
-insertBy
-  :: (Dom f a, CFreeMonoid f)
-  => (a -> a -> Ordering) -> a -> Sized f n a -> Sized f (n + 1) a
-insertBy = S.insertBy @Nat
-
---------------------------------------------------------------------------------
--- Conversion
---------------------------------------------------------------------------------
-
---------------------------------------------------------------------------------
---- List
---------------------------------------------------------------------------------
-
--- | Convert to list.
---
--- Since 0.7.0.0
-{-# INLINE toList #-}
-toList :: (Dom f a, CFoldable f) => Sized f n a -> [a]
-toList = S.toList @Nat
-
--- | 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.7.0.0 (type changed)
-{-# INLINE fromList #-}
-fromList :: (Dom f a, CFreeMonoid f) => SNat n -> [a] -> Maybe (Sized f n a)
-fromList = S.fromList @Nat
-
--- | 'fromList' with the result length inferred.
---
--- Since 0.7.0.0
-{-# INLINE fromList' #-}
-fromList' :: (Dom f a, CFreeMonoid f, KnownNat n) => [a] -> Maybe (Sized f n a)
-fromList' = S.fromList' @Nat
-
--- | Unsafe version of 'fromList'. If the length of the given list does not
---   equal to @n@, then something unusual happens.
---
--- Since 0.7.0.0
-{-# INLINE unsafeFromList #-}
-unsafeFromList :: (Dom f a, CFreeMonoid f) => SNat n -> [a] -> Sized f n a
-unsafeFromList = S.unsafeFromList @Nat
-
--- | 'unsafeFromList' with the result length inferred.
---
--- Since 0.7.0.0
-{-# INLINE unsafeFromList' #-}
-unsafeFromList' :: (Dom f a, KnownNat n, CFreeMonoid f) => [a] -> Sized f n a
-unsafeFromList' = S.unsafeFromList' @Nat
-
--- | Construct a @Sized f n a@ by padding default value if the given list is short.
---
---   Since 0.5.0.0 (type changed)
-{-# INLINE fromListWithDefault #-}
-fromListWithDefault :: (Dom f a, CFreeMonoid f) => SNat n -> a -> [a] -> Sized f n a
-fromListWithDefault = S.fromListWithDefault @Nat
-
--- | 'fromListWithDefault' with the result length inferred.
---
--- Since 0.7.0.0
-{-# INLINE fromListWithDefault' #-}
-fromListWithDefault' :: (Dom f a, KnownNat n, CFreeMonoid f)
-  => a -> [a] -> Sized f n a
-fromListWithDefault' = S.fromListWithDefault' @Nat
-
---------------------------------------------------------------------------------
---- Base containes
---------------------------------------------------------------------------------
-
--- | Forget the length and obtain the wrapped base container.
---
--- Since 0.7.0.0
-{-# INLINE unsized #-}
-unsized :: Sized f n a -> f a
-unsized = S.unsized @Nat
-
--- | 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.7.0.0
-{-# INLINE toSized #-}
-toSized :: (Dom f a, CFreeMonoid f) => SNat n -> f a -> Maybe (Sized f n a)
-toSized = S.toSized @Nat
-
--- | 'toSized' with the result length inferred.
---
--- Since 0.7.0.0
-{-# INLINE toSized' #-}
-toSized' :: (Dom f a, CFreeMonoid f, KnownNat n) => f a -> Maybe (Sized f n a)
-toSized' = S.toSized' @Nat
-
--- | Unsafe version of 'toSized'. If the length of the given list does not
---   equal to @n@, then something unusual happens.
---
--- Since 0.7.0.0
-{-# INLINE unsafeToSized #-}
-unsafeToSized :: SNat n -> f a -> Sized f n a
-unsafeToSized = S.unsafeToSized @Nat
-
--- | 'unsafeToSized' with the result length inferred.
---
--- Since 0.7.0.0
-{-# INLINE unsafeToSized' #-}
-unsafeToSized' :: (Dom f a, KnownNat n) => f a -> Sized f n a
-unsafeToSized' = S.unsafeToSized' @Nat
-
--- | Construct a @Sized f n a@ by padding default value if the given list is short.
---
--- Since 0.7.0.0
-{-# INLINE toSizedWithDefault #-}
-toSizedWithDefault :: (Dom f a, CFreeMonoid f) => SNat n -> a -> f a -> Sized f n a
-toSizedWithDefault = S.toSizedWithDefault @Nat
-
--- | 'toSizedWithDefault' with the result length inferred.
---
--- Since 0.7.0.0
-{-# INLINE toSizedWithDefault' #-}
-toSizedWithDefault' :: (Dom f a, KnownNat n, CFreeMonoid f)
-  => a -> f a -> Sized f n a
-toSizedWithDefault' = S.toSizedWithDefault' @Nat
-
---------------------------------------------------------------------------------
--- Querying
---------------------------------------------------------------------------------
-
---------------------------------------------------------------------------------
---- Partitioning
---------------------------------------------------------------------------------
-
--- | 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.7.0.0
-type Partitioned f (n :: Nat) a = S.Partitioned f n a
-
-pattern Partitioned
-  :: forall (f :: Type -> Type) (n :: Nat) a. ()
-  => forall (n1 :: Nat) (m :: Nat). (n ~ (n1 + m), Dom f a)
-  => SNat n1 -> Sized f n1 a -> SNat m
-  -> Sized f m a -> Partitioned f n a
-{-# COMPLETE Partitioned #-}
-pattern Partitioned ls l rs r = S.Partitioned ls l rs r
-
--- | Take the initial segment as long as elements satisfys the predicate.
---
--- Since 0.7.0.0
-{-# INLINE takeWhile #-}
-takeWhile :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> SomeSized f a
-takeWhile = S.takeWhile @Nat
-
--- | Drop the initial segment as long as elements satisfys the predicate.
---
--- Since 0.7.0.0
-{-# INLINE dropWhile #-}
-dropWhile :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> SomeSized f a
-dropWhile = S.dropWhile @Nat
-
--- | Split the sequence into the longest prefix
---   of elements that satisfy the predicate
---   and the rest.
---
--- Since 0.7.0.0
-span :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> Partitioned f n a
-{-# INLINE span #-}
-span = S.span @Nat
-
--- | Split the sequence into the longest prefix
---   of elements that do not satisfy the
---   predicate and the rest.
---
--- Since 0.7.0.0
-{-# INLINE break #-}
-break :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> Partitioned f n a
-break = S.break @Nat
-
--- | Split the sequence in two parts, the first one containing those elements that satisfy the predicate and the second one those that don't.
---
--- Since 0.7.0.0
-{-# INLINE partition #-}
-partition :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> Partitioned f n a
-partition = S.partition @Nat
-
---------------------------------------------------------------------------------
---- Searching
---------------------------------------------------------------------------------
--- | Membership test; see also 'notElem'.
---
--- Since 0.7.0.0
-{-# INLINE elem #-}
-elem :: (Dom f a, CFoldable f, Eq a) => a -> Sized f n a -> Bool
-elem = S.elem @Nat
-
--- | Negation of 'elem'.
---
--- Since 0.7.0.0
-{-# INLINE notElem #-}
-notElem :: (Dom f a, CFoldable f, Eq a) => a -> Sized f n a -> Bool
-notElem = S.notElem @Nat
-
--- | Find the element satisfying the predicate.
---
--- Since 0.7.0.0
-{-# INLINE find #-}
-find :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe a
-find = S.find @Nat
-
--- | @'findIndex' p xs@ find the element satisfying @p@ and returns its index if exists.
---
--- Since 0.7.0.0
-{-# INLINE findIndex #-}
-findIndex :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe Int
-findIndex = S.findIndex @Nat
-
--- | 'Ordinal' version of 'findIndex'.
---
--- Since 0.7.0.0
-{-# INLINE sFindIndex #-}
-sFindIndex :: (Dom f a, KnownNat n, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe (Ordinal n)
-sFindIndex = S.sFindIndex @Nat
-
--- | @'findIndices' p xs@ find all elements satisfying @p@ and returns their indices.
---
--- Since 0.7.0.0
-{-# INLINE findIndices #-}
-findIndices :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> [Int]
-findIndices = S.findIndices @Nat
-
--- | 'Ordinal' version of 'findIndices'.
---
--- Since 0.7.0.0
-{-# INLINE sFindIndices #-}
-sFindIndices :: (Dom f a, CFoldable f, KnownNat n) => (a -> Bool) -> Sized f n a -> [Ordinal n]
-sFindIndices = S.sFindIndices @Nat
-
--- | Returns the index of the given element in the list, if exists.
---
--- Since 0.8.0.0
-{-# INLINE elemIndex #-}
-elemIndex :: (Dom f a, CFoldable f, Eq a) => a -> Sized f n a -> Maybe Int
-elemIndex = S.elemIndex @Nat
-
-sElemIndex, sUnsafeElemIndex :: (Dom f a, KnownNat n, CFoldable f, Eq a) => a -> Sized f n a -> Maybe (Ordinal n)
-{-# DEPRECATED sUnsafeElemIndex "Use sElemIndex instead" #-}
-
--- | Ordinal version of 'elemIndex'.
---   Since 0.7.0.0, we no longer do boundary check inside the definition.
---
---   Since 0.7.0.0
-sUnsafeElemIndex = S.sElemIndex @Nat
-
--- | Ordinal version of 'elemIndex'.
---   Since 0.7.0.0, we no longer do boundary check inside the definition.
---
---   Since 0.7.0.0
-sElemIndex = S.sElemIndex @Nat
-
--- | Returns all indices of the given element in the list.
---
--- Since 0.8.0.0
-{-# INLINE elemIndices #-}
-elemIndices :: (Dom f a, CFoldable f, Eq a) => a -> Sized f n a -> [Int]
-elemIndices = S.elemIndices @Nat
-
--- | Ordinal version of 'elemIndices'
---
--- Since 0.8.0.0
-{-# INLINE sElemIndices #-}
-sElemIndices
-  :: (Dom f a, CFoldable f, KnownNat n, Eq a)
-  => a -> Sized f n a -> [Ordinal n]
-sElemIndices = S.sElemIndices @Nat
-
---------------------------------------------------------------------------------
--- Views and Patterns
---------------------------------------------------------------------------------
-
-{-$ViewsAndPatterns #ViewsAndPatterns#
-
-   With GHC's @ViewPatterns@ and @PatternSynonym@ extensions,
-   we can pattern-match on arbitrary @Sized f n a@ if @f@ is list-like functor.
-   Curretnly, there are two direction view and patterns: Cons and Snoc.
-   Assuming underlying sequence type @f@ has O(1) implementation for 'cnull', 'chead'
-   (resp. 'clast') and 'ctail' (resp. 'cinit'), We can view and pattern-match on
-   cons (resp. snoc) of @Sized f n a@ in O(1).
--}
-
-{-$views #views#
-
-   With @ViewPatterns@ extension, we can pattern-match on 'Sized' value as follows:
-
-@
-slen :: ('KnownNat' n, 'Dom f a' f) => 'Sized' f n a -> 'Sing' n
-slen ('viewCons' -> 'NilCV')    = 'SZ'
-slen ('viewCons' -> _ ':-' as) = 'SS' (slen as)
-slen _                          = error "impossible"
-@
-
-   The constraint @('KnownNat' n, 'Dom f 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 :: ('KnownNat' n, 'Dom f 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.9.0.0
-data ConsView f n a where
-  NilCV :: ConsView f 0 a
-  (:-)
-    :: (KnownNat n, KnownNat (1 + n))
-    => a -> Sized f n a -> ConsView f (1 + n) a
-
-
-infixr 9 :-
-
--- | Case analysis for the cons-side of sequence.
---
--- Since 0.5.0.0 (type changed)
-viewCons :: forall f n a. (Dom f a, KnownNat n, CFreeMonoid f) => Sized f n a -> ConsView f n a
-viewCons sz = case zeroOrSucc $ sing @n of
-  IsZero -> NilCV
-  IsSucc n' ->
-    withWitness (plusMonotoneR (sing @1) (sing @0) n' Witness) $
-    withKnownNat n'
-    $ withKnownNat (sing @1 %+ n')
-    $ case uncons' sz of
-        Uncons a xs -> a :- xs
-
--- | View of the left end of sequence (snoc-side).
---
--- Since 0.7.0.0
-type SnocView =
-  (S.SnocView :: (Type -> Type) -> Nat -> Type -> Type)
-
--- | Since 0.8.0.0
-pattern NilSV
-  :: forall (f :: Type -> Type) n a. ()
-  => (n ~ 0)
-  => SnocView f n a
-pattern NilSV = S.NilSV
-
-
-infixl 9 :-::
--- | Since 0.8.0.0
-pattern (:-::)
-  :: forall (f :: Type -> Type) n a. ()
-  => forall n1. (n ~ (n1 + 1), SingI n1)
-  => Sized f n1 a -> a -> SnocView f n a
-pattern ls :-:: l = ls S.:-:: l
-{-# COMPLETE NilSV, (:-::) #-}
-
-
--- | Case analysis for the snoc-side of sequence.
---
--- Since 0.8.0.0 (type changed)
-viewSnoc :: (Dom f a, KnownNat n, CFreeMonoid f) => Sized f n a -> SnocView f n a
-viewSnoc = S.viewSnoc @Nat
-
-{-$patterns #patterns#
-
-   So we can pattern match on both end of sequence via views, but
-   it is rather clumsy to nest it. For example:
-
-@
-nextToHead :: ('Dom f 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 :: ('Dom f 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, 'Dom f a' f) => 'Sized' f n a -> 'Sing' n
-slen 'Nil'       = 'SZ'
-slen (_ ':<' as) = 'SS' (slen as)
-@
-
-   So, we can use @':<'@ and @'Nil'@ (resp. @':>'@ and @'Nil'@) to
-   pattern-match directly on cons-side (resp. snoc-side) as we usually do for lists.
-   @'Nil'@, @':<'@, and @':>'@ are neither functions nor data constructors,
-   but pattern synonyms so we cannot use them in expression contexts.
-   For more detail on pattern synonyms, see
-   <http://www.haskell.org/ghc/docs/latest/html/users_guide/syntax-extns.html#pattern-synonyms GHC Users Guide>
-   and
-   <https://ghc.haskell.org/trac/ghc/wiki/PatternSynonyms HaskellWiki>.
--}
-
--- | Pattern synonym for cons-side uncons.
-pattern (:<)
-  :: forall (f :: Type -> Type) a (n :: Nat).
-      (Dom f a, KnownNat n, CFreeMonoid f)
-  => forall (n1 :: Nat). (n ~ (1 + n1), KnownNat n1, KnownNat n)
-  => a -> Sized f n1 a -> Sized f n a
-pattern a :< as <- (viewCons -> a :- as) where
-   a :< as = a <| as
-infixr 5 :<
-
-chkNil
-  :: forall f n a.
-      (KnownNat n)
-  => Sized f n a -> ZeroOrSucc n
-chkNil = const $ zeroOrSucc $ sing @n
-
--- | Pattern synonym for a nil sequence.
-pattern Nil
-  :: forall (f :: Type -> Type) n a.
-      (Dom f a, KnownNat n, CFreeMonoid f)
-  => (n ~ 0) => Sized f n a
-pattern Nil <- (chkNil -> IsZero) where
-  Nil = empty
-
--- | Pattern synonym for snoc-side unsnoc.
-pattern (:>)
-  :: forall (f :: Type -> Type) a (n :: Nat).
-      (Dom f a, KnownNat n, CFreeMonoid f)
-  => forall (n1 :: Nat). (n ~ (n1 + 1), SingI n1)
-  => Sized f n1 a -> a -> Sized f n a
-pattern a :> b = a S.:> b
-infixl 5 :>
-
-{-# COMPLETE (:<), Nil #-}
-{-# COMPLETE (:>), Nil #-}
+module Data.Sized.Builtin
+  {-# DEPRECATED "Use Data.Sized instead" #-}
+  ( module Data.Sized ) where
+import Data.Sized
diff --git a/src/Data/Sized/Flipped.hs b/src/Data/Sized/Flipped.hs
--- a/src/Data/Sized/Flipped.hs
+++ b/src/Data/Sized/Flipped.hs
@@ -1,47 +1,64 @@
-{-# LANGUAGE CPP, ConstraintKinds, DataKinds, DeriveDataTypeable           #-}
-{-# LANGUAGE DeriveFunctor, DeriveTraversable, EmptyDataDecls              #-}
-{-# LANGUAGE ExplicitNamespaces, FlexibleContexts, FlexibleInstances       #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving, KindSignatures                    #-}
-{-# LANGUAGE LiberalTypeSynonyms, MultiParamTypeClasses, PatternSynonyms   #-}
-{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables                    #-}
-{-# LANGUAGE StandaloneDeriving, TemplateHaskell, TypeFamilies, TypeInType #-}
-{-# LANGUAGE TypeOperators, UndecidableInstances, ViewPatterns             #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE EmptyDataDecls #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE LiberalTypeSynonyms #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ViewPatterns #-}
+
 #if __GLASGOW_HASKELL__ && __GLASGOW_HASKELL__ >= 806
 {-# LANGUAGE NoStarIsType #-}
 #endif
-module Data.Sized.Flipped (Flipped(..)) where
-import Data.Sized.Internal
+module Data.Sized.Flipped (Flipped (..)) where
 
-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.MonoTraversable (Element, MonoFoldable (..))
-import           Data.MonoTraversable (MonoFunctor (..))
-import           Data.MonoTraversable (MonoTraversable (..))
-import qualified Data.Sequence        as Seq
-import qualified Data.Type.Natural    as PN
-import           Data.Type.Ordinal    (HasOrdinal, Ordinal (..))
-import           Data.Typeable        (Typeable)
-import qualified Data.Vector          as V
+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.MonoTraversable (Element, MonoFoldable (..), MonoFunctor (..), MonoTraversable (..))
+import qualified Data.Sequence as Seq
+import Data.Sized.Internal
+import qualified Data.Type.Natural as PN
+import Data.Type.Ordinal (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
+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)
+{- | 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 #-}
@@ -49,17 +66,19 @@
   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)) #-}
+instance
+  (Integral (Index (f a)), Ixed (f a)) =>
+  Ixed (Flipped f a n)
+  where
+  {-# SPECIALIZE instance Ixed (Flipped [] a (n :: TL.Nat)) #-}
+  {-# SPECIALIZE instance Ixed (Flipped [] a (n :: PN.Nat)) #-}
+  {-# SPECIALIZE instance Ixed (Flipped V.Vector a (n :: TL.Nat)) #-}
+  {-# SPECIALIZE instance Ixed (Flipped V.Vector a (n :: PN.Nat)) #-}
+  {-# SPECIALIZE instance SV.Storable a => Ixed (Flipped SV.Vector a (n :: TL.Nat)) #-}
+  {-# SPECIALIZE instance SV.Storable a => Ixed (Flipped SV.Vector a (n :: PN.Nat)) #-}
+  {-# SPECIALIZE instance UV.Unbox a => Ixed (Flipped UV.Vector a (n :: TL.Nat)) #-}
+  {-# SPECIALIZE instance UV.Unbox a => Ixed (Flipped UV.Vector a (n :: PN.Nat)) #-}
+  {-# SPECIALIZE instance Ixed (Flipped Seq.Seq a (n :: TL.Nat)) #-}
+  {-# SPECIALIZE instance Ixed (Flipped Seq.Seq a (n :: PN.Nat)) #-}
   ix o = _Wrapped . ix o
   {-# INLINE ix #-}
diff --git a/src/Data/Sized/Internal.hs b/src/Data/Sized/Internal.hs
--- a/src/Data/Sized/Internal.hs
+++ b/src/Data/Sized/Internal.hs
@@ -10,34 +10,31 @@
 #endif
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 module Data.Sized.Internal (Sized(..)) where
-import           Control.DeepSeq         (NFData (..))
-import           Control.Lens.At         (Index, IxValue, Ixed (..))
-import           Control.Lens.Indexed    (FoldableWithIndex (..),
-                                          FunctorWithIndex (..),
-                                          TraversableWithIndex (..))
-import           Control.Subcategory     (CFoldable, CFunctor, Constrained)
-import           Data.Hashable           (Hashable (..))
-import           Data.Kind               (Type)
-import           Data.MonoTraversable    (Element, MonoFoldable (..),
-                                          MonoFunctor (..),
-                                          MonoTraversable (..))
-import qualified Data.Sequence           as Seq
-import           Data.Singletons.Prelude (SingI)
-import qualified Data.Type.Natural       as PN
-import           Data.Type.Ordinal       (HasOrdinal, Ordinal (..),
-                                          ordToNatural, unsafeNaturalToOrd)
-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           Control.DeepSeq      (NFData (..))
+import           Control.Lens.At      (Index, IxValue, Ixed (..))
+import           Control.Lens.Indexed (FoldableWithIndex (..),
+                                       FunctorWithIndex (..),
+                                       TraversableWithIndex (..))
+import           Control.Subcategory  (CFoldable, CFunctor, Constrained)
+import           Data.Hashable        (Hashable (..))
+import           Data.Kind            (Type)
+import           Data.MonoTraversable (Element, MonoFoldable (..),
+                                       MonoFunctor (..), MonoTraversable (..))
+import qualified Data.Sequence        as Seq
+import           Data.Type.Ordinal    (Ordinal (..), ordToNatural,
+                                       unsafeNaturalToOrd)
+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           GHC.TypeNats
 
 -- | @Sized@ wraps a sequential type 'f' and makes length-parametrized version.
 --
 -- Here, 'f' must be the instance of 'CFreeMonoid' (f a) a@ for all @a@.
 --
 -- Since 0.2.0.0
-newtype Sized (f :: Type -> Type) (n :: nat) a =
+newtype Sized (f :: Type -> Type) (n :: Nat) a =
   Sized { runSized :: f a
         } deriving (Eq, Ord, Typeable,
                     Functor, Foldable, Traversable)
@@ -86,42 +83,31 @@
 
 -- | Since 0.3.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) #-}
+instance (Integral (Index (f a)), Ixed (f a))
+         => Ixed (Sized f (n :: Nat) a) where
+  {-# SPECIALISE instance Ixed (Sized [] (n :: Nat) a) #-}
+  {-# SPECIALISE instance Ixed (Sized V.Vector (n :: Nat) a) #-}
+  {-# SPECIALISE instance SV.Storable a => Ixed (Sized SV.Vector (n :: Nat) a) #-}
+  {-# SPECIALISE instance UV.Unbox a => Ixed (Sized UV.Vector (n :: Nat) a) #-}
+  {-# SPECIALISE instance Ixed (Sized Seq.Seq (n :: Nat) a) #-}
   {-# INLINE ix #-}
   ix n f = fmap Sized . ix (fromIntegral $ ordToNatural 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
+instance (Integral i, FunctorWithIndex i f, KnownNat n)
+      => FunctorWithIndex (Ordinal n) (Sized f n) where
   imap f = Sized . imap (f . unsafeNaturalToOrd . 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)) #-}
+  {-# SPECIALISE instance KnownNat n
+                       => FunctorWithIndex (Ordinal n) (Sized [] (n :: Nat)) #-}
+  {-# SPECIALISE instance KnownNat n
+                       => FunctorWithIndex (Ordinal n) (Sized V.Vector (n :: Nat)) #-}
+  {-# SPECIALISE instance KnownNat n
+                       => FunctorWithIndex (Ordinal n) (Sized Seq.Seq (n :: Nat)) #-}
 
 -- | Since 0.4.0.0
-instance {-# OVERLAPPABLE #-}  (Integral i, FoldableWithIndex i f, HasOrdinal nat, SingI n)
-      => FoldableWithIndex (Ordinal (n :: nat)) (Sized f n) where
+instance {-# OVERLAPPABLE #-}  (Integral i, FoldableWithIndex i f, KnownNat n)
+      => FoldableWithIndex (Ordinal n) (Sized f n) where
   ifoldMap f = ifoldMap (f . unsafeNaturalToOrd . fromIntegral) . runSized
   {-# INLINE ifoldMap #-}
 
@@ -137,34 +123,21 @@
   ifoldl' f e = ifoldl' (f . unsafeNaturalToOrd . 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)) #-}
-
+  {-# SPECIALISE instance KnownNat n
+                       => FoldableWithIndex (Ordinal n) (Sized [] (n :: Nat)) #-}
+  {-# SPECIALISE instance KnownNat n
+                       => FoldableWithIndex (Ordinal n) (Sized V.Vector (n :: Nat)) #-}
+  {-# SPECIALISE instance KnownNat n
+                       => FoldableWithIndex (Ordinal n) (Sized Seq.Seq (n :: Nat)) #-}
 -- | Since 0.2.0.0
-instance (Integral i, TraversableWithIndex i f, HasOrdinal nat, SingI n)
-      => TraversableWithIndex (Ordinal (n :: nat)) (Sized f n) where
+instance (Integral i, TraversableWithIndex i f, KnownNat n)
+      => TraversableWithIndex (Ordinal n) (Sized f n) where
   itraverse f = fmap Sized . itraverse (f . unsafeNaturalToOrd . 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))  #-}
+  {-# SPECIALISE instance KnownNat n
+                       => TraversableWithIndex (Ordinal n) (Sized [] (n :: Nat)) #-}
+  {-# SPECIALISE instance KnownNat n
+                       => TraversableWithIndex (Ordinal n) (Sized V.Vector (n :: Nat)) #-}
+  {-# SPECIALISE instance KnownNat n
+                       => TraversableWithIndex (Ordinal n) (Sized Seq.Seq (n :: Nat)) #-}
diff --git a/src/Data/Sized/Peano.hs b/src/Data/Sized/Peano.hs
deleted file mode 100644
--- a/src/Data/Sized/Peano.hs
+++ /dev/null
@@ -1,1002 +0,0 @@
-{-# LANGUAGE CPP, DataKinds, GADTs, KindSignatures, MultiParamTypeClasses #-}
-{-# LANGUAGE NoImplicitPrelude, NoMonomorphismRestriction, NoStarIsType   #-}
-{-# LANGUAGE PatternSynonyms, PolyKinds, RankNTypes, TypeApplications     #-}
-{-# LANGUAGE TypeInType, TypeOperators, ViewPatterns                      #-}
--- | This module exports provides the functionality to make length-parametrized types
---   from existing 'CFreeMonoid' sequential types,
---   parametrised with peano numeral 'PN.Nat' kind.
---
---   Most of the complexity of operations on @'Sized' f n a@ are the same as
---   original operations on @f@. For example, '!!' is O(1) for
---   @Sized Vector n a@ but O(i) for @Sized [] n a@.
---
---  This module also provides powerful view types and pattern synonyms to
---  inspect the sized sequence. See <#ViewsAndPatterns Views and Patterns> for more detail.
-module Data.Sized.Peano {-# DEPRECATED "Removed in future release" #-}
-  ( -- * Main Data-types
-    Sized(), SomeSized, pattern SomeSized, Ordinal,
-    DomC(),
-    -- * Accessors
-    -- ** Length information
-    length, sLength, null,
-    -- ** Indexing
-    (!!), (%!!), index, sIndex, head, last,
-    uncons, uncons', Uncons, pattern Uncons,
-    unsnoc, unsnoc', Unsnoc, pattern Unsnoc,
-    -- ** Slicing
-    tail, init, take, takeAtMost, drop, splitAt, splitAtMost,
-    -- * Construction
-    -- ** Initialisation
-    empty, singleton, toSomeSized, replicate, replicate', generate, generate',
-    -- ** Concatenation
-    cons, (<|), snoc, (|>), append, (++), concat,
-    -- ** Zips
-    zip, zipSame, zipWith, zipWithSame, unzip, unzipWith,
-    -- * Transformation
-    map, reverse, intersperse, nub, sort, sortBy, insert, insertBy,
-    -- * Conversion
-    -- ** List
-    toList, fromList, fromList', unsafeFromList, unsafeFromList',
-    fromListWithDefault, fromListWithDefault',
-    -- ** Base container
-    unsized,
-    toSized, toSized', unsafeToSized, unsafeToSized',
-    toSizedWithDefault, toSizedWithDefault',
-    -- * Querying
-    -- ** Partitioning
-    Partitioned(), pattern Partitioned,
-    takeWhile, dropWhile, span, break, partition,
-    -- ** Searching
-    elem, notElem, find, findIndex, sFindIndex,
-    findIndices, sFindIndices,
-    elemIndex, sElemIndex, sUnsafeElemIndex, elemIndices, sElemIndices,
-    -- * Views and Patterns
-    -- $ViewsAndPatterns
-
-    -- ** Views
-    -- $views
-
-    -- ** Patterns
-    -- $patterns
-
-    -- ** Definitions
-    viewCons, ConsView,
-    pattern (:-), pattern NilCV,
-    viewSnoc, SnocView,
-    pattern (:-::), pattern NilSV,
-
-    pattern Nil, pattern (:<), pattern NilL , pattern (:>), pattern NilR,
-  ) where
-import           Data.Sized (DomC)
-import qualified Data.Sized as S
-
-import           Control.Subcategory
-import           Data.Kind                    (Type)
-import           Data.Singletons.Prelude      (POrd ((<=)), SingI)
-import           Data.Singletons.Prelude.Enum (PEnum (..))
-import           Data.Type.Natural            (Min, Nat (..), One, SNat, Two,
-                                               type (*), type (+), type (-))
-import           Data.Type.Natural.Class      (type (-.), type (<))
-import qualified Data.Type.Ordinal            as O
-import           Prelude                      (Bool (..), Eq, Int, Maybe,
-                                               Monoid, Ord, Ordering)
-
-type Ordinal = (O.Ordinal :: Nat -> Type)
-
--- | @Sized@ wraps a sequential type 'f' and makes length-parametrized version.
---
--- Here, 'f' must satisfy @'CFreeMonoid' f@ and @Dom f a@.
---
--- Since 0.2.0.0
-type Sized = (S.Sized :: (Type -> Type) -> Nat -> Type -> Type)
-
-
--- | 'Sized' sequence with the length is existentially quantified.
---   This type is used mostly when the return type's length cannot
---   be statically determined beforehand.
---
--- @SomeSized' sn xs :: SomeSized' f a@ stands for the 'Sized' sequence
--- @xs@ of element type @a@ and length @sn@.
---
--- Since 0.7.0.0
-type SomeSized f a = S.SomeSized' f Nat a
-
-pattern SomeSized
-  :: forall (f :: Type -> Type) a. ()
-  => forall (n :: Nat). SNat n
-  -> Sized f n a -> SomeSized f a
-{-# COMPLETE SomeSized #-}
-pattern SomeSized n s = S.SomeSized'  n s
-
--- | 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.8.0.0 (type changed)
-{-# INLINE length #-}
-length :: (Dom f a, SingI n) => Sized f n a -> Int
-length = S.length @Nat
-
--- | @Sing@ version of 'length'.
---
--- Since 0.8.0.0 (type changed)
-{-# INLINE sLength #-}
-sLength :: (Dom f a, SingI n) => Sized f n a -> SNat n
-sLength = S.sLength @Nat
-
--- | Test if the sequence is empty or not.
---
--- Since 0.7.0.0
-{-# INLINE null #-}
-null :: (Dom f a, CFoldable f) => Sized f n a -> Bool
-null = S.null @Nat
-
---------------------------------------------------------------------------------
---- Indexing
---------------------------------------------------------------------------------
-
--- | (Unsafe) indexing with @Int@s.
---   If you want to check boundary statically, use '%!!' or 'sIndex'.
---
--- Since 0.7.0.0
-{-# INLINE (!!) #-}
-(!!) :: (Dom f a, CFoldable f, (One <= m) ~ 'True) => Sized f m a -> Int -> a
-(!!) = (S.!!) @Nat
-
--- | Safe indexing with 'Ordinal's.
---
--- Since 0.7.0.0
-{-# INLINE (%!!) #-}
-(%!!) :: (Dom f c, CFoldable f) => Sized f n c -> Ordinal n -> c
-(%!!) = (S.%!!) @Nat
-
--- | Flipped version of '!!'.
---
--- Since 0.7.0.0
-{-# INLINE index #-}
-index
-  :: (Dom f a, CFoldable f, (One <= m) ~ 'True)
-  => Int -> Sized f m a -> a
-index = S.index @Nat
-
--- | Flipped version of '%!!'.
---
--- Since 0.7.0.0
-{-# INLINE sIndex #-}
-sIndex :: (Dom f c, CFoldable f) => Ordinal n -> Sized f n c -> c
-sIndex = S.sIndex @Nat
-
--- | 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.7.0.0
-{-# INLINE head #-}
-head :: (Dom f a, CFoldable f, ('Z < n) ~ 'True) => Sized f n a -> a
-head = S.head @Nat
-
--- | 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.7.0.0
-{-# INLINE last #-}
-last :: (Dom f a, CFoldable f, ('Z < n) ~ 'True) => Sized f n a -> a
-last = S.last @Nat
-
--- | 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.7.0.0
-{-# INLINE uncons #-}
-uncons
-  :: (Dom f a, SingI n, CFreeMonoid f, ('Z < n) ~ 'True)
-  => Sized f n a -> Uncons f n a
-uncons = S.uncons @Nat
-
--- | 'uncons' with explicit specified length @n@
---
---   Since 0.7.0.0
-{-# INLINE uncons' #-}
-uncons'
-  :: (Dom f a, SingI n, CFreeMonoid f, ('Z < n) ~ 'True)
-  => Sized f n a
-  -> Uncons f n a
-uncons' = S.uncons @Nat
-
--- | 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.7.0.0
-{-# INLINE unsnoc #-}
-unsnoc
-  :: (Dom f a, SingI n, CFreeMonoid f, ('Z < n) ~ 'True)
-  => Sized f n a -> Unsnoc f n a
-unsnoc = S.unsnoc @Nat
-
--- | 'unsnoc'' with explicit specified length @n@
---
---   Since 0.7.0.0
-{-# INLINE unsnoc' #-}
-unsnoc' :: (Dom f a, SingI n, CFreeMonoid f) => proxy n -> Sized f ('S n) a -> Unsnoc f ('S n) a
-unsnoc' = S.unsnoc' @Nat
-
-type Uncons f (n :: Nat) a = S.Uncons f n a
-pattern Uncons
-  :: forall (f :: Type -> Type) (n :: Nat) a. ()
-  => forall (n1 :: Nat). (n ~ Succ n1, SingI n1)
-  => a -> Sized f n1 a -> Uncons f n a
-pattern Uncons a as = S.Uncons a as
-
-type Unsnoc f (n :: Nat) a = S.Unsnoc f n a
-
-pattern Unsnoc
-  :: forall (f :: Type -> Type) (n :: Nat) a. ()
-  => forall (n1 :: Nat). (n ~ Succ n1)
-  => Sized f n1 a -> a -> Unsnoc f n a
-pattern Unsnoc xs x = S.Unsnoc xs x
-
--- | 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.7.0.0
-{-# INLINE tail #-}
-tail :: (Dom f a, CFreeMonoid f) => Sized f (One + n) a -> Sized f n a
-tail = S.tail @Nat
-
-
--- | 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.7.0.0
-{-# INLINE init #-}
-init :: (Dom f a, CFreeMonoid f) => Sized f (n + One) a -> Sized f n a
-init = S.init @Nat
-
--- | @take k xs@ takes first @k@ element of @xs@ where
--- the length of @xs@ should be larger than @k@.
---
--- Since 0.7.0.0
-{-# INLINE take #-}
-take
-  :: (Dom f a, CFreeMonoid f, (n <= m) ~ 'True)
-  => SNat n -> Sized f m a -> Sized f n a
-take = S.take @Nat
-
--- | @'takeAtMost' k xs@ takes first at most @k@ elements of @xs@.
---
--- Since 0.7.0.0
-{-# INLINE takeAtMost #-}
-takeAtMost
-  :: (Dom f a, CFreeMonoid f)
-  => SNat n -> Sized f m a -> Sized f (Min n m) a
-takeAtMost = S.takeAtMost @Nat
-
--- | @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@.
---
--- Since 0.7.0.0
-{-# INLINE drop #-}
-drop
-  :: (Dom f a, CFreeMonoid f, (n <= m) ~ 'True)
-  => SNat n -> Sized f m a -> Sized f (m - n) a
-drop = S.drop @Nat
-
--- | @splitAt k xs@ split @xs@ at @k@, where
--- the length of @xs@ should be less than or equal to @k@.
---
--- Since 0.7.0.0
-{-# INLINE splitAt #-}
-splitAt
-  :: (Dom f a, CFreeMonoid f, (n <= m) ~ 'True)
-  => SNat n -> Sized f m a -> (Sized f n a, Sized f (m - n) a)
-splitAt = S.splitAt @Nat
-
--- | @splitAtMost k xs@ split @xs@ at @k@.
---   If @k@ exceeds the length of @xs@, then the second result value become empty.
---
--- Since 0.7.0.0
-{-# INLINE splitAtMost #-}
-splitAtMost
-  :: (Dom f a, CFreeMonoid f)
-  => SNat n -> Sized f m a
-  -> (Sized f (Min n m) a, Sized f (m -. n) a)
-splitAtMost = S.splitAtMost @Nat
-
---------------------------------------------------------------------------------
--- Construction
---------------------------------------------------------------------------------
-
---------------------------------------------------------------------------------
---- Initialisation
---------------------------------------------------------------------------------
-
--- | Empty sequence.
---
--- Since 0.7.0.0 (type changed)
-{-# INLINE empty #-}
-empty :: (Dom f a, Monoid (f a)) => Sized f 'Z a
-empty = S.empty @Nat
-
--- | Sequence with one element.
---
--- Since 0.7.0.0
-{-# INLINE singleton #-}
-singleton :: (Dom f a, CFreeMonoid f) => a -> Sized f One a
-singleton = S.singleton @Nat
-
--- | Consruct the 'Sized' sequence from base type, but
---   the length parameter is dynamically determined and
---   existentially quantified; see also 'SomeSized''.
---
--- Since 0.7.0.0
-{-# INLINE toSomeSized #-}
-toSomeSized :: (Dom f a, CFoldable f) => f a -> SomeSized f a
-toSomeSized = S.toSomeSized @Nat
-
--- | Replicates the same value.
---
--- Since 0.7.0.0
-{-# INLINE replicate #-}
-replicate :: (Dom f a, CFreeMonoid f) => SNat n -> a -> Sized f n a
-replicate = S.replicate @Nat
-
--- | 'replicate' with the length inferred.
---
--- Since 0.7.0.0
-{-# INLINE replicate' #-}
-replicate' :: (Dom f a, CFreeMonoid f, SingI n) => a -> Sized f n a
-replicate' = S.replicate' @Nat
-
--- | Construct a sequence of the given length by applying the function to each index.
---
--- Since 0.7.0.0
-{-# INLINE generate #-}
-generate :: (Dom f a, CFreeMonoid f) => SNat n -> (Ordinal n -> a) -> Sized f n a
-generate = S.generate @Nat
-
--- | 'generate' with length inferred.
---
---   Since 0.8.0.0
-{-# INLINE generate' #-}
-generate' :: forall f n a.
-  (SingI n, Dom f a, CFreeMonoid f)
-  => (Ordinal n -> a) -> Sized f n a
-generate' = S.generate' @Nat
-
---------------------------------------------------------------------------------
---- Concatenation
---------------------------------------------------------------------------------
-
--- | Append an element to the head of sequence.
---
--- Since 0.7.0.0
-{-# INLINE cons #-}
-cons :: (Dom f a, CFreeMonoid f) => a -> Sized f n a -> Sized f ('S n) a
-cons = S.cons @Nat
-
--- | Append an element to the tail of sequence.
---
--- Since 0.7.0.0
-{-# INLINE snoc #-}
-snoc :: (Dom f a, CFreeMonoid f) => Sized f n a -> a -> Sized f (n + One) a
-snoc = S.snoc @Nat
-
--- | Infix version of 'snoc'.
---
--- Since 0.7.0.0
-{-# INLINE (<|) #-}
-(<|) :: (Dom f a, CFreeMonoid f) => a -> Sized f n a -> Sized f ('S n) a
-(<|) = (S.<|) @Nat
-
--- | Append an element to the tail of sequence.
---
--- Since 0.7.0.0
-{-# INLINE (|>) #-}
-(|>) :: (Dom f a, CFreeMonoid f) => Sized f n a -> a -> Sized f (n + One) a
-(|>) = (S.|>) @Nat
-
--- | Infix version of 'append'.
---
--- Since 0.7.0.0
-{-# INLINE (++) #-}
-(++) :: (Dom f a, CFreeMonoid f) => Sized f n a -> Sized f m a -> Sized f (n + m) a
-(++) = (S.++) @Nat
-
--- | Append two lists.
---
--- Since 0.7.0.0
-{-# INLINE append #-}
-append :: (Dom f a, CFreeMonoid f) => Sized f n a -> Sized f m a -> Sized f (n + m) a
-append = S.append @Nat
-
--- | Concatenates multiple sequences into one.
---
--- Since 0.7.0.0
-{-# INLINE concat #-}
-concat
-  :: (Dom f a, Dom f' (f a), Dom f' (Sized f n a),
-      CFreeMonoid f, CFunctor f', CFoldable f'
-    ) => Sized f' m (Sized f n a) -> Sized f (m * n) a
-concat = S.concat @Nat
-
---------------------------------------------------------------------------------
---- Zips
---------------------------------------------------------------------------------
-
--- | Zipping two sequences. Length is adjusted to shorter one.
---
--- Since 0.7.0.0
-{-# INLINE zip #-}
-zip :: (Dom f a, Dom f b, Dom f (a, b), CZip f)
-  => Sized f n a -> Sized f m b -> Sized f (Min n m) (a, b)
-zip = S.zip @Nat
-
--- | 'zip' for the sequences of the same length.
---
--- Since 0.7.0.0
-{-# INLINE zipSame #-}
-zipSame :: (Dom f a, Dom f b, Dom f (a, b), CZip f)
-  => Sized f n a -> Sized f n b -> Sized f n (a, b)
-zipSame = S.zipSame @Nat
-
--- | Zipping two sequences with funtion. Length is adjusted to shorter one.
---
--- Since 0.7.0.0
-{-# INLINE zipWith #-}
-zipWith :: (Dom f a, Dom f b, Dom f c, CZip f, CFreeMonoid f)
-  => (a -> b -> c) -> Sized f n a -> Sized f m b -> Sized f (Min n m) c
-zipWith = S.zipWith @Nat
-
--- | 'zipWith' for the sequences of the same length.
---
--- Since 0.7.0.0
-{-# INLINE zipWithSame #-}
-zipWithSame
-  :: (Dom f a, Dom f b, Dom f c, CZip f, CFreeMonoid f)
-  => (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c
-zipWithSame = S.zipWithSame @Nat
-
--- | Unzipping the sequence of tuples.
---
--- Since 0.7.0.0
-{-# INLINE unzip #-}
-unzip
-  :: (Dom f a, Dom f b, Dom f (a, b), CUnzip f)
-  => Sized f n (a, b) -> (Sized f n a, Sized f n b)
-unzip = S.unzip @Nat
-
--- | Unzipping the sequence of tuples.
---
--- Since 0.7.0.0
-{-# INLINE unzipWith #-}
-unzipWith
-  :: (Dom f a, Dom f b, Dom f c, CUnzip f)
-  => (a -> (b, c)) -> Sized f n a -> (Sized f n b, Sized f n c)
-unzipWith = S.unzipWith @Nat
-
---------------------------------------------------------------------------------
--- Transformation
---------------------------------------------------------------------------------
-
--- | Map function.
---
--- Since 0.7.0.0
-{-# INLINE map #-}
-map
-  :: (Dom f a, Dom f b, CFreeMonoid f)
-  => (a -> b) -> Sized f n a -> Sized f n b
-map = S.map @Nat
-
--- | Reverse function.
---
--- Since 0.7.0.0
-{-# INLINE reverse #-}
-reverse :: (Dom f a, CFreeMonoid f) => Sized f n a -> Sized f n a
-reverse = S.reverse @Nat
-
--- | Intersperces.
---
--- Since 0.7.0.0
-{-# INLINE intersperse #-}
-intersperse
-  :: (Dom f a, CFreeMonoid f)
-  => a -> Sized f n a -> Sized f ((Two * n) -. One) a
-intersperse = S.intersperse @Nat
-
--- | Remove all duplicates.
---
--- Since 0.7.0.0
-{-# INLINE nub #-}
-nub :: (Dom f a, Eq a, CFreeMonoid f) => Sized f n a -> SomeSized f a
-nub = S.nub @Nat
-
--- | Sorting sequence by ascending order.
---
--- Since 0.7.0.0
-{-# INLINE sort #-}
-sort :: (Dom f a, CFreeMonoid f, Ord a) => Sized f n a -> Sized f n a
-sort = S.sort @Nat
-
--- | Generalized version of 'sort'.
---
--- Since 0.7.0.0
-{-# INLINE sortBy #-}
-sortBy
-  :: (Dom f a, CFreeMonoid f)
-  => (a -> a -> Ordering)
-  -> Sized f n a -> Sized f n a
-sortBy = S.sortBy @Nat
-
--- | Insert new element into the presorted sequence.
---
--- Since 0.7.0.0
-{-# INLINE insert #-}
-insert
-  :: (Dom f a, CFreeMonoid f, Ord a)
-  => a -> Sized f n a -> Sized f ('S n) a
-insert = S.insert @Nat
-
--- | Generalized version of 'insert'.
---
--- Since 0.7.0.0
-{-# INLINE insertBy #-}
-insertBy
-  :: (Dom f a, CFreeMonoid f)
-  => (a -> a -> Ordering) -> a -> Sized f n a -> Sized f ('S n) a
-insertBy = S.insertBy @Nat
-
---------------------------------------------------------------------------------
--- Conversion
---------------------------------------------------------------------------------
-
---------------------------------------------------------------------------------
---- List
---------------------------------------------------------------------------------
-
--- | Convert to list.
---
--- Since 0.7.0.0
-{-# INLINE toList #-}
-toList :: (Dom f a, CFoldable f) => Sized f n a -> [a]
-toList = S.toList @Nat
-
--- | 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.7.0.0 (type changed)
-{-# INLINE fromList #-}
-fromList :: (Dom f a, CFreeMonoid f) => SNat n -> [a] -> Maybe (Sized f n a)
-fromList = S.fromList @Nat
-
--- | 'fromList' with the result length inferred.
---
--- Since 0.7.0.0
-{-# INLINE fromList' #-}
-fromList' :: (Dom f a, CFreeMonoid f, SingI n) => [a] -> Maybe (Sized f n a)
-fromList' = S.fromList' @Nat
-
--- | Unsafe version of 'fromList'. If the length of the given list does not
---   equal to @n@, then something unusual happens.
---
--- Since 0.7.0.0
-{-# INLINE unsafeFromList #-}
-unsafeFromList :: (Dom f a, CFreeMonoid f) => SNat n -> [a] -> Sized f n a
-unsafeFromList = S.unsafeFromList @Nat
-
--- | 'unsafeFromList' with the result length inferred.
---
--- Since 0.7.0.0
-{-# INLINE unsafeFromList' #-}
-unsafeFromList' :: (Dom f a, SingI n, CFreeMonoid f) => [a] -> Sized f n a
-unsafeFromList' = S.unsafeFromList' @Nat
-
--- | Construct a @Sized f n a@ by padding default value if the given list is short.
---
---   Since 0.5.0.0 (type changed)
-{-# INLINE fromListWithDefault #-}
-fromListWithDefault :: (Dom f a, CFreeMonoid f) => SNat n -> a -> [a] -> Sized f n a
-fromListWithDefault = S.fromListWithDefault @Nat
-
--- | 'fromListWithDefault' with the result length inferred.
---
--- Since 0.7.0.0
-{-# INLINE fromListWithDefault' #-}
-fromListWithDefault' :: (Dom f a, SingI n, CFreeMonoid f)
-  => a -> [a] -> Sized f n a
-fromListWithDefault' = S.fromListWithDefault' @Nat
-
---------------------------------------------------------------------------------
---- Base containes
---------------------------------------------------------------------------------
-
--- | Forget the length and obtain the wrapped base container.
---
--- Since 0.7.0.0
-{-# INLINE unsized #-}
-unsized :: Sized f n a -> f a
-unsized = S.unsized @Nat
-
--- | 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.7.0.0
-{-# INLINE toSized #-}
-toSized :: (Dom f a, CFreeMonoid f) => SNat n -> f a -> Maybe (Sized f n a)
-toSized = S.toSized @Nat
-
--- | 'toSized' with the result length inferred.
---
--- Since 0.7.0.0
-{-# INLINE toSized' #-}
-toSized' :: (Dom f a, CFreeMonoid f, SingI n) => f a -> Maybe (Sized f n a)
-toSized' = S.toSized' @Nat
-
--- | Unsafe version of 'toSized'. If the length of the given list does not
---   equal to @n@, then something unusual happens.
---
--- Since 0.7.0.0
-{-# INLINE unsafeToSized #-}
-unsafeToSized :: SNat n -> f a -> Sized f n a
-unsafeToSized = S.unsafeToSized @Nat
-
--- | 'unsafeToSized' with the result length inferred.
---
--- Since 0.7.0.0
-{-# INLINE unsafeToSized' #-}
-unsafeToSized' :: (Dom f a, SingI n) => f a -> Sized f n a
-unsafeToSized' = S.unsafeToSized' @Nat
-
--- | Construct a @Sized f n a@ by padding default value if the given list is short.
---
--- Since 0.7.0.0
-{-# INLINE toSizedWithDefault #-}
-toSizedWithDefault :: (Dom f a, CFreeMonoid f) => SNat n -> a -> f a -> Sized f n a
-toSizedWithDefault = S.toSizedWithDefault @Nat
-
--- | 'toSizedWithDefault' with the result length inferred.
---
--- Since 0.7.0.0
-{-# INLINE toSizedWithDefault' #-}
-toSizedWithDefault' :: (Dom f a, SingI n, CFreeMonoid f)
-  => a -> f a -> Sized f n a
-toSizedWithDefault' = S.toSizedWithDefault' @Nat
-
---------------------------------------------------------------------------------
--- Querying
---------------------------------------------------------------------------------
-
---------------------------------------------------------------------------------
---- Partitioning
---------------------------------------------------------------------------------
-
--- | 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.7.0.0
-type Partitioned f (n :: Nat) a = S.Partitioned f n a
-
-pattern Partitioned
-  :: forall (f :: Type -> Type) (n :: Nat) a. ()
-  => forall (n1 :: Nat) (m :: Nat). (n ~ (n1 + m), Dom f a)
-  => SNat n1 -> Sized f n1 a -> SNat m
-  -> Sized f m a -> Partitioned f n a
-{-# COMPLETE Partitioned #-}
-pattern Partitioned ls l rs r = S.Partitioned ls l rs r
-
--- | Take the initial segment as long as elements satisfys the predicate.
---
--- Since 0.7.0.0
-{-# INLINE takeWhile #-}
-takeWhile :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> SomeSized f a
-takeWhile = S.takeWhile @Nat
-
--- | Drop the initial segment as long as elements satisfys the predicate.
---
--- Since 0.7.0.0
-{-# INLINE dropWhile #-}
-dropWhile :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> SomeSized f a
-dropWhile = S.dropWhile @Nat
-
--- | Split the sequence into the longest prefix
---   of elements that satisfy the predicate
---   and the rest.
---
--- Since 0.7.0.0
-{-# INLINE span #-}
-span :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> Partitioned f n a
-span = S.span @Nat
-
-
--- | Split the sequence into the longest prefix
---   of elements that do not satisfy the
---   predicate and the rest.
---
--- Since 0.7.0.0
-{-# INLINE break #-}
-break :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> Partitioned f n a
-break = S.break @Nat
-
--- | Split the sequence in two parts, the first one containing those elements that satisfy the predicate and the second one those that don't.
---
--- Since 0.7.0.0
-{-# INLINE partition #-}
-partition :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> Partitioned f n a
-partition = S.partition @Nat
-
---------------------------------------------------------------------------------
---- Searching
---------------------------------------------------------------------------------
--- | Membership test; see also 'notElem'.
---
--- Since 0.7.0.0
-{-# INLINE elem #-}
-elem :: (Dom f a, CFoldable f, Eq a) => a -> Sized f n a -> Bool
-elem = S.elem @Nat
-
--- | Negation of 'elem'.
---
--- Since 0.7.0.0
-{-# INLINE notElem #-}
-notElem :: (Dom f a, CFoldable f, Eq a) => a -> Sized f n a -> Bool
-notElem = S.notElem @Nat
-
--- | Find the element satisfying the predicate.
---
--- Since 0.7.0.0
-{-# INLINE find #-}
-find :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe a
-find = S.find @Nat
-
--- | @'findIndex' p xs@ find the element satisfying @p@ and returns its index if exists.
---
--- Since 0.7.0.0
-{-# INLINE findIndex #-}
-findIndex :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe Int
-findIndex = S.findIndex @Nat
-
--- | 'Ordinal' version of 'findIndex'.
---
--- Since 0.7.0.0
-{-# INLINE sFindIndex #-}
-sFindIndex :: (Dom f a, SingI n, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe (Ordinal n)
-sFindIndex = S.sFindIndex @Nat
-
--- | @'findIndices' p xs@ find all elements satisfying @p@ and returns their indices.
---
--- Since 0.7.0.0
-{-# INLINE findIndices #-}
-findIndices :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> [Int]
-findIndices = S.findIndices @Nat
-
--- | 'Ordinal' version of 'findIndices'.
---
--- Since 0.7.0.0
-{-# INLINE sFindIndices #-}
-sFindIndices :: (Dom f a, CFoldable f, SingI n) => (a -> Bool) -> Sized f n a -> [Ordinal n]
-sFindIndices = S.sFindIndices @Nat
-
--- | Returns the index of the given element in the list, if exists.
---
--- Since 0.7.0.0
-{-# INLINE elemIndex #-}
-elemIndex :: (Dom f a, CFoldable f, Eq a) => a -> Sized f n a -> Maybe Int
-elemIndex = S.elemIndex @Nat
-
-sElemIndex, sUnsafeElemIndex :: (Dom f a, SingI n, CFoldable f, Eq a) => a -> Sized f n a -> Maybe (Ordinal n)
-{-# DEPRECATED sUnsafeElemIndex "Use sElemIndex instead" #-}
-
--- | Ordinal version of 'elemIndex'.
---   Since 0.7.0.0, we no longer do boundary check inside the definition.
---
---   Since 0.7.0.0
-sUnsafeElemIndex = S.sElemIndex @Nat
-
--- | Ordinal version of 'elemIndex'.
---   Since 0.7.0.0, we no longer do boundary check inside the definition.
---
---   Since 0.7.0.0
-sElemIndex = S.sElemIndex @Nat
-
--- | Returns all indices of the given element in the list.
---
--- Since 0.8.0.0
-{-# INLINE elemIndices #-}
-elemIndices :: (Dom f a, CFoldable f, Eq a) => a -> Sized f n a -> [Int]
-elemIndices = S.elemIndices @Nat
-
--- | Ordinal version of 'elemIndices'
---
--- Since 0.8.0.0
-{-# INLINE sElemIndices #-}
-sElemIndices
-  :: (Dom f a, CFoldable f, SingI n, Eq a)
-  => a -> Sized f n a -> [Ordinal n]
-sElemIndices = S.sElemIndices @Nat
-
-
---------------------------------------------------------------------------------
--- Views and Patterns
---------------------------------------------------------------------------------
-
-{-$ViewsAndPatterns #ViewsAndPatterns#
-
-   With GHC's @ViewPatterns@ and @PatternSynonym@ extensions,
-   we can pattern-match on arbitrary @Sized f n a@ if @f@ is list-like functor.
-   Curretnly, there are two direction view and patterns: Cons and Snoc.
-   Assuming underlying sequence type @f@ has O(1) implementation for 'cnull', 'chead'
-   (resp. 'clast') and 'ctail' (resp. 'cinit'), We can view and pattern-match on
-   cons (resp. snoc) of @Sized f n a@ in O(1).
--}
-
-{-$views #views#
-
-   With @ViewPatterns@ extension, we can pattern-match on 'Sized' value as follows:
-
-@
-slen :: ('KnownNat' n, 'Dom f a' f) => 'Sized' f n a -> 'Sing' n
-slen ('viewCons' -> 'NilCV')    = 'SZ'
-slen ('viewCons' -> _ ':-' as) = 'SS' (slen as)
-slen _                          = error "impossible"
-@
-
-   The constraint @('KnownNat' n, 'Dom f 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 :: ('KnownNat' n, 'Dom f 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.7.0.0
-type ConsView f (n :: Nat) a = S.ConsView f n a
-
--- | Since 0.8.0.0
-pattern NilCV
-  :: forall (f :: Type -> Type) n a. ()
-  => (n ~ 'Z)
-  => ConsView f n a
-pattern NilCV = S.NilCV
-
--- | Since 0.8.0.0
-pattern (:-)
-  :: forall (f :: Type -> Type) n a. ()
-  => forall n1. (n ~ (One + n1), SingI n1)
-  => a -> Sized f n1 a -> ConsView f n a
-pattern l :- ls = l S.:- ls
-
-infixr 9 :-
-{-# COMPLETE NilCV, (:-) #-}
-
--- | Case analysis for the cons-side of sequence.
---
--- Since 0.5.0.0 (type changed)
-viewCons :: (Dom f a, SingI n, CFreeMonoid f) => Sized f n a -> ConsView f n a
-viewCons = S.viewCons @Nat
-
--- | View of the left end of sequence (snoc-side).
---
--- Since 0.7.0.0
-type SnocView f (n :: Nat) a = S.SnocView f n a
-
--- | Since 0.8.0.0
-pattern NilSV
-  :: forall (f :: Type -> Type) n a. ()
-  => (n ~ 'Z)
-  => SnocView f n a
-pattern NilSV = S.NilSV
-
-infixl 9 :-::
--- | Since 0.8.0.0
-pattern (:-::)
-  :: forall (f :: Type -> Type) n a. ()
-  => forall n1. (n ~ (n1 + One), SingI n1)
-  => Sized f n1 a -> a -> SnocView f n a
-pattern ls :-:: l = ls S.:-:: l
-{-# COMPLETE NilSV, (:-::) #-}
-
--- | Case analysis for the snoc-side of sequence.
---
--- Since 0.8.0.0 (type changed)
-viewSnoc :: (Dom f a, SingI n, CFreeMonoid f) => Sized f n a -> ConsView f n a
-viewSnoc = S.viewCons @Nat
-
-
-{-$patterns #patterns#
-
-   So we can pattern match on both end of sequence via views, but
-   it is rather clumsy to nest it. For example:
-
-@
-nextToHead :: ('Dom f 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 :: ('Dom f 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, 'Dom f a' f) => 'Sized' f n a -> 'Sing' n
-slen 'Nil'      = 'SZ'
-slen (_ ':<' as) = 'SS' (slen as)
-slen _           = error "impossible"
-@
-
-   So, we can use @':<'@ and @'Nil'@ (resp. @':>'@ and @'Nil'@) to
-   pattern-match directly on cons-side (resp. snoc-side) as we usually do for lists.
-   @'Nil'@, @':<'@, and @':>'@ are neither functions nor data constructors,
-   but pattern synonyms so we cannot use them in expression contexts.
-   For more detail on pattern synonyms, see
-   <http://www.haskell.org/ghc/docs/latest/html/users_guide/syntax-extns.html#pattern-synonyms GHC Users Guide>
-   and
-   <https://ghc.haskell.org/trac/ghc/wiki/PatternSynonyms HaskellWiki>.
--}
-
--- | Pattern synonym for cons-side uncons.
-pattern (:<)
-  :: forall (f :: Type -> Type) a (n :: Nat).
-      (Dom f a, SingI n, CFreeMonoid f)
-  => forall (n1 :: Nat). (n ~ Succ n1, SingI n1)
-  => a -> Sized f n1 a -> Sized f n a
-pattern a :< b = a S.:< b
-infixr 5 :<
-
--- | Pattern synonym for a nil sequence.
-pattern Nil
-  :: forall (f :: Type -> Type) a n.
-      (Dom f a, SingI n, CFreeMonoid f)
-  => (n ~ 'Z) => Sized f n a
-pattern Nil = S.Nil
-
--- | Pattern synonym for cons-side nil.
-pattern NilL :: forall f (n :: Nat) a.
-                (SingI n, CFreeMonoid f, Dom f a)
-             => n ~ 'Z => Sized f n a
-pattern NilL = Nil
-
--- | Pattern synonym for snoc-side unsnoc.
-pattern (:>)
-  :: forall (f :: Type -> Type) a (n :: Nat).
-      (Dom f a, SingI n, CFreeMonoid f)
-  => forall (n1 :: Nat). (n ~ (n1 + One), SingI n1)
-  => Sized f n1 a -> a -> Sized f n a
-pattern a :> b = a S.:> b
-infixl 5 :>
-
--- | Pattern synonym for snoc-side nil.
-pattern NilR :: forall f (n :: Nat) a.
-                (CFreeMonoid f, Dom f a,  SingI n)
-             => n ~ 'Z => Sized f n a
-pattern NilR = Nil
-{-# COMPLETE (:<), NilL #-}
-{-# COMPLETE (:<), NilR #-}
-{-# COMPLETE (:<), Nil #-}
-{-# COMPLETE (:>), NilL #-}
-{-# COMPLETE (:>), NilR #-}
-{-# COMPLETE (:>), Nil #-}
diff --git a/test/opt-test.hs b/test/opt-test.hs
--- a/test/opt-test.hs
+++ b/test/opt-test.hs
@@ -1,42 +1,50 @@
-{-# LANGUAGE DataKinds, RankNTypes, TemplateHaskell #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TemplateHaskell #-}
 {-# OPTIONS_GHC -O2 -fno-hpc #-}
 {-# OPTIONS_GHC -dsuppress-idinfo -dsuppress-coercions
       -dsuppress-type-applications
       -dsuppress-module-prefixes -dsuppress-type-signatures
       -dsuppress-uniques #-}
+
 module Main where
-import           Control.Subcategory
-import qualified Data.Sequence           as Seq
-import           Data.Singletons.Prelude
-import           Data.Sized.Builtin      (Sized, zipWithSame)
-import qualified Data.Sized.Builtin      as SV
-import qualified Data.Vector             as V
-import qualified Data.Vector.Generic     as G
-import           Data.Vector.Storable    (Storable)
-import qualified Data.Vector.Storable    as S
-import           Data.Vector.Unboxed     (Unbox)
-import qualified Data.Vector.Unboxed     as U
-import           Numeric.Natural         (Natural)
-import           Shared
-import           Test.Hspec
-import           Test.Inspection
 
+import Control.Subcategory
+import qualified Data.Sequence as Seq
+import Data.Sized.Builtin (Sized, zipWithSame)
+import qualified Data.Sized.Builtin as SV
+import Data.Type.Natural
+import qualified Data.Vector as V
+import qualified Data.Vector.Generic as G
+import Data.Vector.Storable (Storable)
+import qualified Data.Vector.Storable as S
+import Data.Vector.Unboxed (Unbox)
+import qualified Data.Vector.Unboxed as U
+import Numeric.Natural (Natural)
+import Shared
+import Test.Hspec
+import Test.Inspection
+
 type LSized = Sized []
+
 type VSized = Sized V.Vector
+
 type USized = Sized U.Vector
+
 type SSized = Sized S.Vector
+
 type SeqSized = Sized Seq.Seq
 
-zipWith_subcat_List
-  :: (Int -> Int -> Int) -> [Int] -> [Int] -> [Int]
+zipWith_subcat_List ::
+  (Int -> Int -> Int) -> [Int] -> [Int] -> [Int]
 zipWith_subcat_List = czipWith
 
-zipWith_List
-  :: (Int -> Int -> Int) -> LSized n Int -> LSized m Int -> LSized (Min n m) Int
+zipWith_List ::
+  (Int -> Int -> Int) -> LSized n Int -> LSized m Int -> LSized (Min n m) Int
 zipWith_List = SV.zipWith
 
-zipWithSame_List
-  :: (Int -> Int -> Int) -> LSized n Int -> LSized n Int -> LSized n Int
+zipWithSame_List ::
+  (Int -> Int -> Int) -> LSized n Int -> LSized n Int -> LSized n Int
 zipWithSame_List = zipWithSame
 
 zipWith_List_Prel :: (Int -> Int -> Int) -> [Int] -> [Int] -> [Int]
@@ -45,36 +53,47 @@
 zipWithSame_Boxed :: (a -> b -> c) -> VSized n a -> VSized n b -> VSized n c
 zipWithSame_Boxed = zipWithSame
 
-zipWithSame_Boxed_mono
-  :: (Int -> (Integer -> Bool) -> [Int])
-  -> VSized n Int -> VSized n (Integer -> Bool) -> VSized n [Int]
+zipWithSame_Boxed_mono ::
+  (Int -> (Integer -> Bool) -> [Int]) ->
+  VSized n Int ->
+  VSized n (Integer -> Bool) ->
+  VSized n [Int]
 zipWithSame_Boxed_mono = zipWithSame
 
-zipWithSame_Unboxed
-  :: (Unbox a, Unbox b, Unbox c)
-  => (a -> b -> c) -> USized n a -> USized n b -> USized n c
+zipWithSame_Unboxed ::
+  (Unbox a, Unbox b, Unbox c) =>
+  (a -> b -> c) ->
+  USized n a ->
+  USized n b ->
+  USized n c
 zipWithSame_Unboxed = zipWithSame
 
-zipWithSame_Unboxed_monomorphic
-  :: (Int -> Char -> Bool) -> USized n Int -> USized n Char -> USized n Bool
+zipWithSame_Unboxed_monomorphic ::
+  (Int -> Char -> Bool) -> USized n Int -> USized n Char -> USized n Bool
 zipWithSame_Unboxed_monomorphic = zipWithSame
 
-zipWith_Unboxed
-  :: (Unbox a, Unbox b, Unbox c)
-  => (a -> b -> c) -> U.Vector a -> U.Vector b -> U.Vector c
+zipWith_Unboxed ::
+  (Unbox a, Unbox b, Unbox c) =>
+  (a -> b -> c) ->
+  U.Vector a ->
+  U.Vector b ->
+  U.Vector c
 zipWith_Unboxed = U.zipWith
 
-zipWith_Unboxed_monomorphic
-  :: (Int -> Char -> Bool) -> U.Vector Int -> U.Vector Char -> U.Vector Bool
+zipWith_Unboxed_monomorphic ::
+  (Int -> Char -> Bool) -> U.Vector Int -> U.Vector Char -> U.Vector Bool
 zipWith_Unboxed_monomorphic = U.zipWith
 
-zipWithSame_Storable
-  :: (Storable a, Storable b, Storable c)
-  => (a -> b -> c) -> SSized n a -> SSized n b -> SSized n c
+zipWithSame_Storable ::
+  (Storable a, Storable b, Storable c) =>
+  (a -> b -> c) ->
+  SSized n a ->
+  SSized n b ->
+  SSized n c
 zipWithSame_Storable = zipWithSame
 
-zipWithSame_Seq
-  :: (a -> b -> c) -> SeqSized n a -> SeqSized n b -> SeqSized n c
+zipWithSame_Seq ::
+  (a -> b -> c) -> SeqSized n a -> SeqSized n b -> SeqSized n c
 zipWithSame_Seq = zipWithSame
 
 zipWith_Boxed :: (a -> b -> c) -> V.Vector a -> V.Vector b -> V.Vector c
@@ -89,66 +108,66 @@
 main :: IO ()
 main = hspec $ do
   describe "czipWith" $ do
-    $(inspecting "doesn't contain type classes"
-      $ hasNoTypeClasses 'zipWith_subcat_List
-      )
+    $( inspecting "doesn't contain type classes" $
+        hasNoTypeClasses 'zipWith_subcat_List
+     )
   describe "zipWith" $ do
-    $(inspecting "doesn't contain type classes"
-      $ hasNoTypeClasses 'zipWith_List
-      )
+    $( inspecting "doesn't contain type classes" $
+        hasNoTypeClasses 'zipWith_List
+     )
   describe "zipWithSame" $ do
     describe "list" $ do
       it "doesn't contain type classes" $
         checkInspection
-        $(inspectTest
-          $ hasNoTypeClasses 'zipWithSame_List
-          )
+          $( inspectTest $
+              hasNoTypeClasses 'zipWithSame_List
+           )
       it "is almost the same as the original zipWith (list)" $
         checkInspection
-          $(inspectTest $
+          $( inspectTest $
               'zipWithSame_List ==- 'zipWith_List_Prel
-          )
+           )
     describe "Boxed Vector" $ do
       it "doesn't contain type classes, except for G.Vector" $
         checkInspection
-        $(inspectTest
-          $ 'zipWithSame_Boxed `hasNoTypeClassesExcept`
-            [''G.Vector]
-          )
+          $( inspectTest $
+              'zipWithSame_Boxed
+                `hasNoTypeClassesExcept` [''G.Vector]
+           )
       it "is almost the same as the original zipWith (Boxed)" $
         checkInspection
-          $(inspectTest $
+          $( inspectTest $
               'zipWithSame_Boxed ==- 'zipWith_Boxed
-          )
+           )
     describe "Unboxed Vector" $ do
       it "doesn't contain type classes except for Unbox" $
         checkInspection
-        $(inspectTest
-          $ 'zipWithSame_Unboxed `hasNoTypeClassesExcept`
-            [''Unbox]
-          )
+          $( inspectTest $
+              'zipWithSame_Unboxed
+                `hasNoTypeClassesExcept` [''Unbox]
+           )
       it "doesn't contain type classes if fully instnatiated" $
         checkInspection
-        $(inspectTest
-          $ hasNoTypeClasses 'zipWithSame_Unboxed_monomorphic
-          )
+          $( inspectTest $
+              hasNoTypeClasses 'zipWithSame_Unboxed_monomorphic
+           )
       it "is almost the same as the original zipWith, if fully instantiated" $
         checkInspection
-          $(inspectTest $
+          $( inspectTest $
               'zipWithSame_Unboxed_monomorphic
-              ==- 'zipWith_Unboxed_monomorphic
-          )
+                ==- 'zipWith_Unboxed_monomorphic
+           )
   describe "length" $ do
     it "is a constant function when length is concrete (with Dom dictionary)" $
       checkInspection
-        $(inspectTest $
-          'length_two ==- 'const_two_dom
-          )
+        $( inspectTest $
+            'length_two ==- 'const_two_dom
+         )
     it "doesn't contain Integer when the length is concrete" $
       checkInspection
-        $(inspectTest $ hasNoType 'length_two ''Integer
-        )
+        $( inspectTest $ hasNoType 'length_two ''Integer
+         )
     it "doesn't contain Natural when the length is concrete" $
       checkInspection
-        $(inspectTest $ hasNoType 'length_two ''Natural
-        )
+        $( inspectTest $ hasNoType 'length_two ''Natural
+         )