diff --git a/examples/ASTExamples.hs b/examples/ASTExamples.hs
--- a/examples/ASTExamples.hs
+++ b/examples/ASTExamples.hs
@@ -31,9 +31,9 @@
 renameVar :: Expr -> Expr
 renameVar = renameVar' Expr
   where
-    renameVar' :: Ix AST a => AST a -> a -> a
+    renameVar' :: AST a -> a -> a
     renameVar' Var x = x ++ "_"
-    renameVar' _   x = compos renameVar' x
+    renameVar' p   x = compos renameVar' p x
 
 -- | Test for 'renameVar'
 
@@ -90,12 +90,12 @@
 -- | Evaluator
 
 eval1 :: Expr -> Env -> Int
-eval1 x = let (EV f) = F.fold evalAlgebra1 x in f
+eval1 x = let (EV f) = F.fold evalAlgebra1 Expr x in f
 
 -- | Evaluator
 
 eval2 :: Expr -> Env -> Int
-eval2 x = let (EV f) = FA.fold evalAlgebra2 x in f
+eval2 x = let (EV f) = FA.fold evalAlgebra2 Expr x in f
 
 -- | Test for 'eval1'
 
diff --git a/examples/ASTUse.hs b/examples/ASTUse.hs
--- a/examples/ASTUse.hs
+++ b/examples/ASTUse.hs
@@ -64,41 +64,37 @@
   :+: (               (K String)
       ) :>: Var
 
--- ** 'Ix' instances
-
-instance Ix AST Expr where
-
-  from_ (Const i)  =  L (Tag (L          (C (K i))))
-  from_ (Add e f)  =  L (Tag (R (L       (C (I (I0 e) :*: I (I0 f))))))
-  from_ (Mul e f)  =  L (Tag (R (R (L    (C (I (I0 e) :*: I (I0 f)))))))
-  from_ (EVar x)   =  L (Tag (R (R (R (L (C (I (I0 x))))))))
-  from_ (Let d e)  =  L (Tag (R (R (R (R (C (I (I0 d) :*: I (I0 e))))))))
-
-  to_ (L (Tag (L          (C (K i)))))                       =  Const i
-  to_ (L (Tag (R (L       (C (I (I0 e) :*: I (I0 f)))))))    =  Add e f
-  to_ (L (Tag (R (R (L    (C (I (I0 e) :*: I (I0 f))))))))   =  Mul e f
-  to_ (L (Tag (R (R (R (L (C (I (I0 x)))))))))               =  EVar x
-  to_ (L (Tag (R (R (R (R (C (I (I0 d) :*: I (I0 e)))))))))  =  Let d e
+-- ** 'El' instances
 
-  index  =  Expr
+instance El AST Expr where proof = Expr
+instance El AST Decl where proof = Decl
+instance El AST Var  where proof = Var
 
-instance Ix AST Decl where
+-- ** 'Fam' instance
 
-  from_ (x := e)   =  R (L (Tag (L    (C (I (I0 x) :*: I (I0 e))))))
-  from_ (Seq c d)  =  R (L (Tag (R (L (C (I (I0 c) :*: I (I0 d)))))))
-  from_ (None)     =  R (L (Tag (R (R (C U)))))
+instance Fam AST where
 
-  to_ (R (L (Tag (L    (C (I (I0 x) :*: I (I0 e)))))))   =  x := e
-  to_ (R (L (Tag (R (L (C (I (I0 c) :*: I (I0 d))))))))  = Seq c d
-  to_ (R (L (Tag (R (R (C U))))))                        = None
+  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))))))
+  from Expr (Mul e f)  =  L (Tag (R (R (L    (C (I (I0 e) :*: I (I0 f)))))))
+  from Expr (EVar x)   =  L (Tag (R (R (R (L (C (I (I0 x))))))))
+  from Expr (Let d e)  =  L (Tag (R (R (R (R (C (I (I0 d) :*: I (I0 e))))))))
 
-  index  =  Decl
+  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 (None)     =  R (L (Tag (R (R (C U)))))
 
-instance Ix AST Var where
+  from Var  x          =  R (R (Tag (K x)))
 
-  from_ x  =  R (R (Tag (K x)))
+  to Expr (L (Tag (L          (C (K i)))))                       =  Const i
+  to Expr (L (Tag (R (L       (C (I (I0 e) :*: I (I0 f)))))))    =  Add e f
+  to Expr (L (Tag (R (R (L    (C (I (I0 e) :*: I (I0 f))))))))   =  Mul e f
+  to Expr (L (Tag (R (R (R (L (C (I (I0 x)))))))))               =  EVar x
+  to Expr (L (Tag (R (R (R (R (C (I (I0 d) :*: I (I0 e)))))))))  =  Let d e
 
-  to_ (R (R (Tag (K x))))  =  x
+  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 (R (C U))))))                            =  None
 
-  index  =  Var
+  to Var  (R (R (Tag (K x))))                                    =  x
 
diff --git a/examples/SingleExamples.hs b/examples/SingleExamples.hs
--- a/examples/SingleExamples.hs
+++ b/examples/SingleExamples.hs
@@ -8,12 +8,13 @@
 -- Replace SingleUse with SingleTHUse below if you want
 -- to test TH code generation.
 import SingleUse
+-- import SingleTHUse
 import Single
 
 -- | evalLogic takes a function that gives a logic values to variables,
 -- | and a Logic expression, and evaluates it.
 evalLogic :: (String -> Bool) -> Logic -> Bool
-evalLogic env = fold algebra 
+evalLogic env = fold algebra Logic
  where
    algebra :: Algebra LogicF Bool
    algebra _ = env & impl & (==) & (&&) & (||) & not & True & False
diff --git a/examples/SingleUse.hs b/examples/SingleUse.hs
--- a/examples/SingleUse.hs
+++ b/examples/SingleUse.hs
@@ -62,26 +62,28 @@
        :+:  C F     U
       ) :>: Logic
 
--- ** 'Ix' instances
+-- ** 'El' instance
 
-instance Ix LogicF Logic where
+instance El LogicF Logic where proof = Logic
 
-  from_ (Var s)       = Tag (L                   (C (K s)))
-  from_ (l1 :->: l2)  = Tag (R (L                (C (I (I0 l1) :*: I (I0 l2)))))
-  from_ (l1 :<->: l2) = Tag (R (R (L             (C (I (I0 l1) :*: I (I0 l2))))))
-  from_ (l1 :&&: l2)  = Tag (R (R (R (L          (C (I (I0 l1) :*: I (I0 l2)))))))
-  from_ (l1 :||: l2)  = Tag (R (R (R (R (L       (C (I (I0 l1) :*: I (I0 l2))))))))
-  from_ (Not l)       = Tag (R (R (R (R (R (L    (C (I (I0 l)))))))))
-  from_ T             = Tag (R (R (R (R (R (R (L (C U))))))))
-  from_ F             = Tag (R (R (R (R (R (R (R (C U))))))))
+-- ** 'Fam' instance
 
-  to_ (Tag (L                   (C (K s))))                         = Var s
-  to_ (Tag (R (L                (C (I (I0 l1) :*: I (I0 l2))))))    = l1 :->: l2
-  to_ (Tag (R (R (L             (C (I (I0 l1) :*: I (I0 l2)))))))   = l1 :<->: l2
-  to_ (Tag (R (R (R (L          (C (I (I0 l1) :*: I (I0 l2))))))))  = l1 :&&: l2
-  to_ (Tag (R (R (R (R (L       (C (I (I0 l1) :*: I (I0 l2))))))))) = l1 :||: l2
-  to_ (Tag (R (R (R (R (R (L    (C (I (I0 l))))))))))               = Not l
-  to_ (Tag (R (R (R (R (R (R (L (C U)))))))))                       = T
-  to_ (Tag (R (R (R (R (R (R (R (C U)))))))))                       = F
+instance Fam LogicF where
 
