diff --git a/Changelog.md b/Changelog.md
--- a/Changelog.md
+++ b/Changelog.md
@@ -1,5 +1,16 @@
 # Changelog for the `parameterized-utils` package
 
+## 2.3.1.0 -- 2026-08-27
+
+* Add `Hashable` and `Num` instances for `Fin`.
+* Add `mkFinModN`, `finFromNatModN`, `addFinModN`, `subFinModN`, `mulFinModN`,
+  `negFinModN`, and `recipFinModN` to `Data.Parameterized.Fin`.
+* Add `modNat`, `modIsLeq`, `withModLeq`, and `withRecipModNat` to
+  `Data.Parameterized.NatRepr`.
+* Add an `Ord` instance for `NatRepr`.
+* Change the `Show` instance for `Fin` such that calling `showsPrec p` will
+  parenthesize the output if `p` is sufficiently large.
+
 ## 2.3.0.0 -- 2026-03-06
 
   * BREAKING: Remove the `Iso`s `fin0Void`, `fin1Unit`, and `fin2Bool`.
diff --git a/parameterized-utils.cabal b/parameterized-utils.cabal
--- a/parameterized-utils.cabal
+++ b/parameterized-utils.cabal
@@ -1,6 +1,6 @@
 Cabal-version: 2.2
 Name:          parameterized-utils
-Version:       2.3.0.0
+Version:       2.3.1.0
 Author:        Galois Inc.
 Maintainer:    kquick@galois.com, rscott@galois.com
 stability:     stable
@@ -65,6 +65,11 @@
                , text
                , vector         >=0.12 && < 0.14
 
+  if impl(ghc >= 9.0)
+    build-depends: ghc-bignum >= 1.0 && < 1.5
+  else
+    build-depends: integer-gmp >= 1.0 && < 1.1
+
   hs-source-dirs: src
 
   exposed-modules:
@@ -108,6 +113,7 @@
 
   other-modules:
     Data.Parameterized.NatRepr.Internal
+    Data.Parameterized.Utils.BinTree.Internal
 
   if flag(unsafe-operations)
     cpp-options: -DUNSAFE_OPS
diff --git a/src/Data/Parameterized/Fin.hs b/src/Data/Parameterized/Fin.hs
--- a/src/Data/Parameterized/Fin.hs
+++ b/src/Data/Parameterized/Fin.hs
@@ -23,21 +23,30 @@
 module Data.Parameterized.Fin
   ( Fin
   , mkFin
+  , mkFinModN
   , buildFin
   , countFin
   , viewFin
+  , finFromNatModN
   , finToNat
   , embed
   , tryEmbed
   , minFin
   , incFin
   , fin0Absurd
+  , addFinModN
+  , subFinModN
+  , mulFinModN
+  , negFinModN
+  , recipFinModN
   ) where
 
+import Data.Hashable (Hashable(..))
 import GHC.TypeNats (KnownNat)
 import Numeric.Natural (Natural)
 
 import Data.Parameterized.NatRepr
+import Data.Parameterized.Some (Some(..))
 
 -- | The type @'Fin' n@ has exactly @n@ inhabitants.
 data Fin n =
@@ -50,20 +59,60 @@
 instance Ord (Fin n) where
   compare i j = compare (finToNat i) (finToNat j)
 
+instance Hashable (Fin n) where
+  hashWithSalt salt (Fin i) = hashWithSalt salt i
+
 instance (1 <= n, KnownNat n) => Bounded (Fin n) where
   minBound = Fin (knownNat @0)
   maxBound =
     case minusPlusCancel (knownNat @n) (knownNat @1) of
       Refl -> Fin (decNat (knownNat @n))
 
--- | Non-lawful instance, intended only for testing.
+-- | Arithmetic is performed modulo @n@.
+instance (1 <= n, KnownNat n) => Num (Fin n) where
+  (+) = addFinModN (knownNat @n)
+  (-) = subFinModN (knownNat @n)
+  (*) = mulFinModN (knownNat @n)
+  negate = negFinModN (knownNat @n)
+
+  -- | We consider all Fin values to be non-negative. Therefore, this always
+  -- returns the input unchanged.
+  abs = id
+
+  -- | We consider all Fin values to be non-negative. Therefore, this always
+  -- returns either 'minFin' (i.e., zero) or @'mkFinModN' n (knownNat \@1)@
+  -- (i.e., one). Note that in the degenerate case of @'Fin' 1@, these values
+  -- will be equal to each other.
+  signum f
+    | f == minFin
+    = f
+    | otherwise
+    = mkFinModN (knownNat @n) (knownNat @1)
+
+  -- | Negative integers are negated, reduced modulo @n@, and then negated
+  -- again using 'negFinModN'.
+  fromInteger i
+    | i >= 0
+    = finFromNatModN n (fromInteger i)
+    | otherwise
+    = negFinModN n (finFromNatModN n (fromInteger (negate i)))
+    where
+      n = knownNat @n
+
+-- Equivalent to what a derived Show instance would be, except that we
+-- intentionally do not print out the (non-exported) _getFin field name.
 instance Show (Fin n) where
