diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,241 @@
+# generic-lens
+
+[![Build
+Status](https://travis-ci.org/kcsongor/generic-lens.svg?branch=master)](https://travis-ci.org/kcsongor/generic-lens)
+
+Generically derive lenses and prisms for data types.
+
+Available on [Hackage](https://hackage.haskell.org/package/generic-lens)
+
+This package uses the GHC 8 `Generic` representation to derive various operations
+on data structures with lens interfaces, including structural subtype
+relationships between records and positional indexing into arbitrary product
+types.
+
+This is made possible by GHC 8's new Generics API, which provides metadata
+at the type-level (previously only value-level metadata was available).
+
+Examples can be found in the `examples` folder. This library makes heavy use of
+[Visible Type Applications](https://ghc.haskell.org/trac/ghc/wiki/TypeApplication).
+
+## Lenses
+
+### Record fields
+
+Record fields can be accessed by their label:
+
+```haskell
+data Person = Person { name :: String, age :: Int } deriving (Generic, Show)
+
+sally :: Person
+sally = Person "Sally" 25
+```
+
+```haskell
+>>> getField @"age" sally
+25
+
+>>> setField @"age" 26 sally
+Person {name = "Sally", age = 26}
+
+>>> sally ^. field @"name"
+"Sally"
+
+>>> sally & field @"name" .~ "Tamas"
+Person {name = "Tamas", age = 25}
+
+>>> sally ^. field @"pet"
+error:
+  • The type Person does not contain a field named "pet"
+```
+
+### Positional fields
+
+Fields can be accessed by their position in the data structure (index starting at 1):
+
+```haskell
+data Point = Point Int Int Int deriving (Generic, Show)
+data Polygon = Polygon Point Point Point deriving (Generic, Show)
+
+polygon :: Polygon
+polygon = Polygon (Point 1 5 3) (Point 2 4 2) (Point 5 7 (-2))
+```
+
+```haskell
+>>> getPosition @2 polygon
+Point 2 4 2
+
+>>> setPosition @1 (Point 26 5 3) polygon
+Polygon (Point 26 5 3) (Point 2 4 2) (Point 5 7 (-2))
+
+>>> polygon ^. position @1 . position @2
+5
+
+>>> polygon & position @3 . position @2 %~ (+10)
+Polygon (Point 1 5 3) (Point 2 4 2) (Point 5 17 (-2))
+
+>>> polygon ^. position @10
+error:
+  • The type Polygon does not contain a field at position 10
+```
+
+Since tuples are an instance of `Generic`, they also have positional lenses:
+
+```haskell
+>>> (("hello", True), 5) ^. position @1 . position @2
+True
+```
+
+### Typed fields
+
+Fields can be accessed by their type in the data structure, assuming that this
+type is unique:
+
+```haskell
+data Person = Person { name :: String, age :: Int } deriving (Generic, Show)
+data Point = Point Int Int Int deriving (Generic, Show)
+
+sally :: Person
+sally = Person "Sally" 25
+
+point :: Point
+point = Point 1 2 3
+```
+
+```haskell
+>>> getTyped @String sally
+"Sally"
+
+>>> setTyped @Int sally 26
+Person {name = "Sally", age = 26}
+
+>>> point ^. typed @Int
+error:
+  • The type Point contains multiple values of type Int; the choice of value is thus ambiguous
+
+>>> point & typed @String .~ "Point"
+error:
+  • The type Point does not contain a value of type [Char]
+```
+
+### Structural subtyping
+
+A record is a (structural) `subtype' of another, if its fields are a superset of
+those of the other.
+
+```haskell
+data Human = Human
+  { name    :: String
+  , age     :: Int
+  , address :: String
+  } deriving (Generic, Show)
+
+data Animal = Animal
+  { name    :: String
+  , age     :: Int
+  } deriving (Generic, Show)
+
+human :: Human
+human = Human {name = "Tunyasz", age = 50, address = "London"}
+```
+
+```haskell
+
+>>> upcast human :: Animal
+Animal {name = "Tunyasz", age = 50}
+
+-- 'smash' plug the smaller structure into the larger one
+>>> smash (Animal "dog" 10) human
+Human {name = "dog", age = 10, address = "London"}
+
+-- 'super' is a lens that focuses on a subrecord of a larger record:
+>>> human ^. super @Animal
+Animal {name = "Tunyasz", age = 50}
+```
+
+We can apply a function that operates on a supertype to the larger (subtype)
+structure, by focusing on the supertype first:
+
+```haskell
+growUp :: Animal -> Animal
+growUp (Animal name age) = Animal name (age + 50)
+
+>>> human & super @Animal %~ growUp
+Human {name = "Tunyasz", age = 60, address = "London"}
+```
+
+## Prisms
+
+### Named constructors
+
+Constructor components can be accessed using the constructor's name:
+
+```haskell
+type Name = String
+type Age  = Int
+
+data Dog = MkDog { name :: Name, age :: Age } deriving (Generic, Show)
+data Animal = Dog Dog | Cat (Name, Age) | Duck Age deriving (Generic, Show)
+
+shep = Dog (MkDog "Shep" 4)
+mog = Cat ("Mog", 5)
+donald = Duck 4
+```
+
+```haskell
+>>> shep ^? _Ctor @"Dog"
+Just (MkDog {name = "Shep", age = 4})
+
+>>> shep ^? _Ctor @"Cat"
+Nothing
+
+>>> mog ^? _Ctor @"Cat"
+Just ("Mog",5)
+
+>>> _Ctor @"Cat" # ("Garfield", 6) :: Animal
+Cat ("Garfield",6)
+
+>>> donald ^? _Ctor @"Giraffe"
+error:
+  • The type Animal does not contain a constructor named "Giraffe"
+```
+
+### Typed constructors
+
+Constructor components can be accessed using the component's type, assuming
+that this type is unique:
+
+```haskell
+type Name = String
+type Age  = Int
+
+data Dog = MkDog { name :: Name, age :: Age } deriving (Generic, Show)
+data Animal = Dog Dog | Cat (Name, Age) | Duck Age deriving (Generic, Show)
+
+shep = Dog (MkDog "Shep" 4)
+mog = Cat ("Mog", 5)
+donald = Duck 4
+```
+
+```haskell
+>>> mog ^? _Typed @Dog
+Nothing
+
+>>> shep ^? _Typed @Dog
+Just (MkDog {name = "Shep", age = 4})
+
+>>> donald ^? _Typed @Age
+Just 4
+
+>>> donald ^? _Typed @Float
+error:
+  • The type Animal does not contain a constructor whose field is of type Float
+
+>>> _Typed @Age # 6 :: Animal
+Duck 6
+```
+
+## Contributors
+
++ [Toby Shaw](https://github.com/TobyShaw)
++ [Will Jones](https://github.com/lunaris)
diff --git a/benchmarks/Bench.hs b/benchmarks/Bench.hs
new file mode 100644
--- /dev/null
+++ b/benchmarks/Bench.hs
@@ -0,0 +1,64 @@
+{-# LANGUAGE DataKinds        #-}
+{-# LANGUAGE DeriveGeneric    #-}
+{-# LANGUAGE NamedFieldPuns   #-}
+{-# LANGUAGE RankNTypes       #-}
+{-# LANGUAGE RecordWildCards  #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Main (main) where
+
+import Control.DeepSeq
+import Control.Lens.Operators
+import Control.Lens.Type
+import Control.Monad
+import Criterion.Main
+import Data.Generics.Product
+import GHC.Generics
+import Test.QuickCheck
+
+main :: IO ()
+main = defaultMain
+  [ env (arbitraryAnimalsOfLength 100) $ products 100
+  , env (arbitraryAnimalsOfLength 1000) $ products 1000
+  , env (arbitraryAnimalsOfLength 10000) $ products 10000
+  , env (arbitraryAnimalsOfLength 100000) $ products 100000
+  ]
+
+products :: Int -> [Animal] -> Benchmark
+products n as
+  = bgroup ("products/" ++ show n)
+      [ bench "generic-lens/get" (nf (const $ map (^. field @"name") as) ())
+      , bench "lens/get" (nf (const $ map (^. aName) as) ())
+      , bench "generic-lens/set" (nf (const $ map (\a -> a & field @"name" .~ "Name") as) ())
+      , bench "lens/set" (nf (const $ map (\a -> a & aName .~ "Name") as) ())
+      ]
+
+arbitraryAnimalsOfLength :: Int -> IO [Animal]
+arbitraryAnimalsOfLength n
+  = replicateM n (generate arbitrary)
+
+data Animal = Animal
+  { name :: String
+  , age  :: Int
+  , eats :: String
+  } deriving (Generic, Show)
+
+instance Arbitrary Animal where
+  arbitrary = Animal <$> arbitrary <*> arbitrary <*> arbitrary
+
+instance NFData Animal where
+  rnf Animal{..} = rnf name `seq` rnf age `seq` rnf eats
+
+aName :: Lens' Animal String
+aName f Animal{..}
+  = (\x -> Animal { name = x, age, eats }) <$> f name
+
+{-
+aAge :: Lens' Animal Int
+aAge f Animal{..}
+  = (\x -> Animal { name, age = x, eats }) <$> f age
+
+aEats :: Lens' Animal String
+aEats f Animal{..}
+  = (\x -> Animal { name, age, eats = x }) <$> f eats
+  -}
diff --git a/examples/Examples.hs b/examples/Examples.hs
new file mode 100644
--- /dev/null
+++ b/examples/Examples.hs
@@ -0,0 +1,43 @@
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE DeriveGeneric         #-}
+{-# LANGUAGE DuplicateRecordFields #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE TypeApplications      #-}
+{-# LANGUAGE UndecidableInstances  #-}
+
+{-# OPTIONS_GHC -fno-warn-unused-imports  #-}
+
+module Examples where
+
+import GHC.Generics
+import Data.Generics.Product
+--import Control.Lens
+
+data Animal = Animal
+  { name :: String
+  , age  :: Int
+  , eats :: String
+  } deriving (Show, Generic)
+
+data Human = Human
+  { name    :: String
+  , age     :: Int
+  , address :: String
+  , eats    :: String
+  } deriving (Show, Generic)
+
+data Living
+  = Animal' { name :: String, eats :: String, age :: Int }
+  | Human'  { name :: String, age :: Int, address :: String, eats :: String }
+  deriving (Show, Generic)
+
+toby :: Human
+toby = Human { name = "Toby", age = 10, address = "London", eats = "Bread" }
+
+growUp :: Animal -> Animal
+growUp (Animal n a _) = Animal n (a + 10) "raw meat"
+
+data MyRecord = MyRecord { field1 :: Int, field2 :: String } deriving Generic
+
+--g :: Subtype s MyRecord => s -> String
+--g s = s ^. super @MyRecord . label @"field2"
diff --git a/examples/StarWars.hs b/examples/StarWars.hs
--- a/examples/StarWars.hs
+++ b/examples/StarWars.hs
@@ -10,7 +10,6 @@
 module StarWars where
 
 import GHC.Generics
-import Data.Generics.Record
 import Data.Generics.Product
 
 data Episode = NEWHOPE | EMPIRE | JEDI
diff --git a/generic-lens.cabal b/generic-lens.cabal
--- a/generic-lens.cabal
+++ b/generic-lens.cabal
@@ -1,66 +1,77 @@
-name:                generic-lens
-
-version:             0.2.0.0
-
-synopsis:            Generic data-structure operations exposed as lenses.
-
-description:         This package uses the GHC 8 Generic representation to derive various operations on data structures with a lens interface, including structural subtype relationship between records and positional indexing into arbitrary product types.
-
-homepage:            https://github.com/kcsongor/generic-lens
-
-license:             BSD3
+name:                 generic-lens
+version:              0.3.0.0
+synopsis:             Generic data-structure operations exposed as lenses.
+description:          This package uses the GHC 8 Generic representation to derive various operations on data structures with a lens interface, including structural subtype relationship between records and positional indexing into arbitrary product types.
 
-license-file:        LICENSE
+homepage:             https://github.com/kcsongor/generic-lens
+license:              BSD3
+license-file:         LICENSE
+author:               Csongor Kiss
+maintainer:           kiss.csongor.kiss@gmail.com
+category:             Generics, Records, Lens
+build-type:           Simple
+cabal-version:        >= 1.10
 
-author:              Csongor Kiss
+extra-source-files:   ChangeLog.md
+                    , examples/StarWars.hs
+                    , examples/Examples.hs
+                    , README.md
 
-maintainer:          kiss.csongor.kiss@gmail.com
+library
+  exposed-modules:    Data.Generics.Product
+                    , Data.Generics.Product.Any
+                    , Data.Generics.Product.Fields
+                    , Data.Generics.Product.Positions
+                    , Data.Generics.Product.Subtype
+                    , Data.Generics.Product.Typed
+                    , Data.Generics.Sum
+                    , Data.Generics.Sum.Any
+                    , Data.Generics.Sum.Constructors
+                    , Data.Generics.Sum.Typed
 
-category:            Generics, Records, Lens
+                    , Data.Generics.Internal.Lens
 
-build-type:          Simple
+  other-modules:      Data.Generics.Internal.Families
+                    , Data.Generics.Internal.Families.Count
+                    , Data.Generics.Internal.Families.Has
+                    , Data.Generics.Internal.HList
 
--- Extra files to be distributed with the package, such as examples or a
--- README.
-extra-source-files:  ChangeLog.md
-                   , examples/StarWars.hs
+  build-depends:      base        >= 4.9 && <= 5.0
+                    , profunctors >= 5.0 && <= 6.0
 
--- Constraint on the version of Cabal needed to build this package.
-cabal-version:       >= 1.10
+  hs-source-dirs:     src
+  default-language:   Haskell2010
+  ghc-options:        -Wall
 
+source-repository head
+  type:               git
+  location:           https://github.com/kcsongor/generic-lens
 
-library
-  exposed-modules:   Data.Generics.Record
-                   , Data.Generics.Product
-                   , Data.Generics.Record.Subtype
-                   , Data.Generics.Record.HasField
-                   , Data.Generics.Product.HasFieldAt
-                   , Data.Generics.Internal.Lens
+test-suite generic-lens-test
+  type:               exitcode-stdio-1.0
+  hs-source-dirs:     test
+  main-is:            Spec.hs
 
-  other-modules:     Data.Generics.Record.Internal.Contains
+  build-depends:      base          >= 4.9 && <= 5.0
+                    , QuickCheck
+                    , hspec
+                    , generic-lens
 
-  other-extensions:  AllowAmbiguousTypes
-                   , DataKinds
-                   , FlexibleInstances
-                   , FunctionalDependencies
-                   , PolyKinds
-                   , Rank2Types
-                   , ScopedTypeVariables
-                   , TypeApplications
-                   , TypeFamilies
-                   , TypeOperators
-                   , UndecidableInstances
+  default-language:   Haskell2010
+  ghc-options:        -Wall
 
-  -- Other library packages from which modules are imported.
-  build-depends:     base >= 4.9 && <= 5.0
+benchmark generic-lens-bench
+  type:               exitcode-stdio-1.0
+  hs-source-dirs:     benchmarks
+  main-is:            Bench.hs
 
-  -- Directories containing source files.
-  hs-source-dirs:    src
+  build-depends:      generic-lens
 
-  -- Base language which the package is written in.
-  default-language:  Haskell2010
-  ghc-options:       -Wall
+                    , base        >= 4.9 && <= 5.0
+                    , QuickCheck
+                    , criterion
+                    , deepseq
+                    , lens
 
-source-repository head
-  type:     git
-  location: https://github.com/kcsongor/generic-lens
+  default-language:   Haskell2010
+  ghc-options:        -Wall
diff --git a/src/Data/Generics/Internal/Families.hs b/src/Data/Generics/Internal/Families.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Generics/Internal/Families.hs
@@ -0,0 +1,16 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Generics.Internal.Families
+-- Copyright   :  (C) 2017 Csongor Kiss
+-- License     :  BSD3
+-- Maintainer  :  Csongor Kiss <kiss.csongor.kiss@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-----------------------------------------------------------------------------
+module Data.Generics.Internal.Families
+  ( module Families
+  ) where
+
+import Data.Generics.Internal.Families.Count as Families
+import Data.Generics.Internal.Families.Has   as Families
diff --git a/src/Data/Generics/Internal/Families/Count.hs b/src/Data/Generics/Internal/Families/Count.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Generics/Internal/Families/Count.hs
@@ -0,0 +1,88 @@
+{-# LANGUAGE DataKinds            #-}
+{-# LANGUAGE PolyKinds            #-}
+{-# LANGUAGE TypeFamilies         #-}
+{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Generics.Internal.Families.Count
+-- Copyright   :  (C) 2017 Csongor Kiss
+-- License     :  BSD3
+-- Maintainer  :  Csongor Kiss <kiss.csongor.kiss@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-----------------------------------------------------------------------------
+module Data.Generics.Internal.Families.Count
+  ( CountTotalType
+  , CountPartialType
+  , Count (..)
+  ) where
+
+import GHC.Generics
+import GHC.TypeLits
+
+type family CountTotalType t f :: Count where
+  CountTotalType t (S1 _ (Rec0 t))
+    = 'One
+  CountTotalType t (l :*: r)
+    = CountTotalType t l <|> CountTotalType t r
+  CountTotalType t (l :+: r)
+    = CountTotalType t l <&> CountTotalType t r
+  CountTotalType t (S1 _ _)
+    = 'None
+  CountTotalType t (C1 _ f)
+    = CountTotalType t f
+  CountTotalType t (D1 _ f)
+    = CountTotalType t f
+  CountTotalType t (Rec0 _)
+    = 'None
+  CountTotalType t U1
+    = 'None
+  CountTotalType t V1
+    = 'None
+  CountTotalType t f
+    = TypeError
+        (     'ShowType f
+        ':<>: 'Text " is not a valid GHC.Generics representation type"
+        )
+
+type family CountPartialType t f :: Count where
+  CountPartialType t (S1 _ (Rec0 t))
+    = 'One
+  CountPartialType t (l :*: r)
+    = CountPartialType t l <|> CountPartialType t r
+  CountPartialType t (l :+: r)
+    = CountPartialType t l <|> CountPartialType t r
+  CountPartialType t (S1 _ _)
+    = 'None
+  CountPartialType t (C1 _ f)
+    = CountPartialType t f
+  CountPartialType t (D1 _ f)
+    = CountPartialType t f
+  CountPartialType t (Rec0 _)
+    = 'None
+  CountPartialType t U1
+    = 'None
+  CountPartialType t V1
+    = 'None
+  CountPartialType t f
+    = TypeError
+        (     'ShowType f
+        ':<>: 'Text " is not a valid GHC.Generics representation type"
+        )
+
+data Count
+  = None
+  | One
+  | Multiple
+
+type family (a :: Count) <|> (b :: Count) :: Count where
+  'None <|> b     = b
+  a     <|> 'None = a
+  a     <|> b     = 'Multiple
+
+type family (a :: Count) <&> (b :: Count) :: Count where
+  a <&> a = a
+  _ <&> _ = 'Multiple
diff --git a/src/Data/Generics/Internal/Families/Has.hs b/src/Data/Generics/Internal/Families/Has.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Generics/Internal/Families/Has.hs
@@ -0,0 +1,111 @@
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE UndecidableInstances  #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Generics.Internal.Families.Has
+-- Copyright   :  (C) 2017 Csongor Kiss
+-- License     :  BSD3
+-- Maintainer  :  Csongor Kiss <kiss.csongor.kiss@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-----------------------------------------------------------------------------
+module Data.Generics.Internal.Families.Has
+  ( HasTotalFieldP
+  , HasTotalTypeP
+  , HasPartialTypeP
+  , HasCtorP
+  ) where
+
+import Data.Type.Bool (type (||), type (&&))
+import GHC.Generics
+import GHC.TypeLits
+
+type family HasTotalFieldP (field :: Symbol) f :: Bool where
+  HasTotalFieldP field (S1 ('MetaSel ('Just field) _ _ _) _)
+    = 'True
+  HasTotalFieldP field (l :*: r)
+    = HasTotalFieldP field l || HasTotalFieldP field r
+  HasTotalFieldP field (l :+: r)
+    = HasTotalFieldP field l && HasTotalFieldP field r
+  HasTotalFieldP field (S1 _ _)
+    = 'False
+  HasTotalFieldP field (C1 _ f)
+    = HasTotalFieldP field f
+  HasTotalFieldP field (D1 _ f)
+    = HasTotalFieldP field f
+  HasTotalFieldP field (Rec0 _)
+    = 'False
+  HasTotalFieldP field U1
+    = 'False
+  HasTotalFieldP field V1
+    = 'False
+  HasTotalFieldP field f
+    = TypeError
+        (     'ShowType f
+        ':<>: 'Text " is not a valid GHC.Generics representation type"
+        )
+
+type family HasTotalTypeP a f :: Bool where
+  HasTotalTypeP t (S1 meta (Rec0 t))
+    = 'True
+  HasTotalTypeP t (l :*: r)
+    = HasTotalTypeP t l || HasTotalTypeP t r
+  HasTotalTypeP t (l :+: r)
+    = HasTotalTypeP t l && HasTotalTypeP t r
+  HasTotalTypeP t (S1 _ _)
+    = 'False
+  HasTotalTypeP t (C1 m f)
+    = HasTotalTypeP t f
+  HasTotalTypeP t (D1 m f)
+    = HasTotalTypeP t f
+  HasTotalTypeP t (Rec0 _)
+    = 'False
+  HasTotalTypeP t U1
+    = 'False
+  HasTotalTypeP t V1
+    = 'False
+  HasTotalTypeP t f
+    = TypeError
+        (     'ShowType f
+        ':<>: 'Text " is not a valid GHC.Generics representation type"
+        )
+
+type family HasPartialTypeP a f :: Bool where
+  HasPartialTypeP t (S1 meta (Rec0 t))
+    = 'True
+  HasPartialTypeP t (l :*: r)
+    = HasPartialTypeP t l || HasPartialTypeP t r
+  HasPartialTypeP t (l :+: r)
+    = HasPartialTypeP t l || HasPartialTypeP t r
+  HasPartialTypeP t (S1 _ _)
+    = 'False
+  HasPartialTypeP t (C1 m f)
+    = HasPartialTypeP t f
+  HasPartialTypeP t (D1 m f)
+    = HasPartialTypeP t f
+  HasPartialTypeP t (Rec0 _)
+    = 'False
+  HasPartialTypeP t U1
+    = 'False
+  HasPartialTypeP t V1
+    = 'False
+  HasPartialTypeP t f
+    = TypeError
+        (     'ShowType f
+        ':<>: 'Text " is not a valid GHC.Generics representation type"
+        )
+
+type family HasCtorP (ctor :: Symbol) f :: Bool where
+  HasCtorP ctor (C1 ('MetaCons ctor _ _) _)
+    = 'True
+  HasCtorP ctor (f :+: g)
+    = HasCtorP ctor f || HasCtorP ctor g
+  HasCtorP ctor (D1 m f)
+    = HasCtorP ctor f
+  HasCtorP ctor _
+    = 'False
diff --git a/src/Data/Generics/Internal/HList.hs b/src/Data/Generics/Internal/HList.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Generics/Internal/HList.hs
@@ -0,0 +1,173 @@
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE GADTs                  #-}
+{-# LANGUAGE KindSignatures         #-}
+{-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE PolyKinds              #-}
+{-# LANGUAGE ScopedTypeVariables    #-}
+{-# LANGUAGE TypeApplications       #-}
+{-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE TypeOperators          #-}
+{-# LANGUAGE UndecidableInstances   #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Generics.Internal.HList
+-- Copyright   :  (C) 2017 Csongor Kiss
+-- License     :  BSD3
+-- Maintainer  :  Csongor Kiss <kiss.csongor.kiss@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-----------------------------------------------------------------------------
+module Data.Generics.Internal.HList
+  ( (++)
+
+  , ListTuple (..)
+
+  , GCollectible (..)
+  ) where
+
+import Data.Kind
+import GHC.Generics
+
+data HList (xs :: [Type]) where
+  Nil  :: HList '[]
+  (:>) :: x -> HList xs -> HList (x ': xs)
+
+infixr 5 :>
+
+type family ((as :: [k]) ++ (bs :: [k])) :: [k] where
+  '[]       ++ bs = bs
+  (a ': as) ++ bs = a ': as ++ bs
+
+append :: HList as -> HList bs -> HList (as ++ bs)
+append Nil       ys = ys
+append (x :> xs) ys = x :> append xs ys
+
+head' :: HList (a ': as) -> a
+head' (x :> _) = x
+
+--------------------------------------------------------------------------------
+-- * Split HList
+
+class Splittable (as :: [Type]) (bs :: [Type]) (cs :: [Type]) | as bs -> cs, as cs -> bs where
+  split :: HList cs -> (HList as, HList bs)
+
+instance Splittable '[] bs bs where
+  split bs = (Nil, bs)
+
+instance Splittable as bs cs => Splittable (a ': as) bs (a ': cs) where
+  split (a :> as)
+    = (a :> as', bs)
+    where (as', bs) = split as
+
+--------------------------------------------------------------------------------
+-- * Convert tuples to/from HLists
+
+class ListTuple (tuple :: Type) (as :: [Type]) | as -> tuple where
+  tupleToList :: tuple -> HList as
+  listToTuple :: HList as -> tuple
+
+instance ListTuple () '[] where
+  tupleToList _ = Nil
+  listToTuple _ = ()
+
+instance ListTuple a '[a] where
+  tupleToList a
+    = a :> Nil
+  listToTuple (a :> Nil)
+    = a
+
+instance ListTuple (a, b) '[a, b] where
+  tupleToList (a, b)
+    = a :> b :> Nil
+  listToTuple (a :> b :> Nil)
+    = (a, b)
+
+instance ListTuple (a, b, c) '[a, b, c] where
+  tupleToList (a, b, c)
+    = a :> b :> c :> Nil
+  listToTuple (a :> b :> c :> Nil)
+    = (a, b, c)
+
+instance ListTuple (a, b, c, d) '[a, b, c, d] where
+  tupleToList (a, b, c, d)
+    = a :> b :> c :> d:> Nil
+  listToTuple (a :> b :> c :> d :> Nil)
+    = (a, b, c, d)
+
+instance ListTuple (a, b, c, d, e) '[a, b, c, d, e] where
+  tupleToList (a, b, c, d, e)
+    = a :> b :> c :> d:> e :> Nil
+  listToTuple (a :> b :> c :> d :> e :> Nil)
+    = (a, b, c, d, e)
+
+instance ListTuple (a, b, c, d, e, f) '[a, b, c, d, e, f] where
+  tupleToList (a, b, c, d, e, f)
+    = a :> b :> c :> d:> e :> f :> Nil
+  listToTuple (a :> b :> c :> d :> e :> f :> Nil)
+    = (a, b, c, d, e, f)
+
+instance ListTuple (a, b, c, d, e, f, g) '[a, b, c, d, e, f, g] where
+  tupleToList (a, b, c, d, e, f, g)
+    = a :> b :> c :> d:> e :> f :> g :> Nil
+  listToTuple (a :> b :> c :> d :> e :> f :> g :> Nil)
+    = (a, b, c, d, e, f, g)
+
+instance ListTuple (a, b, c, d, e, f, g, h) '[a, b, c, d, e, f, g, h] where
+  tupleToList (a, b, c, d, e, f, g, h)
+    = a :> b :> c :> d:> e :> f :> g :> h :> Nil
+  listToTuple (a :> b :> c :> d :> e :> f :> g :> h :> Nil)
+    = (a, b, c, d, e, f, g, h)
+
+instance ListTuple (a, b, c, d, e, f, g, h, j) '[a, b, c, d, e, f, g, h, j] where
+  tupleToList (a, b, c, d, e, f, g, h, j)
+    = a :> b :> c :> d:> e :> f :> g :> h :> j :> Nil
+  listToTuple (a :> b :> c :> d :> e :> f :> g :> h :> j :> Nil)
+    = (a, b, c, d, e, f, g, h, j)
+
+instance ListTuple (a, b, c, d, e, f, g, h, j, k) '[a, b, c, d, e, f, g, h, j, k] where
+  tupleToList (a, b, c, d, e, f, g, h, j, k)
+    = a :> b :> c :> d:> e :> f :> g :> h :> j :> k :> Nil
+  listToTuple (a :> b :> c :> d :> e :> f :> g :> h :> j :> k :> Nil)
+    = (a, b, c, d, e, f, g, h, j, k)
+
+instance ListTuple (a, b, c, d, e, f, g, h, j, k, l) '[a, b, c, d, e, f, g, h, j, k, l] where
+  tupleToList (a, b, c, d, e, f, g, h, j, k, l)
+    = a :> b :> c :> d:> e :> f :> g :> h :> j :> k :> l :> Nil
+  listToTuple (a :> b :> c :> d :> e :> f :> g :> h :> j :> k :> l :> Nil)
+    = (a, b, c, d, e, f, g, h, j, k, l)
+
+--------------------------------------------------------------------------------
+
+class GCollectible (f :: Type -> Type) (as :: [Type]) | f -> as where
+  gtoCollection   :: f x -> HList as
+  gfromCollection :: HList as -> f x
+
+instance
+  ( GCollectible l as
+  , GCollectible r bs
+  , cs ~ (as ++ bs)
+  , Splittable as bs cs
+  ) => GCollectible (l :*: r) cs where
+
+  gtoCollection (l :*: r)
+    = gtoCollection l `append` gtoCollection r
+
+  gfromCollection cs
+    = gfromCollection as :*: gfromCollection bs
+    where (as, bs) = split cs
+
+instance GCollectible (K1 R a) '[a] where
+  gtoCollection   = (:> Nil) . unK1
+  gfromCollection = K1 . head'
+
+instance GCollectible U1 '[] where
+  gtoCollection U1    = Nil
+  gfromCollection Nil = U1
+
+instance GCollectible f as => GCollectible (M1 m meta f) as where
+  gtoCollection   = gtoCollection . unM1
+  gfromCollection = M1 . gfromCollection
diff --git a/src/Data/Generics/Internal/Lens.hs b/src/Data/Generics/Internal/Lens.hs
--- a/src/Data/Generics/Internal/Lens.hs
+++ b/src/Data/Generics/Internal/Lens.hs
@@ -15,22 +15,22 @@
 -----------------------------------------------------------------------------
 module Data.Generics.Internal.Lens where
 
-import Control.Applicative  ( Const (..) )
-import GHC.Generics         ( (:*:) (..), Generic (..), M1 (..), Rep, (:+:) (..) )
-
--- | Identity functor
-newtype Identity a
-  = Identity { runIdentity :: a }
-
--- | Functor instance
-instance Functor Identity where
-  fmap f (Identity a)
-    = Identity (f a)
+import Control.Applicative   (Const(..))
+import Data.Functor.Identity (Identity(..))
+import Data.Profunctor       (Choice(right'), Profunctor(dimap))
+import GHC.Generics          ((:*:)(..), Generic(..), K1(..), M1(..), Rep, (:+:)(..))
 
 -- | Type alias for lens
 type Lens' s a
   = forall f. Functor f => (a -> f a) -> s -> f s
 
+-- | Type alias for prism
+type Prism' s a
+  = forall p f. (Choice p, Applicative f) => p a (f a) -> p s (f s)
+
+type Iso' s a
+  = forall p f. (Profunctor p, Functor f) => p a (f a) -> p s (f s)
+
 -- | Getting
 (^.) :: s -> ((a -> Const a a) -> s -> Const a s) -> a
 s ^. l = getConst (l Const s)
@@ -51,14 +51,43 @@
 second f (a :*: b)
   = fmap (a :*:) (f b)
 
-combine :: Lens' (s x) a -> Lens' (t x) a -> Lens' ((:+:) s t x) a
+left :: Prism' ((a :+: b) x) (a x)
+left = prism L1 $ \x -> case x of
+  L1 a -> Right a
+  R1 _ -> Left x
+
+right :: Prism' ((a :+: b) x) (b x)
+right = prism R1 $ \x -> case x of
+  L1 _ -> Left x
+  R1 a -> Right a
+
+combine :: Lens' (s x) a -> Lens' (t x) a -> Lens' ((s :+: t) x) a
 combine sa _ f (L1 s) = fmap (\a -> L1 (set sa a s)) (f (s ^. sa))
 combine _ ta f (R1 t) = fmap (\a -> R1 (set ta a t)) (f (t ^. ta))
 
+prism :: (a -> s) -> (s -> Either s a) -> Prism' s a
+prism bt seta = dimap seta (either pure (fmap bt)) . right'
+
 -- | A type and its generic representation are isomorphic
-repIso :: Generic a => Lens' a (Rep a x)
-repIso a = fmap to . a . from
+repIso :: Generic a => Iso' a (Rep a x)
+repIso = dimap from (fmap to)
 
 -- | 'M1' is just a wrapper around `f p`
-lensM :: Lens' (M1 i c f p) (f p)
-lensM f (M1 x) = fmap M1 (f x)
+mIso :: Iso' (M1 i c f p) (f p)
+mIso = dimap unM1 (fmap M1)
+
+kIso :: Iso' (K1 t a x) a
+kIso = dimap unK1 (fmap K1)
+
+sumIso :: Iso' ((a :+: b) x) (Either (a x) (b x))
+sumIso = dimap f (fmap t)
+  where f (L1 x) = Left x
+        f (R1 x) = Right x
+        t (Left x) = L1 x
+        t (Right x) = R1 x
+
+_Left :: Prism' (Either a c) a
+_Left = prism Left $ either Right (Left . Right)
+
+_Right :: Prism' (Either c a) a
+_Right = prism Right $ either (Left . Left) Right
diff --git a/src/Data/Generics/Product.hs b/src/Data/Generics/Product.hs
--- a/src/Data/Generics/Product.hs
+++ b/src/Data/Generics/Product.hs
@@ -1,6 +1,6 @@
 -----------------------------------------------------------------------------
 -- |
--- Module      :  Data.Generics.Record
+-- Module      :  Data.Generics.Product
 -- Copyright   :  (C) 2017 Csongor Kiss
 -- License     :  BSD3
 -- Maintainer  :  Csongor Kiss <kiss.csongor.kiss@gmail.com>
@@ -14,15 +14,21 @@
 -- be derived (see examples).
 --
 -----------------------------------------------------------------------------
+
 module Data.Generics.Product
-  (
-    -- * Magic lens
-    HasFieldAt  (..)
+  ( -- *Lenses
+    HasAny (..)
 
-    -- * Getter and setter
-  , getFieldAt
-  , setFieldAt
+  , HasField (..)
+  , HasPosition (..)
+  , HasType (..)
 
+    -- *Subtype relationships
+  , Subtype  (..)
   ) where
 
-import Data.Generics.Product.HasFieldAt
+import Data.Generics.Product.Any
+import Data.Generics.Product.Fields
+import Data.Generics.Product.Positions
+import Data.Generics.Product.Subtype
+import Data.Generics.Product.Typed
diff --git a/src/Data/Generics/Product/Any.hs b/src/Data/Generics/Product/Any.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Generics/Product/Any.hs
@@ -0,0 +1,75 @@
+{-# LANGUAGE AllowAmbiguousTypes    #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE PolyKinds              #-}
+{-# LANGUAGE ScopedTypeVariables    #-}
+{-# LANGUAGE TypeApplications       #-}
+{-# LANGUAGE UndecidableInstances   #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Generics.Product.Any
+-- Copyright   :  (C) 2017 Csongor Kiss
+-- License     :  BSD3
+-- Maintainer  :  Csongor Kiss <kiss.csongor.kiss@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Derive a variety of lenses generically.
+--
+-----------------------------------------------------------------------------
+
+module Data.Generics.Product.Any
+  ( -- *Lenses
+    --
+    --  $example
+    HasAny (..)
+  ) where
+
+import Data.Generics.Internal.Lens
+import Data.Generics.Product.Fields
+import Data.Generics.Product.Positions
+import Data.Generics.Product.Typed
+
+--  $example
+--  @
+--    module Example where
+--
+--    import Data.Generics.Product
+--    import GHC.Generics
+--
+--    data Human = Human
+--      { name    :: String
+--      , age     :: Int
+--      , address :: String
+--      }
+--      deriving (Generic, Show)
+--
+--    human :: Human
+--    human = Human \"Tunyasz\" 50 \"London\"
+--  @
+
+-- |Records that have generic lenses.
+class HasAny (sel :: k) a s | s sel k -> a where
+  -- |A lens that focuses on a part of a product as identified by some
+  --  selector. Currently supported selectors are field names, positions and
+  --  unique types. Compatible with the lens package's 'Control.Lens.Lens'
+  --  type.
+  --
+  --  >>> human ^. the @Int
+  --  50
+  --  >>> human ^. the @"name"
+  --  "Tunyasz"
+  --  >>> human ^. the @3
+  --  "London"
+  the :: Lens' s a
+
+instance HasPosition i a s => HasAny i a s where
+  the = position @i
+
+instance HasField field a s => HasAny field a s where
+  the = field @field
+
+instance HasType a s => HasAny a a s where
+  the = typed @a
diff --git a/src/Data/Generics/Product/Fields.hs b/src/Data/Generics/Product/Fields.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Generics/Product/Fields.hs
@@ -0,0 +1,141 @@
+{-# LANGUAGE AllowAmbiguousTypes    #-}
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE KindSignatures         #-}
+{-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE ScopedTypeVariables    #-}
+{-# LANGUAGE TypeApplications       #-}
+{-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE TypeOperators          #-}
+{-# LANGUAGE UndecidableInstances   #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Generics.Product.Fields
+-- Copyright   :  (C) 2017 Csongor Kiss
+-- License     :  BSD3
+-- Maintainer  :  Csongor Kiss <kiss.csongor.kiss@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Derive record field getters and setters generically.
+--
+-----------------------------------------------------------------------------
+
+module Data.Generics.Product.Fields
+  ( -- *Lenses
+
+    --  $example
+    HasField (..)
+
+    -- *Internals
+  , GHasField (..)
+  ) where
+
+import Data.Generics.Internal.Families
+import Data.Generics.Internal.Lens
+
+import Data.Kind
+import GHC.Generics
+import GHC.TypeLits
+
+--  $example
+--  @
+--    module Example where
+--
+--    import Data.Generics.Product
+--    import GHC.Generics
+--
+--    data Human = Human
+--      { name    :: String
+--      , age     :: Int
+--      , address :: String
+--      }
+--      deriving (Generic, Show)
+--
+--    human :: Human
+--    human = Human \"Tunyasz\" 50 \"London\"
+--  @
+
+-- |Records that have a field with a given name.
+class HasField (field :: Symbol) a s | s field -> a where
+  -- |A lens that focuses on a field with a given name. Compatible with the
+  --  lens package's 'Control.Lens.Lens' type.
+  --
+  --  >>> human ^. field @"age"
+  --  50
+  --  >>> human & field @"name" .~ "Tamas"
+  --  Human {name = "Tamas", age = 50, address = "London"}
+  field :: Lens' s a
+  field f s
+    = fmap (flip (setField @field) s) (f (getField @field s))
+
+  -- |Get 'field'
+  --
+  -- >>> getField @"name" human
+  -- "Tunyasz"
+  getField :: s -> a
+  getField s = s ^. field @field
+
+  -- |Set 'field'
+  --
+  -- >>> setField @"age" (setField @"name" "Tamas" human) 30
+  -- Human {name = "Tamas", age = 30, address = "London"}
+  setField :: a -> s -> s
+  setField = set (field @field)
+
+  {-# MINIMAL field | setField, getField #-}
+
+instance
+  ( Generic s
+  , ErrorUnless field s (HasTotalFieldP field (Rep s))
+  , GHasField field (Rep s) a
+  ) => HasField field a s where
+
+  field = repIso . gfield @field
+
+type family ErrorUnless (field :: Symbol) (s :: Type) (contains :: Bool) :: Constraint where
+  ErrorUnless field s 'False
+    = TypeError
+        (     'Text "The type "
+        ':<>: 'ShowType s
+        ':<>: 'Text " does not contain a field named "
+        ':<>: 'ShowType field
+        )
+
+  ErrorUnless _ _ 'True
+    = ()
+
+-- |As 'HasField' but over generic representations as defined by
+--  "GHC.Generics".
+class GHasField (field :: Symbol) (f :: Type -> Type) a | field f -> a where
+  gfield :: Lens' (f x) a
+
+instance GProductHasField field l r a (HasTotalFieldP field l)
+      => GHasField field (l :*: r) a where
+
+  gfield = gproductField @field @_ @_ @_ @(HasTotalFieldP field l)
+
+instance (GHasField field l a, GHasField field r a)
+      =>  GHasField field (l :+: r) a where
+
+  gfield = combine (gfield @field @l) (gfield @field @r)
+
+instance GHasField field (S1 ('MetaSel ('Just field) upkd str infstr) (Rec0 a)) a where
+  gfield = mIso . kIso
+
+instance GHasField field f a => GHasField field (M1 D meta f) a where
+  gfield = mIso . gfield @field
+
+instance GHasField field f a => GHasField field (M1 C meta f) a where
+  gfield = mIso . gfield @field
+
+class GProductHasField (field :: Symbol) l r a (left :: Bool) | left field l r -> a where
+  gproductField :: Lens' ((l :*: r) x) a
+
+instance GHasField field l a => GProductHasField field l r a 'True where
+  gproductField = first . gfield @field
+
+instance GHasField field r a => GProductHasField field l r a 'False where
+  gproductField = second . gfield @field
diff --git a/src/Data/Generics/Product/HasFieldAt.hs b/src/Data/Generics/Product/HasFieldAt.hs
deleted file mode 100644
--- a/src/Data/Generics/Product/HasFieldAt.hs
+++ /dev/null
@@ -1,176 +0,0 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE Rank2Types #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE UndecidableInstances #-}
-
------------------------------------------------------------------------------
--- |
--- Module      :  Data.Generics.Product.HasFieldAt
--- Copyright   :  (C) 2017 Csongor Kiss
--- License     :  BSD3
--- Maintainer  :  Csongor Kiss <kiss.csongor.kiss@gmail.com>
--- Stability   :  experimental
--- Portability :  non-portable
---
--- Derive product items lenses generically.
---
--- @
---
---   module Example where
---
---   import GHC.Generics
---   import Data.Generics.Product
---
---   data Human = Human String Int String
---     deriving (Generic, Show)
---
---   human :: Human
---   human = Human \"Tunyasz\" 50 \"London\"
---
--- @
---
------------------------------------------------------------------------------
-
-module Data.Generics.Product.HasFieldAt
-  ( HasFieldAt (..)
-    -- * Getter and setter functions
-  , getFieldAt
-  , setFieldAt
-  ) where
-
-import Data.Generics.Internal.Lens
-
-import GHC.TypeLits
-import Data.Kind                (Type)
-import GHC.Generics
-
--- | Get positional field
---
--- >>> getFieldAt @1 human
--- "Tunyasz"
-getFieldAt :: forall index a s. HasFieldAt index a s => s -> a
-getFieldAt s = s ^. itemAt @index
-
--- | Set positional field
---
--- >>> setFieldAt @2 (setField @1 "Tamas" human) 30
--- Human "Tamas" 30 "London"
-setFieldAt :: forall index a s. HasFieldAt index a s => a -> s -> s
-setFieldAt = set (itemAt @index)
-
--- | Types that have a field at given position.
-class HasFieldAt (index :: Nat) a s | s index -> a where
-  -- ^ Lens focusing on a field at a given index.
-  --   Compatible with the lens package.
-  --
-  -- >>> human & itemAt @1 .~ "Tamas"
-  -- Human "Tamas" 50 "London"
-  itemAt :: Lens' s a
-
--- | Fields are indexed from BaseIndex upwards.
-type BaseIndex = 1
-
--- | Instances are generated on the fly for all types that have the required
---   positional field.
-instance
-  ( Generic s
-  , ContainsAt BaseIndex index (Rep s) ~ 'True -- this is needed for the fundep
-  , GHasFieldAt BaseIndex index (Rep s) a
-  ) => HasFieldAt index a s where
-  itemAt =  repIso . gItemAt @BaseIndex @index
-
-data Choice = GoLeft | GoRight
-
-class GHasFieldAtProd offset index a b ret (w :: Choice) | offset index a b w -> ret where
-  prodItemAt :: Lens' ((a :*: b) x) ret
-
-instance (GHasFieldAt offset index f ret) => GHasFieldAtProd offset index f g ret 'GoLeft where
-  prodItemAt = first . gItemAt @offset @index
-
-instance (GHasFieldAt offset index g ret) => GHasFieldAtProd offset index f g ret 'GoRight where
-  prodItemAt = second . gItemAt @offset @index
-
---------------------------------------------------------------------------------
-
-type family Search offset index f g :: Choice where
-  Search offset index f g = Choose (ContainsAt offset index f) (ContainsAt (offset + Size f) index g)
-
-type family Choose f g :: Choice where
-  Choose 'True _ = 'GoLeft 
-  Choose _ 'True = 'GoRight
-  Choose _ _ = TypeError ('Text "Could not find type") 
-
--- | Try find a field by position in the generic representation.
-type family ContainsAt (offset :: Nat) (index :: Nat) f :: Bool where
-  ContainsAt offset index (D1 m f)
-    = ContainsAt offset index f
-  ContainsAt n n (S1 _ _)
-    = 'True
-  ContainsAt _ _ (S1 _ _)
-    = 'False
-  ContainsAt offset index  (f :*: g)
-    = ContainsAt offset index f || ContainsAt (Size f + offset) index g
-  ContainsAt offset index (C1 m f)
-    = ContainsAt offset index f
-  ContainsAt offset index (Rec0 _)
-    = 'False
-  ContainsAt offset index  U1
-    = 'False
-  ContainsAt offset index V1
-    = 'False
-  ContainsAt offset index t = TypeError ('ShowType offset ':<>: 'Text " " ':<>: 'ShowType index)
-
--- | Returns the count of terminal nodes in the generic representation.
-type family Size f :: Nat where
-  Size (D1 m f)
-    = Size f
-  Size (f :*: g)
-    = Size f + Size g
-  Size (C1 m f)
-    = Size f
-  Size t = 1
-
--- | If traversing to the left, offset does not change.
---   If traversing to the right, offset is incremented by size of left subtree.
-type family Offset (offset :: Nat) (choice :: Choice) (size :: Nat) :: Nat where
-  Offset n 'GoLeft _ = n
-  Offset n 'GoRight s = n + s
-
--- | Type-level or
-type family (a :: Bool) || (b :: Bool) :: Bool where
-  'True || _  = 'True
-  _ || b = b
-
---------------------------------------------------------------------------------
-
--- | Like 'HasFieldAt', but on the generic representation
-class GHasFieldAt (offset :: Nat) (index :: Nat) (s :: Type -> Type) a | offset index s -> a where
-  gItemAt :: Lens' (s x) a
-
-instance
-    ( choice ~ (Search offset index s s')
-    , offset' ~ Offset offset choice (Size s)
-    , GHasFieldAtProd offset' index s s' a choice 
-    ) 
-    => GHasFieldAt offset index (s :*: s') a where
-  gItemAt = prodItemAt @offset' @index @_ @_ @_ @choice
-
-instance GHasFieldAt offset index (K1 R a) a where
-  gItemAt f (K1 x) = fmap K1 (f x)
-
-instance GHasFieldAt n n (S1 ('MetaSel m p f b) (Rec0 a)) a where
-  gItemAt = lensM . gItemAt @n @n
-
-instance GHasFieldAt offset index s a => GHasFieldAt offset index (M1 D c s) a where
-  gItemAt = lensM . gItemAt @offset @index
-
-instance GHasFieldAt offset index s a => GHasFieldAt offset index (M1 C c s) a where
-  gItemAt = lensM . gItemAt @offset @index
-
diff --git a/src/Data/Generics/Product/Positions.hs b/src/Data/Generics/Product/Positions.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Generics/Product/Positions.hs
@@ -0,0 +1,161 @@
+{-# LANGUAGE AllowAmbiguousTypes    #-}
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE KindSignatures         #-}
+{-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE PolyKinds              #-}
+{-# LANGUAGE ScopedTypeVariables    #-}
+{-# LANGUAGE TypeApplications       #-}
+{-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE TypeOperators          #-}
+{-# LANGUAGE UndecidableInstances   #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Generics.Product.Positions
+-- Copyright   :  (C) 2017 Csongor Kiss
+-- License     :  BSD3
+-- Maintainer  :  Csongor Kiss <kiss.csongor.kiss@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Derive positional product type getters and setters generically.
+--
+-----------------------------------------------------------------------------
+
+module Data.Generics.Product.Positions
+  ( -- *Lenses
+
+    --  $example
+    HasPosition (..)
+
+    -- *Internals
+  , GHasPosition (..)
+  ) where
+
+import Data.Generics.Internal.Lens
+
+import Data.Kind
+import Data.Type.Bool
+import GHC.Generics
+import GHC.TypeLits
+
+--  $example
+--  @
+--    module Example where
+--
+--    import Data.Generics.Product
+--    import GHC.Generics
+--
+--    data Human = Human
+--      { name    :: String
+--      , age     :: Int
+--      , address :: String
+--      }
+--      deriving (Generic, Show)
+--
+--    human :: Human
+--    human = Human \"Tunyasz\" 50 \"London\"
+--  @
+
+-- |Records that have a field at a given position.
+class HasPosition (i :: Nat) a s | s i -> a where
+  -- |A lens that focuses on a field at a given position. Compatible with the
+  --  lens package's 'Control.Lens.Lens' type.
+  --
+  --  >>> human ^. position @1
+  --  "Tunyasz"
+  --  >>> human & position @2 .~ "Berlin"
+  --  Human {name = "Tunyasz", age = 50, address = "Berlin"}
+  position :: Lens' s a
+  position f s
+    = fmap (flip (setPosition @i) s) (f (getPosition @i s))
+    -- = fmap (setPosition s) (f (getPosition s))
+
+  -- |Get positional field
+  --
+  -- >>> getPosition @1 human
+  -- "Tunyasz"
+  getPosition :: s -> a
+  getPosition s = s ^. position @i
+
+  -- |Set positional field
+  --
+  -- >>> setPosition @2 (setField @1 "Tamas" human) 30
+  -- Human "Tamas" 30 "London"
+  setPosition :: a -> s -> s
+  setPosition = set (position @i)
+
+  {-# MINIMAL position | setPosition, getPosition #-}
+
+instance
+  ( Generic s
+  , ErrorUnless i s (0 <? i && i <=? Size (Rep s))
+  , GHasPosition 1 i (Rep s) a
+  ) => HasPosition i a s where
+
+  position = repIso . gposition @1 @i
+
+type family ErrorUnless (i :: Nat) (s :: Type) (hasP :: Bool) :: Constraint where
+  ErrorUnless i s 'False
+    = TypeError
+        (     'Text "The type "
+        ':<>: 'ShowType s
+        ':<>: 'Text " does not contain a field at position "
+        ':<>: 'ShowType i
+        )
+
+  ErrorUnless _ _ 'True
+    = ()
+
+-- |As 'HasPosition' but over generic representations as defined by
+--  "GHC.Generics".
+class GHasPosition (offset :: Nat) (i :: Nat) (f :: Type -> Type) a | offset i f -> a where
+  gposition :: Lens' (f x) a
+
+instance GHasPosition i i (S1 meta (Rec0 a)) a where
+  gposition = mIso . kIso
+
+instance GHasPosition offset i f a => GHasPosition offset i (M1 D meta f) a where
+  gposition = mIso . gposition @offset @i
+
+instance GHasPosition offset i f a => GHasPosition offset i (M1 C meta f) a where
+  gposition = mIso . gposition @offset @i
+
+instance
+  ( goLeft  ~ (i <? (offset + Size l))
+  , offset' ~ (If goLeft offset (offset + Size l))
+  , GProductHasPosition offset' i l r a goLeft
+  ) => GHasPosition offset i (l :*: r) a where
+
+  gposition = gproductPosition @offset' @i @_ @_ @_ @goLeft
+
+
+class GProductHasPosition (offset :: Nat) (i :: Nat) l r a (left :: Bool) | offset i l r left -> a where
+  gproductPosition :: Lens' ((l :*: r) x) a
+
+instance GHasPosition offset i l a => GProductHasPosition offset i l r a 'True where
+  gproductPosition = first . gposition @offset @i
+
+instance GHasPosition offset i r a => GProductHasPosition offset i l r a 'False where
+  gproductPosition = second . gposition @offset @i
+
+type family Size f :: Nat where
+  Size (l :*: r)
+    = Size l + Size r
+  Size (l :+: r)
+    = Min (Size l) (Size r)
+  Size (D1 meta f)
+    = Size f
+  Size (C1 meta f)
+    = Size f
+  Size f
+    = 1
+
+--------------------------------------------------------------------------------
+
+type x <? y = Not (y <=? x)
+infixl 4 <?
+
+type Min a b = If (a <? b) a b
diff --git a/src/Data/Generics/Product/Subtype.hs b/src/Data/Generics/Product/Subtype.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Generics/Product/Subtype.hs
@@ -0,0 +1,161 @@
+{-# LANGUAGE AllowAmbiguousTypes       #-}
+{-# LANGUAGE DataKinds                 #-}
+{-# LANGUAGE FlexibleContexts          #-}
+{-# LANGUAGE FlexibleInstances         #-}
+{-# LANGUAGE MultiParamTypeClasses     #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE PolyKinds                 #-}
+{-# LANGUAGE Rank2Types                #-}
+{-# LANGUAGE ScopedTypeVariables       #-}
+{-# LANGUAGE TypeApplications          #-}
+{-# LANGUAGE TypeFamilies              #-}
+{-# LANGUAGE TypeOperators             #-}
+{-# LANGUAGE UndecidableInstances      #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Generics.Product.Subtype
+-- Copyright   :  (C) 2017 Csongor Kiss
+-- License     :  BSD3
+-- Maintainer  :  Csongor Kiss <kiss.csongor.kiss@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Structural subtype relationship between record types.
+--
+-- The running example in this module is the following two types:
+--
+-- @
+--
+--   module Test where
+--
+--   import GHC.Generics
+--   import Data.Generics.Record
+--
+--   data Human = Human
+--     { name    :: String
+--     , age     :: Int
+--     , address :: String
+--     } deriving (Generic, Show)
+--
+--   data Animal = Animal
+--     { name    :: String
+--     , age     :: Int
+--     } deriving (Generic, Show)
+--
+--    human :: Human
+--    human = Human \"Tunyasz\" 50 \"London\"
+--
+-- @
+--
+-----------------------------------------------------------------------------
+module Data.Generics.Product.Subtype
+  ( Subtype (..)
+  ) where
+
+import Data.Generics.Internal.Families
+import Data.Generics.Internal.Lens
+import Data.Generics.Product.Fields
+
+import Data.Kind
+import GHC.Generics
+
+-- |Structural subtype relationship
+--
+-- @sub@ is a (structural) `subtype' of @sup@, if its fields are a subset of
+-- those of @sup@.
+--
+class Subtype sup sub where
+  -- | Structural subtype lens. Given a subtype relationship @sub :< sup@,
+  --   we can focus on the @sub@ structure of @sup@.
+  --
+  -- >>> human ^. super @Animal
+  -- Animal {name = "Tunyasz", age = 50}
+  --
+  -- >>> set (super @Animal) (Animal "dog" 10) human
+  -- Human {name = "dog", age = 10, address = "London"}
+  super  :: Lens' sub sup
+  super f sub
+    = fmap (`smash` sub) (f (upcast sub))
+
+  -- | Cast the more specific subtype to the more general supertype
+  --
+  -- >>> upcast human :: Animal
+  -- Animal {name = "Tunyasz", age = 50}
+  --
+  upcast :: sub -> sup
+  upcast s = s ^. super @sup
+
+  -- | Plug a smaller structure into a larger one
+  --
+  -- >>> smash (Animal "dog" 10) human
+  -- Human {name = "dog", age = 10, address = "London"}
+  smash  :: sup -> sub -> sub
+  smash = set (super @sup)
+
+  {-# MINIMAL super | smash, upcast #-}
+
+-- | Instances are created by the compiler
+instance
+  ( GSmash (Rep a) (Rep b)
+  , GUpcast (Rep a) (Rep b)
+  , Generic a
+  , Generic b
+  ) => Subtype b a where
+    smash p b = to $ gsmash (from p) (from b)
+    upcast    = to . gupcast . from
+
+--------------------------------------------------------------------------------
+-- * Generic upcasting
+
+-- | Upcast 'sub to 'sup' (generic rep)
+class GUpcast (sub :: Type -> Type) (sup :: Type -> Type) where
+  gupcast :: sub p -> sup p
+
+instance (GUpcast sub a, GUpcast sub b) => GUpcast sub (a :*: b) where
+  gupcast rep = gupcast rep :*: gupcast rep
+
+instance
+  GHasField field sub t
+  => GUpcast sub (S1 ('MetaSel ('Just field) p f b) (Rec0 t)) where
+
+  gupcast r = M1 (K1 (r ^. gfield @field))
+
+instance GUpcast sub sup => GUpcast sub (C1 c sup) where
+  gupcast = M1 . gupcast
+
+instance GUpcast sub sup => GUpcast sub (D1 c sup) where
+  gupcast = M1 . gupcast
+
+--------------------------------------------------------------------------------
+-- * Generic smashing
+
+class GSmash sub sup where
+  gsmash :: sup p -> sub p -> sub p
+
+instance (GSmash a sup, GSmash b sup) => GSmash (a :*: b) sup where
+  gsmash rep (a :*: b) = gsmash rep a :*: gsmash rep b
+
+instance
+  ( leaf ~ (S1 ('MetaSel ('Just field) p f b) t)
+  , GSmashLeaf leaf sup (HasTotalFieldP field sup)
+  ) => GSmash (S1 ('MetaSel ('Just field) p f b) t) sup where
+
+  gsmash = gsmashLeaf @_ @_ @(HasTotalFieldP field sup)
+
+instance GSmash sub sup => GSmash (C1 c sub) sup where
+  gsmash sup (M1 sub) = M1 (gsmash sup sub)
+
+instance GSmash sub sup => GSmash (D1 c sub) sup where
+  gsmash sup (M1 sub) = M1 (gsmash sup sub)
+
+class GSmashLeaf sub sup (w :: Bool) where
+  gsmashLeaf :: sup p -> sub p -> sub p
+
+instance
+  GHasField field sup t
+  => GSmashLeaf (S1 ('MetaSel ('Just field) p f b) (Rec0 t)) sup 'True where
+  gsmashLeaf sup _ = M1 (K1 (sup ^. gfield @field))
+
+instance GSmashLeaf (S1 ('MetaSel ('Just field) p f b) (Rec0 t)) sup 'False where
+  gsmashLeaf _ = id
diff --git a/src/Data/Generics/Product/Typed.hs b/src/Data/Generics/Product/Typed.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Generics/Product/Typed.hs
@@ -0,0 +1,137 @@
+{-# LANGUAGE AllowAmbiguousTypes   #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeApplications      #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE UndecidableInstances  #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Generics.Product.Typed
+-- Copyright   :  (C) 2017 Csongor Kiss
+-- License     :  BSD3
+-- Maintainer  :  Csongor Kiss <kiss.csongor.kiss@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Derive record field getters and setters generically.
+--
+-----------------------------------------------------------------------------
+
+module Data.Generics.Product.Typed
+  ( -- *Lenses
+    --
+    --  $example
+    HasType (..)
+
+    -- *Internals
+  , GHasType (..)
+  ) where
+
+import Data.Generics.Internal.Families
+import Data.Generics.Internal.Lens
+
+import Data.Kind
+import GHC.Generics
+import GHC.TypeLits
+
+--  $example
+--  @
+--    module Example where
+--
+--    import Data.Generics.Product
+--    import GHC.Generics
+--
+--    data Human = Human
+--      { name    :: String
+--      , age     :: Int
+--      , address :: String
+--      }
+--      deriving (Generic, Show)
+--
+--    human :: Human
+--    human = Human \"Tunyasz\" 50 \"London\"
+--  @
+
+--  | Records that have a field with a unique type.
+class HasType a s where
+  -- |A lens that focuses on a field with a unique type in its parent type.
+  --  Compatible with the lens package's 'Control.Lens.Lens' type.
+  --
+  --  >>> human ^. typed @Int
+  --  50
+  typed :: Lens' s a
+  typed f t
+    = fmap (flip (setTyped @a) t) (f (getTyped @a t))
+
+  -- |Get field at type
+  getTyped :: s -> a
+  getTyped s = s ^. typed @a
+
+  -- |Set field at type
+  setTyped :: a -> s -> s
+  setTyped = set (typed @a)
+
+  {-# MINIMAL typed | setTyped, getTyped #-}
+
+instance
+  ( Generic s
+  , ErrorUnlessOne a s (CountTotalType a (Rep s))
+  , GHasType (Rep s) a
+  ) => HasType a s where
+
+  typed = repIso . gtyped
+
+type family ErrorUnlessOne (a :: Type) (s :: Type) (count :: Count) :: Constraint where
+  ErrorUnlessOne a s 'None
+    = TypeError
+        (     'Text "The type "
+        ':<>: 'ShowType s
+        ':<>: 'Text " does not contain a value of type "
+        ':<>: 'ShowType a
+        )
+
+  ErrorUnlessOne a s 'Multiple
+    = TypeError
+        (     'Text "The type "
+        ':<>: 'ShowType s
+        ':<>: 'Text " contains multiple values of type "
+        ':<>: 'ShowType a
+        ':<>: 'Text "; the choice of value is thus ambiguous"
+        )
+
+  ErrorUnlessOne _ _ 'One
+    = ()
+
+-- |As 'HasType' but over generic representations as defined by
+--  "GHC.Generics".
+class GHasType (f :: Type -> Type) a where
+  gtyped :: Lens' (f x) a
+
+instance GProductHasType l r a (HasTotalTypeP a l)
+      => GHasType (l :*: r) a where
+
+  gtyped = gproductTyped @_ @_ @_ @(HasTotalTypeP a l)
+
+instance (GHasType l a, GHasType r a) => GHasType (l :+: r) a where
+  gtyped = combine (gtyped @l) (gtyped @r)
+
+instance GHasType (K1 R a) a where
+  gtyped f (K1 x) = fmap K1 (f x)
+
+instance GHasType f a => GHasType (M1 m meta f) a where
+  gtyped = mIso . gtyped
+
+class GProductHasType l r a (contains :: Bool) where
+  gproductTyped :: Lens' ((l :*: r) x) a
+
+instance GHasType l a => GProductHasType l r a 'True where
+  gproductTyped = first . gtyped
+
+instance GHasType r a => GProductHasType l r a 'False where
+  gproductTyped = second . gtyped
diff --git a/src/Data/Generics/Record.hs b/src/Data/Generics/Record.hs
deleted file mode 100644
--- a/src/Data/Generics/Record.hs
+++ /dev/null
@@ -1,33 +0,0 @@
------------------------------------------------------------------------------
--- |
--- Module      :  Data.Generics.Record
--- Copyright   :  (C) 2017 Csongor Kiss
--- License     :  BSD3
--- Maintainer  :  Csongor Kiss <kiss.csongor.kiss@gmail.com>
--- Stability   :  experimental
--- Portability :  non-portable
---
--- Magic record operations using Generics
---
--- These classes need not be instantiated manually, as GHC can automatically
--- prove valid instances via Generics. Only the `Generic` class needs to
--- be derived (see examples).
---
------------------------------------------------------------------------------
-module Data.Generics.Record
-  (
-    -- * Subtype relationship
-    Subtype  (..)
-  , super
-
-    -- * Magic lens
-  , HasField (..)
-
-    -- * Getter and setter
-  , getField
-  , setField
-
-  ) where
-
-import Data.Generics.Record.HasField
-import Data.Generics.Record.Subtype
diff --git a/src/Data/Generics/Record/HasField.hs b/src/Data/Generics/Record/HasField.hs
deleted file mode 100644
--- a/src/Data/Generics/Record/HasField.hs
+++ /dev/null
@@ -1,134 +0,0 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE Rank2Types #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE UndecidableInstances #-}
-
------------------------------------------------------------------------------
--- |
--- Module      :  Data.Generics.Record.HasField
--- Copyright   :  (C) 2017 Csongor Kiss
--- License     :  BSD3
--- Maintainer  :  Csongor Kiss <kiss.csongor.kiss@gmail.com>
--- Stability   :  experimental
--- Portability :  non-portable
---
--- Derive record field getters and setters generically.
---
------------------------------------------------------------------------------
-
-module Data.Generics.Record.HasField
-  ( -- * Lens
-    -- $example
-    HasField (..)
-    -- * Getter and setter functions
-  , getField
-  , setField
-    -- * Internals
-  , GHasField (..)
-  ) where
-
-import Data.Generics.Record.Internal.Contains
-
-import Data.Generics.Internal.Lens
-
-import GHC.TypeLits             (Symbol)
-import Data.Kind                (Type)
-import GHC.Generics
-
-
--- $example
--- @
---
---   module Example where
---
---   import GHC.Generics
---   import Data.Generics.Record
---
---   data Human = Human
---     { name    :: String
---     , age     :: Int
---     , address :: String
---     } deriving (Generic, Show)
---
---    human :: Human
---    human = Human \"Tunyasz\" 50 \"London\"
---
--- @
-
--- | Get 'field'
---
--- >>> getField @"name" human
--- "Tunyasz"
-getField :: forall field a s. HasField field a s => s -> a
-getField s = s ^. label @field
-
--- | Set 'field'
---
--- >>> setField @"age" (setField @"name" "Tamas" human) 30
--- Human {name = "Tamas", age = 30, address = "London"}
-setField :: forall field a s. HasField field a s => a -> s -> s
-setField = set (label @field)
-
--- | Records that have a field with a given name.
-class HasField (field :: Symbol) a s | s field -> a where
-  -- ^ Lens focusing on a field with a given name.
-  --   Compatible with the lens package.
-  --
-  -- @
-  --  type Lens' s a
-  --    = forall f. Functor f => (a -> f a) -> s -> f s
-  -- @
-  --
-  -- >>> human & label @"name" .~ "Tamas"
-  -- Human {name = "Tamas", age = 50, address = "London"}
-  label :: Lens' s a
-
--- | Instances are generated on the fly for all records that have the required
---   field.
-instance
-  ( Generic s
-  , Contains field (Rep s) ~ 'Just a -- this is needed for the fundep for some reason
-  , GHasField field (Rep s) a
-  ) => HasField field a s where
-  label =  repIso . glabel @field
-
-
-class GHasFieldProd field a b ret (w :: Maybe Type) | field a b -> ret where
-  prodLabel :: Lens' ((a :*: b) x) ret
-
-instance (GHasField field f ret) => GHasFieldProd field f g ret ('Just ret) where
-  prodLabel = first . glabel @field
-
-instance (GHasField field g ret) => GHasFieldProd field f g ret 'Nothing where
-  prodLabel = second . glabel @field
-
---------------------------------------------------------------------------------
-
--- | Like 'HasField', but on the generic representation
-class GHasField (field :: Symbol) (s :: Type -> Type) a | field s -> a where
-  glabel :: Lens' (s x) a
-
-instance (GHasFieldProd field s s' a (Contains field s)) => GHasField field (s :*: s') a where
-  glabel = prodLabel @field @_ @_ @_ @(Contains field s)
-
-instance (GHasField field s a, GHasField field s' a) => GHasField field (s :+: s') a where
-  glabel = combine (glabel @field @s) (glabel @field @s')
-
-instance GHasField field (S1 ('MetaSel ('Just field) p f b) (Rec0 a)) a where
-  glabel = lensM . glabel @field
-
-instance GHasField field (K1 R a) a where
-  glabel f (K1 x) = fmap K1 (f x)
-
-instance GHasField field s a => GHasField field (M1 D c s) a where
-  glabel = lensM . glabel @field
-
-instance GHasField field s a => GHasField field (M1 C c s) a where
-  glabel = lensM . glabel @field
diff --git a/src/Data/Generics/Record/Internal/Contains.hs b/src/Data/Generics/Record/Internal/Contains.hs
deleted file mode 100644
--- a/src/Data/Generics/Record/Internal/Contains.hs
+++ /dev/null
@@ -1,63 +0,0 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE Rank2Types #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE UndecidableInstances #-}
-
------------------------------------------------------------------------------
--- |
--- Module      :  Data.Generics.Record.Internal.Contains
--- Copyright   :  (C) 2017 Csongor Kiss
--- License     :  BSD3
--- Maintainer  :  Csongor Kiss <kiss.csongor.kiss@gmail.com>
--- Stability   :  experimental
--- Portability :  non-portable
---
--- Look up fields in the generic representation
---
------------------------------------------------------------------------------
-module Data.Generics.Record.Internal.Contains
-  ( Contains
-  ) where
-
-import Data.Kind                (Type)
-import GHC.Generics
-
-import GHC.TypeLits
-
--- | Look up a record field by name in the generic representation, and return
---   its corresponding type, if exists.
-type family Contains (field :: Symbol) f :: Maybe Type where
-  Contains field (S1 ('MetaSel ('Just field) _ _ _) (Rec0 t))
-    = 'Just t
-  Contains field (f :*: g)
-    = Contains field f <|> Contains field g
-  Contains field (f :+: g)
-    = Contains field f <&> Contains field g
-  Contains field (S1 _ _)
-    = 'Nothing
-  Contains field (C1 m f)
-    = Contains field f
-  Contains field (D1 m f)
-    = Contains field f
-  Contains field (Rec0 _)
-    = 'Nothing
-  Contains field U1
-    = 'Nothing
-  Contains field V1
-    = 'Nothing
-  Contains x t = TypeError ('ShowType t)
-
--- | Type-level alternative
-type family (a :: Maybe k) <|> (b :: Maybe k) :: Maybe k where
-  'Just x <|> _  = 'Just x
-  _ <|> b = b
-
-type family (a :: Maybe k) <&> (b :: Maybe k) :: Maybe k where
-  'Just x <&> 'Just x  = 'Just x
-  _ <&> _ = 'Nothing
-
diff --git a/src/Data/Generics/Record/Subtype.hs b/src/Data/Generics/Record/Subtype.hs
deleted file mode 100644
--- a/src/Data/Generics/Record/Subtype.hs
+++ /dev/null
@@ -1,138 +0,0 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE Rank2Types #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE UndecidableInstances #-}
-
------------------------------------------------------------------------------
--- |
--- Module      :  Data.Generics.Record.Subtype
--- Copyright   :  (C) 2017 Csongor Kiss
--- License     :  BSD3
--- Maintainer  :  Csongor Kiss <kiss.csongor.kiss@gmail.com>
--- Stability   :  experimental
--- Portability :  non-portable
---
--- Structural subtype relationship between record types.
---
--- The running example in this module is the following two types:
---
--- @
---
---   module Test where
---
---   import GHC.Generics
---   import Data.Generics.Record
---
---   data Human = Human
---     { name    :: String
---     , age     :: Int
---     , address :: String
---     } deriving (Generic, Show)
---
---   data Animal = Animal
---     { name    :: String
---     , age     :: Int
---     } deriving (Generic, Show)
---
---    human :: Human
---    human = Human \"Tunyasz\" 50 \"London\"
---
--- @
---
------------------------------------------------------------------------------
-module Data.Generics.Record.Subtype
-  ( Subtype (..)
-  , super
-  ) where
-
-import Data.Generics.Record.HasField
-import Data.Generics.Record.Internal.Contains
-
-import Data.Generics.Internal.Lens
-
-import Data.Kind                (Type)
-import GHC.Generics
-
--- |Structural subtype relationship
---
--- @sub@ is a (structural) `subtype' of @sup@, if its fields are a subset of
--- those of @sup@.
---
-class Subtype sub sup where
-  -- | Cast the more specific subtype to the more general supertype
-  --
-  -- >>> upcast human :: Animal
-  -- Animal {name = "Tunyasz", age = 50}
-  --
-  upcast :: sub -> sup
-  -- | Plug a smaller structure into a larger one
-  --
-  -- >>> smash (Animal "dog" 10) human
-  -- Human {name = "dog", age = 10, address = "London"}
-  smash  :: sup -> sub -> sub
-
--- | Instances are created by the compiler
-instance (GSmash (Rep a) (Rep b), GUpcast (Rep a) (Rep b), Generic a, Generic b) => Subtype a b where
-  upcast    = to . gupcast . from
-  smash p b = to $ gsmash (from p) (from b)
-
--- | Structural subtype lens. Given a subtype relationship @sub :< sup@,
---   we can focus on the @sub@ structure of @sup@.
---
--- >>> human ^. super @Animal
--- Animal {name = "Tunyasz", age = 50}
---
--- >>> set (super @Animal) (Animal "dog" 10) human
--- Human {name = "dog", age = 10, address = "London"}
-super :: forall sup sub. Subtype sub sup => Lens' sub sup
-super f sub = fmap (flip smash sub) (f (upcast sub))
-
---------------------------------------------------------------------------------
--- * Generic upcasting
-
--- | Upcast 'sub to 'sup' (generic rep)
-class GUpcast (sub :: Type -> Type) (sup :: Type -> Type) where
-  gupcast :: sub p -> sup p
-
-instance (GUpcast sub a, GUpcast sub b) => GUpcast sub (a :*: b) where
-  gupcast rep = gupcast rep :*: gupcast rep
-
-instance {-# OVERLAPPING #-} GHasField field sub t => GUpcast sub (S1 ('MetaSel ('Just field) p f b) (Rec0 t)) where
-  gupcast r = M1 (K1 (r ^. glabel @field))
-
-instance GUpcast sub sup => GUpcast sub (M1 i c sup) where
-  gupcast = M1 . gupcast
-
---------------------------------------------------------------------------------
--- * Generic smashing
-
-class GSmash sub sup where
-  gsmash :: sup p -> sub p -> sub p
-
-instance (GSmash a sup, GSmash b sup) => GSmash (a :*: b) sup where
-  gsmash rep (a :*: b) = gsmash rep a :*: gsmash rep b
-
-instance {-# OVERLAPPING #-}
-  ( leaf ~ (S1 ('MetaSel ('Just field) p f b) t)
-  , GSmashLeaf leaf sup (Contains field sup)
-  ) => GSmash (S1 ('MetaSel ('Just field) p f b) t) sup where
-  gsmash = gsmashLeaf @_ @_ @(Contains field sup)
-
-instance GSmash sub sup => GSmash (M1 i c sub) sup where
-  gsmash sup (M1 sub) = M1 (gsmash sup sub)
-
-class GSmashLeaf sub sup (w :: Maybe Type) where
-  gsmashLeaf :: sup p -> sub p -> sub p
-
-instance (GHasField field sup t) => GSmashLeaf (S1 ('MetaSel ('Just field) p f b) (Rec0 t)) sup ('Just t) where
-  gsmashLeaf sup (M1 (K1 _)) = M1 (K1 (sup ^. glabel @field))
-
-instance GSmashLeaf (S1 ('MetaSel ('Just field) p f b) (Rec0 t)) sup 'Nothing where
-  gsmashLeaf _ = id
diff --git a/src/Data/Generics/Sum.hs b/src/Data/Generics/Sum.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Generics/Sum.hs
@@ -0,0 +1,28 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Generics.Sum
+-- Copyright   :  (C) 2017 Csongor Kiss
+-- License     :  BSD3
+-- Maintainer  :  Csongor Kiss <kiss.csongor.kiss@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Magic sum operations using Generics
+--
+-- These classes need not be instantiated manually, as GHC can automatically
+-- prove valid instances via Generics. Only the `Generic` class needs to
+-- be derived (see examples).
+--
+-----------------------------------------------------------------------------
+
+module Data.Generics.Sum
+  ( -- *Prisms
+    AsAny (..)
+
+  , AsConstructor (..)
+  , AsType (..)
+  ) where
+
+import Data.Generics.Sum.Any
+import Data.Generics.Sum.Constructors
+import Data.Generics.Sum.Typed
diff --git a/src/Data/Generics/Sum/Any.hs b/src/Data/Generics/Sum/Any.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Generics/Sum/Any.hs
@@ -0,0 +1,87 @@
+{-# LANGUAGE AllowAmbiguousTypes    #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE PolyKinds              #-}
+{-# LANGUAGE ScopedTypeVariables    #-}
+{-# LANGUAGE TypeApplications       #-}
+{-# LANGUAGE UndecidableInstances   #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Generics.Sum.Any
+-- Copyright   :  (C) 2017 Csongor Kiss
+-- License     :  BSD3
+-- Maintainer  :  Csongor Kiss <kiss.csongor.kiss@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Derive a variety of prisms generically.
+--
+-----------------------------------------------------------------------------
+
+module Data.Generics.Sum.Any
+  ( -- *Prisms
+    --
+    --  $example
+    AsAny (..)
+  ) where
+
+import Data.Generics.Internal.Lens
+import Data.Generics.Sum.Constructors
+import Data.Generics.Sum.Typed
+
+--  $example
+--  @
+--    module Example where
+--
+--    import Data.Generics.Sum
+--    import GHC.Generics
+--
+--    data Animal
+--      = Dog Dog
+--      | Cat (Name, Age)
+--      | Duck Age
+--      deriving (Generic, Show)
+--
+--    data Dog = MkDog
+--      { name :: Name
+--      , age  :: Age
+--      }
+--      deriving (Generic, Show)
+--
+--    type Name = String
+--    type Age  = Int
+--
+--    dog, cat, duck :: Animal
+--
+--    dog = Dog (MkDog "Shep" 3)
+--    cat = Cat ("Mog", 5)
+--    duck = Duck 2
+--  @
+
+-- |Sums that have generic prisms.
+class AsAny (sel :: k) a s | s sel k -> a where
+  -- |A prism that projects a sum as identified by some selector. Currently
+  --  supported selectors are constructor names and unique types. Compatible
+  --  with the lens package's 'Control.Lens.Prism' type.
+  --
+  --  >>> dog ^? _As @"Dog"
+  --  Just (MkDog {name = "Shep", age = 3})
+  --  >>> dog ^? _As @Dog
+  --  Just (MkDog {name = "Shep", age = 3})
+  --  >>> dog ^? _As @"Cat"
+  --  Nothing
+  --  >>> cat ^? _As @"Cat"
+  --  Just ("Mog", 5)
+  --  >>> _As @"Cat" # ("Garfield", 6) :: Animal
+  --  Cat ("Garfield", 6)
+  --  >>> duck ^? _As @Age
+  --  Just 2
+  _As :: Prism' s a
+
+instance AsConstructor ctor a s => AsAny ctor a s where
+  _As = _Ctor @ctor
+
+instance AsType a s => AsAny a a s where
+  _As = _Typed @a
diff --git a/src/Data/Generics/Sum/Constructors.hs b/src/Data/Generics/Sum/Constructors.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Generics/Sum/Constructors.hs
@@ -0,0 +1,136 @@
+{-# LANGUAGE AllowAmbiguousTypes    #-}
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE KindSignatures         #-}
+{-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE ScopedTypeVariables    #-}
+{-# LANGUAGE TypeApplications       #-}
+{-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE TypeOperators          #-}
+{-# LANGUAGE UndecidableInstances   #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Generics.Sum.Constructors
+-- Copyright   :  (C) 2017 Csongor Kiss
+-- License     :  BSD3
+-- Maintainer  :  Csongor Kiss <kiss.csongor.kiss@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Derive constructor-name-based prisms generically.
+--
+-----------------------------------------------------------------------------
+
+module Data.Generics.Sum.Constructors
+  ( -- *Prisms
+
+    --  $example
+    AsConstructor (..)
+  ) where
+
+import Data.Generics.Internal.Families
+import Data.Generics.Internal.HList
+import Data.Generics.Internal.Lens
+
+import Data.Kind
+import GHC.Generics
+import GHC.TypeLits
+
+--  $example
+--  @
+--    module Example where
+--
+--    import Data.Generics.Sum
+--    import GHC.Generics
+--
+--    data Animal
+--      = Dog Dog
+--      | Cat (Name, Age)
+--      | Duck Age
+--      deriving (Generic, Show)
+--
+--    data Dog = MkDog
+--      { name :: Name
+--      , age  :: Age
+--      }
+--      deriving (Generic, Show)
+--
+--    type Name = String
+--    type Age  = Int
+--
+--    dog, cat, duck :: Animal
+--
+--    dog = Dog (MkDog "Shep" 3)
+--    cat = Cat ("Mog", 5)
+--    duck = Duck 2
+--  @
+
+-- |Sums that have a constructor with a given name.
+class AsConstructor (ctor :: Symbol) a s | s ctor -> a where
+  -- |A prism that projects a named constructor from a sum. Compatible with the
+  --  lens package's 'Control.Lens.Prism' type.
+  --
+  --  >>> dog ^? _Ctor @"Dog"
+  --  Just (MkDog {name = "Shep", age = 3})
+  --
+  --  >>> dog ^? _Ctor @"Cat"
+  --  Nothing
+  --
+  --  >>> cat ^? _Ctor @"Cat"
+  --  Just ("Mog", 5)
+  --
+  --  >>> _Ctor @"Cat" # ("Garfield", 6) :: Animal
+  --  Cat ("Garfield", 6)
+  _Ctor :: Prism' s a
+
+instance
+  ( Generic s
+  , ErrorUnless ctor s (HasCtorP ctor (Rep s))
+  , GAsConstructor ctor (Rep s) a
+  ) => AsConstructor ctor a s where
+
+  _Ctor = repIso . _GCtor @ctor
+
+type family ErrorUnless (ctor :: Symbol) (s :: Type) (contains :: Bool) :: Constraint where
+  ErrorUnless ctor s 'False
+    = TypeError
+        (     'Text "The type "
+        ':<>: 'ShowType s
+        ':<>: 'Text " does not contain a constructor named "
+        ':<>: 'ShowType ctor
+        )
+
+  ErrorUnless _ _ 'True
+    = ()
+
+-- |As 'AsConstructor' but over generic representations as defined by
+--  "GHC.Generics".
+class GAsConstructor (ctor :: Symbol) (f :: Type -> Type) a | ctor f -> a where
+  _GCtor :: Prism' (f x) a
+
+instance
+  ( GCollectible f as
+  , ListTuple a as
+  ) => GAsConstructor ctor (M1 C ('MetaCons ctor fixity fields) f) a where
+
+  _GCtor = prism (M1 . gfromCollection . tupleToList) (Right . listToTuple @_ @as . gtoCollection . unM1)
+
+instance GSumAsConstructor ctor l r a (HasCtorP ctor l) => GAsConstructor ctor (l :+: r) a where
+  _GCtor = _GSumCtor @ctor @l @r @a @(HasCtorP ctor l)
+
+instance GAsConstructor ctor f a => GAsConstructor ctor (M1 D meta f) a where
+  _GCtor = mIso . _GCtor @ctor
+
+instance GAsConstructor ctor f a => GAsConstructor ctor (M1 S meta f) a where
+  _GCtor = mIso . _GCtor @ctor
+
+class GSumAsConstructor (ctor :: Symbol) l r a (contains :: Bool) | ctor l r contains -> a where
+  _GSumCtor :: Prism' ((l :+: r) x) a
+
+instance GAsConstructor ctor l a => GSumAsConstructor ctor l r a 'True where
+  _GSumCtor = left . _GCtor @ctor
+
+instance GAsConstructor ctor r a => GSumAsConstructor ctor l r a 'False where
+  _GSumCtor = right . _GCtor @ctor
diff --git a/src/Data/Generics/Sum/Typed.hs b/src/Data/Generics/Sum/Typed.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Generics/Sum/Typed.hs
@@ -0,0 +1,142 @@
+{-# LANGUAGE AllowAmbiguousTypes    #-}
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE FlexibleContexts       #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE KindSignatures         #-}
+{-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE ScopedTypeVariables    #-}
+{-# LANGUAGE TypeApplications       #-}
+{-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE TypeOperators          #-}
+{-# LANGUAGE UndecidableInstances   #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Generics.Sum.Typed
+-- Copyright   :  (C) 2017 Csongor Kiss
+-- License     :  BSD3
+-- Maintainer  :  Csongor Kiss <kiss.csongor.kiss@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Derive constructor-field-type-based prisms generically.
+--
+-----------------------------------------------------------------------------
+
+module Data.Generics.Sum.Typed
+  ( -- *Prisms
+    --
+    --  $example
+    AsType (..)
+
+    -- *Internals
+  , GAsType (..)
+  ) where
+
+import Data.Generics.Internal.Families
+import Data.Generics.Internal.HList
+import Data.Generics.Internal.Lens
+
+import Data.Kind
+import GHC.Generics
+import GHC.TypeLits
+
+--  $example
+--  @
+--    module Example where
+--
+--    import Data.Generics.Sum
+--    import GHC.Generics
+--
+--    data Animal
+--      = Dog Dog
+--      | Cat (Name, Age)
+--      | Duck Age
+--      deriving (Generic, Show)
+--
+--    data Dog = MkDog
+--      { name :: Name
+--      , age  :: Age
+--      }
+--      deriving (Generic, Show)
+--
+--    type Name = String
+--    type Age  = Int
+--
+--    dog, cat, duck :: Animal
+--
+--    dog = Dog (MkDog "Shep" 3)
+--    cat = Cat ("Mog", 5)
+--    duck = Duck 2
+--  @
+
+-- |Sums that have a constructor with a field of the given type.
+class AsType a s where
+  -- |A prism that projects a constructor uniquely identifiable by the type of
+  --  its field. Compatible with the lens package's 'Control.Lens.Prism' type.
+  --
+  --  >>> dog ^? _Typed @Dog
+  --  Just (MkDog {name = "Shep", age = 3})
+  --  >>> dog ^? _Typed @Cat
+  --  Nothing
+  --  >>> duck ^? _Typed @Age
+  --  Just 2
+  _Typed :: Prism' s a
+
+instance
+  ( Generic s
+  , ErrorUnlessOne a s (CountPartialType a (Rep s))
+  , GAsType (Rep s) a
+  ) => AsType a s where
+
+  _Typed = repIso . _GTyped
+
+type family ErrorUnlessOne (a :: Type) (s :: Type) (count :: Count) :: Constraint where
+  ErrorUnlessOne a s 'None
+    = TypeError
+        (     'Text "The type "
+        ':<>: 'ShowType s
+        ':<>: 'Text " does not contain a constructor whose field is of type "
+        ':<>: 'ShowType a
+        )
+
+  ErrorUnlessOne a s 'Multiple
+    = TypeError
+        (     'Text "The type "
+        ':<>: 'ShowType s
+        ':<>: 'Text " contains multiple constructors whose fields are of type "
+        ':<>: 'ShowType a
+        ':<>: 'Text "; the choice of constructor is thus ambiguous"
+        )
+
+  ErrorUnlessOne _ _ 'One
+    = ()
+
+-- |As 'AsType' but over generic representations as defined by "GHC.Generics".
+class GAsType (f :: Type -> Type) a where
+  _GTyped :: Prism' (f x) a
+
+instance
+  ( GCollectible f '[a]
+  ) => GAsType (M1 C meta f) a where
+
+  _GTyped = prism (M1 . gfromCollection . tupleToList) (Right . listToTuple @_ @'[a] . gtoCollection . unM1)
+
+instance GSumAsType l r a (HasPartialTypeP a l) => GAsType (l :+: r) a where
+  _GTyped = _GSumTyped @l @r @a @(HasPartialTypeP a l)
+
+instance GAsType f a => GAsType (M1 D meta f) a where
+  _GTyped = mIso . _GTyped
+
+instance GAsType f a => GAsType (M1 S meta f) a where
+  _GTyped = mIso . _GTyped
+
+class GSumAsType l r a (contains :: Bool) where
+  _GSumTyped :: Prism' ((l :+: r) x) a
+
+instance GAsType l a => GSumAsType l r a 'True where
+  _GSumTyped = left . _GTyped
+
+instance GAsType r a => GSumAsType l r a 'False where
+  _GSumTyped = right . _GTyped
diff --git a/test/Spec.hs b/test/Spec.hs
new file mode 100644
--- /dev/null
+++ b/test/Spec.hs
@@ -0,0 +1,1 @@
+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}