diff --git a/examples/AST.hs b/examples/AST.hs
--- a/examples/AST.hs
+++ b/examples/AST.hs
@@ -22,7 +22,7 @@
   deriving Show
 
 data Decl   =  Var := Expr
-            |  Seq    Decl  Decl
+            |  Seq    [Decl]
             |  None
   deriving Show
 
diff --git a/examples/ASTExamples.hs b/examples/ASTExamples.hs
--- a/examples/ASTExamples.hs
+++ b/examples/ASTExamples.hs
@@ -25,8 +25,8 @@
 
 -- | 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'
 
@@ -67,7 +67,7 @@
            &.  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)
@@ -84,7 +84,7 @@
      &  (\ (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)
diff --git a/examples/ASTUse.hs b/examples/ASTUse.hs
--- a/examples/ASTUse.hs
+++ b/examples/ASTUse.hs
@@ -58,7 +58,7 @@
        :+:  C Let     (I Decl :*: I Expr)
       ) :>: Expr
   :+: (     C Assign  (I Var  :*: I Expr)
-       :+:  C Seq     (I Decl :*: I Decl)
+       :+:  C Seq     ([] :.: I Decl)
        :+:  C None    U
       ) :>: Decl
   :+: (               (K String)
@@ -81,7 +81,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,7 +93,7 @@
   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
diff --git a/multirec.cabal b/multirec.cabal
--- a/multirec.cabal
+++ b/multirec.cabal
@@ -1,5 +1,5 @@
 name:                 multirec
-version:              0.5.1
+version:              0.6
 license:              BSD3
 license-file:         LICENSE
 author:               Alexey Rodriguez,
@@ -10,6 +10,7 @@
 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
@@ -36,8 +37,8 @@
  
 stability:            experimental
 build-type:           Simple
-cabal-version:        >= 1.2.1
-tested-with:          GHC == 6.10.4, GHC == 7.0.1
+cabal-version:        >= 1.6
+tested-with:          GHC == 7.0.4
 extra-source-files:   examples/AST.hs
                       examples/ASTUse.hs
                       examples/ASTTHUse.hs
@@ -48,8 +49,13 @@
                       examples/SingleExamples.hs
                       CREDITS
 
+source-repository head
+  type:               git
+  location:           https://github.com/kosmikus/multirec
+
 library
   hs-source-dirs:     src
+  -- ghc-options:        -Wall -fno-warn-name-shadowing -fno-warn-unused-binds -fno-warn-unused-matches
   exposed-modules:    Generics.MultiRec
 
                       -- Base
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
@@ -31,6 +31,7 @@
    I(..),
    K(..), U(..), (:+:)(..), (:*:)(..),
    (:>:)(..), unTag,
+   (:.:)(..),
    C(..), unC,
 
    -- ** Constructor information
@@ -81,6 +82,10 @@
 -- | 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 (f (g r ix))
 
 -- | Represents constructors.
 data C c f     (r :: * -> *) 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
@@ -23,7 +23,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 +41,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/Eq.hs b/src/Generics/MultiRec/Eq.hs
--- a/src/Generics/MultiRec/Eq.hs
+++ b/src/Generics/MultiRec/Eq.hs
@@ -29,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
 
@@ -47,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/FoldAlg.hs b/src/Generics/MultiRec/FoldAlg.hs
--- a/src/Generics/MultiRec/FoldAlg.hs
+++ b/src/Generics/MultiRec/FoldAlg.hs
@@ -39,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
 
@@ -51,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
@@ -63,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 +94,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
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
@@ -27,7 +27,6 @@
 import Generics.MultiRec.HFunctor
 
 import Control.Monad hiding (foldM)
-import Control.Applicative
 
 -- * Generic fold and unfold
 
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
@@ -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
 
@@ -52,6 +52,9 @@
 
 instance HFunctor phi f => HFunctor phi (f :>: ix) where
   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 p (C x) = C <$> hmapA f p x
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
@@ -25,8 +25,10 @@
 
 import Generics.MultiRec.Base
 
-import Data.Char
 import Control.Monad
+import Data.Char
+import Data.Traversable
+import Text.ParserCombinators.ReadP (char, skipSpaces, sepBy)
 import Text.Read hiding (readsPrec, readPrec)
 import Prelude hiding (readsPrec)
 import qualified Prelude as P (readsPrec)
@@ -37,7 +39,7 @@
 
 -- Count the number of terms in a product
 
-class CountAtoms (f :: (* -> *) -> * -> *) where 
+class CountAtoms (f :: (* -> *) -> * -> *) where
   countatoms :: f r ix -> Int
 
 instance CountAtoms (K a) where
@@ -71,41 +73,65 @@
    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 
+   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 p f name)
+                 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 p f True name)
+                 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 p f True name) 
+                 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 
+                     (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 p f (not isInfix) name
+                  in   readCons $
+                               readPrefixCons (hreader p f) (not isInfix) name
                                         +++
                                (do guard (nargs==2)
                                    readInfixCons p f (assoc,prc,isInfix) name
@@ -115,47 +141,44 @@
 readCons :: (Constructor c) => ReadPrec (f I0 ix) -> ReadPrec (C c f I0 ix)
 readCons = liftM C
 
-readPrefixCons :: (HReadPrec phi f) => 
-                     phi ix  
-                  -> (forall ix1. phi ix1 -> ReadPrec (I0 ix1)) 
+readPrefixCons :: ReadPrec (f I0 ix)
                   -> Bool -> String -> ReadPrec (f I0 ix)
-readPrefixCons p f b name = parens . prec appPrec $
-                            do parens (prefixConsNm name b) 
-                               step (hreader p f)
+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)   
+                                       guard (name==n)
                                        Punc ")" <- lexP
                                        return ()
 
 
-readInfixCons :: (HReadPrec phi f, HReadPrec phi g) => 
-                    phi ix 
-                 -> (forall ix1. phi ix1 -> ReadPrec (I0 ix1)) 
+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) 
+     where  infixConsNm name True  = do Symbol n <- lexP
+                                        guard (n==name)
             infixConsNm name False = do Punc "`"  <- lexP
