diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,16 @@
-# Revision history for generic-lens
+## 0.5.0.0
 
-## 0.1.0.0  -- YYYY-mm-dd
+- Lenses and prisms are now type-changing.
+- More informative error messages
+- More readable type signatures in type errors and when using `:t`
+- Use `doctest`
+- Include examples in Haddock
 
-* First version. Released on an unsuspecting world.
+### Breaking API changes
+
+- The type parameters of the classes have been changed to accommodate
+  the type-changing update:
+  
+  `class HasField name a s` -> `class HasField name s t a b` etc.
+  
+  Accordingly, `field :: Lens' s a` -> `field :: Lens s t a b`
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,7 +1,6 @@
 # generic-lens
 
-[![Build
-Status](https://travis-ci.org/kcsongor/generic-lens.svg?branch=master)](https://travis-ci.org/kcsongor/generic-lens)
+[![Build Status](https://travis-ci.org/kcsongor/generic-lens.svg?branch=master)](https://travis-ci.org/kcsongor/generic-lens)
 [![Hackage](https://img.shields.io/hackage/v/generic-lens.svg)](https://hackage.haskell.org/package/generic-lens)
 
 Generically derive lenses and prisms for data types.
@@ -48,6 +47,23 @@
 >>> sally ^. field @"pet"
 error:
   • The type Person does not contain a field named "pet"
+```
+
+If the accessed field is a type parameter that appears uniquely in the type,
+then its type can be changed:
+
+```haskell
+data T a b c d = T
+  { paramA :: a
+  , paramB :: b
+  , paramC :: c
+  , paramD :: d
+  }
+  deriving (Generic, Show)
+
+>>> t = T "a" (10 :: Int) 'c' False
+>>> t & field @"paramA" .~ 'a' & field @"paramB" .~ False
+T {paramA = 'a', paramB = False, paramC = 'c', paramD = False}
 ```
 
 ### Positional fields
diff --git a/examples/Examples.hs b/examples/Examples.hs
--- a/examples/Examples.hs
+++ b/examples/Examples.hs
@@ -1,17 +1,25 @@
-{-# LANGUAGE DataKinds             #-}
-{-# LANGUAGE DeriveGeneric         #-}
-{-# LANGUAGE DuplicateRecordFields #-}
-{-# LANGUAGE FlexibleContexts      #-}
-{-# LANGUAGE TypeApplications      #-}
-{-# LANGUAGE UndecidableInstances  #-}
-
-{-# OPTIONS_GHC -fno-warn-unused-imports  #-}
+{-# LANGUAGE AllowAmbiguousTypes         #-}
+{-# LANGUAGE DataKinds                   #-}
+{-# LANGUAGE DeriveGeneric               #-}
+{-# LANGUAGE DuplicateRecordFields       #-}
+{-# LANGUAGE FlexibleContexts            #-}
+{-# LANGUAGE GADTs                       #-}
+{-# LANGUAGE NoMonomorphismRestriction   #-}
+{-# LANGUAGE PartialTypeSignatures       #-}
+{-# LANGUAGE Rank2Types                  #-}
+{-# LANGUAGE ScopedTypeVariables         #-}
+{-# LANGUAGE TypeApplications            #-}
+{-# LANGUAGE UndecidableInstances        #-}
+{-# OPTIONS_GHC -Wno-missing-signatures  #-}
+{-# OPTIONS_GHC -fno-warn-unused-imports #-}
 
 module Examples where
 
-import GHC.Generics
+import Data.Function ((&))
+import Data.Generics.Internal.Lens
 import Data.Generics.Product
---import Control.Lens
+import Data.Generics.Sum
+import GHC.Generics
 
 data Animal = Animal
   { name :: String
@@ -41,3 +49,56 @@
 
 --g :: Subtype s MyRecord => s -> String
 --g s = s ^. super @MyRecord . label @"field2"
+
+data Test a b = Test { fieldInt :: Int, fieldA :: a, fieldB :: b } deriving (Generic, Show)
+
+-- changedA :: Test Int String
+-- >>> changedA
+-- Test {fieldInt = 10, fieldA = 10, fieldB = "world"}
+changedA = Test 10 "hello" "world" & field @"fieldA" .~ (10 :: Int)
+
+-- changedB :: Test String Int
+-- >>> changedB
+-- Test {fieldInt = 10, fieldA = "hello", fieldB = 10}
+changedB = (Test 10 "hello" "world") & field @"fieldB" .~ (10 :: Int)
+
+--changedInt = set (field @"fieldInt") ("hello") (Test 10 "hello" "world")
+-- type error
+
+data Animal2 a
+  = Dog (Dog a)
+  | Cat Name Age
+  | Duck Age
+  deriving (Generic, Show)
+
+data Dog a
+  = MkDog
+  { name   :: Name
+  , age    :: Age
+  , fieldA :: a
+  }
+  deriving (Generic, Show)
+type Name = String
+type Age  = Int
+dog :: Animal2 Int
+dog = Dog (MkDog "Shep" 3 30)
+
+-- TODO: the error message for this case is ugly
+-- data Dog a
+--   = MkDog
+--   { name    :: Name
+--   , age     :: Age
+--   , fieldA  :: a
+--   , fieldA' :: a
+--   }
+--   deriving (Generic, Show)
+
+--dog' :: Animal2 String
+dog' = dog & _Ctor @"Dog" . field @"fieldA" .~ "now it's a String"
+
+stuff ::
+  ( HasPosition 15 s t a String
+  , HasField "test" s' t' a' b'
+  , HasField "bar" a' b' s t
+  ) => s' -> t'
+stuff r = r & field @"test" . field @"bar" . position @15 .~ "hello"
diff --git a/examples/StarWars.hs b/examples/StarWars.hs
--- a/examples/StarWars.hs
+++ b/examples/StarWars.hs
@@ -59,7 +59,7 @@
   , primaryFunction = "protocol and human relations"
   }
 
-getName :: HasField "name" a r => r -> a
+getName :: HasField' "name" r a => r -> a
 getName = getField @"name"
 
 -- upcast :: Subtype a b => a -> b
diff --git a/generic-lens.cabal b/generic-lens.cabal
--- a/generic-lens.cabal
+++ b/generic-lens.cabal
@@ -1,5 +1,5 @@
 name:                 generic-lens
-version:              0.4.1.0
+version:              0.5.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.
 
@@ -11,6 +11,7 @@
 category:             Generics, Records, Lens
 build-type:           Simple
 cabal-version:        >= 1.10
+Tested-With:          GHC == 8.0.2, GHC == 8.2.1
 
 extra-source-files:   ChangeLog.md
                     , examples/StarWars.hs
@@ -33,18 +34,16 @@
                     , Data.Generics.Internal.Lens
 
   other-modules:      Data.Generics.Internal.Families
-                    , Data.Generics.Internal.Families.Count
+                    , Data.Generics.Internal.Families.Changing
+                    , Data.Generics.Internal.Families.Collect
                     , Data.Generics.Internal.Families.Has
                     , Data.Generics.Internal.HList
+                    , Data.Generics.Internal.Void
 
                     , Data.Generics.Sum.Internal.Constructors
                     , Data.Generics.Sum.Internal.Typed
                     , Data.Generics.Sum.Internal.Subtype
 
-                    , Data.Generics.Internal.Families
-                    , Data.Generics.Internal.Families.Count
-                    , Data.Generics.Internal.Families.Has
-                    , Data.Generics.Internal.HList
                     , Data.Generics.Product.Internal.Fields
                     , Data.Generics.Product.Internal.Positions
                     , Data.Generics.Product.Internal.Subtype
@@ -52,6 +51,7 @@
 
   build-depends:      base        >= 4.9 && <= 5.0
                     , profunctors >= 5.0 && <= 6.0
+                    , tagged      >= 0.8 && <= 0.9
 
   hs-source-dirs:     src
   default-language:   Haskell2010
@@ -72,6 +72,14 @@
 
   default-language:   Haskell2010
   ghc-options:        -Wall
+
+test-suite doctests
+  default-language:   Haskell2010
+  type:               exitcode-stdio-1.0
+  ghc-options:        -threaded
+  main-is:            doctest.hs
+  build-depends:      base >4 && <5, doctest
+  hs-source-dirs:     test
 
 benchmark generic-lens-bench
   type:               exitcode-stdio-1.0
diff --git a/src/Data/Generics/Internal/Families.hs b/src/Data/Generics/Internal/Families.hs
--- a/src/Data/Generics/Internal/Families.hs
+++ b/src/Data/Generics/Internal/Families.hs
@@ -1,3 +1,12 @@
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeApplications      #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
+
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Generics.Internal.Families
@@ -10,7 +19,17 @@
 -----------------------------------------------------------------------------
 module Data.Generics.Internal.Families
   ( module Families
+  , ShowSymbols
   ) where
 
-import Data.Generics.Internal.Families.Count as Families
-import Data.Generics.Internal.Families.Has   as Families
+import Data.Generics.Internal.Families.Collect   as Families
+import Data.Generics.Internal.Families.Has       as Families
+import Data.Generics.Internal.Families.Changing  as Families
+
+import GHC.TypeLits (ErrorMessage (..), Symbol)
+
+type family ShowSymbols (ctors :: [Symbol]) :: ErrorMessage where
+  ShowSymbols '[]
+    = 'Text ""
+  ShowSymbols (c ': cs)
+    = 'Text "• " ':<>: 'Text c ':$$: ShowSymbols cs
diff --git a/src/Data/Generics/Internal/Families/Changing.hs b/src/Data/Generics/Internal/Families/Changing.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Generics/Internal/Families/Changing.hs
@@ -0,0 +1,87 @@
+{-# LANGUAGE AllowAmbiguousTypes    #-}
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE PolyKinds              #-}
+{-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE TypeOperators          #-}
+{-# LANGUAGE UndecidableInstances   #-}
+
+module Data.Generics.Internal.Families.Changing where
+
+import GHC.TypeLits (Nat, type (+))
+
+{-
+  Note [Changing type parameters]
+  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+  To get good type inference for type-changing lenses, we want to be able
+  map the field's type back to the type argument it corresponds to. This way,
+  when the field is changed, we know what the result type of the structure is
+  going to be.
+
+  However, for a given type @t@, its representation @Rep t@ forgets which types
+  in the structure came from type variables, and which didn't. An @Int@ that
+  results from the instantiation of the type paremeter and an @Int@ that was
+  monomorphically specified in the structure are indistinguishable.
+
+  The solution is to replace the type arguments in the type with unique
+  proxies, like: @T a b@ -> @T (P 1 a) (P 0 b)@. This way, if looking up
+  a field's type yields something of shape @P _ _@, we know it came from a type
+  parameter, and also know which.
+
+  If the field's type is a proxy, then its type is allowed to change, otherwise
+  not. This also allows us to satisfy the functional dependency @s field b -> t@.
+  If after doing the conversion on @s@, @field@'s type is @(P _ a), then @t@ is
+  @s[b/a]@, otherwise @t ~ s@ and @b ~ a@.
+-}
+data P (i :: Nat) a
+
+type Proxied t = Proxied' t 0
+
+type family Proxied' (t :: k) (next :: Nat) :: k where
+  Proxied' (t a :: k) next = (Proxied' t (next + 1)) (P next a)
+  Proxied' t _ = t
+
+type family UnProxied (t :: k) :: k where
+  UnProxied (P _ a) = a
+  UnProxied (t (P _ a) :: k) = UnProxied t a
+  UnProxied t = t
+
+type family Change (t :: k) (target :: Nat) (to :: j) :: k where
+  Change (P target _) target to = (P target to)
+  Change (t (P target _) :: k) target to = t (P target to)
+  Change (t a :: k) target to = Change t target to a
+  Change t _ _ = t
+
+type family UnApply (a :: k) :: [*] where
+  UnApply (f x) = x ': UnApply f
+  UnApply x     = '[]
+
+type family Unify a b :: [(*, *)] where
+  Unify (P n a') a = '[ '(P n a', a)]
+  Unify a b = Zip (UnApply a) (UnApply b)
+
+type family PSub (subs :: [(*, *)]) :: [(Nat, *)] where
+  PSub '[] = '[]
+  PSub ('(P n _, b) ': xs) = '(n, b) ': PSub xs
+  PSub (_ ': xs) = PSub xs
+
+type family Zip (xs :: [k]) (ys :: [l]) :: [(k, l)] where
+  Zip '[] '[] = '[]
+  Zip (x ': xs) (y ': ys) = '(x, y) ': Zip xs ys
+
+type family Infer (s :: *) (a' :: *) (a :: *) (w :: *) :: (*, *) where
+  Infer s' a' a w
+    = Infer' s' a' (PSub (Unify a' a)) w
+
+type family Infer' (s :: *) (a' :: *) (subs :: [(Nat, k)]) w :: (*, *) where
+  Infer' s' a' '[ '(p, _)] w
+    = '(UnProxied (Change s' p w), UnProxied (Change a' p w))
+  Infer' s' a' _ _
+    = '(UnProxied s', UnProxied a')
+
+type family PickTv (a :: k) (b :: k) :: * where
+  PickTv (P _ _) b = b
+  PickTv (f (P _ _)) (g b) = b
+  PickTv (f a) (g b) = PickTv f g
diff --git a/src/Data/Generics/Internal/Families/Collect.hs b/src/Data/Generics/Internal/Families/Collect.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Generics/Internal/Families/Collect.hs
@@ -0,0 +1,132 @@
+{-# LANGUAGE DataKinds            #-}
+{-# LANGUAGE PolyKinds            #-}
+{-# LANGUAGE TypeFamilies         #-}
+{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Generics.Internal.Families.Collect
+-- 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.Collect
+  ( CollectTotalType
+  , CollectPartialType
+  , CollectField
+  , CollectFieldsOrdered
+  , TypeStat (..)
+  , type (\\)
+  ) where
+
+import Data.Type.Bool     (If)
+import Data.Type.Equality (type (==))
+import GHC.Generics
+import GHC.TypeLits       (Symbol, CmpSymbol)
+
+import Data.Generics.Internal.HList
+
+data TypeStat
+  = TypeStat
+    { _containsNone :: [Symbol]
+    , _containsMultiple :: [Symbol]
+    , _containsOne :: [Symbol]
+    }
+
+type EmptyStat = 'TypeStat '[] '[] '[]
+
+type family CollectTotalType t f :: TypeStat where
+  CollectTotalType t (C1 ('MetaCons ctor _ _) f)
+    = AddToStat ctor (CountType t f) EmptyStat
+  CollectTotalType t (M1 _ _ r)
+    = CollectTotalType t r
+  CollectTotalType t (l :+: r)
+    = MergeStat (CollectTotalType t l) (CollectTotalType t r)
+
+type family CollectField t f :: TypeStat where
+  CollectField t (C1 ('MetaCons ctor _ _) f)
+    = AddToStat ctor (CountField t f) EmptyStat
+  CollectField t (M1 _ _ r)
+    = CollectField t r
+  CollectField t (l :+: r)
+    = MergeStat (CollectField t l) (CollectField t r)
+
+type family AddToStat (ctor :: Symbol) (count :: Count) (st :: TypeStat) :: TypeStat where
+  AddToStat ctor 'None ('TypeStat n m o)     = 'TypeStat (ctor ': n) m o
+  AddToStat ctor 'Multiple ('TypeStat n m o) = 'TypeStat n (ctor ': m) o
+  AddToStat ctor 'One ('TypeStat n m o)      = 'TypeStat n m (ctor ': o)
+
+type family MergeStat (st1 :: TypeStat) (st2 :: TypeStat) :: TypeStat where
+  MergeStat ('TypeStat n m o) ('TypeStat n' m' o') = 'TypeStat (n ++ n') (m ++ m') (o ++ o')
+
+type family CountType t f :: Count where
+  CountType t (S1 _ (Rec0 t))
+    = 'One
+  CountType t (l :*: r)
+    = CountType t l <|> CountType t r
+  CountType t _
+    = 'None
+
+type family CountField (field :: Symbol) f :: Count where
+  CountField field (S1 ('MetaSel ('Just field) _ _ _) _)
+    = 'One
+  CountField field (l :*: r)
+    = CountField field l <|> CountField field r
+  CountField _ _
+    = 'None
+
+type family CollectPartialType t f :: [Symbol] where
+  CollectPartialType t (l :+: r)
+    = CollectPartialType t l ++ CollectPartialType t r
+  CollectPartialType t (C1 ('MetaCons ctor _ _) f)
+    = If (t == ListToTuple (GCollect f)) '[ctor] '[]
+  CollectPartialType t (D1 _ f)
+    = CollectPartialType t f
+
+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
+
+type family CollectFieldsOrdered (r :: * -> *) :: [Symbol] where
+  CollectFieldsOrdered (l :*: r)
+    = Merge (CollectFieldsOrdered l) (CollectFieldsOrdered r)
+  CollectFieldsOrdered (S1 ('MetaSel ('Just name) _ _ _) _)
+    = '[name]
+  CollectFieldsOrdered (M1 _ m a)
+    = CollectFieldsOrdered a
+  CollectFieldsOrdered _
+    = '[]
+
+type family Merge (xs :: [Symbol]) (ys :: [Symbol]) :: [Symbol] where
+  Merge xs '[] = xs
+  Merge '[] ys = ys
+  Merge (x ': xs) (y ': ys) = Merge' (CmpSymbol x y) x y xs ys
+
+type family Merge' (ord :: Ordering) (x :: Symbol) (y :: Symbol) (xs :: [Symbol]) (ys :: [Symbol]) :: [Symbol] where
+  Merge' 'LT x y xs ys = x ': Merge xs (y ': ys)
+  Merge' _ x y xs ys   = y ': Merge (x ': xs) ys
+
+type family (xs :: [Symbol]) \\ (ys :: [Symbol]) :: [Symbol] where
+  xs \\ '[] = xs
+  '[] \\ xs = '[]
+  (x ': xs) \\ (y ': ys) = Sub' (CmpSymbol x y) x y xs ys
+
+infixr 5 \\
+type family Sub' (ord :: Ordering) (x :: Symbol) (y :: Symbol) (xs :: [Symbol]) (ys :: [Symbol]) :: [Symbol] where
+  Sub' 'LT x y xs ys = x ': (xs \\ y ': ys)
+  Sub' 'GT x _ xs ys = (x ': xs) \\ ys
+  Sub' 'EQ _ _ xs ys = xs \\ ys
diff --git a/src/Data/Generics/Internal/Families/Count.hs b/src/Data/Generics/Internal/Families/Count.hs
deleted file mode 100644
--- a/src/Data/Generics/Internal/Families/Count.hs
+++ /dev/null
@@ -1,75 +0,0 @@
-{-# 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 Data.Type.Bool     (If)
-import Data.Type.Equality (type (==))
-import GHC.Generics
-import GHC.TypeLits       (TypeError, ErrorMessage (..))
-
-import Data.Generics.Internal.HList
-
-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 (l :+: r)
-    = CountPartialType t l <|> CountPartialType t r
-  CountPartialType t (C1 m f)
-    = If (t == ListToTuple (GCollect f)) 'One 'None
-  CountPartialType t (D1 _ f)
-    = CountPartialType t f
-
-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/Lens.hs b/src/Data/Generics/Internal/Lens.hs
--- a/src/Data/Generics/Internal/Lens.hs
+++ b/src/Data/Generics/Internal/Lens.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE GADTs         #-}
 {-# LANGUAGE Rank2Types    #-}
 {-# LANGUAGE TypeOperators #-}
@@ -16,22 +17,34 @@
 -----------------------------------------------------------------------------
 module Data.Generics.Internal.Lens where
 
-import Control.Applicative   (Const(..))
-import Data.Functor.Identity (Identity(..))
-import Data.Profunctor       (Choice(right'), Profunctor(dimap))
-import GHC.Generics          ((:*:)(..), (:+:)(..), Generic(..), M1(..), Rep)
+import Control.Applicative    (Const(..))
+import Data.Functor.Identity  (Identity(..))
+import Data.Monoid            (First (..))
+import Data.Profunctor        (Choice(right'), Profunctor(dimap))
+import Data.Profunctor.Unsafe ((#.), (.#))
+import Data.Tagged
+import GHC.Generics           ((:*:)(..), (:+:)(..), Generic(..), M1(..), Rep)
 
 -- | Type alias for lens
 type Lens' s a
-  = forall f. Functor f => (a -> f a) -> s -> f s
+  = Lens s s a a
 
+type Lens s t a b
+  = forall f. Functor f => (a -> f b) -> s -> f t
+
 -- | Type alias for prism
+type Prism s t a b
+  = forall p f. (Choice p, Applicative f) => p a (f b) -> p s (f t)
+
 type Prism' s a
-  = forall p f. (Choice p, Applicative f) => p a (f a) -> p s (f s)
+  = Prism s s a a
 
 type Iso' s a
   = forall p f. (Profunctor p, Functor f) => p a (f a) -> p s (f s)
 
+type Iso s t a b
+  = forall p f. (Profunctor p, Functor f) => p a (f b) -> p s (f t)
+
 -- | Getting
 (^.) :: s -> ((a -> Const a a) -> s -> Const a s) -> a
 s ^. l = getConst (l Const s)
@@ -42,47 +55,61 @@
 set l b
   = runIdentity . l (\_ -> Identity b)
 
+infixr 4 .~
+(.~) :: ((a -> Identity b) -> s -> Identity t) -> b -> s -> t
+(.~) = set
+
+infixl 8 ^?
+(^?) :: s -> ((a -> Const (First a) a) -> s -> Const (First a) s) -> Maybe a
+s ^? l = getFirst (fmof l (First #. Just) s)
+  where fmof l' f = getConst #. l' (Const #. f)
+
+infixr 8 #
+(#) :: (Tagged b (Identity b) -> Tagged t (Identity t)) -> b -> t
+(#) p = runIdentity #. unTagged #. p .# Tagged .# Identity
+
 -- | Lens focusing on the first element of a product
-first :: Lens' ((a :*: b) x) (a x)
+first :: Lens ((a :*: b) x) ((a' :*: b) x) (a 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 :: Lens ((a :*: b) x) ((a :*: b') x) (b x) (b' x)
 second f (a :*: b)
   = fmap (a :*:) (f b)
 
-left :: Prism' ((a :+: b) x) (a x)
-left = prism L1 $ \x -> case x of
-  L1 a -> Right a
-  R1 _ -> Left x
+left :: Prism ((a :+: c) x) ((b :+: c) x) (a x) (b x)
+left = prism L1 $ gsum Right (Left . R1)
 
-right :: Prism' ((a :+: b) x) (b x)
-right = prism R1 $ \x -> case x of
-  L1 _ -> Left x
-  R1 a -> Right a
+right :: Prism ((a :+: b) x) ((a :+: c) x) (b x) (c x)
+right = prism R1 $ gsum (Left . L1) Right
 
+gsum :: (a x -> c) -> (b x -> c) -> ((a :+: b) x) -> c
+gsum f _ (L1 x) =  f x
+gsum _ g (R1 y) =  g y
+
 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 :: (b -> t) -> (s -> Either t a) -> Prism s t a b
 prism bt seta = dimap seta (either pure (fmap bt)) . right'
 
 -- | A type and its generic representation are isomorphic
-repIso :: Generic a => Iso' a (Rep a x)
+repIso :: (Generic a, Generic b) => Iso a b (Rep a x) (Rep b x)
 repIso = dimap from (fmap to)
 
 -- | 'M1' is just a wrapper around `f p`
-mIso :: Iso' (M1 i c f p) (f p)
+--mIso :: Iso' (M1 i c f p) (f p)
+mIso :: Iso (M1 i c f p) (M1 i c g p) (f p) (g p)
 mIso = dimap unM1 (fmap M1)
 
 -- These are specialised versions of the Isos above. On GHC 8.0.2, having
 -- these functions eta-expanded allows the optimiser to inline these functions.
-mLens :: Lens' (M1 i c f p) (f p)
+mLens :: Lens (M1 i c f p) (M1 i c g p) (f p) (g p)
 mLens f s = mIso f s
 
-repLens :: Generic a => Lens' a (Rep a x)
+repLens :: (Generic a, Generic b) => Lens a b (Rep a x) (Rep b x)
 repLens f s = repIso f s
 
 sumIso :: Iso' ((a :+: b) x) (Either (a x) (b x))
diff --git a/src/Data/Generics/Internal/Void.hs b/src/Data/Generics/Internal/Void.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Generics/Internal/Void.hs
@@ -0,0 +1,18 @@
+module Data.Generics.Internal.Void where
+
+{-
+  Note [Uncluttering type signatures]
+  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+  Because the various instances in the library always match (the Has* classes
+  are essentially glorified constraint synonyms), they get replaced with
+  their constraints, resulting in large, unreadable types.
+
+  Writing an (overlapping instance) for this Void type means that the original
+  instance might not be the one selected, thus GHC leaves the constraints in
+  place until further information is provided, at which point the type
+  machinery has sufficient information to reduce to sensible types.
+-}
+data Void
+data Void1 a
+data Void2 a b
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
@@ -17,14 +17,11 @@
 
 module Data.Generics.Product
   ( -- *Lenses
-    HasAny (..)
-
-  , HasField (..)
-  , HasPosition (..)
-  , HasType (..)
-
-    -- *Subtype relationships
-  , Subtype  (..)
+    module Data.Generics.Product.Any
+  , module Data.Generics.Product.Fields
+  , module Data.Generics.Product.Positions
+  , module Data.Generics.Product.Subtype
+  , module Data.Generics.Product.Typed
   ) where
 
 import Data.Generics.Product.Any
diff --git a/src/Data/Generics/Product/Any.hs b/src/Data/Generics/Product/Any.hs
--- a/src/Data/Generics/Product/Any.hs
+++ b/src/Data/Generics/Product/Any.hs
@@ -6,6 +6,7 @@
 {-# LANGUAGE PolyKinds              #-}
 {-# LANGUAGE ScopedTypeVariables    #-}
 {-# LANGUAGE TypeApplications       #-}
+{-# LANGUAGE TypeFamilies           #-}
 {-# LANGUAGE UndecidableInstances   #-}
 
 -----------------------------------------------------------------------------
@@ -24,7 +25,7 @@
 module Data.Generics.Product.Any
   ( -- *Lenses
     --
-    --  $example
+    -- $setup
     HasAny (..)
   ) where
 
@@ -33,26 +34,26 @@
 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)
+-- $setup
+-- == /Running example:/
 --
---    human :: Human
---    human = Human \"Tunyasz\" 50 \"London\"
---  @
+-- >>> :set -XTypeApplications
+-- >>> :set -XDataKinds
+-- >>> :set -XDeriveGeneric
+-- >>> import GHC.Generics
+-- >>> :m +Data.Generics.Internal.Lens
+-- >>> :{
+-- 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
+class HasAny (sel :: k) s t a b | 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'
@@ -60,17 +61,19 @@
   --
   --  >>> human ^. the @Int
   --  50
+  --
   --  >>> human ^. the @"name"
   --  "Tunyasz"
+  --
   --  >>> human ^. the @3
   --  "London"
-  the :: Lens' s a
+  the :: Lens s t a b
 
-instance HasPosition i a s => HasAny i a s where
+instance HasPosition i s t a b => HasAny i s t a b where
   the = position @i
 
-instance HasField field a s => HasAny field a s where
+instance HasField field s t a b => HasAny field s t a b where
   the = field @field
 
-instance HasType a s => HasAny a a s where
+instance (HasType a s, t ~ s, a ~ b) => HasAny a s t a b where
   the = typed @a
diff --git a/src/Data/Generics/Product/Fields.hs b/src/Data/Generics/Product/Fields.hs
--- a/src/Data/Generics/Product/Fields.hs
+++ b/src/Data/Generics/Product/Fields.hs
@@ -1,14 +1,16 @@
-{-# LANGUAGE AllowAmbiguousTypes    #-}
-{-# LANGUAGE DataKinds              #-}
-{-# LANGUAGE FlexibleInstances      #-}
-{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE KindSignatures         #-}
-{-# LANGUAGE MultiParamTypeClasses  #-}
-{-# LANGUAGE ScopedTypeVariables    #-}
-{-# LANGUAGE TypeApplications       #-}
-{-# LANGUAGE TypeFamilies           #-}
-{-# LANGUAGE TypeOperators          #-}
-{-# LANGUAGE UndecidableInstances   #-}
+{-# LANGUAGE AllowAmbiguousTypes     #-}
+{-# LANGUAGE ConstraintKinds         #-}
+{-# LANGUAGE DataKinds               #-}
+{-# LANGUAGE FlexibleInstances       #-}
+{-# LANGUAGE FunctionalDependencies  #-}
+{-# LANGUAGE MultiParamTypeClasses   #-}
+{-# LANGUAGE ScopedTypeVariables     #-}
+{-# LANGUAGE TypeApplications        #-}
+{-# LANGUAGE TypeFamilies            #-}
+{-# LANGUAGE TypeInType              #-}
+{-# LANGUAGE TypeOperators           #-}
+{-# LANGUAGE UndecidableInstances    #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
 
 -----------------------------------------------------------------------------
 -- |
@@ -26,81 +28,140 @@
 module Data.Generics.Product.Fields
   ( -- *Lenses
 
-    --  $example
+    -- $setup
     HasField (..)
+  , HasField'
+
+  , getField
+  , setField
   ) where
 
 import Data.Generics.Internal.Families
 import Data.Generics.Internal.Lens
+import Data.Generics.Internal.Void
 import Data.Generics.Product.Internal.Fields
 
 import Data.Kind    (Constraint, Type)
 import GHC.Generics
 import GHC.TypeLits (Symbol, ErrorMessage(..), TypeError)
 
---  $example
---  @
---    module Example where
---
---    import Data.Generics.Product
---    import GHC.Generics
---
---    data Human = Human
---      { name    :: String
---      , age     :: Int
---      , address :: String
---      }
---      deriving (Generic, Show)
+-- $setup
+-- == /Running example:/
 --
---    human :: Human
---    human = Human \"Tunyasz\" 50 \"London\"
---  @
+-- >>> :set -XTypeApplications
+-- >>> :set -XDataKinds
+-- >>> :set -XDeriveGeneric
+-- >>> :set -XGADTs
+-- >>> :set -XFlexibleContexts
+-- >>> import GHC.Generics
+-- >>> :m +Data.Generics.Internal.Lens
+-- >>> :m +Data.Function
+-- >>> :{
+-- data Human a
+--   = Human
+--     { name    :: String
+--     , age     :: Int
+--     , address :: String
+--     , other   :: a
+--     }
+--   | HumanNoAddress
+--     { name    :: String
+--     , age     :: Int
+--     , other   :: a
+--     }
+--   deriving (Generic, Show)
+-- human :: Human Bool
+-- human = Human { name = "Tunyasz", age = 50, address = "London", other = False }
+-- :}
 
 -- |Records that have a field with a given name.
-class HasField (field :: Symbol) a s | s field -> a where
+class HasField (field :: Symbol) s t a b | s field -> a, s field b -> t 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'
+  --  === /Type changing/
   --
-  -- >>> setField @"age" (setField @"name" "Tamas" human) 30
-  -- Human {name = "Tamas", age = 30, address = "London"}
-  setField :: a -> s -> s
-  setField = set (field @field)
+  --  >>> :t human
+  --  human :: Human Bool
+  --
+  --  >>> :t human & field @"other" .~ (42 :: Int)
+  --  human & field @"other" .~ (42 :: Int) :: Human Int
+  --
+  --  >>> human & field @"other" .~ 42
+  --  Human {name = "Tunyasz", age = 50, address = "London", other = 42}
+  --
+  --  === /Type errors/
+  --
+  --  >>> human & field @"weight" .~ 42
+  --  ...
+  --  ... The type Human Bool does not contain a field named 'weight'.
+  --  ...
+  --
+  --  >>> human & field @"address" .~ ""
+  --  ...
+  --  ... Not all constructors of the type Human Bool
+  --  ... contain a field named 'address'.
+  --  ... The offending constructors are:
+  --  ... HumanNoAddress
+  --  ...
+  field :: Lens s t a b
 
-  {-# MINIMAL field | setField, getField #-}
+type HasField' field s a = HasField field s s a a
 
-instance
+-- |
+-- >>> getField @"age" human
+-- 50
+getField :: forall f s a. HasField' f s a => s -> a
+getField s = s ^. field @f
+
+-- |
+-- >>> setField @"age" 60 human
+-- Human {name = "Tunyasz", age = 60, address = "London", other = False}
+setField :: forall f s a. HasField' f s a => a -> s -> s
+setField = set (field @f)
+
+instance  -- see Note [Changing type parameters]
   ( Generic s
-  , ErrorUnless field s (HasTotalFieldP field (Rep s))
-  , GHasField field (Rep s) a
-  ) => HasField field a s where
+  , ErrorUnless field s (CollectField field (Rep s))
+  , Generic t
+  , s' ~ Proxied s
+  , Generic s'
+  , GHasField' field (Rep s) a
+  , GHasField' field (Rep s') a'
+  , GHasField field (Rep s) (Rep t) a b
+  , '(t, b) ~ Infer s' a' a (PickTv a' b)
+  ) => HasField field s t a b where
 
-  field = ravel (repLens . gfield @field)
+  field f s = ravel (repLens . gfield @field) f s
 
-type family ErrorUnless (field :: Symbol) (s :: Type) (contains :: Bool) :: Constraint where
-  ErrorUnless field s 'False
+-- See Note [Uncluttering type signatures]
+instance {-# OVERLAPPING #-} HasField f (Void2 t a) t a b where
+  field = undefined
+
+instance {-# OVERLAPPING #-} HasField f (Void1 a) (Void1 b) a b where
+  field = undefined
+
+type family ErrorUnless (field :: Symbol) (s :: Type) (stat :: TypeStat) :: Constraint where
+  ErrorUnless field s ('TypeStat _ _ '[])
     = TypeError
         (     'Text "The type "
         ':<>: 'ShowType s
-        ':<>: 'Text " does not contain a field named "
-        ':<>: 'ShowType field
+        ':<>: 'Text " does not contain a field named '"
+        ':<>: 'Text field ':<>: 'Text "'."
         )
 
-  ErrorUnless _ _ 'True
+  ErrorUnless field s ('TypeStat (n ': ns) _ _)
+    = TypeError
+        (     'Text "Not all constructors of the type "
+        ':<>: 'ShowType s
+        ':$$: 'Text " contain a field named '"
+        ':<>: 'Text field ':<>: 'Text "'."
+        ':$$: 'Text "The offending constructors are:"
+        ':$$: ShowSymbols (n ': ns)
+        )
+
+  ErrorUnless _ _ ('TypeStat '[] '[] _)
     = ()
diff --git a/src/Data/Generics/Product/Internal/Fields.hs b/src/Data/Generics/Product/Internal/Fields.hs
--- a/src/Data/Generics/Product/Internal/Fields.hs
+++ b/src/Data/Generics/Product/Internal/Fields.hs
@@ -1,9 +1,11 @@
 {-# LANGUAGE AllowAmbiguousTypes    #-}
+{-# LANGUAGE ConstraintKinds        #-}
 {-# LANGUAGE DataKinds              #-}
 {-# LANGUAGE FlexibleInstances      #-}
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE KindSignatures         #-}
 {-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE Rank2Types             #-}
 {-# LANGUAGE ScopedTypeVariables    #-}
 {-# LANGUAGE TypeApplications       #-}
 {-# LANGUAGE TypeFamilies           #-}
@@ -25,6 +27,7 @@
 
 module Data.Generics.Product.Internal.Fields
   ( GHasField (..)
+  , GHasField'
   ) where
 
 import Data.Generics.Internal.Families
@@ -36,36 +39,39 @@
 
 -- |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
+class GHasField (field :: Symbol) (s :: Type -> Type) (t :: Type -> Type) a b | s field -> a, t field -> b where
+  gfield :: Lens (s x) (t x) a b
 
-instance GProductHasField field l r a (HasTotalFieldP field l)
-      => GHasField field (l :*: r) a where
+type GHasField' field s a = GHasField field s s a a
 
-  gfield = gproductField @field @_ @_ @_ @(HasTotalFieldP field l)
+instance GProductHasField field l r l' r' a b (HasTotalFieldP field l)
+      => GHasField field (l :*: r) (l' :*: r') a b where
 
-instance (GHasField field l a, GHasField field r a)
-      =>  GHasField field (l :+: r) a where
+  gfield = gproductField @field @_ @_ @_ @_ @_ @_ @(HasTotalFieldP field l)
 
-  gfield = combine (gfield @field @l) (gfield @field @r)
+instance (GHasField' field r a, GHasField' field l a, GHasField field l l' a b, GHasField field r r' a b)
+      =>  GHasField field (l :+: r) (l' :+: r') a b where
 
-instance GHasField field (K1 R a) a where
+  gfield f (L1 s) = fmap (\a -> L1 (set (gfield @field) a s)) (f (s ^. gfield @field))
+  gfield f (R1 t) = fmap (\a -> R1 (set (gfield @field) a t)) (f (t ^. gfield @field))
+
+instance GHasField field (K1 R a) (K1 R b) a b where
   gfield f (K1 x) = fmap K1 (f x)
 
-instance GHasField field (S1 ('MetaSel ('Just field) upkd str infstr) (Rec0 a)) a where
+instance GHasField field (S1 ('MetaSel ('Just field) upkd str infstr) (Rec0 a)) (S1 ('MetaSel ('Just field) upkd str infstr) (Rec0 b)) a b where
   gfield = mLens . gfield @field
 
-instance GHasField field f a => GHasField field (M1 D meta f) a where
+instance (Functor g, GHasField field f g a b) => GHasField field (M1 D meta f) (M1 D meta g) a b where
   gfield = mLens . gfield @field
 
-instance GHasField field f a => GHasField field (M1 C meta f) a where
+instance GHasField field f g a b => GHasField field (M1 C meta f) (M1 C meta g) a b where
   gfield = mLens . gfield @field
 
-class GProductHasField (field :: Symbol) l r a (left :: Bool) | left field l r -> a where
-  gproductField :: Lens' ((l :*: r) x) a
+class GProductHasField (field :: Symbol) l r l' r' a b (left :: Bool) | field l r -> a, field l' r' -> b where
+  gproductField :: Lens ((l :*: r) x) ((l' :*: r') x) a b
 
-instance GHasField field l a => GProductHasField field l r a 'True where
+instance GHasField field l l' a b => GProductHasField field l r l' r a b 'True where
   gproductField = first . gfield @field
 
-instance GHasField field r a => GProductHasField field l r a 'False where
+instance GHasField field r r' a b => GProductHasField field l r l r' a b 'False where
   gproductField = second . gfield @field
diff --git a/src/Data/Generics/Product/Internal/Positions.hs b/src/Data/Generics/Product/Internal/Positions.hs
--- a/src/Data/Generics/Product/Internal/Positions.hs
+++ b/src/Data/Generics/Product/Internal/Positions.hs
@@ -1,5 +1,7 @@
 {-# LANGUAGE AllowAmbiguousTypes    #-}
+{-# LANGUAGE ConstraintKinds        #-}
 {-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE FlexibleContexts       #-}
 {-# LANGUAGE FlexibleInstances      #-}
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE KindSignatures         #-}
@@ -26,6 +28,7 @@
 
 module Data.Generics.Product.Internal.Positions
   ( GHasPosition (..)
+  , GHasPosition'
   , type (<?)
   , Size
   ) where
@@ -39,31 +42,32 @@
 
 -- |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
+class GHasPosition (offset :: Nat) (i :: Nat) (s :: Type -> Type) (t :: Type -> Type) a b | s offset i -> a, s t offset i -> b where
+  gposition :: Lens (s x) (t x) a b
 
-instance GHasPosition i i (K1 R a) a where
+type GHasPosition' i s a = GHasPosition 1 i s s a a
+
+instance GHasPosition i i (K1 R a) (K1 R b) a b where
   gposition f (K1 x) = fmap K1 (f x)
 
-instance GHasPosition offset i f a => GHasPosition offset i (M1 m meta f) a where
+instance GHasPosition offset i s t a b => GHasPosition offset i (M1 m meta s) (M1 m meta t) a b where
   gposition = mLens . 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
+  , GProductHasPosition offset' i l r l' r' a b goLeft
+  ) => GHasPosition offset i (l :*: r) (l' :*: r') a b 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
+class GProductHasPosition (offset :: Nat) (i :: Nat) l r l' r' a b (left :: Bool) | offset i l r -> a, offset i l r l' r' -> b where
+  gproductPosition :: Lens ((l :*: r) x) ((l' :*: r') x) a b
 
-instance GHasPosition offset i l a => GProductHasPosition offset i l r a 'True where
+instance GHasPosition offset i l l' a b => GProductHasPosition offset i l r l' r a b 'True where
   gproductPosition = first . gposition @offset @i
 
-instance GHasPosition offset i r a => GProductHasPosition offset i l r a 'False where
+instance GHasPosition offset i r r' a b => GProductHasPosition offset i l r l r' a b 'False where
   gproductPosition = second . gposition @offset @i
 
 type family Size f :: Nat where
diff --git a/src/Data/Generics/Product/Internal/Subtype.hs b/src/Data/Generics/Product/Internal/Subtype.hs
--- a/src/Data/Generics/Product/Internal/Subtype.hs
+++ b/src/Data/Generics/Product/Internal/Subtype.hs
@@ -47,7 +47,7 @@
   gupcast rep = gupcast rep :*: gupcast rep
 
 instance
-  GHasField field sub t
+  GHasField field sub sub t t
   => GUpcast sub (S1 ('MetaSel ('Just field) p f b) (Rec0 t)) where
 
   gupcast r = M1 (K1 (r ^. gfield @field))
@@ -84,7 +84,7 @@
   gsmashLeaf :: sup p -> sub p -> sub p
 
 instance
-  GHasField field sup t
+  GHasField field sup sup t t
   => GSmashLeaf (S1 ('MetaSel ('Just field) p f b) (Rec0 t)) sup 'True where
   gsmashLeaf sup _ = M1 (K1 (sup ^. gfield @field))
 
diff --git a/src/Data/Generics/Product/Positions.hs b/src/Data/Generics/Product/Positions.hs
--- a/src/Data/Generics/Product/Positions.hs
+++ b/src/Data/Generics/Product/Positions.hs
@@ -1,5 +1,7 @@
 {-# LANGUAGE AllowAmbiguousTypes    #-}
+{-# LANGUAGE ConstraintKinds        #-}
 {-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE FlexibleContexts       #-}
 {-# LANGUAGE FlexibleInstances      #-}
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE KindSignatures         #-}
@@ -27,11 +29,17 @@
 module Data.Generics.Product.Positions
   ( -- *Lenses
 
-    --  $example
+    -- $setup
     HasPosition (..)
+  , HasPosition'
+
+  , getPosition
+  , setPosition
   ) where
 
 import Data.Generics.Internal.Lens
+import Data.Generics.Internal.Void
+import Data.Generics.Internal.Families
 import Data.Generics.Product.Internal.Positions
 
 import Data.Kind      (Constraint, Type)
@@ -39,61 +47,70 @@
 import GHC.Generics
 import GHC.TypeLits   (type (<=?),  Nat, TypeError, ErrorMessage(..))
 
---  $example
---  @
---    module Example where
---
---    import Data.Generics.Product
---    import GHC.Generics
---
---    data Human = Human
---      { name    :: String
---      , age     :: Int
---      , address :: String
---      }
---      deriving (Generic, Show)
+-- $setup
+-- == /Running example:/
 --
---    human :: Human
---    human = Human \"Tunyasz\" 50 \"London\"
---  @
+-- >>> :set -XTypeApplications
+-- >>> :set -XDataKinds
+-- >>> :set -XDeriveGeneric
+-- >>> :set -XGADTs
+-- >>> :set -XFlexibleContexts
+-- >>> import GHC.Generics
+-- >>> :m +Data.Generics.Internal.Lens
+-- >>> :m +Data.Function
+-- >>> :{
+-- 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
+class HasPosition (i :: Nat) s t a b | s i -> a, s i b -> t 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 & position @3 .~ "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
+  --  === /Type errors/
   --
-  -- >>> setPosition @2 (setField @1 "Tamas" human) 30
-  -- Human "Tamas" 30 "London"
-  setPosition :: a -> s -> s
-  setPosition = set (position @i)
+  --  >>> human & position @4 .~ "Berlin"
+  --  ...
+  --  ... The type Human does not contain a field at position 4
+  --  ...
+  position :: Lens s t a b
 
-  {-# MINIMAL position | setPosition, getPosition #-}
+type HasPosition' i s a = HasPosition i s s a a
 
-instance
+getPosition :: forall i s a. HasPosition' i s a => s -> a
+getPosition s = s ^. position @i
+
+setPosition :: forall i s a. HasPosition' i s a => a -> s -> s
+setPosition = set (position @i)
+
+instance  -- see Note [Changing type parameters]
   ( Generic s
   , ErrorUnless i s (0 <? i && i <=? Size (Rep s))
-  , GHasPosition 1 i (Rep s) a
-  ) => HasPosition i a s where
+  , Generic t
+  , s' ~ Proxied s
+  , GHasPosition' i (Rep s) a
+  , GHasPosition' i (Rep s') a'
+  , GHasPosition 1 i (Rep s) (Rep t) a b
+  , '(t, b) ~ Infer s' a' a (PickTv a' b)
+  ) => HasPosition i s t a b where
 
-  position = ravel (repLens . gposition @1 @i)
+  position f s = ravel (repLens . gposition @1 @i) f s
+
+-- See Note [Uncluttering type signatures]
+instance {-# OVERLAPPING #-} HasPosition f (Void2 a t) t a b where
+  position = undefined
 
 type family ErrorUnless (i :: Nat) (s :: Type) (hasP :: Bool) :: Constraint where
   ErrorUnless i s 'False
diff --git a/src/Data/Generics/Product/Subtype.hs b/src/Data/Generics/Product/Subtype.hs
--- a/src/Data/Generics/Product/Subtype.hs
+++ b/src/Data/Generics/Product/Subtype.hs
@@ -28,36 +28,43 @@
 module Data.Generics.Product.Subtype
   ( -- *Lenses
     --
-    --  $example
+    -- $setup
     Subtype (..)
   ) where
 
+import Data.Generics.Internal.Families
 import Data.Generics.Internal.Lens
+import Data.Generics.Internal.Void
 import Data.Generics.Product.Internal.Subtype
 
 import GHC.Generics (Generic (Rep, to, from) )
+import GHC.TypeLits (Symbol, TypeError, ErrorMessage (..))
+import Data.Kind (Type, Constraint)
 
---  $example
---  @
---     module Example where
---
---     import Data.Generics.Product
---     import GHC.Generics
---
---     data Human = Human
---       { name    :: String
---       , age     :: Int
---       , address :: String
---       } deriving (Generic, Show)
---
---     data Animal = Animal
---       { name    :: String
---       , age     :: Int
---       } deriving (Generic, Show)
+-- $setup
+-- == /Running example:/
 --
---     human :: Human
---     human = Human \"Tunyasz\" 50 \"London\"
---  @
+-- >>> :set -XTypeApplications
+-- >>> :set -XDataKinds
+-- >>> :set -XDeriveGeneric
+-- >>> :set -XDuplicateRecordFields
+-- >>> import GHC.Generics
+-- >>> :m +Data.Generics.Internal.Lens
+-- >>> :{
+-- 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"
+-- :}
 
 -- |Structural subtype relationship
 --
@@ -82,6 +89,12 @@
   -- >>> upcast human :: Animal
   -- Animal {name = "Tunyasz", age = 50}
   --
+  -- >>> upcast (upcast human :: Animal) :: Human
+  -- ...
+  -- ... The type 'Human' is not a subtype of 'Animal'.
+  -- ... The following fields are missing from 'Human':
+  -- ... address
+  -- ...
   upcast :: sub -> sup
   upcast s = s ^. super @sup
 
@@ -95,10 +108,32 @@
   {-# MINIMAL super | smash, upcast #-}
 
 instance
-  ( GSmash (Rep a) (Rep b)
-  , GUpcast (Rep a) (Rep b)
-  , Generic a
+  ( Generic a
   , Generic b
+  , GSmash (Rep a) (Rep b)
+  , GUpcast (Rep a) (Rep b)
+  , ErrorUnless b a (CollectFieldsOrdered (Rep b) \\ CollectFieldsOrdered (Rep a))
   ) => Subtype b a where
     smash p b = to $ gsmash (from p) (from b)
     upcast    = to . gupcast . from
+
+-- See Note [Uncluttering type signatures]
+instance {-# OVERLAPPING #-} Subtype a Void where
+  super = undefined
+instance {-# OVERLAPPING #-} Subtype Void a where
+  super = undefined
+
+type family ErrorUnless (sub :: Type) (sup :: Type) (diff :: [Symbol]) :: Constraint where
+  ErrorUnless _ _ '[]
+    = ()
+
+  ErrorUnless sub sup fs
+    = TypeError
+        (     'Text "The type '"
+        ':<>: 'ShowType sub
+        ':<>: 'Text "' is not a subtype of '"
+        ':<>: 'ShowType sup ':<>: 'Text "'."
+        ':$$: 'Text "The following fields are missing from '"
+        ':<>: 'ShowType sub ':<>: 'Text "':"
+        ':$$: ShowSymbols fs
+        )
diff --git a/src/Data/Generics/Product/Typed.hs b/src/Data/Generics/Product/Typed.hs
--- a/src/Data/Generics/Product/Typed.hs
+++ b/src/Data/Generics/Product/Typed.hs
@@ -26,35 +26,44 @@
 module Data.Generics.Product.Typed
   ( -- *Lenses
     --
-    --  $example
+    -- $setup
     HasType (..)
   ) where
 
 import Data.Generics.Internal.Families
 import Data.Generics.Internal.Lens
+import Data.Generics.Internal.Void
 import Data.Generics.Product.Internal.Typed
 
 import Data.Kind    (Constraint, Type)
 import GHC.Generics (Generic (Rep))
 import GHC.TypeLits (TypeError, ErrorMessage (..))
 
---  $example
---  @
---    module Example where
---
---    import Data.Generics.Product
---    import GHC.Generics
---
---    data Human = Human
---      { name    :: String
---      , age     :: Int
---      , address :: String
---      }
---      deriving (Generic, Show)
+-- $setup
+-- == /Running example:/
 --
---    human :: Human
---    human = Human \"Tunyasz\" 50 \"London\"
---  @
+-- >>> :set -XTypeApplications
+-- >>> :set -XDataKinds
+-- >>> :set -XDeriveGeneric
+-- >>> import GHC.Generics
+-- >>> :m +Data.Generics.Internal.Lens
+-- >>> :{
+-- data Human
+--   = Human
+--     { name    :: String
+--     , age     :: Int
+--     , address :: String
+--     , tall    :: Bool
+--     }
+--   | HumanNoTall
+--     { name    :: String
+--     , age     :: Int
+--     , address :: String
+--     }
+--   deriving (Generic, Show)
+-- human :: Human
+-- human = Human "Tunyasz" 50 "London" False
+-- :}
 
 -- |Records that have a field with a unique type.
 class HasType a s where
@@ -63,6 +72,25 @@
   --
   --  >>> human ^. typed @Int
   --  50
+  --
+  --  === /Type errors/
+  --
+  --  >>> human ^. typed @String
+  --  ...
+  --  ...
+  --  ... The type Human contains multiple values of type [Char].
+  --  ... The choice of value is thus ambiguous. The offending constructors are:
+  --  ... Human
+  --  ... HumanNoTall
+  --  ...
+  --
+  --  >>> human ^. typed @Bool
+  --  ...
+  --  ...
+  --  ... Not all constructors of the type Human contain a field of type Bool.
+  --  ... The offending constructors are:
+  --  ... HumanNoTall
+  --  ...
   typed :: Lens' s a
   typed f t
     = fmap (flip (setTyped @a) t) (f (getTyped @a t))
@@ -79,14 +107,18 @@
 
 instance
   ( Generic s
-  , ErrorUnlessOne a s (CountTotalType a (Rep s))
+  , ErrorUnlessOne a s (CollectTotalType a (Rep s))
   , GHasType (Rep s) a
   ) => HasType a s where
 
   typed = ravel (repLens . gtyped)
 
-type family ErrorUnlessOne (a :: Type) (s :: Type) (count :: Count) :: Constraint where
-  ErrorUnlessOne a s 'None
+-- See Note [Uncluttering type signatures]
+instance {-# OVERLAPPING #-} HasType a Void where
+  typed = undefined
+
+type family ErrorUnlessOne (a :: Type) (s :: Type) (stat :: TypeStat) :: Constraint where
+  ErrorUnlessOne a s ('TypeStat '[_] '[] '[])
     = TypeError
         (     'Text "The type "
         ':<>: 'ShowType s
@@ -94,14 +126,25 @@
         ':<>: 'ShowType a
         )
 
-  ErrorUnlessOne a s 'Multiple
+  ErrorUnlessOne a s ('TypeStat (n ': ns) _ _)
     = TypeError
+        (     'Text "Not all constructors of the type "
+        ':<>: 'ShowType s
+        ':<>: 'Text " contain a field of type "
+        ':<>: 'ShowType a ':<>: 'Text "."
+        ':$$: 'Text "The offending constructors are:"
+        ':$$: ShowSymbols (n ': ns)
+        )
+
+  ErrorUnlessOne a s ('TypeStat _ (m ': ms) _)
+    = TypeError
         (     'Text "The type "
         ':<>: 'ShowType s
         ':<>: 'Text " contains multiple values of type "
-        ':<>: 'ShowType a
-        ':<>: 'Text "; the choice of value is thus ambiguous"
+        ':<>: 'ShowType a ':<>: 'Text "."
+        ':$$: 'Text "The choice of value is thus ambiguous. The offending constructors are:"
+        ':$$: ShowSymbols (m ': ms)
         )
 
-  ErrorUnlessOne _ _ 'One
+  ErrorUnlessOne _ _ ('TypeStat '[] '[] _)
     = ()
diff --git a/src/Data/Generics/Sum.hs b/src/Data/Generics/Sum.hs
--- a/src/Data/Generics/Sum.hs
+++ b/src/Data/Generics/Sum.hs
@@ -17,11 +17,10 @@
 
 module Data.Generics.Sum
   ( -- *Prisms
-    AsAny (..)
-
-  , AsConstructor (..)
-  , AsSubtype (..)
-  , AsType (..)
+    module Data.Generics.Sum.Any
+  , module Data.Generics.Sum.Constructors
+  , module Data.Generics.Sum.Subtype
+  , module Data.Generics.Sum.Typed
   ) where
 
 import Data.Generics.Sum.Any
diff --git a/src/Data/Generics/Sum/Any.hs b/src/Data/Generics/Sum/Any.hs
--- a/src/Data/Generics/Sum/Any.hs
+++ b/src/Data/Generics/Sum/Any.hs
@@ -24,7 +24,7 @@
 module Data.Generics.Sum.Any
   ( -- *Prisms
     --
-    --  $example
+    -- $setup
     AsAny (..)
   ) where
 
@@ -32,34 +32,33 @@
 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
+-- $setup
+-- == /Running example:/
 --
---    dog = Dog (MkDog "Shep" 3)
---    cat = Cat "Mog" 5
---    duck = Duck 2
---  @
+-- >>> :set -XTypeApplications
+-- >>> :set -XDataKinds
+-- >>> :set -XDeriveGeneric
+-- >>> import GHC.Generics
+-- >>> :m +Data.Generics.Internal.Lens
+-- >>> :{
+-- 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
@@ -69,22 +68,29 @@
   --
   --  >>> dog ^? _As @"Dog"
   --  Just (MkDog {name = "Shep", age = 3})
+  --
   --  >>> dog ^? _As @Dog
   --  Just (MkDog {name = "Shep", age = 3})
+  --
   --  >>> dog ^? _As @"Cat"
   --  Nothing
+  --
   --  >>> cat ^? _As @(Name, Age)
   --  Just ("Mog",5)
+  --
   --  >>> cat ^? _As @"Cat"
   --  Just ("Mog",5)
+  --
   --  >>> _As @"Cat" # ("Garfield", 6) :: Animal
-  --  Cat ("Garfield",6)
+  --  Cat "Garfield" 6
+  --
   --  >>> duck ^? _As @Age
   --  Just 2
   _As :: Prism' s a
 
-instance AsConstructor ctor a s => AsAny ctor a s where
+instance AsConstructor ctor s s a a => 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
--- a/src/Data/Generics/Sum/Constructors.hs
+++ b/src/Data/Generics/Sum/Constructors.hs
@@ -26,72 +26,95 @@
 module Data.Generics.Sum.Constructors
   ( -- *Prisms
 
-    --  $example
+    -- $setup
     AsConstructor (..)
   ) where
 
 import Data.Generics.Internal.Families
 import Data.Generics.Internal.Lens
+import Data.Generics.Internal.Void
 import Data.Generics.Sum.Internal.Constructors
 
 import Data.Kind    (Constraint, Type)
 import GHC.Generics (Generic (Rep))
 import GHC.TypeLits (Symbol, TypeError, ErrorMessage (..))
 
---  $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
+-- $setup
+-- == /Running example:/
 --
---    dog = Dog (MkDog "Shep" 3)
---    cat = Cat "Mog" 5
---    duck = Duck 2
---  @
+-- >>> :set -XTypeApplications
+-- >>> :set -XDataKinds
+-- >>> :set -XDeriveGeneric
+-- >>> :set -XFlexibleContexts
+-- >>> :set -XTypeFamilies
+-- >>> import GHC.Generics
+-- >>> :m +Data.Generics.Internal.Lens
+-- >>> :m +Data.Generics.Product.Fields
+-- >>> :m +Data.Function
+-- >>> :{
+-- data Animal a
+--   = Dog (Dog a)
+--   | Cat Name Age
+--   | Duck Age
+--   deriving (Generic, Show)
+-- data Dog a
+--   = MkDog
+--   { name   :: Name
+--   , age    :: Age
+--   , fieldA :: a
+--   }
+--   deriving (Generic, Show)
+-- type Name = String
+-- type Age  = Int
+-- dog, cat, duck :: Animal Int
+-- dog = Dog (MkDog "Shep" 3 30)
+-- 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
+class AsConstructor (ctor :: Symbol) s t a b | ctor s -> a, ctor t -> b 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})
+  --  Just (MkDog {name = "Shep", age = 3, fieldA = 30})
   --
   --  >>> dog ^? _Ctor @"Cat"
   --  Nothing
   --
   --  >>> cat ^? _Ctor @"Cat"
-  --  Just ("Mog", 5)
+  --  Just ("Mog",5)
   --
-  --  >>> _Ctor @"Cat" # ("Garfield", 6) :: Animal
-  --  Cat ("Garfield", 6)
-  _Ctor :: Prism' s a
+  --  >>> _Ctor @"Cat" # ("Garfield", 6) :: Animal Int
+  --  Cat "Garfield" 6
+  --
+  --  === /Type errors/
+  --
+  --  >>> cat ^? _Ctor @"Turtle"
+  --  ...
+  --  ...
+  --  ... The type Animal Int does not contain a constructor named "Turtle"
+  --  ...
+  _Ctor :: Prism s t a b
 
 instance
   ( Generic s
   , ErrorUnless ctor s (HasCtorP ctor (Rep s))
-  , GAsConstructor ctor (Rep s) a
-  ) => AsConstructor ctor a s where
+  , Generic t
+  , s' ~ Proxied s
+  , Generic s'
+  , GAsConstructor' ctor (Rep s) a
+  , GAsConstructor' ctor (Rep s') a'
+  , GAsConstructor ctor (Rep s) (Rep t) a b
+  , '(t, b) ~ Infer s' a' a (PickTv a' b)
+  ) => AsConstructor ctor s t a b where
 
   _Ctor = repIso . _GCtor @ctor
+
+-- See Note [Uncluttering type signatures]
+instance {-# OVERLAPPING #-} AsConstructor ctor (Void1 a) (Void1 b) a b where
+  _Ctor = undefined
 
 type family ErrorUnless (ctor :: Symbol) (s :: Type) (contains :: Bool) :: Constraint where
   ErrorUnless ctor s 'False
diff --git a/src/Data/Generics/Sum/Internal/Constructors.hs b/src/Data/Generics/Sum/Internal/Constructors.hs
--- a/src/Data/Generics/Sum/Internal/Constructors.hs
+++ b/src/Data/Generics/Sum/Internal/Constructors.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE AllowAmbiguousTypes    #-}
+{-# LANGUAGE ConstraintKinds        #-}
 {-# LANGUAGE DataKinds              #-}
 {-# LANGUAGE FlexibleInstances      #-}
 {-# LANGUAGE FunctionalDependencies #-}
@@ -25,39 +26,43 @@
 
 module Data.Generics.Sum.Internal.Constructors
   ( GAsConstructor (..)
+  , GAsConstructor'
   ) where
 
 import Data.Generics.Internal.Families
 import Data.Generics.Internal.HList
 import Data.Generics.Internal.Lens
 
-import Data.Kind    (Type)
 import GHC.Generics
 import GHC.TypeLits (Symbol)
 
 -- |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
+class GAsConstructor (ctor :: Symbol) s t a b | ctor s -> a, ctor t -> b where
+  _GCtor :: Prism (s x) (t x) a b
 
+type GAsConstructor' ctor s a = GAsConstructor ctor s s a a
+
 instance
   ( GCollectible f as
+  , GCollectible g bs
   , ListTuple a as
-  ) => GAsConstructor ctor (M1 C ('MetaCons ctor fixity fields) f) a where
+  , ListTuple b bs
+  ) => GAsConstructor ctor (M1 C ('MetaCons ctor fixity fields) f) (M1 C ('MetaCons ctor fixity fields) g) a b where
 
-  _GCtor = prism (M1 . gfromCollection . tupleToList) (Right . listToTuple @_ @as . gtoCollection . unM1)
+  _GCtor = prism (M1 . gfromCollection . tupleToList) (Right . listToTuple . 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 GSumAsConstructor ctor (HasCtorP ctor l) l r l' r' a b => GAsConstructor ctor (l :+: r) (l' :+: r') a b where
+  _GCtor = _GSumCtor @ctor @(HasCtorP ctor l)
 
-instance GAsConstructor ctor f a => GAsConstructor ctor (M1 D meta f) a where
+instance GAsConstructor ctor f f' a b => GAsConstructor ctor (M1 D meta f) (M1 D meta f') a b 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
+class GSumAsConstructor (ctor :: Symbol) (contains :: Bool) l r l' r' a b | ctor l r -> a, ctor l' r' -> b where
+  _GSumCtor :: Prism ((l :+: r) x) ((l' :+: r') x) a b
 
-instance GAsConstructor ctor l a => GSumAsConstructor ctor l r a 'True where
+instance GAsConstructor ctor l l' a b => GSumAsConstructor ctor 'True l r l' r a b where
   _GSumCtor = left . _GCtor @ctor
 
-instance GAsConstructor ctor r a => GSumAsConstructor ctor l r a 'False where
+instance GAsConstructor ctor r r' a b => GSumAsConstructor ctor 'False l r l r' a b where
   _GSumCtor = right . _GCtor @ctor
diff --git a/src/Data/Generics/Sum/Subtype.hs b/src/Data/Generics/Sum/Subtype.hs
--- a/src/Data/Generics/Sum/Subtype.hs
+++ b/src/Data/Generics/Sum/Subtype.hs
@@ -22,53 +22,49 @@
 module Data.Generics.Sum.Subtype
   ( -- *Prisms
     --
-    --  $example
+    -- $setup
     AsSubtype (..)
   ) where
 
 import Data.Generics.Internal.Lens
+import Data.Generics.Internal.Void
 import Data.Generics.Sum.Internal.Subtype
 
 import GHC.Generics (Generic (Rep, to, from))
 
---  $example
---  @
---    module Example where
---
---    import Data.Generics.Sum
---    import GHC.Generics
---
---    data Animal
---      = Dog Dog
---      | Cat Name Age
---      | Duck Age
---      deriving (Generic, Show)
---
---    data FourLeggedAnimal
---      = Dog4 Dog
---      | Cat4 Name 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
---
---    dog4, cat4 :: FourLeggedAnimal
+-- $setup
+-- == /Running example:/
 --
---    dog4 = Dog4 (MkDog "Snowy" 4)
---    cat4 = Cat4 "Garfield" 6
---  @
+-- >>> :set -XTypeApplications
+-- >>> :set -XDataKinds
+-- >>> :set -XDeriveGeneric
+-- >>> import GHC.Generics
+-- >>> :m +Data.Generics.Internal.Lens
+-- >>> :{
+-- data Animal
+--   = Dog Dog
+--   | Cat Name Age
+--   | Duck Age
+--   deriving (Generic, Show)
+-- data FourLeggedAnimal
+--   = Dog4 Dog
+--   | Cat4 Name 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
+-- dog4, cat4 :: FourLeggedAnimal
+-- dog4 = Dog4 (MkDog "Snowy" 4)
+-- cat4 = Cat4 "Garfield" 6
+-- :}
 
 -- |Structural subtyping between sums. A sum 'Sub' is a subtype of another sum
 --  'Sup' if a value of 'Sub' can be given (modulo naming of constructors)
@@ -83,8 +79,10 @@
   --
   --  >>> _Sub # dog4 :: Animal
   --  Dog (MkDog {name = "Snowy", age = 4})
+  --
   --  >>> cat ^? _Sub :: Maybe FourLeggedAnimal
   --  Just (Cat4 "Mog" 5)
+  --
   --  >>> duck ^? _Sub :: Maybe FourLeggedAnimal
   --  Nothing
   _Sub :: Prism' sup sub
@@ -106,3 +104,11 @@
 
   injectSub  = to . ginjectSub . from
   projectSub = either (Left . to) (Right . to) . gprojectSub . from
+
+-- See Note [Uncluttering type signatures]
+instance {-# OVERLAPPING #-} AsSubtype a Void where
+  injectSub = undefined
+  projectSub = undefined
+instance {-# OVERLAPPING #-} AsSubtype Void a where
+  injectSub = undefined
+  projectSub = undefined
diff --git a/src/Data/Generics/Sum/Typed.hs b/src/Data/Generics/Sum/Typed.hs
--- a/src/Data/Generics/Sum/Typed.hs
+++ b/src/Data/Generics/Sum/Typed.hs
@@ -25,60 +25,64 @@
 module Data.Generics.Sum.Typed
   ( -- *Prisms
     --
-    --  $example
+    --  $setup
     AsType (..)
   ) where
 
 import Data.Kind
 import GHC.Generics
-import GHC.TypeLits (TypeError, ErrorMessage (..))
+import GHC.TypeLits (TypeError, ErrorMessage (..), Symbol)
 import Data.Generics.Sum.Internal.Typed
 
 import Data.Generics.Internal.Families
 import Data.Generics.Internal.Lens
+import Data.Generics.Internal.Void
 
---  $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
---  @
+-- $setup
+-- >>> :set -XTypeApplications
+-- >>> :set -XDataKinds
+-- >>> :set -XDeriveGeneric
+-- >>> import GHC.Generics
+-- >>> :m +Data.Generics.Internal.Lens
+-- >>> :{
+-- data Animal
+--   = Dog Dog
+--   | Cat Name Age
+--   | Duck Age
+--   | Turtle Age
+--   deriving (Generic, Show)
+-- data Dog
+--   = MkDog
+--   { name :: Name
+--   , age  :: Age
+--   }
+--   deriving (Generic, Show)
+-- type Name = String
+-- newtype Age  = Age Int deriving Show
+-- dog, cat, duck :: Animal
+-- dog = Dog (MkDog "Shep" (Age 3))
+-- cat = Cat "Mog" (Age 5)
+-- duck = Duck (Age 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 @Age
-  --  Nothing
+  --  Just (MkDog {name = "Shep", age = Age 3})
   --  >>> cat ^? _Typed @(Name, Age)
-  --  Just ("Mog",5)
-  --  >>> duck ^? _Typed @Age
-  --  Just 2
+  --  Just ("Mog",Age 5)
+  --  >>> dog ^? _Typed @Age
+  --  ...
+  --  ...
+  --  ... The type Animal contains multiple constructors whose fields are of type Age.
+  --  ... The choice of constructor is thus ambiguous, could be any of:
+  --  ... Duck
+  --  ... Turtle
+  --  ...
   _Typed :: Prism' s a
 
   -- |Inject by type.
@@ -89,7 +93,7 @@
 
 instance
   ( Generic s
-  , ErrorUnlessOne a s (CountPartialType a (Rep s))
+  , ErrorUnlessOne a s (CollectPartialType a (Rep s))
   , GAsType (Rep s) a
   ) => AsType a s where
 
@@ -100,8 +104,21 @@
   projectTyped
     = either (const Nothing) Just . gprojectTyped . from
 
-type family ErrorUnlessOne (a :: Type) (s :: Type) (count :: Count) :: Constraint where
-  ErrorUnlessOne a s 'None
+-- See Note [Uncluttering type signatures]
+instance {-# OVERLAPPING #-} AsType a Void where
+  _Typed = undefined
+  injectTyped = undefined
+  projectTyped = undefined
+instance {-# OVERLAPPING #-} AsType Void a where
+  _Typed = undefined
+  injectTyped = undefined
+  projectTyped = undefined
+
+type family ErrorUnlessOne (a :: Type) (s :: Type) (ctors :: [Symbol]) :: Constraint where
+  ErrorUnlessOne _ _ '[_]
+    = ()
+
+  ErrorUnlessOne a s '[]
     = TypeError
         (     'Text "The type "
         ':<>: 'ShowType s
@@ -109,14 +126,12 @@
         ':<>: 'ShowType a
         )
 
-  ErrorUnlessOne a s 'Multiple
+  ErrorUnlessOne a s cs
     = 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"
+        ':<>: 'ShowType a ':<>: 'Text "."
+        ':$$: 'Text "The choice of constructor is thus ambiguous, could be any of:"
+        ':$$: ShowSymbols cs
         )
-
-  ErrorUnlessOne _ _ 'One
-    = ()
diff --git a/test/Spec.hs b/test/Spec.hs
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -28,11 +28,23 @@
   { fieldA :: Int
   } deriving Generic
 
-type Lens' s a = forall f. Functor f => (a -> f a) -> s -> f s
+data Record3 a = MkRecord3
+  { fieldA :: a
+  , fieldB :: Bool
+  } deriving (Generic, Show)
 
+type Lens' s a = Lens s s a a
+type Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t
+
 fieldALensManual :: Lens' Record Int
 fieldALensManual f (MkRecord a b) = (\a' -> MkRecord a' b) <$> f a
 
+typeChangingManual :: Lens (Record3 a) (Record3 b) a b
+typeChangingManual f (MkRecord3 a b) = (\a' -> MkRecord3 a' b) <$> f a
+
+typeChangingManualCompose :: Lens (Record3 (Record3 a)) (Record3 (Record3 b)) a b
+typeChangingManualCompose = typeChangingManual . typeChangingManual
+
 newtype L s a = L (Lens' s a)
 
 subtypeLensManual :: Lens' Record Record2
@@ -60,7 +72,19 @@
 subtypeLensGeneric :: Lens' Record Record2
 subtypeLensGeneric = super
 
+typeChangingGeneric :: Lens (Record3 a) (Record3 b) a b
+typeChangingGeneric = field @"fieldA"
+
+typeChangingGenericPos :: Lens (Record3 a) (Record3 b) a b
+typeChangingGenericPos = position @1
+
+typeChangingGenericCompose :: Lens (Record3 (Record3 a)) (Record3 (Record3 b)) a b
+typeChangingGenericCompose = field @"fieldA" . field @"fieldA"
+
 inspect $ 'fieldALensManual === 'fieldALensName
 inspect $ 'fieldALensManual === 'fieldALensType
 inspect $ 'fieldALensManual === 'fieldALensPos
 inspect $ 'subtypeLensManual === 'subtypeLensGeneric
+inspect $ 'typeChangingManual === 'typeChangingGeneric
+inspect $ 'typeChangingManual === 'typeChangingGenericPos
+inspect $ 'typeChangingManualCompose === 'typeChangingGenericCompose
diff --git a/test/doctest.hs b/test/doctest.hs
new file mode 100644
--- /dev/null
+++ b/test/doctest.hs
@@ -0,0 +1,7 @@
+import Test.DocTest
+main
+  = doctest
+      [ "-isrc"
+      , "src/Data/Generics/Product.hs"
+      , "src/Data/Generics/Sum.hs"
+      ]