diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,316 @@
+# 0.5.1.4 (2023-10-18)
+
+* Compatibility with GHC-9.8 / th-abstraction-0.6
+  (thanks to Ganesh Sittampalam).
+
+# 0.5.1.3 (2023-04-23)
+
+* Compatibility with GHC-9.6 / th-abstraction-0.5
+  (thanks to Ryan Scott).
+
+# 0.5.1.2 (2022-01-02)
+
+* Compatibility with GHC-9.2.
+
+# 0.5.1.1 (2021-02-23)
+
+* Compatibility with GHC-9.0.
+
+# 0.5.1.0 (2020-03-29)
+
+* Compatibility with GHC-8.10 (thanks to Ryan Scott).
+
+* Improve TH generation support and extend it to
+  type families (thanks to Ryan Scott).
+
+# 0.5.0.0 (2019-05-09)
+
+* Add strictness info to the metadata. This means that
+  code directly using the `ADT` constructor has to be
+  modified because it now has a new fourth argument.
+  (See #76 and #87.)
+
+* Depend on `sop-core-0.5.0.*` which changes the
+  definition of `SameShapeAs` to improve compiler
+  performance and adds "ejections".
+
+# 0.4.0.1 (2018-10-23)
+
+* Remove `GHC.Event` import in `Generics.SOP.Instances`
+  to fix build on Windows.
+
+# 0.4.0.0 (2018-10-20)
+
+* Split into `sop-core` and `generics-sop` packages.
+
+* Drop support for GHC < 8.0.2, bump `base` dependency
+  to `>= 4.9` and remove dependency on `transformers`.
+
+* Simplify `All2 c` to `All (All c)` and simplify
+  `SListI xs` to `All Top xs`, and some implied
+  refactoring.
+
+* Add `Semigroup` and `Monoid` instances for various
+  datatypes.
+
+* Add specialised conversion functions for product
+  types, enumeration, and wrapped types.
+
+* Add benchmark suite.
+
+* Fix deriving `Generic` for empty datatypes.
+
+* `Generic` is now a superclass of `HasDatatypeInfo`.
+
+* More `Generic` instances for datatypes from recent
+  versions of `base`.
+
+# 0.3.2.0 (2018-01-08)
+
+* Make TH `deriveGenericFunctions` work properly with
+  parameterized types (note that the more widely used
+  `deriveGeneric` was already working correctly).
+
+* Make TH `deriveGeneric` work properly with empty
+  types.
+
+* Add `compare_NS`, `ccompare_NS`, `compare_SOP`, and
+  `ccompare_SOP` to better support comparison of sum
+  structures.
+
+* Add `hctraverse_` and `hctraverse'` as well as their
+  unconstrained variants and a number of derived functions,
+  to support effectful traversals.
+
+# 0.3.1.0 (2017-06-11)
+
+* Add `AllZip`, `htrans`, `hcoerce`, `hfromI`, `htoI`.
+  These functions are for converting between related
+  structures that do not have common signatures.
+
+  The most common application of these functions seems
+  to be the scenario where a datatype has components
+  that are all wrapped in a common type constructor
+  application, e.g. a datatype where every component
+  is a `Maybe`. Then we can use `hfromI` after `from`
+  to turn the generically derived `SOP` of `I`s into
+  an `SOP` of `Maybe`s (and back).
+
+* Add `IsProductType`, `IsEnumType`, `IsWrappedType`
+  and `IsNewtype` constraint synonyms capturing
+  specific classes of datypes.
+
+# 0.3.0.0 (2017-04-29)
+
+* No longer compatible with GHC 7.6, due to the lack of
+  support for type-level literals.
+
+* Support type-level metadata. This is provided by the
+  `Generics.SOP.Type.Metadata` module. The two modules
+  `Generics.SOP.Metadata` and `Generics.SOP.Type.Metadata`
+  export nearly the same names, so for backwards compatibility,
+  we keep exporting `Generics.SOP.Metadata` directly from
+  `Generics.SOP`, whereas `Generics.SOP.Type.Metadata` is
+  supposed to be imported explicitly (and qualified).
+
+  Term-level metadata is still available, but is now usually
+  computed automatically from the type-level metadata which
+  contains the same information, using the function
+  `demoteDatatypeInfo`. Term-level metadata is unchanged
+  from generics-sop-0.2, so in most cases, even if your
+  code makes use of metadata, you should not need to change
+  anything.
+
+  If you use TH deriving, then both type-level metadata and
+  term-level metadata is generated for you automatically,
+  for all supported GHC versions.
+
+  If you use GGP deriving, then type-level metadata is
+  available if you use GHC 8.0 or newer. If you use GHC 7.x,
+  then GHC.Generics supports only term-level metadata, so
+  we cannot translate that into type-level metadata. In
+  this combination, you cannot use code that relies on
+  type-level metadata, so you should either upgrade GHC or
+  switch to TH-based deriving.
+
+# 0.2.5.0 (2017-04-21)
+
+* GHC 8.2 compatibility.
+
+* Make `:.:` an instance of `Applicative`, `Foldable` and
+  `Traversable`.
+
+* Add functions `apInjs'_NP` and `apInjs'_POP`. These are
+  variants of `apInjs_NP` and `apInjs'_POP` that return their
+  result as an n-ary product, rather than collapsing it into
+  a list.
+
+* Add `hexpand` (and `expand_NS` and `expand_SOP`). These
+  functions expand sums into products, given a default value
+  to fill the other slots.
+
+* Add utility functions such as `mapII` or `mapIK` that lift
+  functions into different combinations of identity and
+  constant functors.
+
+* Add `NFData` (and lifted variants) instances for basic functors,
+  products and sums.
+
+# 0.2.4.0 (2017-02-02)
+
+* Add `hindex` (and `index_NS` and `index_SOP`).
+
+* Add `hapInjs` as a generalization of `apInjs_NP` and `apInjs_POP`.
+
+* Make basic functors instances of lifted classes (such as `Eq1` etc).
+
+# 0.2.3.0 (2016-12-04)
+
+* Add various metadata getters
+
+* Add `hdicts`.
+
+* Add catamorphisms and anamorphisms for `NP` and `NS`.
+
+* TH compatibility changes for GHC 8.1 (master).
+
+# 0.2.2.0 (2016-07-10)
+
+* Introduced `unZ` to destruct a unary sum.
+
+* Add Haddock `@since` annotations for various functions.
+
+# 0.2.1.0 (2016-02-08)
+
+* Now includes a CHANGELOG.
+
+* Should now work with ghc-8.0.1-rc1 and -rc2 (thanks to
+  Oleg Grenrus).
+
+* Introduced `hd` and `tl` to project out of a product, and
+  `Projection` and `projections` as duals of `Injection` and
+  `injections`.
+
+# 0.2.0.0 (2015-10-23)
+
+* Now tested with ghc-7.10
+
+* Introduced names `hmap`, `hcmap`, `hzipWith`, `hczipWith` for
+  `hliftA`, `hcliftA`, `hliftA2`, `hcliftA2`, respectively.
+  Similarly for the specialized versions of these functions.
+
+* The constraint transformers `All` and `All2` are now defined
+  as type classes, not type families. As a consequence, the
+  partial applications `All c` and `All2 c` are now possible.
+
+* Because of the redefinition of `All` and `All2`, some special
+  cases are no longer necessary. For example, `cpure_POP` can
+  now be implemented as a nested application of `pure_NP`.
+
+* Because of the redefinition of `All` and `All2`, the functions
+  `hcliftA'` and variants (with prime!) are now deprecated.
+  One can easily use the normal versions instead.
+  For example, the definition of `hcliftA'` is now simply
+
+      hcliftA' p = hcliftA (allP p)
+        where
+          allP :: proxy c -> Proxy (All c)
+          allP _ = Proxy
+
+* Because `All` and `All2` are now type classes, they now have
+  superclass constraints implying that the type-level lists they
+  are ranging over must have singletons.
+
+      class (SListI xs,  ...) => All c xs
+      class (SListI xss, ...) => All2 c xss
+
+  Some type signatures can be simplified due to this.
+
+* The `SingI` typeclass and `Sing` datatypes are now deprecated.
+  The replacements are called `SListI` and `SList`.
+  The `sing` method is now called `sList`. The difference
+  is that the new versions reveal only the spine of the list, and
+  contain no singleton representation for the elements anymore.
+
+  For one-dimensional type-level lists, replace
+
+      SingI xs => ...
+
+  by
+
+      SListI xs => ...
+
+  For two-dimensional type-level lists, replace
+
+      SingI xss => ...
+
+  by
+
+      All SListI xss => ...
+
+  Because All itself implies `SListI xss` (see above), this
+  constraint is equivalent to the old `Sing xss`.
+
+  The old names are provided for (limited) backward
+  compatibility. They map to the new constructs. This will
+  work in some, but not all scenarios.
+
+  The function `lengthSing` has also been renamed to
+  `lengthSList` for consistency, and the old name is
+  deprecated.
+
+* All `Proxy c` arguments have been replaced by `proxy c`
+  flexible arguments, so that other type constructors can be
+  used as proxies.
+
+* Class-level composition (`Compose`), pairing (`And`), and
+  a trivial constraint (`Top`) have been added. Type-level map
+  (`Map`) has been removed. Occurrences such as
+
+      All c (Map f xs)
+
+  should now be replaced with
+
+      All (c `Compose` f) xs
+
+* There is a new module called `Generics.SOP.Dict` that contains
+  functions for manipulating dictionaries explicitly. These can
+  be used to prove theorems about non-trivial class constraints
+  such as the ones that get built using `All` and `All2`. Some
+  such theorems are provided.
+
+* There is a new TH function `deriveGenericFunctions` that
+  derives the code of a datatype and conversion functions, but
+  does not create a class instance. (Contributed by Oleg Grenrus.)
+
+* There is a new TH function `deriveMetadataValue` that
+  derives a `DatatypeInfo` value for a datatype, but does
+  not create an instance of `HasDatatypeInfo`. (Contributed by
+  Oleg Grenrus.)
+
+* There is a very simple example file. (Contributed by Oleg
+  Grenrus.)
+
+* The function `hcollapse` for `NS` now results in an `a` rather
+  than an `I a`, matching the specialized version `collapse_NS`.
+  (Suggested by Roman Cheplyaka.)
+
+# 0.1.1.2 (2015-03-27)
+
+* Updated version bounds for ghc-prim (for ghc-7.10).
+
+# 0.1.1.1 (2015-03-20)
+
+* Preparations for ghc-7.10.
+
+* Documentation fix. (Contributed by Roman Cheplyaka.)
+
+# 0.1.1 (2015-01-06)
+
+* Documentation fixes.
+
+* Add superclass constraint (TODO).
+
+* Now derive tuple instance for tuples up to 30 components.
+  (Contributed by Michael Orlitzky.)
+
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/Setup.hs b/Setup.hs
deleted file mode 100644
--- a/Setup.hs
+++ /dev/null
@@ -1,2 +0,0 @@
-import Distribution.Simple
-main = defaultMain
diff --git a/bench/SOPBench.hs b/bench/SOPBench.hs
new file mode 100644
--- /dev/null
+++ b/bench/SOPBench.hs
@@ -0,0 +1,82 @@
+{-# LANGUAGE DataKinds #-}
+module Main where
+
+import Criterion.Main
+import SOPBench.Type
+import SOPBench.Roundtrip
+
+main :: IO ()
+main =
+  defaultMainWith defaultConfig
+    [ bgroup "Roundtrip"
+      [ bgroup "S2"
+        [ bench "GHCGeneric"     $ nf roundtrip (s2 :: S2 'GHCGeneric)
+        , bench "SOPGGP"         $ nf roundtrip (s2 :: S2 'SOPGGP    )
+        , bench "SOPTH"          $ nf roundtrip (s2 :: S2 'SOPTH     )
+        ]
+      , bgroup "S20"
+        [ bench "GHCGeneric"    $ nf roundtrip (s20 :: S20 'GHCGeneric)
+        , bench "SOPGGP"        $ nf roundtrip (s20 :: S20 'SOPGGP    )
+        , bench "SOPTH"         $ nf roundtrip (s20 :: S20 'SOPTH     )
+        ]
+      , bgroup "PB2"
+        [ bench "GHCGeneric"    $ nf roundtrip (pb2 :: PB2 'GHCGeneric)
+        , bench "SOPGGP"        $ nf roundtrip (pb2 :: PB2 'SOPGGP    )
+        , bench "SOPTH"         $ nf roundtrip (pb2 :: PB2 'SOPTH     )
+        ]
+      ]
+    , bgroup "Eq"
+      [ bgroup "S2"
+        [ bench "GHCDeriving"           $ nf ((==) s2) (s2 :: S2 'GHCDeriving)
+        , bench "SOPGGP"                $ nf ((==) s2) (s2 :: S2 'SOPGGP     )
+        , bench "SOPTH"                 $ nf ((==) s2) (s2 :: S2 'SOPTH      )
+        ]
+      , bgroup "S20"
+        [ bench "GHCDeriving"          $ nf ((==) s20) (s20 :: S20 'GHCDeriving)
+        , bench "SOPGGP"               $ nf ((==) s20) (s20 :: S20 'SOPGGP     )
+        , bench "SOPTH"                $ nf ((==) s20) (s20 :: S20 'SOPTH      )
+        ]
+      , bgroup "PB2"
+        [ bench "GHCDeriving"          $ nf ((==) pb2) (pb2 :: PB2 'GHCDeriving)
+        , bench "SOPGGP"               $ nf ((==) pb2) (pb2 :: PB2 'SOPGGP     )
+        , bench "SOPTH"                $ nf ((==) pb2) (pb2 :: PB2 'SOPTH      )
+        ]
+      , bgroup "Tree"
+        [ bench "GHCDeriving"         $ nf ((==) tree) (tree :: Tree 'GHCDeriving)
+        , bench "SOPGGP"              $ nf ((==) tree) (tree :: Tree 'SOPGGP     )
+        , bench "SOPTH"               $ nf ((==) tree) (tree :: Tree 'SOPTH      )
+        ]
+      , bgroup "Tree large"
+        [ bench "GHCDeriving"   $ nf ((==) tree_large) (tree_large :: Tree 'GHCDeriving)
+        , bench "SOPGGP"        $ nf ((==) tree_large) (tree_large :: Tree 'SOPGGP     )
+        , bench "SOPTH"         $ nf ((==) tree_large) (tree_large :: Tree 'SOPTH      )
+        ]
+      ]
+    , bgroup "Show"
+      [ bgroup "S2"
+        [ bench "GHCDeriving"         $ nf show (s2 :: S2 'GHCDeriving)
+        , bench "SOPGGP"              $ nf show (s2 :: S2 'SOPGGP     )
+        , bench "SOPTH"               $ nf show (s2 :: S2 'SOPTH      )
+        ]
+      , bgroup "S20"
+        [ bench "GHCDeriving"        $ nf show (s20 :: S20 'GHCDeriving)
+        , bench "SOPGGP"             $ nf show (s20 :: S20 'SOPGGP     )
+        , bench "SOPTH"              $ nf show (s20 :: S20 'SOPTH      )
+        ]
+      , bgroup "PB2"
+        [ bench "GHCDeriving"        $ nf show (pb2 :: PB2 'GHCDeriving)
+        , bench "SOPGGP"             $ nf show (pb2 :: PB2 'SOPGGP     )
+        , bench "SOPTH"              $ nf show (pb2 :: PB2 'SOPTH      )
+        ]
+      , bgroup "Tree"
+        [ bench "GHCDeriving"       $ nf show (tree :: Tree 'GHCDeriving)
+        , bench "SOPGGP"            $ nf show (tree :: Tree 'SOPGGP     )
+        , bench "SOPTH"             $ nf show (tree :: Tree 'SOPTH      )
+        ]
+      , bgroup "Tree large"
+        [ bench "GHCDeriving" $ nf show (tree_large :: Tree 'GHCDeriving)
+        , bench "SOPGGP"      $ nf show (tree_large :: Tree 'SOPGGP     )
+        , bench "SOPTH"       $ nf show (tree_large :: Tree 'SOPTH      )
+        ]
+      ]
+    ]
diff --git a/bench/SOPBench/Eq.hs b/bench/SOPBench/Eq.hs
new file mode 100644
--- /dev/null
+++ b/bench/SOPBench/Eq.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE MonoLocalBinds #-}
+module SOPBench.Eq where
+
+import Generics.SOP
+
+geq :: (Generic a, All2 Eq (Code a)) => a -> a -> Bool
+geq x y =
+  eq' (from x) (from y)
+
+eq' :: All2 Eq xss => SOP I xss -> SOP I xss -> Bool
+eq' =
+  ccompare_SOP
+    peq
+    False
+    (\ x y -> and (hcollapse (hczipWith peq (mapIIK (==)) x y)))
+    False
+
+peq :: Proxy Eq
+peq = Proxy
diff --git a/bench/SOPBench/Roundtrip.hs b/bench/SOPBench/Roundtrip.hs
new file mode 100644
--- /dev/null
+++ b/bench/SOPBench/Roundtrip.hs
@@ -0,0 +1,14 @@
+module SOPBench.Roundtrip where
+
+import qualified Generics.SOP as SOP
+import qualified GHC.Generics as GHC
+
+class Roundtrip a where
+  roundtrip :: a -> a
+
+soproundtrip :: SOP.Generic a => a -> a
+soproundtrip = SOP.to . SOP.from
+
+ghcroundtrip :: GHC.Generic a => a -> a
+ghcroundtrip = GHC.to . GHC.from
+
diff --git a/bench/SOPBench/Show.hs b/bench/SOPBench/Show.hs
new file mode 100644
--- /dev/null
+++ b/bench/SOPBench/Show.hs
@@ -0,0 +1,60 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+module SOPBench.Show where
+
+import Data.List (intersperse)
+import Generics.SOP
+
+gshow ::
+  (Generic a, HasDatatypeInfo a, All2 Show (Code a)) => a -> String
+gshow x =
+  gshowsPrec 0 x ""
+
+gshowsPrec ::
+  (Generic a, HasDatatypeInfo a, All2 Show (Code a)) => Int -> a -> ShowS
+gshowsPrec d x =
+    hcollapse
+  $ hczipWith pallshow (gshowsConstructor d)
+      (constructorInfo (datatypeInfo (I x)))
+      (unSOP (from x))
+
+gshowsConstructor ::
+  forall xs . (All Show xs) => Int -> ConstructorInfo xs -> NP I xs -> K ShowS xs
+gshowsConstructor d i =
+  case i of
+    Constructor n -> \ x -> K
+      $ showParen (d > app_prec)
+      $ showString n . showString " " . gshowsConstructorArgs (app_prec + 1) x
+    Infix n _ prec -> \ (I l :* I r :* Nil) -> K
+      $ showParen (d > prec)
+      $ showsPrec (prec + 1) l
+      . showString " " . showString n . showString " "
+      . showsPrec (prec + 1) r
+    Record n fi -> \ x -> K
+      $ showParen (d > app_prec) -- could be even higher, but seems to match GHC behaviour
+      $ showString n . showString " {" . gshowsRecordArgs fi x . showString "}"
+
+gshowsConstructorArgs ::
+  (All Show xs) => Int -> NP I xs -> ShowS
+gshowsConstructorArgs d x =
+  foldr (.) id $ hcollapse $ hcmap pshow (K . showsPrec d . unI) x
+
+gshowsRecordArgs ::
+  (All Show xs) => NP FieldInfo xs -> NP I xs -> ShowS
+gshowsRecordArgs fi x =
+    foldr (.) id
+  $ intersperse (showString ", ")
+  $ hcollapse
+  $ hczipWith pshow
+      (\ (FieldInfo l) (I y) -> K (showString l . showString " = " . showsPrec 0 y))
+      fi x
+
+pallshow :: Proxy (All Show)
+pallshow = Proxy
+
+pshow :: Proxy Show
+pshow = Proxy
+
+app_prec :: Int
+app_prec = 10
diff --git a/bench/SOPBench/Type.hs b/bench/SOPBench/Type.hs
new file mode 100644
--- /dev/null
+++ b/bench/SOPBench/Type.hs
@@ -0,0 +1,296 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies #-}
+module SOPBench.Type where
+
+import Control.DeepSeq
+import qualified Generics.SOP as SOP
+import Generics.SOP.TH
+import qualified GHC.Generics as GHC
+import Language.Haskell.TH
+
+import qualified SOPBench.Eq as SOP
+import qualified SOPBench.Show as SOP
+import SOPBench.Roundtrip
+
+data S2 (tag :: Mode) =
+    S2_0
+  | S2_1
+
+s2 :: S2 tag
+s2 = S2_1
+
+data S20 (tag :: Mode) =
+    S20_00
+  | S20_01
+  | S20_02
+  | S20_03
+  | S20_04
+  | S20_05
+  | S20_06
+  | S20_07
+  | S20_08
+  | S20_09
+  | S20_10
+  | S20_11
+  | S20_12
+  | S20_13
+  | S20_14
+  | S20_15
+  | S20_16
+  | S20_17
+  | S20_18
+  | S20_19
+
+s20 :: S20 tag
+s20 = S20_17
+
+data PB2 (tag :: Mode) =
+    PB2 Bool Bool
+
+pb2 :: PB2 tag
+pb2 = PB2 True False
+
+data Tree (tag :: Mode) =
+    Leaf Int
+  | Node (Tree tag) (Tree tag)
+
+tree :: Tree tag
+tree = Node (Node (Leaf 1) (Leaf 2)) (Node (Leaf 3) (Leaf 4))
+
+tree_medium :: Tree tag
+tree_medium =
+  Node (Node tree (Node tree tree)) (Node (Node tree tree) tree)
+
+tree_large :: Tree tag
+tree_large =
+  Node
+    (Node tree_medium (Node tree_medium tree_medium))
+    (Node (Node tree_medium tree_medium) tree_medium)
+
+data Prop (tag :: Mode) =
+    Var String
+  | T
+  | F
+  | Not (Prop tag)
+  | And (Prop tag) (Prop tag)
+  | Or  (Prop tag) (Prop tag)
+
+data Mode =
+    Handwritten
+  | GHCDeriving
+  | GHCGeneric
+  | SOPGGP
+  | SOPTH
+
+-- NFData is used for forcing benchmark results, so we
+-- derive it by hand for all variants of the datatype
+
+rnfS2 :: S2 tag -> ()
+rnfS2 S2_0 = ()
+rnfS2 S2_1 = ()
+
+instance          NFData              (S2   'GHCDeriving) where
+  rnf = rnfS2
+
+instance          NFData              (S2   'GHCGeneric ) where
+  rnf = rnfS2
+
+instance          NFData              (S2   'SOPGGP     ) where
+  rnf = rnfS2
+
+instance          NFData              (S2   'SOPTH      ) where
+  rnf = rnfS2
+
+rnfS20 :: S20 tag -> ()
+rnfS20 S20_00 = ()
+rnfS20 S20_01 = ()
+rnfS20 S20_02 = ()
+rnfS20 S20_03 = ()
+rnfS20 S20_04 = ()
+rnfS20 S20_05 = ()
+rnfS20 S20_06 = ()
+rnfS20 S20_07 = ()
+rnfS20 S20_08 = ()
+rnfS20 S20_09 = ()
+rnfS20 S20_10 = ()
+rnfS20 S20_11 = ()
+rnfS20 S20_12 = ()
+rnfS20 S20_13 = ()
+rnfS20 S20_14 = ()
+rnfS20 S20_15 = ()
+rnfS20 S20_16 = ()
+rnfS20 S20_17 = ()
+rnfS20 S20_18 = ()
+rnfS20 S20_19 = ()
+
+instance          NFData              (S20  'GHCDeriving) where
+  rnf = rnfS20
+
+instance          NFData              (S20  'GHCGeneric ) where
+  rnf = rnfS20
+
+instance          NFData              (S20  'SOPGGP     ) where
+  rnf = rnfS20
+
+instance          NFData              (S20  'SOPTH      ) where
+  rnf = rnfS20
+
+rnfPB2 :: PB2 tag -> ()
+rnfPB2 (PB2 b0 b1) =
+  rnf b0 `seq` rnf b1
+
+instance          NFData              (PB2  'GHCDeriving) where
+  rnf = rnfPB2
+
+instance          NFData              (PB2  'GHCGeneric ) where
+  rnf = rnfPB2
+
+instance          NFData              (PB2  'SOPGGP     ) where
+  rnf = rnfPB2
+
+instance          NFData              (PB2  'SOPTH      ) where
+  rnf = rnfPB2
+
+deriving instance Eq                  (S2   'GHCDeriving)
+deriving instance Show                (S2   'GHCDeriving)
+
+deriving instance GHC.Generic         (S2   'GHCGeneric)
+deriving instance GHC.Generic         (S2   'SOPGGP)
+instance          SOP.Generic         (S2   'SOPGGP)
+instance          SOP.HasDatatypeInfo (S2   'SOPGGP)
+
+deriveGenericSubst ''S2 (const (promotedT 'SOPTH))
+
+instance          Roundtrip           (S2   'GHCGeneric) where
+  roundtrip = ghcroundtrip
+
+instance          Roundtrip           (S2   'SOPGGP) where
+  roundtrip = soproundtrip
+
+instance          Roundtrip           (S2   'SOPTH) where
+  roundtrip = soproundtrip
+
+instance          Eq                  (S2   'SOPGGP) where
+  (==) = SOP.geq
+
+instance          Eq                  (S2   'SOPTH)  where
+  (==) = SOP.geq
+
+instance          Show                (S2   'SOPGGP) where
+  showsPrec = SOP.gshowsPrec
+
+instance          Show                (S2   'SOPTH)  where
+  showsPrec = SOP.gshowsPrec
+
+deriveGenericSubst ''S20 (const (promotedT 'SOPTH))
+
+instance          Roundtrip           (S20  'GHCGeneric) where
+  roundtrip = ghcroundtrip
+
+instance          Roundtrip           (S20  'SOPGGP) where
+  roundtrip = soproundtrip
+
+instance          Roundtrip           (S20  'SOPTH) where
+  roundtrip = soproundtrip
+
+deriving instance Eq                  (S20  'GHCDeriving)
+deriving instance Show                (S20  'GHCDeriving)
+
+deriving instance GHC.Generic         (S20  'GHCGeneric)
+deriving instance GHC.Generic         (S20  'SOPGGP)
+instance          SOP.Generic         (S20  'SOPGGP)
+instance          SOP.HasDatatypeInfo (S20  'SOPGGP)
+
+instance          Eq                  (S20  'SOPGGP) where
+  (==) = SOP.geq
+
+instance          Eq                  (S20  'SOPTH)  where
+  (==) = SOP.geq
+
+instance          Show                (S20  'SOPGGP) where
+  showsPrec = SOP.gshowsPrec
+
+instance          Show                (S20  'SOPTH)  where
+  showsPrec = SOP.gshowsPrec
+
+deriveGenericSubst ''PB2 (const (promotedT 'SOPTH))
+
+instance          Roundtrip           (PB2  'GHCGeneric) where
+  roundtrip = ghcroundtrip
+
+instance          Roundtrip           (PB2  'SOPGGP) where
+  roundtrip = soproundtrip
+
+instance          Roundtrip           (PB2  'SOPTH) where
+  roundtrip = soproundtrip
+
+deriving instance Eq                  (PB2  'GHCDeriving)
+deriving instance Show                (PB2  'GHCDeriving)
+
+deriving instance GHC.Generic         (PB2  'GHCGeneric)
+deriving instance GHC.Generic         (PB2  'SOPGGP)
+instance          SOP.Generic         (PB2  'SOPGGP)
+instance          SOP.HasDatatypeInfo (PB2  'SOPGGP)
+
+instance          Eq                  (PB2  'SOPGGP) where
+  (==) = SOP.geq
+
+instance          Eq                  (PB2  'SOPTH) where
+  (==) = SOP.geq
+
+instance          Show                (PB2  'SOPGGP) where
+  showsPrec = SOP.gshowsPrec
+
+instance          Show                (PB2  'SOPTH) where
+  showsPrec = SOP.gshowsPrec
+
+deriving instance Eq                  (Tree 'GHCDeriving)
+deriving instance Show                (Tree 'GHCDeriving)
+
+deriving instance GHC.Generic         (Tree 'GHCGeneric)
+deriving instance GHC.Generic         (Tree 'SOPGGP)
+instance          SOP.Generic         (Tree 'SOPGGP)
+instance          SOP.HasDatatypeInfo (Tree 'SOPGGP)
+
+deriveGenericSubst ''Tree (const (promotedT 'SOPTH))
+
+instance          Eq                  (Tree 'SOPGGP) where
+  (==) = SOP.geq
+
+instance          Eq                  (Tree 'SOPTH)  where
+  (==) = SOP.geq
+
+instance          Show                (Tree 'SOPGGP) where
+  showsPrec = SOP.gshowsPrec
+
+instance          Show                (Tree 'SOPTH)  where
+  showsPrec = SOP.gshowsPrec
+
+deriving instance Eq                  (Prop 'GHCDeriving)
+deriving instance Show                (Prop 'GHCDeriving)
+
+deriving instance GHC.Generic         (Prop 'GHCGeneric)
+deriving instance GHC.Generic         (Prop 'SOPGGP)
+instance          SOP.Generic         (Prop 'SOPGGP)
+instance          SOP.HasDatatypeInfo (Prop 'SOPGGP)
+
+deriveGenericSubst ''Prop (const (promotedT 'SOPTH))
+
+instance          Eq                  (Prop 'SOPGGP) where
+  (==) = SOP.geq
+
+instance          Eq                  (Prop 'SOPTH)  where
+  (==) = SOP.geq
+
+instance          Show                (Prop 'SOPGGP) where
+  showsPrec = SOP.gshowsPrec
+
+instance          Show                (Prop 'SOPTH)  where
+  showsPrec = SOP.gshowsPrec
+
+
diff --git a/doctest.sh b/doctest.sh
new file mode 100644
--- /dev/null
+++ b/doctest.sh
@@ -0,0 +1,25 @@
+#!/bin/sh
+
+set -ex
+
+doctest --preserve-it \
+  -XCPP \
+  -XScopedTypeVariables \
+  -XTypeFamilies \
+  -XRankNTypes \
+  -XTypeOperators \
+  -XGADTs \
+  -XConstraintKinds \
+  -XMultiParamTypeClasses \
+  -XTypeSynonymInstances \
+  -XFlexibleInstances \
+  -XFlexibleContexts \
+  -XDeriveFunctor \
+  -XDeriveFoldable \
+  -XDeriveTraversable \
+  -XDefaultSignatures \
+  -XKindSignatures \
+  -XDataKinds \
+  -XFunctionalDependencies \
+  -i../sop/src \
+  $(find src -name '*.hs')
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.5.1.4
 synopsis:            Generic Programming using True Sums of Products
 description:
   A library to support the definition of generic functions.
@@ -11,6 +11,11 @@
   The module "Generics.SOP" is the main module of this library and contains
   more detailed documentation.
   .
+  Since version 0.4.0.0, this package is now based on
+  @<https://hackage.haskell.org/package/sop-core sop-core>@. The core package
+  contains all the functionality of n-ary sums and products, whereas this
+  package provides the datatype-generic programming support on top.
+  .
   Examples of using this library are provided by the following
   packages:
   .
@@ -32,11 +37,12 @@
 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
+extra-source-files:  CHANGELOG.md doctest.sh
+tested-with:         GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.4, GHC == 8.6.5, GHC == 8.8.4, GHC == 8.10.7, GHC == 9.0.2, GHC == 9.2.7, GHC == 9.4.4, GHC == 9.6.1, GHC == 9.8.1
 
 source-repository head
   type:                git
@@ -46,22 +52,24 @@
   exposed-modules:     Generics.SOP
                        Generics.SOP.GGP
                        Generics.SOP.TH
+                       Generics.SOP.Type.Metadata
                        -- exposed via Generics.SOP:
+                       Generics.SOP.Instances
+                       Generics.SOP.Metadata
+                       Generics.SOP.Universe
+                       -- re-exported from Data.SOP:
+                       Generics.SOP.Dict
                        Generics.SOP.BasicFunctors
                        Generics.SOP.Classes
                        Generics.SOP.Constraint
-                       Generics.SOP.Instances
-                       Generics.SOP.Metadata
                        Generics.SOP.NP
                        Generics.SOP.NS
-                       Generics.SOP.Universe
                        Generics.SOP.Sing
-  build-depends:       base                 >= 4.6  && < 5,
-                       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:       base                 >= 4.9  && < 4.20,
+                       sop-core             == 0.5.0.*,
+                       template-haskell     >= 2.8  && < 2.22,
+                       th-abstraction       >= 0.6  && < 0.7,
+                       ghc-prim             >= 0.3  && < 0.12
   hs-source-dirs:      src
   default-language:    Haskell2010
   ghc-options:         -Wall
@@ -83,11 +91,55 @@
                        KindSignatures
                        DataKinds
                        FunctionalDependencies
-  if impl (ghc >= 7.8)
-    default-extensions:  AutoDeriveTypeable
-  other-extensions:    OverloadedStrings
-                       PolyKinds
+
+  if impl(ghc <8.2)
+    default-extensions: AutoDeriveTypeable
+
+  -- if impl(ghc >= 8.6)
+  --   default-extensions: NoStarIsType
+  other-extensions:    PolyKinds
                        UndecidableInstances
                        TemplateHaskell
-                       DeriveGeneric
                        StandaloneDeriving
+                       EmptyCase
+                       UndecidableSuperClasses
+
+test-suite generics-sop-examples
+  type:                exitcode-stdio-1.0
+  main-is:             Example.hs
+  other-modules:       HTransExample
+  hs-source-dirs:      test
+  default-language:    Haskell2010
+  ghc-options:         -Wall
+  build-depends:       base                 >= 4.9  && < 5,
+                       generics-sop
+  other-extensions:    DeriveGeneric
+                       EmptyCase
+                       TemplateHaskell
+                       ConstraintKinds
+                       GADTs
+                       DataKinds
+                       TypeFamilies
+                       FlexibleContexts
+                       FlexibleInstances
+                       PolyKinds
+                       DefaultSignatures
+                       FunctionalDependencies
+                       MultiParamTypeClasses
+                       TypeFamilies
+
+benchmark generics-sop-bench
+  type:                exitcode-stdio-1.0
+  main-is:             SOPBench.hs
+  other-modules:       SOPBench.Type
+                       SOPBench.Roundtrip
+                       SOPBench.Eq
+                       SOPBench.Show
+  hs-source-dirs:      bench
+  default-language:    Haskell2010
+  ghc-options:         -Wall
+  build-depends:       base                 >= 4.6  && < 5,
+                       criterion,
+                       deepseq,
+                       generics-sop,
+                       template-haskell
diff --git a/src/Generics/SOP.hs b/src/Generics/SOP.hs
--- a/src/Generics/SOP.hs
+++ b/src/Generics/SOP.hs
@@ -25,7 +25,7 @@
 --       witness the isomorphism.
 --
 --   3.  Since all 'Rep' types are sums of products, you can define
---       functions over them by performing induction on the structure, of
+--       functions over them by performing induction on the structure, or
 --       by using predefined combinators that the library provides. Such
 --       functions then work for all 'Rep' types.
 --
@@ -52,7 +52,7 @@
 --
 -- To create 'Generic' instances for @A@ and @B@ via "GHC.Generics", we say
 --
--- > {-# LANGUAGE DeriveGenerics #-}
+-- > {-# LANGUAGE DeriveGeneric #-}
 -- >
 -- > import qualified GHC.Generics as GHC
 -- > import Generics.SOP
@@ -145,16 +145,20 @@
 --
 -- @
 -- grnf :: ('Generic' a, 'All2' NFData ('Code' a)) => a -> ()
--- grnf = 'rnf' . 'hcollapse' . 'hcliftA' ('Proxy' :: 'Proxy' NFData) (\\ ('I' x) -> 'K' (rnf x)) . 'from'
+-- grnf = 'rnf' . 'hcollapse' . 'hcmap' ('Proxy' :: 'Proxy' NFData) ('mapIK' rnf) . 'from'
 -- @
 --
+-- 'mapIK' and friends ('mapII', 'mapKI', etc.) are small helpers for working
+-- with 'I' and 'K' functors, for example 'mapIK' is defined as
+-- @'mapIK' f = \\ ('I' x) -> 'K' (f x)@
+--
 -- The following interaction should provide an idea of the individual
 -- transformation steps:
 --
 -- >>> let x = G 2.5 'A' False :: B Double
 -- >>> from x
 -- SOP (S (Z (I 2.5 :* I 'A' :* I False :* Nil)))
--- >>> hcliftA (Proxy :: Proxy NFData) (\ (I x) -> K (rnf x)) it
+-- >>> hcmap (Proxy :: Proxy NFData) (mapIK rnf) it
 -- SOP (S (Z (K () :* K () :* K () :* Nil)))
 -- >>> hcollapse it
 -- [(),(),()]
@@ -162,7 +166,7 @@
 -- ()
 --
 -- The 'from' call converts into the structural representation.
--- Via 'hcliftA', we apply 'rnf' to all the components. The result
+-- Via 'hcmap', we apply 'rnf' to all the components. The result
 -- is a sum of products of the same shape, but the components are
 -- no longer heterogeneous ('I'), but homogeneous (@'K' ()@). A
 -- homogeneous structure can be collapsed ('hcollapse') into a
@@ -179,6 +183,7 @@
 -- ()
 -- >>> grnf (G 2.5 undefined False)
 -- *** Exception: Prelude.undefined
+-- ...
 --
 -- Note that the type of 'grnf' requires that all components of the
 -- type are in the 'Control.DeepSeq.NFData' class. For a recursive
@@ -218,6 +223,20 @@
     -- * Codes and interpretations
     Generic(..)
   , Rep
+  , IsProductType
+  , ProductCode
+  , productTypeFrom
+  , productTypeTo
+  , IsEnumType
+  , enumTypeFrom
+  , enumTypeTo
+  , IsWrappedType
+  , WrappedCode
+  , wrappedTypeFrom
+  , wrappedTypeTo
+  , IsNewtype
+  , newtypeFrom
+  , newtypeTo
     -- * n-ary datatypes
   , NP(..)
   , NS(..)
@@ -227,8 +246,13 @@
   , unPOP
     -- * Metadata
   , DatatypeInfo(..)
+  , moduleName
+  , datatypeName
+  , constructorInfo
   , ConstructorInfo(..)
+  , constructorName
   , FieldInfo(..)
+  , fieldName
   , HasDatatypeInfo(..)
   , DatatypeName
   , ModuleName
@@ -239,8 +263,14 @@
     -- * Combinators
     -- ** Constructing products
   , HPure(..)
+    -- ** Destructing products
+  , hd
+  , tl
+  , Projection
+  , projections
+  , shiftProjection
     -- ** Application
-  , (-.->)(..)
+  , type (-.->)(..)
   , fn
   , fn_2
   , fn_3
@@ -254,25 +284,54 @@
   , hcliftA
   , hcliftA2
   , hcliftA3
+  , hmap
+  , hzipWith
+  , hzipWith3
+  , hcmap
+  , hczipWith
+  , hczipWith3
     -- ** Constructing sums
   , Injection
   , injections
   , shift
-  , apInjs_NP
-  , apInjs_POP
+  , shiftInjection
+  , UnProd
+  , HApInjs(..)
+  , apInjs_NP  -- deprecated export
+  , apInjs_POP -- deprecated export
+    -- ** Destructing sums
+  , unZ
+  , HIndex(..)
+  , Ejection
+  , ejections
+  , shiftEjection
     -- ** Dealing with @'All' c@
-  , AllDict(..)
-  , allDict_NP
   , hcliftA'
   , hcliftA2'
   , hcliftA3'
+    -- ** Comparison
+  , compare_NS
+  , ccompare_NS
+  , compare_SOP
+  , ccompare_SOP
     -- ** Collapsing
   , CollapseTo
   , HCollapse(..)
-    -- ** Sequencing
+    -- ** Folding and sequencing
+  , HTraverse_(..)
+  , hcfoldMap
+  , hcfor_
   , HSequence(..)
   , hsequence
   , hsequenceK
+  , hctraverse
+  , hcfor
+    -- ** Expanding sums to products
+  , HExpand(..)
+    -- ** Transformation of index lists and coercions
+  , HTrans(..)
+  , hfromI
+  , htoI
     -- ** Partial operations
   , fromList
     -- * Utilities
@@ -283,18 +342,45 @@
   , unI
   , (:.:)(..)
   , unComp
+    -- *** Mapping functions
+  , mapII
+  , mapIK
+  , mapKI
+  , mapKK
+  , mapIII
+  , mapIIK
+  , mapIKI
+  , mapIKK
+  , mapKII
+  , mapKIK
+  , mapKKI
+  , mapKKK
     -- ** Mapping constraints
   , All
   , All2
-  , Map
-  , AllMap
+  , cpara_SList
+  , ccase_SList
+  , AllZip
+  , AllZip2
+  , AllN
+  , AllZipN
+    -- ** Other constraints
+  , Compose
+  , And
+  , Top
+  , LiftedCoercible
+  , SameShapeAs
     -- ** Singletons
-  , Sing(..)
-  , SingI(..)
+  , SList(..)
+  , SListI
+  , SListI2
+  , sList
+  , para_SList
+  , case_SList
     -- *** Shape of type-level lists
   , Shape(..)
   , shape
-  , lengthSing
+  , lengthSList
     -- ** Re-exports
 
 -- Workaround for lack of MIN_TOOL_VERSION macro in Cabal 1.18, see:
@@ -320,3 +406,15 @@
 import Generics.SOP.Universe
 import Generics.SOP.Sing
 
+-- $setup
+--
+-- >>> :set -XDeriveGeneric
+-- >>> import qualified GHC.Generics as GHC
+-- >>> import Generics.SOP
+-- >>> import Control.DeepSeq
+-- >>> data B a = F | G a Char Bool deriving (Show, GHC.Generic)
+-- >>> data A   = C Bool | D A Int | E (B ()) deriving (Show, GHC.Generic)
+-- >>> instance Generic A     -- empty
+-- >>> instance Generic (B a) -- empty
+--
+-- >>> let grnf = rnf . hcollapse . hcmap (Proxy :: Proxy NFData) (\ (I x) -> K (rnf x)) . from
diff --git a/src/Generics/SOP/BasicFunctors.hs b/src/Generics/SOP/BasicFunctors.hs
--- a/src/Generics/SOP/BasicFunctors.hs
+++ b/src/Generics/SOP/BasicFunctors.hs
@@ -1,110 +1,6 @@
-{-# LANGUAGE PolyKinds, DeriveGeneric #-}
--- | Basic functors.
---
--- Definitions of the type-level equivalents of
--- 'const', 'id', and ('.'), and a definition of
--- the lifted function space.
---
--- These datatypes are generally useful, but in this
--- library, they're primarily used as parameters for
--- the 'NP', 'NS', 'POP', and 'SOP' types.
---
 module Generics.SOP.BasicFunctors
-  ( K(..)
-  , unK
-  , I(..)
-  , unI
-  , (:.:)(..)
-  , unComp
+  (
+    module Data.SOP.BasicFunctors
   ) where
 
-#if MIN_VERSION_base(4,8,0)
-import Data.Monoid ((<>))
-#else
-import Control.Applicative
-import Data.Foldable (Foldable(..))
-import Data.Monoid (Monoid, mempty, (<>))
-import Data.Traversable (Traversable(..))
-#endif
-import qualified GHC.Generics as GHC
-
--- | The constant type functor.
---
--- Like 'Data.Functor.Constant.Constant', but kind-polymorphic
--- in its second argument and with a shorter name.
---
-newtype K (a :: *) (b :: k) = K a
-#if MIN_VERSION_base(4,7,0)
-  deriving (Show, Functor, Foldable, Traversable, GHC.Generic)
-#else
-  deriving (Show, GHC.Generic)
-
-instance Functor (K a) where
-  fmap _ (K x) = K x
-
-instance Foldable (K a) where
-  foldr _ z (K _) = z
-  foldMap _ (K _) = mempty
-
-instance Traversable (K a) where
-  traverse _ (K x) = pure (K x)
-#endif
-
-instance Monoid a => Applicative (K a) where
-  pure _      = K mempty
-  K x <*> K y = K (x <> y)
-
--- | Extract the contents of a 'K' value.
-unK :: K a b -> a
-unK (K x) = x
-
--- | The identity type functor.
---
--- Like 'Data.Functor.Identity.Identity', but with a shorter name.
---
-newtype I (a :: *) = I a
-#if MIN_VERSION_base(4,7,0)
-  deriving (Show, Functor, Foldable, Traversable, GHC.Generic)
-#else
-  deriving (Show, GHC.Generic)
-
-instance Functor I where
-  fmap f (I x) = I (f x)
-
-instance Foldable I where
-  foldr f z (I x) = f x z
-  foldMap f (I x) = f x
-
-instance Traversable I where
-  traverse f (I x) = fmap I (f x)
-#endif
-
-instance Applicative I where
-  pure = I
-  I f <*> I x = I (f x)
-
-instance Monad I where
-  return = I
-  I x >>= f = f x
-
--- | Extract the contents of an 'I' value.
-unI :: I a -> a
-unI (I x) = x
-
--- | Composition of functors.
---
--- Like 'Data.Functor.Compose.Compose', but kind-polymorphic
--- and with a shorter name.
---
-newtype (:.:) (f :: l -> *) (g :: k -> l) (p :: k) = Comp (f (g p))
-  deriving (Show, GHC.Generic)
-
-infixr 7 :.:
-
-instance (Functor f, Functor g) => Functor (f :.: g) where
-  fmap f (Comp x) = Comp (fmap (fmap f) x)
-
--- | Extract the contents of a 'Comp' value.
-unComp :: (f :.: g) p -> f (g p)
-unComp (Comp x) = x
-
+import Data.SOP.BasicFunctors
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
@@ -1,310 +1,6 @@
-{-# LANGUAGE PolyKinds #-}
--- | Classes for generalized combinators on SOP types.
---
--- In the SOP approach to generic programming, we're predominantly
--- concerned with four structured datatypes:
---
--- @
---   'Generics.SOP.NP.NP'  :: (k -> *) -> ( [k]  -> *)   -- n-ary product
---   'Generics.SOP.NS.NS'  :: (k -> *) -> ( [k]  -> *)   -- n-ary sum
---   'Generics.SOP.NP.POP' :: (k -> *) -> ([[k]] -> *)   -- product of products
---   'Generics.SOP.NS.SOP' :: (k -> *) -> ([[k]] -> *)   -- sum of products
--- @
---
--- All of these have a kind that fits the following pattern:
---
--- @
---   (k -> *) -> (l -> *)
--- @
---
--- These four types support similar interfaces. In order to allow
--- reusing the same combinator names for all of these types, we define
--- various classes in this module that allow the necessary
--- generalization.
---
--- The classes typically lift concepts that exist for kinds @*@ or
--- @* -> *@ to datatypes of kind @(k -> *) -> (l -> *)@. This module
--- also derives a number of derived combinators.
---
--- The actual instances are defined in "Generics.SOP.NP" and
--- "Generics.SOP.NS".
---
-module Generics.SOP.Classes where
-
-#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.
-class HPure (h :: (k -> *) -> (l -> *)) where
-  -- | Corresponds to 'Control.Applicative.pure' directly.
-  --
-  -- /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  ::  SingI xs => (forall a. f a) -> h f xs
-
-  -- | A variant of 'hpure' that allows passing in a constrained
-  -- argument.
-  --
-  -- Calling @'hcpure' f s@ where @s :: h f xs@ causes @f@ to be
-  -- applied at all the types that are contained in @xs@. Therefore,
-  -- the constraint @c@ has to be satisfied for all elements of @xs@,
-  -- which is what @'AllMap' h c xs@ states.
-  --
-  -- Morally, 'hpure' is a special case of 'hcpure' where the
-  -- constraint is empty. However, it is in the nature of how 'AllMap'
-  -- is defined as well as current GHC limitations that it is tricky
-  -- to prove to GHC in general that @'AllMap' h c NoConstraint xs@ is
-  -- always satisfied. Therefore, we typically define 'hpure'
-  -- separately and directly, and make it a member of the class.
-  --
-  -- /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 :: (SingI xs, AllMap h c xs) => Proxy c -> (forall a. c a => f a) -> h f xs
-
-{-------------------------------------------------------------------------------
-  Application
--------------------------------------------------------------------------------}
-
--- | Lifted functions.
-newtype (f -.-> g) a = Fn { apFn :: f a -> g a }
-
--- TODO: What is the right precedence?
-infixr 1 -.->
-
--- | Construct a lifted function.
---
--- Same as 'Fn'. Only available for uniformity with the
--- higher-arity versions.
---
-fn   :: (f a -> f' a) -> (f -.-> f') a
-
--- | Construct a binary lifted function.
-fn_2 :: (f a -> f' a -> f'' a) -> (f -.-> f' -.-> f'') a
-
--- | Construct a ternary lifted function.
-fn_3 :: (f a -> f' a -> f'' a -> f''' a) -> (f -.-> f' -.-> f'' -.-> f''') a
-
--- | Construct a quarternary lifted function.
-fn_4 :: (f a -> f' a -> f'' a -> f''' a -> f'''' a) -> (f -.-> f' -.-> f'' -.-> f''' -.-> f'''') a
-
-fn   f = Fn $ \x -> f x
-fn_2 f = Fn $ \x -> Fn $ \x' -> f x x'
-fn_3 f = Fn $ \x -> Fn $ \x' -> Fn $ \x'' -> f x x' x''
-fn_4 f = Fn $ \x -> Fn $ \x' -> Fn $ \x'' -> Fn $ \x''' -> f x x' x'' x'''
-
--- | Maps a structure containing sums to the corresponding
--- product structure.
-type family Prod (h :: (k -> *) -> (l -> *)) :: (k -> *) -> (l -> *)
-
--- | A generalization of 'Control.Applicative.<*>'.
-class (Prod (Prod h) ~ Prod h, HPure (Prod h)) => HAp (h  :: (k -> *) -> (l -> *)) where
-
-  -- | 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.
-  --
-  -- The same combinator can also be used to combine a product
-  -- structure of functions with a sum structure of arguments, which then
-  -- results in another sum structure of results. The sum structure
-  -- determines which part of the product structure will be used.
-  --
-  -- /Instances:/
-  --
-  -- @
-  -- 'hap', 'Generics.SOP.NP.ap_NP'  :: 'Generics.SOP.NP.NP'  (f -.-> g) xs  -> 'Generics.SOP.NP.NP'  f xs  -> 'Generics.SOP.NP.NP'  g xs
-  -- 'hap', 'Generics.SOP.NS.ap_NS'  :: 'Generics.SOP.NS.NP'  (f -.-> g) xs  -> 'Generics.SOP.NS.NS'  f xs  -> 'Generics.SOP.NS.NS'  g xs
-  -- 'hap', 'Generics.SOP.NP.ap_POP' :: 'Generics.SOP.NP.POP' (f -.-> g) xss -> 'Generics.SOP.NP.POP' f xss -> 'Generics.SOP.NP.POP' g xss
-  -- 'hap', 'Generics.SOP.NS.ap_SOP' :: 'Generics.SOP.NS.POP' (f -.-> g) xss -> 'Generics.SOP.NS.SOP' f xss -> 'Generics.SOP.NS.SOP' g xss
-  -- @
-  --
-  hap :: Prod h (f -.-> g) xs -> h f xs -> h g xs
-
-{-------------------------------------------------------------------------------
-  Derived from application
--------------------------------------------------------------------------------}
-
--- | A generalized form of 'Control.Applicative.liftA',
--- which in turn is a generalized 'map'.
---
--- Takes a lifted function and applies it to every element of
--- a structure while preserving its shape.
---
--- /Specification:/
---
--- @
--- 'hliftA' f xs = 'hpure' ('fn' f) \` 'hap' \` xs
--- @
---
--- /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  :: (SingI 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'.
---
--- Takes a lifted binary function and uses it to combine two
--- structures of equal shape into a single structure.
---
--- It either takes two product structures to a product structure,
--- or one product and one sum structure to a sum structure.
---
--- /Specification:/
---
--- @
--- 'hliftA2' f xs ys = 'hpure' ('fn_2' f) \` 'hap' \` xs \` 'hap' \` ys
--- @
---
--- /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 :: (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
-
--- | A generalized form of 'Control.Applicative.liftA3',
--- which in turn is a generalized 'zipWith3'.
---
--- Takes a lifted ternary function and uses it to combine three
--- structures of equal shape into a single structure.
---
--- It either takes three product structures to a product structure,
--- or two product structures and one sum structure to a sum structure.
---
--- /Specification:/
---
--- @
--- 'hliftA3' f xs ys zs = 'hpure' ('fn_3' f) \` 'hap' \` xs \` 'hap' \` ys \` 'hap' \` zs
--- @
---
--- /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 :: (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
-
-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
-
--- | Variant of 'hliftA' that takes a constrained function.
---
--- /Specification:/
---
--- @
--- '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
-
--- | Variant of 'hcliftA2' that takes a constrained function.
---
--- /Specification:/
---
--- @
--- '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
-
--- | Variant of 'hcliftA3' that takes a constrained function.
---
--- /Specification:/
---
--- @
--- '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
-
-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
-
--- | Maps products to lists, and sums to identities.
-type family CollapseTo (h :: (k -> *) -> (l -> *)) :: * -> *
-
--- | A class for collapsing a heterogeneous structure into
--- a homogeneous one.
-class HCollapse (h :: (k -> *) -> (l -> *)) where
-
-  -- | Collapse a heterogeneous structure with homogeneous elements
-  -- into a homogeneous structure.
-  --
-  -- If a heterogeneous structure is instantiated to the constant
-  -- functor 'K', then it is in fact homogeneous. This function
-  -- maps such a value to a simpler Haskell datatype reflecting that.
-  -- An @'NS' ('K' a)@ contains a single @a@, and an @'NP' ('K' a)@ contains
-  -- a list of @a@s.
-  --
-  -- /Instances:/
-  --
-  -- @
-  -- 'hcollapse', 'Generics.SOP.NP.collapse_NP'  :: 'Generics.SOP.NP.NP'  ('K' a) xs  ->  [a]
-  -- 'hcollapse', 'Generics.SOP.NS.collapse_NS'  :: 'Generics.SOP.NS.NS'  ('K' a) xs  ->   a
-  -- 'hcollapse', 'Generics.SOP.NP.collapse_POP' :: 'Generics.SOP.NP.POP' ('K' a) xss -> [[a]]
-  -- 'hcollapse', 'Generics.SOP.NS.collapse_SOP' :: 'Generics.SOP.NP.SOP' ('K' a) xss ->  [a]
-  -- @
-  --
-  hcollapse :: SingI xs => h (K a) xs -> CollapseTo h a
-
--- | A generalization of 'Data.Traversable.sequenceA'.
-class HAp h => HSequence (h :: (k -> *) -> (l -> *)) where
-
-  -- | Corresponds to 'Data.Traversable.sequenceA'.
-  --
-  -- Lifts an applicative functor out of a structure.
-  --
-  -- /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' :: (SingI 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 = hsequence' . hliftA (Comp . fmap I)
+module Generics.SOP.Classes
+  (
+    module Data.SOP.Classes
+  ) where
 
--- | 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 = hsequence' . hliftA (Comp . fmap K . unK)
+import Data.SOP.Classes
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,83 +1,6 @@
-{-# LANGUAGE PolyKinds #-}
--- | Constraints for indexed datatypes.
---
--- This module contains code that helps to specify that all
--- elements of an indexed structure must satisfy a particular
--- constraint.
---
 module Generics.SOP.Constraint
-  ( module Generics.SOP.Constraint
-  , Constraint
+  (
+    module Data.SOP.Constraint
   ) where
 
-import GHC.Exts (Constraint)
-import Generics.SOP.Sing
-
--- | Require a constraint for every element of a list.
---
--- If you have a datatype that is indexed over a type-level
--- list, then you can use 'All' to indicate that all elements
--- of that type-level list must satisfy a given constraint.
---
--- /Example:/ The constraint
---
--- > All Eq '[ Int, Bool, Char ]
---
--- is equivalent to the constraint
---
--- > (Eq Int, Eq Bool, Eq Char)
---
--- /Example:/ A type signature such as
---
--- > f :: All Eq xs => NP I xs -> ...
---
--- 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)
-
--- | Require a constraint for every element of a list of lists.
---
--- If you have a datatype that is indexed over a type-level
--- list of lists, then you can use 'All2' to indicate that all
--- elements of the innert lists must satisfy a given constraint.
---
--- /Example:/ The constraint
---
--- > All2 Eq '[ '[ Int ], '[ Bool, Char ] ]
---
--- is equivalent to the constraint
---
--- > (Eq Int, Eq Bool, Eq Char)
---
--- /Example:/ A type signature such as
---
--- > f :: All2 Eq xss => SOP I xs -> ...
---
--- 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)
-
--- | 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
-
--- | A generalization of 'All' and 'All2'.
---
--- The family 'AllMap' 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
-
--- | Dictionary for a constraint for all elements of a type-level list.
---
--- A value of type @'AllDict' c xs@ captures the constraint @'All' c xs@.
---
-data AllDict (c :: k -> Constraint) (xs :: [k]) where
-  AllDictC :: (SingI xs, All c xs) => AllDict c xs
+import Data.SOP.Constraint
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,6 @@
+module Generics.SOP.Dict
+  (
+    module Data.SOP.Dict
+  ) where
+
+import Data.SOP.Dict
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
@@ -1,4 +1,5 @@
-{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE EmptyCase, PolyKinds, UndecidableInstances #-}
+{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
 -- | Derive @generics-sop@ boilerplate instances from GHC's 'GHC.Generic'.
 --
 -- The technique being used here is described in the following paper:
@@ -12,97 +13,79 @@
   , GFrom
   , GTo
   , GDatatypeInfo
+  , GDatatypeInfoOf
   , gfrom
   , gto
   , gdatatypeInfo
   ) where
 
-import Data.Proxy
+import Data.Proxy (Proxy (..))
+import Data.Kind (Type)
 import GHC.Generics as GHC
 import Generics.SOP.NP as SOP
 import Generics.SOP.NS as SOP
 import Generics.SOP.BasicFunctors as SOP
+import qualified Generics.SOP.Type.Metadata as SOP.T
 import Generics.SOP.Metadata as SOP
-import Generics.SOP.Sing
 
-type family ToSingleCode (a :: * -> *) :: *
-type instance ToSingleCode (K1 i a) = a
-
-type family ToProductCode (a :: * -> *) (xs :: [*]) :: [*]
-type instance ToProductCode (a :*: b)  xs = ToProductCode a (ToProductCode b xs)
-type instance ToProductCode U1         xs = xs
-type instance ToProductCode (M1 S c a) xs = ToSingleCode a ': xs
-
-type family ToSumCode (a :: * -> *) (xs :: [[*]]) :: [[*]]
-type instance ToSumCode (a :+: b)  xs = ToSumCode a (ToSumCode b xs)
-type instance ToSumCode V1         xs = xs
-type instance ToSumCode (M1 D c a) xs = ToSumCode a xs
-type instance ToSumCode (M1 C c a) xs = ToProductCode a '[] ': xs
-
-data InfoProxy (c :: *) (f :: * -> *) (x :: *) = InfoProxy
+type family ToSingleCode (a :: Type -> Type) :: Type
+type instance ToSingleCode (K1 _i a) = a
 
-class GDatatypeInfo' (a :: * -> *) where
-  gDatatypeInfo' :: Proxy a -> DatatypeInfo (ToSumCode a '[])
+type family ToProductCode (a :: Type -> Type) (xs :: [Type]) :: [Type]
+type instance ToProductCode (a :*: b)   xs = ToProductCode a (ToProductCode b xs)
+type instance ToProductCode U1          xs = xs
+type instance ToProductCode (M1 S _c a) xs = ToSingleCode a ': xs
 
-#if !(MIN_VERSION_base(4,7,0))
+type family ToSumCode (a :: Type -> Type) (xs :: [[Type]]) :: [[Type]]
+type instance ToSumCode (a :+: b)   xs = ToSumCode a (ToSumCode b xs)
+type instance ToSumCode V1          xs = xs
+type instance ToSumCode (M1 D _c a) xs = ToSumCode a xs
+type instance ToSumCode (M1 C _c a) xs = ToProductCode a '[] ': xs
 
--- | 'isNewtype' does not exist in "GHC.Generics" before GHC-7.8.
---
--- The only safe assumption to make is that it always returns 'False'.
---
-isNewtype :: Datatype d => t d (f :: * -> *) a -> Bool
-isNewtype _ = False
+data InfoProxy (c :: Meta) (f :: Type -> Type) (x :: Type) = InfoProxy
 
-#endif
+type family ToInfo (a :: Type -> Type) :: SOP.T.DatatypeInfo
+type instance ToInfo (M1 D (MetaData n m p False) a) =
+  SOP.T.ADT m n (ToSumInfo a '[]) (ToStrictnessInfoss a '[])
+type instance ToInfo (M1 D (MetaData n m p True) a) =
+  SOP.T.Newtype m n (ToSingleConstructorInfo a)
 
-instance (SingI (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
-              NewYes c -> Newtype (moduleName p) (datatypeName p) c
-              NewNo    -> adt ci -- should not happen
-       else adt ci
-    where
-     p :: InfoProxy c a x
-     p = InfoProxy
+type family ToStrictnessInfoss (a :: Type -> Type) (xss :: [[SOP.T.StrictnessInfo]]) :: [[SOP.T.StrictnessInfo]]
+type instance ToStrictnessInfoss (a :+: b)  xss = ToStrictnessInfoss a (ToStrictnessInfoss b xss)
+type instance ToStrictnessInfoss V1         xss = xss
+type instance ToStrictnessInfoss (M1 C _ a) xss = ToStrictnessInfos a '[] ': xss
 
-data IsNewtypeShape (xss :: [[*]]) where
-  NewYes :: ConstructorInfo '[x] -> IsNewtypeShape '[ '[x] ]
-  NewNo  :: IsNewtypeShape xss
+type family ToStrictnessInfos (a :: Type -> Type) (xs :: [SOP.T.StrictnessInfo]) :: [SOP.T.StrictnessInfo]
+type instance ToStrictnessInfos (a :*: b)  xs = ToStrictnessInfos a (ToStrictnessInfos b xs)
+type instance ToStrictnessInfos U1         xs = xs
+type instance ToStrictnessInfos (M1 S s a) xs = ToStrictnessInfo s ': xs
 
-isNewtypeShape :: Sing xss -> NP ConstructorInfo xss -> IsNewtypeShape xss
-isNewtypeShape SCons (x :* Nil) = go shape x
-  where
-    go :: Shape xs -> ConstructorInfo xs -> IsNewtypeShape '[ xs ]
-    go (ShapeCons ShapeNil) c   = NewYes c
-    go _                    _   = NewNo
-isNewtypeShape _     _          = NewNo
+type family ToStrictnessInfo (s :: Meta) :: SOP.T.StrictnessInfo
+type instance ToStrictnessInfo (MetaSel _ su ss ds) = 'SOP.T.StrictnessInfo su ss ds
 
-class GConstructorInfos (a :: * -> *) where
-  gConstructorInfos :: Proxy a -> NP ConstructorInfo xss -> NP ConstructorInfo (ToSumCode a xss)
+type family ToSumInfo (a :: Type -> Type) (xs :: [SOP.T.ConstructorInfo]) :: [SOP.T.ConstructorInfo]
+type instance ToSumInfo (a :+: b)  xs = ToSumInfo a (ToSumInfo b xs)
+type instance ToSumInfo V1         xs = xs
+type instance ToSumInfo (M1 C c a) xs = ToSingleConstructorInfo (M1 C c a) ': xs
 
-instance (GConstructorInfos a, GConstructorInfos b) => GConstructorInfos (a :+: b) where
-  gConstructorInfos _ xss = gConstructorInfos (Proxy :: Proxy a) (gConstructorInfos (Proxy :: Proxy b) xss)
+type family ToSingleConstructorInfo (a :: Type -> Type) :: SOP.T.ConstructorInfo
+type instance ToSingleConstructorInfo (M1 C (MetaCons n PrefixI False) a) =
+  SOP.T.Constructor n
+type instance ToSingleConstructorInfo (M1 C (MetaCons n (InfixI assoc fix) False) a) =
+  SOP.T.Infix n assoc fix
+type instance ToSingleConstructorInfo (M1 C (MetaCons n f True) a) =
+  SOP.T.Record n (ToProductInfo a '[])
 
-instance GConstructorInfos GHC.V1 where
-  gConstructorInfos _ xss = xss
+type family ToProductInfo (a :: Type -> Type) (xs :: [SOP.T.FieldInfo]) :: [SOP.T.FieldInfo]
+type instance ToProductInfo (a :*: b)  xs = ToProductInfo a (ToProductInfo b xs)
+type instance ToProductInfo U1         xs = xs
+type instance ToProductInfo (M1 S c a) xs = ToSingleInfo (M1 S c a) ': xs
 
-instance (Constructor c, GFieldInfos a, SingI (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
-        Prefix        -> Constructor (conName p) :* xss
-        GHC.Infix a f -> case (shape :: Shape (ToProductCode a '[])) of
-          ShapeCons (ShapeCons ShapeNil) -> SOP.Infix (conName p) a f :* xss
-          _                              -> Constructor (conName p) :* xss -- should not happen
-    where
-      p :: InfoProxy c a x
-      p = InfoProxy
+type family ToSingleInfo (a :: Type -> Type) :: SOP.T.FieldInfo
+type instance ToSingleInfo (M1 S (MetaSel (Just n) _su _ss _ds) a) = 'SOP.T.FieldInfo n
 
-class GFieldInfos (a :: * -> *) where
-  gFieldInfos :: Proxy a -> NP FieldInfo xs -> NP FieldInfo (ToProductCode a xs)
+class GFieldInfos (a :: Type -> Type) where
+  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)
@@ -116,13 +99,13 @@
       p :: InfoProxy c a x
       p = InfoProxy
 
-class GSingleFrom (a :: * -> *) where
+class GSingleFrom (a :: Type -> Type) where
   gSingleFrom :: a x -> ToSingleCode a
 
 instance GSingleFrom (K1 i a) where
   gSingleFrom (K1 a) = a
 
-class GProductFrom (a :: * -> *) where
+class GProductFrom (a :: Type -> Type) where
   gProductFrom :: a x -> NP I xs -> NP I (ToProductCode a xs)
 
 instance (GProductFrom a, GProductFrom b) => GProductFrom (a :*: b) where
@@ -134,13 +117,13 @@
 instance GSingleFrom a => GProductFrom (M1 S c a) where
   gProductFrom (M1 a) xs = I (gSingleFrom a) :* xs
 
-class GSingleTo (a :: * -> *) where
+class GSingleTo (a :: Type -> Type) where
   gSingleTo :: ToSingleCode a -> a x
 
 instance GSingleTo (K1 i a) where
   gSingleTo a = K1 a
 
-class GProductTo (a :: * -> *) where
+class GProductTo (a :: Type -> Type) where
   gProductTo :: NP I (ToProductCode a xs) -> (a x -> NP I xs -> r) -> r
 
 instance (GProductTo a, GProductTo b) => GProductTo (a :*: b) where
@@ -148,18 +131,24 @@
 
 instance GSingleTo a => GProductTo (M1 S c a) where
   gProductTo (SOP.I a :* xs) k = k (M1 (gSingleTo a)) xs
-  gProductTo _               _ = error "inaccessible"
 
 instance GProductTo U1 where
   gProductTo xs k = k U1 xs
 
 -- 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)
+class GSumFrom (a :: Type -> Type) where
+  gSumFrom :: a x -> proxy xss -> SOP I (ToSumCode a xss)
+  gSumSkip :: proxy a -> SOP I xss -> SOP I (ToSumCode a xss)
 
+instance GSumFrom V1 where
+  gSumFrom x = case x of {}
+  gSumSkip _ xss = xss
+
 instance (GSumFrom a, GSumFrom b) => GSumFrom (a :+: b) where
-  gSumFrom (L1 a) xss = gSumFrom a (gSumSkip (Proxy :: Proxy b) xss)
+  gSumFrom (L1 a) xss = gSumFrom a (toSumCodeProxy xss) where
+    toSumCodeProxy :: proxy xss -> Proxy (ToSumCode b xss)
+    toSumCodeProxy _ = Proxy
+
   gSumFrom (R1 b) xss = gSumSkip (Proxy :: Proxy a) (gSumFrom b xss)
 
   gSumSkip _ xss = gSumSkip (Proxy :: Proxy a) (gSumSkip (Proxy :: Proxy b) xss)
@@ -172,9 +161,12 @@
   gSumFrom (M1 a) _    = SOP (Z (gProductFrom a Nil))
   gSumSkip _ (SOP xss) = SOP (S xss)
 
-class GSumTo (a :: * -> *) where
+class GSumTo (a :: Type -> Type) where
   gSumTo :: SOP I (ToSumCode a xss) -> (a x -> r) -> (SOP I xss -> r) -> r
 
+instance GSumTo V1 where
+  gSumTo x _ k = k x
+
 instance (GSumTo a, GSumTo b) => GSumTo (a :+: b) where
   gSumTo xss s k = gSumTo xss (s . L1) (\ r -> gSumTo r (s . R1) k)
 
@@ -193,7 +185,7 @@
 -- This is the default definition for 'Generics.SOP.Code'.
 -- For more info, see 'Generics.SOP.Generic'.
 --
-type GCode (a :: *) = ToSumCode (GHC.Rep a) '[]
+type GCode (a :: Type) = ToSumCode (GHC.Rep a) '[]
 
 -- | Constraint for the class that computes 'gfrom'.
 type GFrom a = GSumFrom (GHC.Rep a)
@@ -202,8 +194,14 @@
 type GTo a = GSumTo (GHC.Rep a)
 
 -- | Constraint for the class that computes 'gdatatypeInfo'.
-type GDatatypeInfo a = GDatatypeInfo' (GHC.Rep a)
+type GDatatypeInfo a = SOP.T.DemoteDatatypeInfo (GDatatypeInfoOf a) (GCode a)
 
+-- | Compute the datatype info of a datatype.
+--
+-- @since 0.3.0.0
+--
+type GDatatypeInfoOf (a :: Type) = ToInfo (GHC.Rep a)
+
 -- | An automatically computed version of 'Generics.SOP.from'.
 --
 -- This requires that the type being converted has a
@@ -213,7 +211,7 @@
 -- For more info, see 'Generics.SOP.Generic'.
 --
 gfrom :: (GFrom a, GHC.Generic a) => a -> SOP I (GCode a)
-gfrom x = gSumFrom (GHC.from x) (error "gfrom: internal error" :: SOP.SOP SOP.I '[])
+gfrom x = gSumFrom (GHC.from x) (Proxy :: Proxy '[])
 
 -- | An automatically computed version of 'Generics.SOP.to'.
 --
@@ -224,7 +222,7 @@
 -- 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 ((\ _ -> error "inaccessible") :: SOP I '[] -> (GHC.Rep a) x))
+gto x = GHC.to (gSumTo x id ((\y -> case y of {}) :: SOP I '[] -> (GHC.Rep a) x))
 
 -- | An automatically computed version of 'Generics.SOP.datatypeInfo'.
 --
@@ -234,6 +232,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 _ = gDatatypeInfo' (Proxy :: Proxy (GHC.Rep a))
+gdatatypeInfo :: forall proxy a. (GDatatypeInfo a) => proxy a -> DatatypeInfo (GCode a)
+gdatatypeInfo _ = SOP.T.demoteDatatypeInfo (Proxy :: Proxy (GDatatypeInfoOf a))
 
diff --git a/src/Generics/SOP/Instances.hs b/src/Generics/SOP/Instances.hs
--- a/src/Generics/SOP/Instances.hs
+++ b/src/Generics/SOP/Instances.hs
@@ -1,6 +1,9 @@
+{-# LANGUAGE EmptyCase #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE UnboxedTuples #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
-{-# OPTIONS_GHC -fcontext-stack=50 #-}
+{-# OPTIONS_GHC -freduction-depth=100 #-}
+{-# OPTIONS_GHC -fno-warn-deprecations #-}
 -- | Instances for 'Generic' and 'HasMetadata'.
 --
 -- We define instances for datatypes from @generics-sop@ and
@@ -11,28 +14,62 @@
 --
 module Generics.SOP.Instances () where
 
+-- GHC versions and base versions:
+--
+-- 7.6.3:  4.6.0.1
+-- 7.8.3:  4.7.0.1
+-- 7.8.4:  4.7.0.2
+-- 7.10.3: 4.8.2.0
+-- 8.0.2:  4.9.1.0
+-- 8.2.2:  4.10.1.0
+-- 8.4.3:  4.11.1.0
+-- 8.6.1:  4.12.0.0
+
 import Control.Exception
 import Data.Char
 import Data.Complex
 import Data.Data
 import Data.Fixed
-import Data.Monoid
+import Data.Functor.Compose -- new
+import qualified Data.Functor.Const -- new
+import Data.Functor.Identity -- new
+import Data.Functor.Product -- new
+import Data.Functor.Sum -- new
+import Data.List.NonEmpty -- new
+import qualified Data.Monoid
 import Data.Ord
-#if !(MIN_VERSION_base(4,7,0))
-import Data.Proxy
-#endif
+import qualified Data.Semigroup -- new
 import Data.Version
+import Data.Void -- new
 import Foreign.C.Error
 import Foreign.C.Types
+#if MIN_VERSION_base(4,11,0)
+import GHC.ByteOrder -- new
+#endif
+import GHC.Conc -- new
+import GHC.ExecutionStack -- new
+import GHC.Exts -- new
+-- import GHC.Events -- platform-specific, omitted
+import GHC.Fingerprint -- new
+import GHC.Float -- new
+import qualified GHC.Generics -- new
+import GHC.IO.Buffer -- new
+import GHC.IO.Device -- new
+import GHC.IO.Encoding -- new
+import GHC.IO.Encoding.Failure -- new
+import GHC.IO.Exception -- new
+import GHC.IO.Handle -- new
+import GHC.RTS.Flags -- new
+import qualified GHC.Stack -- new
+import GHC.StaticPtr -- new
+import GHC.Stats -- new
 import System.Console.GetOpt
-import System.Exit
 import System.IO
-#if MIN_VERSION_base(4,7,0)
 import Text.Printf
-#endif
 import Text.Read.Lex
 
 import Generics.SOP.BasicFunctors
+import Generics.SOP.Classes
 import Generics.SOP.TH
 
 -- Types from Generics.SOP:
@@ -40,6 +77,7 @@
 deriveGeneric ''I
 deriveGeneric ''K
 deriveGeneric ''(:.:)
+deriveGeneric ''(-.->) -- new
 
 -- Cannot derive instances for Sing
 -- Cannot derive instances for Shape
@@ -96,6 +134,7 @@
 deriveGeneric ''NestedAtomically
 deriveGeneric ''BlockedIndefinitelyOnMVar
 deriveGeneric ''BlockedIndefinitelyOnSTM
+deriveGeneric ''AllocationLimitExceeded -- new
 deriveGeneric ''Deadlock
 deriveGeneric ''NoMethodError
 deriveGeneric ''PatternMatchFail
@@ -103,6 +142,7 @@
 deriveGeneric ''RecSelError
 deriveGeneric ''RecUpdError
 deriveGeneric ''ErrorCall
+deriveGeneric ''TypeError -- new
 deriveGeneric ''MaskingState
 
 -- From Data.Char:
@@ -118,16 +158,42 @@
 
 -- From Data.Fixed:
 deriveGeneric ''Fixed
+deriveGeneric ''E0
+deriveGeneric ''E1
+deriveGeneric ''E2
+deriveGeneric ''E3
+deriveGeneric ''E6
+deriveGeneric ''E9
+deriveGeneric ''E12
 
+-- From Data.Functor.Compose
+deriveGeneric ''Compose -- new
+
+-- From Data.Functor.Const
+deriveGeneric ''Data.Functor.Const.Const -- new
+
+-- From Data.Functor.Identity
+deriveGeneric ''Identity -- new
+
+-- From Data.Functor.Product
+deriveGeneric ''Product -- new
+
+-- From Data.Functor.Sum
+deriveGeneric ''Sum -- new
+
+-- From Data.List.NonEmpty
+deriveGeneric ''NonEmpty -- new
+
 -- From Data.Monoid:
-deriveGeneric ''Dual
-deriveGeneric ''Endo
-deriveGeneric ''All
-deriveGeneric ''Any
-deriveGeneric ''Sum
-deriveGeneric ''Product
-deriveGeneric ''First
-deriveGeneric ''Last
+deriveGeneric ''Data.Monoid.Dual
+deriveGeneric ''Data.Monoid.Endo
+deriveGeneric ''Data.Monoid.All
+deriveGeneric ''Data.Monoid.Any
+deriveGeneric ''Data.Monoid.Sum
+deriveGeneric ''Data.Monoid.Product
+deriveGeneric ''Data.Monoid.First
+deriveGeneric ''Data.Monoid.Last
+deriveGeneric ''Data.Monoid.Alt -- new
 
 -- From Data.Ord:
 deriveGeneric ''Down
@@ -135,9 +201,23 @@
 -- From Data.Proxy:
 deriveGeneric ''Proxy
 
+-- From Data.Semigroup:
+deriveGeneric ''Data.Semigroup.Min -- new
+deriveGeneric ''Data.Semigroup.Max -- new
+deriveGeneric ''Data.Semigroup.First -- new
+deriveGeneric ''Data.Semigroup.Last -- new
+deriveGeneric ''Data.Semigroup.WrappedMonoid -- new
+#if !MIN_VERSION_base(4,16,0)
+deriveGeneric ''Data.Semigroup.Option -- new
+#endif
+deriveGeneric ''Data.Semigroup.Arg -- new
+
 -- From Data.Version:
 deriveGeneric ''Version
 
+-- From Data.Void:
+deriveGeneric ''Void -- new
+
 -- From Foreign.C.Error:
 deriveGeneric ''Errno
 
@@ -168,6 +248,112 @@
 deriveGeneric ''CFloat
 deriveGeneric ''CDouble
 
+#if MIN_VERSION_base(4,11,0)
+-- From GHC.ByteOrder:
+deriveGeneric ''ByteOrder -- new
+#endif
+
+-- From GHC.Conc:
+deriveGeneric ''ThreadStatus -- new
+deriveGeneric ''BlockReason -- new
+
+-- From GHC.ExecutionStack:
+deriveGeneric ''Location -- new
+deriveGeneric ''SrcLoc -- new
+
+-- From GHC.Exts:
+deriveGeneric ''RuntimeRep -- new
+deriveGeneric ''VecCount -- new
+deriveGeneric ''VecElem -- new
+#if !MIN_VERSION_base(4,15,0)
+deriveGeneric ''SpecConstrAnnotation -- new
+#endif
+
+-- From GHC.Generics:
+deriveGeneric ''GHC.Generics.K1 -- new
+deriveGeneric ''GHC.Generics.U1 -- new
+deriveGeneric ''GHC.Generics.V1 -- new
+deriveGeneric ''GHC.Generics.Par1 -- new
+deriveGeneric ''GHC.Generics.M1 -- new
+deriveGeneric ''GHC.Generics.R -- new
+deriveGeneric ''GHC.Generics.S -- new
+deriveGeneric ''GHC.Generics.D -- new
+deriveGeneric ''GHC.Generics.C -- new
+deriveGeneric ''(GHC.Generics.:*:) -- new
+deriveGeneric ''(GHC.Generics.:+:) -- new
+deriveGeneric ''(GHC.Generics.:.:) -- new
+deriveGeneric ''GHC.Generics.Associativity -- new
+deriveGeneric ''GHC.Generics.DecidedStrictness -- new
+deriveGeneric ''GHC.Generics.SourceStrictness -- new
+deriveGeneric ''GHC.Generics.SourceUnpackedness -- new
+deriveGeneric ''GHC.Generics.Fixity -- new
+
+-- From GHC.IO.Buffer:
+deriveGeneric ''Buffer -- new
+deriveGeneric ''BufferState -- new
+
+-- From GHC.IO.Device:
+deriveGeneric ''IODeviceType -- new
+
+-- From GHC.IO.Encoding:
+deriveGeneric ''BufferCodec -- new
+deriveGeneric ''CodingProgress -- new
+
+-- From GHC.IO.Encoding.Failure:
+deriveGeneric ''CodingFailureMode -- new
+
+-- From GHC.Fingerprint
+deriveGeneric ''Fingerprint -- new
+
+-- From GHC.Float
+deriveGeneric ''FFFormat -- new
+
+-- From GHC.IO.Exception:
+#if MIN_VERSION_base(4,11,0)
+deriveGeneric ''FixIOException -- new
+deriveGeneric ''IOErrorType -- new
+#endif
+
+-- From GHC.IO.Handle:
+deriveGeneric ''HandlePosn -- new
+#if MIN_VERSION_base(4,10,0)
+deriveGeneric ''LockMode -- new
+#endif
+
+-- From GHC.RTS.Flags:
+deriveGeneric ''RTSFlags -- new
+deriveGeneric ''GiveGCStats -- new
+deriveGeneric ''GCFlags -- new
+deriveGeneric ''ConcFlags -- new
+deriveGeneric ''MiscFlags -- new
+deriveGeneric ''DebugFlags -- new
+deriveGeneric ''DoCostCentres -- new
+deriveGeneric ''CCFlags -- new
+deriveGeneric ''DoHeapProfile -- new
+deriveGeneric ''ProfFlags -- new
+deriveGeneric ''DoTrace -- new
+deriveGeneric ''TraceFlags -- new
+deriveGeneric ''TickyFlags -- new
+#if MIN_VERSION_base(4,10,0)
+deriveGeneric ''ParFlags -- new
+#endif
+
+-- From GHC.Stack:
+deriveGeneric ''GHC.Stack.SrcLoc -- new
+deriveGeneric ''GHC.Stack.CallStack -- new
+
+-- From GHC.StaticPtr:
+deriveGeneric ''StaticPtrInfo -- new
+
+-- From GHC.Stats:
+#if MIN_VERSION_base(4,10,0)
+deriveGeneric ''RTSStats -- new
+deriveGeneric ''GCDetails -- new
+#endif
+#if !MIN_VERSION_base(4,11,0)
+deriveGeneric ''GCStats -- new
+#endif
+
 -- From System.Console.GetOpt:
 
 deriveGeneric ''ArgOrder
@@ -188,19 +374,15 @@
 
 -- From Text.Printf:
 
-#if MIN_VERSION_base(4,7,0)
 deriveGeneric ''FieldFormat
 deriveGeneric ''FormatAdjustment
 deriveGeneric ''FormatSign
 deriveGeneric ''FormatParse
-#endif
 
 -- From Text.Read.Lex:
 
 deriveGeneric ''Lexeme
-#if MIN_VERSION_base(4,7,0)
 deriveGeneric ''Number
-#endif
 
 -- Abstract / primitive datatypes (we don't derive Generic for these):
 --
@@ -254,6 +436,13 @@
 -- Weak
 -- ReadP
 -- ReadPrec
+-- STM
+-- TVar
+-- Natural
+-- Event
+-- EventManager
+-- CostCentre
+-- CostCentreStack
 --
 -- Datatypes we cannot currently handle:
 --
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
@@ -15,13 +15,21 @@
   ( module Generics.SOP.Metadata
     -- * re-exports
   , Associativity(..)
+  , DecidedStrictness(..)
+  , SourceStrictness(..)
+  , SourceUnpackedness(..)
   ) where
 
-import GHC.Generics (Associativity(..))
+import Data.Kind (Type)
+import GHC.Generics
+  ( Associativity(..)
+  , DecidedStrictness(..)
+  , SourceStrictness(..)
+  , SourceUnpackedness(..)
+  )
 
 import Generics.SOP.Constraint
 import Generics.SOP.NP
-import Generics.SOP.Sing
 
 -- | Metadata for a datatype.
 --
@@ -33,36 +41,110 @@
 -- The constructor indicates whether the datatype has been declared using @newtype@
 -- or not.
 --
-data DatatypeInfo :: [[*]] -> * where
+data DatatypeInfo :: [[Type]] -> Type where
   -- Standard algebraic datatype
-  ADT     :: ModuleName -> DatatypeName -> NP ConstructorInfo xss -> DatatypeInfo xss
+  ADT     ::
+       ModuleName
+    -> DatatypeName
+    -> NP ConstructorInfo xss
+    -> POP StrictnessInfo xss
+    -> DatatypeInfo xss
   -- Newtype
-  Newtype :: ModuleName -> DatatypeName -> ConstructorInfo '[x]   -> DatatypeInfo '[ '[x] ]
+  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)
+-- | The module name where a datatype is defined.
+--
+-- @since 0.2.3.0
+--
+moduleName :: DatatypeInfo xss -> ModuleName
+moduleName (ADT name _ _ _) = name
+moduleName (Newtype name _ _) = name
 
--- | Metadata for a single constructors.
+-- | The name of a datatype (or newtype).
 --
+-- @since 0.2.3.0
+--
+datatypeName :: DatatypeInfo xss -> DatatypeName
+datatypeName (ADT _ name _ _) = name
+datatypeName (Newtype _ name _) = name
+
+-- | The constructor info for a datatype (or newtype).
+--
+-- @since 0.2.3.0
+--
+constructorInfo :: DatatypeInfo xss -> NP ConstructorInfo xss
+constructorInfo (ADT _ _ cs _) = cs
+constructorInfo (Newtype _ _ c) = c :* Nil
+
+deriving instance
+  ( All (Show `Compose` ConstructorInfo) xs
+  , All (Show `Compose` NP StrictnessInfo) xs
+  ) => Show (DatatypeInfo xs)
+deriving instance
+  ( All (Eq `Compose` ConstructorInfo) xs
+  , All (Eq `Compose` NP StrictnessInfo) xs
+  ) => Eq (DatatypeInfo xs)
+deriving instance
+  ( All (Eq `Compose` ConstructorInfo) xs
+  , All (Ord `Compose` ConstructorInfo) xs
+  , All (Eq `Compose` NP StrictnessInfo) xs
+  , All (Ord `Compose` NP StrictnessInfo) xs
+  ) => Ord (DatatypeInfo xs)
+
+-- | Metadata for a single constructor.
+--
 -- This is indexed by the product structure of the constructor components.
 --
-data ConstructorInfo :: [*] -> * where
+data ConstructorInfo :: [Type] -> Type 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)
+-- | The name of a constructor.
+--
+-- @since 0.2.3.0
+--
+constructorName :: ConstructorInfo xs -> ConstructorName
+constructorName (Constructor name) = name
+constructorName (Infix name _ _)   = name
+constructorName (Record name _)    = name
 
+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)
+
+-- | Metadata for strictness information of a field.
+--
+-- Indexed by the type of the field.
+--
+-- @since 0.4.0.0
+--
+data StrictnessInfo :: Type -> Type where
+  StrictnessInfo ::
+       SourceUnpackedness
+    -> SourceStrictness
+    -> DecidedStrictness
+    -> StrictnessInfo a
+  deriving (Show, Eq, Ord, Functor)
+
 -- | For records, this functor maps the component to its selector name.
-data FieldInfo :: * -> * where
+data FieldInfo :: Type -> Type where
   FieldInfo :: FieldName -> FieldInfo a
   deriving (Show, Eq, Ord, Functor)
+
+-- | The name of a field.
+--
+-- @since 0.2.3.0
+--
+fieldName :: FieldInfo a -> FieldName
+fieldName (FieldInfo n) = n
 
 -- | The name of a datatype.
 type DatatypeName    = String
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
@@ -1,376 +1,6 @@
-{-# LANGUAGE PolyKinds, StandaloneDeriving, UndecidableInstances #-}
--- | n-ary products (and products of products)
 module Generics.SOP.NP
-  ( -- * Datatypes
-    NP(..)
-  , POP(..)
-  , unPOP
-    -- * Constructing products
-  , pure_NP
-  , pure_POP
-  , cpure_NP
-  , cpure_POP
-    -- ** Construction from a list
-  , fromList
-    -- * Application
-  , ap_NP
-  , ap_POP
-    -- * Lifting / mapping
-  , liftA_NP
-  , liftA_POP
-  , liftA2_NP
-  , liftA2_POP
-  , liftA3_NP
-  , liftA3_POP
-  , cliftA_NP
-  , cliftA_POP
-  , cliftA2_NP
-  , cliftA2_POP
-    -- * Dealing with @'All' c@
-  , allDict_NP
-  , hcliftA'
-  , hcliftA2'
-  , hcliftA3'
-  , cliftA2'_NP
-    -- * Collapsing
-  , collapse_NP
-  , collapse_POP
-    -- * Sequencing
-  , sequence'_NP
-  , sequence'_POP
-  , sequence_NP
-  , sequence_POP
+  (
+    module Data.SOP.NP
   ) where
 
-import Control.Applicative
-import Data.Proxy (Proxy(..))
-
-import Generics.SOP.BasicFunctors
-import Generics.SOP.Classes
-import Generics.SOP.Constraint
-import Generics.SOP.Sing
-
--- | An n-ary product.
---
--- The product is parameterized by a type constructor @f@ and
--- indexed by a type-level list @xs@. The length of the list
--- determines the number of elements in the product, and if the
--- @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.
---
--- Two common instantiations of @f@ are the identity functor 'I'
--- and the constant functor 'K'. For 'I', the product becomes a
--- heterogeneous list, where the type-level list describes the
--- types of its components. For @'K' a@, the product becomes a
--- homogeneous list, where the contents of the type-level list are
--- ignored, but its length still specifies the number of elements.
---
--- In the context of the SOP approach to generic programming, an
--- n-ary product describes the structure of the arguments of a
--- single data constructor.
---
--- /Examples:/
---
--- > I 'x'    :* I True  :* Nil  ::  NP I       '[ Char, Bool ]
--- > K 0      :* K 1     :* Nil  ::  NP (K Int) '[ Char, Bool ]
--- > Just 'x' :* Nothing :* Nil  ::  NP Maybe   '[ Char, Bool ]
---
-data NP :: (k -> *) -> [k] -> * where
-  Nil  :: NP f '[]
-  (:*) :: f x -> NP f xs -> NP f (x ': xs)
-
-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)
-
--- | A product of products.
---
--- This is a 'newtype' for an 'NP' of an 'NP'. The elements of the
--- inner products are applications of the parameter @f@. The type
--- 'POP' is indexed by the list of lists that determines the lengths
--- of both the outer and all the inner products, as well as the types
--- of all the elements of the inner products.
---
--- A 'POP' is reminiscent of a two-dimensional table (but the inner
--- lists can all be of different length). In the context of the SOP
--- approach to generic programming, a 'POP' is useful to represent
--- information that is available for all arguments of all constructors
--- of a datatype.
---
-newtype POP (f :: (k -> *)) (xss :: [[k]]) = POP (NP (NP f) xss)
-  deriving (Show, Eq, Ord)
-
--- | 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
-
--- * Constructing products
-
--- | Specialization of 'hpure'.
---
--- The call @'pure_NP' x@ generates a product that contains 'x' in every
--- element position.
---
--- /Example:/
---
--- >>> pure_NP [] :: NP [] '[Char, Bool]
--- "" :* [] :* Nil
--- >>> 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
-  SNil   -> Nil
-  SCons  -> f :* pure_NP f
-
--- | Specialization of 'hpure'.
---
--- 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))
-
--- | 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
-  SNil   -> Nil
-  SCons  -> f :* cpure_NP p f
-
--- | Specialization of 'hcpure'.
---
--- 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))
-
-instance HPure NP where
-  hpure  = pure_NP
-  hcpure = cpure_NP
-
-instance HPure POP where
-  hpure  = pure_POP
-  hcpure = cpure_POP
-
--- ** Construction from a list
-
--- | Construct a homogeneous n-ary product from a normal Haskell list.
---
--- 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
-  where
-    go :: Sing 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 _     _      = Nothing
-
--- * Application
-
--- | Specialization of 'hap'.
---
--- Applies a product of (lifted) functions pointwise to a product of
--- suitable arguments.
---
-ap_NP :: NP (f -.-> g) xs -> NP f xs -> NP g xs
-ap_NP Nil           Nil        = Nil
-ap_NP (Fn f :* fs)  (x :* xs)  = f x :* ap_NP fs xs
-ap_NP _ _ = error "inaccessible"
-
--- | Specialization of 'hap'.
---
--- 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"
-
-type instance Prod NP  = NP
-type instance Prod POP = POP
-
-instance HAp NP  where hap = ap_NP
-instance HAp POP where hap = ap_POP
-
--- * Lifting / mapping
-
--- | Specialization of 'hliftA'.
-liftA_NP  :: SingI 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_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
--- | 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_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
--- | 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_NP  = hliftA3
-liftA3_POP = hliftA3
-
--- | 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
--- | 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_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
--- | 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_NP  = hcliftA2
-cliftA2_POP = hcliftA2
-
--- * Dealing with @'All' c@
-
--- | 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
-
--- | Lift a constrained function operating on a list-indexed structure
--- to a function on a list-of-list-indexed structure.
---
--- This is a variant of 'hcliftA'.
---
--- /Specification:/
---
--- @
--- 'hcliftA'' p f xs = 'hpure' ('fn_2' $ \\ 'AllDictC' -> f) \` 'hap' \` 'allDict_NP' p \` 'hap' \` xs
--- @
---
--- /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, 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
-
--- | 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
-
--- | 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
-
-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
-
--- | 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
-
-cliftA2'_NP = hcliftA2'
-
--- * Collapsing
-
--- | Specialization of 'hcollapse'.
---
--- /Example:/
---
--- >>> collapse_NP (K 1 :* K 2 :* K 3 :* Nil)
--- [1,2,3]
---
-collapse_NP  ::              NP  (K a) xs  ->  [a]
-
--- | Specialization of 'hcollapse'.
---
--- /Example:/
---
--- >>> collapse_POP (POP ((K 'a' :* Nil) :* (K 'b' :* K 'c' :* Nil) :* Nil) :: POP (K Char) '[ '[(a :: *)], '[b, c] ])
--- ["a", "bc"]
---
--- (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_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 = ([] :.: [])
-
-instance HCollapse NP  where hcollapse = collapse_NP
-instance HCollapse POP where hcollapse = Comp . collapse_POP
-
--- * Sequencing
-
--- | Specialization of 'hsequence''.
-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'_NP Nil         = pure Nil
-sequence'_NP (mx :* mxs) = (:*) <$> unComp mx <*> sequence'_NP mxs
-
-sequence'_POP = fmap POP . sequence'_NP . hliftA (Comp . sequence'_NP) . unPOP
-
-instance HSequence NP  where hsequence' = sequence'_NP
-instance HSequence POP where hsequence' = sequence'_POP
-
--- | Specialization of 'hsequence'.
---
--- /Example:/
---
--- >>> 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)
-
--- | Specialization of 'hsequence'.
---
--- /Example:/
---
--- >>> 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_NP   = hsequence
-sequence_POP  = hsequence
-
+import Data.SOP.NP
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,278 +1,6 @@
-{-# LANGUAGE PolyKinds, StandaloneDeriving, UndecidableInstances #-}
--- | n-ary sums (and sums of products)
 module Generics.SOP.NS
-  ( -- * Datatypes
-    NS(..)
-  , SOP(..)
-  , unSOP
-    -- * Constructing sums
-  , Injection
-  , injections
-  , shift
-  , apInjs_NP
-  , apInjs_POP
-    -- * Application
-  , ap_NS
-  , ap_SOP
-    -- * Lifting / mapping
-  , liftA_NS
-  , liftA_SOP
-  , liftA2_NS
-  , liftA2_SOP
-  , cliftA_NS
-  , cliftA_SOP
-  , cliftA2_NS
-  , cliftA2_SOP
-    -- * Dealing with @'All' c@
-  , cliftA2'_NS
-    -- * Collapsing
-  , collapse_NS
-  , collapse_SOP
-    -- * Sequencing
-  , sequence'_NS
-  , sequence'_SOP
-  , sequence_NS
-  , sequence_SOP
+  (
+    module Data.SOP.NS
   ) where
 
-import Control.Applicative
-import Data.Proxy (Proxy(..))
-
-import Generics.SOP.BasicFunctors
-import Generics.SOP.Classes
-import Generics.SOP.Constraint
-import Generics.SOP.NP
-import Generics.SOP.Sing
-
--- * Datatypes
-
--- | An n-ary sum.
---
--- The sum is parameterized by a type constructor @f@ and
--- indexed by a type-level list @xs@. The length of the list
--- determines the number of choices in the sum and if the
--- @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
--- natural numbers, i.e., 'Z' is for "zero", and 'S' is for
--- "successor". Chaining 'S' and 'Z' chooses the corresponding
--- component of the sum.
---
--- /Examples:/
---
--- > Z         :: f x -> NS f (x ': xs)
--- > S . Z     :: f y -> NS f (x ': y ': xs)
--- > S . S . Z :: f z -> NS f (x ': y ': z ': xs)
--- > ...
---
--- Note that empty sums (indexed by an empty list) have no
--- non-bottom elements.
---
--- Two common instantiations of @f@ are the identity functor 'I'
--- and the constant functor 'K'. For 'I', the sum becomes a
--- direct generalization of the 'Either' type to arbitrarily many
--- choices. For @'K' a@, the result is a homogeneous choice type,
--- where the contents of the type-level list are ignored, but its
--- length specifies the number of options.
---
--- In the context of the SOP approach to generic programming, an
--- n-ary sum describes the top-level structure of a datatype,
--- which is a choice between all of its constructors.
---
--- /Examples:/
---
--- > Z (I 'x')      :: NS I       '[ Char, Bool ]
--- > S (Z (I True)) :: NS I       '[ Char, Bool ]
--- > S (Z (I 1))    :: NS (K Int) '[ Char, Bool ]
---
-data NS :: (k -> *) -> [k] -> * where
-  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)
-
--- | A sum of products.
---
--- This is a 'newtype' for an 'NS' of an 'NP'. The elements of the
--- (inner) products are applications of the parameter @f@. The type
--- 'SOP' is indexed by the list of lists that determines the sizes
--- of both the (outer) sum and all the (inner) products, as well as
--- the types of all the elements of the inner products.
---
--- An @'SOP' 'I'@ reflects the structure of a normal Haskell datatype.
--- The sum structure represents the choice between the different
--- constructors, the product structure represents the arguments of
--- each constructor.
---
-newtype SOP (f :: (k -> *)) (xss :: [[k]]) = SOP (NS (NP f) xss)
-  deriving (Show, Eq, Ord)
-
--- | Unwrap a sum of products.
-unSOP :: SOP f xss -> NS (NP f) xss
-unSOP (SOP xss) = xss
-
--- * Constructing sums
-
--- | The type of injections into an n-ary sum.
---
--- If you expand the type synonyms and newtypes involved, you get
---
--- > Injection f xs a = (f -.-> K (NS f xs)) a ~= f a -> K (NS f xs) a ~= f a -> NS f xs
---
--- If we pick @a@ to be an element of @xs@, this indeed corresponds to an
--- injection into the sum.
---
-type Injection (f :: k -> *) (xs :: [k]) = f -.-> K (NS f xs)
-
--- | Compute all injections into an n-ary sum.
---
--- 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
-  SNil   -> Nil
-  SCons  -> fn (K . Z) :* liftA_NP shift injections
-
--- | Shift an injection.
---
--- Given an injection, return an injection into a sum that is one component larger.
---
-shift :: Injection f xs a -> Injection f (x ': xs) a
-shift (Fn f) = Fn $ K . S . unK . f
-
--- | Apply injections to a product.
---
--- Given a product containing all possible choices, produce a
--- list of sums by applying each injection to the appropriate
--- element.
---
--- /Example:/
---
--- >>> 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  = hcollapse . hap injections
-
--- | Apply injections to a product of product.
---
--- This operates on the outer product only. Given a product
--- containing all possible choices (that are products),
--- produce a list of sums (of products) by applying each
--- injection to the appropriate element.
---
--- /Example:/
---
--- >>> 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 = map SOP . apInjs_NP . unPOP
-
--- * Application
-
--- | 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 _ _ = 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"
-
-type instance Prod NS  = NP
-type instance Prod SOP = POP
-
-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
--- | Specialization of 'hliftA'.
-liftA_SOP :: SingI 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
--- | 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_NS  = hliftA2
-liftA2_SOP = hliftA2
-
--- | 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
--- | 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_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
--- | 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_NS  = hcliftA2
-cliftA2_SOP = hcliftA2
-
--- * 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
-
-cliftA2'_NS = hcliftA2'
-
--- * Collapsing
-
--- | Specialization of 'hcollapse'.
-collapse_NS  ::              NS  (K a) xs  ->   a
--- | Specialization of 'hcollapse'.
-collapse_SOP :: SingI 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 = []
-
-instance HCollapse NS  where hcollapse = I . 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)
-
--- | Specialization of 'hsequence''.
-sequence'_SOP :: (SingI 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
-
-sequence'_SOP = fmap SOP . sequence'_NS . hliftA (Comp . sequence'_NP) . unSOP
-
-instance HSequence NS  where hsequence' = sequence'_NS
-instance HSequence SOP where hsequence' = sequence'_SOP
-
--- | Specialization of 'hsequence'.
-sequence_NS  :: (SingI 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_NS   = hsequence
-sequence_SOP  = hsequence
-
+import Data.SOP.NS
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
@@ -1,104 +1,6 @@
-{-# LANGUAGE PolyKinds, StandaloneDeriving #-}
-#if MIN_VERSION_base(4,7,0)
-{-# LANGUAGE NoAutoDeriveTypeable #-}
-#endif
--- | Singleton types corresponding to type-level data structures.
---
--- The implementation is similar, but subtly different to that of the
--- @<https://hackage.haskell.org/package/singletons singletons>@ package.
--- See the <http://www.andres-loeh.de/TrueSumsOfProducts "True Sums of Products">
--- paper for details.
---
 module Generics.SOP.Sing
-  ( -- * Singletons
-    Sing(..)
-  , SingI(..)
-    -- ** Shape of type-level lists
-  , Shape(..)
-  , shape
-  , lengthSing
+  (
+    module Data.SOP.Sing
   ) 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'.
---
-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 '*'.
---
--- 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 '*'.
---
-data instance Sing (x :: *) where
-  SStar :: Sing (x :: *)
-
-deriving instance Show (Sing (x :: *))
-deriving instance Eq   (Sing (x :: *))
-deriving instance Ord  (Sing (x :: *))
-
--- | Implicit singleton.
---
--- A singleton can be used to reveal the structure of a type
--- argument that the function is quantified over.
---
--- The class 'SingI' should have instances that match the
--- family instances for 'Sing'.
---
-class SingI (a :: k) where
-  -- | Get hold of the explicit singleton (that one can then
-  -- pattern match on).
-  sing :: Sing a
-
-instance SingI (x :: *) where
-  sing = SStar
-
-instance SingI '[] where
-  sing = SNil
-
-instance (SingI x, SingI xs) => SingI (x ': xs) where
-  sing = SCons
-
--- * 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)
-
-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
-          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)
-  where
-    lengthShape :: forall xs'. Shape xs' -> Int
-    lengthShape ShapeNil      = 0
-    lengthShape (ShapeCons s) = 1 + lengthShape s
+import Data.SOP.Sing
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
@@ -1,17 +1,30 @@
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE TemplateHaskell #-}
 -- | Generate @generics-sop@ boilerplate instances using Template Haskell.
 module Generics.SOP.TH
   ( deriveGeneric
   , deriveGenericOnly
+  , deriveGenericSubst
+  , deriveGenericOnlySubst
+  , deriveGenericFunctions
+  , deriveMetadataValue
+  , deriveMetadataType
   ) where
 
-import Control.Monad (replicateM)
+import Control.Monad (join, replicateM, unless)
+import Data.List (foldl')
 import Data.Maybe (fromMaybe)
+import Data.Proxy
+
+-- importing in this order to avoid unused import warning
+import Language.Haskell.TH.Datatype.TyVarBndr
 import Language.Haskell.TH
-import Language.Haskell.TH.Syntax hiding (Infix)
+import Language.Haskell.TH.Datatype as TH
+import Language.Haskell.TH.Datatype.TyVarBndr
 
 import Generics.SOP.BasicFunctors
-import Generics.SOP.Metadata
+import qualified Generics.SOP.Metadata as SOP
+import qualified Generics.SOP.Type.Metadata as SOP.T
 import Generics.SOP.NP
 import Generics.SOP.NS
 import Generics.SOP.Universe
@@ -46,74 +59,201 @@
 -- >
 -- >   to (SOP    (Z (I x :* Nil)))         = Leaf x
 -- >   to (SOP (S (Z (I l :* I r :* Nil)))) = Node l r
--- >   to _ = error "unreachable" -- to avoid GHC warnings
+-- >   to (SOP (S (S x)))                   = x `seq` error "inaccessible"
 -- >
 -- > instance HasDatatypeInfo Tree where
--- >   datatypeInfo _ = ADT "Main" "Tree"
--- >     (Constructor "Leaf" :* Constructor "Node" :* Nil)
+-- >   type DatatypeInfoOf Tree =
+-- >     T.ADT "Main" "Tree"
+-- >       '[ T.Constructor "Leaf", T.Constructor "Node" ]
+-- >
+-- >   datatypeInfo _ =
+-- >     T.demoteDatatypeInfo (Proxy :: Proxy (DatatypeInfoOf Tree))
 --
 -- /Limitations:/ Generation does not work for GADTs, for
 -- datatypes that involve existential quantification, for
 -- datatypes with unboxed fields.
 --
 deriveGeneric :: Name -> Q [Dec]
-deriveGeneric n = do
-  dec <- reifyDec n
-  ds1 <- withDataDec dec deriveGenericForDataDec
-  ds2 <- withDataDec dec deriveMetadataForDataDec
-  return (ds1 ++ ds2)
+deriveGeneric n =
+  deriveGenericSubst n varT
 
 -- | Like 'deriveGeneric', but omit the 'HasDatatypeInfo' instance.
 deriveGenericOnly :: Name -> Q [Dec]
-deriveGenericOnly n = do
-  dec <- reifyDec n
-  withDataDec dec deriveMetadataForDataDec
+deriveGenericOnly n =
+  deriveGenericOnlySubst n varT
 
-deriveGenericForDataDec :: Bool -> Cxt -> Name -> [TyVarBndr] -> [Con] -> [Name] -> Q [Dec]
-deriveGenericForDataDec _isNewtype _cxt name bndrs cons _derivs = do
-  let typ = appTyVars name bndrs
-#if MIN_VERSION_template_haskell(2,9,0)
-  let codeSyn = tySynInstD ''Code $ tySynEqn [typ] (codeFor cons)
-#else
-  let codeSyn = tySynInstD ''Code [typ] (codeFor cons)
-#endif
+-- | Variant of 'deriveGeneric' that allows to restrict the type parameters.
+--
+-- Experimental function, exposed primarily for benchmarking.
+--
+deriveGenericSubst :: Name -> (Name -> Q Type) -> Q [Dec]
+deriveGenericSubst n f = do
+  dec <- reifyDatatype n
+  ds1 <- withDataDec dec (deriveGenericForDataDec  f)
+  ds2 <- withDataDec dec (deriveMetadataForDataDec f)
+  return (ds1 ++ ds2)
+
+-- | Variant of 'deriveGenericOnly' that allows to restrict the type parameters.
+--
+-- Experimental function, exposed primarily for benchmarking.
+--
+deriveGenericOnlySubst :: Name -> (Name -> Q Type) -> Q [Dec]
+deriveGenericOnlySubst n f = do
+  dec <- reifyDatatype n
+  withDataDec dec (deriveGenericForDataDec f)
+
+-- | 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 (SOP (S (S x)))                   = x `seq` error "inaccessible"
+--
+-- @since 0.2
+--
+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 <- reifyDatatype n
+  withDataDec dec $ \_variant _cxt name bndrs instTys cons -> do
+    let codeType = codeFor varT cons                     -- '[ '[Int], '[Tree, Tree] ]
+    let origType = appTysSubst varT name instTys         -- Tree
+    let repType  = [t| SOP I $(appTyVars varT codeName' bndrs) |] -- SOP I TreeCode
+    sequence
+      [ tySynD codeName' bndrs codeType                 -- type TreeCode = '[ '[Int], '[Tree, Tree] ]
+      , sigD fromName' [t| $origType -> $repType |]     -- fromTree :: Tree -> SOP I TreeCode
+      , embedding fromName' cons                        -- fromTree ... =
+      , sigD toName' [t| $repType -> $origType |]       -- 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 needs to be derived with 'deriveGenericFunctions'.
+--
+-- @since 0.2
+--
+deriveMetadataValue :: Name -> String -> String -> Q [Dec]
+deriveMetadataValue n codeName datatypeInfoName = do
+  let codeName'  = mkName codeName
+  let datatypeInfoName' = mkName datatypeInfoName
+  dec <- reifyDatatype n
+  withDataDec dec $ \variant _cxt name bndrs _instTys cons -> do
+    sequence [ sigD datatypeInfoName' [t| SOP.DatatypeInfo $(appTyVars varT codeName' bndrs) |] -- treeDatatypeInfo :: DatatypeInfo TreeCode
+             , funD datatypeInfoName' [clause [] (normalB $ metadata' variant name cons) []]    -- treeDatatypeInfo = ...
+             ]
+{-# DEPRECATED deriveMetadataValue "Use 'deriveMetadataType' and 'demoteDatatypeInfo' instead." #-}
+
+-- | Derive @DatatypeInfo@ type for the type.
+--
+-- /Example:/ If you say
+--
+-- > deriveMetadataType ''Tree "TreeDatatypeInfo"
+--
+-- then you get code that is equivalent to:
+--
+-- > type TreeDatatypeInfo =
+-- >   T.ADT "Main" "Tree"
+-- >     [ T.Constructor "Leaf", T.Constructor "Node" ]
+--
+-- @since 0.3.0.0
+--
+deriveMetadataType :: Name -> String -> Q [Dec]
+deriveMetadataType n datatypeInfoName = do
+  let datatypeInfoName' = mkName datatypeInfoName
+  dec <- reifyDatatype n
+  withDataDec dec $ \ variant _ctx name _bndrs _instTys cons ->
+    sequence
+      [ tySynD datatypeInfoName' [] (metadataType' variant name cons) ]
+
+deriveGenericForDataDec ::
+  (Name -> Q Type) -> DatatypeVariant -> Cxt -> Name -> [TyVarBndrVis] -> [Type] -> [TH.ConstructorInfo] -> Q [Dec]
+deriveGenericForDataDec f _variant _cxt name _bndrs instTys cons = do
+  let typ = appTysSubst f name instTys
+  deriveGenericForDataType f typ cons
+
+deriveGenericForDataType :: (Name -> Q Type) -> Q Type -> [TH.ConstructorInfo] -> Q [Dec]
+deriveGenericForDataType f typ cons = do
+  let codeSyn = tySynInstDCompat ''Generics.SOP.Universe.Code Nothing [typ] (codeFor f cons)
   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]
-deriveMetadataForDataDec isNewtype _cxt name bndrs cons _derivs = do
-  let typ = appTyVars name bndrs
+deriveMetadataForDataDec ::
+  (Name -> Q Type) -> DatatypeVariant -> Cxt -> Name -> [TyVarBndrVis] -> [Type] -> [TH.ConstructorInfo] -> Q [Dec]
+deriveMetadataForDataDec f variant _cxt name _bndrs instTys cons = do
+  let typ = appTysSubst f name instTys
+  deriveMetadataForDataType variant name typ cons
+
+deriveMetadataForDataType :: DatatypeVariant -> Name -> Q Type -> [TH.ConstructorInfo] -> Q [Dec]
+deriveMetadataForDataType variant name typ cons = do
   md   <- instanceD (cxt [])
             [t| HasDatatypeInfo $typ |]
-            [metadata isNewtype name cons]
+            [ metadataType typ variant name cons
+            , funD 'datatypeInfo
+                [ clause [wildP]
+                  (normalB [| SOP.T.demoteDatatypeInfo (Proxy :: Proxy (DatatypeInfoOf $typ)) |])
+                  []
+                ]
+            ]
+            -- [metadata variant name cons]
   return [md]
 
 {-------------------------------------------------------------------------------
   Computing the code for a data type
 -------------------------------------------------------------------------------}
 
-codeFor :: [Con] -> Q Type
-codeFor = promotedTypeList . map go
+codeFor :: (Name -> Q Type) -> [TH.ConstructorInfo] -> Q Type
+codeFor f = promotedTypeList . map go
   where
-    go :: Con -> Q Type
+    go :: TH.ConstructorInfo -> Q Type
     go c = do (_, ts) <- conInfo c
-              promotedTypeList ts
+              promotedTypeListSubst f ts
 
 {-------------------------------------------------------------------------------
   Computing the embedding/projection pair
 -------------------------------------------------------------------------------}
 
-embedding :: [Con] -> Q Dec
-embedding = funD 'from . go (\e -> [| Z $e |])
+embedding :: Name -> [TH.ConstructorInfo] -> Q Dec
+embedding fromName = funD fromName . go' (\e -> [| Z $e |])
   where
-    go :: (Q Exp -> Q Exp) -> [Con] -> [Q Clause]
+    go' :: (Q Exp -> Q Exp) -> [TH.ConstructorInfo] -> [Q Clause]
+    go' _ [] = (:[]) $ do
+      x <- newName "x"
+      clause [varP x] (normalB (caseE (varE x) [])) []
+    go' br cs = go br cs
+
+    go :: (Q Exp -> Q Exp) -> [TH.ConstructorInfo] -> [Q Clause]
     go _  []     = []
     go br (c:cs) = mkClause br c : go (\e -> [| S $(br e) |]) cs
 
-    mkClause :: (Q Exp -> Q Exp) -> Con -> Q Clause
+    mkClause :: (Q Exp -> Q Exp) -> TH.ConstructorInfo -> Q Clause
     mkClause br c = do
       (n, ts) <- conInfo c
       vars    <- replicateM (length ts) (newName "x")
@@ -121,66 +261,200 @@
              (normalB [| SOP $(br . npE . map (appE (conE 'I) . varE) $ vars) |])
              []
 
-projection :: [Con] -> Q Dec
-projection = funD 'to . go (\p -> conP 'Z [p])
+projection :: Name -> [TH.ConstructorInfo] -> Q Dec
+projection toName = funD toName . go'
   where
-    go :: (Q Pat -> Q Pat) -> [Con] -> [Q Clause]
-    go _ [] = [unreachable]
+    go' :: [TH.ConstructorInfo] -> [Q Clause]
+    go' [] = (:[]) $ do
+      x <- newName "x"
+      clause [varP x] (normalB (caseE (varE x) [])) []
+    go' cs = go id cs
+
+    go :: (Q Pat -> Q Pat) -> [TH.ConstructorInfo] -> [Q Clause]
+    go br [] = [mkUnreachableClause br]
     go br (c:cs) = mkClause br c : go (\p -> conP 'S [br p]) cs
 
-    mkClause :: (Q Pat -> Q Pat) -> Con -> Q Clause
+    -- Generates a final clause of the form:
+    --
+    --   to (S (... (S x))) = x `seq` error "inaccessible"
+    --
+    -- An equivalent way of achieving this would be:
+    --
+    --   to (S (... (S x))) = case x of {}
+    --
+    -- This, however, would require clients to enable the EmptyCase extension
+    -- in their own code, which is something which we have not previously
+    -- required. Therefore, we do not generate this code at the moment.
+    mkUnreachableClause :: (Q Pat -> Q Pat) -> Q Clause
+    mkUnreachableClause br = do
+      var <- newName "x"
+      clause [conP 'SOP [br (varP var)]]
+             (normalB [| $(varE var) `seq` error "inaccessible" |])
+             []
+
+    mkClause :: (Q Pat -> Q Pat) -> TH.ConstructorInfo -> Q Clause
     mkClause br c = do
       (n, ts) <- conInfo c
       vars    <- replicateM (length ts) (newName "x")
-      clause [conP 'SOP [br . npP . map (\v -> conP 'I [varP v]) $ vars]]
+      clause [conP 'SOP [br . conP 'Z . (:[]) . npP . map (\v -> conP 'I [varP v]) $ vars]]
              (normalB . appsE $ conE n : map varE vars)
              []
 
-unreachable :: Q Clause
-unreachable = clause [wildP]
-                     (normalB [| error "unreachable" |])
-                     []
-
 {-------------------------------------------------------------------------------
   Compute metadata
 -------------------------------------------------------------------------------}
 
-metadata :: Bool -> Name -> [Con] -> Q Dec
-metadata isNewtype typeName cs =
-    funD 'datatypeInfo [clause [wildP] (normalB md) []]
+metadataType :: Q Type -> DatatypeVariant -> Name -> [TH.ConstructorInfo] -> Q Dec
+metadataType typ variant typeName cs =
+  tySynInstDCompat ''DatatypeInfoOf Nothing [typ] (metadataType' variant typeName cs)
+
+-- | Derive term-level metadata.
+metadata' :: DatatypeVariant -> Name -> [TH.ConstructorInfo] -> Q Exp
+metadata' dataVariant typeName cs = md
   where
     md :: Q Exp
-    md | isNewtype = [| Newtype $(stringE (nameModule' typeName))
-                                $(stringE (nameBase typeName))
-                                $(mdCon (head cs))
-                      |]
-       | otherwise = [| ADT     $(stringE (nameModule' typeName))
-                                $(stringE (nameBase typeName))
-                                $(npE $ map mdCon cs)
-                      |]
+    md | isNewtypeVariant dataVariant
+       = [| SOP.Newtype $(stringE (nameModule' typeName))
+                        $(stringE (nameBase typeName))
+                        $(mdCon (head cs))
+          |]
 
+       | otherwise
+       = [| SOP.ADT     $(stringE (nameModule' typeName))
+                        $(stringE (nameBase typeName))
+                        $(npE $ map mdCon cs)
+                        $(popE $ map mdStrictness cs)
+          |]
 
-    mdCon :: Con -> Q Exp
-    mdCon (NormalC n _)   = [| Constructor $(stringE (nameBase n)) |]
-    mdCon (RecC n ts)     = [| Record      $(stringE (nameBase n))
-                                           $(npE (map mdField ts))
-                             |]
-    mdCon (InfixC _ n _)  = do
-      i <- reify n
-      case i of
-        DataConI _ _ _ (Fixity f a) ->
-                            [| Infix       $(stringE (nameBase n)) $(mdAssociativity a) f |]
-        _                -> fail "Strange infix operator"
-    mdCon (ForallC _ _ _) = fail "Existentials not supported"
+    mdStrictness :: TH.ConstructorInfo -> Q [Q Exp]
+    mdStrictness ci@(ConstructorInfo { constructorName       = n
+                                     , constructorStrictness = bs }) =
+      checkForGADTs ci $ mdConStrictness n bs
 
-    mdField :: VarStrictType -> Q Exp
-    mdField (n, _, _) = [| FieldInfo $(stringE (nameBase n)) |]
+    mdConStrictness :: Name -> [FieldStrictness] -> Q [Q Exp]
+    mdConStrictness n bs = do
+      dss <- reifyConStrictness n
+      return (zipWith (\ (FieldStrictness su ss) ds ->
+        [| SOP.StrictnessInfo
+          $(mdTHUnpackedness     su)
+          $(mdTHStrictness       ss)
+          $(mdDecidedStrictness  ds)
+        |]) bs dss)
 
+    mdCon :: TH.ConstructorInfo -> Q Exp
+    mdCon ci@(ConstructorInfo { constructorName    = n
+                              , constructorVariant = conVariant }) =
+      checkForGADTs ci $
+      case conVariant of
+        NormalConstructor    -> [| SOP.Constructor $(stringE (nameBase n)) |]
+        RecordConstructor ts -> [| SOP.Record      $(stringE (nameBase n))
+                                                   $(npE (map mdField ts))
+                                 |]
+        InfixConstructor     -> do
+          fixity <- reifyFixity n
+          case fromMaybe defaultFixity fixity of
+            Fixity f a ->       [| SOP.Infix       $(stringE (nameBase n))
+                                                   $(mdAssociativity a)
+                                                   f
+                                 |]
+
+
+    mdField :: Name -> Q Exp
+    mdField n = [| SOP.FieldInfo $(stringE (nameBase n)) |]
+
+    mdTHUnpackedness :: TH.Unpackedness -> Q Exp
+    mdTHUnpackedness UnspecifiedUnpackedness = [| SOP.NoSourceUnpackedness |]
+    mdTHUnpackedness NoUnpack                = [| SOP.SourceNoUnpack       |]
+    mdTHUnpackedness Unpack                  = [| SOP.SourceUnpack         |]
+
+    mdTHStrictness :: TH.Strictness -> Q Exp
+    mdTHStrictness UnspecifiedStrictness = [| SOP.NoSourceStrictness |]
+    mdTHStrictness Lazy                  = [| SOP.SourceLazy         |]
+    mdTHStrictness TH.Strict             = [| SOP.SourceStrict       |]
+
+    mdDecidedStrictness :: DecidedStrictness -> Q Exp
+    mdDecidedStrictness DecidedLazy   = [| SOP.DecidedLazy   |]
+    mdDecidedStrictness DecidedStrict = [| SOP.DecidedStrict |]
+    mdDecidedStrictness DecidedUnpack = [| SOP.DecidedUnpack |]
+
     mdAssociativity :: FixityDirection -> Q Exp
-    mdAssociativity InfixL = [| LeftAssociative  |]
-    mdAssociativity InfixR = [| RightAssociative |]
-    mdAssociativity InfixN = [| NotAssociative   |]
+    mdAssociativity InfixL = [| SOP.LeftAssociative  |]
+    mdAssociativity InfixR = [| SOP.RightAssociative |]
+    mdAssociativity InfixN = [| SOP.NotAssociative   |]
 
+-- | Derive type-level metadata.
+metadataType' :: DatatypeVariant -> Name -> [TH.ConstructorInfo] -> Q Type
+metadataType' dataVariant typeName cs = md
+  where
+    md :: Q Type
+    md | isNewtypeVariant dataVariant
+       = [t| 'SOP.T.Newtype $(stringT (nameModule' typeName))
+                            $(stringT (nameBase typeName))
+                            $(mdCon (head cs))
+           |]
+
+       | otherwise
+       = [t| 'SOP.T.ADT     $(stringT (nameModule' typeName))
+                            $(stringT (nameBase typeName))
+                            $(promotedTypeList $ map mdCon cs)
+                            $(promotedTypeListOfList $ map mdStrictness cs)
+           |]
+
+    mdStrictness :: TH.ConstructorInfo -> Q [Q Type]
+    mdStrictness ci@(ConstructorInfo { constructorName       = n
+                                     , constructorStrictness = bs }) =
+      checkForGADTs ci $ mdConStrictness n bs
+
+    mdConStrictness :: Name -> [FieldStrictness] -> Q [Q Type]
+    mdConStrictness n bs = do
+      dss <- reifyConStrictness n
+      return (zipWith (\ (FieldStrictness su ss) ds ->
+        [t| 'SOP.T.StrictnessInfo
+          $(mdTHUnpackedness     su)
+          $(mdTHStrictness       ss)
+          $(mdDecidedStrictness  ds)
+        |]) bs dss)
+
+    mdCon :: TH.ConstructorInfo -> Q Type
+    mdCon ci@(ConstructorInfo { constructorName    = n
+                              , constructorVariant = conVariant }) =
+      checkForGADTs ci $
+      case conVariant of
+        NormalConstructor    -> [t| 'SOP.T.Constructor $(stringT (nameBase n)) |]
+        RecordConstructor ts -> [t| 'SOP.T.Record      $(stringT (nameBase n))
+                                                       $(promotedTypeList (map mdField ts))
+                                  |]
+        InfixConstructor     -> do
+          fixity <- reifyFixity n
+          case fromMaybe defaultFixity fixity of
+            Fixity f a ->       [t| 'SOP.T.Infix       $(stringT (nameBase n))
+                                                       $(mdAssociativity a)
+                                                       $(natT f)
+                                  |]
+
+    mdField :: Name -> Q Type
+    mdField n = [t| 'SOP.T.FieldInfo $(stringT (nameBase n)) |]
+
+    mdTHUnpackedness :: TH.Unpackedness -> Q Type
+    mdTHUnpackedness UnspecifiedUnpackedness = [t| 'SOP.NoSourceUnpackedness |]
+    mdTHUnpackedness NoUnpack                = [t| 'SOP.SourceNoUnpack       |]
+    mdTHUnpackedness Unpack                  = [t| 'SOP.SourceUnpack         |]
+
+    mdTHStrictness :: TH.Strictness -> Q Type
+    mdTHStrictness UnspecifiedStrictness = [t| 'SOP.NoSourceStrictness |]
+    mdTHStrictness Lazy                  = [t| 'SOP.SourceLazy         |]
+    mdTHStrictness TH.Strict             = [t| 'SOP.SourceStrict       |]
+
+    mdDecidedStrictness :: DecidedStrictness -> Q Type
+    mdDecidedStrictness DecidedLazy   = [t| 'SOP.DecidedLazy   |]
+    mdDecidedStrictness DecidedStrict = [t| 'SOP.DecidedStrict |]
+    mdDecidedStrictness DecidedUnpack = [t| 'SOP.DecidedUnpack |]
+
+    mdAssociativity :: FixityDirection -> Q Type
+    mdAssociativity InfixL = [t| 'SOP.T.LeftAssociative  |]
+    mdAssociativity InfixR = [t| 'SOP.T.RightAssociative |]
+    mdAssociativity InfixN = [t| 'SOP.T.NotAssociative   |]
+
 nameModule' :: Name -> String
 nameModule' = fromMaybe "" . nameModule
 
@@ -199,6 +473,11 @@
 npE []     = [| Nil |]
 npE (e:es) = [| $e :* $(npE es) |]
 
+-- Construct a POP.
+popE :: [Q [Q Exp]] -> Q Exp
+popE ess =
+  [| POP $(npE (map (join . fmap npE) ess)) |]
+
 -- Like npE, but construct a pattern instead
 npP :: [Q Pat] -> Q Pat
 npP []     = conP 'Nil []
@@ -208,31 +487,125 @@
   Some auxiliary definitions for working with TH
 -------------------------------------------------------------------------------}
 
-conInfo :: Con -> Q (Name, [Q Type])
-conInfo (NormalC n ts) = return (n, map (return . (\(_, t)    -> t)) ts)
-conInfo (RecC    n ts) = return (n, map (return . (\(_, _, t) -> t)) ts)
-conInfo (InfixC (_, t) n (_, t')) = return (n, map return [t, t'])
-conInfo (ForallC _ _ _) = fail "Existentials not supported"
+conInfo :: TH.ConstructorInfo -> Q (Name, [Q Type])
+conInfo ci@(ConstructorInfo { constructorName    = n
+                            , constructorFields  = ts }) =
+  checkForGADTs ci $ return (n, map return ts)
 
+stringT :: String -> Q Type
+stringT = litT . strTyLit
+
+natT :: Int -> Q Type
+natT = litT . numTyLit . fromIntegral
+
 promotedTypeList :: [Q Type] -> Q Type
 promotedTypeList []     = promotedNilT
 promotedTypeList (t:ts) = [t| $promotedConsT $t $(promotedTypeList ts) |]
 
-appTyVars :: Name -> [TyVarBndr] -> Q Type
-appTyVars n = go (conT n)
+promotedTypeListOfList :: [Q [Q Type]] -> Q Type
+promotedTypeListOfList =
+  promotedTypeList . map (join . fmap promotedTypeList)
+
+promotedTypeListSubst :: (Name -> Q Type) -> [Q Type] -> Q Type
+promotedTypeListSubst _ []     = promotedNilT
+promotedTypeListSubst f (t:ts) = [t| $promotedConsT $(t >>= substType f) $(promotedTypeListSubst f ts) |]
+
+appsT :: Name -> [Q Type] -> Q Type
+appsT n = foldl' appT (conT n)
+
+appTyVars :: (Name -> Q Type) -> Name -> [TyVarBndrVis] -> Q Type
+appTyVars f n bndrs =
+  appsT n (map (f . tvName) bndrs)
+
+appTysSubst :: (Name -> Q Type) -> Name -> [Type] -> Q Type
+appTysSubst f n args =
+  appsT n (map (substType f . unSigType) args)
+
+unSigType :: Type -> Type
+unSigType (SigT t _) = t
+unSigType t          = t
+
+substType :: (Name -> Q Type) -> Type -> Q Type
+substType f = go
   where
-    go :: Q Type -> [TyVarBndr] -> Q Type
-    go t []                  = t
-    go t (PlainTV  v   : vs) = go [t| $t $(varT v) |] vs
-    go t (KindedTV v _ : vs) = go [t| $t $(varT v) |] vs
+    go (VarT n)     = f n
+    go (AppT t1 t2) = AppT <$> go t1 <*> go t2
+    go ListT        = return ListT
+    go (ConT n)     = return (ConT n)
+    go ArrowT       = return ArrowT
+    go (TupleT i)   = return (TupleT i)
+    go t            = return t -- error (show t)
+      -- TODO: This is incorrect, but we only need substitution to work
+      -- in simple cases for now. The reason is that substitution is normally
+      -- the identity, except if we use TH derivation for the tagged datatypes
+      -- in the benchmarking suite. So we can fall back on identity in all
+      -- but the cases we need for the benchmarking suite.
 
-reifyDec :: Name -> Q Dec
-reifyDec name =
-  do info <- reify name
-     case info of TyConI dec -> return dec
-                  _          -> fail "Info must be type declaration type."
+-- Process a DatatypeInfo using continuation-passing style.
+withDataDec :: TH.DatatypeInfo
+            -> (DatatypeVariant
+                   -- The variety of data type
+                   -- (@data@, @newtype@, @data instance@, or @newtype instance@)
+                -> Cxt
+                   -- The datatype context
+                -> Name
+                   -- The data type's name
+                -> [TyVarBndrVis]
+                   -- The datatype's type variable binders, both implicit and explicit.
+                   -- Examples:
+                   --
+                   -- - For `data Maybe a = Nothing | Just a`, the binders are
+                   --   [PlainTV a]
+                   -- - For `data Proxy (a :: k) = Proxy`, the binders are
+                   --   [PlainTV k, KindedTV a (VarT k)]
+                   -- - For `data instance DF Int (Maybe b) = DF b`, the binders are
+                   --   [PlainTV b]
+                -> [Type]
+                   -- For vanilla data types, these are the explicitly bound
+                   -- type variable binders, but in Type form.
+                   -- For data family instances, these are the type arguments.
+                   -- Examples:
+                   --
+                   -- - For `data Maybe a = Nothing | Just a`, the types are
+                   --   [VarT a]
+                   -- - For `data Proxy (a :: k) = Proxy`, the types are
+                   --   [SigT (VarT a) (VarT k)]
+                   -- - For `data instance DF Int (Maybe b) = DF b`, the binders are
+                   --   [ConT ''Int, ConT ''Maybe `AppT` VarT b]
+                -> [TH.ConstructorInfo]
+                   -- The data type's constructors
+                -> Q a)
+            -> Q a
+withDataDec (TH.DatatypeInfo { datatypeContext   = ctxt
+                             , datatypeName      = name
+                             , datatypeVars      = bndrs
+                             , datatypeInstTypes = instTypes
+                             , datatypeVariant   = variant
+                             , datatypeCons      = cons }) f =
+  checkForTypeData variant $
+  f variant ctxt name (changeTVFlags bndrReq bndrs) instTypes cons
 
-withDataDec :: Dec -> (Bool -> Cxt -> Name -> [TyVarBndr] -> [Con] -> [Name] -> Q a) -> Q a
-withDataDec (DataD    ctxt name bndrs cons derivs) f = f False ctxt name bndrs cons  derivs
-withDataDec (NewtypeD ctxt name bndrs con  derivs) f = f True  ctxt name bndrs [con] derivs
-withDataDec _ _ = fail "Can only derive labels for datatypes and newtypes."
+checkForTypeData :: DatatypeVariant -> Q a -> Q a
+checkForTypeData variant q = do
+  case variant of
+#if MIN_VERSION_th_abstraction(0,5,0)
+    TH.TypeData -> fail $ "`type data` declarations not supported"
+#endif
+    _ -> return ()
+  q
+
+checkForGADTs :: TH.ConstructorInfo -> Q a -> Q a
+checkForGADTs (ConstructorInfo { constructorVars    = exVars
+                               , constructorContext = exCxt }) q = do
+  unless (null exVars) $ fail "Existentials not supported"
+  unless (null exCxt)  $ fail "GADTs not supported"
+  q
+
+isNewtypeVariant :: DatatypeVariant -> Bool
+isNewtypeVariant Datatype        = False
+isNewtypeVariant DataInstance    = False
+isNewtypeVariant Newtype         = True
+isNewtypeVariant NewtypeInstance = True
+#if MIN_VERSION_th_abstraction(0,5,0)
+isNewtypeVariant TH.TypeData     = False
+#endif
diff --git a/src/Generics/SOP/Type/Metadata.hs b/src/Generics/SOP/Type/Metadata.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/SOP/Type/Metadata.hs
@@ -0,0 +1,376 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+-- | Type-level metadata
+--
+-- This module provides datatypes (to be used promoted) that can represent the
+-- metadata of Haskell datatypes on the type level.
+--
+-- We do not reuse the term-level metadata types, because these are GADTs that
+-- incorporate additional invariants. We could (at least in GHC 8) impose the
+-- same invariants on the type level as well, but some tests have revealed that
+-- the resulting type are rather inconvenient to work with.
+--
+-- So we use simple datatypes to represent the type-level metadata, even if
+-- this means that some invariants are not explicitly captured.
+--
+-- We establish a relation between the term- and type-level versions of the
+-- metadata by automatically computing the term-level version from the type-level
+-- version.
+--
+-- As we now have two versions of metadata (term-level and type-level)
+-- with very similar, yet slightly different datatype definitions, the names
+-- between the modules clash, and this module is recommended to be imported
+-- qualified when needed.
+--
+-- The interface exported by this module is still somewhat experimental.
+--
+-- @since 0.3.0.0
+--
+module Generics.SOP.Type.Metadata
+  ( module Generics.SOP.Type.Metadata
+    -- * re-exports
+  , Associativity(..)
+  ) where
+
+#if __GLASGOW_HASKELL__ <802
+import Data.Kind (Type)
+#endif
+import Data.Proxy (Proxy (..))
+import GHC.Generics
+  ( Associativity(..)
+  , DecidedStrictness(..)
+  , SourceStrictness(..)
+  , SourceUnpackedness(..)
+  )
+import GHC.Types
+import GHC.TypeLits
+
+import qualified Generics.SOP.Metadata as M
+import Generics.SOP.NP
+import Generics.SOP.Sing
+
+-- Regarding the CPP in the datatype definitions below:
+--
+-- We cannot promote type synonyms in GHC 7, so we
+-- use equivalent yet less descriptive definitions
+-- for the older GHCs.
+
+-- | Metadata for a datatype (to be used promoted).
+--
+-- A type of kind @'DatatypeInfo'@ contains meta-information about a datatype
+-- that is not contained in its code. This information consists
+-- primarily of the names of the datatype, its constructors, and possibly its
+-- record selectors.
+--
+-- The constructor indicates whether the datatype has been declared using @newtype@
+-- or not.
+--
+-- @since 0.3.0.0
+--
+data DatatypeInfo =
+    ADT ModuleName DatatypeName [ConstructorInfo] [[StrictnessInfo]]
+    -- ^ Standard algebraic datatype
+  | Newtype ModuleName DatatypeName ConstructorInfo
+    -- ^ Newtype
+
+-- | Metadata for a single constructors (to be used promoted).
+--
+-- @since 0.3.0.0
+--
+data ConstructorInfo =
+    Constructor ConstructorName
+    -- ^ Normal constructor
+  | Infix ConstructorName Associativity Fixity
+    -- ^ Infix constructor
+  | Record ConstructorName [FieldInfo]
+    -- ^ Record constructor
+
+-- | Strictness information for a single field (to be used promoted).
+--
+-- @since 0.4.0.0
+--
+data StrictnessInfo =
+    StrictnessInfo SourceUnpackedness SourceStrictness DecidedStrictness
+
+-- | Metadata for a single record field (to be used promoted).
+--
+-- @since 0.3.0.0
+--
+data FieldInfo =
+    FieldInfo FieldName
+
+-- | The name of a datatype.
+type DatatypeName    = Symbol
+
+-- | The name of a module.
+type ModuleName      = Symbol
+
+-- | The name of a data constructor.
+type ConstructorName = Symbol
+
+-- | The name of a field / record selector.
+type FieldName       = Symbol
+
+-- | The fixity of an infix constructor.
+type Fixity          = Nat
+
+-- Demotion
+--
+-- The following classes are concerned with computing the
+-- term-level metadata from the type-level metadata.
+
+-- | Class for computing term-level datatype information from
+-- type-level datatype information.
+--
+-- @since 0.3.0.0
+--
+class DemoteDatatypeInfo (x :: DatatypeInfo) (xss :: [[Type]]) where
+  -- | Given a proxy of some type-level datatype information,
+  -- return the corresponding term-level information.
+  --
+  -- @since 0.3.0.0
+  --
+  demoteDatatypeInfo :: proxy x -> M.DatatypeInfo xss
+
+instance
+     ( KnownSymbol m
+     , KnownSymbol d
+     , DemoteConstructorInfos cs xss
+     , DemoteStrictnessInfoss sss xss
+     )
+  => DemoteDatatypeInfo ('ADT m d cs sss) xss where
+  demoteDatatypeInfo _ =
+    M.ADT
+      (symbolVal (Proxy :: Proxy m))
+      (symbolVal (Proxy :: Proxy d))
+      (demoteConstructorInfos (Proxy :: Proxy cs))
+      (POP (demoteStrictnessInfoss (Proxy :: Proxy sss)))
+
+instance
+     (KnownSymbol m, KnownSymbol d, DemoteConstructorInfo c '[ x ])
+  => DemoteDatatypeInfo ('Newtype m d c) '[ '[ x ] ] where
+  demoteDatatypeInfo _ =
+    M.Newtype
+      (symbolVal (Proxy :: Proxy m))
+      (symbolVal (Proxy :: Proxy d))
+      (demoteConstructorInfo (Proxy :: Proxy c))
+
+-- | Class for computing term-level constructor information from
+-- type-level constructor information.
+--
+-- @since 0.3.0.0
+--
+class DemoteConstructorInfos (cs :: [ConstructorInfo]) (xss :: [[Type]]) where
+  -- | Given a proxy of some type-level constructor information,
+  -- return the corresponding term-level information as a product.
+  --
+  -- @since 0.3.0.0
+  --
+  demoteConstructorInfos :: proxy cs -> NP M.ConstructorInfo xss
+
+instance DemoteConstructorInfos '[] '[] where
+  demoteConstructorInfos _ = Nil
+
+instance
+     (DemoteConstructorInfo c xs, DemoteConstructorInfos cs xss)
+  => DemoteConstructorInfos (c ': cs) (xs ': xss) where
+  demoteConstructorInfos _ =
+    demoteConstructorInfo (Proxy :: Proxy c) :* demoteConstructorInfos (Proxy :: Proxy cs)
+
+-- | Class for computing term-level constructor information from
+-- type-level constructor information.
+--
+-- @since 0.3.0.0
+--
+class DemoteConstructorInfo (x :: ConstructorInfo) (xs :: [Type]) where
+  -- | Given a proxy of some type-level constructor information,
+  -- return the corresponding term-level information.
+  --
+  -- @since 0.3.0.0
+  --
+  demoteConstructorInfo :: proxy x -> M.ConstructorInfo xs
+
+instance (KnownSymbol s, SListI xs) => DemoteConstructorInfo ('Constructor s) xs where
+  demoteConstructorInfo _ = M.Constructor (symbolVal (Proxy :: Proxy s))
+
+instance
+     (KnownSymbol s, DemoteAssociativity a, KnownNat f)
+  => DemoteConstructorInfo ('Infix s a f) [y, z] where
+  demoteConstructorInfo _ =
+    M.Infix
+      (symbolVal (Proxy :: Proxy s))
+      (demoteAssociativity (Proxy :: Proxy a))
+      (fromInteger (natVal (Proxy :: Proxy f)))
+
+instance (KnownSymbol s, DemoteFieldInfos fs xs) => DemoteConstructorInfo ('Record s fs) xs where
+  demoteConstructorInfo _ =
+    M.Record (symbolVal (Proxy :: Proxy s)) (demoteFieldInfos (Proxy :: Proxy fs))
+
+
+class DemoteStrictnessInfoss (sss :: [[StrictnessInfo]]) (xss :: [[Type]]) where
+  demoteStrictnessInfoss :: proxy sss -> NP (NP M.StrictnessInfo) xss
+
+instance DemoteStrictnessInfoss '[] '[] where
+  demoteStrictnessInfoss _ = Nil
+
+instance
+     (DemoteStrictnessInfos ss xs, DemoteStrictnessInfoss sss xss)
+  => DemoteStrictnessInfoss (ss ': sss) (xs ': xss) where
+  demoteStrictnessInfoss _ =
+       demoteStrictnessInfos  (Proxy :: Proxy ss )
+    :* demoteStrictnessInfoss (Proxy :: Proxy sss)
+
+class DemoteStrictnessInfos (ss :: [StrictnessInfo]) (xs :: [Type]) where
+  demoteStrictnessInfos :: proxy ss -> NP M.StrictnessInfo xs
+
+instance DemoteStrictnessInfos '[] '[] where
+  demoteStrictnessInfos _ = Nil
+
+instance
+     (DemoteStrictnessInfo s x, DemoteStrictnessInfos ss xs)
+  => DemoteStrictnessInfos (s ': ss) (x ': xs) where
+  demoteStrictnessInfos _ =
+       demoteStrictnessInfo  (Proxy :: Proxy s )
+    :* demoteStrictnessInfos (Proxy :: Proxy ss)
+
+class DemoteStrictnessInfo (s :: StrictnessInfo) (x :: Type) where
+  demoteStrictnessInfo :: proxy s -> M.StrictnessInfo x
+
+instance
+     ( DemoteSourceUnpackedness su
+     , DemoteSourceStrictness   ss
+     , DemoteDecidedStrictness  ds
+     )
+  => DemoteStrictnessInfo ('StrictnessInfo su ss ds) x where
+  demoteStrictnessInfo _ =
+    M.StrictnessInfo
+      (demoteSourceUnpackedness (Proxy :: Proxy su))
+      (demoteSourceStrictness   (Proxy :: Proxy ss))
+      (demoteDecidedStrictness  (Proxy :: Proxy ds))
+
+-- | Class for computing term-level field information from
+-- type-level field information.
+--
+-- @since 0.3.0.0
+--
+class SListI xs => DemoteFieldInfos (fs :: [FieldInfo]) (xs :: [Type]) where
+  -- | Given a proxy of some type-level field information,
+  -- return the corresponding term-level information as a product.
+  --
+  -- @since 0.3.0.0
+  --
+  demoteFieldInfos :: proxy fs -> NP M.FieldInfo xs
+
+instance DemoteFieldInfos '[] '[] where
+  demoteFieldInfos _ = Nil
+
+instance
+     (DemoteFieldInfo f x, DemoteFieldInfos fs xs)
+  => DemoteFieldInfos (f ': fs) (x ': xs) where
+  demoteFieldInfos _ = demoteFieldInfo (Proxy :: Proxy f) :* demoteFieldInfos (Proxy :: Proxy fs)
+
+-- | Class for computing term-level field information from
+-- type-level field information.
+--
+-- @since 0.3.0.0
+--
+class DemoteFieldInfo (x :: FieldInfo) (a :: Type) where
+  -- | Given a proxy of some type-level field information,
+  -- return the corresponding term-level information.
+  --
+  -- @since 0.3.0.0
+  --
+  demoteFieldInfo :: proxy x -> M.FieldInfo a
+
+instance KnownSymbol s => DemoteFieldInfo ('FieldInfo s) a where
+  demoteFieldInfo _ = M.FieldInfo (symbolVal (Proxy :: Proxy s))
+
+-- | Class for computing term-level associativity information
+-- from type-level associativity information.
+--
+-- @since 0.3.0.0
+--
+class DemoteAssociativity (a :: Associativity) where
+  -- | Given a proxy of some type-level associativity information,
+  -- return the corresponding term-level information.
+  --
+  -- @since 0.3.0.0
+  --
+  demoteAssociativity :: proxy a -> M.Associativity
+
+instance DemoteAssociativity 'LeftAssociative where
+  demoteAssociativity _ = M.LeftAssociative
+
+instance DemoteAssociativity 'RightAssociative where
+  demoteAssociativity _ = M.RightAssociative
+
+instance DemoteAssociativity 'NotAssociative where
+  demoteAssociativity _ = M.NotAssociative
+
+-- | Class for computing term-level source unpackedness information
+-- from type-level source unpackedness information.
+--
+-- @since 0.4.0.0
+--
+class DemoteSourceUnpackedness (a :: SourceUnpackedness) where
+  -- | Given a proxy of some type-level source unpackedness information,
+  -- return the corresponding term-level information.
+  --
+  -- @since 0.4.0.0
+  --
+  demoteSourceUnpackedness :: proxy a -> M.SourceUnpackedness
+
+instance DemoteSourceUnpackedness 'NoSourceUnpackedness where
+  demoteSourceUnpackedness _ = M.NoSourceUnpackedness
+
+instance DemoteSourceUnpackedness 'SourceNoUnpack where
+  demoteSourceUnpackedness _ = M.SourceNoUnpack
+
+instance DemoteSourceUnpackedness 'SourceUnpack where
+  demoteSourceUnpackedness _ = M.SourceUnpack
+
+-- | Class for computing term-level source strictness information
+-- from type-level source strictness information.
+--
+-- @since 0.4.0.0
+--
+class DemoteSourceStrictness (a :: SourceStrictness) where
+  -- | Given a proxy of some type-level source strictness information,
+  -- return the corresponding term-level information.
+  --
+  -- @since 0.4.0.0
+  --
+  demoteSourceStrictness :: proxy a -> M.SourceStrictness
+
+instance DemoteSourceStrictness 'NoSourceStrictness where
+  demoteSourceStrictness _ = M.NoSourceStrictness
+
+instance DemoteSourceStrictness 'SourceLazy where
+  demoteSourceStrictness _ = M.SourceLazy
+
+instance DemoteSourceStrictness 'SourceStrict where
+  demoteSourceStrictness _ = M.SourceStrict
+
+-- | Class for computing term-level decided strictness information
+-- from type-level decided strictness information.
+--
+-- @since 0.4.0.0
+--
+class DemoteDecidedStrictness (a :: DecidedStrictness) where
+  -- | Given a proxy of some type-level source strictness information,
+  -- return the corresponding term-level information.
+  --
+  -- @since 0.4.0.0
+  --
+  demoteDecidedStrictness :: proxy a -> M.DecidedStrictness
+
+instance DemoteDecidedStrictness 'DecidedLazy where
+  demoteDecidedStrictness _ = M.DecidedLazy
+
+instance DemoteDecidedStrictness 'DecidedStrict where
+  demoteDecidedStrictness _ = M.DecidedStrict
+
+instance DemoteDecidedStrictness 'DecidedUnpack where
+  demoteDecidedStrictness _ = M.DecidedUnpack
+
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
@@ -1,16 +1,20 @@
 {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
 -- | Codes and interpretations
 module Generics.SOP.Universe where
 
+import Data.Kind (Type)
+import Data.Coerce (Coercible, coerce)
 import Data.Proxy
 import qualified GHC.Generics as GHC
 
 import Generics.SOP.BasicFunctors
 import Generics.SOP.Constraint
+import Generics.SOP.NP
 import Generics.SOP.NS
-import Generics.SOP.Sing
 import Generics.SOP.GGP
 import Generics.SOP.Metadata
+import qualified Generics.SOP.Type.Metadata as T
 
 -- | The (generic) representation of a datatype.
 --
@@ -24,7 +28,7 @@
 --
 -- The SOP approach to generic programming is based on viewing
 -- datatypes as a representation ('Rep') built from the sum of
--- products of its components. The components of are datatype
+-- products of its components. The components of a datatype
 -- are specified using the 'Code' type family.
 --
 -- The isomorphism between the original Haskell datatype and its
@@ -90,7 +94,7 @@
 --
 -- still holds.
 --
-class (SingI (Code a), All SingI (Code a)) => Generic (a :: *) where
+class (All SListI (Code a)) => Generic (a :: Type) where
   -- | The code of a datatype.
   --
   -- This is a list of lists of its components. The outer list contains
@@ -108,18 +112,20 @@
   -- >    , '[ Tree, Tree ]
   -- >    ]
   --
-  type Code a :: [[*]]
+  type Code a :: [[Type]]
   type Code a = GCode a
 
   -- | Converts from a value to its structural representation.
   from         :: a -> Rep a
-  default from :: (GFrom a, GHC.Generic a) => a -> SOP I (GCode a)
+  default from :: (GFrom a, GHC.Generic a, Rep a ~ SOP I (GCode a))
+               => a -> Rep a
   from = gfrom
 
   -- | Converts from a structural representation back to the
   -- original value.
   to         :: Rep a -> a
-  default to :: (GTo a, GHC.Generic a) => SOP I (GCode a) -> a
+  default to :: (GTo a, GHC.Generic a, Rep a ~ SOP I (GCode a))
+             => Rep a -> a
   to = gto
 
 -- | A class of datatypes that have associated metadata.
@@ -132,7 +138,135 @@
 -- rather derive the class instance automatically. See the documentation
 -- of 'Generic' for the options.
 --
-class HasDatatypeInfo a where
-  datatypeInfo         :: Proxy a -> DatatypeInfo (Code a)
-  default datatypeInfo :: (GDatatypeInfo a) => Proxy a -> DatatypeInfo (GCode a)
+class Generic a => HasDatatypeInfo a where
+  -- | Type-level datatype info
+  type DatatypeInfoOf a :: T.DatatypeInfo
+  type DatatypeInfoOf a = GDatatypeInfoOf a
+
+  -- | Term-level datatype info; by default, the term-level datatype info is produced
+  -- from the type-level info.
+  --
+  datatypeInfo         :: proxy a -> DatatypeInfo (Code a)
+  default datatypeInfo :: (GDatatypeInfo a, GCode a ~ Code a) => proxy a -> DatatypeInfo (Code a)
   datatypeInfo = gdatatypeInfo
+
+-- | Constraint that captures that a datatype is a product type,
+-- i.e., a type with a single constructor.
+--
+-- It also gives access to the code for the arguments of that
+-- constructor.
+--
+-- @since 0.3.1.0
+--
+type IsProductType (a :: Type) (xs :: [Type]) =
+  (Generic a, Code a ~ '[ xs ])
+
+-- | Direct access to the part of the code that is relevant
+-- for a product type.
+--
+-- @since 0.4.0.0
+--
+type ProductCode (a :: Type) =
+  Head (Code a)
+
+-- | Convert from a product type to its product representation.
+--
+-- @since 0.4.0.0
+--
+productTypeFrom :: IsProductType a xs => a -> NP I xs
+productTypeFrom = unZ . unSOP . from
+{-# INLINE productTypeFrom #-}
+
+-- | Convert a product representation to the original type.
+--
+-- @since 0.4.0.0
+--
+productTypeTo :: IsProductType a xs => NP I xs -> a
+productTypeTo = to . SOP . Z
+{-# INLINE productTypeTo #-}
+
+-- | Constraint that captures that a datatype is an enumeration type,
+-- i.e., none of the constructors have any arguments.
+--
+-- @since 0.3.1.0
+--
+type IsEnumType (a :: Type) =
+  (Generic a, All ((~) '[]) (Code a))
+
+-- | Convert from an enum type to its sum representation.
+--
+-- @since 0.4.0.0
+--
+enumTypeFrom :: IsEnumType a => a -> NS (K ()) (Code a)
+enumTypeFrom = map_NS (const (K ())) . unSOP . from
+{-# INLINE enumTypeFrom #-}
+
+-- | Convert a sum representation to ihe original type.
+--
+enumTypeTo :: IsEnumType a => NS (K ()) (Code a) -> a
+enumTypeTo = to . SOP . cmap_NS (Proxy :: Proxy ((~) '[])) (const Nil)
+{-# INLINE enumTypeTo #-}
+
+-- | Constraint that captures that a datatype is a single-constructor,
+-- single-field datatype. This always holds for newtype-defined types,
+-- but it can also be true for data-defined types.
+--
+-- The constraint also gives access to the type that is wrapped.
+--
+-- @since 0.3.1.0
+--
+type IsWrappedType (a :: Type) (x :: Type) =
+  (Generic a, Code a ~ '[ '[ x ] ])
+
+-- | Direct access to the part of the code that is relevant
+-- for wrapped types and newtypes.
+--
+-- @since 0.4.0.0
+--
+type WrappedCode (a :: Type) =
+  Head (Head (Code a))
+
+-- | Convert from a wrapped type to its inner type.
+--
+-- @since 0.4.0.0
+--
+wrappedTypeFrom :: IsWrappedType a x => a -> x
+wrappedTypeFrom = unI . hd . unZ . unSOP . from
+{-# INLINE wrappedTypeFrom #-}
+
+-- | Convert a type to a wrapped type.
+--
+-- @since 0.4.0.0
+--
+wrappedTypeTo :: IsWrappedType a x => x -> a
+wrappedTypeTo = to . SOP . Z . (:* Nil) . I
+{-# INLINE wrappedTypeTo #-}
+
+-- | Constraint that captures that a datatype is a newtype.
+-- This makes use of the fact that newtypes are always coercible
+-- to the type they wrap, whereas datatypes are not.
+--
+-- @since 0.3.1.0
+--
+type IsNewtype (a :: Type) (x :: Type) =
+  (IsWrappedType a x, Coercible a x)
+
+-- | Convert a newtype to its inner type.
+--
+-- This is a specialised synonym for 'coerce'.
+--
+-- @since 0.4.0.0
+--
+newtypeFrom :: IsNewtype a x => a -> x
+newtypeFrom = coerce
+{-# INLINE newtypeFrom #-}
+
+-- | Convert a type to a newtype.
+--
+-- This is a specialised synonym for 'coerce'.
+--
+-- @since 0.4.0.0
+--
+newtypeTo :: IsNewtype a x => x -> a
+newtypeTo = coerce
+{-# INLINE newtypeTo #-}
diff --git a/test/Example.hs b/test/Example.hs
new file mode 100644
--- /dev/null
+++ b/test/Example.hs
@@ -0,0 +1,240 @@
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE PolyKinds #-}
+{-# OPTIONS_GHC -fno-warn-deprecations #-}
+module Main (main, toTreeC, toDataFamC) where
+
+import qualified GHC.Generics as GHC
+import Generics.SOP
+import Generics.SOP.TH
+import qualified Generics.SOP.Type.Metadata as T
+
+import HTransExample
+
+-- 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)
+
+-- Generic enum, kind of
+class Enumerable a where
+  enum :: [a]
+
+genum :: (Generic a, All2 Enumerable (Code a)) => [a]
+genum =
+  fmap to genumS
+
+genumS :: (All SListI xss, All2 Enumerable xss) => [SOP I xss]
+genumS =
+  concat (fmap apInjs_POP
+    (hsequence (hcpure (Proxy :: Proxy Enumerable) enum)))
+
+-- GHC.Generics
+data Tree = Leaf Int | Node Tree Tree
+  deriving (GHC.Generic)
+
+tree :: Tree
+tree = Node (Leaf 1) (Leaf 2)
+
+abc :: ABC
+abc = B
+
+instance Generic Tree
+instance HasDatatypeInfo Tree
+
+data ABC = A | B | C
+  deriving (GHC.Generic)
+
+instance Generic ABC
+instance HasDatatypeInfo ABC
+
+data Void
+  deriving (GHC.Generic)
+
+instance Generic Void
+instance HasDatatypeInfo Void
+
+data family   DataFam a b c
+data instance DataFam Int (Maybe b) c = DF b c
+  deriving (GHC.Generic)
+
+dataFam :: DataFam Int (Maybe Int) Int
+dataFam = DF 1 2
+
+instance Generic (DataFam Int (Maybe b) c)
+instance HasDatatypeInfo (DataFam Int (Maybe b) c)
+
+instance Show Tree where
+  show = gshow
+
+instance Show ABC where
+  show = gshow
+
+instance Show Void where
+  show = gshow
+
+instance (Show b, Show c) => Show (DataFam Int (Maybe b) c) where
+  show = gshow
+
+instance Enumerable ABC where
+  enum = genum
+
+instance Enumerable Void where
+  enum = genum
+
+-- Template Haskell
+data TreeB = LeafB Int | NodeB TreeB TreeB
+
+treeB :: TreeB
+treeB = NodeB (LeafB 1) (LeafB 2)
+
+deriveGeneric ''TreeB
+
+data ABCB = AB | BB | CB
+
+abcB :: ABCB
+abcB = BB
+
+deriveGeneric ''ABCB
+
+data VoidB
+
+deriveGeneric ''VoidB
+
+data family   DataFamB a b c
+data instance DataFamB Int (Maybe b) c = DFB b c
+
+dataFamB :: DataFamB Int (Maybe Int) Int
+dataFamB = DFB 1 2
+
+deriveGeneric 'DFB
+
+instance Show TreeB where
+  show = gshow
+
+instance Show ABCB where
+  show = gshow
+
+instance Show VoidB where
+  show = gshow
+
+instance (Show b, Show c) => Show (DataFamB Int (Maybe b) c) where
+  show = gshow
+
+instance Enumerable ABCB where
+  enum = genum
+
+instance Enumerable VoidB where
+  enum = genum
+
+-- Orphan approach
+data TreeC = LeafC Int | NodeC TreeC TreeC
+
+treeC :: TreeC
+treeC = NodeC (LeafC 1) (LeafC 2)
+
+data ABCC = AC | BC | CC
+
+abcC :: ABCC
+abcC = BC
+
+data VoidC
+
+data family   DataFamC a b c
+data instance DataFamC Int (Maybe b) c = DFC b c
+
+dataFamC :: DataFamC Int (Maybe Int) Int
+dataFamC = DFC 1 2
+
+deriveGenericFunctions ''TreeC "TreeCCode" "fromTreeC" "toTreeC"
+deriveMetadataValue ''TreeC "TreeCCode" "treeDatatypeInfo"
+deriveMetadataType ''TreeC "TreeDatatypeInfo"
+
+deriveGenericFunctions ''ABCC "ABCCCode" "fromABCC" "toABCC"
+deriveMetadataValue ''ABCC "ABCCCode" "abcDatatypeInfo"
+deriveMetadataType ''ABCC "ABCDatatypeInfo"
+
+deriveGenericFunctions ''VoidC "VoidCCode" "fromVoidC" "toVoidC"
+deriveMetadataValue ''VoidC "VoidCCode" "voidDatatypeInfo"
+deriveMetadataType ''VoidC "VoidDatatypeInfo"
+
+deriveGenericFunctions 'DFC "DataFamCCode" "fromDataFamC" "toDataFamC"
+deriveMetadataValue 'DFC "DataFamCCode" "dataFamDatatypeInfo"
+deriveMetadataType 'DFC "DataFamDatatypeInfo"
+
+demotedTreeDatatypeInfo :: DatatypeInfo TreeCCode
+demotedTreeDatatypeInfo = T.demoteDatatypeInfo (Proxy :: Proxy TreeDatatypeInfo)
+
+demotedABCDatatypeInfo :: DatatypeInfo ABCCCode
+demotedABCDatatypeInfo = T.demoteDatatypeInfo (Proxy :: Proxy ABCDatatypeInfo)
+
+demotedVoidDatatypeInfo :: DatatypeInfo VoidCCode
+demotedVoidDatatypeInfo = T.demoteDatatypeInfo (Proxy :: Proxy VoidDatatypeInfo)
+
+demotedDataFamDatatypeInfo :: DatatypeInfo (DataFamCCode b c)
+demotedDataFamDatatypeInfo = T.demoteDatatypeInfo (Proxy :: Proxy DataFamDatatypeInfo)
+
+instance Show TreeC where
+  show x = gshowS (fromTreeC x)
+
+instance Show ABCC where
+  show x = gshowS (fromABCC x)
+
+instance Show VoidC where
+  show x = gshowS (fromVoidC x)
+
+instance (Show b, Show c) => Show (DataFamC Int (Maybe b) c) where
+  show x = gshowS (fromDataFamC x)
+
+instance Enumerable ABCC where
+  enum = fmap toABCC genumS
+
+instance Enumerable VoidC where
+  enum = fmap toVoidC genumS
+
+-- Tests
+main :: IO ()
+main = do
+  print tree
+  print abc
+  print dataFam
+  print $ (enum :: [ABC])
+  print $ (enum :: [Void])
+  print $ datatypeInfo (Proxy :: Proxy Tree)
+  print $ datatypeInfo (Proxy :: Proxy Void)
+  print $ datatypeInfo (Proxy :: Proxy (DataFam Int (Maybe Int) Int))
+  print treeB
+  print abcB
+  print dataFamB
+  print $ (enum :: [ABCB])
+  print $ (enum :: [VoidB])
+  print $ datatypeInfo (Proxy :: Proxy TreeB)
+  print $ datatypeInfo (Proxy :: Proxy VoidB)
+  print $ datatypeInfo (Proxy :: Proxy (DataFamB Int (Maybe Int) Int))
+  print treeC
+  print abcC
+  print dataFamC
+  print $ (enum :: [ABCC])
+  print $ (enum :: [VoidC])
+  print treeDatatypeInfo
+  print demotedTreeDatatypeInfo
+  print demotedDataFamDatatypeInfo
+  print (treeDatatypeInfo == demotedTreeDatatypeInfo)
+  print (abcDatatypeInfo == demotedABCDatatypeInfo)
+  print (voidDatatypeInfo == demotedVoidDatatypeInfo)
+  print (dataFamDatatypeInfo == demotedDataFamDatatypeInfo)
+  print $ convertFull tree
diff --git a/test/HTransExample.hs b/test/HTransExample.hs
new file mode 100644
--- /dev/null
+++ b/test/HTransExample.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+module HTransExample where
+
+import Generics.SOP
+
+class IsTupleTypeOf xs y | xs -> y where
+  toTuple :: NP I xs -> y
+  default toTuple :: (Generic y, Code y ~ '[ xs ]) => NP I xs -> y
+  toTuple = to . SOP . Z
+
+instance IsTupleTypeOf '[] ()
+instance IsTupleTypeOf '[x1] x1 where toTuple = unI . hd
+instance IsTupleTypeOf '[x1, x2] (x1, x2)
+instance IsTupleTypeOf '[x1, x2, x3] (x1, x2, x3)
+instance IsTupleTypeOf '[x1, x2, x3, x4] (x1, x2, x3, x4)
+
+convert :: (AllZip IsTupleTypeOf xss ys) => NS (NP I) xss -> NS I ys
+convert = htrans (Proxy :: Proxy IsTupleTypeOf) (I . toTuple)
+
+convertFull :: (Generic a, AllZip IsTupleTypeOf (Code a) ys) => a -> NS I ys
+convertFull = convert . unSOP . from