diff --git a/generics-sop/generics-sop.cabal b/generics-sop/generics-sop.cabal
index 493b623..7f66f46 100644
--- a/generics-sop/generics-sop.cabal
+++ b/generics-sop/generics-sop.cabal
@@ -66,7 +66,7 @@ library
                        Generics.SOP.NS
                        Generics.SOP.Sing
   build-depends:       base                 >= 4.9  && < 4.16,
-                       sop-core             == 0.5.0.*,
+                       sop-core             == 0.5.1.*,
                        template-haskell     >= 2.8  && < 2.18,
                        th-abstraction       >= 0.4  && < 0.5,
                        ghc-prim             >= 0.3  && < 0.8
diff --git a/generics-sop/src/Generics/SOP/GGP.hs b/generics-sop/src/Generics/SOP/GGP.hs
index 7b3e6ff..5bb5aae 100644
--- a/generics-sop/src/Generics/SOP/GGP.hs
+++ b/generics-sop/src/Generics/SOP/GGP.hs
@@ -222,7 +222,7 @@ gfrom x = gSumFrom (GHC.from x) (Proxy :: Proxy '[])
 -- For more info, see 'Generics.SOP.Generic'.
 --
 gto :: forall a. (GTo a, GHC.Generic a) => SOP I (GCode a) -> a
-gto x = GHC.to (gSumTo x id ((\y -> case y of {}) :: SOP I '[] -> (GHC.Rep a) x))
+gto x = GHC.to (gSumTo x id ((\y -> case emptySOP y of {}) :: SOP I '[] -> (GHC.Rep a) x))
 
 -- | An automatically computed version of 'Generics.SOP.datatypeInfo'.
 --
@@ -234,4 +234,3 @@ gto x = GHC.to (gSumTo x id ((\y -> case y of {}) :: SOP I '[] -> (GHC.Rep a) x)
 --
 gdatatypeInfo :: forall proxy a. (GDatatypeInfo a) => proxy a -> DatatypeInfo (GCode a)
 gdatatypeInfo _ = SOP.T.demoteDatatypeInfo (Proxy :: Proxy (GDatatypeInfoOf a))
-
diff --git a/sop-core/sop-core.cabal b/sop-core/sop-core.cabal
index a87a8cd..8ac00a5 100644
--- a/sop-core/sop-core.cabal
+++ b/sop-core/sop-core.cabal
@@ -1,5 +1,5 @@
 name:                sop-core
-version:             0.5.0.1
+version:             0.5.1.0
 synopsis:            True Sums of Products
 description:
   Implementation of n-ary sums and n-ary products.
@@ -42,7 +42,8 @@ library
                        Data.SOP.NS
                        Data.SOP.Sing
   build-depends:       base                 >= 4.9  && < 4.16,
-                       deepseq              >= 1.3  && < 1.5
+                       deepseq              >= 1.3  && < 1.5,
+                       vector               >= 0.12 && < 0.13
   hs-source-dirs:      src
   default-language:    Haskell2010
   ghc-options:         -Wall
diff --git a/sop-core/src/Data/SOP/NP.hs b/sop-core/src/Data/SOP/NP.hs
index 4d92cfb..d6ce9d2 100644
--- a/sop-core/src/Data/SOP/NP.hs
+++ b/sop-core/src/Data/SOP/NP.hs
@@ -1,8 +1,13 @@
-{-# LANGUAGE PolyKinds, StandaloneDeriving, UndecidableInstances #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ViewPatterns #-}
+
 -- | n-ary products (and products of products)
 module Data.SOP.NP
   ( -- * Datatypes
-    NP(..)
+    NP(.., Nil, (:*))
   , POP(..)
   , unPOP
     -- * Constructing products
@@ -90,6 +95,8 @@ module Data.SOP.NP
 import Data.Coerce
 import Data.Kind (Type)
 import Data.Proxy (Proxy(..))
+import qualified Data.Vector as V
+import GHC.Exts (Any)
 import Unsafe.Coerce
 #if !MIN_VERSION_base(4,11,0)
 import Data.Semigroup (Semigroup (..))
@@ -110,8 +117,14 @@ import Data.SOP.Sing
 -- @i@-th element of the list is of type @x@, then the @i@-th
 -- element of the product is of type @f x@.
 --
--- The constructor names are chosen to resemble the names of the
--- list constructors.
+-- The pattern synoyms are chosen to resemble the names of the
+-- list constructors. @NP@ is morally equivalent to:
+--
+-- > data NP :: (k -> Type) -> [k] -> Type where
+-- >   Nil  :: NP f '[]
+-- >   (:*) :: f x -> NP f xs -> NP f (x ': xs)
+--
+-- The actual representation however is compact, using an array.
 --
 -- Two common instantiations of @f@ are the identity functor 'I'
 -- and the constant functor 'K'. For 'I', the product becomes a
@@ -130,12 +143,40 @@ import Data.SOP.Sing
 -- > K 0      :* K 1     :* Nil  ::  NP (K Int) '[ Char, Bool ]
 -- > Just 'x' :* Nothing :* Nil  ::  NP Maybe   '[ Char, Bool ]
 --
-data NP :: (k -> Type) -> [k] -> Type where
-  Nil  :: NP f '[]
-  (:*) :: f x -> NP f xs -> NP f (x ': xs)
+newtype NP (f :: k -> *) (xs :: [k]) = NP (V.Vector Any)
+
+-- | View on NP
+--
+-- This is only used internally, for the definition of the pattern synonyms.
+data ViewNP (f :: k -> *) (xs :: [k]) where
+  IsNil  :: ViewNP f '[]
+  IsCons :: f x -> NP f xs -> ViewNP f (x ': xs)
+
+-- | Construct 'ViewNP'
+--
+-- NOTE: 'V.unsafeTail' is O(1).
+viewNP :: NP f xs -> ViewNP f xs
+viewNP (NP xs)
+  | null xs   = unsafeCoerce $ IsNil
+  | otherwise = unsafeCoerce $ IsCons (unsafeCoerce (V.unsafeHead xs))
+                                      (NP (V.unsafeTail xs))
 
+pattern Nil :: forall f xs . () => (xs ~ '[]) => NP f xs
+pattern Nil <- (viewNP -> IsNil)
+  where
+    Nil = NP V.empty
+
+pattern (:*) :: forall f xs' . ()
+             => forall x xs . (xs' ~ (x ': xs)) => f x -> NP f xs -> NP f xs'
+pattern x :* xs <- (viewNP -> IsCons x xs)
+  where
+    x :* NP xs = NP (V.cons (unsafeCoerce x) xs)
 infixr 5 :*
 
+#if __GLASGOW_HASKELL__ >= 802
+{-# COMPLETE Nil, (:*) #-}
+#endif
+
 -- This is written manually,
 -- because built-in deriving doesn't use associativity information!
 instance All (Show `Compose` f) xs => Show (NP f xs) where
@@ -145,8 +186,13 @@ instance All (Show `Compose` f) xs => Show (NP f xs) where
     . showString " :* "
     . showsPrec 5 fs
 
-deriving instance All (Eq   `Compose` f) xs => Eq   (NP f xs)
-deriving instance (All (Eq `Compose` f) xs, All (Ord `Compose` f) xs) => Ord (NP f xs)
+instance All (Eq `Compose` f) xs => Eq (NP f xs) where
+  xs == ys =
+    and (hcollapse (hczipWith (Proxy :: Proxy (Eq `Compose` f)) (\ x y -> K (x == y)) xs ys))
+
+instance (All (Eq `Compose` f) xs, All (Ord `Compose` f) xs) => Ord (NP f xs) where
+  compare xs ys =
+    mconcat (hcollapse (hczipWith (Proxy :: Proxy (Ord `Compose` f)) (\ x y -> K (compare x y)) xs ys))
 
 -- | @since 0.4.0.0
 instance All (Semigroup `Compose` f) xs => Semigroup (NP f xs) where
diff --git a/sop-core/src/Data/SOP/NS.hs b/sop-core/src/Data/SOP/NS.hs
index 5424132..7144fe2 100644
--- a/sop-core/src/Data/SOP/NS.hs
+++ b/sop-core/src/Data/SOP/NS.hs
@@ -1,14 +1,18 @@
 {-# LANGUAGE BangPatterns #-}
 {-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ViewPatterns #-}
+
 {-# OPTIONS_GHC -fno-warn-deprecations #-}
+
 -- | n-ary sums (and sums of products)
 module Data.SOP.NS
   ( -- * Datatypes
-    NS(..)
+    NS(.., Z, S)
   , SOP(..)
   , unSOP
     -- * Constructing sums
@@ -20,7 +24,11 @@ module Data.SOP.NS
   , apInjs'_NP
   , apInjs_POP
   , apInjs'_POP
+  -- See also 'emptySOP'.
+  --
     -- * Destructing sums
+  , emptyNS
+  , emptySOP
   , unZ
   , index_NS
   , index_SOP
@@ -94,6 +102,9 @@ module Data.SOP.NS
 import Data.Coerce
 import Data.Kind (Type)
 import Data.Proxy (Proxy (..))
+import qualified Data.Vector as V
+import Data.Void (Void)
+import GHC.Exts (Any)
 import Unsafe.Coerce
 
 import Control.DeepSeq (NFData(..))
@@ -114,10 +125,16 @@ import Data.SOP.Sing
 -- @i@-th element of the list is of type @x@, then the @i@-th
 -- choice of the sum is of type @f x@.
 --
--- The constructor names are chosen to resemble Peano-style
+-- The pattern synonym names are chosen to resemble Peano-style
 -- natural numbers, i.e., 'Z' is for "zero", and 'S' is for
 -- "successor". Chaining 'S' and 'Z' chooses the corresponding
--- component of the sum.
+-- component of the sum. @NS@ is morally equivalent to
+--
+-- > data NS :: (k -> Type) -> [k] -> Type where
+-- >   Z :: f x -> NS f (x ': xs)
+-- >   S :: NS f xs -> NS f (x ': xs)
+--
+-- The actual representation however is compact, using just an 'Int'.
 --
 -- /Examples:/
 --
@@ -146,13 +163,45 @@ import Data.SOP.Sing
 -- > S (Z (I True)) :: NS I       '[ Char, Bool ]
 -- > S (Z (K 1))    :: NS (K Int) '[ Char, Bool ]
 --
-data NS :: (k -> Type) -> [k] -> Type where
-  Z :: f x -> NS f (x ': xs)
-  S :: NS f xs -> NS f (x ': xs)
+data NS (f :: k -> *) (xs :: [k]) = NS !Int Any
+
+-- | View on NP
+--
+-- This is only used internally, for the definition of the pattern synonyms.
+data ViewNS (f :: k -> *) (xs :: [k]) where
+  IsZ :: f x     -> ViewNS f (x ': xs)
+  IsS :: NS f xs -> ViewNS f (x ': xs)
+
+viewNS :: NS f xs -> ViewNS f xs
+viewNS (NS i x)
+  | i == 0    = unsafeCoerce (IsZ (unsafeCoerce x))
+  | otherwise = unsafeCoerce (IsS (NS (i - 1) x))
+
+pattern Z :: forall f xs' . ()
+          => forall x xs . (xs' ~ (x ': xs)) => f x -> NS f xs'
+pattern Z x <- (viewNS -> IsZ x)
+  where
+    Z x = NS 0 (unsafeCoerce x)
+
+pattern S :: forall f xs' . ()
+          => forall x xs . (xs' ~ (x ': xs)) => NS f xs -> NS f xs'
+pattern S p <- (viewNS -> IsS p)
+  where
+    S (NS i x) = NS (i + 1) x
+
+#if __GLASGOW_HASKELL__ >= 802
+{-# COMPLETE Z, S #-}
+#endif
 
-deriving instance All (Show `Compose` f) xs => Show (NS f xs)
-deriving instance All (Eq   `Compose` f) xs => Eq   (NS f xs)
-deriving instance (All (Eq `Compose` f) xs, All (Ord `Compose` f) xs) => Ord (NS f xs)
+instance All (Show `Compose` f) xs => Show (NS f xs) where
+  show ns @ (NS i _) =
+    show i ++ " " ++ hcollapse (hcmap (Proxy :: Proxy (Show `Compose` f)) (K . show) ns)
+
+instance All (Eq `Compose` f) xs => Eq (NS f xs) where
+  (==) = ccompare_NS (Proxy :: Proxy (Eq `Compose` f)) False (==) False
+
+instance (All (Eq `Compose` f) xs, All (Ord `Compose` f) xs) => Ord (NS f xs) where
+  compare = ccompare_NS (Proxy :: Proxy (Ord `Compose` f)) LT compare GT
 
 -- | @since 0.2.5.0
 instance All (NFData `Compose` f) xs => NFData (NS f xs) where
@@ -188,6 +237,34 @@ ejections = case sList :: SList xs of
 shiftEjection :: forall f x xs a . Ejection f xs a -> Ejection f (x ': xs) a
 shiftEjection (Fn f) = Fn $ (\ns -> case ns of Z _ -> Comp Nothing; S s -> f (K s)) . unK
 
+-- | An 'NS' cannot be empty.
+--
+-- Although the 'Z'/'S' pattern synonyms are marked as @COMPLETE@, older @ghc@
+-- (before 8.10) are not clever enough to deduce from that an empty pattern
+-- match in which both @Z@ and @S@ would be type incorrect is not, in fact,
+-- incomplete. This function can be used to avoid warnings in such cases;
+-- instead of writing
+--
+-- > case x of {}
+--
+-- (where @x :: NS f '[])@), instead write
+--
+-- > case emptyNS x of {}
+--
+-- See also 'emptySOP'.
+--
+-- @since 0.5.1.0
+emptyNS :: NS f '[] -> Void
+emptyNS _ = error "emptyNS: impossible"
+
+-- | An 'SOP' cannot be empty (beacuse an 'NS' cannot be).
+--
+-- See also 'emptyNS'.
+--
+-- @since 0.5.1.0
+emptySOP :: SOP f '[] -> Void
+emptySOP = emptyNS . unSOP
+
 -- | Extract the payload from a unary sum.
 --
 -- For larger sums, this function would be partial, so it is only
@@ -201,8 +278,7 @@ shiftEjection (Fn f) = Fn $ (\ns -> case ns of Z _ -> Comp Nothing; S s -> f (K
 -- @since 0.2.2.0
 --
 unZ :: NS f '[x] -> f x
-unZ (Z x) = x
-unZ (S x) = case x of {}
+unZ (NS _ x) = unsafeCoerce x
 
 -- | Obtain the index from an n-ary sum.
 --
@@ -385,18 +461,14 @@ instance HApInjs SOP where
 
 -- | Specialization of 'hap'.
 ap_NS :: NP (f -.-> g) xs -> NS f xs -> NS g xs
-ap_NS (Fn f  :* _)   (Z x)   = Z (f x)
-ap_NS (_     :* fs)  (S xs)  = S (ap_NS fs xs)
-ap_NS Nil            x       = case x of {}
+ap_NS (NP fs) (NS i x) = NS i (unsafeCoerce (fs V.! i) x)
 
 -- | Specialization of 'hap'.
 ap_SOP  :: POP (f -.-> g) xss -> SOP f xss -> SOP g xss
 ap_SOP (POP fss') (SOP xss') = SOP (go fss' xss')
   where
     go :: NP (NP (f -.-> g)) xss -> NS (NP f) xss -> NS (NP g) xss
-    go (fs :* _  ) (Z xs ) = Z (ap_NP fs  xs )
-    go (_  :* fss) (S xss) = S (go    fss xss)
-    go Nil         x       = case x of {}
+    go (NP nps) (NS i ns) = NS i (unsafeCoerce ap_NS (nps V.! i) ns)
 
 -- The definition of 'ap_SOP' is a more direct variant of
 -- '_ap_SOP_spec'. The direct definition has the advantage