diff --git a/examples/AST.hs b/examples/AST.hs
--- a/examples/AST.hs
+++ b/examples/AST.hs
@@ -14,17 +14,17 @@
 
 infix 1 :=
 
-data Expr   =  Const  Int
-            |  Add    Expr  Expr
-            |  Mul    Expr  Expr
-            |  EVar   Var
-            |  Let    Decl  Expr
+data Expr a =  Const  Int
+            |  Add    (Expr a)  (Expr a)
+            |  Mul    (Expr a)  (Expr a)
+            |  EVar   (Var a)
+            |  Let    (Decl a)  (Expr a)
   deriving Show
 
-data Decl   =  Var := Expr
-            |  Seq    [Decl]
+data Decl a =  Var a := Expr a
+            |  Seq    [Decl a]
             |  None
   deriving Show
 
-type Var   =  String
+type Var a  =  a
 
diff --git a/examples/ASTExamples.hs b/examples/ASTExamples.hs
--- a/examples/ASTExamples.hs
+++ b/examples/ASTExamples.hs
@@ -10,8 +10,8 @@
 
 -- Replace ASTUse with ASTTHUse below if you want
 -- to test TH code generation.
-import ASTUse
--- import ASTTHUse
+import qualified ASTUse
+import ASTTHUse
 import AST
 
 import Generics.MultiRec.Base
@@ -30,26 +30,26 @@
 
 -- | Renaming variables using 'compos'
 
-renameVar :: Expr -> Expr
+renameVar :: Expr String -> Expr String
 renameVar = renameVar' Expr
   where
-    renameVar' :: AST a -> a -> a
+    renameVar' :: AST String a -> a -> a
     renameVar' Var x = x ++ "_"
     renameVar' p   x = compos renameVar' p x
 
 -- | Test for 'renameVar'
 
-testRename :: Expr
+testRename :: Expr String
 testRename = renameVar example
 
 -- | Result of evaluating an expression
 
 data family Value aT :: *
-data instance Value Expr  =  EV  (Env -> Int)
-data instance Value Decl  =  DV  (Env -> Env)
-data instance Value Var   =  VV  Var
+data instance Value (Expr String)  =  EV  (Env -> Int)
+data instance Value (Decl String)  =  DV  (Env -> Env)
+data instance Value (Var String)   =  VV  (Var String)
 
-type Env = [(Var, Int)]
+type Env = [(Var String, Int)]
 
 -- | Algebra for evaluating an expression
 
@@ -57,7 +57,7 @@
 
 (&.) = (F.&)
 