-  index  =  Logic
+  from Logic (Var s)       = Tag (L                   (C (K s)))
+  from Logic (l1 :->: l2)  = Tag (R (L                (C (I (I0 l1) :*: I (I0 l2)))))
+  from Logic (l1 :<->: l2) = Tag (R (R (L             (C (I (I0 l1) :*: I (I0 l2))))))
+  from Logic (l1 :&&: l2)  = Tag (R (R (R (L          (C (I (I0 l1) :*: I (I0 l2)))))))
+  from Logic (l1 :||: l2)  = Tag (R (R (R (R (L       (C (I (I0 l1) :*: I (I0 l2))))))))
+  from Logic (Not l)       = Tag (R (R (R (R (R (L    (C (I (I0 l)))))))))
+  from Logic T             = Tag (R (R (R (R (R (R (L (C U))))))))
+  from Logic F             = Tag (R (R (R (R (R (R (R (C U))))))))
+
+  to Logic (Tag (L                   (C (K s))))                         = Var s
+  to Logic (Tag (R (L                (C (I (I0 l1) :*: I (I0 l2))))))    = l1 :->: l2
+  to Logic (Tag (R (R (L             (C (I (I0 l1) :*: I (I0 l2)))))))   = l1 :<->: l2
+  to Logic (Tag (R (R (R (L          (C (I (I0 l1) :*: I (I0 l2))))))))  = l1 :&&: l2
+  to Logic (Tag (R (R (R (R (L       (C (I (I0 l1) :*: I (I0 l2))))))))) = l1 :||: l2
+  to Logic (Tag (R (R (R (R (R (L    (C (I (I0 l))))))))))               = Not l
+  to Logic (Tag (R (R (R (R (R (R (L (C U)))))))))                       = T
+  to Logic (Tag (R (R (R (R (R (R (R (C U)))))))))                       = F
diff --git a/multirec.cabal b/multirec.cabal
--- a/multirec.cabal
+++ b/multirec.cabal
@@ -1,5 +1,5 @@
 name:			multirec
-version:		0.2
+version:		0.3
 license:		BSD3
 license-file:		LICENSE
 author:			Alexey Rodriguez,
@@ -8,7 +8,7 @@
                         Johan Jeuring
 maintainer:		generics@haskell.org
 category:		Generics
-synopsis:		Generic programming with systems of recursive datatypes
+synopsis:		Generic programming for families of recursive datatypes
 homepage:		http://www.cs.uu.nl/wiki/GenericProgramming/Multirec
 description:
   Many generic programs require information about the recursive positions
@@ -16,16 +16,16 @@
   the Zipper data structure. Several generic programming systems allow to
   write such functions by viewing datatypes as fixed points of a pattern
   functor. Traditionally, this view has been limited to so-called regular
-  datatypes such as lists and binary trees. In particular, systems of
+  datatypes such as lists and binary trees. In particular, families of
   mutually recursive datatypes have been excluded.
   .
   With the multirec library, we provide a mechanism to talk about fixed
-  points of systems of datatypes that may be mutually recursive. On top
+  points of families of datatypes that may be mutually recursive. On top
   of this representations, generic functions such as the fold or the Zipper
   can then be defined.
   .
   We expect that the library will be especially interesting for compiler
-  writers, because ASTs are typically systems of mutually recursive datatypes,
+  writers, because ASTs are typically families of mutually recursive datatypes,
   and with multirec it becomes easy to write generic functions on ASTs.
   .
   The library is based on ideas described in the paper:
@@ -38,7 +38,7 @@
 stability:		experimental
 build-type:		Simple
 cabal-version:		>= 1.2.1
-tested-with:		GHC == 6.8.3, GHC == 6.10.1
+tested-with:		GHC == 6.8.3, GHC == 6.10.3
 hs-source-dirs:		src
 exposed-modules:	Generics.MultiRec
 
@@ -59,6 +59,9 @@
 			Generics.MultiRec.Eq
 			Generics.MultiRec.Show
 
+			-- Extra
+			Generics.MultiRec.TEq
+
 extra-source-files:	examples/AST.hs
                         examples/ASTUse.hs
                         examples/ASTTHUse.hs
@@ -68,5 +71,5 @@
 			examples/SingleTHUse.hs
 			examples/SingleExamples.hs
 			CREDITS
-build-depends:		base >= 3.0 && < 4,
+build-depends:		base >= 3.0 && < 5,
                         template-haskell >= 2.2 && < 2.4
diff --git a/src/Generics/MultiRec.hs b/src/Generics/MultiRec.hs
--- a/src/Generics/MultiRec.hs
+++ b/src/Generics/MultiRec.hs
@@ -9,7 +9,7 @@
 -- Portability :  non-portable
 --
 -- multirec --
--- generic programming with systems of recursive datatypes
+-- generic programming for families of recursive datatypes
 -- 
 -- This top-level module re-exports all other modules of the library.
 --
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
@@ -17,9 +17,9 @@
 -- Portability :  non-portable
 --
 -- This module is the base of the multirec library. It defines the view of a
--- system of datatypes: All the datatypes of the system are represented as
+-- family of datatypes: All the datatypes of the family are represented as
 -- indexed functors that are built up from the structure types defined in this
--- module. Furthermore, in order to use the library for a system, conversion
+-- module. Furthermore, in order to use the library for a family, conversion
 -- functions have to be defined between the original datatypes and their
 -- representation. The type class that holds these conversion functions are
 -- also defined here.
@@ -28,7 +28,7 @@
 
 module Generics.MultiRec.Base 
   (-- * Structure types
-   I(..), unI,
+   I(..),
    K(..), U(..), (:+:)(..), (:*:)(..),
    (:>:)(..), unTag,
    C(..), unC,
@@ -39,12 +39,17 @@
    -- ** Unlifted variants
    I0(..), K0(..),
 
-   -- * Indexed systems
-   PF, Str, Ix(..)
+   -- * Indexed families
+   PF, El(..), Fam(..), index,
+
+   -- ** Equality for indexed families
+   module Generics.MultiRec.TEq,
+   EqS(..)
   ) where
 
 import Control.Applicative
 import Generics.MultiRec.Constructor
+import Generics.MultiRec.TEq
 
 -- * Structure types
 
@@ -53,41 +58,36 @@
 infixr 7 :*:
 
 -- | Represents recursive positions. The first argument indicates
--- which type (within the system) to recurse on.
-data I :: * -> (* -> *) -> (* -> *) -> * -> * where
-  I :: Ix s xi => r xi -> I xi s r ix
-
--- | Destructor for 'I'.
-unI :: I xi s r ix -> r xi
-unI (I x) = x
+-- which type to recurse on.
+data I xi      (r :: * -> *) ix = I {unI :: r xi}
 
--- | Represents constant types that do not belong to the system.
-data K a       (s :: * -> *) (r :: * -> *) ix = K {unK :: a}
+-- | Represents constant types that do not belong to the family.
+data K a       (r :: * -> *) ix = K {unK :: a}
 
 -- | Represents constructors without fields.
-data U         (s :: * -> *) (r :: * -> *) ix = U
+data U         (r :: * -> *) ix = U
 
 -- | Represents sums (choices between constructors).
-data (f :+: g) (s :: * -> *) (r :: * -> *) ix = L (f s r ix) | R (g s r ix)
+data (f :+: g) (r :: * -> *) ix = L (f r ix) | R (g r ix)
 
 -- | Represents products (sequences of fields of a constructor).
-data (f :*: g) (s :: * -> *) (r :: * -> *) ix = f s r ix :*: g s r ix
+data (f :*: g) (r :: * -> *) ix = f r ix :*: g r ix
 
