diff --git a/Data/BatchedQueue.hs b/Data/BatchedQueue.hs
--- a/Data/BatchedQueue.hs
+++ b/Data/BatchedQueue.hs
@@ -1,5 +1,5 @@
 -- | A queue where entries can be added in batches and stored compactly.
-{-# LANGUAGE TypeFamilies, RecordWildCards, FlexibleContexts, ScopedTypeVariables #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
 module Data.BatchedQueue(
   Queue, Batch(..), StandardBatch, unbatch, empty, insert, removeMin, removeMinFilter, mapMaybe, toBatches, toList, size) where
 
@@ -8,11 +8,12 @@
 import qualified Data.Maybe
 import Data.PackedSequence(PackedSequence)
 import qualified Data.PackedSequence as PackedSequence
-import Data.Serialize
+import qualified Data.Binary as Cereal
+import Data.Binary.Sharing
 import Data.Ord
 
 -- | A queue of batches.
-newtype Queue a = Queue (Heap.Heap (Best a))
+newtype Queue a = Queue (Heap.Heap (Best a)) deriving Binary
 
 -- | The type of batches must be a member of this class.
 class Ord (Entry a) => Batch a where
@@ -47,7 +48,7 @@
   type Label a = ()
 
 -- A newtype wrapper for batches which compares the smallest entry.
-newtype Best a = Best { unBest :: a }
+newtype Best a = Best { unBest :: a } deriving Binary
 instance Batch a => Eq (Best a) where x == y = compare x y == EQ
 instance Batch a => Ord (Best a) where
   {-# INLINEABLE compare #-}
@@ -130,7 +131,7 @@
 instance Ord a => Ord (StandardBatch a) where
   compare = comparing batch_best
 
-instance (Ord a, Serialize a) => Batch (StandardBatch a) where
+instance (Ord a, Cereal.Binary a) => Batch (StandardBatch a) where
   type Label (StandardBatch a) = ()
   type Entry (StandardBatch a) = a
 
diff --git a/Data/Binary/Sharing.hs b/Data/Binary/Sharing.hs
new file mode 100644
--- /dev/null
+++ b/Data/Binary/Sharing.hs
@@ -0,0 +1,424 @@
+-- | A serialisation library with support for sharing. Built on top of binary.
+
+{-# LANGUAGE ConstraintKinds, GADTs, DerivingVia, TypeSynonymInstances, FlexibleInstances, DefaultSignatures, DeriveAnyClass, DeriveFunctor, TupleSections #-}
+module Data.Binary.Sharing(Binary(..), Shared(..), Put, PutM, encode, encodeFile, runPut, liftPut, unliftPut, Get, decode, decodeFile, runGet, liftGet, unliftGet, putList, getList, putWord8, getWord8, putInt8, getInt8, putIntegral, getIntegral, ReadShowBinary(..)) where
+import qualified Data.Binary as S
+import qualified Data.Binary.Get as S
+import qualified Data.Binary.Put as S
+import Data.Typeable
+import qualified Data.HashMap.Strict as HashMap
+import Data.HashMap.Strict(HashMap)
+import Data.Maybe
+import GHC.Generics
+import Data.Hashable
+import Control.Monad
+import Data.Bits
+import Data.Word
+import Data.Int
+import Data.Char
+import qualified Data.ByteString.Lazy as BS
+import qualified Data.ByteString as BSS
+import Control.Monad.Trans.State.Strict hiding (get, put)
+import qualified Control.Monad.Trans.State.Strict as State
+import qualified Data.Primitive.SmallArray as SmallArray
+import qualified Data.Foldable as Foldable
+import qualified Data.Map as Map
+import qualified Data.IntMap as IntMap
+import qualified Data.Set as Set
+import qualified Data.IntSet as IntSet
+import qualified Data.HashSet as HashSet
+
+----------------------------------------------------------------------
+-- The basic serialiser/deserialiser types.
+--
+-- The idea is that both serialisation and deserialisation maintain a
+-- store of shared values we have already seen (each associated with an
+-- ID). When we emit a value we have already seen, we instead just emit
+-- its ID. This is handled in the "Binary (Shared a)" instance.
+----------------------------------------------------------------------
+
+-- | A serialiser.
+newtype PutM a = PutM { unPutM :: Store -> S.PutM (a, Store) } deriving Functor
+-- Note we can't use StateT because then generalised newtype deriving doesn't work
+instance Applicative PutM where
+  pure x = PutM $ \store -> pure (x, store)
+  mf <*> mx = mf >>= \f -> mx >>= \x -> pure (f x)
+instance Monad PutM where
+  mx >>= f =
+    PutM $ \store -> do
+      (x, store) <- unPutM mx store
+      unPutM (f x) store
+type Put = PutM ()
+
+instance Semigroup Put where
+  mx <> my = do { mx; my }
+
+instance Monoid Put where
+  mempty = pure mempty
+
+-- Lift a state-monadic computation into Put.
+liftStatePut :: State Store a -> PutM a
+liftStatePut act = PutM $ \store -> return (runState act store)
+
+-- | Lift a binary serialiser into Put.
+liftPut :: S.PutM a -> PutM a
+liftPut putter = PutM $ \store -> (, store) <$> putter
+
+-- | Convert a 'Put' back into a binary serialiser.
+unliftPut :: PutM a -> S.PutM a
+unliftPut (PutM putter) = fst <$> putter emptyStore
+
+-- | Serialise a value.
+runPut :: Put -> BS.ByteString
+runPut = S.runPut . unliftPut
+
+-- | Serialise a value.
+encode :: Binary a => a -> BS.ByteString
+encode = runPut . put
+
+-- | Serialise a value to a file.
+encodeFile :: Binary a => FilePath -> a -> IO ()
+encodeFile path = BS.writeFile path . encode
+
+-- | A deserialiser.
+newtype Get a = Get { unGet :: Store -> S.Get (a, Store) } deriving Functor
+instance Applicative Get where
+  pure x = Get $ \store -> pure (x, store)
+  mf <*> mx = mf >>= \f -> mx >>= \x -> pure (f x)
+instance Monad Get where
+  mx >>= f =
+    Get $ \store -> do
+      (x, store) <- unGet mx store
+      unGet (f x) store
+
+-- Lift a state-monadic computation into Get.
+liftStateGet :: State Store a -> Get a
+liftStateGet act = Get $ \store -> return (runState act store)
+
+-- | Lift a binary serialiser into Get.
+liftGet :: S.Get a -> Get a
+liftGet getter = Get $ \store -> (, store) <$> getter
+
+-- | Convert a 'Get' back into a binary serialiser.
+unliftGet :: Get a -> S.Get a
+unliftGet (Get getter) = fst <$> getter emptyStore
+
+-- | Deserialise a value.
+runGet :: Get a -> BS.ByteString -> a
+runGet = S.runGet . unliftGet
+
+-- | Deserialise a value.
+decode :: Binary a => BS.ByteString -> a
+decode = runGet get
+
+-- | Deserialise a value from a file.
+decodeFile :: Binary a => FilePath -> IO a
+decodeFile path = decode <$> BS.readFile path
+
+----------------------------------------------------------------------
+-- The sharing primitive.
+----------------------------------------------------------------------
+
+-- | A newtype wrapper which uses sharing on serialisation.
+-- If the same 'Shared' value is 'put' multiple times, only the first
+-- occurrence will be serialised in full and the later ones will
+-- instead serialise as a "pointer" to the first one. The test for
+-- whether a value is the same as a previous one uses '(==)'.
+newtype Shared a = Shared { getShared :: a } deriving (Eq, Show)
+
+-- The binary format for a "Shared a".
+-- The first time a given Shared value appears, we allocate a key (ID) for
+-- it and emit it as a 'Let'; if it reoccurs, we emit a 'Ref' to the existing ID.
+data SharedEncoding a = Let Key a | Ref Key
+
+instance Binary a => Binary (SharedEncoding a) where
+  put (Let key x) = do
+    put (key `unsafeShiftL` 1)
+    put x
+  put (Ref key) = do
+    put (key `unsafeShiftL` 1 + 1)
+
+  get = do
+    keyTag <- get
+    let key = keyTag `unsafeShiftR` 1
+    case testBit keyTag 0 of
+      False -> do -- Let
+        x <- get
+        return (Let key x)
+      True -> -- Ref
+        return (Ref key)
+
+instance (Typeable a, Eq a, Hashable a, Binary a) => Binary (Shared a) where
+  put (Shared x) = do
+    mkey <- liftStatePut (lookupValue x)
+    case mkey of
+      Just key ->
+        put (Ref key :: SharedEncoding a)
+      Nothing -> do
+        key <- liftStatePut reserveKey
+        put (Let key x)
+        liftStatePut (addValue key x)
+
+  get = Shared <$> do
+    value <- get
+    case value of
+      Let key x -> do
+        liftStateGet (addValue key x)
+        return x
+      Ref key ->
+        liftStateGet (lookupKey key)
+
+----------------------------------------------------------------------
+-- The store of previously-seen values.
+----------------------------------------------------------------------
+
+data Store =
+  Store {
+    -- Maps between values and ID numbers.
+    store_keys :: HashMap Key Value,
+    store_values :: HashMap Value Key,
+    -- The next available ID number.
+    store_next_key :: Key }
+type Key = Integer
+
+-- Useful for making heterogeneous maps.
+data Value where
+  Value :: (Eq a, Hashable a, Typeable a) => a -> Value
+
+instance Eq Value where
+  Value x == Value y =
+    case cast x of
+      Just x' -> x' == y
+      Nothing -> error "type error"
+
+instance Hashable Value where
+  hashWithSalt s (Value x) = hashWithSalt s (typeOf x, x)
+
+emptyStore :: Store
+emptyStore = Store HashMap.empty HashMap.empty 0
+
+-- Check if an existing value exists in the store.
+lookupValue :: (Eq a, Hashable a, Typeable a) => a -> State Store (Maybe Key)
+lookupValue x = do
+  let value = Value x
+  Store{..} <- State.get
+  return (fromIntegral <$> HashMap.lookup value store_values)
+
+-- Allocate a new key.
+reserveKey :: Monad m => StateT Store m Key
+reserveKey = do
+  store@Store{..} <- State.get
+  State.put store{store_next_key = store_next_key+1}
+  return (fromIntegral store_next_key)
+
+-- Add a new value to the store.
+addValue :: (Eq a, Hashable a, Typeable a) => Key -> a -> State Store ()
+addValue key x = do
+  let value = Value x
+  store@Store{..} <- State.get
+  when (HashMap.member key store_keys) $ error "key already found"
+  when (HashMap.member value store_values) $ error "value already found"
+  State.put store{
+    store_keys = HashMap.insert key value store_keys,
+    store_values = HashMap.insert value key store_values }
+
+-- Find a value by ID number.
+lookupKey :: Typeable a => Key -> State Store a
+lookupKey key = do
+  Store{..} <- State.get
+  case HashMap.lookup key store_keys of
+    Just (Value x) -> return (fromJust (cast x))
+    Nothing -> error ("invalid value " ++ show key ++ " " ++ show store_next_key)
+
+----------------------------------------------------------------------
+-- Primitive serialisers.
+----------------------------------------------------------------------
+
+putWord8 = liftPut . S.putWord8
+getWord8 = liftGet S.getWord8
+putInt8 = liftPut . S.putInt8
+getInt8 = liftGet S.getInt8
+
+putIntegral :: (Integral a, Bits a) => a -> Put
+putIntegral n
+  | toInteger n >= -1 && toInteger n < 126 =
+    putWord8 (clearBit (fromIntegral n) 7)
+  | otherwise = do
+    putWord8 (setBit (fromIntegral n) 7)
+    putIntegral (n `shiftR` 7)
+
+getIntegral :: (Integral a, Bits a) => Get a
+getIntegral = getIntegral' 0 0
+
+getIntegral' :: (Integral a, Bits a) => Int -> a -> Get a
+getIntegral' !k !n = do
+  x <- getWord8
+  let !n' = n + fromIntegral (clearBit x 7) `shiftL` k
+  if testBit x 7 then getIntegral' (k+7) n'
+    else if x == 127 then return (n' - (1 `shiftL` (k+7)))
+    else return n'
+
+-- QuickCheck property:
+-- quickCheck (withNumTests 1000000 (withMaxSize 100000 (\x -> runGet getIntegral (runPut (putIntegral (x :: Int))) === Right x)))
+-- TODO: add to test suite
+
+putList :: (a -> Put) -> [a] -> Put
+putList putter xs = do
+  put (length xs)
+  mapM_ putter xs
+
+getList :: Get a -> Get [a]
+getList getter = do
+  len <- get
+  replicateM len getter
+
+----------------------------------------------------------------------
+-- A class for serialisation/deserialisation.
+----------------------------------------------------------------------
+
+class Binary a where
+  put :: a -> Put
+  get :: Get a
+
+  default put :: (Generic a, GBinary (Rep a)) => a -> Put
+  put x = gput (from x)
+
+  default get :: (Generic a, GBinary (Rep a)) => Get a
+  get = to <$> gget
+
+instance Binary Int where { put = putIntegral; get = getIntegral }
+instance Binary Int8 where { put = putInt8; get = getInt8 }
+instance Binary Int16 where { put = putIntegral; get = getIntegral }
+instance Binary Int32 where { put = putIntegral; get = getIntegral }
+instance Binary Int64 where { put = putIntegral; get = getIntegral }
+instance Binary Word where { put = putIntegral; get = getIntegral }
+instance Binary Word8 where { put = putWord8; get = getWord8 }
+instance Binary Word16 where { put = putIntegral; get = getIntegral }
+instance Binary Word32 where { put = putIntegral; get = getIntegral }
+instance Binary Word64 where { put = putIntegral; get = getIntegral }
+instance Binary Integer where { put = putIntegral; get = getIntegral }
+instance Binary Char where { put = putIntegral . ord; get = chr <$> getIntegral }
+instance Binary BS.ByteString where { put = liftPut . S.put; get = liftGet S.get }
+instance Binary BSS.ByteString where { put = liftPut . S.put; get = liftGet S.get }
+instance Binary Float where { put = liftPut. S.put; get = liftGet S.get }
+instance Binary Double where { put = liftPut . S.put; get = liftGet S.get }
+deriving instance Binary Bool
+deriving instance Binary ()
+deriving instance (Binary a, Binary b) => Binary (a, b)
+deriving instance (Binary a, Binary b, Binary c) => Binary (a, b, c)
+deriving instance (Binary a, Binary b, Binary c, Binary d) => Binary (a, b, c, d)
+deriving instance (Binary a, Binary b, Binary c, Binary d, Binary e) => Binary (a, b, c, d, e)
+deriving instance Binary a => Binary (Maybe a)
+deriving instance (Binary a, Binary b) => Binary (Either a b)
+instance Binary a => Binary (SmallArray.SmallArray a) where
+  put = put . Foldable.toList
+  get = SmallArray.smallArrayFromList <$> get
+
+-- | Serialise a value via read/show.
+newtype ReadShowBinary a = ReadShowBinary { getReadShowBinary :: a }
+instance (Show a, Read a) => Binary (ReadShowBinary a) where
+  put = put . show . getReadShowBinary
+  get = ReadShowBinary . read <$> get
+
+instance Binary a => Binary [a] where
+  put = putList put
+  get = getList get
+
+instance (Binary k, Binary v, Ord k) => Binary (Map.Map k v) where
+  put = put . Map.toList
+  get = Map.fromList <$> get
+
+instance (Binary k, Binary v, Hashable k) => Binary (HashMap k v) where
+  put = put . HashMap.toList
+  get = HashMap.fromList <$> get
+
+instance Binary v => Binary (IntMap.IntMap v) where
+  put = put . IntMap.toList
+  get = IntMap.fromList <$> get
+
+instance (Binary k, Ord k) => Binary (Set.Set k) where
+  put = put . Set.toList
+  get = Set.fromList <$> get
+
+instance (Binary k, Hashable k) => Binary (HashSet.HashSet k) where
+  put = put . HashSet.toList
+  get = HashSet.fromList <$> get
+
+instance Binary IntSet.IntSet where
+  put = put . IntSet.toList
+  get = IntSet.fromList <$> get
+
+----------------------------------------------------------------------
+-- Generic instances.
+----------------------------------------------------------------------
+
+class GBinary f where
+  gput :: f a -> Put
+  gget :: Get (f a)
+
+  gconstructors :: proxy (f a) -> Int
+  gconstructors _ = 1
+
+  gconstructor :: f a -> Int
+  gconstructor _ = 0
+
+  gputConstructor :: f a -> Put
+  gputConstructor = gput
+
+  ggetConstructor :: Int -> Get (f a)
+  ggetConstructor 0 = gget
+  ggetConstructor _ = error "ggetConstructor: out of bounds"
+
+instance (GBinary f, GBinary g) => GBinary (f :*: g) where
+  gput (x :*: y) = do
+    gput x
+    gput y
+  gget = liftM2 (:*:) gget gget
+
+instance (GBinary f, GBinary g) => GBinary (f :+: g) where
+  gput x = do
+    put (gconstructor x)
+    gputConstructor x
+
+  gget = do
+    tag <- get
+    ggetConstructor tag
+
+  gconstructors _ =
+    gconstructors (Proxy :: Proxy (f a)) + gconstructors (Proxy :: Proxy (g a))
+
+  gconstructor (L1 x) = gconstructor x
+  gconstructor (R1 x) = gconstructor x + gconstructors (Proxy :: Proxy (f a))
+
+  gputConstructor (L1 x) = gputConstructor x
+  gputConstructor (R1 x) = gputConstructor x
+
+  ggetConstructor n
+    | n < m = L1 <$> ggetConstructor n
+    | otherwise = R1 <$> ggetConstructor (n-m)
+    where
+      m = gconstructors (Proxy :: Proxy (f a))
+
+instance GBinary f => GBinary (M1 i c f) where
+  gput (M1 x) = gput x
+  gget = M1 <$> gget
+  gconstructors _ = gconstructors (Proxy :: Proxy (f a))
+  gconstructor (M1 x) = gconstructor x
+  gputConstructor (M1 x) = gputConstructor x
+  ggetConstructor n = M1 <$> ggetConstructor n
+
+instance Binary a => GBinary (K1 i a) where
+  gput (K1 x) = put x
+  gget = K1 <$> get
+
+instance GBinary U1 where
+  gput U1 = return ()
+  gget = return U1
+
+instance GBinary V1 where
+  gput _ = error "gput: void"
+  gget = error "gget: void"
+  gconstructors _ = 0
+  gconstructor _ = error "gconstructor: void"
+  gputConstructor = error "gputConstructor: void"
+  ggetConstructor _ = error "ggetConstructor: void"
diff --git a/Data/ChurchList.hs b/Data/ChurchList.hs
--- a/Data/ChurchList.hs
+++ b/Data/ChurchList.hs
@@ -1,5 +1,5 @@
 -- | Church-encoded lists. Used in Twee.CP to make sure that fusion happens.
-{-# LANGUAGE Rank2Types, BangPatterns #-}
+{-# LANGUAGE Rank2Types #-}
 module Data.ChurchList where
 
 import Prelude(Functor(..), Applicative(..), Monad(..), Bool(..), Maybe(..), (.), ($), id)
diff --git a/Data/DynamicArray.hs b/Data/DynamicArray.hs
--- a/Data/DynamicArray.hs
+++ b/Data/DynamicArray.hs
@@ -1,6 +1,6 @@
 -- | Zero-indexed dynamic arrays, optimised for lookup.
 -- Modification is slow. Uninitialised indices have a default value.
-{-# LANGUAGE CPP #-}
+{-# LANGUAGE CPP, DeriveAnyClass #-}
 module Data.DynamicArray where
 
 #ifdef BOUNDS_CHECKS
@@ -10,6 +10,8 @@
 #endif
 import Control.Monad.ST
 import Data.List
+import Data.Binary.Sharing
+import GHC.Generics
 
 -- | A type which has a default value.
 class Default a where
@@ -22,6 +24,7 @@
     arrayStart    :: {-# UNPACK #-} !Int,
     -- | The contents of the array.
     arrayContents :: {-# UNPACK #-} !(P.SmallArray a) }
+  deriving (Generic, Binary)
 
 arraySize :: Array a -> Int
 arraySize = P.sizeofSmallArray . arrayContents
diff --git a/Data/Heap.hs b/Data/Heap.hs
--- a/Data/Heap.hs
+++ b/Data/Heap.hs
@@ -1,15 +1,18 @@
 -- | Skew heaps.
 
-{-# LANGUAGE BangPatterns, ScopedTypeVariables #-}
+{-# LANGUAGE DeriveAnyClass #-}
 module Data.Heap(
   Heap, empty, singleton, insert, removeMin, union, mapMaybe, size, toList) where
 
+import Data.Binary.Sharing
+import GHC.Generics
+
 -- | A heap.
 
 -- N.B.: arguments are not strict so code has to take care
 -- to force stuff appropriately.
 -- The Int field is the size of the heap.
-data Heap a = Nil | Node {-# UNPACK #-} !Int a (Heap a) (Heap a) deriving Show
+data Heap a = Nil | Node {-# UNPACK #-} !Int a (Heap a) (Heap a) deriving (Show, Generic, Binary)
 
 -- | Take the union of two heaps.
 {-# INLINEABLE union #-}
diff --git a/Data/Intern.hs b/Data/Intern.hs
--- a/Data/Intern.hs
+++ b/Data/Intern.hs
@@ -1,28 +1,30 @@
 -- | Interning, annotating values with unique IDs.
 
-{-# LANGUAGE RecordWildCards, ScopedTypeVariables, BangPatterns, MagicHash, RoleAnnotations, CPP, PatternSynonyms, ViewPatterns, ConstraintKinds #-}
+{-# LANGUAGE MagicHash, RoleAnnotations, CPP, PatternSynonyms, ViewPatterns, ConstraintKinds, GeneralizedNewtypeDeriving #-}
 module Data.Intern(Intern, Sym, pattern Sym, intern, unintern, unsafeMkSym, symId) where
 
 import Data.IORef
 import System.IO.Unsafe
-import qualified Data.Map.Strict as Map
-import Data.Map.Strict(Map)
+import qualified Data.HashMap.Strict as HashMap
+import Data.HashMap.Strict(HashMap)
 import qualified Data.DynamicArray as DynamicArray
 import Data.DynamicArray(Array)
 import Data.Typeable
 import GHC.Exts
 import GHC.Int
 import Unsafe.Coerce
+import Data.Hashable
+import Data.Binary.Sharing
 
 -- | Type class constraints for a value to be internable.
-type Intern a = (Typeable a, Ord a)
+type Intern a = (Typeable a, Eq a, Hashable a)
 
 -- | An interned value of type @a@.
 newtype Sym a = MkSym Int32
-  deriving (Eq, Ord)
+  deriving (Eq, Ord, Hashable)
 
 instance Show a => Show (Sym a) where
-  show = show . unintern
+  showsPrec n = showsPrec n . unintern
 
 -- | The unique ID of a symbol.
 symId :: Sym a -> Int
@@ -38,19 +40,17 @@
 -- The global cache of interned values.
 {-# NOINLINE cachesRef #-}
 cachesRef :: IORef Caches
-cachesRef = unsafePerformIO (newIORef (Caches 0 Map.empty DynamicArray.newArray))
+cachesRef = unsafePerformIO (newIORef (Caches 0 HashMap.empty DynamicArray.newArray))
 
 data Caches =
   Caches {
     -- The next id number to assign.
     caches_nextId :: {-# UNPACK #-} !Int32,
     -- A map from values to IDs.
-    caches_from   :: !(Map TypeRep (Cache Any)),
+    caches_from   :: !(HashMap TypeRep (HashMap Any Int32)),
     -- The reverse map from IDs to values.
     caches_to     :: !(Array Any) }
 
-type Cache a = Map a Int32
-
 atomicModifyCaches :: (Caches -> (Caches, a)) -> IO a
 atomicModifyCaches f = do
   -- N.B. atomicModifyIORef' ref f evaluates f ref *after* doing the
@@ -70,10 +70,10 @@
   if ok then return x else atomicModifyCaches f
 
 -- Versions of unsafeCoerce with slightly more type checking
-toAnyCache :: Cache a -> Cache Any
+toAnyCache :: HashMap a Int32 -> HashMap Any Int32
 toAnyCache = unsafeCoerce
 
-fromAnyCache :: Cache Any -> Cache a
+fromAnyCache :: HashMap Any Int32 -> HashMap a Int32
 fromAnyCache = unsafeCoerce
 
 toAny :: a -> Any
@@ -86,6 +86,7 @@
 {-# NOINLINE intern #-}
 intern :: forall a. Intern a => a -> Sym a
 intern x =
+  hash x `seq`
   unsafeDupablePerformIO $ do
     -- Common case: symbol is already interned.
     caches <- readIORef cachesRef
@@ -105,21 +106,21 @@
 
     tryFind :: Caches -> Maybe (Sym a)
     tryFind Caches{..} =
-      MkSym <$> (Map.lookup ty caches_from >>= Map.lookup x . fromAnyCache)
+      MkSym <$> (HashMap.lookup ty caches_from >>= HashMap.lookup x . fromAnyCache)
 
     insert :: Caches -> (Caches, Sym a)
     insert caches@Caches{..} =
       if n < 0 then error "label overflow" else
       (caches {
          caches_nextId = n+1,
-         caches_from = Map.insert ty (toAnyCache (Map.insert x n cache)) caches_from,
+         caches_from = HashMap.insert ty (toAnyCache (HashMap.insert x n cache)) caches_from,
          caches_to = DynamicArray.updateWithDefault undefined (fromIntegral n) (toAny x) caches_to },
        MkSym n)
       where
         n = caches_nextId
         cache =
           fromAnyCache $
-          Map.findWithDefault Map.empty ty caches_from
+          HashMap.findWithDefault HashMap.empty ty caches_from
 
 -- | Recover the underlying value from a 'Sym'.
 unintern :: Sym a -> a
@@ -145,3 +146,8 @@
 pattern Sym :: Intern a => a -> Sym a
 pattern Sym x <- (unintern -> x) where
   Sym x = intern x
+
+-- Serialise a Sym as the underlying value, because it needs to be interned on deserialisation.
+instance (Intern a, Binary a) => Binary (Sym a) where
+  put = put . Shared . unintern
+  get = intern . getShared <$> get
diff --git a/Data/Numbered.hs b/Data/Numbered.hs
--- a/Data/Numbered.hs
+++ b/Data/Numbered.hs
@@ -13,6 +13,8 @@
 import Data.Primitive.SmallArray
 import Data.Int
 import Data.Maybe
+import qualified Data.Binary.Sharing as Binary
+import Data.Binary.Sharing(Binary)
 
 -- | An array of key-value pairs.
 data Numbered a =
@@ -21,6 +23,10 @@
     {-# UNPACK #-} !(SmallArray a)
 
 instance Show a => Show (Numbered a) where show = show . toList
+
+instance Binary a => Binary (Numbered a) where
+  put = Binary.put . toList
+  get = fromList <$> Binary.get
 
 -- | An empty array.
 empty :: Numbered a
diff --git a/Data/PackedSequence.hs b/Data/PackedSequence.hs
--- a/Data/PackedSequence.hs
+++ b/Data/PackedSequence.hs
@@ -1,17 +1,22 @@
 -- | Sequences which are stored compactly in memory
 -- by serialising their contents as a @ByteString@.
+{-# LANGUAGE DeriveAnyClass #-}
 module Data.PackedSequence(PackedSequence, empty, null, size, fromList, toList, uncons) where
 
 import Prelude hiding (null)
-import Data.Serialize
+import Data.Binary
+import Data.Binary.Get
+import Data.Binary.Put
+import qualified Data.Binary.Sharing as Sharing
 import Data.ByteString(ByteString)
 import qualified Data.ByteString as BS
 import Data.List(unfoldr)
+import GHC.Generics
 
 -- | A sequence, stored in a serialised form
 data PackedSequence a =
   Seq {-# UNPACK #-} !Int {-# UNPACK #-} !ByteString
-  deriving Eq
+  deriving (Eq, Generic, Sharing.Binary)
 
 -- | An empty sequence.
 empty :: PackedSequence a
@@ -27,19 +32,19 @@
 
 -- | Convert a list into a sequence.
 {-# INLINEABLE fromList #-}
-fromList :: Serialize a => [a] -> PackedSequence a
-fromList xs = Seq (length xs) (runPut (mapM_ put xs))
+fromList :: Binary a => [a] -> PackedSequence a
+fromList xs = Seq (length xs) (BS.toStrict (runPut (mapM_ put xs)))
 
 -- | Convert a sequence into a list.
 {-# INLINEABLE toList #-}
-toList :: Serialize a => PackedSequence a -> [a]
+toList :: Binary 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 :: Binary 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)
+  Just $ case runGetOrFail get (BS.fromStrict bs) of
+    Left (_, _, err) -> error err
+    Right (bs, _, x) -> (x, Seq (n-1) (BS.toStrict bs))
diff --git a/Data/Primitive/ByteArray/Checked.hs b/Data/Primitive/ByteArray/Checked.hs
--- a/Data/Primitive/ByteArray/Checked.hs
+++ b/Data/Primitive/ByteArray/Checked.hs
@@ -1,7 +1,6 @@
 -- | A bounds-checked version of 'Data.Primitive.ByteArray'.
 -- See that module for documentation.
 
-{-# LANGUAGE ScopedTypeVariables #-}
 module Data.Primitive.ByteArray.Checked(
   module Data.Primitive.ByteArray,
   module Data.Primitive.ByteArray.Checked) where
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, FlexibleInstances, RankNTypes, TupleSections #-}
+{-# LANGUAGE MultiParamTypeClasses, GADTs, OverloadedStrings, GeneralizedNewtypeDeriving, FlexibleInstances, RankNTypes, TupleSections, DeriveAnyClass, CPP #-}
 module Twee where
 
 import Twee.Base
@@ -41,9 +41,11 @@
 import qualified Data.PackedSequence as PackedSequence
 import Test.QuickCheck.Gen hiding (sample)
 import Test.QuickCheck.Random
-import Debug.Trace
+--import Debug.Trace
 import Twee.Generate
 import qualified System.Random as Random
+import GHC.Generics
+import Data.Binary.Sharing
 
 ----------------------------------------------------------------------
 -- * Configuration and prover state.
@@ -64,7 +66,8 @@
     cfg_set_join_goals            :: Bool,
     cfg_always_simplify           :: Bool,
     cfg_complete_subsets          :: Bool,
-    cfg_score_cp                  :: Depth -> Index f (Hint f) -> Equation f -> Float,
+    cfg_hint_func                 :: Int -> Float -> Sym f,
+    cfg_cp_config                 :: !CP.Config,
     cfg_join                      :: Join.Config,
     cfg_proof_presentation        :: Proof.Config f,
     cfg_eliminate_axioms          :: [Axiom f],
@@ -86,7 +89,7 @@
     st_joinable       :: !(Index f (Equation f)),
     st_goals          :: ![Goal f],
     st_queue          :: !(Queue Batch),
-    st_hints          :: !(Index f (Hint f)),
+    st_hints          :: {-# UNPACK #-} !(Hints f),
     st_next_active    :: {-# UNPACK #-} !Id,
     st_considered     :: {-# UNPACK #-} !Int64,
     st_simplified_at  :: {-# UNPACK #-} !Id,
@@ -94,8 +97,9 @@
     st_not_complete   :: !IntSet,
     st_complete       :: !(Index f (Rule f)),
     st_messages_rev   :: ![Message f],
-    st_random_seed    :: Maybe QCGen,
+    st_random_seed    :: Maybe (ReadShowBinary QCGen),
     st_problem_term   :: Maybe (ConfluenceFailure f) }
+  deriving (Generic, Binary)
 
 -- | The default prover configuration.
 defaultConfig :: Function f => Config f
@@ -113,7 +117,8 @@
     cfg_set_join_goals = True,
     cfg_always_simplify = False,
     cfg_complete_subsets = False,
-    cfg_score_cp = \d hints eqn -> score CP.defaultConfig d hints eqn,
+    cfg_hint_func = \_ _ -> error "cfg_hint_func not configured",
+    cfg_cp_config = CP.defaultConfig,
     cfg_join = Join.defaultConfig,
     cfg_proof_presentation = Proof.defaultConfig,
     cfg_eliminate_axioms = [],
@@ -126,6 +131,21 @@
     cfg_hint_skel_factor = 0,
     cfg_print_score = False }
 
+-- | Compute cfg_score_cp from the CP configuration.
+{-# INLINE scoreCP #-}
+scoreCP :: Function f => Config f -> Depth -> Hints f -> Equation f -> Float
+scoreCP config@Config{..} d hints eqn =
+  let s1 = score cfg_cp_config d (scoreTerm config hints) eqn
+      -- s2 = score cfg_cp_config d (scoreTerm config (Hints [] Index.empty 0)) eqn
+  {-
+  in if s1 /= s2 then trace ("used hint for " ++ prettyShow eqn) (trace (prettyShow eqn ++ " => " ++ prettyShow (bothSides (applyHints hints) eqn)) s1) else s1
+  -}
+  in s1
+
+{-# INLINE scoreTerm #-}
+scoreTerm :: Function f => Config f -> Hints f -> Term f -> Float
+scoreTerm Config{..} hints t = termScore cfg_cp_config (applyHints hints t)
+
 -- | Does this configuration run the prover in a complete mode?
 configIsComplete :: Config f -> Bool
 configIsComplete Config{..} =
@@ -145,7 +165,11 @@
     st_joinable = Index.empty,
     st_goals = [],
     st_queue = Queue.empty,
-    st_hints = Index.empty,
+    st_hints =
+      Hints {
+        hints_list = [],
+        hints_index = Index.empty,
+        hints_next = 0 },
     st_next_active = 1,
     st_considered = 0,
     st_simplified_at = 1,
@@ -156,7 +180,7 @@
     st_random_seed =
       case cfg_random_mode of
         False -> Nothing
-        True -> Just (mkQCGen 12345),
+        True -> Just (ReadShowBinary (mkQCGen 12345)),
     st_problem_term = Nothing }
 
 ----------------------------------------------------------------------
@@ -169,6 +193,8 @@
     NewActive !(Maybe Float) !(Active f)
     -- | A new joinable equation.
   | NewEquation !(Equation f)
+    -- | A new hint was added.
+  | NewHint !(Rule f) !HintKind
     -- | A rule was deleted.
   | DeleteActive !(Active f)
     -- | The CP queue was simplified.
@@ -181,6 +207,7 @@
   | Status !Int
     -- | New problem term discovered.
   | NewProblemTerm !(ConfluenceFailure f)
+  deriving (Generic, Binary)
 
 instance Function f => Pretty (Message f) where
   pPrint (NewActive mscore rule) =
@@ -190,6 +217,8 @@
  --   $$ case cp_top (active_cp rule) of { Just t -> text "  (normal forms of term" <+> pPrint t <#> text ")"; Nothing -> pPrintEmpty }
   pPrint (NewEquation eqn) =
     text "  (hard)" <+> pPrint eqn
+  pPrint (NewHint rule kind) =
+    text "  (" <#> pPrint kind <+> text "hint)" <+> pPrint rule
   pPrint (DeleteActive rule) =
     text "  (delete rule " <#> pPrint (active_id rule) <#> text ")"
   pPrint SimplifyQueue =
@@ -255,7 +284,7 @@
     passive_rule1 :: {-# UNPACK #-} !Id,
     passive_rule2 :: {-# UNPACK #-} !Id,
     passive_how   :: !How }
-  deriving Eq
+  deriving (Eq, Generic, Binary)
 
 instance Ord Passive where
   compare = comparing f
@@ -272,8 +301,9 @@
     batch_rule      :: {-# UNPACK #-} !Id,
     batch_best      :: {-# UNPACK #-} !Passive,
     batch_rest      :: {-# UNPACK #-} !(PackedSequence (Float, Id, How)) }
+  deriving (Eq, Generic, Binary)
 
-data BatchKind = Rule1 | Rule2 deriving Eq
+data BatchKind = Rule1 | Rule2 deriving (Eq, Generic, Binary)
 
 instance Queue.Batch Batch where
   type Label Batch = Id
@@ -311,14 +341,14 @@
 
 {-# INLINEABLE makePassive #-}
 makePassive :: Function f => Config f -> State f -> Overlap (Active f) f -> Passive
-makePassive Config{..} State{..} Overlap{..} =
+makePassive config@Config{..} State{..} Overlap{..} =
   Passive {
-    passive_score = cfg_score_cp depth st_hints overlap_eqn,
+    passive_score = scoreCP config depth st_hints overlap_eqn,
     passive_rule1 = active_id overlap_rule1,
     passive_rule2 = active_id overlap_rule2,
     passive_how   = overlap_how }
   where
-    depth = succ (the overlap_rule1 `max` the overlap_rule2)
+    depth = Depth (succ (getDepth (the overlap_rule1) `max` getDepth (the overlap_rule2)))
 
 -- | Turn a Passive back into an overlap.
 -- Doesn't try to simplify it.
@@ -333,16 +363,18 @@
 -- | Renormalise a queued Passive.
 {-# INLINEABLE simplifyPassive #-}
 simplifyPassive :: Function f => Config f -> State f -> Passive -> Maybe (Passive)
-simplifyPassive Config{..} state@State{..} passive = do
+simplifyPassive config@Config{..} state@State{..} passive = do
   overlap <- findPassive state passive
   overlap <- simplifyOverlap (index_oriented st_rules) overlap
   let r1 = overlap_rule1 overlap
       r2 = overlap_rule2 overlap
   return passive {
     passive_score =
+#ifndef USE_LPO
       passive_score passive `min`
+#endif
       -- XXX factor out depth calculation
-      cfg_score_cp (succ (the r1 `max` the r2)) st_hints (overlap_eqn overlap) }
+      scoreCP config (Depth (succ (getDepth (the r1) `max` getDepth (the r2)))) st_hints (overlap_eqn overlap) }
 
 -- | Check if we should renormalise the queue.
 {-# INLINEABLE shouldSimplifyQueue #-}
@@ -371,9 +403,10 @@
 --
 --   * removing any orphans from the head of the queue
 --   * ignoring CPs that are too big
+--   * putting back any CPs whose score got bigger since they were enqueued
 {-# INLINEABLE dequeue #-}
 dequeue :: Function f => Config f -> State f -> (Maybe (Info, CriticalPair f, Active f, Active f), State f)
-dequeue Config{..} state@State{..} =
+dequeue config@Config{..} state@State{..} =
   case deq 0 st_queue of
     -- Explicitly make the queue empty, in case it e.g. contained a
     -- lot of orphans
@@ -389,14 +422,19 @@
         Just (overlap@Overlap{overlap_eqn = t :=: u, overlap_rule1 = rule1, overlap_rule2 = rule2})
           | fromMaybe True (cfg_accept_term <*> pure t),
             fromMaybe True (cfg_accept_term <*> pure u),
-            cp <- makeCriticalPair overlap ->
-              return ((combineInfo (active_info rule1) (active_info rule2), cp, rule1, rule2), n+1, queue)
+            cp <- makeCriticalPair overlap,
+            Just newPassive <- simplifyPassive config state passive ->
+              if passive_score newPassive <= passive_score passive then
+                return ((combineInfo (active_info rule1) (active_info rule2), cp, rule1, rule2), n+1, queue)
+              else
+                deq (n+1) (Queue.insert (passive_rule1 newPassive) [newPassive] queue)
+
         _ -> deq (n+1) queue
 
     combineInfo i1 i2 =
       Info {
         -- XXX factor out depth calculation
-        info_depth = succ (max (info_depth i1) (info_depth i2)),
+        info_depth = Depth (succ (max (getDepth (info_depth i1)) (getDepth (info_depth i2)))),
         info_max = IntSet.union (info_max i1) (info_max i2) }
 
 ----------------------------------------------------------------------
@@ -413,6 +451,7 @@
     -- A model in which the rule is false (used when reorienting)
     active_model :: !(Model f),
     active_positions :: !(Positions2 f) }
+  deriving (Generic, Binary)
 
 active_cp :: Active f -> CriticalPair f
 active_cp Active{..} =
@@ -421,9 +460,9 @@
     cp_top = active_top,
     cp_proof = derivation active_proof }
 
-activeScore :: Config f -> State f -> Active f -> Float
-activeScore Config{..} State{..} Active{..} =
-  cfg_score_cp (info_depth active_info) st_hints (equation active_proof)
+activeScore :: Function f => Config f -> State f -> Active f -> Float
+activeScore config@Config{..} State{..} Active{..} =
+  scoreCP config (info_depth active_info) st_hints (equation active_proof)
 
 activeRules :: Active f -> [Rule f]
 activeRules Active{..} =
@@ -435,6 +474,7 @@
   Info {
     info_depth :: {-# UNPACK #-} !Depth,
     info_max   :: !IntSet }
+  deriving (Generic, Binary)
 
 instance Eq (Active f) where
   (==) = (==) `on` active_id
@@ -459,7 +499,7 @@
       | otherwise = Nothing
     state' =
       message (NewActive mscore active) $
-      addActiveOnly state{st_next_active = st_next_active+1} active
+      addActiveOnly config state{st_next_active = st_next_active+1} active
   in if subsumed (st_joinable, st_complete) st_rules (unorient active_rule) then
     state
   else
@@ -509,8 +549,9 @@
 
 -- Add an active without generating critical pairs. Used in interreduction.
 {-# INLINEABLE addActiveOnly #-}
-addActiveOnly :: Function f => State f -> Active f -> State f
-addActiveOnly state@State{..} active@Active{..} =
+addActiveOnly :: Function f => Config f -> State f -> Active f -> State f
+addActiveOnly config state@State{..} active@Active{..} =
+  addHintsRulePairs config active $
   state {
     st_rules = foldl' insertRule st_rules (activeRules active),
     st_active_set = IntMap.insert (fromIntegral active_id) active st_active_set }
@@ -520,8 +561,9 @@
 
 -- Add an active without generating critical pairs. Used in interreduction.
 {-# INLINEABLE addActiveSimp #-}
-addActiveSimp :: Function f => State f -> Active f -> State f
-addActiveSimp state@State{..} active@Active{..} =
+addActiveSimp :: Function f => Config f -> State f -> Active f -> State f
+addActiveSimp config state@State{..} active@Active{..} =
+  addHintsRulePairs config active $
   state {
     st_rules = foldl' insertRule st_rules (activeRules active) }
   where
@@ -603,22 +645,12 @@
 addAxiom :: Function f => Config f -> State f -> Axiom f -> State f
 addAxiom config state axiom =
   consider config state{st_axioms = axiom:st_axioms state}
-    Info { info_depth = 0, info_max = IntSet.fromList [axiom_number axiom | cfg_complete_subsets config] }
+    Info { info_depth = Depth 0, info_max = IntSet.fromList [axiom_number axiom | cfg_complete_subsets config] }
     CriticalPair {
       cp_eqn = axiom_eqn axiom,
       cp_top = Nothing,
       cp_proof = Proof.axiom axiom }
 
--- Add a new hint.
-{-# INLINEABLE addHint #-}
-addHint :: Function f => Config f -> State f -> Term f -> State f
-addHint Config{..} state@State{..} hint =
-  state { st_hints = Index.insert hint (Hint hint cost) st_hints }
-  where
-    cost = fromIntegral (len hint - length (vars hint)) * cfg_hint_skel_factor + cfg_hint_skel_cost +
-      -- Add a cost for duplicated variables (since they only get counted once otherwise)
-      fromIntegral (length (vars hint) - length (usort (vars hint)))
-
 -- Record an equation as being joinable.
 {-# INLINEABLE addJoinable #-}
 addJoinable :: Function f => State f -> Equation f -> State f
@@ -675,7 +707,7 @@
     goal_expanded_rhs :: Map (Term f) (Derivation f),
     goal_lhs          :: Map (Term f) (Term f, Reduction f),
     goal_rhs          :: Map (Term f) (Term f, Reduction f) }
-  deriving Show
+  deriving (Show, Generic, Binary)
 
 -- Add a new goal.
 {-# INLINEABLE addGoal #-}
@@ -766,6 +798,113 @@
     goal_rhs = Map.singleton u (u, []) }
 
 ----------------------------------------------------------------------
+-- Hints.
+----------------------------------------------------------------------
+
+data Hints f =
+  Hints {
+    -- contains only user-provided hints
+    hints_list  :: ![Rule f],
+    -- also contains hints formed through CPs
+    hints_index :: !(Index f (Rule f)),
+    hints_next   :: !Int }
+  deriving (Generic, Binary)
+
+data HintKind = UserHint | DerivedHint deriving (Eq, Show, Generic, Binary)
+
+instance Pretty HintKind where
+  pPrint UserHint = text "show"
+  pPrint DerivedHint = text "auto"
+
+-- Add a new hint.
+{-# INLINEABLE addHint #-}
+addHint :: Function f => Config f -> State f -> Term f -> State f
+addHint config@Config{..} state@State{..} hint =
+  addHint' config state hint UserHint cost
+  where
+    cost = fromIntegral (len hint - length (vars hint)) * cfg_hint_skel_factor + cfg_hint_skel_cost
+
+-- Add a new hint, with a specified kind and cost.
+{-# INLINEABLE addHint' #-}
+addHint' :: Function f => Config f -> State f -> Term f -> HintKind -> Float -> State f
+addHint' config@Config{..} state@State{st_hints = Hints{..}, ..} hint kind cost =
+  (if kind == UserHint then addHintRulesPairs config rule . addHintHintsPairs config rule else id) $
+  {-
+  trace ("hint: " ++ prettyShow hint) $
+  trace ("kind: " ++ show kind) $
+  trace ("cost: " ++ show cost) $
+  trace ("hint term: " ++ prettyShow hintTerm) $
+  trace "" $
+  -}
+  message (NewHint rule kind) $
+  state {
+    st_hints = Hints {
+      hints_list = if kind == UserHint then rule:hints_list else hints_list,
+      hints_index = Index.insert hint rule hints_index,
+      hints_next = hints_next + 1 } }
+  where
+    args = usort (vars hint)
+
+    hintTerm = build (app (cfg_hint_func hints_next cost) (map var args))
+
+    -- A rule expressing applying the hint. Uses a dummy value for the proof
+    -- field since this rule should never be used in a proof anyway. 
+    rule = Rule Oriented (certify (Proof.Refl hintTerm)) hint hintTerm
+
+-- Add various kiknds of derived hints.
+{-# INLINEABLE addHintsRulePairs #-}
+addHintsRulePairs :: Function f => Config f -> Active f -> State f -> State f
+addHintsRulePairs config active state =
+  foldl' (\state rule -> addHintRulePairs config rule active state) state (hints_list (st_hints state))
+
+{-# INLINEABLE addHintRulesPairs #-}
+addHintRulesPairs :: Function f => Config f -> Rule f -> State f -> State f
+addHintRulesPairs config rule state =
+  foldl' (\state active -> addHintRulePairs config rule active state) state (IntMap.elems (st_active_set state))
+
+{-# INLINEABLE addHintRulePairs #-}
+addHintRulePairs :: Function f => Config f -> Rule f -> Active f -> State f -> State f
+addHintRulePairs config rule active state =
+  foldl' considerOverlap state (overlaps (Index.empty :: Index f (Rule f)) [makeActive rule] active)
+    where
+      -- hack: need to turn the turn into an Active to invoke 'overlaps'
+      makeActive rule = Active 0 (Info (Depth 0) IntSet.empty) rule Nothing (rule_proof rule) (modelFromOrder []) (positionsRule rule)
+      considerOverlap state Overlap{..} = considerNorm (simplifyTerm state) t u state
+        where
+          t = eqn_lhs overlap_eqn
+          u = eqn_rhs overlap_eqn
+
+      -- t: term we are considering adding a hint for
+      -- u: version of the term where perhaps a hint has already been added
+      considerNorm norm t u state
+        | st > su =
+        {-
+          trace ("rule: " ++ prettyShow rule) $
+          trace ("active: " ++ prettyShow (active_id active)) $
+          trace ("term: " ++ prettyShow t) $
+          trace ("norm first: " ++ prettyShow t' ++ " (cost " ++ show st ++ ")") $
+          trace ("hint first: " ++ prettyShow u' ++ " (cost " ++ show su ++ ")") $
+        -}
+          addHint' config state t' DerivedHint su
+        | otherwise = state
+        where
+          t' = norm t
+          u' = norm u
+          st = scoreTerm config (st_hints state) t'
+          su = scoreTerm config (st_hints state) u'
+
+{-# INLINEABLE addHintHintsPairs #-}
+addHintHintsPairs :: Function f => Config f -> Rule f -> State f -> State f
+addHintHintsPairs _ _ state = state
+
+-- Apply hints to a term.
+applyHints :: Function f => Hints f -> Term f -> Term f
+applyHints Hints{..} t =
+  {-let u = simplify idx t in
+  if t == u then u else traceShow ("hint: " ++ prettyShow t ++ " => " ++ prettyShow u) u-}
+  simplify hints_index t
+
+----------------------------------------------------------------------
 -- Interreduction.
 ----------------------------------------------------------------------
 
@@ -795,18 +934,18 @@
       (Just active_model) (active_cp active)
   of
     Right (_, cps) ->
-      flip addActiveSimp active $
+      flip (addActiveSimp config) active $
       flip (foldl' (\state cp -> consider config state active_info cp)) cps $
       message (DeleteActive active) $
       deleteActive state active
     Left (cp, model)
       | cp_eqn cp `simplerThan` cp_eqn (active_cp active) ->
-        flip addActiveSimp active $
+        flip (addActiveSimp config) active $
         flip (foldl' (\state cp -> consider config state active_info cp)) (split cp) $
         message (DeleteActive active) $
         deleteActive state active
       | model /= active_model ->
-        flip addActiveOnly active { active_model = model } $
+        flip (addActiveOnly config) active { active_model = model } $
         deleteActive state active
       | otherwise ->
         state
@@ -886,9 +1025,9 @@
           (Nothing, state) -> (False, state)
           (Just (info, overlap, _, _), state) ->
             (True, consider config state info overlap)
-      Just g -> -- random mode
+      Just (ReadShowBinary g) -> -- random mode
         let (g1, g2) = Random.split g in
-        let state' = state { st_random_seed = Just g2 } in
+        let state' = state { st_random_seed = Just (ReadShowBinary g2) } in
         case findCriticalPair config state' g1 of
           Nothing -> (True, state'{st_problem_term = Nothing})
           Just (info, overlap, changed, cf) ->
@@ -949,7 +1088,7 @@
         Nothing ->
           trace ("Overlap " ++ prettyShow (overlap_eqn o) ++ " was spurious") Nothing -- should be rare
         Just o' ->
-          Just (cfg_score_cp config 0 (st_hints state) (overlap_eqn o'), (Info 0 IntSet.empty, makeCriticalPair o, changed, cf))
+          Just (scoreCP config (Depth 0) (st_hints state) (overlap_eqn o'), (Info (Depth 0) IntSet.empty, makeCriticalPair o, changed, cf))
 
 -- Return all goal terms. Handles the $equals coding.
 goalTerms :: Function f => State f -> [Term f]
diff --git a/Twee/Base.hs b/Twee/Base.hs
--- a/Twee/Base.hs
+++ b/Twee/Base.hs
@@ -1,7 +1,7 @@
 -- | Useful operations on terms and similar. Also re-exports some generally
 -- useful modules such as 'Twee.Term' and 'Twee.Pretty'.
 
-{-# LANGUAGE TypeFamilies, FlexibleInstances, UndecidableInstances, DeriveFunctor, DefaultSignatures, FlexibleContexts, TypeOperators, MultiParamTypeClasses, GeneralizedNewtypeDeriving, ConstraintKinds, RecordWildCards, BangPatterns, PatternSynonyms #-}
+{-# LANGUAGE FlexibleInstances, UndecidableInstances, DeriveFunctor, DefaultSignatures, TypeOperators, MultiParamTypeClasses, GeneralizedNewtypeDeriving, ConstraintKinds, PatternSynonyms, RankNTypes #-}
 module Twee.Base(
   -- * Re-exported functionality
   module Twee.Term, module Twee.Pretty,
@@ -14,7 +14,7 @@
   -- * Typeclasses
   Minimal(..), minimalTerm, isMinimal, erase, eraseExcept, ground, skolemise,
   Ordered(..), lessThan, orientTerms,
-  EqualsBonus(..), isTrueTerm, isFalseTerm, decodeEquality,
+  EqualsBonus(..), Weighted(..), isTrueTerm, isFalseTerm, decodeEquality,
   Strictness(..), Function) where
 
 import Prelude hiding (lookup)
@@ -30,12 +30,13 @@
 import Data.List hiding (singleton)
 import Data.Maybe
 import qualified Data.IntMap.Strict as IntMap
-import Data.Serialize
+import Data.Binary.Sharing
+import qualified Data.Binary as Cereal
 import Data.Intern
 
 -- | Represents a unique identifier (e.g., for a rule).
 newtype Id = Id { unId :: Int32 }
-  deriving (Eq, Ord, Show, Enum, Bounded, Num, Real, Integral, Serialize)
+  deriving (Eq, Ord, Show, Enum, Bounded, Num, Real, Integral, Binary, Cereal.Binary)
 
 instance Pretty Id where
   pPrint = text . show . unId
@@ -244,10 +245,18 @@
 skolemise :: (Symbolic a, ConstantOf a ~ f, Minimal f) => a -> a
 skolemise t = subst (\(V x) -> con (skolem x)) t
 
--- | For types which have a notion of size.
 -- | The collection of constraints which the type of function symbols must
 -- satisfy in order to be used by twee.
-type Function f = (Ordered f, Minimal f, PrettyTerm f, EqualsBonus f, Intern f)
+type Function f = (Ordered f, Minimal f, PrettyTerm f, EqualsBonus f, Intern f, Weighted f)
+
+-- | For functions which have a notion of weight.
+-- Used for weighing terms in CP selection.
+class Weighted f where
+  weight :: f -> Float
+  weight _ = 1
+
+instance Weighted f => Weighted (Sym f) where
+  weight = weight . unintern
 
 -- | A hack for encoding Horn clauses. See 'Twee.CP.Score'.
 -- The default implementation of 'hasEqualsBonus' should work OK.
diff --git a/Twee/CP.hs b/Twee/CP.hs
--- a/Twee/CP.hs
+++ b/Twee/CP.hs
@@ -1,12 +1,12 @@
 -- | Critical pair generation.
-{-# LANGUAGE BangPatterns, FlexibleContexts, ScopedTypeVariables, MultiParamTypeClasses, RecordWildCards, OverloadedStrings, TypeFamilies, GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE MultiParamTypeClasses, OverloadedStrings, DeriveAnyClass #-}
+{-# OPTIONS_GHC -fno-warn-overlapping-patterns #-}
 module Twee.CP where
 
 import qualified Twee.Term as Term
 import Twee.Base
 import Twee.Rule
 import Twee.Index(Index)
-import qualified Twee.Index as Index
 import qualified Data.Set as Set
 import Control.Monad
 import Data.List hiding (singleton)
@@ -17,15 +17,24 @@
 import qualified Twee.Proof as Proof
 import Twee.Proof(Derivation, congPath)
 import Data.Bits
-import Data.Serialize
+import Data.Binary.Sharing
+import qualified Data.Binary as Cereal
 import Data.Int
 --import Debug.Trace
+import GHC.Generics
 
 -- | The set of positions at which a term can have critical overlaps.
 data Positions f = NilP | ConsP {-# UNPACK #-} !Int !(Positions f)
+instance Binary (Positions f) where
+  put = put . unfoldr op
+    where
+      op NilP = Nothing
+      op (ConsP x xs) = Just (x, xs)
+  get = foldr ConsP NilP <$> (get :: Get [Int])
+
 type PositionsOf a = Positions (ConstantOf a)
 -- | Like Positions but for an equation (one set of positions per term).
-data Positions2 f = ForwardsPos !(Positions f) | BothPos !(Positions f) !(Positions f)
+data Positions2 f = ForwardsPos !(Positions f) | BothPos !(Positions f) !(Positions f) deriving (Generic, Binary)
 
 instance Show (Positions f) where
   show = show . ChurchList.toList . positionsChurch
@@ -73,7 +82,7 @@
     overlap_top   :: {-# UNPACK #-} !(Term f),
     -- | The critical pair itself.
     overlap_eqn   :: {-# UNPACK #-} !(Equation f) }
-  deriving Show
+  deriving (Show, Generic, Binary)
 
 data How =
   How {
@@ -82,14 +91,14 @@
     how_dir2 :: !Direction }
   deriving (Eq, Ord, Show)
 
-data Direction = Forwards | Backwards deriving (Eq, Ord, Enum, Show)
+data Direction = Forwards | Backwards deriving (Eq, Ord, Enum, Show, Generic, Binary)
 
 direct :: Rule f -> Direction -> Rule f
 direct rule Forwards = rule
 direct rule Backwards = backwards rule
 
-instance Serialize How where
-  put = put . packHow
+instance Cereal.Binary How where
+  put = Cereal.put . packHow
     where
       packHow :: How -> Int32
       packHow How{..} =
@@ -98,7 +107,7 @@
         fromEnum how_dir2 `shiftL` 1 +
         how_pos `shiftL` 2
 
-  get = fmap unpackHow get
+  get = fmap unpackHow Cereal.get
     where
       unpackHow :: Int32 -> How
       unpackHow n0 =
@@ -108,8 +117,12 @@
           how_dir2 = toEnum ((n `shiftR` 1) .&. 1),
           how_pos  = n `shiftR` 2 }
 
+instance Binary How where
+  put = liftPut . Cereal.put
+  get = liftGet Cereal.get
+
 -- | Represents the depth of a critical pair.
-newtype Depth = Depth Int deriving (Eq, Ord, Num, Real, Enum, Integral, Show)
+newtype Depth = Depth { getDepth :: Int } deriving (Eq, Ord, Show, Generic, Binary)
 
 -- | Compute all overlaps of a rule with a set of rules.
 {-# INLINEABLE overlaps #-}
@@ -200,22 +213,10 @@
   Config {
     cfg_lhsweight :: !Float,
     cfg_rhsweight :: !Float,
-    cfg_funweight :: !Float,
     cfg_varweight :: !Float,
     cfg_depthweight :: !Float,
     cfg_dupcost :: !Float,
-    cfg_dupfactor :: !Float,
-    cfg_resonance :: !Bool }
-
-data Hint f =
-  Hint {
-    hint_term :: {-# UNPACK #-} !(Term f),
-    hint_cost :: {-# UNPACK #-} !Float }
-
-instance Symbolic (Hint f) where
-  type ConstantOf (Hint f) = f
-  termsDL Hint{..} = termsDL hint_term
-  subst_ sub (Hint t c) = Hint (subst_ sub t) c
+    cfg_dupfactor :: !Float }
 
 -- | The default heuristic configuration.
 defaultConfig :: Config
@@ -223,29 +224,33 @@
   Config {
     cfg_lhsweight = 4,
     cfg_rhsweight = 1,
-    cfg_funweight = 1,
     cfg_varweight = 6/7,
     cfg_depthweight = 2,
     cfg_dupcost = 1,
-    cfg_dupfactor = 0,
-    cfg_resonance = False }
+    cfg_dupfactor = 0 }
 
 -- | Compute a score for a critical pair.
 
 -- We compute:
 --   cfg_lhsweight * size l + cfg_rhsweight * size r
 -- where l is the biggest term and r is the smallest,
--- and variables have weight 1 and functions have weight cfg_funweight.
-{-# INLINEABLE score #-}
-score :: Function f => Config -> Depth -> Index f (Hint f) -> Equation f -> Float
-score Config{..} depth hints (l :=: r) =
-  fromIntegral depth * cfg_depthweight +
+-- and variables have weight cfg_varweight.
+{-# INLINE score #-}
+score :: Function f => Config -> Depth -> (Term f -> Float) -> Equation f -> Float
+score Config{..} depth termScore (l :=: r) =
+  fromIntegral (getDepth depth) * cfg_depthweight +
   (m + n) * cfg_rhsweight +
   max m n * (cfg_lhsweight - cfg_rhsweight)
   where
-    m = size' 0 (singleton l) []
-    n = size' 0 (singleton r) []
+    m = termScore l
+    n = termScore r
 
+-- | Compute a score for a single term.
+{-# INLINEABLE termScore #-}
+termScore :: Function f => Config -> Term f -> Float
+termScore Config{..} t =
+  size' 0 (singleton t) []
+  where
     size' !_ !_ !_ | False = undefined
     size' n Nil ts =
       case ts of
@@ -254,23 +259,18 @@
     size' n (Cons t ts) us
       | len t > 1, t `isSubtermOfList` ts || any (t `isSubtermOfList`) us =
         size' (n+cfg_dupcost+cfg_dupfactor*fromIntegral (len t)) ts us
-    size' n (Cons t ts) us
-      | len t > 1, (sub, Hint{..}):_ <- Index.matches t hints,
-        not cfg_resonance || allSubst (\_ t -> case t of { UnsafeCons (Var _) _ -> True; _ -> False }) sub =
-        size' (n + hint_cost) ts (map snd (Term.substToList' sub) ++ us)
-        --trace ("hint: len " ++ show (len t) ++ ", new cost " ++ show new_cost ++ ": " ++ prettyShow t) $
     size' n ts xs
       | Cons (App f ws@(Cons a (Cons b us))) vs <- ts,
         not (isVar a),
         not (isVar b),
         hasEqualsBonus f,
         Just sub <- unify a b =
-        size' (n+cfg_funweight) ws xs `min`
+        size' (n+weight f) ws xs `min`
         size' (n+1) (subst sub us) (subst sub (vs:xs))
     size' n (Cons (Var _) ts) us =
       size' (n+cfg_varweight) ts us
-    size' n ConsSym{hd = App{}, rest = ts} us =
-      size' (n+cfg_funweight) ts us
+    size' n ConsSym{hd = App f _, rest = ts} us =
+      size' (n+weight f) ts us
 
 ----------------------------------------------------------------------
 -- * Higher-level handling of critical pairs.
diff --git a/Twee/Constraints.hs b/Twee/Constraints.hs
--- a/Twee/Constraints.hs
+++ b/Twee/Constraints.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE FlexibleContexts, UndecidableInstances, RecordWildCards #-}
+{-# LANGUAGE DeriveAnyClass #-}
 -- | Solving constraints on variable ordering.
 module Twee.Constraints where
 
@@ -18,8 +18,10 @@
 import Test.QuickCheck.Gen(unGen)
 import Test.QuickCheck.Random(mkQCGen)
 import Data.Intern
+import GHC.Generics
+import Data.Binary.Sharing
 
-data Atom f = Constant (Sym f) | Variable Var deriving (Show, Eq, Ord)
+data Atom f = Constant (Sym f) | Variable Var deriving (Show, Eq, Ord, Generic, Binary)
 
 {-# INLINE atoms #-}
 atoms :: Term f -> [Atom f]
@@ -188,7 +190,7 @@
 addTerm _ b = b
 
 newtype Model f = Model (Map (Atom f) (Int, Int))
-  deriving (Eq, Show)
+  deriving (Eq, Ord, Show, Generic, Binary)
 -- Representation: map from atom to (major, minor)
 -- x <  y if major x < major y
 -- x <= y if major x = major y and minor x < minor y
@@ -215,8 +217,11 @@
         rel = if i == j then LessEq else Less
 
 modelFromOrder :: (Minimal f, Ord f) => [Atom f] -> Model f
-modelFromOrder xs =
-  Model (Map.fromList [(x, (i, i)) | (x, i) <- zip xs [0..]])
+modelFromOrder xs = modelFromOrder' [[x] | x <- xs]
+
+modelFromOrder' :: (Minimal f, Ord f) => [[Atom f]] -> Model f
+modelFromOrder' xss =
+  Model (Map.fromList [(x, (i, j)) | (xs, i) <- zip xss [0..], (x, j) <- zip xs [0..]])
 
 weakenModel :: Model f -> [Model f]
 weakenModel (Model m) =
diff --git a/Twee/Equation.hs b/Twee/Equation.hs
--- a/Twee/Equation.hs
+++ b/Twee/Equation.hs
@@ -1,9 +1,12 @@
 -- | Equations.
-{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE DeriveAnyClass #-}
 module Twee.Equation where
 
 import Twee.Base
 import Control.Monad
+import GHC.Generics
+import Data.Binary.Sharing
+import Data.Hashable
 
 --------------------------------------------------------------------------------
 -- * Equations.
@@ -13,7 +16,8 @@
   (:=:) {
     eqn_lhs :: {-# UNPACK #-} !(Term f),
     eqn_rhs :: {-# UNPACK #-} !(Term f) }
-  deriving (Eq, Ord, Show)
+  deriving (Eq, Ord, Show, Generic, Hashable, Binary)
+
 type EquationOf a = Equation (ConstantOf a)
 
 instance Symbolic (Equation f) where
diff --git a/Twee/Generate.hs b/Twee/Generate.hs
--- a/Twee/Generate.hs
+++ b/Twee/Generate.hs
@@ -7,7 +7,7 @@
 import Data.Maybe
 import Twee.Profile
 import Twee.Utils
-import Debug.Trace
+--import Debug.Trace
 
 type Pat f = Term f
 type LHS f = Term f
@@ -31,7 +31,7 @@
   [ (1, return sub) ] ++
   -- commit to top-level function...
   [ (n, genList (reduce n (length ps)) lhss ps sub)
-  | App f psl <- [p]
+  | App _f psl <- [p]
   , let ps = unpack psl
   ] ++
   -- ...or use a LHS for inspiration
diff --git a/Twee/Index.hs b/Twee/Index.hs
--- a/Twee/Index.hs
+++ b/Twee/Index.hs
@@ -5,7 +5,7 @@
 -- the search term is an instance of the key, and return the corresponding
 -- values.
 
-{-# LANGUAGE BangPatterns, RecordWildCards, OverloadedStrings, FlexibleContexts, CPP, TupleSections, TypeFamilies #-}
+{-# LANGUAGE OverloadedStrings, CPP, TupleSections, DeriveAnyClass #-}
 -- We get some bogus warnings because of pattern synonyms.
 {-# OPTIONS_GHC -fno-warn-overlapping-patterns #-}
 {-# OPTIONS_GHC -O2 -fmax-worker-args=100 #-}
@@ -40,6 +40,8 @@
 import qualified Data.IntMap.Strict as IntMap
 import Twee.Profile
 import Data.Intern
+import Data.Binary.Sharing
+import GHC.Generics
 
 -- The term index in this module is a _perfect discrimination tree_.
 -- This is a trie whose keys are terms, represented as flat lists of symbols
@@ -489,3 +491,26 @@
       Nothing ->
         searchVars t ts binds var (start+1) rest
 
+----------------------------------------------------------------------
+-- Serialisation.
+----------------------------------------------------------------------
+
+-- When serialising, we must change the 'fun' array to index by function and not function number.
+data  SIndex f a = SIndex Int (TermList f) [a] [(Sym f, Index f a)] (Numbered (Index f a)) | SEmpty
+  deriving (Generic, Binary)
+
+toSerialised :: Index f a -> SIndex f a
+toSerialised Empty = SEmpty
+toSerialised (Index minSize prefix here funs vars) = SIndex minSize prefix here funs' vars
+  where
+    funs' = [(unsafeMkSym f, idx) | (f, idx) <- Array.toList funs, not (null idx)]
+
+fromSerialised :: SIndex f a -> Index f a
+fromSerialised SEmpty = Empty
+fromSerialised (SIndex minSize prefix here funs vars) = Index minSize prefix here funs' vars
+  where
+    funs' = foldr (uncurry Array.update) newArray [(symId f, idx) | (f, idx) <- funs]
+
+instance (Intern f, Binary f, Binary a) => Binary (Index f a) where
+  put = put . toSerialised
+  get = fromSerialised <$> get
diff --git a/Twee/Join.hs b/Twee/Join.hs
--- a/Twee/Join.hs
+++ b/Twee/Join.hs
@@ -1,5 +1,4 @@
 -- | Tactics for joining critical pairs.
-{-# LANGUAGE FlexibleContexts, BangPatterns, RecordWildCards, TypeFamilies, ScopedTypeVariables #-}
 module Twee.Join where
 
 import Twee.Base
@@ -220,7 +219,7 @@
         _ -> normaliseWith (const True) (rewrite (ok t u m) (index_all idx)) t
     ok t u m rule sub =
       case cp_top of
-        Just top | cfg_use_connectedness_in_ground_joining ->
+        Just _top | cfg_use_connectedness_in_ground_joining ->
           reducesWith lessEqSkolemModel rule sub &&
           unorient rule `simplerThan` (t :=: u)
         _ ->
diff --git a/Twee/KBO.hs b/Twee/KBO.hs
--- a/Twee/KBO.hs
+++ b/Twee/KBO.hs
@@ -1,7 +1,6 @@
 -- | An implementation of Knuth-Bendix ordering.
 
-{-# LANGUAGE PatternGuards, BangPatterns #-}
-module Twee.KBO(lessEq, lessIn, lessEqSkolem, Sized(..), Weighted(..)) where
+module Twee.KBO(lessEq, lessIn, lessEqSkolem, Sized(..), ArgWeighted(..)) where
 
 import Twee.Base hiding (lessEq, lessIn, lessEqSkolem)
 import Twee.Equation
@@ -13,7 +12,7 @@
 import Twee.Utils
 import Data.Intern
 
-lessEqSkolem :: (Function f, Sized f, Weighted f) => Term f -> Term f -> Bool
+lessEqSkolem :: (Function f, Sized f, ArgWeighted f) => Term f -> Term f -> Bool
 lessEqSkolem !t !u
   | m < n = True
   | m > n = False
@@ -39,7 +38,7 @@
       in loop ts us
 
 -- | Check if one term is less than another in KBO.
-lessEq :: (Function f, Sized f, Weighted f) => Term f -> Term f -> Bool
+lessEq :: (Function f, Sized f, ArgWeighted f) => Term f -> Term f -> Bool
 lessEq (App f Nil) _ | f == minimal = True
 lessEq (Var x) (Var y) | x == y = True
 lessEq _ (Var _) = False
@@ -76,14 +75,14 @@
 
 -- See "notes/kbo under assumptions" for how this works.
 
-lessIn :: (Function f, Sized f, Weighted f) => Model f -> Term f -> Term f -> Maybe Strictness
+lessIn :: (Function f, Sized f, ArgWeighted f) => Model f -> Term f -> Term f -> Maybe Strictness
 lessIn model t u =
   case sizeLessIn model t u of
     Nothing -> Nothing
     Just Strict -> Just Strict
     Just Nonstrict -> lexLessIn model t u
 
-sizeLessIn :: (Function f, Sized f, Weighted f) => Model f -> Term f -> Term f -> Maybe Strictness
+sizeLessIn :: (Function f, Sized f, ArgWeighted f) => Model f -> Term f -> Term f -> Maybe Strictness
 sizeLessIn model t u =
   case minimumIn model m of
     Just l
@@ -123,7 +122,7 @@
       | k < 0 = Nothing
       | otherwise = Just k
 
-lexLessIn :: (Function f, Sized f, Weighted f) => Model f -> Term f -> Term f -> Maybe Strictness
+lexLessIn :: (Function f, Sized f, ArgWeighted f) => Model f -> Term f -> Term f -> Maybe Strictness
 lexLessIn _ t u | t == u = Just Nonstrict
 lexLessIn cond t u
   | Just a <- fromTerm t,
@@ -157,13 +156,13 @@
   -- | Compute the size.
   size  :: a -> Integer
 
-class Weighted f where
+class ArgWeighted f where
   argWeight :: f -> Integer
 
-instance (Weighted f, Intern f) => Weighted (Sym f) where
+instance (ArgWeighted f, Intern f) => ArgWeighted (Sym f) where
   argWeight = argWeight . unintern
 
-weightedVars :: (Weighted f, Intern f) => Term f -> [(Var, Integer)]
+weightedVars :: (ArgWeighted f, Intern f) => Term f -> [(Var, Integer)]
 weightedVars t = collate sum (loop 1 t)
   where
     loop k (Var x) = [(x, k)]
@@ -173,7 +172,7 @@
 instance (Intern f, Sized f) => Sized (Sym f) where
   size = size . unintern
 
-instance (Intern f, Sized f, Weighted f) => Sized (TermList f) where
+instance (Intern f, Sized f, ArgWeighted f) => Sized (TermList f) where
   size = aux 0
     where
       aux n Nil = n
@@ -181,9 +180,9 @@
         aux (n + size f + argWeight f * size t) u
       aux n (Cons (Var _) t) = aux (n+1) t
 
-instance (Intern f, Sized f, Weighted f) => Sized (Term f) where
+instance (Intern f, Sized f, ArgWeighted f) => Sized (Term f) where
   size = size . singleton
 
-instance (Intern f, Sized f, Weighted f) => Sized (Equation f) where
+instance (Intern f, Sized f, ArgWeighted f) => Sized (Equation f) where
   size (x :=: y) = size x + size y
 
diff --git a/Twee/LPO.hs b/Twee/LPO.hs
new file mode 100644
--- /dev/null
+++ b/Twee/LPO.hs
@@ -0,0 +1,107 @@
+-- | An implementation of lexicographic path ordering.
+
+module Twee.LPO(lessEqBasic, lessEq, lessIn, lessEqSkolem) where
+
+import Twee.Base hiding (lessEq, lessIn, lessEqSkolem)
+import Twee.Constraints hiding (lessEq, lessIn, lessEqSkolem)
+import Data.Maybe
+import Control.Monad
+
+lessEqSkolem :: Function f => Term f -> Term f -> Bool
+lessEqSkolem (App f Nil) _ | f == minimal = True
+lessEqSkolem _ (App f Nil) | f == minimal = False
+lessEqSkolem (Var x) (Var y) = x <= y
+lessEqSkolem _ (Var _) = False
+lessEqSkolem (Var _) _ = True
+lessEqSkolem t@(App f ts) u@(App g us)
+  | f == g = lexMA ts us
+  | f << g = majo ts u
+  | otherwise = alpha t us
+  where
+    lexMA Nil Nil = True
+    lexMA (Cons t' ts) (Cons u' us)
+      | t' == u' = lexMA ts us
+      | lessEqSkolem t' u' = majo ts u
+      | otherwise = alpha t us
+
+    majo ts u = and [t /= u && lessEqSkolem t u | t <- unpack ts]
+    alpha t us = or [lessEqSkolem t u | u <- unpack us]
+
+-- For testing
+lessEqBasic :: Function f => Term f -> Term f -> Bool
+lessEqBasic t u = eqModErasure t u || lessBasic t u
+  where
+    eqModErasure (App f _) _ | f == minimal = True
+    eqModErasure (Var x) (Var y) = x == y
+    eqModErasure (App f ts) (App g us) =
+      f == g && and (zipWith eqModErasure (unpack ts) (unpack us))
+    eqModErasure _ _ = False
+
+lessBasic :: Function f => Term f -> Term f -> Bool
+lessBasic (App f Nil) (App g _) | f == minimal && g /= minimal = True
+lessBasic (Var _) (Var _) = False
+lessBasic (Var x) (App _ ts) = x `elem` vars ts
+lessBasic t@(App f ts) u@(App g us)
+  | or [lessEqBasic t u' | u' <- unpack us] = True
+  | f << g && and [lessBasic t' u | t' <- unpack ts] = True
+  | f == g = and [lessBasic t' u | t' <- unpack ts] && loop ts us
+  where
+    loop Nil Nil = False
+    loop (Cons t ts) (Cons u us) =
+      if t == u then loop ts us else lessBasic t u
+lessBasic _ _ = False
+
+-- | Check if one term is less than another in LPO.
+lessEq :: Function f => Term f -> Term f -> Bool
+lessEq (App f Nil) _ | f == minimal = True
+lessEq (Var x) (Var y) = x == y
+lessEq _ (Var _) = False
+lessEq (Var x) t = x `elem` vars t
+lessEq t@(App f ts) u@(App g us)
+  | f == g = lexMA ts us
+  | f << g = majo ts u
+  | otherwise = alpha t us
+  where
+    lexMA Nil Nil = True
+    lexMA (Cons t' ts) (Cons u' us)
+      | t' == u' = lexMA ts us
+      | lessEq t' u' =
+        case unify t' u' of
+          Just sub -> majo ts u && lexMA (subst sub ts) (subst sub us)
+          Nothing -> majo ts u
+      | otherwise = alpha t us
+
+    majo ts u = and [isNothing (unify t u) && lessEq t u | t <- unpack ts]
+    alpha t us = or [lessEq t u | u <- unpack us]
+
+lessIn :: Function f => Model f -> Term f -> Term f -> Maybe Strictness
+lessIn model t u
+  | Just a <- fromTerm t,
+    Just b <- fromTerm u,
+    Just s <- lessEqInModel model a b = Just s
+lessIn _ _ (Var _) = Nothing
+lessIn model (Var x) t
+  | any isJust [lessEqInModel model (Variable x) a | a <- catMaybes (map fromTerm (subterms t))] = Just Strict
+  | otherwise = Nothing
+lessIn model t@(App f ts) u@(App g us)
+  | f == g = lexMA ts us
+  | f << g = majo ts u
+  | otherwise = alpha t us
+  where
+    lexMA Nil Nil = Just Nonstrict
+    lexMA (Cons t' ts) (Cons u' us) =
+      case lessIn model t' u' of
+        Just Nonstrict ->
+          case (let Just sub = unify t' u' in lexMA (subst sub ts) (subst sub us), majo ts u) of
+            (Just Strict, Just Strict) -> Just Strict
+            (Just _, Just _) -> Just Nonstrict
+            _ -> Nothing
+        Just Strict -> majo ts u
+        Nothing -> alpha t us
+
+    majo ts u = do
+      guard (and [lessIn model t u == Just Strict | t <- unpack ts])
+      return Strict
+    alpha t us = do
+      guard (or [isJust (lessIn model t u) | u <- unpack us])
+      return Strict
diff --git a/Twee/Profile.hs b/Twee/Profile.hs
--- a/Twee/Profile.hs
+++ b/Twee/Profile.hs
@@ -1,5 +1,5 @@
 -- Basic support for profiling.
-{-# LANGUAGE BangPatterns, RecordWildCards, CPP, OverloadedStrings #-}
+{-# LANGUAGE CPP, OverloadedStrings #-}
 module Twee.Profile(stamp, stampWith, stampM, stampGen, stampGen', profile) where
 
 #ifdef PROFILE
diff --git a/Twee/Proof.hs b/Twee/Proof.hs
--- a/Twee/Proof.hs
+++ b/Twee/Proof.hs
@@ -1,5 +1,5 @@
--- | Equational proofs which are checked for correctedness.
-{-# LANGUAGE TypeFamilies, PatternGuards, RecordWildCards, ScopedTypeVariables, OverloadedStrings #-}
+-- | Equational proofs which are checked for correctness.
+{-# LANGUAGE OverloadedStrings, DeriveAnyClass #-}
 module Twee.Proof(
   -- * Constructing proofs
   Proof, Derivation(..), Axiom(..),
@@ -33,6 +33,10 @@
 import Control.Monad.Trans.State.Strict
 import Data.Graph
 import Twee.Profile
+import qualified Data.Binary.Sharing as Binary
+import Data.Binary.Sharing(Binary, Shared(..))
+import GHC.Generics
+import Data.Hashable
 
 ----------------------------------------------------------------------
 -- Equational proofs. Only valid proofs can be constructed.
@@ -65,7 +69,7 @@
     -- Parallel, i.e., takes a function symbol and one derivation for each
     -- argument of that function.
   | Cong {-# UNPACK #-} !(Sym f) ![Derivation f]
-  deriving (Eq, Show)
+  deriving (Eq, Show, Generic, Hashable, Binary)
 
 --  | An axiom, which comes without proof.
 data Axiom f =
@@ -76,9 +80,12 @@
     -- | A description of the axiom.
     -- Has no semantic meaning; for convenience only.
     axiom_name :: !String,
+    -- | Human-readable names for the variables of the axiom.
+    -- Has no semantic meaning; for convenience only.
+    axiom_vars :: !(Maybe (Map Var String)),
     -- | The equation which the axiom asserts.
     axiom_eqn :: !(Equation f) }
-  deriving (Eq, Ord, Show)
+  deriving (Eq, Ord, Show, Generic, Hashable)
 
 -- | Checks a 'Derivation' and, if it is correct, returns a
 -- certified 'Proof'.
@@ -87,11 +94,11 @@
 
 -- This is the trusted core of the module.
 {-# INLINEABLE certify #-}
-certify :: Function f => Derivation f -> Proof f
+certify :: Derivation f -> Proof f
 certify p =
   stamp "certify proof" $
   case check p of
-    Nothing -> error ("Invalid proof created!\n" ++ prettyShow p)
+    Nothing -> error "Invalid proof created!"
     Just eqn -> Proof eqn p
   where
     check (UseLemma proof sub) =
@@ -129,6 +136,8 @@
   -- Don't look at the proof itself, to prevent exponential blowup
   -- when a proof contains UseLemma
   compare = comparing equation
+instance Hashable (Proof f) where
+  hashWithSalt s = hashWithSalt s . equation
 
 instance Symbolic (Derivation f) where
   type ConstantOf (Derivation f) = f
@@ -167,6 +176,16 @@
     text "axiom" <#>
     pPrintTuple [pPrint axiom_number, text axiom_name, pPrint axiom_eqn]
 
+instance (Intern f, Binary f) => Binary (Axiom f) where
+  put Axiom{..} = Binary.put (Shared (axiom_number, axiom_name, axiom_vars, axiom_eqn))
+  get = do
+    Shared (num, name, vars, eqn) <- Binary.get
+    return (Axiom num name vars eqn)
+
+instance (Intern f, Binary f) => Binary (Proof f) where
+  put = Binary.put . Shared . derivation
+  get = certify . getShared <$> Binary.get
+
 foldLemmas :: (Intern f, PrettyTerm f) => (Map (Proof f) a -> Derivation f -> a) -> [Derivation f] -> Map (Proof f) a
 foldLemmas op ds =
   execState (mapM_ foldGoal ds) Map.empty
@@ -498,7 +517,7 @@
     pres_lemmas :: [Proof f],
     -- | The goals proved.
     pres_goals  :: [ProvedGoal f] }
-  deriving Show
+  deriving (Show, Generic, Binary)
 
 -- Note: only the pg_proof field should be trusted!
 -- The remaining fields are for information only.
@@ -515,9 +534,10 @@
     -- In general, subst pg_witness_hint pg_goal_hint == equation pg_proof.
     -- For non-existential goals, pg_goal_hint == equation pg_proof
     -- and pg_witness_hint is the empty substitution.
+    pg_vars         :: Maybe (Map Var String),
     pg_goal_hint    :: Equation f,
     pg_witness_hint :: Subst f }
-  deriving Show
+  deriving (Show, Generic, Binary)
 
 -- | Construct a @ProvedGoal@.
 provedGoal :: Int -> String -> Proof f -> ProvedGoal f
@@ -526,6 +546,7 @@
     pg_number = number,
     pg_name = name,
     pg_proof = proof,
+    pg_vars = Nothing,
     pg_goal_hint = equation proof,
     pg_witness_hint = emptySubst }
 
@@ -731,8 +752,11 @@
       Symm <$> generaliseStep p
     generaliseStep (Trans p q) =
       liftM2 Trans (generaliseStep p) (generaliseStep q)
-    generaliseStep (Cong f ps) =
-      Cong f <$> mapM generaliseStep ps
+    generaliseStep (Cong f ps) = do
+      q <- cong f <$> mapM generaliseStep ps
+      case q of
+        Refl{} -> generaliseStep q
+        _ -> return q
 
     freshen xs f = do
       n <- get
@@ -842,19 +866,19 @@
 pPrintPresentation :: forall f. Function f => Config f -> Presentation f -> Doc
 pPrintPresentation config (Presentation axioms lemmas goals) =
   vcat $ intersperse (text "") $
-    vcat [ describeEquation "Axiom" (axiomNum axiom) (Just name) eqn $$
+    vcat [ describeEquation "Axiom" (axiomNum axiom) (Just name) vars eqn $$
            ppAxiomUses axiom
-         | axiom@(Axiom _ name eqn) <- axioms,
+         | axiom@(Axiom _ name vars eqn) <- axioms,
            not (invisible eqn) ]:
-    [ pp "Lemma" (lemmaNum p) Nothing (equation p) emptySubst p
+    [ pp "Lemma" (lemmaNum p) Nothing (equation p) Nothing emptySubst p
     | p <- lemmas,
       not (invisible (equation p)) ] ++
-    [ pp "Goal" (show num) (Just pg_name) pg_goal_hint pg_witness_hint pg_proof
+    [ pp "Goal" (show num) (Just pg_name) pg_goal_hint pg_vars pg_witness_hint pg_proof
     | (num, ProvedGoal{..}) <- zip [1..] goals ]
   where
-    pp kind n mname eqn witness p =
-      describeEquation kind n mname eqn $$
-      ppWitness witness $$
+    pp kind n mname eqn names witness p =
+      describeEquation kind n mname names eqn $$
+      ppWitness names witness $$
       text "Proof:" $$
       pPrintLemma config axiomNum lemmaNum p
 
@@ -863,14 +887,18 @@
     axiomNum x = show (fromJust (Map.lookup x axiomNums))
     lemmaNum x = show (fromJust (Map.lookup x lemmaNums))
 
-    ppWitness sub
+    ppWitness names sub
       | sub == emptySubst = pPrintEmpty
       | otherwise =
           vcat [
             text "The goal is true when:",
             nest 2 $ vcat
-              [ pPrint x <+> text "=" <+> pPrint t
-              | (x, t) <- substToList sub ],
+              [ text name <+> text "=" <+> pPrint t
+              | (x, t) <- substToList sub,
+                let name =
+                      case names of
+                        Nothing -> prettyShow x
+                        Just names -> fromJust (Map.lookup x names) ],
             if minimal `elem` funs sub then
               text "where" <+> doubleQuotes (pPrint (minimal :: Sym f)) <+>
               text "stands for an arbitrary term of your choice."
@@ -900,14 +928,31 @@
 -- Used both here and in the main file.
 describeEquation ::
   Function f =>
-  String -> String -> Maybe String -> Equation f -> Doc
-describeEquation kind num mname eqn =
+  String -> String -> Maybe String -> Maybe (Map Var String) -> Equation f -> Doc
+describeEquation kind num mname mvars eqn =
   text kind <+> text num <#>
   (case mname of
      Nothing -> text ""
      Just name -> text (" (" ++ name ++ ")")) <#>
-  text ":" <+> pPrint eqn <#> text "."
+  text ":" <+> pPrint (prettyVars eqn) <#> text "."
+  where
+    var x =
+      case mvars of
+        Nothing -> prettyShow x
+        Just vars -> fromJust (Map.lookup x vars)
+    prettyVars (t :=: u) = build (pv t) :=: build (pv u)
+    pv (Var x) = con (Sym (PrettyVar (var x)))
+    pv (App (Sym f) ts) = app (Sym (PrettyFunc f)) (map pv (unpack ts))
 
+data PrettyVars f = PrettyVar String | PrettyFunc f
+  deriving (Eq, Generic, Hashable)
+instance Pretty f => Pretty (PrettyVars f) where
+  pPrint (PrettyVar x) = text x
+  pPrint (PrettyFunc f) = pPrint f
+instance PrettyTerm f => PrettyTerm (PrettyVars f) where
+  termStyle (PrettyVar _) = uncurried
+  termStyle (PrettyFunc f) = termStyle f
+
 ----------------------------------------------------------------------
 -- Making proofs of existential goals more readable.
 ----------------------------------------------------------------------
@@ -945,16 +990,17 @@
 decodeGoal config pg =
   case maybeDecodeGoal config pg of
     Nothing -> pg
-    Just (name, witness, goal, deriv) ->
+    Just (name, vars, witness, goal, deriv) ->
       checkProvedGoal $
       pg {
         pg_name = name,
         pg_proof = certify deriv,
+        pg_vars = vars,
         pg_goal_hint = goal,
         pg_witness_hint = witness }
 
 maybeDecodeGoal :: forall f. Function f =>
-  Config f -> ProvedGoal f -> Maybe (String, Subst f, Equation f, Derivation f)
+  Config f -> ProvedGoal f -> Maybe (String, Maybe (Map Var String), Subst f, Equation f, Derivation f)
 maybeDecodeGoal Config{..} ProvedGoal{..}
   | not cfg_eliminate_existentials_coding = Nothing
   --  N.B. presentWithGoals takes care of expanding any lemma which mentions
@@ -977,11 +1023,11 @@
     decodeReflexivity _ = Nothing
 
     -- Detect $equals(t, u) = $false.
-    decodeConjecture :: Derivation f -> Maybe (String, Equation f, Subst f)
+    decodeConjecture :: Derivation f -> Maybe (String, Maybe (Map Var String), Equation f, Subst f)
     decodeConjecture (UseAxiom Axiom{..} sub) = do
       guard (isFalseTerm (eqn_rhs axiom_eqn))
       (t, u) <- decodeEquality (eqn_lhs axiom_eqn)
-      return (axiom_name, t :=: u, sub)
+      return (axiom_name, axiom_vars, t :=: u, sub)
     decodeConjecture _ = Nothing
 
     extract (p:ps) = do
@@ -993,10 +1039,10 @@
     cont p1 p2 (p:ps)
       | Just t <- decodeReflexivity p =
         cont (Refl t) (Refl t) ps
-      | Just (name, eqn, sub) <- decodeConjecture p =
+      | Just (name, vars, eqn, sub) <- decodeConjecture p =
         -- If p1: s=t and p2: s=u
         -- then symm p1 `trans` p2: t=u.
-        return (name, sub, eqn, symm p1 `trans` p2)
+        return (name, vars, sub, eqn, symm p1 `trans` p2)
       | Cong eq [p1', p2'] <- p, isEquals eq =
         cont (p1 `trans` p1') (p2 `trans` p2') ps
     cont _ _ _ = Nothing
diff --git a/Twee/Rule.hs b/Twee/Rule.hs
--- a/Twee/Rule.hs
+++ b/Twee/Rule.hs
@@ -1,5 +1,5 @@
 -- | Term rewriting.
-{-# LANGUAGE TypeFamilies, FlexibleContexts, RecordWildCards, BangPatterns, OverloadedStrings, MultiParamTypeClasses, ScopedTypeVariables, GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE OverloadedStrings, MultiParamTypeClasses, DeriveAnyClass #-}
 module Twee.Rule where
 
 import Twee.Base
@@ -22,17 +22,16 @@
 import Data.Tuple
 import Twee.Profile
 import Data.MemoUgly
-import Debug.Trace
-import Twee.Pretty
-import Data.Function
+--import Debug.Trace
 import Control.Arrow((***))
 import GHC.Stack
 import Test.QuickCheck hiding (Function, subterms, Fun)
-import Twee.Profile
 import Test.QuickCheck.Gen
 import Data.Semigroup
 import qualified Data.List.NonEmpty as NonEmpty
 import Test.QuickCheck.Random
+import GHC.Generics
+import Data.Binary.Sharing
 
 --------------------------------------------------------------------------------
 -- * Rewrite rules.
@@ -48,13 +47,15 @@
     -- For unoriented rules: vars lhs == vars rhs
     
     -- | A proof that the rule holds.
+    -- For efficiency, is not updated on substitution or on using 'backwards'.
+    -- Use 'ruleDerivation' to extract a proof which accounts for this.
     rule_proof :: !(Proof f),
 
     -- | The left-hand side of the rule.
     lhs :: {-# UNPACK #-} !(Term f),
     -- | The right-hand side of the rule.
     rhs :: {-# UNPACK #-} !(Term f) }
-  deriving Show
+  deriving (Show, Generic, Binary)
 instance Eq (Rule f) where
   x == y = compare x y == EQ
 instance Ord (Rule f) where
@@ -92,7 +93,7 @@
   | Permutative [(Term f, Term f)]
     -- | An unoriented rule.
   | Unoriented
-  deriving Show
+  deriving (Show, Generic, Binary)
 
 instance Eq (Orientation f) where _ == _ = True
 instance Ord (Orientation f) where compare _ _ = EQ
@@ -542,6 +543,7 @@
     cf_right :: Reduction1 f,
     cf_orig_term :: Term f,
     cf_orig_left :: Reduction1 f }
+  deriving (Generic, Binary)
 
 cf_left_term, cf_right_term :: ConfluenceFailure f -> Term f
 cf_left_term ConfluenceFailure{..} = result1 cf_term cf_left
@@ -628,7 +630,7 @@
     trace _ x = x
     --normFirstStep t = trace (prettyShow (t, take 1 $ anywhere1 strat t)) $ head (head (anywhere1 strat t))
     normSteps t = normaliseWith1 (const True) strat t
-    normStepsVia r t = r `trans1` normSteps (result1 t r)
+    --normStepsVia r t = r `trans1` normSteps (result1 t r)
     norm =
       memo $ \t ->
         stamp "hasUNF.norm" $
@@ -660,7 +662,7 @@
     -- precondition: normR t r1 /= normR t r2
     --conflict, conflict' :: Term f -> Reduction1 f -> Term f -> Reduction1 f -> Term f -> UNF f
     conflict t rs1 u rs2 v = stamp "conflict" (conflict' t rs1 u rs2 v)
-    conflict' t (r1:rs1) u (r2:rs2) v
+    conflict' t (r1:_rs1) _u (r2:_rs2) _v
       | trace "" $
         trace ("Conflicting term: " ++ prettyShow t) $
         trace ("Rule 1: " ++ prettyShow r1) $
diff --git a/Twee/Rule/Index.hs b/Twee/Rule/Index.hs
--- a/Twee/Rule/Index.hs
+++ b/Twee/Rule/Index.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE RecordWildCards, ScopedTypeVariables, FlexibleContexts, TypeFamilies #-}
+{-# LANGUAGE DeriveAnyClass #-}
 module Twee.Rule.Index(
   RuleIndex(..),
   empty, insert, delete,
@@ -9,12 +9,14 @@
 import Twee.Rule
 import Twee.Index hiding (insert, delete, empty)
 import qualified Twee.Index as Index
+import GHC.Generics
+import Data.Binary.Sharing(Binary)
 
 data RuleIndex f a =
   RuleIndex {
     index_oriented :: !(Index f a),
     index_all      :: !(Index f a) }
-  deriving Show
+  deriving (Show, Generic, Binary)
 
 empty :: RuleIndex f a
 empty = RuleIndex Index.empty Index.empty
diff --git a/Twee/Task.hs b/Twee/Task.hs
--- a/Twee/Task.hs
+++ b/Twee/Task.hs
@@ -1,5 +1,4 @@
 -- | A module which can run housekeeping tasks every so often.
-{-# LANGUAGE RecordWildCards #-}
 module Twee.Task(Task, newTask, checkTask) where
 
 import System.CPUTime
diff --git a/Twee/Term.hs b/Twee/Term.hs
--- a/Twee/Term.hs
+++ b/Twee/Term.hs
@@ -1,4 +1,4 @@
--- | Terms and substitutions.
+-- | Terms and substitutions
 --
 -- Terms in twee are represented as arrays rather than as an algebraic data
 -- type. This module defines pattern synonyms ('App', 'Var', 'Cons', 'Nil')
@@ -13,7 +13,7 @@
 --   * substitutions ('Substitution', 'Subst', 'subst');
 --   * unification ('unify') and matching ('match');
 --   * miscellaneous useful functions on terms.
-{-# LANGUAGE BangPatterns, PatternSynonyms, ViewPatterns, TypeFamilies, OverloadedStrings, ScopedTypeVariables, CPP, DefaultSignatures #-}
+{-# LANGUAGE PatternSynonyms, ViewPatterns, OverloadedStrings, CPP, DefaultSignatures, TypeApplications, GeneralizedNewtypeDeriving #-}
 {-# OPTIONS_GHC -O2 -fmax-worker-args=100 #-}
 #ifdef USE_LLVM
 {-# OPTIONS_GHC -fllvm #-}
@@ -65,7 +65,6 @@
 
 import Prelude hiding (lookup)
 import Twee.Term.Core hiding (F)
-import qualified Twee.Term.Core as Core
 import Data.List hiding (lookup, find, singleton)
 import Data.Maybe
 #if __GLASGOW_HASKELL__ < 804
@@ -73,10 +72,11 @@
 #endif
 import Data.IntMap.Strict(IntMap)
 import qualified Data.IntMap.Strict as IntMap
-import Control.Arrow((&&&))
 import Twee.Utils
 import Data.Intern
 import GHC.Stack
+import Data.Binary.Sharing
+import Data.Hashable
 
 --------------------------------------------------------------------------------
 -- * A type class for builders
@@ -211,6 +211,8 @@
   Subst {
     unSubst :: IntMap (TermList f) }
   deriving (Eq, Ord)
+instance Hashable (Subst f) where
+  hashWithSalt s = hashWithSalt s . substToList
 
 -- | Return the highest-number variable in a substitution plus 1.
 {-# INLINE substSize #-}
@@ -351,7 +353,7 @@
 matchListIn !sub !pat !t
   | lenList t < lenList pat = Nothing
   | otherwise =
-    let 
+    let
         loop !sub ConsSym{hd = pat, tl = pats, rest = pats1} !ts = do
           ConsSym{hd = t, tl = ts, rest = ts1} <- Just ts
           case (pat, t) of
@@ -510,6 +512,34 @@
     occurs _ _ _ = Just ()
 
 --------------------------------------------------------------------------------
+-- Serialisation.
+--------------------------------------------------------------------------------
+
+instance (Intern f, Binary f) => Binary (TermList f) where
+  put t = put (unpack t)
+  get = buildList <$> getList getTerm
+
+type BinarydTerm f = Either Var (Sym f, TermList f)
+
+instance (Intern f, Binary f) => Binary (Term f) where
+  put (Var x) = put (Left x :: BinarydTerm f)
+  put (App f ts) = put (Right (f, ts) :: BinarydTerm f)
+  get = build <$> getTerm
+
+getTerm :: forall f. (Intern f, Binary f) => Get (Builder f)
+getTerm = do
+  val <- get :: Get (BinarydTerm f)
+  case val of
+    Left x -> return (var x)
+    Right (f, ts) -> return (app f ts)
+
+instance (Intern f, Binary f) => Binary (Subst f) where
+  put = put . substToList
+  get = fromJust . listToSubst <$> get
+
+deriving instance Binary Var
+
+--------------------------------------------------------------------------------
 -- Miscellaneous stuff.
 --------------------------------------------------------------------------------
 
@@ -731,3 +761,9 @@
 -- | Compare the values of two 'Sym's.
 (<<) :: (Intern f, Ord f) => Sym f -> Sym f -> Bool
 f << g = unintern f < unintern g
+
+instance Hashable (Term f) where
+  hashWithSalt s = hashWithSalt s . singleton
+instance Hashable (TermList f) where
+  hashWithSalt s = hashWithSalt s . map root . subtermsList
+deriving instance Hashable Var
diff --git a/Twee/Term/Core.hs b/Twee/Term/Core.hs
--- a/Twee/Term/Core.hs
+++ b/Twee/Term/Core.hs
@@ -2,8 +2,8 @@
 -- This module contains all the low-level icky bits
 -- and provides primitives for building higher-level stuff.
 {-# LANGUAGE CPP, PatternSynonyms, ViewPatterns,
-    MagicHash, UnboxedTuples, BangPatterns,
-    RankNTypes, RecordWildCards, GeneralizedNewtypeDeriving,
+    MagicHash, UnboxedTuples,
+    RankNTypes, GeneralizedNewtypeDeriving,
     OverloadedStrings, RoleAnnotations #-}
 {-# OPTIONS_GHC -O2 -fmax-worker-args=100 #-}
 #ifdef USE_LLVM
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, GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE CPP, MagicHash #-}
 module Twee.Utils where
 
 import Control.Arrow((&&&))
@@ -12,8 +12,9 @@
 import GHC.Types
 import Data.Bits
 import System.Random
-import Data.Serialize
+import qualified Data.Set as Set
 --import Test.QuickCheck hiding ((.&.))
+import Data.Binary.Sharing
 
 repeatM :: Monad m => m a -> m [a]
 repeatM = sequence . repeat
@@ -48,6 +49,15 @@
 usortBy' :: Ord b => (a -> b) -> [a] -> [a]
 usortBy' f = map snd . usortBy (comparing fst) . map (\x -> (f x, x))
 
+-- Like usort but preserves order
+fastNub :: Ord a => [a] -> [a]
+fastNub xs = collect Set.empty xs
+  where
+    collect _ [] = []
+    collect seen (x:xs)
+      | x `Set.member` seen = collect seen xs
+      | otherwise = x:collect (Set.insert x seen) xs
+
 orElse :: Ordering -> Ordering -> Ordering
 EQ `orElse` x = x
 x  `orElse` _ = x
@@ -143,6 +153,12 @@
     prefix = [0..k-1]
 
 data Sample a = Sample Integer [(Integer, Int)] [a]
+-- TODO serialise properly
+instance Binary a => Binary (Sample a) where
+  put _ = put ()
+  get = do
+    () <- get
+    return (emptySample 10)
 
 emptySample :: Int -> Sample a
 emptySample k = Sample 0 (reservoir k) []
@@ -178,41 +194,6 @@
 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
diff --git a/twee-lib.cabal b/twee-lib.cabal
--- a/twee-lib.cabal
+++ b/twee-lib.cabal
@@ -1,7 +1,7 @@
 name:                twee-lib
-version:             2.6.1
+version:             2.7.1
 synopsis:            An equational theorem prover
-homepage:            http://github.com/nick8325/twee
+homepage:            http://smallbone.se
 license:             BSD3
 license-file:        LICENSE
 author:              Nick Smallbone
@@ -26,8 +26,8 @@
 
 source-repository head
   type:     git
-  location: https://github.com/nick8325/twee.git
-  branch:   master
+  location: https://codeberg.org/nick8325/twee
+  branch:   main
 
 flag llvm
   description: Build using LLVM backend for faster code.
@@ -55,6 +55,7 @@
     Twee.Index
     Twee.Join
     Twee.KBO
+    Twee.LPO
     Twee.Pretty
     Twee.Profile
     Twee.Proof
@@ -65,7 +66,7 @@
     Twee.Utils
     Twee.Term.Core
     Data.Intern
-  other-modules:
+    Data.Binary.Sharing
     Data.BatchedQueue
     Data.ChurchList
     Data.DynamicArray
@@ -83,14 +84,26 @@
     ghc-prim,
     primitive >= 0.7.1.0,
     uglymemo,
-    random,
+    random >= 1.2,
     bytestring,
-    cereal,
-    QuickCheck
+    binary,
+    QuickCheck,
+    deepseq >= 1.4.0.0,
+    unordered-containers,
+    hashable
   hs-source-dirs:      .
-  ghc-options:         -W -fno-warn-incomplete-patterns -fno-warn-dodgy-imports -fno-warn-x-partial
+  ghc-options:         -W -fno-warn-incomplete-patterns -fno-warn-dodgy-imports -fno-warn-deprecations
   default-language:    Haskell2010
-  default-extensions:  TypeOperators
+  default-extensions:
+    BangPatterns
+    DeriveGeneric
+    FlexibleContexts
+    PatternGuards
+    RecordWildCards
+    ScopedTypeVariables
+    StandaloneDeriving
+    TypeFamilies
+    TypeOperators
 
   if flag(llvm)
     cpp-options: -DUSE_LLVM