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.0.0
+version:              0.4.0.1
 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.
 
@@ -41,6 +41,10 @@
                     , 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
@@ -63,9 +67,8 @@
   main-is:            Spec.hs
 
   build-depends:      base          >= 4.9 && <= 5.0
-                    , QuickCheck
-                    , hspec
                     , generic-lens
+                    , ghc-proofs >= 0.1.1
 
   default-language:   Haskell2010
   ghc-options:        -Wall
diff --git a/src/Data/Generics/Internal/HList.hs b/src/Data/Generics/Internal/HList.hs
--- a/src/Data/Generics/Internal/HList.hs
+++ b/src/Data/Generics/Internal/HList.hs
@@ -21,7 +21,7 @@
 --
 -----------------------------------------------------------------------------
 module Data.Generics.Internal.HList
-  ( (++)
+  ( type (++)
 
   , ListTuple (..)
 
@@ -151,6 +151,55 @@
     = a :> b :> c :> d:> e :> f :> g :> h :> j :> k :> l :> Nil
   listToTuple (a :> b :> c :> d :> e :> f :> g :> h :> j :> k :> l :> Nil)
     = (a, b, c, d, e, f, g, h, j, k, l)
+
+instance ListTuple (a, b, c, d, e, f, g, h, j, k, l, m) '[a, b, c, d, e, f, g, h, j, k, l, m] where
+  type ListToTuple '[a, b, c, d, e, f, g, h, j, k, l, m] = (a, b, c, d, e, f, g, h, j, k, l, m)
+  tupleToList (a, b, c, d, e, f, g, h, j, k, l, m)
+    = a :> b :> c :> d:> e :> f :> g :> h :> j :> k :> l :> m :> Nil
+  listToTuple (a :> b :> c :> d :> e :> f :> g :> h :> j :> k :> l :> m :> Nil)
+    = (a, b, c, d, e, f, g, h, j, k, l, m)
+
+instance ListTuple (a, b, c, d, e, f, g, h, j, k, l, m, n) '[a, b, c, d, e, f, g, h, j, k, l, m, n] where
+  type ListToTuple '[a, b, c, d, e, f, g, h, j, k, l, m, n] = (a, b, c, d, e, f, g, h, j, k, l, m, n)
+  tupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n)
+    = a :> b :> c :> d:> e :> f :> g :> h :> j :> k :> l :> m :> n :> Nil
+  listToTuple (a :> b :> c :> d :> e :> f :> g :> h :> j :> k :> l :> m :> n :> Nil)
+    = (a, b, c, d, e, f, g, h, j, k, l, m, n)
+
+instance ListTuple (a, b, c, d, e, f, g, h, j, k, l, m, n, o) '[a, b, c, d, e, f, g, h, j, k, l, m, n, o] where
+  type ListToTuple '[a, b, c, d, e, f, g, h, j, k, l, m, n, o] = (a, b, c, d, e, f, g, h, j, k, l, m, n, o)
+  tupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n, o)
+    = a :> b :> c :> d:> e :> f :> g :> h :> j :> k :> l :> m :> n :> o :> Nil
+  listToTuple (a :> b :> c :> d :> e :> f :> g :> h :> j :> k :> l :> m :> n :> o :> Nil)
+    = (a, b, c, d, e, f, g, h, j, k, l, m, n, o)
+
+instance ListTuple (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p) '[a, b, c, d, e, f, g, h, j, k, l, m, n, o, p] where
+  type ListToTuple '[a, b, c, d, e, f, g, h, j, k, l, m, n, o, p] = (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p)
+  tupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p)
+    = a :> b :> c :> d:> e :> f :> g :> h :> j :> k :> l :> m :> n :> o :> p :> Nil
+  listToTuple (a :> b :> c :> d :> e :> f :> g :> h :> j :> k :> l :> m :> n :> o :> p :> Nil)
+    = (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p)
+
+instance ListTuple (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q) '[a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q] where
+  type ListToTuple '[a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q] = (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q)
+  tupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q)
+    = a :> b :> c :> d:> e :> f :> g :> h :> j :> k :> l :> m :> n :> o :> p :> q :> Nil
+  listToTuple (a :> b :> c :> d :> e :> f :> g :> h :> j :> k :> l :> m :> n :> o :> p :> q :> Nil)
+    = (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q)
+
+instance ListTuple (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q, r) '[a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q, r] where
+  type ListToTuple '[a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q, r] = (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q, r)
+  tupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q, r)
+    = a :> b :> c :> d:> e :> f :> g :> h :> j :> k :> l :> m :> n :> o :> p :> q :> r :> Nil
+  listToTuple (a :> b :> c :> d :> e :> f :> g :> h :> j :> k :> l :> m :> n :> o :> p :> q :> r :> Nil)
+    = (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q, r)
+
+instance ListTuple (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q, r, s) '[a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q, r, s] where
+  type ListToTuple '[a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q, r, s] = (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q, r, s)
+  tupleToList (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q, r, s)
+    = a :> b :> c :> d:> e :> f :> g :> h :> j :> k :> l :> m :> n :> o :> p :> q :> r :> s :> Nil
+  listToTuple (a :> b :> c :> d :> e :> f :> g :> h :> j :> k :> l :> m :> n :> o :> p :> q :> r :> s :> Nil)
+    = (a, b, c, d, e, f, g, h, j, k, l, m, n, o, p, q, r, s)
 
 --------------------------------------------------------------------------------
 
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,4 +1,5 @@
-{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE GADTs         #-}
+{-# LANGUAGE Rank2Types    #-}
 {-# LANGUAGE TypeOperators #-}
 
 -----------------------------------------------------------------------------
@@ -18,7 +19,7 @@
 import Control.Applicative   (Const(..))
 import Data.Functor.Identity (Identity(..))
 import Data.Profunctor       (Choice(right'), Profunctor(dimap))
-import GHC.Generics          ((:*:)(..), (:+:)(..), Generic(..), K1(..), M1(..), Rep)
+import GHC.Generics          ((:*:)(..), (:+:)(..), Generic(..), M1(..), Rep)
 
 -- | Type alias for lens
 type Lens' s a
@@ -76,8 +77,6 @@
 mIso :: Iso' (M1 i c f p) (f p)
 mIso = dimap unM1 (fmap M1)
 
-kIso :: Iso' (K1 t a x) a
-kIso = dimap unK1 (fmap K1)
 
 sumIso :: Iso' ((a :+: b) x) (Either (a x) (b x))
 sumIso = dimap f (fmap t)
@@ -91,3 +90,20 @@
 
 _Right :: Prism' (Either c a) a
 _Right = prism Right $ either (Left . Left) Right
+
+--------------------------------------------------------------------------------
+
+data Coyoneda f b = forall a. Coyoneda (a -> b) (f a)
+
+instance Functor (Coyoneda f) where
+  fmap f (Coyoneda g fa)
+    = Coyoneda (f . g) fa
+
+inj :: Functor f => Coyoneda f a -> f a
+inj (Coyoneda f a) = fmap f a
+
+proj :: Functor f => f a -> Coyoneda f a
+proj fa = Coyoneda id fa
+
+ravel :: Functor f => ((a -> Coyoneda f b) -> s -> Coyoneda f t) -> (a -> f b) -> (s -> f t)
+ravel coy f s = inj $ coy (\a -> proj (f a)) s
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
@@ -91,7 +91,7 @@
   , GHasField field (Rep s) a
   ) => HasField field a s where
 
-  field = repIso . gfield @field
+  field = ravel (repIso . gfield @field)
 
 type family ErrorUnless (field :: Symbol) (s :: Type) (contains :: Bool) :: Constraint where
   ErrorUnless field s 'False
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
@@ -49,8 +49,11 @@
 
   gfield = combine (gfield @field @l) (gfield @field @r)
 
+instance GHasField field (K1 R a) a where
+  gfield f (K1 x) = fmap K1 (f x)
+
 instance GHasField field (S1 ('MetaSel ('Just field) upkd str infstr) (Rec0 a)) a where
-  gfield = mIso . kIso
+  gfield = mIso . gfield @field
 
 instance GHasField field f a => GHasField field (M1 D meta f) a where
   gfield = mIso . 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
@@ -42,13 +42,10 @@
 class GHasPosition (offset :: Nat) (i :: Nat) (f :: Type -> Type) a | offset i f -> a where
   gposition :: Lens' (f x) a
 
-instance GHasPosition i i (S1 meta (Rec0 a)) a where
-  gposition = mIso . kIso
-
-instance GHasPosition offset i f a => GHasPosition offset i (M1 D meta f) a where
-  gposition = mIso . gposition @offset @i
+instance GHasPosition i i (K1 R a) a where
+  gposition f (K1 x) = fmap K1 (f x)
 
-instance GHasPosition offset i f a => GHasPosition offset i (M1 C meta f) a where
+instance GHasPosition offset i f a => GHasPosition offset i (M1 m meta f) a where
   gposition = mIso . gposition @offset @i
 
 instance
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
@@ -93,7 +93,7 @@
   , GHasPosition 1 i (Rep s) a
   ) => HasPosition i a s where
 
-  position = repIso . gposition @1 @i
+  position = ravel (repIso . gposition @1 @i)
 
 type family ErrorUnless (i :: Nat) (s :: Type) (hasP :: Bool) :: Constraint where
   ErrorUnless i s 'False
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
@@ -83,7 +83,7 @@
   , GHasType (Rep s) a
   ) => HasType a s where
 
-  typed = repIso . gtyped
+  typed = ravel (repIso . gtyped)
 
 type family ErrorUnlessOne (a :: Type) (s :: Type) (count :: Count) :: Constraint where
   ErrorUnlessOne a s 'None
diff --git a/test/Spec.hs b/test/Spec.hs
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -1,1 +1,60 @@
-{-# OPTIONS_GHC -F -pgmF hspec-discover #-}
+{-# OPTIONS_GHC -O -fplugin GHC.Proof.Plugin #-}
+
+{-# LANGUAGE AllowAmbiguousTypes             #-}
+{-# LANGUAGE DataKinds                       #-}
+{-# LANGUAGE DeriveGeneric                   #-}
+{-# LANGUAGE DuplicateRecordFields           #-}
+{-# LANGUAGE ExistentialQuantification       #-}
+{-# LANGUAGE RankNTypes                      #-}
+{-# LANGUAGE ScopedTypeVariables             #-}
+{-# LANGUAGE TypeApplications                #-}
+
+module Main where
+
+import GHC.Generics
+import Data.Generics.Product
+import GHC.Proof
+
+main :: IO ()
+main = putStrLn "Hello world"
+
+data Record = MkRecord
+  { fieldA :: Int
+  , fieldB :: Bool
+  } deriving Generic
+
+data Record2 = MkRecord2
+  { fieldA :: Int
+  } deriving Generic
+
+type Lens' s a = forall f. Functor f => (a -> f a) -> s -> f s
+
+fieldALensManual :: Lens' Record Int
+fieldALensManual f (MkRecord a b) = (\a' -> MkRecord a' b) <$> f a
+
+newtype L s a = L (Lens' s a)
+
+subtypeLensManual :: Lens' Record Record2
+subtypeLensManual f record
+  = fmap (\ds -> case record of
+                  MkRecord _ b -> MkRecord (case ds of {MkRecord2 g1 -> g1}) b
+         ) (f (MkRecord2 (case record of {MkRecord a _ -> a})))
+
+--------------------------------------------------------------------------------
+-- * Tests
+-- The ghc-proofs plugin checks that the following equalities hold, by checking
+-- that the LHSs and the RHSs are CSEd. This also means that the runtime
+-- characteristics of the derived lenses is the same as the manually written
+-- ones above.
+
+fieldP :: Proof
+fieldP = L fieldALensManual === L (field @"fieldA")
+
+typedP :: Proof
+typedP = L fieldALensManual === L (typed @Int)
+
+posP :: Proof
+posP = L fieldALensManual === L (position @1)
+
+subtypeP :: Proof
+subtypeP = L subtypeLensManual === L super