--- | Is used to indicate the type (within the system) that a
+-- | Is used to indicate the type that a
 -- particular constructor injects to.
-data (:>:) :: ((* -> *) -> (* -> *) -> * -> *) -> * -> (* -> *) -> (* -> *) -> * -> * where
-  Tag :: f s r ix -> (f :>: ix) s r ix
+data f :>: ix :: (* -> *) -> * -> * where
+  Tag :: f r ix -> (f :>: ix) r ix
 
 -- | Destructor for '(:>:)'.
-unTag :: (f :>: ix) s r ix -> f s r ix
+unTag :: (f :>: ix) r ix -> f r ix
 unTag (Tag x) = x
 
 -- | Represents constructors.
-data C c f     (s :: * -> *) (r :: * -> *) ix where
-  C :: (Constructor c) => f s r ix -> C c f s r ix
+data C c f     (r :: * -> *) ix where
+  C :: f r ix -> C c f r ix
 
 -- | Destructor for 'C'.
-unC :: C c f s r ix -> f s r ix
+unC :: C c f r ix -> f r ix
 unC (C x) = x
 
 -- ** Unlifted variants
@@ -108,23 +108,25 @@
 instance Functor (K0 a) where
   fmap f = K0 . unK0
 
--- * Indexed systems
+-- * Indexed families
 
--- | Type family describing the pattern functor of a system.
-type family PF s :: (* -> *) -> (* -> *) -> * -> *
-type Str s ix = (PF s) s I0 ix
+-- | Type family describing the pattern functor of a family.
+type family PF phi :: (* -> *) -> * -> *
 
-class Ix s ix where
-  from_ :: ix -> Str s ix
-  to_   :: Str s ix -> ix
+-- | Class for the members of a family.
+class El phi ix where
+  proof :: phi ix
 
-  -- | Some functions need to have their types desugared in order to make programs
-  -- that use them typable.  Desugaring consists in transforming ``inline'' type
-  -- family applications into equality constraints. This is a strangeness in current
-  -- versions of GHC that hopefully will be fixed sometime in the future.
-  from  :: (pfs ~ PF s) => ix -> pfs s I0 ix
-  from = from_
-  to    :: (pfs ~ PF s) => pfs s I0 ix -> ix
-  to = to_
+-- | For backwards-compatibility: a synonym for 'proof'.
+index :: El phi ix => phi ix
+index = proof
 
-  index :: s ix
+-- | Class that contains the shallow conversion functions for a family.
+class Fam phi where
+  from :: phi ix -> ix -> PF phi I0 ix
+  to   :: phi ix -> PF phi I0 ix -> ix
+
+-- | Semi-decidable equality for types of a family.
+class EqS phi where
+  eqS :: phi ix -> phi ix' -> Maybe (ix :=: ix')
+
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
@@ -30,16 +30,16 @@
 -- * Compos
 
 -- | Normal version.
-compos :: (Ix s ix, HFunctor (PF s)) =>
-          (forall ix. Ix s ix => s ix -> ix -> ix) -> ix -> ix
-compos f = to . hmap (\ ix -> I0 . f ix . unI0) . from
+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
 
 -- | Monadic version of 'compos'.
-composM :: (Ix s ix, HFunctor (PF s), Monad m) =>
-           (forall ix. Ix s ix => s ix -> ix -> m ix) -> ix -> m ix
-composM f = liftM to . hmapM (\ ix -> liftM I0 . f ix . unI0) . from
+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
 
 -- | Applicative version of 'compos'.
-composA :: (Ix s ix, HFunctor (PF s), Applicative a) =>
-           (forall ix. Ix s ix => s ix -> ix -> a ix) -> ix -> a ix
-composA f = liftA to . hmapA (\ ix -> liftA I0 . f ix . unI0) . from
+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
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
@@ -15,7 +15,7 @@
 -- Stability   :  experimental
 -- Portability :  non-portable
 --
--- Generic function that returns the constructor names available in a system
+-- Generic function that returns the constructor names available in a family
 -- of datatypes.
 --
 -----------------------------------------------------------------------------
@@ -25,15 +25,15 @@
 import Generics.MultiRec.Base
 import Generics.MultiRec.Constructor
 
-class ConNames (f :: (* -> *) -> (* -> *) -> * -> *) where
-  hconNames :: f s r ix -> [String]
+class ConNames (f :: (* -> *) -> * -> *) where
+  hconNames :: f r ix -> [String]
 
 instance Constructor c => ConNames (C c f) where
   hconNames c = [conName c]
 
 instance (ConNames f, ConNames g) => ConNames (f :+: g) where
-  hconNames (_ :: (f :+: g) r s ix) = hconNames (undefined :: f r s ix) ++
-                                      hconNames (undefined :: g r s ix)
+  hconNames (_ :: (f :+: g) r ix) = hconNames (undefined :: f r ix) ++
+                                    hconNames (undefined :: g r ix)
 
 instance ConNames (K x) where
   hconNames _ = []
@@ -48,7 +48,7 @@
   hconNames _ = []
 
 instance (ConNames f) => ConNames (f :>: ix) where
-  hconNames (_ :: (f :>: ix) r s xi) = hconNames (undefined :: f r s ix)
+  hconNames (_ :: (f :>: ix) r xi) = hconNames (undefined :: f r ix)
 
-conNames :: forall s ix . (Ix s ix, ConNames (PF s)) => s ix -> [String]
-conNames s = hconNames (undefined :: PF s s I0 ix)
+conNames :: forall phi ix . (ConNames (PF phi)) => phi ix -> [String]
+conNames _ = hconNames (undefined :: PF phi I0 ix)
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
@@ -24,8 +24,8 @@
 -- The weird argument is supposed to be instantiated with 'C' from
 -- base, hence the complex kind.
 class Constructor c where
