diff --git a/lens.cabal b/lens.cabal
--- a/lens.cabal
+++ b/lens.cabal
@@ -1,6 +1,6 @@
 name:          lens
 category:      Data, Lenses
-version:       1.2
+version:       1.3
 license:       BSD3
 cabal-version: >= 1.6
 license-file:  LICENSE
@@ -105,8 +105,8 @@
   .
   /Isomorphisms and Iso/
   .
-  Control.Isomorphic provides easy overloading of function application for isomorphisms and @Iso a b a d@ uses it
-  to form isomorphism families that can be composed with other isomorphisms and with lenses, setters, folds, 
+  Control.Isomorphic provides easy overloading of function application for isomorphisms and @Iso a b c d@ uses it
+  to form isomorphism families that can be composed with other isomorphisms and with lenses, setters, folds,
   traversals and getters.
   .
   > type Iso a b c d = forall k f. (Isomorphic k, Functor f) => k (c -> f d) (a -> f b)
@@ -155,44 +155,51 @@
   location: git://github.com/ekmett/lens.git
 
 library
-  exposed-modules:
-    Control.Exception.Lens
-    Control.Isomorphic
-    Control.Lens
-    Control.Lens.Internal
-    Control.Lens.Representable
-    Control.Lens.TH
-    Control.Parallel.Strategies.Lens
-    Control.Seq.Lens
-    Data.Array.Lens
-    Data.Bits.Lens
-    Data.ByteString.Lens
-    Data.ByteString.Lazy.Lens
-    Data.Complex.Lens
-    Data.Dynamic.Lens
-    Data.Map.Lens
-    Data.IntMap.Lens
-    Data.IntSet.Lens
-    Data.Sequence.Lens
-    Data.Set.Lens
-    Data.Text.Lens
-    Data.Text.Lazy.Lens
-    Data.Time.Calendar.Lens
-    Data.Tree.Lens
-
-  -- All dependencies are in the Haskell Platform
   build-depends:
-    array            == 0.4.*,
-    base             == 4.*,
-    bytestring       == 0.9.*,
-    containers       >= 0.3   && < 0.6,
-    mtl              >= 2.1.1 && < 2.2,
-    parallel         == 3.2.*,
-    template-haskell >= 2.4   && < 2.8,
-    text             == 0.11.*,
-    time             == 1.4.*,
-    transformers     >= 0.2   && < 0.4
+    base         == 4.*,
+    containers   >= 0.3   && < 0.6,
+    mtl          >= 2.1.1 && < 2.2,
+    transformers >= 0.2   && < 0.4
 
+  exposed-modules: Control.Isomorphic
+                   Control.Lens
+                   Control.Lens.Internal
+                   Control.Lens.Representable
+
+  -- base
+  exposed-modules: Control.Exception.Lens
+                   Data.Bits.Lens
+                   Data.Complex.Lens
+                   Data.Dynamic.Lens
+
+  -- containers
+  exposed-modules: Data.IntMap.Lens
+                   Data.IntSet.Lens
+                   Data.Map.Lens
+                   Data.Sequence.Lens
+                   Data.Set.Lens
+                   Data.Tree.Lens
+
+  build-depends:   template-haskell >= 2.4 && < 2.8
+  exposed-modules: Language.Haskell.TH.Lens
+                   Control.Lens.TH
+
+  -- platform
+  build-depends:   array == 0.4.*
+  exposed-modules: Data.Array.Lens
+
+  build-depends:   bytestring == 0.9.*
+  exposed-modules: Data.ByteString.Lens Data.ByteString.Lazy.Lens
+
+  build-depends:   text == 0.11.*
+  exposed-modules: Data.Text.Lens Data.Text.Lazy.Lens
+
+  build-depends:   parallel == 3.2.*
+  exposed-modules: Control.Parallel.Strategies.Lens Control.Seq.Lens
+
+  -- build-depends:   time == 1.4.*
+  -- exposed-modules: Data.Time.Calendar.Lens Data.Time.Clock.Lens
+
   other-extensions:
     CPP
     DeriveDataTypeable
@@ -205,6 +212,8 @@
 
   if (impl(ghc>=7.4))
     other-extensions: Trustworthy
+    build-depends: ghc-prim
+    exposed-modules: GHC.Generics.Lens
 
   ghc-options: -Wall -fwarn-tabs -O2 -fdicts-cheap -funbox-strict-fields
   hs-source-dirs: src
diff --git a/src/Control/Lens.hs b/src/Control/Lens.hs
--- a/src/Control/Lens.hs
+++ b/src/Control/Lens.hs
@@ -61,6 +61,8 @@
   -- ** Common Lenses
   , _1, _2
   , resultAt
+  , element
+  , elementOf
 
   -- * Isomorphisms
   , Iso
@@ -80,7 +82,7 @@
   , adjust, mapOf
   , set
   , whisper
-  , (^~), (%~)
+  , (^~), (%~), (<~)
   , (^=), (%=)
 
   -- * Getters and Folds
@@ -174,7 +176,7 @@
 import Prelude hiding ((.),id)
 
 infixl 8 ^.
-infixr 4 ^~, +~, *~, -~, //~, &&~, ||~, %~, <>~, %%~
+infixr 4 ^~, +~, *~, -~, //~, &&~, ||~, %~, <>~, %%~, <~
 infix  4 ^=, +=, *=, -=, //=, &&=, ||=, %=, <>=, %%=
 infixr 0 ^$
 
@@ -205,6 +207,16 @@
 --
 -- You can also use a 'Lens' for 'Getting' as if it were a 'Fold' or 'Getter'.
 --
+-- Since every lens is a valid 'Traversal', the traversal laws should also apply to any lenses you create.
+--
+-- 1.) Idiomatic naturality:
+--
+-- > l pure = pure
+--
+-- 2.) Sequential composition:
+--
+-- > fmap (l f) . l g = getCompose . l (Compose . fmap f . g)
+--
 -- > type Lens = forall f. Functor f => LensLike f a b c d
 type Lens a b c d = forall f. Functor f => (c -> f d) -> a -> f b
 
@@ -224,6 +236,22 @@
 -- Most of the time the 'Traversal' you will want to use is just 'traverse', but you can also pass any
 -- 'Lens' or 'Iso' as a Traversal, and composition of a 'Traversal' (or 'Lens' or 'Iso') with a 'Traversal' (or 'Lens' or 'Iso')
 -- using (.) forms a valid 'Traversal'.
