diff --git a/cflp.cabal b/cflp.cabal
--- a/cflp.cabal
+++ b/cflp.cabal
@@ -1,5 +1,5 @@
 Name:          cflp
-Version:       2009.1.13
+Version:       2009.1.15
 Cabal-Version: >= 1.6
 Synopsis:      Constraint Functional-Logic Programming in Haskell
 Description:   This package provides combinators for constraint
@@ -39,14 +39,16 @@
                     Data.LazyNondet.Narrowing,
                     Data.LazyNondet.Primitive,
                     Data.LazyNondet.HigherOrder,
+                    Data.LazyNondet.Generic,
                     Control.CFLP.Tests,
                     Control.CFLP.Tests.CallTimeChoice
                     Control.CFLP.Tests.HigherOrder
   Hs-Source-Dirs:   src
-  Extensions:       FunctionalDependencies,
+  Extensions:       NoMonomorphismRestriction,
                     MultiParamTypeClasses,
                     FlexibleInstances,
                     FlexibleContexts,
+                    NoMonoPatBinds,
                     PatternGuards,
                     TypeFamilies,
                     RankNTypes
diff --git a/src/Control/CFLP.lhs b/src/Control/CFLP.lhs
--- a/src/Control/CFLP.lhs
+++ b/src/Control/CFLP.lhs
@@ -25,6 +25,7 @@
 >
 > import Control.Monad.State
 > import Control.Monad.Update
+> import Control.Monad.Trans.Update
 >
 > import Control.Constraint.Choice
 >
@@ -73,13 +74,13 @@
 The `evaluate` function enumerates the non-deterministic solutions of a
 constraint functional-logic computation according to a given strategy.
 