-  conName   :: t c (f :: (* -> *) -> (* -> *) -> * -> *) (s :: * -> *) (r :: * -> *) ix -> String
-  conFixity :: t c (f :: (* -> *) -> (* -> *) -> * -> *) (s :: * -> *) (r :: * -> *) ix -> Fixity
+  conName   :: t c (f :: (* -> *) -> * -> *) (r :: * -> *) ix -> String
+  conFixity :: t c (f :: (* -> *) -> * -> *) (r :: * -> *) ix -> Fixity
   conFixity = const Prefix
 
 -- | Datatype to represent the fixity of a constructor. An infix declaration
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
@@ -1,6 +1,8 @@
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE RankNTypes       #-}
-{-# LANGUAGE TypeOperators    #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances     #-}
 
 -----------------------------------------------------------------------------
 -- |
@@ -22,52 +24,51 @@
 
 -- * Generic equality
 
-class HEq f where
-  heq :: s ix ->
-         (forall ix. Ix s ix => s ix -> r ix -> r ix -> Bool) ->
-         f s r ix -> f s r ix -> Bool
+class HEq phi f where
+  heq :: (forall ix. phi ix -> r ix -> r ix -> Bool) ->
+         phi ix -> f r ix -> f r ix -> Bool
 
-instance HEq (I xi) where
-  heq _ eq (I x1) (I x2) = eq index x1 x2
+instance El phi xi => HEq phi (I xi) where
+  heq eq _ (I x1) (I x2) = eq proof x1 x2
 
 -- | For constant types, we make use of the standard
 -- equality function.
-instance Eq x => HEq (K x) where
-  heq _ eq (K x1) (K x2) = x1 == x2
+instance Eq a => HEq phi (K a) where
+  heq eq _ (K x1) (K x2) = x1 == x2
 
-instance HEq U where
-  heq _ eq U U = True
+instance HEq phi U where
+  heq eq _ U U = True
 
-instance (HEq f, HEq g) => HEq (f :+: g) where
-  heq ix eq (L x1) (L x2) = heq ix eq x1 x2
-  heq ix eq (R y1) (R y2) = heq ix eq y1 y2
-  heq _  eq _     _       = False
+instance (HEq phi f, HEq phi g) => HEq phi (f :+: g) where
+  heq eq p (L x1) (L x2) = heq eq p x1 x2
+  heq eq p (R y1) (R y2) = heq eq p y1 y2
+  heq eq _ _     _       = False
 
-instance (HEq f, HEq g) => HEq (f :*: g) where
-  heq ix eq (x1 :*: y1) (x2 :*: y2) = heq ix eq x1 x2 && heq ix eq y1 y2
+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
 
 -- The following instance does not compile with ghc-6.8.2
-instance HEq f => HEq (f :>: ix) where
-  heq ix eq (Tag x1) (Tag x2) = heq ix eq x1 x2
+instance HEq phi f => HEq phi (f :>: ix) where
+  heq eq p (Tag x1) (Tag x2) = heq eq p x1 x2
 
-instance HEq f => HEq (C c f) where
-  heq ix eq (C x1) (C x2) = heq ix eq x1 x2
+instance (Constructor c, HEq phi f) => HEq phi (C c f) where
+  heq eq p (C x1) (C x2) = heq eq p x1 x2
 
-eq :: (Ix s ix, HEq (PF s)) => s ix -> ix -> ix -> Bool
-eq ix x1 x2 = heq ix (\ ix (I0 x1) (I0 x2) -> eq ix x1 x2) (from x1) (from x2)
+eq :: (Fam phi, HEq phi (PF phi)) => phi ix -> ix -> ix -> Bool
+eq p x1 x2 = heq (\ p (I0 x1) (I0 x2) -> eq p x1 x2) p (from p x1) (from p x2)
 
 -- Note:
 -- 
 -- We do not declare an equality instance such as
 --
---   instance (Ix s ix, HEq (PF s)) => Eq ix where
---     (==) = eq index
+--   instance (El phi ix, HEq phi (PF phi)) => Eq ix where
+--     (==) = eq proof
 --
--- because "s" is not mentioned on the right hand side.
--- One datatype may belong to multiple systems, and
+-- because "phi" is not mentioned on the right hand side.
+-- One datatype may belong to multiple families, and
 -- although the generic equality instances should be
 -- the same, there is no good way to decide which instance
 -- to use.
 --
--- For a concrete "s", it is still possible to manually
+-- For a concrete "phi", it is still possible to manually
 -- define an "Eq" instance as above.
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
@@ -25,7 +25,8 @@
 --   * for folds with constant return type, look at 
 --     "Generics.MultiRec.FoldAlgK" (or "Generics.MultiRec.FoldK"),
 --
---   * for other folds, look at "Generics.MultiRec.FoldAlg".
+--   * for folds with convenient algebras, look at
+--     "Generics.MultiRec.FoldAlg".
 --
 -----------------------------------------------------------------------------
 
@@ -39,64 +40,59 @@
 
 -- * Generic fold and unfold
 
-type Algebra'  s f   r = forall ix. Ix s ix => s ix -> f s r ix -> r ix
-type Algebra   s     r = Algebra' s (PF s) r
-type AlgebraF' s f g r = forall ix. Ix s ix => s ix -> f s r ix -> g (r ix)
-type AlgebraF  s   g r = AlgebraF' s (PF s) g r
+type Algebra'  phi f   r = forall ix. phi ix -> f r ix -> r ix
+type Algebra   phi     r = Algebra' phi (PF phi) r
+type AlgebraF' phi f g r = forall ix. phi ix -> f r ix -> g (r ix)
+type AlgebraF  phi   g r = AlgebraF' phi (PF phi) g r
 
-fold :: (Ix s ix, HFunctor (PF s)) =>
-        Algebra s r -> ix -> r ix
-fold f = f index . hmap (\ _ (I0 x) -> fold f x) . from
+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
 
-foldM :: (Ix s ix, HFunctor (PF s), Monad m) =>
-         AlgebraF s m r -> ix -> m (r ix)
-foldM f x = hmapM (\ _ (I0 x) -> foldM f x) (from x) >>= f index
+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
 
-type CoAlgebra'  s f   r = forall ix. Ix s ix => s ix -> r ix -> f s r ix
-type CoAlgebra   s     r = CoAlgebra' s (PF s) r
-type CoAlgebraF' s f g r = forall ix. Ix s ix => s ix -> r ix -> g (f s r ix)
-type CoAlgebraF  s   g r = CoAlgebraF' s (PF s) g r
+type CoAlgebra'  phi f   r = forall ix. phi ix -> r ix -> f r ix
+type CoAlgebra   phi     r = CoAlgebra' phi (PF phi) r
+type CoAlgebraF' phi f g r = forall ix. phi ix -> r ix -> g (f r ix)
+type CoAlgebraF  phi   g r = CoAlgebraF' phi (PF phi) g r
 
-unfold :: (Ix s ix, HFunctor (PF s)) =>
-          CoAlgebra s r -> r ix -> ix
-unfold f = to . hmap (\ _ x -> I0 (unfold f x)) . f index
+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
 
-unfoldM :: (Ix s ix, HFunctor (PF s), Monad m) =>
-           CoAlgebraF s m r -> r ix -> m ix
-unfoldM f x = f index x >>= liftMto . hmapM (\ _ x -> liftM I0 (unfoldM f x))
-  where
-    -- only for ghc-6.8.3 compatibility
-    liftMto :: (Monad m, Ix s ix, pfs ~ PF s) => m (pfs s I0 ix) -> m ix
-    liftMto = liftM to
+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))
 
-type ParaAlgebra'  s f   r = forall ix. Ix s ix => s ix -> f s r ix -> ix -> r ix
-type ParaAlgebra   s     r = ParaAlgebra' s (PF s) r
-type ParaAlgebraF' s f g r = forall ix. Ix s ix => s ix -> f s r ix -> ix -> g (r ix)
-type ParaAlgebraF  s   g r = ParaAlgebraF' s (PF s) g r
+type ParaAlgebra'  phi f   r = forall ix. phi ix -> f r ix -> ix -> r ix
+type ParaAlgebra   phi     r = ParaAlgebra' phi (PF phi) r
+type ParaAlgebraF' phi f g r = forall ix. phi ix -> f r ix -> ix -> g (r ix)
+type ParaAlgebraF  phi   g r = ParaAlgebraF' phi (PF phi) g r
 
-para :: (Ix s ix, HFunctor (PF s)) => 
-        ParaAlgebra s r -> ix -> r ix
-para f x = f index (hmap (\ _ (I0 x) -> para f x) (from x)) x
+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
 
-paraM :: (Ix s ix, HFunctor (PF s), Monad m) => 
-         ParaAlgebraF s m r -> ix -> m (r ix)
-paraM f x = hmapM (\ _ (I0 x) -> paraM f x) (from x) >>= \ r -> f index r 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
 
 -- * Creating an algebra
 
 infixr 5 &
 infixr :->
 
-type AlgPart a (s :: * -> *) r ix = a s r ix -> r ix
-type (f :-> g) (s :: * -> *) (r :: * -> *) ix = f s r ix -> g s r ix
+type AlgPart f r ix = f r ix -> r ix
+type (f :-> g) (r :: * -> *) ix = f r ix -> g r ix
 
-(&) :: (AlgPart a :-> AlgPart b :-> AlgPart (a :+: b)) s r ix
+(&) :: (AlgPart a :-> AlgPart b :-> AlgPart (a :+: b)) r ix
 (f & g) (L x) = f x
 (f & g) (R x) = g x 
 
