diff --git a/Data/BatchedQueue.hs b/Data/BatchedQueue.hs
new file mode 100644
--- /dev/null
+++ b/Data/BatchedQueue.hs
@@ -0,0 +1,145 @@
+-- | A queue where entries can be added in batches and stored compactly.
+{-# LANGUAGE TypeFamilies, RecordWildCards, FlexibleContexts, ScopedTypeVariables #-}
+module Data.BatchedQueue(
+  Queue, Batch(..), StandardBatch, unbatch, empty, insert, removeMin, removeMinFilter, mapMaybe, toBatches, toList, size) where
+
+import qualified Data.Heap as Heap
+import Data.List(unfoldr, sort, foldl')
+import qualified Data.Maybe
+import Data.PackedSequence(PackedSequence)
+import qualified Data.PackedSequence as PackedSequence
+import Data.Serialize
+import Data.Ord
+
+-- | A queue of batches.
+newtype Queue a = Queue (Heap.Heap (Best a))
+
+-- | The type of batches must be a member of this class.
+class Ord (Entry a) => Batch a where
+  -- | Each batch can have an associated label,
+  -- which is specified when calling 'insert'.
+  -- A label represents a piece of information which is
+  -- shared in common between all entries in a batch,
+  -- and which might be used to store that batch more
+  -- efficiently. 
+  -- Labels are optional, and by default @Label a = ()@.
+  type Label a
+
+  -- | Individual entries in the batch.
+  type Entry a
+
+  -- | Given a label, and a non-empty list of entries,
+  -- sorted in ascending order, produce a list of batches.
+  makeBatch :: Label a -> [Entry a] -> [a]
+
+  -- | Remove the smallest entry from a batch.
+  unconsBatch :: a -> (Entry a, Maybe a)
+  
+  -- | Return the label of a batch.
+  batchLabel :: a -> Label a
+
+  -- | Compute the size of a batch. Used in 'size'.
+  -- The default implementation works by repeatedly calling
+  -- 'unconsBatch'.
+  batchSize :: a -> Int
+  batchSize = length . unbatch
+
+  type Label a = ()
+
+-- A newtype wrapper for batches which compares the smallest entry.
+newtype Best a = Best { unBest :: a }
+instance Batch a => Eq (Best a) where x == y = compare x y == EQ
+instance Batch a => Ord (Best a) where
+  {-# INLINEABLE compare #-}
+  compare = comparing (fst . unconsBatch . unBest)
+
+-- | Convert a batch into a list of entries.
+{-# INLINEABLE unbatch #-}
+unbatch :: Batch a => a -> [Entry a]
+unbatch batch = unfoldr (fmap unconsBatch) (Just batch)
+
+-- | The empty queue.
+empty :: Queue a
+empty = Queue Heap.empty
+
+-- | Add entries to the queue.
+{-# INLINEABLE insert #-}
+insert :: forall a. Batch a => Label a -> [Entry a] -> Queue a -> Queue a
+insert _ [] q = q
+insert l is (Queue q) =
+  Queue $ foldl' (flip (Heap.insert . Best)) q (makeBatch l (sort is))
+
+-- | Remove the minimum entry from the queue.
+{-# INLINEABLE removeMin #-}
+removeMin :: Batch a => Queue a -> Maybe (Entry a, Queue a)
+removeMin q = removeMinFilter (const True) q
+
+-- | Remove the minimum entry from the queue, discarding any
+-- batches that do not satisfy the predicate.
+{-# INLINEABLE removeMinFilter #-}
+removeMinFilter :: Batch a => (Label a -> Bool) -> Queue a -> Maybe (Entry a, Queue a)
+removeMinFilter ok (Queue q) = do
+  (Best batch, q) <- Heap.removeMin q
+  if not (ok (batchLabel batch)) then removeMinFilter ok (Queue q) else
+    case unconsBatch batch of
+      (entry, Just batch') ->
+        Just (entry, Queue (Heap.insert (Best batch') q))
+      (entry, Nothing) ->
+        Just (entry, Queue q)
+
+-- | Map a function over all entries.
+-- The function must preserve the label of each batch,
+-- and must not split existing batches into two.
+{-# INLINEABLE mapMaybe #-}
+mapMaybe :: Batch a => (Entry a -> Maybe (Entry a)) -> Queue a -> Queue a
+mapMaybe f (Queue q) = Queue (Heap.mapMaybe g q)
+  where
+    g (Best batch) =
+      case Data.Maybe.mapMaybe f (unbatch batch) of
+        [] -> Nothing
+        is ->
+          case makeBatch (batchLabel batch) (sort is) of
+            [] -> Nothing
+            [batch'] -> Just (Best batch')
+            _ -> error "multiple batches produced"
+
+-- | Convert a queue into a list of batches, in unspecified order.
+{-# INLINEABLE toBatches #-}
+toBatches :: Queue a -> [a]
+toBatches (Queue q) = map unBest (Heap.toList q)
+
+-- | Convert a queue into a list of entries, in unspecified order.
+{-# INLINEABLE toList #-}
+toList :: Batch a => Queue a -> [Entry a]
+toList q = concatMap unbatch (toBatches q)
+
+{-# INLINEABLE size #-}
+size :: Batch a => Queue a -> Int
+size = sum . map batchSize . toBatches
+
+-- | A "standard" type of batches. By using @Queue (StandardBatch a)@,
+-- you will get a queue where entries have type @a@ and labels have
+-- type @()@.
+data StandardBatch a =
+  StandardBatch {
+    batch_best :: !a,
+    batch_rest :: {-# UNPACK #-} !(PackedSequence a) }
+
+instance Ord a => Eq (StandardBatch a) where
+  x == y = compare x y == EQ
+instance Ord a => Ord (StandardBatch a) where
+  compare = comparing batch_best
+
+instance (Ord a, Serialize a) => Batch (StandardBatch a) where
+  type Label (StandardBatch a) = ()
+  type Entry (StandardBatch a) = a
+
+  makeBatch _ (x:xs) = [StandardBatch x (PackedSequence.fromList xs)]
+  unconsBatch StandardBatch{..} =
+    (batch_best,
+     case PackedSequence.uncons batch_rest of
+       Nothing -> Nothing
+       Just (x, xs) -> Just (StandardBatch x xs))
+  batchLabel _ = ()
+  batchSize StandardBatch{..} = 1 + PackedSequence.size batch_rest
+
diff --git a/Data/ChurchList.hs b/Data/ChurchList.hs
--- a/Data/ChurchList.hs
+++ b/Data/ChurchList.hs
@@ -48,13 +48,11 @@
 
 instance Applicative ChurchList where
   {-# INLINE pure #-}
-  pure = return
+  pure = unit
   {-# INLINE (<*>) #-}
   (<*>) = liftM2 ($)
 
 instance Monad ChurchList where
-  {-# INLINE return #-}
-  return = unit
   {-# INLINE (>>=) #-}
   xs >>= f = join (fmap f xs)
 
diff --git a/Data/Label.hs b/Data/Label.hs
--- a/Data/Label.hs
+++ b/Data/Label.hs
@@ -1,7 +1,7 @@
 -- | Assignment of unique IDs to values.
 -- Inspired by the 'intern' package.
 
-{-# LANGUAGE RecordWildCards, ScopedTypeVariables, BangPatterns, MagicHash, RoleAnnotations #-}
+{-# LANGUAGE RecordWildCards, ScopedTypeVariables, BangPatterns, MagicHash, RoleAnnotations, CPP #-}
 module Data.Label(Label, unsafeMkLabel, labelNum, label, find) where
 
 import Data.IORef
@@ -124,7 +124,11 @@
 find (Label !(I32# n#)) = findWorker n#
 
 {-# NOINLINE findWorker #-}
+#if __GLASGOW_HASKELL__ >= 902
+findWorker :: Int32# -> a
+#else
 findWorker :: Int# -> a
+#endif
 findWorker n# =
   unsafeDupablePerformIO $ do
     let n = I32# n#
diff --git a/Data/Numbered.hs b/Data/Numbered.hs
--- a/Data/Numbered.hs
+++ b/Data/Numbered.hs
@@ -1,3 +1,7 @@
+-- | An array of key-value pairs, where the keys are integers.
+-- Can be accessed both as a map ("give me the value corresponding
+-- to the key 2") and as an array ("give me the 3rd key-value pair").
+-- Array-like access is fast; everything else is slow.
 module Data.Numbered(
   Numbered,
   empty, fromList, singleton, toList, size, (!),
@@ -10,6 +14,7 @@
 import Data.Int
 import Data.Maybe
 
+-- | An array of key-value pairs.
 data Numbered a =
   Numbered
     {-# UNPACK #-} !ByteArray
@@ -17,34 +22,46 @@
 
 instance Show a => Show (Numbered a) where show = show . toList
 
+-- | An empty array.
 empty :: Numbered a
 empty = fromList []
 
+-- | A singleton array.
 singleton :: Int -> a -> Numbered a
 singleton i x = fromList [(i, x)]
 
+-- | Convert a list of pairs to an array.
+-- Duplicate keys are allowed.
 fromList :: [(Int, a)] -> Numbered a
 fromList xs =
   Numbered
     (byteArrayFromList (map (fromIntegral . fst) xs :: [Int32]))
     (smallArrayFromList (map snd xs))
 
+-- | Convert an array to a list.
 toList :: Numbered a -> [(Int, a)]
 toList num =
   [num ! i | i <- [0..size num-1]]
 
+-- | Get the number of key-value pairs in an array. O(1) time.
 size :: Numbered a -> Int
 size (Numbered _ elems) = sizeofSmallArray elems
 
+-- | Index into the array. O(1) time.
 (!) :: Numbered a -> Int -> (Int, a)
 Numbered idxs elems ! i =
   (fromIntegral (indexByteArray idxs i :: Int32),
    indexSmallArray elems i)
 
+-- | Look up the value associated with a particular key.
+-- If the key occurs multiple times, any of its values
+-- may be returned. O(n) time.
 lookup :: Int -> Numbered a -> Maybe a
 lookup i num =
   List.lookup i (toList num)
 
+-- | Associate a value with a key. Any existing occurences
+-- of the key are removed. O(n) time.
 put :: Int -> a -> Numbered a -> Numbered a
 put i x num =
   fromList $ lt ++ [(i, x)] ++ gt
@@ -53,13 +70,20 @@
     lt = List.filter ((< i) . fst) xs
     gt = List.filter ((> i) . fst) xs
 
+-- | Remove a given key. O(n) time.
 delete :: Int -> Numbered a -> Numbered a
 delete i = fromList . List.filter ((/= i) . fst) . toList
 
+-- | Modify the value associated with a given key.
+-- If the key occurs multiple times, one of its values
+-- is chosen and the others deleted. In the call
+-- @modify k def f@, if the key @k@ is not present,
+-- the entry @k -> f def@ is added. O(n) time.
 modify :: Int -> a -> (a -> a) -> Numbered a -> Numbered a
 modify i def f num =
   put i (f (fromMaybe def (lookup i num))) num
 
+-- | Keep only keys satisfying a predicate.
 filter :: (a -> Bool) -> Numbered a -> Numbered a
 filter p = fromList . List.filter (p . snd) . toList
 
diff --git a/Data/PackedSequence.hs b/Data/PackedSequence.hs
new file mode 100644
--- /dev/null
+++ b/Data/PackedSequence.hs
@@ -0,0 +1,45 @@
+-- | Sequences which are stored compactly in memory
+-- by serialising their contents as a @ByteString@.
+module Data.PackedSequence(PackedSequence, empty, null, size, fromList, toList, uncons) where
+
+import Prelude hiding (null)
+import Data.Serialize
+import Data.ByteString(ByteString)
+import qualified Data.ByteString as BS
+import Data.List(unfoldr)
+
+-- | A sequence, stored in a serialised form
+data PackedSequence a =
+  Seq {-# UNPACK #-} !Int {-# UNPACK #-} !ByteString
+  deriving Eq
+
+-- | An empty sequence.
+empty :: PackedSequence a
+empty = Seq 0 BS.empty
+
+-- | Is a given sequency empty?
+null :: PackedSequence a -> Bool
+null s = size s == 0
+
+-- | Find the number of items in a sequence.
+size :: PackedSequence a -> Int
+size (Seq n _) = n
+
+-- | Convert a list into a sequence.
+{-# INLINEABLE fromList #-}
+fromList :: Serialize a => [a] -> PackedSequence a
+fromList xs = Seq (length xs) (runPut (mapM_ put xs))
+
+-- | Convert a sequence into a list.
+{-# INLINEABLE toList #-}
+toList :: Serialize a => PackedSequence a -> [a]
+toList = unfoldr uncons
+
+-- | Find and remove the first value from a sequence.
+{-# INLINEABLE uncons #-}
+uncons :: Serialize a => PackedSequence a -> Maybe (a, PackedSequence a)
+uncons (Seq 0 _) = Nothing
+uncons (Seq n bs) =
+  Just $ case runGetState get bs 0 of
+    Left err -> error err
+    Right (x, bs) -> (x, Seq (n-1) bs)
diff --git a/Twee.hs b/Twee.hs
--- a/Twee.hs
+++ b/Twee.hs
@@ -1,5 +1,5 @@
 -- | The main prover loop.
-{-# LANGUAGE RecordWildCards, MultiParamTypeClasses, GADTs, BangPatterns, OverloadedStrings, ScopedTypeVariables, GeneralizedNewtypeDeriving, PatternGuards, TypeFamilies #-}
+{-# LANGUAGE RecordWildCards, MultiParamTypeClasses, GADTs, BangPatterns, OverloadedStrings, ScopedTypeVariables, GeneralizedNewtypeDeriving, PatternGuards, TypeFamilies, FlexibleInstances #-}
 module Twee where
 
 import Twee.Base
@@ -19,8 +19,8 @@
 import Twee.Constraints
 import Twee.Utils
 import Twee.Task
-import qualified Twee.PassiveQueue as Queue
-import Twee.PassiveQueue(Queue, Passive(..))
+import qualified Data.BatchedQueue as Queue
+import Data.BatchedQueue(Queue)
 import qualified Data.IntMap.Strict as IntMap
 import Data.IntMap(IntMap)
 import Data.Maybe
@@ -36,6 +36,9 @@
 import qualified Data.IntSet as IntSet
 import Data.IntSet(IntSet)
 import Twee.Profile
+import Data.Ord
+import Data.PackedSequence(PackedSequence)
+import qualified Data.PackedSequence as PackedSequence
 
 ----------------------------------------------------------------------
 -- * Configuration and prover state.
@@ -65,7 +68,7 @@
     st_active_set     :: !(IntMap (Active f)),
     st_joinable       :: !(Index f (Equation f)),
     st_goals          :: ![Goal f],
-    st_queue          :: !(Queue Params),
+    st_queue          :: !(Queue Batch),
     st_next_active    :: {-# UNPACK #-} !Id,
     st_considered     :: {-# UNPACK #-} !Int64,
     st_simplified_at  :: {-# UNPACK #-} !Id,
@@ -174,20 +177,9 @@
 -- * The CP queue.
 ----------------------------------------------------------------------
 
-data Params
-instance Queue.Params Params where
-  type Score Params = Int
-  type Id Params = Id
-  type PackedId Params = Int32
-  type PackedScore Params = Int32
-  packScore _ = fromIntegral
-  unpackScore _ = fromIntegral
-  packId _ = fromIntegral
-  unpackId _ = fromIntegral
-
 -- | Compute all critical pairs from a rule.
 {-# INLINEABLE makePassives #-}
-makePassives :: Function f => Config f -> State f -> Active f -> [Passive Params]
+makePassives :: Function f => Config f -> State f -> Active f -> [Passive]
 makePassives config@Config{..} State{..} rule =
 -- XXX factor out depth calculation
   stampWith "make critical pair" length
@@ -198,30 +190,90 @@
     rules = IntMap.elems st_active_set
     ok rule = the rule < Depth cfg_max_cp_depth
 
+data Passive =
+  Passive {
+    passive_score :: {-# UNPACK #-} !Int32,
+    passive_rule1 :: {-# UNPACK #-} !Id,
+    passive_rule2 :: {-# UNPACK #-} !Id,
+    passive_how   :: !How }
+  deriving Eq
+
+instance Ord Passive where
+  compare = comparing f
+    where
+      f Passive{..} =
+        (passive_score,
+         intMax (fromIntegral passive_rule1) (fromIntegral passive_rule2),
+         intMin (fromIntegral passive_rule1) (fromIntegral passive_rule2),
+         passive_how)
+
+data Batch =
+  Batch {
+    batch_kind      :: !BatchKind,
+    batch_rule      :: {-# UNPACK #-} !Id,
+    batch_best      :: {-# UNPACK #-} !Passive,
+    batch_rest      :: {-# UNPACK #-} !(PackedSequence (Int32, Id, How)) }
+
+data BatchKind = Rule1 | Rule2 deriving Eq
+
+instance Queue.Batch Batch where
+  type Label Batch = Id
+  type Entry Batch = Passive
+
+  makeBatch rule ps =
+    make1 Rule1 ps1 ++ make1 Rule2 ps2
+    where
+      (ps1, ps2) = partition isRule1 ps
+      isRule1 Passive{..} = rule == passive_rule1
+
+      make1 _ [] = []
+      make1 kind (p:ps) =
+        [Batch {
+           batch_kind = kind,
+           batch_rule = rule,
+           batch_best = p,
+           batch_rest = 
+             PackedSequence.fromList $
+               [ (passive_score, if kind == Rule1 then passive_rule2 else passive_rule1, passive_how)
+               | Passive{..} <- ps ] }]
+
+  unconsBatch batch@Batch{..} =
+    (batch_best,
+     do (p, ps) <- PackedSequence.uncons batch_rest
+        return batch{batch_best = unpack batch_kind p, batch_rest = ps})
+    where
+      unpack Rule1 (score, rule2, how) =
+        Passive score batch_rule rule2 how
+      unpack Rule2 (score, rule1, how) =
+        Passive score rule1 batch_rule how
+
+  batchLabel Batch{..} = batch_rule
+  batchSize Batch{..} = 1 + PackedSequence.size batch_rest
+
 {-# INLINEABLE makePassive #-}
-makePassive :: Function f => Config f -> Overlap (Active f) f -> Passive Params
+makePassive :: Function f => Config f -> Overlap (Active f) f -> Passive
 makePassive Config{..} overlap@Overlap{..} =
   Passive {
     passive_score = fromIntegral (score cfg_critical_pairs depth overlap),
     passive_rule1 = active_id overlap_rule1,
     passive_rule2 = active_id overlap_rule2,
-    passive_pos   = packHow overlap_how }
+    passive_how   = overlap_how }
   where
     depth = succ (the overlap_rule1 `max` the overlap_rule2)
 
 -- | Turn a Passive back into an overlap.
 -- Doesn't try to simplify it.
 {-# INLINEABLE findPassive #-}
-findPassive :: forall f. Function f => State f -> Passive Params -> Maybe (Overlap (Active f) f)
+findPassive :: forall f. Function f => State f -> Passive -> Maybe (Overlap (Active f) f)
 findPassive State{..} Passive{..} = do
   rule1 <- IntMap.lookup (fromIntegral passive_rule1) st_active_set
   rule2 <- IntMap.lookup (fromIntegral passive_rule2) st_active_set
-  overlapAt (unpackHow passive_pos) rule1 rule2
+  overlapAt passive_how rule1 rule2
     (renameAvoiding (the rule2 :: Rule f) (the rule1)) (the rule2)
 
 -- | Renormalise a queued Passive.
 {-# INLINEABLE simplifyPassive #-}
-simplifyPassive :: Function f => Config f -> State f -> Passive Params -> Maybe (Passive Params)
+simplifyPassive :: Function f => Config f -> State f -> Passive -> Maybe (Passive)
 simplifyPassive Config{..} state@State{..} passive = do
   overlap <- findPassive state passive
   overlap <- simplifyOverlap (index_oriented st_rules) overlap
@@ -250,7 +302,7 @@
 
 -- | Enqueue a set of critical pairs.
 {-# INLINEABLE enqueue #-}
-enqueue :: Function f => State f -> Id -> [Passive Params] -> State f
+enqueue :: Function f => State f -> Id -> [Passive] -> State f
 enqueue state rule passives =
   state { st_queue = Queue.insert rule passives (st_queue state) }
 
@@ -272,7 +324,8 @@
        state { st_queue = queue, st_considered = st_considered + n })
   where
     deq !n queue = do
-      (passive, queue) <- Queue.removeMin queue
+      let ok id = fromIntegral id `IntMap.member` st_active_set
+      (passive, queue) <- Queue.removeMinFilter ok queue
       case findPassive state passive of
         Just (overlap@Overlap{overlap_eqn = t :=: u, overlap_rule1 = rule1, overlap_rule2 = rule2})
           | fromMaybe True (cfg_accept_term <*> pure t),
@@ -355,7 +408,7 @@
 
 -- Update the list of sampled critical pairs.
 {-# INLINEABLE sample #-}
-sample :: Function f => Int -> [Passive Params] -> State f -> State f
+sample :: Function f => Int -> [Passive] -> State f -> State f
 sample m passives state@State{..} =
   state{st_cp_sample = addSample (m, map find passives) st_cp_sample}
   where
@@ -367,13 +420,13 @@
 {-# INLINEABLE resetSample #-}
 resetSample :: Function f => Config f -> State f -> State f
 resetSample Config{..} state@State{..} =
-  foldl' sample1 state' (Queue.toList st_queue)
+  foldl' sample1 state' (Queue.toBatches st_queue)
   where
     state' =
       state {
         st_cp_sample = emptySample cfg_cp_sample_size }
 
-    sample1 state (n, passives) = sample n passives state
+    sample1 state batch = sample (Queue.batchSize batch) (Queue.unbatch batch) state
 
 -- Simplify the sampled critical pairs.
 -- (A sampled critical pair is replaced with Nothing if it can be
@@ -493,7 +546,7 @@
       where
         m = bound excl
 
-    bound excl = minimum . map (passiveMax excl) . concatMap snd . Queue.toList $ st_queue state
+    bound excl = minimum . map (passiveMax excl) . Queue.toList $ st_queue state
 
     passiveMax excl p = fromMaybe maxBound $ do
       Overlap{overlap_rule1 = r1, overlap_rule2 = r2} <- findPassive state p
@@ -690,7 +743,7 @@
           StateM.put $! recomputeGoals config state,
        newTask 60 0.01 $ do
           State{..} <- StateM.get
-          let !n = Queue.queueSize st_queue
+          let !n = Queue.size st_queue
           lift $ output_message (Status n)]
 
     let
diff --git a/Twee/Base.hs b/Twee/Base.hs
--- a/Twee/Base.hs
+++ b/Twee/Base.hs
@@ -28,10 +28,11 @@
 import Data.List hiding (singleton)
 import Data.Maybe
 import qualified Data.IntMap.Strict as IntMap
+import Data.Serialize
 
 -- | Represents a unique identifier (e.g., for a rule).
 newtype Id = Id { unId :: Int32 }
-  deriving (Eq, Ord, Show, Enum, Bounded, Num, Real, Integral)
+  deriving (Eq, Ord, Show, Enum, Bounded, Num, Real, Integral, Serialize)
 
 instance Pretty Id where
   pPrint = text . show . unId
diff --git a/Twee/CP.hs b/Twee/CP.hs
--- a/Twee/CP.hs
+++ b/Twee/CP.hs
@@ -16,6 +16,8 @@
 import qualified Twee.Proof as Proof
 import Twee.Proof(Derivation, congPath)
 import Data.Bits
+import Data.Serialize
+import Data.Int
 
 -- | The set of positions at which a term can have critical overlaps.
 data Positions f = NilP | ConsP {-# UNPACK #-} !Int !(Positions f)
@@ -62,7 +64,8 @@
     overlap_rule1 :: !a,
     -- | The rule which applies at some subterm.
     overlap_rule2 :: !a,
-    -- | The position in the critical term which is rewritten.
+    -- | The position in the critical term which is rewritten,
+    -- together with the direction of the two rules.
     overlap_how   :: {-# UNPACK #-} !How,
     -- | The top term of the critical pair
     overlap_top   :: {-# UNPACK #-} !(Term f),
@@ -70,31 +73,38 @@
     overlap_eqn   :: {-# UNPACK #-} !(Equation f) }
   deriving Show
 
-data Direction = Forwards | Backwards deriving (Eq, Enum, Show)
+data How =
+  How {
+    how_pos  :: {-# UNPACK #-} !Int,
+    how_dir1 :: !Direction,
+    how_dir2 :: !Direction }
+  deriving (Eq, Ord, Show)
 
+data Direction = Forwards | Backwards deriving (Eq, Ord, Enum, Show)
+
 direct :: Rule f -> Direction -> Rule f
 direct rule Forwards = rule
 direct rule Backwards = backwards rule
 
-data How =
-  How {
-    how_dir1 :: !Direction,
-    how_dir2 :: !Direction,
-    how_pos  :: {-# UNPACK #-} !Int }
-  deriving Show
-
-packHow :: How -> Int
-packHow How{..} =
-  fromEnum how_dir1 +
-  fromEnum how_dir2 `shiftL` 1 +
-  how_pos `shiftL` 2
+instance Serialize How where
+  put = put . packHow
+    where
+      packHow :: How -> Int32
+      packHow How{..} =
+        fromIntegral $
+        fromEnum how_dir1 +
+        fromEnum how_dir2 `shiftL` 1 +
+        how_pos `shiftL` 2
 
-unpackHow :: Int -> How
-unpackHow n =
-  How {
-    how_dir1 = toEnum (n .&. 1),
-    how_dir2 = toEnum ((n `shiftR` 1) .&. 1),
-    how_pos  = n `shiftR` 2 }
+  get = fmap unpackHow get
+    where
+      unpackHow :: Int32 -> How
+      unpackHow n0 =
+        let n = fromIntegral n0 in
+        How {
+          how_dir1 = toEnum (n .&. 1),
+          how_dir2 = toEnum ((n `shiftR` 1) .&. 1),
+          how_pos  = n `shiftR` 2 }
 
 -- | Represents the depth of a critical pair.
 newtype Depth = Depth Int deriving (Eq, Ord, Num, Real, Enum, Integral, Show)
@@ -135,14 +145,14 @@
 asymmetricOverlaps idx r1 r2 d1 d2 posns eq1 eq2 = do
   n <- positionsChurch posns
   ChurchList.fromMaybe $
-    overlapAt' (How d1 d2 n) r1 r2 eq1 eq2 >>=
+    overlapAt' (How n d1 d2) r1 r2 eq1 eq2 >>=
     simplifyOverlap idx
 
 -- | Create an overlap at a particular position in a term.
 -- Doesn't simplify the overlap.
 {-# INLINE overlapAt #-}
 overlapAt :: How -> a -> a -> Rule f -> Rule f -> Maybe (Overlap a f)
-overlapAt how@(How d1 d2 _) x1 x2 r1 r2 =
+overlapAt how@(How _ d1 d2) x1 x2 r1 r2 =
   overlapAt' how x1 x2 (unorient (direct r1 d1)) (unorient (direct r2 d2))
 
 {-# INLINE overlapAt' #-}
diff --git a/Twee/Equation.hs b/Twee/Equation.hs
--- a/Twee/Equation.hs
+++ b/Twee/Equation.hs
@@ -4,8 +4,6 @@
 
 import Twee.Base
 import Control.Monad
-import Data.List
-import Data.Ord
 
 --------------------------------------------------------------------------------
 -- * Equations.
diff --git a/Twee/Join.hs b/Twee/Join.hs
--- a/Twee/Join.hs
+++ b/Twee/Join.hs
@@ -153,7 +153,7 @@
     -- No need to do this symmetrically because addJoinable adds
     -- both orientations of each equation
   | or [ u == subst sub u'
-       | (sub, t' :=: u') <- Index.matches t eqns ] = True
+       | (sub, _ :=: u') <- Index.matches t eqns ] = True
 subsumed1 eqns idx (App f ts :=: App g us)
   | f == g =
     let
diff --git a/Twee/PassiveQueue.hs b/Twee/PassiveQueue.hs
deleted file mode 100644
--- a/Twee/PassiveQueue.hs
+++ /dev/null
@@ -1,201 +0,0 @@
--- | A queue of passive critical pairs, using a memory-efficient representation.
-{-# LANGUAGE TypeFamilies, RecordWildCards, FlexibleContexts, ScopedTypeVariables, StandaloneDeriving #-}
-module Twee.PassiveQueue(
-  Params(..),
-  Queue,
-  Passive(..),
-  empty, insert, removeMin, mapMaybe, toList, queueSize) where
-
-import qualified Data.Heap as Heap
-import qualified Data.Vector.Unboxed as Vector
-import Data.Int
-import Data.List hiding (insert)
-import qualified Data.Maybe
-import Data.Ord
-import Data.Proxy
-import Twee.Utils
-
--- | A datatype representing all the type parameters of the queue.
-class (Eq (Id params), Integral (Id params), Ord (Score params), Vector.Unbox (PackedScore params), Vector.Unbox (PackedId params)) => Params params where
-  -- | The score assigned to critical pairs. Smaller scores are better.
-  type Score params
-  -- | The type of ID numbers used to name rules.
-  type Id params
-
-  -- | A 'Score' packed for storage into a 'Vector.Vector'. Must be an instance of 'Vector.Unbox'.
-  type PackedScore params
-  -- | An 'Id' packed for storage into a 'Vector.Vector'. Must be an instance of 'Vector.Unbox'.
-  type PackedId params
-
-  -- | Pack a 'Score'.
-  packScore :: proxy params -> Score params -> PackedScore params
-  -- | Unpack a 'PackedScore'.
-  unpackScore :: proxy params -> PackedScore params -> Score params
-  -- | Pack an 'Id'.
-  packId :: proxy params -> Id params -> PackedId params
-  -- | Unpack a 'PackedId'.
-  unpackId :: proxy params -> PackedId params -> Id params
-
--- | A critical pair queue.
-newtype Queue params =
-  Queue (Heap.Heap (PassiveSet params))
-
--- All passive CPs generated from one given rule.
-data PassiveSet params =
-  PassiveSet {
-    passiveset_best  :: {-# UNPACK #-} !(Passive params),
-    passiveset_rule  :: !(Id params),
-    -- CPs where the rule is the left-hand rule
-    passiveset_left  :: {-# UNPACK #-} !(Vector.Vector (PackedScore params, PackedId params, Int32)),
-    -- CPs where the rule is the right-hand rule
-    passiveset_right :: {-# UNPACK #-} !(Vector.Vector (PackedScore params, PackedId params, Int32)) }
-instance Params params => Eq (PassiveSet params) where
-  x == y = compare x y == EQ
-instance Params params => Ord (PassiveSet params) where
-  compare = comparing passiveset_best
-
--- A smart-ish constructor.
-{-# INLINEABLE mkPassiveSet #-}
-mkPassiveSet ::
-  Params params =>
-  Proxy params ->
-  Id params ->
-  Vector.Vector (PackedScore params, PackedId params, Int32) ->
-  Vector.Vector (PackedScore params, PackedId params, Int32) ->
-  Maybe (PassiveSet params)
-mkPassiveSet proxy rule left right
-  | Vector.null left && Vector.null right = Nothing
-  | not (Vector.null left) &&
-    (Vector.null right || l <= r) =
-    Just PassiveSet {
-      passiveset_best  = l,
-      passiveset_rule  = rule,
-      passiveset_left  = Vector.tail left,
-      passiveset_right = right }
-    -- In this case we must have not (Vector.null right).
-  | otherwise =
-    Just PassiveSet {
-      passiveset_best  = r,
-      passiveset_rule  = rule,
-      passiveset_left  = left,
-      passiveset_right = Vector.tail right }
-  where
-    l = unpack proxy rule True (Vector.head left)
-    r = unpack proxy rule False (Vector.head right)
-
--- Unpack a triple into a Passive.
-{-# INLINEABLE unpack #-}
-unpack :: Params params => Proxy params -> Id params -> Bool -> (PackedScore params, PackedId params, Int32) -> Passive params
-unpack proxy rule isLeft (score, id, pos) =
-  Passive {
-    passive_score = unpackScore proxy score,
-    passive_rule1 = if isLeft then rule else rule',
-    passive_rule2 = if isLeft then rule' else rule,
-    passive_pos = fromIntegral pos }
-  where
-    rule' = unpackId proxy id
-
--- Make a PassiveSet from a list of Passives.
-{-# INLINEABLE makePassiveSet #-}
-makePassiveSet :: forall params. Params params => Id params -> [Passive params] -> Maybe (PassiveSet params)
-makePassiveSet _ [] = Nothing
-makePassiveSet rule ps
-  | and [passive_rule2 p == rule | p <- right] =
-    mkPassiveSet proxy rule
-      (Vector.fromList (map (pack True) (sort left)))
-      (Vector.fromList (map (pack False) (sort right)))
-  | otherwise = error "rule id does not occur in passive"
-  where
-    proxy :: Proxy params
-    proxy = Proxy
-    
-    (left, right) = partition (\p -> passive_rule1 p == rule) ps
-    pack isLeft Passive{..} =
-      (packScore proxy passive_score,
-       packId proxy (if isLeft then passive_rule2 else passive_rule1),
-       fromIntegral passive_pos)
-
--- Convert a PassiveSet back into a list of Passives.
-{-# INLINEABLE unpackPassiveSet #-}
-unpackPassiveSet :: forall params.Params params => PassiveSet params -> (Int, [Passive params])
-unpackPassiveSet PassiveSet{..} =
-  (1 + Vector.length passiveset_left + Vector.length passiveset_right,
-   passiveset_best:
-   map (unpack proxy passiveset_rule True) (Vector.toList passiveset_left) ++
-   map (unpack proxy passiveset_rule False) (Vector.toList passiveset_right))
-  where
-    proxy :: Proxy params
-    proxy = Proxy
-
--- Find and remove the best element from a PassiveSet.
-{-# INLINEABLE unconsPassiveSet #-}
-unconsPassiveSet :: forall params. Params params => PassiveSet params -> (Passive params, Maybe (PassiveSet params))
-unconsPassiveSet PassiveSet{..} =
-  (passiveset_best, mkPassiveSet (Proxy :: Proxy params) passiveset_rule passiveset_left passiveset_right)
-
--- | A queued critical pair.
-data Passive params =
-  Passive {
-    -- | The score of this critical pair.
-    passive_score :: !(Score params),
-    -- | The rule which does the outermost rewrite in this critical pair.
-    passive_rule1 :: !(Id params),
-    -- | The rule which does the innermost rewrite in this critical pair.
-    passive_rule2 :: !(Id params),
-    -- | The position of the overlap. See 'Twee.CP.overlap_pos'.
-    passive_pos   :: {-# UNPACK #-} !Int }
-
-instance Params params => Eq (Passive params) where
-  x == y = compare x y == EQ
-
-instance Params params => Ord (Passive params) where
-  compare = comparing f
-    where
-      f Passive{..} =
-        (passive_score,
-         intMax (fromIntegral passive_rule1) (fromIntegral passive_rule2),
-         intMin (fromIntegral passive_rule1) (fromIntegral passive_rule2),
-         passive_pos)
-
--- | The empty queue.
-empty :: Queue params
-empty = Queue Heap.empty
-
--- | Add a set of 'Passive's to the queue.
-{-# INLINEABLE insert #-}
-insert :: Params params => Id params -> [Passive params] -> Queue params -> Queue params
-insert rule passives (Queue q) =
-  Queue $
-  case makePassiveSet rule passives of
-    Nothing -> q
-    Just p -> Heap.insert p q
-
--- | Remove the minimum 'Passive' from the queue.
-{-# INLINEABLE removeMin #-}
-removeMin :: Params params => Queue params -> Maybe (Passive params, Queue params)
-removeMin (Queue q) = do
-  (passiveset, q) <- Heap.removeMin q
-  case unconsPassiveSet passiveset of
-    (passive, Just passiveset') ->
-      Just (passive, Queue (Heap.insert passiveset' q))
-    (passive, Nothing) ->
-      Just (passive, Queue q)
-
--- | Map a function over all 'Passive's.
-{-# INLINEABLE mapMaybe #-}
-mapMaybe :: Params params => (Passive params -> Maybe (Passive params)) -> Queue params -> Queue params
-mapMaybe f (Queue q) = Queue (Heap.mapMaybe g q)
-  where
-    g passiveSet@PassiveSet{..} =
-      makePassiveSet passiveset_rule $ Data.Maybe.mapMaybe f $
-        snd (unpackPassiveSet passiveSet)
-
--- | Convert a queue into a list of 'Passive's.
--- The 'Passive's are produced in batches, with each batch labelled
--- with its size.
-{-# INLINEABLE toList #-}
-toList :: Params params => Queue params -> [(Int, [Passive params])]
-toList (Queue h) = map unpackPassiveSet (Heap.toList h)
-
-queueSize :: Params params => Queue params -> Int
-queueSize = sum . map fst . toList
diff --git a/Twee/Term.hs b/Twee/Term.hs
--- a/Twee/Term.hs
+++ b/Twee/Term.hs
@@ -70,7 +70,9 @@
 import qualified Twee.Term.Core as Core
 import Data.List hiding (lookup, find, singleton)
 import Data.Maybe
+#if __GLASGOW_HASKELL__ < 804
 import Data.Semigroup(Semigroup(..))
+#endif
 import Data.IntMap.Strict(IntMap)
 import qualified Data.IntMap.Strict as IntMap
 import Control.Arrow((&&&))
@@ -300,7 +302,7 @@
         -- (n = minBound, m = maxBound), which is OK.
         mconcat [emitVar (V x) | x <- [0..n-m+1]]
 
-    loop !_ !_ !_ !_ | False = undefined
+    loop !_ !_ !_ !_ | never = undefined
     loop sub _ Empty [] = sub
     loop sub Empty _ _ = sub
     loop sub vs Empty (t:ts) = loop sub vs t ts
@@ -464,7 +466,7 @@
 unifyListTriFrom !t !u (Triangle !sub) =
   fmap Triangle (loop sub t u)
   where
-    loop !_ !_ !_ | False = undefined
+    loop !_ !_ !_ | never = undefined
     loop sub (ConsSym{hd = t, tl = ts, rest = ts1}) u = do
       ConsSym{hd = u, tl = us, rest =  us1} <- Just u
       case (t, u) of
@@ -668,7 +670,7 @@
 replacePosition :: (Build a, BuildFun a ~ f) => Int -> a -> TermList f -> Builder f
 replacePosition n !x = aux n
   where
-    aux !_ !_ | False = undefined
+    aux !_ !_ | never = undefined
     aux _ Empty = mempty
     aux 0 (Cons _ t) = builder x `mappend` builder t
     aux n (Cons (Var x) t) = var x `mappend` aux (n-1) t
@@ -684,7 +686,7 @@
 replacePositionSub :: (Substitution sub, SubstFun sub ~ f) => sub -> Int -> TermList f -> TermList f -> Builder f
 replacePositionSub sub n !x = aux n
   where
-    aux !_ !_ | False = undefined
+    aux !_ !_ | never = undefined
     aux _ Empty = mempty
     aux n (Cons t u)
       | n < len t = inside n t `mappend` outside u
diff --git a/Twee/Term/Core.hs b/Twee/Term/Core.hs
--- a/Twee/Term/Core.hs
+++ b/Twee/Term/Core.hs
@@ -24,7 +24,6 @@
 import GHC.Prim
 import GHC.ST hiding (liftST)
 import Data.Ord
-import Data.Semigroup(Semigroup(..))
 import Twee.Profile
 
 --------------------------------------------------------------------------------
diff --git a/Twee/Utils.hs b/Twee/Utils.hs
--- a/Twee/Utils.hs
+++ b/Twee/Utils.hs
@@ -1,6 +1,6 @@
 -- | Miscellaneous utility functions.
 
-{-# LANGUAGE CPP, MagicHash #-}
+{-# LANGUAGE CPP, MagicHash, GeneralizedNewtypeDeriving #-}
 module Twee.Utils where
 
 import Control.Arrow((&&&))
@@ -12,6 +12,7 @@
 import GHC.Types
 import Data.Bits
 import System.Random
+import Data.Serialize
 --import Test.QuickCheck hiding ((.&.))
 
 repeatM :: Monad m => m a -> m [a]
@@ -177,3 +178,45 @@
 foldn :: (a -> a) -> a -> Int -> a
 foldn _ e 0 = e
 foldn op e n | n > 0 = op (foldn op e (n-1))
+
+newtype U8 = U8 Int deriving (Eq, Ord, Num, Real, Enum, Integral)
+
+-- Untested!
+instance Serialize U8 where
+  put (U8 n)
+    | n < 0x80 = putWord8 (fromIntegral n)
+    | n < 0x4000 = do
+      putWord16be (fromIntegral n + 0x8000)
+    | otherwise = do
+      putWord32be (fromIntegral n + 0xc0000000)
+  get = do
+    x <- lookAhead getWord8
+    if x < 0x80 then fromIntegral <$> getWord8
+    else if x < 0xc0 then do
+      n <- getWord16be
+      return (fromIntegral (n - 0x8000))
+    else do
+      n <- getWord32be
+      return (fromIntegral (n - 0xc0000000))
+
+-- Untested!
+newtype U16 = U16 Int deriving (Eq, Ord, Num, Real, Enum, Integral)
+instance Serialize U16 where
+  put (U16 n)
+    | n < 0x8000 = do
+      putWord16be (fromIntegral n)
+    | otherwise = do
+      putWord32be (fromIntegral n + 0x80000000)
+  get = do
+    x <- lookAhead getWord8
+    if x < 0x80 then fromIntegral <$> getWord16be
+    else do
+      n <- getWord32be
+      return (fromIntegral (n - 0x80000000))
+
+-- Can be used to write strictness annotations e.g.
+-- f !_ !_ | never = undefined
+-- which otherwise trigger a spurious warning from GHC.
+{-# INLINE never #-}
+never :: Bool
+never = False
diff --git a/twee-lib.cabal b/twee-lib.cabal
--- a/twee-lib.cabal
+++ b/twee-lib.cabal
@@ -1,5 +1,5 @@
 name:                twee-lib
-version:             2.4.1
+version:             2.4.2
 synopsis:            An equational theorem prover
 homepage:            http://github.com/nick8325/twee
 license:             BSD3
@@ -54,7 +54,6 @@
     Twee.Index
     Twee.Join
     Twee.KBO
-    Twee.PassiveQueue
     Twee.Pretty
     Twee.Profile
     Twee.Proof
@@ -65,10 +64,12 @@
     Twee.Utils
     Data.Label
   other-modules:
+    Data.BatchedQueue
     Data.ChurchList
     Data.DynamicArray
     Data.Heap
     Data.Numbered
+    Data.PackedSequence
     Twee.Term.Core
 
   build-depends:
@@ -79,11 +80,12 @@
     pretty >= 1.1.2.0,
     ghc-prim,
     primitive >= 0.7.1.0,
-    vector,
     uglymemo,
-    random
+    random,
+    bytestring,
+    cereal
   hs-source-dirs:      .
-  ghc-options:         -W -fno-warn-incomplete-patterns
+  ghc-options:         -W -fno-warn-incomplete-patterns -fno-warn-dodgy-imports
   default-language:    Haskell2010
 
   if flag(llvm)