diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,36 @@
 # Revision history for hegg
 
+## Unreleased
+
+## 0.3.0.0 -- 2022-12-09
+
+* A better `Analysis` tutorial in the README.
+
+* Complete `Analysis` redesign.
+    * The `Analysis` class now has two type parameters: a `domain` and a
+        `language`, and no longer has an associated type family
+    * The analysis no longer has any knowledge of the e-graph:
+        * `makeA` now has type `l domain -> domain`, that is, to make a domain
+            of a new node we only have to take into consideration the data of
+            the sub-nodes of the new node.
+        * `joinA` is unchanged.
+        * `modifyA` now has type `EClass domain lang -> (EClass domain lang,
+            [Fix lang])`. It takes an e-class and optionally modifies it,
+            possibly by adding nodes to it. The return value is the modified
+            e-class, and a list of expressions from the language to add to the
+            e-class.
+    * We can now compose analysis and create language-polymorphic analysis. Such
+        two examples are the analysis with domain `()` which regardless of the
+        language simply ignores the domain: `instance Analysis () l`; and the
+        second example is the product of analysis, which composes two separate
+        analysis into one: `instance (Analysis a l, Analysis b l) => Analysis
+        (a,b) l`.
+    * An `EGraph` now also has two type parameters instead of one (the latter is
+      the language is the former the domain of the analysis).
+
+* Allow customization of Schedulers through parameters (by accepting a scheduler
+    rather than a proxy for it)
+
 ## 0.2.0.0 -- 2022-09-19
 
 * Expose `runEqualitySaturation` to run equality saturation on existing e-graphs
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -96,14 +96,94 @@
 can be read about e-class analysis in the [`Data.Equality.Analsysis`]() module and
 in the paper.
 
-We could easily define constant folding (`2+2` being simplified to `4`) through
-an `Analysis` instance, but for the sake of simplicity we'll simply define the
-analysis data as `()` and always ignore it.
+We can easily define constant folding (`2+2` being simplified to `4`) through
+an `Analysis` instance.
 
+An `Analysis` is defined over a `domain` and a `language`. To define constant
+folding, we'll say the domain is `Maybe Double` to attach a value of that type to
+each e-class, where `Nothing` indicates the e-class does not currently have a
+constant value and `Just i` means the e-class has constant value `i`.
+
 ```hs
-instance Analysis SymExpr where
-  type Domain SymExpr = ()
-  makeA _ _ = ()
+instance Analysis (Maybe Double) SymExpr
+  makeA = ...
+  joinA = ...
+  modifyA = ...
+```
+
+Let's now understand and implement the three methods of the analysis instance we want.
+
+`makeA` is called when a new e-node is added to a new e-class, and constructs
+for the new e-class a new value of the domain to be associated with it, always
+by accessing the associated data of the node's children data.  Its type is `l
+domain -> domain`, so note that the e-node's children associated data is
+directly available in place of the actual children.
+
+We want to associate constant data to the e-class, so we must find if the
+e-node has a constant value or otherwise return `Nothing`:
+
+```hs
+makeA :: SymExpr (Maybe Double) -> Maybe Int
+makeA = \case
+  Const x -> Just x
+  Symbol _ -> Nothing
+  x :+: y -> (+) <$> x <*> y
+  x :*: y -> (*) <$> x <*> y
+  x :/: y -> (/) <$> x <*> y
+```
+ 
+`joinA` is called when e-classes c1 c2 are being merged into c. In this case, we
+must join the e-class data from both classes to form the e-class data to be
+associated with new e-class c. Its type is `domain -> domain -> domain`.  In our
+case, to merge `Just _` with `Nothing` we simply take the `Just`, and if we
+merge two e-classes with a constant value (that is, both are `Just`), then the
+constant value is the same (or something went very wrong) and we just keep it.
+
+```hs
+joinA :: Maybe Double -> Maybe Double -> Maybe Double
+joinA Nothing (Just x) = Just x
+joinA (Just x) Nothing = Just x
+joinA Nothing Nothing  = Nothing
+joinA (Just x) (Just y) = if x == y then Just x else error "ouch, that shouldn't have happened"
+```
+
+Finally, `modifyA` describes how an e-class should (optionally) be modified
+according to the e-class data and what new language expressions are to be added
+to the e-class also w.r.t. the e-class data.
+Its type is `EClass domain l -> (EClass domain l, [Fix l])`, where the argument
+is the class to modify, the first element of the return tuple is the
+(optionally) modified e-class and the second element is a list of the
+expressions to represent and merge with this e-class.
+For our example, if the e-class has a constant value associated to it, we want
+to create a new e-class with that constant value and merge it to this e-class.
+
+```hs
+-- import Data.Equality.Graph.Lens ((^.), _data)
+modifyA :: EClass (Maybe Double) SymExpr -> (EClass (Maybe Double) SymExpr, [Fix SymExpr])
+modifyA c = case c^._data of
+              Nothing -> (c, [])
+              Just i  -> (c, [Fix (Const i)])
+```
+
+Modify is a bit trickier than the other methods, but it allows our e-graph to
+change based on the e-class analysis data. Note that the method is optional and
+there's a default implementation for it which doesn't change the e-class or adds
+anything to it. Analysis data can be otherwise used, e.g., to inform rewrite
+conditions.
+
+By instancing this e-class analysis, all e-classes that have a constant value
+associated to them will also have an e-node with a constant value. This is great
+for our simple symbolic library because it means if we ever find e.g. an
+expression equal to `3+1`, we'll also know it to be equal to `4`, which is a
+better result than `3+1` (we've then successfully implemented constant folding).
+
+If, otherwise, we didn't want to use an analysis, we could specify the analysis
+domain as `()` which will make the analysis do nothing, because there's an
+instance polymorphic over `lang` for `()` that looks like this:
+
+```hs
+instance Analysis () lang where
+  makeA _ = ()
   joinA _ _ = ()
 ```
 
@@ -202,6 +282,10 @@
 let expr = fst (equalitySaturation e1 rewrites cost)
 ```
 And upon printing we'd see `expr = Symbol "x"`!
+
+If we had instead `e2 = Fix (Fix (Fix (Symbol "x") :/: Fix (Symbol "x")) :+:
+(Fix (Const 3))) -- (x/x)+3`, we'd get `expr = Const 4` because of our rewrite
+rules put together with our constant folding!
 
 This was a first introduction which skipped over some details but that tried to
 walk through fundamental concepts for using e-graphs and equality saturation
diff --git a/hegg.cabal b/hegg.cabal
--- a/hegg.cabal
+++ b/hegg.cabal
@@ -1,7 +1,7 @@
 cabal-version:      2.4
 name:               hegg
-version:            0.2.0.0
-Tested-With:        GHC ==9.4.1 || ==9.2.2 || ==9.0.2 || ==8.10.7
+version:            0.3.0.0
+Tested-With:        GHC ==9.4.2 || ==9.2.2 || ==9.0.2 || ==8.10.7
 synopsis:           Fast equality saturation in Haskell
 
 description:        Fast equality saturation and equality graphs based on "egg:
@@ -107,7 +107,9 @@
     type:             exitcode-stdio-1.0
     hs-source-dirs:   test
     main-is:          Test.hs
-    other-modules:    Invariants, Sym, Lambda, SimpleSym
+    other-modules:    Invariants, Sym, Lambda, SimpleSym,
+                      T1, T2
+
     other-extensions: OverloadedStrings
     build-depends:    base,
                       hegg,