-tag :: AlgPart a s r ix -> AlgPart (a :>: ix) s r ix'
+tag :: AlgPart a r ix -> AlgPart (a :>: ix) r ix'
 tag f (Tag x) = f x
 
-con :: AlgPart a s r ix -> AlgPart (C c a) s r ix
+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
@@ -30,51 +30,50 @@
 -- * The type family of convenient algebras.
 
 -- | The type family we use to describe the convenient algebras.
-type family Alg (f :: (* -> *) -> (* -> *) -> * -> *) 
-                (s :: * -> *)      -- system
+type family Alg (f :: (* -> *) -> * -> *) 
                 (r :: * -> *)      -- recursive positions
                 (ix :: *)          -- index
                 :: *
 
 -- | For a constant, we take the constant value to a result.
-type instance Alg (K a) (s :: * -> *) (r :: * -> *) ix = a -> r ix
+type instance Alg (K a) (r :: * -> *) ix = a -> r ix
 
 -- | For a unit, no arguments are available.
-type instance Alg U (s :: * -> *) (r :: * -> *) ix = r ix
+type instance Alg U (r :: * -> *) ix = r ix
 
 -- | For an identity, we turn the recursive result into a final result.
 --   Note that the index can change.
-type instance Alg (I xi) (s :: * -> *) r ix = r xi -> r ix
+type instance Alg (I xi) r ix = r xi -> r ix
 
 -- | For a sum, the algebra is a pair of two algebras.
-type instance Alg (f :+: g) s r ix = (Alg f s r ix, Alg g s r ix)
+type instance Alg (f :+: g) r ix = (Alg f r ix, Alg g r ix)
 
 -- | 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) s r ix = a -> Alg g s r ix
+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) s r ix = r xi -> Alg g s r ix
+type instance Alg (I xi :*: g) r ix = r xi -> Alg g r ix
 
 -- | A tag changes the index of the final result.
-type instance Alg (f :>: xi) s r ix = Alg f s r xi
+type instance Alg (f :>: xi) r ix = Alg f r xi
 
 -- | Constructors are ignored.
-type instance Alg (C c f) s r ix = Alg f s r ix
+type instance Alg (C c f) r ix = Alg f r ix
 
 -- | The algebras passed to the fold have to work for all index types
---   in the system. The additional witness argument is required only
+--   in the family. The additional witness argument is required only
 --   to make GHC's typechecker happy.
-type Algebra s r = forall ix. Ix s ix => s ix -> Alg (PF s) s r ix
+type Algebra phi r = forall ix. phi ix -> Alg (PF phi) r ix
 
 -- * The class to turn convenient algebras into standard algebras.
 
 -- | The class fold explains how to convert a convenient algebra
 --   'Alg' back into a function from functor to result, as required
 --   by the standard fold function.
-class Fold (f :: (* -> *) -> (* -> *) -> * -> *) where
-  alg :: (Ix s ix) => Alg f s r ix -> f s r ix -> r ix
+class Fold (f :: (* -> *) -> * -> *) where
+  alg :: Alg f r ix -> f r ix -> r ix
 
 instance Fold (K a) where
   alg f (K x) = f x
@@ -103,20 +102,12 @@
 
 -- * Interface
 
--- | Variant of fold that takes an additional witness argument.
-fold_ :: forall s ix r . (Ix s ix, HFunctor (PF s), Fold (PF s)) =>
-         s ix ->
-         Algebra s r ->
-         ix -> r ix
-fold_ ix f = (alg :: Alg (PF s) s r ix -> (PF s) s r ix -> r ix) (f ix) .
-             hmap (\ _ (I0 x) -> fold_ index f x) .
-             from
-
 -- | Fold with convenient algebras.
-fold :: forall s ix r . (Ix s ix, HFunctor (PF s), Fold (PF s)) =>
-        Algebra s r ->
-        ix -> r ix
-fold = fold_ index
+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) .
+           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
@@ -30,50 +30,49 @@
 -- * The type family of convenient algebras.
 
 -- | The type family we use to describe the convenient algebras.
-type family Alg (f :: (* -> *) -> (* -> *) -> * -> *) 
-                (s :: * -> *)      -- system
+type family Alg (f :: (* -> *) -> * -> *) 
                 (r :: *)           -- result type
                 :: *
 
 -- | For a constant, we take the constant value to a result.
-type instance Alg (K a) (s :: * -> *) r = a -> r
+type instance Alg (K a) r = a -> r
 
 -- | For a unit, no arguments are available.
-type instance Alg U (s :: * -> *) r = r
+type instance Alg U r = r
 
 -- | For an identity, we turn the recursive result into a final result.
 --   Note that the index can change.
-type instance Alg (I xi) (s :: * -> *) r = r -> r
+type instance Alg (I xi) r = r -> r
 
 -- | For a sum, the algebra is a pair of two algebras.
-type instance Alg (f :+: g) s r = (Alg f s r, Alg g s r)
+type instance Alg (f :+: g) r = (Alg f r, Alg g r)
 
 -- | 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) s r = a -> Alg g s r
+type instance Alg (K a :*: g) r = a -> Alg g r
 
 -- | 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) s r = r -> Alg g s r
+type instance Alg (I xi :*: g) r = r -> Alg g r
 
--- | A tag changes the index of the final result.
-type instance Alg (f :>: xi) s r = Alg f s r
+-- | Tags are ignored.
+type instance Alg (f :>: xi) r = Alg f r
 
 -- | Constructors are ignored.
-type instance Alg (C c f) s r = Alg f s r
+type instance Alg (C c f) r = Alg f r
 
 -- | The algebras passed to the fold have to work for all index types
---   in the system. The additional witness argument is required only
+--   in the family. The additional witness argument is required only
 --   to make GHC's typechecker happy.
-type Algebra s r = forall ix. Ix s ix => s ix -> Alg (PF s) s r
+type Algebra phi r = forall ix. phi ix -> Alg (PF phi) r
 
 -- * The class to turn convenient algebras into standard algebras.
 
 -- | The class fold explains how to convert a convenient algebra
 --   'Alg' back into a function from functor to result, as required
 --   by the standard fold function.
-class Fold (f :: (* -> *) -> (* -> *) -> * -> *) where
-  alg :: (Ix s ix) => Alg f s r -> f s (K0 r) ix -> r
+class Fold (f :: (* -> *) -> * -> *) where
+  alg :: Alg f r -> f (K0 r) ix -> r
 
 instance Fold (K a) where
   alg f (K x) = f x
@@ -102,20 +101,12 @@
 
 -- * Interface
 
--- | Variant of fold that takes an additional witness argument.
-fold_ :: forall s ix r . (Ix s ix, HFunctor (PF s), Fold (PF s)) =>
-         s ix ->
-         Algebra s r ->
-         ix -> r
-fold_ ix f = (alg :: Alg (PF s) s r -> (PF s) s (K0 r) ix -> r) (f ix) .
-             hmap (\ _ (I0 x) -> K0 (fold_ index f x)) .
-             from
-
 -- | Fold with convenient algebras.
-fold :: forall s ix r . (Ix s ix, HFunctor (PF s), Fold (PF s)) =>
-        Algebra s r ->
-        ix -> r
-fold = fold_ index
+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)) .
+           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
@@ -31,63 +31,59 @@
 
 -- * Generic fold and unfold
 
-type Algebra'  s f   r = forall ix. Ix s ix => s ix -> f s (K0 r) ix -> r
-type Algebra   s     r = Algebra' s (PF s) r
-type AlgebraF' s f g r = forall ix. Ix s ix => s ix -> f s (K0 r) ix -> g r
-type AlgebraF  s   g r = AlgebraF' s (PF s) g r
+type Algebra'  phi f   r = forall ix. phi ix -> f (K0 r) ix -> r
+type Algebra   phi     r = Algebra' phi (PF phi) r
+type AlgebraF' phi f g r = forall ix. phi ix -> f (K0 r) ix -> g r
+type AlgebraF  phi   g r = AlgebraF' phi (PF phi) g r
 