-evalAlgebra1 :: F.Algebra AST Value
+evalAlgebra1 :: F.Algebra (AST String) Value
 evalAlgebra1 _ =
 
       tag  (   con (\ (K x)                   -> EV (const x))
@@ -74,7 +74,7 @@
 
 -- | More convenient algebra for evaluating an expression
 
-evalAlgebra2 :: FA.Algebra AST Value
+evalAlgebra2 :: FA.Algebra (AST String) Value
 evalAlgebra2 _ =
 
      (  (\ x             -> EV (const x))
@@ -91,12 +91,12 @@
 
 -- | Evaluator
 
-eval1 :: Expr -> Env -> Int
+eval1 :: Expr String -> Env -> Int
 eval1 x = let (EV f) = F.fold evalAlgebra1 Expr x in f
 
 -- | Evaluator
 
-eval2 :: Expr -> Env -> Int
+eval2 :: Expr String -> Env -> Int
 eval2 x = let (EV f) = FA.fold evalAlgebra2 Expr x in f
 
 -- | Test for 'eval1'
@@ -111,7 +111,7 @@
 
 -- | Equality instance for 'Expr'
 
-instance Eq Expr where
+instance Eq a => Eq (Expr a) where
   (==) = eq Expr
 
 -- | Test for equality
diff --git a/examples/ASTTHUse.hs b/examples/ASTTHUse.hs
--- a/examples/ASTTHUse.hs
+++ b/examples/ASTTHUse.hs
@@ -18,10 +18,10 @@
 
 -- ** Index type
 
-data AST :: * -> * where
-  Expr  ::  AST Expr
-  Decl  ::  AST Decl
-  Var   ::  AST Var
+data AST :: * -> * -> * where
+  Expr  ::  AST a (Expr a)
+  Decl  ::  AST a (Decl a)
+  Var   ::  AST a (Var  a)
 
 $(deriveAll ''AST)
 
diff --git a/examples/ASTUse.hs b/examples/ASTUse.hs
--- a/examples/ASTUse.hs
+++ b/examples/ASTUse.hs
@@ -16,10 +16,10 @@
 
 -- ** Index type
 
-data AST :: * -> * where
-  Expr  ::  AST Expr
-  Decl  ::  AST Decl
-  Var   ::  AST Var
+data AST :: * -> * -> * where
+  Expr  ::  AST a (Expr a)
+  Decl  ::  AST a (Decl a)
+  Var   ::  AST a (Var  a)
 
 -- ** Constructors
 
@@ -51,29 +51,29 @@
 -- the overall structure slightly simpler, but makes the nesting
 -- of 'L' and 'R' constructors larger in turn.
 
-type instance PF AST  =    
+type instance PF (AST a)  =
       (     C Const   (K Int)
-       :+:  C Add     (I Expr :*: I Expr)
-       :+:  C Mul     (I Expr :*: I Expr)
-       :+:  C EVar    (I Var)
-       :+:  C Let     (I Decl :*: I Expr)
-      ) :>: Expr
-  :+: (     C Assign  (I Var  :*: I Expr)
-       :+:  C Seq     ([] :.: I Decl)
+       :+:  C Add     (I (Expr a) :*: I (Expr a))
+       :+:  C Mul     (I (Expr a) :*: I (Expr a))
+       :+:  C EVar    (I (Var a))
+       :+:  C Let     (I (Decl a) :*: I (Expr a))
+      ) :>: Expr a
+  :+: (     C Assign  (I (Var a)  :*: I (Expr a))
+       :+:  C Seq     ([] :.: I (Decl a))
        :+:  C None    U
-      ) :>: Decl
-  :+: (               (K String)
-      ) :>: Var
+      ) :>: Decl a
+  :+: (               (K a)
+      ) :>: Var a
 
 -- ** 'El' instances
 
-instance El AST Expr where proof = Expr
-instance El AST Decl where proof = Decl
-instance El AST Var  where proof = Var
+instance El (AST a) (Expr a) where proof = Expr
+instance El (AST a) (Decl a) where proof = Decl
+instance El (AST a) (Var a)  where proof = Var
 
 -- ** 'Fam' instance
 
-instance Fam AST where
+instance Fam (AST a) where
 
   from Expr (Const i)  =  L (Tag (L          (C (K i))))
   from Expr (Add e f)  =  L (Tag (R (L       (C (I (I0 e) :*: I (I0 f))))))
@@ -101,7 +101,7 @@
 
 -- ** EqS instance
 
-instance EqS AST where
+instance EqS (AST a) where
   eqS Expr Expr = Just Refl
   eqS Decl Decl = Just Refl
   eqS Var  Var  = Just Refl
diff --git a/examples/All.hs b/examples/All.hs
new file mode 100644
--- /dev/null
+++ b/examples/All.hs
@@ -0,0 +1,5 @@
+module All where
+
+import GRose
+import SingleExamples
+import ASTExamples
diff --git a/examples/SingleExamples.hs b/examples/SingleExamples.hs
--- a/examples/SingleExamples.hs
+++ b/examples/SingleExamples.hs
@@ -7,8 +7,8 @@
 
 -- Replace SingleUse with SingleTHUse below if you want
 -- to test TH code generation.
-import SingleUse
--- import SingleTHUse
+import qualified SingleUse
+import SingleTHUse
 import Single
 
 -- | evalLogic takes a function that gives a logic values to variables,
diff --git a/multirec.cabal b/multirec.cabal
--- a/multirec.cabal
+++ b/multirec.cabal
@@ -1,5 +1,5 @@
 name:                 multirec
-version:              0.7.1
+version:              0.7.2
 license:              BSD3
 license-file:         LICENSE
 author:               Alexey Rodriguez,
@@ -39,7 +39,8 @@
 build-type:           Simple
 cabal-version:        >= 1.6
 tested-with:          GHC == 7.0.4
-extra-source-files:   examples/AST.hs
+extra-source-files:   examples/All.hs
+                      examples/AST.hs
                       examples/ASTUse.hs
                       examples/ASTTHUse.hs
                       examples/ASTExamples.hs
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
@@ -76,7 +76,7 @@
 
 -- | Is used to indicate the type that a
 -- particular constructor injects to.
-data f :>: ix :: (* -> *) -> * -> * where
+data (f :>: ix) (r :: * -> *) ix' where
   Tag :: f r ix -> (f :>: ix) r ix
 
 -- | Destructor for '(:>:)'.
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
@@ -1,6 +1,7 @@
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE GADTs           #-}
 {-# LANGUAGE KindSignatures  #-}
+{-# LANGUAGE PatternGuards   #-}
 
 -----------------------------------------------------------------------------
 -- |
@@ -41,12 +42,15 @@
   do
     info <- reify n
     -- runIO (print info)
-    let ns = map remakeName (extractConstructorNames info)
+    let ps  = init (extractParameters info)
+    let nps = map (\ (n, ps) -> (remakeName n, ps)) (extractConstructorNames ps info)
+    let ns  = map fst nps
+    -- runIO (print nps)
     cs  <- deriveConstructors ns
-    pf  <- derivePFInstance n ns
-    el  <- deriveEl n ns
-    fam <- deriveFam n ns
-    eq  <- deriveEqS n ns
+    pf  <- derivePFInstance n ps nps
+    el  <- deriveEl n ps nps
+    fam <- deriveFam n ps ns
+    eq  <- deriveEqS n ps ns
     return $ cs ++ pf ++ el ++ fam ++ eq
 
 -- | Given a list of datatype names, derive datatypes and
@@ -69,9 +73,9 @@
 deriveFamily n ns pfn =
   do
     pf  <- derivePF pfn ns
-    el  <- deriveEl n ns
-    fam <- deriveFam n ns
-    eq  <- deriveEqS n (map remakeName ns)
+    el  <- deriveEl n [] (zip ns (repeat []))
+    fam <- deriveFam n [] ns
+    eq  <- deriveEqS n [] (map remakeName ns)
     return $ pf ++ el ++ fam ++ eq
 
 -- | Compatibility. Use 'deriveAll' instead.
@@ -84,42 +88,42 @@
 derivePF :: String -> [Name] -> Q [Dec]
 derivePF pfn ns =
     return <$>
-    tySynD (mkName pfn) [] (foldr1 sum (map (pfType ns) ns))
+    tySynD (mkName pfn) [] (foldr1 sum (map (pfType ns []) (zip ns (repeat []))))
   where
     sum :: Q Type -> Q Type -> Q Type
     sum a b = conT ''(:+:) `appT` a `appT` b
 
-derivePFInstance :: Name -> [Name] -> Q [Dec]
-derivePFInstance n ns =
+derivePFInstance :: Name -> [Name] -> [(Name, [Name])] -> Q [Dec]
+derivePFInstance n ps nps =
     return <$>
-    tySynInstD ''PF [conT n] (foldr1 sum (map (pfType ns) ns))
+    tySynInstD ''PF [foldl appT (conT n) (map varT ps)] (foldr1 sum (map (pfType (map fst nps) ps) nps))
   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
+deriveEl :: Name -> [Name] -> [(Name, [Name])] -> Q [Dec]
+deriveEl s ps ns =
+  mapM (elInstance s ps) ns
 
 -- | Derive only the 'Fam' instance. Not needed if 'deriveAll'
 -- is used.
-deriveFam :: Name -> [Name] -> Q [Dec]
-deriveFam s ns =
+deriveFam :: Name -> [Name] -> [Name] -> Q [Dec]
+deriveFam s ps ns =
   do
     fcs <- liftM concat $ zipWithM (mkFrom ns (length ns)) [0..] ns
     tcs <- liftM concat $ zipWithM (mkTo   ns (length ns)) [0..] ns
     return <$>
-      instanceD (cxt []) (conT ''Fam `appT` conT s)
+      instanceD (cxt []) (conT ''Fam `appT` (foldl appT (conT s) (map varT ps)))
         [funD 'from fcs, funD 'to tcs]
 
 -- | Derive only the 'EqS' instance. Not needed if 'deriveAll'
 -- is used.
-deriveEqS :: Name -> [Name] -> Q [Dec]
-deriveEqS s ns =
+deriveEqS :: Name -> [Name] -> [Name] -> Q [Dec]
+deriveEqS s ps ns =
     return <$>
-    instanceD (cxt []) (conT ''EqS `appT` conT s)
+    instanceD (cxt []) (conT ''EqS `appT` (foldl appT (conT s) (map varT ps)))
       [funD 'eqS (trues ++ falses)]
   where
     trueClause n = clause [conP n [], conP n []] (normalB (conE 'Just `appE` conE 'Refl)) []
@@ -130,17 +134,39 @@
 -- | 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
+extractConstructorNames :: [Name] -> Info -> [(Name, [Name])]
+extractConstructorNames ps (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 _                           = []
+    extractFrom :: Con -> [(Name, [Name])]
+    extractFrom (ForallC _ eqs c) = map (\ (n, _) -> (n, concatMap extractEq eqs)) (extractFrom c)
+    extractFrom (InfixC _ n _)    = [(n, [])]
+    extractFrom (RecC n _)        = [(n, [])]
+    extractFrom (NormalC n [])    = [(n, [])]
+    extractFrom _                 = []
 
+    extractEq :: Pred -> [Name]
+    extractEq (EqualP t1 t2) = filter (\ p -> p `elem` ps) (extractArgs t1 ++ extractArgs t2)
+    extractEq _              = []
+
+    extractArgs :: Type -> [Name]
+    extractArgs (AppT x (VarT n)) = extractArgs x ++ [n]
+    extractArgs (VarT n)          = [n]
+    extractArgs _                 = []
+
+extractConstructorNames _  _                           = []
+
+
+-- | Process the reified info of the index GADT, and extract
+-- its type parameters.
+extractParameters :: Info -> [Name]
+extractParameters (TyConI (DataD _ _ ns _ _)) = concatMap extractFromBndr ns
+extractParameters (TyConI (TySynD _ ns _))    = concatMap extractFromBndr ns
+extractParameters _                           = []
+
+extractFromBndr :: TyVarBndr -> [Name]
+extractFromBndr (PlainTV n)    = [n]
+extractFromBndr (KindedTV n _) = [n]
+
 -- | Turn a record-constructor into a normal constructor by just
 -- removing all the field names.
 stripRecordNames :: Con -> Con
@@ -213,20 +239,21 @@
 -- | 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 =
+pfType :: [Name] -> [Name] -> (Name, [Name]) -> Q Type
+pfType ns ps (n, rs) =
     do
-      -- runIO $ putStrLn $ "processing " ++ show n
       i <- reify n
+      let qs = extractParameters i
+      -- runIO $ putStrLn $ "processing " ++ show n
       let b = case i of
                 -- datatypes are nested binary sums of their constructors
                 TyConI (DataD _ _ _ cs _) ->
-                  foldr1 sum (map (pfCon ns) cs)
+                  foldr1 sum (map (pfCon ns (zip qs rs)) cs)
                 -- type synonyms are always treated as constants
                 TyConI (TySynD t _ _) ->
-                  conT ''K `appT` conT t
+                  conT ''K `appT` foldl appT (conT t) (map varT rs)
                 _ -> error "unknown construct"
-      appT (appT (conT ''(:>:)) b) (conT $ remakeName n)
+      appT (appT (conT ''(:>:)) b) (foldl appT (conT $ remakeName n) (map varT rs))
   where
     sum :: Q Type -> Q Type -> Q Type
     sum a b = conT ''(:+:) `appT` a `appT` b
@@ -234,20 +261,20 @@
 -- | 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 []) =
+pfCon :: [Name] -> [(Name, Name)] -> Con -> Q Type
+pfCon ns ps r@(RecC _ _) =
+    pfCon ns ps (stripRecordNames r)
+pfCon ns ps (InfixC t1 n t2) =
+    pfCon ns ps (NormalC n [t1,t2])
+pfCon ns ps (ForallC _ _ c) =
+    pfCon ns ps c
+pfCon ns ps (NormalC n []) =
     -- a constructor without arguments is represented using 'U'
     appT (appT (conT ''C) (conT $ remakeName n)) (conT ''U)
-pfCon ns (NormalC n fs) =
+pfCon ns ps (NormalC n fs) =
     -- a constructor with arguments is a nested binary product
     appT (appT (conT ''C) (conT $ remakeName n))
-         (foldr1 prod (map (pfField ns . snd) fs))
+         (foldr1 prod (map (pfField ns ps . snd) fs))
   where
     prod :: Q Type -> Q Type -> Q Type
     prod a b = conT ''(:*:) `appT` a `appT` b
@@ -260,17 +287,32 @@
 -- 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)
-  | 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
+pfField :: [Name] -> [(Name, Name)] -> Type -> Q Type
+pfField ns ps t@(ConT n)
+  | remakeName n `elem` ns             = conT ''I `appT` return t
+pfField ns ps t
+  | ConT n : a <- unApp t, remakeName n `elem` ns
+                                       = conT ''I `appT` (foldl appT (conT n) (map rename a))
+  where
+    rename (VarT n)
+      | Just p <- lookup n ps          = varT p
+    rename t                           = return t
+pfField ns ps t@(AppT f a)             = conT ''(:.:) `appT` return f `appT` pfField ns ps a
+pfField ns ps t@(VarT n)
+  | Just p <- lookup n ps              = {- runIO (print (ps, n)) >> -} conT ''K `appT` varT p
+pfField ns ps t                        = conT ''K `appT` return t
 
-elInstance :: Name -> Name -> Q Dec
-elInstance s n =
-  instanceD (cxt []) (conT ''El `appT` conT s `appT` conT n)
-    [mkProof n]
+unApp :: Type -> [Type]
+unApp (AppT f a) = unApp f ++ [a]
+unApp t          = [t]
 
+elInstance :: Name -> [Name] -> (Name, [Name]) -> Q Dec
+elInstance s ps (n, qs) =
+  do
+    -- runIO (print (ps, qs))
+    instanceD (cxt []) (conT ''El `appT` (foldl appT (conT s) (map varT ps)) `appT` (foldl appT (conT n) (map varT qs)))
+      [mkProof n]
+
 mkFrom :: [Name] -> Int -> Int -> Name -> Q [Q Clause]
 mkFrom ns m i n =
     do
@@ -349,6 +391,9 @@
 fromFieldFun :: [Name] -> Type -> Q Exp
 fromFieldFun ns t@(ConT n)
   | remakeName n `elem` ns   = [| I . I0 |]
+fromFieldFun ns t
+  | ConT n : a <- unApp t, remakeName n `elem` ns
+                             = [| I . I0 |]
 fromFieldFun ns t@(AppT f a) = [| D . fmap $(fromFieldFun ns a) |]
 fromFieldFun ns t            = [| K |]
 
@@ -358,6 +403,9 @@
 toFieldFun :: [Name] -> Type -> Q Exp
 toFieldFun ns t@(ConT n)
   | remakeName n `elem` ns = [| unI0 . unI |]
+toFieldFun ns t
+  | ConT n : a <- unApp t, remakeName n `elem` ns
+                           = [| unI0 . unI |]
 toFieldFun ns t@(AppT f a) = [| fmap $(toFieldFun ns a) . unD |]
 toFieldFun ns t            = [| unK |]