diff --git a/examples/GMapAssoc.hs b/examples/GMapAssoc.hs
--- a/examples/GMapAssoc.hs
+++ b/examples/GMapAssoc.hs
@@ -1,4 +1,8 @@
-{-# OPTIONS_GHC -fglasgow-exts #-}
+{-# LANGUAGE TypeOperators            #-}
+{-# LANGUAGE TypeFamilies             #-}
+{-# LANGUAGE StandaloneDeriving       #-}
+{-# LANGUAGE GADTs                    #-}
+{-# LANGUAGE FlexibleInstances        #-}
 
 module Main where
 
@@ -52,8 +56,8 @@
   insert (R a) v (GMapSum gm1 gm2)  = GMapSum gm1 (insert a v gm2)
 
 -- Uninteresting cases, but necessary
-instance (GMapKey a) => GMapKey (C c a) where
-  data GMap (C c a) v        = GMapCon (GMap a v)
+instance (GMapKey a) => GMapKey (CEq c p q a) where
+  data GMap (CEq c p q a) v  = GMapCon (GMap a v)
   empty                      = GMapCon empty
   lookup (C c) (GMapCon m)   = lookup c m
   insert (C c) v (GMapCon m) = GMapCon (insert c v m)
diff --git a/examples/Test.hs b/examples/Test.hs
--- a/examples/Test.hs
+++ b/examples/Test.hs
@@ -1,17 +1,73 @@
-{-# LANGUAGE TypeFamilies             #-}
-{-# LANGUAGE TypeOperators            #-}
-{-# LANGUAGE FlexibleInstances        #-}
-{-# LANGUAGE MultiParamTypeClasses    #-}
-{-# LANGUAGE EmptyDataDecls           #-}
-{-# LANGUAGE TemplateHaskell          #-}
-{-# LANGUAGE OverlappingInstances     #-}
+{-# LANGUAGE TypeFamilies               #-}
+{-# LANGUAGE TypeOperators              #-}
+{-# LANGUAGE FlexibleInstances          #-}
+{-# LANGUAGE FlexibleContexts           #-}
+{-# LANGUAGE MultiParamTypeClasses      #-}
+{-# LANGUAGE EmptyDataDecls             #-}
+{-# LANGUAGE TemplateHaskell            #-}
+{-# LANGUAGE OverlappingInstances       #-}
+{-# LANGUAGE UndecidableInstances       #-}
+{-# LANGUAGE GADTs                      #-}
+{-# LANGUAGE ExistentialQuantification  #-}
+{-# LANGUAGE StandaloneDeriving         #-}
 
 import Generics.Instant
 import Generics.Instant.TH
 import Generics.Instant.Functions
-import Prelude hiding (Eq, Show(..))
-import qualified Prelude as P (Show(..))
 
+--------------------------------------------------------------------------------
+-- Generic enum
+
+class GEnum a where
+  genum' :: [a]
+
+instance GEnum U where
+  genum' = [U]
+
+instance (GEnum a) => GEnum (Rec a) where
+  genum' = map Rec genum'
+
+instance (GEnum a) => GEnum (Var a) where
+  genum' = map Var genum'
+
+instance (GEnum a) => GEnum (CEq c p p a) where genum' = map C genum'
+instance              GEnum (CEq c p q a) where genum' = []
+
+instance (GEnum f, GEnum g) => GEnum (f :+: g) where
+  genum' = map L genum' ||| map R genum'
+
+instance (GEnum f, GEnum g) => GEnum (f :*: g) where
+  genum' = diag (map (\x -> map (\y -> x :*: y) genum') genum')
+
+
+instance GEnum Int where
+  genum' = [0..9]
+
+
+-- Dispatcher
+genum :: (Representable a, GEnum (Rep a)) => [a]
+genum = map to genum'
+
+
+-- Utilities
+infixr 5 |||
+
+(|||) :: [a] -> [a] -> [a]
+[]     ||| ys = ys
+(x:xs) ||| ys = x : ys ||| xs
+
+diag :: [[a]] -> [a]
+diag = concat . foldr skew [] . map (map (\x -> [x]))
+
+skew :: [[a]] -> [[a]] -> [[a]]
+skew []     ys = ys
+skew (x:xs) ys = x : combine (++) xs ys
+
+combine :: (a -> a -> a) -> [a] -> [a] -> [a]
+combine _ xs     []     = xs
+combine _ []     ys     = ys
+combine f (x:xs) (y:ys) = f x y : combine f xs ys
+
 -------------------------------------------------------------------------------
 -- Simple Datatype
 -------------------------------------------------------------------------------
@@ -38,18 +94,18 @@
 exp1 = Plus (Const 1) (Const 2)
 exp2 = Plus exp1 (Const 3)
 
-instance Eq Exp where eq' = eq
+instance GEq Exp where geq = geqDefault
 
 testExp1 :: (Bool, Bool)
-testExp1 = (eq exp2 exp2, eq exp1 exp2)
+testExp1 = (geq exp2 exp2, geq exp1 exp2)
 
 instance Empty Exp where empty' = empty
 
 testExp2 :: Exp
 testExp2 = empty
 
-instance Show Exp where show' = show
-instance P.Show Exp where show = show -- convenience
+instance GShow Exp where gshow = gshowDefault
+instance Show Exp  where show = gshow -- convenience
 
 testExp3 :: String
 testExp3 = show exp2
@@ -67,54 +123,8 @@
 data Decl = None | Seq Decl Decl | Assign String Expr
 
 data Expr = V String | Lam String Expr | App Expr Expr | Let Decl Expr
-{-
-data None
-data Seq
-data Assign
-data V
-data Lam
-data App
-data Let
 
-instance Constructor None   where conName _ = "None"
-instance Constructor Seq    where conName _ = "Seq"
-instance Constructor Assign where conName _ = "Assign"
-instance Constructor V      where conName _ = "V"
-instance Constructor Lam    where conName _ = "Lam"
-instance Constructor App    where conName _ = "App"
-instance Constructor Let    where conName _ = "Let"
-
-instance Representable Decl where
-  type Rep Decl =    C None U 
-                 :+: C Seq (Rec Decl :*: Rec Decl)
-                 :+: C Assign (Var String :*: Rec Expr)
-
-  from None         = L (C U)
-  from (Seq d1 d2)  = R (L (C (Rec d1 :*: Rec d2)))
-  from (Assign v e) = R (R (C (Var v :*: Rec e)))
-
-  to (L (C U))                       = None
-  to (R (L (C (Rec d1 :*: Rec d2)))) = Seq d1 d2
-  to (R (R (C (Var v :*: Rec e))))   = Assign v e
-
-instance Representable Expr where
-  type Rep Expr =    C V (Var String)
-                 :+: C Lam (Var String :*: Rec Expr)
-                 :+: C App (Rec Expr :*: Rec Expr)
-                 :+: C Let (Rec Decl :*: Rec Expr)
-
-  from (V x)     = L (C (Var x))
-  from (Lam v e) = R (L (C (Var v :*: Rec e)))
-  from (App f e) = R (R (L (C (Rec f :*: Rec e))))
-  from (Let d e) = R (R (R (C (Rec d :*: Rec e))))
-
-  to (L (C (Var x)))                   = V x
-  to (R (L (C (Var v :*: Rec e))))     = Lam v e
-  to (R (R (L (C (Rec f :*: Rec e))))) = App f e
-  to (R (R (R (C (Rec d :*: Rec e))))) = Let d e
--}
-
--- Using TH instead
+-- Using TH
 $(deriveAll ''Decl)
 $(deriveAll ''Expr)
 
@@ -122,10 +132,10 @@
 decls = Seq (Assign "x" (Lam "z" (V "z"))) (Assign "y" (V "x"))
 expr  = Let decls (App (V "x") (V "y"))
 
-instance Show Expr where show' = show
-instance Show Decl where show' = show
-instance P.Show Expr where show = show -- convenience
-instance P.Show Decl where show = show -- convenience
+instance GShow Expr where gshow = gshowDefault
+instance GShow Decl where gshow = gshowDefault
+instance Show Expr where show = gshow -- convenience
+instance Show Decl where show = gshow -- convenience
 
 testAST1 :: String
 testAST1 = show expr
@@ -139,11 +149,11 @@
 testAST3 :: Decl
 testAST3 = empty
 
-instance Eq Expr where eq' = eq
-instance Eq Decl where eq' = eq
+instance GEq Expr where geq = geqDefault
+instance GEq Decl where geq = geqDefault
 
 testAST4 :: Bool
-testAST4 = eq expr expr
+testAST4 = geq expr expr
 {-
 instance Update Decl where update' = update
 instance Update Expr where update' = update
@@ -155,3 +165,89 @@
 testAST6 :: Expr
 testAST6 = update expr
 -}
+
+-------------------------------------------------------------------------------
+-- Equality constraints
+-------------------------------------------------------------------------------
+
+-- Example 1
+
+-- G1 has one index
+data G1 :: * -> * where
+  G11 :: Int    -> G1 Int
+  G12 :: G1 Int -> G1 a
+
+$(deriveAll ''G1)
+
+
+-- Generic function instances
+simplInstance ''GShow ''G1 'gshow 'gshowDefault
+gadtInstance ''GEnum ''G1 'genum' 'genum
+
+-- Testing
+gshowG1 = gshow (G12 (G11 3))
+genumG1 = gshow (take 100 $ genum :: [G1 Int])
+
+
+-- Example 2: vectors
+
+-- Vec has a parameter 'a' and an index 'n'
+data Vec a :: * -> * where
+  Nil :: Vec a Ze
+  Cons :: a -> Vec a n -> Vec a (Su n)
+
+deriveAll ''Vec
+
+-- Generic function instances
+-- These are not automatically generated because of the parameter `a`
+-- The user needs to supply the instance context
+instance (GShow a) => GShow (Vec a n) where gshow = gshowDefault
+
+instance (GEnum a, GEnum (Vec a n)) => GEnum (Vec a (Su n)) where
+  genum' = genum
+
+instance (GEnum a) => GEnum (Vec a Ze) where
+  genum' = genum
+
+
+-- Testing
+gshowVec = gshow (Cons 'p' Nil)
+genumVec = gshow . take 10 $ (genum :: [Vec Int (Su (Su Ze))])
+
+
+-- Example 3: terms
+
+-- Term has one index
+data Term :: * -> * where
+  Lit    :: Int -> Term Int
+  IsZero :: Term Int -> Term Bool
+  Pair   :: Term a -> Term b -> Term (a,b)
+  If     :: Term Bool -> Term a -> Term a -> Term a
+
+deriveAll ''Term
+
+-- Generic function instances
+simplInstance ''GShow ''Term 'gshow 'gshowDefault
+gadtInstance ''GEnum ''Term 'genum' 'genum
+
+
+-- Testing
+gshowTerm = gshow (Pair (If (IsZero (Lit 1)) (Lit 2) (Lit 0)) (Lit 1))
+genumTerm = gshow (take 10 (genum :: [Term (Bool,Int)]))
+
+-- Example 4: Fin
+
+data Fin n where
+  FZe ::          Fin (Su n)
+  FSu :: Fin n -> Fin (Su n)
+
+deriveAll ''Fin
+
+simplInstance ''GShow ''Fin 'gshow 'gshowDefault
+gadtInstance  ''GEnum ''Fin 'genum' 'genum
+-- We need to give this instance manually because the index Ze is never
+-- used in the datatype definition
+instance GEnum (Fin Ze) where genum' = []
+
+gshowFin = gshow (FSu (FSu FZe))
+genumFin = gshow (take 10 (genum :: [Fin (Su (Su Ze))]))
diff --git a/instant-generics.cabal b/instant-generics.cabal
--- a/instant-generics.cabal
+++ b/instant-generics.cabal
@@ -1,11 +1,10 @@
 category:               Generics
-copyright:              (c) 2010 Universiteit Utrecht
+copyright:              (c) 2011 Universiteit Utrecht
 name:                   instant-generics
-version:                0.2.1
+version:                0.3
 license:                BSD3
 license-file:           LICENSE
-author:                 Manuel Chakravarty, Gabriel Ditu, Roman Leshchinskiy,
-                        José Pedro Magalhães
+author:                 José Pedro Magalhães
 maintainer:             generics@haskell.org
 synopsis:               Generic programming library with a sum of products view
 description:               
@@ -26,13 +25,14 @@
 build-type:             Simple
 homepage:               http://www.cs.uu.nl/wiki/GenericProgramming/InstantGenerics
 cabal-version:          >= 1.2.3
-tested-with:            GHC == 6.8.3, GHC == 6.10.4, GHC == 6.12.1, GHC == 7.0.1
+tested-with:            GHC == 6.8.3, GHC == 6.10.4, GHC == 6.12.1, GHC == 7.0.2
 extra-source-files:     examples/GMapAssoc.hs
                         examples/Test.hs
 
 library
   hs-source-dirs:         src
-  build-depends:          base >= 3.0 && < 5, template-haskell >=2.4 && <2.6
+  build-depends:          base >= 3.0 && < 5, template-haskell >=2.4 && <2.6,
+                          containers, syb
   exposed-modules:        Generics.Instant,
                           Generics.Instant.Base,
                           Generics.Instant.TH,
diff --git a/src/Generics/Instant/Base.hs b/src/Generics/Instant/Base.hs
--- a/src/Generics/Instant/Base.hs
+++ b/src/Generics/Instant/Base.hs
@@ -1,5 +1,9 @@
 {-# LANGUAGE TypeOperators            #-}
 {-# LANGUAGE TypeFamilies             #-}
+{-# LANGUAGE StandaloneDeriving       #-}
+{-# LANGUAGE GADTs                    #-}
+{-# LANGUAGE FlexibleInstances        #-}
+{-# LANGUAGE EmptyDataDecls           #-}
 
 -----------------------------------------------------------------------------
 -- |
@@ -38,28 +42,39 @@
 -----------------------------------------------------------------------------
 
 module Generics.Instant.Base (
-      U(..), (:+:)(..), (:*:)(..), C(..), Var(..), Rec(..)
+      Z, U(..), (:+:)(..), (:*:)(..), CEq(..), C, Var(..), Rec(..)
     , Constructor(..), Fixity(..), Associativity(..)
     , Representable(..)
+    , X, Ze, Su
   ) where
 
 infixr 5 :+:
 infixr 6 :*:
 
+data Z
 data U       = U              deriving (Show, Read)
 data a :+: b = L a | R b      deriving (Show, Read)
 data a :*: b = a :*: b        deriving (Show, Read)
-data C c a   = C a            deriving (Show, Read)
 data Var a   = Var a          deriving (Show, Read)
 data Rec a   = Rec a          deriving (Show, Read)
 
+data CEq c p q a where C :: a -> CEq c p p a
+deriving instance (Show a) => Show (CEq c p q a)
+deriving instance (Read a) => Read (CEq c p p a)
+
+-- Shorthand when no proofs are required
+type C c a = CEq c () () a
+
 -- | Class for datatypes that represent data constructors.
 -- For non-symbolic constructors, only 'conName' has to be defined.
 class Constructor c where
-  conName   :: t c a -> String
-  conFixity :: t c a -> Fixity
+  {-# INLINE conName #-}
+  conName   :: t c p q a -> String
+  {-# INLINE conFixity #-}
+  conFixity :: t c p q a -> Fixity
   conFixity = const Prefix
-  conIsRecord :: t c a -> Bool
+  {-# INLINE conIsRecord #-}
+  conIsRecord :: t c p q a -> Bool
   conIsRecord = const False
 
 -- | Datatype to represent the fixity of a constructor. An infix declaration
@@ -74,7 +89,9 @@
 
 class Representable a where
   type Rep a
+  {-# INLINE [1] to #-}
   to   :: Rep a -> a
+  {-# INLINE [1] from #-}
   from :: a -> Rep a
   -- defaults
   {-
@@ -82,3 +99,10 @@
   to   = id
   from = id
   -}
+
+-- Type family for representing existentially-quantified variables
+type family X c n a
+
+-- Type-level natural numbers
+data Ze :: *
+data Su :: * -> *
diff --git a/src/Generics/Instant/Functions/Empty.hs b/src/Generics/Instant/Functions/Empty.hs
--- a/src/Generics/Instant/Functions/Empty.hs
+++ b/src/Generics/Instant/Functions/Empty.hs
@@ -2,6 +2,8 @@
 {-# LANGUAGE TypeOperators            #-}
 {-# LANGUAGE FlexibleContexts         #-}
 {-# LANGUAGE OverlappingInstances     #-}
+{-# LANGUAGE FlexibleInstances        #-}
+{-# LANGUAGE GADTs                    #-}
 
 -----------------------------------------------------------------------------
 -- |
@@ -38,7 +40,7 @@
 instance (Empty a, Empty b) => Empty (a :*: b) where
   empty' = empty' :*: empty'
   
-instance (Empty a) => Empty (C c a) where
+instance (Empty a) => Empty (CEq c p p a) where
   empty' = C empty'
 
 instance (Empty a) => Empty (Var a) where
@@ -96,7 +98,7 @@
   hasRec' (L x) = hasRec' x
   hasRec' (R x) = hasRec' x
 
-instance (HasRec a) => HasRec (C c a) where
+instance (HasRec a) => HasRec (CEq c p q a) where
   hasRec' (C x) = hasRec' x
   
 instance HasRec (Rec a) where
diff --git a/src/Generics/Instant/Functions/Eq.hs b/src/Generics/Instant/Functions/Eq.hs
--- a/src/Generics/Instant/Functions/Eq.hs
+++ b/src/Generics/Instant/Functions/Eq.hs
@@ -1,11 +1,12 @@
 {-# LANGUAGE FlexibleContexts         #-}
 {-# LANGUAGE TypeOperators            #-}
 {-# LANGUAGE OverlappingInstances     #-}
+{-# LANGUAGE GADTs                    #-}
 
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Generics.Instant.Functions.Eq
--- Copyright   :  (c) 2010, Universiteit Utrecht
+-- Copyright   :  (c) 2011, Universiteit Utrecht
 -- License     :  BSD3
 --
 -- Maintainer  :  generics@haskell.org
@@ -16,51 +17,54 @@
 --
 -----------------------------------------------------------------------------
 
-module Generics.Instant.Functions.Eq (Eq(..), eq) where
+module Generics.Instant.Functions.Eq (GEq(..), geqDefault) where
 
 import Generics.Instant.Base
 import Generics.Instant.Instances ()
 
-import Prelude hiding (Eq)
 
 -- Generic eq on Representable (worker)
-class Eq a where
-  eq' :: a -> a -> Bool
+class GEq' a where
+  geq' :: a -> a -> Bool
 
-instance Eq U where
-  eq' U U = True
+instance GEq' U where
+  geq' U U = True
   
-instance (Eq a, Eq b) => Eq (a :+: b) where
-  eq' (L x) (L x') = eq' x x'
-  eq' (R x) (R x') = eq' x x'
-  eq' _      _     = False
+instance (GEq' a, GEq' b) => GEq' (a :+: b) where
+  geq' (L x) (L x') = geq' x x'
+  geq' (R x) (R x') = geq' x x'
+  geq' _      _     = False
   
-instance (Eq a, Eq b) => Eq (a :*: b) where
-  eq' (a :*: b) (a' :*: b') = eq' a a' && eq' b b'
+instance (GEq' a, GEq' b) => GEq' (a :*: b) where
+  geq' (a :*: b) (a' :*: b') = geq' a a' && geq' b b'
   
-instance (Eq a) => Eq (C c a) where
-  eq' (C a) (C a') = eq' a a'
+instance (GEq' a) => GEq' (CEq c p q a) where
+  geq' (C a) (C a') = geq' a a'
 
-instance Eq a => Eq (Var a) where
-  eq' (Var x) (Var x') = eq' x x'
+instance GEq a => GEq' (Var a) where
+  geq' (Var x) (Var x') = geq x x'
 
-instance (Eq a) => Eq (Rec a) where
-  eq' (Rec x) (Rec x') = eq' x x'
+instance (GEq a) => GEq' (Rec a) where
+  geq' (Rec x) (Rec x') = geq x x'
 
+
+class GEq a where
+  geq :: a -> a -> Bool
+
 -- Dispatcher
-eq :: (Representable a, Eq (Rep a)) => a -> a -> Bool
-eq x y = eq' (from x) (from y)
+geqDefault :: (Representable a, GEq' (Rep a)) => a -> a -> Bool
+geqDefault x y = geq' (from x) (from y)
 
 
 -- Adhoc instances
-instance Eq Int      where eq' = (==)
-instance Eq Integer  where eq' = (==)
-instance Eq Float    where eq' = (==)
-instance Eq Double   where eq' = (==)
-instance Eq Char     where eq' = (==)
-instance Eq Bool     where eq' = (==)
+instance GEq Int      where geq = (==)
+instance GEq Integer  where geq = (==)
+instance GEq Float    where geq = (==)
+instance GEq Double   where geq = (==)
+instance GEq Char     where geq = (==)
+instance GEq Bool     where geq = (==)
 
 -- Generic instances
-instance (Eq a) => Eq (Maybe a)    where eq' = eq
-instance (Eq a) => Eq [a]          where eq' = eq
-instance (Eq a, Eq b) => Eq (a, b) where eq' = eq
+instance (GEq a) => GEq (Maybe a)     where geq = geqDefault
+instance (GEq a) => GEq [a]           where geq = geqDefault
+instance (GEq a, GEq b) => GEq (a, b) where geq = geqDefault
diff --git a/src/Generics/Instant/Functions/Show.hs b/src/Generics/Instant/Functions/Show.hs
--- a/src/Generics/Instant/Functions/Show.hs
+++ b/src/Generics/Instant/Functions/Show.hs
@@ -2,11 +2,12 @@
 {-# LANGUAGE FlexibleInstances        #-}
 {-# LANGUAGE FlexibleContexts         #-}
 {-# LANGUAGE OverlappingInstances     #-}
+{-# LANGUAGE GADTs                    #-}
 
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Generics.Instant.Functions.Show
--- Copyright   :  (c) 2010, Universiteit Utrecht
+-- Copyright   :  (c) 2011, Universiteit Utrecht
 -- License     :  BSD3
 --
 -- Maintainer  :  generics@haskell.org
@@ -17,65 +18,65 @@
 --
 -----------------------------------------------------------------------------
 
-module Generics.Instant.Functions.Show (Show(..), show) where
+module Generics.Instant.Functions.Show (GShow(..), gshowDefault) where
 
 import Generics.Instant.Base
 import Generics.Instant.Instances ()
 
-import Prelude hiding (Show, show)
-import qualified Prelude as P (Show, show)
 import Data.List (intersperse)
 
 -- Generic show on Representable (worker)
-class Show a where
-  show' :: a -> String
+class GShow' a where
+  gshow' :: a -> String
 
-instance Show U where
-  show' U = ""
+instance GShow' U where
+  gshow' U = ""
   
-instance (Show a, Show b) => Show (a :+: b) where
-  show' (L x) = show' x
-  show' (R x) = show' x
+instance (GShow' a, GShow' b) => GShow' (a :+: b) where
+  gshow' (L x) = gshow' x
+  gshow' (R x) = gshow' x
   
-instance (Show a, Show b) => Show (a :*: b) where
-  show' (a :*: b) = show' a `space` show' b
+instance (GShow' a, GShow' b) => GShow' (a :*: b) where
+  gshow' (a :*: b) = gshow' a `space` gshow' b
   
-instance (Show a, Constructor c) => Show (C c a) where
-  show' c@(C a) | show' a == "" = paren $ conName c
-                | otherwise     = paren $ (conName c) `space` show' a
+instance (GShow' a, Constructor c) => GShow' (CEq c p q a) where
+  gshow' c@(C a) | gshow' a == "" = paren $ conName c
+                | otherwise     = paren $ (conName c) `space` gshow' a
 
-instance Show a => Show (Var a) where
-  show' (Var x) = show' x
+instance GShow a => GShow' (Var a) where
+  gshow' (Var x) = gshow x
 
-instance Show a => Show (Rec a) where
-  show' (Rec x) = show' x
+instance GShow a => GShow' (Rec a) where
+  gshow' (Rec x) = gshow x
 
 
+class GShow a where
+  gshow :: a -> String
+
 -- Dispatcher
-show :: (Representable a, Show (Rep a)) => a -> String
-show = show' . from
+gshowDefault :: (Representable a, GShow' (Rep a)) => a -> String
+gshowDefault = gshow' . from
 
 
 -- Adhoc instances
-instance Show Int      where show' = P.show
-instance Show Integer  where show' = P.show
-instance Show Float    where show' = P.show
-instance Show Double   where show' = P.show
-instance Show Char     where show' = P.show
-instance Show Bool     where show' = P.show
+instance GShow Int      where gshow = show
+instance GShow Integer  where gshow = show
+instance GShow Float    where gshow = show
+instance GShow Double   where gshow = show
+instance GShow Char     where gshow = show
+instance GShow Bool     where gshow = show
 
-instance Show a => Show [a] where
-  show' = concat . wrap "[" "]" . intersperse "," . map show'
+instance GShow a => GShow [a] where
+  gshow = concat . wrap "[" "]" . intersperse "," . map gshow
 
-instance Show [Char] where
-  show' = P.show
+instance GShow [Char] where gshow = show
 
-instance (Show a, Show b) => Show (a, b) where
-  show' (a,b) = "(" ++ show' a ++ "," ++ show' b ++ ")"
+instance (GShow a, GShow b) => GShow (a, b) where
+  gshow (a,b) = "(" ++ gshow a ++ "," ++ gshow b ++ ")"
 
 
 -- Generic instances
-instance (Show a) => Show (Maybe a) where show' = show
+instance (GShow a) => GShow (Maybe a) where gshow = gshowDefault
 
 
 -- Utilities
diff --git a/src/Generics/Instant/Instances.hs b/src/Generics/Instant/Instances.hs
--- a/src/Generics/Instant/Instances.hs
+++ b/src/Generics/Instant/Instances.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE EmptyDataDecls           #-}
 {-# LANGUAGE TypeOperators            #-}
 {-# LANGUAGE TypeFamilies             #-}
+{-# LANGUAGE GADTs                    #-}
 {-# OPTIONS -fno-warn-orphans         #-}
 
 -----------------------------------------------------------------------------
@@ -57,8 +58,8 @@
   to = id
   from = id
   
-instance Representable a => Representable (C c a) where 
-  type Rep (C c a) = C c a
+instance Representable a => Representable (CEq c p q a) where 
+  type Rep (CEq c p q a) = CEq c p q a
   to = id
   from = id
   
diff --git a/src/Generics/Instant/TH.hs b/src/Generics/Instant/TH.hs
--- a/src/Generics/Instant/TH.hs
+++ b/src/Generics/Instant/TH.hs
@@ -4,7 +4,7 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Generics.Instant.TH
--- Copyright   :  (c) 2010 Universiteit Utrecht
+-- Copyright   :  (c) 2011 Universiteit Utrecht
 -- License     :  BSD3
 --
 -- Maintainer  :  generics@haskell.org
@@ -18,32 +18,151 @@
 
 -- Adapted from Generics.Deriving.TH
 module Generics.Instant.TH (
+    -- * Main generator
       deriveAll
+
+    -- * Individual generators
     , deriveConstructors
     , deriveRepresentable
     , deriveRep
-    , simplInstance
+
+    -- * Utilities
+    , simplInstance, gadtInstance
+    , genRepName, typeVariables, tyVarBndrToName
   ) where
 
 import Generics.Instant.Base
+import Generics.SYB (everywhere, mkT, everything, mkQ, gshow)
 
 import Language.Haskell.TH hiding (Fixity())
-import Language.Haskell.TH.Syntax (Lift(..))
+import Language.Haskell.TH.Syntax (Lift(..), showName)
 
-import Data.List (intercalate)
+import Data.List (intercalate, nub, elemIndex)
+import qualified Data.Map as M
 import Control.Monad
+import Control.Arrow ((&&&))
 
+-- Used by gadtInstance
+data TypeArgsEqs = TypeArgsEqs { args :: [Type]        -- ^ Constructor args
+                               , vars :: [Name]        -- ^ Variables
+                               , teqs :: [(Type,Type)] -- ^ Type equalities
+                               } deriving Show
 
 -- | Given the names of a generic class, a type to instantiate, a function in
 -- the class and the default implementation, generates the code for a basic
 -- generic instance.
 simplInstance :: Name -> Name -> Name -> Name -> Q [Dec]
 simplInstance cl ty fn df = do
-  i <- reify (genRepName ty)
-  x <- newName "x"
-  fmap (: []) $ instanceD (cxt []) (conT cl `appT` conT ty)
+  i <- reify ty
+  let typ = return (foldl (\a -> AppT a . VarT . tyVarBndrToName) 
+                              (ConT ty) (typeVariables i))
+  fmap (: []) $ instanceD (cxt []) (conT cl `appT` typ)
     [funD fn [clause [] (normalB (varE df)) []]]
 
+-- | Given the names of a generic class, a GADT type to instantiate, a function
+-- in the class and the default implementation, generates the code for a basic
+-- generic instance. This is tricky in general because we have to analyze the
+-- return types of each of the GADT constructors and give instances accordingly.
+gadtInstance :: Name -> Name -> Name -> Name -> Q [Dec]
+gadtInstance cl ty fn df = do
+  i <- reify ty
+  let typ = (foldl (\a -> AppT a . VarT . tyVarBndrToName) 
+                              (ConT ty) (typeVariables i))
+
+      dt :: ([TyVarBndr],[Con])
+      dt = case i of
+             TyConI (DataD _ _ vs cs _) -> (vs, cs)
+             _ -> error ("gadtInstance: " ++ show ty ++ "is not a valid type")
+
+      -- List of index variable names
+      idxs :: [Name]
+      idxs = extractIndices (fst dt) (snd dt)
+
+      -- Get all the arguments, variables, and type equalities introduced by the
+      -- constructors
+      eqs :: [Name] -> [Con] -> [TypeArgsEqs]
+      eqs nms cs = map f cs where
+        f :: Con -> TypeArgsEqs
+        f (NormalC _ tys)    = TypeArgsEqs (map snd tys)             [] []
+        f (RecC _ tys)       = TypeArgsEqs (map (\(_,_,t) -> t) tys) [] []
+        f (InfixC t1 _ t2)   = TypeArgsEqs [snd t1, snd t2]          [] []
+        f (ForallC vs cxt c) = case f c of
+            TypeArgsEqs ts vs' eqs' -> 
+              TypeArgsEqs ts (tyVarBndrsToNames vs ++ vs') 
+                          ((concatMap g cxt) ++ eqs')
+        g :: Pred -> [(Type,Type)]
+        g (EqualP (VarT t1) t2) | t1 `elem` nms = [(VarT t1,t2)]
+                                | otherwise     = []
+        g _                                     = []
+
+      subst :: [(Type,Type)] -> Type -> Type
+      subst s = everywhere (mkT f) where
+        f (VarT a) = case lookup (VarT a) s of
+                       Nothing -> VarT a
+                       Just t  -> t
+        f x        = x
+
+      mkInst :: TypeArgsEqs -> Dec
+      mkInst t = InstanceD (map mkCxt (args t)) 
+                           (ConT cl `AppT` subst (teqs t) typ) instBody
+
+      mkCxt :: Type -> Pred
+      mkCxt = ClassP cl . (:[])
+
+      -- The instance body is empty for regular cases
+      instBody :: [Dec]
+      instBody = [FunD fn [Clause [] (NormalB (VarE df)) []]]
+
+      update :: TypeArgsEqs -> [TypeArgsEqs] -> [TypeArgsEqs]
+      -- update True  t1 [] = [t1]
+      update _  [] = []
+      update t1 (t2:ts) | teqs t1 == teqs t2 = 
+                            t2 {args = nub (args t1 ++ args t2)} : ts
+                        | otherwise          = t2 : update t1 ts
+
+      -- Types without any type equalities (not real GADTs) need to be handled
+      -- differently. Others are dealt with using filterMerge.
+      handleADTs :: ([TypeArgsEqs] -> [TypeArgsEqs]) 
+                 -> [TypeArgsEqs] -> [TypeArgsEqs]
+      handleADTs f ts | and (map (null . teqs) ts) 
+                      = [TypeArgsEqs (concatMap args ts) [] []]
+                      | otherwise = f ts                      
+
+      -- We need to
+      -- 1) ignore constructors that don't introduce any type equalities
+      -- 2) merge constructors with the same return type
+      -- This code is terribly inefficient and could easily be improved, btw.
+      filterMerge :: [TypeArgsEqs] -> [TypeArgsEqs]
+      filterMerge (t0@(TypeArgsEqs ts vs eqs):t)
+        | eqs == [] = update t0 (filterMerge t)
+        | otherwise = case filterMerge t of
+                        l -> if or (concat 
+                                  [ [ typeMatch vs (vars t2) eq1 eq2
+                                    | eq1 <- eqs, eq2 <- teqs t2 ] | t2 <- l ])
+                             then update t0 l
+                             else t0 : l
+      filterMerge [] = []
+
+      -- For (2) above, we need to consider type equality modulo
+      -- quantified-variable names
+      typeMatch :: [Name] -> [Name] -> (Type,Type) -> (Type,Type) -> Bool
+      typeMatch vs1 vs2 eq1 eq2 | length vs1 /= length vs2 = False 
+                                | otherwise 
+                                = eq1 == everywhere (mkT f) eq2
+        where f (VarT n) = case n `elemIndex` vs2 of
+                             -- is not a quantified variable
+                             Nothing -> VarT n
+                             -- it is, replace it with the equivalent var
+                             Just i  -> VarT (vs1 !! i)
+              f x        = x
+
+      allTypeArgsEqs = eqs idxs (snd dt)
+    
+      normInsts = map mkInst   (handleADTs filterMerge allTypeArgsEqs)
+
+  return $ normInsts
+
+
 -- | Given the type and the name (as string) for the type to derive,
 -- generate the 'Constructor' instances and the 'Representable' instance.
 deriveAll :: Name -> Q [Dec]
@@ -70,20 +189,28 @@
 deriveRep :: Name -> Q [Dec]
 deriveRep n = do
   i <- reify n
-  fmap (:[]) $ tySynD (genRepName n) (typeVariables i) (repType n)
 
+  let d = case i of
+            TyConI dec -> dec
+            _ -> error "unknown construct"
+  
+  exTyFamsInsts <- genExTyFamInsts d
+  fmap (: exTyFamsInsts) $ 
+    tySynD (genRepName n) (typeVariables i) (repType d (typeVariables i))
+
 deriveInst :: Name -> Q [Dec]
 deriveInst t = do
   i <- reify t
   let typ q = return $ foldl (\a -> AppT a . VarT . tyVarBndrToName) (ConT q) 
                 (typeVariables i)
+      inlPrg = pragInlD t (inlineSpecPhase True False True 1)
   fcs <- mkFrom t 1 0 t
   tcs <- mkTo   t 1 0 t
   liftM (:[]) $
     instanceD (cxt [])
       (conT ''Representable `appT` typ t)
         [ tySynInstD ''Rep [typ t] (typ (genRepName t))
-        , funD 'from fcs, funD 'to tcs]
+        , {- inlPrg, -} funD 'from fcs, funD 'to tcs]
 
 constrInstance :: Name -> Q [Dec]
 constrInstance n = do
@@ -103,6 +230,9 @@
 typeVariables (TyConI (NewtypeD _ _ tv _ _)) = tv
 typeVariables _                           = []
 
+tyVarBndrsToNames :: [TyVarBndr] -> [Name]
+tyVarBndrsToNames = map tyVarBndrToName
+
 tyVarBndrToName :: TyVarBndr -> Name
 tyVarBndrToName (PlainTV  name)   = name
 tyVarBndrToName (KindedTV name _) = name
@@ -125,6 +255,8 @@
   mkConstrData dt (stripRecordNames r)
 mkConstrData dt (InfixC t1 n t2) =
   mkConstrData dt (NormalC n [t1,t2])
+-- Contexts are ignored
+mkConstrData dt (ForallC _ _ c) = mkConstrData dt c
 
 instance Lift Fixity where
   lift Prefix      = conE 'Prefix
@@ -136,6 +268,8 @@
   lift NotAssociative   = conE 'NotAssociative
 
 mkConstrInstance :: Name -> Con -> Q Dec
+-- Contexts are ignored
+mkConstrInstance dt (ForallC _ _ c) = mkConstrInstance dt c
 mkConstrInstance dt (NormalC n _) = mkConstrInstanceWith dt n []
 mkConstrInstance dt (RecC    n _) = mkConstrInstanceWith dt n
       [ funD 'conIsRecord [clause [wildP] (normalB (conE 'True)) []]]
@@ -159,42 +293,140 @@
   instanceD (cxt []) (appT (conT ''Constructor) (conT $ genName [dt, n]))
     (funD 'conName [clause [wildP] (normalB (stringE (nameBase n))) []] : extra)
 
-repType :: Name -> Q Type
-repType n =
-    do
-      -- runIO $ putStrLn $ "processing " ++ show n
-      i <- reify n
-      let b = case i of
-                TyConI (DataD _ dt vs cs _) ->
-                  (foldr1' sum (error "Empty datatypes are not supported.")
-                    (map (repCon (dt, map tyVarBndrToName vs)) cs))
-                TyConI (NewtypeD _ dt vs c _) ->
-                  repCon (dt, map tyVarBndrToName vs) c
-                TyConI (TySynD t _ _) -> error "type synonym?" 
-                _ -> error "unknown construct" 
-      --appT b (conT $ mkName (nameBase n))
-      b where
-    sum :: Q Type -> Q Type -> Q Type
-    sum a b = conT ''(:+:) `appT` a `appT` b
+repType :: Dec -> [TyVarBndr] -> Q Type
+repType i repVs = 
+  do let sum :: Q Type -> Q Type -> Q Type
+         sum a b = conT ''(:+:) `appT` a `appT` b
+     case i of
+        (DataD _ dt vs cs _)   ->
+          (foldBal' sum (error "Empty datatypes are not supported.")
+            (map (repConGADT (dt, tyVarBndrsToNames vs) repVs 
+                   (extractIndices vs cs)) cs))
+        (NewtypeD _ dt vs c _) -> repConGADT (dt, tyVarBndrsToNames vs) repVs
+                                   (extractIndices vs [c]) c
+        (TySynD t _ _)         -> error "type synonym?" 
+        _                      -> error "unknown construct"
 
 
-repCon :: (Name, [Name]) -> Con -> Q Type
-repCon (dt, vs) (NormalC n []) =
-    conT ''C `appT` (conT $ genName [dt, n]) `appT` conT ''U
-repCon (dt, vs) (NormalC n fs) =
-    conT ''C `appT` (conT $ genName [dt, n]) `appT` 
-     (foldr1 prod (map (repField (dt, vs) . snd) fs)) where
+-- Given a datatype declaration, returns a list of its type variables which are
+-- used as index and not as data
+extractIndices :: [TyVarBndr] -> [Con] -> [Name]
+extractIndices vs = nub . everything (++) ([] `mkQ` isIndexEq) where
+  isIndexEq :: Pred -> [Name]
+  isIndexEq (EqualP (VarT a) (VarT b)) = if a `elem` tyVarBndrsToNames vs
+                                         then (a:)
+                                           (if b `elem` tyVarBndrsToNames vs
+                                           then [b] else []) else []
+  isIndexEq (EqualP (VarT a) _)        = if a `elem` tyVarBndrsToNames vs
+                                         then [a] else []
+  isIndexEq (EqualP _ (VarT a))        = if a `elem` tyVarBndrsToNames vs
+                                         then [a] else []
+  isIndexEq _                          = []
+
+repConGADT :: (Name, [Name]) -> [TyVarBndr] -> [Name] -> Con -> Q Type
+-- We only accept one index variable, for now
+repConGADT _ _ vs@(_:_:_) (ForallC _ _ _) = 
+  error ("Datatype indexed over >1 variable: " ++ show vs)
+-- Handle type equality constraints
+repConGADT d@(dt, dtVs) repVs [indexVar] (ForallC vs ctx c) = 
+  do
+     let
+        genTypeEqs ((EqualP t1 t2):r) | otherwise = case genTypeEqs r of 
+            (t1s,t2s) -> ( ConT ''(:*:) `AppT` (substTyVar vsN t1) `AppT` t1s
+                         , ConT ''(:*:) `AppT` (substTyVar vsN t2) `AppT` t2s)
+        genTypeEqs (_:r) = genTypeEqs r -- other constraints are ignored
+        genTypeEqs []    = baseEqs
+
+        substTyVar :: [Name] -> Type -> Type
+        substTyVar ns = everywhere (mkT f) where
+          f (VarT v) = case elemIndex v ns of
+                         Nothing -> VarT v
+                         Just i  -> ConT ''X 
+                                     `AppT` ConT (genName [dt,getConName c])
+                                     `AppT` int2TLNat i
+                                     `AppT` VarT indexVar
+          f x        = x
+
+        vsN :: [Name]
+        vsN = tyVarBndrsToNames vs
+
+     -- Go on with generating the representation type, taking the equalities
+     repCon (dt, dtVs) (everywhere (mkT (substTyVar vsN)) c) (genTypeEqs ctx)
+-- No constraints, go on as usual
+repConGADT d _repVs _ c = repCon d c baseEqs
+
+-- Extract the constructor name
+getConName :: Con -> Name
+getConName (NormalC n _)   = n
+getConName (RecC n _)      = n
+getConName (InfixC _ n _)  = n
+getConName (ForallC _ _ c) = getConName c
+
+-- Generate a type-level natural from an Int
+int2TLNat :: Int -> Type
+int2TLNat 0 = ConT ''Ze
+int2TLNat n = ConT ''Su `AppT` int2TLNat (n-1)
+
+-- Generate the mobility rules for the existential type families
+genExTyFamInsts :: Dec -> Q [Dec]
+genExTyFamInsts (DataD    _ n _ cs _) = fmap concat $ 
+                                          mapM (genExTyFamInsts' n) cs
+genExTyFamInsts (NewtypeD _ n _ c  _) = genExTyFamInsts' n c
+
+genExTyFamInsts' :: Name -> Con -> Q [Dec]
+genExTyFamInsts' dt (ForallC vs cxt c) = 
+  do let mR = mobilityRules (tyVarBndrsToNames vs) cxt
+         conName = ConT (genName [dt,getConName c])
+         tySynInst ty n x = TySynInstD ''X [conName, int2TLNat n, ty] x
+     return [ tySynInst ty n (VarT nm) | (n,(nm, ty)) <- zip [0..] mR ]
+genExTyFamInsts' _ _ = return []
+
+-- Compute the shape of the mobility rules
+mobilityRules :: [Name] -> Cxt -> [(Name,Type)]
+mobilityRules [] _   = []
+mobilityRules vs cxt = concat [ mobilityRules' v p | v <- vs, p <- cxt ] where
+  mobilityRules' :: Name -> Pred -> [(Name,Type)]
+  mobilityRules' _ (EqualP (VarT _) (VarT _)) = []
+  mobilityRules' v (EqualP (VarT a) x) | v `inComplex` x = [(v,x)]
+                                       | otherwise       = []
+  mobilityRules' v (EqualP x (VarT a)) = mobilityRules' v (EqualP (VarT a) x)
+  mobilityRules' v _                   = []
+
+  inComplex :: Name -> Type -> Bool
+  inComplex v (VarT _) = False
+  inComplex v x = everything (||) (False `mkQ` q) x where
+    q (VarT x) | x == v    = True
+    q (VarT x) | otherwise = False
+    q _                    = False
+
+flattenEqs :: (Type, Type) -> Q Type
+flattenEqs (t1, t2) = return t1 `appT` return t2
+
+-- () ~ ()
+baseEqs :: (Type, Type)
+baseEqs = (TupleT 0, TupleT 0)
+
+repCon :: (Name, [Name]) -> Con -> (Type,Type) -> Q Type
+repCon _ (ForallC _ _ _) _ = error "impossible"
+repCon (dt, vs) (NormalC n []) (t1,t2) =
+    conT ''CEq `appT` (conT $ genName [dt, n]) `appT` return t1 
+                                               `appT` return t2 `appT` conT ''U
+repCon (dt, vs) (NormalC n fs) (t1,t2) =
+    conT ''CEq `appT` (conT $ genName [dt, n]) `appT` return t1 
+                                               `appT` return t2 `appT` 
+     (foldBal prod (map (repField (dt, vs) . snd) fs)) where
     prod :: Q Type -> Q Type -> Q Type
     prod a b = conT ''(:*:) `appT` a `appT` b
-repCon (dt, vs) r@(RecC n []) =
-    conT ''C `appT` (conT $ genName [dt, n]) `appT` conT ''U
-repCon (dt, vs) r@(RecC n fs) =
-    conT ''C `appT` (conT $ genName [dt, n]) `appT` 
-      (foldr1 prod (map (repField' (dt, vs) n) fs)) where
+repCon (dt, vs) r@(RecC n []) (t1,t2)  =
+    conT ''CEq `appT` (conT $ genName [dt, n]) `appT` return t1
+                                               `appT` return t2 `appT` conT ''U
+repCon (dt, vs) r@(RecC n fs) (t1,t2) =
+    conT ''CEq `appT` (conT $ genName [dt, n]) `appT` return t1 
+                                               `appT` return t2 `appT` 
+      (foldBal prod (map (repField' (dt, vs) n) fs)) where
     prod :: Q Type -> Q Type -> Q Type
     prod a b = conT ''(:*:) `appT` a `appT` b
-
-repCon d (InfixC t1 n t2) = repCon d (NormalC n [t1,t2])
+repCon d (InfixC t1 n t2) eqs = repCon d (NormalC n [t1,t2]) eqs
 
 --dataDeclToType :: (Name, [Name]) -> Type
 --dataDeclToType (dt, vs) = foldl (\a b -> AppT a (VarT b)) (ConT dt) vs
@@ -213,12 +445,12 @@
 mkFrom ns m i n =
     do
       -- runIO $ putStrLn $ "processing " ++ show n
-      let wrapE e = lrE m i e
+      let wrapE e = e -- lrE m i e
       i <- reify n
       let b = case i of
                 TyConI (DataD _ dt vs cs _) ->
                   zipWith (fromCon wrapE ns (dt, map tyVarBndrToName vs)
-                    (length cs)) [0..] cs
+                    (length cs)) [1..] cs
                 TyConI (NewtypeD _ dt vs c _) ->
                   [fromCon wrapE ns (dt, map tyVarBndrToName vs) 1 0 c]
                 TyConI (TySynD t _ _) -> error "type synonym?" 
@@ -230,12 +462,12 @@
 mkTo ns m i n =
     do
       -- runIO $ putStrLn $ "processing " ++ show n
-      let wrapP p = lrP m i p
+      let wrapP p = p -- lrP m i p
       i <- reify n
       let b = case i of
                 TyConI (DataD _ dt vs cs _) ->
                   zipWith (toCon wrapP ns (dt, map tyVarBndrToName vs)
-                    (length cs)) [0..] cs
+                    (length cs)) [1..] cs
                 TyConI (NewtypeD _ dt vs c _) ->
                   [toCon wrapP ns (dt, map tyVarBndrToName vs) 1 0 c]
                 TyConI (TySynD t _ _) -> error "type synonym?" 
@@ -244,6 +476,8 @@
       return b
 
 fromCon :: (Q Exp -> Q Exp) -> Name -> (Name, [Name]) -> Int -> Int -> Con -> Q Clause
+-- Contexts are ignored
+fromCon wrap ns d m i (ForallC _ _ c) = fromCon wrap ns d m i c
 fromCon wrap ns (dt, vs) m i (NormalC cn []) =
   clause
     [conP cn []]
@@ -253,7 +487,7 @@
   clause
     [conP cn (map (varP . field) [0..length fs - 1])]
     (normalB $ wrap $ lrE m i $ conE 'C `appE` 
-      foldr1 prod (zipWith (fromField (dt, vs)) [0..] (map snd fs))) []
+      foldBal prod (zipWith (fromField (dt, vs)) [0..] (map snd fs))) []
   where prod x y = conE '(:*:) `appE` x `appE` y
 fromCon wrap ns (dt, vs) m i r@(RecC cn []) =
   clause
@@ -263,7 +497,7 @@
   clause
     [conP cn (map (varP . field) [0..length fs - 1])]
     (normalB $ wrap $ lrE m i $ conE 'C `appE` 
-      foldr1 prod (zipWith (fromField (dt, vs)) [0..] (map trd fs))) []
+      foldBal prod (zipWith (fromField (dt, vs)) [0..] (map trd fs))) []
   where prod x y = conE '(:*:) `appE` x `appE` y
 fromCon wrap ns (dt, vs) m i (InfixC t1 cn t2) =
   fromCon wrap ns (dt, vs) m i (NormalC cn [t1,t2])
@@ -273,6 +507,8 @@
 fromField (dt, vs) nr t = conE 'Rec `appE` varE (field nr)
 
 toCon :: (Q Pat -> Q Pat) -> Name -> (Name, [Name]) -> Int -> Int -> Con -> Q Clause
+-- Contexts are ignored
+toCon wrap ns d m i (ForallC _ _ c) = toCon wrap ns d m i c
 toCon wrap ns (dt, vs) m i (NormalC cn []) =
     clause
       [wrap $ lrP m i $ conP 'C [conP 'U []]]
@@ -281,7 +517,7 @@
     -- runIO (putStrLn ("constructor " ++ show ix)) >>
     clause
       [wrap $ lrP m i $ conP 'C
-        [foldr1 prod (zipWith (toField (dt, vs)) [0..] (map snd fs))]]
+        [foldBal prod (zipWith (toField (dt, vs)) [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 (dt, vs) m i r@(RecC cn []) =
@@ -291,7 +527,7 @@
 toCon wrap ns (dt, vs) m i r@(RecC cn fs) =
     clause
       [wrap $ lrP m i $ conP 'C
-        [foldr1 prod (zipWith (toField (dt, vs)) [0..] (map trd fs))]]
+        [foldBal prod (zipWith (toField (dt, vs)) [0..] (map trd fs))]]
       (normalB $ foldl appE (conE cn) (map (varE . field) [0..length fs - 1])) []
   where prod x y = conP '(:*:) [x,y]
 toCon wrap ns (dt, vs) m i (InfixC t1 cn t2) =
@@ -306,14 +542,26 @@
 field n = mkName $ "f" ++ show n
 
 lrP :: Int -> Int -> (Q Pat -> Q Pat)
+{-
 lrP 1 0 p = p
 lrP m 0 p = conP 'L [p]
 lrP m i p = conP 'R [lrP (m-1) (i-1) p]
+-}
+lrP m i p | m == 0       = error "1"
+          | m == 1       = p
+          | i <= div m 2 = conP 'L [lrP (div m 2)     i             p]
+          | i >  div m 2 = conP 'R [lrP (m - div m 2) (i - div m 2) p]
 
 lrE :: Int -> Int -> (Q Exp -> Q Exp)
+{-
 lrE 1 0 e = e
 lrE m 0 e = conE 'L `appE` e
 lrE m i e = conE 'R `appE` lrE (m-1) (i-1) e
+-}
+lrE m i e | m == 0       = error "2"
+          | m == 1       = e
+          | i <= div m 2 = conE 'L `appE` lrE (div m 2)     i         e
+          | i >  div m 2 = conE 'R `appE` lrE (m - div m 2) (i - div m 2) e
 
 trd (_,_,c) = c
 
@@ -321,3 +569,13 @@
 foldr1' f x [] = x
 foldr1' _ _ [x] = x
 foldr1' f x (h:t) = f h (foldr1' f x t)
+
+-- | Variant of foldr1 for producing balanced lists
+foldBal :: (a -> a -> a) -> [a] -> a
+foldBal op = foldBal' op (error "foldBal: empty list")
+
+foldBal' :: (a -> a -> a) -> a -> [a] -> a
+foldBal' _  x []  = x
+foldBal' _  _ [y] = y
+foldBal' op x l   = let (a,b) = splitAt (length l `div` 2) l
+                    in foldBal' op x a `op` foldBal' op x b