-fold :: (Ix s ix, HFunctor (PF s)) =>
-        Algebra s r -> ix -> r
-fold f = f index . hmap (\ _ (I0 x) -> K0 (fold f x)) . from
+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
 
-foldM :: (Ix s ix, HFunctor (PF s), Monad m) =>
-         AlgebraF s m r -> ix -> m r
-foldM f x = hmapM (\ _ (I0 x) -> liftM K0 (foldM f x)) (from x) >>= f index
+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
 
-type CoAlgebra'  s f   r = forall ix. Ix s ix => s ix -> r -> f s (K0 r) ix
-type CoAlgebra   s     r = CoAlgebra' s (PF s) r
-type CoAlgebraF' s f g r = forall ix. Ix s ix => s ix -> r -> g (f s (K0 r) ix)
-type CoAlgebraF  s   g r = CoAlgebraF' s (PF s) g r
+type CoAlgebra'  phi f   r = forall ix. phi ix -> r -> f (K0 r) ix
+type CoAlgebra   phi     r = CoAlgebra' phi (PF phi) r
+type CoAlgebraF' phi f g r = forall ix. phi ix -> r -> g (f (K0 r) ix)
+type CoAlgebraF  phi   g r = CoAlgebraF' phi (PF phi) g r
 
-unfold :: (Ix s ix, HFunctor (PF s)) =>
-          CoAlgebra s r -> r -> ix
-unfold f = to . hmap (\ _ (K0 x) -> I0 (unfold f x)) . f index
+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
 
-unfoldM :: (Ix s ix, HFunctor (PF s), Monad m) =>
-           CoAlgebraF s m r -> r -> m ix
-unfoldM f x = f index x >>= liftMto . hmapM (\ _ (K0 x) -> liftM I0 (unfoldM f x))
-  where
-    -- only for ghc-6.8.3 compatibility
-    liftMto :: (Monad m, Ix s ix, pfs ~ PF s) => m (pfs s I0 ix) -> m ix
-    liftMto = liftM to
+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))
 
-type ParaAlgebra'  s f   r = forall ix. Ix s ix => s ix -> f s (K0 r) ix -> ix -> r
-type ParaAlgebra   s     r = ParaAlgebra' s (PF s) r
-type ParaAlgebraF' s f g r = forall ix. Ix s ix => s ix -> f s (K0 r) ix -> ix -> g r
-type ParaAlgebraF  s   g r = ParaAlgebraF' s (PF s) g r
+type ParaAlgebra'  phi f   r = forall ix. phi ix -> f (K0 r) ix -> ix -> r
+type ParaAlgebra   phi     r = ParaAlgebra' phi (PF phi) r
+type ParaAlgebraF' phi f g r = forall ix. phi ix -> f (K0 r) ix -> ix -> g r
+type ParaAlgebraF  phi   g r = ParaAlgebraF' phi (PF phi) g r
 
-para :: (Ix s ix, HFunctor (PF s)) => 
-        ParaAlgebra s r -> ix -> r
-para f x = f index (hmap (\ _ (I0 x) -> K0 (para f x)) (from x)) x
+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
 
-paraM :: (Ix s ix, HFunctor (PF s), Monad m) => 
-         ParaAlgebraF s m r -> ix -> m r
-paraM f x = hmapM (\ _ (I0 x) -> liftM K0 (paraM f x)) (from x) >>= \ r -> f index r 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
 
 -- * Creating an algebra
 
 infixr 5 &
 infixr :->
 
-type AlgPart a (s :: * -> *) b ix = a s (K0 b) ix -> b
-type (f :-> g) (s :: * -> *) b ix = f s b ix -> g s b ix
+type AlgPart f b ix = f (K0 b) ix -> b
+type (f :-> g) b ix = f b ix -> g b ix
 
-(&) :: (AlgPart a :-> AlgPart b :-> AlgPart (a :+: b)) s c ix
+(&) :: (AlgPart a :-> AlgPart b :-> AlgPart (a :+: b)) c ix
 (f & g) (L x) = f x
 (f & g) (R x) = g x 
 
-tag :: AlgPart a s c ix -> AlgPart (a :>: ix) s c ix'
+tag :: AlgPart a c ix -> AlgPart (a :>: ix) c ix'
 tag f (Tag x) = f x
 
-con :: AlgPart a s b ix -> AlgPart (C c a) s b ix
+con :: AlgPart a b ix -> AlgPart (C c a) b ix
 con f (C x) = f x
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
@@ -22,13 +22,14 @@
 
 import Generics.MultiRec.Base
 import Generics.MultiRec.HFunctor
+import Generics.MultiRec.Fold
 
 -- * Fixed point of indexed types
 
 data HFix (h :: (* -> *) -> * -> *) ix = HIn { hout :: h (HFix h) ix }
 
-hfrom :: (pfs ~ PF s, Ix s ix, HFunctor (PF s)) => ix -> HFix (pfs s) ix
-hfrom = HIn . hmap (const (hfrom . unI0)) . from
+hfrom :: (Fam phi, HFunctor phi (PF phi)) => phi ix -> ix -> HFix (PF phi) ix
+hfrom = fold (const HIn)
 
