diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright (c) 2014, Well-Typed LLP, Edsko de Vries, Andres Löh
+Copyright (c) 2014-2015, Well-Typed LLP, Edsko de Vries, Andres Löh
 All rights reserved.
 
 Redistribution and use in source and binary forms, with or without
diff --git a/generics-sop.cabal b/generics-sop.cabal
--- a/generics-sop.cabal
+++ b/generics-sop.cabal
@@ -1,5 +1,5 @@
 name:                generics-sop
-version:             0.1.1.2
+version:             0.2.0.0
 synopsis:            Generic Programming using True Sums of Products
 description:
   A library to support the definition of generic functions.
@@ -32,11 +32,11 @@
 license:             BSD3
 license-file:        LICENSE
 author:              Edsko de Vries <edsko@well-typed.com>, Andres Löh <andres@well-typed.com>
-maintainer:          edsko@well-typed.com
+maintainer:          andres@well-typed.com
 category:            Generics
 build-type:          Simple
 cabal-version:       >=1.10
-tested-with:         GHC == 7.6.3, GHC == 7.8.2
+tested-with:         GHC == 7.6.3, GHC == 7.8.4, GHC == 7.10.2
 
 source-repository head
   type:                git
@@ -46,6 +46,7 @@
   exposed-modules:     Generics.SOP
                        Generics.SOP.GGP
                        Generics.SOP.TH
+                       Generics.SOP.Dict
                        -- exposed via Generics.SOP:
                        Generics.SOP.BasicFunctors
                        Generics.SOP.Classes
@@ -60,7 +61,7 @@
                        template-haskell     >= 2.8  && < 2.11,
                        ghc-prim             >= 0.3  && < 0.5
   if impl (ghc < 7.8)
-    build-depends:     tagged               >= 0.7  && < 0.8
+    build-depends:     tagged               >= 0.7  && < 0.9
 
   hs-source-dirs:      src
   default-language:    Haskell2010
@@ -91,3 +92,14 @@
                        TemplateHaskell
                        DeriveGeneric
                        StandaloneDeriving
+  if impl (ghc < 7.10)
+    other-extensions:    OverlappingInstances
+
+test-suite generic-sop-examples
+  type:                exitcode-stdio-1.0
+  main-is:             Example.hs
+  hs-source-dirs:      test
+  default-language:    Haskell2010
+  ghc-options:         -Wall
+  build-depends:       base                 >= 4.6  && < 5,
+                       generics-sop
diff --git a/src/Generics/SOP.hs b/src/Generics/SOP.hs
--- a/src/Generics/SOP.hs
+++ b/src/Generics/SOP.hs
@@ -254,6 +254,12 @@
   , hcliftA
   , hcliftA2
   , hcliftA3
+  , hmap
+  , hzipWith
+  , hzipWith3
+  , hcmap
+  , hczipWith
+  , hczipWith3
     -- ** Constructing sums
   , Injection
   , injections
@@ -261,8 +267,6 @@
   , apInjs_NP
   , apInjs_POP
     -- ** Dealing with @'All' c@
-  , AllDict(..)
-  , allDict_NP
   , hcliftA'
   , hcliftA2'
   , hcliftA3'
@@ -286,14 +290,19 @@
     -- ** Mapping constraints
   , All
   , All2
-  , Map
-  , AllMap
+  , Compose
+  , And
+  , Top
+  , AllN
     -- ** Singletons
-  , Sing(..)
+  , SList(..)
+  , SListI(..)
+  , Sing
   , SingI(..)
     -- *** Shape of type-level lists
   , Shape(..)
   , shape
+  , lengthSList
   , lengthSing
     -- ** Re-exports
 
diff --git a/src/Generics/SOP/Classes.hs b/src/Generics/SOP/Classes.hs
--- a/src/Generics/SOP/Classes.hs
+++ b/src/Generics/SOP/Classes.hs
@@ -34,11 +34,9 @@
 #if !(MIN_VERSION_base(4,8,0))
 import Control.Applicative (Applicative)
 #endif
-import Data.Proxy (Proxy)
 
 import Generics.SOP.BasicFunctors
 import Generics.SOP.Constraint
-import Generics.SOP.Sing
 
 -- | A generalization of 'Control.Applicative.pure' or
 -- 'Control.Monad.return' to higher kinds.
@@ -48,11 +46,11 @@
   -- /Instances:/
   --
   -- @
-  -- 'hpure', 'Generics.SOP.NP.pure_NP'  :: 'SingI' xs  => (forall a. f a) -> 'Generics.SOP.NP.NP'  f xs
-  -- 'hpure', 'Generics.SOP.NP.pure_POP' :: 'SingI' xss => (forall a. f a) -> 'Generics.SOP.NP.POP' f xss
+  -- 'hpure', 'Generics.SOP.NP.pure_NP'  :: 'SListI'  xs  => (forall a. f a) -> 'Generics.SOP.NP.NP'  f xs
+  -- 'hpure', 'Generics.SOP.NP.pure_POP' :: 'SListI2' xss => (forall a. f a) -> 'Generics.SOP.NP.POP' f xss
   -- @
   --
-  hpure  ::  SingI xs => (forall a. f a) -> h f xs
+  hpure  ::  SListIN h xs => (forall a. f a) -> h f xs
 
   -- | A variant of 'hpure' that allows passing in a constrained
   -- argument.
@@ -72,11 +70,11 @@
   -- /Instances:/
   --
   -- @
-  -- 'hcpure', 'Generics.SOP.NP.cpure_NP'  :: ('SingI' xs,  'All'  c xs ) => 'Proxy' c -> (forall a. c a => f a) -> 'Generics.SOP.NP.NP'  f xs
-  -- 'hcpure', 'Generics.SOP.NP.cpure_POP' :: ('SingI' xss, 'All2' c xss) => 'Proxy' c -> (forall a. c a => f a) -> 'Generics.SOP.NP.POP' f xss
+  -- 'hcpure', 'Generics.SOP.NP.cpure_NP'  :: ('All'  c xs ) => proxy c -> (forall a. c a => f a) -> 'Generics.SOP.NP.NP'  f xs
+  -- 'hcpure', 'Generics.SOP.NP.cpure_POP' :: ('All2' c xss) => proxy c -> (forall a. c a => f a) -> 'Generics.SOP.NP.POP' f xss
   -- @
   --
