diff --git a/benchmark/DataTypes/Comp.hs b/benchmark/DataTypes/Comp.hs
--- a/benchmark/DataTypes/Comp.hs
+++ b/benchmark/DataTypes/Comp.hs
@@ -20,9 +20,8 @@
 import Data.Comp
 import Data.Comp.Ops
 import Data.Comp.Arbitrary ()
-import Data.Comp.Show
+import Data.Comp.Show ()
 import Data.Traversable
-import Test.QuickCheck.Arbitrary
 import Test.QuickCheck.Gen
 import Test.QuickCheck.Property
 
diff --git a/benchmark/Functions/Comp/Eval.hs b/benchmark/Functions/Comp/Eval.hs
--- a/benchmark/Functions/Comp/Eval.hs
+++ b/benchmark/Functions/Comp/Eval.hs
@@ -14,11 +14,9 @@
 import DataTypes.Comp
 import Functions.Comp.Desugar
 import Data.Comp
-import Data.Comp.Ops
 import Data.Comp.Thunk hiding (eval, eval2)
 import Data.Comp.Derive
 import Control.Monad
-import Data.Traversable
 
 -- evaluation with thunks
 
@@ -30,8 +28,8 @@
 
 $(derive [liftSum] [''EvalT])
 
-instance (Monad m, Traversable v, Value :<: v) => EvalT Value v m where
-    evalTAlg = injectT
+instance (Monad m, Traversable v, Value :<: m :+: v) => EvalT Value v m where
+    evalTAlg = inject
 
 instance (Value :<: (m :+: v), Value :<: v, Traversable v, EqF v, Monad m) => EvalT Op v m where
     evalTAlg (Plus x y) = thunk $ do
diff --git a/compdata.cabal b/compdata.cabal
--- a/compdata.cabal
+++ b/compdata.cabal
@@ -1,5 +1,5 @@
 Name:			compdata
-Version:		0.8.0.1
+Version:		0.8.1.0
 Synopsis:            	Compositional Data Types
 Description:
 
@@ -166,7 +166,6 @@
                         Data.Comp.Derive.SmartAConstructors
                         Data.Comp.Derive.Foldable
                         Data.Comp.Derive.Traversable
-                        Data.Comp.Derive.Projections
                         Data.Comp.Derive.HaskellStrict
                         Data.Comp.Automata.Product.Derive
 
@@ -178,8 +177,6 @@
                         Data.Comp.Multi.Derive.Show
                         Data.Comp.Multi.Derive.SmartConstructors
                         Data.Comp.Multi.Derive.SmartAConstructors
-                        Data.Comp.Multi.Derive.Injections
-                        Data.Comp.Multi.Derive.Projections
 
   Build-Depends:	base >= 4.7, base < 5, template-haskell, containers, mtl, QuickCheck >= 2, derive,
                         deepseq, th-expand-syns, transformers, tree-view
