diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2015, Emil Axelsson
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Emil Axelsson nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,6 @@
+This package gives a generic implementation of higher-order rewriting. The main idea is to use techniques from embedded domain-specific languages to offer an interface which is both safe and syntactically appealing.
+
+Some examples are found in the [examples directory](examples). For more information, see "Lightweight Higher-Order Rewriting in Haskell":
+
+  * [Paper](http://www.cse.chalmers.se/~emax/documents/axelsson2015lightweight_DRAFT.pdf)
+  * [Slides](http://www.cse.chalmers.se/~emax/documents/axelsson2015lightweight_slides.pdf)
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/examples/Feldspar.hs b/examples/Feldspar.hs
new file mode 100644
--- /dev/null
+++ b/examples/Feldspar.hs
@@ -0,0 +1,117 @@
+{-# LANGUAGE DeriveFoldable #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{-# OPTIONS_GHC -fno-warn-missing-methods #-}
+
+import Data.Comp
+import Data.Comp.Derive
+import Data.Comp.Render
+
+import Data.Rewriting.Rules
+import Data.Rewriting.HigherOrder
+
+import Simple
+
+
+
+main = return () -- For `cabal test`
+
+data FORLOOP a = ForLoop a a a
+  deriving (Eq, Show, Functor, Foldable, Traversable)
+
+derive [makeEqF, makeShowF, makeShowConstr] [''FORLOOP]
+
+instance Render FORLOOP
+
+type Feld = VAR :+: LAM :+: APP :+: NUM :+: LOGIC :+: FORLOOP
+
+newtype Data a = Data { unData :: Term Feld }
+  deriving (Eq, Show)
+
+instance Rep Data
+  where
+    type PF Data = Feld
+    toRep   = Data
+    fromRep = unData
+
+type instance Var Data = Data
+
+instance Bind Data
+  where
+    var = id
+    lam = mkLam (Data . inject . Var . toInteger)
+
+deriving instance Num a => Num (Data a)
+
+class ForLoop r
+  where
+    forLoop_ :: r Int -> r s -> r (Int -> s -> s) -> r s
+
+instance (Rep r, FORLOOP :<: PF r) => ForLoop r
+  where
+    forLoop_ len init step = toRep $ inject $ ForLoop (fromRep len) (fromRep init) (fromRep step)
+
+forLoop :: (ForLoop r, Bind r) => r Int -> r s -> (Var r Int -> Var r s -> r s) -> r s
+forLoop len init body = forLoop_ len init (lam $ \i -> lam $ \s -> body i s)
+
+-- forLoop 0 init _  ===>  init
+rule_for1 init = forLoop 0 (mvar init) (\i s -> __)  ===>  mvar init
+
+-- forLoop 0 init (\i s -> s)  ===>  init
+rule_for2 init = forLoop __ (mvar init) (\i s -> var s)  ===>  mvar init
+
+rule_for3 len init body =
+    forLoop (mvar len) (mvar init) (\i s -> body -$- i)
+      ===>
+    cond (mvar len === 0) (mvar init) (body -$- (mvar len - 1))
+
+rulesFeld = rules ++
+    [ quantify rule_for1
+    , quantify rule_for2
+    , quantify rule_for3
+    ]
+
+stripAnn :: Functor f => Term (f :&: a) -> Term f
+stripAnn = cata (\(f :&: _) -> Term f)
+
+forExample :: Data Int -> Data Int
+forExample a
+    = forLoop (a-a) a (\i s -> i*s+70)
+    + forLoop a a (\i s -> i*i+100)
+
+drawForExample  = drawTerm $ unData $ lam forExample
+drawForExampleR = drawTerm $ stripAnn $ bottomUp app rulesFeld $ unData $ lam forExample
+
+feld1 :: Data Int -> Data Int
+feld1 a = a + a + 3
+
+drawFeld1  = drawTerm $ unData $ lam feld1
+drawFeld1R = drawTerm $ stripAnn $ bottomUp app rulesFeld $ unData $ lam feld1
+
+feld2 :: Data Int
+feld2 = forLoop 0 0 (+)
+
+drawFeld2  = drawTerm $ unData feld2
+drawFeld2R = drawTerm $ stripAnn $ bottomUp app rulesFeld $ unData feld2
+
+feld3 :: Data Int -> Data Int
+feld3 a = forLoop a 0 (\i s -> a+i)
+
+drawFeld3  = drawTerm $ unData $ lam feld3
+drawFeld3R = drawTerm $ stripAnn $ bottomUp app rulesFeld $ unData $ lam feld3
+
+feld4 :: Data Int -> Data Int
+feld4 a = forLoop a 0 (\i s -> a + i + s) + forLoop a 0 (\i s -> a + i + s)
+
+drawFeld4  = drawTerm $ unData $ lam feld4
+drawFeld4R = drawTerm $ stripAnn $ bottomUp app rulesFeld $ unData $ lam feld4
+
diff --git a/examples/Simple.hs b/examples/Simple.hs
new file mode 100644
--- /dev/null
+++ b/examples/Simple.hs
@@ -0,0 +1,158 @@
+{-# LANGUAGE DeriveFoldable #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{-# OPTIONS_GHC -fno-warn-missing-methods #-}
+
+module Simple where
+
+
+
+import Data.Comp
+import Data.Comp.Derive
+import Data.Comp.Render
+import Data.Patch
+
+import Data.Rewriting.Rules
+import Data.Rewriting.FirstOrder
+
+
+
+-- Using the `Num` class as a tagless DSL:
+
+-- 0 + x  ===>  x
+rule_add1 x = 0 + mvar x  ===>  mvar x
+
+rule_add1
+    :: (Num (lhs a), MetaVar lhs, MetaVar rhs, MetaRep lhs ~ MetaRep rhs)
+    => MetaRep rhs a -> Rule lhs rhs
+
+-- x + x  ===>  x*2
+rule_add2 x = mvar x + mvar x  ===>  mvar x * 2
+
+-- x - x  ===>  0
+rule_sub x = mvar x - mvar x  ===>  0
+
+-- 0 * x  ===>  0
+rule_mul = 0 * __  ===>  (0 -:: tCon tInteger)
+  -- Rules cannot be polymorphic
+
+-- Adding language constructs for "logic" expressions:
+
+class Logic r
+  where
+    false :: r Bool
+    true  :: r Bool
+    noT   :: r Bool -> r Bool
+    (<&>) :: r Bool -> r Bool -> r Bool
+    (===) :: Eq a => r a -> r a -> r Bool
+    cond  :: r Bool -> r a -> r a -> r a
+
+-- not (not x)  ===>  x
+rule_not x = noT (noT (mvar x))  ===>  mvar x
+
+-- false <&> x  ===>  false
+rule_and x = false <&> mvar x  ===>  false
+
+-- x === x  ===>  true
+rule_eq x = mvar x === mvar x  ===>  true
+
+-- cond _ tf tf  ===>  tf
+rule_cond1 tf = cond __ (mvar tf) (mvar tf)  ===>  mvar tf
+
+-- cond (not c) t f  ===>  cond c f t
+rule_cond2 c t f = cond (noT (mvar c)) (mvar t) (mvar f)  ===>  cond (mvar c) (mvar f) (mvar t)
+
+data NUM a
+    = Num Integer
+    | Add a a
+    | Sub a a
+    | Mul a a
+  deriving (Eq, Show, Functor, Foldable, Traversable)
+
+derive [makeEqF, makeShowF, makeShowConstr] [''NUM]
+
+instance Render NUM
+
+data LOGIC a
+    = Bool Bool
+    | Not a
+    | And a a
+    | Equal a a
+    | Cond a a a
+  deriving (Eq, Show, Functor, Foldable, Traversable)
+
+derive [makeEqF, makeShowF, makeShowConstr] [''LOGIC]
+
+instance Render LOGIC
+
+type Lang = NUM :+: LOGIC
+
+newtype Expr a = Expr { unExpr :: Term Lang }
+  deriving (Eq, Show)
+
+instance Rep Expr
+  where
+    type PF Expr = Lang
+    toRep   = Expr
+    fromRep = unExpr
+
+instance (NUM :<: f) => Num (Term f)
+  where
+    fromInteger = inject . Num
+    a + b       = inject $ Add a b
+    a - b       = inject $ Sub a b
+    a * b       = inject $ Mul a b
+
+deriving instance Num a => Num (Expr a)
+
+deriving instance (NUM :<: PF (LHS f), Num a) => Num (LHS f a)
+deriving instance (NUM :<: PF (RHS f), Num a) => Num (RHS f a)
+
+instance (Rep r, LOGIC :<: PF r) => Logic r
+  where
+    false      = toRep $ inject (Bool False)
+    true       = toRep $ inject (Bool True)
+    noT        = toRep . inject . Not . fromRep
+    a <&> b    = toRep $ inject $ And (fromRep a) (fromRep b)
+    a === b    = toRep $ inject $ Equal (fromRep a) (fromRep b)
+    cond c t f = toRep $ inject $ Cond (fromRep c) (fromRep t) (fromRep f)
+
+rules =
+    [ quantify rule_add1
+    , quantify rule_add2
+    , quantify rule_sub
+    , quantify rule_mul
+    , quantify rule_and
+    , quantify (rule_eq -:: tCon tA >-> tRule)
+    , quantify rule_cond1
+    , quantify rule_cond2
+    ]
+
+expr1 :: Expr Integer
+expr1 = 0 + 4
+
+draw1  = drawTerm $ unExpr expr1
+draw1R = drawTerm $ bottomUp rules (unExpr expr1)
+
+expr2 :: Expr Integer
+expr2 = (5 + 5 + 3) + (0 + 4)
+
+draw2  = drawTerm $ unExpr expr2
+draw2R = drawTerm $ bottomUp rules (unExpr expr2)
+
+expr3 :: Expr Integer
+expr3 = cond (0 === 1) (5+5) (5*2)
+
+draw3  = drawTerm $ unExpr expr3
+draw3R = drawTerm $ bottomUp rules (unExpr expr3)
+
diff --git a/ho-rewriting.cabal b/ho-rewriting.cabal
new file mode 100644
--- /dev/null
+++ b/ho-rewriting.cabal
@@ -0,0 +1,85 @@
+name:                ho-rewriting
+version:             0.1
+synopsis:            Generic rewrite rules with safe treatment of variables and binders
+description:         This package gives a generic implementation of higher-order
+                     rewriting. The main idea is to use techniques from embedded
+                     domain-specific languages to offer an interface which is
+                     both safe and syntactically appealing.
+                     .
+                     Some examples are found in the @examples@ directory. For
+                     more information, see
+                     "Lightweight Higher-Order Rewriting in Haskell" (presented at TFP 2015):
+                     .
+                       * Paper: <http://www.cse.chalmers.se/~emax/documents/axelsson2015lightweight_DRAFT.pdf>
+                     .
+                       * Slides: <http://www.cse.chalmers.se/~emax/documents/axelsson2015lightweight_slides.pdf>
+homepage:            https://github.com/emilaxelsson/ho-rewriting
+bug-reports:         https://github.com/emilaxelsson/ho-rewriting/issues
+license:             BSD3
+license-file:        LICENSE
+author:              Emil Axelsson
+maintainer:          emax@chalmers.se
+copyright:           Copyright (c) 2015, Emil Axelsson
+category:            Language
+build-type:          Simple
+extra-source-files:  README.md
+cabal-version:       >=1.10
+
+extra-source-files:
+  examples/*.hs
+
+source-repository head
+  type:     git
+  location: https://github.com/emilaxelsson/ho-rewriting
+
+library
+  exposed-modules:
+    Data.Rewriting.Rules
+    Data.Rewriting.FirstOrder
+    Data.Rewriting.HigherOrder
+
+  hs-source-dirs:
+    src
+
+  build-depends:
+    base >=4.7 && <5,
+    containers,
+    compdata >=0.9,
+    mtl,
+    patch-combinators
+
+  default-language: Haskell2010
+
+  default-extensions:
+    DeriveFoldable
+    DeriveFunctor
+    DeriveTraversable
+    FlexibleContexts
+    GeneralizedNewtypeDeriving
+    ScopedTypeVariables
+    TypeFamilies
+    TypeOperators
+
+  other-extensions:
+    NoMonomorphismRestriction
+    TemplateHaskell
+    TupleSections
+    UndecidableInstances
+
+  default-language:
+    Haskell2010
+
+test-suite examples
+  type: exitcode-stdio-1.0
+
+  hs-source-dirs: examples
+
+  main-is: Feldspar.hs
+
+  build-depends:
+    base,
+    compdata,
+    ho-rewriting,
+    patch-combinators
+
+  default-language: Haskell2010
diff --git a/src/Data/Rewriting/FirstOrder.hs b/src/Data/Rewriting/FirstOrder.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Rewriting/FirstOrder.hs
@@ -0,0 +1,92 @@
+{-# LANGUAGE TupleSections #-}
+
+-- | First-order rewriting
+module Data.Rewriting.FirstOrder where
+
+
+
+import Control.Monad.Reader
+import Control.Monad.Writer
+import Data.Foldable (Foldable)
+import Data.Function (on)
+import Data.List (groupBy)
+import Data.Traversable (Traversable)
+
+import Data.Comp
+import Data.Comp.Ops
+
+import Data.Rewriting.Rules
+
+
+
+-- | First-order matching. Results in a list of candidate mappings.
+--
+-- This function assumes that there are no applications of meta-variables in `LHS`.
+matchM :: (Functor f, Foldable f, EqF f) => LHS f a -> Term f -> WriterT (Subst f) Maybe ()
+matchM (LHS lhs) t = go lhs t
+  where
+    go (Term (Inl WildCard)) _                       = return ()
+    go (Term (Inr (Inl (Meta (MVar (MetaId v)))))) t = tell [(v,t)]
+    go (Term (Inr (Inr f))) (Term g)
+      | Just subs <- eqMod f g                       = mapM_ (uncurry go) subs
+    go _ _                                           = fail "No match"
+
+-- | Check if all terms are equal, and if so, return one of them
+solveTerm :: EqF f => [Term f] -> Maybe (Term f)
+solveTerm (t:ts) = guard (all (==t) ts) >> return t
+solveTerm _      = Nothing
+
+-- | Turn a list of candidate mappings into a substitution. Succeeds iff. all mappings for the same
+-- variable are equal.
+solveSubst :: EqF f => [(Name, Term f)] -> Maybe (Subst f)
+solveSubst s = sequence [fmap (v,) $ solveTerm ts | g <- gs, let (v:_,ts) = unzip g]
+  where
+    gs = groupBy ((==) `on` fst) s
+      -- TODO Make O(n * log n)
+
+-- | First-order matching. Succeeds if the pattern matches and all occurrences of a given
+-- meta-variable are matched against equal terms.
+--
+-- This function assumes that there are no applications of meta-variables in `LHS`.
+match :: (Functor f, Foldable f, EqF f) => LHS f a -> Term f -> Maybe (Subst f)
+match lhs = solveSubst <=< execWriterT . matchM lhs
+
+-- | Naive substitution. Succeeds iff. each meta-variable in 'RHS' has a mapping in the
+-- substitution.
+--
+-- This function assumes that there are no applications of meta-variables in `RHS`.
+substitute :: Traversable f => Subst f -> RHS f a -> Maybe (Term f)
+substitute subst = cataM go . unRHS
+  where
+    go (Inl (Meta (MVar (MetaId v)))) = lookup v subst
+    go (Inr f)                        = return (Term f)
+
+-- | Apply a rule. Succeeds iff. both matching and substitution succeeds.
+--
+-- This function assumes that there are no applications of meta-variables in `LHS` or `RHS`.
+rewrite :: (Traversable f, EqF f) => Rule (LHS f) (RHS f) -> Term f -> Maybe (Term f)
+rewrite (Rule lhs rhs) t = do
+    subst <- match lhs t
+    substitute subst rhs
+
+-- | Apply the first succeeding rule from a list of rules. If no rule succeeds the term is returned
+-- unchanged.
+--
+-- This function assumes that there are no applications of meta-variables in `LHS` or `RHS`.
+applyFirst :: (Traversable f, EqF f) => [Rule (LHS f) (RHS f)] -> Term f -> Term f
+applyFirst rs t = case [t' | r <- rs, Just t' <- [rewrite r t]] of
+    t':_ -> t'
+    _    -> t
+
+-- | Apply a list of rules bottom-up across a term
+--
+-- This function assumes that there are no applications of meta-variables in `LHS` or `RHS`.
+bottomUp :: (Traversable f, EqF f) => [Rule (LHS f) (RHS f)] -> Term f -> Term f
+bottomUp rs = applyFirst rs . Term . fmap (bottomUp rs) . unTerm
+
+-- | Apply a list of rules top-down across a term
+--
+-- This function assumes that there are no applications of meta-variables in `LHS` or `RHS`.
+topDown :: (Traversable f, EqF f) => [Rule (LHS f) (RHS f)] -> Term f -> Term f
+topDown rs = Term . fmap (topDown rs) . unTerm . applyFirst rs
+
diff --git a/src/Data/Rewriting/HigherOrder.hs b/src/Data/Rewriting/HigherOrder.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Rewriting/HigherOrder.hs
@@ -0,0 +1,304 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | Higher-order rewriting
+module Data.Rewriting.HigherOrder where
+
+
+
+import Control.Monad.Reader
+import Control.Monad.Writer
+import qualified Data.Foldable as Foldable
+import Data.Function (on)
+import Data.List (groupBy)
+import Data.Map (Map)
+import qualified Data.Map as Map
+import Data.Set (Set)
+import qualified Data.Set as Set
+
+import Data.Comp
+import Data.Comp.Derive
+import Data.Comp.Ops
+import Data.Comp.Render
+
+import Data.Rewriting.Rules
+
+
+
+-- | Representations supporting variable binding
+class Bind r
+  where
+    var :: Var r a -> r a
+    lam :: (Var r a -> r b) -> r (a -> b)
+
+-- | Functor representing object variables
+newtype VAR a = Var Name
+  deriving (Eq, Show, Ord, Num, Enum, Real, Integral, Functor, Foldable, Traversable)
+
+-- | Functor representing lambda abstraction
+data LAM a = Lam Name a
+  deriving (Eq, Show, Functor, Foldable, Traversable)
+
+-- | Functor representing application
+data APP a = App a a
+  deriving (Eq, Show, Functor, Foldable, Traversable)
+
+derive [makeEqF, makeShowF, makeShowConstr] [''VAR]
+derive [makeEqF, makeShowF, makeShowConstr] [''LAM]
+derive [makeEqF, makeShowF, makeShowConstr] [''APP]
+
+instance Render VAR
+instance Render LAM
+instance Render APP
+
+fresh :: (LAM :<: f, Functor f, Foldable f) => Term f -> Name
+fresh f
+    | Just (Lam v _) <- project f = v+1
+    | otherwise = maximum $ (0:) $ Foldable.toList $ fmap fresh $ unTerm f
+
+-- | Generic lambda abstraction
+mkLam
+    :: (Rep r, VAR :<: PF r, LAM :<: PF r, Functor (PF r), Foldable (PF r))
+    => (VAR a -> Var r a) -> (Var r a -> r b) -> r (a -> b)
+mkLam mkVar f = toRep $ inject $ Lam v $ fromRep body
+  where
+    body = f (mkVar $ Var v)
+    v    = fresh (fromRep body)
+
+-- | Application operator, to use as argument to functions like 'applyFirst', 'bottomUp', etc.
+app :: (APP :<: f) => Term (f :&: Set Name) -> Term (f :&: Set Name) -> Term (f :&: Set Name)
+app f@(Term (_ :&: fv)) a@(Term (_ :&: av)) = Term (inj (App f a) :&: Set.union fv av)
+
+type instance Var (LHS f) = VAR
+type instance Var (RHS f) = VAR
+
+instance (VAR :<: PF (LHS f), LAM :<: PF (LHS f), Functor f, Foldable f) =>
+    Bind (LHS f)
+  where
+    var = LHS . inject . Var . toInteger
+    lam = mkLam id
+
+instance (VAR :<: PF (RHS f), LAM :<: PF (RHS f), Functor f, Foldable f) =>
+    Bind (RHS f)
+  where
+    var = RHS . inject . Var . toInteger
+    lam = mkLam id
+
+-- | One-to-one map
+type OneToOne a b = (Map a b, Map b a)
+
+-- | Empty one-to-one map
+oEmpty :: OneToOne a b
+oEmpty = (Map.empty, Map.empty)
+
+-- | Test if a mapping is in a one-to-one map
+oMember :: (Ord a, Ord b) => (a,b) -> OneToOne a b -> Bool
+oMember (a,b) (ab,_) = case Map.lookup a ab of
+    Just b' -> b == b'
+    Nothing -> False
+
+-- | Test if either side of a mapping is in a one-to-one map
+oMemberEither :: (Ord a, Ord b) => (a,b) -> OneToOne a b -> Bool
+oMemberEither (a,b) (ab,ba) = Map.member a ab || Map.member b ba
+
+-- | Left lookup in a one-to-one map
+oLookupL :: Ord a => a -> OneToOne a b -> Maybe b
+oLookupL a (ab,_) = Map.lookup a ab
+
+-- | Insert a one-to-one mapping
+oInsert :: (Ord a, Ord b) => (a,b) -> OneToOne a b -> OneToOne a b
+oInsert (a,b) (ab,ba) = (Map.insert a b ab', Map.insert b a ba')
+  where
+    ab' = case Map.lookup b ba of
+      Just a' -> Map.delete a' ab
+      Nothing -> ab
+    ba' = case Map.lookup a ab of
+      Just b' -> Map.delete b' ba
+      Nothing -> ba
+
+getAnn :: Term (f :&: a) -> a
+getAnn (Term (_ :&: a)) = a
+
+-- | Environment keeping track of alpha-renaming
+type AlphaEnv = OneToOne Name {-pattern-} Name {-term-}
+
+-- | Higher-order matching. Results in a list of candidate mappings.
+matchM :: forall f a
+    .  ( VAR :<: f
+       , LAM :<: f
+       , VAR :<: PF (LHS f)
+       , LAM :<: PF (LHS f)
+       , Functor f, Foldable f, EqF f
+       )
+    => LHS f a
+    -> Term (f :&: Set Name)
+    -> ReaderT AlphaEnv (WriterT (Subst (f :&: Set Name)) Maybe) ()
+matchM (LHS lhs) t = go lhs t
+  where
+    go (Term (Inl WildCard)) _ = return ()
+
+    go (Term (Inr (Inl (Meta mv)))) t = ReaderT $ \env -> goo env mv t
+      where
+        goo :: AlphaEnv
+            -> MetaExp (LHS f) b
+            -> Term (f :&: Set Name)
+            -> WriterT (Subst (f :&: Set Name)) Maybe ()
+        goo env (MVar (MetaId m)) t
+            | Set.null (Set.intersection boundInPatt freeIn_t) = tell [(m,t)]
+            | otherwise = fail "Variables would escape"
+          where
+            boundInPatt = Map.keysSet $ snd env
+            freeIn_t    = getAnn t
+        goo env (MApp mv (Var v)) t = do
+          let Just w = oLookupL v env
+                -- Lookup failure is a bug rather than a matching failure
+          goo env mv (Term (inj (Lam w t) :&: Set.delete w (getAnn t)))
+
+    go p (Term (g :&: _))
+      | Just (Var v) <- project p
+      , Just (Var w) <- proj g
+      = do
+          env <- ask
+          guard ((v,w) `oMember` env)
+            -- Rules should be closed, so `w` can't be free
+
+    go p (Term (g :&: _))
+      | Just (Lam v a) <- project p
+      , Just (Lam w b) <- proj g
+      = local (oInsert (v,w)) $ go a b
+
+    go (Term (Inr (Inr f))) (Term (g :&: _))
+      | Just subs <- eqMod f g
+      = mapM_ (uncurry go) subs
+
+    go _ _ = fail "No match"
+
+-- | Alpha-equivalence
+alphaEq :: (VAR :<: f, LAM :<: f, Functor f, Foldable f, EqF f) => Term f -> Term f -> Bool
+alphaEq a b = runReader (go a b) oEmpty
+  where
+    go t u
+      | Just (Var v) <- project t
+      , Just (Var w) <- project u
+      = reader $ \env -> oMember (v,w) env || (not (oMemberEither (v,w) env) && v==w)
+    go t u
+      | Just (Lam v a) <- project t
+      , Just (Lam w b) <- project u
+      = local (oInsert (v,w)) $ go a b
+    go (Term f) (Term g)
+      | Just subs <- eqMod f g
+      = fmap and $ mapM (uncurry go) subs
+    go _ _ = return False
+
+-- | Check if all terms are alpha-equivalent, and if so, return one of them
+solveTermAlpha :: (VAR :<: f, LAM :<: f, Functor f, Foldable f, EqF f) =>
+    [Term (f :&: a)] -> Maybe (Term (f :&: a))
+solveTermAlpha (t:ts) = guard (all (alphaEq (stripA t)) (map stripA ts)) >> return t
+solveTermAlpha _      = Nothing
+
+-- | Turn a list of candidate mappings into a substitution. Succeeds iff. all mappings for the same
+-- variable are alpha-equivalent.
+solveSubstAlpha :: (VAR :<: f, LAM :<: f, Functor f, Foldable f, EqF f) =>
+    Subst (f :&: a) -> Maybe (Subst (f :&: a))
+solveSubstAlpha s = sequence [fmap (v,) $ solveTermAlpha ts | g <- gs, let (v:_,ts) = unzip g]
+  where
+    gs = groupBy ((==) `on` fst) s
+      -- TODO Make O(n * log n)
+
+-- | Higher-order matching. Succeeds if the pattern matches and all occurrences of a given
+-- meta-variable are matched against equal terms.
+match
+    :: ( VAR :<: f
+       , LAM :<: f
+       , VAR :<: PF (LHS f)
+       , LAM :<: PF (LHS f)
+       , Functor f, Foldable f, EqF f
+       )
+    => LHS f a -> Term (f :&: Set Name) -> Maybe (Subst (f :&: Set Name))
+match lhs = solveSubstAlpha <=< execWriterT . flip runReaderT oEmpty . matchM lhs
+
+-- | Annotate a node with its set of free variables
+annFreeVars :: (VAR :<: f, LAM :<: f, Functor f, Foldable f) =>
+    f (Term (f :&: Set Name)) -> Term (f :&: Set Name)
+annFreeVars f
+    | Just (Var v) <- proj f = Term (inj (Var v) :&: Set.singleton v)
+annFreeVars f
+    | Just (Lam v a) <- proj f
+    , vars <- getAnn a
+    = Term (inj (Lam v a) :&: Set.delete v vars)
+annFreeVars f = Term (f :&: Foldable.foldMap getAnn f)
+
+-- | Capture-avoiding substitution. Succeeds iff. each meta-variable in 'RHS' has a mapping in the
+-- substitution.
+substitute :: forall f g a
+    .  ( VAR :<: f
+       , LAM :<: f
+       , Traversable f
+       , g ~ (f :&: Set Name)
+       )
+    => (Term g -> Term g -> Term g)  -- ^ Application operator
+    -> Subst g
+    -> RHS f a
+    -> Maybe (Term g)
+substitute app subst = cataM go . unRHS
+  where
+    go :: PF (RHS f) (Term g) -> Maybe (Term g)
+    go (Inl (Meta mv)) = goo mv
+      where
+        goo :: MetaExp (RHS f) b -> Maybe (Term g)
+        goo (MVar (MetaId v)) = lookup v subst
+        goo (MApp mv t)       = liftM2 app (goo mv) $ cataM go (unRHS t)
+    go (Inr f) = return $ annFreeVars f
+  -- TODO Should avoid capturing
+
+-- | Apply a rule. Succeeds iff. both matching and substitution succeeds.
+rewrite
+    :: ( VAR :<: f
+       , LAM :<: f
+       , VAR :<: PF (LHS f)
+       , LAM :<: PF (LHS f)
+       , Traversable f, EqF f
+       , g ~ (f :&: Set Name)
+       )
+    => (Term g -> Term g -> Term g)  -- ^ Application operator
+    -> Rule (LHS f) (RHS f)
+    -> Term (f :&: Set Name)
+    -> Maybe (Term (f :&: Set Name))
+rewrite app (Rule lhs rhs) t = do
+    subst <- match lhs t
+    substitute app subst rhs
+
+-- | Apply the first succeeding rule from a list of rules. If no rule succeeds the term is returned
+-- unchanged.
+applyFirst
+    :: ( VAR :<: f
+       , LAM :<: f
+       , VAR :<: PF (LHS f)
+       , LAM :<: PF (LHS f)
+       , Traversable f, EqF f
+       , g ~ (f :&: Set Name)
+       )
+    => (Term g -> Term g -> Term g)  -- ^ Application operator
+    -> [Rule (LHS f) (RHS f)]
+    -> Term (f :&: Set Name)
+    -> Term (f :&: Set Name)
+applyFirst app rs t = case [t' | r <- rs, Just t' <- [rewrite app r t]] of
+    t':_ -> t'
+    _    -> t
+
+-- | Apply a list of rules bottom-up across a term
+bottomUp
+    :: ( VAR :<: f
+       , LAM :<: f
+       , VAR :<: PF (LHS f)
+       , LAM :<: PF (LHS f)
+       , Traversable f, EqF f
+       , g ~ (f :&: Set Name)
+       )
+    => (Term g -> Term g -> Term g)  -- ^ Application operator
+    -> [Rule (LHS f) (RHS f)]
+    -> Term f
+    -> Term (f :&: Set Name)
+bottomUp app rs = applyFirst app rs . annFreeVars . fmap (bottomUp app rs) . unTerm
+
diff --git a/src/Data/Rewriting/Rules.hs b/src/Data/Rewriting/Rules.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Rewriting/Rules.hs
@@ -0,0 +1,208 @@
+{-# LANGUAGE DeriveFoldable #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | Rewrite rules
+module Data.Rewriting.Rules where
+
+
+
+import Control.Applicative (pure)
+import qualified Data.Foldable as Fold
+import Data.Traversable (Traversable (traverse))
+
+import Data.Comp
+import Data.Comp.Derive
+import Data.Comp.Ops
+import Data.Patch
+
+
+
+----------------------------------------------------------------------------------------------------
+-- * Tagless rewrite rules
+----------------------------------------------------------------------------------------------------
+
+-- | Rewrite rules
+data Rule lhs rhs
+  where
+    Rule :: lhs a -> rhs a -> Rule lhs rhs
+
+-- | Construct a rule from an LHS and an RHS
+(===>) :: lhs a -> rhs a -> Rule lhs rhs
+(===>) = Rule
+
+infix 1 ===>
+
+-- | Representations supporting wildcards
+class WildCard r
+  where
+    __ :: r a
+
+-- | Meta-variable applied to a number of 'Var' expressions
+data MetaExp r a
+  where
+    MVar :: MetaRep r a -> MetaExp r a
+    MApp :: MetaExp r (a -> b) -> MetaArg r a -> MetaExp r b
+
+-- | Representations supporting meta-variables
+class MetaVar r
+  where
+    -- Representation of meta-variable identifiers
+    type MetaRep r :: * -> *
+    type MetaArg r :: * -> *
+    metaExp :: MetaExp r a -> r a
+
+-- TODO Move `MetaRep` and `MetaArg` out of the class as in the paper?
+
+-- | Construct a meta-variable
+mvar :: MetaVar r => MetaRep r a -> r a
+mvar = metaExp . MVar
+
+-- | Meta-variable application (used for all but the first and last variable)
+($$) :: MetaExp r (a -> b) -> MetaArg r a -> MetaExp r b
+($$) = MApp
+
+-- | Meta-variable application (used for the last variable)
+($-) :: MetaVar r => MetaExp r (a -> b) -> MetaArg r a -> r b
+f $- a = metaExp (MApp f a)
+
+-- | Meta-variable application (used for the first variable)
+(-$) :: MetaRep r (a -> b) -> MetaArg r a -> MetaExp r b
+f -$ a = MApp (MVar f) a
+
+-- | Meta-variable application (used when there is only variable)
+(-$-) :: MetaVar r => MetaRep r (a -> b) -> MetaArg r a -> r b
+f -$- a = metaExp (MApp (MVar f) a)
+
+infixl 2 $$, $-, -$, -$-
+
+-- | Variable identifier
+type Name = Integer
+
+-- | Typed meta-variable identifiers
+newtype MetaId a = MetaId Name
+  deriving (Eq, Show, Ord, Num, Enum, Real, Integral)
+
+-- | Rules that may take a number of meta-variables as arguments. Those meta-variables are
+-- implicitly forall-quantified.
+class Quantifiable rule
+  where
+    -- | Rule type after quantification
+    type RuleType rule
+
+    -- | Quantify a rule starting from the provided variable identifier
+    quantify' :: Name -> rule -> RuleType rule
+
+-- | Base case: no meta-variables
+instance Quantifiable (Rule lhs rhs)
+  where
+    type RuleType (Rule lhs rhs) = Rule lhs rhs
+    quantify' _ = id
+
+-- | Recursive case: one more meta-variable
+instance (Quantifiable rule, m ~ MetaId a) => Quantifiable (m -> rule)
+  where
+    type RuleType (m -> rule) = RuleType rule
+    quantify' i rule = quantify' (i+1) (rule (MetaId i))
+
+-- | Forall-quantify the meta-variable arguments of a rule
+quantify :: (Quantifiable rule, RuleType rule ~ Rule lhs rhs) => rule -> Rule lhs rhs
+quantify = quantify' 0
+
+
+
+----------------------------------------------------------------------------------------------------
+-- * Representation of rules
+----------------------------------------------------------------------------------------------------
+
+-- | Functor representing wildcards
+data WILD a = WildCard
+  deriving (Eq, Show, Functor, Foldable, Traversable)
+
+-- | Functor representing meta variables applied to a number of 'Var' expressions
+data META r a = forall b . Meta (MetaExp r b)
+
+instance Functor     (META r) where fmap f (Meta m) = Meta m
+instance Foldable    (META r) where foldr _ a _ = a
+instance Traversable (META r) where traverse _ (Meta m) = pure (Meta m)
+
+-- | Left hand side of a rule
+newtype LHS f a = LHS { unLHS :: Term (WILD :+: META (LHS f) :+: f) }
+
+-- | Right hand side of a rule
+newtype RHS f a = RHS { unRHS :: Term (META (RHS f) :+: f) }
+
+instance WildCard (LHS f)
+  where
+    __ = LHS $ Term $ Inl WildCard
+
+-- | Representation of object variables
+type family Var (r :: * -> *) :: * -> *
+
+instance MetaVar (LHS f)
+  where
+    type MetaRep (LHS f) = MetaId
+    type MetaArg (LHS f) = Var (LHS f)
+    metaExp = LHS . Term . Inr . Inl . Meta
+
+instance MetaVar (RHS f)
+  where
+    type MetaRep (RHS f) = MetaId
+    type MetaArg (RHS f) = RHS f
+    metaExp = RHS . Term . Inl . Meta
+
+
+
+----------------------------------------------------------------------------------------------------
+-- * Generalize over representations
+----------------------------------------------------------------------------------------------------
+
+class Rep r
+  where
+    type PF r :: * -> *
+    toRep   :: Term (PF r) -> r a
+    fromRep :: r a -> Term (PF r)
+
+instance Rep (LHS f)
+  where
+    type PF (LHS f) = WILD :+: META (LHS f) :+: f
+    toRep   = LHS
+    fromRep = unLHS
+
+instance Rep (RHS f)
+  where
+    type PF (RHS f) = META (RHS f) :+: f
+    toRep   = RHS
+    fromRep = unRHS
+
+
+
+----------------------------------------------------------------------------------------------------
+-- * Misc.
+----------------------------------------------------------------------------------------------------
+
+tRule :: Patch (Rule (LHS f) (RHS f)) (Rule (LHS f) (RHS f))
+tRule = id
+
+data A = A deriving (Eq)  -- Denoting a polymorphic type
+data B = B deriving (Eq)  -- Denoting a polymorphic type
+data C = C deriving (Eq)  -- Denoting a polymorphic type
+
+tA :: Patch A A
+tA = id
+
+tB :: Patch B B
+tB = id
+
+tC :: Patch C C
+tC = id
+
+-- | Substitution
+type Subst f = [(Name, Term f)]
+