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  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
@@ -1,5 +1,7 @@
 {-# LANGUAGE FlexibleContexts     #-}
+{-# LANGUAGE LiberalTypeSynonyms  #-}
 {-# LANGUAGE TypeFamilies         #-}
+{-# LANGUAGE GADTs                #-}
 
 module ASTExamples where
 
@@ -9,9 +11,9 @@
 
 -- Replace ASTUse with ASTTHUse below if you want
 -- to test TH code generation.
+import qualified ASTUse
+import ASTTHUse
 import AST
-import ASTUse
--- import ASTTHUse
 
 import Generics.MultiRec.Base
 import Generics.MultiRec.Compos
@@ -20,34 +22,35 @@
 import Generics.MultiRec.FoldAlg as FA
 import Generics.MultiRec.Eq
 import Generics.MultiRec.Show as GS
+import Generics.MultiRec.Read as GR
 
 -- | Example expression
 
-example = Let (Seq ("x" := Mul (Const 6) (Const 9)) None)
-              (Add (EVar "x") (EVar "y"))
+example = Let (Seq ["x" := Mul (Const 6) (Const 9), "z" := Const 1])
+              (Mul (EVar "z") (Add (EVar "x") (EVar "y")))
 
 -- | 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
 
@@ -55,9 +58,9 @@
 
 (&.) = (F.&)
 
-evalAlgebra1 :: F.Algebra AST Value
-evalAlgebra1 _ =  
- 
+evalAlgebra1 :: F.Algebra (AST String) Value
+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))
@@ -65,14 +68,14 @@
            &.  con (\ (I (DV e) :*: I (EV x)) -> EV (\ env -> x (e env)))
            )
   &.  tag  (   con (\ (I (VV x) :*: I (EV v)) -> DV (\ env -> (x, v env) : env ))
-           &.  con (\ (I (DV f) :*: I (DV g)) -> DV (g . f))
+           &.  con (\ (D fs)                  -> DV (foldl (\ f (I (DV g)) -> f . g) id fs))
            &.  con (\ U                       -> DV id)
            )
   &.  tag          (\ (K x)                   -> VV x)
 
 -- | More convenient algebra for evaluating an expression
 
-evalAlgebra2 :: FA.Algebra AST Value
+evalAlgebra2 :: FA.Algebra (AST String) Value
 evalAlgebra2 _ =
 
      (  (\ x             -> EV (const x))
@@ -82,34 +85,34 @@
      &  (\ (DV e) (EV x) -> EV (\ env -> x (e env)))
      )
   &  (  (\ (VV x) (EV v) -> DV (\ env -> (x, v env) : env ))
-     &  (\ (DV f) (DV g) -> DV (g . f))
+     &  (\ fs            -> DV (foldl (\ f (DV g) -> f . g) id fs))
      &  (                   DV id)
      )
   &     (\ x             -> VV x)
 
 -- | 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'
 
 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'
 
-instance Eq Expr where
+instance Eq a => Eq (Expr a) where
   (==) = eq Expr
 
 -- | Test for equality
@@ -121,3 +124,8 @@
 
 testShow :: IO ()
 testShow = putStrLn $ GS.show Expr example
+
+-- | Test for generic show, read and equality
+
+testReadShowEq :: Bool
+testReadShowEq = GR.read Expr (GS.show Expr example) == example
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
 
@@ -17,17 +18,10 @@
 
 -- ** Index type
 
-data AST :: * -> * where
-  Expr  ::  AST Expr
-  Decl  ::  AST Decl
-  Var   ::  AST Var
-
--- ** Constructors
-
-$(deriveConstructors [''Expr, ''Decl, ''Var])
-
--- ** Functor encoding and 'Ix' instances
+data AST :: * -> * -> * where
+  Expr  ::  AST a (Expr a)
+  Decl  ::  AST a (Decl a)
+  Var   ::  AST a (Var  a)
 
-$(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,20 +5,21 @@
 {-# 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
 
-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
 
@@ -50,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 :*: 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))))))
@@ -81,7 +82,7 @@
   from Expr (Let d e)  =  L (Tag (R (R (R (R (C (I (I0 d) :*: I (I0 e))))))))
 
   from Decl (x := e)   =  R (L (Tag (L    (C (I (I0 x) :*: I (I0 e))))))
-  from Decl (Seq c d)  =  R (L (Tag (R (L (C (I (I0 c) :*: I (I0 d)))))))
+  from Decl (Seq ds)   =  R (L (Tag (R (L (C (D (map (I . I0) ds)))))))
   from Decl (None)     =  R (L (Tag (R (R (C U)))))
 
   from Var  x          =  R (R (Tag (K x)))
@@ -93,8 +94,15 @@
   to Expr (L (Tag (R (R (R (R (C (I (I0 d) :*: I (I0 e)))))))))  =  Let d e
 
   to Decl (R (L (Tag (L    (C (I (I0 x) :*: I (I0 e)))))))       =  x := e
-  to Decl (R (L (Tag (R (L (C (I (I0 c) :*: I (I0 d))))))))      =  Seq c d
+  to Decl (R (L (Tag (R (L (C (D ds)))))))                       =  Seq (map (unI0 . unI) ds)
   to Decl (R (L (Tag (R (R (C U))))))                            =  None
 
   to Var  (R (R (Tag (K x))))                                    =  x
 