-  hcpure :: (SingI xs, AllMap h c xs) => Proxy c -> (forall a. c a => f a) -> h f xs
+  hcpure :: (AllN h c xs) => proxy c -> (forall a. c a => f a) -> h f xs
 
 {-------------------------------------------------------------------------------
   Application
@@ -118,10 +116,11 @@
 
   -- | Corresponds to 'Control.Applicative.<*>'.
   --
-  -- For products as well as products or products, the correspondence
-  -- is rather direct. We combine a structure containing (lifted)
-  -- functions and a compatible structure containing corresponding arguments
-  -- into a compatible structure containing results.
+  -- For products ('Generics.SOP.NP.NP') as well as products of products
+  -- ('Generics.SOP.NP.POP), the correspondence is rather direct. We combine
+  -- a structure containing (lifted) functions and a compatible structure
+  -- containing corresponding arguments into a compatible structure
+  -- containing results.
   --
   -- The same combinator can also be used to combine a product
   -- structure of functions with a sum structure of arguments, which then
@@ -158,13 +157,13 @@
 -- /Instances:/
 --
 -- @
--- 'hliftA', 'Generics.SOP.NP.liftA_NP'  :: 'SingI' xs  => (forall a. f a -> f' a) -> 'Generics.SOP.NP.NP'  f xs  -> 'Generics.SOP.NP.NP'  f' xs
--- 'hliftA', 'Generics.SOP.NS.liftA_NS'  :: 'SingI' xs  => (forall a. f a -> f' a) -> 'Generics.SOP.NS.NS'  f xs  -> 'Generics.SOP.NS.NS'  f' xs
--- 'hliftA', 'Generics.SOP.NP.liftA_POP' :: 'SingI' xss => (forall a. f a -> f' a) -> 'Generics.SOP.NP.POP' f xss -> 'Generics.SOP.NP.POP' f' xss
--- 'hliftA', 'Generics.SOP.NS.liftA_SOP' :: 'SingI' xss => (forall a. f a -> f' a) -> 'Generics.SOP.NS.SOP' f xss -> 'Generics.SOP.NS.SOP' f' xss
+-- 'hliftA', 'Generics.SOP.NP.liftA_NP'  :: 'SListI'  xs  => (forall a. f a -> f' a) -> 'Generics.SOP.NP.NP'  f xs  -> 'Generics.SOP.NP.NP'  f' xs
+-- 'hliftA', 'Generics.SOP.NS.liftA_NS'  :: 'SListI'  xs  => (forall a. f a -> f' a) -> 'Generics.SOP.NS.NS'  f xs  -> 'Generics.SOP.NS.NS'  f' xs
+-- 'hliftA', 'Generics.SOP.NP.liftA_POP' :: 'SListI2' xss => (forall a. f a -> f' a) -> 'Generics.SOP.NP.POP' f xss -> 'Generics.SOP.NP.POP' f' xss
+-- 'hliftA', 'Generics.SOP.NS.liftA_SOP' :: 'SListI2' xss => (forall a. f a -> f' a) -> 'Generics.SOP.NS.SOP' f xss -> 'Generics.SOP.NS.SOP' f' xss
 -- @
 --
-hliftA  :: (SingI xs, HAp h)               => (forall a. f a -> f' a)                                                   -> h f   xs -> h f'   xs
+hliftA  :: (SListIN (Prod h) xs, HAp h)               => (forall a. f a -> f' a)                                                   -> h f   xs -> h f'   xs
 
 -- | A generalized form of 'Control.Applicative.liftA2',
 -- which in turn is a generalized 'zipWith'.
@@ -184,13 +183,13 @@
 -- /Instances:/
 --
 -- @
--- 'hliftA2', 'Generics.SOP.NP.liftA2_NP'  :: 'SingI' xs  => (forall a. f a -> f' a -> f'' a) -> 'Generics.SOP.NP.NP'  f xs  -> 'Generics.SOP.NP.NP'  f' xs  -> 'Generics.SOP.NP.NP'  f'' xs
--- 'hliftA2', 'Generics.SOP.NS.liftA2_NS'  :: 'SingI' xs  => (forall a. f a -> f' a -> f'' a) -> 'Generics.SOP.NP.NP'  f xs  -> 'Generics.SOP.NS.NS'  f' xs  -> 'Generics.SOP.NS.NS'  f'' xs
--- 'hliftA2', 'Generics.SOP.NP.liftA2_POP' :: 'SingI' xss => (forall a. f a -> f' a -> f'' a) -> 'Generics.SOP.NP.POP' f xss -> 'Generics.SOP.NP.POP' f' xss -> 'Generics.SOP.NP.POP' f'' xss
--- 'hliftA2', 'Generics.SOP.NS.liftA2_SOP' :: 'SingI' xss => (forall a. f a -> f' a -> f'' a) -> 'Generics.SOP.NP.POP' f xss -> 'Generics.SOP.NS.SOP' f' xss -> 'Generics.SOP.NS.SOP' f'' xss
+-- 'hliftA2', 'Generics.SOP.NP.liftA2_NP'  :: 'SListI'  xs  => (forall a. f a -> f' a -> f'' a) -> 'Generics.SOP.NP.NP'  f xs  -> 'Generics.SOP.NP.NP'  f' xs  -> 'Generics.SOP.NP.NP'  f'' xs
+-- 'hliftA2', 'Generics.SOP.NS.liftA2_NS'  :: 'SListI'  xs  => (forall a. f a -> f' a -> f'' a) -> 'Generics.SOP.NP.NP'  f xs  -> 'Generics.SOP.NS.NS'  f' xs  -> 'Generics.SOP.NS.NS'  f'' xs
+-- 'hliftA2', 'Generics.SOP.NP.liftA2_POP' :: 'SListI2' xss => (forall a. f a -> f' a -> f'' a) -> 'Generics.SOP.NP.POP' f xss -> 'Generics.SOP.NP.POP' f' xss -> 'Generics.SOP.NP.POP' f'' xss
+-- 'hliftA2', 'Generics.SOP.NS.liftA2_SOP' :: 'SListI2' xss => (forall a. f a -> f' a -> f'' a) -> 'Generics.SOP.NP.POP' f xss -> 'Generics.SOP.NS.SOP' f' xss -> 'Generics.SOP.NS.SOP' f'' xss
 -- @
 --
-hliftA2 :: (SingI xs, HAp h, HAp (Prod h)) => (forall a. f a -> f' a -> f'' a)           -> Prod h f xs                 -> h f'  xs -> h f''  xs
+hliftA2 :: (SListIN (Prod h) xs, HAp h, HAp (Prod h)) => (forall a. f a -> f' a -> f'' a)           -> Prod h f xs                 -> h f'  xs -> h f''  xs
 
 -- | A generalized form of 'Control.Applicative.liftA3',
 -- which in turn is a generalized 'zipWith3'.
@@ -210,18 +209,29 @@
 -- /Instances:/
 --
 -- @
--- 'hliftA3', 'Generics.SOP.NP.liftA3_NP'  :: 'SingI' xs  => (forall a. f a -> f' a -> f'' a -> f''' a) -> 'Generics.SOP.NP.NP'  f xs  -> 'Generics.SOP.NP.NP'  f' xs  -> 'Generics.SOP.NP.NP'  f'' xs  -> 'Generics.SOP.NP.NP'  f''' xs
--- 'hliftA3', 'Generics.SOP.NS.liftA3_NS'  :: 'SingI' xs  => (forall a. f a -> f' a -> f'' a -> f''' a) -> 'Generics.SOP.NP.NP'  f xs  -> 'Generics.SOP.NP.NP'  f' xs  -> 'Generics.SOP.NS.NS'  f'' xs  -> 'Generics.SOP.NS.NS'  f''' xs
--- 'hliftA3', 'Generics.SOP.NP.liftA3_POP' :: 'SingI' xss => (forall a. f a -> f' a -> f'' a -> f''' a) -> 'Generics.SOP.NP.POP' f xss -> 'Generics.SOP.NP.POP' f' xss -> 'Generics.SOP.NP.POP' f'' xss -> 'Generics.SOP.NP.POP' f''' xs
--- 'hliftA3', 'Generics.SOP.NS.liftA3_SOP' :: 'SingI' xss => (forall a. f a -> f' a -> f'' a -> f''' a) -> 'Generics.SOP.NP.POP' f xss -> 'Generics.SOP.NP.POP' f' xss -> 'Generics.SOP.NS.SOP' f'' xss -> 'Generics.SOP.NP.SOP' f''' xs
+-- 'hliftA3', 'Generics.SOP.NP.liftA3_NP'  :: 'SListI'  xs  => (forall a. f a -> f' a -> f'' a -> f''' a) -> 'Generics.SOP.NP.NP'  f xs  -> 'Generics.SOP.NP.NP'  f' xs  -> 'Generics.SOP.NP.NP'  f'' xs  -> 'Generics.SOP.NP.NP'  f''' xs
+-- 'hliftA3', 'Generics.SOP.NS.liftA3_NS'  :: 'SListI'  xs  => (forall a. f a -> f' a -> f'' a -> f''' a) -> 'Generics.SOP.NP.NP'  f xs  -> 'Generics.SOP.NP.NP'  f' xs  -> 'Generics.SOP.NS.NS'  f'' xs  -> 'Generics.SOP.NS.NS'  f''' xs
+-- 'hliftA3', 'Generics.SOP.NP.liftA3_POP' :: 'SListI2' xss => (forall a. f a -> f' a -> f'' a -> f''' a) -> 'Generics.SOP.NP.POP' f xss -> 'Generics.SOP.NP.POP' f' xss -> 'Generics.SOP.NP.POP' f'' xss -> 'Generics.SOP.NP.POP' f''' xs
+-- 'hliftA3', 'Generics.SOP.NS.liftA3_SOP' :: 'SListI2' xss => (forall a. f a -> f' a -> f'' a -> f''' a) -> 'Generics.SOP.NP.POP' f xss -> 'Generics.SOP.NP.POP' f' xss -> 'Generics.SOP.NS.SOP' f'' xss -> 'Generics.SOP.NP.SOP' f''' xs
 -- @
 --
-hliftA3 :: (SingI xs, HAp h, HAp (Prod h)) => (forall a. f a -> f' a -> f'' a -> f''' a) -> Prod h f xs -> Prod h f' xs -> h f'' xs -> h f''' xs
+hliftA3 :: (SListIN (Prod h) xs, HAp h, HAp (Prod h)) => (forall a. f a -> f' a -> f'' a -> f''' a) -> Prod h f xs -> Prod h f' xs -> h f'' xs -> h f''' xs
 
 hliftA  f xs       = hpure (fn   f) `hap` xs
 hliftA2 f xs ys    = hpure (fn_2 f) `hap` xs `hap` ys
 hliftA3 f xs ys zs = hpure (fn_3 f) `hap` xs `hap` ys `hap` zs
 
+-- | Another name for 'hliftA'.
+hmap      :: (SListIN (Prod h) xs, HAp h)               => (forall a. f a -> f' a)                                                   -> h f   xs -> h f'   xs
+-- | Another name for 'hliftA2'.
+hzipWith  :: (SListIN (Prod h) xs, HAp h, HAp (Prod h)) => (forall a. f a -> f' a -> f'' a)           -> Prod h f xs                 -> h f'  xs -> h f''  xs
+-- | Another name for 'hliftA3'.
+hzipWith3 :: (SListIN (Prod h) xs, HAp h, HAp (Prod h)) => (forall a. f a -> f' a -> f'' a -> f''' a) -> Prod h f xs -> Prod h f' xs -> h f'' xs -> h f''' xs
+
+hmap      = hliftA
+hzipWith  = hliftA2
+hzipWith3 = hliftA3
+
 -- | Variant of 'hliftA' that takes a constrained function.
 --
 -- /Specification:/
@@ -230,7 +240,7 @@
 -- 'hcliftA' p f xs = 'hcpure' p ('fn' f) \` 'hap' \` xs
 -- @
 --
-hcliftA  :: (AllMap (Prod h) c xs, SingI xs, HAp h)               => Proxy c -> (forall a. c a => f a -> f' a)                                                   -> h f   xs -> h f'   xs
+hcliftA  :: (AllN (Prod h) c xs, HAp h)               => proxy c -> (forall a. c a => f a -> f' a)                                                   -> h f   xs -> h f'   xs
 
 -- | Variant of 'hcliftA2' that takes a constrained function.
 --
@@ -240,7 +250,7 @@
 -- 'hcliftA2' p f xs ys = 'hcpure' p ('fn_2' f) \` 'hap' \` xs \` 'hap' \` ys
 -- @
 --
-hcliftA2 :: (AllMap (Prod h) c xs, SingI xs, HAp h, HAp (Prod h)) => Proxy c -> (forall a. c a => f a -> f' a -> f'' a)           -> Prod h f xs                 -> h f'  xs -> h f''  xs
+hcliftA2 :: (AllN (Prod h) c xs, HAp h, HAp (Prod h)) => proxy c -> (forall a. c a => f a -> f' a -> f'' a)           -> Prod h f xs                 -> h f'  xs -> h f''  xs
 
 -- | Variant of 'hcliftA3' that takes a constrained function.
 --
@@ -250,14 +260,25 @@
 -- 'hcliftA3' p f xs ys zs = 'hcpure' p ('fn_3' f) \` 'hap' \` xs \` 'hap' \` ys \` 'hap' \` zs
 -- @
 --
-hcliftA3 :: (AllMap (Prod h) c xs, SingI xs, HAp h, HAp (Prod h)) => Proxy c -> (forall a. c a => f a -> f' a -> f'' a -> f''' a) -> Prod h f xs -> Prod h f' xs -> h f'' xs -> h f''' xs
+hcliftA3 :: (AllN (Prod h) c xs, HAp h, HAp (Prod h)) => proxy c -> (forall a. c a => f a -> f' a -> f'' a -> f''' a) -> Prod h f xs -> Prod h f' xs -> h f'' xs -> h f''' xs
 
 hcliftA  p f xs       = hcpure p (fn   f) `hap` xs
 hcliftA2 p f xs ys    = hcpure p (fn_2 f) `hap` xs `hap` ys
 hcliftA3 p f xs ys zs = hcpure p (fn_3 f) `hap` xs `hap` ys `hap` zs
 
+-- | Another name for 'hcliftA'.
+hcmap      :: (AllN (Prod h) c xs, HAp h)               => proxy c -> (forall a. c a => f a -> f' a)                                                   -> h f   xs -> h f'   xs
+-- | Another name for 'hcliftA2'.
+hczipWith  :: (AllN (Prod h) c xs, HAp h, HAp (Prod h)) => proxy c -> (forall a. c a => f a -> f' a -> f'' a)           -> Prod h f xs                 -> h f'  xs -> h f''  xs
+-- | Another name for 'hcliftA3'.
+hczipWith3 :: (AllN (Prod h) c xs, HAp h, HAp (Prod h)) => proxy c -> (forall a. c a => f a -> f' a -> f'' a -> f''' a) -> Prod h f xs -> Prod h f' xs -> h f'' xs -> h f''' xs
+
+hcmap      = hcliftA
+hczipWith  = hcliftA2
+hczipWith3 = hcliftA3
+
 -- | Maps products to lists, and sums to identities.
-type family CollapseTo (h :: (k -> *) -> (l -> *)) :: * -> *
+type family CollapseTo (h :: (k -> *) -> (l -> *)) (x :: *) :: *
 
 -- | A class for collapsing a heterogeneous structure into
 -- a homogeneous one.
@@ -281,7 +302,7 @@
   -- 'hcollapse', 'Generics.SOP.NS.collapse_SOP' :: 'Generics.SOP.NP.SOP' ('K' a) xss ->  [a]
   -- @
   --
-  hcollapse :: SingI xs => h (K a) xs -> CollapseTo h a
+  hcollapse :: SListIN h xs => h (K a) xs -> CollapseTo h a
 
 -- | A generalization of 'Data.Traversable.sequenceA'.
 class HAp h => HSequence (h :: (k -> *) -> (l -> *)) where
@@ -293,18 +314,18 @@
   -- /Instances:/
   --
   -- @
-  -- 'hsequence'', 'Generics.SOP.NP.sequence'_NP'  :: ('SingI' xs , 'Applicative' f) => 'Generics.SOP.NP.NP'  (f ':.:' g) xs  -> f ('Generics.SOP.NP.NP'  g xs )
-  -- 'hsequence'', 'Generics.SOP.NS.sequence'_NS'  :: ('SingI' xs , 'Applicative' f) => 'Generics.SOP.NS.NS'  (f ':.:' g) xs  -> f ('Generics.SOP.NS.NS'  g xs )
-  -- 'hsequence'', 'Generics.SOP.NP.sequence'_POP' :: ('SingI' xss, 'Applicative' f) => 'Generics.SOP.NP.POP' (f ':.:' g) xss -> f ('Generics.SOP.NP.POP' g xss)
-  -- 'hsequence'', 'Generics.SOP.NS.sequence'_SOP' :: ('SingI' xss, 'Applicative' f) => 'Generics.SOP.NS.SOP' (f ':.:' g) xss -> f ('Generics.SOP.NS.SOP' g xss)
+  -- 'hsequence'', 'Generics.SOP.NP.sequence'_NP'  :: ('SListI'  xs , 'Applicative' f) => 'Generics.SOP.NP.NP'  (f ':.:' g) xs  -> f ('Generics.SOP.NP.NP'  g xs )
+  -- 'hsequence'', 'Generics.SOP.NS.sequence'_NS'  :: ('SListI'  xs , 'Applicative' f) => 'Generics.SOP.NS.NS'  (f ':.:' g) xs  -> f ('Generics.SOP.NS.NS'  g xs )
+  -- 'hsequence'', 'Generics.SOP.NP.sequence'_POP' :: ('SListI2' xss, 'Applicative' f) => 'Generics.SOP.NP.POP' (f ':.:' g) xss -> f ('Generics.SOP.NP.POP' g xss)
+  -- 'hsequence'', 'Generics.SOP.NS.sequence'_SOP' :: ('SListI2' xss, 'Applicative' f) => 'Generics.SOP.NS.SOP' (f ':.:' g) xss -> f ('Generics.SOP.NS.SOP' g xss)
   -- @
   --
-  hsequence' :: (SingI xs, Applicative f) => h (f :.: g) xs -> f (h g xs)
+  hsequence' :: (SListIN h xs, Applicative f) => h (f :.: g) xs -> f (h g xs)
 
 -- | Special case of 'hsequence'' where @g = 'I'@.
-hsequence :: (SingI xs, HSequence h) => Applicative f => h f xs -> f (h I xs)
+hsequence :: (SListIN h xs, SListIN (Prod h) xs, HSequence h) => Applicative f => h f xs -> f (h I xs)
 hsequence = hsequence' . hliftA (Comp . fmap I)
 
 -- | Special case of 'hsequence'' where @g = 'K' a@.
-hsequenceK ::  (SingI xs, Applicative f, HSequence h) => h (K (f a)) xs -> f (h (K a) xs)
+hsequenceK ::  (SListIN h xs, SListIN (Prod h) xs, Applicative f, HSequence h) => h (K (f a)) xs -> f (h (K a) xs)
 hsequenceK = hsequence' . hliftA (Comp . fmap K . unK)
diff --git a/src/Generics/SOP/Constraint.hs b/src/Generics/SOP/Constraint.hs
--- a/src/Generics/SOP/Constraint.hs
+++ b/src/Generics/SOP/Constraint.hs
@@ -1,4 +1,8 @@
-{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE PolyKinds, UndecidableInstances #-}
+#if __GLASGOW_HASKELL__ < 710
+{-# LANGUAGE OverlappingInstances #-}
+#endif
+{-# OPTIONS_GHC -fno-warn-orphans -fno-warn-deprecations #-}
 -- | Constraints for indexed datatypes.
 --
 -- This module contains code that helps to specify that all
@@ -34,10 +38,18 @@
 -- means that 'f' can assume that all elements of the n-ary
 -- product satisfy 'Eq'.
 --
-type family All (c :: k -> Constraint) (xs :: [k]) :: Constraint
-type instance All c '[]       = ()
-type instance All c (x ': xs) = (c x, All c xs)
+class (AllF f xs, SListI xs) => All (f :: k -> Constraint) (xs :: [k])
+instance (AllF f xs, SListI xs) => All f xs
 
+-- | Type family used to implement 'All'.
+--
+type family AllF (c :: k -> Constraint) (xs :: [k]) :: Constraint
+type instance AllF c '[]       = ()
+type instance AllF c (x ': xs) = (c x, All c xs)
+
+-- | Require a singleton for every inner list in a list of lists.
+type SListI2 = All SListI
+
 -- | Require a constraint for every element of a list of lists.
 --
 -- If you have a datatype that is indexed over a type-level
@@ -59,25 +71,69 @@
 -- means that 'f' can assume that all elements of the sum
 -- of product satisfy 'Eq'.
 --
-type family All2 (c :: k -> Constraint) (xs :: [[k]]) :: Constraint
-type instance All2 c '[]       = ()
-type instance All2 c (x ': xs) = (All c x, All2 c xs)
+class (AllF (All f) xss, SListI xss) => All2 f xss
+instance (AllF (All f) xss, SListI xss) => All2 f xss
+--
+-- NOTE:
+--
+-- The definition
+--
+-- type All2 f = All (All f)
+--
+-- is more direct, but has the unfortunate disadvantage the
+-- it triggers GHC's superclass cycle check when used in a
+-- class context.
 
--- | A type-level 'map'.
-type family Map (f :: k -> l) (xs :: [k]) :: [l]
-type instance Map f '[]       = '[]
-type instance Map f (x ': xs) = f x ': Map f xs
+-- | Composition of constraints.
+--
+-- Note that the result of the composition must be a constraint,
+-- and therefore, in @f ':.' g@, the kind of @f@ is @k -> 'Constraint'@.
+-- The kind of @g@, however, is @l -> k@ and can thus be an normal
+-- type constructor.
+--
+-- A typical use case is in connection with 'All' on an 'NP' or an
+-- 'NS'. For example, in order to denote that all elements on an
+-- @'NP' f xs@ satisfy 'Show', we can say @'All' ('Show' :. f) xs@.
+--
+class (f (g x)) => (f `Compose` g) x
+instance (f (g x)) => (f `Compose` g) x
+infixr 9 `Compose`
 
+-- | Pairing of constraints.
+--
+class (f x, g x) => (f `And` g) x
+instance (f x, g x) => (f `And` g) x
+infixl 7 `And`
+
+-- | A constraint that can always be satisfied.
+--
+class Top x
+instance Top x
+
 -- | A generalization of 'All' and 'All2'.
 --
--- The family 'AllMap' expands to 'All' or 'All2' depending on whether
+-- The family 'AllN' expands to 'All' or 'All2' depending on whether
 -- the argument is indexed by a list or a list of lists.
 --
-type family AllMap (h :: (k -> *) -> (l -> *)) (c :: k -> Constraint) (xs :: l) :: Constraint
+type family AllN (h :: (k -> *) -> (l -> *)) (c :: k -> Constraint) :: l -> Constraint
 
--- | Dictionary for a constraint for all elements of a type-level list.
+-- | A generalization of 'SListI'.
 --
--- A value of type @'AllDict' c xs@ captures the constraint @'All' c xs@.
+-- The family 'SListIN' expands to 'SListI' or 'SListI2' depending
+-- on whether the argument is indexed by a list or a list of lists.
 --
-data AllDict (c :: k -> Constraint) (xs :: [k]) where
-  AllDictC :: (SingI xs, All c xs) => AllDict c xs
+type family SListIN (h :: (k -> *) -> (l -> *)) :: l -> Constraint
+
+instance
+#if __GLASGOW_HASKELL__ >= 710
+  {-# OVERLAPPABLE #-}
+#endif
+  SListI xs => SingI (xs :: [k]) where
+  sing = sList
+
+instance
+#if __GLASGOW_HASKELL__ >= 710
+  {-# OVERLAPPING #-}
+#endif
+  All SListI xss => SingI (xss :: [[k]]) where
+  sing = sList
diff --git a/src/Generics/SOP/Dict.hs b/src/Generics/SOP/Dict.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/SOP/Dict.hs
@@ -0,0 +1,109 @@
+{-# LANGUAGE PolyKinds #-}
+-- | Explicit dictionaries.
+--
+-- When working with compound constraints such as constructed
+-- using 'All' or 'All2', GHC cannot always prove automatically
+-- what one would expect to hold.
+--
+-- This module provides a way of explicitly proving
+-- conversions between such constraints to GHC. Such conversions
+-- still have to be manually applied.
+--
+-- This module is new and experimental in generics-sop 0.2.
+-- It is therefore not yet exported via the main module and
+-- has to be imported explicitly. Its interface is to be
+-- considered even less stable than that of the rest of the
+-- library. Feedback is very welcome though.
+--
+module Generics.SOP.Dict where
+
+import Data.Proxy
+import Generics.SOP.Classes
+import Generics.SOP.Constraint
+import Generics.SOP.NP
+import Generics.SOP.Sing
+
+-- | An explicit dictionary carrying evidence of a
+-- class constraint.
+--
+-- The constraint parameter is separated into a
+-- second argument so that @'Dict' c@ is of the correct
+-- kind to be used directly as a parameter to e.g. 'NP'.
+--
+data Dict (c :: k -> Constraint) (a :: k) where
+  Dict :: c a => Dict c a
+
+-- | A proof that the trivial constraint holds
+-- over all type-level lists.
+pureAll :: SListI xs => Dict (All Top) xs
+pureAll = all_NP (hpure Dict)
+
+-- | A proof that the trivial constraint holds
+-- over all type-level lists of lists.
+pureAll2 :: All SListI xss => Dict (All2 Top) xss
+pureAll2 = all_POP (hpure Dict)
+
+-- | Lifts a dictionary conversion over a type-level list.
+mapAll :: forall c d xs .
+          (forall a . Dict c a -> Dict d a)
+       -> Dict (All c) xs -> Dict (All d) xs
+mapAll f Dict = (all_NP . hmap f . unAll_NP) Dict
+
+-- | Lifts a dictionary conversion over a type-level list
+-- of lists.
+mapAll2 :: forall c d xss .
+           (forall a . Dict c a -> Dict d a)
+        -> Dict (All2 c) xss -> Dict (All2 d) xss
+mapAll2 f d @ Dict = (all2 . mapAll (mapAll f) . unAll2) d
+
+-- | If two constraints 'c' and 'd' hold over a type-level
+-- list 'xs', then the combination of both constraints holds
+-- over that list.
+zipAll :: Dict (All c) xs -> Dict (All d) xs -> Dict (All (c `And` d)) xs
+zipAll dc @ Dict dd = all_NP (hzipWith (\ Dict Dict -> Dict) (unAll_NP dc) (unAll_NP dd))
+
+-- | If two constraints 'c' and 'd' hold over a type-level
+-- list of lists 'xss', then the combination of both constraints
+-- holds over that list of lists.
+zipAll2 :: All SListI xss => Dict (All2 c) xss -> Dict (All2 d) xss -> Dict (All2 (c `And` d)) xss
+zipAll2 dc dd = all_POP (hzipWith (\ Dict Dict -> Dict) (unAll_POP dc) (unAll_POP dd))
+-- TODO: I currently don't understand why the All constraint in the beginning
+-- cannot be inferred.
+
+-- | If we have a constraint 'c' that holds over a type-level
+-- list 'xs', we can create a product containing proofs that
+-- each individual list element satisfies 'c'.
+unAll_NP :: forall c xs . Dict (All c) xs -> NP (Dict c) xs
+unAll_NP Dict = hcpure (Proxy :: Proxy c) Dict
+
+-- | If we have a constraint 'c' that holds over a type-level
+-- list of lists 'xss', we can create a product of products
+-- containing proofs that all the inner elements satisfy 'c'.
+unAll_POP :: forall c xss . Dict (All2 c) xss -> POP (Dict c) xss
+unAll_POP Dict = hcpure (Proxy :: Proxy c) Dict
+
+-- | If we have a product containing proofs that each element
+-- of 'xs' satisfies 'c', then 'All c' holds for 'xs'.
+all_NP :: NP (Dict c) xs -> Dict (All c) xs
+all_NP Nil          = Dict
+all_NP (Dict :* ds) = withDict (all_NP ds) Dict
+
+-- | If we have a product of products containing proofs that
+-- each inner element of 'xss' satisfies 'c', then 'All2 c'
+-- holds for 'xss'.
+all_POP :: SListI xss => POP (Dict c) xss -> Dict (All2 c) xss
+all_POP = all2 . all_NP . hmap all_NP . unPOP
+-- TODO: Is the constraint necessary?
+
+-- | The constraint 'All2 c' is convertible to 'All (All c)'.
+unAll2 :: Dict (All2 c) xss -> Dict (All (All c)) xss
+unAll2 Dict = Dict
+
+-- | The constraint 'All (All c)' is convertible to 'All2 c'.
+all2 :: Dict (All (All c)) xss -> Dict (All2 c) xss
+all2 Dict = Dict
+
+-- | If we have an explicit dictionary, we can unwrap it and
+-- pass a function that makes use of it.
+withDict :: Dict c a -> (c a => r) -> r
+withDict Dict x = x
diff --git a/src/Generics/SOP/GGP.hs b/src/Generics/SOP/GGP.hs
--- a/src/Generics/SOP/GGP.hs
+++ b/src/Generics/SOP/GGP.hs
@@ -22,6 +22,7 @@
 import Generics.SOP.NP as SOP
 import Generics.SOP.NS as SOP
 import Generics.SOP.BasicFunctors as SOP
+import Generics.SOP.Constraint as SOP
 import Generics.SOP.Metadata as SOP
 import Generics.SOP.Sing
 
@@ -42,7 +43,7 @@
 data InfoProxy (c :: *) (f :: * -> *) (x :: *) = InfoProxy
 
 class GDatatypeInfo' (a :: * -> *) where
-  gDatatypeInfo' :: Proxy a -> DatatypeInfo (ToSumCode a '[])
+  gDatatypeInfo' :: proxy a -> DatatypeInfo (ToSumCode a '[])
 
 #if !(MIN_VERSION_base(4,7,0))
 
@@ -55,12 +56,12 @@
 
 #endif
 
-instance (SingI (ToSumCode a '[]), Datatype c, GConstructorInfos a) => GDatatypeInfo' (M1 D c a) where
+instance (All SListI (ToSumCode a '[]), Datatype c, GConstructorInfos a) => GDatatypeInfo' (M1 D c a) where
   gDatatypeInfo' _ =
     let adt = ADT     (moduleName p) (datatypeName p)
         ci  = gConstructorInfos (Proxy :: Proxy a) Nil
     in if isNewtype p
-       then case isNewtypeShape sing ci of
+       then case isNewtypeShape ci of
               NewYes c -> Newtype (moduleName p) (datatypeName p) c
               NewNo    -> adt ci -- should not happen
        else adt ci
@@ -72,16 +73,16 @@
   NewYes :: ConstructorInfo '[x] -> IsNewtypeShape '[ '[x] ]
   NewNo  :: IsNewtypeShape xss
 
-isNewtypeShape :: Sing xss -> NP ConstructorInfo xss -> IsNewtypeShape xss
-isNewtypeShape SCons (x :* Nil) = go shape x
+isNewtypeShape :: All SListI xss => NP ConstructorInfo xss -> IsNewtypeShape xss
+isNewtypeShape (x :* Nil) = go shape x
   where
     go :: Shape xs -> ConstructorInfo xs -> IsNewtypeShape '[ xs ]
     go (ShapeCons ShapeNil) c   = NewYes c
     go _                    _   = NewNo
-isNewtypeShape _     _          = NewNo
+isNewtypeShape _          = NewNo
 
 class GConstructorInfos (a :: * -> *) where
-  gConstructorInfos :: Proxy a -> NP ConstructorInfo xss -> NP ConstructorInfo (ToSumCode a xss)
+  gConstructorInfos :: proxy a -> NP ConstructorInfo xss -> NP ConstructorInfo (ToSumCode a xss)
 
 instance (GConstructorInfos a, GConstructorInfos b) => GConstructorInfos (a :+: b) where
   gConstructorInfos _ xss = gConstructorInfos (Proxy :: Proxy a) (gConstructorInfos (Proxy :: Proxy b) xss)
@@ -89,7 +90,7 @@
 instance GConstructorInfos GHC.V1 where
   gConstructorInfos _ xss = xss
 
-instance (Constructor c, GFieldInfos a, SingI (ToProductCode a '[])) => GConstructorInfos (M1 C c a) where
+instance (Constructor c, GFieldInfos a, SListI (ToProductCode a '[])) => GConstructorInfos (M1 C c a) where
   gConstructorInfos _ xss
     | conIsRecord p = Record (conName p) (gFieldInfos (Proxy :: Proxy a) Nil) :* xss
     | otherwise     = case conFixity p of
@@ -102,7 +103,7 @@
       p = InfoProxy
 
 class GFieldInfos (a :: * -> *) where
-  gFieldInfos :: Proxy a -> NP FieldInfo xs -> NP FieldInfo (ToProductCode a xs)
+  gFieldInfos :: proxy a -> NP FieldInfo xs -> NP FieldInfo (ToProductCode a xs)
 
 instance (GFieldInfos a, GFieldInfos b) => GFieldInfos (a :*: b) where
   gFieldInfos _ xs = gFieldInfos (Proxy :: Proxy a) (gFieldInfos (Proxy :: Proxy b) xs)
@@ -156,7 +157,7 @@
 -- This can most certainly be simplified
 class GSumFrom (a :: * -> *) where
   gSumFrom :: a x -> SOP I xss -> SOP I (ToSumCode a xss)
-  gSumSkip :: Proxy a -> SOP I xss -> SOP I (ToSumCode a xss)
+  gSumSkip :: proxy a -> SOP I xss -> SOP I (ToSumCode a xss)
 
 instance (GSumFrom a, GSumFrom b) => GSumFrom (a :+: b) where
   gSumFrom (L1 a) xss = gSumFrom a (gSumSkip (Proxy :: Proxy b) xss)
@@ -234,6 +235,6 @@
 -- This is the default definition for 'Generics.SOP.datatypeInfo'.
 -- For more info, see 'Generics.SOP.HasDatatypeInfo'.
 --
-gdatatypeInfo :: forall a. (GDatatypeInfo a) => Proxy a -> DatatypeInfo (GCode a)
+gdatatypeInfo :: forall proxy a. (GDatatypeInfo a) => proxy a -> DatatypeInfo (GCode a)
 gdatatypeInfo _ = gDatatypeInfo' (Proxy :: Proxy (GHC.Rep a))
 
diff --git a/src/Generics/SOP/Metadata.hs b/src/Generics/SOP/Metadata.hs
--- a/src/Generics/SOP/Metadata.hs
+++ b/src/Generics/SOP/Metadata.hs
@@ -39,9 +39,9 @@
   -- Newtype
   Newtype :: ModuleName -> DatatypeName -> ConstructorInfo '[x]   -> DatatypeInfo '[ '[x] ]
 
-deriving instance All Show (Map ConstructorInfo xs) => Show (DatatypeInfo xs)
-deriving instance All Eq   (Map ConstructorInfo xs) => Eq   (DatatypeInfo xs)
-deriving instance (All Eq (Map ConstructorInfo xs), All Ord (Map ConstructorInfo xs)) => Ord (DatatypeInfo xs)
+deriving instance All (Show `Compose` ConstructorInfo) xs => Show (DatatypeInfo xs)
+deriving instance All (Eq   `Compose` ConstructorInfo) xs => Eq   (DatatypeInfo xs)
+deriving instance (All (Eq `Compose` ConstructorInfo) xs, All (Ord `Compose` ConstructorInfo) xs) => Ord (DatatypeInfo xs)
 
 -- | Metadata for a single constructors.
 --
@@ -49,15 +49,15 @@
 --
 data ConstructorInfo :: [*] -> * where
   -- Normal constructor
-  Constructor :: SingI xs => ConstructorName -> ConstructorInfo xs
+  Constructor :: SListI xs => ConstructorName -> ConstructorInfo xs
   -- Infix constructor
   Infix :: ConstructorName -> Associativity -> Fixity -> ConstructorInfo '[ x, y ]
   -- Record constructor
-  Record :: SingI xs => ConstructorName -> NP FieldInfo xs -> ConstructorInfo xs
+  Record :: SListI xs => ConstructorName -> NP FieldInfo xs -> ConstructorInfo xs
 
-deriving instance All Show (Map FieldInfo xs) => Show (ConstructorInfo xs)
-deriving instance All Eq   (Map FieldInfo xs) => Eq   (ConstructorInfo xs)
-deriving instance (All Eq (Map FieldInfo xs), All Ord (Map FieldInfo xs)) => Ord (ConstructorInfo xs)
+deriving instance All (Show `Compose` FieldInfo) xs => Show (ConstructorInfo xs)
+deriving instance All (Eq   `Compose` FieldInfo) xs => Eq   (ConstructorInfo xs)
+deriving instance (All (Eq `Compose` FieldInfo) xs, All (Ord `Compose` FieldInfo) xs) => Ord (ConstructorInfo xs)
 
 -- | For records, this functor maps the component to its selector name.
 data FieldInfo :: * -> * where
diff --git a/src/Generics/SOP/NP.hs b/src/Generics/SOP/NP.hs
--- a/src/Generics/SOP/NP.hs
+++ b/src/Generics/SOP/NP.hs
@@ -22,12 +22,25 @@
   , liftA2_POP
   , liftA3_NP
   , liftA3_POP
+  , map_NP
+  , map_POP
+  , zipWith_NP
+  , zipWith_POP
+  , zipWith3_NP
+  , zipWith3_POP
   , cliftA_NP
   , cliftA_POP
   , cliftA2_NP
   , cliftA2_POP
+  , cliftA3_NP
+  , cliftA3_POP
+  , cmap_NP
+  , cmap_POP
+  , czipWith_NP
+  , czipWith_POP
+  , czipWith3_NP
+  , czipWith3_POP
     -- * Dealing with @'All' c@
-  , allDict_NP
   , hcliftA'
   , hcliftA2'
   , hcliftA3'
@@ -42,7 +55,9 @@
   , sequence_POP
   ) where
 
+#if !(MIN_VERSION_base(4,8,0))
 import Control.Applicative
+#endif
 import Data.Proxy (Proxy(..))
 
 import Generics.SOP.BasicFunctors
@@ -84,9 +99,9 @@
 
 infixr 5 :*
 
-deriving instance All Show (Map f xs) => Show (NP f xs)
-deriving instance All Eq   (Map f xs) => Eq   (NP f xs)
-deriving instance (All Eq (Map f xs), All Ord (Map f xs)) => Ord (NP f xs)
+deriving instance All (Show `Compose` f) xs => Show (NP f xs)
+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)
 
 -- | A product of products.
 --
@@ -103,15 +118,21 @@
 -- of a datatype.
 --
 newtype POP (f :: (k -> *)) (xss :: [[k]]) = POP (NP (NP f) xss)
-  deriving (Show, Eq, Ord)
 
+deriving instance (Show (NP (NP f) xss)) => Show (POP f xss)
+deriving instance (Eq   (NP (NP f) xss)) => Eq   (POP f xss)
+deriving instance (Ord  (NP (NP f) xss)) => Ord  (POP f xss)
+
 -- | Unwrap a product of products.
 unPOP :: POP f xss -> NP (NP f) xss
 unPOP (POP xss) = xss
 
-type instance AllMap NP  c xs = All  c xs
-type instance AllMap POP c xs = All2 c xs
+type instance AllN NP  c = All  c
+type instance AllN POP c = All2 c
 
+type instance SListIN NP  = SListI
+type instance SListIN POP = SListI2
+
 -- * Constructing products
 
 -- | Specialization of 'hpure'.
@@ -126,8 +147,8 @@
 -- >>> pure_NP (K 0) :: NP (K Int) '[Double, Int, String]
 -- K 0 :* K 0 :* K 0 :* Nil
 --
-pure_NP :: forall f xs. SingI xs => (forall a. f a) -> NP f xs
-pure_NP f = case sing :: Sing xs of
+pure_NP :: forall f xs. SListI xs => (forall a. f a) -> NP f xs
+pure_NP f = case sList :: SList xs of
   SNil   -> Nil
   SCons  -> f :* pure_NP f
 
@@ -136,19 +157,20 @@
 -- The call @'pure_POP' x@ generates a product of products that contains 'x'
 -- in every element position.
 --
-pure_POP :: forall f xss. SingI xss => (forall a. f a) -> POP f xss
-pure_POP f = case sing :: Sing xss of
-  SNil   -> POP Nil
-  SCons  -> POP (pure_NP f :* unPOP (pure_POP f))
+pure_POP :: All SListI xss => (forall a. f a) -> POP f xss
+pure_POP f = POP (cpure_NP sListP (pure_NP f))
 
+sListP :: Proxy SListI
+sListP = Proxy
+
 -- | Specialization of 'hcpure'.
 --
 -- The call @'cpure_NP' p x@ generates a product that contains 'x' in every
 -- element position.
 --
-cpure_NP :: forall c xs f. (All c xs, SingI xs)
-         => Proxy c -> (forall a. c a => f a) -> NP f xs
-cpure_NP p f = case sing :: Sing xs of
+cpure_NP :: forall c xs proxy f. All c xs
+         => proxy c -> (forall a. c a => f a) -> NP f xs
+cpure_NP p f = case sList :: SList xs of
   SNil   -> Nil
   SCons  -> f :* cpure_NP p f
 
@@ -157,12 +179,13 @@
 -- The call @'cpure_NP' p x@ generates a product of products that contains 'x'
 -- in every element position.
 --
-cpure_POP :: forall c f xss. (All2 c xss, SingI xss)
-          => Proxy c -> (forall a. c a => f a) -> POP f xss
-cpure_POP p f = case sing :: Sing xss of
-  SNil   -> POP Nil
-  SCons  -> POP (cpure_NP p f :* unPOP (cpure_POP p f))
+cpure_POP :: forall c xss proxy f. All2 c xss
+          => proxy c -> (forall a. c a => f a) -> POP f xss
+cpure_POP p f = POP (cpure_NP (allP p) (cpure_NP p f))
 
+allP :: proxy c -> Proxy (All c)
+allP _ = Proxy
+
 instance HPure NP where
   hpure  = pure_NP
   hcpure = cpure_NP
@@ -178,12 +201,12 @@
 -- Returns 'Nothing' if the length of the list does not exactly match the
 -- expected size of the product.
 --
-fromList :: (SingI xs) => [a] -> Maybe (NP (K a) xs)
-fromList = go sing
+fromList :: SListI xs => [a] -> Maybe (NP (K a) xs)
+fromList = go sList
   where
-    go :: Sing xs -> [a] -> Maybe (NP (K a) xs)
+    go :: SList xs -> [a] -> Maybe (NP (K a) xs)
     go SNil  []     = return Nil
-    go SCons (x:xs) = do ys <- go sing xs ; return (K x :* ys)
+    go SCons (x:xs) = do ys <- go sList xs ; return (K x :* ys)
     go _     _      = Nothing
 
 -- * Application
@@ -203,11 +226,20 @@
 -- Applies a product of (lifted) functions pointwise to a product of
 -- suitable arguments.
 --
-ap_POP  :: POP (f -.-> g) xs -> POP  f xs -> POP  g xs
-ap_POP (POP Nil        ) (POP Nil        ) = POP Nil
-ap_POP (POP (fs :* fss)) (POP (xs :* xss)) = POP (ap_NP fs xs :* unPOP (ap_POP (POP fss) (POP xss)))
-ap_POP _ _ = error "inaccessible"
+ap_POP :: POP (f -.-> g) xss -> POP f xss -> POP g xss
+ap_POP (POP fss') (POP xss') = POP (go fss' xss')
+  where
+    go :: NP (NP (f -.-> g)) xss -> NP (NP f) xss -> NP (NP g) xss
+    go Nil         Nil         = Nil
+    go (fs :* fss) (xs :* xss) = ap_NP fs xs :* go fss xss
+    go _           _           = error "inaccessible"
 
+-- The definition of 'ap_POP' is a more direct variant of
+-- '_ap_POP_spec'. The direct definition has the advantage
+-- that it avoids the 'SListI' constraint.
+_ap_POP_spec :: SListI xss => POP (f -.-> g) xss -> POP  f xss -> POP  g xss
+_ap_POP_spec (POP fs) (POP xs) = POP (liftA2_NP ap_NP fs xs)
+
 type instance Prod NP  = NP
 type instance Prod POP = POP
 
@@ -217,58 +249,103 @@
 -- * Lifting / mapping
 
 -- | Specialization of 'hliftA'.
-liftA_NP  :: SingI xs  => (forall a. f a -> g a) -> NP  f xs  -> NP  g xs
+liftA_NP  :: SListI     xs  => (forall a. f a -> g a) -> NP  f xs  -> NP  g xs
 -- | Specialization of 'hliftA'.
-liftA_POP :: SingI xss => (forall a. f a -> g a) -> POP f xss -> POP g xss
+liftA_POP :: All SListI xss => (forall a. f a -> g a) -> POP f xss -> POP g xss
 
 liftA_NP  = hliftA
 liftA_POP = hliftA
 
 -- | Specialization of 'hliftA2'.
-liftA2_NP  :: SingI xs  => (forall a. f a -> g a -> h a) -> NP  f xs  -> NP  g xs  -> NP   h xs
+liftA2_NP  :: SListI     xs  => (forall a. f a -> g a -> h a) -> NP  f xs  -> NP  g xs  -> NP   h xs
 -- | Specialization of 'hliftA2'.
-liftA2_POP :: SingI xss => (forall a. f a -> g a -> h a) -> POP f xss -> POP g xss -> POP  h xss
+liftA2_POP :: All SListI xss => (forall a. f a -> g a -> h a) -> POP f xss -> POP g xss -> POP  h xss
 
 liftA2_NP  = hliftA2
 liftA2_POP = hliftA2
 
 -- | Specialization of 'hliftA3'.
-liftA3_NP  :: SingI xs  => (forall a. f a -> g a -> h a -> i a) -> NP  f xs  -> NP  g xs  -> NP  h xs  -> NP  i xs
+liftA3_NP  :: SListI     xs  => (forall a. f a -> g a -> h a -> i a) -> NP  f xs  -> NP  g xs  -> NP  h xs  -> NP  i xs
 -- | Specialization of 'hliftA3'.
-liftA3_POP :: SingI xss => (forall a. f a -> g a -> h a -> i a) -> POP f xss -> POP g xss -> POP h xss -> POP i xss
+liftA3_POP :: All SListI xss => (forall a. f a -> g a -> h a -> i a) -> POP f xss -> POP g xss -> POP h xss -> POP i xss
 
 liftA3_NP  = hliftA3
 liftA3_POP = hliftA3
 
+-- | Specialization of 'hmap', which is equivalent to 'hliftA'.
+map_NP  :: SListI     xs  => (forall a. f a -> g a) -> NP  f xs  -> NP  g xs
+-- | Specialization of 'hmap', which is equivalent to 'hliftA'.
+map_POP :: All SListI xss => (forall a. f a -> g a) -> POP f xss -> POP g xss
+
+map_NP  = hmap
+map_POP = hmap
+
+-- | Specialization of 'hzipWith', which is equivalent to 'hliftA2'.
+zipWith_NP  :: SListI     xs  => (forall a. f a -> g a -> h a) -> NP  f xs  -> NP  g xs  -> NP   h xs
+-- | Specialization of 'hzipWith', which is equivalent to 'hliftA2'.
+zipWith_POP :: All SListI xss => (forall a. f a -> g a -> h a) -> POP f xss -> POP g xss -> POP  h xss
+
+zipWith_NP  = hzipWith
+zipWith_POP = hzipWith
+
+-- | Specialization of 'hzipWith3', which is equivalent to 'hliftA3'.
+zipWith3_NP  :: SListI     xs  => (forall a. f a -> g a -> h a -> i a) -> NP  f xs  -> NP  g xs  -> NP  h xs  -> NP  i xs
+-- | Specialization of 'hzipWith3', which is equivalent to 'hliftA3'.
+zipWith3_POP :: All SListI xss => (forall a. f a -> g a -> h a -> i a) -> POP f xss -> POP g xss -> POP h xss -> POP i xss
+
+zipWith3_NP  = hzipWith3
+zipWith3_POP = hzipWith3
+
 -- | Specialization of 'hcliftA'.
-cliftA_NP  :: (All  c xs,  SingI xs)  => Proxy c -> (forall a. c a => f a -> g a) -> NP   f xs  -> NP  g xs
+cliftA_NP  :: All  c xs  => proxy c -> (forall a. c a => f a -> g a) -> NP   f xs  -> NP  g xs
 -- | Specialization of 'hcliftA'.
-cliftA_POP :: (All2 c xss, SingI xss) => Proxy c -> (forall a. c a => f a -> g a) -> POP  f xss -> POP g xss
+cliftA_POP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a) -> POP  f xss -> POP g xss
 
 cliftA_NP  = hcliftA
 cliftA_POP = hcliftA
 
 -- | Specialization of 'hcliftA2'.
-cliftA2_NP  :: (All  c xs,  SingI xs)  => Proxy c -> (forall a. c a => f a -> g a -> h a) -> NP  f xs  -> NP  g xs  -> NP  h xs
+cliftA2_NP  :: All  c xs  => proxy c -> (forall a. c a => f a -> g a -> h a) -> NP  f xs  -> NP  g xs  -> NP  h xs
 -- | Specialization of 'hcliftA2'.
-cliftA2_POP :: (All2 c xss, SingI xss) => Proxy c -> (forall a. c a => f a -> g a -> h a) -> POP f xss -> POP g xss -> POP h xss
+cliftA2_POP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a -> h a) -> POP f xss -> POP g xss -> POP h xss
 
 cliftA2_NP  = hcliftA2
 cliftA2_POP = hcliftA2
 
--- * Dealing with @'All' c@
+-- | Specialization of 'hcliftA3'.
+cliftA3_NP  :: All  c xs  => proxy c -> (forall a. c a => f a -> g a -> h a -> i a) -> NP  f xs  -> NP  g xs  -> NP  h xs  -> NP  i xs
+-- | Specialization of 'hcliftA3'.
+cliftA3_POP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a -> h a -> i a) -> POP f xss -> POP g xss -> POP h xss -> POP i xss
 
--- | Construct a product of dictionaries for a type-level list of lists.
---
--- The structure of the product matches the outer list, the dictionaries
--- contained are 'AllDict'-dictionaries for the inner list.
---
-allDict_NP :: forall (c :: k -> Constraint) (xss :: [[k]]). (All2 c xss, SingI xss)
-           => Proxy c -> NP (AllDict c) xss
-allDict_NP p = case sing :: Sing xss of
-  SNil  -> Nil
-  SCons -> AllDictC :* allDict_NP p
+cliftA3_NP  = hcliftA3
+cliftA3_POP = hcliftA3
 
+-- | Specialization of 'hcmap', which is equivalent to 'hcliftA'.
+cmap_NP  :: All  c xs  => proxy c -> (forall a. c a => f a -> g a) -> NP   f xs  -> NP  g xs
+-- | Specialization of 'hcmap', which is equivalent to 'hcliftA'.
+cmap_POP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a) -> POP  f xss -> POP g xss
+
+cmap_NP  = hcmap
+cmap_POP = hcmap
+
+-- | Specialization of 'hczipWith', which is equivalent to 'hcliftA2'.
+czipWith_NP  :: All  c xs  => proxy c -> (forall a. c a => f a -> g a -> h a) -> NP  f xs  -> NP  g xs  -> NP  h xs
+-- | Specialization of 'hczipWith', which is equivalent to 'hcliftA2'.
+czipWith_POP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a -> h a) -> POP f xss -> POP g xss -> POP h xss
+
+czipWith_NP  = hczipWith
+czipWith_POP = hczipWith
+
+-- | Specialization of 'hczipWith3', which is equivalent to 'hcliftA3'.
+czipWith3_NP  :: All  c xs  => proxy c -> (forall a. c a => f a -> g a -> h a -> i a) -> NP  f xs  -> NP  g xs  -> NP  h xs  -> NP  i xs
+-- | Specialization of 'hczipWith3', which is equivalent to 'hcliftA3'.
+czipWith3_POP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a -> h a -> i a) -> POP f xss -> POP g xss -> POP h xss -> POP i xss
+
+czipWith3_NP  = hczipWith3
+czipWith3_POP = hczipWith3
+
+-- * Dealing with @'All' c@
+
 -- | Lift a constrained function operating on a list-indexed structure
 -- to a function on a list-of-list-indexed structure.
 --
@@ -283,24 +360,28 @@
 -- /Instances:/
 --
 -- @
--- 'hcliftA'' :: ('All2' c xss, 'SingI' xss) => 'Proxy' c -> (forall xs. ('SingI' xs, 'All' c xs) => f xs -> f' xs) -> 'NP' f xss -> 'NP' f' xss
--- 'hcliftA'' :: ('All2' c xss, 'SingI' xss) => 'Proxy' c -> (forall xs. ('SingI' xs, 'All' c xs) => f xs -> f' xs) -> 'Generics.SOP.NS.NS' f xss -> 'Generics.SOP.NS.NS' f' xss
+-- 'hcliftA'' :: 'All2' c xss => proxy c -> (forall xs. 'All' c xs => f xs -> f' xs) -> 'NP' f xss -> 'NP' f' xss
+-- 'hcliftA'' :: 'All2' c xss => proxy c -> (forall xs. 'All' c xs => f xs -> f' xs) -> 'Generics.SOP.NS.NS' f xss -> 'Generics.SOP.NS.NS' f' xss
 -- @
 --
-hcliftA'  :: (All2 c xss, SingI xss, Prod h ~ NP, HAp h) => Proxy c -> (forall xs. (SingI xs, All c xs) => f xs -> f' xs)                                                       -> h f   xss -> h f'   xss
+{-# DEPRECATED hcliftA' "Use 'hclift' or 'hcmap' instead." #-}
+hcliftA'  :: (All2 c xss, Prod h ~ NP, HAp h) => proxy c -> (forall xs. All c xs => f xs -> f' xs)                                                       -> h f   xss -> h f'   xss
 
 -- | Like 'hcliftA'', but for binary functions.
-hcliftA2' :: (All2 c xss, SingI xss, Prod h ~ NP, HAp h) => Proxy c -> (forall xs. (SingI xs, All c xs) => f xs -> f' xs -> f'' xs)            -> Prod h f xss                  -> h f'  xss -> h f''  xss
+{-# DEPRECATED hcliftA2' "Use 'hcliftA2' or 'hczipWith' instead." #-}
+hcliftA2' :: (All2 c xss, Prod h ~ NP, HAp h) => proxy c -> (forall xs. All c xs => f xs -> f' xs -> f'' xs)            -> Prod h f xss                  -> h f'  xss -> h f''  xss
 
 -- | Like 'hcliftA'', but for ternay functions.
-hcliftA3' :: (All2 c xss, SingI xss, Prod h ~ NP, HAp h) => Proxy c -> (forall xs. (SingI xs, All c xs) => f xs -> f' xs -> f'' xs -> f''' xs) -> Prod h f xss -> Prod h f' xss -> h f'' xss -> h f''' xss
+{-# DEPRECATED hcliftA3' "Use 'hcliftA3' or 'hczipWith3' instead." #-}
+hcliftA3' :: (All2 c xss, Prod h ~ NP, HAp h) => proxy c -> (forall xs. All c xs => f xs -> f' xs -> f'' xs -> f''' xs) -> Prod h f xss -> Prod h f' xss -> h f'' xss -> h f''' xss
 
-hcliftA'  p f xs       = hpure (fn_2 $ \AllDictC -> f) `hap` allDict_NP p `hap` xs
-hcliftA2' p f xs ys    = hpure (fn_3 $ \AllDictC -> f) `hap` allDict_NP p `hap` xs `hap` ys
-hcliftA3' p f xs ys zs = hpure (fn_4 $ \AllDictC -> f) `hap` allDict_NP p `hap` xs `hap` ys `hap` zs
+hcliftA'  p = hcliftA  (allP p)
+hcliftA2' p = hcliftA2 (allP p)
+hcliftA3' p = hcliftA3 (allP p)
 
 -- | Specialization of 'hcliftA2''.
-cliftA2'_NP :: (All2 c xss, SingI xss) => Proxy c -> (forall xs. (SingI xs, All c xs) => f xs -> g xs -> h xs) -> NP f xss -> NP g xss -> NP h xss
+{-# DEPRECATED cliftA2'_NP "Use 'cliftA2_NP'  instead." #-}
+cliftA2'_NP :: All2 c xss => proxy c -> (forall xs. All c xs => f xs -> g xs -> h xs) -> NP f xss -> NP g xss -> NP h xss
 
 cliftA2'_NP = hcliftA2'
 
@@ -324,18 +405,18 @@
 --
 -- (The type signature is only necessary in this case to fix the kind of the type variables.)
 --
-collapse_POP :: SingI xss => POP (K a) xss -> [[a]]
+collapse_POP :: SListI xss => POP (K a) xss -> [[a]]
 
 collapse_NP Nil         = []
 collapse_NP (K x :* xs) = x : collapse_NP xs
 
 collapse_POP = collapse_NP . hliftA (K . collapse_NP) . unPOP
 
-type instance CollapseTo NP  = []
-type instance CollapseTo POP = ([] :.: [])
+type instance CollapseTo NP  a = [a]
+type instance CollapseTo POP a = [[a]]
 
 instance HCollapse NP  where hcollapse = collapse_NP
-instance HCollapse POP where hcollapse = Comp . collapse_POP
+instance HCollapse POP where hcollapse = collapse_POP
 
 -- * Sequencing
 
@@ -343,7 +424,7 @@
 sequence'_NP  ::             Applicative f  => NP  (f :.: g) xs  -> f (NP  g xs)
 
 -- | Specialization of 'hsequence''.
-sequence'_POP :: (SingI xss, Applicative f) => POP (f :.: g) xss -> f (POP g xss)
+sequence'_POP :: (SListI xss, Applicative f) => POP (f :.: g) xss -> f (POP g xss)
 
 sequence'_NP Nil         = pure Nil
 sequence'_NP (mx :* mxs) = (:*) <$> unComp mx <*> sequence'_NP mxs
@@ -360,7 +441,7 @@
 -- >>> sequence_NP (Just 1 :* Just 2 :* Nil)
 -- Just (I 1 :* I 2 :* Nil)
 --
-sequence_NP  :: (SingI xs,  Applicative f) => NP  f xs  -> f (NP  I xs)
+sequence_NP  :: (SListI xs,  Applicative f) => NP  f xs  -> f (NP  I xs)
 
 -- | Specialization of 'hsequence'.
 --
@@ -369,7 +450,7 @@
 -- >>> sequence_POP (POP ((Just 1 :* Nil) :* (Just 2 :* Just 3 :* Nil) :* Nil))
 -- Just (POP ((I 1 :* Nil) :* ((I 2 :* (I 3 :* Nil)) :* Nil)))
 --
-sequence_POP :: (SingI xss, Applicative f) => POP f xss -> f (POP I xss)
+sequence_POP :: (All SListI xss, Applicative f) => POP f xss -> f (POP I xss)
 
 sequence_NP   = hsequence
 sequence_POP  = hsequence
diff --git a/src/Generics/SOP/NS.hs b/src/Generics/SOP/NS.hs
--- a/src/Generics/SOP/NS.hs
+++ b/src/Generics/SOP/NS.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE PolyKinds, StandaloneDeriving, UndecidableInstances #-}
+{-# OPTIONS_GHC -fno-warn-deprecations #-}
 -- | n-ary sums (and sums of products)
 module Generics.SOP.NS
   ( -- * Datatypes
@@ -23,6 +24,10 @@
   , cliftA_SOP
   , cliftA2_NS
   , cliftA2_SOP
+  , map_NS
+  , map_SOP
+  , cmap_NS
+  , cmap_SOP
     -- * Dealing with @'All' c@
   , cliftA2'_NS
     -- * Collapsing
@@ -35,8 +40,9 @@
   , sequence_SOP
   ) where
 
+#if !(MIN_VERSION_base(4,8,0))
 import Control.Applicative
-import Data.Proxy (Proxy(..))
+#endif
 
 import Generics.SOP.BasicFunctors
 import Generics.SOP.Classes
@@ -90,9 +96,9 @@
   Z :: f x -> NS f (x ': xs)
   S :: NS f xs -> NS f (x ': xs)
 
-deriving instance All Show (Map f xs) => Show (NS f xs)
-deriving instance All Eq   (Map f xs) => Eq   (NS f xs)
-deriving instance (All Eq (Map f xs), All Ord (Map f xs)) => Ord (NS f xs)
+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)
 
 -- | A sum of products.
 --
@@ -108,8 +114,11 @@
 -- each constructor.
 --
 newtype SOP (f :: (k -> *)) (xss :: [[k]]) = SOP (NS (NP f) xss)
-  deriving (Show, Eq, Ord)
 
+deriving instance (Show (NS (NP f) xss)) => Show (SOP f xss)
+deriving instance (Eq   (NS (NP f) xss)) => Eq   (SOP f xss)
+deriving instance (Ord  (NS (NP f) xss)) => Ord  (SOP f xss) 
+
 -- | Unwrap a sum of products.
 unSOP :: SOP f xss -> NS (NP f) xss
 unSOP (SOP xss) = xss
@@ -131,8 +140,8 @@
 --
 -- Each element of the resulting product contains one of the injections.
 --
-injections :: forall xs f. SingI xs => NP (Injection f xs) xs
-injections = case sing :: Sing xs of
+injections :: forall xs f. SListI xs => NP (Injection f xs) xs
+injections = case sList :: SList xs of
   SNil   -> Nil
   SCons  -> fn (K . Z) :* liftA_NP shift injections
 
@@ -154,7 +163,7 @@
 -- >>> apInjs_NP (I 'x' :* I True :* I 2 :* Nil)
 -- [Z (I 'x'), S (Z (I True)), S (S (Z (I 2)))]
 --
-apInjs_NP  :: SingI xs  => NP  f xs  -> [NS  f xs]
+apInjs_NP  :: SListI xs  => NP  f xs  -> [NS  f xs]
 apInjs_NP  = hcollapse . hap injections
 
 -- | Apply injections to a product of product.
@@ -169,7 +178,7 @@
 -- >>> apInjs_POP (POP ((I 'x' :* Nil) :* (I True :* I 2 :* Nil) :* Nil))
 -- [SOP (Z (I 'x' :* Nil)),SOP (S (Z (I True :* (I 2 :* Nil))))]
 --
-apInjs_POP :: SingI xss => POP f xss -> [SOP f xss]
+apInjs_POP :: SListI xss => POP f xss -> [SOP f xss]
 apInjs_POP = map SOP . apInjs_NP . unPOP
 
 -- * Application
@@ -181,83 +190,112 @@
 ap_NS _ _ = error "inaccessible"
 
 -- | Specialization of 'hap'.
-ap_SOP  :: POP (f -.-> g) xs -> SOP  f xs -> SOP  g xs
-ap_SOP (POP (fs :* _)  ) (SOP (Z xs) ) = SOP (Z (ap_NP  fs  xs))
-ap_SOP (POP (_  :* fss)) (SOP (S xss)) = SOP (S (unSOP (ap_SOP (POP fss) (SOP xss))))
-ap_SOP _ _ = error "inaccessible"
+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 _           _       = error "inaccessible"
 
+-- The definition of 'ap_SOP' is a more direct variant of
+-- '_ap_SOP_spec'. The direct definition has the advantage
+-- that it avoids the 'SListI' constraint.
+_ap_SOP_spec :: SListI xss => POP (t -.-> f) xss -> SOP t xss -> SOP f xss
+_ap_SOP_spec (POP fs) (SOP xs) = SOP (liftA2_NS ap_NP fs xs)
+
 type instance Prod NS  = NP
 type instance Prod SOP = POP
 
+type instance SListIN NS  = SListI
+type instance SListIN SOP = SListI2
+
 instance HAp NS  where hap = ap_NS
 instance HAp SOP where hap = ap_SOP
 
 -- * Lifting / mapping
 
 -- | Specialization of 'hliftA'.
-liftA_NS  :: SingI xs  => (forall a. f a -> g a) -> NS  f xs  -> NS  g xs
+liftA_NS  :: SListI     xs  => (forall a. f a -> g a) -> NS  f xs  -> NS  g xs
 -- | Specialization of 'hliftA'.
-liftA_SOP :: SingI xss => (forall a. f a -> g a) -> SOP f xss -> SOP g xss
+liftA_SOP :: All SListI xss => (forall a. f a -> g a) -> SOP f xss -> SOP g xss
 
 liftA_NS  = hliftA
 liftA_SOP = hliftA
 
 -- | Specialization of 'hliftA2'.
-liftA2_NS  :: SingI xs  => (forall a. f a -> g a -> h a) -> NP  f xs  -> NS  g xs  -> NS   h xs
+liftA2_NS  :: SListI     xs  => (forall a. f a -> g a -> h a) -> NP  f xs  -> NS  g xs  -> NS   h xs
 -- | Specialization of 'hliftA2'.
-liftA2_SOP :: SingI xss => (forall a. f a -> g a -> h a) -> POP f xss -> SOP g xss -> SOP  h xss
+liftA2_SOP :: All SListI xss => (forall a. f a -> g a -> h a) -> POP f xss -> SOP g xss -> SOP  h xss
 
 liftA2_NS  = hliftA2
 liftA2_SOP = hliftA2
 
+-- | Specialization of 'hmap', which is equivalent to 'hliftA'.
+map_NS  :: SListI     xs  => (forall a. f a -> g a) -> NS  f xs  -> NS  g xs
+-- | Specialization of 'hmap', which is equivalent to 'hliftA'.
+map_SOP :: All SListI xss => (forall a. f a -> g a) -> SOP f xss -> SOP g xss
+
+map_NS  = hmap
+map_SOP = hmap
+
 -- | Specialization of 'hcliftA'.
-cliftA_NS  :: (All  c xs,  SingI xs)  => Proxy c -> (forall a. c a => f a -> g a) -> NS   f xs  -> NS  g xs
+cliftA_NS  :: All  c xs  => proxy c -> (forall a. c a => f a -> g a) -> NS   f xs  -> NS  g xs
 -- | Specialization of 'hcliftA'.
-cliftA_SOP :: (All2 c xss, SingI xss) => Proxy c -> (forall a. c a => f a -> g a) -> SOP  f xss -> SOP g xss
+cliftA_SOP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a) -> SOP  f xss -> SOP g xss
 
 cliftA_NS  = hcliftA
 cliftA_SOP = hcliftA
 
 -- | Specialization of 'hcliftA2'.
-cliftA2_NS  :: (All  c xs,  SingI xs)  => Proxy c -> (forall a. c a => f a -> g a -> h a) -> NP  f xs  -> NS  g xs  -> NS  h xs
+cliftA2_NS  :: All  c xs  => proxy c -> (forall a. c a => f a -> g a -> h a) -> NP  f xs  -> NS  g xs  -> NS  h xs
 -- | Specialization of 'hcliftA2'.
-cliftA2_SOP :: (All2 c xss, SingI xss) => Proxy c -> (forall a. c a => f a -> g a -> h a) -> POP f xss -> SOP g xss -> SOP h xss
+cliftA2_SOP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a -> h a) -> POP f xss -> SOP g xss -> SOP h xss
 
 cliftA2_NS  = hcliftA2
 cliftA2_SOP = hcliftA2
 
+-- | Specialization of 'hcmap', which is equivalent to 'hcliftA'.
+cmap_NS  :: All  c xs  => proxy c -> (forall a. c a => f a -> g a) -> NS   f xs  -> NS  g xs
+-- | Specialization of 'hcmap', which is equivalent to 'hcliftA'.
+cmap_SOP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a) -> SOP  f xss -> SOP g xss
+
+cmap_NS  = hcmap
+cmap_SOP = hcmap
+
 -- * Dealing with @'All' c@
 
 -- | Specialization of 'hcliftA2''.
-cliftA2'_NS :: (All2 c xss, SingI xss) => Proxy c -> (forall xs. (SingI xs, All c xs) => f xs -> g xs -> h xs) -> NP f xss -> NS g xss -> NS h xss
+{-# DEPRECATED cliftA2'_NS "Use 'cliftA2_NS' instead." #-}
+cliftA2'_NS :: All2 c xss => proxy c -> (forall xs. All c xs => f xs -> g xs -> h xs) -> NP f xss -> NS g xss -> NS h xss
 
 cliftA2'_NS = hcliftA2'
 
 -- * Collapsing
 
 -- | Specialization of 'hcollapse'.
-collapse_NS  ::              NS  (K a) xs  ->   a
+collapse_NS  ::               NS  (K a) xs  ->   a
 -- | Specialization of 'hcollapse'.
-collapse_SOP :: SingI xss => SOP (K a) xss ->  [a]
+collapse_SOP :: SListI xss => SOP (K a) xss ->  [a]
 
 collapse_NS (Z (K x)) = x
 collapse_NS (S xs)    = collapse_NS xs
 
 collapse_SOP = collapse_NS . hliftA (K . collapse_NP) . unSOP
 
-type instance CollapseTo NS  = I
-type instance CollapseTo SOP = []
+type instance CollapseTo NS  a =  a
+type instance CollapseTo SOP a = [a]
 
-instance HCollapse NS  where hcollapse = I . collapse_NS
+instance HCollapse NS  where hcollapse = collapse_NS
 instance HCollapse SOP where hcollapse = collapse_SOP
 
 -- * Sequencing
 
 -- | Specialization of 'hsequence''.
-sequence'_NS  ::             Applicative f  => NS  (f :.: g) xs  -> f (NS  g xs)
+sequence'_NS  ::              Applicative f  => NS  (f :.: g) xs  -> f (NS  g xs)
 
 -- | Specialization of 'hsequence''.
-sequence'_SOP :: (SingI xss, Applicative f) => SOP (f :.: g) xss -> f (SOP g xss)
+sequence'_SOP :: (SListI xss, Applicative f) => SOP (f :.: g) xss -> f (SOP g xss)
 
 sequence'_NS (Z mx)  = Z <$> unComp mx
 sequence'_NS (S mxs) = S <$> sequence'_NS mxs
@@ -268,10 +306,10 @@
 instance HSequence SOP where hsequence' = sequence'_SOP
 
 -- | Specialization of 'hsequence'.
-sequence_NS  :: (SingI xs,  Applicative f) => NS  f xs  -> f (NS  I xs)
+sequence_NS  :: (SListI xs,  Applicative f) => NS  f xs  -> f (NS  I xs)
 
 -- | Specialization of 'hsequence'.
-sequence_SOP :: (SingI xss, Applicative f) => SOP f xss -> f (SOP I xss)
+sequence_SOP :: (All SListI xss, Applicative f) => SOP f xss -> f (SOP I xss)
 
 sequence_NS   = hsequence
 sequence_SOP  = hsequence
diff --git a/src/Generics/SOP/Sing.hs b/src/Generics/SOP/Sing.hs
--- a/src/Generics/SOP/Sing.hs
+++ b/src/Generics/SOP/Sing.hs
@@ -11,94 +11,100 @@
 --
 module Generics.SOP.Sing
   ( -- * Singletons
-    Sing(..)
+    SList(..)
+  , SListI(..)
+  , Sing
   , SingI(..)
     -- ** Shape of type-level lists
   , Shape(..)
   , shape
+  , lengthSList
   , lengthSing
   ) where
 
-import Data.Proxy (Proxy(..))
-
 -- * Singletons
 
--- | Explicit singleton.
---
--- A singleton can be used to reveal the structure of a type
--- argument that the function is quantified over.
---
--- The family 'Sing' should have at most one instance per kind,
--- and there should be a matching instance for 'SingI'.
+-- | Explicit singleton list.
 --
-data family Sing (a :: k)
-
--- | Singleton for type-level lists.
-data instance Sing (xs :: [k]) where
-  SNil  :: Sing '[]
-  SCons :: (SingI x, SingI xs) => Sing (x ': xs)
-
-deriving instance Show (Sing (xs :: [k]))
-deriving instance Eq   (Sing (xs :: [k]))
-deriving instance Ord  (Sing (xs :: [k]))
-
--- | Singleton for types of kind '*'.
+-- A singleton list can be used to reveal the structure of
+-- a type-level list argument that the function is quantified
+-- over. For every type-level list @xs@, there is one non-bottom
+-- value of type @'SList' xs@.
 --
--- For types of kind '*', we explicitly /don't/ want to reveal
--- more type analysis. Even functions that have a 'Sing' constraint
--- should still be parametric in everything that is of kind '*'.
+-- Note that these singleton lists are polymorphic in the
+-- list elements; we do not require a singleton representation
+-- for them.
 --
-data instance Sing (x :: *) where
-  SStar :: Sing (x :: *)
+data SList :: [k] -> * where
+  SNil  :: SList '[]
+  SCons :: SListI xs => SList (x ': xs)
 
-deriving instance Show (Sing (x :: *))
-deriving instance Eq   (Sing (x :: *))
-deriving instance Ord  (Sing (x :: *))
+deriving instance Show (SList (xs :: [k]))
+deriving instance Eq   (SList (xs :: [k]))
+deriving instance Ord  (SList (xs :: [k]))
 
--- | Implicit singleton.
+-- | Implicit singleton list.
 --
--- A singleton can be used to reveal the structure of a type
--- argument that the function is quantified over.
+-- A singleton list can be used to reveal the structure of
+-- a type-level list argument that the function is quantified
+-- over.
 --
--- The class 'SingI' should have instances that match the
--- family instances for 'Sing'.
+-- The class 'SListI' should have instances that match the
+-- constructors of 'SList'.
 --
-class SingI (a :: k) where
+class SListI (xs :: [k]) where
   -- | Get hold of the explicit singleton (that one can then
   -- pattern match on).
-  sing :: Sing a
+  sList :: SList xs
 
-instance SingI (x :: *) where
-  sing = SStar
+instance SListI '[] where
+  sList = SNil
 
-instance SingI '[] where
-  sing = SNil
+instance SListI xs => SListI (x ': xs) where
+  sList = SCons
 
-instance (SingI x, SingI xs) => SingI (x ': xs) where
-  sing = SCons
+-- | General class for implicit singletons.
+--
+-- Just provided for limited backward compatibility.
+--
+{-# DEPRECATED SingI "Use 'SListI' instead." #-}
+{-# DEPRECATED sing "Use 'sList' instead." #-}
+class SListI xs => SingI (xs :: [k]) where
+  sing :: Sing xs
 
+-- | Explicit singleton type.
+--
+-- Just provided for limited backward compatibility.
+{-# DEPRECATED Sing "Use 'SList' instead." #-}
+type Sing = SList
+
 -- * Shape of type-level lists
 
 -- | Occassionally it is useful to have an explicit, term-level, representation
 -- of type-level lists (esp because of https://ghc.haskell.org/trac/ghc/ticket/9108)
 data Shape :: [k] -> * where
   ShapeNil  :: Shape '[]
-  ShapeCons :: (SingI x, SingI xs) => Shape xs -> Shape (x ': xs)
+  ShapeCons :: SListI xs => Shape xs -> Shape (x ': xs)
 
 deriving instance Show (Shape xs)
 deriving instance Eq   (Shape xs)
 deriving instance Ord  (Shape xs)
 
 -- | The shape of a type-level list.
-shape :: forall (xs :: [k]). SingI xs => Shape xs
-shape = case sing :: Sing xs of
+shape :: forall (xs :: [k]). SListI xs => Shape xs
+shape = case sList :: SList xs of
           SNil  -> ShapeNil
           SCons -> ShapeCons shape
 
 -- | The length of a type-level list.
-lengthSing :: forall (xs :: [k]). SingI xs => Proxy xs -> Int
-lengthSing _ = lengthShape (shape :: Shape xs)
+lengthSList :: forall (xs :: [k]) proxy. SListI xs => proxy xs -> Int
+lengthSList _ = lengthShape (shape :: Shape xs)
   where
     lengthShape :: forall xs'. Shape xs' -> Int
     lengthShape ShapeNil      = 0
     lengthShape (ShapeCons s) = 1 + lengthShape s
+
+-- | Old name for 'lengthSList'.
+{-# DEPRECATED lengthSing "Use 'lengthSList' instead." #-}
+lengthSing :: SListI xs => proxy xs -> Int
+lengthSing = lengthSList
diff --git a/src/Generics/SOP/TH.hs b/src/Generics/SOP/TH.hs
--- a/src/Generics/SOP/TH.hs
+++ b/src/Generics/SOP/TH.hs
@@ -3,6 +3,8 @@
 module Generics.SOP.TH
   ( deriveGeneric
   , deriveGenericOnly
+  , deriveGenericFunctions
+  , deriveMetadataValue
   ) where
 
 import Control.Monad (replicateM)
@@ -67,8 +69,67 @@
 deriveGenericOnly :: Name -> Q [Dec]
 deriveGenericOnly n = do
   dec <- reifyDec n
-  withDataDec dec deriveMetadataForDataDec
+  withDataDec dec deriveGenericForDataDec
 
+-- | Like 'deriveGenericOnly', but don't derive class instance, only functions.
+--
+-- /Example:/ If you say
+--
+-- > deriveGenericFunctions ''Tree "TreeCode" "fromTree" "toTree"
+--
+-- then you get code that is equivalent to:
+--
+-- > type TreeCode = '[ '[Int], '[Tree, Tree] ]
+-- >
+-- > fromTree :: Tree -> SOP I TreeCode
+-- > fromTree (Leaf x)   = SOP (   Z (I x :* Nil))
+-- > fromTree (Node l r) = SOP (S (Z (I l :* I r :* Nil)))
+-- >
+-- > toTree :: SOP I TreeCode -> Tree
+-- > toTree (SOP    (Z (I x :* Nil)))         = Leaf x
+-- > toTree (SOP (S (Z (I l :* I r :* Nil)))) = Node l r
+-- > toTree _ = error "unreachable" -- to avoid GHC warnings
+--
+deriveGenericFunctions :: Name -> String -> String -> String -> Q [Dec]
+deriveGenericFunctions n codeName fromName toName = do
+  let codeName'  = mkName codeName
+  let fromName' = mkName fromName
+  let toName'   = mkName toName
+  dec <- reifyDec n
+  withDataDec dec $ \_isNewtype _cxt name _bndrs cons _derivs -> do
+    let codeType = codeFor cons                        -- '[ '[Int], '[Tree, Tree] ]
+    let repType = [t| SOP I $(conT codeName') |]       -- SOP I TreeCode
+    sequence
+      [ tySynD codeName' [] codeType                    -- type TreeCode = '[ '[Int], '[Tree, Tree] ]
+      , sigD fromName' [t| $(conT name) -> $repType |]  -- fromTree :: Tree -> SOP I TreeCode
+      , embedding fromName' cons                        -- fromTree ... =
+      , sigD toName' [t| $repType -> $(conT name) |]    -- toTree :: SOP I TreeCode -> Tree
+      , projection toName' cons                         -- toTree ... =
+      ]
+
+-- | Derive @DatatypeInfo@ value for the type.
+--
+-- /Example:/ If you say
+--
+-- > deriveMetadataValue ''Tree "TreeCode" "treeDatatypeInfo"
+--
+-- then you get code that is equivalent to:
+--
+-- > treeDatatypeInfo :: DatatypeInfo TreeCode
+-- > treeDatatypeInfo = ADT "Main" "Tree"
+-- >     (Constructor "Leaf" :* Constructor "Node" :* Nil)
+--
+-- /Note:/ CodeType need to be derived with 'deriveGenericFunctions'.
+deriveMetadataValue :: Name -> String -> String -> Q [Dec]
+deriveMetadataValue n codeName datatypeInfoName = do
+  let codeName'  = mkName codeName
+  let datatypeInfoName' = mkName datatypeInfoName
+  dec <- reifyDec n
+  withDataDec dec $ \isNewtype _cxt name _bndrs cons _derivs -> do
+    sequence [ sigD datatypeInfoName' [t| DatatypeInfo $(conT codeName') |]                    -- treeDatatypeInfo :: DatatypeInfo TreeCode
+             , funD datatypeInfoName' [clause [] (normalB $ metadata' isNewtype name cons) []] -- treeDatatypeInfo = ...
+             ]
+
 deriveGenericForDataDec :: Bool -> Cxt -> Name -> [TyVarBndr] -> [Con] -> [Name] -> Q [Dec]
 deriveGenericForDataDec _isNewtype _cxt name bndrs cons _derivs = do
   let typ = appTyVars name bndrs
@@ -80,7 +141,7 @@
   inst <- instanceD
             (cxt [])
             [t| Generic $typ |]
-            [codeSyn, embedding cons, projection cons]
+            [codeSyn, embedding 'from cons, projection 'to cons]
   return [inst]
 
 deriveMetadataForDataDec :: Bool -> Cxt -> Name -> [TyVarBndr] -> [Con] -> [Name] -> Q [Dec]
@@ -106,8 +167,8 @@
   Computing the embedding/projection pair
 -------------------------------------------------------------------------------}
 
-embedding :: [Con] -> Q Dec
-embedding = funD 'from . go (\e -> [| Z $e |])
+embedding :: Name -> [Con] -> Q Dec
+embedding fromName = funD fromName . go (\e -> [| Z $e |])
   where
     go :: (Q Exp -> Q Exp) -> [Con] -> [Q Clause]
     go _  []     = []
@@ -121,8 +182,8 @@
              (normalB [| SOP $(br . npE . map (appE (conE 'I) . varE) $ vars) |])
              []
 
-projection :: [Con] -> Q Dec
-projection = funD 'to . go (\p -> conP 'Z [p])
+projection :: Name -> [Con] -> Q Dec
+projection toName = funD toName . go (\p -> conP 'Z [p])
   where
     go :: (Q Pat -> Q Pat) -> [Con] -> [Q Clause]
     go _ [] = [unreachable]
@@ -147,7 +208,10 @@
 
 metadata :: Bool -> Name -> [Con] -> Q Dec
 metadata isNewtype typeName cs =
-    funD 'datatypeInfo [clause [wildP] (normalB md) []]
+    funD 'datatypeInfo [clause [wildP] (normalB $ metadata' isNewtype typeName cs) []]
+
+metadata' :: Bool -> Name -> [Con] -> Q Exp
+metadata' isNewtype typeName cs = md
   where
     md :: Q Exp
     md | isNewtype = [| Newtype $(stringE (nameModule' typeName))
diff --git a/src/Generics/SOP/Universe.hs b/src/Generics/SOP/Universe.hs
--- a/src/Generics/SOP/Universe.hs
+++ b/src/Generics/SOP/Universe.hs
@@ -2,7 +2,6 @@
 -- | Codes and interpretations
 module Generics.SOP.Universe where
 
-import Data.Proxy
 import qualified GHC.Generics as GHC
 
 import Generics.SOP.BasicFunctors
@@ -90,7 +89,7 @@
 --
 -- still holds.
 --
-class (SingI (Code a), All SingI (Code a)) => Generic (a :: *) where
+class (All SListI (Code a)) => Generic (a :: *) where
   -- | The code of a datatype.
   --
   -- This is a list of lists of its components. The outer list contains
@@ -133,6 +132,6 @@
 -- of 'Generic' for the options.
 --
 class HasDatatypeInfo a where
-  datatypeInfo         :: Proxy a -> DatatypeInfo (Code a)
-  default datatypeInfo :: (GDatatypeInfo a) => Proxy a -> DatatypeInfo (GCode a)
+  datatypeInfo         :: proxy a -> DatatypeInfo (Code a)
+  default datatypeInfo :: GDatatypeInfo a => proxy a -> DatatypeInfo (GCode a)
   datatypeInfo = gdatatypeInfo
diff --git a/test/Example.hs b/test/Example.hs
new file mode 100644
--- /dev/null
+++ b/test/Example.hs
@@ -0,0 +1,70 @@
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE FlexibleContexts #-}
+module Main (main, toTreeC) where
+
+import qualified GHC.Generics as GHC
+import Generics.SOP
+import Generics.SOP.TH
+
+-- Generic show, kind of
+gshow :: (Generic a, All2 Show (Code a)) => a -> String
+gshow x = gshowS (from x)
+
+gshowS :: (All2 Show xss) => SOP I xss -> String
+gshowS (SOP (Z xs))  = gshowP xs
+gshowS (SOP (S xss)) = gshowS (SOP xss)
+
+gshowP :: (All Show xs) => NP I xs -> String
+gshowP Nil         = ""
+gshowP (I x :* xs) = show x ++ (gshowP xs)
+
+
+-- GHC.Generics
+data Tree = Leaf Int | Node Tree Tree
+  deriving (GHC.Generic)
+
+tree :: Tree
+tree = Node (Leaf 1) (Leaf 2)
+
+instance Generic Tree
+instance HasDatatypeInfo Tree
+
+instance Show Tree where
+  show = gshow
+
+-- Template Haskell
+data TreeB = LeafB Int | NodeB TreeB TreeB
+
+treeB :: TreeB
+treeB = NodeB (LeafB 1) (LeafB 2)
+
+deriveGenericOnly ''TreeB
+
+instance Show TreeB where
+  show = gshow
+
+-- Orphan approach
+data TreeC = LeafC Int | NodeC TreeC TreeC
+
+treeC :: TreeC
+treeC = NodeC (LeafC 1) (LeafC 2)
+
+deriveGenericFunctions ''TreeC "TreeCCode" "fromTreeC" "toTreeC"
+deriveMetadataValue ''TreeC "TreeCCode" "treeDatatypeInfo"
+
+instance Show TreeC where
+  show x = gshowS (fromTreeC x)
+
+-- Tests
+main :: IO ()
+main = do
+  print tree
+  print $ datatypeInfo (Proxy :: Proxy Tree)
+  print treeB
+  print treeC
+  print treeDatatypeInfo