-> eval, evalPartial :: (CFLP CS m, Update CS m m', Data a)
+> eval, evalPartial :: (CFLP CS m, Update CS m m', Generic a)
 >                   => Strategy m' -> (Context CS -> ID -> Nondet CS m a)
 >                   -> IO [a]
-> eval        s = liftM (map prim) . evaluate groundNormalForm  s
-> evalPartial s = liftM (map prim) . evaluate partialNormalForm s
+> eval        s = liftM (map primitive) . evaluate groundNormalForm  s
+> evalPartial s = liftM (map primitive) . evaluate partialNormalForm s
 >
-> evalPrint :: (CFLP CS m, Update CS m m', Data a, Show a)
+> evalPrint :: (CFLP CS m, Update CS m m', Generic a)
 >           => Strategy m' -> (Context CS -> ID -> Nondet CS m a)
 >           -> IO ()
 > evalPrint s op = evaluate partialNormalForm s op >>= printSols
diff --git a/src/Control/CFLP/Tests.lhs b/src/Control/CFLP/Tests.lhs
--- a/src/Control/CFLP/Tests.lhs
+++ b/src/Control/CFLP/Tests.lhs
@@ -11,15 +11,15 @@
 We use HUnit for testing because we need to test IO actions and want
 to use errors when testing laziness.
 
-> assertResults :: (Data a, Show a, Eq a)
+> assertResults :: (Generic a, Show a, Eq a)
 >               => (Computation [] a) -> [a] -> Assertion
 > assertResults = assertResultsLimit Nothing
 >
-> assertResultsN :: (Data a, Show a, Eq a)
+> assertResultsN :: (Generic a, Show a, Eq a)
 >                => Int -> (Computation [] a) -> [a] -> Assertion
 > assertResultsN = assertResultsLimit . Just
 >
-> assertResultsLimit :: (Data a, Show a, Eq a)
+> assertResultsLimit :: (Generic a, Show a, Eq a)
 >                    => Maybe Int -> (Computation [] a) -> [a] -> Assertion
 > assertResultsLimit limit op expected = do
 >   actual <- eval depthFirst op
diff --git a/src/Control/CFLP/Tests/CallTimeChoice.lhs b/src/Control/CFLP/Tests/CallTimeChoice.lhs
--- a/src/Control/CFLP/Tests/CallTimeChoice.lhs
+++ b/src/Control/CFLP/Tests/CallTimeChoice.lhs
@@ -47,7 +47,7 @@
 >  where
 >   comp _ = two . unknown
 >
-> two :: Monad m => Nondet cs m a -> Nondet cs m [a]
+> two :: (Monad m, Generic a) => Nondet cs m a -> Nondet cs m [a]
 > two x = x ^: x ^: nil
 
 This test checks call-time choice semantics: variables represent
diff --git a/src/Control/CFLP/Tests/HigherOrder.lhs b/src/Control/CFLP/Tests/HigherOrder.lhs
--- a/src/Control/CFLP/Tests/HigherOrder.lhs
+++ b/src/Control/CFLP/Tests/HigherOrder.lhs
@@ -58,7 +58,7 @@
 >               apply (fun two)
 >                     (apply (apply (fun (?)) false cs u1) true cs u2) cs u3
 >
-> two :: Monad m => Nondet cs m a -> Nondet cs m [a]
+> two :: (Monad m, Generic a) => Nondet cs m a -> Nondet cs m [a]
 > two x = x ^: x ^: nil
 
 The following test maps the function `not` over a list with a
diff --git a/src/Control/Monad/Update.lhs b/src/Control/Monad/Update.lhs
--- a/src/Control/Monad/Update.lhs
+++ b/src/Control/Monad/Update.lhs
@@ -2,37 +2,28 @@
 % Sebastian Fischer (sebf@informatik.uni-kiel.de)
 
 We define type classes and instances for monads that
-non-deterministically update state. The challenge is to define the
-interface such that instances can implement it without threading a
-store through monadic computations and shared monadic computations are
-evaluated only once.
+non-deterministically update state.
 
 > {-# LANGUAGE 
 >       MultiParamTypeClasses,
 >       FlexibleInstances,
->       FlexibleContexts,
 >       RankNTypes
 >   #-}
 >
 > module Control.Monad.Update (
 >
->   -- type classes
 >   MonadUpdate(..), Update(..),
 >
->   -- monad transformer
->   UpdateT
->
 > ) where
 > 
 > import Control.Monad.State
-> import Control.Monad.Trans
 >
 > class MonadPlus m => MonadUpdate s m
 >  where
 >   update :: (forall m' . MonadPlus m' => s -> m' s) -> m ()
 
 A monad that supports non-deterministic state updates is an instance
-of the class `MonadUpdate` that provides an operation to incorporate a
+of the class `MonadUpdate` that defines an operation to incorporate a
 monadic update-action into monadic computations.
 
 > instance MonadPlus m => MonadUpdate s (StateT s m)
@@ -63,91 +54,3 @@
 State monads are a natural choice for a monad that updates state, but
 they have a drawback: monadic values are functions that are reexecuted
 for each shared occurrence of a monadic sub computation.
-
-Shared Monadic Values
----------------------
-
-We define a monad transformer `UpdateT` that adds the capability of
-non-deterministic state updates to arbitrary instances of
-`MonadPlus`. Monadic actions in the resulting monads are data terms if
-monadic actions are data terms in the base monad. As a consequence,
-they are evaluated only once if they are shared.
-
-> newtype UpdateT s m a = UpdateT { unUpdateT :: m (WithUpdate s m a) }
-> data WithUpdate s m a
->   = Return a
->   | Update (forall m' . MonadPlus m' => s -> m' s)
->            (UpdateT s m a)
-
-The updating monadic action must be polymorphic in the used monad
-`m'`.
-
-> instance MonadPlus m => MonadUpdate s (UpdateT s m)
->  where
->   update upd = UpdateT (return (Update upd (return ())))
-
-A transformed instance of `MonadPlus` is an instance of `MonadUpdate`.
-
-> instance MonadPlus m => Update s (UpdateT s m) m
->  where
->   updateState = run
->    where
->     run :: MonadPlus m => UpdateT s m a -> StateT s m a
->     run x = lift (unUpdateT x) >>= doUpdate
->
->     doUpdate (Return a)     = return a
->     doUpdate (Update upd y) = do update upd; run y
-
-It is also an instance of `Update` where results are returned in the
-base monad. In order to perform stored updates, we thread a state
-through the monadic computation.
-
-> instance MonadPlus m => Update s (UpdateT s m) (UpdateT s m)
->  where
->   updateState = run
->    where
->     run :: MonadPlus m => UpdateT s m a -> StateT s (UpdateT s m) a
->     run x = lift (lift (unUpdateT x)) >>= doUpdate
->
->     doUpdate (Return a)     = return a
->     doUpdate (Update upd y) = do update upd; lift (update upd); run y
-
-We define another instance of `Update` where results are not returned
-in the base monad but in the transformed base monad. This instance is
-useful to support computations that may or may not consider the
-threaded store. All upcate actions are kept in the monadic values and
-threaded additionally.
-
-> instance Monad m => Monad (UpdateT s m)
->  where
->   return = UpdateT . return . Return
->
->   x >>= f = UpdateT (unUpdateT x >>= g)
->    where g (Return a)     = unUpdateT (f a)
->          g (Update upd y) = return (Update upd (y >>= f))
->
-> instance MonadPlus m => MonadPlus (UpdateT s m)
->  where
->   mzero       = UpdateT mzero
->   x `mplus` y = UpdateT (unUpdateT x `mplus` unUpdateT y)
->
-> instance MonadTrans (UpdateT s)
->  where
->   lift = UpdateT . liftM Return
-
-We specify that a transformed monad is indeed a monad, that it is an
-instance of `MonadPlus` if the base monad is, and that, `UpdateT`
-(with an arbitrary store `s`) is a monad transformer.
-
-> instance Show a => Show (UpdateT s [] a)
->  where
->   show (UpdateT x) = show x
->
-> instance Show a => Show (WithUpdate cs [] a)
->  where
->   show (Return x) = "(Return "++show x++")"
->   show (Update _ (UpdateT x)) = "(Update _ "++show x++")"
-
-To simplify debugging, we define `Show` instances for transformed list
-monads.
-
diff --git a/src/Data/LazyNondet.lhs b/src/Data/LazyNondet.lhs
--- a/src/Data/LazyNondet.lhs
+++ b/src/Data/LazyNondet.lhs
@@ -16,16 +16,20 @@
 >
 >   withHNF, caseOf, caseOf_, Match,
 >
->   Data, nondet, prim, groundNormalForm, partialNormalForm,
+>   Generic(..), primitive, generic, nondet,
 >
->   ConsRep(..), cons, match,
+>   Decons, ApplyCons(..), (!), cons,
 >
+>   groundNormalForm, partialNormalForm,
+>
+>   ConsPatList(..), constructors, patterns,
+>
 >   apply, fun
 >
 > ) where
 >
-> import Data.Data
 > import Data.LazyNondet.Types
+> import Data.LazyNondet.Generic
 > import Data.LazyNondet.UniqueID
 > import Data.LazyNondet.Matching
 > import Data.LazyNondet.Narrowing
diff --git a/src/Data/LazyNondet/Generic.lhs b/src/Data/LazyNondet/Generic.lhs
new file mode 100644
--- /dev/null
+++ b/src/Data/LazyNondet/Generic.lhs
@@ -0,0 +1,186 @@
+% Generic Operations on Lazy Non-Deterministic Data
+% Sebastian Fischer (sebf@informatik.uni-kiel.de)
+
+This module provides generic operations on the datatypes used
+internally for constraint functional-logic programming. We cannot use
+the `Data.Data` class, because we also want to handle functions.
+
+`Typeable` or `DrIFT` may be applicable, however, to derive some of
+the instances for classes defined in this module.
+
+> {-# LANGUAGE TypeFamilies #-}
+>
+> module Data.LazyNondet.Generic (
+>
+>   Generic(..), GenericOps, generic, primitive, nondet, consLabels,
+>
+>   ApplyCons(..), Decons, (!), cons
+>
+>  ) where
+>
+> import Data.Maybe
+> import Data.LazyNondet.Types
+
+Here is a record with generic operations:
+
+> data GenericOps a = GenericOps {
+
+The operation `gen` converts a value of type `a` into the generic
+normal-form representation.
+
+>   gen :: a -> Maybe NormalForm ,
+
+The operation `prim` converts a normal form into a primitive Haskell
+value of type `a`.
+
+>   prim :: NormalForm -> Maybe a ,
+
+The field `labels` stores a list of `ConsLabels` corresponding to the
+constructors of a datatype.
+
+>   labels :: [ConsLabel] }
+
+The generic operations `gen` and `prim` return optional
+results. However, failure is only used internally and there are
+wrapper functions that always succeed:
+
+> generic :: Generic a => a -> NormalForm
+> generic = fromJust . gen genericOps
+>
+> primitive :: Generic a => NormalForm -> a
+> primitive = fromJust . prim genericOps
+
+We also provide a generic operation `nondet` to translate instances of
+`Generic` into non-deterministic data.
+
+> nondet :: (Monad m, Generic a) => a -> Nondet cs m a
+> nondet = Typed . nf2hnf . generic
+>
+> nf2hnf :: Monad m => NormalForm -> Untyped cs m
+> nf2hnf (Var _) = error "Primitive.nf2hnf: cannot convert logic variable"
+> nf2hnf (Fun _) = error "nf2hnf: conversion of function not yet implemented"
+> nf2hnf (Data label args) = return (Cons label (map nf2hnf args))
+
+The operation `consLabels` yields the list of constructors
+corresponding to a datatype `a`.
+
+> consLabels :: Generic a => a -> [ConsLabel]
+> consLabels x = labels (genericOps `forTypeOf` x)
+>
+> forTypeOf :: GenericOps a -> a -> GenericOps a
+> forTypeOf = const
+
+The operation `genericOps` is defined in the type class `Generic`:
+
+> class Generic a
+>  where
+>   genericOps :: GenericOps a
+>   genericOps = constr 0
+>
+>   constr :: Int -> GenericOps a
+>   constr _ = error "Generic.constr: not implemented"
+
+Primitive Haskell types that should be convertible to be used in
+constraint functional-logic programs need to be instances of
+`Generic`.
+
+The operation `genericOps` has a default implementation in terms of
+`constr` to simplify the definition of instances for *data*types. The
+instance for function types defines `genericOps` directly:
+
+> instance (Generic a, Generic b) => Generic (a -> b)
+>  where
+>   genericOps = GenericOps {
+>     gen    = \ f       -> Just (Fun (generic   . f . primitive)) ,
+>     prim   = \ (Fun f) -> Just      (primitive . f . generic   ) ,
+>     labels = [] }
+
+
+Defining Instances
+==================
+
+We provide combinators to simplify the definition of `Generic`
+instances for datatypes. For example, the instance for booleans looks
+like this:
+
+> instance Generic Bool
+>  where
+>   constr = cons "False" False dFalse ! cons "True" True dTrue
+
+The arguments `dFalse` and `dTrue` are deconstructors for the
+corresponding constructors:
+
+> type Decons a = ([NormalForm] -> NormalForm) -> Result a -> Maybe NormalForm
+
+The type `Result a` used in the type of deconstructors is associated
+to the type class `ApplyCons`. 
+
+> class ApplyCons a
+>  where
+>   type Result a
+>   applyCons :: a -> [NormalForm] -> Result a
+
+We can use `applyCons` to apply constructors of arbitrary arity:
+
+> instance (Generic a, ApplyCons b) => ApplyCons (a -> b)
+>  where
+>   type Result (a -> b) = Result b
+>
+>   applyCons c (x:xs) = applyCons (c (primitive x)) xs
+>   applyCons _ _ = error "applyCons: insufficient arguments"
+
+We need an instance of `ApplyCons` for booleans in order to define the
+`Generic` instance using our combinators. Instantiating `ApplyCons` is
+easy, however. The definitions are always the same: `Result a = a` and
+`applyCons = const`.
+
+> instance ApplyCons Bool
+>  where
+>   type Result Bool = Bool
+>   applyCons = const
+
+Deconstructors are also defined mechanically:
+
+> dFalse, dTrue :: Decons Bool
+> dFalse c False = Just (c [])
+> dFalse _ _     = Nothing
+> dTrue  c True  = Just (c [])
+> dTrue  _ _     = Nothing
+
+Combinators
+-----------
+
+The combinator `(!)` used to enumerate the constructors of a datatype combines records with generic operations. The integer argument is used to label the different constructors.
+
+> infixr 0 !
+> (!) :: (Int -> GenericOps a) -> (Int -> GenericOps a) -> Int -> GenericOps a
+> (c1!c2) n =
+>   GenericOps {
+>     gen    = \x -> maybe (gen  genOps2 x) Just (gen  genOps1 x) ,
+>     prim   = \x -> maybe (prim genOps2 x) Just (prim genOps1 x) ,
+>     labels = labels genOps1 ++ labels genOps2 }
+>  where genOps1 = c1 n; genOps2 = c2 (n+1)
+
+We rely on `(!)` to be right associative: if `(!)` takes the result of
+a different call to `(!)` as left argument then the distributed
+numbers won't be distinct!
+
+Finally, we define the `cons` combinator that takes constructors and
+corresponding destructors.
+
+> cons :: ApplyCons a => String -> a -> Decons a -> Int -> GenericOps (Result a)
+> cons s c d n =
+>   GenericOps {
+>     gen    = d (Data (ConsLabel n s)),
+>     prim   = \ (Data l xs) ->
+>                  if n == index l then Just (applyCons c xs) else Nothing,
+>     labels = [ConsLabel n s]
+>    }
+
+In order to convert a value to the generic normal-form representation
+we can use the destructor function. To convert in the other direction
+we check whether the label of the constructor equals the label of the
+converter and, if it does, we use `applyCons` to apply the
+corresponding constructor.
+
+
diff --git a/src/Data/LazyNondet/HigherOrder.lhs b/src/Data/LazyNondet/HigherOrder.lhs
--- a/src/Data/LazyNondet/HigherOrder.lhs
+++ b/src/Data/LazyNondet/HigherOrder.lhs
@@ -4,10 +4,7 @@
 This module defines combinators for higher-order CFLP.
 
 > {-# LANGUAGE 
->       MultiParamTypeClasses, NoMonomorphismRestriction,
->       FunctionalDependencies,
->       TypeSynonymInstances,
->       UndecidableInstances,
+>       TypeFamilies,
 >       FlexibleInstances,
 >       FlexibleContexts
 >   #-}
@@ -46,7 +43,7 @@
 non-deterministic data (of arbitrary arity) into a (possibly nested)
 lambda.
 
-> fun :: (Monad m, LiftFun f g, NestLambda g cs m t)
+> fun :: (Monad m, LiftFun f, NestLambda g, g ~ Lift f, m~M g, cs~C g, t~T g)
 >     => f -> Nondet cs m t
 > fun = nestLambda . liftFun
 
@@ -55,21 +52,33 @@
 > newtype Lifted cs m a b
 >   = Lifted { lifted :: Nondet cs m a -> Context cs -> ID -> Nondet cs m b }
 
-> class NestLambda a cs m b | a -> cs, a -> m, a -> b
+> class NestLambda a
 >  where
->   nestLambda :: Monad m => a -> Nondet cs m b
+>   type C a :: *
+>   type M a :: * -> *
+>   type T a :: *
+>
+>   nestLambda :: Monad (M a) => a -> Nondet (C a) (M a) (T a)
 
 Single-argument functions can be lifted using `lambda`.
 
-> instance NestLambda (Lifted cs m a b) cs m (a -> b)
+> instance NestLambda (Lifted cs m a b)
 >  where
+>   type C (Lifted cs m a b) = cs
+>   type M (Lifted cs m a b) = m
+>   type T (Lifted cs m a b) = a -> b
+>
 >   nestLambda = lambda . lifted
 
 If we have a function on non-deterministic data we can lift it to the
 `Nondet` type with the following instance.
 
-> instance NestLambda f cs m b => NestLambda (Nondet cs m a -> f) cs m (a -> b)
+> instance (NestLambda f, C f ~ cs, M f ~ m) => NestLambda (Nondet cs m a -> f)
 >  where
+>   type C (Nondet cs m a -> f) = cs
+>   type M (Nondet cs m a -> f) = m
+>   type T (Nondet cs m a -> f) = a -> T f
+>
 >   nestLambda f = lambda (\x _ _ -> nestLambda (f x))
 
 We provide a combinator `liftFun` for 
@@ -81,29 +90,41 @@
 
   * non-deterministic functions that only take a unique id.
 
-> class LiftFun f g | f -> g
+> class LiftFun f
 >  where
->   liftFun :: f -> g
+>   type Lift f
 >
-> instance LiftFun (Nondet cs m a -> Nondet cs m b) (Lifted cs m a b)
+>   liftFun :: f -> Lift f
+>
+> instance LiftFun (Nondet cs m a -> Nondet cs m b)
 >  where
+>   type Lift (Nondet cs m a -> Nondet cs m b) = Lifted cs m a b
+>
 >   liftFun f = Lifted (\x _ _ -> f x)
 >
 > instance LiftFun (Nondet cs m a -> Context cs -> Nondet cs m b)
->                  (Lifted cs m a b)
 >  where
+>   type Lift (Nondet cs m a -> Context cs -> Nondet cs m b) = Lifted cs m a b
+>
 >   liftFun f = Lifted (\x cs _ -> f x cs)
 >
-> instance LiftFun (Nondet cs m a -> ID -> Nondet cs m b) (Lifted cs m a b)
+> instance LiftFun (Nondet cs m a -> ID -> Nondet cs m b)
 >  where
+>   type Lift (Nondet cs m a -> ID -> Nondet cs m b) = Lifted cs m a b
+>
 >   liftFun f = Lifted (\x _ u -> f x u)
 >
 > instance LiftFun (Nondet cs m a -> Context cs -> ID -> Nondet cs m b)
->                  (Lifted cs m a b)
 >  where
+>   type Lift (Nondet cs m a -> Context cs -> ID -> Nondet cs m b)
+>           = Lifted cs m a b
+>
 >   liftFun = Lifted
 >
-> instance LiftFun (Nondet cs m b -> f) g => 
->          LiftFun (Nondet cs m a -> Nondet cs m b -> f) (Nondet cs m a -> g)
+> instance LiftFun (Nondet cs m b -> f)
+>       => LiftFun (Nondet cs m a -> Nondet cs m b -> f)
 >  where
+>   type Lift (Nondet cs m a -> Nondet cs m b -> f)
+>           = Nondet cs m a -> Lift (Nondet cs m b -> f)
+>
 >   liftFun f = liftFun . f
diff --git a/src/Data/LazyNondet/Matching.lhs b/src/Data/LazyNondet/Matching.lhs
--- a/src/Data/LazyNondet/Matching.lhs
+++ b/src/Data/LazyNondet/Matching.lhs
@@ -5,21 +5,19 @@
 >       RankNTypes,
 >       TypeFamilies,
 >       FlexibleContexts,
->       FlexibleInstances,
->       MultiParamTypeClasses,
->       FunctionalDependencies
+>       FlexibleInstances
 >   #-}
 >
 > module Data.LazyNondet.Matching (
 >
->   Match, match, ConsRep(..), cons,
+>   Match, match, ConsPatList(..), constructors, patterns,
 >
 >   withHNF, failure, caseOf, caseOf_
 >
 > ) where
 >
-> import Data.Data
 > import Data.LazyNondet.Types
+> import Data.LazyNondet.Generic
 >
 > import Control.Monad.State
 > import Control.Monad.Update
@@ -97,13 +95,13 @@
 function to typed versions of these values.
 
 > newtype Match a cs m b
->   = Match { unMatch :: (ConIndex, Context cs -> Branch cs m b) }
+>   = Match { unMatch :: (Int, Context cs -> Branch cs m b) }
 >
 > type Branch cs m a = [Untyped cs m] -> Nondet cs m a
 >
-> match :: (ConsRep a, WithUntyped b)
->       => a -> (Context (C b) -> b) -> Match t (C b) (M b) (T b)
-> match c alt = Match (constrIndex (consRep c), withUntyped . alt)
+> match :: WithUntyped a
+>       => Int -> (Context (C a) -> a) -> Match t (C a) (M a) (T a)
+> match n alt = Match (n, withUntyped . alt)
 
 The operation `match` is used to build destructor functions for
 non-deterministic values that can be used with `caseOf`.
@@ -127,8 +125,8 @@
 >     Delayed p res
 >       | p cs      -> delayed p (\cs -> caseOf_ (Typed (res cs)) bs def cs)
 >       | otherwise -> caseOf_ (Typed (res cs)) bs def cs
->     Cons _ idx args ->
->       maybe def (\b -> b cs args) (lookup idx (map unMatch bs))
+>     Cons label args ->
+>       maybe def (\b -> b cs args) (lookup (index label) (map unMatch bs))
 >     Lambda _ -> error "Data.LazyNondet.Matching.caseOf: cannot match lambda"
 
 We provide operations `caseOf_` and `caseOf` (with and without a
@@ -139,41 +137,82 @@
 to be checked how big the slowdown of using `caseOf` is compared to
 using `withHNF` directly.
 
-> class MkCons cs m a b | b -> m, b -> cs
+> class MkCons a
 >  where
->   mkCons :: a -> [Untyped cs m] -> b
+>   type Ctx a :: *
+>   type Mon a :: * -> *
+>   type Res a :: *
 >
-> instance (Monad m, Data a) => MkCons cs m a (Nondet cs m t)
+>   mkCons :: ConsLabel -> [Untyped (Ctx a) (Mon a)] -> a
+>
+> instance Monad m => MkCons (Nondet cs m a)
 >  where
->   mkCons c = Typed . return . mkHNF (toConstr c) . reverse
+>   type Ctx (Nondet cs m a) = cs
+>   type Mon (Nondet cs m a) = m
+>   type Res (Nondet cs m a) = a
 >
-> instance MkCons cs m b c => MkCons cs m (a -> b) (Nondet cs m t -> c)
+>   mkCons l = Typed . return . Cons l . reverse
+>
+> instance (MkCons b, cs ~ Ctx b, m ~ Mon b) => MkCons (Nondet cs m a -> b)
 >  where
->   mkCons c xs x = mkCons (c undefined) (untyped x:xs)
+>   type Ctx (Nondet cs m a -> b) = cs
+>   type Mon (Nondet cs m a -> b) = m
+>   type Res (Nondet cs m a -> b) = Res b
 >
-> cons :: MkCons cs m a b => a -> b
-> cons c = mkCons c []
+>   mkCons l xs x = mkCons l (untyped x:xs)
 
-The overloaded operation `cons` takes a Haskell constructor and yields
-a corresponding constructor function for non-deterministic values.
+> infixr 0 :!
+>
+> data ConsPatList a b = a :! b
 
-> class ConsRep a
+> class ConsList a
 >  where
->   consRep :: a -> Constr
+>   type CData a
 >
-> instance ConsRep b => ConsRep (a -> b)
+>   consList :: [ConsLabel] -> a
+
+> instance ConsList ()
 >  where
->   consRep c = consRep (c undefined)
+>   type CData () = ()
+>   consList _ = ()
 
-We provide an overloaded operation `consRep` that yields a `Constr`
-representation for a constructor rather than for a constructed value
-like `Data.Data.toConstr` does. We do not provide the base instance
+> instance (MkCons a, ConsList b) => ConsList (ConsPatList a b)
+>  where
+>   type CData (ConsPatList a b) = Res a
+>
+>   consList (l:ls) = mkCons l [] :! consList ls
+>   consList _ = error "consList: insufficient cons labels"
 
-    instance Data a => ConsRep a
-     where
-      consRep = toConstr
+> constructors :: (ConsList a, Generic (CData a)) => a
+> constructors = cs
+>  where cs = consList (consLabels (undefined `asCDataOf` cs))
+>
+> asCDataOf :: ConsList a => CData a -> a -> CData a
+> asCDataOf = const
 
-because this would require to allow undecidable instances. As a
-consequence, specialized base instances need to be defined for every
-used datatype. See `Data.LazyNondet.List` for an example of how to get
-the representation of polymorphic constructors and destructors.
+> class PatternList a
+>  where
+>   type PData a
+>
+>   patternList :: [ConsLabel] -> a
+
+> instance PatternList ()
+>  where
+>   type PData () = ()
+>   patternList _ = ()
+
+> instance (WithUntyped a, PatternList p, cs ~ C a, m ~ M a, b ~ T a)
+>       => PatternList (ConsPatList ((Context cs -> a) -> Match t cs m b) p)
+>  where
+>   type PData (ConsPatList ((Context cs -> a) -> Match t cs m b) p) = t
+>
+>   patternList (l:ls) = match (index l) :! patternList ls
+>   patternList _ = error "patternList: insufficient cons labels"
+
+> patterns :: (PatternList a, Generic (PData a)) => a
+> patterns = cs
+>  where cs = patternList (consLabels (undefined `asPDataOf` cs))
+>
+> asPDataOf :: PatternList a => PData a -> a -> PData a
+> asPDataOf = const
+
diff --git a/src/Data/LazyNondet/Primitive.lhs b/src/Data/LazyNondet/Primitive.lhs
--- a/src/Data/LazyNondet/Primitive.lhs
+++ b/src/Data/LazyNondet/Primitive.lhs
@@ -7,14 +7,12 @@
 >
 > module Data.LazyNondet.Primitive (
 >
->   nondet, prim, groundNormalForm, partialNormalForm,
+>   groundNormalForm, partialNormalForm,
 >
 >   prim_eq
 >
 > ) where
 >
-> import Data.Data
-> import Data.Generics.Twins
 > import Data.LazyNondet.Types
 >
 > import Control.Monad.State
@@ -24,31 +22,7 @@
 >
 > import Data.Supply
 >
-> prim :: Data a => NormalForm -> a
-> prim (Var u) = error $ "demand on logic variable " ++ show u
-> prim (NormalForm con args) =
->   snd (gmapAccumT perkid args (fromConstr con))
->  where
->   perkid ts _ = (tail ts, prim (head ts))
 
-The operation `prim` translates a normal form into a primitive Haskell
-value. Free logic variables are translated into a call to `error` so
-the result is a partial value if the argument contains logic
-variables.
-
-> generic :: Data a => a -> NormalForm
-> generic x = NormalForm (toConstr x) (gmapQ generic x)
->
-> nf2hnf :: Monad m => NormalForm -> Untyped cs m
-> nf2hnf (Var _) = error "Primitive.nf2hnf: cannot convert logic variable"
-> nf2hnf (NormalForm con args) = return (mkHNF con (map nf2hnf args))
->
-> nondet :: (Monad m, Data a) => a -> Nondet cs m a
-> nondet = Typed . nf2hnf . generic
-
-We also provide a generic operation `nondet` to translate instances of
-the `Data` class into non-deterministic data.
-
 > groundNormalForm :: Update cs m m'
 >                  => Nondet cs m a -> Context cs -> m' NormalForm
 > groundNormalForm x (Context cs) = evalStateT (gnf (untyped x)) cs
@@ -64,15 +38,16 @@
 variables while ground normal forms are data terms.
 
 > gnf :: Update cs m m' => Untyped cs m -> StateT cs m' NormalForm
-> gnf = nf (\_ _ -> Just ()) NormalForm mkVar
+> gnf = nf (\_ _ -> Just ()) Data mkVar Fun
 >
 > mkVar :: ID -> a -> NormalForm
 > mkVar (ID us) _ = Var (supplyValue us)
 >
 > pnf :: (Update cs m m', ChoiceStore cs)
 >     => Untyped cs m -> StateT cs m' NormalForm
-> pnf x = nf lookupChoice ((return.).mkHNF) ((return.).FreeVar) x
->     >>= nf lookupChoice NormalForm mkVar
+> pnf x
+>    = nf lookupChoice ((return.).Cons) ((return.).FreeVar) (return.Lambda) x
+>  >>= nf lookupChoice Data mkVar Fun
 
 To compute ground normal forms, we ignore free variables and narrow
 them to ground terms. To compute partial normal forms, we do not
@@ -84,20 +59,21 @@
 
 > nf :: Update cs m m'
 >    => (Int -> cs -> Maybe a)
->    -> (Constr -> [nf] -> nf)
+>    -> (ConsLabel -> [nf] -> nf)
 >    -> (ID -> Untyped cs m -> nf)
+>    -> (b -> nf)
 >    -> Untyped cs m -> StateT cs m' nf
-> nf lkp cns fv x = do
+> nf lkp cns fv fun x = do
 >   hnf <- updateState x
 >   case hnf of
 >     FreeVar u@(ID us) y ->
->       get >>= maybe (return (fv u y)) (const (nf lkp cns fv y))
+>       get >>= maybe (return (fv u y)) (const (nf lkp cns fv fun y))
 >             . lkp (supplyValue us)
->     Delayed _ resume -> get >>= nf lkp cns fv . resume . Context
->     Cons typ idx args -> do
->       nfs <- mapM (nf lkp cns fv) args
->       return (cns (indexConstr typ idx) nfs)
->     Lambda _ -> error "Data.LazyNondet.Primitive.nf: cannot convert lambda"
+>     Delayed _ resume -> get >>= nf lkp cns fv fun . resume . Context
+>     Cons label args -> do
+>       nfs <- mapM (nf lkp cns fv fun) args
+>       return (cns label nfs)
+>     Lambda _ -> return . fun $ error "Data.LazyNondet.Primitive.nf: function"
 
 The `nf` function is used by all normal-form functions and performs
 all the work.
@@ -105,9 +81,9 @@
 > prim_eq :: Update cs m m
 >         => Untyped cs m -> Untyped cs m -> StateT cs m Bool
 > prim_eq x y = do
->   Cons _ ix xs <- solveCons x
->   Cons _ iy ys <- solveCons y
->   if ix==iy then all_eq xs ys else return False
+>   Cons lx xs <- solveCons x
+>   Cons ly ys <- solveCons y
+>   if index lx == index ly then all_eq xs ys else return False
 >  where
 >   all_eq [] [] = return True
 >   all_eq (v:vs) (w:ws) = do
@@ -126,6 +102,7 @@
 >   case hnf of
 >     FreeVar _ y -> solveCons y
 >     Delayed _ res -> get >>= solveCons . res . Context
+>     Lambda _ -> error "Data.LazyNondet.Primitive.solveCons: matched lambda"
 >     _ -> return hnf
 
 The function `solveCons` is like `solve` but always yields a
diff --git a/src/Data/LazyNondet/Types.lhs b/src/Data/LazyNondet/Types.lhs
--- a/src/Data/LazyNondet/Types.lhs
+++ b/src/Data/LazyNondet/Types.lhs
@@ -13,32 +13,36 @@
 >
 >   Context(..), ID(..), 
 >
->   NormalForm(..), HeadNormalForm(..), Untyped, Nondet(..),
+>   ConsLabel(..), NormalForm(..), HeadNormalForm(..), Untyped, Nondet(..),
 >
->   mkHNF, freeVar, delayed
+>   freeVar, delayed
 >
 > ) where
 >
-> import Data.Data
->
-> import Control.Monad.Update
->
 > import Data.Supply
 >
+> import Control.Monad.Trans.Update
+>
 > newtype Context cs = Context cs
 >
 > newtype ID = ID (Supply Int)
 >
-> data NormalForm = NormalForm Constr [NormalForm] | Var Int
+> data NormalForm
+>   = Data ConsLabel [NormalForm]
+>   | Var  Int
+>   | Fun  (NormalForm -> NormalForm)
+>
+> data ConsLabel = ConsLabel { index :: Int, name :: String }
+>
+> instance Show ConsLabel
+>  where
+>   showsPrec _ = (++) . name
 
 The normal form of data is represented by the type `NormalForm` which
-defines a tree of constructors and logic variables. The type `Constr`
-is a representation of constructors defined in the `Data.Generics`
-package. With generic programming we can convert between Haskell data
-types and the `NormalForm` type.
+defines a tree of constructors and logic variables or functions.
 
 > data HeadNormalForm cs m
->   = Cons DataType ConIndex [Untyped cs m]
+>   = Cons ConsLabel [Untyped cs m]
 >   | FreeVar ID (Untyped cs m)
 >   | Delayed (Context cs -> Bool) (Context cs -> Untyped cs m)
 >   | Lambda (Untyped cs m -> Context cs -> ID -> Untyped cs m)
@@ -56,13 +60,6 @@
 logic variables by overloading. The phantom type must be the Haskell
 data type that should be used for conversion into primitive data.
 
-> mkHNF :: Constr -> [Untyped cs m] -> HeadNormalForm cs m
-> mkHNF c = Cons (constrType c) (constrIndex c)
-
-In head-normal forms we split the constructor representation into a
-representation of the data type and the index of the constructor, to
-enable pattern matching on the index.
-
 Free (logic) variables are represented by `FreeVar u x` where `u` is a
 uniqe identifier and `x` represents the result of narrowing the
 variable according to the constraint store passed to the operation
@@ -95,10 +92,9 @@
 >   show (FreeVar (ID u) _) = '_':show (supplyValue u)
 >   show (Delayed _ _) = "<delayed>"
 >   show (Lambda _) = "<function>"
->   show (Cons typ idx args) 
->     | null args = show con
->     | otherwise = unwords (('(':show con):map show args++[")"])
->    where con = indexConstr typ idx
+>   show (Cons label args) 
+>     | null args = show label
+>     | otherwise = unwords (('(':show label):map show args++[")"])
 >
 > instance Show (Nondet cs [] a)
 >  where
@@ -110,12 +106,12 @@
 >
 > instance Show (HeadNormalForm cs (UpdateT cs []))
 >  where
->   show (FreeVar (ID u) _)  = '_':show (supplyValue u)
->   show (Delayed _ _)       = "<delayed>"
->   show (Lambda _)          = "<function>"
->   show (Cons typ idx [])   = show (indexConstr typ idx)
->   show (Cons typ idx args) =
->     "("++show (indexConstr typ idx)++" "++unwords (map show args)++")" 
+>   show (FreeVar (ID u) _) = '_':show (supplyValue u)
+>   show (Delayed _ _)      = "<delayed>"
+>   show (Lambda _)         = "<function>"
+>   show (Cons label [])    = show label
+>   show (Cons label args)  =
+>     "("++show label++" "++unwords (map show args)++")" 
 
 To simplify debugging, we provide `Show` instances for head-normal
 forms and non-deterministic values.
@@ -123,17 +119,18 @@
 > instance Show NormalForm
 >  where
 >   showsPrec _ (Var u) = ('_':) . shows u
->   showsPrec _ (NormalForm cons []) = shows cons
->   showsPrec n x@(NormalForm cons args)
+>   showsPrec _ (Fun _) = ("<function>"++)
+>   showsPrec _ (Data label []) = shows label
+>   showsPrec n x@(Data label args)
 >     | Just xs <- fromList x = shows xs
->     | n == 0 = shows cons . (' ':) . foldr1 (\y z -> y.(' ':).z)
+>     | n == 0 = shows label . (' ':) . foldr1 (\y z -> y.(' ':).z)
 >                 (map (showsPrec 1) args)
 >     | otherwise = ('(':) . shows x . (')':)
 >
 > fromList :: NormalForm -> Maybe [NormalForm]
-> fromList (NormalForm cons args)
->   | show cons == "[]" = Just []
->   | show cons == "(:)", [x,l] <- args, Just xs <- fromList l = Just (x:xs)
+> fromList (Data label args)
+>   | show label == "[]" = Just []
+>   | show label == "(:)", [x,l] <- args, Just xs <- fromList l = Just (x:xs)
 > fromList _ = Nothing
 
 For normal forms we provide a custum `Show` instance because we want
diff --git a/src/Data/LazyNondet/Types/Bool.lhs b/src/Data/LazyNondet/Types/Bool.lhs
--- a/src/Data/LazyNondet/Types/Bool.lhs
+++ b/src/Data/LazyNondet/Types/Bool.lhs
@@ -4,14 +4,15 @@
 This module provides non-deterministic booleans.
 
 > {-# LANGUAGE
+>       NoMonomorphismRestriction,
 >       MultiParamTypeClasses,
 >       FlexibleInstances,
->       FlexibleContexts
+>       FlexibleContexts,
+>       NoMonoPatBinds
 >   #-}
 >
 > module Data.LazyNondet.Types.Bool where
 >
-> import Data.Data
 > import Data.LazyNondet
 > import Data.LazyNondet.Types
 > import Data.LazyNondet.Primitive
@@ -20,20 +21,15 @@
 > import Control.Monad.Update
 >
 > import Control.Constraint.Choice
->
-> instance ConsRep Bool where consRep = toConstr
->
-> true :: Monad m => Nondet cs m Bool
-> true = cons True
->
-> pTrue :: (Context cs -> Nondet cs m a) -> Match Bool cs m a
-> pTrue = match True
->
-> false :: Monad m => Nondet cs m Bool
-> false = cons False
+
+Instances for the classes `ApplyCons` and `Generic` for booleans are
+defined in the module `Data.LazyNondet.Generic`.
+
+> false, true :: Monad m => Nondet cs m Bool
+> false :! true :! () = constructors
 >
-> pFalse :: (Context cs -> Nondet cs m a) -> Match Bool cs m a
-> pFalse = match False
+> pFalse, pTrue :: (Context cs -> Nondet cs m a) -> Match Bool cs m a
+> pFalse :! pTrue :! () = patterns
 
 In order to be able to use logic variables of boolean type, we make it
 an instance of the type class `Narrow`.
diff --git a/src/Data/LazyNondet/Types/List.lhs b/src/Data/LazyNondet/Types/List.lhs
--- a/src/Data/LazyNondet/Types/List.lhs
+++ b/src/Data/LazyNondet/Types/List.lhs
@@ -4,15 +4,18 @@
 This module provides non-deterministic lists.
 
 > {-# LANGUAGE
+>       NoMonomorphismRestriction,
 >       MultiParamTypeClasses,
 >       FlexibleInstances,
->       FlexibleContexts
+>       FlexibleContexts,
+>       NoMonoPatBinds,
+>       TypeFamilies
 >   #-}
 >
 > module Data.LazyNondet.Types.List where
 >
-> import Data.Data
 > import Data.LazyNondet
+> import Data.LazyNondet.Types
 > import Data.LazyNondet.Types.Bool
 >
 > import Control.Monad.Update
@@ -22,53 +25,62 @@
 > import Prelude hiding ( map, foldr )
 > import qualified Prelude as P
 >
-> instance ConsRep [()] where consRep = toConstr
+> instance ApplyCons [a] where type Result [a] = [a]; applyCons = const
 >
-> nil :: Monad m => Nondet cs m [a]
-> nil = cons ([] :: [()])
+> instance Generic a => Generic [a]
+>  where constr = cons "[]" [] dNil ! cons "(:)" (:) dCons
 >
-> pNil :: (Context cs -> Nondet cs m b) -> Match [a] cs m b
-> pNil = match ([] :: [()])
+> dNil :: Decons [a]
+> dNil c [] = Just (c [])
+> dNil _ _  = Nothing
 >
+> dCons :: Generic a => Decons [a]
+> dCons c (x:xs) = Just (c [generic x, generic xs])
+> dCons _ _      = Nothing
+>
 > infixr 5 ^:
-> (^:) :: Monad m => Nondet cs m a -> Nondet cs m [a] -> Nondet cs m [a]
-> (^:) = cons ((:) :: () -> [()] -> [()])
+> nil  :: (Monad m, Generic a) => Nondet cs m [a]
+> (^:) :: (Monad m, Generic a)
+>      => Nondet cs m a -> Nondet cs m [a] -> Nondet cs m [a]
+> nil :! (^:) :! () = constructors
 >
-> pCons :: (Context cs -> Nondet cs m a -> Nondet cs m [a] -> Nondet cs m b)
+> pNil  :: Generic a => (Context cs -> Nondet cs m b) -> Match [a] cs m b
+> pCons :: Generic a
+>       => (Context cs -> Nondet cs m a -> Nondet cs m [a] -> Nondet cs m b)
 >       -> Match [a] cs m b
-> pCons = match ((:) :: () -> [()] -> [()])
->
-> fromList :: Monad m => [Nondet cs m a] -> Nondet cs m [a]
-> fromList = P.foldr (^:) nil
+> pNil :! pCons :! () = patterns
 
 We can use logic variables of a list type if there are logic variables
 for the element type.
 
-> instance (ChoiceStore cs, Narrow cs a) => Narrow cs [a]
+> instance (ChoiceStore cs, Narrow cs a, Generic a) => Narrow cs [a]
 >  where
 >   narrow cs u = withUnique (\u1 u2 -> 
 >                   (oneOf [nil, unknown u1 ^: unknown u2] cs u)) u
 
 Some operations on lists:
 
-> null :: Update cs m m => Nondet cs m [a] -> Context cs -> Nondet cs m Bool
+> null :: (Update cs m m, Generic a)
+>      => Nondet cs m [a] -> Context cs -> Nondet cs m Bool
 > null xs = caseOf_ xs [pNil (const true)] false
 >
-> head :: Update cs m m => Nondet cs m [a] -> Context cs -> Nondet cs m a
+> head :: (Update cs m m, Generic a)
+>      => Nondet cs m [a] -> Context cs -> Nondet cs m a
 > head l = caseOf l [pCons (\_ x _ -> x)]
 >
-> tail :: Update cs m m => Nondet cs m [a] -> Context cs -> Nondet cs m [a]
+> tail :: (Update cs m m, Generic a)
+>      => Nondet cs m [a] -> Context cs -> Nondet cs m [a]
 > tail l = caseOf l [pCons (\_ _ xs -> xs)]
 
 Higher-order functions:
 
-> map :: Update cs m m
+> map :: (Update cs m m, Generic a, Generic b)
 >     => Nondet cs m (a -> b) -> Nondet cs m [a]
 >     -> Context cs -> ID -> Nondet cs m [b]
 > map f l cs = withUnique $ \u ->
 >               foldr (fun (\x xs -> apply f x cs u ^: xs)) nil l cs
 >
-> foldr :: Update cs m m
+> foldr :: (Update cs m m, Generic a)
 >       => Nondet cs m (a -> b -> b) -> Nondet cs m b -> Nondet cs m [a]
 >       -> Context cs -> ID -> Nondet cs m b
 > foldr f y l cs = withUnique $ \u1 u2 u3 ->