+--
+-- The laws for a Traversal @t@ follow from the laws for Traversable as stated in \"The Essence of the Iterator Pattern\".
+--
+-- 1) Idiomatic naturality:
+--
+-- > t pure = pure
+--
+-- 2) Sequential composition:
+--
+-- > fmap (t f) . t g = getCompose . t (Compose . fmap f . g)
+--
+-- One consequence of this requirement is that a traversal needs to leave the same number of elements as a candidate for 
+-- subsequent traversal as it started with.
+--
+-- 3) No duplication of elements (as defined in \"The Essence of the Iterator Pattern\" section 5.5), which states
+-- that you should incur no effect caused by visiting the same element of the container twice.
 type Traversal a b c d = forall f. Applicative f => (c -> f d) -> a -> f b
 
 -- | A @'Simple' 'Lens'@, @'Simple' 'Traversal'@, ... can be used instead of a 'Lens','Traversal', ...
@@ -531,21 +559,27 @@
 --
 -- You can't 'view' a 'Setter' in general, so the other two laws are irrelevant.
 --
--- However, two Functor laws apply to a 'Setter'
+-- However, two functor laws apply to a 'Setter'
 --
 -- > adjust l id = id
 -- > adjust l f . adjust l g = adjust l (f . g)
 --
+-- These an be stated more directly:
+--
+-- > l Identity = Identity
+-- > l f . runIdentity . l g = l (f . runIdentity . g)
+--
 -- You can compose a 'Setter' with a 'Lens' or a 'Traversal' using @(.)@ from the Prelude
 -- and the result is always only a 'Setter' and nothing more.
 --
 -- > type Setter a b c d = LensLike Identity a b c d
 type Setter a b c d = (c -> Identity d) -> a -> Identity b
 
--- | This alias is supplied for those who don't want to use @LiberalTypeSynonyms@ with 'Simple'.
+-- | This alias is supplied for those who don't want to use @LiberalTypeSynonyms@ with
+-- 'Simple'.
 --
 -- > 'SimpleSetter ' = 'Simple' 'Setter'
-type SimpleSetter a b = Lens a a b b
+type SimpleSetter a b = Setter a a b b
 
 -- | This setter can be used to map over all of the values in a 'Functor'.
 --
@@ -641,20 +675,28 @@
 -- | Replace the target of a 'Lens' or all of the targets of a 'Setter'
 -- or 'Traversal' with a constant value.
 --
+-- This is an infix version of 'set', provided for consistency with '(^=)'
+(^~) :: Setter a b c d -> d -> a -> b
+(^~) = set
+{-# INLINE (^~) #-}
+
+-- | Replace the target of a 'Lens' or all of the targets of a 'Setter'
+-- or 'Traversal' with a constant value.
+--
 -- This is an infix version of 'set'
 --
--- > f <$ a = mapped ^~ f $ a
+-- > f <$ a = mapped <~ f $ a
 --
--- > ghci> bitAt 0 ^~ True $ 0
+-- > ghci> bitAt 0 <~ True $ 0
 -- > 1
 --
--- > (^~) :: Setter a b c d    -> d -> a -> b
--- > (^~) :: Iso a b c d       -> d -> a -> b
--- > (^~) :: Lens a b c d      -> d -> a -> b
--- > (^~) :: Traversal a b c d -> d -> a -> b
-(^~) :: Setter a b c d -> d -> a -> b
-(^~) = set
-{-# INLINE (^~) #-}
+-- > (<~) :: Setter a b c d    -> d -> a -> b
+-- > (<~) :: Iso a b c d       -> d -> a -> b
+-- > (<~) :: Lens a b c d      -> d -> a -> b
+-- > (<~) :: Traversal a b c d -> d -> a -> b
+(<~) :: Setter a b c d -> d -> a -> b
+(<~) = set
+{-# INLINE (<~) #-}
 
 -- | Increment the target(s) of a numerically valued 'Lens', Setter' or 'Traversal'
 --
@@ -714,7 +756,7 @@
 -- In practice the @b@ and @d@ are left dangling and unused, and as such is no real point in
 -- using a @'Simple' 'Getter'@.
 --
--- type Getter a c = forall r. LensLike (Const r) a b c d
+-- > type Getter a c = forall r. LensLike (Const r) a b c d
 type Getter a c = forall r b d. (c -> Const r d) -> a -> Const r b
 
 -- | Build a 'Getter' from an arbitrary Haskell function.
@@ -841,7 +883,27 @@
 _2 f (c,a) = (,) c <$> f a
 {-# INLINE _2 #-}
 
+-- | A 'Lens' to view/edit the nth element 'elementOf' a 'Traversal', 'Lens' or 'Iso'.
+--
+-- Attempts to access beyond the range of the 'Traversal' will cause an error.
+--
+-- > ghci> [[1],[3,4]]^.elementOf (traverse.traverse) 1
+-- > 3
+elementOf :: Functor f => LensLike (ElementOf f) a b c c -> Int -> LensLike f a b c c
+elementOf l i f a = case getElementOf (l go a) 0 of
+    Found _ fb -> fb
+    Searching _ _ -> error "elementOf: index out of range"
+  where
+    go c = ElementOf $ \j -> if i == j then Found (j + 1) (f c) else Searching (j + 1) c
 
+-- | Access the nth element of a 'Traversable' container.
+--
+-- Attempts to access beyond the range of the 'Traversal' will cause an error.
+--
+-- > element = elementOf traverse
+element :: Traversable t => Int -> Simple Lens (t a) a
+element = elementOf traverse
+
 -- | This lens can be used to change the result of a function but only where
 -- the arguments match the key given.
 resultAt :: Eq e => e -> Simple Lens (e -> a) a
@@ -945,6 +1007,9 @@
 -- > (^=) :: MonadState a m => Lens a a c d      -> d -> m ()
 -- > (^=) :: MonadState a m => Traversal a a c d -> d -> m ()
 -- > (^=) :: MonadState a m => Setter a a c d    -> d -> m ()
+--
+
+-- "It puts the state in the monad or it gets the hose again."
 (^=) :: MonadState a m => Setter a a c d -> d -> m ()
 l ^= b = State.modify (l ^~ b)
 {-# INLINE (^=) #-}
@@ -1045,14 +1110,14 @@
 folded = folds foldMap
 {-# INLINE folded #-}
 
--- | Obtain a 'Fold' by filtering a 'Lens', 'Iso', 'Getter, 'Fold' or 'Traversal'.
+-- | Obtain a 'Fold' by filtering a 'Lens', 'Iso', 'Getter', 'Fold' or 'Traversal'.
 filtered :: Monoid m => (c -> Bool) -> Getting m a b c d -> Getting m a b c d
 filtered p l f = l (\c -> if p c then f c else Const mempty)
 {-# INLINE filtered #-}
 
 -- | Obtain a 'Fold' by reversing the order of traversal for a 'Lens', 'Iso', 'Getter', 'Fold' or 'Traversal'.
 --
--- Of course, reversing a 'Fold' or 'Getter' has no effect.
+-- Of course, reversing a 'Lens', 'Iso' or 'Getter' has no effect.
 reversed :: Getting (Dual m) a b c d -> Getting m a b c d
 reversed l f = Const . getDual . getConst . l (Const .  Dual . getConst . f)
 {-# INLINE reversed #-}
@@ -1796,3 +1861,4 @@
 clone f cfd a = case f (IndexedStore id) a of
   IndexedStore db c -> db <$> cfd c
 {-# INLINE clone #-}
+
diff --git a/src/Control/Lens/Internal.hs b/src/Control/Lens/Internal.hs
--- a/src/Control/Lens/Internal.hs
+++ b/src/Control/Lens/Internal.hs
@@ -25,6 +25,8 @@
   , getMin
   , Max(..)
   , getMax
+  , ElementOf(..)
+  , ElementOfResult(..)
   ) where
 
 import Control.Applicative
@@ -117,4 +119,31 @@
 getMax :: Max a -> Maybe a
 getMax NoMax   = Nothing
 getMax (Max a) = Just a
+
+-- | The result of trying to find the nth element of a 'Traversal'.
+data ElementOfResult f a
+  = Searching {-# UNPACK #-} !Int a
+  | Found {-# UNPACK #-} !Int (f a)
+
+instance Functor f => Functor (ElementOfResult f) where
+  fmap f (Searching i a) = Searching i (f a)
+  fmap f (Found i as) = Found i (fmap f as)
+
+-- | Used to find the nth element of a 'Traversal'.
+data ElementOf f a = ElementOf { getElementOf :: Int -> ElementOfResult f a }
+
+instance Functor f => Functor (ElementOf f) where
+  fmap f (ElementOf m) = ElementOf $ \i -> case m i of
+    Searching j a -> Searching j (f a)
+    Found j as -> Found j (fmap f as)
+
+instance Functor f => Applicative (ElementOf f) where
+  pure a = ElementOf $ \i -> Searching i a
+  ElementOf mf <*> ElementOf ma = ElementOf $ \i -> case mf i of
+    Found j ff -> case ma j of
+      Found _ _ -> error "elementOf: found multiple results"
+      Searching k a -> Found k (fmap ($a) ff)
+    Searching j f -> case ma j of
+      Found k as -> Found k (fmap f as)
+      Searching k a -> Searching k (f a)
 
diff --git a/src/Control/Lens/Representable.hs b/src/Control/Lens/Representable.hs
--- a/src/Control/Lens/Representable.hs
+++ b/src/Control/Lens/Representable.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeOperators #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Control.Lens.Representable
@@ -58,6 +59,7 @@
   -- * Wrapped Representations
   , Key(..)
   , keys
+  , tabulated
   -- * Traversal with representation
   , mapWithRep
   , foldMapWithRep
@@ -71,6 +73,7 @@
   ) where
 
 import Control.Applicative
+import Control.Isomorphic
 import Control.Lens
 import Data.Foldable         as Foldable
 import Data.Functor.Identity
@@ -99,6 +102,7 @@
 class Functor f => Representable f where
   rep :: (Rep f -> a) -> f a
 
+
 instance Representable Identity where
   rep f = Identity (f (from identity))
 
@@ -189,11 +193,17 @@
 -- This type provides a way to, say, store a list of polymorphic lenses.
 newtype Key f = Key { turn :: Rep f }
 
--- | A 'Representable' 'Functor' has a fixed shape. This fills each position 
+-- | A 'Representable' 'Functor' has a fixed shape. This fills each position
 -- in it with a 'Key'
 keys :: Representable f => f (Key f)
 keys = rep Key
 {-# INLINE keys #-}
+
+-- | A version of 'rep' that is an isomorphism. Predicativity requires that
+-- we wrap the 'Rep' as a 'Key', however.
+tabulated :: Representable f => (Key f -> a) :~> f a
+tabulated = isomorphic (\f -> rep (f . Key)) (\fa key -> view (turn key) fa)
+{-# INLINE tabulated #-}
 
 -----------------------------------------------------------------------------
 -- Traversal
diff --git a/src/Control/Lens/TH.hs b/src/Control/Lens/TH.hs
--- a/src/Control/Lens/TH.hs
+++ b/src/Control/Lens/TH.hs
@@ -6,7 +6,7 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Control.Lens.TH
--- Copyright   :  (C) 2012 Edward Kmett, Dan Burton
+-- Copyright   :  (C) 2012 Edward Kmett
 -- License     :  BSD-style (see the file LICENSE)
 -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
 -- Stability   :  experimental
@@ -14,124 +14,233 @@
 --
 ----------------------------------------------------------------------------
 module Control.Lens.TH
-  (
+  ( LensRules(LensRules)
+  , isoLensRule
+  , fieldLensRule
+  , defaultLensRules
   -- ** Constructing Lenses Automatically
-    makeLenses
-  , makeLensesBy
+  , makeLenses
+  , makeLensesWith
   , makeLensesFor
   ) where
 
-import           Data.Char (toLower)
-import           Control.Applicative
-import           Language.Haskell.TH
+import Control.Applicative
+import Control.Lens
+import Data.Char (toLower)
+import Data.Foldable
+import Data.List as List
+import Data.Map as Map hiding (toList,map,filter)
+import Data.Map.Lens
+import Data.Maybe (isNothing)
+import Data.Monoid
+import Data.Set as Set hiding (toList,map,filter)
+import Data.Set.Lens
+import Data.Traversable
+import Language.Haskell.TH
+import Language.Haskell.TH.Lens
 
--------------------------------------
--- Constructing Lenses Automatically
--------------------------------------
+-- | This configuration describes the options we'll be using to make isomorphisms or lenses
+data LensRules = LensRules
+  { _isoLensRule   :: String -> Maybe String -- ^ used to name the top level isomorphism for single constructor, single field data types and newtypes
+  , _fieldLensRule :: String -> Maybe String -- ^ used to name the lens, given the name of the basic field
+  , _addBothLensRule :: Bool
+  }
 
--- | Derive lenses for the record selectors in
--- a single-constructor data declaration,
--- or for the record selector in a newtype declaration.
--- Lenses will only be generated for record fields which
--- are prefixed with an underscore.
---
--- Example usage:
---
--- > makeLenses ''Foo
-makeLenses :: Name -> Q [Dec]
-makeLenses = makeLensesBy defaultNameTransform
+-- | Lens to access the convention for naming top level isomorphisms in our lens rules
+isoLensRule :: Simple Lens LensRules (String -> Maybe String)
+isoLensRule f (LensRules i n b) = (\i' -> LensRules i' n b) <$> f i
 
--- | Derive lenses, specifying explicit pairings of @(fieldName, lensName)@.
---
--- Example usage:
---
--- > makeLensesFor [("_foo", "fooLens"), ("bar", "lbar")] ''Foo
-makeLensesFor :: [(String, String)] -> Name -> Q [Dec]
-makeLensesFor fields = makeLensesBy (`Prelude.lookup` fields)
+-- | Lens to access the convention for naming fields in our lens rules
+fieldLensRule :: Simple Lens LensRules (String -> Maybe String)
+fieldLensRule f (LensRules i n b) = (\n' -> LensRules i n' b) <$> f n
 
--- | Derive lenses with the provided name transformation
--- and filtering function. Produce @Just lensName@ to generate a lens
--- of the resultant name, or @Nothing@ to not generate a lens
--- for the input record name.
+-- | This flag indicates whether or not we should attempt to add both an isomorphism lens and a top level accessor
+addBothLensRule :: Simple Lens LensRules Bool
+addBothLensRule f (LensRules i n b) = LensRules i n <$> f b
+
+-- | Default lens rules
+defaultLensRules :: LensRules
+defaultLensRules = LensRules top field True where
+  top (c:cs) = Just (toLower c:cs)
+  top _      = Nothing
+  field ('_':c:cs) = Just (toLower c:cs)
+  field _          = Nothing
+
+-- | Given a set of names, build a map from those names to a set of fresh names based on them.
+freshMap :: Set Name -> Q (Map Name Name)
+freshMap ns = Map.fromList <$> for (toList ns) (\ n -> (,) n <$> newName (nameBase n))
+
+makeIsoTo :: Name -> ExpQ
+makeIsoTo conName = lamE [varP (mkName "f"), conP conName [varP (mkName "a")]] $
+  appsE [ varE (mkName "fmap")
+        , conE conName
+        , varE (mkName "f") `appE` varE (mkName "a")
+        ]
+
+makeIsoFrom :: Name -> ExpQ
+makeIsoFrom conName = lamE [varP (mkName "f"), varP (mkName "a")] $
+  appsE [ varE (mkName "fmap")
+        , lamE [conP conName [varP (mkName "b")]] $ varE (mkName "b")
+        , varE (mkName "f") `appE` (conE conName `appE` varE (mkName "a"))
+        ]
+
+makeIsoBody :: Name -> Name -> (Name -> ExpQ) -> (Name -> ExpQ) -> DecQ
+makeIsoBody lensName conName f g = funD lensName [clause [] (normalB body) []] where
+  body = appsE [ varE (mkName "isomorphic")
+               , f conName
+               , g conName
+               ]
+
+appArgs :: Type -> [TyVarBndr] -> Type
+appArgs t [] = t
+appArgs t (x:xs) = appArgs (AppT t (VarT (x^.name))) xs
+
+apps :: Type -> [Type] -> Type
+apps t [] = t
+apps t (x:xs) = apps (t `AppT` x) xs
+
+-- | Given
 --
--- Example usage:
+-- > newtype Cxt b => Foo a b c d = Foo { _baz :: Bar a b }
 --
--- > makeLensesBy (\n -> Just (n ++ "L")) ''Foo
-makeLensesBy ::
-     (String -> Maybe String) -- ^ the name transformer
-  -> Name -> Q [Dec]
-makeLensesBy nameTransform datatype = do
-  typeInfo          <- extractLensTypeInfo datatype
-  let derive1 = deriveLens nameTransform typeInfo
-  constructorFields <- extractConstructorFields datatype
-  Prelude.concat <$> Prelude.mapM derive1 constructorFields
+-- This will generate:
+--
+-- > foo :: (Cxt b, Cxt f) => Iso (Foo a b c d) (Foo e f g h) (Bar a b) (Bar e f)
+-- > foo = isomorphic (\f a -> (\(Foo b) -> b) <$> f (Foo a))
+-- >                  (\f (Foo a) -> fmap Foo (f a))
+-- > {-# INLINE foo #-}
 
-------------------------------------------------------------------------------
--- Template Haskell Implementation Details
-------------------------------------------------------------------------------
+-- > baz :: (Cxt b, Cxt f) => Iso (Bar a b) (Bar e f) (Foo a b c d) (Foo e f g h)
+-- > baz = isomorphic (\f (Foo a) -> fmap Foo (f a))
+-- >                  (\f a -> fmap (\(Foo b) -> b) (f (Foo a)))
+-- > {-# INLINE baz #-}
+makeIso :: LensRules
+        -> Cxt
+        -> Name
+        -> [TyVarBndr]
+        -> Name
+        -> Maybe Name
+        -> Type
+        -> Q [Dec]
+makeIso cfg ctx tyConName tyArgs dataConName maybeFieldName partTy = do
+  m <- freshMap $ setOf typeVars tyArgs
+  let aty = partTy
+      bty = substTypeVars m aty
+      cty = appArgs (ConT tyConName) tyArgs
+      dty = substTypeVars m cty
+      quantified = ForallT (tyArgs ++ substTypeVars m tyArgs) (ctx ++ substTypeVars m ctx)
+      maybeIsoName = mkName <$> view isoLensRule cfg (nameBase dataConName)
+  isoDecls <- flip (maybe (return [])) maybeIsoName $ \isoName -> do
+    let decl = SigD isoName $ quantified $
+                 ConT (mkName "Control.Lens.Iso") `apps` [aty,bty,cty,dty]
+    body <- makeIsoBody isoName dataConName makeIsoFrom makeIsoTo
+    inlining <- pragInlD isoName (inlineSpecNoPhase True False)
+    return [decl, body, inlining]
+  accessorDecls <- case mkName <$> (maybeFieldName >>= view fieldLensRule cfg . nameBase) of
+    jfn@(Just lensName)
+      | (jfn /= maybeIsoName) && (isNothing maybeIsoName || view addBothLensRule cfg) -> do
+      let decl = SigD lensName $ quantified $
+                   ConT (mkName "Control.Lens.Iso") `apps` [cty,dty,aty,bty]
+      body <- makeIsoBody lensName dataConName makeIsoTo makeIsoFrom
+      inlining <- pragInlD lensName (inlineSpecNoPhase True False)
+      return [decl, body, inlining]
+    _ -> return []
+  return $ isoDecls ++ accessorDecls
 
--- | By default, if the field name begins with an underscore,
--- then the underscore will simply be removed (and the new first character
--- lowercased if necessary).
-defaultNameTransform :: String -> Maybe String
-defaultNameTransform ('_':c:rest) = Just $ toLower c : rest
-defaultNameTransform _ = Nothing
+data FieldDesc = FieldDesc
+  { _fieldName                   :: Name
+  , _fieldType                   :: Type
+  , _fieldTypeVarsBoundElsewhere :: Set Name
+  }
 
--- | Information about the larger type the lens will operate on.
-type LensTypeInfo = (Name, [TyVarBndr])
+thd :: (a,b,c) -> c
+thd (_,_,c) = c
 
--- | Information about the smaller type the lens will operate on.
-type ConstructorFieldInfo = (Name, Strict, Type)
+fieldDescs :: Set Name -> [(Name,Strict,Type)] -> [FieldDesc]
+fieldDescs acc ((nm,_,ty):rest) = FieldDesc nm ty (acc <> setOf typeVars (map thd rest)) : fieldDescs (acc <> setOf typeVars ty) rest
+fieldDescs _ [] = []
 
-extractLensTypeInfo :: Name -> Q LensTypeInfo
-extractLensTypeInfo datatype = do
-  let datatypeStr = nameBase datatype
-  i <- reify datatype
-  return $ case i of
-    TyConI (DataD    _ n ts _ _) -> (n, ts)
-    TyConI (NewtypeD _ n ts _ _) -> (n, ts)
-    _ -> error $ "Can't derive Lens for: "  ++ datatypeStr ++ ", type name required."
+conFieldDescs :: Con -> [FieldDesc]
+conFieldDescs (RecC _ fields) = fieldDescs mempty fields
+conFieldDescs _ = []
 
-extractConstructorFields :: Name -> Q [ConstructorFieldInfo]
-extractConstructorFields datatype = do
-  let datatypeStr = nameBase datatype
-  i <- reify datatype
-  return $ case i of
-    TyConI (DataD    _ _ _ [RecC _ fs] _) -> fs
-    TyConI (NewtypeD _ _ _ (RecC _ fs) _) -> fs
-    TyConI (DataD    _ _ _ [_]         _) -> error $ "Can't derive Lens without record selectors: " ++ datatypeStr
-    TyConI NewtypeD{} -> error $ "Can't derive Lens without record selectors: " ++ datatypeStr
-    TyConI TySynD{}   -> error $ "Can't derive Lens for type synonym: " ++ datatypeStr
-    TyConI DataD{}    -> error $ "Can't derive Lens for tagged union: " ++ datatypeStr
-    _                 -> error $ "Can't derive Lens for: "  ++ datatypeStr ++ ", type name required."
+commonFieldDescs :: [Con] -> [FieldDesc]
+commonFieldDescs = toList . Prelude.foldr walk mempty where
+  walk con m = Prelude.foldr step m (conFieldDescs con)
+  step d@(FieldDesc nm ty bds) m = case m^.at nm of
+    Just (FieldDesc _ _ bds') -> at nm <~ Just (FieldDesc nm ty (bds <> bds')) $ m
+    Nothing                   -> at nm <~ Just d                               $ m
 
--- Derive a lens for the given record selector
--- using the given name transformation function.
-deriveLens :: (String -> Maybe String)
-           -> LensTypeInfo
-           -> ConstructorFieldInfo
-           -> Q [Dec]
-deriveLens nameTransform ty field = case nameTransform (nameBase fieldName) of
-  Nothing          -> return []
-  Just lensNameStr -> do
-    body <- deriveLensBody (mkName lensNameStr) fieldName
-    return [body]
-  where
-    (fieldName, _fieldStrict, _fieldType) = field
-    (_tyName, _tyVars) = ty  -- just to clarify what's here
+errorClause :: Name -> Name -> Name -> ClauseQ
+errorClause lensName fieldName conName = clause [] (normalB (varE (mkName "error") `appE` litE (stringL err))) [] where
+  err = show lensName ++ ": no matching field " ++ show fieldName ++ " in constructor " ++ show conName
 
--- Given a record field name,
--- produces a single function declaration:
--- lensName f a = (\x -> a { field = x }) `fmap` f (field a)
-deriveLensBody :: Name -> Name -> Q Dec
-deriveLensBody lensName fieldName = funD lensName [defLine]
-  where
-    a = mkName "a"
-    f = mkName "f"
-    defLine = clause pats (normalB body) []
-    pats = [varP f, varP a]
-    body = [| (\x -> $(record a fieldName [|x|]))
-              `fmap` $(appE (varE f) (appE (varE fieldName) (varE a)))
-            |]
-    record rec fld val = val >>= \v -> recUpdE (varE rec) [return (fld, v)]
+makeFieldLensBody :: Name -> Name -> [Con] -> Q Dec
+makeFieldLensBody lensName fieldName = funD lensName . map clauses where
+  clauses (RecC conName fields) = case List.findIndex (\(n,_,_) -> n == fieldName) fields of
+    Just i -> do
+      names  <- for fields $ \(n,_,_) -> newName (nameBase n)
+      f      <- newName "f"
+      nm     <- newName "x"
+      clause [varP f, conP conName $ map varP names] (normalB
+             (appsE [ varE (mkName "fmap")
+                    , lamE [varP nm] $ appsE (conE conName : map varE (element i <~ nm $ names))
+                    , varE (mkName "f") `appE` varE (names^.element i)
+                    ])) []
+    Nothing -> errorClause lensName fieldName conName
+  clauses con = errorClause lensName fieldName (con^.name)
 
+-- TODO: When there are constructors with missing fields, turn that field into a _traversal_ not a lens.
+-- TODO: When the supplied mapping function maps multiple different fields to the same name, try to unify them into a Traversal.
+makeFieldLenses :: LensRules
+                -> Cxt         -- ^ surrounding cxt driven by the data type context
+                -> Name        -- ^ data/newtype constructor name
+                -> [TyVarBndr] -- ^ args
+                -> [Con]
+                -> Q [Dec]
+makeFieldLenses cfg ctx tyConName tyArgs cons = do
+  let aty = appArgs (ConT tyConName) tyArgs
+      vs = setOf typeVars tyArgs
+      fieldMap = commonFieldDescs cons
+  fmap Prelude.concat . for (toList fieldMap) $ \ (FieldDesc nm cty bds) ->
+     case mkName <$> view fieldLensRule cfg (nameBase nm) of
+       Nothing -> return []
+       Just lensName -> do
+         m <- freshMap $ Set.difference vs bds
+         let bty = substTypeVars m aty
+             dty = substTypeVars m cty
+             s = setOf folded m -- get the target values
+             relevantBndr b = s^.contains (b^.name)
+             relevantCtx = not . Set.null . Set.intersection s . setOf typeVars
+             tvs = tyArgs ++ filter relevantBndr (substTypeVars m tyArgs)
+             ps = ctx ++ filter relevantCtx (substTypeVars m ctx)
+         let decl = SigD lensName $ ForallT tvs ps $ ConT (mkName "Control.Lens.Lens") `apps` [aty,bty,cty,dty]
+         body <- makeFieldLensBody lensName nm cons
+         inlining <- pragInlD lensName (inlineSpecNoPhase True False)
+         return [decl, body, inlining]
+
+-- | Build lenses with a custom configuration
+makeLensesWith :: LensRules -> Name -> Q [Dec]
+makeLensesWith cfg nm = reify nm >>= \inf -> case inf of
+  TyConI dt -> case dt of
+    NewtypeD ctx tyConName args (NormalC dataConName [(_,ty)])  _ -> makeIso cfg ctx tyConName args dataConName Nothing ty
+    DataD    ctx tyConName args [NormalC dataConName [(_,ty)]]  _ -> makeIso cfg ctx tyConName args dataConName Nothing ty
+    NewtypeD ctx tyConName args (RecC dataConName [(fld,_,ty)]) _ -> makeIso cfg ctx tyConName args dataConName (Just fld) ty
+    DataD    ctx tyConName args [RecC dataConName [(fld,_,ty)]] _ -> makeIso cfg ctx tyConName args dataConName (Just fld) ty
+    DataD    ctx tyConName args dataCons _                        -> makeFieldLenses cfg ctx tyConName args dataCons
+    _ -> error "Unsupported data type"
+  _ -> error "Expected the name of a data type or newtype"
+
+-- | Build lenses with a sensible default configuration
+makeLenses :: Name -> Q [Dec]
+makeLenses = makeLensesWith defaultLensRules
+
+-- | Derive lenses, specifying explicit pairings of @(fieldName, lensName)@.
+--
+-- Example usage:
+--
+-- > makeLensesFor [("_foo", "fooLens"), ("bar", "lbar")] ''Foo
+makeLensesFor :: [(String, String)] -> Name -> Q [Dec]
+makeLensesFor fields = makeLensesWith $ fieldLensRule <~ (`Prelude.lookup` fields)
+                                      $ isoLensRule <~ const Nothing
+                                      $ defaultLensRules
diff --git a/src/Data/Array/Lens.hs b/src/Data/Array/Lens.hs
--- a/src/Data/Array/Lens.hs
+++ b/src/Data/Array/Lens.hs
@@ -52,8 +52,13 @@
 -- | This setter can be used to derive a new array from an old array by
 -- applying a function to each of the indices.
 --
+-- This is a /contravariant/ Setter.
+--
 -- > ixmap = adjust . ixmapped
 -- > ixmapped = sets . ixmap
+--
+-- > adjust (ixmapped b) f arr ! i = arr ! f i
+-- > bounds (adjust (ixmapped b) f arr) = b
 ixmapped :: (IArray a e, Ix i, Ix j) => (i,i) -> Setter (a j e) (a i e) i j
 ixmapped = sets . ixmap
 {-# INLINE ixmapped #-}
diff --git a/src/Data/IntSet/Lens.hs b/src/Data/IntSet/Lens.hs
--- a/src/Data/IntSet/Lens.hs
+++ b/src/Data/IntSet/Lens.hs
@@ -11,10 +11,11 @@
 module Data.IntSet.Lens
   ( contains
   , members
+  , setOf
   ) where
 
+import Control.Applicative
 import Control.Lens
-import Data.Functor
 import Data.IntSet as IntSet
 
 -- | This 'Lens' can be used to read, write or delete a member of an 'IntSet'
@@ -40,3 +41,13 @@
 -- > fromList [2,3,4,5]
 members :: Setter IntSet IntSet Int Int
 members = sets IntSet.map
+
+-- | Construct an 'IntSet' from a 'Getter', 'Fold', 'Traversal', 'Lens' or 'Iso'.
+--
+-- > setOf :: Getter a Int        -> a -> IntSet
+-- > setOf :: Fold a Int          -> a -> IntSet
+-- > setOf :: Iso a b Int d       -> a -> IntSet
+-- > setOf :: Lens a b Int d      -> a -> IntSet
+-- > setOf :: Traversal a b Int d -> a -> IntSet
+setOf :: Getting IntSet a b Int d -> a -> IntSet
+setOf l = getConst . l (Const . IntSet.singleton)
diff --git a/src/Data/Set/Lens.hs b/src/Data/Set/Lens.hs
--- a/src/Data/Set/Lens.hs
+++ b/src/Data/Set/Lens.hs
@@ -11,11 +11,12 @@
 module Data.Set.Lens
   ( contains
   , members
+  , setOf
   ) where
 
+import Control.Applicative
 import Control.Lens
 import Data.Set as Set
-import Data.Functor
 
 -- | This 'Lens' can be used to read, write or delete a member of a 'Set'
 --
@@ -39,3 +40,13 @@
 -- > fromList [2,3,4,5]
 members :: (Ord i, Ord j) => Setter (Set i) (Set j) i j
 members = sets Set.map
+
+-- | Construct a set from a 'Getter', 'Fold', 'Traversal', 'Lens' or 'Iso'.
+--
+-- > setOf ::          Getter a c        -> a -> Set c
+-- > setOf :: Ord c => Fold a c          -> a -> Set c
+-- > setOf ::          Iso a b c d       -> a -> Set c
+-- > setOf ::          Lens a b c d      -> a -> Set c
+-- > setOf :: Ord c => Traversal a b c d -> a -> Set c
+setOf :: Getting (Set c) a b c d -> a -> Set c
+setOf l = getConst . l (Const . Set.singleton)
diff --git a/src/Data/Time/Calendar/Lens.hs b/src/Data/Time/Calendar/Lens.hs
deleted file mode 100644
--- a/src/Data/Time/Calendar/Lens.hs
+++ /dev/null
@@ -1,179 +0,0 @@
-{-# LANGUAGE TemplateHaskell #-}
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE LiberalTypeSynonyms #-}
------------------------------------------------------------------------------
--- |
--- Module      :  Data.Time.Calendar.Lens
--- Copyright   :  (C) 2012 Edward Kmett
--- License     :  BSD-style (see the file LICENSE)
--- Maintainer  :  Edward Kmett <ekmett@gmail.com>
--- Stability   :  provisional
--- Portability :  LiberalTypeSynonyms
---
--- Provides fairly ad hoc overloading to access different notions of a 'Day'.
---
--- To convert from a 'Day':
---
--- > myDay^.gregorian.year
--- > myDay^.julian.year
---
-----------------------------------------------------------------------------
-module Data.Time.Calendar.Lens
-  ( modifiedJulianDay
-  , TraverseDay(..)
-  , HasYear(..)
-  , HasMonth(..)
-  , HasWeek(..)
-  , HasDay(..)
-  , Gregorian(..)
-  , gregorian
-  , JulianYearAndDay(..)
-  , julianYearAndDay
-  , WeekDate(..)
-  , weekDate
-  , OrdinalDate(..)
-  , ordinalDate
-  ) where
-
-import Control.Applicative
-import Control.Lens
-import Data.Data
-import Data.Time.Calendar
-import Data.Time.Calendar.Julian
-import Data.Time.Calendar.WeekDate
-import Data.Time.Calendar.OrdinalDate
-
--- | Provide ad hoc overloading for traversing the modified Julian day
-class TraverseDay t where
-  -- | Convert the type to a modified Julian day if possible and traverse it.
-  --
-  -- Traverses nothing if the date isn't valid.
-  traverseDay :: Simple Traversal t Day
-
--- | Returns the modified Julian Day as a standard count of days,
--- with zero being the day 1858-11-17.
-modifiedJulianDay :: Simple Iso Day Integer
-modifiedJulianDay = iso toModifiedJulianDay ModifiedJulianDay
-
-instance TraverseDay Day where
-  traverseDay = id
-
--- | Ad hoc overloading for accessing the year
-class HasYear t where
-  -- | Get the year of a date
-  year :: Simple Lens t Integer
-
--- | Ad hoc overloading for accessing the month
-class HasMonth t where
-  -- | Get the month of a date
-  month :: Simple Lens t Int
-
--- | Ad hoc overloading for accessing the week (what it is relative to may vary from type to type)
-class HasWeek t where
-  -- | Get the week of a date
-  week :: Simple Lens t Int
-
--- | Ad hoc overloading for accessing the day (what it is relative to may vary from type to type)
-class HasDay t where
-  -- | Get the day of a date
-  day :: Simple Lens t Int
-
--- | Date in the proleptic Gregorian calendar.
-data Gregorian = Gregorian
-  { gregorianYear :: !Integer -- ^ year
-  , gregorianMonth :: !Int    -- ^ month (1-12)
-  , gregorianDay :: !Int      -- ^ day   (1-31)
-  } deriving (Eq,Ord,Show,Read,Typeable,Data)
-
-uncurry3 :: (a -> b -> c -> d) -> (a,b,c) -> d
-uncurry3 f (a,b,c) = f a b c
-
--- | Convert to/from a /valid/ date in the proleptic Gregorian calendar
-gregorian :: Simple Iso Day Gregorian
-gregorian = iso (uncurry3 Gregorian . toGregorian) $ \(Gregorian y m d) -> fromGregorian y m d
-
-instance TraverseDay Gregorian where
-  traverseDay f g@(Gregorian y m d) = case fromGregorianValid y m d of
-    Nothing -> pure g
-    Just j -> (\i -> case toGregorian i of (y', m', d') -> Gregorian y' m' d') <$> f j
-
-instance HasYear Gregorian where
-  year f (Gregorian y m d) = (\y' -> Gregorian y' m d) <$> f y
-
-instance HasMonth Gregorian where
-  month f (Gregorian y m d) = (\m' -> Gregorian y m' d) <$> f m
-
--- | Day of month
-instance HasDay Gregorian where
-  day f (Gregorian y m d) = Gregorian y m <$> f d
-
--- | Proleptic Julian year and day format.
-data JulianYearAndDay = JulianYearAndDay
-  { julianYearAndDayYear :: !Integer -- ^ year (in the proleptic Julian calendar)
-  , julianYearAndDayDay  :: !Int     -- ^ day of the year, with 1 for Jan 1, and 365 (or 366 in leap years) for Dec 31.
-  } deriving (Eq,Ord,Show,Read,Typeable,Data)
-
--- | Convert to/from a /valid/ proleptic Julian year and day.
-julianYearAndDay :: Simple Iso Day JulianYearAndDay
-julianYearAndDay = iso (uncurry JulianYearAndDay . toJulianYearAndDay) $ \(JulianYearAndDay y d) -> fromJulianYearAndDay y d
-
-instance TraverseDay JulianYearAndDay where
-  traverseDay f j@(JulianYearAndDay y d) = case fromJulianYearAndDayValid y d of
-    Nothing -> pure j
-    Just k -> (\i -> case toJulianYearAndDay i of (y', d') -> JulianYearAndDay y' d') <$> f k
-
-instance HasYear JulianYearAndDay where
-  year f (JulianYearAndDay y d) = (`JulianYearAndDay` d) <$> f y
-
--- | Day of year
-instance HasDay JulianYearAndDay where
-  day f (JulianYearAndDay y d) = JulianYearAndDay y <$> f d
-
--- | ISO 8601 Week Date format.
---
--- The first week of a year is the first week to contain at least four days in the corresponding Gregorian year.
-data WeekDate = WeekDate 
-  { weekDateYear :: !Integer -- ^ year. Note: that "Week" years are not quite the same as Gregorian years, as the first day of the year is always a Monday.
-  , weekDateWeek :: !Int -- ^ week number (1-53)
-  , weekDateDay  :: !Int -- ^ day of week (1 for Monday to 7 for Sunday).
-  } deriving (Eq,Ord,Show,Read,Typeable,Data)
-
--- | Convert to/from a valid WeekDate
-weekDate :: Simple Iso Day WeekDate
-weekDate = iso (uncurry3 WeekDate . toWeekDate) $ \(WeekDate y w d) -> fromWeekDate y w d
-
-instance TraverseDay WeekDate where
-  traverseDay f wd@(WeekDate y w d) = case fromWeekDateValid y w d of
-    Nothing -> pure wd
-    Just k -> (\i -> case toWeekDate i of (y', w', d') -> WeekDate y' w' d') <$> f k
-
-instance HasYear WeekDate where
-  year f (WeekDate y w d) = (\y' -> WeekDate y' w d) <$> f y
-
-instance HasWeek WeekDate where
-  week f (WeekDate y w d) = (\w' -> WeekDate y w' d) <$> f w
-
--- | Day of week
-instance HasDay WeekDate where
-  day f (WeekDate y w d) = WeekDate y w <$> f d
-
--- | ISO 8601 Ordinal Date format
-data OrdinalDate = OrdinalDate
-  { ordinalDateYear :: !Integer -- ^ year (proleptic Gregorian calendar)
-  , ordinalDateDay  :: !Int     -- ^ day of the year, with 1 for Jan 1, and 365 (or 366 in leap years) for Dec 31.
-  } deriving (Eq,Ord,Show,Read,Typeable,Data)
-
--- | Convert to/from a valid ISO 8601 Ordinal Date format.
-ordinalDate :: Simple Iso Day OrdinalDate
-ordinalDate = iso (uncurry OrdinalDate . toOrdinalDate) $ \(OrdinalDate y d) -> fromOrdinalDate y d
-
-instance TraverseDay OrdinalDate where
-  traverseDay f od@(OrdinalDate y d) = case fromOrdinalDateValid y d of
-    Nothing -> pure od
-    Just k -> (\i -> case toOrdinalDate i of (y', d') -> OrdinalDate y' d') <$> f k
-
-instance HasYear OrdinalDate where
-  year f (OrdinalDate y d) = (`OrdinalDate` d) <$> f y
-
-instance HasDay OrdinalDate where
-  day f (OrdinalDate y d) = OrdinalDate y <$> f d
diff --git a/src/GHC/Generics/Lens.hs b/src/GHC/Generics/Lens.hs
new file mode 100644
--- /dev/null
+++ b/src/GHC/Generics/Lens.hs
@@ -0,0 +1,25 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  GHC.Generics.Lens
+-- Copyright   :  (C) 2012 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  experimental
+-- Portability :  GHC
+--
+----------------------------------------------------------------------------
+module GHC.Generics.Lens
+  ( generic
+  , generic1
+  ) where
+
+import Control.Lens hiding (from, to)
+import GHC.Generics
+
+-- | Convert from the data type to its representation (or back)
+generic :: (Generic a, Generic b) => Iso a b (Rep a x) (Rep b y)
+generic = isos from to from to
+
+-- | Convert from the data type to its representation (or back)
+generic1 :: (Generic1 f, Generic1 g) => Iso (f a) (g b) (Rep1 f a) (Rep1 g b)
+generic1 = isos from1 to1 from1 to1
diff --git a/src/Language/Haskell/TH/Lens.hs b/src/Language/Haskell/TH/Lens.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Haskell/TH/Lens.hs
@@ -0,0 +1,106 @@
+{-# LANGUAGE TemplateHaskell #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Language.Haskell.TH.Lens
+-- Copyright   :  (C) 2012 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  experimental
+-- Portability :  TemplateHaskell
+--
+-- Lenses and Traversals for working with Template Haskell
+----------------------------------------------------------------------------
+module Language.Haskell.TH.Lens
+  ( HasName(..)
+  , HasTypeVars(..)
+  , SubstType(..)
+  , typeVars      -- :: HasTypeVars t => Simple Traversal t Name
+  , substTypeVars -- :: HasTypeVars t => Map Name Name -> t -> t
+  ) where
+
+import Control.Applicative
+import Control.Lens
+import Data.Map as Map hiding (toList,map)
+import Data.Map.Lens
+import Data.Maybe (fromMaybe)
+import Data.Monoid
+import Data.Set as Set hiding (toList,map)
+import Data.Set.Lens
+import Language.Haskell.TH
+
+-- | Has a 'Name'
+class HasName t where
+  -- | Extract (or modify) the 'Name' of something
+  name :: Simple Lens t Name
+
+instance HasName TyVarBndr where
+  name f (PlainTV n) = PlainTV <$> f n
+  name f (KindedTV n k) = (`KindedTV` k) <$> f n
+
+instance HasName Name where
+  name = id
+
+instance HasName Con where
+  name f (NormalC n tys)       = (`NormalC` tys) <$> f n
+  name f (RecC n tys)          = (`RecC` tys) <$> f n
+  name f (InfixC l n r)        = (\n' -> InfixC l n' r) <$> f n
+  name f (ForallC bds ctx con) = ForallC bds ctx <$> name f con
+
+-- | Provides for the extraction of free type variables, and alpha renaming.
+class HasTypeVars t where
+  -- | When performing substitution into this traversal you're not allowed
+  -- to substitute in a name that is bound internally or you'll violate
+  -- the 'Traversal' laws, when in doubt generate your names with 'newName'.
+  typeVarsEx :: Set Name -> Simple Traversal t Name
+
+instance HasTypeVars TyVarBndr where
+  typeVarsEx s f b
+    | s^.contains (b^.name) = pure b
+    | otherwise             = name f b
+
+instance HasTypeVars Name where
+  typeVarsEx s f n
+    | s^.contains n = pure n
+    | otherwise     = f n
+
+instance HasTypeVars Type where
+  typeVarsEx s f (VarT n)            = VarT <$> typeVarsEx s f n
+  typeVarsEx s f (AppT l r)          = AppT <$> typeVarsEx s f l <*> typeVarsEx s f r
+  typeVarsEx s f (SigT t k)          = (`SigT` k) <$> typeVarsEx s f t
+  typeVarsEx s f (ForallT bs ctx ty) = ForallT bs <$> typeVarsEx s' f ctx <*> typeVarsEx s' f ty
+       where s' = s <> foldMapOf typeVars Set.singleton bs
+  typeVarsEx _ _ t                   = pure t
+
+instance HasTypeVars Pred where
+  typeVarsEx s f (ClassP n ts) = ClassP n <$> typeVarsEx s f ts
+  typeVarsEx s f (EqualP l r)  = EqualP <$> typeVarsEx s f l <*> typeVarsEx s f r
+
+instance HasTypeVars t => HasTypeVars [t] where
+  typeVarsEx s = traverse . typeVarsEx s
+
+-- | Traverse /free/ type variables
+typeVars :: HasTypeVars t => Simple Traversal t Name
+typeVars = typeVarsEx mempty
+
+-- | Substitute using a map of names in for /free/ type variables
+substTypeVars :: HasTypeVars t => Map Name Name -> t -> t
+substTypeVars m = mapOf typeVars $ \n -> fromMaybe n (m^.at n)
+
+-- | Provides substitution for types
+class SubstType t where
+  -- | Perform substitution for types
+  substType :: Map Name Type -> t -> t
+
+instance SubstType Type where
+  substType m t@(VarT n)          = fromMaybe t (m^.at n)
+  substType m (ForallT bs ctx ty) = ForallT bs (substType m ctx) (substType m ty)
+  substType m (SigT t k)          = SigT (substType m t) k
+  substType m (AppT l r)          = AppT (substType m l) (substType m r)
+  substType _ t                   = t
+
+instance SubstType t => SubstType [t] where
+  substType = map . substType
+
+instance SubstType Pred where
+  substType m (ClassP n ts) = ClassP n (substType m ts)
+  substType m (EqualP l r)  = substType m (EqualP l r)