diff --git a/ChangeLog.md b/ChangeLog.md
new file mode 100644
--- /dev/null
+++ b/ChangeLog.md
@@ -0,0 +1,5 @@
+# Revision history for generic-lens
+
+## 0.1.0.0  -- YYYY-mm-dd
+
+* First version. Released on an unsuspecting world.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2017, Csongor Kiss
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Csongor Kiss nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/examples/StarWars.hs b/examples/StarWars.hs
new file mode 100644
--- /dev/null
+++ b/examples/StarWars.hs
@@ -0,0 +1,72 @@
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DuplicateRecordFields #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+
+-- Note: this file may contain spoilers
+-- (although I would be really surprised if it did, I haven't seen the films)
+module StarWars where
+
+import GHC.Generics
+import Data.Generics.Record
+import Data.Generics.Product
+
+data Episode = NEWHOPE | EMPIRE | JEDI
+  deriving (Generic, Show, Eq)
+
+data Character = Character
+   { name      :: String
+   , friends   :: [Character]
+   , appearsIn :: [Episode]
+   } deriving (Generic, Show, Eq)
+
+data Human = Human
+  { name        :: String
+  , friends     :: [Character]
+  , appearsIn   :: [Episode]
+  , homePlanet  :: String
+  } deriving (Generic, Show)
+
+data Droid = Droid
+  { friends         :: [Character]
+  , appearsIn       :: [Episode]
+  , name            :: String
+  , primaryFunction :: String
+  } deriving (Generic, Show)
+
+luke :: Human
+luke = Human
+  { name           = "Luke Skywalker"
+  , friends        = []
+  , appearsIn      = [NEWHOPE, EMPIRE, JEDI]
+  , homePlanet     = "Saturn (?)"
+  }
+
+r2d2 :: Droid
+r2d2 = Droid
+  { name            = "R2-D2"
+  , friends         = [upcast luke]
+  , appearsIn       = [NEWHOPE, EMPIRE, JEDI]
+  , primaryFunction = "repair ships"
+  }
+
+c3po :: Droid
+c3po = Droid
+  { name            = "C3PO"
+  , friends         = [upcast r2d2, upcast luke]
+  , appearsIn       = [NEWHOPE, EMPIRE, JEDI]
+  , primaryFunction = "protocol and human relations"
+  }
+
+getName :: HasField "name" a r => r -> a
+getName = getField @"name"
+
+-- upcast :: Subtype a b => a -> b
+characters :: [Character]
+characters = [upcast r2d2, upcast luke, upcast c3po]
+
+names :: [String]
+names = map getName characters
+-- => ["R2-D2","Luke Skywalker","C3PO"]
diff --git a/generic-lens.cabal b/generic-lens.cabal
new file mode 100644
--- /dev/null
+++ b/generic-lens.cabal
@@ -0,0 +1,66 @@
+name:                generic-lens
+
+version:             0.1.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
+
+license-file:        LICENSE
+
+author:              Csongor Kiss
+
+maintainer:          kiss.csongor.kiss@gmail.com
+
+category:            Generics, Records, Lens
+
+build-type:          Simple
+
+-- Extra files to be distributed with the package, such as examples or a
+-- README.
+extra-source-files:  ChangeLog.md
+                   , examples/StarWars.hs
+
+-- Constraint on the version of Cabal needed to build this package.
+cabal-version:       >= 1.10
+
+
+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
+
+  other-modules:     Data.Generics.Record.Internal.Contains
+
+  other-extensions:  AllowAmbiguousTypes
+                   , DataKinds
+                   , FlexibleInstances
+                   , FunctionalDependencies
+                   , PolyKinds
+                   , Rank2Types
+                   , ScopedTypeVariables
+                   , TypeApplications
+                   , TypeFamilies
+                   , TypeOperators
+                   , UndecidableInstances
+
+  -- Other library packages from which modules are imported.
+  build-depends:     base >= 4.9 && <= 5.0
+
+  -- Directories containing source files.
+  hs-source-dirs:    src
+
+  -- Base language which the package is written in.
+  default-language:  Haskell2010
+  ghc-options:       -Wall
+
+source-repository head
+  type:     git
+  location: https://github.com/kcsongor/generic-lens
diff --git a/src/Data/Generics/Internal/Lens.hs b/src/Data/Generics/Internal/Lens.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Generics/Internal/Lens.hs
@@ -0,0 +1,59 @@
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE TypeOperators #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Generics.Internal.Lens
+-- Copyright   :  (C) 2017 Csongor Kiss
+-- License     :  BSD3
+-- Maintainer  :  Csongor Kiss <kiss.csongor.kiss@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Internal lens helpers. Only exported for Haddock
+--
+-----------------------------------------------------------------------------
+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)
+
+-- | Type alias for lens
+type Lens' s a
+  = forall f. Functor f => (a -> f a) -> s -> f s
+
+-- | Getting
+(^.) :: s -> ((a -> Const a a) -> s -> Const a s) -> a
+s ^. l = getConst (l Const s)
+
+-- | Setting
+set :: ((a -> Identity b) -> s -> Identity t) -> b -> s -> t
+set l b
+  = runIdentity . l (\_ -> Identity b)
+
+-- | Lens focusing on the first element of a product
+first :: Lens' ((a :*: b) x) (a x)
+first f (a :*: b)
+  = fmap (:*: b) (f a)
+
+-- | Lens focusing on the second element of a product
+second :: Lens' ((a :*: b) x) (b x)
+second f (a :*: b)
+  = fmap (a :*:) (f b)
+
+-- | A type and its generic representation are isomorphic
+repIso :: Generic a => Lens' a (Rep a x)
+repIso a = fmap to . a . from
+
+-- | '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)
diff --git a/src/Data/Generics/Product.hs b/src/Data/Generics/Product.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Generics/Product.hs
@@ -0,0 +1,28 @@
+-----------------------------------------------------------------------------
+-- |
+-- 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 product 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.Product
+  (
+    -- * Magic lens
+    HasFieldAt  (..)
+
+    -- * Getter and setter
+  , getFieldAt
+  , setFieldAt
+
+  ) where
+
+import Data.Generics.Product.HasFieldAt
diff --git a/src/Data/Generics/Product/HasFieldAt.hs b/src/Data/Generics/Product/HasFieldAt.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Generics/Product/HasFieldAt.hs
@@ -0,0 +1,176 @@
+{-# 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/Record.hs b/src/Data/Generics/Record.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Generics/Record.hs
@@ -0,0 +1,33 @@
+-----------------------------------------------------------------------------
+-- |
+-- 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  (..)
+  , subtype
+
+    -- * 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
new file mode 100644
--- /dev/null
+++ b/src/Data/Generics/Record/HasField.hs
@@ -0,0 +1,131 @@
+{-# 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 (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
new file mode 100644
--- /dev/null
+++ b/src/Data/Generics/Record/Internal/Contains.hs
@@ -0,0 +1,59 @@
+{-# 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.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 (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
+
diff --git a/src/Data/Generics/Record/Subtype.hs b/src/Data/Generics/Record/Subtype.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Generics/Record/Subtype.hs
@@ -0,0 +1,138 @@
+{-# 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 (..)
+  , subtype
+  ) 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 ^. subtype @Animal
+-- Animal {name = "Tunyasz", age = 50}
+--
+-- >>> set (subtype @Animal) (Animal "dog" 10) human
+-- Human {name = "dog", age = 10, address = "London"}
+subtype :: forall sup sub. Subtype sub sup => Lens' sub sup
+subtype 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