+-- ** EqS instance
+
+instance EqS (AST a) where
+  eqS Expr Expr = Just Refl
+  eqS Decl Decl = Just Refl
+  eqS Var  Var  = Just Refl
+  eqS _    _    = Nothing
diff --git a/examples/All.hs b/examples/All.hs
new file mode 100644
--- /dev/null
+++ b/examples/All.hs
@@ -0,0 +1,10 @@
+module Main where
+
+import GRose
+import VarTypes
+import J
+import SingleExamples
+import ASTExamples
+
+main :: IO ()
+main = return ()
diff --git a/examples/GRose.hs b/examples/GRose.hs
new file mode 100644
--- /dev/null
+++ b/examples/GRose.hs
@@ -0,0 +1,47 @@
+{-# LANGUAGE EmptyDataDecls        #-}
+{-# LANGUAGE TemplateHaskell       #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+module GRose where
+
+-- Test case for Issue #1.
+
+import Generics.MultiRec.Base
+import Generics.MultiRec.TH
+
+data GRose a = Leaf a | Node [GRose a]
+
+data GRoseF :: * -> * -> * where
+  GRose :: GRoseF a (GRose a)
+
+$(deriveAll ''GRoseF)
+
+-- Desired output:
+--
+-- data Leaf
+-- data Node
+--
+-- instance Constructor Leaf where
+--   conName _ = "Leaf"
+-- instance Constructor Node where
+--   conName _ = "Node"
+--
+-- type instance PF (GRoseF a) =
+--   (:>:) ((:+:) (C Leaf (K a)) (C Node ((:.:) [] (I (GRose a))))) (GRose a)
+--
+-- instance El (GRoseF a) (GRose a) where
+--   proof = GRose
+--
+-- instance Fam (GRoseF a) where
+--
+--   from GRose (Leaf f0) = Tag (L (C (K f0)))
+--   from GRose (Node f0) = Tag (R (C ((D . (fmap (I . I0))) f0)))
+--
+--   to GRose (Tag (L (C f0))) = Leaf (unK f0)
+--   to GRose (Tag (R (C f0))) = Node (((fmap (unI0 . unI)) . unD) f0)
+--
+-- instance EqS (GRoseF a) where
+--   eqS GRose GRose = Just Refl
diff --git a/examples/J.hs b/examples/J.hs
new file mode 100644
--- /dev/null
+++ b/examples/J.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE TypeSynonymInstances  #-}
+{-# LANGUAGE EmptyDataDecls        #-}
+{-# LANGUAGE TemplateHaskell       #-}
+{-# LANGUAGE FlexibleInstances     #-}
+
+module J where
+
+import Generics.MultiRec.Base
+import Generics.MultiRec.TH
+
+-- Issue #4 test case
+
+data J a = JJ (a, J a)
+
+data AST :: * -> * -> * where
+  J :: AST a (J a)
+
+$(deriveAll ''AST)
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/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/examples/VarTypes.hs b/examples/VarTypes.hs
new file mode 100644
--- /dev/null
+++ b/examples/VarTypes.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE EmptyDataDecls        #-}
+{-# LANGUAGE TemplateHaskell       #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+module VarTypes where
+
+import Generics.MultiRec.TH
+
+data Type1 a b = CA a | CB b
+data Type2 c   = CC c | CD
+data Type3     = CE
+
+data TypesF :: * -> * -> * -> * -> * where
+  Type1 :: TypesF a b c (Type1 a b)
+  Type2 :: TypesF a b c (Type2 c)
+  Type3 :: TypesF a b c  Type3
+
+$(deriveAll ''TypesF)
+
diff --git a/multirec.cabal b/multirec.cabal
--- a/multirec.cabal
+++ b/multirec.cabal
@@ -1,15 +1,16 @@
-name:			multirec
-version:		0.3
-license:		BSD3
-license-file:		LICENSE
-author:			Alexey Rodriguez,
-                        Stefan Holdermans,
-                        Andres Löh,
-                        Johan Jeuring
-maintainer:		generics@haskell.org
-category:		Generics
-synopsis:		Generic programming for families of recursive datatypes
-homepage:		http://www.cs.uu.nl/wiki/GenericProgramming/Multirec
+name:                 multirec
+version:              0.7.9
+license:              BSD3
+license-file:         LICENSE
+author:               Alexey Rodriguez,
+                      Stefan Holdermans,
+                      Andres Löh,
+                      Johan Jeuring
+maintainer:           generics@haskell.org
+category:             Generics
+synopsis:             Generic programming for families of recursive datatypes
+homepage:             http://www.cs.uu.nl/wiki/GenericProgramming/Multirec
+bug-reports:          https://github.com/kosmikus/multirec/issues
 description:
   Many generic programs require information about the recursive positions
   of a datatype. Examples include the generic fold, generic rewriting or
@@ -32,44 +33,64 @@
   .
   *  Alexey Rodriguez, Stefan Holdermans, Andres Löh, Johan Jeuring.
      /Generic programming with fixed points for mutually recursive datatypes/.
-     Technical Report, Universiteit Utrecht
-     (<http://www.cs.uu.nl/research/techreps/repo/CS-2008/2008-019.pdf>).
- 
-stability:		experimental
-build-type:		Simple
-cabal-version:		>= 1.2.1
-tested-with:		GHC == 6.8.3, GHC == 6.10.3
-hs-source-dirs:		src
-exposed-modules:	Generics.MultiRec
+     ICFP 2009.
 
-			-- Base
-                        Generics.MultiRec.Base
-			Generics.MultiRec.Constructor
-                        Generics.MultiRec.TH
+stability:            experimental
+build-type:           Simple
+cabal-version:        >= 1.10
+tested-with:          GHC == 7.6.3, GHC == 7.8.4, GHC == 7.10.3, GHC == 8.0.2, GHC == 8.2.2
+extra-source-files:   CREDITS
 
-			-- Generic functions
-			Generics.MultiRec.ConNames
-			Generics.MultiRec.HFunctor
-			Generics.MultiRec.HFix
-			Generics.MultiRec.Fold
-			Generics.MultiRec.FoldK
-			Generics.MultiRec.FoldAlg
-			Generics.MultiRec.FoldAlgK
-			Generics.MultiRec.Compos
-			Generics.MultiRec.Eq
-			Generics.MultiRec.Show
+source-repository head
+  type:               git
+  location:           https://github.com/kosmikus/multirec
 
-			-- Extra
-			Generics.MultiRec.TEq
+library
+  hs-source-dirs:     src
+  -- ghc-options:        -Wall -fno-warn-name-shadowing -fno-warn-unused-binds -fno-warn-unused-matches
+  exposed-modules:    Generics.MultiRec
 
-extra-source-files:	examples/AST.hs
-                        examples/ASTUse.hs
-                        examples/ASTTHUse.hs
-			examples/ASTExamples.hs
-			examples/Single.hs
-			examples/SingleUse.hs
-			examples/SingleTHUse.hs
-			examples/SingleExamples.hs
-			CREDITS
-build-depends:		base >= 3.0 && < 5,
-                        template-haskell >= 2.2 && < 2.4
+                      -- Base
+                      Generics.MultiRec.Base
+                      Generics.MultiRec.Constructor
+                      Generics.MultiRec.TH
+
+                      -- Generic functions
+                      Generics.MultiRec.ConNames
+                      Generics.MultiRec.HFunctor
+                      Generics.MultiRec.HFix
+                      Generics.MultiRec.Fold
+                      Generics.MultiRec.FoldK
+                      Generics.MultiRec.FoldAlg
+                      Generics.MultiRec.FoldAlgK
+                      Generics.MultiRec.Compos
+                      Generics.MultiRec.Eq
+                      Generics.MultiRec.Read
+                      Generics.MultiRec.Show
+
+                      -- Extra
+                      Generics.MultiRec.TEq
+
+  default-language:   Haskell2010
+
+  build-depends:      base >= 3.0 && < 5,
+                      template-haskell >= 2.4 && < 2.15
+
+test-suite examples
+  type:               exitcode-stdio-1.0
+  main-is:            All.hs
+  other-modules:      AST
+                      ASTExamples
+                      ASTTHUse
+                      ASTUse
+                      GRose
+                      J
+                      Single
+                      SingleExamples
+                      SingleTHUse
+                      SingleUse
+                      VarTypes
+  hs-source-dirs:     examples
+  default-language:   Haskell2010
+  build-depends:      base >= 3.0 && < 5,
+                      multirec
diff --git a/src/Generics/MultiRec.hs b/src/Generics/MultiRec.hs
--- a/src/Generics/MultiRec.hs
+++ b/src/Generics/MultiRec.hs
@@ -11,7 +11,7 @@
 -- multirec --
 -- generic programming for families of recursive datatypes
 -- 
--- This top-level module re-exports all other modules of the library.
+-- This top-level module re-exports most modules of the library.
 --
 -----------------------------------------------------------------------------
 
@@ -24,7 +24,9 @@
     module Generics.MultiRec.HFunctor,
     module Generics.MultiRec.Fold,
     module Generics.MultiRec.Compos,
-    module Generics.MultiRec.Eq
+    module Generics.MultiRec.Eq,
+    module Generics.MultiRec.HFix,
+    module Generics.MultiRec.Show,
   )
   where
 
@@ -33,5 +35,7 @@
 import Generics.MultiRec.Fold
 import Generics.MultiRec.Compos
 import Generics.MultiRec.Eq
+import Generics.MultiRec.HFix
+import Generics.MultiRec.Show
 
 
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
@@ -9,7 +9,7 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Generics.MultiRec.Base
--- Copyright   :  (c) 2008--2009 Universiteit Utrecht
+-- Copyright   :  (c) 2008--2010 Universiteit Utrecht
 -- License     :  BSD3
 --
 -- Maintainer  :  generics@haskell.org
@@ -31,6 +31,7 @@
    I(..),
    K(..), U(..), (:+:)(..), (:*:)(..),
    (:>:)(..), unTag,
+   (:.:)(..),
    C(..), unC,
 
    -- ** Constructor information
@@ -75,13 +76,17 @@
 
 -- | 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 '(:>:)'.
 unTag :: (f :>: ix) r ix -> f r ix
 unTag (Tag x) = x
 
+-- | Represents composition with functors
+-- of kind * -> *.
+data (f :.: g) (r :: * -> *) ix = D {unD :: f (g r ix)}
+
 -- | Represents constructors.
 data C c f     (r :: * -> *) ix where
   C :: f r ix -> C c f r ix
@@ -111,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/Compos.hs b/src/Generics/MultiRec/Compos.hs
--- a/src/Generics/MultiRec/Compos.hs
+++ b/src/Generics/MultiRec/Compos.hs
@@ -4,7 +4,7 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Generics.MultiRec.Compos
--- Copyright   :  (c) 2008--2009 Universiteit Utrecht
+-- Copyright   :  (c) 2008--2010 Universiteit Utrecht
 -- License     :  BSD3
 --
 -- Maintainer  :  generics@haskell.org
@@ -32,14 +32,14 @@
 -- | Normal version.
 compos :: (Fam phi, HFunctor phi (PF phi)) =>
           (forall ix. phi ix -> ix -> ix) -> phi ix -> ix -> ix
-compos f p = to p . hmap (\ p -> I0 . f p . unI0) . from p
+compos f p = to p . hmap (\ p -> I0 . f p . unI0) p . from p
 
 -- | Monadic version of 'compos'.
 composM :: (Fam phi, HFunctor phi (PF phi), Monad m) =>
            (forall ix. phi ix -> ix -> m ix) -> phi ix -> ix -> m ix
-composM f p = liftM (to p) . hmapM (\ p -> liftM I0 . f p . unI0) . from p
+composM f p = liftM (to p) . hmapM (\ p -> liftM I0 . f p . unI0) p . from p
 
 -- | Applicative version of 'compos'.
 composA :: (Fam phi, HFunctor phi (PF phi), Applicative a) =>
            (forall ix. phi ix -> ix -> a ix) -> phi ix -> ix -> a ix
-composA f p = liftA (to p) . hmapA (\ p -> liftA I0 . f p . unI0) . from p
+composA f p = liftA (to p) . hmapA (\ p -> liftA I0 . f p . unI0) p . from p
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,12 +3,11 @@
 {-# LANGUAGE TypeOperators    #-}
 {-# LANGUAGE KindSignatures   #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE PatternSignatures #-}
 
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Generics.MultiRec.ConNames
--- Copyright   :  (c) 2008--2009 Universiteit Utrecht
+-- Copyright   :  (c) 2008--2010 Universiteit Utrecht
 -- License     :  BSD3
 --
 -- Maintainer  :  generics@haskell.org
@@ -23,7 +22,6 @@
 module Generics.MultiRec.ConNames where
 
 import Generics.MultiRec.Base
-import Generics.MultiRec.Constructor
 
 class ConNames (f :: (* -> *) -> * -> *) where
   hconNames :: f r ix -> [String]
@@ -42,6 +40,9 @@
   hconNames _ = []
 
 instance ConNames (f :*: g) where
+  hconNames _ = []
+
+instance ConNames (f :.: g) where
   hconNames _ = []
 
 instance ConNames (I a) where
diff --git a/src/Generics/MultiRec/Constructor.hs b/src/Generics/MultiRec/Constructor.hs
--- a/src/Generics/MultiRec/Constructor.hs
+++ b/src/Generics/MultiRec/Constructor.hs
@@ -3,7 +3,7 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Generics.MultiRec.Constructor
--- Copyright   :  (c) 2008--2009 Universiteit Utrecht
+-- Copyright   :  (c) 2008--2010 Universiteit Utrecht
 -- License     :  BSD3
 --
 -- Maintainer  :  generics@haskell.org
diff --git a/src/Generics/MultiRec/Eq.hs b/src/Generics/MultiRec/Eq.hs
--- a/src/Generics/MultiRec/Eq.hs
+++ b/src/Generics/MultiRec/Eq.hs
@@ -3,11 +3,12 @@
 {-# LANGUAGE TypeOperators         #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE GADTs                 #-}
 
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Generics.MultiRec.Eq
--- Copyright   :  (c) 2008--2009 Universiteit Utrecht
+-- Copyright   :  (c) 2008--2010 Universiteit Utrecht
 -- License     :  BSD3
 --
 -- Maintainer  :  generics@haskell.org
@@ -28,6 +29,20 @@
   heq :: (forall ix. phi ix -> r ix -> r ix -> Bool) ->
          phi ix -> f r ix -> f r ix -> Bool
 
+class Eq1 f where
+  eq1 :: (a -> a -> Bool) -> f a -> f a -> Bool
+
+-- TODO: Think about more generic instances
+instance Eq1 [] where
+  eq1 eq []       []       = True
+  eq1 eq (x1:xs1) (x2:xs2) = eq x1 x2 && eq1 eq xs1 xs2
+  eq1 eq _        _        = False
+
+instance Eq1 Maybe where
+  eq1 eq Nothing   Nothing   = True
+  eq1 eq (Just x1) (Just x2) = eq x1 x2
+  eq1 eq _         _         = False
+
 instance El phi xi => HEq phi (I xi) where
   heq eq _ (I x1) (I x2) = eq proof x1 x2
 
@@ -46,6 +61,9 @@
 
 instance (HEq phi f, HEq phi g) => HEq phi (f :*: g) where
   heq eq p (x1 :*: y1) (x2 :*: y2) = heq eq p x1 x2 && heq eq p y1 y2
+
+instance (Eq1 f, HEq phi g) => HEq phi (f :.: g) where
+  heq eq p (D x1) (D x2) = eq1 (heq eq p) x1 x2
 
 -- The following instance does not compile with ghc-6.8.2
 instance HEq phi f => HEq phi (f :>: ix) where
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
@@ -9,7 +9,7 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Generics.MultiRec.Fold
--- Copyright   :  (c) 2008--2009 Universiteit Utrecht
+-- Copyright   :  (c) 2008--2010 Universiteit Utrecht
 -- License     :  BSD3
 --
 -- Maintainer  :  generics@haskell.org
@@ -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
 
@@ -47,11 +46,11 @@
 
 fold :: (Fam phi, HFunctor phi (PF phi)) =>
         Algebra phi r -> phi ix -> ix -> r ix
-fold f p = f p . hmap (\ p (I0 x) -> fold f p x) . from p
+fold f p = f p . hmap (\ p (I0 x) -> fold f p x) p . from p
 
 foldM :: (Fam phi, HFunctor phi (PF phi), Monad m) =>
          AlgebraF phi m r -> phi ix -> ix -> m (r ix)
-foldM f p x = hmapM (\ p (I0 x) -> foldM f p x) (from p x) >>= f p
+foldM f p x = hmapM (\ p (I0 x) -> foldM f p x) p (from p x) >>= f p
 
 type CoAlgebra'  phi f   r = forall ix. phi ix -> r ix -> f r ix
 type CoAlgebra   phi     r = CoAlgebra' phi (PF phi) r
@@ -60,11 +59,11 @@
 
 unfold :: (Fam phi, HFunctor phi (PF phi)) =>
           CoAlgebra phi r -> phi ix -> r ix -> ix
-unfold f p = to p . hmap (\ p x -> I0 (unfold f p x)) . f p
+unfold f p = to p . hmap (\ p x -> I0 (unfold f p x)) p . f p
 
 unfoldM :: (Fam phi, HFunctor phi (PF phi), Monad m) =>
            CoAlgebraF phi m r -> phi ix -> r ix -> m ix
-unfoldM f p x = f p x >>= liftM (to p) . hmapM (\ p x -> liftM I0 (unfoldM f p x))
+unfoldM f p x = f p x >>= liftM (to p) . hmapM (\ p x -> liftM I0 (unfoldM f p x)) p
 
 type ParaAlgebra'  phi f   r = forall ix. phi ix -> f r ix -> ix -> r ix
 type ParaAlgebra   phi     r = ParaAlgebra' phi (PF phi) r
@@ -73,11 +72,11 @@
 
 para :: (Fam phi, HFunctor phi (PF phi)) => 
         ParaAlgebra phi r -> phi ix -> ix -> r ix
-para f p x = f p (hmap (\ p (I0 x) -> para f p x) (from p x)) x
+para f p x = f p (hmap (\ p (I0 x) -> para f p x) p (from p x)) x
 
 paraM :: (Fam phi, HFunctor phi (PF phi), Monad m) => 
          ParaAlgebraF phi m r -> phi ix -> ix -> m (r ix)
-paraM f p x = hmapM (\ p (I0 x) -> paraM f p x) (from p x) >>= \ r -> f p r x
+paraM f p x = hmapM (\ p (I0 x) -> paraM f p x) p (from p x) >>= \ r -> f p r x
 
 -- * Creating an algebra
 
@@ -96,3 +95,4 @@
 
 con :: AlgPart a r ix -> AlgPart (C c a) r ix
 con f (C x) = f x
+
diff --git a/src/Generics/MultiRec/FoldAlg.hs b/src/Generics/MultiRec/FoldAlg.hs
--- a/src/Generics/MultiRec/FoldAlg.hs
+++ b/src/Generics/MultiRec/FoldAlg.hs
@@ -6,11 +6,12 @@
 {-# LANGUAGE Rank2Types            #-}
 {-# LANGUAGE ScopedTypeVariables   #-}
 {-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE GADTs                 #-}
 
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Generics.MultiRec.FoldAlg
--- Copyright   :  (c) 2009 Universiteit Utrecht
+-- Copyright   :  (c) 2009--2010 Universiteit Utrecht
 -- License     :  BSD3
 --
 -- Maintainer  :  generics@haskell.org
@@ -38,6 +39,9 @@
 -- | For a constant, we take the constant value to a result.
 type instance Alg (K a) (r :: * -> *) ix = a -> r ix
 
+-- type instance Alg (f :.: g) r ix = f (r ix) -> r ix -- f (Comp g r ix) -> r ix
+type instance Alg (f :.: I xi) r ix = f (r xi) -> r ix
+
 -- | For a unit, no arguments are available.
 type instance Alg U (r :: * -> *) ix = r ix
 
@@ -50,11 +54,7 @@
 
 -- | For a product where the left hand side is a constant, we
 --   take the value as an additional argument.
-type instance Alg (K a :*: g) r ix = a -> Alg g r ix
-
--- | For a product where the left hand side is an identity, we
---   take the recursive result as an additional argument.
-type instance Alg (I xi :*: g) r ix = r xi -> Alg g r ix
+type instance Alg (f :*: g) r ix = Comp f r ix -> Alg g r ix
 
 -- | A tag changes the index of the final result.
 type instance Alg (f :>: xi) r ix = Alg f r xi
@@ -62,6 +62,17 @@
 -- | Constructors are ignored.
 type instance Alg (C c f) r ix = Alg f r ix
 
+type family Comp (f :: (* -> *) -> * -> *) 
+                 (r :: * -> *)      -- recursive positions
+                 (ix :: *)          -- index
+                 :: *
+
+type instance Comp (I xi)    r ix = r xi
+
+type instance Comp (K a)     r ix = a
+
+type instance Comp (f :.: g) r ix = f (Comp g r ix)
+
 -- | The algebras passed to the fold have to work for all index types
 --   in the family. The additional witness argument is required only
 --   to make GHC's typechecker happy.
@@ -84,6 +95,9 @@
 instance Fold (I xi) where
   alg f (I x) = f x
 
+instance (Functor f) => Fold (f :.: I xi) where
+  alg f (D x) = f (fmap unI x)
+
 instance (Fold f, Fold g) => Fold (f :+: g) where
   alg (f, g) (L x) = alg f x
   alg (f, g) (R x) = alg g x
@@ -106,7 +120,7 @@
 fold :: forall phi ix r . (Fam phi, HFunctor phi (PF phi), Fold (PF phi)) =>
         Algebra phi r -> phi ix -> ix -> r ix
 fold f p = alg (f p) .
-           hmap (\ p (I0 x) -> fold f p x) .
+           hmap (\ p (I0 x) -> fold f p x) p .
            from p
 
 -- * Construction of algebras
diff --git a/src/Generics/MultiRec/FoldAlgK.hs b/src/Generics/MultiRec/FoldAlgK.hs
--- a/src/Generics/MultiRec/FoldAlgK.hs
+++ b/src/Generics/MultiRec/FoldAlgK.hs
@@ -6,11 +6,12 @@
 {-# LANGUAGE Rank2Types            #-}
 {-# LANGUAGE ScopedTypeVariables   #-}
 {-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE GADTs                 #-}
 
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Generics.MultiRec.FoldAlgK
--- Copyright   :  (c) 2009 Universiteit Utrecht
+-- Copyright   :  (c) 2009--2010 Universiteit Utrecht
 -- License     :  BSD3
 --
 -- Maintainer  :  generics@haskell.org
@@ -105,7 +106,7 @@
 fold :: forall phi ix r . (Fam phi, HFunctor phi (PF phi), Fold (PF phi)) =>
         Algebra phi r -> phi ix -> ix -> r
 fold f p = alg (f p) .
-           hmap (\ p (I0 x) -> K0 (fold f p x)) .
+           hmap (\ p (I0 x) -> K0 (fold f p x)) p .
            from p
 
 -- * Construction of algebras
diff --git a/src/Generics/MultiRec/FoldK.hs b/src/Generics/MultiRec/FoldK.hs
--- a/src/Generics/MultiRec/FoldK.hs
+++ b/src/Generics/MultiRec/FoldK.hs
@@ -9,7 +9,7 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Generics.MultiRec.FoldK
--- Copyright   :  (c) 2009 Universiteit Utrecht
+-- Copyright   :  (c) 2009--2010 Universiteit Utrecht
 -- License     :  BSD3
 --
 -- Maintainer  :  generics@haskell.org
@@ -27,7 +27,6 @@
 import Generics.MultiRec.HFunctor
 
 import Control.Monad hiding (foldM)
-import Control.Applicative
 
 -- * Generic fold and unfold
 
@@ -38,11 +37,11 @@
 
 fold :: (Fam phi, HFunctor phi (PF phi)) =>
         Algebra phi r -> phi ix -> ix -> r
-fold f p = f p . hmap (\ p (I0 x) -> K0 (fold f p x)) . from p
+fold f p = f p . hmap (\ p (I0 x) -> K0 (fold f p x)) p . from p
 
 foldM :: (Fam phi, HFunctor phi (PF phi), Monad m) =>
          AlgebraF phi m r -> phi ix -> ix -> m r
-foldM f p x = hmapM (\ p (I0 x) -> liftM K0 (foldM f p x)) (from p x) >>= f p
+foldM f p x = hmapM (\ p (I0 x) -> liftM K0 (foldM f p x)) p (from p x) >>= f p
 
 type CoAlgebra'  phi f   r = forall ix. phi ix -> r -> f (K0 r) ix
 type CoAlgebra   phi     r = CoAlgebra' phi (PF phi) r
@@ -51,11 +50,11 @@
 
 unfold :: (Fam phi, HFunctor phi (PF phi)) =>
           CoAlgebra phi r -> phi ix -> r -> ix
-unfold f p = to p . hmap (\ p (K0 x) -> I0 (unfold f p x)) . f p
+unfold f p = to p . hmap (\ p (K0 x) -> I0 (unfold f p x)) p . f p
 
 unfoldM :: (Fam phi, HFunctor phi (PF phi), Monad m) =>
            CoAlgebraF phi m r -> phi ix -> r -> m ix
-unfoldM f p x = f p x >>= liftM (to p) . hmapM (\ p (K0 x) -> liftM I0 (unfoldM f p x))
+unfoldM f p x = f p x >>= liftM (to p) . hmapM (\ p (K0 x) -> liftM I0 (unfoldM f p x)) p
 
 type ParaAlgebra'  phi f   r = forall ix. phi ix -> f (K0 r) ix -> ix -> r
 type ParaAlgebra   phi     r = ParaAlgebra' phi (PF phi) r
@@ -64,11 +63,11 @@
 
 para :: (Fam phi, HFunctor phi (PF phi)) => 
         ParaAlgebra phi r -> phi ix -> ix -> r
-para f p x = f p (hmap (\ p (I0 x) -> K0 (para f p x)) (from p x)) x
+para f p x = f p (hmap (\ p (I0 x) -> K0 (para f p x)) p (from p x)) x
 
 paraM :: (Fam phi, HFunctor phi (PF phi), Monad m) => 
          ParaAlgebraF phi m r -> phi ix -> ix -> m r
-paraM f p x = hmapM (\ p (I0 x) -> liftM K0 (paraM f p x)) (from p x) >>= \ r -> f p r x
+paraM f p x = hmapM (\ p (I0 x) -> liftM K0 (paraM f p x)) p (from p x) >>= \ r -> f p r x
 
 -- * Creating an algebra
 
diff --git a/src/Generics/MultiRec/HFix.hs b/src/Generics/MultiRec/HFix.hs
--- a/src/Generics/MultiRec/HFix.hs
+++ b/src/Generics/MultiRec/HFix.hs
@@ -5,7 +5,7 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Generics.MultiRec.HFix
--- Copyright   :  (c) 2008--2009 Universiteit Utrecht
+-- Copyright   :  (c) 2008--2010 Universiteit Utrecht
 -- License     :  BSD3
 --
 -- Maintainer  :  generics@haskell.org
diff --git a/src/Generics/MultiRec/HFunctor.hs b/src/Generics/MultiRec/HFunctor.hs
--- a/src/Generics/MultiRec/HFunctor.hs
+++ b/src/Generics/MultiRec/HFunctor.hs
@@ -7,7 +7,7 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Generics.MultiRec.HFunctor
--- Copyright   :  (c) 2008--2009 Universiteit Utrecht
+-- Copyright   :  (c) 2008--2010 Universiteit Utrecht
 -- License     :  BSD3
 --
 -- Maintainer  :  generics@haskell.org
@@ -19,8 +19,8 @@
 -----------------------------------------------------------------------------
 module Generics.MultiRec.HFunctor where
 
-import Control.Monad (liftM, liftM2)
 import Control.Applicative (Applicative(..), (<$>), (<*>), WrappedMonad(..))
+import Data.Traversable (Traversable(..))
 
 import Generics.MultiRec.Base
 
@@ -32,29 +32,32 @@
 class HFunctor phi f where
   hmapA :: (Applicative a) =>
            (forall ix. phi ix -> r ix -> a (r' ix)) ->
-           f r ix -> a (f r' ix)
+           phi ix -> f r ix -> a (f r' ix)
 
 instance El phi xi => HFunctor phi (I xi) where
-  hmapA f (I x) = I <$> f proof x
+  hmapA f _ (I x) = I <$> f proof x
 
 instance HFunctor phi (K x) where
-  hmapA _ (K x) = pure (K x)
+  hmapA _ _ (K x) = pure (K x)
 
 instance HFunctor phi U where
-  hmapA _ U = pure U
+  hmapA _ _ U = pure U
 
 instance (HFunctor phi f, HFunctor phi g) => HFunctor phi (f :+: g) where
-  hmapA f (L x) = L <$> hmapA f x
-  hmapA f (R y) = R <$> hmapA f y
+  hmapA f p (L x) = L <$> hmapA f p x
+  hmapA f p (R y) = R <$> hmapA f p y
 
 instance (HFunctor phi f, HFunctor phi g) => HFunctor phi (f :*: g) where
-  hmapA f (x :*: y) = (:*:) <$> hmapA f x <*> hmapA f y
+  hmapA f p (x :*: y) = (:*:) <$> hmapA f p x <*> hmapA f p y
 
 instance HFunctor phi f => HFunctor phi (f :>: ix) where
-  hmapA f (Tag x) = Tag <$> hmapA f x
+  hmapA f p (Tag x) = Tag <$> hmapA f p x
 
+instance (Traversable f, HFunctor phi g) => HFunctor phi (f :.: g) where
+  hmapA f p (D x) = D <$> traverse (hmapA f p) x
+
 instance (Constructor c, HFunctor phi f) => HFunctor phi (C c f) where
-  hmapA f (C x) = C <$> hmapA f x
+  hmapA f p (C x) = C <$> hmapA f p x
 
 -- | The function 'hmap' takes a functor @f@. All the recursive instances
 -- in that functor are wrapped by an application of @r@. The argument to
@@ -64,11 +67,11 @@
 -- parameterized by a witness of type @phi ix@. 
 hmap  :: (HFunctor phi f) =>
          (forall ix. phi ix -> r ix -> r' ix) ->
-         f r ix -> f r' ix
-hmap f x = unI0 (hmapA (\ ix x -> I0 (f ix x)) x)
+         phi ix -> f r ix -> f r' ix
+hmap f p x = unI0 (hmapA (\ ix x -> I0 (f ix x)) p x)
 
 -- | Monadic version of 'hmap'.
 hmapM :: (HFunctor phi f, Monad m) =>
          (forall ix. phi ix -> r ix -> m (r' ix)) ->
-         f r ix -> m (f r' ix)
-hmapM f x = unwrapMonad (hmapA (\ ix x -> WrapMonad (f ix x)) x)
+         phi ix -> f r ix -> m (f r' ix)
+hmapM f p x = unwrapMonad (hmapA (\ ix x -> WrapMonad (f ix x)) p x)
diff --git a/src/Generics/MultiRec/Read.hs b/src/Generics/MultiRec/Read.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/MultiRec/Read.hs
@@ -0,0 +1,196 @@
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE Rank2Types            #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE GADTs                 #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Generics.MultiRec.Read
+-- Copyright   :  (c) 2009--2010 Universiteit Utrecht
+-- License     :  BSD3
+--
+-- Maintainer  :  generics@haskell.org
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Generic read.
+--
+-----------------------------------------------------------------------------
+module Generics.MultiRec.Read where
+
+import Generics.MultiRec.Base
+
+import Control.Monad
+import Data.Char
+import Text.ParserCombinators.ReadP (sepBy)
+import Text.Read hiding (readsPrec, readPrec)
+import Prelude hiding (readsPrec)
+import qualified Prelude as P (readsPrec)
+
+
+-- Based on Rui Barbosa's solution.
+
+
+-- Count the number of terms in a product
+
+class CountAtoms (f :: (* -> *) -> * -> *) where
+  countatoms :: f r ix -> Int
+
+instance CountAtoms (K a) where
+  countatoms _ = 1
+
+instance CountAtoms (I xi) where
+  countatoms _ = 1
+
+instance (CountAtoms f, CountAtoms g) => CountAtoms (f :*: g) where
+  countatoms (_ :: (f :*: g) r ix) = countatoms (undefined :: f r ix) + countatoms (undefined :: g r ix)
+
+-- * Generic read
+
+class HReadPrec (phi :: * -> *) (f :: (* -> *) -> * -> *) where
+   hreader :: forall ix . phi ix -> (forall ix1 . phi ix1 -> ReadPrec (I0 ix1)) -> ReadPrec (f I0 ix)
+
+
+instance HReadPrec phi U where
+   hreader p f = return U
+
+instance (Read a) => HReadPrec phi (K a) where
+   hreader p f = liftM K (readS_to_Prec P.readsPrec)
+
+instance (El phi xi) => HReadPrec phi (I xi) where
+   hreader p f = liftM I (f proof)
+
+instance (HReadPrec phi f, HReadPrec phi g) => HReadPrec phi (f :+: g) where
+   hreader p f = liftM L (hreader p f)  +++ liftM R (hreader p f)
+
+instance (HReadPrec phi f, HReadPrec phi g) => HReadPrec phi (f :*: g) where
+   hreader p f = liftM2 (:*:) (hreader p f) (hreader p f)
+
+instance (HReadPrec phi f, EqS phi, El phi ix) => HReadPrec phi (f :>: ix) where
+   hreader p f = case eqS p (proof :: phi ix) of
+                       Nothing    ->  pfail
+                       Just Refl  ->  liftM Tag (hreader p f)
+
+instance (Read1 f, HReadPrec phi g) => HReadPrec phi (f :.: g) where
+   hreader p f = liftM D (read1 (hreader p f))
+
+class Read1 f where
+  read1 :: ReadPrec (g I0 ix) -> ReadPrec (f (g I0 ix))
+
+instance Read1 [] where
+  read1 pe = do
+    Punc "[" <- lexP
+    xs <- lift $ sepBy (readPrec_to_P pe 0)
+                       (readPrec_to_P (do Punc "," <- lexP; return ()) 0)
+    Punc "]" <- lexP
+    return xs
+
+instance Read1 Maybe where
+  read1 pe =
+    (readNoArgsCons "Nothing" >> return Nothing) +++
+    (liftM Just $ readPrefixCons pe True "Just")
+
+-- Dealing with constructors
+
+-- No arguments
+instance (Constructor c) => HReadPrec phi (C c U) where
+   hreader p f = let constr = undefined :: C c U I0 ix
+                     name   = conName constr
+                 in readCons (readNoArgsCons name)
+
+-- 1 argument
+instance (Constructor c, HReadPrec phi (I xi)) => HReadPrec phi (C c (I xi)) where
+   hreader p f = let constr = undefined :: C c (I xi) I0 ix
+                     name   = conName constr
+                 in  readCons (readPrefixCons (hreader p f) True name)
+
+instance (Constructor c, HReadPrec phi (K a)) => HReadPrec phi (C c (K a)) where
+   hreader p f = let constr = undefined :: C c (K a) I0 ix
+                     name   = conName constr
+                 in  readCons (readPrefixCons (hreader p f) True name)
+
+instance (Constructor c, HReadPrec phi (f :.: g)) => HReadPrec phi (C c (f :.: g)) where
+   hreader p f = let constr = undefined :: C c (f :.: g) I0 ix
+                     name   = conName constr
+                 in  readCons (readPrefixCons (hreader p f) True name)
+
+-- 2 arguments or more
+instance forall f g phi c . (Constructor c, CountAtoms (f :*: g), HReadPrec phi f , HReadPrec phi g) => HReadPrec phi (C c (f:*:g)) where
+   hreader p f = let constr = undefined :: C c (f:*:g) I0 ix
+                     name   = conName constr
+                     fixity = conFixity constr
+                     (assoc,prc,isInfix) = case fixity of
+                                            Prefix      -> (LeftAssociative, 9, False)
+                                            Infix a p   -> (a, p, True)
+                     --K0F nargs  = countatoms  :: K0F Int (f:*:g)
+                     nargs  = countatoms (undefined :: (f :*: g) r ix)
+                  in   readCons $
+                               readPrefixCons (hreader p f) (not isInfix) name
+                                        +++
+                               (do guard (nargs==2)
+                                   readInfixCons p f (assoc,prc,isInfix) name
+                               )
+
+
+readCons :: (Constructor c) => ReadPrec (f I0 ix) -> ReadPrec (C c f I0 ix)
+readCons = liftM C
+
+readPrefixCons :: ReadPrec (f I0 ix)
+                  -> Bool -> String -> ReadPrec (f I0 ix)
+readPrefixCons pe b name  = parens . prec appPrec $
+                            do parens (prefixConsNm name b)
+                               step pe
+    where prefixConsNm name True  = do Ident n <- lexP
+                                       guard (name == n)
+          prefixConsNm name False = do Punc "(" <-lexP
+                                       Symbol n <- lexP
+                                       guard (name==n)
+                                       Punc ")" <- lexP
+                                       return ()
+
+
+readInfixCons :: (HReadPrec phi f, HReadPrec phi g) =>
+                    phi ix
+                 -> (forall ix1. phi ix1 -> ReadPrec (I0 ix1))
+                 -> (Associativity,Int,Bool) -> String -> ReadPrec ((f :*: g) I0 ix)
+readInfixCons p f (asc,prc,b) name = parens . prec prc $
+                                       do x <- {- (if asc == LeftAssociative  then id else step) -} step (hreader p f)
+                                          parens (infixConsNm name b)
+                                          y <- (if asc == RightAssociative then id else step) (hreader p f)
+                                          return  (x :*: y)
+     where  infixConsNm name True  = do Symbol n <- lexP
+                                        guard (n==name)
+            infixConsNm name False = do Punc "`"  <- lexP
+                                        Ident n   <- lexP
+                                        guard (n==name)
+                                        Punc "`"  <- lexP
+                                        return ()
+
+readNoArgsCons :: String -> ReadPrec (U I0 ix)
+readNoArgsCons name = parens $
+                      do Ident n <- lexP
+                         guard (n==name)
+                         return U
+
+appPrec :: Int
+appPrec = 10
+
+
+-- Exported functions
+
+readPrec :: (Fam phi, HReadPrec phi (PF phi)) => phi ix -> ReadPrec ix
+readPrec p = liftM (to p)  (hreader p (liftM I0 . readPrec))
+
+
+readsPrec :: (Fam phi, HReadPrec phi (PF phi)) => phi ix -> Int -> ReadS ix
+readsPrec = readPrec_to_S . readPrec
+
+read :: (Fam phi, HReadPrec phi (PF phi)) => phi ix -> String -> ix
+read p s = case [x |  (x,remain) <- readsPrec p 0 s , all isSpace remain] of
+               [x] -> x
+               [ ] -> error "no parse"
+               _   -> error "ambiguous parse"
diff --git a/src/Generics/MultiRec/Show.hs b/src/Generics/MultiRec/Show.hs
--- a/src/Generics/MultiRec/Show.hs
+++ b/src/Generics/MultiRec/Show.hs
@@ -3,11 +3,13 @@
 {-# LANGUAGE TypeOperators         #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE UndecidableInstances  #-}
 
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Generics.MultiRec.Show
--- Copyright   :  (c) 2008--2009 Universiteit Utrecht
+-- Copyright   :  (c) 2008--2010 Universiteit Utrecht
 -- License     :  BSD3
 --
 -- Maintainer  :  generics@haskell.org
@@ -26,9 +28,14 @@
 
 import qualified Prelude as P
 import Prelude hiding (show, showsPrec)
+import Data.Traversable (Traversable(..))
 
 -- * Generic show
 
+-- | The list in the result type allows us to get at
+-- the fields of a constructor individually, which in
+-- turn allows us to insert additional stuff in between
+-- if record notation is used.
 class HFunctor phi f => HShow phi f where
   hShowsPrecAlg :: Algebra' phi f [Int -> ShowS]
 
@@ -53,6 +60,9 @@
 instance HShow phi f => HShow phi (f :>: ix) where
   hShowsPrecAlg ix (Tag x) = hShowsPrecAlg ix x
 
+instance (Show1 f, Traversable f, HShow phi g) => HShow phi (f :.: g) where
+  hShowsPrecAlg ix (D x) = [show1 (fmap (hShowsPrecAlg ix) x)]
+ 
 instance (Constructor c, HShow phi f) => HShow phi (C c f) where
   hShowsPrecAlg ix cx@(C x) =
     case conFixity cx of
@@ -63,6 +73,17 @@
    where
     fields = hShowsPrecAlg ix x
 
+class Show1 f where
+  show1 :: f [Int -> ShowS] -> Int -> ShowS
+
+instance Show1 Maybe where
+  show1 Nothing  _ = ("Nothing" ++)
+  show1 (Just x) n = showParen (n > 10) (spaces (("Just" ++) : map ($ 11) x))
+
+instance Show1 [] where
+  show1 [] _ = ("[]" ++)
+  show1 xs _ = ('[':) . commas (map ($ 0) (concat xs)) . (']':)
+
 showsPrec :: (Fam phi, HShow phi (PF phi)) => phi ix -> Int -> ix -> ShowS
 showsPrec p n x = spaces (map ($ n) (fold hShowsPrecAlg p x))
 
@@ -72,6 +93,13 @@
 -- * Utilities
 
 spaces :: [ShowS] -> ShowS
-spaces []     = id
-spaces [x]    = x
-spaces (x:xs) = x . (' ':) . spaces xs
+spaces = intersperse " "
+
+commas :: [ShowS] -> ShowS
+commas = intersperse ", "
+
+intersperse :: String -> [ShowS] -> ShowS
+intersperse s []     = id
+intersperse s [x]    = x
+intersperse s (x:xs) = x . (s ++) . spaces xs
+
diff --git a/src/Generics/MultiRec/TEq.hs b/src/Generics/MultiRec/TEq.hs
--- a/src/Generics/MultiRec/TEq.hs
+++ b/src/Generics/MultiRec/TEq.hs
@@ -5,7 +5,7 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Generics.MultiRec.TEq
--- Copyright   :  (c) 2008--2009 Universiteit Utrecht
+-- Copyright   :  (c) 2008--2010 Universiteit Utrecht
 -- License     :  BSD3
 --
 -- Maintainer  :  generics@haskell.org
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,11 +1,13 @@
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE GADTs           #-}
 {-# LANGUAGE KindSignatures  #-}
+{-# LANGUAGE PatternGuards   #-}
+{-# LANGUAGE CPP             #-}
 
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Generics.MultiRec.TH
--- Copyright   :  (c) 2008--2009 Universiteit Utrecht
+-- Copyright   :  (c) 2008--2010 Universiteit Utrecht
 -- License     :  BSD3
 --
 -- Maintainer  :  generics@haskell.org
@@ -13,7 +15,7 @@
 -- Portability :  non-portable
 --
 -- This module contains Template Haskell code that can be used to
--- automatically generate the boilerplate code for the multiplate
+-- automatically generate the boilerplate code for the multirec
 -- library. The constructor information can be generated per datatype,
 -- the rest per family of datatypes.
 --
@@ -21,7 +23,8 @@
 
 
 module Generics.MultiRec.TH
-  ( deriveConstructors,
+  ( deriveAll,
+    deriveConstructors,
     deriveFamily, deriveSystem,
     derivePF,
     deriveEl,
@@ -30,172 +33,364 @@
   ) where
 
 import Generics.MultiRec.Base
-import Generics.MultiRec.Constructor
 import Language.Haskell.TH hiding (Fixity())
-import Language.Haskell.TH.Syntax (Lift(..))
+import Control.Applicative
 import Control.Monad
+import Data.Foldable (foldrM)
+import Data.Maybe (fromJust)
 
--- | 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 ps  = init (extractParameters info)
+    -- runIO (print $ ps)
+    -- runIO (print $ extractConstructorNames ps 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 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
+-- 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)
+    el  <- deriveEl n [] (zip ns (repeat []))
+    fam <- deriveFam n [] 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 (:[]) $
-    tySynD (mkName pfn) [] (foldr1 sum (map (pfType ns) ns))
+    return <$>
+    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
 
--- | Derive only the 'El' instances. Not needed if 'deriveFamily'
--- is used.
-
-deriveEl :: Name -> [Name] -> Q [Dec]
-deriveEl s ns =
-  mapM (elInstance s) ns
+derivePFInstance :: Name -> [Name] -> [(Name, [Name])] -> Q [Dec]
+derivePFInstance n ps nps = return <$> myTySynInst
+  where
+    sum :: Q Type -> Q Type -> Q Type
+    sum a b = conT ''(:+:) `appT` a `appT` b
+    tys = [foldl appT (conT n) (map varT ps)]
+    ty  = foldr1 sum (map (pfType (map fst nps) ps) nps)
+#if __GLASGOW_HASKELL__ > 706
+    myTySynInst = tySynInstD ''PF (tySynEqn tys ty)
+#else
+    myTySynInst = tySynInstD ''PF tys ty
+#endif
 
--- | Dervie only the 'Fam' instance. Not needed if 'deriveFamily'
+-- | Derive only the 'El' instances. Not needed if 'deriveAll'
 -- is used.
+deriveEl :: Name -> [Name] -> [(Name, [Name])] -> Q [Dec]
+deriveEl s ps ns =
+  mapM (elInstance s ps) ns
 
-deriveFam :: Name -> [Name] -> Q [Dec]
-deriveFam s ns =
+-- | Derive only the 'Fam' instance. Not needed if 'deriveAll'
+-- is used.
+deriveFam :: Name -> [Name] -> [Name] -> Q [Dec]
+deriveFam s ps ns =
   do
-    fcs <- liftM concat $ zipWithM (mkFrom ns (length ns)) [0..] ns  
+    fcs <- liftM concat $ zipWithM (mkFrom ns (length ns)) [0..] ns
     tcs <- liftM concat $ zipWithM (mkTo   ns (length ns)) [0..] ns
-    liftM (:[]) $
-      instanceD (cxt []) (conT ''Fam `appT` conT s)
+    return <$>
+      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 'deriveFamily'
+-- | Derive only the 'EqS' instance. Not needed if 'deriveAll'
 -- is used.
-
-deriveEqS :: Name -> [Name] -> Q [Dec]
-deriveEqS s ns =
-    liftM (:[]) $
-    instanceD (cxt []) (conT ''EqS `appT` conT s)
-      [funD 'eqS (map trueClause ns ++ [falseClause])]
+deriveEqS :: Name -> [Name] -> [Name] -> Q [Dec]
+deriveEqS s ps ns =
+    return <$>
+    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)) []
     falseClause  = clause [wildP,  wildP]        (normalB (conE 'Nothing)) []
+    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 :: [Name] -> Info -> [(Name, [Name])]
+#if MIN_VERSION_template_haskell(2,11,0)
+extractConstructorNames ps (TyConI (DataD _ _ _ _ cs _)) = concatMap extractFrom cs
+#else
+extractConstructorNames ps (TyConI (DataD _ _ _ cs _)) = concatMap extractFrom cs
+#endif
+  where
+    extractFrom :: Con -> [(Name, [Name])]
+    extractFrom (ForallC _ eqs c) = map (\ (n, ps) -> (n, ps ++ concatMap extractEq eqs)) (extractFrom c)
+    extractFrom (InfixC _ n _)    = [(n, [])]
+    extractFrom (RecC n _)        = [(n, [])]
+    extractFrom (NormalC n [])    = [(n, [])]
+#if MIN_VERSION_template_haskell(2,11,0)
+    extractFrom (GadtC ns _ t)    = map (\ n -> (n, extractType t)) ns
+#endif
+    extractFrom _                 = []
+
+    extractEq :: Pred -> [Name]
+#if __GLASGOW_HASKELL__ > 708
+    extractEq (EqualityT `AppT` t1 `AppT` t2) =
+#else
+    extractEq (EqualP t1 t2) =
+#endif
+      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 _                 = []
+
+    extractType :: Type -> [Name]
+    extractType (AppT a1 a2) = combine (extractVars a1) (extractVars a2)
+      where
+        combine :: [Name] -> [Name] -> [Name]
+        combine vs1 vs2 =
+          let
+            table = zip vs1 ps
+          in
+            map (fromJust . flip lookup table) vs2
+    extractType _            = []
+
+    extractVars :: Type -> [Name]
+    extractVars (AppT t (VarT v)) = extractVars t ++ [v]
+    extractVars (AppT t _)        = extractVars t
+    extractVars _                 = []
+
+extractConstructorNames _  _                           = []
+
+
+-- | Process the reified info of the index GADT, and extract
+-- its type parameters.
+extractParameters :: Info -> [Name]
+#if MIN_VERSION_template_haskell(2,11,0)
+extractParameters (TyConI (DataD _ _ ns _ _ _)) = concatMap extractFromBndr ns
+#else
+extractParameters (TyConI (DataD _ _ ns _ _)) = concatMap extractFromBndr ns
+#endif
+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
+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
     i <- reify n
     -- runIO (print i)
     let cs = case i of
+#if MIN_VERSION_template_haskell(2,11,0)
+               TyConI (DataD _ _ _ _ cs _) -> cs
+#else
                TyConI (DataD _ _ _ cs _) -> cs
+#endif
                _ -> []
     ds <- mapM mkData cs
     is <- mapM mkInstance cs
     return $ ds ++ is
 
+-- | Given a constructor, create an empty datatype of
+-- the same name.
 mkData :: Con -> Q Dec
 mkData (NormalC n _) =
-  dataD (cxt []) (mkName (nameBase n)) [] [] [] 
+#if MIN_VERSION_template_haskell(2,12,0)
+  dataD (cxt []) (remakeName n) [] Nothing [] []
+#elif MIN_VERSION_template_haskell(2,11,0)
+  dataD (cxt []) (remakeName n) [] Nothing [] (cxt [])
+#else
+  dataD (cxt []) (remakeName n) [] [] []
+#endif
+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
+#if MIN_VERSION_template_haskell(2,11,0)
+      i <- reifyFixity n
+      let fi = case i of
+                 Just f  -> convertFixity f
+                 Nothing -> Prefix
+#else
       i <- reify n
       let fi = case i of
                  DataConI _ _ _ f -> convertFixity f
                  _ -> Prefix
-      instanceD (cxt []) (appT (conT ''Constructor) (conT $ mkName (nameBase n)))
+#endif
+      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
 
-pfType :: [Name] -> Name -> Q Type
-pfType ns n =
+-- | 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] -> (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
+#if MIN_VERSION_template_haskell(2,11,0)
+                TyConI (DataD _ _ _ _ cs _) ->
+#else
                 TyConI (DataD _ _ _ cs _) ->
-                  foldr1 sum (map (pfCon ns) cs)
+#endif
+                  foldr1 sum (map (pfCon ns (zip qs rs)) 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))
+                  conT ''K `appT` foldl appT (conT t) (map varT rs)
+                _ -> error "unknown construct"
+      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
 
-pfCon :: [Name] -> Con -> Q Type
-pfCon ns (NormalC n []) =
-    appT (appT (conT ''C) (conT $ mkName (nameBase n))) (conT ''U)
-pfCon ns (NormalC n fs) =
-    appT (appT (conT ''C) (conT $ mkName (nameBase n))) (foldr1 prod (map (pfField ns . snd) fs))
+-- | 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] -> [(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 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 ps . snd) fs))
   where
     prod :: Q Type -> Q Type -> Q Type
     prod a b = conT ''(:*:) `appT` a `appT` b
-pfCon ns (InfixC t1 n t2) =
-    pfCon ns (NormalC n [t1,t2])
 
-pfField :: [Name] -> Type -> Q Type
-pfField ns t@(ConT n) | n `elem` ns = conT ''I `appT` return t
-pfField ns t                        = conT ''K `appT` return t
+-- | 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] -> [(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)
+  | TupleT n : ts <- unApp t           = foldrM (\ s t -> conT ''(:*:) `appT` pfField ns ps s `appT` return t) (ConT ''U) ts
+  | otherwise                          = 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
       -- 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
+#if MIN_VERSION_template_haskell(2,11,0)
+                TyConI (DataD _ _ _ _ cs _) ->
+#else
                 TyConI (DataD _ _ _ cs _) ->
+#endif
                   zipWith (fromCon wrapE ns dn (length cs)) [0..] cs
                 TyConI (TySynD t _ _) ->
                   [clause [conP dn [], varP (field 0)] (normalB (wrapE $ conE 'K `appE` varE (field 0))) []]
@@ -208,18 +403,22 @@
       -- 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
+#if MIN_VERSION_template_haskell(2,11,0)
+                TyConI (DataD _ _ _ _ cs _) ->
+#else
                 TyConI (DataD _ _ _ cs _) ->
+#endif
                   zipWith (toCon wrapP ns dn (length cs)) [0..] cs
                 TyConI (TySynD t _ _) ->
                   [clause [conP dn [], wrapP $ conP 'K [varP (field 0)]] (normalB $ varE (field 0)) []]
-                _ -> error "unknown construct" 
+                _ -> error "unknown construct"
       return b
 
 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 []) =
@@ -233,8 +432,12 @@
       (normalB $ wrap $ lrE m i $ conE 'C `appE` foldr1 prod (zipWith (fromField ns) [0..] (map snd fs))) []
   where
     prod x y = conE '(:*:) `appE` x `appE` y
+fromCon wrap ns n m i r@(RecC _ _) =
+  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 []) =
@@ -244,21 +447,49 @@
 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) (map (varE . field) [0..length fs - 1])) []
+      [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 = conE 'I `appE` (conE 'I0 `appE` varE (field nr))
-fromField ns nr t                        = conE 'K `appE` 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                        = conP 'K [varP (field nr)]
+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)
+  | TupleT n : ts <- unApp t = mapM (newName . ("x" ++) . show) [1..n] >>= \ vs ->
+                               lam1E (tupP (varP <$> vs)) $
+                               foldrM (\ (v, t) x -> conE '(:*:) `appE` (fromFieldFun ns t `appE` varE v) `appE` return x) (ConE 'U) (zip vs ts)
+  | otherwise                = [| D . fmap $(fromFieldFun ns a) |]
+fromFieldFun ns t            = [| K |]
 
+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
+  | ConT n : a <- unApp t, remakeName n `elem` ns
+                             = [| unI0 . unI |]
+toFieldFun ns t@(AppT f a)
+  | TupleT n : ts <- unApp t = mapM (newName . ("x" ++) . show) [1..n] >>= \ vs ->
+                               lam1E (foldr (\ v p -> conP '(:*:) [varP v, p]) (conP 'U []) vs) $
+                               tupE (zipWith (\ v t -> toFieldFun ns t `appE` varE v) vs ts)
+  | otherwise                = [| fmap $(toFieldFun ns a) . unD |]
+toFieldFun ns t              = [| unK |]
+
 field :: Int -> Name
 field n = mkName $ "f" ++ show n
 
@@ -272,3 +503,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)