-hto :: (pfs ~ PF s, Ix s ix, HFunctor (PF s)) => HFix (pfs s) ix -> ix
-hto = to . hmap (const (I0 . hto)) . hout
+hto :: (Fam phi, HFunctor phi (PF phi)) => phi ix -> HFix (PF phi) ix -> ix
+hto = unfold (const hout)
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
@@ -1,6 +1,8 @@
-{-# LANGUAGE GADTs         #-}
-{-# LANGUAGE RankNTypes    #-}
-{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances     #-}
 
 -----------------------------------------------------------------------------
 -- |
@@ -18,7 +20,7 @@
 module Generics.MultiRec.HFunctor where
 
 import Control.Monad (liftM, liftM2)
-import Control.Applicative (Applicative(..), liftA, liftA2, WrappedMonad(..))
+import Control.Applicative (Applicative(..), (<$>), (<*>), WrappedMonad(..))
 
 import Generics.MultiRec.Base
 
@@ -27,46 +29,46 @@
 -- We define a general 'hmapA' that works on applicative functors.
 -- The simpler 'hmap' is a special case.
 
-class HFunctor f where
+class HFunctor phi f where
   hmapA :: (Applicative a) =>
-           (forall ix. Ix s ix => s ix -> r ix -> a (r' ix)) ->
-           f s r ix -> a (f s r' ix)
+           (forall ix. phi ix -> r ix -> a (r' ix)) ->
+           f r ix -> a (f r' ix)
 
-instance HFunctor (I xi) where
-  hmapA f (I x) = liftA I (f index x)
+instance El phi xi => HFunctor phi (I xi) where
+  hmapA f (I x) = I <$> f proof x
 
-instance HFunctor (K x) where
-  hmapA _ (K x)  = pure (K x)
+instance HFunctor phi (K x) where
+  hmapA _ (K x) = pure (K x)
 
-instance HFunctor U where
+instance HFunctor phi U where
   hmapA _ U = pure U
 
-instance (HFunctor f, HFunctor g) => HFunctor (f :+: g) where
-  hmapA f (L x) = liftA L (hmapA f x)
-  hmapA f (R y) = liftA R (hmapA f y)
+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
 
-instance (HFunctor f, HFunctor g) => HFunctor (f :*: g) where
-  hmapA f (x :*: y) = liftA2 (:*:) (hmapA f x) (hmapA f y)
+instance (HFunctor phi f, HFunctor phi g) => HFunctor phi (f :*: g) where
+  hmapA f (x :*: y) = (:*:) <$> hmapA f x <*> hmapA f y
 
-instance HFunctor f => HFunctor (f :>: ix) where
-  hmapA f (Tag x) = liftA Tag (hmapA f x)
+instance HFunctor phi f => HFunctor phi (f :>: ix) where
+  hmapA f (Tag x) = Tag <$> hmapA f x
 
-instance HFunctor f => HFunctor (C c f) where
-  hmapA f (C x) = liftA C (hmapA f x)
+instance (Constructor c, HFunctor phi f) => HFunctor phi (C c f) where
+  hmapA f (C x) = C <$> hmapA f 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
 -- 'hmap' takes a function that transformes @r@ occurrences into @r'@
 -- occurrences, for every @ix@. In order to associate the index @ix@
--- with the correct system @s@, the argument to @hmap@ is additionally
--- parameterized by a witness of type @s ix@. 
-hmap  :: (HFunctor f) =>
-         (forall ix. Ix s ix => s ix -> r ix -> r' ix) ->
-         f s r ix -> f s r' ix
+-- with the correct family @phi@, the argument to @hmap@ is additionally
+-- 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)
 
 -- | Monadic version of 'hmap'.
-hmapM :: (HFunctor f, Monad m) =>
-         (forall ix. Ix s ix => s ix -> r ix -> m (r' ix)) ->
-         f s r ix -> m (f s r' ix)
+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)
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
@@ -1,6 +1,8 @@
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE RankNTypes       #-}
-{-# LANGUAGE TypeOperators    #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances     #-}
 
 -----------------------------------------------------------------------------
 -- |
@@ -20,56 +22,51 @@
 
 import Generics.MultiRec.Base
 import Generics.MultiRec.HFunctor
-import Generics.MultiRec.Fold
+import Generics.MultiRec.FoldK
 
 import qualified Prelude as P
 import Prelude hiding (show, showsPrec)
 
 -- * Generic show
 
-class HFunctor f => HShow f where
-  hShowsPrecAlg :: Algebra' s f (K0 [Int -> ShowS])
+class HFunctor phi f => HShow phi f where
+  hShowsPrecAlg :: Algebra' phi f [Int -> ShowS]
 
-instance HShow (I xi) where
-  hShowsPrecAlg _ (I (K0 x)) = K0 x
+instance El phi xi => HShow phi (I xi) where
+  hShowsPrecAlg _ (I (K0 x)) = x
 
 -- | For constant types, we make use of the standard
 -- show function.
-instance Show x => HShow (K x) where
-  hShowsPrecAlg _ (K x) = K0 [\ n -> P.showsPrec n x]
+instance Show a => HShow phi (K a) where
+  hShowsPrecAlg _ (K x) = [\ n -> P.showsPrec n x]
 
-instance HShow U where
-  hShowsPrecAlg _ U = K0 []
+instance HShow phi U where
+  hShowsPrecAlg _ U = []
 
-instance (HShow f, HShow g) => HShow (f :+: g) where
+instance (HShow phi f, HShow phi g) => HShow phi (f :+: g) where
   hShowsPrecAlg ix (L x) = hShowsPrecAlg ix x
   hShowsPrecAlg ix (R y) = hShowsPrecAlg ix y
 
-instance (HShow f, HShow g) => HShow (f :*: g) where
-  hShowsPrecAlg ix (x :*: y) = K0 (unK0 (hShowsPrecAlg ix x) ++ unK0 (hShowsPrecAlg ix y))
+instance (HShow phi f, HShow phi g) => HShow phi (f :*: g) where
+  hShowsPrecAlg ix (x :*: y) = hShowsPrecAlg ix x ++ hShowsPrecAlg ix y
 
-instance HShow f => HShow (f :>: ix) where
+instance HShow phi f => HShow phi (f :>: ix) where
   hShowsPrecAlg ix (Tag x) = hShowsPrecAlg ix x
 
-instance HShow f => HShow (C c f) where
+instance (Constructor c, HShow phi f) => HShow phi (C c f) where
   hShowsPrecAlg ix cx@(C x) =
     case conFixity cx of
-      Prefix    -> K0 [\ n -> showParen (not (null fields) && n > 10)
-                                        (spaces ((conName cx ++) : map ($ 11) fields))]
-      Infix a p -> K0 [\ n -> showParen (n > p)
-                                        (spaces (head fields p : (conName cx ++) : map ($ p) (tail fields)))]
+      Prefix    -> [\ n -> showParen (not (null fields) && n > 10)
+                                     (spaces ((conName cx ++) : map ($ 11) fields))]
+      Infix a p -> [\ n -> showParen (n > p)
+                                     (spaces (head fields p : (conName cx ++) : map ($ p) (tail fields)))]
    where
-    fields = unK0 $ hShowsPrecAlg ix x
-
--- | A variant of the algebra that takes an extra argument
--- to fix the system 's' the algebra works on.
-hShowsPrecAlg_ :: (HShow f) => s ix -> Algebra' s f (K0 [Int -> ShowS])
-hShowsPrecAlg_ _ = hShowsPrecAlg 
+    fields = hShowsPrecAlg ix x
 
-showsPrec :: forall s ix. (Ix s ix, HShow (PF s)) => s ix -> Int -> ix -> ShowS
-showsPrec ix n x = spaces (map ($ n) (unK0 (fold (hShowsPrecAlg_ ix) x)))
+showsPrec :: (Fam phi, HShow phi (PF phi)) => phi ix -> Int -> ix -> ShowS
+showsPrec p n x = spaces (map ($ n) (fold hShowsPrecAlg p x))
 
-show :: forall s ix. (Ix s ix, HShow (PF s)) => s ix -> ix -> String
+show :: (Fam phi, HShow phi (PF phi)) => phi ix -> ix -> String
 show ix x = showsPrec ix 0 x ""
 
 -- * Utilities
diff --git a/src/Generics/MultiRec/TEq.hs b/src/Generics/MultiRec/TEq.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/MultiRec/TEq.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE GADTs          #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeOperators  #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Generics.MultiRec.TEq
+-- Copyright   :  (c) 2008--2009 Universiteit Utrecht
+-- License     :  BSD3
+--
+-- Maintainer  :  generics@haskell.org
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Type-level equality. This module is currently provided by the multirec
+-- library, even though it is more general and does not really belong here.
+-- 
+-----------------------------------------------------------------------------
+module Generics.MultiRec.TEq where
+
+infix 4 :=:
+
+data (:=:) :: * -> * -> * where
+  Refl :: a :=: a
+
+cast :: a :=: b -> a -> b
+cast Refl x = x
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
@@ -15,16 +15,18 @@
 -- This module contains Template Haskell code that can be used to
 -- automatically generate the boilerplate code for the multiplate
 -- library. The constructor information can be generated per datatype,
--- the rest per system of datatypes.
+-- the rest per family of datatypes.
 --
 -----------------------------------------------------------------------------
 
 
 module Generics.MultiRec.TH
   ( deriveConstructors,
-    deriveSystem,
+    deriveFamily, deriveSystem,
     derivePF,
-    deriveIx
+    deriveEl,
+    deriveFam,
+    deriveEqS
   ) where
 
 import Generics.MultiRec.Base
@@ -41,20 +43,27 @@
   liftM concat . mapM constrInstance
 
 -- | Given the name of the index GADT, the names of the
--- types in the system, and the name (as string) for 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.
 
-deriveSystem :: Name -> [Name] -> String -> Q [Dec]
-deriveSystem n ns pfn =
+deriveFamily :: Name -> [Name] -> String -> Q [Dec]
+deriveFamily n ns pfn =
   do
-    pf <- derivePF pfn ns
-    ix <- deriveIx n ns
-    return $ pf ++ ix
+    pf  <- derivePF pfn ns
+    el  <- deriveEl n ns
+    fam <- deriveFam n ns
+    eq  <- deriveEqS n (map (mkName . nameBase) ns)
+    return $ pf ++ el ++ fam ++ eq
 
--- | Derive only the 'PF' instance. Not needed if 'deriveSystem'
+-- | Compatibility. Use deriveFamily instead.
+
+deriveSystem :: Name -> [Name] -> String -> Q [Dec]
+deriveSystem = deriveFamily
+
+-- | Derive only the 'PF' instance. Not needed if 'deriveFamily'
 -- is used.
 
 derivePF :: String -> [Name] -> Q [Dec]
@@ -65,13 +74,37 @@
     sum :: Q Type -> Q Type -> Q Type
     sum a b = conT ''(:+:) `appT` a `appT` b
 
--- | Derive only the 'Ix' instances. Not needed if 'deriveSystem'
+-- | Derive only the 'El' instances. Not needed if 'deriveFamily'
 -- is used.
 
-deriveIx :: Name -> [Name] -> Q [Dec]
-deriveIx s ns =
-  zipWithM (ixInstance s ns (length ns)) [0..] ns
+deriveEl :: Name -> [Name] -> Q [Dec]
+deriveEl s ns =
+  mapM (elInstance s) ns
 
+-- | Dervie only the 'Fam' instance. Not needed if 'deriveFamily'
+-- is used.
+
+deriveFam :: Name -> [Name] -> Q [Dec]
+deriveFam s ns =
+  do
+    fcs <- liftM concat $ zipWithM (mkFrom ns (length ns)) [0..] ns  
+    tcs <- liftM concat $ zipWithM (mkTo   ns (length ns)) [0..] ns
+    liftM (:[]) $
+      instanceD (cxt []) (conT ''Fam `appT` conT s)
+        [funD 'from fcs, funD 'to tcs]
+
+-- | Derive only the 'EqS' instance. Not needed if 'deriveFamily'
+-- is used.
+
+deriveEqS :: Name -> [Name] -> Q [Dec]
+deriveEqS s ns =
+    liftM (:[]) $
+    instanceD (cxt []) (conT ''EqS `appT` conT s)
+      [funD 'eqS (map trueClause ns ++ [falseClause])]
+  where
+    trueClause n = clause [conP n [], conP n []] (normalB (conE 'Just `appE` conE 'Refl)) []
+    falseClause  = clause [wildP,  wildP]        (normalB (conE 'Nothing)) []
+
 constrInstance :: Name -> Q [Dec]
 constrInstance n =
   do
@@ -149,72 +182,74 @@
 pfField ns t@(ConT n) | n `elem` ns = conT ''I `appT` return t
 pfField ns t                        = conT ''K `appT` return t
 
-ixInstance :: Name -> [Name] -> Int -> Int -> Name -> Q Dec
-ixInstance s ns m i n =
-  instanceD (cxt []) (conT ''Ix `appT` conT s `appT` conT n)
-    [mkFrom ns n m i, mkTo ns n m i, mkIndex n]
+elInstance :: Name -> Name -> Q Dec
+elInstance s n =
+  instanceD (cxt []) (conT ''El `appT` conT s `appT` conT n)
+    [mkProof n]
 
-mkFrom :: [Name] -> Name -> Int -> Int -> Q Dec
-mkFrom ns n m i =
+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 b = case i of
                 TyConI (DataD _ _ _ cs _) ->
-                  zipWith (fromCon wrapE ns (length cs)) [0..] cs
+                  zipWith (fromCon wrapE ns dn (length cs)) [0..] cs
                 TyConI (TySynD t _ _) ->
-                  [clause [varP (field 0)] (normalB (wrapE $ conE 'K `appE` varE (field 0))) []]
-                _ -> error "unknown construct" 
-      funD 'from_ b 
+                  [clause [conP dn [], varP (field 0)] (normalB (wrapE $ conE 'K `appE` varE (field 0))) []]
+                _ -> error "unknown construct"
+      return b
 
-mkTo :: [Name] -> Name -> Int -> Int -> Q Dec
-mkTo ns n m i =
+mkTo :: [Name] -> Int -> Int -> Name -> Q [Q Clause]
+mkTo ns m i n =
     do
       -- runIO $ putStrLn $ "processing " ++ show n
       let wrapP p = lrP m i (conP 'Tag [p])
       i <- reify n
+      let dn = mkName (nameBase n)
       let b = case i of
                 TyConI (DataD _ _ _ cs _) ->
-                  zipWith (toCon wrapP ns (length cs)) [0..] cs
+                  zipWith (toCon wrapP ns dn (length cs)) [0..] cs
                 TyConI (TySynD t _ _) ->
-                  [clause [wrapP $ conP 'K [varP (field 0)]] (normalB $ varE (field 0)) []]
+                  [clause [conP dn [], wrapP $ conP 'K [varP (field 0)]] (normalB $ varE (field 0)) []]
                 _ -> error "unknown construct" 
-      funD 'to_ b 
+      return b
 
-mkIndex :: Name -> Q Dec
-mkIndex n =
-  funD 'index [clause [] (normalB (conE (mkName (nameBase n)))) []]
+mkProof :: Name -> Q Dec
+mkProof n =
+  funD 'proof [clause [] (normalB (conE (mkName (nameBase n)))) []]
 
-fromCon :: (Q Exp -> Q Exp) -> [Name] -> Int -> Int -> Con -> Q Clause
-fromCon wrap ns m i (NormalC n []) =
+fromCon :: (Q Exp -> Q Exp) -> [Name] -> Name -> Int -> Int -> Con -> Q Clause
+fromCon wrap ns n m i (NormalC cn []) =
     clause
-      [conP n []]
+      [conP n [], conP cn []]
       (normalB $ wrap $ lrE m i $ conE 'C `appE` (conE 'U)) []
-fromCon wrap ns m i (NormalC n fs) =
+fromCon wrap ns n m i (NormalC cn fs) =
     -- runIO (putStrLn ("constructor " ++ show ix)) >>
     clause
-      [conP n (map (varP . field) [0..length fs - 1])]
+      [conP n [], conP cn (map (varP . field) [0..length fs - 1])]
       (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 m i (InfixC t1 n t2) =
-  fromCon wrap ns m i (NormalC n [t1,t2])
+fromCon wrap ns n m i (InfixC t1 cn t2) =
+  fromCon wrap ns n m i (NormalC cn [t1,t2])
 
-toCon :: (Q Pat -> Q Pat) -> [Name] -> Int -> Int -> Con -> Q Clause
-toCon wrap ns m i (NormalC n []) =
+toCon :: (Q Pat -> Q Pat) -> [Name] -> Name -> Int -> Int -> Con -> Q Clause
+toCon wrap ns n m i (NormalC cn []) =
     clause
-      [wrap $ lrP m i $ conP 'C [conP 'U []]]
-      (normalB $ conE n) []
-toCon wrap ns m i (NormalC n fs) =
+      [conP n [], wrap $ lrP m i $ conP 'C [conP 'U []]]
+      (normalB $ conE cn) []
+toCon wrap ns n m i (NormalC cn fs) =
     -- runIO (putStrLn ("constructor " ++ show ix)) >>
     clause
-      [wrap $ lrP m i $ conP 'C [foldr1 prod (zipWith (toField ns) [0..] (map snd fs))]]
-      (normalB $ foldl appE (conE n) (map (varE . field) [0..length fs - 1])) []
+      [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])) []
   where
     prod x y = conP '(:*:) [x,y]
-toCon wrap ns m i (InfixC t1 n t2) =
-  toCon wrap ns m i (NormalC n [t1,t2])
+toCon wrap ns n m i (InfixC t1 cn t2) =
+  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))