diff --git a/examples/ASTExamples.hs b/examples/ASTExamples.hs
--- a/examples/ASTExamples.hs
+++ b/examples/ASTExamples.hs
@@ -10,9 +10,9 @@
 
 -- Replace ASTUse with ASTTHUse below if you want
 -- to test TH code generation.
-import AST
 import ASTUse
 -- import ASTTHUse
+import AST
 
 import Generics.MultiRec.Base
 import Generics.MultiRec.Compos
@@ -58,8 +58,8 @@
 (&.) = (F.&)
 
 evalAlgebra1 :: F.Algebra AST Value
-evalAlgebra1 _ =  
- 
+evalAlgebra1 _ =
+
       tag  (   con (\ (K x)                   -> EV (const x))
            &.  con (\ (I (EV x) :*: I (EV y)) -> EV (\ env -> x env  +  y env))
            &.  con (\ (I (EV x) :*: I (EV y)) -> EV (\ env -> x env  *  y env))
@@ -102,12 +102,12 @@
 -- | Test for 'eval1'
 
 testEval1 :: Int
-testEval1 = eval1 example [("y", -12)] 
+testEval1 = eval1 example [("y", -12)]
 
 -- | Test for 'eval2'
 
 testEval2 :: Int
-testEval2 = eval2 example [("y", -12)] 
+testEval2 = eval2 example [("y", -12)]
 
 -- | Equality instance for 'Expr'
 
diff --git a/examples/ASTTHUse.hs b/examples/ASTTHUse.hs
--- a/examples/ASTTHUse.hs
+++ b/examples/ASTTHUse.hs
@@ -6,6 +6,7 @@
 {-# LANGUAGE TypeSynonymInstances  #-}
 {-# LANGUAGE EmptyDataDecls        #-}
 {-# LANGUAGE TemplateHaskell       #-}
+{-# LANGUAGE FlexibleInstances     #-}
 
 module ASTTHUse where
 
@@ -22,12 +23,5 @@
   Decl  ::  AST Decl
   Var   ::  AST Var
 
--- ** Constructors
-
-$(deriveConstructors [''Expr, ''Decl, ''Var])
-
--- ** Functor encoding and 'Ix' instances
-
-$(deriveSystem ''AST [''Expr, ''Decl, ''Var] "PFAST")
-type instance PF AST = PFAST
+$(deriveAll ''AST)
 
diff --git a/examples/ASTUse.hs b/examples/ASTUse.hs
--- a/examples/ASTUse.hs
+++ b/examples/ASTUse.hs
@@ -5,13 +5,14 @@
 {-# LANGUAGE TypeOperators         #-}
 {-# LANGUAGE TypeSynonymInstances  #-}
 {-# LANGUAGE EmptyDataDecls        #-}
+{-# LANGUAGE FlexibleInstances     #-}
 
 module ASTUse where
 
 import Generics.MultiRec.Base
 import AST
 
--- * Instantiating the library for AST 
+-- * Instantiating the library for AST
 
 -- ** Index type
 
diff --git a/examples/SingleTHUse.hs b/examples/SingleTHUse.hs
--- a/examples/SingleTHUse.hs
+++ b/examples/SingleTHUse.hs
@@ -18,9 +18,4 @@
 data LogicF :: * -> * where
   Logic :: LogicF Logic
 
--- ** Constructors
-$(deriveConstructors [''Logic])
-
--- ** Functor encoding and 'Ix' instances
-$(deriveSystem ''LogicF [''Logic] "PFLogic")
-type instance PF LogicF = PFLogic
+$(deriveAll ''LogicF)
diff --git a/multirec.cabal b/multirec.cabal
--- a/multirec.cabal
+++ b/multirec.cabal
@@ -1,5 +1,5 @@
 name:                 multirec
-version:              0.6
+version:              0.7
 license:              BSD3
 license-file:         LICENSE
 author:               Alexey Rodriguez,
@@ -79,4 +79,5 @@
                       -- Extra
                       Generics.MultiRec.TEq
 
-  build-depends:      base >= 3.0 && < 5, template-haskell >= 2.2 && < 2.7
+  build-depends:      base >= 3.0 && < 5,
+                      template-haskell >= 2.4 && < 2.7
diff --git a/src/Generics/MultiRec/Base.hs b/src/Generics/MultiRec/Base.hs
--- a/src/Generics/MultiRec/Base.hs
+++ b/src/Generics/MultiRec/Base.hs
@@ -85,7 +85,7 @@
 
 -- | Represents composition with functors
 -- of kind * -> *.
-data (f :.: g) (r :: * -> *) ix = D (f (g r ix))
+data (f :.: g) (r :: * -> *) ix = D {unD :: f (g r ix)}
 
 -- | Represents constructors.
 data C c f     (r :: * -> *) ix where
@@ -116,7 +116,7 @@
 -- * Indexed families
 
 -- | Type family describing the pattern functor of a family.
-type family PF phi :: (* -> *) -> * -> *
+type family PF (phi :: * -> *) :: (* -> *) -> * -> *
 
 -- | Class for the members of a family.
 class El phi ix where
diff --git a/src/Generics/MultiRec/ConNames.hs b/src/Generics/MultiRec/ConNames.hs
--- a/src/Generics/MultiRec/ConNames.hs
+++ b/src/Generics/MultiRec/ConNames.hs
@@ -3,7 +3,6 @@
 {-# LANGUAGE TypeOperators    #-}
 {-# LANGUAGE KindSignatures   #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE PatternSignatures #-}
 
 -----------------------------------------------------------------------------
 -- |
diff --git a/src/Generics/MultiRec/Fold.hs b/src/Generics/MultiRec/Fold.hs
--- a/src/Generics/MultiRec/Fold.hs
+++ b/src/Generics/MultiRec/Fold.hs
@@ -22,7 +22,7 @@
 -- There are several variants of fold in other modules that are probably
 -- easier to use:
 --
---   * for folds with constant return type, look at 
+--   * for folds with constant return type, look at
 --     "Generics.MultiRec.FoldAlgK" (or "Generics.MultiRec.FoldK"),
 --
 --   * for folds with convenient algebras, look at
@@ -36,7 +36,6 @@
 import Generics.MultiRec.HFunctor
 
 import Control.Monad hiding (foldM)
-import Control.Applicative
 
 -- * Generic fold and unfold
 
diff --git a/src/Generics/MultiRec/Read.hs b/src/Generics/MultiRec/Read.hs
--- a/src/Generics/MultiRec/Read.hs
+++ b/src/Generics/MultiRec/Read.hs
@@ -6,7 +6,6 @@
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE GADTs                 #-}
-{-# LANGUAGE PatternSignatures     #-}
 
 -----------------------------------------------------------------------------
 -- |
@@ -27,8 +26,7 @@
 
 import Control.Monad
 import Data.Char
-import Data.Traversable
-import Text.ParserCombinators.ReadP (char, skipSpaces, sepBy)
+import Text.ParserCombinators.ReadP (sepBy)
 import Text.Read hiding (readsPrec, readPrec)
 import Prelude hiding (readsPrec)
 import qualified Prelude as P (readsPrec)
diff --git a/src/Generics/MultiRec/TH.hs b/src/Generics/MultiRec/TH.hs
--- a/src/Generics/MultiRec/TH.hs
+++ b/src/Generics/MultiRec/TH.hs
@@ -21,7 +21,8 @@
 
 
 module Generics.MultiRec.TH
-  ( deriveConstructors,
+  ( deriveAll,
+    deriveConstructors,
     deriveFamily, deriveSystem,
     derivePF,
     deriveEl,
@@ -31,73 +32,93 @@
 
 import Generics.MultiRec.Base
 import Language.Haskell.TH hiding (Fixity())
-import Language.Haskell.TH.Syntax (Lift(..))
+import Control.Applicative
 import Control.Monad
 
--- | Given a list of datatype names, derive datatypes and
--- instances of class 'Constructor'.
+-- | Given the name of the family index GADT, derive everything.
+deriveAll :: Name -> Q [Dec]
+deriveAll n =
+  do
+    info <- reify n
+    -- runIO (print info)
+    let ns = map remakeName (extractConstructorNames info)
+    cs  <- deriveConstructors ns
+    pf  <- derivePFInstance n ns
+    el  <- deriveEl n ns
+    fam <- deriveFam n ns
+    eq  <- deriveEqS n ns
+    return $ cs ++ pf ++ el ++ fam ++ eq
 
+-- | Given a list of datatype names, derive datatypes and
+-- instances of class 'Constructor'. Not needed if 'deriveAll'
+-- is used.
 deriveConstructors :: [Name] -> Q [Dec]
 deriveConstructors =
   liftM concat . mapM constrInstance
 
--- | Given the name of the index GADT, the names of the
+-- | Compatibility. Use 'deriveAll' instead.
+--
+-- Given the name of the index GADT, the names of the
 -- types in the family, and the name (as string) for the
 -- pattern functor to derive, generate the 'Ix' and 'PF'
 -- instances. /IMPORTANT/: It is assumed that the constructors
 -- of the GADT have the same names as the datatypes in the
 -- family.
-
+{-# DEPRECATED deriveFamily "Use deriveAll instead." #-}
 deriveFamily :: Name -> [Name] -> String -> Q [Dec]
 deriveFamily n ns pfn =
   do
     pf  <- derivePF pfn ns
     el  <- deriveEl n ns
     fam <- deriveFam n ns
-    eq  <- deriveEqS n (map (mkName . nameBase) ns)
+    eq  <- deriveEqS n (map remakeName ns)
     return $ pf ++ el ++ fam ++ eq
 
--- | Compatibility. Use deriveFamily instead.
-
+-- | Compatibility. Use 'deriveAll' instead.
+{-# DEPRECATED deriveSystem "Use deriveFamily instead" #-}
 deriveSystem :: Name -> [Name] -> String -> Q [Dec]
 deriveSystem = deriveFamily
 
--- | Derive only the 'PF' instance. Not needed if 'deriveFamily'
+-- | Derive only the 'PF' instance. Not needed if 'deriveAll'
 -- is used.
-
 derivePF :: String -> [Name] -> Q [Dec]
 derivePF pfn ns =
-    fmap (:[]) $
+    return <$>
     tySynD (mkName pfn) [] (foldr1 sum (map (pfType ns) ns))
   where
     sum :: Q Type -> Q Type -> Q Type
     sum a b = conT ''(:+:) `appT` a `appT` b
 
--- | Derive only the 'El' instances. Not needed if 'deriveFamily'
--- is used.
+derivePFInstance :: Name -> [Name] -> Q [Dec]
+derivePFInstance n ns =
+    return <$>
+    tySynInstD ''PF [conT n] (foldr1 sum (map (pfType ns) ns))
+  where
+    sum :: Q Type -> Q Type -> Q Type
+    sum a b = conT ''(:+:) `appT` a `appT` b
 
+-- | Derive only the 'El' instances. Not needed if 'deriveAll'
+-- is used.
 deriveEl :: Name -> [Name] -> Q [Dec]
 deriveEl s ns =
   mapM (elInstance s) ns
 
--- | Derive only the 'Fam' instance. Not needed if 'deriveFamily'
+-- | Derive only the 'Fam' instance. Not needed if 'deriveAll'
 -- is used.
-
 deriveFam :: Name -> [Name] -> Q [Dec]
 deriveFam s ns =
   do
     fcs <- liftM concat $ zipWithM (mkFrom ns (length ns)) [0..] ns
     tcs <- liftM concat $ zipWithM (mkTo   ns (length ns)) [0..] ns
-    liftM (:[]) $
+    return <$>
       instanceD (cxt []) (conT ''Fam `appT` conT s)
         [funD 'from fcs, funD 'to tcs]
 
--- | Derive only the 'EqS' instance. Not needed if 'deriveFamily'
+-- | Derive only the 'EqS' instance. Not needed if 'deriveAll'
 -- is used.
-
 deriveEqS :: Name -> [Name] -> Q [Dec]
 deriveEqS s ns =
-    liftM (:[]) $
+    return <$>
     instanceD (cxt []) (conT ''EqS `appT` conT s)
       [funD 'eqS (trues ++ falses)]
   where
@@ -106,6 +127,31 @@
     trues        = map trueClause ns
     falses       = if length trues == 1 then [] else [falseClause]
 
+-- | Process the reified info of the index GADT, and extract
+-- its constructor names, which are also the names of the datatypes
+-- that are part of the family.
+extractConstructorNames :: Info -> [Name]
+extractConstructorNames (TyConI (DataD _ _ _ cs _)) = concatMap extractFrom cs
+  where
+    extractFrom :: Con -> [Name]
+    extractFrom (ForallC _ _ c) = extractFrom c
+    extractFrom (InfixC _ n _)  = [n]
+    extractFrom (RecC n _)      = [n]
+    extractFrom (NormalC n [])  = [n]
+    extractFrom _               = []
+extractConstructorNames _                           = []
+
+-- | Turn a record-constructor into a normal constructor by just
+-- removing all the field names.
+stripRecordNames :: Con -> Con
+stripRecordNames (RecC n f) =
+  NormalC n (map (\(_, s, t) -> (s, t)) f)
+stripRecordNames c = c
+
+-- | Takes the name of a datatype (element of the family).
+-- By reifying the datatype, we obtain its constructors.
+-- For each constructor, we then generate a constructor-specific
+-- datatype, and an instance of the 'Constructor' class.
 constrInstance :: Name -> Q [Dec]
 constrInstance n =
   do
@@ -118,80 +164,105 @@
     is <- mapM mkInstance cs
     return $ ds ++ is
 
-stripRecordNames :: Con -> Con
-stripRecordNames (RecC n f) =
-  NormalC n (map (\(_, s, t) -> (s, t)) f)
-stripRecordNames c = c
-
+-- | Given a constructor, create an empty datatype of
+-- the same name.
 mkData :: Con -> Q Dec
 mkData (NormalC n _) =
-  dataD (cxt []) (mkName (nameBase n)) [] [] []
+  dataD (cxt []) (remakeName n) [] [] []
 mkData r@(RecC _ _) =
   mkData (stripRecordNames r)
 mkData (InfixC t1 n t2) =
   mkData (NormalC n [t1,t2])
+mkData (ForallC _ _ c) =
+  mkData c
 
-instance Lift Fixity where
-  lift Prefix      = conE 'Prefix
-  lift (Infix a n) = conE 'Infix `appE` [| a |] `appE` [| n |]
+fixity :: Fixity -> ExpQ
+fixity Prefix      = conE 'Prefix
+fixity (Infix a n) = conE 'Infix `appE` assoc a `appE` [| n |]
 
-instance Lift Associativity where
-  lift LeftAssociative  = conE 'LeftAssociative
-  lift RightAssociative = conE 'RightAssociative
-  lift NotAssociative   = conE 'NotAssociative
+assoc :: Associativity -> ExpQ
+assoc LeftAssociative  = conE 'LeftAssociative
+assoc RightAssociative = conE 'RightAssociative
+assoc NotAssociative   = conE 'NotAssociative
 
+-- | Given a constructor, create an instance of the 'Constructor'
+-- class for the datatype associated with the constructor.
 mkInstance :: Con -> Q Dec
 mkInstance (NormalC n _) =
-    instanceD (cxt []) (appT (conT ''Constructor) (conT $ mkName (nameBase n)))
+    instanceD (cxt []) (appT (conT ''Constructor) (conT $ remakeName n))
       [funD 'conName [clause [wildP] (normalB (stringE (nameBase n))) []]]
 mkInstance r@(RecC _ _) =
   mkInstance (stripRecordNames r)
+mkInstance (ForallC _ _ c) =
+  mkInstance c
 mkInstance (InfixC t1 n t2) =
     do
       i <- reify n
       let fi = case i of
                  DataConI _ _ _ f -> convertFixity f
                  _ -> Prefix
-      instanceD (cxt []) (appT (conT ''Constructor) (conT $ mkName (nameBase n)))
+      instanceD (cxt []) (appT (conT ''Constructor) (conT $ remakeName n))
         [funD 'conName   [clause [wildP] (normalB (stringE (nameBase n))) []],
-         funD 'conFixity [clause [wildP] (normalB [| fi |]) []]]
+         funD 'conFixity [clause [wildP] (normalB (fixity fi)) []]]
   where
     convertFixity (Fixity n d) = Infix (convertDirection d) n
     convertDirection InfixL = LeftAssociative
     convertDirection InfixR = RightAssociative
     convertDirection InfixN = NotAssociative
 
+-- | Takes all the names of datatypes belonging to the family, and
+-- a particular of these names. Produces the right hand side of the 'PF'
+-- type family instance for this family.
 pfType :: [Name] -> Name -> Q Type
 pfType ns n =
     do
       -- runIO $ putStrLn $ "processing " ++ show n
       i <- reify n
       let b = case i of
+                -- datatypes are nested binary sums of their constructors
                 TyConI (DataD _ _ _ cs _) ->
                   foldr1 sum (map (pfCon ns) cs)
+                -- type synonyms are always treated as constants
                 TyConI (TySynD t _ _) ->
                   conT ''K `appT` conT t
                 _ -> error "unknown construct"
-      appT (appT (conT ''(:>:)) b) (conT $ mkName (nameBase n))
+      appT (appT (conT ''(:>:)) b) (conT $ remakeName n)
   where
     sum :: Q Type -> Q Type -> Q Type
     sum a b = conT ''(:+:) `appT` a `appT` b
 
+-- | Takes all the names of datatypes belonging to the family, and
+-- a particular name of a constructor of one of the datatypes. Creates
+-- the product structure for this constructor.
 pfCon :: [Name] -> Con -> Q Type
+pfCon ns r@(RecC _ _) =
+  pfCon ns (stripRecordNames r)
+pfCon ns (InfixC t1 n t2) =
+    pfCon ns (NormalC n [t1,t2])
+pfCon ns (ForallC _ _ c) =
+    pfCon ns c
 pfCon ns (NormalC n []) =
-    appT (appT (conT ''C) (conT $ mkName (nameBase n))) (conT ''U)
+    -- a constructor without arguments is represented using 'U'
+    appT (appT (conT ''C) (conT $ remakeName n)) (conT ''U)
 pfCon ns (NormalC n fs) =
-    appT (appT (conT ''C) (conT $ mkName (nameBase n))) (foldr1 prod (map (pfField ns . snd) fs))
+    -- a constructor with arguments is a nested binary product
+    appT (appT (conT ''C) (conT $ remakeName n))
+         (foldr1 prod (map (pfField ns . snd) fs))
   where
     prod :: Q Type -> Q Type -> Q Type
     prod a b = conT ''(:*:) `appT` a `appT` b
-pfCon ns r@(RecC _ _) =
-  pfCon ns (stripRecordNames r)
-pfCon ns (InfixC t1 n t2) =
-    pfCon ns (NormalC n [t1,t2])
 
+-- | Takes all the names of datatypes belonging to the family, and
+-- a particular type (that occurs as a field in one of these
+-- datatypes). Produces the structure for this type. We have to
+-- distinguish between recursive calls, compositions, and constants.
+--
+-- TODO: We currently treat all applications as compositions. However,
+-- we can argue that applications should be treated as compositions only
+-- if the entire construct cannot be treated as a constant.
 pfField :: [Name] -> Type -> Q Type
-pfField ns t@(ConT n) | n `elem` ns = conT ''I `appT` return t
+pfField ns t@(ConT n)
+  | remakeName n `elem` ns          = conT ''I `appT` return t
 pfField ns t@(AppT f a)             = conT ''(:.:) `appT` return f `appT` pfField ns a
 pfField ns t                        = conT ''K `appT` return t
 
@@ -206,7 +277,7 @@
       -- runIO $ putStrLn $ "processing " ++ show n
       let wrapE e = lrE m i (conE 'Tag `appE` e)
       i <- reify n
-      let dn = mkName (nameBase n)
+      let dn = remakeName n
       let b = case i of
                 TyConI (DataD _ _ _ cs _) ->
                   zipWith (fromCon wrapE ns dn (length cs)) [0..] cs
@@ -221,7 +292,7 @@
       -- runIO $ putStrLn $ "processing " ++ show n
       let wrapP p = lrP m i (conP 'Tag [p])
       i <- reify n
-      let dn = mkName (nameBase n)
+      let dn = remakeName n
       let b = case i of
                 TyConI (DataD _ _ _ cs _) ->
                   zipWith (toCon wrapP ns dn (length cs)) [0..] cs
@@ -232,7 +303,7 @@
 
 mkProof :: Name -> Q Dec
 mkProof n =
-  funD 'proof [clause [] (normalB (conE (mkName (nameBase n)))) []]
+  funD 'proof [clause [] (normalB (conE (remakeName n))) []]
 
 fromCon :: (Q Exp -> Q Exp) -> [Name] -> Name -> Int -> Int -> Con -> Q Clause
 fromCon wrap ns n m i (NormalC cn []) =
@@ -250,6 +321,8 @@
   fromCon wrap ns n m i (stripRecordNames r)
 fromCon wrap ns n m i (InfixC t1 cn t2) =
   fromCon wrap ns n m i (NormalC cn [t1,t2])
+fromCon wrap ns n m i (ForallC _ _ c) =
+  fromCon wrap ns n m i c
 
 toCon :: (Q Pat -> Q Pat) -> [Name] -> Name -> Int -> Int -> Con -> Q Clause
 toCon wrap ns n m i (NormalC cn []) =
@@ -259,29 +332,35 @@
 toCon wrap ns n m i (NormalC cn fs) =
     -- runIO (putStrLn ("constructor " ++ show ix)) >>
     clause
-      [conP n [], wrap $ lrP m i $ conP 'C [foldr1 prod (zipWith (toField ns) [0..] (map snd fs))]]
-      (normalB $ foldl appE (conE cn) (zipWith toFieldR [0..] (map snd fs))) []
+      [conP n [], wrap $ lrP m i $ conP 'C [foldr1 prod (map (varP . field) [0..length fs - 1])]]
+      (normalB $ foldl appE (conE cn) (zipWith (toField ns) [0..] (map snd fs))) []
   where
     prod x y = conP '(:*:) [x,y]
 toCon wrap ns n m i r@(RecC _ _) =
   toCon wrap ns n m i (stripRecordNames r)
 toCon wrap ns n m i (InfixC t1 cn t2) =
   toCon wrap ns n m i (NormalC cn [t1,t2])
+toCon wrap ns n m i (ForallC _ _ c) =
+  toCon wrap ns n m i c
 
 fromField :: [Name] -> Int -> Type -> Q Exp
-fromField ns nr t@(ConT n) | n `elem` ns = [| I (I0 $(varE (field nr))) |]
-fromField ns nr t@(AppT f a)             = [| D (fmap (I . I0) $(varE (field nr))) |]
-fromField ns nr t                        = [| K $(varE (field nr)) |]
+fromField ns nr t = [| $(fromFieldFun ns t) $(varE (field nr)) |]
 
-toField :: [Name] -> Int -> Type -> Q Pat
-toField ns nr t@(ConT n) | n `elem` ns = conP 'I [conP 'I0 [varP (field nr)]]
-toField ns nr t@(AppT f a)             = conP 'D [varP (field nr)]
-toField ns nr t                        = conP 'K [varP (field nr)]
+fromFieldFun :: [Name] -> Type -> Q Exp
+fromFieldFun ns t@(ConT n)
+  | remakeName n `elem` ns   = [| I . I0 |]
+fromFieldFun ns t@(AppT f a) = [| D . fmap $(fromFieldFun ns a) |]
+fromFieldFun ns t            = [| K |]
 
-toFieldR :: Int -> Type -> Q Exp
-toFieldR nr t@(AppT f a) = [| fmap (unI0 . unI) $(varE (field nr)) |]
-toFieldR nr _            = varE (field nr)
+toField :: [Name] -> Int -> Type -> Q Exp
+toField ns nr t = [| $(toFieldFun ns t) $(varE (field nr)) |]
 
+toFieldFun :: [Name] -> Type -> Q Exp
+toFieldFun ns t@(ConT n)
+  | remakeName n `elem` ns = [| unI0 . unI |]
+toFieldFun ns t@(AppT f a) = [| fmap $(toFieldFun ns a) . unD |]
+toFieldFun ns t            = [| unK |]
+
 field :: Int -> Name
 field n = mkName $ "f" ++ show n
 
@@ -295,3 +374,6 @@
 lrE m 0 e = conE 'L `appE` e
 lrE m i e = conE 'R `appE` lrE (m-1) (i-1) e
 
+-- Should we, under certain circumstances, maintain the module name?
+remakeName :: Name -> Name
+remakeName n = mkName (nameBase n)