diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,3 +1,9 @@
+## 0.5.1.0
+- Infer input type from result type (#25)
+- Allow changing of multiple type parameters (#24)
+- Allow changing of type parameters that have kinds other than `*` (#23)
+- Fix error message in subtype lens
+
 ## 0.5.0.0
 
 - Lenses and prisms are now type-changing.
diff --git a/examples/Examples.hs b/examples/Examples.hs
--- a/examples/Examples.hs
+++ b/examples/Examples.hs
@@ -1,17 +1,18 @@
-{-# 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 #-}
+{-# LANGUAGE AllowAmbiguousTypes          #-}
+{-# LANGUAGE DataKinds                    #-}
+{-# LANGUAGE DeriveGeneric                #-}
+{-# LANGUAGE DuplicateRecordFields        #-}
+{-# LANGUAGE FlexibleContexts             #-}
+{-# LANGUAGE GADTs                        #-}
+{-# LANGUAGE NoMonomorphismRestriction    #-}
+{-# LANGUAGE OverloadedLabels             #-}
+{-# LANGUAGE PartialTypeSignatures        #-}
+{-# LANGUAGE Rank2Types                   #-}
+{-# LANGUAGE ScopedTypeVariables          #-}
+{-# LANGUAGE TypeApplications             #-}
+{-# LANGUAGE UndecidableInstances         #-}
+{-# OPTIONS_GHC -Wno-missing-signatures   #-}
+{-# OPTIONS_GHC -fno-warn-unused-imports  #-}
 
 module Examples where
 
@@ -20,6 +21,7 @@
 import Data.Generics.Product
 import Data.Generics.Sum
 import GHC.Generics
+import Data.Generics.Labels
 
 data Animal = Animal
   { name :: String
@@ -102,3 +104,24 @@
   , HasField "bar" a' b' s t
   ) => s' -> t'
 stuff r = r & field @"test" . field @"bar" . position @15 .~ "hello"
+
+stuff' ::
+  ( HasPosition 15 s t a String
+  , HasField "test" s' t' a' b'
+  , HasField "bar" a' b' s t
+  ) => s' -> t'
+stuff' r = r & #test . #bar . position @15 .~ "hello"
+
+data Foo m s = Foo
+  { foo1 :: m s
+  , foo2 :: [s]
+  } deriving Generic
+
+modifyFoo2 :: Foo (Either String) Int -> Foo Maybe Int
+modifyFoo2 x = x & field @"foo1" .~ pure (1 :: Int)
+
+data Bar a b = Bar
+  { barField :: (a, b)
+  } deriving Generic
+
+modifiedBar = (Bar ("hello", "world")) & field @"barField" .~ ('c', 1 :: Int)
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.5.0.0
+version:              0.5.1.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.
 
@@ -25,6 +25,7 @@
                     , Data.Generics.Product.Positions
                     , Data.Generics.Product.Subtype
                     , Data.Generics.Product.Typed
+                    --, Data.Generics.Labels
 
                     , Data.Generics.Sum
                     , Data.Generics.Sum.Any
@@ -69,6 +70,30 @@
   build-depends:      base          >= 4.9 && <= 5.0
                     , generic-lens
                     , inspection-testing >= 0.1
+
+  default-language:   Haskell2010
+  ghc-options:        -Wall
+
+test-suite generic-lens-test-25
+  type:               exitcode-stdio-1.0
+  hs-source-dirs:     test
+  main-is:            25.hs
+
+  build-depends:      base          >= 4.9 && <= 5.0
+                    , generic-lens
+                    , lens
+
+  default-language:   Haskell2010
+  ghc-options:        -Wall
+
+test-suite generic-lens-test-24
+  type:               exitcode-stdio-1.0
+  hs-source-dirs:     test
+  main-is:            24.hs
+
+  build-depends:      base          >= 4.9 && <= 5.0
+                    , generic-lens
+                    , lens
 
   default-language:   Haskell2010
   ghc-options:        -Wall
diff --git a/src/Data/Generics/Internal/Families/Changing.hs b/src/Data/Generics/Internal/Families/Changing.hs
--- a/src/Data/Generics/Internal/Families/Changing.hs
+++ b/src/Data/Generics/Internal/Families/Changing.hs
@@ -2,14 +2,19 @@
 {-# LANGUAGE DataKinds              #-}
 {-# LANGUAGE FlexibleInstances      #-}
 {-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE GADTs                  #-}
 {-# LANGUAGE PolyKinds              #-}
 {-# LANGUAGE TypeFamilies           #-}
 {-# LANGUAGE TypeOperators          #-}
 {-# LANGUAGE UndecidableInstances   #-}
 
-module Data.Generics.Internal.Families.Changing where
+module Data.Generics.Internal.Families.Changing
+  ( Proxied
+  , Infer
+  ) where
 
-import GHC.TypeLits (Nat, type (+))
+import GHC.TypeLits (TypeError, ErrorMessage (..))
+import Data.Type.Bool (If)
 
 {-
   Note [Changing type parameters]
@@ -35,53 +40,106 @@
   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
+-- `P` can be used in place of any type parameter, which means that it can have
+-- any kind, not just *, so a data type won't work.
+-- (this caused https://github.com/kcsongor/generic-lens/issues/23)
+-- Instead, we use a matchable type family to wrap any `k` - however, we can no longer directly
+-- pattern match on `P`, as it's not a type constructor. But we can still take it apart as a polymorphic
+-- application form. In order to distinguish between applications of P and other type constructors, we use a tag, `PTag`
+-- to fake a type constructor.
+data PTag = PTag
+type family P :: Peano -> k -> PTag -> k
 
-type family Proxied' (t :: k) (next :: Nat) :: k where
-  Proxied' (t a :: k) next = (Proxied' t (next + 1)) (P next a)
+type Proxied t = Proxied' t 'Z
+
+type family Proxied' (t :: k) (next :: Peano) :: k where
+  Proxied' (t (a :: j) :: k) next = (Proxied' t ('S next)) (P next a 'PTag)
   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
+data Sub where
+  Sub :: Peano -> k -> Sub
 
-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 Unify (a :: k) (b :: k) :: [Sub] where
+  Unify (a b) a' = If (IsPTag b) '[HandleP (a b) a'] (HandleOther (a b) a')
+  Unify a a = '[]
+  Unify a b = TypeError
+                ( 'Text "Couldn't match type "
+                  ':<>: 'ShowType a
+                  ':<>: 'Text " with "
+                  ':<>: 'ShowType b
+                )
 
-type family UnApply (a :: k) :: [*] where
-  UnApply (f x) = x ': UnApply f
-  UnApply x     = '[]
+type family HandleP a b where
+  HandleP (p n _ 'PTag) a' = 'Sub n a'
 
-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 HandleOther a b where
+  HandleOther (a x) (b y) = Unify x y ++ Unify a b
+  HandleOther a a = '[]
+  HandleOther a b = TypeError
+                     ( 'Text "Couldn't match type "
+                       ':<>: 'ShowType a
+                       ':<>: 'Text " with "
+                       ':<>: 'ShowType b
+                     )
 
-type family PSub (subs :: [(*, *)]) :: [(Nat, *)] where
-  PSub '[] = '[]
-  PSub ('(P n _, b) ': xs) = '(n, b) ': PSub xs
-  PSub (_ ': xs) = PSub xs
+type family IsPTag (a :: k) :: Bool where
+  IsPTag 'PTag = 'True
+  IsPTag _ = 'False
 
-type family Zip (xs :: [k]) (ys :: [l]) :: [(k, l)] where
-  Zip '[] '[] = '[]
-  Zip (x ': xs) (y ': ys) = '(x, y) ': Zip xs ys
+type family (xs :: [k]) ++ (ys :: [k]) :: [k] where
+  '[] ++ ys = ys
+  (x ': xs) ++ ys = x ': (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' :: *) (b :: *) :: * where
+  Infer (s a) a' b
+    = ReplaceArgs (s a) (Unify a' b)
+  Infer s _ _ = s
 
-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
+data Peano = Z | S Peano
+
+-- [TODO]: work this out
+--
+--type family ArgKind (t :: k) (pos :: Peano) :: * where
+--  ArgKind (t (a :: k)) 'Z = k
+--  ArgKind (t _) ('S pos) = ArgKind t pos
+--
+--type family ReplaceArg (t :: k) (pos :: Peano) (to :: ArgKind t pos) :: k where
+--  ReplaceArg (t a) 'Z to = t to
+--  ReplaceArg (t a) ('S pos) to = ReplaceArg t pos to a
+--  ReplaceArg t _ _ = t
+
+type family ReplaceArg (t :: k) (pos :: Peano) (to :: j) :: k where
+  ReplaceArg (t a) 'Z to = t to
+  ReplaceArg (t a) ('S pos) to = ReplaceArg t pos to a
+  ReplaceArg t _ _ = t
+
+type family ReplaceArgs (t :: k) (subs :: [Sub]) :: k where
+  ReplaceArgs t '[] = t
+  ReplaceArgs t ('Sub n arg ': ss) = ReplaceArgs (ReplaceArg t n arg) ss
+
+-- Note [CPP in instance constraints]
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+--
+-- In GHC 8.0.2, the calculated size of the expressions is too large for the
+-- inliner to consider them under the default -funfolding-use-threshold value
+-- (60).
+--
+-- To reduce the size, the constraints
+--
+-- ```
+-- s' ~ Proxied s
+-- t' ~ Proxied t
+-- ```
+--
+-- are written as the following single equality:
+--
+-- ```
+-- '(s', t') ~ '(Proxied s, Proxied t)
+-- ```
+--
+-- However, for some reason, this violates the functional dependencies on 8.2.2.
+-- Therefore, when using a newer version of the compiler, the original constraints
+-- are used, as the expression size is smaller under 8.2.2.
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,4 +1,5 @@
 {-# LANGUAGE AllowAmbiguousTypes     #-}
+{-# LANGUAGE CPP                     #-}
 {-# LANGUAGE ConstraintKinds         #-}
 {-# LANGUAGE DataKinds               #-}
 {-# LANGUAGE FlexibleInstances       #-}
@@ -75,7 +76,7 @@
 -- :}
 
 -- |Records that have a field with a given name.
-class HasField (field :: Symbol) s t a b | s field -> a, s field b -> t where
+class HasField (field :: Symbol) s t a b | s field -> a, s field b -> t, t field a -> s where
   -- |A lens that focuses on a field with a given name. Compatible with the
   --  lens package's 'Control.Lens.Lens' type.
   --
@@ -127,20 +128,26 @@
   ( Generic s
   , ErrorUnless field s (CollectField field (Rep s))
   , Generic t
+  -- see Note [CPP in instance constraints]
+#if __GLASGOW_HASKELL__ < 802
+  , '(s', t') ~ '(Proxied s, Proxied t)
+#else
   , s' ~ Proxied s
+  , t' ~ Proxied t
+#endif
   , Generic s'
+  , Generic t'
   , GHasField' field (Rep s) a
   , GHasField' field (Rep s') a'
+  , GHasField' field (Rep t') b'
   , GHasField field (Rep s) (Rep t) a b
-  , '(t, b) ~ Infer s' a' a (PickTv a' b)
+  , t ~ Infer s a' b
+  , s ~ Infer t b' a
   ) => HasField field s t a b where
 
   field f s = ravel (repLens . gfield @field) f s
 
--- See Note [Uncluttering type signatures]
-instance {-# OVERLAPPING #-} HasField f (Void2 t a) t a b where
-  field = undefined
-
+-- -- See Note [Uncluttering type signatures]
 instance {-# OVERLAPPING #-} HasField f (Void1 a) (Void1 b) a b where
   field = undefined
 
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,3 +1,4 @@
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE AllowAmbiguousTypes    #-}
 {-# LANGUAGE ConstraintKinds        #-}
 {-# LANGUAGE DataKinds              #-}
@@ -70,7 +71,7 @@
 -- :}
 
 -- |Records that have a field at a given position.
-class HasPosition (i :: Nat) s t a b | s i -> a, s i b -> t where
+class HasPosition (i :: Nat) s t a b | s i -> a, s i b -> t, t i a -> s where
   -- |A lens that focuses on a field at a given position. Compatible with the
   --  lens package's 'Control.Lens.Lens' type.
   --
@@ -99,17 +100,27 @@
   ( Generic s
   , ErrorUnless i s (0 <? i && i <=? Size (Rep s))
   , Generic t
+  -- see Note [CPP in instance constraints]
+#if __GLASGOW_HASKELL__ < 802
+  , '(s', t') ~ '(Proxied s, Proxied t)
+#else
   , s' ~ Proxied s
+  , t' ~ Proxied t
+#endif
+  , Generic s'
+  , Generic t'
   , 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)
+  , t ~ Infer s a' b
+  , GHasPosition' i (Rep t') b'
+  , s ~ Infer t b' a
   ) => HasPosition i s t a b where
 
   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
+instance {-# OVERLAPPING #-} HasPosition f (Void1 a) (Void1 b) a b where
   position = undefined
 
 type family ErrorUnless (i :: Nat) (s :: Type) (hasP :: Bool) :: Constraint where
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
@@ -91,8 +91,8 @@
   --
   -- >>> upcast (upcast human :: Animal) :: Human
   -- ...
-  -- ... The type 'Human' is not a subtype of 'Animal'.
-  -- ... The following fields are missing from 'Human':
+  -- ... The type 'Animal' is not a subtype of 'Human'.
+  -- ... The following fields are missing from 'Animal':
   -- ... address
   -- ...
   upcast :: sub -> sup
@@ -123,11 +123,11 @@
 instance {-# OVERLAPPING #-} Subtype Void a where
   super = undefined
 
-type family ErrorUnless (sub :: Type) (sup :: Type) (diff :: [Symbol]) :: Constraint where
+type family ErrorUnless (sup :: Type) (sub :: Type) (diff :: [Symbol]) :: Constraint where
   ErrorUnless _ _ '[]
     = ()
 
-  ErrorUnless sub sup fs
+  ErrorUnless sup sub fs
     = TypeError
         (     'Text "The type '"
         ':<>: 'ShowType sub
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
@@ -1,4 +1,5 @@
 {-# LANGUAGE AllowAmbiguousTypes    #-}
+{-# LANGUAGE CPP                    #-}
 {-# LANGUAGE DataKinds              #-}
 {-# LANGUAGE FlexibleInstances      #-}
 {-# LANGUAGE FunctionalDependencies #-}
@@ -102,12 +103,21 @@
   ( Generic s
   , ErrorUnless ctor s (HasCtorP ctor (Rep s))
   , Generic t
+  -- see Note [CPP in instance constraints]
+#if __GLASGOW_HASKELL__ < 802
+  , '(s', t') ~ '(Proxied s, Proxied t)
+#else
   , s' ~ Proxied s
+  , t' ~ Proxied t
+#endif
   , Generic s'
+  , Generic t'
   , 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)
+  , t ~ Infer s a' b
+  , GAsConstructor' ctor (Rep t') b'
+  , s ~ Infer t b' a
   ) => AsConstructor ctor s t a b where
 
   _Ctor = repIso . _GCtor @ctor
diff --git a/test/24.hs b/test/24.hs
new file mode 100644
--- /dev/null
+++ b/test/24.hs
@@ -0,0 +1,47 @@
+{-# LANGUAGE DataKinds, DeriveGeneric, TypeApplications #-}
+
+module Main where
+
+-- Test case from #24, comments preserved
+import Control.Lens
+import Data.Generics.Product.Fields
+import Data.Generics.Product.Positions
+import GHC.Generics
+
+data Foo a b = Foo { x1 :: a, x2 :: b } deriving (Generic, Show)
+
+data Bar a b = Bar { x3 :: Foo a b, x4 :: Int } deriving (Generic, Show)
+
+tup :: ((Int, Char), Int)
+tup = ((1, 'a'), 2)
+tup2, tup3, tup4 :: ((Char, Char), Int)
+tup2 = tup & _1 . _1 %~ toEnum  -- Works.
+tup3 = tup & x %~ toEnum  -- Works also with type annotation.
+  where x :: Lens ((Int, Char), Int) ((Char, Char), Int) Int Char
+        x = _1 . _1
+-- Works.
+tup4 = tup & position @1 . position @1 %~ toEnum
+
+foo :: Foo Int Char
+foo = Foo 1 'a'
+foo2, foo3 :: Foo Char Char
+foo2 = foo & field @"x1" %~ toEnum  -- Works when there's just one 'field'.
+foo3 = foo & position @1 %~ toEnum -- Works when there's just one 'position'.
+
+bar :: Bar Int Char
+bar = Bar (Foo 1 'a') 2
+bar2, bar3, bar4 :: Bar Char Char
+-- Doesn't work, error at first 'field' (Couldn't match type ‘Int’ with ‘Char’ arising from a use of ‘field’).
+bar2 = bar & field @"x3" . field @"x1" %~ toEnum
+-- Type annotation doesn't help.
+bar3 = bar & l %~ toEnum
+  where l :: Lens (Bar Int Char) (Bar Char Char) Int Char
+        l = field @"x3" . field @"x1"
+-- Doesn't work, error at first 'position' (Couldn't match type ‘Int’ with ‘Char’ arising from a use of ‘position’).
+bar4 = bar & position @1 . position @1 %~ toEnum
+-- Works if we stick to simple Lens' (modify to the same type).
+bar5 :: Bar Int Char
+bar5 = bar & field @"x3" . field @"x1" %~ (+1)
+
+main :: IO ()
+main = print bar5
diff --git a/test/25.hs b/test/25.hs
new file mode 100644
--- /dev/null
+++ b/test/25.hs
@@ -0,0 +1,33 @@
+{-# LANGUAGE DuplicateRecordFields #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# OPTIONS_GHC -Wall #-}
+
+module Main where
+
+import Control.Lens
+import Data.Generics.Product
+import GHC.Generics
+
+data Record1 = Record1
+    { field1 :: Int
+    , field2 :: Double
+    } deriving (Generic)
+
+class Default a where
+    def :: a
+
+instance Default Record1 where
+    def = Record1 0 0.0
+
+f :: Record1 -> Int
+f r = r ^. field @"field1"
+
+main :: IO ()
+main = do
+    print $ f def
+    print $ f ( field @"field1" .~ 1 $ (def :: Record1))
+    print $ f ( field @"field1" .~ 2 $ Record1 0 0.0)
+    print $ f ( field @"field1" .~ (1 :: Int) $ def)
+    print $ f ( position @1 .~ (1 :: Int) $ def)