diff --git a/src/Data/Equality/Analysis.hs b/src/Data/Equality/Analysis.hs
--- a/src/Data/Equality/Analysis.hs
+++ b/src/Data/Equality/Analysis.hs
@@ -1,4 +1,8 @@
 {-# LANGUAGE AllowAmbiguousTypes #-} -- joinA
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
@@ -23,41 +27,115 @@
 module Data.Equality.Analysis where
 
 import Data.Kind (Type)
-
-import Data.Equality.Graph.Classes.Id
-import Data.Equality.Graph.Nodes
-
-import {-# SOURCE #-} Data.Equality.Graph.Internal (EGraph)
+import Control.Arrow ((***))
 
--- | The e-class analysis defined for a language @l@.
-class Eq (Domain l) => Analysis (l :: Type -> Type) where
+import Data.Equality.Utils
+import Data.Equality.Language
+import Data.Equality.Graph.Classes
 
-    -- | Domain of data stored in e-class according to e-class analysis
-    type Domain l
+-- | An e-class analysis with domain @domain@ defined for a language @l@.
+--
+-- The @domain@ is the type of the domain of the e-class analysis, that is, the
+-- type of the data stored in an e-class according to this e-class analysis
+class Eq domain => Analysis domain (l :: Type -> Type) where
 
     -- | When a new e-node is added into a new, singleton e-class, construct a
-    -- new value of the domain to be associated with the new e-class, typically
-    -- by accessing the associated data of n's children
-    makeA :: ENode l -> EGraph l -> Domain l
+    -- new value of the domain to be associated with the new e-class, by
+    -- accessing the associated data of the node's children
+    --
+    -- The argument is the e-node term populated with its children data
+    --
+    -- === Example
+    --
+    -- @
+    -- -- domain = Maybe Double
+    -- makeA :: Expr (Maybe Double) -> Maybe Double
+    -- makeA = \case
+    --     BinOp Div e1 e2 -> liftA2 (/) e1 e2
+    --     BinOp Sub e1 e2 -> liftA2 (-) e1 e2
+    --     BinOp Mul e1 e2 -> liftA2 (*) e1 e2
+    --     BinOp Add e1 e2 -> liftA2 (+) e1 e2
+    --     Const x -> Just x
+    --     Sym _ -> Nothing
+    -- @
+    makeA :: l domain -> domain
 
     -- | When e-classes c1 c2 are being merged into c, join d_c1 and
     -- d_c2 into a new value d_c to be associated with the new
     -- e-class c
-    joinA :: Domain l -> Domain l -> Domain l
+    joinA :: domain -> domain -> domain
 
-    -- | Optionaly modify the e-class c (based on d_c), typically by adding an
+    -- | Optionally modify the e-class c (based on d_c), typically by adding an
     -- e-node to c. Modify should be idempotent if no other changes occur to
     -- the e-class, i.e., modify(modify(c)) = modify(c)
     --
+    -- The return value of the modify function is both the modified class and
+    -- the expressions (in their fixed-point form) to add to this class. We
+    -- can't manually add them because not only would it skip some of the
+    -- internal steps of representing + merging, but also because it's
+    -- impossible to add any expression with depth > 0 without access to the
+    -- e-graph (since we must represent every sub-expression in the e-graph
+    -- first).
+    --
+    -- That's why we must return the modified class and the expressions to add
+    -- to this class.
+    --
     -- === Example
     --
     -- Pruning an e-class with a constant value of all its nodes except for the
-    -- leaf values
+    -- leaf values, and adding a constant value node
     --
     -- @
     --  -- Prune all except leaf e-nodes
-    --  modify (_class i._nodes %~ S.filter (null . children))
+    --  modifyA cl =
+    --    case cl^._data of
+    --      Nothing -> (cl, [])
+    --      Just d -> ((_nodes %~ S.filter (F.null .unNode)) cl, [Fix (Const d)])
     -- @
-    modifyA :: ClassId -> EGraph l -> EGraph l
-    modifyA _ = id
+    modifyA :: EClass domain l -> (EClass domain l, [Fix l])
+    modifyA c = (c, [])
     {-# INLINE modifyA #-}
+
+
+-- | The simplest analysis that defines the domain to be () and does nothing
+-- otherwise
+instance forall l. Analysis () l where
+  makeA _ = ()
+  joinA = (<>)
+
+
+-- This instance is not necessarily well behaved for any two analysis, so care
+-- must be taken when using it.
+--
+-- A possible criterion is:
+--
+-- For any two analysis, where 'modifyA' is called @m1@ and @m2@ respectively,
+-- this instance is well behaved if @m1@ and @m2@ commute.
+--
+-- That is, if @m1@ and @m2@ satisfy the following law:
+-- @
+-- m1 . m2 = m2 . m1
+-- @
+--
+-- A simple criterion that should suffice for commutativity. If:
+--  * The modify function only depends on the analysis value, and
+--  * The modify function doesn't change the analysis value
+-- Then any two such functions commute.
+--
+-- Note: there are weaker (or at least different) criteria for this instance to
+-- be well behaved.
+instance (Language l, Analysis a l, Analysis b l) => Analysis (a, b) l where
+
+  makeA :: l (a, b) -> (a, b)
+  makeA g = (makeA @a (fst <$> g), makeA @b (snd <$> g))
+
+  joinA :: (a,b) -> (a,b) -> (a,b)
+  joinA (x,y) = joinA @a @l x *** joinA @b @l y
+
+  modifyA :: EClass (a, b) l -> (EClass (a, b) l, [Fix l])
+  modifyA c =
+    let (ca, la) = modifyA @a (c { eClassData = fst (eClassData c) })
+        (cb, lb) = modifyA @b (c { eClassData = snd (eClassData c) })
+     in ( EClass (eClassId c) (eClassNodes ca <> eClassNodes cb) (eClassData ca, eClassData cb) (eClassParents ca <> eClassParents cb)
+        , la <> lb
+        )
diff --git a/src/Data/Equality/Extraction.hs b/src/Data/Equality/Extraction.hs
--- a/src/Data/Equality/Extraction.hs
+++ b/src/Data/Equality/Extraction.hs
@@ -1,10 +1,4 @@
-{-# LANGUAGE RecordWildCards #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ViewPatterns #-}
 {-|
    Given an e-graph representing expressions of our language, we might want to
@@ -45,9 +39,9 @@
 -- @
 --
 -- For a real example you might want to check out the source code of 'Data.Equality.Saturation.equalitySaturation''
-extractBest :: forall lang cost
+extractBest :: forall anl lang cost
              . (Language lang, Ord cost)
-            => EGraph lang            -- ^ The e-graph out of which we are extracting an expression
+            => EGraph anl lang        -- ^ The e-graph out of which we are extracting an expression
             -> CostFunction lang cost -- ^ The cost function to define /best/
             -> ClassId                -- ^ The e-class from which we'll extract the expression
             -> Fix lang               -- ^ The resulting /best/ expression, in its fixed point form.
@@ -66,14 +60,14 @@
   where
 
     -- | Find the lowest cost of all e-classes in an e-graph in an extraction
-    findCosts :: ClassIdMap (EClass lang) -> ClassIdMap (CostWithExpr lang cost) -> ClassIdMap (CostWithExpr lang cost)
+    findCosts :: ClassIdMap (EClass anl lang) -> ClassIdMap (CostWithExpr lang cost) -> ClassIdMap (CostWithExpr lang cost)
     findCosts eclasses current =
 
       let (modified, updated) = IM.foldlWithKey f (False, current) eclasses
 
           {-# INLINE f #-}
-          f :: (Bool, ClassIdMap (CostWithExpr lang cost)) -> Int -> EClass lang -> (Bool, ClassIdMap (CostWithExpr lang cost))
-          f = \acc@(_, beingUpdated) i' EClass{eClassNodes = nodes} ->
+          f :: (Bool, ClassIdMap (CostWithExpr lang cost)) -> Int -> EClass anl lang -> (Bool, ClassIdMap (CostWithExpr lang cost))
+          f acc@(_, beingUpdated) i' EClass{eClassNodes = nodes} =
                 let
                     currentCost = IM.lookup i' beingUpdated
 
@@ -107,7 +101,7 @@
     nodeTotalCost :: Traversable lang => ClassIdMap (CostWithExpr lang cost) -> ENode lang -> Maybe (CostWithExpr lang cost)
     nodeTotalCost m (Node n) = do
         expr <- traverse ((`IM.lookup` m) . flip find egr) n
-        return $ CostWithExpr (cost ((fst . unCWE) <$> expr), (Fix $ (snd . unCWE) <$> expr))
+        return $ CostWithExpr (cost (fst . unCWE <$> expr), Fix $ snd . unCWE <$> expr)
     {-# INLINE nodeTotalCost #-}
 {-# INLINABLE extractBest #-}
 
@@ -140,7 +134,7 @@
 -- | Find the current best node and its cost in an equivalence class given only the class and the current extraction
 -- This is not necessarily the best node in the e-graph, only the best in the current extraction state
 findBest :: ClassId -> ClassIdMap (CostWithExpr lang a) -> Maybe (CostWithExpr lang a)
-findBest i = IM.lookup i
+findBest = IM.lookup
 {-# INLINE findBest #-}
 
 newtype CostWithExpr lang a = CostWithExpr { unCWE :: (a, Fix lang) }
diff --git a/src/Data/Equality/Graph.hs b/src/Data/Equality/Graph.hs
--- a/src/Data/Equality/Graph.hs
+++ b/src/Data/Equality/Graph.hs
@@ -1,6 +1,5 @@
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE BangPatterns #-}
-{-# LANGUAGE TupleSections #-}
 -- {-# LANGUAGE ApplicativeDo #-}
 {-# LANGUAGE BlockArguments #-}
 {-# LANGUAGE FlexibleContexts #-}
@@ -20,7 +19,7 @@
     , emptyEGraph
 
       -- ** Transformations
-    , add, merge, rebuild
+    , represent, add, merge, rebuild
     -- , repair, repairAnal
 
       -- ** Querying
@@ -38,6 +37,10 @@
 import Data.Bifunctor
 import Data.Containers.ListUtils
 
+import Control.Monad
+import Control.Monad.Trans.State
+import Control.Exception (assert)
+
 import qualified Data.IntMap.Strict as IM
 import qualified Data.Set    as S
 
@@ -51,18 +54,24 @@
 import Data.Equality.Language
 import Data.Equality.Graph.Lens
 
+import Data.Equality.Utils
+
 -- ROMES:TODO: join things built in paralell?
 -- instance Ord1 l => Semigroup (EGraph l) where
 --     (<>) eg1 eg2 = undefined -- not so easy
 -- instance Ord1 l => Monoid (EGraph l) where
 --     mempty = EGraph emptyUF mempty mempty mempty
 
+-- | Represent an expression (in it's fixed point form) in an e-graph.
+-- Returns the updated e-graph and the id from the e-class in which it was represented.
+represent :: forall a l. (Analysis a l, Language l) => Fix l -> EGraph a l -> (ClassId, EGraph a l)
+represent = cata (flip $ \e -> uncurry add . first Node . (`runState` e) . traverse (gets >=> \(x,e') -> x <$ put e'))
 
 -- | Add an e-node to the e-graph
 --
 -- If the e-node is already represented in this e-graph, the class-id of the
 -- class it's already represented in will be returned.
-add :: forall l. Language l => ENode l -> EGraph l -> (ClassId, EGraph l)
+add :: forall a l. (Analysis a l, Language l) => ENode l -> EGraph a l -> (ClassId, EGraph a l)
 add uncanon_e egr =
     let !new_en = canonicalize uncanon_e egr
 
@@ -76,7 +85,12 @@
             (new_eclass_id, new_uf) = makeNewSet (unionFind egr)
 
             -- New singleton e-class stores the e-node and its analysis data
-            new_eclass       = EClass new_eclass_id (S.singleton new_en) (makeA new_en egr) mempty
+            -- which is modified according to analysis
+            --
+            -- The modification also produces a list of expressions to
+            -- represent and merge with this class, which we'll do before
+            -- returning from this function
+            (new_eclass, added_nodes) = modifyA $ EClass new_eclass_id (S.singleton new_en) (makeA @a ((\i -> egr^._class i._data @a) <$> unNode new_en)) mempty
 
             -- TODO:Performance: All updates can be done to the map first? Parallelize?
             --
@@ -86,7 +100,7 @@
             -- And add new e-class to existing e-classes
             new_parents      = ((new_eclass_id, new_en) |:)
             new_classes      = IM.insert new_eclass_id new_eclass $
-                                    foldr  (IM.adjust ((_parents %~ new_parents)))
+                                    foldr  (IM.adjust (_parents %~ new_parents))
                                            (classes egr)
                                            (unNode new_en)
 
@@ -115,27 +129,30 @@
             -- something else?
             --
             -- So in the end, we do need to addToWorklist to get correct results
-            new_worklist     = (new_eclass_id, new_en):(worklist egr)
+            new_worklist     = (new_eclass_id, new_en):worklist egr
 
             -- Add the e-node's e-class id at the e-node's id
             new_memo         = insertNM new_en new_eclass_id (memo egr)
 
-         in ( new_eclass_id
+            -- So we have our almost final e-graph. We just need to represent
+            -- and merge in it all expressions which resulted from 'modifyA'
+            -- above
+            egr1             = egr { unionFind = new_uf
+                                   , classes   = new_classes
+                                   , worklist  = new_worklist
+                                   , memo      = new_memo
+                                   }
 
-            , egr { unionFind = new_uf
-                  , classes   = new_classes
-                  , worklist  = new_worklist
-                  , memo      = new_memo
-                  }
+            egr2             = foldr (representAndMerge new_eclass_id) egr1 added_nodes
 
-                  -- Modify created node according to analysis
-                  & modifyA new_eclass_id
 
+         in ( new_eclass_id
+            , egr2
             )
 {-# INLINABLE add #-}
 
 -- | Merge 2 e-classes by id
-merge :: forall l. Language l => ClassId -> ClassId -> EGraph l -> (ClassId, EGraph l)
+merge :: forall a l. (Analysis a l, Language l) => ClassId -> ClassId -> EGraph a l -> (ClassId, EGraph a l)
 merge a b egr0 =
 
   -- Use canonical ids
@@ -159,22 +176,28 @@
 
            -- Make leader the leader in the union find
            (new_id, new_uf) = unionSets leader sub (unionFind egr0)
+                                & first (\n -> assert (leader == n) n)
 
            -- Update leader class with all e-nodes and parents from the
            -- subsumed class
-           updatedLeader = leader_class & _parents %~ (sub_class^._parents <>)
-                                        & _nodes   %~ (sub_class^._nodes <>)
-                                        & _data    .~ new_data
-           new_data = joinA @l (leader_class^._data) (sub_class^._data)
+           (updatedLeader, added_nodes) = leader_class
+                                            & _parents %~ (sub_class^._parents <>)
+                                            & _nodes   %~ (sub_class^._nodes <>)
+                                            & _data    .~ new_data
+                                            & modifyA
 
+           new_data = joinA @a @l (leader_class^._data) (sub_class^._data)
+
            -- Update leader in classes so that it has all nodes and parents
            -- from subsumed class, and delete the subsumed class
-           new_classes = ((IM.insert leader updatedLeader) . (IM.delete sub)) (classes egr0)
+           --
+           -- Additionally modify the e-class according to the analysis
+           new_classes = (IM.insert leader updatedLeader . IM.delete sub) (classes egr0)
 
            -- Add all subsumed parents to worklist We can do this instead of
            -- adding the new e-class itself to the worklist because it would end
            -- up adding its parents anyway
-           new_worklist = toListSL (sub_class^._parents) <> (worklist egr0)
+           new_worklist = toListSL (sub_class^._parents) <> worklist egr0
 
            -- If the new_data is different from the classes, the parents of the
            -- class whose data is different from the merged must be put on the
@@ -186,13 +209,13 @@
              (if new_data /= (leader_class^._data)
                 then toListSL (leader_class^._parents)
                 else mempty) <>
-             (analysisWorklist egr0)
+             analysisWorklist egr0
 
            -- ROMES:TODO: The code that makes the -1 * cos test pass when some other things are tweaked
            -- new_memo = foldr (`insertNM` leader) (memo egr0) (sub_class^._nodes)
 
            -- Build new e-graph
-           new_egr = egr0
+           egr1 = egr0
              { unionFind = new_uf
              , classes   = new_classes
              -- , memo      = new_memo
@@ -200,10 +223,9 @@
              , analysisWorklist = new_analysis_worklist
              }
 
-             -- Modify according to analysis
-             & modifyA new_id
+           egr2 = foldr (representAndMerge leader) egr1 added_nodes
 
-        in (new_id, new_egr)
+        in (new_id, egr2)
 {-# INLINEABLE merge #-}
             
 
@@ -212,12 +234,12 @@
 -- similar to other approaches in how it restores congruence; but it uniquely
 -- allows the client to choose when to restore invariants in the context of a
 -- larger algorithm like equality saturation.
-rebuild :: Language l => EGraph l -> EGraph l
+rebuild :: (Analysis a l, Language l) => EGraph a l -> EGraph a l
 rebuild (EGraph uf cls mm wl awl) =
   -- empty worklists
   -- repair deduplicated e-classes
   let
-    emptiedEgr = (EGraph uf cls mm mempty mempty)
+    emptiedEgr = EGraph uf cls mm mempty mempty
 
     wl'   = nubOrd $ bimap (`find` emptiedEgr) (`canonicalize` emptiedEgr) <$> wl
     egr'  = foldr repair emptiedEgr wl'
@@ -234,7 +256,7 @@
 -- ROMES:TODO: find repair_id could be shared between repair and repairAnal?
 
 -- | Repair a single worklist entry.
-repair :: forall l. Language l => (ClassId, ENode l) -> EGraph l -> EGraph l
+repair :: forall a l. (Analysis a l, Language l) => (ClassId, ENode l) -> EGraph a l -> EGraph a l
 repair (repair_id, node) egr =
 
    -- TODO We're no longer deleting the uncanonicalized node, how much does it matter that the structure keeps growing?
@@ -247,20 +269,25 @@
 {-# INLINE repair #-}
 
 -- | Repair a single analysis-worklist entry.
-repairAnal :: forall l. Language l => (ClassId, ENode l) -> EGraph l -> EGraph l
+repairAnal :: forall a l. (Analysis a l, Language l) => (ClassId, ENode l) -> EGraph a l -> EGraph a l
 repairAnal (repair_id, node) egr =
     let
-        c        = (egr^._classes) IM.! repair_id
-        new_data = joinA @l (c^._data) (makeA node egr)
+        c1                = (egr^._classes) IM.! repair_id
+        new_data          = joinA @a @l (c1^._data) (makeA @a ((\i -> egr^._class i^._data @a) <$> unNode node))
+        (c2, added_nodes) = modifyA (c1 & _data .~ new_data)
     in
     -- Take action if the new_data is different from the existing data
-    if c^._data /= new_data
+    if c1^._data /= new_data
         -- Merge result is different from original class data, update class
         -- with new_data
-       then egr { analysisWorklist = toListSL (c^._parents) <> analysisWorklist egr
-                }
-                & _classes %~ (IM.adjust (_data .~ new_data) repair_id)
-                & modifyA repair_id
+       then
+        let
+            new_classes = IM.insert repair_id c2 (classes egr)
+            egr1 = egr { analysisWorklist = toListSL (c1^._parents) <> analysisWorklist egr
+                       , classes = new_classes
+                       }
+            egr2 = foldr (representAndMerge repair_id) egr1 added_nodes
+         in egr2
        else egr
 {-# INLINE repairAnal #-}
 
@@ -272,17 +299,22 @@
 -- that their e-class ids are represented by the same e-class canonical ids
 --
 -- canonicalize(𝑓(𝑎,𝑏,𝑐,...)) = 𝑓((find 𝑎), (find 𝑏), (find 𝑐),...)
-canonicalize :: Functor l => ENode l -> EGraph l -> ENode l
+canonicalize :: Functor l => ENode l -> EGraph a l -> ENode l
 canonicalize (Node enode) eg = Node $ fmap (`find` eg) enode
 {-# INLINE canonicalize #-}
 
 -- | Find the canonical representation of an e-class id in the e-graph
 -- Invariant: The e-class id always exists.
-find :: ClassId -> EGraph l -> ClassId
+find :: ClassId -> EGraph a l -> ClassId
 find cid = findRepr cid . unionFind
 {-# INLINE find #-}
 
 -- | The empty e-graph. Nothing is represented in it yet.
-emptyEGraph :: Language l => EGraph l
+emptyEGraph :: Language l => EGraph a l
 emptyEGraph = EGraph emptyUF mempty mempty mempty mempty
 {-# INLINE emptyEGraph #-}
+
+-- | Represent an expression (in fix-point form) and merge it with the e-class with the given id
+representAndMerge :: (Analysis a l, Language l) => ClassId -> Fix l -> EGraph a l -> EGraph a l
+representAndMerge o f g = case represent f g of
+                        (i, e) -> snd $ merge o i e
diff --git a/src/Data/Equality/Graph/Classes.hs b/src/Data/Equality/Graph/Classes.hs
--- a/src/Data/Equality/Graph/Classes.hs
+++ b/src/Data/Equality/Graph/Classes.hs
@@ -17,21 +17,19 @@
 
 import Data.Equality.Utils.SizedList
 
-import Data.Equality.Analysis
-
 -- | An e-class (an equivalence class of terms) of a language @l@.
 --
 -- Intuitively, an e-graph is a set of equivalence classes (e-classes). Each
 -- e-class is a set of e-nodes representing equivalent terms from a given
 -- language, and an e-node is a function symbol paired with a list of children
 -- e-classes.
-data EClass l = EClass
+data EClass analysis_domain language = EClass
     { eClassId      :: {-# UNPACK #-} !ClassId -- ^ E-class identifier
-    , eClassNodes   :: !(S.Set (ENode l))      -- ^ E-nodes in this class
-    , eClassData    :: Domain l                -- ^ The analysis data associated with this eclass.
-    , eClassParents :: !(SList (ClassId, ENode l))   -- ^ E-nodes which are parents of this e-class and their corresponding e-class ids.
+    , eClassNodes   :: !(S.Set (ENode language))      -- ^ E-nodes in this class
+    , eClassData    :: analysis_domain                       -- ^ The analysis data associated with this eclass.
+    , eClassParents :: !(SList (ClassId, ENode language)) -- ^ E-nodes which are parents of this e-class and their corresponding e-class ids.
     }
 
-instance (Show (Domain l), Show1 l) => Show (EClass l) where
+instance (Show a, Show1 l) => Show (EClass a l) where
     show (EClass a b d (SList c _)) = "Id: " <> show a <> "\nNodes: " <> show b <> "\nParents: " <> show c <> "\nData: " <> show d
 
diff --git a/src/Data/Equality/Graph/Classes.hs-boot b/src/Data/Equality/Graph/Classes.hs-boot
--- a/src/Data/Equality/Graph/Classes.hs-boot
+++ b/src/Data/Equality/Graph/Classes.hs-boot
@@ -4,5 +4,5 @@
 
 import Data.Kind
 
-type role EClass nominal
-data EClass (l :: Type -> Type)
+type role EClass representational nominal
+data EClass a (l :: Type -> Type)
diff --git a/src/Data/Equality/Graph/Internal.hs b/src/Data/Equality/Graph/Internal.hs
--- a/src/Data/Equality/Graph/Internal.hs
+++ b/src/Data/Equality/Graph/Internal.hs
@@ -11,19 +11,18 @@
 import Data.Equality.Graph.ReprUnionFind
 import Data.Equality.Graph.Classes
 import Data.Equality.Graph.Nodes
-import Data.Equality.Analysis
 
 -- | E-graph representing terms of language @l@.
 --
 -- Intuitively, an e-graph is a set of equivalence classes (e-classes). Each e-class is a
 -- set of e-nodes representing equivalent terms from a given language, and an e-node is a function
 -- symbol paired with a list of children e-classes.
-data EGraph l = EGraph
-    { unionFind :: !ReprUnionFind           -- ^ Union find like structure to find canonical representation of an e-class id
-    , classes   :: !(ClassIdMap (EClass l)) -- ^ Map canonical e-class ids to their e-classes
-    , memo      :: !(Memo l)                -- ^ Hashcons maps all canonical e-nodes to their e-class ids
-    , worklist  :: !(Worklist l)            -- ^ Worklist of e-class ids that need to be upward merged
-    , analysisWorklist :: !(Worklist l)     -- ^ Like 'worklist' but for analysis repairing
+data EGraph analysis language = EGraph
+    { unionFind :: !ReprUnionFind              -- ^ Union find like structure to find canonical representation of an e-class id
+    , classes   :: !(ClassIdMap (EClass analysis language)) -- ^ Map canonical e-class ids to their e-classes
+    , memo      :: !(Memo language)            -- ^ Hashcons maps all canonical e-nodes to their e-class ids
+    , worklist  :: !(Worklist language)        -- ^ Worklist of e-class ids that need to be upward merged
+    , analysisWorklist :: !(Worklist language) -- ^ Like 'worklist' but for analysis repairing
     }
 
 -- | The hashcons 𝐻  is a map from e-nodes to e-class ids
@@ -32,7 +31,7 @@
 -- | Maintained worklist of e-class ids that need to be “upward merged”
 type Worklist l = [(ClassId, ENode l)]
 
-instance (Show (Domain l), Show1 l) => Show (EGraph l) where
+instance (Show a, Show1 l) => Show (EGraph a l) where
     show (EGraph a b c d e) =
         "UnionFind: " <> show a <>
             "\n\nE-Classes: " <> show b <>
diff --git a/src/Data/Equality/Graph/Internal.hs-boot b/src/Data/Equality/Graph/Internal.hs-boot
--- a/src/Data/Equality/Graph/Internal.hs-boot
+++ b/src/Data/Equality/Graph/Internal.hs-boot
@@ -4,6 +4,6 @@
 
 import Data.Kind
 
-type EGraph :: (Type -> Type) -> Type
-type role EGraph nominal
-data EGraph l
+type role EGraph representational nominal
+type EGraph :: Type -> (Type -> Type) -> Type
+data EGraph a l
diff --git a/src/Data/Equality/Graph/Lens.hs b/src/Data/Equality/Graph/Lens.hs
--- a/src/Data/Equality/Graph/Lens.hs
+++ b/src/Data/Equality/Graph/Lens.hs
@@ -20,7 +20,6 @@
 import Data.Equality.Graph.Nodes
 import Data.Equality.Graph.Classes
 import Data.Equality.Graph.ReprUnionFind
-import Data.Equality.Analysis
 
 -- | A 'Lens'' as defined in other lenses libraries
 type Lens' s a = forall f. Functor f => (a -> f a) -> (s -> f s)
@@ -39,7 +38,7 @@
 -- | Lens for the e-class with the given id in an e-graph
 --
 -- Calls 'error' when the e-class doesn't exist
-_class :: ClassId -> Lens' (EGraph l) (EClass l)
+_class :: ClassId -> Lens' (EGraph a l) (EClass a l)
 _class i afa s =
     let canon_id = findRepr i (unionFind s)
      in (\c' -> s { classes = IM.insert canon_id c' (classes s) }) <$> afa (classes s IM.! canon_id)
@@ -47,27 +46,27 @@
 
 -- | Lens for the memo of e-nodes in an e-graph, that is, a mapping from
 -- e-nodes to the e-class they're represented in
-_memo :: Lens' (EGraph l) (NodeMap l ClassId)
+_memo :: Lens' (EGraph a l) (NodeMap l ClassId)
 _memo afa egr = (\m1 -> egr {memo = m1}) <$> afa (memo egr)
 {-# INLINE _memo #-}
 
 -- | Lens for the map of existing classes by id in an e-graph
-_classes :: Lens' (EGraph l) (ClassIdMap (EClass l))
+_classes :: Lens' (EGraph a l) (ClassIdMap (EClass a l))
 _classes afa egr = (\m1 -> egr {classes = m1}) <$> afa (classes egr)
 {-# INLINE _classes #-}
 
 -- | Lens for the 'Domain' of an e-class
-_data :: Lens' (EClass l) (Domain l)
+_data :: Lens' (EClass domain l) domain
 _data afa EClass{..} = (\d1 -> EClass eClassId eClassNodes d1 eClassParents) <$> afa eClassData
 {-# INLINE _data #-}
 
 -- | Lens for the parent e-classes of an e-class
-_parents :: Lens' (EClass l) (SList (ClassId, ENode l))
-_parents afa EClass{..} = (\ps -> EClass eClassId eClassNodes eClassData ps) <$> afa eClassParents
+_parents :: Lens' (EClass a l) (SList (ClassId, ENode l))
+_parents afa EClass{..} = EClass eClassId eClassNodes eClassData <$> afa eClassParents
 {-# INLINE _parents #-}
 
 -- | Lens for the e-nodes in an e-class
-_nodes :: Lens' (EClass l) (S.Set (ENode l))
+_nodes :: Lens' (EClass a l) (S.Set (ENode l))
 _nodes afa EClass{..} = (\ns -> EClass eClassId ns eClassData eClassParents) <$> afa eClassNodes
 {-# INLINE _nodes #-}
 
diff --git a/src/Data/Equality/Graph/Monad.hs b/src/Data/Equality/Graph/Monad.hs
--- a/src/Data/Equality/Graph/Monad.hs
+++ b/src/Data/Equality/Graph/Monad.hs
@@ -28,11 +28,12 @@
 
 import Data.Equality.Utils (Fix, cata)
 
+import Data.Equality.Analysis
 import Data.Equality.Graph (EGraph, ClassId, Language, ENode(..))
 import qualified Data.Equality.Graph as EG
 
 -- | E-graph stateful computation
-type EGraphM s = State (EGraph s)
+type EGraphM a l = State (EGraph a l)
 
 -- | Run EGraph computation on an empty e-graph
 --
@@ -43,18 +44,18 @@
 --  id2 <- represent t2
 --  merge id1 id2
 -- @
-egraph :: Language l => EGraphM l a -> (a, EGraph l)
+egraph :: Language l => EGraphM anl l a -> (a, EGraph anl l)
 egraph = runEGraphM EG.emptyEGraph
 {-# INLINE egraph #-}
 
 -- | Represent an expression (@Fix l@) in an e-graph by recursively
 -- representing sub expressions
-represent :: Language l => Fix l -> EGraphM l ClassId
+represent :: (Analysis anl l, Language l) => Fix l -> EGraphM anl l ClassId
 represent = cata $ sequence >=> add . Node
 {-# INLINE represent #-}
 
 -- | Add an e-node to the e-graph
-add :: Language l => ENode l -> EGraphM l ClassId
+add :: (Analysis anl l, Language l) => ENode l -> EGraphM anl l ClassId
 add = StateT . fmap pure . EG.add
 {-# INLINE add #-}
 
@@ -62,7 +63,7 @@
 --
 -- E-graph invariants may be broken by merging, and 'rebuild' should be used
 -- /eventually/ to restore them
-merge :: Language l => ClassId -> ClassId -> EGraphM l ClassId
+merge :: (Analysis anl l, Language l) => ClassId -> ClassId -> EGraphM anl l ClassId
 merge a b = StateT (pure <$> EG.merge a b)
 {-# INLINE merge #-}
 
@@ -73,11 +74,11 @@
 -- 'rebuild')
 --
 -- The paper describing rebuilding in detail is https://arxiv.org/abs/2004.03082
-rebuild :: Language l => EGraphM l ()
+rebuild :: (Analysis anl l, Language l) => EGraphM anl l ()
 rebuild = StateT (pure . ((),). EG.rebuild)
 {-# INLINE rebuild #-}
 
 -- | Run 'EGraphM' computation on a given e-graph
-runEGraphM :: EGraph l -> EGraphM l a -> (a, EGraph l)
+runEGraphM :: EGraph anl l -> EGraphM anl l a -> (a, EGraph anl l)
 runEGraphM = flip runState
 {-# INLINE runEGraphM #-}
diff --git a/src/Data/Equality/Language.hs b/src/Data/Equality/Language.hs
--- a/src/Data/Equality/Language.hs
+++ b/src/Data/Equality/Language.hs
@@ -30,8 +30,6 @@
 
 import Data.Functor.Classes
 
-import Data.Equality.Analysis
-
 -- | A 'Language' is the required constraint on /expressions/ that are to be
 -- represented in an e-graph.
 --
@@ -40,5 +38,5 @@
 -- e-graphs), note that it must satisfy the other class constraints. In
 -- particular an 'Data.Equality.Analysis.Analysis' must be defined for the
 -- language.
-class (Analysis l, Traversable l, Ord1 l) => Language l where
+class (Traversable l, Ord1 l) => Language l where
 
diff --git a/src/Data/Equality/Matching.hs b/src/Data/Equality/Matching.hs
--- a/src/Data/Equality/Matching.hs
+++ b/src/Data/Equality/Matching.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE ViewPatterns #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-|
@@ -69,7 +68,7 @@
      in mapMaybe f (genericJoin db q)
 
 -- | Convert an e-graph into a database
-eGraphToDatabase :: Language l => EGraph l -> Database l
+eGraphToDatabase :: Language l => EGraph a l -> Database l
 eGraphToDatabase egr = foldrWithKeyNM' addENodeToDB (DB mempty) (egr^._memo)
   where
 
diff --git a/src/Data/Equality/Saturation.hs b/src/Data/Equality/Saturation.hs
--- a/src/Data/Equality/Saturation.hs
+++ b/src/Data/Equality/Saturation.hs
@@ -48,14 +48,13 @@
 import Data.Bifunctor
 import Control.Monad
 
-import Data.Proxy
-
 import Data.Equality.Utils
 import Data.Equality.Graph.Nodes
 import Data.Equality.Graph.Lens
 import qualified Data.Equality.Graph as G
 import Data.Equality.Graph.Monad
 import Data.Equality.Language
+import Data.Equality.Analysis
 import Data.Equality.Graph.Classes
 import Data.Equality.Matching
 import Data.Equality.Matching.Database
@@ -65,33 +64,33 @@
 import Data.Equality.Saturation.Scheduler
 
 -- | Equality saturation with defaults
-equalitySaturation :: forall l cost
-                    . (Language l, Ord cost)
+equalitySaturation :: forall a l cost
+                    . (Analysis a l, Language l, Ord cost)
                    => Fix l               -- ^ Expression to run equality saturation on
-                   -> [Rewrite l]         -- ^ List of rewrite rules
+                   -> [Rewrite a l]         -- ^ List of rewrite rules
                    -> CostFunction l cost -- ^ Cost function to extract the best equivalent representation
-                   -> (Fix l, EGraph l)   -- ^ Best equivalent expression and resulting e-graph
-equalitySaturation = equalitySaturation' (Proxy @BackoffScheduler)
+                   -> (Fix l, EGraph a l)   -- ^ Best equivalent expression and resulting e-graph
+equalitySaturation = equalitySaturation' defaultBackoffScheduler
 
 
 -- | Run equality saturation on an expression given a list of rewrites, and
 -- extract the best equivalent expression according to the given cost function
 --
 -- This variant takes all arguments instead of using defaults
-equalitySaturation' :: forall l schd cost
-                    . (Language l, Scheduler schd, Ord cost)
-                    => Proxy schd          -- ^ Proxy for the scheduler to use
+equalitySaturation' :: forall a l schd cost
+                    . (Analysis a l, Language l, Scheduler schd, Ord cost)
+                    => schd                -- ^ Scheduler to use
                     -> Fix l               -- ^ Expression to run equality saturation on
-                    -> [Rewrite l]         -- ^ List of rewrite rules
+                    -> [Rewrite a l]       -- ^ List of rewrite rules
                     -> CostFunction l cost -- ^ Cost function to extract the best equivalent representation
-                    -> (Fix l, EGraph l)   -- ^ Best equivalent expression and resulting e-graph
-equalitySaturation' proxy expr rewrites cost = egraph $ do
+                    -> (Fix l, EGraph a l)   -- ^ Best equivalent expression and resulting e-graph
+equalitySaturation' schd expr rewrites cost = egraph $ do
 
     -- Represent expression as an e-graph
     origClass <- represent expr
 
     -- Run equality saturation (by applying non-destructively all rewrites)
-    runEqualitySaturation proxy rewrites
+    runEqualitySaturation schd rewrites
 
     -- Extract best solution from the e-class of the original expression
     gets $ \g -> extractBest g cost origClass
@@ -100,17 +99,17 @@
 
 -- | Run equality saturation on an e-graph by non-destructively applying all
 -- given rewrite rules until saturation (using the given 'Scheduler')
-runEqualitySaturation :: forall l schd
-                       . (Language l, Scheduler schd)
-                      => Proxy schd          -- ^ Proxy for the scheduler to use
-                      -> [Rewrite l]         -- ^ List of rewrite rules
-                      -> EGraphM l ()
-runEqualitySaturation _ rewrites = runEqualitySaturation' 0 mempty where -- Start at iteration 0
+runEqualitySaturation :: forall a l schd
+                       . (Analysis a l, Language l, Scheduler schd)
+                      => schd                -- ^ Scheduler to use
+                      -> [Rewrite a l]       -- ^ List of rewrite rules
+                      -> EGraphM a l ()
+runEqualitySaturation schd rewrites = runEqualitySaturation' 0 mempty where -- Start at iteration 0
 
   -- Take map each rewrite rule to stats on its usage so we can do
   -- backoff scheduling. Each rewrite rule is assigned an integer
   -- (corresponding to its position in the list of rewrite rules)
-  runEqualitySaturation' :: Int -> IM.IntMap (Stat schd) -> EGraphM l ()
+  runEqualitySaturation' :: Int -> IM.IntMap (Stat schd) -> EGraphM a l ()
   runEqualitySaturation' 30 _ = return () -- Stop after X iterations
   runEqualitySaturation' i stats = do
 
@@ -140,7 +139,7 @@
                 && IM.size afterClasses == IM.size beforeClasses)
           (runEqualitySaturation' (i+1) newStats)
 
-  matchWithScheduler :: Database l -> Int -> IM.IntMap (Stat schd) -> (Int, Rewrite l) -> ([(Rewrite l, Match)], IM.IntMap (Stat schd))
+  matchWithScheduler :: Database l -> Int -> IM.IntMap (Stat schd) -> (Int, Rewrite a l) -> ([(Rewrite a l, Match)], IM.IntMap (Stat schd))
   matchWithScheduler db i stats = \case
       (rw_id, rw :| cnd) -> first (map (first (:| cnd))) $ matchWithScheduler db i stats (rw_id, rw)
       (rw_id, lhs := rhs) -> do
@@ -156,11 +155,11 @@
                 let matches' = ematch db lhs -- Add rewrite to the e-match substitutions
 
                 -- Backoff scheduler: update stats
-                let newStats = updateStats @schd i rw_id x stats matches'
+                let newStats = updateStats schd i rw_id x stats matches'
 
                 (map (lhs := rhs,) matches', newStats)
 
-  applyMatchesRhs :: (Rewrite l, Match) -> EGraphM l ()
+  applyMatchesRhs :: (Rewrite a l, Match) -> EGraphM a l ()
   applyMatchesRhs =
       \case
           (rw :| cond, m@(Match subst _)) -> do
@@ -189,12 +188,12 @@
               return ()
 
   -- | Represent a pattern in the e-graph a pattern given substitions
-  reprPat :: Subst -> l (Pattern l) -> EGraphM l ClassId
+  reprPat :: Subst -> l (Pattern l) -> EGraphM a l ClassId
   reprPat subst = add . Node <=< traverse \case
       VariablePattern v ->
           case IM.lookup v subst of
               Nothing -> error "impossible: couldn't find v in subst?"
               Just i  -> return i
       NonVariablePattern p -> reprPat subst p
-
 {-# INLINEABLE runEqualitySaturation #-}
+
diff --git a/src/Data/Equality/Saturation/Rewrites.hs b/src/Data/Equality/Saturation/Rewrites.hs
--- a/src/Data/Equality/Saturation/Rewrites.hs
+++ b/src/Data/Equality/Saturation/Rewrites.hs
@@ -8,6 +8,8 @@
 -}
 module Data.Equality.Saturation.Rewrites where
 
+import Data.Functor.Classes
+
 import Data.Equality.Graph
 import Data.Equality.Matching
 import Data.Equality.Matching.Database
@@ -31,8 +33,8 @@
 --
 -- See the definition of @is_not_zero@ in the documentation for
 -- 'RewriteCondition'
-data Rewrite lang = !(Pattern lang) := !(Pattern lang)          -- ^ Trivial Rewrite
-                  | !(Rewrite lang) :| !(RewriteCondition lang) -- ^ Conditional Rewrite
+data Rewrite anl lang = !(Pattern lang) := !(Pattern lang)          -- ^ Trivial Rewrite
+                      | !(Rewrite anl lang) :| !(RewriteCondition anl lang) -- ^ Conditional Rewrite
 infix 3 :=
 infixl 2 :|
 
@@ -48,5 +50,9 @@
 --      Just class_id ->
 --          egr^._class class_id._data /= Just 0
 -- @
-type RewriteCondition lang = Subst -> EGraph lang -> Bool
+type RewriteCondition anl lang = Subst -> EGraph anl lang -> Bool
 
+
+instance Show1 lang => Show (Rewrite anl lang) where
+  show (rw :| _) = show rw <> " :| <cond>"
+  show (lhs := rhs) = show lhs <> " := " <> show rhs
diff --git a/src/Data/Equality/Saturation/Scheduler.hs b/src/Data/Equality/Saturation/Scheduler.hs
--- a/src/Data/Equality/Saturation/Scheduler.hs
+++ b/src/Data/Equality/Saturation/Scheduler.hs
@@ -11,7 +11,7 @@
 
 -}
 module Data.Equality.Saturation.Scheduler
-    ( Scheduler(..), BackoffScheduler
+    ( Scheduler(..), BackoffScheduler(..), defaultBackoffScheduler
     ) where
 
 import qualified Data.IntMap.Strict as IM
@@ -21,10 +21,11 @@
 -- being used based on statistics it defines and collects on applied rewrite
 -- rules.
 class Scheduler s where
-    type Stat s
+    data Stat s
 
     -- | Scheduler: update stats
-    updateStats :: Int                -- ^ Iteration we're in
+    updateStats :: s                  -- ^ The scheduler itself
+                -> Int                -- ^ Iteration we're in
                 -> Int                -- ^ Index of rewrite rule we're updating
                 -> Maybe (Stat s)     -- ^ Current stat for this rewrite rule (we already got it so no point in doing a lookup again)
                 -> IM.IntMap (Stat s) -- ^ The current stats map
@@ -46,11 +47,23 @@
 -- taking an unfair amount of resources.
 --
 -- Originaly in [egg](https://docs.rs/egg/0.6.0/egg/struct.BackoffScheduler.html)
-data BackoffScheduler
+data BackoffScheduler = BackoffScheduler
+  { matchLimit :: {-# UNPACK #-} !Int
+  , banLength  :: {-# UNPACK #-} !Int }
+
+-- | The default 'BackoffScheduler'.
+-- 
+-- The match limit is set to @1000@ and the ban length is set to @10@.
+defaultBackoffScheduler :: BackoffScheduler
+defaultBackoffScheduler = BackoffScheduler 1000 10
+
 instance Scheduler BackoffScheduler where
-    type Stat BackoffScheduler = BoSchStat
+    data Stat BackoffScheduler =
+      BSS { bannedUntil :: {-# UNPACK #-} !Int
+          , timesBanned :: {-# UNPACK #-} !Int
+          } deriving Show
 
-    updateStats i rw currentStat stats matches =
+    updateStats bos i rw currentStat stats matches =
 
         if total_len > threshold
 
@@ -65,16 +78,13 @@
           -- TODO: Overall difficult, and buggy at the moment.
           total_len = sum (map (length . matchSubst) matches)
 
-          defaultMatchLimit = 1000
-          defaultBanLength  = 10
-
           bannedN = case currentStat of
                       Nothing -> 0;
                       Just (timesBanned -> n) -> n
 
-          threshold = defaultMatchLimit * (2^bannedN)
+          threshold = matchLimit bos * (2^bannedN)
 
-          ban_length = defaultBanLength * (2^bannedN)
+          ban_length = banLength bos * (2^bannedN)
 
           updateBans = \case
             Nothing -> Just (BSS (i + ban_length) 1)
@@ -82,7 +92,3 @@
 
     isBanned i s = i < bannedUntil s
 
-
-data BoSchStat = BSS { bannedUntil :: {-# UNPACK #-} !Int
-                     , timesBanned :: {-# UNPACK #-} !Int
-                     } deriving Show
diff --git a/test/Invariants.hs b/test/Invariants.hs
--- a/test/Invariants.hs
+++ b/test/Invariants.hs
@@ -9,7 +9,6 @@
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE RecordWildCards #-}
 module Invariants where
 
 import Test.Tasty
@@ -27,7 +26,6 @@
 import Data.Equality.Graph.Monad as GM
 import Data.Equality.Graph.Lens
 import Data.Equality.Graph
-import Data.Equality.Analysis
 import Data.Equality.Extraction
 import Data.Equality.Saturation
 import Data.Equality.Matching
@@ -40,12 +38,6 @@
 newtype SimpleExpr l = SE (Expr l)
     deriving (Functor, Foldable, Traversable, Show1, Eq1, Ord1, Language)
 
-instance Analysis SimpleExpr where
-    type Domain SimpleExpr = ()
-    makeA _ _ = ()
-    joinA = (<>)
-    modifyA _ = id
-
 -- | When a rewrite of type "x":=c where x is a pattern variable and c is a
 -- constant is used in equality saturation of any expression, all e-classes
 -- should be merged into a single one, since all classes are equal to c and
@@ -53,11 +45,11 @@
 patFoldAllClasses :: forall l. (Language l, Num (Pattern l))
                   => Fix l -> Integer -> Bool
 patFoldAllClasses expr i =
-    case IM.toList $ (eg^._classes) of
+    case IM.toList (eg^._classes) of
         [_] -> True
         _   -> False
     where
-        eg :: EGraph l
+        eg :: EGraph () l
         eg = snd $ equalitySaturation expr [VariablePattern 1:=fromInteger i] (error "Cost function shouldn't be used" :: CostFunction l Int)
 
 -- | Test 'compileToQuery'.
@@ -93,7 +85,7 @@
 
 -- | If we match a singleton variable pattern against an e-graph, we should get
 -- a match on all e-classes in the e-graph
-ematchSingletonVar :: Language lang => Var -> EGraph lang -> Bool
+ematchSingletonVar :: Language lang => Var -> EGraph () lang -> Bool
 ematchSingletonVar v eg =
     let
         db = eGraphToDatabase eg
@@ -122,7 +114,7 @@
 --
 -- ROMES:TODO Should I rebuild it here? Then the property test is that after rebuilding ...HashConsInvariant
 hashConsInvariant :: forall l. Language l
-                  => EGraph l -> Bool
+                  => EGraph () l -> Bool
 hashConsInvariant eg =
     all f (IM.toList (eg^._classes))
     where
@@ -134,7 +126,7 @@
             Just i' -> i' == find i eg 
 
 benchSaturate :: forall l. Language l
-              => [Rewrite l] -> (l Int -> Int) -> Fix l -> Bool
+              => [Rewrite () l] -> (l Int -> Int) -> Fix l -> Bool
 benchSaturate rws cost expr =
     equalitySaturation expr rws cost `seq` True
 
@@ -142,12 +134,12 @@
 -- ROMES:TODO: Property: Extract expression after equality saturation is always better or equal to the original expression
 
 -- ROMES:TODO: Use action trick https://jaspervdj.be/posts/2015-03-13-practical-testing-in-haskell.html
-instance Arbitrary (EGraph SimpleExpr) where
+instance Arbitrary (EGraph () SimpleExpr) where
     arbitrary = sized $ \n -> do
         exps <- forM [0..n] $ const arbitrary
         -- rws :: [Rewrite Expr] <- forM [0..n] $ const arbitrary
         (ids, eg) <- return $ egraph $
-            mapM represent exps
+            mapM GM.represent exps
         ids1 <- sublistOf ids
         ids2 <- sublistOf ids
         return $ snd $ runEGraphM eg $ do
diff --git a/test/Lambda.hs b/test/Lambda.hs
--- a/test/Lambda.hs
+++ b/test/Lambda.hs
@@ -1,4 +1,6 @@
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE OverloadedStrings #-}
@@ -8,9 +10,14 @@
 {-# LANGUAGE DeriveTraversable #-}
 module Lambda where
 
+import Data.String
+
 import Test.Tasty
 import Test.Tasty.HUnit
 
+import Data.Maybe
+
+import qualified Data.IntMap as IM
 import qualified Data.Set as S
 
 import Control.Applicative ((<|>))
@@ -19,26 +26,29 @@
 import Data.Ord.Deriving
 import Text.Show.Deriving
 
-import Data.Equality.Graph.Lens
-import Data.Equality.Graph.Monad as GM
 import Data.Equality.Graph
 import Data.Equality.Extraction
 import Data.Equality.Analysis
 import Data.Equality.Saturation
 import Data.Equality.Matching
+import Data.Equality.Matching.Database as D
+import Data.Equality.Graph.Lens
 
 data Lambda a
-    = Bool Bool
-    | Num Int
-    | Var a
+    = Bool !Bool
+    | Num !Int
+    | Symbol !String
+    | Use a
+    | Subst a a a
+
     | Add a a
     | Eq a a
+    | If a a a
+
     | App a a
     | Lam a a
     | Let a a a
     | LFix a a
-    | If a a a
-    | Symbol String
     deriving ( Eq, Ord, Functor
              , Foldable, Traversable
              )
@@ -47,72 +57,109 @@
 deriveOrd1 ''Lambda
 deriveShow1 ''Lambda
 
-data Data = Data { free :: S.Set ClassId
-                 , constant :: Maybe (Fix Lambda)
-                 } deriving Eq
-
-evalL :: EGraph Lambda -> Lambda ClassId -> Maybe (Fix Lambda)
-evalL egr = \case
-    Bool n -> Just (Fix $ Bool n)
-    Num n  -> Just (Fix $ Num n)
+evalL :: Lambda (Maybe (Lambda ())) -> Maybe (Lambda ())
+evalL = \case
+    Bool n -> Just (Bool n)
+    Num n  -> Just (Num n)
     Add a b -> do
-        a' <- constant (egr^._class a._data) >>= num
-        b' <- constant (egr^._class b._data) >>= num
-        return (Fix $ Num $ a' + b')
+        a' <- a >>= num
+        b' <- b >>= num
+        return (Num $ a' + b')
     Eq  a b -> do
-        a' <- constant (egr^._class a._data)
-        b' <- constant (egr^._class b._data)
-        return (Fix $ Bool $  a' == b')
+        a' <- a
+        b' <- b
+        return (Bool $ a' == b')
     _ -> Nothing
   where
-    num :: Fix Lambda -> Maybe Int
+    num :: Lambda () -> Maybe Int
     num = \case
-        Fix (Num i) -> Just i
+        Num i -> Just i
         _ -> Nothing
 
-instance Analysis Lambda where
-    type Domain Lambda = Data
+type FreeVars = S.Set String
+-- the lambda evaluator analysis is a combined analysis of the free variable analysis and the constant folding analysis
+type LA = (FreeVars, Maybe (Lambda ()))
 
-    makeA n egr =
-      let
-          freeVs = case unNode n of
-            Var x -> S.singleton x
-            Let v a b ->
-                free (egr^._class a._data) <> S.delete v (free (egr^._class b._data))
-            Lam v a -> S.delete v (free (egr^._class a._data))
-            LFix v a -> S.delete v (free (egr^._class a._data))
-            _ -> mconcat (map (\i -> free $ egr^._class i._data) (children n))
+-- Constant folding for lambda evaluator
+instance Analysis (Maybe (Lambda ())) Lambda where
+  makeA = evalL
+  joinA = (<|>)
+  modifyA c = case c^._data of
+                Nothing -> (c, [])
+                Just v  -> (c, [f v])
+                  where
+                    f = \case
+                      Bool b -> Fix $ Bool b
+                      Num i  -> Fix $ Num i
+                      _ -> error "impossible, lambda () can't construct this"
+                      
 
-          cnst = evalL egr (unNode n)
-       in
-          Data freeVs cnst
+-- Free variable analysis for lambda
+instance Analysis FreeVars Lambda where
+  makeA = \case
+    Use x -> x
+    Let v a b -> (b S.\\ v) <> a
+    Lam v a -> a S.\\ v
+    LFix v a -> a S.\\ v
+    Bool _ -> mempty
+    Num _  -> mempty
+    Add a b -> a <> b
+    Eq a b -> a <> b
+    App a b -> a <> b
+    If a b c -> a <> b <> c
+    Symbol x -> S.singleton x
+    Subst a b c -> b <> a <> c
 
-    joinA (Data fv1 c1) (Data fv2 c2) =
-        Data (fv1 `S.intersection` fv2) (c1 <|> c2)
+  joinA = (<>)
 
-    -- modifyA :: ClassId -> EGraph l -> EGraph l
-    modifyA i egr = 
-        case constant (egr^._class i._data) of
-          Nothing -> egr
-          Just c -> snd $ runEGraphM egr $ do
-            new_c <- represent c
-            GM.merge i new_c
 
 instance Language Lambda
 
 instance Num (Fix Lambda) where
     fromInteger = Fix . Num . fromInteger
-    (+) = error "todo..."
+    (+) a b = Fix $ Add a b
     (-) = error "todo..."
     (*) = error "todo..."
     abs = error "todo..."
     signum = error "todo..."
 
-rules :: [Rewrite Lambda]
+unsafeGetSubst :: Pattern Lambda -> D.Subst -> ClassId
+unsafeGetSubst (NonVariablePattern _) _ = error "unsafeGetSubst: NonVariablePattern; expecting VariablePattern"
+unsafeGetSubst (VariablePattern v) subst = case IM.lookup v subst of
+      Nothing -> error "Searching for non existent bound var in conditional"
+      Just class_id -> class_id
+
+isConst :: Pattern Lambda -> RewriteCondition LA Lambda
+isConst v subst egr = isJust $ snd $ egr^._class (unsafeGetSubst v subst)._data
+
+isNotSameVar :: Pattern Lambda -> Pattern Lambda -> RewriteCondition LA Lambda
+isNotSameVar v1 v2 subst egr = find (unsafeGetSubst v1 subst) egr /= find (unsafeGetSubst v2 subst) egr
+
+rules :: [Rewrite LA Lambda]
 rules =
     [ ifP trP "x" "y" := "x"
     , ifP flP "x" "y" := "y"
-    -- , ifP (pat $ eq (varP "x") "e" "then" "else") := "else" :| if ...
+    -- , ifP (pat $ Eq (pat $ Use "x") "e") "then" "else" := "else" :| conditionEqual (pat $ Let "x" "e" "then") (pat $ Let "x" "e" "else")
+
+    , pat (Add "x" "y") := pat (Add "y" "x")
+    , pat (Add (pat $ Add "x" "y") "z") := pat (Add "x" $ pat $ Add "y" "z")
+    , pat (Eq "x" "y") := pat (Eq "y" "x")
+
+    -- substitution introduction
+    , pat (LFix "v" "e") := pat (Let "v" (pat $ LFix "v" "e") "e")
+    , pat (App (pat $ Lam "v" "body") "e") := pat (Let "v" "e" "body")
+
+    -- substitution propagation
+    , pat (Let "v" "e" (pat $ App "a" "b")) := pat (App (pat $ Let "v" "e" "a") (pat $ Let "v" "e" "b"))
+    , pat (Let "v" "e" (pat $ Add "a" "b")) := pat (Add (pat $ Let "v" "e" "a") (pat $ Let "v" "e" "b"))
+    , pat (Let "v" "e" (pat $ Eq "a" "b")) := pat (Eq (pat $ Let "v" "e" "a") (pat $ Let "v" "e" "b"))
+    , pat (Let "v" "e" (pat $ If "a" "b" "c")) := pat (If (pat $ Let "v" "e" "a") (pat $ Let "v" "e" "b") (pat $ Let "v" "e" "c"))
+
+    -- substitution elimination
+    , pat (Let "v" "e" "c") := "c" :| isConst "c" -- let const
+    , pat (Let "v1" "e" (pat $ Use "v1")) := "e" -- let var same
+    , pat (Let "v1" "e" (pat $ Use "v2")) := "v2" :| isNotSameVar "v1" "v2" -- let var diff
+    , pat (Let "v1" "e" (pat $ Lam "v1" "body")) := pat (Lam "v1" "body") -- let lam same
     ]
 
 rewrite :: Fix Lambda -> Fix Lambda
@@ -125,18 +172,33 @@
 
     , testCase "if fl" $
         rewrite (ifL fl 1 2) @?= 2
-    ]
 
+    , testCase "lambda_under" $
+      -- \x -> 4 + ((\y -> y) 4) = \x -> 8
+        rewrite (lam "x" (4 + app (lam "y" (var "y")) 4)) @?= lam "x" 8
 
+    {-
+       This test requires at least the ConditionEqual rewrite condition helper
+       and possibly dynamic rewrites. It would also be better to improve
+       rewrite conditions before continuing down this path.
 
+       For the analysis patch, being able to define the analysis
+       compositionally and without expressiveness problems is good enough.
 
+    , testCase "lambda_compose_many" $
+        rewrite (Fix (Let "compose" (lam "f" (lam "g" (lam "x" (app (var "f") (app (var "g") (var "x"))))))
+                          (Fix $ Let "add1" (lam "y" (Fix $ Add (var "y") 1)) (app (app (var "compose") (var "add1"))
+                                                                                   (app (app (var "compose") (var "add1"))
+                                                                                        (app (app (var "compose") (var "add1"))
+                                                                                             (var "add1"))))))) @?= lam "x" (Fix $ Add "x" 5)
+                                                                                             -}
+    ]
+
 ifP :: Pattern Lambda -> Pattern Lambda -> Pattern Lambda -> Pattern Lambda
 ifP a b c = pat (If a b c)
 trP, flP :: Pattern Lambda
 trP = pat (Bool True)
 flP = pat (Bool False)
-varP :: Pattern Lambda -> Pattern Lambda
-varP x = pat (Var x)
 
 -- TODO: recursion-schemes extension in separate package
 ifL :: Fix Lambda -> Fix Lambda -> Fix Lambda -> Fix Lambda
@@ -144,3 +206,12 @@
 tr, fl :: Fix Lambda
 tr = Fix $ Bool True
 fl = Fix $ Bool False
+lam :: Fix Lambda -> Fix Lambda -> Fix Lambda
+lam i = Fix . Lam i
+var :: Fix Lambda -> Fix Lambda
+var = Fix . Use
+app :: Fix Lambda -> Fix Lambda -> Fix Lambda
+app x y = Fix $ App x y
+
+instance IsString (Fix Lambda) where
+  fromString = Fix . Symbol
diff --git a/test/SimpleSym.hs b/test/SimpleSym.hs
--- a/test/SimpleSym.hs
+++ b/test/SimpleSym.hs
@@ -1,5 +1,7 @@
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE DeriveTraversable #-}
@@ -17,6 +19,7 @@
 import Data.Equality.Saturation
 import Data.Equality.Language
 import Data.Equality.Analysis
+import Data.Equality.Graph.Lens ((^.), _data)
 
 data SymExpr a = Const Double
                | Symbol String
@@ -31,13 +34,25 @@
 deriveOrd1  ''SymExpr
 deriveShow1 ''SymExpr
 
-instance Analysis SymExpr where
-  type Domain SymExpr = ()
-  makeA _ _ = ()
-  joinA _ _ = ()
-
 instance Language SymExpr
 
+instance Analysis (Maybe Double) SymExpr where
+  makeA = \case
+    Const x -> Just x
+    Symbol _ -> Nothing
+    x :+: y -> (+) <$> x <*> y
+    x :*: y -> (*) <$> x <*> y
+    x :/: y -> (/) <$> x <*> y
+
+  joinA Nothing (Just x) = Just x
+  joinA (Just x) Nothing = Just x
+  joinA Nothing Nothing  = Nothing
+  joinA (Just x) (Just y) = if x == y then Just x else error "ouch, that shouldn't have happened"
+
+  modifyA c = case c^._data of
+                Nothing -> (c, [])
+                Just i  -> (c, [Fix (Const i)])
+
 cost :: CostFunction SymExpr Int
 cost = \case
   Const  _ -> 1
@@ -46,20 +61,21 @@
   c1 :*: c2 -> c1 + c2 + 3
   c1 :/: c2 -> c1 + c2 + 4
 
-rewrites :: [Rewrite SymExpr]
+rewrites :: [Rewrite (Maybe Double) SymExpr]
 rewrites =
   [ pat (pat ("a" :*: "b") :/: "c") := pat ("a" :*: pat ("b" :/: "c"))
   , pat ("x" :/: "x")               := pat (Const 1)
-  , pat ("x" :*: (pat (Const 1)))   := "x"
+  , pat ("x" :*: pat (Const 1))     := "x"
   ]
 
 rewrite :: Fix SymExpr -> Fix SymExpr
 rewrite e = fst (equalitySaturation e rewrites cost)
 
 e1 :: Fix SymExpr
-e1 = Fix (Fix (Fix (Symbol "x") :*: Fix (Const 2)) :/: (Fix (Const 2))) -- (x*2)/2
+e1 = Fix (Fix (Fix (Symbol "x") :*: Fix (Const 2)) :/: Fix (Const 2)) -- (x*2)/2
 
 simpleSymTests :: TestTree
 simpleSymTests = testGroup "Simple Sym"
-    [ testCase "(a*2)/2 = a" $ rewrite e1 @?= Fix (Symbol "x")
+    [ testCase "(a*2)/2 = a"  $ rewrite e1 @?= Fix (Symbol "x")
+    , testCase "(x/x)+1) = 4" $ rewrite (Fix $ Fix (Const 3) :+: Fix (Fix (Symbol "x") :/: Fix (Symbol "x"))) @?= Fix (Const 4)
     ]
diff --git a/test/Sym.hs b/test/Sym.hs
--- a/test/Sym.hs
+++ b/test/Sym.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE BangPatterns #-}
 {-# LANGUAGE OverloadedStrings #-}
@@ -25,7 +26,6 @@
 import Control.Applicative (liftA2)
 import Control.Monad (unless)
 
-import Data.Equality.Graph.Monad as GM
 import Data.Equality.Graph.Lens
 import Data.Equality.Graph
 import Data.Equality.Extraction
@@ -109,10 +109,9 @@
 
 -- | Define analysis for the @Expr@ language over domain @Maybe Double@ for
 -- constant folding
-instance Analysis Expr where
-    type Domain Expr = Maybe Double
+instance Analysis (Maybe Double) Expr where
 
-    makeA (Node e) egr = evalConstant ((\c -> egr^._class c._data) <$> e)
+    makeA = evalConstant
 
     -- joinA = (<|>)
     joinA ma mb = do
@@ -124,17 +123,16 @@
         !_ <- unless (a == b || (a == 0 && b == (-0)) || (a == (-0) && b == 0)) (error "Merged non-equal constants!")
         return a
 
-    modifyA i egr =
-        case egr ^._class i._data of
-          Nothing -> egr
-          Just d  -> snd $ runEGraphM egr $ do
+    modifyA cl = case cl^._data of
+                 Nothing -> (cl, [])
+                 Just d -> ((_nodes %~ S.filter (F.null .unNode)) cl, [Fix (Const d)])
 
-            -- Add constant as e-node
-            new_c <- represent (Fix $ Const d)
-            _     <- GM.merge i new_c
+    --         -- Add constant as e-node
+    --         new_c <- represent (Fix $ Const d)
+    --         _     <- GM.merge i new_c
 
-            -- Prune all except leaf e-nodes
-            modify (_class i._nodes %~ S.filter (F.null . unNode))
+    --         -- Prune all except leaf e-nodes
+    --         modify (_class i._nodes %~ S.filter (F.null . unNode))
 
 
 
@@ -161,19 +159,19 @@
       Nothing -> error "Searching for non existent bound var in conditional"
       Just class_id -> class_id
 
-is_not_zero :: Pattern Expr -> RewriteCondition Expr
+is_not_zero :: Pattern Expr -> RewriteCondition (Maybe Double) Expr
 is_not_zero v subst egr =
     egr^._class (unsafeGetSubst v subst)._data /= Just 0
 
-is_sym :: Pattern Expr -> RewriteCondition Expr
+is_sym :: Pattern Expr -> RewriteCondition (Maybe Double) Expr
 is_sym v subst egr =
     any ((\case (Sym _) -> True; _ -> False) . unNode) (egr^._class (unsafeGetSubst v subst)._nodes)
 
-is_const :: Pattern Expr -> RewriteCondition Expr
+is_const :: Pattern Expr -> RewriteCondition (Maybe Double) Expr
 is_const v subst egr =
     isJust (egr^._class (unsafeGetSubst v subst)._data)
 
-is_const_or_distinct_var :: Pattern Expr -> Pattern Expr -> RewriteCondition Expr
+is_const_or_distinct_var :: Pattern Expr -> Pattern Expr -> RewriteCondition (Maybe Double) Expr
 is_const_or_distinct_var v w subst egr =
     let v' = unsafeGetSubst v subst
         w' = unsafeGetSubst w subst
@@ -181,7 +179,7 @@
         && (isJust (egr^._class v'._data)
             || any ((\case (Sym _) -> True; _ -> False) . unNode) (egr^._class v'._nodes))
 
-rewrites :: [Rewrite Expr]
+rewrites :: [Rewrite (Maybe Double) Expr]
 rewrites =
     [ "a"+"b" := "b"+"a" -- comm add
     , "a"*"b" := "b"*"a" -- comm mul
@@ -257,9 +255,9 @@
 symTests :: TestTree
 symTests = testGroup "Symbolic"
     [ testCase "(a*2)/2 = a (custom rules)" $
-        fst (equalitySaturation (("a"*2)/2) [ ("x"*"y")/"z" := "x"*("y"/"z")
-                                            , "y"/"y" := 1
-                                            , "x"*1 := "x"] symCost) @?= "a"
+        fst (equalitySaturation @(Maybe Double) (("a"*2)/2) [ ("x"*"y")/"z" := "x"*("y"/"z")
+                                                            , "y"/"y" := 1
+                                                            , "x"*1 := "x"] symCost) @?= "a"
 
     , testCase "(a/2)*2 = a (all rules)" $
         rewrite (("a"/2)*2) @?= "a"
@@ -269,7 +267,7 @@
 
     , testCase "x/y (custom rules)" $
         -- without backoff scheduler this will loop forever
-        fst (equalitySaturation
+        fst (equalitySaturation @(Maybe Double)
                 ("x"/"y")
 
                 [ "x"/"y" := "x"*(1/"y")
@@ -282,13 +280,13 @@
         fst (equalitySaturation (0+1) rewrites symCost)   @?= 1
 
     , testCase "b*(1/b) = 1 (custom rules)" $
-        fst (equalitySaturation ("b"*(1/"b")) [ "a"*(1/"a") := 1 ] symCost) @?= 1
+        fst (equalitySaturation @(Maybe Double) ("b"*(1/"b")) [ "a"*(1/"a") := 1 ] symCost) @?= 1
 
     , testCase "1+1=2 (constant folding)" $
-        fst (equalitySaturation (1+1) [] symCost) @?= 2
+        fst (equalitySaturation @(Maybe Double) (1+1) [] symCost) @?= 2
 
     , testCase "a*(2-1) (1 rule + constant folding)" $
-        fst (equalitySaturation ("a" * (2-1)) ["x"*1:="x"] symCost) @?= "a"
+        fst (equalitySaturation @(Maybe Double) ("a" * (2-1)) ["x"*1:="x"] symCost) @?= "a"
 
     , testCase "1+a*(2-1) = 1+a (all + constant folding)" $
         rewrite (1+("a"*(2-1))) @?= (1+"a")
diff --git a/test/T1.hs b/test/T1.hs
new file mode 100644
--- /dev/null
+++ b/test/T1.hs
@@ -0,0 +1,145 @@
+{-# language DeriveTraversable #-}
+{-# language LambdaCase #-}
+{-# language TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# OPTIONS_GHC -Wno-unused-matches #-}
+module T1 (main) where
+
+import Test.Tasty.HUnit
+import Data.Eq.Deriving
+import Data.Ord.Deriving
+import Text.Show.Deriving
+
+import Data.Equality.Graph
+import Data.Equality.Matching
+import Data.Equality.Saturation
+import Data.Equality.Saturation.Scheduler
+
+data TreeF a = VarF Int
+             | ConstF Double
+             | AddF a a
+             | SubF a a
+             | MulF a a
+             | DivF a a
+             | LogF a
+               deriving (Functor, Foldable, Traversable)
+
+deriveEq1 ''TreeF
+deriveOrd1 ''TreeF
+deriveShow1 ''TreeF
+
+instance Num (Fix TreeF) where
+  l + r = Fix $ AddF l r
+  l - r = Fix $ SubF l r
+  l * r = Fix $ MulF l r
+  abs   = undefined
+
+  negate t    = fromInteger (-1) * t
+  signum t    = undefined
+  fromInteger = Fix . ConstF . fromInteger
+
+instance Fractional (Fix TreeF) where
+    (/) a b = Fix (DivF a b)
+    fromRational = Fix . ConstF . fromRational
+
+instance Floating (Fix TreeF) where
+  pi      = undefined
+  exp     = undefined
+  log     = Fix . LogF
+  sqrt    = undefined
+  sin     = undefined
+  cos     = undefined
+  tan     = undefined
+  asin    = undefined
+  acos    = undefined
+  atan    = undefined
+  sinh    = undefined
+  cosh    = undefined
+  tanh    = undefined
+  asinh   = undefined
+  acosh   = undefined
+  atanh   = undefined
+
+  l ** r      = undefined
+  logBase l r = undefined
+
+instance Num (Pattern TreeF) where
+  l + r = NonVariablePattern $ AddF l r
+  l - r = NonVariablePattern $ SubF l r
+  l * r = NonVariablePattern $ MulF l r
+  abs   = undefined
+
+  negate t    = fromInteger (-1) * t
+  signum t    = undefined
+  fromInteger = NonVariablePattern . ConstF . fromInteger
+
+instance Fractional (Pattern TreeF) where
+    (/) a b = NonVariablePattern (DivF a b)
+    fromRational = NonVariablePattern . ConstF . fromRational
+
+instance Floating (Pattern TreeF) where
+  pi      = undefined
+  exp     = undefined
+  log     = NonVariablePattern . LogF
+  sqrt    = undefined
+  sin     = undefined
+  cos     = undefined
+  tan     = undefined
+  asin    = undefined
+  acos    = undefined
+  atan    = undefined
+  sinh    = undefined
+  cosh    = undefined
+  tanh    = undefined
+  asinh   = undefined
+  acosh   = undefined
+  atanh   = undefined
+
+  l ** r      = undefined
+  logBase l r = undefined
+
+instance Language TreeF
+
+cost :: CostFunction TreeF Int
+cost = \case
+  ConstF _ -> 5
+  VarF _ -> 1
+  AddF c1 c2 -> c1 + c2 + 2
+  SubF c1 c2 -> c1 + c2 + 2
+  MulF c1 c2 -> c1 + c2 + 4
+  DivF c1 c2 -> c1 + c2 + 5
+  LogF c -> c + 2
+
+tmpRewrites :: [Rewrite () TreeF]
+tmpRewrites = [
+        "x" + "y" := "y" + "x"
+      , "x" * "y" := "y" * "x"
+      , "x" + ("y" + "z") := ("x" + "y") + "z"
+      , "x" * ("y" * "z") := ("x" * "y") * "z"
+      , "x" * ("y" / "z") := ("x" * "y") / "z"
+      , "x" + 0 := "x"
+      , "x" * 1 := "x"
+      , "x" * 0 := 0
+      , "x" / "x" := 1
+      , ("x" * "y") + ("x" * "z") := "x" * ("y" + "z") 
+      , negate ("x" + "y") := negate "x" - "y"
+      , 0 - "x" := negate "x"
+      , log ("x" * "y") := log "x" + log "y"
+      , log ("x" / "y") := log "x" - log "y"
+      , log 1 := 0
+    ]
+
+rewriteTree :: Fix TreeF -> (Fix TreeF, EGraph () TreeF)
+rewriteTree t = equalitySaturation' (BackoffScheduler 1000 15) t tmpRewrites cost
+
+x, y :: Fix TreeF
+x = Fix (VarF 0)
+y = Fix (VarF 1)
+
+main :: IO ()
+main = do
+  fst (rewriteTree ((log x) / (x * ((y / y) / y)))) @?= (Fix $ DivF (Fix $ LogF (Fix $ VarF 0)) (Fix $ DivF (Fix $ VarF 0) (Fix $ VarF 1)))
+  pure ()
+
diff --git a/test/T2.hs b/test/T2.hs
new file mode 100644
--- /dev/null
+++ b/test/T2.hs
@@ -0,0 +1,49 @@
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE OverloadedStrings #-}
+module T2 where
+
+-- Tests whether this saturates just like mwillsey claims that it does in egg!
+
+import Prelude hiding (not)
+
+import Test.Tasty.HUnit
+import Data.Deriving
+import Data.Equality.Matching
+import Data.Equality.Language
+import Data.Equality.Extraction
+import Data.Equality.Saturation
+
+data Lang a = And a a
+            | Or a a
+            | Not a
+            | ToElim a
+            | Sym Int
+            deriving (Functor, Foldable, Traversable)
+
+deriveEq1 ''Lang
+deriveOrd1 ''Lang
+deriveShow1 ''Lang
+
+instance Language Lang
+
+x, y :: Pattern Lang
+x = "x"
+y = "y"
+not :: Pattern Lang -> Pattern Lang
+not = pat . Not
+
+rules :: [Rewrite () Lang]
+rules =
+  [ pat (x `And` y) := not (pat (not x `Or` not y))
+  , pat (x `Or` y) := not (pat (not x `And` not y))
+  , not (not x) := pat (ToElim x)
+  , pat (ToElim x) := x
+  ]
+
+main :: IO ()
+main = do
+  fst (equalitySaturation (Fix $ (Fix $ Not $ Fix $ Sym 0) `And` (Fix $ Not $ Fix $ Sym 1)) rules depthCost) @?= Fix (Not $ Fix $ (Fix $ Sym 0) `Or` (Fix $ Sym 1))
+  pure ()
+
diff --git a/test/Test.hs b/test/Test.hs
--- a/test/Test.hs
+++ b/test/Test.hs
@@ -1,18 +1,27 @@
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE OverloadedStrings #-}
 import Test.Tasty
+import Test.Tasty.HUnit
 
+import Control.Exception
+
 -- import Data.Equality.Utils
 import Invariants
 import Sym
 import Lambda
 import SimpleSym
 
+import qualified T1
+import qualified T2
+
 tests :: TestTree
 tests = testGroup "Tests"
   [ symTests
   , lambdaTests
   , simpleSymTests
   , invariants
+  , testCase "T1" (T1.main `catch` (\(e :: SomeException) -> assertFailure (show e)))
+  , testCase "T2" (T2.main `catch` (\(e :: SomeException) -> assertFailure (show e)))
   ]
 
 main :: IO ()