diff --git a/examples/Examples/Automata/Compiler.hs b/examples/Examples/Automata/Compiler.hs
--- a/examples/Examples/Automata/Compiler.hs
+++ b/examples/Examples/Automata/Compiler.hs
@@ -1,7 +1,7 @@
 {-# LANGUAGE TemplateHaskell, FlexibleContexts, MultiParamTypeClasses,
 TypeOperators, FlexibleInstances, UndecidableInstances,
 ScopedTypeVariables, TypeSynonymInstances, GeneralizedNewtypeDeriving,
-OverlappingInstances #-}
+OverlappingInstances, ConstraintKinds #-}
 
 module Examples.Automata.Compiler where
 
diff --git a/examples/Examples/Automata/MHom.hs b/examples/Examples/Automata/MHom.hs
deleted file mode 100644
--- a/examples/Examples/Automata/MHom.hs
+++ /dev/null
@@ -1,229 +0,0 @@
-{-# LANGUAGE RankNTypes, MultiParamTypeClasses, FlexibleInstances,
-  FlexibleContexts, UndecidableInstances, TypeOperators,
-  ImplicitParams, GADTs, IncoherentInstances, ScopedTypeVariables,
-  TupleSections #-}
---------------------------------------------------------------------------------
--- |
--- Module      :  Examples.MHom
--- Copyright   :  (c) 2011 Patrick Bahr
--- License     :  BSD3
--- Maintainer  :  Patrick Bahr <paba@diku.dk>
--- Stability   :  experimental
--- Portability :  non-portable (GHC Extensions)
---
---
---------------------------------------------------------------------------------
-
-module Examples.Automata.MHom
-    ( module Examples.Automata.MHom
-    , module Data.Stream ) where
-
-import Data.Comp.Zippable
-import Data.Comp
-import Data.Comp.Ops
-import Data.Stream (Stream(..), (<:>))
-import Data.Comp.Show ()
-import Data.Map (Map)
-import qualified Data.Map as Map
-import Control.Monad
-import Control.Arrow (first, (&&&))
-import Data.Comp.Derive
-
--- | An instance @a :< b@ means that @a@ is a component of @b@. @a@
--- can be extracted from @b@ via the method 'ex'.
-class p :< q where
-    pr :: q a -> p a
-    up :: p a -> q a -> q a
-
-instance q :< q where
-    pr = id
-    up = const
-
-instance p :< p :*: q where
-    pr = ffst
-    up x (_ :*: y) = x :*: y
-
-instance (p :< q) => p :< (p' :*: q) where
-    pr = pr . fsnd
-    up  y (x :*: y') = x :*: up y y'
-
--- | This function provides access to components of the states from
--- "below".
-below :: (?below :: i -> q a, p :< q) => i -> p a
-below = pr . ?below
-
--- | This function provides access to components of the state from
--- "above"
-above :: (?above :: q a, p :< q) => p a
-above = pr ?above
-
-hole :: (?get :: i -> a) => i -> Context f a
-hole = Hole . ?get
-
--- | Turns the explicit parameters @?above@ and @?below@ into explicit
--- ones.
-explicit :: q a -> (i -> q a) -> (i -> a)
-         -> ((?get :: i -> a, ?below :: i -> q a, ?above :: q a) => b) -> b
-explicit ab bel get x = x
-    where ?above = ab
-          ?below = bel
-          ?get = get
--- | This type represents generalised term homomorphisms. Generalised
--- term homomorphisms have access to a state that is provided
--- (separately) by a DUTA or a DDTA (or both).
-type MHom q f g = forall a i . (?get :: i -> a, ?below :: i -> q a, ?above :: q a)
-    => f i -> Context g a
-
-
--- | This type represents transition functions of deterministic
--- bottom-up tree transducers (DUTTs).
-
-type UpTrans q f g = forall a. f (q a,a) -> (q (Context g a), Context g a)
-
--- | This function transforms DUTT transition function into an
--- algebra.
-upAlg :: (Functor g, Functor q)  => UpTrans q f g -> Alg f (q (Term g), Term g)
-upAlg trans t = let (q , c) = trans t
-                in (fmap appCxt q, appCxt c)
-
-
--- | This function runs the given DUTT on the given term.
-
-runUpTrans :: (Functor f, Functor g, Functor q) => UpTrans q f g -> Term f -> (q (Term g), Term g)
-runUpTrans = cata . upAlg
-
--- | This function generalises 'runUpTrans' to contexts. Therefore,
--- additionally, a transition function for the holes is needed.
-runUpTrans' :: (Functor f, Functor g, Functor q)
-            => UpTrans q f g -> Context f (q a,a) -> (q (Context g a), Context g a)
-runUpTrans' trans = run where
-    run (Hole (q,a)) = (fmap Hole q, Hole a)
-    run (Term t) = let (q, c) = trans $ fmap run t
-                   in (fmap appCxt q, appCxt c)
-
--- | This function composes two DUTTs. (I'm not sure whether it is correct, yet.)
-compUpTrans :: (Functor f, Functor g, Functor h, Functor q1, Functor q2)
-               => UpTrans q2 g h -> UpTrans q1 f g -> UpTrans (q1 :*: q2) f h
-compUpTrans t2 t1 x = (q1' :*: q2, c2) where
-    (q1, c1) = t1 $ fmap shuffle  x
-    shuffle (q1 :*: q2,a) = (fmap (q2,) q1 ,(q2,a) )
-    q1' = fmap (snd . runUpTrans' t2) q1
-    (q2, c2) = runUpTrans' t2 c1
-
--- | This type represents transition functions of deterministic
--- bottom-up tree acceptors (DUTAs).
-type UpState f q = forall a . f (q a, a) -> q a
-
--- | This combinator runs the given DUTA on a term returning the final
--- state of the run.
-runUpState :: (Functor f) => UpState f q -> Term f -> q (Term f)
-runUpState st = run where
-    run (Term t) = st $ fmap (\ s -> (run s, s)) t
-
-
--- | This function combines the product DUTA of the two given DUTAs.
-prodUpState :: Functor f => UpState f p -> UpState f q -> UpState f (p :*:q)
-prodUpState sp sq t = p :*: q where
-    p = sp $ fmap (first ffst) t
-    q = sq $ fmap (first fsnd) t
-
--- | This function turns constructs a DUTT from a given macro term
--- homomorphism with the state propagated by the given DUTA.
-toUpTrans :: (Functor f, Functor g, Functor q)
-          => UpState f q -> MHom q f g -> UpTrans q f g
-toUpTrans st f t = (fmap Hole q, c)
-    where q = st t
-          c = explicit q (pr . fst) snd f t
-
--- | This function applies a given generalised term homomorphism with
--- a state space propagated by the given DUTA to a term.
-upHom :: (Functor f, Functor g, Functor q) => UpState f q -> MHom q f g -> Term f -> (q (Term g),Term g)
-upHom alg h = runUpTrans (toUpTrans alg h)
-
--- | This type represents transition functions of generalised
--- deterministic bottom-up tree acceptors (GDUTAs) which have access
--- to an extended state space.
-type GUpState f q p = forall a i . (?get :: i -> a, ?below :: i -> p a, ?above :: p a, q :< p) => f i -> q a
-
--- | This combinator turns an arbitrary DUTA into a GDUTA.
-gUpState :: Functor f => UpState f q -> GUpState f q p
-gUpState f = f . fmap (below &&& (?get))
-
--- | This combinator turns a GDUTA with the smallest possible state
--- space into a DUTA.
-upState :: GUpState f q q -> UpState f q
-upState f s = let res = explicit res fst snd f s in res
-
--- | This combinator runs a GDUTA on a term.
-runGUpState :: Functor f => GUpState f q q -> Term f -> q (Term f)
-runGUpState s = runUpState (upState s)
-
--- | This combinator constructs the product of two GDUTA.
-prodGUpState :: (p :< pq, q :< pq)
-             => GUpState f p pq -> GUpState f q pq -> GUpState f (p :*: q) pq
-prodGUpState sp sq t = sp t :*: sq t
-
--- | This type represents transition functions of deterministic
--- top-down tree transducers (DDTTs).
-
-type DownTrans q f g = forall a. (q a, f a) -> Context g (q (Context f a),a)
-
--- | This function runs the given DDTT on the given tree.
-runDownTrans :: (Functor f, Functor g, Functor q) => DownTrans q f g -> q (Cxt h g a) -> Cxt h f a -> Cxt h g a
-runDownTrans tr q t = run (q,t) where
-    run (q,Term t) = appCxt $ fmap (\(q,a) -> run (fmap appCxt q,a)) $  tr (q, t)
-    run (_,Hole a) = Hole a
-
--- | This function runs the given DDTT on the given tree.
-runDownTrans' :: (Functor f, Functor g, Functor q) => DownTrans q f g -> q (Cxt h f a)
-              -> Cxt h f a -> Cxt h g (q (Cxt h f a),a)
-runDownTrans' tr q t = run (q,t) where
-    run (q,Term t) = appCxt $ fmap (\(q,a) -> run (fmap appCxt q,a)) $  tr (q, t)
-    run (q,Hole a)      = Hole (q,a)
-
--- | This function composes two DDTTs. (not implemented yet)
-compDownTrans :: (Functor f, Functor g, Functor h)
-              => DownTrans p g h -> DownTrans q f g -> DownTrans (q :*:p) f h
-compDownTrans = undefined
-
--- | This type represents transition functions of deterministic
--- top-down tree acceptors (DDTAs).
-type DownState f q = forall a i. Ord i => (q a, f (i,a)) -> Map i (q a)
-
--- | This function constructs the product DDTA of the given two DDTAs.
-prodDownState :: DownState f p -> DownState f q -> DownState f (p :*: q)
-prodDownState sp sq (p :*: q,t) = prodMap p q (sp (p, t)) (sq (q, t))
-
-
-
--- | This type is needed to construct the product of two DDTAs.
-data ProdState p q = LState p
-                   | RState q
-                   | BState p q
--- | This function constructs the pointwise product of two maps each
--- with a default value.
-prodMap :: (Ord i) => p a -> q a -> Map i (p a) -> Map i (q a) -> Map i ((p :*: q) a)
-prodMap p q mp mq = Map.map final $ Map.unionWith combine ps qs
-    where ps = Map.map LState mp
-          qs = Map.map RState mq
-          combine (LState p) (RState q) = BState p q
-          combine (RState q) (LState p) = BState p q
-          combine _ _                   = error "unexpected merging"
-          final (LState p) = p :*: q
-          final (RState q) = p :*: q
-          final (BState p q) = p :*: q
-
--- | Apply the given state mapping to the given functorial value by
--- adding the state to the corresponding index if it is in the map and
--- otherwise adding the provided default state.
-appMap :: Zippable f => DownState f q -> q a -> f a -> f (q a,a)
-appMap qmap q s = fmap qfun s'
-    where s' = number' s
-          mapping  = qmap (q,s')
-          qfun (k,a) = (Map.findWithDefault q k mapping ,a)
-
--- -- | This function constructs a DDTT from a given stateful term
--- -- homomorphism with the state propagated by the given DDTA.
--- toDownTrans :: (Zippable f, Functor q) => DownState f q -> MHom q f g -> DownTrans q f g
--- toDownTrans st f (q, s) = fmap mkQCxt $ explicit q fst id f (appMap st q s)
---     where mkQCxt (q,a) = (fmap Hole q, a)
diff --git a/examples/Examples/Automata/SimpComp.hs b/examples/Examples/Automata/SimpComp.hs
deleted file mode 100644
--- a/examples/Examples/Automata/SimpComp.hs
+++ /dev/null
@@ -1,79 +0,0 @@
-{-# LANGUAGE TemplateHaskell, FlexibleContexts, MultiParamTypeClasses,
-  TypeOperators, FlexibleInstances, UndecidableInstances,
-  ScopedTypeVariables, TypeSynonymInstances, RankNTypes #-}
-
-module Examples.Automata.Compiler where
-
-
-import Data.Comp.Automata hiding (DUpState, (<*>), runDUpState, dUpState)
-import Data.Comp.Zippable
-import Data.Comp.Derive
-import Data.Comp.Ops
-import Data.Comp hiding (height)
-import Prelude hiding (foldl)
-
-
-
-type Var = String
-
-data Sig a = Const Int | Plus a a
-data Let a = Let Var a a
-           | Var Var
-
-
-$(derive [makeFunctor, makeFoldable, smartConstructors, makeShowF] [''Sig, ''Let])
-
-instance Zippable Sig where
-    fzip _ (Const i) = Const i
-    fzip (Cons a (Cons b _)) (Plus x y) = Plus (a,x) (b,y)
-
-instance Zippable Let where
-    fzip (Cons a (Cons b _)) (Let v x y) = Let v (a,x) (b,y)
-    fzip _ (Var v) = Var v
-
-
-instance (Zippable f, Zippable g) => Zippable (f :+: g) where
-    fzip x (Inl v) = Inl $ fzip x v
-    fzip x (Inr v) = Inr $ fzip x v
-
-evalSt :: UpState Sig Int
-evalSt (Const i) = i
-evalSt (Plus x y) = x + y
-
-type Addr = Int
-
-data Instr = Acc Int
-           | Load Addr
-           | Store Addr
-           | Add Addr
-             deriving (Show)
-
-type Code = [Instr]
-
-
-
-type DUpState f q p = (q :< p) => f p -> q
-
-dUpState :: Functor f => UpState f q -> DUpState f q p
-dUpState st = st . fmap pr
-
-
-heightSt :: UpState Sig Int
-heightSt (Const _) = 0
-heightSt (Plus x y) = 1 + max x y
-
-codeSt :: (Int :< q) => DUpState Sig Code q
-codeSt (Const x) = [Acc x]
-codeSt (Plus x y) = pr x ++ [Store a] ++ pr y ++ [Add a] where a = pr y
-
--- | This combinator constructs the product of two GDUTA.
-(<*>) :: (p :< pq, q :< pq)
-             => DUpState f p pq -> DUpState f q pq -> DUpState f (p,q) pq
-(sp <*> sq) t = (sp t, sq t)
-    
-runDUpState :: Functor f => DUpState f q q -> Term f -> q
-runDUpState = cata
-
-code :: Term Sig -> Code
-code = fst . runDUpState (codeSt <*> dUpState heightSt)
- 
diff --git a/examples/Examples/Automata/SimpComp2.hs b/examples/Examples/Automata/SimpComp2.hs
deleted file mode 100644
--- a/examples/Examples/Automata/SimpComp2.hs
+++ /dev/null
@@ -1,153 +0,0 @@
-{-# LANGUAGE TemplateHaskell, FlexibleContexts, MultiParamTypeClasses,
-  TypeOperators, FlexibleInstances, UndecidableInstances,
-  ScopedTypeVariables, TypeSynonymInstances, RankNTypes, ImplicitParams, DeriveDataTypeable #-}
-
-module Examples.Automata.Compiler where
-
-import Data.Comp.Automata
-import Data.Comp.Zippable
-import Data.Comp.Derive
-import Data.Comp.Ops
-import Data.Comp hiding (height)
-import Data.Foldable
-import Prelude hiding (foldl)
-
-import Data.Set (Set, union, singleton, delete, member)
-import qualified Data.Set as Set
-
-import Data.Map (Map)
-import qualified Data.Map as Map
-
-
-
-
-type Var = String
-
-data Sig e = Const Int | Plus e e | LetIn Var e e | Var Var
-
-
-$(derive [makeFunctor, makeFoldable, smartConstructors, makeShowF] [''Sig])
-
-instance Zippable Sig where
-    fzip _ (Const i) = Const i
-    fzip (Cons a (Cons b _)) (Plus x y) = Plus (a,x) (b,y)
-    fzip (Cons a (Cons b _)) (LetIn v x y) = LetIn v (a,x) (b,y)
-    fzip _ (Var v) = Var v
-
-
-instance (Zippable f, Zippable g) => Zippable (f :+: g) where
-    fzip x (Inl v) = Inl $ fzip x v
-    fzip x (Inr v) = Inr $ fzip x v
-
--- evalSt :: UpState Sig Int
--- evalSt (Const i) = i
--- evalSt (Plus x y) = x + y
-
-type Addr = Int
-
-data Instr = Acc Int
-           | Load Addr
-           | Store Addr
-           | Add Addr
-             deriving (Show)
-
-type Code = [Instr]
-
-
-
--- heightSt :: UpState Sig Int
--- heightSt (Const _) = 0
--- heightSt (Plus x y) = 1 + max x y
--- heightSt (LetIn _ e b) = 1 + max e b
--- heightSt (Var _) = 0
-
--- codeSt :: (Int :< q) => DUpState Sig q Code 
--- codeSt (Const x) = [Acc x]
--- codeSt (Plus x y) = below x ++ [Store a] ++ below y ++ [Add a] where a = below y
-
-
--- code :: Term Sig -> Code
--- code = fst . runDUpState (codeSt <*> dUpState heightSt)
-
-
-type Vars = Set Var
-
-fvSt :: UpState Sig Vars
-fvSt (Var v)  = singleton v
-fvSt (LetIn v e b)  | v `member` b  = e `union` delete v b
-                    | otherwise     =  delete v b
-fvSt t        = foldl union Set.empty t
-
--- | Stateful homomorphism that removes unnecessary let bindings.
-remLetHom :: (Vars :< q) => QHom Sig q Sig
-remLetHom (LetIn v _ y) | not (v `Set.member` below y) = Hole y
-remLetHom  t = simpCxt t
-
-remLet :: Term Sig -> Term Sig
-remLet = runUpHom fvSt remLetHom
-
-ldepthSt :: DownState Sig Int
-ldepthSt (d,LetIn _ _ b) = b |-> d + 1
-ldepthSt _               = o
-
-type Ren = Map Var Var
-
-
-newVar :: (?above :: q, Int :< q) => Var
-newVar = show (above :: Int)
-
-renSt :: (Int :< q) => DDownState Sig q Ren
-renSt (LetIn v _ b) = b |-> (v |-> newVar & above)
-renSt _             = o
-
-renameHom :: (Ren :< q, Int :< q) => QHom Sig q Sig
-renameHom (LetIn _ a b) = iLetIn newVar (Hole a) (Hole b)
-renameHom (Var v) = case Map.lookup v above of
-                      Nothing -> iVar v
-                      Just v' -> iVar v'
-renameHom t = simpCxt t
-
-renameInit :: (Ren, Int)
-renameInit = (o, 0)
-
-rename :: Term Sig -> Term Sig
-rename = runDownHom (downState (renSt >*< dDownState ldepthSt))
-         renameHom renameInit
-
-
-heightSt :: Foldable f => UpState f Int
-heightSt t = foldl max 0 t + 1
-
-newtype Height = Height {height :: Int}
-
-heightSt' :: (Functor f,Foldable f) => UpState f Height
-heightSt' = tagUpState Height height heightSt
-
-
-newtype Depth = Depth {depth :: Int}
-
-ldepthSt' :: DownState Sig Depth
-ldepthSt' = tagDownState Depth depth ldepthSt
-
-type Bind = Map Var Int
-
-bindSt :: (Depth :< q) => DDownState Sig q Bind 
-bindSt (LetIn v _ e)  = e |-> (v |-> 2 * depth above & above)
-bindSt _              = o
-
-codeSt :: (Height :< q, Depth :< q, Bind :< q) => DUpState Sig q Code 
-codeSt (Const x) = [Acc x]
-codeSt (Plus x y) = below x ++ [Store a] ++ below y ++ [Add a] 
-    where a = 2 * height (below y) + 1
-codeSt (LetIn _ b e) = below b ++ [Store a] ++ below e
-    where a = 2 * depth above
-codeSt (Var v) = case Map.lookup v above of
-                       Nothing -> error $ "unbound variable " ++ v
-                       Just i -> [Load i]
-
-
-code :: Term Sig -> (Code, Height)
-code = runDState 
-          (codeSt <*> dUpState heightSt')
-          (bindSt >*< dDownState ldepthSt')
-          (o :: Bind, Depth 0)
diff --git a/examples/Examples/Multi/Desugar.hs b/examples/Examples/Multi/Desugar.hs
--- a/examples/Examples/Multi/Desugar.hs
+++ b/examples/Examples/Multi/Desugar.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,
   FlexibleInstances, FlexibleContexts, UndecidableInstances, GADTs,
-  IncoherentInstances #-}
+  ConstraintKinds #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Examples.Multi.Desugar
diff --git a/examples/Examples/Multi/Eval.hs b/examples/Examples/Multi/Eval.hs
--- a/examples/Examples/Multi/Eval.hs
+++ b/examples/Examples/Multi/Eval.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,
   FlexibleInstances, FlexibleContexts, UndecidableInstances, GADTs,
-  OverlappingInstances #-}
+  OverlappingInstances, ConstraintKinds #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Examples.Multi.Eval
diff --git a/examples/Examples/Multi/EvalM.hs b/examples/Examples/Multi/EvalM.hs
--- a/examples/Examples/Multi/EvalM.hs
+++ b/examples/Examples/Multi/EvalM.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,
   FlexibleInstances, FlexibleContexts, UndecidableInstances, GADTs,
-  OverlappingInstances #-}
+  OverlappingInstances, ConstraintKinds #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Examples.Multi.EvalM
diff --git a/examples/Examples/Thunk.hs b/examples/Examples/Thunk.hs
--- a/examples/Examples/Thunk.hs
+++ b/examples/Examples/Thunk.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,
-  FlexibleInstances, FlexibleContexts, UndecidableInstances, OverlappingInstances #-}
+  FlexibleInstances, FlexibleContexts, UndecidableInstances, ConstraintKinds #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Examples.Thunk
@@ -21,8 +21,7 @@
 import Data.Comp.Thunk
 import Data.Comp.Derive
 import Data.Comp.Show()
-import Control.Monad
-import Examples.Common hiding (Value(..), Sig)
+import Examples.Common hiding (Value(..), Sig, iConst, iPair)
 
 -- Signature for values, strict pairs
 data Value a = Const Int | Pair !a !a
@@ -36,16 +35,16 @@
          [''Value])
 
 -- Monadic term evaluation algebra
-class EvalT f v where
+class EvalT f m v where
   evalAlgT :: Monad m => AlgT m f v
 
 $(derive [liftSum] [''EvalT])
 
 -- Lift the monadic evaluation algebra to a monadic catamorphism
-evalT :: (Traversable v, Functor f, EvalT f v, Monad m) => Term f -> m (Term v)
+evalT :: (Traversable v, Functor f, EvalT f m v, Monad m) => Term f -> m (Term v)
 evalT = nf . cata evalAlgT
 
-instance (Value :<: v) => EvalT Value v where
+instance (Value :<: m :+: v) => EvalT Value m v where
 -- make pairs strict in both components
 --  evalAlgT x@Pair{} = strict x
 -- or explicitly:
@@ -55,7 +54,7 @@
 -- or only partially strict
   evalAlgT = haskellStrict'
 
-instance (Value :<: v) => EvalT Op v where
+instance (Value :<: m :+: v, Value :<: v) => EvalT Op m v where
   evalAlgT (Add x y) = thunk $ do
                          Const n1 <- whnfPr x
                          Const n2 <- whnfPr y
diff --git a/src/Data/Comp/Automata.hs b/src/Data/Comp/Automata.hs
--- a/src/Data/Comp/Automata.hs
+++ b/src/Data/Comp/Automata.hs
@@ -291,7 +291,8 @@
 -- deterministic bottom-up tree acceptors (GUTAs) which have access
 -- to an extended state space.
 
-type DUpState f p q = forall a . (?below :: a -> p, ?above :: p, q :< p) => f a -> q
+type DUpState f p q = (q :< p) => DUpState' f p q
+type DUpState' f p q = forall a . (?below :: a -> p, ?above :: p) => f a -> q
 
 -- | This combinator turns an arbitrary UTA into a GUTA.
 
@@ -451,7 +452,9 @@
 -- deterministic top-down tree acceptors (GDTAs) which have access
 
 -- to an extended state space.
-type DDownState f p q = forall i . (Ord i, ?below :: i -> p, ?above :: p, q :< p)
+type DDownState f p q = (q :< p) => DDownState' f p q
+
+type DDownState' f p q = forall i . (Ord i, ?below :: i -> p, ?above :: p)
                                 => f i -> Map i q
 
 -- | This combinator turns an arbitrary DTA into a GDTA.
@@ -486,7 +489,7 @@
 -- transformations. Both state transformations can depend mutually
 -- recursive on each other.
 
-runDState :: Traversable f => DUpState f (u,d) u -> DDownState f (u,d) d -> d -> Term f -> u
+runDState :: Traversable f => DUpState' f (u,d) u -> DDownState' f (u,d) d -> d -> Term f -> u
 runDState up down d (Term t) = u where
         t' = fmap bel $ number t
         bel (Numbered (i,s)) = 
@@ -500,7 +503,7 @@
 -- transformation.
         
 runQHom :: (Traversable f, Functor g) =>
-           DUpState f (u,d) u -> DDownState f (u,d) d -> 
+           DUpState' f (u,d) u -> DDownState' f (u,d) d -> 
            QHom f (u,d) g ->
            d -> Term f -> (u, Term g)
 runQHom up down trans d (Term t) = (u,t'') where
diff --git a/src/Data/Comp/Automata/Product.hs b/src/Data/Comp/Automata/Product.hs
--- a/src/Data/Comp/Automata/Product.hs
+++ b/src/Data/Comp/Automata/Product.hs
@@ -1,8 +1,10 @@
-{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FlexibleInstances, IncoherentInstances, TemplateHaskell #-}
+{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FlexibleInstances,
+IncoherentInstances, TemplateHaskell, ScopedTypeVariables, DataKinds, TypeFamilies,
+UndecidableInstances, GADTs, ConstraintKinds, FlexibleContexts, PolyKinds #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Automata.Product
--- Copyright   :  (c) 2011 Patrick Bahr
+-- Copyright   :  (c) 2014 Patrick Bahr
 -- License     :  BSD3
 -- Maintainer  :  Patrick Bahr <paba@diku.dk>
 -- Stability   :  experimental
@@ -11,19 +13,43 @@
 --
 --------------------------------------------------------------------------------
 
-module Data.Comp.Automata.Product ((:<)(..)) where
+module Data.Comp.Automata.Product ((:<), pr) where
 
-import Data.Comp.Automata.Product.Derive
 
 
-instance a :< a where
-    pr = id
+data Pos = Here | Le Pos | Ri Pos
 
+data Res = NotFound | Ambiguous | Found Pos
 
-instance (a,b) :< (a,b) where
-    pr = id
+type family Ch (l :: Res) (r :: Res) :: Res where
+    Ch (Found x) (Found y) = Ambiguous
+    Ch Ambiguous y = Ambiguous
+    Ch x Ambiguous = Ambiguous
+    Ch (Found x) y = Found (Le x)
+    Ch x (Found y) = Found (Ri y)
+    Ch x y = NotFound
 
-$(genAllInsts 7)
+type family Elem (e :: *) (p :: *) :: Res where
+    Elem e e = Found Here
+    Elem e (l,r) = Ch (Elem e l) (Elem e r)
+    Elem e p = NotFound
 
-instance (c :< b) => c :< (a,b) where
-    pr = pr . snd
+data Proxy a = P
+
+class IsElem (res :: Res) e p where
+    pr' :: Proxy res -> p -> e
+
+instance IsElem (Found Here) e e where
+    pr' _ = id
+
+instance IsElem (Found pos) e p => IsElem (Found (Le pos)) e (p, p') where
+    pr' _ (x,_) = pr' (P :: Proxy (Found pos)) x
+
+instance IsElem (Found pos) e p => IsElem (Found (Ri pos)) e (p', p) where
+    pr' _ (_,y) = pr' (P :: Proxy (Found pos)) y
+
+
+type (e :< p) = IsElem (Elem e p) e p
+
+pr :: forall e p . (e :< p) => p -> e
+pr = pr' (P :: Proxy (Elem e p))
diff --git a/src/Data/Comp/Derive/HaskellStrict.hs b/src/Data/Comp/Derive/HaskellStrict.hs
--- a/src/Data/Comp/Derive/HaskellStrict.hs
+++ b/src/Data/Comp/Derive/HaskellStrict.hs
@@ -24,7 +24,6 @@
 import Data.Maybe
 import Data.Comp.Thunk
 import Data.Comp.Sum
-import Data.Comp.Ops
 import Data.Traversable
 import Data.Foldable hiding (any,or)
 import Control.Monad hiding (mapM, sequence)
@@ -34,15 +33,15 @@
 
 class HaskellStrict f where
     thunkSequence :: (Monad m) => f (TermT m g) -> m (f (TermT m g))
-    thunkSequenceInject :: (Monad m, f :<: g) => f (TermT m g) -> TermT m g
-    thunkSequenceInject t = thunk $ liftM (inject_ (Inr . inj)) $ thunkSequence t
-    thunkSequenceInject' :: (Monad m, f :<: g) => f (TermT m g) -> TermT m g
+    thunkSequenceInject :: (Monad m, f :<: m :+: g) => f (TermT m g) -> TermT m g
+    thunkSequenceInject t = thunk $ liftM inject $ thunkSequence t
+    thunkSequenceInject' :: (Monad m, f :<: m :+: g) => f (TermT m g) -> TermT m g
     thunkSequenceInject' = thunkSequenceInject
 
-haskellStrict :: (Monad m, HaskellStrict f, f :<: g) => f (TermT m g) -> TermT m g
+haskellStrict :: (Monad m, HaskellStrict f, f :<: m :+: g) => f (TermT m g) -> TermT m g
 haskellStrict = thunkSequenceInject
 
-haskellStrict' :: (Monad m, HaskellStrict f, f :<: g) => f (TermT m g) -> TermT m g
+haskellStrict' :: (Monad m, HaskellStrict f, f :<: m :+: g) => f (TermT m g) -> TermT m g
 haskellStrict' = thunkSequenceInject'
 
 deepThunk d = iter d [|thunkSequence|]
diff --git a/src/Data/Comp/Derive/Projections.hs b/src/Data/Comp/Derive/Projections.hs
deleted file mode 100644
--- a/src/Data/Comp/Derive/Projections.hs
+++ /dev/null
@@ -1,95 +0,0 @@
-{-# LANGUAGE TemplateHaskell, GADTs #-}
---------------------------------------------------------------------------------
--- |
--- Module      :  Data.Comp.Derive.Projections
--- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
--- License     :  BSD3
--- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
--- Stability   :  experimental
--- Portability :  non-portable (GHC Extensions)
---
--- Derive functions for signature projections.
---
---------------------------------------------------------------------------------
-
-module Data.Comp.Derive.Projections
-    (
-     projn,
-     projectn,
-     deepProjectn
-    ) where
-
-import Language.Haskell.TH hiding (Cxt)
-import Control.Monad (liftM)
-import Data.Traversable (Traversable)
-import Data.Comp.Term
-import Data.Comp.Algebra (CxtFunM, appSigFunM')
-import Data.Comp.Ops ((:+:)(..), (:<:), proj, inj)
-
-projn :: Int -> Q [Dec]
-projn n = do
-  let p = mkName $ "proj" ++ show n
-  let gvars = map (\n -> mkName $ 'g' : show n) [1..n]
-  let avar = mkName "a"
-  let xvar = mkName "x"
-  let d = [funD p [clause [varP xvar] (normalB $ genDecl xvar gvars avar) []]]
-  sequence $ (sigD p $ genSig gvars avar) : d
-    where genSig gvars avar = do
-            let fvar = mkName "f"
-            let cxt = map (\g -> classP ''(:<:) [varT g, varT fvar]) gvars
-            let tp = foldl1 (\a g -> conT ''(:+:) `appT` g `appT` a)
-                            (map varT gvars)
-            let tp' = arrowT `appT` (varT fvar `appT` varT avar)
-                             `appT` (conT ''Maybe `appT`
-                                     (tp `appT` varT avar))
-            forallT (map PlainTV $ fvar : avar : gvars) (sequence cxt) tp'
-          genDecl x [g] a =
-            [| liftM inj (proj $(varE x)
-                          :: Maybe ($(varT g `appT` varT a))) |]
-          genDecl x (g:gs) a =
-            [| case (proj $(varE x)
-                         :: Maybe ($(varT g `appT` varT a))) of
-                 Just y -> Just $ inj y
-                 _ -> $(genDecl x gs a) |]
-          genDecl _ _ _ = error "genDecl called with empty list"
-
-projectn :: Int -> Q [Dec]
-projectn n = do
-  let p = mkName ("project" ++ show n)
-  let gvars = map (\n -> mkName $ 'g' : show n) [1..n]
-  let avar = mkName "a"
-  let xvar = mkName "x"
-  let d = [funD p [clause [varP xvar] (normalB $ genDecl xvar n) []]]
-  sequence $ (sigD p $ genSig gvars avar) : d
-    where genSig gvars avar = do
-            let fvar = mkName "f"
-            let hvar = mkName "h"
-            let cxt = map (\g -> classP ''(:<:) [varT g, varT fvar]) gvars
-            let tp = foldl1 (\a g -> conT ''(:+:) `appT` g `appT` a)
-                            (map varT gvars)
-            let tp' = conT ''Cxt `appT` varT hvar `appT` varT fvar
-                                 `appT` varT avar
-            let tp'' = arrowT `appT` tp'
-                              `appT` (conT ''Maybe `appT` (tp `appT` tp'))
-            forallT (map PlainTV $ hvar : fvar : avar : gvars)
-                    (sequence cxt) tp''
-          genDecl x n = [| case $(varE x) of
-                             Hole _ -> Nothing
-                             Term t -> $(varE $ mkName $ "proj" ++ show n) t |]
-
-deepProjectn :: Int -> Q [Dec]
-deepProjectn n = do
-  let p = mkName ("deepProject" ++ show n)
-  let gvars = map (\n -> mkName $ 'g' : show n) [1..n]
-  let d = [funD p [clause [] (normalB $ genDecl n) []]]
-  sequence $ (sigD p $ genSig gvars) : d
-    where genSig gvars = do
-            let fvar = mkName "f"
-            let cxt = map (\g -> classP ''(:<:) [varT g, varT fvar]) gvars
-            let tp = foldl1 (\a g -> conT ''(:+:) `appT` g `appT` a)
-                            (map varT gvars)
-            let cxt' = classP ''Traversable [tp]
-            let tp' = conT ''CxtFunM `appT` conT ''Maybe
-                                     `appT` varT fvar `appT` tp
-            forallT (map PlainTV $ fvar : gvars) (sequence $ cxt' : cxt) tp'
-          genDecl n = [| appSigFunM' $(varE $ mkName $ "proj" ++ show n) |]
diff --git a/src/Data/Comp/Multi/Annotation.hs b/src/Data/Comp/Multi/Annotation.hs
--- a/src/Data/Comp/Multi/Annotation.hs
+++ b/src/Data/Comp/Multi/Annotation.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators, MultiParamTypeClasses,
+{-# LANGUAGE TypeOperators, MultiParamTypeClasses, ConstraintKinds, FlexibleContexts,
   FlexibleInstances, UndecidableInstances, Rank2Types, GADTs, ScopedTypeVariables #-}
 --------------------------------------------------------------------------------
 -- |
diff --git a/src/Data/Comp/Multi/Derive/Equality.hs b/src/Data/Comp/Multi/Derive/Equality.hs
--- a/src/Data/Comp/Multi/Derive/Equality.hs
+++ b/src/Data/Comp/Multi/Derive/Equality.hs
@@ -38,7 +38,6 @@
   return [InstanceD preCond classType [eqFDecl]]
       where eqFClauses ftyp constrs constrs' = map (genEqClause ftyp) constrs'
                                    ++ defEqClause constrs
-            filterFarg fArg ty x = (containsType ty fArg, varE x)
             defEqClause constrs
                 | length constrs  < 2 = []
                 | otherwise = [clause [wildP,wildP] (normalB [|False|]) []]
diff --git a/src/Data/Comp/Multi/Derive/HTraversable.hs b/src/Data/Comp/Multi/Derive/HTraversable.hs
--- a/src/Data/Comp/Multi/Derive/HTraversable.hs
+++ b/src/Data/Comp/Multi/Derive/HTraversable.hs
@@ -32,10 +32,6 @@
 iter 0 _ e = e
 iter n f e = iter (n-1) f (f `appE` e)
 
-iter' n f e = run n f e
-    where run 0 _ e = e
-          run m f e = let f' = iter (m-1) [|fmap|] f
-                        in run (m-1) f (f' `appE` e)
 
 {-| Derive an instance of 'HTraversable' for a type constructor of any
   higher-order kind taking at least two arguments. -}
diff --git a/src/Data/Comp/Multi/Derive/Injections.hs b/src/Data/Comp/Multi/Derive/Injections.hs
deleted file mode 100644
--- a/src/Data/Comp/Multi/Derive/Injections.hs
+++ /dev/null
@@ -1,87 +0,0 @@
-{-# LANGUAGE TemplateHaskell #-}
---------------------------------------------------------------------------------
--- |
--- Module      :  Data.Comp.Multi.Derive.Injections
--- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
--- License     :  BSD3
--- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
--- Stability   :  experimental
--- Portability :  non-portable (GHC Extensions)
---
--- Derive functions for signature injections.
---
---------------------------------------------------------------------------------
-
-module Data.Comp.Multi.Derive.Injections
-    (
-     injn,
-     injectn,
-     deepInjectn
-    ) where
-
-import Language.Haskell.TH hiding (Cxt)
-import Data.Comp.Multi.HFunctor
-import Data.Comp.Multi.Term
-import Data.Comp.Multi.Algebra (CxtFun, appSigFun)
-import Data.Comp.Multi.Ops ((:+:)(..), (:<:)(..))
-
-injn :: Int -> Q [Dec]
-injn n = do
-  let i = mkName $ "inj" ++ show n
-  let fvars = map (\n -> mkName $ 'f' : show n) [1..n]
-  let gvar = mkName "g"
-  let avar = mkName "a"
-  let ivar = mkName "i"
-  let xvar = mkName "x"
-  let d = [funD i [clause [varP xvar] (normalB $ genDecl xvar n) []]]
-  sequence $ sigD i (genSig fvars gvar avar ivar) : d
-    where genSig fvars gvar avar ivar = do
-            let cxt = map (\f -> classP ''(:<:) [varT f, varT gvar]) fvars
-            let tp = foldl1 (\a f -> conT ''(:+:) `appT` f `appT` a)
-                            (map varT fvars)
-            let tp' = arrowT `appT` (tp `appT` varT avar `appT` varT ivar)
-                             `appT` (varT gvar `appT` varT avar
-                                               `appT` varT ivar)
-            forallT (map PlainTV $ gvar : avar : ivar : fvars)
-                    (sequence cxt) tp'
-          genDecl x n = [| case $(varE x) of
-                             Inl x -> $(varE $ mkName "inj") x
-                             Inr x -> $(varE $ mkName $ "inj" ++
-                                        if n > 2 then show (n - 1) else "") x |]
-injectn :: Int -> Q [Dec]
-injectn n = do
-  let i = mkName ("inject" ++ show n)
-  let fvars = map (\n -> mkName $ 'f' : show n) [1..n]
-  let gvar = mkName "g"
-  let avar = mkName "a"
-  let ivar = mkName "i"
-  let d = [funD i [clause [] (normalB $ genDecl n) []]]
-  sequence $ sigD i (genSig fvars gvar avar ivar) : d
-    where genSig fvars gvar avar ivar = do
-            let hvar = mkName "h"
-            let cxt = map (\f -> classP ''(:<:) [varT f, varT gvar]) fvars
-            let tp = foldl1 (\a f -> conT ''(:+:) `appT` f `appT` a)
-                            (map varT fvars)
-            let tp' = conT ''Cxt `appT` varT hvar `appT` varT gvar
-                                 `appT` varT avar
-            let tp'' = arrowT `appT` (tp `appT` tp' `appT` varT ivar)
-                              `appT` (tp' `appT` varT ivar)
-            forallT (map PlainTV $ hvar : gvar : avar : ivar : fvars)
-                    (sequence cxt) tp''
-          genDecl n = [| Term . $(varE $ mkName $ "inj" ++ show n) |]
-
-deepInjectn :: Int -> Q [Dec]
-deepInjectn n = do
-  let i = mkName ("deepInject" ++ show n)
-  let fvars = map (\n -> mkName $ 'f' : show n) [1..n]
-  let gvar = mkName "g"
-  let d = [funD i [clause [] (normalB $ genDecl n) []]]
-  sequence $ sigD i (genSig fvars gvar) : d
-    where genSig fvars gvar = do
-            let cxt = map (\f -> classP ''(:<:) [varT f, varT gvar]) fvars
-            let tp = foldl1 (\a f -> conT ''(:+:) `appT` f `appT` a)
-                            (map varT fvars)
-            let cxt' = classP ''HFunctor [tp]
-            let tp' = conT ''CxtFun `appT` tp `appT` varT gvar
-            forallT (map PlainTV $ gvar : fvars) (sequence $ cxt' : cxt) tp'
-          genDecl n = [| appSigFun $(varE $ mkName $ "inj" ++ show n) |]
diff --git a/src/Data/Comp/Multi/Derive/Projections.hs b/src/Data/Comp/Multi/Derive/Projections.hs
deleted file mode 100644
--- a/src/Data/Comp/Multi/Derive/Projections.hs
+++ /dev/null
@@ -1,100 +0,0 @@
-{-# LANGUAGE TemplateHaskell, GADTs #-}
---------------------------------------------------------------------------------
--- |
--- Module      :  Data.Comp.Multi.Derive.Projections
--- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
--- License     :  BSD3
--- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
--- Stability   :  experimental
--- Portability :  non-portable (GHC Extensions)
---
--- Derive functions for signature projections.
---
---------------------------------------------------------------------------------
-
-module Data.Comp.Multi.Derive.Projections
-    (
-     projn,
-     projectn,
-     deepProjectn
-    ) where
-
-import Language.Haskell.TH hiding (Cxt)
-import Control.Monad (liftM)
-import Data.Comp.Multi.HTraversable (HTraversable)
-import Data.Comp.Multi.Term
-import Data.Comp.Multi.Algebra (CxtFunM, appSigFunM')
-import Data.Comp.Multi.Ops ((:+:)(..), (:<:)(..))
-
-projn :: Int -> Q [Dec]
-projn n = do
-  let p = mkName $ "proj" ++ show n
-  let gvars = map (\n -> mkName $ 'g' : show n) [1..n]
-  let avar = mkName "a"
-  let ivar = mkName "i"
-  let xvar = mkName "x"
-  let d = [funD p [clause [varP xvar] (normalB $ genDecl xvar gvars avar ivar) []]]
-  sequence $ (sigD p $ genSig gvars avar ivar) : d
-    where genSig gvars avar ivar = do
-            let fvar = mkName "f"
-            let cxt = map (\g -> classP ''(:<:) [varT g, varT fvar]) gvars
-            let tp = foldl1 (\a g -> conT ''(:+:) `appT` g `appT` a)
-                            (map varT gvars)
-            let tp' = arrowT
-                      `appT` (varT fvar `appT` varT avar `appT` varT ivar)
-                      `appT` (conT ''Maybe `appT`
-                              (tp `appT` varT avar `appT` varT ivar))
-            forallT (map PlainTV $ fvar : ivar : avar : gvars)
-                    (sequence cxt) tp'
-          genDecl x [g] a i =
-            [| liftM inj (proj $(varE x)
-                          :: Maybe ($(varT g `appT` varT a `appT` varT i))) |]
-          genDecl x (g:gs) a i =
-            [| case (proj $(varE x)
-                         :: Maybe ($(varT g `appT` varT a `appT` varT i))) of
-                 Just y -> Just $ inj y
-                 _ -> $(genDecl x gs a i) |]
-          genDecl _ _ _ _ = error "genDecl called with empty list"
-
-projectn :: Int -> Q [Dec]
-projectn n = do
-  let p = mkName ("project" ++ show n)
-  let gvars = map (\n -> mkName $ 'g' : show n) [1..n]
-  let avar = mkName "a"
-  let ivar = mkName "i"
-  let xvar = mkName "x"
-  let d = [funD p [clause [varP xvar] (normalB $ genDecl xvar n) []]]
-  sequence $ (sigD p $ genSig gvars avar ivar) : d
-    where genSig gvars avar ivar = do
-            let fvar = mkName "f"
-            let hvar = mkName "h"
-            let cxt = map (\g -> classP ''(:<:) [varT g, varT fvar]) gvars
-            let tp = foldl1 (\a g -> conT ''(:+:) `appT` g `appT` a)
-                            (map varT gvars)
-            let tp' = conT ''Cxt `appT` varT hvar `appT` varT fvar
-                                 `appT` varT avar
-            let tp'' = arrowT `appT` (tp' `appT` varT ivar)
-                              `appT` (conT ''Maybe `appT`
-                                      (tp `appT` tp' `appT` varT ivar))
-            forallT (map PlainTV $ hvar : fvar : avar : ivar : gvars)
-                    (sequence cxt) tp''
-          genDecl x n = [| case $(varE x) of
-                             Hole _ -> Nothing
-                             Term t -> $(varE $ mkName $ "proj" ++ show n) t |]
-
-deepProjectn :: Int -> Q [Dec]
-deepProjectn n = do
-  let p = mkName ("deepProject" ++ show n)
-  let gvars = map (\n -> mkName $ 'g' : show n) [1..n]
-  let d = [funD p [clause [] (normalB $ genDecl n) []]]
-  sequence $ (sigD p $ genSig gvars) : d
-    where genSig gvars = do
-            let fvar = mkName "f"
-            let cxt = map (\g -> classP ''(:<:) [varT g, varT fvar]) gvars
-            let tp = foldl1 (\a g -> conT ''(:+:) `appT` g `appT` a)
-                            (map varT gvars)
-            let cxt' = classP ''HTraversable [tp]
-            let tp' = conT ''CxtFunM `appT` conT ''Maybe
-                                     `appT` varT fvar `appT` tp
-            forallT (map PlainTV $ fvar : gvars) (sequence $ cxt' : cxt) tp'
-          genDecl n = [| appSigFunM' $(varE $ mkName $ "proj" ++ show n) |]
diff --git a/src/Data/Comp/Multi/Derive/SmartAConstructors.hs b/src/Data/Comp/Multi/Derive/SmartAConstructors.hs
--- a/src/Data/Comp/Multi/Derive/SmartAConstructors.hs
+++ b/src/Data/Comp/Multi/Derive/SmartAConstructors.hs
@@ -30,13 +30,13 @@
   inserted. -}
 smartAConstructors :: Name -> Q [Dec]
 smartAConstructors fname = do
-    TyConI (DataD _cxt tname targs constrs _deriving) <- abstractNewtypeQ $ reify fname
+    TyConI (DataD _cxt _tname _targs constrs _deriving) <- abstractNewtypeQ $ reify fname
     let cons = map abstractConType constrs
-    liftM concat $ mapM (genSmartConstr (map tyVarBndrName targs) tname) cons
-        where genSmartConstr targs tname (name, args) = do
+    liftM concat $ mapM genSmartConstr cons
+        where genSmartConstr (name, args) = do
                 let bname = nameBase name
-                genSmartConstr' targs tname (mkName $ "iA" ++ bname) name args
-              genSmartConstr' targs tname sname name args = do
+                genSmartConstr' (mkName $ "iA" ++ bname) name args
+              genSmartConstr' sname name args = do
                 varNs <- newNames args "x"
                 varPr <- newName "_p"
                 let pats = map varP (varPr : varNs)
diff --git a/src/Data/Comp/Multi/Desugar.hs b/src/Data/Comp/Multi/Desugar.hs
--- a/src/Data/Comp/Multi/Desugar.hs
+++ b/src/Data/Comp/Multi/Desugar.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE TemplateHaskell, MultiParamTypeClasses, FlexibleInstances,
-  UndecidableInstances, TypeOperators, OverlappingInstances #-}
+  UndecidableInstances, TypeOperators, OverlappingInstances, ConstraintKinds #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Multi.Desugar
diff --git a/src/Data/Comp/Multi/Generic.hs b/src/Data/Comp/Multi/Generic.hs
--- a/src/Data/Comp/Multi/Generic.hs
+++ b/src/Data/Comp/Multi/Generic.hs
@@ -1,4 +1,5 @@
-{-# LANGUAGE GADTs, ExistentialQuantification, TypeOperators, ScopedTypeVariables, Rank2Types #-}
+{-# LANGUAGE GADTs, ExistentialQuantification, TypeOperators, ScopedTypeVariables, 
+  Rank2Types, ConstraintKinds, FlexibleContexts #-}
 
 --------------------------------------------------------------------------------
 -- |
diff --git a/src/Data/Comp/Multi/Ops.hs b/src/Data/Comp/Multi/Ops.hs
--- a/src/Data/Comp/Multi/Ops.hs
+++ b/src/Data/Comp/Multi/Ops.hs
@@ -1,8 +1,8 @@
-{-# LANGUAGE TypeOperators, MultiParamTypeClasses, IncoherentInstances,
+{-# LANGUAGE TypeOperators, MultiParamTypeClasses, OverlappingInstances,
              FlexibleInstances, FlexibleContexts, GADTs, TypeSynonymInstances,
-             ScopedTypeVariables, FunctionalDependencies, UndecidableInstances, KindSignatures, RankNTypes{-|
-  
--} #-}
+             ScopedTypeVariables, FunctionalDependencies, UndecidableInstances, 
+             KindSignatures, RankNTypes, TypeFamilies, DataKinds, ConstraintKinds,
+             PolyKinds #-}
 
 --------------------------------------------------------------------------------
 -- |
@@ -28,7 +28,7 @@
 import Control.Applicative
 
 
-infixr 5 :+:
+infixr 6 :+:
 
 
 -- |Data type defining coproducts.
@@ -67,24 +67,131 @@
     hmapM f (Inl e) = Inl `liftM` hmapM f e
     hmapM f (Inr e) = Inr `liftM` hmapM f e
 
--- |The subsumption relation.
-class (sub :: (* -> *) -> * -> *) :<: sup where
-    inj :: sub a :-> sup a
-    proj :: NatM Maybe (sup a) (sub a)
+-- The subsumption relation.
 
-instance (:<:) f f where
-    inj = id
-    proj = Just
+infixl 5 :<:
+infixl 5 :=:
 
-instance (:<:) f (f :+: g) where
-    inj = Inl
-    proj (Inl x) = Just x
-    proj (Inr _) = Nothing
+data Pos = Here | Le Pos | Ri Pos | Sum Pos Pos
+data Emb = Found Pos | NotFound | Ambiguous
 
-instance (f :<: g) => (:<:) f (h :+: g) where
-    inj = Inr . inj
-    proj (Inr x) = proj x
-    proj (Inl _) = Nothing
+
+type family Elem (f :: (* -> *) -> * -> *)
+                 (g :: (* -> *) -> * -> *) :: Emb where
+    Elem f f = Found Here
+    Elem f (g1 :+: g2) = Choose f (g1 :+: g2) (Elem f g1) (Elem f g2)
+    Elem f g = NotFound
+
+
+type family Choose f g (e1 :: Emb) (r :: Emb) :: Emb where
+    Choose f g (Found x) (Found y) = Ambiguous
+    Choose f g Ambiguous y = Ambiguous
+    Choose f g x Ambiguous = Ambiguous
+    Choose f g (Found x) y = Found (Le x)
+    Choose f g x (Found y) = Found (Ri y)
+    Choose (f1 :+: f2) g x y =  Sum' (Elem f1 g) (Elem f2 g) 
+    Choose f g x y = NotFound
+
+
+type family Sum' (e1 :: Emb) (r :: Emb) :: Emb where
+    Sum' (Found x) (Found y) = Found (Sum x y)
+    Sum' Ambiguous y = Ambiguous
+    Sum' x Ambiguous = Ambiguous
+    Sum' NotFound y = NotFound
+    Sum' x NotFound = NotFound
+
+data Proxy a = P
+
+class Subsume (e :: Emb) (f :: (* -> *) -> * -> *)
+                         (g :: (* -> *) -> * -> *) where
+  inj'  :: Proxy e -> f a :-> g a
+  prj'  :: Proxy e -> NatM Maybe (g a) (f a)
+
+instance Subsume (Found Here) f f where
+    inj' _ = id
+
+    prj' _ = Just
+
+instance Subsume (Found p) f g => Subsume (Found (Le p)) f (g :+: g') where
+    inj' _ = Inl . inj' (P :: Proxy (Found p))
+    
+    prj' _ (Inl x) = prj' (P :: Proxy (Found p)) x
+    prj' _ _       = Nothing
+
+instance Subsume (Found p) f g => Subsume (Found (Ri p)) f (g' :+: g) where
+    inj' _ = Inr . inj' (P :: Proxy (Found p))
+
+    prj' _ (Inr x) = prj' (P :: Proxy (Found p)) x
+    prj' _ _       = Nothing
+              
+instance (Subsume (Found p1) f1 g, Subsume (Found p2) f2 g) 
+    => Subsume (Found (Sum p1 p2)) (f1 :+: f2) g where
+    inj' _ (Inl x) = inj' (P :: Proxy (Found p1)) x
+    inj' _ (Inr x) = inj' (P :: Proxy (Found p2)) x
+
+    prj' _ x = case prj' (P :: Proxy (Found p1)) x of
+                 Just y -> Just (Inl y)
+                 _      -> case prj' (P :: Proxy (Found p2)) x of
+                             Just y -> Just (Inr y)
+                             _      -> Nothing
+
+
+type family Or (a :: Bool) (b :: Bool) :: Bool where
+    Or  False  False  = False
+    Or  a      b      = True
+
+
+type family AnyDupl f g where
+    AnyDupl f f = False -- ignore check for duplication if subsumption is reflexive
+    AnyDupl f g = Or (Dupl f '[]) (Dupl g '[])
+
+type family Dupl (f :: (* -> *) -> * -> *) (l :: [(* -> *) -> * -> *]) :: Bool where
+    Dupl (f :+: g) l = Dupl f (g ': l)
+    Dupl f l         = Or (Find f l) (Dupl' l)
+
+type family Dupl' (l :: [(* -> *) -> * -> *]) :: Bool where
+    Dupl' (f ': l) = Or (Dupl f l) (Dupl' l)
+    Dupl' '[]      = False
+
+type family Find (f :: (* -> *) -> * -> *) (l :: [(* -> *) -> * -> *]) :: Bool where
+    Find f (g ': l) = Or (Find' f g) (Find f l)
+    Find f '[]       = False
+
+type family Find' (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *) :: Bool where
+    Find' f (g1 :+: g2) = Or (Find' f g1) (Find' f g2)
+    Find' f f = True
+    Find' f g = False
+
+
+class NoDupl f g s
+instance NoDupl f g False
+
+-- | The :<: constraint is a conjunction of two constraints. The first
+-- one is used to construct the evidence that is used to implement the
+-- injection and projection functions. The first constraint alone
+-- would allow instances such as @F :+: F :<: F@ or @F :+: (F :+: G)
+-- :<: F :+: G@ which have multiple occurrences of the same
+-- sub-signature on the left-hand side. Such instances are usually
+-- unintended and yield injection functions that are not
+-- injective. The second constraint excludes such instances.
+type f :<: g = (Subsume (Elem f g) f g , 
+                NoDupl f g (AnyDupl f g))
+
+
+inj :: forall f g a . (f :<: g) => f a :-> g a
+inj = inj' (P :: Proxy (Elem f g))
+
+proj :: forall f g a . (f :<: g) => NatM Maybe (g a) (f a)
+proj = prj' (P :: Proxy (Elem f g))
+
+type f :=: g = (f :<: g, g :<: f) 
+
+
+
+spl :: (f :=: f1 :+: f2) => (f1 a :-> b) -> (f2 a :-> b) -> f a :-> b
+spl f1 f2 x = case inj x of 
+            Inl y -> f1 y
+            Inr y -> f2 y
 
 -- Products
 
diff --git a/src/Data/Comp/Multi/Sum.hs b/src/Data/Comp/Multi/Sum.hs
--- a/src/Data/Comp/Multi/Sum.hs
+++ b/src/Data/Comp/Multi/Sum.hs
@@ -1,5 +1,5 @@
-{-# LANGUAGE TypeOperators, GADTs, ScopedTypeVariables, IncoherentInstances,
-  Rank2Types, FlexibleContexts, TemplateHaskell #-}
+{-# LANGUAGE TypeOperators, GADTs, ScopedTypeVariables,
+  Rank2Types, FlexibleContexts, TemplateHaskell, ConstraintKinds #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Multi.Sum
@@ -22,72 +22,18 @@
 
      -- * Projections for Signatures and Terms
      proj,
-     proj2,
-     proj3,
-     proj4,
-     proj5,
-     proj6,
-     proj7,
-     proj8,
-     proj9,
-     proj10,
      project,
-     project2,
-     project3,
-     project4,
-     project5,
-     project6,
-     project7,
-     project8,
-     project9,
-     project10,
      deepProject,
-     deepProject2,
-     deepProject3,
-     deepProject4,
-     deepProject5,
-     deepProject6,
-     deepProject7,
-     deepProject8,
-     deepProject9,
-     deepProject10,
 
      -- * Injections for Signatures and Terms
      inj,
-     inj2,
-     inj3,
-     inj4,
-     inj5,
-     inj6,
-     inj7,
-     inj8,
-     inj9,
-     inj10,
      inject,
-     inject2,
-     inject3,
-     inject4,
-     inject5,
-     inject6,
-     inject7,
-     inject8,
-     inject9,
-     inject10,
      deepInject,
-     deepInject2,
-     deepInject3,
-     deepInject4,
-     deepInject5,
-     deepInject6,
-     deepInject7,
-     deepInject8,
-     deepInject9,
-     deepInject10,
 
+     split,
+
      -- * Injections and Projections for Constants
      injectConst,
-     injectConst2,
-     injectConst3,
      projectConst,
      injectCxt,
      liftCxt,
@@ -100,11 +46,7 @@
 import Data.Comp.Multi.Ops
 import Data.Comp.Multi.Term
 import Data.Comp.Multi.Algebra
-import Data.Comp.Multi.Derive.Projections
-import Data.Comp.Multi.Derive.Injections
-import Control.Monad (liftM)
 
-$(liftM concat $ mapM projn [2..10])
 
 -- |Project the outermost layer of a term to a sub signature. If the signature
 -- @g@ is compound of /n/ atomic signatures, use @project@/n/ instead.
@@ -112,7 +54,6 @@
 project (Hole _) = Nothing
 project (Term t) = proj t
 
-$(liftM concat $ mapM projectn [2..10])
 
 -- | Tries to coerce a term/context to a term/context over a sub-signature. If
 -- the signature @g@ is compound of /n/ atomic signatures, use
@@ -121,25 +62,12 @@
 {-# INLINE deepProject #-}
 deepProject = appSigFunM' proj
 
-$(liftM concat $ mapM deepProjectn [2..10])
-{-# INLINE deepProject2 #-}
-{-# INLINE deepProject3 #-}
-{-# INLINE deepProject4 #-}
-{-# INLINE deepProject5 #-}
-{-# INLINE deepProject6 #-}
-{-# INLINE deepProject7 #-}
-{-# INLINE deepProject8 #-}
-{-# INLINE deepProject9 #-}
-{-# INLINE deepProject10 #-}
 
-$(liftM concat $ mapM injn [2..10])
-
 -- |Inject a term where the outermost layer is a sub signature. If the signature
 -- @g@ is compound of /n/ atomic signatures, use @inject@/n/ instead.
 inject :: (g :<: f) => g (Cxt h f a) :-> Cxt h f a
 inject = Term . inj
 
-$(liftM concat $ mapM injectn [2..10])
 
 -- |Inject a term over a sub signature to a term over larger signature. If the
 -- signature @g@ is compound of /n/ atomic signatures, use @deepInject@/n/
@@ -148,17 +76,11 @@
 {-# INLINE deepInject #-}
 deepInject = appSigFun inj
 
-$(liftM concat $ mapM deepInjectn [2..10])
-{-# INLINE deepInject2 #-}
-{-# INLINE deepInject3 #-}
-{-# INLINE deepInject4 #-}
-{-# INLINE deepInject5 #-}
-{-# INLINE deepInject6 #-}
-{-# INLINE deepInject7 #-}
-{-# INLINE deepInject8 #-}
-{-# INLINE deepInject9 #-}
-{-# INLINE deepInject10 #-}
 
+split :: (f :=: f1 :+: f2) => (f1 (Term f) :-> a) -> (f2 (Term f) :-> a) -> Term f :-> a
+split f1 f2 (Term t) = spl f1 f2 t
+
+
 -- | This function injects a whole context into another context.
 injectCxt :: (HFunctor g, g :<: f) => Cxt h' g (Cxt h f a) :-> Cxt h f a
 injectCxt = cata' inject
@@ -177,15 +99,6 @@
 
 injectConst :: (HFunctor g, g :<: f) => Const g :-> Cxt h f a
 injectConst = inject . hfmap (const undefined)
-
-injectConst2 :: (HFunctor f1, HFunctor f2, HFunctor g, f1 :<: g, f2 :<: g)
-               => Const (f1 :+: f2) :-> Cxt h g a
-injectConst2 = inject2 . hfmap (const undefined)
-
-injectConst3 :: (HFunctor f1, HFunctor f2, HFunctor f3, HFunctor g,
-                   f1 :<: g, f2 :<: g, f3 :<: g)
-               => Const (f1 :+: f2 :+: f3) :-> Cxt h g a
-injectConst3 = inject3 . hfmap (const undefined)
 
 projectConst :: (HFunctor g, g :<: f) => NatM Maybe (Cxt h f a) (Const g)
 projectConst = fmap (hfmap (const (K ()))) . project
diff --git a/src/Data/Comp/Ops.hs b/src/Data/Comp/Ops.hs
--- a/src/Data/Comp/Ops.hs
+++ b/src/Data/Comp/Ops.hs
@@ -1,7 +1,7 @@
-{-# LANGUAGE TypeOperators, MultiParamTypeClasses, IncoherentInstances,
+{-# LANGUAGE TypeOperators, MultiParamTypeClasses,
              FlexibleInstances, FlexibleContexts, GADTs, TypeSynonymInstances,
              ScopedTypeVariables, FunctionalDependencies, UndecidableInstances,
-             TypeFamilies, DataKinds, ConstraintKinds #-}
+             TypeFamilies, DataKinds, ConstraintKinds, PolyKinds #-}
 
 --------------------------------------------------------------------------------
 -- |
@@ -81,115 +81,96 @@
 infixl 5 :<:
 infixl 5 :=:
 
-data Pos = Here | GoLeft Pos | GoRight Pos | Sum Pos Pos
-data Emb = NotFound | Ambiguous | Found Pos
+data Pos = Here | Le Pos | Ri Pos | Sum Pos Pos
+data Emb = Found Pos | NotFound | Ambiguous
 
 
-type family GetEmb (f :: * -> *) (g :: * -> *) :: Emb where
-    GetEmb f f = Found Here
-    GetEmb f (g1 :+: g2) = Pick f (g1 :+: g2) (GetEmb f g1) (GetEmb f g2)
-    GetEmb f g = NotFound
+type family Elem (f :: * -> *) (g :: * -> *) :: Emb where
+    Elem f f = Found Here
+    Elem f (g1 :+: g2) = Choose f (g1 :+: g2) (Elem f g1) (Elem f g2)
+    Elem f g = NotFound
 
 
-type family Pick f g (e1 :: Emb) (r :: Emb) :: Emb where
-    Pick f g (Found x) (Found y) = Ambiguous
-    Pick f g Ambiguous y = Ambiguous
-    Pick f g x Ambiguous = Ambiguous
-    Pick f g (Found x) y = Found (GoLeft x)
-    Pick f g x (Found y) = Found (GoRight y)
-    Pick f g x y = Split f g
+type family Choose f g (e1 :: Emb) (r :: Emb) :: Emb where
+    Choose f g (Found x) (Found y) = Ambiguous
+    Choose f g Ambiguous y = Ambiguous
+    Choose f g x Ambiguous = Ambiguous
+    Choose f g (Found x) y = Found (Le x)
+    Choose f g x (Found y) = Found (Ri y)
+    Choose (f1 :+: f2) g x y =  Sum' (Elem f1 g) (Elem f2 g) 
+    Choose f g x y = NotFound
 
-type family Split (f :: * -> *) (g :: * -> *) :: Emb where
-    Split (f1 :+: f2) g = Pick2 (GetEmb f1 g) (GetEmb f2 g) 
-    Split f g = NotFound
 
-type family Pick2 (e1 :: Emb) (r :: Emb) :: Emb where
-    Pick2 (Found x) (Found y) = Found (Sum x y)
-    Pick2 Ambiguous y = Ambiguous
-    Pick2 x Ambiguous = Ambiguous
-    Pick2 NotFound y = NotFound
-    Pick2 x NotFound = NotFound
+type family Sum' (e1 :: Emb) (r :: Emb) :: Emb where
+    Sum' (Found x) (Found y) = Found (Sum x y)
+    Sum' Ambiguous y = Ambiguous
+    Sum' x Ambiguous = Ambiguous
+    Sum' NotFound y = NotFound
+    Sum' x NotFound = NotFound
 
-data EmbD (e :: Emb) (f :: * -> *) (g :: * -> *) where
-    HereD :: EmbD (Found Here) f f
-    GoLeftD :: EmbD (Found p) f g -> EmbD (Found (GoLeft p)) f (g :+: g')
-    GoRightD :: EmbD (Found p) f g -> EmbD (Found (GoRight p)) f (g' :+: g)
-    SumD :: EmbD (Found p1) f1 g -> EmbD (Found p2) f2 g -> EmbD (Found (Sum p1 p2)) (f1 :+: f2) g
+data Proxy a = P
 
-class GetEmbD (e :: Emb) (f :: * -> *) (g :: * -> *) where
-    getEmbD :: EmbD e f g
+class Subsume (e :: Emb) (f :: * -> *) (g :: * -> *) where
+  inj'  :: Proxy e -> f a -> g a
+  prj'  :: Proxy e -> g a -> Maybe (f a)
 
-instance GetEmbD (Found Here) f f where
-    getEmbD = HereD
+instance Subsume (Found Here) f f where
+    inj' _ = id
 
-instance GetEmbD (Found p) f g => GetEmbD (Found (GoLeft p)) f (g :+: g') where
-    getEmbD = GoLeftD getEmbD
+    prj' _ = Just
 
-instance GetEmbD (Found p) f g => GetEmbD (Found (GoRight p)) f (g' :+: g) where
-    getEmbD = GoRightD getEmbD
+instance Subsume (Found p) f g => Subsume (Found (Le p)) f (g :+: g') where
+    inj' _ = Inl . inj' (P :: Proxy (Found p))
+    
+    prj' _ (Inl x) = prj' (P :: Proxy (Found p)) x
+    prj' _ _       = Nothing
 
-instance (GetEmbD (Found p1) f1 g, GetEmbD (Found p2) f2 g) 
-    => GetEmbD (Found (Sum p1 p2)) (f1 :+: f2) g where
-    getEmbD = SumD getEmbD getEmbD
+instance Subsume (Found p) f g => Subsume (Found (Ri p)) f (g' :+: g) where
+    inj' _ = Inr . inj' (P :: Proxy (Found p))
 
+    prj' _ (Inr x) = prj' (P :: Proxy (Found p)) x
+    prj' _ _       = Nothing
+              
+instance (Subsume (Found p1) f1 g, Subsume (Found p2) f2 g) 
+    => Subsume (Found (Sum p1 p2)) (f1 :+: f2) g where
+    inj' _ (Inl x) = inj' (P :: Proxy (Found p1)) x
+    inj' _ (Inr x) = inj' (P :: Proxy (Found p2)) x
 
--- The following definitions are used to reject instances of :<: such
--- as @F :+: F :<: F@ or @F :+: (F :+: G) :<: F :+: G@.
+    prj' _ x = case prj' (P :: Proxy (Found p1)) x of
+                 Just y -> Just (Inl y)
+                 _      -> case prj' (P :: Proxy (Found p2)) x of
+                             Just y -> Just (Inr y)
+                             _      -> Nothing
 
-data SimpPos = SimpHere | SimpLeft SimpPos | SimpRight SimpPos
 
-data Res = CompPos SimpPos Pos | SingPos SimpPos
+type family Or (a :: Bool) (b :: Bool) :: Bool where
+    Or  False  False  = False
+    Or  a      b      = True
 
+type family AnyDupl f g where
+    AnyDupl f f = False -- ignore check for duplication if subsumption is reflexive
+    AnyDupl f g = Or (Dupl f '[]) (Dupl g '[])
 
-type family DestrPos (e :: Pos) :: Res where
-    DestrPos (GoLeft e) = ResLeft (DestrPos e)
-    DestrPos (GoRight e) = ResRight (DestrPos e)
-    DestrPos (Sum e1 e2) = ResSum (DestrPos e1) e2
-    DestrPos Here = SingPos SimpHere
+type family Dupl (f :: * -> *) (l :: [* -> *]) :: Bool where
+    Dupl (f :+: g) l = Dupl f (g ': l)
+    Dupl f l         = Or (Find f l) (Dupl' l)
 
-type family ResLeft (r :: Res) :: Res where
-    ResLeft (CompPos p e) = CompPos (SimpLeft p) (GoLeft e)
-    ResLeft (SingPos p) = SingPos (SimpLeft p)
+type family Dupl' (l :: [* -> *]) :: Bool where
+    Dupl' (f ': l) = Or (Dupl f l) (Dupl' l)
+    Dupl' '[]      = False
 
-type family ResRight (r :: Res) :: Res where
-    ResRight (CompPos p e) = CompPos (SimpRight p) (GoRight e)
-    ResRight (SingPos p) = SingPos (SimpRight p)
+type family Find (f :: * -> *) (l :: [* -> *]) :: Bool where
+    Find f (g ': l) = Or (Find' f g) (Find f l)
+    Find f '[]       = False
 
-type family ResSum (r :: Res) (e :: Pos) :: Res where
-    ResSum (CompPos p e1) e2 = CompPos p (Sum e1 e2)
-    ResSum (SingPos p) e = CompPos p e
+type family Find' (f :: * -> *) (g :: * -> *) :: Bool where
+    Find' f (g1 :+: g2) = Or (Find' f g1) (Find' f g2)
+    Find' f f = True
+    Find' f g = False
 
-type family Or x y where
-    Or x False = x
-    Or False y = y
-    Or x y  = True
 
-type family In (p :: SimpPos) (e :: Pos) :: Bool where
-    In SimpHere e = True
-    In p Here = True
-    In (SimpLeft p) (GoLeft e) = In p e
-    In (SimpRight p) (GoRight e) = In p e
-    In p (Sum e1 e2) = Or (In p e1)  (In p e2)
-    In p e = False
-
-type family Duplicates' (r :: Res) :: Bool where
-    Duplicates' (SingPos p) = False
-    Duplicates' (CompPos p e) = Or (In p e) (Duplicates' (DestrPos e))
-
-type family Duplicates (e :: Emb) where
-    Duplicates (Found p) = Duplicates' (DestrPos p)
-
--- This class is used to produce more informative error messages
-class NoDup (b :: Bool) (f :: * -> *) (g :: * -> *)
-instance NoDup False f g
-
-inj_ :: EmbD e f g -> f a -> g a
-inj_ HereD x = x
-inj_ (GoLeftD e) x = Inl (inj_ e x)
-inj_ (GoRightD e) x = Inr (inj_ e x)
-inj_ (SumD e1 e2) x = case x of
-                        Inl y -> inj_ e1 y
-                        Inr y -> inj_ e2 y
+class NoDupl f g s
+instance NoDupl f g False
 
 -- | The :<: constraint is a conjunction of two constraints. The first
 -- one is used to construct the evidence that is used to implement the
@@ -199,33 +180,20 @@
 -- sub-signature on the left-hand side. Such instances are usually
 -- unintended and yield injection functions that are not
 -- injective. The second constraint excludes such instances.
-type f :<: g = (GetEmbD (GetEmb f g) f g, NoDup (Duplicates (GetEmb f g)) f g)
+type f :<: g = (Subsume (Elem f g) f g, 
+                NoDupl f g (AnyDupl f g))
 
 inj :: forall f g a . (f :<: g) => f a -> g a
-inj = inj_ (getEmbD :: EmbD (GetEmb f g) f g)
+inj = inj' (P :: Proxy (Elem f g))
 
+proj :: forall f g a . (f :<: g) => g a -> Maybe (f a)
+proj = prj' (P :: Proxy (Elem f g))
+
 type f :=: g = (f :<: g, g :<: f) 
 
 
-proj_ :: EmbD e f g -> g a -> Maybe (f a)
-proj_ HereD x = Just x
-proj_ (GoLeftD p) x = case x of 
-                        Inl y -> proj_ p y
-                        _ -> Nothing
-proj_ (GoRightD p) x = case x of 
-                          Inr x -> proj_ p x
-                          _ -> Nothing
-proj_ (SumD p1 p2) x = case proj_ p1 x of
-                         Just y -> Just (Inl y)
-                         _ -> case proj_ p2 x of
-                                Just y -> Just (Inr y)
-                                _ -> Nothing
 
-
-proj :: forall f g a . (f :<: g) => g a -> Maybe (f a)
-proj = proj_ (getEmbD :: EmbD (GetEmb f g) f g)
-
-spl :: (f :<: f1 :+: f2) => (f1 a -> b) -> (f2 a -> b) -> f a -> b
+spl :: (f :=: f1 :+: f2) => (f1 a -> b) -> (f2 a -> b) -> f a -> b
 spl f1 f2 x = case inj x of 
             Inl y -> f1 y
             Inr y -> f2 y
diff --git a/src/Data/Comp/Sum.hs b/src/Data/Comp/Sum.hs
--- a/src/Data/Comp/Sum.hs
+++ b/src/Data/Comp/Sum.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators, MultiParamTypeClasses, IncoherentInstances,
+{-# LANGUAGE TypeOperators, MultiParamTypeClasses, OverlappingInstances,
   FlexibleInstances, FlexibleContexts, GADTs, TypeSynonymInstances,
   ScopedTypeVariables, TemplateHaskell, ConstraintKinds, Rank2Types #-}
 --------------------------------------------------------------------------------
@@ -20,6 +20,7 @@
      (:=:),
      (:+:),
      caseF,
+     Proxy (..),
 
      -- * Projections for Signatures and Terms
      proj,
@@ -51,7 +52,6 @@
 import Data.Comp.Ops
 
 import Control.Monad hiding (mapM,sequence)
-import Control.Applicative (Applicative (..))
 import Prelude hiding (mapM,sequence)
 
 import Data.Maybe
@@ -113,7 +113,7 @@
 deepInject_ f = appSigFun f
 
 
-split :: (f :<: f1 :+: f2) => (f1 (Term f) -> a) -> (f2 (Term f) -> a) -> Term f -> a
+split :: (f :=: f1 :+: f2) => (f1 (Term f) -> a) -> (f2 (Term f) -> a) -> Term f -> a
 split f1 f2 (Term t) = spl f1 f2 t
 
 injectConst :: (Functor g, g :<: f) => Const g -> Cxt h f a
diff --git a/src/Data/Comp/TermRewriting.hs b/src/Data/Comp/TermRewriting.hs
--- a/src/Data/Comp/TermRewriting.hs
+++ b/src/Data/Comp/TermRewriting.hs
diff --git a/src/Data/Comp/Thunk.hs b/src/Data/Comp/Thunk.hs
--- a/src/Data/Comp/Thunk.hs
+++ b/src/Data/Comp/Thunk.hs
@@ -18,7 +18,6 @@
     (TermT
     ,CxtT
     ,thunk
-    ,injectT
     ,whnf
     ,whnf'
     ,whnfPr
@@ -63,10 +62,6 @@
 -- | This function turns a monadic computation into a thunk.
 thunk :: m (CxtT m h f a) -> CxtT m h f a
 thunk = inject_ Inl
-
--- | Variant of 'inject' for the typex 'CxtT' and 'TermT'.
-injectT :: (g :<: f) => g (CxtT m h f a) -> CxtT m h f a
-injectT = inject_ (Inr . inj)
 
 -- | This function evaluates all thunks until a non-thunk node is
 -- found.
diff --git a/testsuite/tests/Data/Comp/Multi/Variables_Test.hs b/testsuite/tests/Data/Comp/Multi/Variables_Test.hs
--- a/testsuite/tests/Data/Comp/Multi/Variables_Test.hs
+++ b/testsuite/tests/Data/Comp/Multi/Variables_Test.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE TemplateHaskell, TypeSynonymInstances, FlexibleInstances,
 MultiParamTypeClasses, TypeOperators, FlexibleContexts , RankNTypes,
-GADTs, ScopedTypeVariables, EmptyDataDecls#-}
+GADTs, ScopedTypeVariables, EmptyDataDecls, ConstraintKinds #-}
 
 module Data.Comp.Multi.Variables_Test where