-  show i = "Fin " ++ show (finToNat i)
+  showsPrec p i = showParen (p >= 11) $ showString "Fin " . shows (finToNat i)
 
 mkFin :: forall i n. (i + 1 <= n) => NatRepr i -> Fin n
 mkFin = Fin
 {-# INLINE mkFin #-}
 
+-- | Construct a @'Fin' n@ value from the number @i@, where @i@ is reduced
+-- modulo @n@.
+mkFinModN :: (1 <= n) => NatRepr n -> NatRepr i -> Fin n
+mkFinModN n i = withModLeq i n Fin
+
 newtype Fin' n = Fin' { getFin' :: Fin (n + 1) }
 
 buildFin ::
@@ -92,6 +141,13 @@
 viewFin ::  (forall i. (i + 1 <= n) => NatRepr i -> r) -> Fin n -> r
 viewFin f (Fin i) = f i
 
+-- | Construct a @'Fin' n@ value from a 'Natural' input, where the input is
+-- reduced modulo @n@.
+finFromNatModN :: forall n. (1 <= n) => NatRepr n -> Natural -> Fin n
+finFromNatModN n i
+  | Some i' <- mkNatRepr i
+  = mkFinModN n i'
+
 finToNat :: Fin n -> Natural
 finToNat (Fin i) = natValue i
 {-# INLINABLE finToNat #-}
@@ -128,3 +184,36 @@
       case plusComm x (knownNat @1) of
         Refl ->
           case addIsLeqLeft1 @1 @o @0 LeqProof of {})
+
+-- | Add two @'Fin' n@ values and reduce the result modulo @n@.
+addFinModN :: (1 <= n) => NatRepr n -> Fin n -> Fin n -> Fin n
+addFinModN n (Fin x) (Fin y) = mkFinModN n (addNat x y)
+
+-- | Subtract two @'Fin' n@ values and reduce the result modulo @n@.
+subFinModN :: (1 <= n) => NatRepr n -> Fin n -> Fin n -> Fin n
+subFinModN n x y = addFinModN n x (negFinModN n y)
+
+-- | Multiply two @'Fin' n@ values and reduce the result modulo @n@.
+mulFinModN :: (1 <= n) => NatRepr n -> Fin n -> Fin n -> Fin n
+mulFinModN n (Fin x) (Fin y) = mkFinModN n (natMultiply x y)
+
+-- | Given a value @i :: 'Fin' n@ value, negate it. That is, if @i@ is zero,
+-- then return @i@ unchanged, and if @i@ is non-zero, then compute @n - i@.
+-- This is a negation in the sense that it is an additive inverse: adding @i@
+-- to its negation will yield 'minFin'.
+negFinModN :: forall n. (1 <= n) => NatRepr n -> Fin n -> Fin n
+negFinModN n (Fin (i :: NatRepr i))
+  | LeqProof <- addIsLeqLeft1 @i @1 @n LeqProof
+  = mkFinModN n (subNat n i)
+
+-- | Given a value @i :: 'Fin' n@, compute the reciprocal (i.e., the modular
+-- inverse) if one exists. That is, attempt to compute @i^-1@ such that
+-- @i * i^-1@ equals @1@ modulo @n@. Note that a reciprocal will only exist if
+-- @i@ and @n@ are relatively prime, i.e., if @gcd i n == 1@. If they are not
+-- relatively prime, then this function will return 'Nothing'.
+--
+-- Note that in the degenerate case where @n == 1@, this function will always
+-- return @Just 0@. The value @0@ is the only element of @'Fin' 1@, and @0@ is
+-- its own reciprocal.
+recipFinModN :: forall n. (1 <= n) => NatRepr n -> Fin n -> Maybe (Fin n)
+recipFinModN n (Fin i) = withRecipModNat i n Fin
diff --git a/src/Data/Parameterized/Map.hs b/src/Data/Parameterized/Map.hs
--- a/src/Data/Parameterized/Map.hs
+++ b/src/Data/Parameterized/Map.hs
@@ -94,7 +94,7 @@
 import           Data.Parameterized.Some
 import           Data.Parameterized.Pair ( Pair(..) )
 import           Data.Parameterized.TraversableF
-import           Data.Parameterized.Utils.BinTree
+import           Data.Parameterized.Utils.BinTree.Internal
   ( MaybeS(..)
   , fromMaybeS
   , Updated(..)
@@ -106,7 +106,7 @@
   , balanceR
   , glue
   )
-import qualified Data.Parameterized.Utils.BinTree as Bin
+import qualified Data.Parameterized.Utils.BinTree.Internal as Bin
 
 ------------------------------------------------------------------------
 -- * Pair
@@ -115,6 +115,53 @@
 comparePairKeys (Pair x _) (Pair y _) = toOrdering (compareF x y)
 {-# INLINABLE comparePairKeys #-}
 
+-- 'MapF' is the only 'IsBinTree' instance, so specialize each polymorphic
+-- 'BinTree' helper used below. This removes class-dictionary indirection
+-- through 'asBin'/'bin'/'size'/'tip' in the generated Core.
+{-# SPECIALIZE Bin.insert
+      :: (Pair k a -> Pair k a -> Ordering)
+      -> Pair k a -> MapF k a -> Updated (MapF k a) #-}
+{-# SPECIALIZE Bin.delete
+      :: (Pair k a -> Ordering) -> MapF k a -> MaybeS (MapF k a) #-}
+{-# SPECIALIZE Bin.union
+      :: (Pair k a -> Pair k a -> Ordering)
+      -> MapF k a -> MapF k a -> MapF k a #-}
+{-# SPECIALIZE Bin.link
+      :: Pair k a -> MapF k a -> MapF k a -> MapF k a #-}
+{-# SPECIALIZE Bin.merge :: MapF k a -> MapF k a -> MapF k a #-}
+{-# SPECIALIZE balanceL
+      :: Pair k a -> MapF k a -> MapF k a -> MapF k a #-}
+{-# SPECIALIZE balanceR
+      :: Pair k a -> MapF k a -> MapF k a -> MapF k a #-}
+{-# SPECIALIZE glue :: MapF k a -> MapF k a -> MapF k a #-}
+{-# SPECIALIZE Bin.filterGt
+      :: (Pair k a -> Ordering) -> MapF k a -> MaybeS (MapF k a) #-}
+{-# SPECIALIZE Bin.filterLt
+      :: (Pair k a -> Ordering) -> MapF k a -> MaybeS (MapF k a) #-}
+-- These helpers are called from the bodies of the specialized exported
+-- 'BinTree' functions above, but the specializer doesn't propagate the
+-- concrete instance dictionary into them, so we specialize them explicitly
+-- (import site: 'Data.Parameterized.Utils.BinTree.Internal').
+{-# SPECIALIZE Bin.insertMax :: Pair k a -> MapF k a -> MapF k a #-}
+{-# SPECIALIZE Bin.insertMin :: Pair k a -> MapF k a -> MapF k a #-}
+{-# SPECIALIZE Bin.insertR
+      :: (Pair k a -> Pair k a -> Ordering)
+      -> Pair k a -> MapF k a -> MapF k a #-}
+{-# SPECIALIZE Bin.hedgeUnion_LB
+      :: (Pair k a -> Pair k a -> Ordering)
+      -> Pair k a -> MapF k a -> MapF k a -> MapF k a #-}
+{-# SPECIALIZE Bin.hedgeUnion_UB
+      :: (Pair k a -> Pair k a -> Ordering)
+      -> Pair k a -> MapF k a -> MapF k a -> MapF k a #-}
+{-# SPECIALIZE Bin.hedgeUnion_LB_UB
+      :: (Pair k a -> Pair k a -> Ordering)
+      -> Pair k a -> Pair k a -> MapF k a -> MapF k a -> MapF k a #-}
+-- 'deleteFindMin' and 'deleteFindMax' use an 'INLINE' pragma instead of
+-- 'SPECIALIZE': they are tight recursive functions (driven by their own
+-- worker 'go') whose outer wrappers are easy to inline, which resolves the
+-- dictionary at each call site without introducing a lingering worker
+-- ('$wdeleteFindM{in,ax}') that still receives a dictionary parameter.
+
 ------------------------------------------------------------------------
 -- MapF
 
@@ -147,12 +194,17 @@
 instance Bin.IsBinTree (MapF k a) (Pair k a) where
   asBin (Bin _ k v l r) = BinTree (Pair k v) l r
   asBin Tip = TipTree
+  {-# INLINE asBin #-}
 
   tip = Tip
+  {-# INLINE tip #-}
+
   bin (Pair k v) l r = Bin (size l + size r + 1) k v l r
+  {-# INLINE bin #-}
 
   size Tip              = 0
   size (Bin sz _ _ _ _) = sz
+  {-# INLINE size #-}
 
 instance (TestEquality k, EqF a) => Eq (MapF k a) where
   x == y = size x == size y && toList x == toList y
@@ -409,7 +461,6 @@
 insert :: OrdF k => k tp -> a tp -> MapF k a -> MapF k a
 insert = \k v m -> seq k $ updatedValue (Bin.insert comparePairKeys (Pair k v) m)
 {-# INLINABLE insert #-}
--- {-# SPECIALIZE Bin.insert :: OrdF k => Pair k a -> MapF k a -> Updated (MapF k a) #-}
 
 -- | Insert a binding into the map, replacing the existing binding if needed.
 insertWithImpl :: OrdF k => (a tp -> a tp -> a tp) -> k tp -> a tp -> MapF k a -> Updated (MapF k a)
@@ -445,7 +496,6 @@
   where p :: OrdF k => k tp -> Pair k a -> Ordering
         p k (Pair kx _) = toOrdering (compareF k kx)
 {-# INLINABLE delete #-}
-{-# SPECIALIZE Bin.delete :: (Pair k a -> Ordering) -> MapF k a -> MaybeS (MapF k a) #-}
 
 -- | Left-biased union of two maps. The resulting map will contain the
 -- union of the keys of the two arguments. When a key is contained in
@@ -453,7 +503,6 @@
 union :: OrdF k => MapF k a -> MapF k a -> MapF k a
 union t1 t2 = Bin.union comparePairKeys t1 t2
 {-# INLINABLE union #-}
--- {-# SPECIALIZE Bin.union compare :: OrdF k => MapF k a -> MapF k a -> MapF k a #-}
 
 ------------------------------------------------------------------------
 -- updateAtKey
diff --git a/src/Data/Parameterized/NatRepr.hs b/src/Data/Parameterized/NatRepr.hs
--- a/src/Data/Parameterized/NatRepr.hs
+++ b/src/Data/Parameterized/NatRepr.hs
@@ -25,6 +25,7 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MagicHash #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE ScopedTypeVariables #-}
@@ -33,6 +34,7 @@
 {-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE UnboxedSums #-}
 {-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
 #if __GLASGOW_HASKELL__ >= 805
 {-# LANGUAGE NoStarIsType #-}
@@ -54,8 +56,10 @@
   , addNat
   , subNat
   , divNat
+  , modNat
   , halfNat
   , withDivModNat
+  , withRecipModNat
   , natMultiply
   , someNat
   , mkNatRepr
@@ -108,6 +112,8 @@
   , addIsLeqLeft1
   , dblPosIsPos
   , leqMulMono
+  , modIsLeq
+  , withModLeq
     -- * Arithmetic proof
   , plusComm
   , plusAssoc
@@ -137,7 +143,7 @@
 import Data.Void as Void
 import Numeric.Natural
 import GHC.TypeNats ( KnownNat, Nat, SomeNat(..)
-                    , type (+), type (-), type (*), type (<=)
+                    , type (+), type (-), type (*), type (<=), type Mod
                     , someNatVal )
 import Unsafe.Coerce
 
@@ -145,6 +151,12 @@
 import Data.Parameterized.NatRepr.Internal
 import Data.Parameterized.Some
 
+#if MIN_VERSION_base(4,15,0)
+import qualified GHC.Num.Integer as Integer
+#else
+import qualified GHC.Integer.GMP.Internals as GMP
+#endif
+
 maxInt :: Natural
 maxInt = fromIntegral (maxBound :: Int)
 
@@ -218,6 +230,9 @@
 divNat :: (1 <= n) => NatRepr (m * n) -> NatRepr n -> NatRepr m
 divNat (NatRepr x) (NatRepr y) = NatRepr (div x y)
 
+modNat :: (1 <= n) => NatRepr m -> NatRepr n -> NatRepr (Mod m n)
+modNat (NatRepr x) (NatRepr y) = NatRepr (mod x y)
+
 withDivModNat :: forall n m a.
                  NatRepr n
               -> NatRepr m
@@ -232,6 +247,67 @@
   where
     (divPart, modPart) = divMod (natValue n) (natValue m)
 
+-- | @'withRecipModNat' n m@ computes the reciprocal (i.e., the modular
+-- inverse) of @n@ mod @m@. If @n@ and @m@ are relatively prime (i.e., if
+-- @gcd n m == 1@), then this will pass the reciprocal @r@ to a continuation
+-- and return the result with 'Just'. Otherwise, this will return 'Nothing',
+-- as a reciprocal does not exist.
+withRecipModNat ::
+  forall n m a.
+  (1 <= m) =>
+  NatRepr n ->
+  NatRepr m ->
+  (forall r. (r + 1 <= m, Mod (n * r) m ~ 1) => NatRepr r -> a) ->
+  Maybe a
+withRecipModNat n m f =
+  fmap (go . mkNatRepr) (integerRecipMod (intValue n) (natValue m))
+  where
+    go :: Some NatRepr -> a
+    go (Some (r :: NatRepr r)) =
+      case ( unsafeCoerce @(LeqProof 0 0) @(LeqProof (r + 1) m) LeqProof
+           , unsafeAxiom @(Mod (n * r) m) @1
+           ) of
+        (LeqProof, Refl) -> f r
+
+-- | Compute the modular inverse, returning 'Nothing' when this is not
+-- possible. This behaves much like 'Integer.integerRecipMod#' in @ghc-bignum@,
+-- except that this returns a 'Maybe' instead of an unboxed sum to represent
+-- the possibility of failure. For more details on when this can return
+-- 'Nothing', see the Haddocks for 'Integer.integerRecipMod#'.
+--
+-- Because 'Integer.integerRecipMod#' is only defined on GHC 9.0 or later, we
+-- fall back to a different implementation using the @integer-gmp@ library on
+-- older versions of GHC.
+#if MIN_VERSION_base(4,15,0)
+integerRecipMod :: Integer -> Natural -> Maybe Natural
+integerRecipMod x y
+  -- Due to https://gitlab.haskell.org/ghc/ghc/-/issues/26017, old versions of
+  -- GHC have a bug in which `integerRecipMod# x 1` would return (# | () #)
+  -- instead of (# 0 | #) for all `x`, contrary to the function's Haddocks. We
+  -- include an extra check on old versions of GHC to work around this issue.
+# if !MIN_VERSION_base(4,22,0)
+  | y == 1 = Just 0
+# endif
+  | otherwise =
+      case Integer.integerRecipMod# x y of
+        (# r | #)  -> Just r
+        (# | () #) -> Nothing
+#else
+integerRecipMod :: Integer -> Natural -> Maybe Natural
+integerRecipMod x y
+    -- Special case for `y == 1`, which we include to make the behavior of this
+    -- function match that of integerRecipMod# on GHC 9.0 or later. Without
+    -- this special case, this function would always return `Nothing` when the
+    -- modulus is `1`.
+  | y == 1 = Just 0
+  | res == 0 = Nothing
+  | otherwise = Just res
+  where
+    -- SAFETY: GMP.recipModInteger always returns a non-negative Integer, so
+    -- the call to `fromInteger @Natural` below will always succeed.
+    res = fromInteger @Natural (GMP.recipModInteger x (toInteger y))
+#endif
+
 natMultiply :: NatRepr n -> NatRepr m -> NatRepr (n * m)
 natMultiply (NatRepr n) (NatRepr m) = NatRepr (n * m)
 
@@ -523,6 +599,18 @@
 
 withAddLeq :: forall n m a. NatRepr n -> NatRepr m -> ((n <= n + m) => NatRepr (n + m) -> a) -> a
 withAddLeq n m f = withLeqProof (addIsLeq n m) (f (addNat n m))
+
+modIsLeq :: (1 <= m) => f n -> g m -> LeqProof (Mod n m + 1) m
+modIsLeq _ _ = unsafeCoerce (LeqProof @0 @0)
+{-# NOINLINE modIsLeq #-}
+
+withModLeq ::
+  (1 <= m) =>
+  NatRepr n ->
+  NatRepr m ->
+  ((Mod n m + 1 <= m) => NatRepr (Mod n m) -> a) ->
+  a
+withModLeq n m f = withLeqProof (modIsLeq n m) (f (modNat n m))
 
 natForEach' :: forall l h a
             . NatRepr l
diff --git a/src/Data/Parameterized/NatRepr/Internal.hs b/src/Data/Parameterized/NatRepr/Internal.hs
--- a/src/Data/Parameterized/NatRepr/Internal.hs
+++ b/src/Data/Parameterized/NatRepr/Internal.hs
@@ -51,6 +51,9 @@
 instance EqF NatRepr where
   eqF _ _ = True
 
+instance Ord (NatRepr x) where
+   compare _ _ = EQ
+
 instance TestEquality NatRepr where
   testEquality (NatRepr m) (NatRepr n)
     | m == n = Just unsafeAxiom
diff --git a/src/Data/Parameterized/Utils/BinTree.hs b/src/Data/Parameterized/Utils/BinTree.hs
--- a/src/Data/Parameterized/Utils/BinTree.hs
+++ b/src/Data/Parameterized/Utils/BinTree.hs
@@ -3,13 +3,6 @@
 Copyright        : (c) Galois, Inc 2014-2019
 Maintainer       : Joe Hendrix <jhendrix@galois.com>
 -}
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE ViewPatterns #-}
 {-# LANGUAGE Safe #-}
 module Data.Parameterized.Utils.BinTree
   ( MaybeS(..)
@@ -31,338 +24,4 @@
   , PairS(..)
   ) where
 
-import Control.Applicative
-
-------------------------------------------------------------------------
--- MaybeS
-
--- | A strict version of 'Maybe'
-data MaybeS v
-   = JustS !v
-   | NothingS
-
-instance Functor MaybeS where
-  fmap _ NothingS = NothingS
-  fmap f (JustS v) = JustS (f v)
-
-instance Alternative MaybeS where
-  empty = NothingS
-  mv@JustS{} <|> _ = mv
-  NothingS <|> v = v
-
-instance Applicative MaybeS where
-  pure = JustS
-
-  NothingS <*> _ = NothingS
-  JustS{} <*> NothingS = NothingS
-  JustS f <*> JustS x = JustS (f x)
-
-fromMaybeS :: a -> MaybeS a -> a
-fromMaybeS r NothingS = r
-fromMaybeS _ (JustS v) = v
-
-------------------------------------------------------------------------
--- Updated
-
--- | @Updated a@ contains a value that has been flagged on whether it was
--- modified by an operation.
-data Updated a
-   = Updated   !a
-   | Unchanged !a
-
-updatedValue :: Updated a -> a
-updatedValue (Updated a) = a
-updatedValue (Unchanged a) = a
-
-------------------------------------------------------------------------
--- IsBinTree
-
-data TreeApp e t
-   = BinTree !e !t !t
-   | TipTree
-
-class IsBinTree t e | t -> e where
-  asBin :: t -> TreeApp e t
-  tip :: t
-
-  bin :: e -> t -> t -> t
-  size :: t -> Int
-
-delta,ratio :: Int
-delta = 3
-ratio = 2
-
--- | @balanceL p l r@ returns a balanced tree for the sequence @l ++ [p] ++ r@.
---
--- It assumes that @l@ and @r@ are close to being balanced, and that only
--- @l@ may contain too many elements.
-balanceL :: (IsBinTree c e) => e -> c -> c -> c
-balanceL p l r = do
-  case asBin l of
-    BinTree l_pair ll lr | size l > max 1 (delta*size r) ->
-      case asBin lr of
-        BinTree lr_pair lrl lrr | size lr >= max 2 (ratio*size ll) ->
-          bin lr_pair (bin l_pair ll lrl) (bin p lrr r)
-        _ -> bin l_pair ll (bin p lr r)
-
-    _ -> bin p l r
-{-# INLINE balanceL #-}
-
--- | @balanceR p l r@ returns a balanced tree for the sequence @l ++ [p] ++ r@.
---
--- It assumes that @l@ and @r@ are close to being balanced, and that only
--- @r@ may contain too many elements.
-balanceR :: (IsBinTree c e) => e -> c -> c -> c
-balanceR p l r = do
-  case asBin r of
-    BinTree r_pair rl rr | size r > max 1 (delta*size l) ->
-      case asBin rl of
-        BinTree rl_pair rll rlr | size rl >= max 2 (ratio*size rr) ->
-          (bin rl_pair $! bin p l rll) $! bin r_pair rlr rr
-        _ -> bin r_pair (bin p l rl) rr
-    _ -> bin p l r
-{-# INLINE balanceR #-}
-
--- | Insert a new maximal element.
-insertMax :: IsBinTree c e => e -> c -> c
-insertMax p t =
-  case asBin t of
-    TipTree -> bin p tip tip
-    BinTree q l r -> balanceR q l (insertMax p r)
-
--- | Insert a new minimal element.
-insertMin :: IsBinTree c e => e -> c -> c
-insertMin p t =
-  case asBin t of
-    TipTree -> bin p tip tip
-    BinTree q l r -> balanceL q (insertMin p l) r
-
--- | @link@ is called to insert a key and value between two disjoint subtrees.
-link :: IsBinTree c e => e -> c -> c -> c
-link p l r =
-  case (asBin l, asBin r) of
-    (TipTree, _) -> insertMin p r
-    (_, TipTree) -> insertMax p l
-    (BinTree py ly ry, BinTree pz lz rz)
-     | delta*size l < size r -> balanceL pz (link p l lz) rz
-     | delta*size r < size l -> balanceR py ly (link p ry r)
-     | otherwise             -> bin p l r
-{-# INLINE link #-}
-
--- | A Strict pair
-data PairS f s = PairS !f !s
-
-deleteFindMin :: IsBinTree c e => e -> c -> c -> PairS e c
-deleteFindMin p l r =
-  case asBin l of
-    TipTree -> PairS p r
-    BinTree lp ll lr ->
-      case deleteFindMin lp ll lr of
-        PairS q l' -> PairS q (balanceR p l' r)
-{-# INLINABLE deleteFindMin #-}
-
-deleteFindMax :: IsBinTree c e => e -> c -> c -> PairS e c
-deleteFindMax p l r =
-  case asBin r of
-    TipTree -> PairS p l
-    BinTree rp rl rr ->
-      case deleteFindMax rp rl rr of
-        PairS q r' -> PairS q (balanceL p l r')
-{-# INLINABLE deleteFindMax #-}
-
--- | Concatenate two trees that are ordered with respect to each other.
-merge :: IsBinTree c e => c -> c -> c
-merge l r =
-  case (asBin l, asBin r) of
-    (TipTree, _) -> r
-    (_, TipTree) -> l
-    (BinTree x lx rx, BinTree y ly ry)
-      | delta*size l < size r -> balanceL y (merge l ly) ry
-      | delta*size r < size l -> balanceR x lx (merge rx r)
-      | size l > size r ->
-        case deleteFindMax x lx rx of
-          PairS q l' -> balanceR q l' r
-      | otherwise ->
-        case deleteFindMin y ly ry of
-          PairS q r' -> balanceL q l r'
-{-# INLINABLE merge #-}
-
-------------------------------------------------------------------------
--- Ordered operations
-
--- | @insert p m@ inserts the binding into @m@.  It returns
--- an Unchanged value if the map stays the same size and an updated
--- value if a new entry was inserted.
-insert :: (IsBinTree c e) => (e -> e -> Ordering) -> e -> c -> Updated c
-insert comp x t =
-  case asBin t of
-    TipTree -> Updated (bin x tip tip)
-    BinTree y l r ->
-      case comp x y of
-        LT ->
-          case insert comp x l of
-            Updated l'   -> Updated   (balanceL y l' r)
-            Unchanged l' -> Unchanged (bin       y l' r)
-        GT ->
-          case insert comp x r of
-            Updated r'   -> Updated   (balanceR y l r')
-            Unchanged r' -> Unchanged (bin       y l r')
-        EQ -> Unchanged (bin x l r)
-{-# INLINABLE insert #-}
-
--- | @glue l r@ concatenates @l@ and @r@.
---
--- It assumes that @l@ and @r@ are already balanced with respect to each other.
-glue :: IsBinTree c e => c -> c -> c
-glue l r =
-  case (asBin l, asBin r) of
-    (TipTree, _) -> r
-    (_, TipTree) -> l
-    (BinTree x lx rx, BinTree y ly ry)
-     | size l > size r ->
-       case deleteFindMax x lx rx of
-         PairS q l' -> balanceR q l' r
-     | otherwise ->
-       case deleteFindMin y ly ry of
-         PairS q r' -> balanceL q l r'
-{-# INLINABLE glue #-}
-
-delete :: IsBinTree c e
-       => (e -> Ordering)
-          -- ^ Predicate that returns whether the entry is less than, greater than, or equal
-          -- to the key we are entry that we are looking for.
-       -> c
-       -> MaybeS c
-delete k t =
-  case asBin t of
-    TipTree -> NothingS
-    BinTree p l r ->
-      case k p of
-        LT -> (\l' -> balanceR p l' r) <$> delete k l
-        GT -> (\r' -> balanceL p l r') <$> delete k r
-        EQ -> JustS (glue l r)
-{-# INLINABLE delete #-}
-
-------------------------------------------------------------------------
--- filter
-
--- | Returns only entries that are less than predicate with respect to the ordering
--- and Nothing if no elements are discarded.
-filterGt :: IsBinTree c e => (e -> Ordering) -> c -> MaybeS c
-filterGt k t =
-  case asBin t of
-    TipTree -> NothingS
-    BinTree x l r ->
-      case k x of
-        LT -> (\l' -> link x l' r) <$> filterGt k l
-        GT -> filterGt k r <|> JustS r
-        EQ -> JustS r
-{-# INLINABLE filterGt #-}
-
-
--- | @filterLt k m@ returns submap of @m@ that only contains entries
--- that are smaller than @k@.  If no entries are deleted then return Nothing.
-filterLt :: IsBinTree c e => (e -> Ordering) -> c -> MaybeS c
-filterLt k t =
-  case asBin t of
-    TipTree -> NothingS
-    BinTree x l r ->
-      case k x of
-        LT -> filterLt k l <|> JustS l
-        GT -> (\r' -> link x l r') <$> filterLt k r
-        EQ -> JustS l
-{-# INLINABLE filterLt #-}
-
-------------------------------------------------------------------------
--- Union
-
--- | Insert a new key and value in the map if it is not already present.
--- Used by 'union'.
-insertR :: forall c e . (IsBinTree c e) => (e -> e -> Ordering) -> e -> c -> c
-insertR comp e m = fromMaybeS m (go e m)
-  where
-    go :: e -> c -> MaybeS c
-    go x t =
-      case asBin t of
-        TipTree -> JustS (bin x tip tip)
-        BinTree y l r ->
-          case comp x y of
-            LT -> (\l' -> balanceL y l' r) <$> go x l
-            GT -> (\r' -> balanceR y l r') <$> go x r
-            EQ -> NothingS
-{-# INLINABLE insertR #-}
-
--- | Union two sets
-union :: (IsBinTree c e) => (e -> e -> Ordering) -> c -> c -> c
-union comp t1 t2 =
-  case (asBin t1, asBin t2) of
-    (TipTree, _) -> t2
-    (_, TipTree) -> t1
-    (_, BinTree p (asBin -> TipTree) (asBin -> TipTree)) -> insertR comp p t1
-    (BinTree x l r, _) ->
-      link x
-           (hedgeUnion_UB comp x   l t2)
-           (hedgeUnion_LB comp x r   t2)
-{-# INLINABLE union #-}
-
--- | Hedge union where we only add elements in second map if key is
--- strictly above a lower bound.
-hedgeUnion_LB :: (IsBinTree c e) => (e -> e -> Ordering) -> e -> c -> c -> c
-hedgeUnion_LB comp lo t1 t2 =
-  case (asBin t1, asBin t2) of
-    (_, TipTree) -> t1
-    (TipTree, _) -> fromMaybeS t2 (filterGt (comp lo) t2)
-    -- Prune left tree.
-    (_, BinTree k _ r) | comp k lo <= EQ -> hedgeUnion_LB comp lo t1 r
-    -- Special case when t2 is a single element.
-    (_, BinTree x (asBin -> TipTree) (asBin -> TipTree)) -> insertR comp x t1
-    -- Split on left-and-right subtrees of t1.
-    (BinTree x l r, _) ->
-      link x
-           (hedgeUnion_LB_UB comp lo x  l t2)
-           (hedgeUnion_LB    comp x     r t2)
-{-# INLINABLE hedgeUnion_LB #-}
-
--- | Hedge union where we only add elements in second map if key is
--- strictly below a upper bound.
-hedgeUnion_UB :: (IsBinTree c e) => (e -> e -> Ordering) -> e -> c -> c -> c
-hedgeUnion_UB comp hi t1 t2 =
-  case (asBin t1, asBin t2) of
-    (_, TipTree) -> t1
-    (TipTree, _) -> fromMaybeS t2 (filterLt (comp hi) t2)
-    -- Prune right tree.
-    (_, BinTree x l _) | comp x hi >= EQ -> hedgeUnion_UB comp hi t1 l
-    -- Special case when t2 is a single element.
-    (_, BinTree x (asBin -> TipTree) (asBin -> TipTree))  -> insertR comp x t1
-    -- Split on left-and-right subtrees of t1.
-    (BinTree x l r, _) ->
-      link x
-           (hedgeUnion_UB    comp x      l t2)
-           (hedgeUnion_LB_UB comp x  hi  r t2)
-{-# INLINABLE hedgeUnion_UB #-}
-
--- | Hedge union where we only add elements in second map if key is
--- strictly between a lower and upper bound.
-hedgeUnion_LB_UB :: (IsBinTree c e) => (e -> e -> Ordering) -> e -> e -> c -> c -> c
-hedgeUnion_LB_UB comp lo hi t1 t2 =
-  case (asBin t1, asBin t2) of
-    (_, TipTree) -> t1
-    -- Prune left tree.
-    (_,   BinTree k _ r) | comp k lo <= EQ -> hedgeUnion_LB_UB comp lo hi t1 r
-    -- Prune right tree.
-    (_,   BinTree k l _) | comp k hi >= EQ -> hedgeUnion_LB_UB comp lo hi t1 l
-    -- When t1 becomes empty (assumes lo <= k <= hi)
-    (TipTree, BinTree x l r) ->
-      case (filterGt (comp lo) l, filterLt (comp hi) r) of
-        -- No variables in t2 were eliminated.
-        (NothingS, NothingS) -> t2
-        -- Relink t2 with filtered elements removed.
-        (l',r') -> link x (fromMaybeS l l') (fromMaybeS r r')
-    -- Special case when t2 is a single element.
-    (_, BinTree x (asBin -> TipTree) (asBin -> TipTree)) -> insertR comp x t1
-    -- Split on left-and-right subtrees of t1.
-    (BinTree x l r, _) ->
-      link x
-           (hedgeUnion_LB_UB comp lo x  l t2)
-           (hedgeUnion_LB_UB comp x  hi r t2)
-{-# INLINABLE hedgeUnion_LB_UB #-}
+import Data.Parameterized.Utils.BinTree.Internal
diff --git a/src/Data/Parameterized/Utils/BinTree/Internal.hs b/src/Data/Parameterized/Utils/BinTree/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Parameterized/Utils/BinTree/Internal.hs
@@ -0,0 +1,387 @@
+{-|
+Description      : Utilities for balanced binary trees (internal module).
+Copyright        : (c) Galois, Inc 2014-2019
+Maintainer       : Joe Hendrix <jhendrix@galois.com>
+
+This module exports every helper in the file so that downstream modules
+can attach @SPECIALIZE@ pragmas to the internal ones (e.g. 'insertMax',
+'hedgeUnion_LB'). The stable public interface is re-exported from
+"Data.Parameterized.Utils.BinTree".
+-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE Safe #-}
+module Data.Parameterized.Utils.BinTree.Internal
+  ( MaybeS(..)
+  , fromMaybeS
+  , Updated(..)
+  , updatedValue
+  , TreeApp(..)
+  , IsBinTree(..)
+  , balanceL
+  , balanceR
+  , insertMax
+  , insertMin
+  , link
+  , PairS(..)
+  , deleteFindMin
+  , deleteFindMax
+  , merge
+  , insert
+  , glue
+  , delete
+  , filterGt
+  , filterLt
+  , insertR
+  , union
+  , hedgeUnion_LB
+  , hedgeUnion_UB
+  , hedgeUnion_LB_UB
+  ) where
+
+import Control.Applicative
+
+------------------------------------------------------------------------
+-- MaybeS
+
+-- | A strict version of 'Maybe'
+data MaybeS v
+   = JustS !v
+   | NothingS
+
+instance Functor MaybeS where
+  fmap _ NothingS = NothingS
+  fmap f (JustS v) = JustS (f v)
+
+instance Alternative MaybeS where
+  empty = NothingS
+  mv@JustS{} <|> _ = mv
+  NothingS <|> v = v
+
+instance Applicative MaybeS where
+  pure = JustS
+
+  NothingS <*> _ = NothingS
+  JustS{} <*> NothingS = NothingS
+  JustS f <*> JustS x = JustS (f x)
+
+fromMaybeS :: a -> MaybeS a -> a
+fromMaybeS r NothingS = r
+fromMaybeS _ (JustS v) = v
+
+------------------------------------------------------------------------
+-- Updated
+
+-- | @Updated a@ contains a value that has been flagged on whether it was
+-- modified by an operation.
+data Updated a
+   = Updated   !a
+   | Unchanged !a
+
+updatedValue :: Updated a -> a
+updatedValue (Updated a) = a
+updatedValue (Unchanged a) = a
+
+------------------------------------------------------------------------
+-- IsBinTree
+
+data TreeApp e t
+   = BinTree !e !t !t
+   | TipTree
+
+class IsBinTree t e | t -> e where
+  asBin :: t -> TreeApp e t
+  tip :: t
+
+  bin :: e -> t -> t -> t
+  size :: t -> Int
+
+delta,ratio :: Int
+delta = 3
+ratio = 2
+
+-- | @balanceL p l r@ returns a balanced tree for the sequence @l ++ [p] ++ r@.
+--
+-- It assumes that @l@ and @r@ are close to being balanced, and that only
+-- @l@ may contain too many elements.
+balanceL :: (IsBinTree c e) => e -> c -> c -> c
+balanceL p l r = do
+  case asBin l of
+    BinTree l_pair ll lr | size l > max 1 (delta*size r) ->
+      case asBin lr of
+        BinTree lr_pair lrl lrr | size lr >= max 2 (ratio*size ll) ->
+          bin lr_pair (bin l_pair ll lrl) (bin p lrr r)
+        _ -> bin l_pair ll (bin p lr r)
+
+    _ -> bin p l r
+{-# INLINE balanceL #-}
+
+-- | @balanceR p l r@ returns a balanced tree for the sequence @l ++ [p] ++ r@.
+--
+-- It assumes that @l@ and @r@ are close to being balanced, and that only
+-- @r@ may contain too many elements.
+balanceR :: (IsBinTree c e) => e -> c -> c -> c
+balanceR p l r = do
+  case asBin r of
+    BinTree r_pair rl rr | size r > max 1 (delta*size l) ->
+      case asBin rl of
+        BinTree rl_pair rll rlr | size rl >= max 2 (ratio*size rr) ->
+          (bin rl_pair $! bin p l rll) $! bin r_pair rlr rr
+        _ -> bin r_pair (bin p l rl) rr
+    _ -> bin p l r
+{-# INLINE balanceR #-}
+
+-- | Insert a new maximal element.
+insertMax :: IsBinTree c e => e -> c -> c
+insertMax p t =
+  case asBin t of
+    TipTree -> bin p tip tip
+    BinTree q l r -> balanceR q l (insertMax p r)
+{-# INLINABLE insertMax #-}
+
+-- | Insert a new minimal element.
+insertMin :: IsBinTree c e => e -> c -> c
+insertMin p t =
+  case asBin t of
+    TipTree -> bin p tip tip
+    BinTree q l r -> balanceL q (insertMin p l) r
+{-# INLINABLE insertMin #-}
+
+-- | @link@ is called to insert a key and value between two disjoint subtrees.
+link :: IsBinTree c e => e -> c -> c -> c
+link p l r =
+  case (asBin l, asBin r) of
+    (TipTree, _) -> insertMin p r
+    (_, TipTree) -> insertMax p l
+    (BinTree py ly ry, BinTree pz lz rz)
+     | delta*size l < size r -> balanceL pz (link p l lz) rz
+     | delta*size r < size l -> balanceR py ly (link p ry r)
+     | otherwise             -> bin p l r
+{-# INLINE link #-}
+
+-- | A Strict pair
+data PairS f s = PairS !f !s
+
+deleteFindMin :: IsBinTree c e => e -> c -> c -> PairS e c
+deleteFindMin = \p0 l0 r0 ->
+  let go p l r =
+        case asBin l of
+          TipTree -> PairS p r
+          BinTree lp ll lr ->
+            case go lp ll lr of
+              PairS q l' -> PairS q (balanceR p l' r)
+  in go p0 l0 r0
+{-# INLINE deleteFindMin #-}
+
+deleteFindMax :: IsBinTree c e => e -> c -> c -> PairS e c
+deleteFindMax = \p0 l0 r0 ->
+  let go p l r =
+        case asBin r of
+          TipTree -> PairS p l
+          BinTree rp rl rr ->
+            case go rp rl rr of
+              PairS q r' -> PairS q (balanceL p l r')
+  in go p0 l0 r0
+{-# INLINE deleteFindMax #-}
+
+-- | Concatenate two trees that are ordered with respect to each other.
+merge :: IsBinTree c e => c -> c -> c
+merge l r =
+  case (asBin l, asBin r) of
+    (TipTree, _) -> r
+    (_, TipTree) -> l
+    (BinTree x lx rx, BinTree y ly ry)
+      | delta*size l < size r -> balanceL y (merge l ly) ry
+      | delta*size r < size l -> balanceR x lx (merge rx r)
+      | size l > size r ->
+        case deleteFindMax x lx rx of
+          PairS q l' -> balanceR q l' r
+      | otherwise ->
+        case deleteFindMin y ly ry of
+          PairS q r' -> balanceL q l r'
+{-# INLINABLE merge #-}
+
+------------------------------------------------------------------------
+-- Ordered operations
+
+-- | @insert p m@ inserts the binding into @m@.  It returns
+-- an Unchanged value if the map stays the same size and an updated
+-- value if a new entry was inserted.
+insert :: (IsBinTree c e) => (e -> e -> Ordering) -> e -> c -> Updated c
+insert comp x t =
+  case asBin t of
+    TipTree -> Updated (bin x tip tip)
+    BinTree y l r ->
+      case comp x y of
+        LT ->
+          case insert comp x l of
+            Updated l'   -> Updated   (balanceL y l' r)
+            Unchanged l' -> Unchanged (bin       y l' r)
+        GT ->
+          case insert comp x r of
+            Updated r'   -> Updated   (balanceR y l r')
+            Unchanged r' -> Unchanged (bin       y l r')
+        EQ -> Unchanged (bin x l r)
+{-# INLINABLE insert #-}
+
+-- | @glue l r@ concatenates @l@ and @r@.
+--
+-- It assumes that @l@ and @r@ are already balanced with respect to each other.
+glue :: IsBinTree c e => c -> c -> c
+glue l r =
+  case (asBin l, asBin r) of
+    (TipTree, _) -> r
+    (_, TipTree) -> l
+    (BinTree x lx rx, BinTree y ly ry)
+     | size l > size r ->
+       case deleteFindMax x lx rx of
+         PairS q l' -> balanceR q l' r
+     | otherwise ->
+       case deleteFindMin y ly ry of
+         PairS q r' -> balanceL q l r'
+{-# INLINABLE glue #-}
+
+delete :: IsBinTree c e
+       => (e -> Ordering)
+          -- ^ Predicate that returns whether the entry is less than, greater than, or equal
+          -- to the key we are entry that we are looking for.
+       -> c
+       -> MaybeS c
+delete k t =
+  case asBin t of
+    TipTree -> NothingS
+    BinTree p l r ->
+      case k p of
+        LT -> (\l' -> balanceR p l' r) <$> delete k l
+        GT -> (\r' -> balanceL p l r') <$> delete k r
+        EQ -> JustS (glue l r)
+{-# INLINABLE delete #-}
+
+------------------------------------------------------------------------
+-- filter
+
+-- | Returns only entries that are less than predicate with respect to the ordering
+-- and Nothing if no elements are discarded.
+filterGt :: IsBinTree c e => (e -> Ordering) -> c -> MaybeS c
+filterGt k t =
+  case asBin t of
+    TipTree -> NothingS
+    BinTree x l r ->
+      case k x of
+        LT -> (\l' -> link x l' r) <$> filterGt k l
+        GT -> filterGt k r <|> JustS r
+        EQ -> JustS r
+{-# INLINABLE filterGt #-}
+
+
+-- | @filterLt k m@ returns submap of @m@ that only contains entries
+-- that are smaller than @k@.  If no entries are deleted then return Nothing.
+filterLt :: IsBinTree c e => (e -> Ordering) -> c -> MaybeS c
+filterLt k t =
+  case asBin t of
+    TipTree -> NothingS
+    BinTree x l r ->
+      case k x of
+        LT -> filterLt k l <|> JustS l
+        GT -> (\r' -> link x l r') <$> filterLt k r
+        EQ -> JustS l
+{-# INLINABLE filterLt #-}
+
+------------------------------------------------------------------------
+-- Union
+
+-- | Insert a new key and value in the map if it is not already present.
+-- Used by 'union'.
+insertR :: forall c e . (IsBinTree c e) => (e -> e -> Ordering) -> e -> c -> c
+insertR comp e m = fromMaybeS m (go e m)
+  where
+    go :: e -> c -> MaybeS c
+    go x t =
+      case asBin t of
+        TipTree -> JustS (bin x tip tip)
+        BinTree y l r ->
+          case comp x y of
+            LT -> (\l' -> balanceL y l' r) <$> go x l
+            GT -> (\r' -> balanceR y l r') <$> go x r
+            EQ -> NothingS
+{-# INLINABLE insertR #-}
+
+-- | Union two sets
+union :: (IsBinTree c e) => (e -> e -> Ordering) -> c -> c -> c
+union comp t1 t2 =
+  case (asBin t1, asBin t2) of
+    (TipTree, _) -> t2
+    (_, TipTree) -> t1
+    (_, BinTree p (asBin -> TipTree) (asBin -> TipTree)) -> insertR comp p t1
+    (BinTree x l r, _) ->
+      link x
+           (hedgeUnion_UB comp x   l t2)
+           (hedgeUnion_LB comp x r   t2)
+{-# INLINABLE union #-}
+
+-- | Hedge union where we only add elements in second map if key is
+-- strictly above a lower bound.
+hedgeUnion_LB :: (IsBinTree c e) => (e -> e -> Ordering) -> e -> c -> c -> c
+hedgeUnion_LB comp lo t1 t2 =
+  case (asBin t1, asBin t2) of
+    (_, TipTree) -> t1
+    (TipTree, _) -> fromMaybeS t2 (filterGt (comp lo) t2)
+    -- Prune left tree.
+    (_, BinTree k _ r) | comp k lo <= EQ -> hedgeUnion_LB comp lo t1 r
+    -- Special case when t2 is a single element.
+    (_, BinTree x (asBin -> TipTree) (asBin -> TipTree)) -> insertR comp x t1
+    -- Split on left-and-right subtrees of t1.
+    (BinTree x l r, _) ->
+      link x
+           (hedgeUnion_LB_UB comp lo x  l t2)
+           (hedgeUnion_LB    comp x     r t2)
+{-# INLINABLE hedgeUnion_LB #-}
+
+-- | Hedge union where we only add elements in second map if key is
+-- strictly below a upper bound.
+hedgeUnion_UB :: (IsBinTree c e) => (e -> e -> Ordering) -> e -> c -> c -> c
+hedgeUnion_UB comp hi t1 t2 =
+  case (asBin t1, asBin t2) of
+    (_, TipTree) -> t1
+    (TipTree, _) -> fromMaybeS t2 (filterLt (comp hi) t2)
+    -- Prune right tree.
+    (_, BinTree x l _) | comp x hi >= EQ -> hedgeUnion_UB comp hi t1 l
+    -- Special case when t2 is a single element.
+    (_, BinTree x (asBin -> TipTree) (asBin -> TipTree))  -> insertR comp x t1
+    -- Split on left-and-right subtrees of t1.
+    (BinTree x l r, _) ->
+      link x
+           (hedgeUnion_UB    comp x      l t2)
+           (hedgeUnion_LB_UB comp x  hi  r t2)
+{-# INLINABLE hedgeUnion_UB #-}
+
+-- | Hedge union where we only add elements in second map if key is
+-- strictly between a lower and upper bound.
+hedgeUnion_LB_UB :: (IsBinTree c e) => (e -> e -> Ordering) -> e -> e -> c -> c -> c
+hedgeUnion_LB_UB comp lo hi t1 t2 =
+  case (asBin t1, asBin t2) of
+    (_, TipTree) -> t1
+    -- Prune left tree.
+    (_,   BinTree k _ r) | comp k lo <= EQ -> hedgeUnion_LB_UB comp lo hi t1 r
+    -- Prune right tree.
+    (_,   BinTree k l _) | comp k hi >= EQ -> hedgeUnion_LB_UB comp lo hi t1 l
+    -- When t1 becomes empty (assumes lo <= k <= hi)
+    (TipTree, BinTree x l r) ->
+      case (filterGt (comp lo) l, filterLt (comp hi) r) of
+        -- No variables in t2 were eliminated.
+        (NothingS, NothingS) -> t2
+        -- Relink t2 with filtered elements removed.
+        (l',r') -> link x (fromMaybeS l l') (fromMaybeS r r')
+    -- Special case when t2 is a single element.
+    (_, BinTree x (asBin -> TipTree) (asBin -> TipTree)) -> insertR comp x t1
+    -- Split on left-and-right subtrees of t1.
+    (BinTree x l r, _) ->
+      link x
+           (hedgeUnion_LB_UB comp lo x  l t2)
+           (hedgeUnion_LB_UB comp x  hi r t2)
+{-# INLINABLE hedgeUnion_LB_UB #-}
diff --git a/test/Test/Fin.hs b/test/Test/Fin.hs
--- a/test/Test/Fin.hs
+++ b/test/Test/Fin.hs
@@ -11,11 +11,12 @@
   )
 where
 
+import           Data.Hashable (hashWithSalt)
 import           Numeric.Natural (Natural)
 
 import           Hedgehog
 import qualified Hedgehog.Gen as HG
-import           Hedgehog.Range (linear)
+import           Hedgehog.Range (linear, linearBounded)
 import           Test.Tasty (TestTree, testGroup)
 import           Test.Tasty.Hedgehog (testPropertyNamed)
 import           Test.Tasty.HUnit (assertBool, testCase)
@@ -41,6 +42,14 @@
          Just LeqProof -> mkFin x
          Nothing -> error "Impossible"
 
+prop_eq_hash :: Property
+prop_eq_hash = property $
+  do salt <- forAll (HG.int linearBounded)
+     (f1, f2) <- forAll $
+                 HG.filter (\(f1, f2) -> f1 == f2) $
+                 (,) <$> genFin (knownNat @100) <*> genFin (knownNat @100)
+     hashWithSalt salt f1 === hashWithSalt salt f2
+
 prop_count_true :: Property
 prop_count_true = property $
   do Some n <- forAll (genNatRepr 100)
@@ -51,6 +60,117 @@
   do Some n <- forAll (genNatRepr 100)
      finToNat (countFin n (\_ _ -> False)) === 0
 
+prop_add_comm :: Property
+prop_add_comm = property $
+  do let n10 = knownNat @10
+     a <- forAll (genFin n10)
+     b <- forAll (genFin n10)
+     (a + b) === (b + a)
+
+prop_add_identity :: Property
+prop_add_identity = property $
+  do let n10 = knownNat @10
+     a <- forAll (genFin n10)
+     (mkFin (knownNat @0) + a) === a
+
+prop_add_inverse :: Property
+prop_add_inverse = property $
+  do let n10 = knownNat @10
+     a <- forAll (genFin n10)
+     (a + negate a) === mkFin (knownNat @0)
+
+prop_add_assoc :: Property
+prop_add_assoc = property $
+  do let n10 = knownNat @10
+     a <- forAll (genFin n10)
+     b <- forAll (genFin n10)
+     c <- forAll (genFin n10)
+     a + (b + c) === (a + b) + c
+
+prop_add_negate_sub :: Property
+prop_add_negate_sub = property $
+  do let n10 = knownNat @10
+     a <- forAll (genFin n10)
+     b <- forAll (genFin n10)
+     (a + negate b) === (a - b)
+
+prop_sub_anticomm :: Property
+prop_sub_anticomm = property $
+  do let n10 = knownNat @10
+     a <- forAll (genFin n10)
+     b <- forAll (genFin n10)
+     (a - b) === negate (b - a)
+
+prop_mul_comm :: Property
+prop_mul_comm = property $
+  do let n10 = knownNat @10
+     a <- forAll (genFin n10)
+     b <- forAll (genFin n10)
+     (a * b) === (b * a)
+
+prop_mul_identity :: Property
+prop_mul_identity = property $
+  do let n10 = knownNat @10
+     a <- forAll (genFin n10)
+     (mkFin (knownNat @1) * a) === a
+
+prop_mul_assoc :: Property
+prop_mul_assoc = property $
+  do let n10 = knownNat @10
+     a <- forAll (genFin n10)
+     b <- forAll (genFin n10)
+     c <- forAll (genFin n10)
+     a * (b * c) === (a * b) * c
+
+prop_mul_annihilate :: Property
+prop_mul_annihilate = property $
+  do let n10 = knownNat @10
+     a <- forAll (genFin n10)
+     (mkFin (knownNat @0) * a) === mkFin (knownNat @0)
+
+prop_neg_inv :: Property
+prop_neg_inv = property $
+  do let n10 = knownNat @10
+     a <- forAll (genFin n10)
+     negate (negate a) === a
+
+prop_abs_idem :: Property
+prop_abs_idem = property $
+  do let n10 = knownNat @10
+     a <- forAll (genFin n10)
+     abs (abs a) === abs a
+
+prop_signum_idem :: Property
+prop_signum_idem = property $
+  do let n10 = knownNat @10
+     a <- forAll (genFin n10)
+     signum (signum a) === signum a
+
+prop_abs_signum :: Property
+prop_abs_signum = property $
+  do let n10 = knownNat @10
+     a <- forAll (genFin n10)
+     (abs a * signum a) === a
+
+prop_recip_1 :: Property
+prop_recip_1 = property $
+  do let n1 = knownNat @1
+     a <- forAll (genFin n1)
+     recipFinModN n1 a === Just (mkFin (knownNat @0))
+
+prop_recip_10 :: Property
+prop_recip_10 = property $
+  do let n10 = knownNat @10
+     a <- forAll (genFin n10)
+     let aInv = recipFinModN n10 a
+     let d = gcd (finToNat a) (natValue n10)
+     case aInv of
+       Nothing ->
+         assert $ d >= 1
+       Just aInv' ->
+         do d === 1
+            (a * aInv') === mkFin (knownNat @1)
+
 finTests :: IO TestTree
 finTests =
   testGroup "Fin" <$>
@@ -63,9 +183,44 @@
           assertBool
             "minBound <= maxBound (2)"
             ((minBound :: Fin 2) <= (minBound :: Fin 2))
+      , testCase "show (minFin @1) == \"Fin 0\"" $
+          assertBool
+            "show (minFin @1) == \"Fin 0\""
+            (show (minFin @1) == "Fin 0")
+      , testCase "show (Just (minFin @1)) == \"Just (Fin 0)\"" $
+          assertBool
+            "show (Just (minFin @1)) == \"Just (Fin 0)\""
+            (show (Just (minFin @1)) == "Just (Fin 0)")
+      , testCase "fromInteger @(Fin 7) (-1) == fromInteger 6" $
+          assertBool
+            "fromInteger @(Fin 7) (-1) == fromInteger 6"
+            (fromInteger @(Fin 7) (-1) == fromInteger 6)
 
+      , testPropertyNamed
+          "Eq equality implies hash equality"
+          "prop_eq_hash"
+          prop_eq_hash
+
       , testPropertyNamed "count-true" "prop_count_true" prop_count_true
       , testPropertyNamed "count-false" "prop_count_false" prop_count_false
+
+      , testPropertyNamed "add-comm" "prop_add_comm" prop_add_comm
+      , testPropertyNamed "add-identity" "prop_add_identity" prop_add_identity
+      , testPropertyNamed "add-inverse" "prop_add_inverse" prop_add_inverse
+      , testPropertyNamed "add-assoc" "prop_add_assoc" prop_add_assoc
+      , testPropertyNamed "add-negate-sub" "prop_add_negate_sub" prop_add_negate_sub
+      , testPropertyNamed "sub-anticomm" "prop_sub_anticomm" prop_sub_anticomm
+      , testPropertyNamed "mul-comm" "prop_mul_comm" prop_mul_comm
+      , testPropertyNamed "mul-identity" "prop_mul_identity" prop_mul_identity
+      , testPropertyNamed "mul-annihilate" "prop_mul_annihilate" prop_mul_annihilate
+      , testPropertyNamed "mul-assoc" "prop_mul_assoc" prop_mul_assoc
+      , testPropertyNamed "neg-inv" "prop_neg_inv" prop_neg_inv
+      , testPropertyNamed "abs-idem" "prop_abs_idem" prop_abs_idem
+      , testPropertyNamed "signum-idem" "prop_signum_idem" prop_signum_idem
+      , testPropertyNamed "abs-signum" "prop_abs_signum" prop_abs_signum
+
+      , testPropertyNamed "recip-1" "prop_recip_1" prop_recip_1
+      , testPropertyNamed "recip-10" "prop_recip_10" prop_recip_10
 
 #if __GLASGOW_HASKELL__ >= 806
       , testCase "Eq-Fin-laws-1" $