-                                        Ident n   <- lexP  
+                                        Ident n   <- lexP
                                         guard (n==name)
-                                        Punc "`"  <- lexP 
+                                        Punc "`"  <- lexP
                                         return ()
 
-readNoArgsCons ::   phi ix 
-                 -> (forall ix1. phi ix1 -> ReadPrec (I0 ix1)) 
-                 -> String -> ReadPrec (U I0 ix)
-readNoArgsCons p f name = parens $ 
-                             do Ident n <- lexP
-                                guard (n==name)
-                                return U
+readNoArgsCons :: String -> ReadPrec (U I0 ix)
+readNoArgsCons name = parens $
+                      do Ident n <- lexP
+                         guard (n==name)
+                         return U
 
+appPrec :: Int
 appPrec = 10
 
 
@@ -166,10 +189,10 @@
 
 
 readsPrec :: (Fam phi, HReadPrec phi (PF phi)) => phi ix -> Int -> ReadS ix
-readsPrec = readPrec_to_S . readPrec 
+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 
+               [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
@@ -4,6 +4,7 @@
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE UndecidableInstances  #-}
 
 -----------------------------------------------------------------------------
 -- |
@@ -27,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]
 
@@ -54,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
@@ -64,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))
 
@@ -73,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/TH.hs b/src/Generics/MultiRec/TH.hs
--- a/src/Generics/MultiRec/TH.hs
+++ b/src/Generics/MultiRec/TH.hs
@@ -30,12 +30,11 @@
   ) where
 
 import Generics.MultiRec.Base
-import Generics.MultiRec.Constructor
 import Language.Haskell.TH hiding (Fixity())
 import Language.Haskell.TH.Syntax (Lift(..))
 import Control.Monad
 
--- | Given a list of datatype names, derive datatypes and 
+-- | Given a list of datatype names, derive datatypes and
 -- instances of class 'Constructor'.
 
 deriveConstructors :: [Name] -> Q [Dec]
@@ -87,7 +86,7 @@
 deriveFam :: Name -> [Name] -> Q [Dec]
 deriveFam s 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)
@@ -126,7 +125,7 @@
 
 mkData :: Con -> Q Dec
 mkData (NormalC n _) =
-  dataD (cxt []) (mkName (nameBase n)) [] [] [] 
+  dataD (cxt []) (mkName (nameBase n)) [] [] []
 mkData r@(RecC _ _) =
   mkData (stripRecordNames r)
 mkData (InfixC t1 n t2) =
@@ -172,7 +171,7 @@
                   foldr1 sum (map (pfCon ns) cs)
                 TyConI (TySynD t _ _) ->
                   conT ''K `appT` conT t
-                _ -> error "unknown construct" 
+                _ -> error "unknown construct"
       appT (appT (conT ''(:>:)) b) (conT $ mkName (nameBase n))
   where
     sum :: Q Type -> Q Type -> Q Type
@@ -193,6 +192,7 @@
 
 pfField :: [Name] -> Type -> Q Type
 pfField ns t@(ConT n) | 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
 
 elInstance :: Name -> Name -> Q Dec
@@ -227,7 +227,7 @@
                   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
@@ -260,7 +260,7 @@
     -- 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])) []
+      (normalB $ foldl appE (conE cn) (zipWith toFieldR [0..] (map snd fs))) []
   where
     prod x y = conP '(:*:) [x,y]
 toCon wrap ns n m i r@(RecC _ _) =
@@ -269,12 +269,18 @@
   toCon wrap ns n m i (NormalC cn [t1,t2])
 
 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@(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)) |]
 
 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)]
+
+toFieldR :: Int -> Type -> Q Exp
+toFieldR nr t@(AppT f a) = [| fmap (unI0 . unI) $(varE (field nr)) |]
+toFieldR nr _            = varE (field nr)
 
 field :: Int -> Name
 field n = mkName $ "f" ++ show n